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

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

Revision: 1724
          http://toss.svn.sourceforge.net/toss/?rev=1724&view=rev
Author:   lukaszkaiser
Date:     2012-06-15 15:23:31 +0000 (Fri, 15 Jun 2012)
Log Message:
-----------
Allowing non-PNF QBFs and adding a separate SO evaluation function.

Modified Paths:
--------------
    trunk/Toss/Client/State.js
    trunk/Toss/Formula/BoolFormula.ml
    trunk/Toss/Formula/BoolFormula.mli
    trunk/Toss/Solver/Solver.ml
    trunk/Toss/Solver/SolverTest.ml

Modified: trunk/Toss/Client/State.js
===================================================================
--- trunk/Toss/Client/State.js	2012-06-09 20:09:07 UTC (rev 1723)
+++ trunk/Toss/Client/State.js	2012-06-15 15:23:31 UTC (rev 1724)
@@ -227,7 +227,7 @@
 	    document.getElementById("svg").appendChild(r);
 	} else {
 	    var circ = SHAPES.circle (
-		elem.x, elem.y, 30,
+		elem.x, elem.y, SHAPES.circle_size,
 		[["id", "elem_" + elem.id], ["class", elem_class(elem.id)],
 		 ["onclick", "handle_elem_click('" + elem.id + "')"]]);
 	    document.getElementById("svg").appendChild(circ);
@@ -269,9 +269,13 @@
     if (sqrt * sqrt == this.elems.length && (sqrt > 4 || game=="Tic-Tac-Toe")) {
         SHAPES.elem_size_x = SVG_WIDTH / (2.0 * (sqrt-1));
         SHAPES.elem_size_y = SVG_HEIGHT / (2.0 * (sqrt-1));
+    } else if (this.elems.length < 30) {
+        SHAPES.elem_size_x = SVG_WIDTH / 20;
+        SHAPES.elem_size_y = SVG_HEIGHT / 20;
     } else {
         SHAPES.elem_size_x = SVG_WIDTH / 20;
-        SHAPES.elem_size_y = SVG_HEIGHT / 20;
+        SHAPES.elem_size_y = SVG_WIDTH / 20;
+        SHAPES.circle_size = 300 / this.elems.length;
     }
     draw_background (game);
     for (var i = 0; i < this.elems.length; i++) {
@@ -305,6 +309,7 @@
 function Shapes () {
     this.elem_size_x = 25; // suggested size of elements
     this.elem_size_y = 25; // suggested size of elements
+    this.circle_size = 30;
 
     var DEFpawn = '<g transform="translate(-22.5,-22.5)"> \
     <path \

Modified: trunk/Toss/Formula/BoolFormula.ml
===================================================================
--- trunk/Toss/Formula/BoolFormula.ml	2012-06-09 20:09:07 UTC (rev 1723)
+++ trunk/Toss/Formula/BoolFormula.ml	2012-06-15 15:23:31 UTC (rev 1724)
@@ -892,13 +892,21 @@
 
 (* Type for quantified Boolean formulas. *)
 type qbf = 
-  | QFree of bool_formula
+  | QVar of int
+  | QNot of qbf
+  | QAnd of qbf list
+  | QOr of qbf list
   | QEx of int list * qbf
   | QAll of int list * qbf
 
 (* Print a QBF formula. *)
 let rec qbf_str = function
-  | QFree phi -> str phi
+  | QVar v -> var_str v
+  | QNot phi -> "(not " ^ (qbf_str phi) ^ ")"
+  | QAnd [] -> "true"
+  | QOr [] -> "false"
+  | QAnd (qbflist) -> qbf_list_str " and " qbflist
+  | QOr (qbflist) -> qbf_list_str " or " qbflist
   | QEx (vars, phi) -> 
     "(ex " ^ (String.concat ", " (List.map string_of_int vars)) ^ 
       " " ^ qbf_str phi ^ ")"
@@ -906,7 +914,12 @@
     "(ex " ^ (String.concat ", " (List.map string_of_int vars)) ^ 
       " " ^ qbf_str phi ^ ")"
 
+and qbf_list_str sep = function
+  | [] -> "[]"
+  | [phi] -> qbf_str phi
+  | lst -> "(" ^ (String.concat sep (List.map qbf_str lst)) ^ ")"
 
+
 (* Read a qdimacs description of a QBF from [in_ch]. *)
 let read_qdimacs in_str =
   let in_ch = ref in_str in
@@ -970,8 +983,7 @@
 	for i = 1 to (no_cl-1) do
 	  cls := (read_clause (sinput_line ())) :: !cls
 	done;
-	QFree (
-	  BAnd (List.map (fun lits -> BOr (List.map lit_of_int lits)) !cls))
+	QAnd (List.map (fun lits -> QOr (List.map (fun v -> QVar v) lits)) !cls)
       ) in
     read_phi () in
   
@@ -980,7 +992,10 @@
 
 (* Eliminating quantifiers from QBF formulas. *)
 let rec elim_quant_rec = function
-  | QFree (phi) -> phi
+  | QVar (v) -> BVar (v)
+  | QNot (f) -> BNot (elim_quant_rec f)
+  | QAnd (l) -> BAnd (List.map elim_quant_rec l)
+  | QOr (l) -> BOr (List.map elim_quant_rec l)
   | QEx (vars, qphi) ->
     Hashtbl.clear has_vars_mem;
     let inside, len = elim_quant_rec qphi, List.length vars in

Modified: trunk/Toss/Formula/BoolFormula.mli
===================================================================
--- trunk/Toss/Formula/BoolFormula.mli	2012-06-09 20:09:07 UTC (rev 1723)
+++ trunk/Toss/Formula/BoolFormula.mli	2012-06-15 15:23:31 UTC (rev 1724)
@@ -5,7 +5,7 @@
 (** This type describes formulas of relational logic with equality.
    We allow only simple boolean junctors, other are resolved during parsing. *)
 type bool_formula =
-    BVar of int
+  | BVar of int
   | BNot of bool_formula
   | BAnd of bool_formula list
   | BOr of bool_formula list
@@ -80,7 +80,10 @@
 
 (** Type for quantified Boolean formulas. *)
 type qbf = 
-  | QFree of bool_formula
+  | QVar of int
+  | QNot of qbf
+  | QAnd of qbf list
+  | QOr of qbf list
   | QEx of int list * qbf
   | QAll of int list * qbf
 

Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml	2012-06-09 20:09:07 UTC (rev 1723)
+++ trunk/Toss/Solver/Solver.ml	2012-06-15 15:23:31 UTC (rev 1724)
@@ -393,6 +393,9 @@
 	Hashtbl.clear !re_cache_results;
 	List.iter (fun (p, r) -> Hashtbl.add !re_cache_results p r) !ok_re
 
+(* Evaluation with second-order variables. *)
+let eval_so struc phi = 
+  Empty
 
 (* Eval with very basic caching. *)
 let eval_m struc phi = 
@@ -405,12 +408,21 @@
       res
     with Not_found ->
       LOG 1 "Eval_m %s" (str phi);
-      let els = Assignments.set_to_set_list (Structure.elems struc) in
-      check_timeout "Solver.eval_m.not_found";
-      let asg = eval [] struc els Any phi in
-      incr eval_counter;
-      Hashtbl.add !cache_results phi (asg, phi_rels phi);
-      asg
+      let vars = FormulaSubst.all_vars phi in
+      if List.exists (fun v -> Formula.is_so v) vars then (
+        check_timeout "Solver.eval_m.not_found_so";
+        let asg = eval_so struc phi in
+        incr eval_counter;
+        Hashtbl.add !cache_results phi (asg, phi_rels phi);
+        asg
+      ) else (
+        let els = Assignments.set_to_set_list (Structure.elems struc) in
+        check_timeout "Solver.eval_m.not_found_noso";
+        let asg = eval [] struc els Any phi in
+        incr eval_counter;
+        Hashtbl.add !cache_results phi (asg, phi_rels phi);
+        asg
+      )
   )
 
 (* Evaluate real expressions. Result is represented as assignments with

Modified: trunk/Toss/Solver/SolverTest.ml
===================================================================
--- trunk/Toss/Solver/SolverTest.ml	2012-06-09 20:09:07 UTC (rev 1723)
+++ trunk/Toss/Solver/SolverTest.ml	2012-06-15 15:23:31 UTC (rev 1724)
@@ -165,6 +165,13 @@
 	"{ z->1, z->2, z->3 }";
     );
 
+  "eval: second-order" >::
+    (fun () ->
+      eval_eq "[ a, b | T { a } | ]" 
+        "ex |R all x, y (|R (x, y) <-> (T(x) and not T(y)))"
+        "T";
+    );
+
   "eval: game heuristic tests" >::
     (fun () ->
       let heur_phi = "(((R(v, w) and R(w, x) and R(x, y) and R(y, z)) or 

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