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

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

Revision: 1432
          http://toss.svn.sourceforge.net/toss/?rev=1432&view=rev
Author:   lukaszkaiser
Date:     2011-05-07 00:43:34 +0000 (Sat, 07 May 2011)

Log Message:
-----------
Fixed-points in Solver.

Modified Paths:
--------------
    trunk/Toss/Formula/FormulaOps.ml
    trunk/Toss/Formula/FormulaOpsTest.ml
    trunk/Toss/Solver/Assignments.ml
    trunk/Toss/Solver/Assignments.mli
    trunk/Toss/Solver/Solver.ml
    trunk/Toss/Solver/SolverTest.ml

Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml	2011-05-03 21:18:08 UTC (rev 1431)
+++ trunk/Toss/Formula/FormulaOps.ml	2011-05-07 00:43:34 UTC (rev 1432)
@@ -107,7 +107,8 @@
   | Lfp (r, xs, phi) | Gfp (r, xs, phi) ->
     let vs = (r :> var) :: ((Array.to_list xs) :> var list) in
     let fv_phi = free_vars_acc [] phi in
-    List.rev_append (List.filter (fun v -> not (List.mem v vs)) fv_phi) acc
+    List.rev_append ((Array.to_list xs) :> var list) (List.rev_append (
+      List.filter (fun v -> not (List.mem v vs)) fv_phi) acc)
 
 and free_vars_real = function
   | RVar s -> [s]
@@ -489,24 +490,22 @@
 	  let (new_bad, bad_subst) = newnames new_subst bad_vs in
 	  All (new_bad @ ok_vs, subst_vars (bad_subst @ new_subst) phi)
     | Lfp (v, vs, phi) ->
-      let ((bad_vs,ok_vs),new_subst) = 
-	splitvs subst ((v :> var) :: ((Array.to_list vs) :> var list)) in
-      if new_subst = [] then Lfp (v, vs, phi) else if bad_vs = [] then
-	  Lfp (v, vs, subst_vars new_subst phi) 
+      let subvs = Array.map (fo_var_subst subst) vs in
+      let ((bad_vs,ok_vs),new_subst) = splitvs subst [(v :> var)] in
+      if new_subst = [] then Lfp (v, subvs, phi) else if bad_vs = [] then
+	  Lfp (v, subvs, subst_vars new_subst phi) 
 	else
 	  let (_, bad_subst) = newnames new_subst bad_vs in
