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

[<ab...@us...>]

Revision: 1735
          http://toss.svn.sourceforge.net/toss/?rev=1735&view=rev
Author:   abuzaid
Date:     2012-06-27 17:33:04 +0000 (Wed, 27 Jun 2012)
Log Message:
-----------
Evaluation of SO-Formulae by reduction to SAT

Modified Paths:
--------------
    trunk/Toss/Client/JsEval.ml
    trunk/Toss/Client/eval.html
    trunk/Toss/Formula/BoolFormula.ml
    trunk/Toss/Formula/BoolFormula.mli
    trunk/Toss/Formula/Formula.ml
    trunk/Toss/Solver/Solver.ml
    trunk/Toss/Solver/Solver.mli
    trunk/Toss/Solver/SolverTest.ml

Added Paths:
-----------
    trunk/Toss/Formula/myTest.ml

Modified: trunk/Toss/Client/JsEval.ml
===================================================================
--- trunk/Toss/Client/JsEval.ml	2012-06-25 18:03:52 UTC (rev 1734)
+++ trunk/Toss/Client/JsEval.ml	2012-06-27 17:33:04 UTC (rev 1735)
@@ -43,13 +43,27 @@
 (* The Formula evaluation and registration in JS. *)
 let js_eval phi struc = 
   let (phi, struc) = (Js.to_string phi, Js.to_string struc) in
-  LOG 0 "Evaluation of %s on %s" phi struc;
   let (f, struc) = (formula_of_string phi, structure_of_string struc) in
   Js.string (AssignmentSet.named_str struc (Solver.M.evaluate struc f))
-		
+
+
+(*
+let js_eval_so phi struc =
+	let (phi, struc) = (Js.to_string phi, Js.to_string struc) in
+	 let (f, struc) = (formula_of_string phi, structure_of_string struc) in
+	  let qbf = (Solver.so_to_qbf struc f) in
+		 let sat = (Solver.elim_quant_naiv qbf) in
+	    LOG 0 "Formula: %s"  (Formula.str f);
+		  LOG 0 "QBF Formula: %s"  (BoolFormula.qbf_str qbf);
+			LOG 0 "SAT Formula: %s" (BoolFormula.str sat);
+			Js.string (AssignmentSet.named_str struc (Solver.eval_so struc f))
+*)		 
+
 let _ = set_handle "eval" js_eval
 
 
+
+
 (* Drawing the structure. *)
 let draw_struc_js struc_s =
   let st = structure_of_string (Js.to_string struc_s) in

Modified: trunk/Toss/Client/eval.html
===================================================================
--- trunk/Toss/Client/eval.html	2012-06-25 18:03:52 UTC (rev 1734)
+++ trunk/Toss/Client/eval.html	2012-06-27 17:33:04 UTC (rev 1735)
@@ -59,6 +59,7 @@
   })
 }
 
