[Toss-devel-svn] SF.net SVN: toss:[1737] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1737] trunk/Toss
|
From: <luk...@us...> - 2012-06-27 23:29:15
|
Revision: 1737
http://toss.svn.sourceforge.net/toss/?rev=1737&view=rev
Author: lukaszkaiser
Date: 2012-06-27 23:29:07 +0000 (Wed, 27 Jun 2012)
Log Message:
-----------
New code cleanups and tests.
Modified Paths:
--------------
trunk/Toss/Client/eval.html
trunk/Toss/Formula/BoolFormula.ml
trunk/Toss/Formula/BoolFormula.mli
trunk/Toss/Makefile
trunk/Toss/Solver/Solver.ml
trunk/Toss/Solver/Solver.mli
trunk/Toss/Solver/SolverTest.ml
Modified: trunk/Toss/Client/eval.html
===================================================================
--- trunk/Toss/Client/eval.html 2012-06-27 18:18:35 UTC (rev 1736)
+++ trunk/Toss/Client/eval.html 2012-06-27 23:29:07 UTC (rev 1737)
@@ -138,11 +138,25 @@
"\n y { a -> 0, b -> -1, c -> 0 } ]";
eval_it ();
}
+
+function example_heart_drawing () {
+ document.getElementById ("relations").value =
+ "E(x, y) = (&y = &x + 1 and &x != 18) ∨ (&x=37 ∧ &y=18)";
+ document.getElementById ("positions").value =
+ ":x(a) = :(&a <= 18) * (:(&a =< 10) * &a - :(&a > 10) * (&a - 20)) \n" +
+ " - let :b = &a - 18 in :(&a > 18) * (:(:b =< 10) * :b - \n " +
+ " :(:b > 10) * (:b - 20) - 2); \n\n" +
+ ":y(a) = :(&a <= 18) * (:(&a =< 10) *&a · (10 - &a) / 10 - \n " +
+ " :(&a > 10)*(&a - 10)) + let :b = &a - 18 in \n" +
+ " :(&a > 18) * (:(:b =< 10) *:b · (10 - :b) / 10 - :(:b > 10)*(:b - 10))";
+ document.getElementById ("no-elems").value = "37";
+ eval_it ();
+}
//-->
</script>
</head>
-<body onload="init_canvas ()">
+<body onload="init_canvas (); eval_it ()">
<div id="main">
<div id="top">
Modified: trunk/Toss/Formula/BoolFormula.ml
===================================================================
--- trunk/Toss/Formula/BoolFormula.ml 2012-06-27 18:18:35 UTC (rev 1736)
+++ trunk/Toss/Formula/BoolFormula.ml 2012-06-27 23:29:07 UTC (rev 1737)
@@ -1030,37 +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 [])
+(* Reduce QBF to SAT by taking all possibilities for universal variables *)
+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
+ (* 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.rev_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.rev_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 redl = [(sat_of_qbf_rec (QAll (tl, f)) ((var, BOr [])::asgn));
+ (sat_of_qbf_rec (QAll (tl, f)) ((var, BAnd [])::asgn))] in
+ let resl = Aux.unique_sorted (List.filter (fun x->x <> BAnd []) redl) 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-27 18:18:35 UTC (rev 1736)
+++ trunk/Toss/Formula/BoolFormula.mli 2012-06-27 23:29:07 UTC (rev 1737)
@@ -96,5 +96,5 @@
(** 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
+(** Reduce QBF to SAT by taking all possibilities for universal variables *)
+val sat_of_qbf : qbf -> bool_formula
Modified: trunk/Toss/Makefile
===================================================================
--- trunk/Toss/Makefile 2012-06-27 18:18:35 UTC (rev 1736)
+++ trunk/Toss/Makefile 2012-06-27 23:29:07 UTC (rev 1737)
@@ -186,48 +186,48 @@
# Formula tests
FormulaTests: Server/Server.native
cp _build/Server/Server.native TossServer
- OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -fulltest Formula
-FormulaTestsVerbose: Server/Server.native
+ OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -test Formula -v
+FormulaTestsFull: Server/Server.native
cp _build/Server/Server.native TossServer
OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -fulltest Formula -v
# Solver tests
SolverTests: Server/Server.native
cp _build/Server/Server.native TossServer
- OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -fulltest Solver
-SolverTestsVerbose: Server/Server.native
+ OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -test Solver -v
+SolverTestsFull: Server/Server.native
cp _build/Server/Server.native TossServer
OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -fulltest Solver -v
# Term tests
TermTests: Server/Server.native
cp _build/Server/Server.native TossServer
- OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -fulltest Term
-TermTestsVerbose: Server/Server.native
+ OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -test Term -v
+TermTestsFull: Server/Server.native
cp _build/Server/Server.native TossServer
OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -fulltest Term -v
# Arena tests
ArenaTests: Server/Server.native
cp _build/Server/Server.native TossServer
- OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -fulltest Arena
-ArenaTestsVerbose: Server/Server.native
+ OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -test Arena -v
+ArenaTestsFull: Server/Server.native
cp _build/Server/Server.native TossServer
OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -fulltest Arena -v
# Play tests
PlayTests: Server/Server.native
cp _build/Server/Server.native TossServer
- OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -fulltest Play
-PlayTestsVerbose: Server/Server.native
+ OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -test Play -v
+PlayTestsFull: Server/Server.native
cp _build/Server/Server.native TossServer
OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -fulltest Play -v
# GGP tests
GGPTests: Server/Server.native
cp _build/Server/Server.native TossServer
- OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -fulltest GGP
-GGPTestsVerbose: Server/Server.native
+ OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -test GGP -v
+GGPTestsFull: Server/Server.native
cp _build/Server/Server.native TossServer
OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -fulltest GGP -v
@@ -237,8 +237,8 @@
# Learn tests
LearnTests: Server/Server.native
cp _build/Server/Server.native TossServer
- OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -fulltest Learn
-LearnTestsVerbose: Server/Server.native
+ OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -test Learn -v
+LearnTestsFull: Server/Server.native
cp _build/Server/Server.native TossServer
OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -fulltest Learn -v
@@ -249,16 +249,16 @@
# Client tests
ClientTests: Server/Server.native
cp _build/Server/Server.native TossServer
- OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -fulltest Client
-ClientTestsVerbose: Server/Server.native
+ OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -test Client -v
+ClientTestsFull: Server/Server.native
cp _build/Server/Server.native TossServer
OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -fulltest Client -v
# Server tests
ServerTests: Server/Server.native
cp _build/Server/Server.native TossServer
- OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -fulltest Server
-ServerTestsVerbose: Server/Server.native
+ OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -test Server -v
+ServerTestsFull: Server/Server.native
cp _build/Server/Server.native TossServer
OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -fulltest Server -v
Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml 2012-06-27 18:18:35 UTC (rev 1736)
+++ trunk/Toss/Solver/Solver.ml 2012-06-27 23:29:07 UTC (rev 1737)
@@ -396,103 +396,96 @@
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 [])
+(* Compute the QBF equivalent to the given SO formula on the given structure. *)
+let so_to_qbf struc psi =
+ let ids, free_id, elems = Hashtbl.create 7, ref 0, Structure.elements struc 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
+ let assoc_or_zero asgn x = try List.assoc x asgn with Not_found -> 0 in
+ (* Reduce the Evaluation Problem of SO formulae to QBF *)
+ let rec so_to_qbf_rec asgn = function
+ | 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 (assoc_or_zero asgn) va in
+ if (Structure.check_rel struc rel args) then (QAnd [], [])
+ else (QOr [], [])
+ | Eq (var1, var2) ->
+ if assoc_or_zero asgn var1 = assoc_or_zero asgn var2 then
+ (QAnd [], [])
+ else (QOr [], [])
+ | And phil ->
+ let resl = (List.map (fun phi -> (so_to_qbf_rec asgn phi)) 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 asgn phi)) 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 asgn phi in
+ if qphi = QOr [] then (QAnd [], dict)
+ else if qphi = QAnd [] then(QOr [], dict)
+ else (QNot qphi, dict)
+ | Ex ([], phi) -> so_to_qbf_rec asgn phi
+ | Ex (var::tl, phi) when is_fo var ->
+ let asgn_list = List.map (fun x -> (Formula.to_fo var, x)::asgn) elems in
+ let res = List.map (fun x -> so_to_qbf_rec x (Ex (tl, phi))) 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)
+ )
+ | Ex (var::tl, phi) when is_so var ->
+ let (qbf_phi, dict_phi) = (so_to_qbf_rec asgn (Ex (tl, phi))) 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)
+ | Ex (var::tl, phi) -> (*stub*) failwith "not implemented yet (so_qbf_Ex)"
+ | All ([], phi) -> so_to_qbf_rec asgn phi
+ | All (var::tl, phi) when is_fo var ->
+ let asgn_list = List.map (fun x -> (Formula.to_fo var, x)::asgn) elems in
+ let res = List.map (fun x -> so_to_qbf_rec x (All (tl, phi))) 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)
+ )
+ | All (var::tl, phi) when is_so var ->
+ let (qbf_phi, dict_phi) = so_to_qbf_rec asgn (All (tl, phi)) 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)
+ | All (var::tl, _) -> (*stub*) failwith "not implemented yet (so_qbf_All)"
+ | _ -> failwith "not implemented yet (so_qbf_Other)"
+ in fst (so_to_qbf_rec [] psi)
-
-
(* Evaluation with second-order variables. *)
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
+ let qbf = so_to_qbf struc phi in
+ let bf = (* BoolFormula.sat_of_qbf qbf *) BoolFormula.elim_quant qbf in
+ let cnf = BoolFormula.convert bf in
+ LOG 1 "QBF %s BF %s CNF %s:" (BoolFormula.qbf_str qbf) (BoolFormula.str bf)
+ (Sat.cnf_str cnf);
+ if Sat.is_sat cnf then Any else Empty
(* Eval with very basic caching. *)
let eval_m struc phi =
Modified: trunk/Toss/Solver/Solver.mli
===================================================================
--- trunk/Toss/Solver/Solver.mli 2012-06-27 18:18:35 UTC (rev 1736)
+++ trunk/Toss/Solver/Solver.mli 2012-06-27 23:29:07 UTC (rev 1737)
@@ -38,5 +38,6 @@
(** Counter of internal formula evaluations for profiling. *)
val eval_counter : int ref
+(** Compute the QBF equivalent to the given SO formula on the given structure.*)
+val so_to_qbf : Structure.structure -> Formula.formula -> BoolFormula.qbf
-
Modified: trunk/Toss/Solver/SolverTest.ml
===================================================================
--- trunk/Toss/Solver/SolverTest.ml 2012-06-27 18:18:35 UTC (rev 1736)
+++ trunk/Toss/Solver/SolverTest.ml 2012-06-27 23:29:07 UTC (rev 1737)
@@ -15,8 +15,8 @@
let eval_eq struc_s phi_s aset_s =
let res = ref "" in
- let (struc, phi) = (struc_of_string struc_s, formula_of_string phi_s) in
- res := AssignmentSet.str (evaluate struc phi);
+ let (struc, phi) = (struc_of_string struc_s, formula_of_string phi_s) in
+ res := AssignmentSet.str (evaluate struc phi);
assert_equal ~printer:(fun x -> x) aset_s !res
@@ -165,41 +165,46 @@
"{ z->1, z->2, z->3 }";
);
- "eval: second-order T" >::
- (fun () ->
- 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";
- )
+ "convert: second-order to QBF" >::
+ (fun () ->(
+ let qbf_str_eq struc_s phi_s qbf_s =
+ let phi, struc = formula_of_string phi_s, struc_of_string struc_s in
+ LOG 1 "%s" (Formula.str phi);
+ assert_equal ~printer:(fun x -> x) qbf_s
+ (BoolFormula.qbf_str (Solver.so_to_qbf struc phi)) in
+
+ qbf_str_eq "[ a, b | T { a } | ]" "ex |R all x, y (T(x) or |R (x, y))"
+ "which result is ok?";
+
+ 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: second-order F" >::
+
+ "eval: second-order" >::
(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
- "{}";
- )
+ let phi = "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 phi "T";
+
+ 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 "{}";
+
+ let col3phi =
+ ("ex |R, |G, |B all x, y ( (|R(x) or |G(x) or |B(x)) and (" ^
+ " E(x,y) -> not ( (|R(x) and |R(y)) " ^
+ " or (|G(x) and |G(y)) or (|B(x) and |B(y)) ) ) )") in
+ let triangle = "[ | E { (a, b); (b, c); (c, a) } | ] " in
+ eval_eq triangle col3phi "T";
);
-(*
- "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
@@ -270,12 +275,10 @@
real_val_eq "[ | R { (a, a); (a, b) } | ] "
"Sum (x, y | R (x, y) : 1)" 2.;
);
-
]
let bigtests = "SolverBig" >::: [
-(*
"eval: bigger tc tests" >::
(fun () ->
let diag_phi_mso =
@@ -442,5 +445,4 @@
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.
|