-	  let nvs = Array.map (fo_var_subst bad_subst) vs in
-	  Lfp (fp_var_subst bad_subst v, nvs,
+	  Lfp (fp_var_subst bad_subst v, subvs,
 	       subst_vars (bad_subst @ new_subst) phi)
     | Gfp (v, vs, phi) ->
-      let ((bad_vs,ok_vs),new_subst) = 
-	splitvs subst ((v :> var) :: ((Array.to_list vs) :> var list)) in
-      if new_subst = [] then Gfp (v, vs, phi) else if bad_vs = [] then
-	  Gfp (v, vs, subst_vars new_subst phi) 
+      let subvs = Array.map (fo_var_subst subst) vs in
+      let ((bad_vs,ok_vs),new_subst) = splitvs subst [(v :> var)] in
+      if new_subst = [] then Gfp (v, subvs, phi) else if bad_vs = [] then
+	  Gfp (v, subvs, subst_vars new_subst phi) 
 	else
 	  let (_, bad_subst) = newnames new_subst bad_vs in
-	  let nvs = Array.map (fo_var_subst bad_subst) vs in
-	  Gfp (fp_var_subst bad_subst v, nvs,
+	  Gfp (fp_var_subst bad_subst v, subvs,
 	       subst_vars (bad_subst @ new_subst) phi)
 
 and subst_vars_expr subst = function
@@ -1328,21 +1327,19 @@
       let nvs = okv @ (List.map var_of_string (snd (List.split subst))) in
       All (nvs, subst_vars subst (rename_quant_avoiding (avs @ nvs) phi))
   | Lfp (v, vs, phi) ->
-    let vars = (v :> var) :: ((Array.to_list vs) :> var list) in
+    let vars = [(v :> var)] in
     let (avoidv, okv) = List.partition (fun v -> List.mem v avs) vars in
     if avoidv=[] then Lfp (v, vs, rename_quant_avoiding (avs @ vars) phi) else
       let subst = List.map (subst_name_avoiding avs) avoidv in
-      let nvs, nv = Array.map (fo_var_subst subst) vs, fp_var_subst subst v in
-      let nvars = (nv :> var) :: ((Array.to_list nvs) :> var list) in
-      Lfp (nv, nvs, rename_quant_avoiding (avs @ nvars) phi)
+      let nv = fp_var_subst subst v in
+      Lfp (nv, vs, rename_quant_avoiding ((nv :> var) ::  avs) phi)
   | Gfp (v, vs, phi) ->
-    let vars = (v :> var) :: ((Array.to_list vs) :> var list) in
+    let vars = [(v :> var)] in
     let (avoidv, okv) = List.partition (fun v -> List.mem v avs) vars in
     if avoidv=[] then Gfp (v, vs, rename_quant_avoiding (avs @ vars) phi) else
       let subst = List.map (subst_name_avoiding avs) avoidv in
-      let nvs, nv = Array.map (fo_var_subst subst) vs, fp_var_subst subst v in
-      let nvars = (nv :> var) :: ((Array.to_list nvs) :> var list) in
-      Gfp (nv, nvs, rename_quant_avoiding (avs @ nvars) phi)
+      let nv = fp_var_subst subst v in
+      Gfp (nv, vs, rename_quant_avoiding ((nv :> var) ::  avs) phi)
 
 
 let rec has_mso = function

Modified: trunk/Toss/Formula/FormulaOpsTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaOpsTest.ml	2011-05-03 21:18:08 UTC (rev 1431)
+++ trunk/Toss/Formula/FormulaOpsTest.ml	2011-05-07 00:43:34 UTC (rev 1432)
@@ -57,6 +57,8 @@
 	    FormulaOps.free_vars (formula_of_string phi))) in
       fv_eq "not (P(x) and not Q(y))" "y, x";
       fv_eq "Q(x) or (ex x P(x))" "x";
+      fv_eq "P(x) or ex y (E(x, y) and y in T)" "x, T";
+      fv_eq "lfp T(x) = (P(x) or ex y (E(x, y) and y in T))" "x";
     );
 
    "cnf" >::
@@ -151,10 +153,10 @@
        subst_free_eq ~sub:[("x", "m"); ("m", "x")]
 	 "R(m) and ex m (S(m) or T(x))" "R(x) and (ex m0 (S(m0) or T(m)))";
        subst_free_eq "P(x) and lfp X(x) = (P(x) or ex y (E(x, y) and y in X))"
-	 "P(a) and lfp X(x) = (P(x) or ex y (E(x, y) and y in X))";
+	 "P(a) and lfp X(a) = (P(a) or ex y (E(a, y) and y in X))";
        subst_free_eq ~sub:[("x", "a"); ("y", "x"); ("Y", "X")]
 	 "x in Y and gfp X(x) = (x in Y or ex y (E(x, y) and y in X))"
-	 "a in X and gfp X0(x0) = (x0 in X or ex y (E(x0, y) and y in X0))";
+	 "a in X and gfp X0(a) = (a in X or ex y (E(a, y) and y in X0))";
      );
 
    "assign emptyset" >::

Modified: trunk/Toss/Solver/Assignments.ml
===================================================================
--- trunk/Toss/Solver/Assignments.ml	2011-05-03 21:18:08 UTC (rev 1431)
+++ trunk/Toss/Solver/Assignments.ml	2011-05-07 00:43:34 UTC (rev 1432)
@@ -45,11 +45,19 @@
 (* List a set or list ref; changes from set to list if required. *)
 let slist slr = 
   match !slr with 