+
 function canvasCoords (event) { // From stackoverflow.com
     var totalOffsetX = 0;
     var totalOffsetY = 0;
@@ -128,9 +129,9 @@
 
 function example_3col () {
   document.getElementById ("formula").value = 
-    "ex R, G, B all x, y ( \n  (x in R or x in G or x in B) and (" +
-    "\n    E(x,y) -> not ( (x in R and y in R) " +
-    "\n      or (x in G and y in G) or (x in B and y in B) ) ) )";
+    "ex |R, |G, |B all x, y ( \n  ( |R(x) or |G(x) or |B(x)) and (" +
+    "\n    E(x,y) -> not ( ( |R(x) and  |R(y)) " +
+    "\n      or (|G(x) and |G(y)) or (|B(x) and |B(y)) ) ) )";
   document.getElementById ("structure").value = 
     "[ | E { (a, b); (b, c); (c, a) } | " + 
     "\n  x { a -> 1, b -> 2, c -> 3 }; " +
@@ -161,7 +162,6 @@
 </textarea> 
 
 <p>Positions:</p>
-
 <textarea id="positions" rows="3" cols="60">
 :x(a) = &a;
 :y(a) = &a · (10 - &a) / 10

Modified: trunk/Toss/Formula/BoolFormula.ml
===================================================================
--- trunk/Toss/Formula/BoolFormula.ml	2012-06-25 18:03:52 UTC (rev 1734)
+++ trunk/Toss/Formula/BoolFormula.ml	2012-06-27 17:33:04 UTC (rev 1735)
@@ -911,7 +911,7 @@
     "(ex " ^ (String.concat ", " (List.map string_of_int vars)) ^ 
       " " ^ qbf_str phi ^ ")"
   | QAll (vars, phi) -> 
-    "(ex " ^ (String.concat ", " (List.map string_of_int vars)) ^ 
+    "(all " ^ (String.concat ", " (List.map string_of_int vars)) ^ 
       " " ^ qbf_str phi ^ ")"
 
 and qbf_list_str sep = function
@@ -1030,3 +1030,37 @@
   let res = elim_quant_rec phi in
   set_simplification 2;
   res
+	
+(* reduce QBF to SAT *)		
+let sat_of_qbf phi = let ids, free_id = Hashtbl.create 7, ref 0 in
+   let get_id x = try Hashtbl.find ids x with Not_found ->
+   (Hashtbl.add ids x (!free_id +1); incr free_id; !free_id ) in
+    let compute_id var asgn = get_id (var, asgn) in
+		 (* reduce QBF to SAT (recursive helper)*)
+      let rec sat_of_qbf_rec phi asgn = (match phi with
+	     | QVar v -> (try List.assoc v asgn with Not_found ->  (BVar v))
+	     | QAnd l -> 
+				let resl = (Aux.unique_sorted (List.filter (fun x -> x <> BAnd []) (List.map (fun x -> sat_of_qbf_rec x asgn) l))) in
+				(try List.find (fun x -> x = BOr []) resl with Not_found -> (BAnd resl))
+	     | QOr l -> 
+				let resl = (Aux.unique_sorted (List.filter (fun x -> x <> BOr []) (List.map (fun x -> sat_of_qbf_rec x asgn) l))) in
+				(try List.find (fun x -> x = BAnd []) resl with Not_found -> (BOr resl))
+	     | QNot f ->
+				let res = (sat_of_qbf_rec f asgn) in 
+				if res = BAnd [] then BOr []
+				else if res = BOr [] then BAnd []
+				else BNot res
+	     | QEx (var::vl, f) -> (sat_of_qbf_rec (QEx (vl, f)) ((var, (BVar (get_id (var, asgn))))::asgn))
+	     | QEx ([], f) -> (sat_of_qbf_rec f asgn)
+	     | QAll (var::tl, f) -> 
+				let resl = 
+					(Aux.unique_sorted (List.filter 
+					 (fun x -> x <> BAnd []) 
+					  [(sat_of_qbf_rec (QAll (tl, f)) ((var, BOr [])::asgn)); (sat_of_qbf_rec (QAll (tl, f)) ((var, BAnd [])::asgn))]
+					)) in
+				(try (List.find (fun x -> x = BOr []) resl) with Not_found -> (BAnd resl))				
+	     | QAll ([], f) -> (sat_of_qbf_rec f asgn)
+			)
+      in
+			(sat_of_qbf_rec phi []) 			
+

Modified: trunk/Toss/Formula/BoolFormula.mli
===================================================================
--- trunk/Toss/Formula/BoolFormula.mli	2012-06-25 18:03:52 UTC (rev 1734)
+++ trunk/Toss/Formula/BoolFormula.mli	2012-06-27 17:33:04 UTC (rev 1735)
@@ -95,3 +95,6 @@
 
 (** Eliminating quantifiers from QBF formulas. *)
 val elim_quant : qbf -> bool_formula
+
+(** Reduce QBF to SAT by elimination of quantifiers. *)
+val sat_of_qbf : qbf -> bool_formula
\ No newline at end of file

Modified: trunk/Toss/Formula/Formula.ml
===================================================================
--- trunk/Toss/Formula/Formula.ml	2012-06-25 18:03:52 UTC (rev 1734)
+++ trunk/Toss/Formula/Formula.ml	2012-06-27 17:33:04 UTC (rev 1735)
@@ -757,3 +757,4 @@
 	quit2 := max 1. (min 10000. q2);
 	(y5, h, h *. (min 5. (sf /. e4)))
       )
+			

Added: trunk/Toss/Formula/myTest.ml
===================================================================
--- trunk/Toss/Formula/myTest.ml	                        (rev 0)
+++ trunk/Toss/Formula/myTest.ml	2012-06-27 17:33:04 UTC (rev 1735)
@@ -0,0 +1,6 @@
+open Formula
+
+let formula_of_string s = 
+  FormulaParser.parse_formula Lexer.lex (Lexing.from_string s)
+
+Hashtbl.iter (fun v a -> Printf.printf "%s: %d" v a) so_arities (Hashtbl.create 10) (formula_of_string "Ex |R (All x |R(x))") 
\ No newline at end of file


Property changes on: trunk/Toss/Formula/myTest.ml
___________________________________________________________________
Added: svn:mime-type
   + text/plain

Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml	2012-06-25 18:03:52 UTC (rev 1734)
+++ trunk/Toss/Solver/Solver.ml	2012-06-27 17:33:04 UTC (rev 1735)
@@ -1,11 +1,13 @@
 (* Solver for checking if formulas hold on structures. *)
 
+open BoolFormula
 open Bitvector
 open AssignmentSet
 open Assignments
 open Structure
 open Formula
 
+
 (* CACHE *)
 
 type cachetbl = 
@@ -393,10 +395,105 @@
 	Hashtbl.clear !re_cache_results;
 	List.iter (fun (p, r) -> Hashtbl.add !re_cache_results p r) !ok_re
 
+
+	
+let so_to_qbf struc psi =	
+ let ids, free_id = Hashtbl.create 7, ref 0 in	
+	let get_id x = try Hashtbl.find ids x with Not_found ->
+   (Hashtbl.add ids x (!free_id +1); incr free_id; !free_id ) in
+    let compute_id var args asgn = get_id (var, args, asgn) in  
+     (* Reduce the Evaluation Problem of SO formulae to QBF *)
+let rec so_to_qbf_rec struc psi asgn  = match psi with
+ | SO (rel, args) ->
+     let v = (compute_id (var_str rel) args asgn) in		 
+     (QVar v, [(var_str rel, v)])
+ | Rel (rel, va) -> 
+	let args = Array.map (fun x -> try List.assoc x asgn with Not_found -> 0) va in
+	 if (Structure.check_rel struc rel args) then (QAnd [], []) else (QOr [], [])
+ | Eq (var1, var2) -> if (try List.assoc var1 asgn with Not_found -> 0) = (try List.assoc var1 asgn with Not_found -> 0) then (QAnd [], []) else (QOr [], [])    	
+ | And phil ->
+	let resl = (List.map (fun phi -> (so_to_qbf_rec struc phi asgn)) phil) in
+	 let qphil = (Aux.unique_sorted (List.map (fst) resl)) in
+	  let dictl = (List.map (snd) resl) in		 					   
+	   (try 
+			((List.find (fun x -> x = QOr []) qphil), []) 
+			with Not_found -> (				
+				QAnd (List.filter (fun x -> x <> QAnd []) qphil), List.concat dictl
+			))
+			 
+ | Or phil -> 
+	let resl = (List.map (fun phi -> (so_to_qbf_rec struc phi asgn)) phil) in
+	 let qphil = (Aux.unique_sorted (List.map (fst) resl)) in
+	  let dictl = (List.map (snd) resl) in	
+		 (try ((List.find (fun x -> x = QAnd []) qphil), []) with Not_found -> (QOr (List.filter (fun x -> x <> QOr []) qphil), List.concat dictl))
+ | Not phi -> let (qphi, dict) =  so_to_qbf_rec struc phi asgn in 
+             (if qphi = QOr [] then 
+	            (QAnd [], dict)
+						 else if qphi = QAnd [] then
+							(QOr [], dict)
+						 else
+							(QNot qphi, dict))   
+ | Ex (vl, phi) -> 
+	(
+	 match vl with
+	 | [] -> so_to_qbf_rec struc phi asgn
+	 | var::tl -> 		  
+	    if is_fo var then 
+			 let asgn_list = List.map (fun x -> (Formula.to_fo var, x)::asgn) (Structure.elements struc) in
+				let res = (List.map (fun x -> so_to_qbf_rec struc  (Ex (tl, phi)) x) asgn_list) in
+			   let (qphil, dictl) = ((Aux.unique_sorted (List.map (fst) res)), List.map (snd) res)in
+				  (try ((List.find (fun x -> x = QAnd []) qphil), []) with Not_found -> (QOr (List.filter (fun x -> x <> QOr []) qphil), List.concat dictl)) 
+		  else if is_so var then	
+       let (qbf_phi, dict_phi) = (so_to_qbf_rec struc (Ex (tl, phi)) asgn) in
+			  let rel_qbf_vars = Aux.unique_sorted (Aux.assoc_all (var_str var) dict_phi) in
+         if qbf_phi = QAnd [] then (QAnd [], [])
+				else if qbf_phi = QOr [] then (QOr [], [])
+				else if (rel_qbf_vars = []) then (qbf_phi, dict_phi)
+				else (QEx (rel_qbf_vars, qbf_phi), dict_phi)
+		  else (* stub *)
+		    (so_to_qbf_rec struc phi asgn)
+	)	
+ | All (vl, phi) -> 
+	(
+	 match vl with
+	 | [] -> so_to_qbf_rec struc phi asgn
+	 | var::tl -> 		  
+	    if is_fo var then 
+		 	let asgn_list = List.map (fun x -> (Formula.to_fo var, x)::asgn) (Structure.elements struc) in
+			  let res = (List.map (fun x -> so_to_qbf_rec struc  (All (tl, phi)) x) asgn_list) in
+				 let (qphil, dictl) = ((Aux.unique_sorted (List.map (fst) res)), List.map (snd) res)in				   
+			  	(try 
+						((List.find (fun x -> x = (QOr [])) qphil), []) 
+					with Not_found -> 
+						(QAnd (List.filter (fun x -> x <> (QAnd [])) qphil), List.concat dictl)) 
+	 	 else if is_so var then
+       let (qbf_phi, dict_phi) = so_to_qbf_rec struc (All (tl, phi)) asgn in
+       let rel_qbf_vars = Aux.unique_sorted (Aux.assoc_all (var_str var) dict_phi) in
+			  if qbf_phi = QAnd [] then (QAnd [], [])
+				else if qbf_phi = QOr [] then (QOr [], [])
+				else if (rel_qbf_vars = []) then (qbf_phi, dict_phi)
+				else (QAll (rel_qbf_vars, qbf_phi), dict_phi)
+		  else (* stub *)
+		    (so_to_qbf_rec struc phi asgn)
+   ) in
+fst (so_to_qbf_rec struc psi [])			  
+
+						
+
+
 (* Evaluation with second-order variables. *)
-let eval_so struc phi = 
-  Empty
-
+let eval_so struc phi =	
+	let qbf = (so_to_qbf struc phi) in
+	let bf = (BoolFormula.sat_of_qbf qbf) in
+	let cnf = (BoolFormula.convert bf) in
+	 LOG 0 "QBF:";
+	 LOG 0 "%s" (BoolFormula.qbf_str qbf);
+	 LOG 0 "BF:";
+	 LOG 0 "%s" (BoolFormula.str bf);
+	 LOG 0 "CNF:";
+	 LOG 0 "%s" (Sat.cnf_str cnf);
+   if (Sat.is_sat cnf) then Any else Empty		
+				 
 (* Eval with very basic caching. *)
 let eval_m struc phi = 
   if phi = And [] then Any else (

Modified: trunk/Toss/Solver/Solver.mli
===================================================================
--- trunk/Toss/Solver/Solver.mli	2012-06-25 18:03:52 UTC (rev 1734)
+++ trunk/Toss/Solver/Solver.mli	2012-06-27 17:33:04 UTC (rev 1735)
@@ -2,7 +2,6 @@
 
 (** {1 Interface} *)
 
-
 (** Interface to the solver. *)
 module M : sig
   (** Check the formula on the structure. *)
@@ -31,7 +30,8 @@
   val set_timeout : (unit -> bool) -> unit
 
   (** Clear timeout function. *)
-  val clear_timeout : unit -> unit
+  val clear_timeout : unit -> unit	
+	 
 end
 
 

Modified: trunk/Toss/Solver/SolverTest.ml
===================================================================
--- trunk/Toss/Solver/SolverTest.ml	2012-06-25 18:03:52 UTC (rev 1734)
+++ trunk/Toss/Solver/SolverTest.ml	2012-06-27 17:33:04 UTC (rev 1735)
@@ -34,7 +34,7 @@
 
 
 let tests = "Solver" >::: [
-  "eval: first-order quantifier free" >::
+ "eval: first-order quantifier free" >::
     (fun () ->
       eval_eq "[ | P { (a1) }; R:1 {} | ]" "P(x0)" "{ x0->1 }";
       eval_eq "[ | P:1 {}; R { (a1) } | ]" "P(x0)" "{}";
@@ -165,13 +165,41 @@
 	"{ z->1, z->2, z->3 }";
     );
 
-  "eval: second-order" >::
+  "eval: second-order T" >::
     (fun () ->
-      eval_eq "[ a, b | T { a } | ]" 
-        "ex |R all x, y (|R (x, y) <-> (T(x) and not T(y)))"
-        "T";
+			let formula = "all |Q ex |R all x, y (|R (x, y) <-> (|Q(x) and not T(y)))" in
+			 let struc = "[ a, b | T { a } | ]" in
+        (			  			
+			  eval_eq struc 
+         formula
+         "T";
+				)
     );
-
+		
+		"eval: second-order F" >::
+    (fun () ->
+			let formula = "ex |R all |Q all x (not (|R(x) and |Q(x)) and (|R(x) or |Q(x)))" in
+			 let struc = "[ a, b | T { a } | ]" in
+        (			  			
+			  eval_eq struc 
+         formula
+         "{}";
+				)
+    );
+(*  
+	"convert: eval second-order to QBF" >::
+    (fun () ->(
+			 print_endline (Formula.str (formula_of_string "ex |V all |Q ex |R all x, y (T(x) or |R (x, y))")); 
+       print_endline (BoolFormula.qbf_str (Solver.so_to_qbf (struc_of_string "[ a, b | T { a } | ]") (formula_of_string "ex |R all x, y (T(x) or |R (x, y))")));
+			
+			 print_endline (Formula.str (formula_of_string "all |Q  all x, y (T(x) or Q(y) or (x = y))")); 
+       print_endline (BoolFormula.qbf_str (Solver.so_to_qbf (struc_of_string "[ a, b | T { a } | ]") (formula_of_string "all |Q  all x, y (T(x) or Q(y) or (x = y))")));
+			
+			 print_endline (Formula.str (formula_of_string "ex x all  y ((T(x) and T(y)) -> x = y)")); 
+       print_endline (BoolFormula.qbf_str (Solver.so_to_qbf (struc_of_string "[ a, b | T { a } | ]") (formula_of_string "ex x all  y ((T(x) and T(y)) -> x = y)")));
+			)			
+    );
+*)
   "eval: game heuristic tests" >::
     (fun () ->
       let heur_phi = "(((R(v, w) and R(w, x) and R(x, y) and R(y, z)) or 
@@ -247,6 +275,7 @@
 
 
 let bigtests = "SolverBig" >::: [
+(*	
   "eval: bigger tc tests" >::
     (fun () ->
       let diag_phi_mso = 
@@ -413,5 +442,5 @@
 
       eval_eq (grid 2) four_color_f "";
     );*)
-
+*)
 ]

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