[Toss-devel-svn] SF.net SVN: toss:[1564] trunk/Toss

[<luk...@us...>]

Revision: 1564
          http://toss.svn.sourceforge.net/toss/?rev=1564&view=rev
Author:   lukstafi
Date:     2011-09-12 14:56:02 +0000 (Mon, 12 Sep 2011)
Log Message:
-----------
GDL translation: uses of counters in formulas specified and implemented; new ideas required for nice translation of pacman3p.gdl.

Modified Paths:
--------------
    trunk/Toss/GGP/GDL.ml
    trunk/Toss/GGP/GDL.mli
    trunk/Toss/GGP/GameSimpl.ml
    trunk/Toss/GGP/TranslateFormula.ml
    trunk/Toss/GGP/TranslateFormula.mli
    trunk/Toss/GGP/TranslateFormulaTest.ml
    trunk/Toss/GGP/TranslateGame.ml
    trunk/Toss/GGP/TranslateGameTest.ml
    trunk/Toss/www/reference/reference.tex

Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml	2011-09-11 18:47:06 UTC (rev 1563)
+++ trunk/Toss/GGP/GDL.ml	2011-09-12 14:56:02 UTC (rev 1564)
@@ -1675,7 +1675,9 @@
 let pred_on_path_subterm path subterm =
   path_str path ^ term_to_name subterm
 
+let counter_n = "gdl__counter"
 
+
 (* [expand_path_vars_by prepare_lits p ts clauses] expands subterms
    that have occurrences at path [p] in some state term of a clause
    (from which pre-processed literals are extracted by

Modified: trunk/Toss/GGP/GDL.mli
===================================================================
--- trunk/Toss/GGP/GDL.mli	2011-09-11 18:47:06 UTC (rev 1563)
+++ trunk/Toss/GGP/GDL.mli	2011-09-12 14:56:02 UTC (rev 1564)
@@ -151,6 +151,8 @@
 
 val blank : term
 
+val counter_n : string
+
 val term_str : term -> string
 val term_to_name : ?nested:bool -> term -> string
 

Modified: trunk/Toss/GGP/GameSimpl.ml
===================================================================
--- trunk/Toss/GGP/GameSimpl.ml	2011-09-11 18:47:06 UTC (rev 1563)
+++ trunk/Toss/GGP/GameSimpl.ml	2011-09-12 14:56:02 UTC (rev 1564)
@@ -124,9 +124,16 @@
     (for example with {!FormulaOps.simplify} or
     {!FormulaOps.remove_redundant} without the [implies] argument).
 
-    (5) TODO: Glue redundant rules (equal and having the same roles in
-    the game graph).
+    (5) TODO: Remove redundant existential quantifiers in formulas of
+    the form "ex x. x = v and ...".
 
+    (6) TODO: Remove redundant stable predicate literals, where the
+    literal is implied by its argument appearing as an argument to a
+    relation: when the relation projected on the argument is a subset
+    of the predicate (or outside the predicate for negative
+    literal). Compute the relation-argument-position, predicate
+    implications including relations produced by gluing.
+
 *)
 
 open Formula

Modified: trunk/Toss/GGP/TranslateFormula.ml
===================================================================
--- trunk/Toss/GGP/TranslateFormula.ml	2011-09-11 18:47:06 UTC (rev 1563)
+++ trunk/Toss/GGP/TranslateFormula.ml	2011-09-12 14:56:02 UTC (rev 1564)
@@ -15,23 +15,27 @@
 
 (* [separate_disj] is $\mathrm{TrDistr}$. Separate each disjunct,
    splitting disjuncts if necessary, into "positive state terms",
-   "negative state terms" and "reminder". *)
-let separate_disj disj =
-  (* FIXME see tests *)
+   "negative state terms" (excluding counters) and "reminder". *)
+let separate_disj counters disj =
+  let is_c = function
+    | Func (f, _) when List.mem f counters -> true | _ -> false in
   let aux conj =
     List.fold_right (fun lit acc -> match lit with
-      | (Pos (True _) | Neg (True _)) as lit ->
+      | (Pos (True t) | Neg (True t)) as lit when not (is_c t) ->
         List.map (fun conj -> Aux.Left lit::conj) acc
       | Disj ls as lit ->
-        if List.for_all (function Pos (True _) -> true | _ -> false) ls
-          || List.for_all (function Neg (True _) -> true | _ -> false) ls
+        if List.for_all
+          (function Pos (True t) when not (is_c t) -> true | _ -> false) ls
+          || List.for_all
+          (function Neg (True t) when not (is_c t) -> true | _ -> false) ls
         then
           List.map (fun conj -> Aux.Left lit::conj) acc
         else if List.exists
-            (function Pos (True _) | Neg (True _) -> true | _ -> false) ls
+            (function (Pos (True t) | Neg (True t))
+            when not (is_c t) -> true | _ -> false) ls
         then
           Aux.concat_map (function
-            | (Pos (True _) | Neg (True _)) as lit ->
+            | (Pos (True t) | Neg (True t)) as lit when not (is_c t) ->
               List.map (fun conj -> Aux.Left lit::conj) acc
             | lit -> List.map (fun conj -> Aux.Right lit::conj) acc
           ) ls
@@ -47,10 +51,12 @@
         | Pos _ as lit -> Aux.Left lit
         | Neg _ as lit -> Aux.Right lit
         | Disj ls as lit
-            when List.for_all (function Pos (True _) -> true | _ -> false) ls
+            when List.for_all
+              (function Pos (True t) when not (is_c t) -> true | _ -> false) ls
               -> Aux.Left lit
         | Disj ls as lit
-            when List.for_all (function Neg (True _) -> true | _ -> false) ls
+            when List.for_all
+              (function Neg (True t) when not (is_c t) -> true | _ -> false) ls
               -> Aux.Right lit
         | _ -> assert false
       ) state_terms in