-      List (i, l) -> l
+    | List (i, l) -> l
     | Set (i, s) ->
         if !debug_level>1 then print_endline "  converting set to list (slist)";
         let l = Elems.elements s in (slr := List (i, l); l)
 
+(* Set from a set or list ref; changes from list to set if required. *)
+let sset slr = 
+  match !slr with 
+    | Set (_, s) -> s
+    | List (_, l) ->
+      if !debug_level>1 then print_endline "  converting list to set (slist)";
+      List.fold_left (fun acc e -> Elems.add e acc) Elems.empty l
+
 let sllen slr = match !slr with List (i, _) -> i | Set (i, _) -> i
 
 

Modified: trunk/Toss/Solver/Assignments.mli
===================================================================
--- trunk/Toss/Solver/Assignments.mli	2011-05-03 21:18:08 UTC (rev 1431)
+++ trunk/Toss/Solver/Assignments.mli	2011-05-07 00:43:34 UTC (rev 1432)
@@ -22,6 +22,7 @@
 
 (** List a set or list ref; changes from set to list if required. *)
 val slist : set_list ref -> int list
+val sset  : set_list ref -> Structure.Elems.t
 val sllen : set_list ref -> int
 
 
@@ -99,7 +100,10 @@
 val join_rel : assignment_set -> Formula.fo_var array -> Structure.Tuples.t ->
   Structure.Tuples.t Structure.IntMap.t -> set_list ref -> assignment_set
 
+val full_join_rel : assignment_set -> Formula.fo_var array ->
+  Structure.Tuples.t -> set_list ref -> assignment_set
 
+
 (** {2 Debugging} *)
 
 

Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml	2011-05-03 21:18:08 UTC (rev 1431)
+++ trunk/Toss/Solver/Solver.ml	2011-05-07 00:43:34 UTC (rev 1432)
@@ -93,81 +93,110 @@
         | _ -> remove_dup_vars (v1::acc) (v2::vs)
 
 (* Calculate valuations which are both in [aset] and satisfy given formula. *)
-let rec eval model elems aset phi = 
+let rec eval fp model elems aset phi = 
   let report res =
     if !debug_level > 1 then print_endline ("Got: " ^ (AssignmentSet.str res));
     res in
   if !debug_level > 1 then print_endline ("Evaluating: " ^ (str phi)) else ();
+  let fp_split vl nasg =
+    let vlen, vs = Array.length vl, (Array.to_list vl :> var list) in
+    let avars = List.map to_fo (AssignmentSet.assigned_vars [] nasg) in
+    let ovars = List.filter (fun v -> not (List.mem (v :> var) vs)) avars in
+    let vars = vs @ (ovars :> var list) in
+    let tps = AssignmentSet.tuples (Assignments.sset elems)
+      (List.map var_str vars) nasg in
+    let split tp = 
+      if Array.length tp = vlen then (tp, [||]) else
+	Array.sub tp 0 vlen, Array.sub tp vlen ((Array.length tp) - vlen) in
+    let asplit tp =
+      let (vasg, rst) = split tp in
+      ((if rst = [||] then Any else
+          Assignments.assignments_of_list elems (Array.of_list ovars) [rst]),
+       vasg) in
+    Aux.collect (List.map asplit tps) in
+  let fp_next v vl psi nasg =
+    let nx (a, vsl) =
+      eval ((v, Structure.tuples_of_list vsl)::fp) model elems a psi in
+    List.fold_left (fun acc a -> Assignments.sum elems (nx a) acc)
+      Empty (fp_split vl nasg) in
+  let rec fixpnt v vl psi a =
+    let nxt = fp_next v vl psi a in
+    if nxt = a then nxt else fixpnt v vl psi nxt in
   if aset = Empty then Empty else
     match phi with
