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

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

Revision: 1633
          http://toss.svn.sourceforge.net/toss/?rev=1633&view=rev
Author:   lukaszkaiser
Date:     2011-11-16 21:58:12 +0000 (Wed, 16 Nov 2011)
Log Message:
-----------
Better ordering in distinguish_by_type, gives more readable formulas.

Modified Paths:
--------------
    trunk/Toss/Formula/Formula.ml
    trunk/Toss/Formula/Formula.mli
    trunk/Toss/Formula/FormulaTest.ml
    trunk/Toss/Server/Makefile
    trunk/Toss/Solver/Distinguish.ml
    trunk/Toss/Solver/DistinguishTest.ml

Modified: trunk/Toss/Formula/Formula.ml
===================================================================
--- trunk/Toss/Formula/Formula.ml	2011-11-14 15:49:50 UTC (rev 1632)
+++ trunk/Toss/Formula/Formula.ml	2011-11-16 21:58:12 UTC (rev 1633)
@@ -129,10 +129,14 @@
 
 
 let is_atom = function
-  | Rel _ | Eq _ | In _ | SO _ | RealExpr _ -> true
+  | Rel _ | Eq _ | In _ | SO _ -> true
   | _ -> false
 
+let rec is_literal = function
+  | Not f -> is_literal f
+  | f -> is_atom f
 
+
 (* Helper power function, used in parser. *)
 let rec pow p n = 
   if n = 0 then Const 1. else if n = 1 then p else Times (p, pow p (n-1))

Modified: trunk/Toss/Formula/Formula.mli
===================================================================
--- trunk/Toss/Formula/Formula.mli	2011-11-14 15:49:50 UTC (rev 1632)
+++ trunk/Toss/Formula/Formula.mli	2011-11-16 21:58:12 UTC (rev 1633)
@@ -81,6 +81,7 @@
 val compare : formula -> formula -> int
 
 val is_atom : formula -> bool
