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

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

Revision: 1622
          http://toss.svn.sourceforge.net/toss/?rev=1622&view=rev
Author:   lukaszkaiser
Date:     2011-11-06 22:11:48 +0000 (Sun, 06 Nov 2011)
Log Message:
-----------
Towards more general distinguishing of sets of structures: adding a module and starting guarded types work.

Modified Paths:
--------------
    trunk/Toss/Formula/Aux.ml
    trunk/Toss/Formula/Aux.mli
    trunk/Toss/Server/Tests.ml
    trunk/Toss/Solver/Makefile
    trunk/Toss/Solver/WL.ml

Added Paths:
-----------
    trunk/Toss/Solver/Distinguish.ml
    trunk/Toss/Solver/Distinguish.mli
    trunk/Toss/Solver/DistinguishTest.ml

Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml	2011-11-05 17:01:26 UTC (rev 1621)
+++ trunk/Toss/Formula/Aux.ml	2011-11-06 22:11:48 UTC (rev 1622)
@@ -361,9 +361,8 @@
     | _ -> acc in
   List.rev (aux n [] l)
 
-let rec range ?(from=1) k =
-  if from>=k then [k]
-  else from :: range ~from:(from+1) k 
+let rec range ?(from=0) k =
+  if from >= k then [] else from :: range ~from:(from+1) k 
 
 let array_map_some f a =
   let r = Array.map f a in

Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli	2011-11-05 17:01:26 UTC (rev 1621)
+++ trunk/Toss/Formula/Aux.mli	2011-11-06 22:11:48 UTC (rev 1622)
@@ -68,7 +68,7 @@
 val map_reduce :
   ('a -> 'b * 'c) -> ('d -> 'c -> 'd) -> 'd -> 'a list -> ('b * 'd) list
 
-(** Collects elements by key, in a list sorted by key. Same as
+(** Collects elements by key (returns a list sorted by key). Same as
     [map_reduce (fun x -> x) (fun y x->x::y) []]. *)
 val collect : ('a * 'b) list -> ('a * 'b list) list
 
@@ -217,7 +217,7 @@
     contain enough values. *)
 val take_n : int -> 'a list -> 'a list
 