-        Rel (relname, vl) -> (* TODO: move to assignments, use incidence *)
-          let tuples_s =
-            try StringMap.find relname model.relations
-            with Not_found -> Tuples.empty in
-          let inc_map =
-            try StringMap.find relname model.incidence
-            with Not_found -> IntMap.empty in
-          report (join_rel aset vl tuples_s inc_map elems)
+      | Rel (relname, vl) ->
+        let tuples_s =
+          try StringMap.find relname model.relations
+          with Not_found -> Tuples.empty in
+        let inc_map =
+          try StringMap.find relname model.incidence
+          with Not_found -> IntMap.empty in
+        report (join_rel aset vl tuples_s inc_map elems)
       | Eq (x, y) -> report (equal_vars elems x y aset)
-      | In (x, y) ->
-          let sing_mso e = 
+      | SO (v, vl) ->
+	let tuples_s = List.assoc (v :> [ mso_var | so_var ]) fp in
+	report (full_join_rel aset vl tuples_s elems)
+      | In (x, y) -> (
+	try
+	  let tuples_s = List.assoc (y :> [ mso_var | so_var ]) fp in
+	  report (full_join_rel aset [|x|] tuples_s elems)
+        with Not_found ->
+	  let sing_mso e = 
             MSO (y, [((Elems.add e Elems.empty, Elems.empty), Any)]) in
           report (join aset (FO (x, List.map (fun e -> (e, sing_mso e)) 
-                                   (slist elems))))
+            (slist elems))))
+      )
       | Not (In (x, y)) ->
           let sing_non_mso e = 
             MSO (y, [((Elems.empty, Elems.add e Elems.empty), Any)]) in
           report (join aset (FO (x, List.map (fun e -> (e, sing_non_mso e))
                                    (slist elems))))
       | RealExpr (p, s) -> (* TODO: use aset directly as context for speed *)
-          report (join aset (assignment_of_real_expr model elems (p, s)))
+          report (join aset (assignment_of_real_expr fp model elems (p, s)))
       | Not phi -> 
           (*A intersect (complement B)=A intersect (complement(B intersect A))*)
-          report (complement_join elems aset (eval model elems aset phi))
+          report (complement_join elems aset (eval fp model elems aset phi))
       | And [] -> aset
-      | And [phi] -> report (eval model elems aset phi)
-      | And fl -> report (List.fold_left (eval model elems) aset fl)
-      | Or [phi] -> report (eval model elems aset phi)
+      | And [phi] -> report (eval fp model elems aset phi)
+      | And fl -> report (List.fold_left (eval fp model elems) aset fl)
+      | Or [phi] -> report (eval fp model elems aset phi)
       | Or fl -> 
 	let step_or (ast, asets) = function
 	  (* | Not psi -> 
-	    let nast = eval model elems ast psi in
+	    let nast = eval fp model elems ast psi in
 	    (nast, report (complement_join elems ast nast) :: asets) 
 	  | (In (x, y)) as psi -> 
-	    let nast = eval model elems ast (Not psi) in 
-	    (nast, report (eval model elems ast psi) :: asets) *)
-	  | psi -> (ast, report (eval model elems ast psi) :: asets) in
+	    let nast = eval fp model elems ast (Not psi) in 
+	    (nast, report (eval fp model elems ast psi) :: asets) *)
+	  | psi -> (ast, report (eval fp model elems ast psi) :: asets) in
         let (_, asets) = List.fold_left step_or (aset, []) fl in
         report (List.fold_left (sum elems) Empty asets)
       | Ex ([], phi) | All ([], phi) -> failwith "evaluating empty quantifier"
       | Ex (vl, phi) ->
 	check_timeout "Solver.eval.Ex";
 	let aset_vars = AssignmentSet.assigned_vars [] aset in