+val is_literal : formula -> bool
 
 (** Equation system: a left-hand-side [f,a] actually represents
     [Fun (f, `FO a)] *)

Modified: trunk/Toss/Formula/FormulaTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaTest.ml	2011-11-14 15:49:50 UTC (rev 1632)
+++ trunk/Toss/Formula/FormulaTest.ml	2011-11-16 21:58:12 UTC (rev 1633)
@@ -14,6 +14,16 @@
 	(And [rel "P" 1; rel "Q" 1; rel "S" 1]);
     );
 
+  "size, compare" >::
+    (fun () ->
+      assert_equal ~printer:(fun x -> string_of_int x) 5
+	(size (And [rel "P" 1; rel "Q" 1; Not (rel "R" 2)]));
+
+      assert_equal ~printer:(fun x -> string_of_int x) 1
+	(compare (And [rel "P" 1; Not (rel "Q" 1); Not (rel "R" 2)])
+	   (And [rel "P" 1; rel "Q" 1; Not (rel "R" 2)]));
+    );
+
   "syntax check" >::
     (fun () ->
       assert_equal ~printer:string_of_bool true

Modified: trunk/Toss/Server/Makefile
===================================================================
--- trunk/Toss/Server/Makefile	2011-11-14 15:49:50 UTC (rev 1632)
+++ trunk/Toss/Server/Makefile	2011-11-16 21:58:12 UTC (rev 1633)
@@ -5,6 +5,7 @@
 
 PictureTest:
 ReqHandlerTest:
+LearnGameTest:
 
 tests:
 	make -C .. ServerTestsVerbose

Modified: trunk/Toss/Solver/Distinguish.ml
===================================================================
--- trunk/Toss/Solver/Distinguish.ml	2011-11-14 15:49:50 UTC (rev 1632)
+++ trunk/Toss/Solver/Distinguish.ml	2011-11-16 21:58:12 UTC (rev 1633)
@@ -37,24 +37,40 @@
   ) (atoms @ (equalities (varnames k)))
 
 
+(* The [qr]-type in [length of tuple]-variables of [tuple] in [struc].
+   In [mem] we memorize the results for [qr] and [tuple], but *not* [struc]. *)
+let rec ntype_memo struc mem qr tuple =
+  try Hashtbl.find mem (qr, tuple) with Not_found ->
+    if qr = 0 then (
+      let res = Formula.flatten_sort (And (atoms struc tuple)) in
+      Hashtbl.add mem (qr, tuple) res;
+      res
+    ) else (
+      let prevtp i e = 
+	ntype_memo struc mem (qr-1) (Aux.array_replace tuple i e) in
+      let elems = Structure.elements struc in
+      let conj_prev_ex i =
+	And (List.map (fun e -> Ex ([var i], prevtp i e)) elems) in
+      let all_prev_disj i =
+	All ([var i], Or (List.map (prevtp i) elems)) in
+      let next_ntype i = And [conj_prev_ex i; all_prev_disj i] in
+      let nexttp = And (List.map next_ntype (Aux.range (Array.length tuple))) in
+      let res = Formula.flatten_sort (
+	And [ntype_memo struc mem (qr-1) tuple; nexttp]) in
+      Hashtbl.add mem (qr, tuple) res;
+      res
+    )
+
 (* The [qr]-type in [length of tuple]-variables of [tuple] in [struc]. *)
-let rec ntype struc qr tuple =
-  if qr = 0 then Formula.flatten_sort (And (atoms struc tuple)) else
-    let prevtp i e = ntype struc (qr-1) (Aux.array_replace tuple i e) in
-    let elems = Structure.elements struc in
-    let conj_prev_ex i =
-      And (List.map (fun e -> Ex ([var i], prevtp i e)) elems) in
-    let all_prev_disj i =
-      All ([var i], Or (List.map (prevtp i) elems)) in
-    let next_ntype i = And [conj_prev_ex i; all_prev_disj i] in
-    let nexttp = And (List.map next_ntype (Aux.range (Array.length tuple))) in
-    Formula.flatten_sort (And [ntype struc (qr-1) tuple; nexttp])
+let ntype struc qr tuple = ntype_memo struc (Hashtbl.create 7) qr tuple
 
+
 (* All types of rank [qr] of all [k]-tuples in [struc]. *)
 let ntypes struc ~qr ~k =
   let elems = Structure.elements struc in
   let tups = List.map Array.of_list (Aux.all_ntuples elems k) in
-  Aux.unique_sorted (List.rev_map (ntype struc qr) tups)
+  let mem = Hashtbl.create 63 in
+  Aux.unique_sorted (List.rev_map (ntype_memo struc mem qr) tups)
 
 
 (* - Guards and Guarded Types - *)
@@ -104,39 +120,57 @@
     (Formula.str atom) ^ " >"
 
 
+(* Guarded [qr]-type in [length of tuple]-variables of [tuple] in [struc]. 
+   In [mem] we memorize the results for [qr] and [tuple], but *not* [struc]. *)
+let rec guarded_type_memo struc mem qr tuple =
+  try Hashtbl.find mem (qr, tuple) with Not_found ->
+    if qr = 0 then (
+      let res = Formula.flatten_sort (And (atoms struc tuple)) in
+      Hashtbl.add mem (qr, tuple) res;
+      res
+    ) else (
+      let prevtp tup = guarded_type_memo struc mem (qr-1) tup in
+      let conj_prev_ex vars guard subst_tuples =
+	let subst_tuples = List.filter (fun tup -> tup <> tuple) subst_tuples in
+	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 subst_tuples = 
+	List.rev_map (fun (_,vs,t,_,_) -> (vs, t)) (guards struc tuple) in
+      let subst_tuples = Aux.unique_sorted (([], tuple) :: subst_tuples) in
+      let all_vars = varnames (Array.length tuple) in
+      let at_most_vs_tuples vs = List.concat (List.map (
+	fun vs -> Aux.assoc_all vs subst_tuples) (Aux.all_subsets vs)) in
+      let tuples_by_vs = List.map (fun vs -> (vs, at_most_vs_tuples vs))
+	(Aux.all_subsets (List.map var_of_string all_vars)) in
+      let all_guards =
+	FormulaOps.atoms (Structure.rel_signature struc) all_vars in
+      let guards_to_tups (vs, tuples) =
+	let has_vs a = List.for_all (fun v -> Aux.array_mem (to_fo v) a) vs in
+	let is_vs_guard a = has_vs a && 
+	  Aux.array_existsi (fun _ v -> not (List.mem (v :> var) vs)) a in
+	let is_vs_guard = function Rel (_, a) -> is_vs_guard a | _ -> false in
+	let vs_guards = List.filter is_vs_guard all_guards in
+	let guarded_tups g = List.filter (fun tup-> check struc tup g) tuples in
+	(vs, List.map (fun g -> (g, guarded_tups g)) vs_guards) in
+      let tups_with_guards = List.map guards_to_tups tuples_by_vs in
+      let tups_with_guards = 
+	List.filter (fun (vs,_) -> vs <> []) tups_with_guards in
+      let next_gtype_vs (vs, gtups) = And (List.map (next_gtype vs) gtups) in
+      let nextf = And (List.map next_gtype_vs tups_with_guards) in
+      let res = Formula.flatten_sort (
+	And [guarded_type_memo struc mem (qr-1) tuple; nextf]) in
+      Hashtbl.add mem (qr, tuple) res;
+      res
+    )
+
 (* 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 =
-      let subst_tuples = List.filter (fun tup -> tup <> tuple) subst_tuples in
-      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 subst_tuples = Aux.unique_sorted (([], tuple) ::
-      List.rev_map (fun (_,vs,t,_,_) -> (vs, t)) (guards struc tuple)) in
-    let all_vars = varnames (Array.length tuple) in
-    let at_most_vs_tuples vs = List.concat (List.map (
-      fun vs -> Aux.assoc_all vs subst_tuples) (Aux.all_subsets vs)) in
-    let tuples_by_vs = List.map (fun vs -> (vs, at_most_vs_tuples vs))
-      (Aux.all_subsets (List.map var_of_string all_vars)) in
-    let all_guards= FormulaOps.atoms (Structure.rel_signature struc) all_vars in
-    let guards_to_tups (vs, tuples) =
-      let has_vs a = List.for_all (fun v -> Aux.array_mem (to_fo v) a) vs in
-      let is_vs_guard a = has_vs a && 
-	Aux.array_existsi (fun _ v -> not (List.mem (v :> var) vs)) a in
-      let is_vs_guard = function Rel (_, a) -> is_vs_guard a | _ -> false in
-      let vs_guards = List.filter is_vs_guard all_guards in
-      let guarded_tups g = List.filter (fun tup -> check struc tup g) tuples in
-      (vs, List.map (fun g -> (g, guarded_tups g)) vs_guards) in
-    let tups_with_guards = List.map guards_to_tups tuples_by_vs in
-    let tups_with_guards = List.filter (fun (vs,_)-> vs<>[]) tups_with_guards in
-    let next_gtype_vs (vs, gtups) = And (List.map (next_gtype vs) gtups) in
-    let nextf = And (List.map next_gtype_vs tups_with_guards) in
-    Formula.flatten_sort (And [guarded_type struc (qr-1) tuple; nextf])
+let guarded_type struc qr tuple = 
+  guarded_type_memo struc (Hashtbl.create 7) qr tuple
 
+
 (* 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
@@ -146,7 +180,8 @@
     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)
+  let mem = Hashtbl.create 63 in
+  Aux.unique_sorted (List.rev_map (guarded_type_memo struc mem qr) ktups)
 
 
 
@@ -172,30 +207,29 @@
     | phi -> phi
 
 
-let distinguish_by_type ?(how=Guarded) ?(skip_outer_exists=false) ~qr ~k
-    sPos sNeg =
+let distinguish_by_type ?(how=Guarded) ?(skip_outer_exists=false) 
+    ~qr ~k pos_struc neg_struc =
   let types s = match how with 
     | Guarded -> guarded_types s ~qr ~k 
     | Types -> ntypes 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 (pos_tp, neg_tp) = (List.map types pos_struc, List.map types neg_struc) in
+  let candidates = List.rev_append (List.concat pos_tp) 
+    (List.map (fun f -> Not f) (List.concat neg_tp)) in
+  let fails_neg f = not (List.exists (fun s -> check s [||] f) neg_struc) 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 fail_neg = 
+    List.rev_map (fun f -> Formula.flatten_sort (FormulaOps.nnf f)) fail_neg in
+  let tp_lits = function And fl -> List.filter Formula.is_literal fl | _-> [] in
+  let cmp_tp tp1 tp2 = 
+    let c = Formula.compare (And (tp_lits tp1)) (And (tp_lits tp2)) in
+    if c <> 0 then c else Formula.compare tp1 tp2 in
+  let fail_neg = Aux.unique_sorted ~cmp:cmp_tp fail_neg in
+  let succ_pos fl = List.for_all (fun s -> check s [||] (Or fl)) pos_struc 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
+  let dtypes = find_type [] fail_neg 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

Modified: trunk/Toss/Solver/DistinguishTest.ml
===================================================================
--- trunk/Toss/Solver/DistinguishTest.ml	2011-11-14 15:49:50 UTC (rev 1632)
+++ trunk/Toss/Solver/DistinguishTest.ml	2011-11-16 21:58:12 UTC (rev 1633)
@@ -293,13 +293,10 @@
 	   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]);
-      assert true;
+\"" in formula_eq 
+    "P(x0) and P(x1) and C(x0, x1) and ex x2 (P(x2) and C(x2, x0))"
+    (Distinguish.distinguish ~skip_outer_exists:true 
+       [strucP] [strucN1; strucN2; strucN3]);
     );
 
   "breakthrough" >::
@@ -339,9 +336,8 @@
 	   ...   ...   ...   W..
 	...   ...   ...   ...   
 	...W  ...   ...   ...   
-\"" in (* "W(x2) and all x3 not C(x2, x3)" *)
-      (* Distinguish.set_debug_level 1; *)
-      formula_eq "W(x0) and R(x0, x1) and all x2 not C(x1, x2)"
+\"" in (* Distinguish.set_debug_level 1; *)
+      formula_eq "W(x1) and all x0 not C(x1, x0)"
 	(Distinguish.distinguish ~skip_outer_exists:true [struc1] [struc2]);
     );
 ]

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