-(** Returns an int list from from to k.*)
+(** Returns an int list from [from] (default 0) to k-1.*)
 val range: ?from : int -> int -> int list
 
 (** Make an array from an association from indices to values. The

Modified: trunk/Toss/Server/Tests.ml
===================================================================
--- trunk/Toss/Server/Tests.ml	2011-11-05 17:01:26 UTC (rev 1621)
+++ trunk/Toss/Server/Tests.ml	2011-11-06 22:11:48 UTC (rev 1622)
@@ -18,6 +18,7 @@
   "SolverTest",      [SolverTest.tests; SolverTest.bigtests];
   "ClassTest",       [ClassTest.tests; ClassTest.bigtests];
   "WLTest",          [WLTest.tests; WLTest.bigtests];
+  "DistinguishTest", [DistinguishTest.tests; DistinguishTest.bigtests];
 ]
 
 let arena_tests = "Arena", [

Added: trunk/Toss/Solver/Distinguish.ml
===================================================================
--- trunk/Toss/Solver/Distinguish.ml	                        (rev 0)
+++ trunk/Toss/Solver/Distinguish.ml	2011-11-06 22:11:48 UTC (rev 1622)
@@ -0,0 +1,180 @@
+open Formula
+
+let debug_level = ref 0
+let set_debug_level i = (debug_level := i)
+
+(* Helper functions to construct variables for indices. *)
+let varname i = "x" ^ string_of_int i
+let varnames k = List.map varname (Aux.range k)
+let var i = var_of_string (varname i)
+let fo_var i = fo_var_of_string (varname i)
+
+(* Helper function: check if a formula holds for a tuple on a structure. *)
+let check structure tuple formula = 
+  let eval structure phi assignment =
+    (Solver.M.evaluate_partial structure assignment phi) in
+  let elems = Assignments.set_to_set_list (Structure.elems structure) in
+  let vars =Array.map fo_var (Array.of_list (Aux.range (Array.length tuple))) in
+  let assignment = if tuple = [||] then AssignmentSet.Any else
+      Assignments.assignments_of_list elems vars [tuple] in
+  eval structure formula assignment <> AssignmentSet.Empty
+
+(* - Atoms - *)
+
+(* The list of literals which hold for a tuple on a structure. *)
+let atoms struc tuple =
+  let k = Array.length tuple in
+  let rec equalities = function
+    | [] -> []
+    | v :: vs -> (List.map (fun x -> Eq (`FO v,`FO x)) vs) @ (equalities vs) in
+  let atoms = FormulaOps.atoms (Structure.rel_signature struc) (varnames k) in
+  List.map (
+    fun atom -> if check struc tuple atom then atom else (Not atom)
+  ) (atoms @ (equalities (varnames k)))
+
+
+
+(* - Guards and Guarded Types - *)
+
+(* Generate all guarded substitutions of [tuple] with the guards.
+   A subst-tuple is a guarded substitution of [tuple] if a permuted
+   sub-tuple a of subst-tuple containig at least one element of
+   the original [tuple] is in some relation R in the structure [struc].
+   The guard for subst-tuple is then the atomic formula R(x_i1, ..., x_iK)
+   such that a = (subst-tuple_i1, ..., subst-tuple_iK) and R(a) holds.
+   For every subst-tuple as above we return the quintuple:
+   <new elems in subst-tuple, their indices as vars, subst-tuple, a, guard>. 
+   We do not generate subst-tuples with repeated new elements. *)
+let guards struc tuple =
+  let in_tuple e = Aux.array_mem e tuple in
+  let tuple = Array.to_list tuple in
+  let all_incident = List.concat (List.map (Structure.incident struc) tuple) in
+  let subst_tuples a = (* all subst-tuples for which [a] witnesses a guard *)
+    let new_in = 
+      Aux.unique_sorted (Aux.array_find_all (fun x -> not (in_tuple x)) a) in
+    let subst_tups = Aux.product (
+      List.map (fun e->if List.mem e new_in then new_in else e::new_in) tuple)in
+    let is_complete subst = 
+      List.for_all (fun e -> List.mem e subst) (Array.to_list a) in
+    let complete_new_once subst = is_complete subst && List.for_all (
+      fun n -> List.length (List.filter (fun x -> x = n) subst) = 1
+    ) new_in in
+    List.rev_map Array.of_list (List.filter complete_new_once subst_tups) in
+  let make_guard rel a stp =
+    let new_els = List.filter (fun x -> not (in_tuple x)) (Array.to_list stp) in
+    let sindex e = Aux.array_argfind (fun x -> x = e) stp in
+    let guard = Rel (rel, Array.map (fun e -> fo_var (sindex e)) a) in
+    let ret_els = Aux.unique_sorted new_els in
+    (ret_els, List.map (fun e -> var (sindex e)) ret_els, stp, a, guard) in
+  let make_guard rel a = List.rev_map (make_guard rel a) (subst_tuples a) in
+  let make_guard (rel, tps) = List.concat (List.rev_map (make_guard rel) tps) in
+  let guards = List.filter (fun (e,_,_,_,_) -> e <> []) 
+    (List.concat (List.rev_map make_guard all_incident)) in
+  Aux.unique_sorted guards
+
+(* Print a guard tuple, as returned above, to string. *)
+let guard_tuple_str (new_elems, vars, tup, a, atom) =
+  "< " ^ (String.concat ", " (List.map string_of_int new_elems)) ^ " | " ^
+    (String.concat ", " (List.map var_str vars)) ^ " | " ^
+    (String.concat ", " (List.map string_of_int (Array.to_list tup))) ^ " | " ^
+    (String.concat ", " (List.map string_of_int (Array.to_list a))) ^ " | " ^
+    (Formula.str atom) ^ " >"
+
+
+(* Guarded [qr]-type in [length of tuple]-variables of [tuple] in [struc]. *)
+let rec guarded_type struc qr tuple =
+  if qr = 0 then Formula.flatten_sort (And (atoms struc tuple)) else
+    let prevtp tup = guarded_type struc (qr-1) tup in
+    let conj_prev_ex vars guard subst_tuples =
+      And (List.map (fun tup -> Ex (vars, prevtp tup)) subst_tuples) in
+    let all_prev_disj vars guard subst_tuples =
+      All (vars, Or ((Not guard) :: (List.map prevtp subst_tuples))) in
+    let next_gtype ((vs, g), ts) = 
+      And [conj_prev_ex vs g ts; all_prev_disj vs g ts] in
+    let (guards, subst_tuples) = List.split (
+      List.rev_map (fun (_, vs, t, _, f) -> (vs,f), t) (guards struc tuple)) in
+    let (guards, subst_tuples) = 
+      (Aux.unique_sorted guards, Aux.unique_sorted subst_tuples) in
+    let guarded_tups (_, f) = 
+      List.filter (fun tup -> check struc tup f) subst_tuples in
+    let guards_with_tups = List.map (fun g -> (g, guarded_tups g)) guards in
+    let nextf = And (List.map next_gtype guards_with_tups) in
+    Formula.flatten_sort (And [guarded_type struc (qr-1) tuple; nextf])
+
+(* All guarded types of rank [qr] of guarded [k]-tuples in [struc]. *)
+let guarded_types struc ~qr ~k =
+  let tups = List.map (Structure.incident struc) (Structure.elements struc) in
+  let tups = List.concat (List.map snd (List.concat tups)) in
+  let tups = List.filter (fun tup -> Array.length tup >= k) tups in
+  let k_subtuples tup = 
+    List.map Array.of_list (Aux.all_ntuples (Array.to_list tup) k) in
+  let ktups = List.rev_map k_subtuples (Aux.unique_sorted tups) in
+  let ktups = Aux.unique_sorted (List.concat ktups) in
+  Aux.unique_sorted (List.rev_map (guarded_type struc qr) ktups)
+
+
+
+(* - Distinguishing Structure Sets - *)
+
+
+(* Helper function: remove atoms from a formula if [cond] is still satisfied.
+   Note that this is just a greedy heuristic, only And/Or and into Ex/All. *)
+let rec greedy_remove cond phi =
+  let rec greedy_remove_list constructor acc = function
+    | [] -> acc 
+    | x :: xs -> 
+      let rest = acc @ xs in
+      if cond (constructor rest) then greedy_remove_list constructor acc xs else
+	let minx = greedy_remove (fun y -> cond (constructor (y :: rest))) x in
+	greedy_remove_list constructor (minx::acc) xs in
+  match phi with
+    | And fl -> And (greedy_remove_list (fun l -> And l) [] (List.rev fl))
+    | Or fl -> Or (greedy_remove_list (fun l -> Or l) [] (List.rev fl))
+    | Not f -> Not (greedy_remove (fun x -> cond (Not x)) f)
+    | Ex (vs, f) -> Ex (vs, greedy_remove (fun x -> cond (Ex (vs, x))) f)
+    | All (vs, f) -> All (vs, greedy_remove (fun x -> cond (All (vs, x))) f)
+    | phi -> phi
+
+
+let distinguish_by_type ?(skip_outer_exists=false) ~qr ~k sPos sNeg=
+  let types s = guarded_types s ~qr ~k in
+  let (tpPos, tpNeg) = (List.map types sPos, List.map types sNeg) in
+  (*let all_diff vars = Aux.map_some (
+    function [x; y] -> if x < y then Some (Not (Eq (x, y))) else None| _ -> None
+  ) (Aux.all_ntuples (List.map to_fo vars) 2) in *)
+  let fails_neg f = (* check whether f fails on all negative structs *)
+    (* let f = And (f :: (all_diff (FormulaSubst.free_vars f))) in *)
+    not (List.exists (fun s -> check s [||] f) sNeg) in
+  let succ_pos fl = (* check whether disjunction of fl holds on all positives *)
+    (* let f = And ((Or fl):: (all_diff (FormulaSubst.free_vars (Or fl)))) in *)
+    List.for_all (fun s -> check s [||] (Or fl)) sPos in
+  let candidates = List.rev_append (List.concat tpPos) 
+    (List.map (fun f -> Not f) (List.concat tpNeg)) in
+  let fail_neg = List.filter fails_neg (Aux.unique_sorted candidates) in
+  let phis = List.sort Formula.compare (Aux.unique_sorted fail_neg) in
+  let rec find_type acc = function
+    | [] -> []
+    | x :: xs -> if succ_pos (x::acc) then x :: acc else 
+	find_type (x::acc) xs in
+  let dtypes = find_type [] phis in
+  if dtypes = [] then None else
+    let is_ok f = fails_neg f && succ_pos [f] in
+    let mintp = greedy_remove is_ok (Or dtypes) in
+    let fv = FormulaSubst.free_vars (Or dtypes) in
+    let t= FormulaOps.rename_quant_avoiding fv mintp in 
+    if skip_outer_exists then Some t else
+      Some (Ex (List.sort Formula.compare_vars fv, t))
+
+let distinguish ?(skip_outer_exists=false) strucs1 strucs2 = 
+  if !debug_level > 0 then
+    Printf.printf "distinguishing:\n\n%s\n\n and\n\n %s\n%!" 
+      (String.concat "\n" (List.map Structure.str strucs1))
+      (String.concat "\n" (List.map Structure.str strucs2));
+  let rec diff qr k =
+    if qr > k then diff 0 (k+1) else (
+      if !debug_level > 0 then Printf.printf "distinguish qr %i k %i\n%!" qr k;
+      match distinguish_by_type ~skip_outer_exists ~qr ~k strucs1 strucs2 with
+	| Some f -> f
+	| None -> diff (qr+1) k
+    ) in
+  diff 0 1

Added: trunk/Toss/Solver/Distinguish.mli
===================================================================
--- trunk/Toss/Solver/Distinguish.mli	                        (rev 0)
+++ trunk/Toss/Solver/Distinguish.mli	2011-11-06 22:11:48 UTC (rev 1622)
@@ -0,0 +1,48 @@
+(** Distinguish sets of structures by formulas. *)
+
+(** {2 Atoms} *)
+
+(** The list of literals which hold for a tuple on a structure,
+    i.e. the atomic type of this tuple. *)
+val atoms: Structure.structure -> int array -> Formula.formula list
+
+
+(** {2 Guards and Guarded Types} *)
+
+(** Generate all guarded substitutions of [tuple] with the guards.
+    A subst-tuple is a guarded substitution of [tuple] if a permuted
+    sub-tuple a of subst-tuple containig at least one element of
+    the original [tuple] is in some relation R in the structure [struc].
+    The guard for subst-tuple is then the atomic formula R(x_i1, ..., x_iK)
+    such that a = (subst-tuple_i1, ..., subst-tuple_iK) and R(a) holds.
+    For every subst-tuple as above we return the quintuple:
+    <new elems in subst-tuple, their indices as vars, subst-tuple, a, guard>. 
+    We do not generate subst-tuples with repeated new elements. *)
+val guards: Structure.structure -> int array -> 
+  (int list * Formula.var list * int array * int array * Formula.formula) list
+
+(** Print a guard tuple, as returned above, to string. *)
+val guard_tuple_str:
+  (int list * Formula.var list * int array * int array * Formula.formula) -> 
+  string
+
+(** Guarded [qr]-type in [length of tuple]-variables of [tuple] in [struc]. *)
+val guarded_type: Structure.structure -> int -> int array -> Formula.formula
+
+(** All guarded types of rank [qr] of guarded [k]-tuples in [struc]. *)
+val guarded_types: Structure.structure -> qr: int -> k:int -> 
+  Formula.formula list
+
+
+(** {2 Distinguishing Structure Sets} *)
+
+val distinguish_by_type: ?skip_outer_exists: bool -> qr: int -> k: int ->
+  Structure.structure list -> Structure.structure list -> Formula.formula option
+    
+val distinguish: ?skip_outer_exists: bool -> 
+  Structure.structure list -> Structure.structure list -> Formula.formula
+
+
+(** {2 Debugging} *)
+
+val set_debug_level: int -> unit

Added: trunk/Toss/Solver/DistinguishTest.ml
===================================================================
--- trunk/Toss/Solver/DistinguishTest.ml	                        (rev 0)
+++ trunk/Toss/Solver/DistinguishTest.ml	2011-11-06 22:11:48 UTC (rev 1622)
@@ -0,0 +1,280 @@
+open OUnit
+open Distinguish
+
+let formula_of_string s = 
+  FormulaParser.parse_formula Lexer.lex (Lexing.from_string s)
+
+let struc_of_string s = 
+  StructureParser.parse_structure Lexer.lex (Lexing.from_string s)
+
+let formula_eq ?(flatten_sort=true) phi1 phi2 =
+  if flatten_sort then 
+    assert_equal ~printer:(fun x -> Formula.sprint x)
+      (Formula.flatten_sort (formula_of_string phi1))
+      (Formula.flatten_sort phi2)
+  else
+    assert_equal ~printer:(fun x -> Formula.sprint x)
+      (formula_of_string phi1) phi2
+
+let guards_eq res guards =
+  let guards_str gl = String.concat "\n" (List.map guard_tuple_str gl) in
+  assert_equal ~printer:(fun s -> s) res (guards_str guards)
+
+let formula_list_eq ?(flatten_sort=true) l1 l2 =
+  if List.length l1 = List.length l2 then
+    List.iter2 (formula_eq ~flatten_sort) l1 l2
+  else 
+    let lstr l = "Length " ^ (string_of_int (List.length l)) ^ 
+      " [ " ^ (String.concat " | " l) ^ " ]" in
+    assert_equal ~printer:lstr l1 (List.map Formula.str l2)
+
+let formula_option_eq ?(flatten_sort=true) fopt1 fopt2 =
+  let fopt_str = function None -> "None" | Some f -> Formula.str f in
+  if fopt1 = "None" then 
+    assert_equal ~printer:fopt_str None fopt2 
+  else match fopt2 with
+    | None -> assert_equal ~printer:(fun x -> x) fopt1 "None"
+    | Some f -> formula_eq ~flatten_sort fopt1 f
+
+
+
+let tests = "Distinguish" >::: [
+  "atoms" >::
+    (fun () ->
+      let struc = struc_of_string "[ | R { (1, 2); (2, 3) } | ]" in
+      formula_eq
+        ("(not R(x0, x0) and R(x0, x1) and not R(x1, x0) " ^ 
+	    "and not R(x1, x1) and not x0=x1)")
+	(Formula.And (atoms struc [|2; 3|]));
+    );
+
+  "guards" >::
+    (fun () ->
+      let struc = struc_of_string "[ | R { (1, 2); (2, 3) } | ]" in
+      guards_eq "< 3 | x0 | 3, 2 | 2, 3 | R(x1, x0) >" (guards struc [|1; 2|]);
+      guards_eq ("< 2 | x0 | 2, 1 | 1, 2 | R(x1, x0) >\n" ^ 
+		    "< 2 | x1 | 1, 2 | 1, 2 | R(x0, x1) >")
+	(guards struc [|1; 1|]);
+      guards_eq ("< 1 | x0 | 1, 2 | 1, 2 | R(x0, x1) >\n" ^
+		    "< 1 | x1 | 2, 1 | 1, 2 | R(x1, x0) >\n" ^
+		    "< 3 | x0 | 3, 2 | 2, 3 | R(x1, x0) >\n" ^
+		    "< 3 | x1 | 2, 3 | 2, 3 | R(x0, x1) >")
+	(guards struc [|2; 2|]);
+      guards_eq ("< 2 | x0 | 2, 3 | 2, 3 | R(x0, x1) >\n" ^ 
+		    "< 2 | x1 | 1, 2 | 1, 2 | R(x0, x1) >")
+	(guards struc [|1; 3|]);
+      guards_eq ("< 2 | x0 | 2, 1 | 1, 2 | R(x1, x0) >\n" ^ 
+		    "< 2 | x1 | 3, 2 | 2, 3 | R(x1, x0) >")
+	(guards struc [|3; 1|]);
+      guards_eq "" (guards struc [|1|]);
+      guards_eq "" (guards struc [|2|]);
+      guards_eq "" (guards struc [|3|]);
+      guards_eq "" (guards struc [|1; 2; 3|]);
+
+      let struc = struc_of_string "[ | R { (1, 2); (2, 4) } | ]" in
+      guards_eq ("< 4 | x0 | 4, 2, 3 | 2, 4 | R(x1, x0) >\n" ^ 
+		    "< 4 | x2 | 1, 2, 4 | 2, 4 | R(x1, x2) >")
+	(guards struc [|1; 2; 3|]);
+
+      let struc = struc_of_string "[ | R { (1, 2, 2) } | ]" in
+      guards_eq ("< 2 | x0 | 2, 1 | 1, 2, 2 | R(x1, x0, x0) >\n" ^
+		    "< 2 | x1 | 1, 2 | 1, 2, 2 | R(x0, x1, x1) >")
+	(guards struc [|1; 1|]);
+
+      let struc = struc_of_string "[ | R { (1, 2, 3) } | ]" in
+      guards_eq "" (guards struc [|1; 1|]);
+      guards_eq "" (guards struc [|1; 2; 3|]);
+      guards_eq ("< 3 | x0 | 3, 1, 2 | 1, 2, 3 | R(x1, x2, x0) >\n" ^
+		    "< 3 | x1 | 1, 3, 2 | 1, 2, 3 | R(x0, x2, x1) >")
+	(guards struc [|1; 1; 2|]);
+      guards_eq ("< 2 | x0 | 2, 1, 3 | 1, 2, 3 | R(x1, x0, x2) >\n" ^
+		    "< 2 | x1 | 1, 2, 3 | 1, 2, 3 | R(x0, x1, x2) >")
+	(guards struc [|1; 1; 3|]);
+      guards_eq ("< 1 | x0 | 1, 2, 3 | 1, 2, 3 | R(x0, x1, x2) >\n" ^
+		    "< 1 | x2 | 3, 2, 1 | 1, 2, 3 | R(x2, x1, x0) >")
+	(guards struc [|3; 2; 3|]);
+      guards_eq ("< 1, 3 | x0, x1 | 1, 3, 2 | 1, 2, 3 | R(x0, x2, x1) >\n" ^
+		    "< 1, 3 | x0, x2 | 1, 2, 3 | 1, 2, 3 | R(x0, x1, x2) >\n" ^
+		    "< 1, 3 | x1, x0 | 3, 1, 2 | 1, 2, 3 | R(x1, x2, x0) >\n" ^
+		    "< 1, 3 | x1, x2 | 2, 1, 3 | 1, 2, 3 | R(x1, x0, x2) >\n" ^
+		    "< 1, 3 | x2, x0 | 3, 2, 1 | 1, 2, 3 | R(x2, x1, x0) >\n" ^
+		    "< 1, 3 | x2, x1 | 2, 3, 1 | 1, 2, 3 | R(x2, x0, x1) >")
+	(guards struc [|2; 2; 2|]);
+      
+      let struc = struc_of_string "[  |  |  ] \"
+	...   ...
+	...   P..
+	   ...   
+	   P..   
+	...   ...
+	...P  ...
+\"" in 
+      guards_eq ("< 3 | x0 | 3, 2 | 2, 3 | R(x1, x0) >\n" ^ 
+		    "< 4 | x1 | 1, 4 | 1, 4 | C(x0, x1) >\n" ^ 
+		    "< 5 | x0 | 5, 2 | 2, 5 | C(x1, x0) >") 
+	(guards struc [|1; 2|]);
+    );
+
+  "guarded_type" >::
+    (fun () ->
+      let struc = (struc_of_string "[ | R { (1, 2) } | ]") in
+      let lits = "R(x0,x1) and not R(x0,x0) and not x0=x1 and not R(x1,x0) " ^ 
+	"and not R(x1,x1)" in
+      formula_eq lits (guarded_type struc 0 [|1; 2|]);
+      formula_eq lits (guarded_type struc 1 [|1; 2|]); (* no guards *)
+      formula_eq lits (guarded_type struc 2 [|1; 2|]); (* no guards *)
+
+      let struc = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
+      formula_eq lits (guarded_type struc 0 [|1; 2|]);
+      formula_eq (lits ^ " and ex x0 (R(x1, x0) and not R(x0, x0) and " ^ 
+		    "not R(x0, x1) and not x0 = x1 and not R(x1, x1)) and " ^
+		    "all x0 (not R(x1, x0) or (not R(x0, x0) and not R(x0,x1)" ^
+		    " and not x0 = x1 and not R(x1, x1)))")
+	(guarded_type struc 1 [|1; 2|]);
+    );
+
+  "guarded_types" >::
+    (fun () ->
+      let struc = (struc_of_string "[ | R { (1, 2) } | ]") in
+      formula_list_eq [
+	("(R(x0, x1) and not R(x0, x0) and not x0 = x1 and " ^ 
+	    " not R(x1, x0) and not R(x1, x1))");
+	("(R(x1, x0) and not R(x0, x0) and not R(x0, x1) and " ^ 
+	    " not x0 = x1 and not R(x1, x1))");
+	("(x0 = x1 and not R(x0, x0) and not R(x0, x1) and " ^ 
+	    " not R(x1, x0) and not R(x1, x1))") ]
+        (Distinguish.guarded_types struc ~qr:0 ~k:2);
+      assert_equal ~printer:string_of_int 4
+	(List.length (Distinguish.guarded_types struc ~qr:1 ~k:2));
+
+      let struc = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
+      formula_list_eq [
+	("(R(x0, x1) and not R(x0, x0) and not x0 = x1 and " ^ 
+	    " not R(x1, x0) and not R(x1, x1))");
+	("(R(x1, x0) and not R(x0, x0) and not R(x0, x1) and " ^ 
+	    " not x0 = x1 and not R(x1, x1))");
+	("(x0 = x1 and not R(x0, x0) and not R(x0, x1) and " ^ 
+	    " not R(x1, x0) and not R(x1, x1))") ]
+        (Distinguish.guarded_types struc ~qr:0 ~k:2);
+      assert_equal ~printer:string_of_int 7
+	(List.length (Distinguish.guarded_types struc ~qr:1 ~k:2));
+    );
+
+  "distinguish_by_type" >::
+    (fun () ->
+      let struc1 = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
+      let struc2 = (struc_of_string "[ | R { (1, 2) } | ]") in
+      formula_option_eq "None" 
+	(Distinguish.distinguish_by_type ~qr:2 ~k:1 [struc1] [struc2]);
+      formula_option_eq "None" (* we use guarded types - so None here *)
+	(Distinguish.distinguish_by_type ~qr:0 ~k:2 [struc1] [struc2]);
+      formula_option_eq "None" (* we use guarded types - so None here *)
+	(Distinguish.distinguish_by_type ~qr:0 ~k:3 [struc1] [struc2]);
+      formula_option_eq "R(x0, x1) and ex x2 R(x1, x2)" 
+	(Distinguish.distinguish_by_type ~skip_outer_exists:true ~qr:1 ~k:2
+	   [struc1] [struc2]);
+
+      let struc1 = (struc_of_string "[ | P { (1) }; R:1 {} | ]") in
+      let struc2 = (struc_of_string "[ | P:1 {}; R { (1) } | ]") in
+      formula_option_eq "ex x0 P(x0)" 
+	(Distinguish.distinguish_by_type ~qr:0 ~k:1 [struc1] [struc2]);
+    );
+
+  "distinguish" >::
+    (fun () ->
+      let struc1 = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
+      let struc2 = (struc_of_string "[ | R { (1, 2) } | ]") in
+      formula_eq "ex x0, x1 (R(x0, x1) and ex x2 R(x1, x2))"
+	(Distinguish.distinguish [struc1] [struc2]);
+
+      let struc1 = (struc_of_string "[ | P { (1) }; R:1 {} | ]") in
+      let struc2 = (struc_of_string "[ | P:1 {}; R { (1) } | ]") in
+      formula_eq "ex x0 P(x0)" (Distinguish.distinguish [struc1] [struc2]);
+    );
+]
+
+let bigtests = "DistinguishBig" >::: [
+  "semi-tic-tac-toe" >::
+    (fun () ->
+      let strucN1 = struc_of_string "[  |  |  ] \"
+	...   ...
+	...   P..
+	   ...   
+	   P..   
+	...   ...
+	...P  ...
+\"" in
+      let strucN2 = struc_of_string "[  |  |  ] \"
+	...   ...
+	...P  ...
+	   ...   
+	   ...   
+	...   ...
+	...P  ...
+\"" in
+      let strucN3 = struc_of_string "[  |  |  ] \"
+	...   ...
+	...P  ...
+	   ...   
+	   P..   
+	...   ...
+	...   ...
+\"" in
+      let strucP = struc_of_string "[  |  |  ] \"
+	...   ...
+	...P  ...
+	   ...   
+	   P..   
+	...   ...
+	...P  ...
+\"" in (*"P(x2) and ex x3 (P(x3) and C(x2,x3)) and ex x3 (P(x3) and C(x3,x2))"*)
+      formula_eq 
+	("C(x0, x1) and ex x2 (P(x2) and R(x2, x0)) and " ^
+	    "ex x2 (P(x2) and R(x2, x1)) and ex x2 (C(x1, x2) and not P(x2))")
+	(Distinguish.distinguish ~skip_outer_exists:true 
+	   [strucP] [strucN1; strucN2; strucN3]);
+    );
+
+  "breakthrough" >::
+    (fun () ->
+      let struc1 = struc_of_string "[  |  |  ] \"
+	   ...   ...   ...   ...
+	   ...   W..   ...B  ...
+	...   ...   ...   ...   
+	...   ...   ...   B..   
+	   ...   ...   ...   ...
+	   ...   ...   ...   ...
+	...   ...   ...   ...   
+	...   ...   ...   ...   
+	   ...   ...   ...   ...
+	   ...   ...   ...   ...
+	...   ...   ...   ...   
+	...   ...   ...   ...   
+	   ...   ...   ...   ...
+	   ...   ...   ...   W..
+	...   ...   ...   ...   
+	...W  ...   ...   ...   
+\"" in
+      let struc2 = struc_of_string "[  |  |  ] \"
+	   ...   ...   ...   ...
+	   ...   ...   ...B  ...
+	...   ...   ...   ...   
+	...   ...W  ...   B..   
+	   ...   ...   ...   ...
+	   ...   ...   ...   ...
+	...   ...   ...   ...   
+	...   ...   ...   ...   
+	   ...   ...   ...   ...
+	   ...   ...   ...   ...
+	...   ...   ...   ...   
+	...   ...   ...   ...   
+	   ...   ...   ...   ...
+	   ...   ...   ...   W..
+	...   ...   ...   ...   
+	...W  ...   ...   ...   
+\"" in 
+      Distinguish.set_debug_level 1;
+      formula_eq "W(x2) and all x3 not C(x2, x3)"
+	(Distinguish.distinguish ~skip_outer_exists:true [struc1] [struc2]);
+    );
+]

Modified: trunk/Toss/Solver/Makefile
===================================================================
--- trunk/Toss/Solver/Makefile	2011-11-05 17:01:26 UTC (rev 1621)
+++ trunk/Toss/Solver/Makefile	2011-11-06 22:11:48 UTC (rev 1622)
@@ -10,6 +10,7 @@
 ClassTest:
 PresbTest:
 WLTest:
+DistinguishTest:
 
 tests:
 	make -C .. SolverTestsVerbose

Modified: trunk/Toss/Solver/WL.ml
===================================================================
--- trunk/Toss/Solver/WL.ml	2011-11-05 17:01:26 UTC (rev 1621)
+++ trunk/Toss/Solver/WL.ml	2011-11-06 22:11:48 UTC (rev 1622)
@@ -61,12 +61,13 @@
     if check structure tuple variables literal then literal else (Not literal)
   ) (List.append listOfLiterals (inequalities (Array.to_list variables)))
 