-	let in_aset = (* FIXME; TODO; same-name quantified vars?! (tnf_fv!) *)
-	  if List.exists (fun v -> List.mem v aset_vars) vl then 
-	    (*let asg_s = AssignmentSet.str aset in
-	    let form_s = Formula.str (Ex (vl, phi)) in
-	    let msg_s =
-              "solver: multiple vars?\n  "^ asg_s ^ "\n  "^ form_s in
-	    failwith msg_s *) Any
-	  else aset in
-        let phi_asgn = eval model elems in_aset phi in
+	let in_aset =
+	  if List.exists (fun v->List.mem v aset_vars) vl then Any else aset in
+        let phi_asgn = eval fp model elems in_aset phi in
         report (join aset (project_list elems phi_asgn vl))
       | All (vl, phi) ->
 	check_timeout "Solver.eval.All";
 	let aset_vars = AssignmentSet.assigned_vars [] aset in
-	let in_aset = (* FIXME; TODO; same-name quantified vars?! (tnf_fv!) *)
-	  if List.exists (fun v -> List.mem v aset_vars) vl then 
-	    (*let asg_s = AssignmentSet.str aset in
-	    let form_s = Formula.str (Ex (vl, phi)) in
-	    let msg_s =
-              "solver: multiple vars?\n  "^ asg_s ^ "\n  "^ form_s in
-	    failwith msg_s *) Any
-	  else aset in
-        let phi_asgn = eval model elems in_aset phi in
+	let in_aset =
+	  if List.exists (fun v->List.mem v aset_vars) vl then Any else aset in
+        let phi_asgn = eval fp model elems in_aset phi in
         report (join aset (universal_list elems phi_asgn vl))
+      | Lfp (v, vl, phi) ->
+	let a0 = eval ((v, Structure.Tuples.empty)::fp) model elems aset phi in
+	report (if a0 = Empty then Empty else fixpnt v vl phi a0)
+      | Gfp (v, vl, phi) -> 
+	let alltps = Structure.tuples_of_list
+	  (AssignmentSet.tuples (Assignments.sset elems)
+	     (List.map var_str ((Array.to_list vl) :> var list)) Any) in
+	let a0 = eval ((v, alltps)::fp) model elems aset phi in
+	report (if a0 = Empty then Empty else fixpnt v vl phi a0)
 
-and assignment_of_real_expr ?(check=true) model elems (p, sgn) =
+and assignment_of_real_expr fp ?(check=true) model elems (p, sgn) =
   let rec fo_vars_r_rec = function
       RVar s -> []
     | Const _ -> []
@@ -203,33 +232,33 @@
     | Char phi -> (
         let make_fo_asg asg (v, e) = FO (v, [(e, asg)]) in
         let fo_aset = List.fold_left make_fo_asg Any assgn in
-        match eval model elems fo_aset phi with
+        match eval fp model elems fo_aset phi with
             Empty -> Poly.Const (0.)
           | _ -> Poly.Const (1.)
       )
     | Sum (_, guard, r) -> (* FIXME; TODO; for many vars is that ok? *)
         let make_fo_asg asg (v, e) = FO (v, [(e, asg)]) in
         let fo_aset = List.fold_left make_fo_asg Any assgn in
-        let r_a = assignment_of_real_expr ~check:false model elems (r, sgn) in
-        let asg = join (eval model elems fo_aset guard) r_a in
+        let r_a = assignment_of_real_expr fp ~check:false model elems (r,sgn) in
+        let asg = join (eval fp model elems fo_aset guard) r_a in
         sum_polys asg (* Note: above "sgn" is irrelevant! *) in
   let rec process_vars assgn = function
-      [] -> 
-        let poly = poly_of assgn p in
-        if check then
-          if not (RealQuantElim.sat [(poly, sgn)]) then Empty else
-            if RealQuantElim.sat [(poly, SignTable.neg_sign_op sgn)] then
-              Real [[(poly, sgn)]]
-            else Any
-        else Real [[(poly, sgn)]]
+    | [] -> 
+      let poly = poly_of assgn p in
+      if check then
+        if not (RealQuantElim.sat [(poly, sgn)]) then Empty else
+          if RealQuantElim.sat [(poly, SignTable.neg_sign_op sgn)] then
+            Real [[(poly, sgn)]]
+          else Any
+      else Real [[(poly, sgn)]]
     | v :: vs -> 