@@ -63,6 +69,8 @@
   c_paths : path_set;                   (* coordinate paths *)
   all_paths : path_set;                 (* sum of f_paths and c_paths *)
   root_reps : term list;                (* coordinate root terms *)
+  counters : string list;
+  num_functions : (string * Formula.real_expr) list;
   defined_rels : string list;
   mutable defrel_argpaths : (string * defrel_argpaths) list;
   (* late binding to store $ArgMode# data *)
@@ -75,6 +83,8 @@
   c_paths = empty_path_set;
   all_paths = empty_path_set;
   root_reps = [];
+  num_functions = [];
+  counters = [];
   defined_rels = [];
   defrel_argpaths = [];
   term_arities = [];
@@ -118,7 +128,10 @@
   let defrel_phi = Formula.Rel (rel, vtup) in
   if sign then defrel_phi else Formula.Not defrel_phi
 
-let transl_rels data rels_phi sterms_all vterms_in =
+let minus a b = Formula.Plus (a, Formula.Times (Formula.Const (-1.), b))
+let counter_v = `FO counter_n
+
+let transl_rels data cv_map counter_vars rels_phi sterms_all vterms_in =
   (* coordinate subterms to locate paths on which to generate relations *)
   let s_subterms = Aux.concat_map
     (fun sterm ->
@@ -165,7 +178,46 @@
     then
       [translate_defrel data sterms_all sign rel args]
     else transl_rel sign rel args in
+  let transl_c = function
+    | Const v when
+        (try ignore (float_of_string v); true with _ -> false) ->
+      Formula.Const (float_of_string v)
+    | Var x when List.mem_assoc x cv_map ->
+      Formula.Fun (List.assoc x cv_map, counter_v)
+    | _ -> raise Not_found in
+  let transl_counter_term sign c t =
+    let sign_op =
+      if sign then Formula.EQZero else Formula.NEQZero in
+    let cc = Formula.Fun (c, counter_v) and ct = transl_c t in
+    if cc = ct then []
+    else [Formula.RealExpr (minus cc ct, sign_op)] in
+  let transl_numfun_rel sign rel t1 t2 =
+    let sign_op =
+      if sign then Formula.EQZero else Formula.NEQZero in
+    let f_result =
+      FormulaSubst.subst_real [":x", transl_c t1]
+        (List.assoc rel data.num_functions) in
+    [Formula.RealExpr
+        (minus f_result (transl_c t2), sign_op)] in    
   let rec aux = function
+    | Pos (True (Func (c, [|t|])))
+        when List.mem c data.counters &&
+          (try ignore (transl_c t); true with Not_found -> false) ->
+      transl_counter_term true c t
+    | Neg (True (Func (c, [|t|])))
+        when List.mem c data.counters &&
+          (try ignore (transl_c t); true with Not_found -> false) ->
+      transl_counter_term false c t
+    | Pos (Rel (rel, [|t1; t2|]))
+        when List.mem_assoc rel data.num_functions &&
+          (try ignore [transl_c t1; transl_c t2]; true
+           with Not_found -> false) ->
+      transl_numfun_rel true rel t1 t2
+    | Neg (Rel (rel, [|t1; t2|]))
+        when List.mem_assoc rel data.num_functions &&
+          (try ignore [transl_c t1; transl_c t2]; true
+           with Not_found -> false) ->
+      transl_numfun_rel false rel t1 t2
     | Pos (Rel (rel, args)) -> transl_posdefrel true rel args
     | Neg (Rel (rel, args)) -> transl_posdefrel false rel args
     | Pos (Does _ | Role _) | Neg (Does _ | Role _) ->
@@ -239,6 +291,15 @@
    $G_i$, [pos_state_phi] is $ST^{+}_i$, [neg_state_phi] is
    $ST^{-}_i$, [ext_phi] is $E$. *)
 let transl_disjunct data rels_phi pos_state_phi neg_state_phi ext_phi =
+  let is_c = function
+    | Func (f, _) when List.mem f data.counters -> true
+    | _ -> false in
+  let cv_map = Aux.map_some
+    (function
+      | Pos (True (Func (f, [|Var x|]))) when List.mem f data.counters ->
+        Some (x, f) | _ -> None) rels_phi in
+  let counter_vars =
+    terms_vars (Array.of_list (List.filter is_c (state_terms rels_phi))) in
   let pos_terms = state_terms pos_state_phi in
   let pos_vars = List.map (var_of_term data) pos_terms in
   let neg_terms = state_terms neg_state_phi in
@@ -255,7 +316,7 @@
      rels_phi @ pos_state_phi @ neg_state_phi) in
   let eqs = 
     List.map (fun v -> Pos (Rel ("EQ_", [|Var v; Var v|])))
-      (Aux.Strings.elements phi_vars) in
+      (Aux.Strings.elements (Aux.Strings.diff phi_vars counter_vars)) in
   let rels_eqs = rels_phi @ eqs in
   (* {{{ log entry *)
   if !debug_level > 2 then (
@@ -275,7 +336,7 @@
       neg_ext @
         [
           (* positive because they form a "premise" *)
-          transl_rels data rels_eqs all_terms neg_vars;
+          transl_rels data cv_map counter_vars rels_eqs all_terms neg_vars;
           (* the universal "conclusion" *)
           negated_neg_state_transl]) in
   let universal_part =
@@ -287,22 +348,29 @@
   let base_part =
     Formula.And (
       pos_ext @
-      [ transl_rels data rels_eqs pos_terms pos_vars;
+      [ transl_rels data cv_map counter_vars rels_eqs pos_terms pos_vars;
         transl_state data pos_state_phi] @
         universal_part) in
   if pos_vars = [] then base_part
   else Formula.Ex ((pos_vars :> Formula.var list), base_part)
 
-    
+let has_counter t =
+  FormulaMap.fold_formula
+    {FormulaMap.make_fold ( || ) false with
+      FormulaMap.fold_Fun = (fun _ v -> v = counter_v)} t
 
 (* Translate a disjunction of conjunctions of literals (and disjs of lits). *)
 let translate data disj =
-  let disj = separate_disj disj in
-  Formula.Or (List.map (fun (rels_phi, pos_state, neg_state) ->
-    transl_disjunct data rels_phi pos_state neg_state []
-  ) disj)
+  let disj = separate_disj data.counters disj in
+  let res = 
+    Formula.Or (List.map (fun (rels_phi, pos_state, neg_state) ->
+      transl_disjunct data rels_phi pos_state neg_state []
+    ) disj) in
+  if has_counter res
+  then Formula.Ex
+    ([counter_v], Formula.And [Formula.Rel (counter_n, [|counter_v|]); res])
+  else res
 
-
 (* **************************************** *)
 (* {3 Build and use defined relations.} *)
 

Modified: trunk/Toss/GGP/TranslateFormula.mli
===================================================================
--- trunk/Toss/GGP/TranslateFormula.mli	2011-09-11 18:47:06 UTC (rev 1563)
+++ trunk/Toss/GGP/TranslateFormula.mli	2011-09-12 14:56:02 UTC (rev 1564)
@@ -7,6 +7,8 @@
   c_paths : GDL.path_set;             (** coordinate paths *)
   all_paths : GDL.path_set;          (** sum of f_paths and c_paths *)
   root_reps : GDL.term list;         (** root terms *)
+  counters : string list;
+  num_functions : (string * Formula.real_expr) list;
   defined_rels : string list;
   mutable defrel_argpaths : (string * defrel_argpaths) list;
   (** late binding to store argument paths data *)
@@ -21,7 +23,7 @@
 
 (** Exposed for testing purposes only. *)
 val separate_disj :
-  GDL.literal list list ->
+  string list -> GDL.literal list list ->
   (GDL.literal list * GDL.literal list * GDL.literal list) list
 
 val translate :

Modified: trunk/Toss/GGP/TranslateFormulaTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateFormulaTest.ml	2011-09-11 18:47:06 UTC (rev 1563)
+++ trunk/Toss/GGP/TranslateFormulaTest.ml	2011-09-12 14:56:02 UTC (rev 1564)
@@ -65,6 +65,8 @@
     c_paths = c_paths;
     all_paths = all_paths;
     root_reps = root_reps;
+    counters = [];
+    num_functions = [];
     defined_rels = defined_rels;
     defrel_argpaths = [];
     term_arities = term_arities;
@@ -85,7 +87,7 @@
 
       let phi = "(or (col ?r) (row ?r) (diag1 ?r) (diag2 ?r))" in
       let conj = parse_literal_list phi in
-      let disj = separate_disj [conj] in
+      let disj = separate_disj [] [conj] in
       assert_equal ~msg:phi ~printer:(fun x->x)
         "(<= (rels#0 )
     (or (col ?r) (row ?r) (diag1 ?r) (diag2 ?r)))
@@ -98,7 +100,7 @@
 
       let phi = "(or (arel x) (true s1)) (brel y)" in
       let conj = parse_literal_list phi in
-      let disj = separate_disj [conj] in
+      let disj = separate_disj [] [conj] in
       assert_equal ~msg:phi ~printer:(fun x->x)
         "(<= (rels#0 )
     (arel x)
@@ -119,7 +121,7 @@
 
       let phi = "(or (arel x) (true s1)) (not (true s2))" in
       let conj = parse_literal_list phi in
-      let disj = separate_disj [conj] in
+      let disj = separate_disj [] [conj] in
       assert_equal ~msg:phi ~printer:(fun x->x)
         "(<= (rels#0 )
     (arel x))

Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml	2011-09-11 18:47:06 UTC (rev 1563)
+++ trunk/Toss/GGP/TranslateGame.ml	2011-09-12 14:56:02 UTC (rev 1564)
@@ -18,6 +18,19 @@
     occur in the structure)
 
     TODO: filter out legal tuples that are not statically satisfiable
+
+    TODO: after detecting that some state terms do not have any fluent
+    paths in them, eliminate these state terms by performing a GDL
+    source-level transformation into relations (i.e. erase the "init"
+    and "true" wrappers, and their "next" clauses, which are frame
+    clauses)
+    
+    TODO: perform the argument-path analysis for all GDL relations,
+    not only future defined relations; if fact-only GDL relations have
+    no conflicting paths (i.e. each argument is only used with a
+    specific path), translate them using the mechanism of defined
+    relations, but as stable (structure) relations, called
+    "materialized defined relations".
 *)
 
 open GDL
@@ -1325,8 +1338,6 @@
   else raise Not_turn_based
 
 
-let counter_n = "gdl__counter"
-
 let transl_update_path num_functions update =
   let comp_f acc = function
     | Pos (Rel (f, _)) when List.mem_assoc f num_functions ->
@@ -2048,6 +2059,8 @@
     c_paths = c_paths;
     all_paths = paths_union f_paths c_paths;
     root_reps = root_reps;
+    counters = counters;
+    num_functions = num_functions;
     defined_rels = defined_rels;
     defrel_argpaths = [];           (* built in TranslateFormula *)
     term_arities = term_arities;

Modified: trunk/Toss/GGP/TranslateGameTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateGameTest.ml	2011-09-11 18:47:06 UTC (rev 1563)
+++ trunk/Toss/GGP/TranslateGameTest.ml	2011-09-12 14:56:02 UTC (rev 1564)
@@ -307,18 +307,20 @@
 
 let a () =
   set_debug_level 4;
-       game_test_case ~game_name:"tictactoe" ~player:"xplayer"
+      game_test_case ~game_name:"breakthrough" ~player:"white"
         ~own_plnum:0 ~opponent_plnum:1
-        ~loc0_rule_name:"mark_x6_y_noop"
+        ~loc0_rule_name:"move_x2_y3_x3_y4_noop"
         ~loc0_emb:[
-          "cell_x6_y__BLANK_", "cell_2_2__BLANK_";
+          "cellholds_x2_y3__BLANK_", "cellholds_2_2__BLANK_";
+          "cellholds_x3_y4__BLANK_", "cellholds_1_3__BLANK_";
           "control__BLANK_", "control__BLANK_"]
-        ~loc0_move:"(mark 2 2)" ~loc0_noop:"noop"
-        ~loc1:1 ~loc1_rule_name:"noop_mark_x7_y0"
+        ~loc0_move:"(move 2 2 1 3)" ~loc0_noop:"noop" ~loc1:1
+        ~loc1_rule_name:"noop_move_x7_y9_x8_y10"
         ~loc1_emb:[
-          "cell_x7_y0__BLANK_", "cell_1_1__BLANK_";
+          "cellholds_x7_y9__BLANK_", "cellholds_7_7__BLANK_";
+          "cellholds_x8_y10__BLANK_", "cellholds_6_6__BLANK_";
           "control__BLANK_", "control__BLANK_"]
-        ~loc1_noop:"noop" ~loc1_move:"(mark 1 1)"
+        ~loc1_noop:"noop" ~loc1_move:"(move 7 7 6 6)"
 
 
 let a () =
@@ -360,7 +362,7 @@
   (* regenerate ~debug:true ~game_name:"pawn_whopping" ~player:"x"; *)
   (* regenerate ~debug:false ~game_name:"connect4" ~player:"white"; *)
   (* regenerate ~debug:false ~game_name:"2player_normal_form_2010" ~player:"row"; *)
-  regenerate ~debug:true ~game_name:"pacman3p" ~player:"pacman";
+  (* regenerate ~debug:true ~game_name:"pacman3p" ~player:"pacman"; *)
   (* failwith "generated"; *)
   ()
 

Modified: trunk/Toss/www/reference/reference.tex
===================================================================
--- trunk/Toss/www/reference/reference.tex	2011-09-11 18:47:06 UTC (rev 1563)
+++ trunk/Toss/www/reference/reference.tex	2011-09-12 14:56:02 UTC (rev 1564)
@@ -2036,22 +2036,45 @@
 composed of conjunctions, disjunctions and literals, into a
 disjunction $\mathrm{TrDistr}(\Phi) := \Phi_1 \vee \ldots \vee
 \Phi_n$, so that every $\Phi_i = G_i \wedge ST^{+}_i \wedge ST^{-}_i$,
-where all literals in $ST^{+}_i$ are positive \texttt{true} atoms and all
-literals in $ST^{-}_i$ are negated \texttt{true} atoms. (We
-avoid unnecessary expansions.) Let $\mathtt{ST}(\phi)$ be all the
-state terms, \ie arguments of \texttt{true} atoms, in $\phi$.
+where all literals in $ST^{+}_i$ are positive \texttt{true} atoms and
+all literals in $ST^{-}_i$ are negated \texttt{true} atoms, excluding
+application over counter terms (we avoid unnecessary expansions), note
+that \texttt{true} atoms over counter terms are left in $G_i$. Let
+$\mathtt{ST}(\phi)$ be all the state terms, \ie arguments of
+\texttt{true} atoms, in $\phi$, that are not counter
+terms, and let $\mathtt{CT}(\phi)$ be the counter term atoms respectively.
 
-$\TrRels(\phi, S_1, S_2)$ descends $\phi$ translating each literal as a
-conjunction of literals, for every combination of coordinate paths into $S_1$
-state terms, such that at least one of those terms is from $S_2$.
+For the purpose of translation involving counters, let $C^V_i$ be an
+assignment of counters (identified by their names) to GDL variables $x
+\ot c$ such that a positive atom $(\mathtt{true} \ (c \ x))$ occurs in
+$\Phi_i$. Also, let $CQ(\Psi)$ be $\exists v_C\big(\textmd{COUNTER}(v_C)
+\wedge \Psi \big)$ when $v_C \in \fv(\Psi)$, and $CQ(\Psi) = \Psi$
+otherwise, where $v_C$ is a distinguished variable for handling
+counters translation.
 
-$\TrST(\phi)$ translates \texttt{true} atoms as a conjunction of their
-coordinate and fluent predicates.
+$\TrRels(\phi, S_1, S_2)$ descends $\phi$ translating each literal not
+involving counters as a conjunction of literals, for every combination
+of coordinate paths into $S_1$ state terms, such that at least one of
+those terms is from $S_2$.
 
+When $\TrRels$ encounters a \texttt{true} atom over counter $c$, it
+builds an equation between $c(v_C)$ and the argument of $c$ in the
+atom when it is a constant, or in case $c$ is applied to a variable
+$x$, the value $c'(v_C)$ for $c' = C^V_i(x)$. If $\TrRels$ encounters
+a numeric function applied to either constants or variables in the
+domain of $C^V_i$, it applies the function to the right argument when
+building a similar equation. The translation will currently fail if
+relations other than numeric functions are applied to variables that
+also occur in counter terms: general case left as future work.
+
+$\TrST(\phi)$ translates \texttt{true} atoms which are not counters as
+a conjunction of their coordinate and fluent predicates.
+
 Let $eqs_i$ be $\Land \big\{ \mathtt{EQ}(x,x) | x \in \fv(\Phi_i)
-\big\}$. The relation name $\mathtt{EQ}$ serves technical purposes:
-fact relations $\mathtt{EQ}_{p,q}$ are identified with subterm
-equality relations $Eq_{p,q}$.
+\setminus \fv(\mathtt{CT}(\Phi_i)) \big\}$. The relation name
+$\mathtt{EQ}$ serves technical purposes: fact relations
+$\mathtt{EQ}_{p,q}$ are identified with subterm equality relations
+$Eq_{p,q}$.
 
 The result of translation is the disjunction of translations of each
 $\Phi_i$. Let $\mathtt{BL}(t)=t\big[\calP_f \ot \mathtt{BLANK}\big]$. A single $\Phi_i = G_i \wedge ST^{+}_i \wedge ST^{-}_i$
@@ -2071,13 +2094,13 @@
 V^{-} & := \big( \mathtt{BL}(\mathtt{ST}(ST^{-}_i)) \setminus V^{+} \big)
 \end{align*}
 
-The result of translation is $\mathrm{Tr}(\Phi) := \mathrm{Tr}(\Phi_1)
-\vee \ldots \vee \mathrm{Tr}(\Phi_n)$. Note how variables with both
-positive and negative instantiating state terms are excluded from
-universal treatment; in particular, the variables corresponding to
-Toss rewrite rule structure elements will not be quantified
-universally, thanks to adding their ``blank representants'' to the
-rule condition.
+The result of translation is $\mathrm{Tr}(\Phi) := CQ \big(
+\mathrm{Tr}(\Phi_1) \vee \ldots \vee \mathrm{Tr}(\Phi_n) \big)$. Note how
+variables with both positive and negative instantiating state terms
+are excluded from universal treatment; in particular, the variables
+corresponding to Toss rewrite rule structure elements will not be
+quantified universally, thanks to adding their ``blank representants''
+to the rule condition.
 
 We now proceed to define $\TrRels$ and $\TrST$. For an atom $r$, let
 $\pm r$ mean either $r$ or $\neg r$ when on the left-hand-side, and
@@ -2097,20 +2120,30 @@
   & p_1, \ldots, p_n \in \calP_c \wedge
   s_1 \tpos_{p_1} = t_1 \wedge \ldots \wedge s_n \tpos_{p_n} = t_n \big\} \\
   & \textit{(when $R$ is not translated as defined relation)} \\
+  \TrRels (\pm \mathtt{true}(c(t))) =
+  & \pm \big(c(v_C)-\mathtt{TrC}(t) = 0 \big) \\
+  \TrRels (\pm R(t_1,t_2)) = &
+  \pm \big(\big(\mathtt{NumF}(R)\big) (\mathtt{TrC}(t_1))
+  - \mathtt{TrC}(t_2) = 0 \big) \\
+  & \textit{(when $R$ can be translated as a numeric function
+    $\mathtt{NumF}(R)$} \\
+  & \textit{and both $t_1$ and $t_2$ are in the domain of $\mathtt{TrC}$)} \\
+  \mathtt{TrC}(n) = & n \ \ \textit{(when $n$ is a constant)} \\
+  \mathtt{TrC}(x) = & \big(C^V_i(x)\big)(v_C) \ \
+  \textit{(when $x$ is a variable in the domain of $C^V_i$)} \\
   \TrST (\phi_1 \wedge \phi_2) = &
   \TrST (\phi_1) \wedge \TrST(\phi_2) \\
   \TrST (\phi_1 \vee \phi_2) = &
   \TrST (\phi_1) \vee \TrST(\phi_2) \\
-  \TrST (\mathtt{true}(t)) = & \Land \big\{
-  Coord^s_p(v) \; \big| \; v = \mathtt{BL}(t) \wedge 
-  p \in \calP_c \wedge t \tpos_p = s \wedge s \neq \mathtt{BLANK}
+  \TrST (\mathtt{true}(t)) = & \Land \big\{ Coord^s_p(v) \; \big| \; v
+  = \mathtt{BL}(t) \wedge p \in \calP_c \wedge t \tpos_p = s \wedge s
+  \neq \mathtt{BLANK}
   \big\} \wedge \\
-  & \Land \big\{
-  Flu^s_p(v) \; \big| \; v = \mathtt{BL}(t) \wedge 
-  p \in \calP_f \wedge t \tpos_p = s \wedge s \neq \mathtt{BLANK}
+  & \Land \big\{ Flu^s_p(v) \; \big| \; v = \mathtt{BL}(t) \wedge p
+  \in \calP_f \wedge t \tpos_p = s \wedge s \neq \mathtt{BLANK}
   \big\} \wedge \\
-  & \Land \big\{
-  Root_m(v) \; \big| \; v = \mathtt{BL}(t) \wedge t \in m \big\}
+  & \Land \big\{ Root_m(v) \; \big| \; v = \mathtt{BL}(t) \wedge t \in
+  m \big\}
 \end{align*}
 
 The case of $\TrRels$ for relations intended to be translated as

This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.