+let range k = Aux.range ~from:1 (k+1)
 
 (* The n-type from FO^k for the [tuple] in [structure]. *)
 let rec ntype structure tuple k_in n =
   let m = Array.length tuple in
   let k = max k_in m in
-  let variables = (List.map (fun i -> "x"^string_of_int(i)) (Aux.range k)) in
+  let variables = (List.map (fun i -> "x"^string_of_int(i)) (range k)) in
   if n=0 then 
     Formula.flatten_sort (And (atoms structure tuple (Array.of_list variables)))
   else
@@ -85,7 +86,7 @@
 	(conj_b_ex_xmplus1_typesN structure tuple k (n-1));
 	(all_xmplus1_disj_b_typesN structure tuple k (n-1))])
     else (* all variables already used, substitute *)
-      let indices = Aux.range k in
+      let indices = range k in
       let substituted i e = (Aux.array_replace tuple (i-1) e) in
       let conj_b_ex_xi_typesN_replace_ai_by_b structure tuple k n i =
 	And (List.map (fun x -> 
@@ -110,7 +111,7 @@
   match tuples with 
     | head::tail ->
       let ntyp = (ntype structure head k n) in
-      let vars = (List.map (fun i -> "x"^string_of_int i) (Aux.range k)) in
+      let vars = (List.map (fun i -> "x"^string_of_int i) (range k)) in
       let check tuple = check structure tuple (Array.of_list vars) ntyp in
       let filtered = List.filter (fun t -> not (check t)) tail in
       (all_ntypes_ktuples ~acc_types:(ntyp::acc_types)
@@ -133,7 +134,7 @@
 
 let nextTypes ?(min=true) structure tuples variables types =
   let conjuncts tuple = 
-    let indices = Aux.range (Array.length tuple) in
+    let indices = range (Array.length tuple) in
     let substituted i e = Aux.array_replace tuple (i-1) e in
     let sorted tp = Array.of_list (Aux.unique_sorted (Array.to_list tp)) in
     let all_diff i = Array.to_list (Aux.array_mapi_some (
@@ -184,7 +185,7 @@
     Array.of_list (List.map Array.of_list (List.filter no_rept (
       Aux.all_ntuples (Structure.elements structure) k))) in
   let variables = 
-    Array.map (fun i -> "x"^string_of_int(i)) (Array.of_list (Aux.range k)) in
+    Array.map (fun i -> "x"^string_of_int(i)) (Array.of_list (range k)) in
   ntypesSimplified ~min tuples variables structure n k
 
 (* Helper function: remove atoms from a formula if [cond] is still satisfied.

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