-        let append_elem_asg acc e =
-          let asg = process_vars ((v, e)::assgn) vs in
-            if asg = Empty then acc else (e, asg) :: acc in
-        let asg_list = List.fold_left append_elem_asg [] (slist elems) in
-          if asg_list = [] then Empty else
-            FO (v, List.rev asg_list) in
-    process_vars [] (List.sort Formula.compare_vars (fo_vars_real p))
+      let append_elem_asg acc e =
+        let asg = process_vars ((v, e)::assgn) vs in
+        if asg = Empty then acc else (e, asg) :: acc in
+      let asg_list = List.fold_left append_elem_asg [] (slist elems) in
+      if asg_list = [] then Empty else
+        FO (v, List.rev asg_list) in
+  process_vars [] (List.sort Formula.compare_vars (fo_vars_real p))
 
 let eval_counter = ref 0
 
@@ -239,7 +268,7 @@
     ref (Set (Elems.cardinal struc.elements, struc.elements)) in
   let phi = Hashtbl.find solver.formulas_eval formula in
   incr eval_counter;
-  eval struc elems fo_aset phi
+  eval [] struc elems fo_aset phi
 
 (* Helper: find assoc and remove. *)
 let rec assoc_del (x : Formula.formula) = function
@@ -334,7 +363,7 @@
       if !debug_level > 0 then print_endline ("Eval_m " ^ (str phi));    
       let els = Set (Elems.cardinal struc.elements, struc.elements) in
       check_timeout "Solver.eval_m.not_found";
-      let asg = eval struc (ref els) Any phi in
+      let asg = eval [] struc (ref els) Any phi in
       incr eval_counter;
       Hashtbl.add !cache_results phi (asg, phi_rels phi);
       asg

Modified: trunk/Toss/Solver/SolverTest.ml
===================================================================
--- trunk/Toss/Solver/SolverTest.ml	2011-05-03 21:18:08 UTC (rev 1431)
+++ trunk/Toss/Solver/SolverTest.ml	2011-05-07 00:43:34 UTC (rev 1432)
@@ -1,46 +1,45 @@
-open Solver.M ;;
-open OUnit ;;
+open Solver.M
+open OUnit
 
-Solver.set_debug_level 0 ;;
-Sat.set_debug_level 0;;
-BoolFormula.set_debug_level 0;;
-FormulaOps.set_debug_level 0;;
+Solver.set_debug_level 0;
+Sat.set_debug_level 0;
+BoolFormula.set_debug_level 0;
+FormulaOps.set_debug_level 0
 
 let formula_of_string s = 
   FormulaParser.parse_formula Lexer.lex (Lexing.from_string s)
-;;
 
+
 let real_expr_of_string s = 
   FormulaParser.parse_real_expr Lexer.lex (Lexing.from_string s)
-;;
 
+
 let struc_of_string s = 
   StructureParser.parse_structure Lexer.lex (Lexing.from_string s)
-;;
 
+
 let eval_eq struc_s phi_s aset_s =
   let res = ref "" in
   backtrace (
     let (struc, phi) = (struc_of_string struc_s, formula_of_string phi_s) in
-    (* let solver = new_solver ()  in *)
     res := AssignmentSet.str (evaluate struc phi);
   );
   assert_equal ~printer:(fun x -> x) aset_s !res
-;;
 
+
 let eval_real_eq var_s struc_s expr_s aset_s =
   let (struc, expr) = (struc_of_string struc_s, real_expr_of_string expr_s) in
   assert_equal ~printer:(fun x -> x)
     aset_s (AssignmentSet.str (evaluate_real var_s expr struc))
-;;
 
+
 let real_val_eq struc_s expr_s x =
   let (struc, expr) = (struc_of_string struc_s, real_expr_of_string expr_s) in
   assert_equal ~printer:(fun x -> string_of_float x)
     x (get_real_val expr struc)
-;;
 
 
+
 let tests = "Solver" >::: [
   "eval: first-order quantifier free" >::
     (fun () ->
@@ -90,7 +89,8 @@
       eval_eq "[ | P { a } | ]" "(t in X2) and ((t in X) or ((t in C)))"
 	("{ t->1{ X2->(inc {1} excl {}){ X->(inc {} excl {}){ C->(inc {1}" ^
             " excl {}) }, X->(inc {1} excl {}) } }  }");
-      eval_eq "[ | P { a } | ]" "(t in X2) and ((t in X) or ((t in C) or (t in X)))"
+      eval_eq "[ | P { a } | ]"
+	"(t in X2) and ((t in X) or ((t in C) or (t in X)))"
 	("{ t->1{ X2->(inc {1} excl {}){ X->(inc {} excl {}){ C->(inc {1}" ^
 	    " excl {}) }, X->(inc {1} excl {}) } }  }");
       eval_eq "[ | P { a } | ]" 
@@ -132,6 +132,18 @@
 	    " x->5 } , y->8{ x->1, x->2, x->3, x->4, x->5, x->6 }  }");
     );
 
+  "eval: fixed-points" >::
+    (fun () ->
+      eval_eq "[ | P (a)  | ]" "lfp T(x) = P(x)" "{ x->1 }";
+      eval_eq "[ | P:1 {} | ]" "lfp T(x) = P(x)" "{}";
+      eval_eq "[ | R { (a, b); (b, c) } | ]"
+	"lfp T(x) = (x = y or ex z (z in T and R (x, z)))"
+	"{ y->1{ x->1 } , y->2{ x->1, x->2 } , y->3 }";
+      eval_eq "[ | R { (a, b); (b, a); (b, c) } | ]"
+	"gfp T(x) = (x != y and x in T and all z (R (x, z) -> z in T))"
+	"{ y->1{ x->3 } , y->2{ x->3 }  }";
+    );
+
   "eval: bigger tc tests" >::
     (fun () ->
       let diag_phi = 
@@ -256,19 +268,14 @@
       real_val_eq "[ | R { (a, a); (a, b) } | ] " 
 	"Sum (x, y | R (x, y) : 1)" 2.;
     );
+]
 
-] ;;
 
-let a =
-    match test_filter [""] tests with
-      | Some tests -> Aux.run_test_if_target "SolverTest" tests
-      | None -> ()
-;;
+let exec = Aux.run_test_if_target "SolverTest" tests
 
 
 
 
-
 (* ----------------------- FOUR POINTS PROBLEM --------------------------- *)
 
 (*
@@ -277,7 +284,7 @@
     (P(x) -> (x in X <-> (:px>:rl and :px<:rr and :py>:rb and :py<:rt))) and
     (Q(x) -> (x in X <-> (:qx>:rl and :qx<:rr and :qy>:rb and :qy<:rt))) and
     (Z(x) -> (x in X <-> (:zx>:rl and :zx<:rr and :zy>:rb and :zy<:rt))) and
-    (S(x) -> (x in X <-> (:sx>:rl and :sx<:rr and :sy>:rb and :sy<:rt))))" ;;
+    (S(x) -> (x in X <-> (:sx>:rl and :sx<:rr and :sy>:rb and :sy<:rt))))"
 *)
 
 
@@ -288,7 +295,7 @@
     not (a in C1 and b in C1 and c in C1 and d in C1) and
     not (a in C2 and b in C2 and c in C2 and d in C2) and
     not (a in C3 and b in C3 and c in C3 and d in C3) and
-    not (a in C4 and b in C4 and c in C4 and d in C4) ))" ;;
+    not (a in C4 and b in C4 and c in C4 and d in C4) ))"
 
 let rec linear_order name do_pref i =
   let elem j = 
@@ -307,6 +314,5 @@
   let cols = String.concat ", " (List.map col (upto n)) in
   let rows = String.concat ", " (List.map row (upto n)) in
     "[ | C { " ^ cols ^ " }; R { " ^ rows ^ " } | ]"
-;;
 
 (* test_eval (grid 2) four_color_f ;; *)


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