toss-devel-svn Mailing List for Toss (Page 23)
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
toss-devel-svn — Toss development: svn commits
You can subscribe to this list here.
| 2010 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
(25) |
Dec
(62) |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2011 |
Jan
(26) |
Feb
(38) |
Mar
(67) |
Apr
(22) |
May
(41) |
Jun
(30) |
Jul
(24) |
Aug
(32) |
Sep
(29) |
Oct
(34) |
Nov
(18) |
Dec
(2) |
| 2012 |
Jan
(19) |
Feb
(25) |
Mar
(16) |
Apr
(2) |
May
(18) |
Jun
(21) |
Jul
(11) |
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
|
From: <luk...@us...> - 2010-11-27 21:41:41
|
Revision: 1198
http://toss.svn.sourceforge.net/toss/?rev=1198&view=rev
Author: lukaszkaiser
Date: 2010-11-27 21:41:35 +0000 (Sat, 27 Nov 2010)
Log Message:
-----------
Changing the default subst_vars to check for clashes.
Modified Paths:
--------------
trunk/Toss/Formula/FormulaOps.ml
trunk/Toss/Formula/FormulaOps.mli
trunk/Toss/Formula/FormulaOpsTest.ml
Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml 2010-11-27 20:55:24 UTC (rev 1197)
+++ trunk/Toss/Formula/FormulaOps.ml 2010-11-27 21:41:35 UTC (rev 1198)
@@ -249,6 +249,7 @@
subst_vars subst (rename_quant_avoiding avoidvars phi)
let subst_vars_nocheck subst phi = subst_vars subst phi
+let subst_vars subst phi = subst_vars_check subst phi
(* --------------------------- TRANSITIVE CLOSURE --------------------------- *)
Modified: trunk/Toss/Formula/FormulaOps.mli
===================================================================
--- trunk/Toss/Formula/FormulaOps.mli 2010-11-27 20:55:24 UTC (rev 1197)
+++ trunk/Toss/Formula/FormulaOps.mli 2010-11-27 21:41:35 UTC (rev 1198)
@@ -28,19 +28,15 @@
val map_to_atoms : (formula -> formula) -> formula -> formula
val map_to_atoms_expr : (formula -> formula) -> real_expr -> real_expr
-(* Map [f] to all variables occurring in the formula. Preserves order
- of subformulas. *)
+(** Map [f] to all variables occurring in the formula.
+ Preserves order of subformulas. *)
val map_to_all_vars : (var -> var) -> formula -> formula
-(* Apply substitution [subst] to all free variables in the given
- formula. Preserves order of subformulas. *)
+(** Apply substitution [subst] to all free variables in the given formula
+ checking for and preventing name clashes with quantified variables. *)
val subst_vars : (string * string) list -> formula -> formula
val subst_vars_nocheck : (string * string) list -> formula -> formula
-(* Apply substitution [subst] to all free variables in the given formula
- checking for and preventing name clashes with quantified variables. *)
-val subst_vars_check : (string * string) list -> formula -> formula
-
(** Rename quantified variables avoiding the ones from [avs] list,
and the above-quantified ones. Does not go into real_expr. *)
val rename_quant_avoiding : var list -> formula -> formula
Modified: trunk/Toss/Formula/FormulaOpsTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaOpsTest.ml 2010-11-27 20:55:24 UTC (rev 1197)
+++ trunk/Toss/Formula/FormulaOpsTest.ml 2010-11-27 21:41:35 UTC (rev 1198)
@@ -111,10 +111,13 @@
let subst_free_eq phi1 phi2 = formula_eq id phi2 subst phi1 in
let subst_all_eq phi1 phi2 =
formula_eq id phi2 (FormulaOps.map_to_atoms subst) phi1 in
+ subst_all_eq "ex x (P(x) and (not R(x, y)))"
+ "ex x (P(a) and (not R(a, b)))";
subst_free_eq "ex x (P(x) and not R(x, y))"
"ex x (P(x) and (not R(x, b)))";
- subst_all_eq "ex x (P(x) and (not R(x, y)))"
- "ex x (P(a) and (not R(a, b)))";
+ subst_free_eq "ex a R(x, a)" "ex a0 R(a, a0)";
+ formula_eq id "ex a R(a, a)"
+ (FormulaOps.subst_vars_nocheck [("x", "a")]) "ex a R(x, a)";
);
"assign emptyset" >::
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <luk...@us...> - 2010-11-27 20:55:30
|
Revision: 1197
http://toss.svn.sourceforge.net/toss/?rev=1197&view=rev
Author: lukaszkaiser
Date: 2010-11-27 20:55:24 +0000 (Sat, 27 Nov 2010)
Log Message:
-----------
First-order transitive closure and subst_vars debugging.
Modified Paths:
--------------
trunk/Toss/Formula/Aux.ml
trunk/Toss/Formula/Aux.mli
trunk/Toss/Formula/Formula.ml
trunk/Toss/Formula/FormulaOps.ml
trunk/Toss/Formula/FormulaOps.mli
trunk/Toss/Formula/FormulaOpsTest.ml
trunk/Toss/Formula/FormulaParser.mly
trunk/Toss/Solver/SolverTest.ml
Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml 2010-11-27 14:29:19 UTC (rev 1196)
+++ trunk/Toss/Formula/Aux.ml 2010-11-27 20:55:24 UTC (rev 1197)
@@ -11,8 +11,10 @@
let strings_of_list nvs =
add_strings nvs Strings.empty
+let is_digit c =
+ (c = '0') || (c = '1') || (c = '2') || (c = '3') || (c = '4') ||
+ (c = '5') || (c = '6') || (c = '7') || (c = '8') || (c = '9')
-
(* {2 Helper functions on lists and other functions lacking from the
standard library.} *)
let concat_map f l =
Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli 2010-11-27 14:29:19 UTC (rev 1196)
+++ trunk/Toss/Formula/Aux.mli 2010-11-27 20:55:24 UTC (rev 1197)
@@ -7,6 +7,8 @@
val add_strings : string list -> Strings.t -> Strings.t
val strings_of_list : string list -> Strings.t
+val is_digit : char -> bool
+
(** {2 Helper functions on lists and other functions lacking from the
standard library.} *)
Modified: trunk/Toss/Formula/Formula.ml
===================================================================
--- trunk/Toss/Formula/Formula.ml 2010-11-27 14:29:19 UTC (rev 1196)
+++ trunk/Toss/Formula/Formula.ml 2010-11-27 20:55:24 UTC (rev 1197)
@@ -12,15 +12,14 @@
type mso_var = [ `MSO of string ];;
type real_var = [ `Real of string ];;
-let is_digit c =
- (c = '0') || (c = '1') || (c = '2') || (c = '3') || (c = '4') ||
- (c = '5') || (c = '6') || (c = '7') || (c = '8') || (c = '9')
-
(* We recognize if the variable is FO (x, y) or MSO (X, Y) or Real (r1, r2). *)
let var_of_string s : var =
- if String.length s = 0 then failwith "empty strings not allowed as vars"
- else if s.[0] = ':' then `Real s
- else if ((Char.uppercase s.[0]) = s.[0]) && (not (is_digit s.[0])) then `MSO s
+ if String.length s = 0 then
+ failwith "empty strings not allowed as vars"
+ else if s.[0] = ':' then
+ `Real s
+ else if ((Char.uppercase s.[0]) = s.[0]) && (not (Aux.is_digit s.[0])) then
+ `MSO s
else `FO s
let fo_var_of_string s : fo_var =
Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml 2010-11-27 14:29:19 UTC (rev 1196)
+++ trunk/Toss/Formula/FormulaOps.ml 2010-11-27 20:55:24 UTC (rev 1197)
@@ -205,13 +205,21 @@
let new_vs = List.filter (fun x -> not (in_vs x)) subst in
if new_vs = [] then Sum(vs, phi, r) else Sum(vs, subst_vars new_vs phi, r)
+(* Helper function: strip digits from string end except if it starts with one. *)
+let rec strip_digits s =
+ if Aux.is_digit s.[0] then s else
+ let len = String.length s in
+ if Aux.is_digit s.[len-1] then
+ strip_digits (String.sub s 0 (len-1))
+ else s
+
(* Find a substitution for [v] which avoids [avs]. *)
let subst_name_avoiding avoidv var =
- let (avs, v) = (List.rev_map var_str avoidv, var_str var) in
+ let (avs, v) = (List.rev_map var_str avoidv, strip_digits (var_str var)) in
let rec asubst i =
let vi = v ^ (string_of_int i) in
- if not (List.mem vi avs) then (v, vi) else asubst (i+1) in
- if List.mem v avs then asubst 0 else (v, v)
+ if not (List.mem vi avs) then (var_str var, vi) else asubst (i+1) in
+ if List.mem v avs then asubst 0 else (var_str var, v)
(** Rename quantified variables avoiding the ones from [avs],
and the above-quantified ones. Does not go into real_expr. *)
@@ -225,7 +233,7 @@
if avoidv = [] then Ex (vs, rename_quant_avoiding (avs @ vs) phi) else
let subst = List.map (subst_name_avoiding avs) avoidv in
let nvs = okv @ (List.map var_of_string (snd (List.split subst))) in
- Ex (nvs, rename_quant_avoiding (avs @ nvs) (subst_vars subst phi))
+ Ex (nvs, subst_vars subst (rename_quant_avoiding (avs @ nvs) phi))
| All (vs, phi) ->
let (avoidv, okv) = List.partition (fun v -> List.mem v avs) vs in
if avoidv = [] then All (vs, rename_quant_avoiding (avs @ vs) phi) else
@@ -233,7 +241,16 @@
let nvs = okv @ (List.map var_of_string (snd (List.split subst))) in
All (nvs, rename_quant_avoiding (avs @ nvs) (subst_vars subst phi))
+(* Apply substitution [subst] to all free variables in the given formula
+ checking for and preventing name clashes with quantified variables. *)
+let subst_vars_check subst phi =
+ let nvars = List.map (fun (_, nv) -> var_of_string nv) subst in
+ let avoidvars = List.rev_append (free_vars phi) nvars in
+ subst_vars subst (rename_quant_avoiding avoidvars phi)
+let subst_vars_nocheck subst phi = subst_vars subst phi
+
+
(* --------------------------- TRANSITIVE CLOSURE --------------------------- *)
(* We construct transitive closure of phi(x, y, z) over x, y as
@@ -245,14 +262,23 @@
let (_, ny) = subst_name_avoiding fv yv in
let (nxv, nyv) = (fo_var_of_string nx, fo_var_of_string ny) in
let frX = mso_var_of_string(snd(subst_name_avoiding fv(var_of_string "X"))) in
- let nphi = subst_vars [(x, nx); (y, ny)] phi in
+ let nphi = subst_vars_check [(x, nx); (y, ny)] phi in
let impphi = Or [Not (And [In (nxv, frX); nphi]); In (nyv, frX)] in
let inphi = And [In (xv, frX); All (([nxv; nyv] :> var list), impphi)] in
All ([(frX :> var)], Or [Not inphi; In (yv, frX)])
+(* First-order [k]-step refl. transitive closure of [phi] over [x] and [y]. *)
+let rec make_fo_tc k x y phi =
+ let (xv, yv) = (fo_var_of_string x, fo_var_of_string y) in
+ if k = 0 then Eq (xv, yv) else if k = 1 then Or [Eq (xv, yv); phi] else
+ let (fv, k1, k2) = (free_vars phi, k / 2, k - (k / 2)) in
+ let (_, t) = subst_name_avoiding fv (var_of_string "t") in
+ let (phi1, phi2) = (make_fo_tc k1 x y phi, make_fo_tc k2 x y phi) in
+ let (phi1s, phi2s) =
+ (subst_vars_check [(y,t)] phi1, subst_vars_check [(x,t)] phi2) in
+ Ex ([var_of_string t], And [phi1s; phi2s])
-
(* --------- SUBSTITUTE DEFINED RELATIONS ------------ *)
(* Substitute in relations defined in [defs] by their definitions. *)
Modified: trunk/Toss/Formula/FormulaOps.mli
===================================================================
--- trunk/Toss/Formula/FormulaOps.mli 2010-11-27 14:29:19 UTC (rev 1196)
+++ trunk/Toss/Formula/FormulaOps.mli 2010-11-27 20:55:24 UTC (rev 1197)
@@ -35,7 +35,12 @@
(* Apply substitution [subst] to all free variables in the given
formula. Preserves order of subformulas. *)
val subst_vars : (string * string) list -> formula -> formula
+val subst_vars_nocheck : (string * string) list -> formula -> formula
+(* Apply substitution [subst] to all free variables in the given formula
+ checking for and preventing name clashes with quantified variables. *)
+val subst_vars_check : (string * string) list -> formula -> formula
+
(** Rename quantified variables avoiding the ones from [avs] list,
and the above-quantified ones. Does not go into real_expr. *)
val rename_quant_avoiding : var list -> formula -> formula
@@ -55,8 +60,12 @@
(* ------------------------ Transitive Closure ---------------------------- *)
+(* Transitive closure of phi(x, y, z) over x and y, an MSO formula. *)
val make_tc : string -> string -> formula -> formula
+(* First-order [k]-step refl. transitive closure of [phi] over [x] and [y]. *)
+val make_fo_tc : int -> string -> string -> formula -> formula
+
(* -------------------------- Simplification ------------------------------ *)
(* Recursively simplify a formula *)
Modified: trunk/Toss/Formula/FormulaOpsTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaOpsTest.ml 2010-11-27 14:29:19 UTC (rev 1196)
+++ trunk/Toss/Formula/FormulaOpsTest.ml 2010-11-27 20:55:24 UTC (rev 1197)
@@ -15,7 +15,7 @@
let id x = x ;;
-let tests = "Formula" >::: [
+let tests = "FormulaOps" >::: [
"nnf and parsing" >::
(fun () ->
let nnf_eq phi1 phi2 = formula_eq id phi2 FormulaOps.nnf phi1 in
@@ -259,6 +259,17 @@
"R (y, x)" "S(y, x) and ex x0 (S(x, x0))";
);
+ "rename quantified variables" >::
+ (fun () ->
+ let rq_eq vs phi1 phi2 =
+ let avs = List.map Formula.var_of_string vs in
+ formula_eq id phi2 (FormulaOps.rename_quant_avoiding avs) phi1 in
+ rq_eq ["x"] "ex x R(x, y)" "ex x0 R(x0, y)";
+ rq_eq ["x"] "ex y R(x, y)" "ex y R(x, y)";
+ rq_eq ["t"] "ex t ( (x = t or R(x, t)) and ex t0 ( t=t0 or R(t, t0) ))"
+ "ex t0 ( (x = t0 or R(x, t0)) and ex t1 ((t0 = t1 or R(t0, t1)) ))";
+ );
+
"transitive closure creation" >::
(fun () ->
let tc_eq x y phi1 phi2 =
@@ -268,6 +279,18 @@
tc_eq "x" "y" "R(x, y) and x in X" "all X0 (x in X0 and (all x0,y0
(x0 in X0 and (R(x0,y0) and x0 in X) -> y0 in X0)) -> y in X0)";
);
+
+ "first-order transitive closure creation" >::
+ (fun () ->
+ let tc_eq k x y phi1 phi2 =
+ formula_eq id phi2 (FormulaOps.make_fo_tc k x y) phi1 in
+ tc_eq 2 "x" "y" "R(x, y)" "ex t((x=t or R(x,t)) and (t=y or R(t,y)))";
+ tc_eq 3 "x" "y" "R(x, y, t)" "ex t0 ( (x = t0 or R(x, t0, t)) and
+ ex t1 ( (t0 = t1 or R(t0, t1, t)) and (t1 = y or R(t1, y, t)) ) )";
+ tc_eq 5 "x" "y" "R(x, y)" "ex t ( ex t0 ( ((x = t0) or R(x, t0)) and
+ ((t0 = t) or R(t0, t)) ) and ex t0( ((t = t0) or R(t, t0)) and ex t1 (
+ (t0 = t1 or R(t0, t1)) and (t1 = y or R(t1, y)) )))";
+ );
] ;;
let a =
Modified: trunk/Toss/Formula/FormulaParser.mly
===================================================================
--- trunk/Toss/Formula/FormulaParser.mly 2010-11-27 14:29:19 UTC (rev 1196)
+++ trunk/Toss/Formula/FormulaParser.mly 2010-11-27 20:55:24 UTC (rev 1197)
@@ -77,6 +77,7 @@
| EX var_list formula_expr { Ex ($2, $3) }
| ALL var_list formula_expr { All ($2, $3) }
| TC ID COMMA ID formula_expr { FormulaOps.make_tc $2 $4 $5 }
+ | TC INT ID COMMA ID formula_expr { FormulaOps.make_fo_tc $2 $3 $5 $6 }
| OPEN formula_expr CLOSE { $2 }
| formula_expr AND formula_expr { And [$1; $3] }
| formula_expr OR formula_expr { Or [$1; $3] }
Modified: trunk/Toss/Solver/SolverTest.ml
===================================================================
--- trunk/Toss/Solver/SolverTest.ml 2010-11-27 14:29:19 UTC (rev 1196)
+++ trunk/Toss/Solver/SolverTest.ml 2010-11-27 20:55:24 UTC (rev 1197)
@@ -26,19 +26,19 @@
let f = register_formula solver phi in
res := AssignmentSet.str (evaluate solver f struc);
);
- assert_equal ~printer:(fun x -> x) !res aset_s
+ assert_equal ~printer:(fun x -> x) aset_s !res
;;
let eval_real_eq var_s struc_s expr_s aset_s =
let (struc, expr) = (struc_of_string struc_s, real_expr_of_string expr_s) in
assert_equal ~printer:(fun x -> x)
- (AssignmentSet.str (evaluate_real var_s expr struc)) aset_s
+ aset_s (AssignmentSet.str (evaluate_real var_s expr struc))
;;
let real_val_eq struc_s expr_s x =
let (struc, expr) = (struc_of_string struc_s, real_expr_of_string expr_s) in
assert_equal ~printer:(fun x -> string_of_float x)
- (get_real_val (new_solver ()) AssignmentSet.Any expr struc) x
+ x (get_real_val (new_solver ()) AssignmentSet.Any expr struc)
;;
@@ -112,16 +112,25 @@
"eval: mso with quantifiers" >::
(fun () ->
- let reach_f = "tc x, y R(x, y)" in
- eval_eq "[ | R { (a, b); (a, c) } | ]" reach_f
+ eval_eq "[ | R { (a, b); (a, c) } | ]" "tc x, y R(x, y)"
"{ y->1{ x->1 } , y->2{ x->1, x->2 } , y->3{ x->1, x->3 } }";
- eval_eq "[ | R { (a, b); (b, c) } | ]" reach_f
- "{ y->1{ x->1 } , y->2{ x->1, x->2 } , y->3 }";
+ eval_eq "[ | R { (a, b); (b, c) } | ]" "tc x, y R(x, y)"
+ "{ y->1{ x->1 } , y->2{ x->1, x->2 } , y->3 }";
eval_eq "[ | R { (a,b); (b,c); (c,d); (d,e); (e,f); (f,g); (g,h) } | ]"
- ("x != y and not R(x, y) and " ^ reach_f)
+ "x != y and not R(x, y) and tc x, y R(x, y)"
("{ y->3{ x->1 } , y->4{ x->1, x->2 } , y->5{ x->1, x->2, x->3 } ," ^
" y->6{ x->1, x->2, x->3, x->4 } , y->7{ x->1, x->2, x->3, x->4," ^
" x->5 } , y->8{ x->1, x->2, x->3, x->4, x->5, x->6 } }");
+ eval_eq "[ | R { (a,b); (b,c); (c,d); (d,e); (e,f); (f,g); (g,h) } | ]"
+ "x != y and not R(x, y) and tc 4 x, y R(x, y)"
+ ("{ y->3{ x->1 } , y->4{ x->1, x->2 } , y->5{ x->1, x->2, x->3 } ," ^
+ " y->6{ x->2, x->3, x->4 } , y->7{ x->3, x->4," ^
+ " x->5 } , y->8{ x->4, x->5, x->6 } }");
+ eval_eq "[ | R { (a,b); (b,c); (c,d); (d,e); (e,f); (f,g); (g,h) } | ]"
+ "x != y and not R(x, y) and tc 7 x, y R(x, y)"
+ ("{ y->3{ x->1 } , y->4{ x->1, x->2 } , y->5{ x->1, x->2, x->3 } ," ^
+ " y->6{ x->1, x->2, x->3, x->4 } , y->7{ x->1, x->2, x->3, x->4," ^
+ " x->5 } , y->8{ x->1, x->2, x->3, x->4, x->5, x->6 } }");
);
"eval: with real values" >::
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <luk...@us...> - 2010-11-27 14:29:25
|
Revision: 1196
http://toss.svn.sourceforge.net/toss/?rev=1196&view=rev
Author: lukaszkaiser
Date: 2010-11-27 14:29:19 +0000 (Sat, 27 Nov 2010)
Log Message:
-----------
Transitive closure syntax.
Modified Paths:
--------------
trunk/Toss/Formula/FormulaOps.ml
trunk/Toss/Formula/FormulaOps.mli
trunk/Toss/Formula/FormulaOpsTest.ml
trunk/Toss/Formula/FormulaParser.mly
trunk/Toss/Formula/Lexer.mll
trunk/Toss/Formula/Tokens.mly
trunk/Toss/Solver/SolverTest.ml
trunk/Toss/examples/Tic-Tac-Toe.tossstyle
Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml 2010-11-24 00:34:10 UTC (rev 1195)
+++ trunk/Toss/Formula/FormulaOps.ml 2010-11-27 14:29:19 UTC (rev 1196)
@@ -234,7 +234,25 @@
All (nvs, rename_quant_avoiding (avs @ nvs) (subst_vars subst phi))
+(* --------------------------- TRANSITIVE CLOSURE --------------------------- *)
+(* We construct transitive closure of phi(x, y, z) over x, y as
+ "all X (x in X and (all x',y'
+ (x' in X and phi(x',y',z)-> y' in X)) -> y in X)" *)
+let make_tc x y phi =
+ let (fv, xv, yv) = (free_vars phi, fo_var_of_string x, fo_var_of_string y) in
+ let (_, nx) = subst_name_avoiding fv xv in
+ let (_, ny) = subst_name_avoiding fv yv in
+ let (nxv, nyv) = (fo_var_of_string nx, fo_var_of_string ny) in
+ let frX = mso_var_of_string(snd(subst_name_avoiding fv(var_of_string "X"))) in
+ let nphi = subst_vars [(x, nx); (y, ny)] phi in
+ let impphi = Or [Not (And [In (nxv, frX); nphi]); In (nyv, frX)] in
+ let inphi = And [In (xv, frX); All (([nxv; nyv] :> var list), impphi)] in
+ All ([(frX :> var)], Or [Not inphi; In (yv, frX)])
+
+
+
+
(* --------- SUBSTITUTE DEFINED RELATIONS ------------ *)
(* Substitute in relations defined in [defs] by their definitions. *)
Modified: trunk/Toss/Formula/FormulaOps.mli
===================================================================
--- trunk/Toss/Formula/FormulaOps.mli 2010-11-24 00:34:10 UTC (rev 1195)
+++ trunk/Toss/Formula/FormulaOps.mli 2010-11-27 14:29:19 UTC (rev 1196)
@@ -53,6 +53,10 @@
val assign_emptyset : string -> formula -> formula
+(* ------------------------ Transitive Closure ---------------------------- *)
+
+val make_tc : string -> string -> formula -> formula
+
(* -------------------------- Simplification ------------------------------ *)
(* Recursively simplify a formula *)
Modified: trunk/Toss/Formula/FormulaOpsTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaOpsTest.ml 2010-11-24 00:34:10 UTC (rev 1195)
+++ trunk/Toss/Formula/FormulaOpsTest.ml 2010-11-27 14:29:19 UTC (rev 1196)
@@ -258,6 +258,16 @@
[("R", (["x"; "y"], formula_of_string "S (x, y) and ex x S(y, x)"))]
"R (y, x)" "S(y, x) and ex x0 (S(x, x0))";
);
+
+ "transitive closure creation" >::
+ (fun () ->
+ let tc_eq x y phi1 phi2 =
+ formula_eq id phi2 (FormulaOps.make_tc x y) phi1 in
+ tc_eq "x" "y" "R(x, y)" "all X (x in X and (all x0,y0
+ (x0 in X and R(x0,y0) -> y0 in X)) -> y in X)";
+ tc_eq "x" "y" "R(x, y) and x in X" "all X0 (x in X0 and (all x0,y0
+ (x0 in X0 and (R(x0,y0) and x0 in X) -> y0 in X0)) -> y in X0)";
+ );
] ;;
let a =
Modified: trunk/Toss/Formula/FormulaParser.mly
===================================================================
--- trunk/Toss/Formula/FormulaParser.mly 2010-11-24 00:34:10 UTC (rev 1195)
+++ trunk/Toss/Formula/FormulaParser.mly 2010-11-27 14:29:19 UTC (rev 1196)
@@ -76,6 +76,7 @@
| NOT formula_expr { Not ($2) }
| EX var_list formula_expr { Ex ($2, $3) }
| ALL var_list formula_expr { All ($2, $3) }
+ | TC ID COMMA ID formula_expr { FormulaOps.make_tc $2 $4 $5 }
| OPEN formula_expr CLOSE { $2 }
| formula_expr AND formula_expr { And [$1; $3] }
| formula_expr OR formula_expr { Or [$1; $3] }
Modified: trunk/Toss/Formula/Lexer.mll
===================================================================
--- trunk/Toss/Formula/Lexer.mll 2010-11-24 00:34:10 UTC (rev 1195)
+++ trunk/Toss/Formula/Lexer.mll 2010-11-27 14:29:19 UTC (rev 1196)
@@ -1,21 +1,4 @@
{
-(* Tokens for parsers: must be in the same order as the type def. below.
-%token <string> ID
-%token <int> INT
-%token <float> FLOAT
-%token <string> BOARD_STRING
-%token APOSTROPHE
-%token COLON SEMICOLON COMMA MID
-%token SUM PLUS MINUS TIMES DIV POW GR GREQ LT EQLT EQ LTGR NEQ
-%token LARR LDARR RARR RDARR LRARR LRDARR INTERV
-%token OPENCUR CLOSECUR OPENSQ CLOSESQ OPEN CLOSE
-%token IN AND OR XOR NOT EX ALL
-%token WITH EMB PRE INV POST UPDATE DYNAMICS TRUE FALSE ASSOC COND PAYOFF MOVES
-%token ADD_CMD DEL_CMD GET_CMD SET_CMD EVAL_CMD
-%token ELEM_MOD REL_MOD ALLOF_MOD SIG_MOD FUN_MOD DATA_MOD LOC_MOD TIMEOUT_MOD TIME_MOD PLAYER_MOD PLAYERS_MOD
-%token MODEL_SPEC RULE_SPEC STATE_SPEC LEFT_SPEC RIGHT_SPEC EOF
-*)
-
type token =
| ID of (string)
| INT of (int)
@@ -59,6 +42,7 @@
| NOT
| EX
| ALL
+ | TC
| WITH
| EMB
| PRE
@@ -174,6 +158,8 @@
| "not" { NOT }
| "ex" { EX }
| "all" { ALL }
+ | "tc" { TC }
+ | "TC" { TC }
| "with" { WITH }
| "emb" { EMB }
| "pre" { PRE }
Modified: trunk/Toss/Formula/Tokens.mly
===================================================================
--- trunk/Toss/Formula/Tokens.mly 2010-11-24 00:34:10 UTC (rev 1195)
+++ trunk/Toss/Formula/Tokens.mly 2010-11-27 14:29:19 UTC (rev 1196)
@@ -7,7 +7,7 @@
%token SUM PLUS MINUS TIMES DIV POW GR GREQ LT EQLT EQ LTGR NEQ
%token LARR LDARR RARR RDARR LRARR LRDARR INTERV
%token OPENCUR CLOSECUR OPENSQ CLOSESQ OPEN CLOSE
-%token IN AND OR XOR NOT EX ALL
+%token IN AND OR XOR NOT EX ALL TC
%token WITH EMB PRE INV POST UPDATE DYNAMICS TRUE FALSE ASSOC COND PAYOFF MOVES
%token ADD_CMD DEL_CMD GET_CMD SET_CMD EVAL_CMD
%token ELEM_MOD REL_MOD ALLOF_MOD SIG_MOD FUN_MOD DATA_MOD LOC_MOD TIMEOUT_MOD TIME_MOD PLAYER_MOD PLAYERS_MOD
Modified: trunk/Toss/Solver/SolverTest.ml
===================================================================
--- trunk/Toss/Solver/SolverTest.ml 2010-11-24 00:34:10 UTC (rev 1195)
+++ trunk/Toss/Solver/SolverTest.ml 2010-11-27 14:29:19 UTC (rev 1196)
@@ -112,8 +112,7 @@
"eval: mso with quantifiers" >::
(fun () ->
- let reach_f =
- "all X (x in X and (all z,v (z in X and R(z,v)-> v in X))-> y in X)" in
+ let reach_f = "tc x, y R(x, y)" in
eval_eq "[ | R { (a, b); (a, c) } | ]" reach_f
"{ y->1{ x->1 } , y->2{ x->1, x->2 } , y->3{ x->1, x->3 } }";
eval_eq "[ | R { (a, b); (b, c) } | ]" reach_f
Modified: trunk/Toss/examples/Tic-Tac-Toe.tossstyle
===================================================================
--- trunk/Toss/examples/Tic-Tac-Toe.tossstyle 2010-11-24 00:34:10 UTC (rev 1195)
+++ trunk/Toss/examples/Tic-Tac-Toe.tossstyle 2010-11-27 14:29:19 UTC (rev 1196)
@@ -1,6 +1,6 @@
nocolor ;
elOPACITY: 30 ;
relOPACITY: 150 ;
-arrLENscale: 0.1 ;
+arrLENscale: 0 ;
P: ~/greencircle.svg;
Q: ~/cross.svg;
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <luk...@us...> - 2010-11-24 00:34:16
|
Revision: 1195
http://toss.svn.sourceforge.net/toss/?rev=1195&view=rev
Author: lukaszkaiser
Date: 2010-11-24 00:34:10 +0000 (Wed, 24 Nov 2010)
Log Message:
-----------
Correcting solver cache gives significant speed improvement. Added profiling targets.
Modified Paths:
--------------
trunk/Toss/.cvsignore
trunk/Toss/Arena/.cvsignore
trunk/Toss/Formula/.cvsignore
trunk/Toss/Makefile
trunk/Toss/Play/.cvsignore
trunk/Toss/Solver/.cvsignore
trunk/Toss/Solver/Solver.ml
Property Changed:
----------------
trunk/Toss/
trunk/Toss/Arena/
trunk/Toss/Formula/
trunk/Toss/Play/
trunk/Toss/Solver/
Property changes on: trunk/Toss
___________________________________________________________________
Modified: svn:ignore
- # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
# svn propset svn:ignore -F .cvsignore .
Toss.docdir
_build
Server
*.native
*~
*.annot
*.cmx
*.cmi
*.o
*.cmo
*.a
*.cmxa
log.*
+ # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
# svn propset svn:ignore -F .cvsignore .
Toss.docdir
_build
Server
*.native
*Profile.log
gmon.out
*~
*.annot
*.cmx
*.cmi
*.o
*.cmo
*.a
*.cmxa
log.*
Modified: trunk/Toss/.cvsignore
===================================================================
--- trunk/Toss/.cvsignore 2010-11-23 11:20:21 UTC (rev 1194)
+++ trunk/Toss/.cvsignore 2010-11-24 00:34:10 UTC (rev 1195)
@@ -6,6 +6,8 @@
_build
Server
*.native
+*Profile.log
+gmon.out
*~
*.annot
*.cmx
Property changes on: trunk/Toss/Arena
___________________________________________________________________
Modified: svn:ignore
- # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
# svn propset svn:ignore -F .cvsignore .
*~
+ # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
# svn propset svn:ignore -F .cvsignore .
*Profile.log
*~
Modified: trunk/Toss/Arena/.cvsignore
===================================================================
--- trunk/Toss/Arena/.cvsignore 2010-11-23 11:20:21 UTC (rev 1194)
+++ trunk/Toss/Arena/.cvsignore 2010-11-24 00:34:10 UTC (rev 1195)
@@ -2,4 +2,5 @@
# than svn properties. Therefore if you change .cvsignore do the following.
# svn propset svn:ignore -F .cvsignore .
+*Profile.log
*~
Property changes on: trunk/Toss/Formula
___________________________________________________________________
Modified: svn:ignore
- # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
# svn propset svn:ignore -F .cvsignore .
*~
+ # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
# svn propset svn:ignore -F .cvsignore .
*Profile.log
*~
Modified: trunk/Toss/Formula/.cvsignore
===================================================================
--- trunk/Toss/Formula/.cvsignore 2010-11-23 11:20:21 UTC (rev 1194)
+++ trunk/Toss/Formula/.cvsignore 2010-11-24 00:34:10 UTC (rev 1195)
@@ -2,4 +2,5 @@
# than svn properties. Therefore if you change .cvsignore do the following.
# svn propset svn:ignore -F .cvsignore .
+*Profile.log
*~
Modified: trunk/Toss/Makefile
===================================================================
--- trunk/Toss/Makefile 2010-11-23 11:20:21 UTC (rev 1194)
+++ trunk/Toss/Makefile 2010-11-24 00:34:10 UTC (rev 1195)
@@ -71,6 +71,11 @@
%TestDebug: %Test.d.byte
OCAMLRUNPARAM=b; export OCAMLRUNPARAM; _build/$<
+%TestProfile: %Test.p.native
+ _build/$<
+ gprof _build/$< > $@.log
+
+
# Formula tests
Formula_tests: \
Formula/AuxTest \
Property changes on: trunk/Toss/Play
___________________________________________________________________
Modified: svn:ignore
- # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
# svn propset svn:ignore -F .cvsignore .
*~
+ # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
# svn propset svn:ignore -F .cvsignore .
*~
*Profile.log
Modified: trunk/Toss/Play/.cvsignore
===================================================================
--- trunk/Toss/Play/.cvsignore 2010-11-23 11:20:21 UTC (rev 1194)
+++ trunk/Toss/Play/.cvsignore 2010-11-24 00:34:10 UTC (rev 1195)
@@ -2,4 +2,5 @@
# than svn properties. Therefore if you change .cvsignore do the following.
# svn propset svn:ignore -F .cvsignore .
+*Profile.log
*~
Property changes on: trunk/Toss/Solver
___________________________________________________________________
Modified: svn:ignore
- # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
# svn propset svn:ignore -F .cvsignore .
*~
+ # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
# svn propset svn:ignore -F .cvsignore .
*Profile.log
*~
Modified: trunk/Toss/Solver/.cvsignore
===================================================================
--- trunk/Toss/Solver/.cvsignore 2010-11-23 11:20:21 UTC (rev 1194)
+++ trunk/Toss/Solver/.cvsignore 2010-11-24 00:34:10 UTC (rev 1195)
@@ -2,4 +2,5 @@
# than svn properties. Therefore if you change .cvsignore do the following.
# svn propset svn:ignore -F .cvsignore .
+*Profile.log
*~
Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml 2010-11-23 11:20:21 UTC (rev 1194)
+++ trunk/Toss/Solver/Solver.ml 2010-11-24 00:34:10 UTC (rev 1195)
@@ -11,14 +11,13 @@
(* CACHE *)
let cache_struc = ref (empty_structure ())
-let cache_results = ref []
-let cCACHESIZE = ref 50
+let cache_results = Hashtbl.create 15;
(* ----------------------- BASIC TYPE DEFINITION -------------------------- *)
type solver = {
- reg_formulas : (Formula.formula * int) list ref ;
+ reg_formulas : (Formula.formula, int) Hashtbl.t ;
formulas_eval : (int, Formula.formula) Hashtbl.t ;
formulas_check : (int, Formula.formula) Hashtbl.t ;
}
@@ -27,7 +26,7 @@
(* ----------------------- CONSTRUCTOR FUNCTIONS -------------------------- *)
let new_solver () = {
- reg_formulas = ref [] ;
+ reg_formulas = Hashtbl.create 3 ;
formulas_eval = Hashtbl.create 3 ;
formulas_check = Hashtbl.create 3 ;
}
@@ -36,16 +35,16 @@
let rec check_form = function
Ex (vs, phi) -> check_form phi
| phi -> phi in
- let psi = FormulaOps.tnf_fv phi in
try
- let res = List.assoc psi !(solver.reg_formulas) in
+ let res = Hashtbl.find solver.reg_formulas phi in
if !debug_level > 0 then print_endline ("Found " ^ (str phi));
res
with Not_found ->
+ let psi = FormulaOps.tnf_fv phi in
if !debug_level > 0 then print_endline ("Entered " ^ (str phi));
if !debug_level > 0 then print_endline ("Registering " ^ (str psi));
let id = Hashtbl.length solver.formulas_eval + 1 in
- solver.reg_formulas := (psi, id) :: !(solver.reg_formulas);
+ Hashtbl.add solver.reg_formulas phi id;
Hashtbl.add solver.formulas_eval id psi;
Hashtbl.add solver.formulas_check id (check_form psi);
id
@@ -193,23 +192,21 @@
let els = Set (Elems.cardinal struc.elements, struc.elements) in
let asg = eval struc (ref els) Any phi in
cache_struc := struc;
- cache_results := [(phi, asg)];
+ Hashtbl.clear cache_results;
+ Hashtbl.add cache_results phi asg;
asg
) else
try
- let (res, new_cache) = assoc_del phi !cache_results in
- cache_results := (phi, res) :: new_cache;
+ let res = Hashtbl.find cache_results phi in
if !debug_level > 1 then (
print_endline ("found in cache: " ^ (Formula.str phi));
- print_endline ("size: "^ (string_of_int (List.length !cache_results)));
);
res
with Not_found ->
if !debug_level > 0 then print_endline ("Eval_m " ^ (str phi));
- if List.length !cache_results > !cCACHESIZE then cache_results := [];
let els = Set (Elems.cardinal struc.elements, struc.elements) in
let asg = eval struc (ref els) Any phi in
- cache_results := (phi, asg) :: !cache_results;
+ Hashtbl.add cache_results phi asg;
asg
(* Helper function, assignment of tuple. *)
@@ -234,7 +231,7 @@
let eval_cache_sentences solver struc in_phi =
let reg_tnf phi =
try
- let phi_id = List.assoc phi !(solver.reg_formulas) in
+ let phi_id = Hashtbl.find solver.reg_formulas phi in
Hashtbl.find solver.formulas_eval phi_id
with Not_found ->
Hashtbl.find solver.formulas_eval (register_formula solver phi) in
@@ -257,7 +254,7 @@
| f -> eval_no_fv f in
let phi = subst_no_fv in_phi in
let proc_phi = reg_tnf phi in
- if !debug_level > 0 then (
+ if !debug_level > 1 then (
print_endline ("in phi: " ^ (Formula.str in_phi));
print_endline ("phi: " ^ (Formula.str phi));
print_endline ("proc phi: " ^ (Formula.str proc_phi));
@@ -283,9 +280,9 @@
print_endline ("sum vars " ^ (Formula.var_list_str vl));
print_endline ("all vars " ^ (Formula.var_list_str all_vs));
);
- let gd = FFTNF.ff_tnf (FFSolver.promote_for struc) guard in
- let asg_gd = join asg (FFSolver.evaluate struc gd) in
- (* let asg_gd = join asg (eval_cache_sentences solver struc guard) in *)
+ (* let gd = FFTNF.ff_tnf (FFSolver.promote_for struc) guard in
+ let asg_gd = join asg (FFSolver.evaluate struc gd) in *)
+ let asg_gd = join asg (eval_cache_sentences solver struc guard) in
let tps = tuples struc.elements (List.map var_str all_vs) asg_gd in
let add_val acc tp =
let tp_asg = asg_of_tuple struc all_vs tp in
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <luk...@us...> - 2010-11-23 11:20:28
|
Revision: 1194
http://toss.svn.sourceforge.net/toss/?rev=1194&view=rev
Author: lukaszkaiser
Date: 2010-11-23 11:20:21 +0000 (Tue, 23 Nov 2010)
Log Message:
-----------
Back to FFSolver eval for profiling.
Modified Paths:
--------------
trunk/Toss/Makefile
trunk/Toss/Solver/Solver.ml
Modified: trunk/Toss/Makefile
===================================================================
--- trunk/Toss/Makefile 2010-11-23 09:56:32 UTC (rev 1193)
+++ trunk/Toss/Makefile 2010-11-23 11:20:21 UTC (rev 1194)
@@ -48,6 +48,11 @@
caml_extensions/pa_let_try.cmo caml_extensions/pa_backtrace.cmo
$(OCAMLBUILD) -Is $($(subst /,INC,$(dir $@))) $@
+%.p.native: %.ml \
+ Formula/Sat/minisat/SatSolver.o Formula/Sat/minisat/MiniSATWrap.o \
+ caml_extensions/pa_let_try.cmo caml_extensions/pa_backtrace.cmo
+ $(OCAMLBUILD) -Is $($(subst /,INC,$(dir $@))) $@
+
%.d.byte: %.ml \
Formula/Sat/minisat/SatSolver.o Formula/Sat/minisat/MiniSATWrap.o \
caml_extensions/pa_let_try.cmo caml_extensions/pa_backtrace.cmo
Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml 2010-11-23 09:56:32 UTC (rev 1193)
+++ trunk/Toss/Solver/Solver.ml 2010-11-23 11:20:21 UTC (rev 1194)
@@ -283,7 +283,9 @@
print_endline ("sum vars " ^ (Formula.var_list_str vl));
print_endline ("all vars " ^ (Formula.var_list_str all_vs));
);
- let asg_gd = join asg (eval_cache_sentences solver struc guard) in
+ let gd = FFTNF.ff_tnf (FFSolver.promote_for struc) guard in
+ let asg_gd = join asg (FFSolver.evaluate struc gd) in
+ (* let asg_gd = join asg (eval_cache_sentences solver struc guard) in *)
let tps = tuples struc.elements (List.map var_str all_vs) asg_gd in
let add_val acc tp =
let tp_asg = asg_of_tuple struc all_vs tp in
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <luk...@us...> - 2010-11-23 09:56:39
|
Revision: 1193
http://toss.svn.sourceforge.net/toss/?rev=1193&view=rev
Author: lukstafi
Date: 2010-11-23 09:56:32 +0000 (Tue, 23 Nov 2010)
Log Message:
-----------
Alpha-beta bug fix. adv_ratio lowered to 2.
Modified Paths:
--------------
trunk/Toss/Client/Wrapper.py
trunk/Toss/Play/Game.ml
trunk/Toss/Play/GameTest.ml
Modified: trunk/Toss/Client/Wrapper.py
===================================================================
--- trunk/Toss/Client/Wrapper.py 2010-11-23 01:44:43 UTC (rev 1192)
+++ trunk/Toss/Client/Wrapper.py 2010-11-23 09:56:32 UTC (rev 1193)
@@ -396,7 +396,7 @@
# "EVAL LOC MOVES advancement_ratio location TIMEOUT time_in_sec iters_or_depth_limit method optional_playout_horizon"
# syntax variant 2:
# "EVAL LOC MOVES [{0: heuristic_player_0_loc_0; 1: heuristic_player_1_loc_0}; {0: heuristic_player_0_loc_1; 1: heuristic_player_1_loc_1}] advancement_ratio location TIMEOUT time_in_sec iters_or_depth_limit method optional_playout_horizon"
- m = self.msg ("EVAL LOC MOVES 5.0 " + str(loc) +" TIMEOUT 1200 "+ str(no_iters) + " alpha_beta_ord")
+ m = self.msg ("EVAL LOC MOVES 2.0 " + str(loc) +" TIMEOUT 1200 "+ str(no_iters) + " alpha_beta_ord")
self.set_time (ts, t)
msg = [s.strip() for s in m.split(';')]
emb = dict()
Modified: trunk/Toss/Play/Game.ml
===================================================================
--- trunk/Toss/Play/Game.ml 2010-11-23 01:44:43 UTC (rev 1192)
+++ trunk/Toss/Play/Game.ml 2010-11-23 09:56:32 UTC (rev 1193)
@@ -225,8 +225,7 @@
cooperative = false ;
}
-(* At least 5th degree monotonic heuristic needed for Gomoku. *)
-let default_adv_ratio = 5.0
+let default_adv_ratio = 2.0
let default_heuristic ?struc advance_ratio
@@ -736,7 +735,8 @@
let state = models.(pos) in
let sub_heur =
maximax_tree player new_betas (depth-1) state in
- if now_pruning && sub_heur.(player) >= betas.(player)
+ (* note strong inequality: don't lose ordering info *)
+ if now_pruning && sub_heur.(player) > betas.(player)
then (
(* {{{ log entry *)
if !debug_level > 2 && (depth0 > 2 || !debug_level > 6) &&
Modified: trunk/Toss/Play/GameTest.ml
===================================================================
--- trunk/Toss/Play/GameTest.ml 2010-11-23 01:44:43 UTC (rev 1192)
+++ trunk/Toss/Play/GameTest.ml 2010-11-23 09:56:32 UTC (rev 1193)
@@ -753,7 +753,7 @@
\"" 1 in
(* TODO: replace with easy_case after monotonic heur done *)
easy_case state 1 "Q should block straight"
- (fun mov_s -> "2{1:a1}" = mov_s);
+ (fun mov_s -> "2{1:b1}" = mov_s);
);
"tictactoe suggest win" >::
@@ -845,6 +845,31 @@
easy_case state 0 "W should beat the lower B" (* or medium *)
(fun mov_s -> "3{1:e3, 2:f3, 3:e4, 4:f4}" = mov_s));
+ "breakthrough suggest adv_ratio" >::
+ (fun () ->
+ let state = update_game breakthrough_game
+"[ | | ] \"
+ ... ... ... ...
+ B B..B B..B B..B B..
+ ... ... ... ...
+ B.. ... -B.B B..B
+ ... ... ... ...
+ ... ...+B ... ...
+ ... ... ... ...
+ ...B ... B.. ...
+ ... ... ... ...
+ ... ...W ... ...
+ ... ... ... ...
+ ... ... ... ...
+ ... ... ... ...
+ W W.. W..W W.. W..
+ ... ... ... ...
+ W..W W..W W..W W..W
+\"" 0 in
+ (* white move should beat the lower black *)
+ easy_case state 0 "W should play cool"
+ (fun mov_s -> mov_s <> "3{1:e4, 2:f4, 3:e5, 4:f5}"
+ && mov_s <> "2{1:d4, 2:e4, 3:d5, 4:e5}"));
"gomoku8x8 avoid endgame" >::
@@ -1009,7 +1034,7 @@
);
]
-let a =
+let a =
let file_from_path p =
String.sub p (String.rindex p '/'+1)
(String.length p - String.rindex p '/' - 1) in
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <luk...@us...> - 2010-11-23 01:44:52
|
Revision: 1192
http://toss.svn.sourceforge.net/toss/?rev=1192&view=rev
Author: lukaszkaiser
Date: 2010-11-23 01:44:43 +0000 (Tue, 23 Nov 2010)
Log Message:
-----------
Optimizing evaluation order in solver.
Modified Paths:
--------------
trunk/Toss/Formula/FormulaOps.ml
trunk/Toss/Solver/Assignments.ml
trunk/Toss/Solver/Solver.ml
trunk/Toss/Solver/SolverTest.ml
Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml 2010-11-22 21:18:46 UTC (rev 1191)
+++ trunk/Toss/Formula/FormulaOps.ml 2010-11-23 01:44:43 UTC (rev 1192)
@@ -685,6 +685,16 @@
| Or fl -> Or (List.rev_map unprotect fl)
| phi -> phi
+(* Choose a variable from [vs] to put topmost for [phi]. *)
+let pick_var phi (vs : var list) =
+ let rec has_pos_pred v = function (* Simple positive-predicate heuristic. *)
+ | Rel (_, [|w|]) when v = (w :> var) -> true
+ | And fl | Or fl -> List.exists (has_pos_pred v) fl
+ | _ -> false in
+ let (posp, other) = List.partition (fun v -> has_pos_pred v phi) vs in
+ if posp = [] then (List.hd other, List.tl other) else
+ (List.hd posp, (List.tl posp) @ other)
+
(* A formula is in TNF if, and only if, it is a boolean combination of formulas
tau of the form: a literal or Ex (xs, boolean combination of tau's) or
All (xs, boolean combination of tau's). One invariant must additionally hold:
@@ -709,7 +719,9 @@
let dnf_phi = List.rev_map unand conv_phi in
if !debug_level_tnf > 0 then print_endline ("TNF done: "^ (var_str x));
Or (List.rev_map (append_quant [x] ~universal:false) dnf_phi)
- | Ex (x :: xs, phi) -> tnf_fun (Ex ([x], Ex (xs, phi)))
+ | Ex (vs, phi) ->
+ let (x, xs) = pick_var phi vs in
+ tnf_fun (Ex ([x], Ex (xs, phi)))
| All ([], phi) -> failwith "empty universal when computing TNF"
| All (xs, And fl) -> And (List.rev_map (fun f -> tnf_fun (All (xs, f))) fl)
| All ([x], phi) ->
@@ -723,7 +735,9 @@
let cnf_phi = List.rev_map unor conv_phi in
if !debug_level_tnf > 0 then print_endline ("TNF done: " ^ (var_str x));
And (List.rev_map (append_quant [x] ~universal:true) cnf_phi)
- | All (x :: xs, phi) -> tnf_fun (All ([x], All (xs, phi)))
+ | All (vs, phi) ->
+ let (x, xs) = pick_var phi vs in
+ tnf_fun (All ([x], All (xs, phi)))
and tnf_re_fun = function
RVar _ | Const _ | Fun _ as x -> x
@@ -757,7 +771,30 @@
let tnf_fv phi =
let fv = free_vars phi in
let psi = rename_quant_avoiding [] (Ex (fv, phi)) in
- del_vars_quant fv (tnf psi)
+ let rec order_by_fv acc_fv = function
+ | [] -> []
+ | [f] -> [f]
+ | l ->
+ let cross x = List.exists (fun v -> List.mem v acc_fv) (free_vars x) in
+ let (cf, o) = List.partition cross l in
+ if cf = [] then
+ let new_fv = free_vars (List.hd l) in
+ order_by_fv new_fv (List.map (order_by_fv_phi new_fv) l)
+ else
+ let new_fv = acc_fv @ (free_vars (And cf)) in
+ cf @ (order_by_fv new_fv (List.map (order_by_fv_phi new_fv) o))
+ and order_by_fv_phi acc_fv = function
+ | And fl ->
+ let is_pred = function Rel (_, [|_|]) -> true | _ -> false in
+ let (p, np) = List.partition is_pred fl in
+ let res = And (order_by_fv acc_fv (p @ np)) in
+ if !debug_level > 1 then print_endline ("fvordered: " ^ (str res));
+ res
+ | Ex (vs, phi) -> Ex (vs, order_by_fv_phi acc_fv phi)
+ | f -> f in
+ match flatten (del_vars_quant fv (tnf psi)) with
+ | Or fl -> Or (List.map (order_by_fv_phi []) fl)
+ | f -> f
(* Assign emptyset to the MSO-variable v by replacing "x in X" with "false". *)
let assign_emptyset v phi =
Modified: trunk/Toss/Solver/Assignments.ml
===================================================================
--- trunk/Toss/Solver/Assignments.ml 2010-11-22 21:18:46 UTC (rev 1191)
+++ trunk/Toss/Solver/Assignments.ml 2010-11-23 01:44:43 UTC (rev 1192)
@@ -470,7 +470,8 @@
let aset_tuples =
List.fold_left (fun s (e,_)-> Tuples.union s (tps e)) Tuples.empty map
in
- full_join_rel aset vars aset_tuples all_elems
+ if aset_tuples = Tuples.empty then Empty else
+ full_join_rel aset vars aset_tuples all_elems
| _ -> full_join_rel aset vars tuples_set all_elems
and full_join_rel aset vars tuples_set all_elems =
Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml 2010-11-22 21:18:46 UTC (rev 1191)
+++ trunk/Toss/Solver/Solver.ml 2010-11-23 01:44:43 UTC (rev 1192)
@@ -91,6 +91,7 @@
| Not phi ->
(*A intersect (complement B)=A intersect (complement(B intersect A))*)
report (complement_join elems aset (eval model elems aset phi))
+ | And [] -> aset
| And [phi] -> report (eval model elems aset phi)
| And fl -> report (List.fold_left (eval model elems) aset fl)
| Or [phi] -> report (eval model elems aset phi)
@@ -101,13 +102,13 @@
| Ex ([], phi) | All ([], phi) -> failwith "evaluating empty quantifier"
| Ex (vl, phi) ->
let aset_vars = AssignmentSet.assigned_vars [] aset in
- let in_aset = (* FIXME; TODO; care for same-name quantified vars! *)
+ let in_aset = (* FIXME; TODO; same-name quantified vars?! (tnf_fv!) *)
if List.exists (fun v -> List.mem v aset_vars) vl then Any else aset in
let phi_asgn = eval model elems in_aset phi in
report (join aset (project_list elems phi_asgn vl))
| All (vl, phi) ->
let aset_vars = AssignmentSet.assigned_vars [] aset in
- let in_aset = (* FIXME; TODO; care for same-name quantified vars! *)
+ let in_aset = (* FIXME; TODO; same-name quantified vars?! (tnf_fv!) *)
if List.exists (fun v -> List.mem v aset_vars) vl then Any else aset in
let phi_asgn = eval model elems in_aset phi in
report (join aset (universal_list elems phi_asgn vl))
Modified: trunk/Toss/Solver/SolverTest.ml
===================================================================
--- trunk/Toss/Solver/SolverTest.ml 2010-11-22 21:18:46 UTC (rev 1191)
+++ trunk/Toss/Solver/SolverTest.ml 2010-11-23 01:44:43 UTC (rev 1192)
@@ -19,11 +19,14 @@
;;
let eval_eq struc_s phi_s aset_s =
- let (struc, phi) = (struc_of_string struc_s, formula_of_string phi_s) in
- let solver = new_solver () in
- let f = register_formula solver phi in
- assert_equal ~printer:(fun x -> x)
- (AssignmentSet.str (evaluate solver f struc)) aset_s
+ let res = ref "" in
+ backtrace (
+ let (struc, phi) = (struc_of_string struc_s, formula_of_string phi_s) in
+ let solver = new_solver () in
+ let f = register_formula solver phi in
+ res := AssignmentSet.str (evaluate solver f struc);
+ );
+ assert_equal ~printer:(fun x -> x) !res aset_s
;;
let eval_real_eq var_s struc_s expr_s aset_s =
@@ -179,7 +182,7 @@
" z->58{ y->50{ x->42{ w->34{ v->26 } } } } ," ^
" z->62{ y->53{ x->44{ w->35{ v->26 } } } } ," ^
" z->63{ y->54{ x->45{ w->36{ v->27 } } } } }");
- );
+ );
"eval real: basic" >::
(fun () ->
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <luk...@us...> - 2010-11-22 21:18:53
|
Revision: 1191
http://toss.svn.sourceforge.net/toss/?rev=1191&view=rev
Author: lukstafi
Date: 2010-11-22 21:18:46 +0000 (Mon, 22 Nov 2010)
Log Message:
-----------
Test adjustments. Bug fixes in FFSolver. Display of _new_ on boards fix.
Modified Paths:
--------------
trunk/Toss/Arena/DiscreteRuleTest.ml
trunk/Toss/Play/GameTest.ml
trunk/Toss/Play/HeuristicTest.ml
trunk/Toss/Solver/FFSolver.ml
trunk/Toss/Solver/FFSolverTest.ml
trunk/Toss/Solver/Structure.ml
Modified: trunk/Toss/Arena/DiscreteRuleTest.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRuleTest.ml 2010-11-22 02:05:26 UTC (rev 1190)
+++ trunk/Toss/Arena/DiscreteRuleTest.ml 2010-11-22 21:18:46 UTC (rev 1191)
@@ -18,6 +18,12 @@
let rev_names = Structure.rev_string_to_int_map
+let assert_one_of ?msg str_list str =
+ let msg = match msg with None -> "" | Some msg -> msg^": " in
+ let elements = String.concat ", " str_list in
+ assert_bool (msg^"expected one of "^elements^", but got "^str)
+ (List.mem str str_list)
+
let tests = "DiscreteRule" >::: [
"parsing: simple tests" >::
(fun () ->
@@ -522,7 +528,7 @@
pre = Formula.And [];
rule_s = [1,1]} in
assert_equal ~printer:(fun x->x) ~msg:"one not opt"
- "(true and (not O(b)) and true and true)-> true"
+ "(not O(b))-> true"
(rule_obj_str rule_obj);
let lhs_struc = struc_of_str "[ e | _opt_D (e); O(e) | ]" in
@@ -538,7 +544,7 @@
pre = Formula.And [];
rule_s = [1,1]} in
assert_equal ~printer:(fun x->x) ~msg:"del one not opt"
- "(O(b) and true and true and true)-> (not O(b))"
+ "O(b)-> (not O(b))"
(rule_obj_str rule_obj);
let lhs_struc = struc_of_str "[ e | D (e); _opt_O(e) | ]" in
@@ -553,8 +559,8 @@
emb_rels = ["O"; "D"];
pre = Formula.And [];
rule_s = [1,1]} in
- assert_equal ~printer:(fun x->x) ~msg:"match defined"
- "((P(b) or Q(b)) and true and true and true)-> O(b)"
+ assert_one_of ~msg:"match defined"
+ ["(P(b) or Q(b))-> O(b)"; "(Q(b) or P(b))-> O(b)"]
(rule_obj_str rule_obj);
let lhs_struc = struc_of_str "[ e | D (e); _opt_O(e) | ]" in
@@ -569,8 +575,8 @@
emb_rels = ["O"; "D"];
pre = Formula.And [];
rule_s = [1,1]} in
- assert_equal ~printer:(fun x->x) ~msg:"match defined"
- "((P(b) or Q(b)) and true and true and true)-> (O(b) and (not P(b)) and (not Q(b)))"
+ assert_one_of ~msg:"match defined 2"
+ ["(P(b) or Q(b))-> (O(b) and (not P(b)) and (not Q(b)))";"(Q(b) or P(b))-> (O(b) and (not P(b)) and (not Q(b)))"]
(rule_obj_str rule_obj);
);
@@ -591,7 +597,7 @@
pre = Formula.And [];
rule_s = [1,1]} in
assert_equal ~printer:(fun x->x) ~msg:"defrel: diffthan P Q"
- "(true and ((not P(b)) and (not Q(b))) and true and true)-> true"
+ "((not P(b)) and (not Q(b)))-> true"
(rule_obj_str rule_obj);
let lhs_struc = struc_of_str "[ e | _del_D (e); O(e) | ]" in
@@ -606,8 +612,8 @@
emb_rels = ["O"; "D"];
pre = Formula.And [];
rule_s = [1,1]} in
- assert_equal ~printer:(fun x->x) ~msg:"del defrel"
- "(((_del_P(b) or _del_Q(b)) and O(b)) and ((not P(b)) and (not Q(b))) and true and true)-> (P(b) and (not O(b)))"
+ assert_one_of ~msg:"del defrel"
+ ["(O(b) and (not P(b)) and (not Q(b)) and (_del_P(b) or _del_Q(b)))-> (P(b) and (not O(b)))";"((_del_Q(b) or _del_P(b)) and O(b) and (not P(b)) and (not Q(b)))-> (P(b) and (not O(b)))"]
(rule_obj_str rule_obj);
let lhs_struc = struc_of_str "[ e | _opt_D (e); _diffthan_P(e) | ]" in
@@ -623,7 +629,7 @@
pre = Formula.And [];
rule_s = [1,1]} in
assert_equal ~printer:(fun x->x) ~msg:"diffthan override"
- "(true and ((not O(b)) and (not P(b))) and true and true)-> (O(b) and (not Q(b)))"
+ "((not O(b)) and (not P(b)))-> (O(b) and (not Q(b)))"
(rule_obj_str rule_obj);
);
Modified: trunk/Toss/Play/GameTest.ml
===================================================================
--- trunk/Toss/Play/GameTest.ml 2010-11-22 02:05:26 UTC (rev 1190)
+++ trunk/Toss/Play/GameTest.ml 2010-11-22 21:18:46 UTC (rev 1191)
@@ -39,7 +39,8 @@
let p_name (r, e) =
(* Structure.elem_str rhs_struc r *)
string_of_int r ^ ":" ^ Structure.elem_str struc e in
- let emb = String.concat ", " (List.map p_name move.Game.embedding) in
+ let emb = String.concat ", "
+ (List.sort compare (List.map p_name move.Game.embedding)) in
move.Game.rule ^ "{" ^ emb ^ "}"
let move_gs_str state move =
@@ -724,7 +725,7 @@
(fun mov_s -> List.mem mov_s
["2{1:a1}"; "2{1:a3}"; "2{1:c1}"; "2{1:c3}"]));
- "tictactoe suggest avoid endgame" >::
+ "tictactoe suggest avoid endgame diagonal" >::
(fun () ->
let state = update_game tictactoe_game
"[ | P:1 { }; Q:1 { } | ] \"
@@ -736,9 +737,25 @@
. . .
\"" 1 in
(* TODO: replace with easy_case after monotonic heur done *)
- easy_case state 1 "Q should block"
+ easy_case state 1 "Q should block diagonal"
(fun mov_s -> "2{1:a1}" = mov_s));
+ "tictactoe suggest avoid endgame straight" >::
+ (fun () ->
+ let state = update_game tictactoe_game
+"[ | P:1 { }; Q:1 { } | ] \"
+
+ . P Q
+
+ . P .
+
+ . . .
+\"" 1 in
+ (* TODO: replace with easy_case after monotonic heur done *)
+ easy_case state 1 "Q should block straight"
+ (fun mov_s -> "2{1:a1}" = mov_s);
+ );
+
"tictactoe suggest win" >::
(fun () ->
let state = update_game tictactoe_game
@@ -800,8 +817,8 @@
... ... ... ...
W.. ...W W..W W..W
\"" 1 in
- easy_case state 1 "B should attack left" (* or medium *)
- (fun mov_s -> "6{4:b3, 3:a3, 2:b2, 1:a2}" = mov_s));
+ easy_case state 1 "B should attack left"
+ (fun mov_s -> "6{1:a2, 2:b2, 3:a3, 4:b3}" = mov_s));
"breakthrough suggest midgame" >::
(fun () ->
@@ -826,12 +843,13 @@
\"" 0 in
(* white move should beat the lower black *)
easy_case state 0 "W should beat the lower B" (* or medium *)
- (fun mov_s -> "3{1:e3, 3:e4, 2:f3, 4:f4}" = mov_s));
+ (fun mov_s -> "3{1:e3, 2:f3, 3:e4, 4:f4}" = mov_s));
"gomoku8x8 avoid endgame" >::
(fun () ->
+ skip_if true "takes too long -- uncheck later";
let state = update_game gomoku8x8_game
"[ | | ] \"
... ... ... ...
@@ -881,6 +899,7 @@
"gomoku8x8 block gameover" >::
(fun () ->
+ skip_if true "takes too long -- uncheck later";
let state = update_game gomoku8x8_game
"[ | | ] \"
... ... ... ...
@@ -908,6 +927,7 @@
"gomoku8x8 more pieces" >::
(fun () ->
+ skip_if true "takes too long -- uncheck later";
let state = update_game gomoku8x8_game
"[ | | ] \"
... ... ... ...
@@ -989,7 +1009,7 @@
);
]
-let a =
+let a =
let file_from_path p =
String.sub p (String.rindex p '/'+1)
(String.length p - String.rindex p '/' - 1) in
@@ -1012,7 +1032,7 @@
let a () =
match test_filter
- ["Game:0:misc:1:breakthrough payoff"]
+ ["Game:1:alpha_beta_ord:4:tictactoe suggest avoid endgame straight"]
tests
with
| Some tests -> ignore (run_test_tt ~verbose:true tests)
Modified: trunk/Toss/Play/HeuristicTest.ml
===================================================================
--- trunk/Toss/Play/HeuristicTest.ml 2010-11-22 02:05:26 UTC (rev 1190)
+++ trunk/Toss/Play/HeuristicTest.ml 2010-11-22 21:18:46 UTC (rev 1191)
@@ -127,7 +127,7 @@
F F F F F F F F
\"" in
assert_equal ~printer:(fun x->x)
- "ex y7, y6, y5, y4, y3, y2, y1, y0, y ((C(x, y7) and C(y6, y5) and C(y5, y4) and C(y4, y3) and C(y3, y2) and C(y2, y1) and C(y1, y0) and C(y0, y) and C(y, x)))"
+ "ex y7, y6, y5, y4, y3, y2, y1, y0, y ((C(y7, y6) and C(y6, y5) and C(y5, y4) and C(y4, y3) and C(y3, y2) and C(y2, y1) and C(y1, y0) and C(y0, x) and C(x, y)))"
(Formula.str (Heuristic.expanded_description 5
(Aux.strings_of_list ["B"; "W"])
state (formula_of_str "ex y (C(x, y) and F(y))")));
@@ -267,7 +267,7 @@
F F F F F F F F
\"" in
assert_equal ~printer:(fun x->x)
- "ex y7, y6, y5, y4, y3, y2, y1, y0, y ((C(x, y7) and C(y6, y5) and C(y5, y4) and C(y4, y3) and C(y3, y2) and C(y2, y1) and C(y1, y0) and C(y0, y) and C(y, x)))"
+ "ex y7, y6, y5, y4, y3, y2, y1, y0, y ((C(y7, y6) and C(y6, y5) and C(y5, y4) and C(y4, y3) and C(y3, y2) and C(y2, y1) and C(y1, y0) and C(y0, x) and C(x, y)))"
(Formula.str (Heuristic.expanded_form 5
(Aux.strings_of_list ["B"; "W"])
state (formula_of_str "ex y (C(x, y) and F(y))")));
Modified: trunk/Toss/Solver/FFSolver.ml
===================================================================
--- trunk/Toss/Solver/FFSolver.ml 2010-11-22 02:05:26 UTC (rev 1190)
+++ trunk/Toss/Solver/FFSolver.ml 2010-11-22 21:18:46 UTC (rev 1191)
@@ -26,7 +26,23 @@
let vars_of_array nvs =
Array.fold_left (fun vs nv -> Vars.add nv vs) Vars.empty nvs
+let sb_str struc sb =
+ String.concat ", " (List.map (fun (v,e) ->
+ var_str v^"->"^Structure.elem_str struc e) sb)
+let rec is_unique_assoc = function
+ | [] -> true
+ | (e,_)::tl -> if List.mem_assoc e tl then false
+ else is_unique_assoc tl
+
+(*
+let aFO lnum (v,assgns) =
+ Printf.printf "(%d:%s) %!" lnum (var_str v);
+ if is_unique_assoc assgns then A.FO (v, assgns)
+ else failwith
+ ("not unique "^string_of_int lnum^": "^A.str (A.FO (v,assgns)))
+*)
+
let rec invert_aset acc = function
| A.Empty -> []
| A.Any -> acc
@@ -266,9 +282,13 @@
Tuples.fold (fun tup dom ->
if Aux.array_for_all2 (fun known asked->
known = -1 || known = asked) known_tup tup
+ && not (List.mem tup.(nvi) dom)
then tup.(nvi)::dom
else dom) tuples [] in
- if not multi_unkn && conj_cont = [] && delayed1 = [] &&
+ if init_domain = []
+ then raise
+ (Unsatisfiable_FO (vars_of_array (var_tup vtup)))
+ else if not multi_unkn && conj_cont = [] && delayed1 = [] &&
delayed2 = []
then (* no more vars and conjuncts *)
A.FO (nvar, List.map (fun e->e,A.Any) init_domain)
@@ -383,7 +403,9 @@
then Elems.add tup.(nvi) dom
else dom) tuples Elems.empty in
Elems.elements (Elems.diff model.elements init_domain_co) in
- if conj_cont = [] && delayed1 = [] && delayed2 = []
+ if init_domain = []
+ then raise Unsatisfiable
+ else if conj_cont = [] && delayed1 = [] && delayed2 = []
then (* no more vars and conjuncts *)
A.FO (nvar, List.map (fun e->e,A.Any) init_domain)
else
@@ -669,7 +691,9 @@
let register_real_expr expr = ref (expr, false)
let evaluate struc reg_phi =
if not (snd !reg_phi) then
- reg_phi := normalize_for_model struc (fst !reg_phi), true;
+ reg_phi :=
+ normalize_for_model struc
+ (FormulaOps.simplify (fst !reg_phi)), true;
evaluate struc (fst !reg_phi)
let check_formula struc reg_phi =
if not (snd !reg_phi) then
@@ -680,5 +704,9 @@
reg_expr :=
normalize_expr_for_model struc (fst !reg_expr), true;
get_real_val (fst !reg_expr) struc
- let formula_str reg_phi = Formula.str (fst !reg_phi)
+ let formula_str reg_phi =
+ if not (snd !reg_phi) then
+ (* to increase consistency of display *)
+ reg_phi := FormulaOps.simplify (fst !reg_phi), false;
+ Formula.str (fst !reg_phi)
end
Modified: trunk/Toss/Solver/FFSolverTest.ml
===================================================================
--- trunk/Toss/Solver/FFSolverTest.ml 2010-11-22 02:05:26 UTC (rev 1190)
+++ trunk/Toss/Solver/FFSolverTest.ml 2010-11-22 21:18:46 UTC (rev 1191)
@@ -30,15 +30,31 @@
(* alfa-conversion of the above *)
let winQvwxyz_idempotent = "ex z ((Q(z) and (ex u0 ((C(u0, z) and ex y2 ((R(y2, u0) and Q(y2) and ex t0 ((C(t0, y2) and ex x2 ((R(x2, t0) and Q(x2) and ex s0 ((C(s0, x2) and ex w2 ((R(w2, s0) and Q(w2) and ex r0 ((C(r0, w2) and ex v2 ((R(v2, r0) and Q(v2))))))))))))))))) or ex u ((C(z, u) and ex y1 ((R(y1, u) and Q(y1) and ex t ((C(y1, t) and ex x1 ((R(x1, t) and Q(x1) and ex s ((C(x1, s) and ex w1 ((R(w1, s) and Q(w1) and ex r ((C(w1, r) and ex v1 ((R(v1, r) and Q(v1))))))))))))))))) or ex y0 ((C(y0, z) and Q(y0) and ex x0 ((C(x0, y0) and Q(x0) and ex w0 ((C(w0, x0) and Q(w0) and ex v0 ((C(v0, w0) and Q(v0))))))))) or ex y ((R(y, z) and Q(y) and ex x ((R(x, y) and Q(x) and ex w ((R(w, x) and Q(w) and ex v ((R(v, w) and Q(v))))))))))))"
+let real_val_eq struc_s expr_s x =
+ let struc = struc_of_str struc_s in
+ let expr =
+ FFSolver.normalize_expr_for_model struc (real_of_str expr_s) in
+ assert_equal ~printer:(fun x -> string_of_float x) ~msg:expr_s
+ x (FFSolver.get_real_val expr struc)
let tests = "FFSolver" >::: [
- "get_real_val: simple sum" >::
+ "get_real_val: tests from Solver.ml" >::
(fun () ->
- let r = real_of_str "Sum (x, y | R (x, y) : 1)" in
- let model = struc_of_str "[ | R { (a, a); (a, b) } | ] " in
- assert_equal ~printer:(fun x -> string_of_float x) (2.)
- (FFSolver.get_real_val r model)
- );
+ real_val_eq "[ | R { (a, a); (a, b) } | ] "
+ ":(ex x (R (x, x))) + 1" 2.;
+ real_val_eq "[ | P { x } | f { x->1, y->2, z->3 } ]"
+ "Sum (x | true : :f(x)^2)" 14.;
+ real_val_eq "[ | R { (a, a); (a, b) } | ] "
+ "Sum (x | true : :(all y (R (x, y))))" 1.;
+ real_val_eq "[ | R { (a, a); (a, b) } | ] "
+ "Sum (x | all y (R (x, y)) : 1)" 1.;
+ real_val_eq "[ | P { x } | f { x->1, y->2, z->3 } ]"
+ "Sum (x, y | P(x) : :f(x) * :f(y))" 6.;
+ real_val_eq "[ | P { x } | f { x->1, y->2, z->3 } ]"
+ "Sum (x, y | true : :f(x) * :f(y))" 36.;
+ real_val_eq "[ | R { (a, a); (a, b) } | ] "
+ "Sum (x, y | R (x, y) : 1)" 2.;
+ );
"evaluate: negation" >::
(fun () ->
@@ -195,3 +211,4 @@
with
| Some tests -> ignore (run_test_tt ~verbose:true tests)
| None -> ()
+
Modified: trunk/Toss/Solver/Structure.ml
===================================================================
--- trunk/Toss/Solver/Structure.ml 2010-11-22 02:05:26 UTC (rev 1190)
+++ trunk/Toss/Solver/Structure.ml 2010-11-22 21:18:46 UTC (rev 1191)
@@ -640,7 +640,8 @@
predicates in
let long_preds =
List.filter (fun r ->
- List.mem_assoc r uniq_long && not (List.mem r short_preds))
+ List.mem_assoc r uniq_long && not (List.mem r news)
+ && not (List.mem r short_preds))
predicates in
let used1, rep1, short_preds, diffthans, opts, news, dels, long_preds =
if use_any then
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <luk...@us...> - 2010-11-22 02:05:32
|
Revision: 1190
http://toss.svn.sourceforge.net/toss/?rev=1190&view=rev
Author: lukaszkaiser
Date: 2010-11-22 02:05:26 +0000 (Mon, 22 Nov 2010)
Log Message:
-----------
Solver optimization and small corrections.
Modified Paths:
--------------
trunk/Toss/Formula/Makefile
trunk/Toss/Makefile
trunk/Toss/Solver/Solver.ml
trunk/Toss/TossTest.ml
Modified: trunk/Toss/Formula/Makefile
===================================================================
--- trunk/Toss/Formula/Makefile 2010-11-21 21:44:23 UTC (rev 1189)
+++ trunk/Toss/Formula/Makefile 2010-11-22 02:05:26 UTC (rev 1190)
@@ -3,6 +3,7 @@
%Test:
make -C .. Formula/$@
+AuxTest:
FormulaTest:
BoolFormulaTest:
FormulaOpsTest:
Modified: trunk/Toss/Makefile
===================================================================
--- trunk/Toss/Makefile 2010-11-21 21:44:23 UTC (rev 1189)
+++ trunk/Toss/Makefile 2010-11-22 02:05:26 UTC (rev 1190)
@@ -32,9 +32,9 @@
OCB_CFLAG=-cflags -I,+oUnit,-g
OCB_LIB=-libs str,nums,unix,oUnit
OCB_PP=-pp "camlp4o ../caml_extensions/pa_let_try.cmo ../caml_extensions/pa_backtrace.cmo"
-OCAMLBUILD=ocamlbuild -j 4 -menhir ../menhir_conf $(OCB_PP) \
+OCAMLBUILD=ocamlbuild -j 8 -menhir ../menhir_conf $(OCB_PP) \
$(OCB_LIB) $(OCB_CFLAG) $(OCB_LFLAG)
-OCAMLBUILDBT=ocamlbuild -j 4 menhir ../menhir_conf $(OCB_PP) \
+OCAMLBUILDBT=ocamlbuild -j 8 menhir ../menhir_conf $(OCB_PP) \
$(OCB_LIB) $(OCB_CFLAG) $(OCB_LFLAGBT)
FormulaINC=Formula/Sat
@@ -68,6 +68,7 @@
# Formula tests
Formula_tests: \
+ Formula/AuxTest \
Formula/FormulaTest \
Formula/BoolFormulaTest \
Formula/FormulaOpsTest \
Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml 2010-11-21 21:44:23 UTC (rev 1189)
+++ trunk/Toss/Solver/Solver.ml 2010-11-22 02:05:26 UTC (rev 1190)
@@ -177,23 +177,39 @@
process_vars [] (List.sort Formula.compare_vars (fo_vars_real p))
+(* Helper: find assoc and remove. *)
+let rec assoc_del (x : Formula.formula) = function
+ | [] -> raise Not_found
+ | (a, b as pair) :: l ->
+ if x = a then (b, l) else
+ let (b, nl) = assoc_del x l in
+ (b, pair :: nl)
+
(* Eval with very basic caching. *)
let eval_m struc phi =
+ if phi = And [] then Any else
if !cache_struc != struc then (
let els = Set (Elems.cardinal struc.elements, struc.elements) in
let asg = eval struc (ref els) Any phi in
cache_struc := struc;
cache_results := [(phi, asg)];
asg
- ) else try
- List.assoc phi !cache_results
- with Not_found ->
- if !debug_level > 0 then print_endline ("Eval_m " ^ (str phi));
- if List.length !cache_results > !cCACHESIZE then cache_results := [];
- let els = Set (Elems.cardinal struc.elements, struc.elements) in
- let asg = eval struc (ref els) Any phi in
- cache_results := (phi, asg) :: !cache_results;
- asg
+ ) else
+ try
+ let (res, new_cache) = assoc_del phi !cache_results in
+ cache_results := (phi, res) :: new_cache;
+ if !debug_level > 1 then (
+ print_endline ("found in cache: " ^ (Formula.str phi));
+ print_endline ("size: "^ (string_of_int (List.length !cache_results)));
+ );
+ res
+ with Not_found ->
+ if !debug_level > 0 then print_endline ("Eval_m " ^ (str phi));
+ if List.length !cache_results > !cCACHESIZE then cache_results := [];
+ let els = Set (Elems.cardinal struc.elements, struc.elements) in
+ let asg = eval struc (ref els) Any phi in
+ cache_results := (phi, asg) :: !cache_results;
+ asg
(* Helper function, assignment of tuple. *)
let asg_of_tuple struc vars tuple =
@@ -207,37 +223,66 @@
eval_m struc
(RealExpr (Plus (expr, Times (Const (-1.), RVar rvar)), Formula.EQZero))
+(* Helper checking function. *)
+let rec check_f struc asg = function
+ | Ex (vs, phi) -> check_f struc asg phi
+ | Or (fl) -> List.exists (check_f struc asg) fl
+ | phi -> join asg (eval_m struc phi) <> Empty
+(* Almost as eval_m but cache sub-formulas in boolean form without free vars. *)
+let eval_cache_sentences solver struc in_phi =
+ let reg_tnf phi =
+ try
+ let phi_id = List.assoc phi !(solver.reg_formulas) in
+ Hashtbl.find solver.formulas_eval phi_id
+ with Not_found ->
+ Hashtbl.find solver.formulas_eval (register_formula solver phi) in
+ let eval_no_fv phi =
+ if FormulaOps.free_vars phi = [] then (
+ if !debug_level > 1 then
+ print_endline ("sentence check: " ^ (Formula.str phi));
+ if check_f struc Any (reg_tnf phi) then And [] else Or []
+ )
+ else phi in
+ let not_true f = f <> And [] in
+ let not_false f = f <> Or [] in
+ let rec subst_no_fv = function
+ | And fl ->
+ let nfl = List.filter not_true (List.map subst_no_fv fl) in
+ if List.exists (fun f -> f = Or []) nfl then Or [] else And nfl
+ | Or fl ->
+ let nfl = List.filter not_false (List.map subst_no_fv fl) in
+ if List.exists (fun f -> f = And []) nfl then And [] else Or nfl
+ | f -> eval_no_fv f in
+ let phi = subst_no_fv in_phi in
+ let proc_phi = reg_tnf phi in
+ if !debug_level > 0 then (
+ print_endline ("in phi: " ^ (Formula.str in_phi));
+ print_endline ("phi: " ^ (Formula.str phi));
+ print_endline ("proc phi: " ^ (Formula.str proc_phi));
+ );
+ eval_m struc proc_phi
+
+
(* Fast function to get a value of a real expression without free variables
other than those assigned in [asg] explicitely. *)
let rec get_real_val solver asg expr struc =
- let rec check_f = function
- Ex (vs, phi) -> check_f phi
- | Or (fl) -> List.exists check_f fl
- | phi -> join asg (eval_m struc phi) <> Empty in
+ let check_fa = check_f struc asg in
match expr with
- Char phi -> if check_f phi then 1. else 0.
+ Char phi -> if check_fa phi then 1. else 0.
| Const v -> v
| Times (e1, e2) ->
(get_real_val solver asg e1 struc) *. (get_real_val solver asg e2 struc)
| Plus (e1, e2) ->
(get_real_val solver asg e1 struc) +. (get_real_val solver asg e2 struc)
| Sum (vl, guard, r) ->
- let gd = (
- try
- let gd_id = List.assoc guard !(solver.reg_formulas) in
- Hashtbl.find solver.formulas_eval gd_id
- with Not_found ->
- Hashtbl.find solver.formulas_eval (register_formula solver guard)
- ) in
let all_vs = (List.map to_fo (AssignmentSet.assigned_vars [] asg)) @ vl in
if !debug_level > 0 then (
- print_endline ("guard " ^ (Formula.str guard));
print_endline ("asg " ^ (AssignmentSet.str asg));
print_endline ("sum vars " ^ (Formula.var_list_str vl));
print_endline ("all vars " ^ (Formula.var_list_str all_vs));
);
- let asg_gd = join asg (eval_m struc gd) in
+ let asg_gd = join asg (eval_cache_sentences solver struc guard) in
let tps = tuples struc.elements (List.map var_str all_vs) asg_gd in
let add_val acc tp =
let tp_asg = asg_of_tuple struc all_vs tp in
Modified: trunk/Toss/TossTest.ml
===================================================================
--- trunk/Toss/TossTest.ml 2010-11-21 21:44:23 UTC (rev 1189)
+++ trunk/Toss/TossTest.ml 2010-11-22 02:05:26 UTC (rev 1190)
@@ -1,7 +1,7 @@
open OUnit
let formula_tests = "Formula" >::: [
- (* AuxTest.tests; *)
+ AuxTest.tests;
FormulaTest.tests;
FormulaOpsTest.tests;
FFTNFTest.tests;
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <luk...@us...> - 2010-11-21 21:44:29
|
Revision: 1189
http://toss.svn.sourceforge.net/toss/?rev=1189&view=rev
Author: lukstafi
Date: 2010-11-21 21:44:23 +0000 (Sun, 21 Nov 2010)
Log Message:
-----------
AuxTest test suite: missing file.
Added Paths:
-----------
trunk/Toss/Formula/AuxTest.ml
Added: trunk/Toss/Formula/AuxTest.ml
===================================================================
--- trunk/Toss/Formula/AuxTest.ml (rev 0)
+++ trunk/Toss/Formula/AuxTest.ml 2010-11-21 21:44:23 UTC (rev 1189)
@@ -0,0 +1,401 @@
+(* Unit tests for auxiliary functions. *)
+open OUnit
+
+let print_alist f l =
+ String.concat ", " (List.map (fun (k,v) -> k^": "^f v) l)
+
+let tests = "Aux" >::: [
+ "concat_map, map_some" >::
+ (fun () ->
+ let f = function `A -> ["a";"b"] | `B -> ["c"] | `C -> []
+ | `D -> ["d";"e"] in
+ assert_equal ~printer:(String.concat "; ")
+ ["a";"b";"c";"d";"e"]
+ (Aux.concat_map f [`A;`B;`C;`D]);
+
+ let f = function `A -> Some "a" | `B -> Some "b" | `C -> None
+ | `D -> Some "d" in
+ assert_equal ~printer:(String.concat "; ")
+ ["a";"b";"d"]
+ (Aux.map_some f [`A;`B;`C;`D]);
+ );
+
+ "map_reduce" >::
+ (fun () ->
+ let mapf = function `A -> "1", ["a";"b"] | `B -> "2", ["c"]
+ | `C -> "1", [] | `D -> "2", ["d";"e"] in
+ assert_equal ~msg:"simple test"
+ ~printer:(print_alist (String.concat ", "))
+ ["1", ["a";"b"]; "2", ["d";"e"; "c"]]
+ (Aux.map_reduce mapf (@) [] [`A;`B;`C;`D]);
+
+ assert_equal ~msg:"histogram" ~printer:(print_alist string_of_int)
+ ["abra",3; "bra", 1; "cada",2]
+ (Aux.map_reduce (fun k->k,1) (+) 0
+ ["abra"; "cada"; "abra"; "bra"; "cada"; "abra"]);
+ );
+
+ "rev_assoc, rev_assoc_all" >::
+ (fun () ->
+ assert_equal ~printer:(fun x -> x)
+ "G"
+ (Aux.rev_assoc
+ ["B","f";"C","B"; "G","T"; "F", "T"]
+ "T");
+
+ assert_raises ~msg:"should not find"
+ Not_found
+ (fun () -> Aux.rev_assoc
+ ["B","f";"C","B"; "G","Ts"]
+ "T");
+
+ assert_equal ~printer:(String.concat "; ")
+ ["F"; "G"]
+ (Aux.rev_assoc_all
+ ["B","f";"C","B"; "G","T"; "F", "T"]
+ "T");
+
+ assert_equal ~printer:(String.concat "; ")
+ []
+ (Aux.rev_assoc_all
+ ["B","f";"C","B"; "G","Ts"]
+ "T");
+ );
+
+
+ "replace_assoc, pop_assoc" >::
+ (fun () ->
+ assert_equal ~printer:(print_alist (fun x -> x))
+ ["B","f";"C","B"; "G","replaced"; "G", "T"]
+ (Aux.replace_assoc "G" "replaced"
+ ["B","f";"C","B"; "G","T"; "G", "T"]);
+
+ assert_equal ~printer:(print_alist (fun x -> x))
+ ["B","f";"C","B"; "F", "T"; "G","replaced"]
+ (Aux.replace_assoc "G" "replaced"
+ ["B","f";"C","B"; "F", "T"]);
+
+ assert_equal
+ ~printer:(fun (x,y) -> x^" -- "^print_alist (fun e->e) y)
+ ("T", ["B","f";"C","B"; "G", "T2"])
+ (Aux.pop_assoc "G"
+ ["B","f";"C","B"; "G","T"; "G", "T2"]);
+
+ assert_raises ~msg:"should not find"
+ Not_found
+ (fun () -> Aux.pop_assoc "G"
+ ["B","f";"C","B"; "F","Ts"]);
+ );
+
+ "unsome, map_try" >::
+ (fun () ->
+ assert_equal ~printer:(fun x->x)
+ "x" (Aux.unsome (Some "x"));
+
+ assert_raises ~msg:"None"
+ (Invalid_argument "unsome")
+ (fun () -> Aux.unsome None);
+
+ let f = function `A -> "a" | `B -> "b" | `C -> raise Not_found
+ | `D -> "d" in
+ assert_equal ~printer:(String.concat "; ")
+ ["a";"b";"d"]
+ (Aux.map_try f [`A;`B;`C;`D]);
+ );
+
+ "product, all_tuples_for" >::
+ (fun () ->
+ let print_llist l = String.concat "; "
+ (List.map (String.concat ", ") l) in
+
+ assert_equal ~printer:print_llist
+ [["a"; "c"; "d"]; ["a"; "c"; "e"]; ["b"; "c"; "d"]; ["b"; "c"; "e"]]
+ (Aux.product [["a";"b"]; ["c"]; ["d";"e"]]);
+
+ assert_equal ~printer:print_llist
+ [] (Aux.product [["a";"b"]; []; ["c"]; ["d";"e"]]);
+
+ assert_equal ~printer:print_llist
+ [["a"; "a"]; ["a"; "b"]; ["a"; "c"]; ["b"; "a"]; ["b"; "b"]; ["b"; "c"]; ["c"; "a"]; ["c"; "b"]; ["c"; "c"]]
+ (Aux.all_tuples_for [();()] ["a";"b";"c"]);
+
+ assert_equal ~printer:print_llist
+ [["a"; "a"; "a"]; ["a"; "a"; "b"]; ["a"; "b"; "a"]; ["a"; "b"; "b"]; ["b"; "a"; "a"]; ["b"; "a"; "b"]; ["b"; "b"; "a"]; ["b"; "b"; "b"]]
+ (Aux.all_tuples_for [();(); ()] ["a";"b"]);
+ );
+
+ "list_remove, remove_one" >::
+ (fun () ->
+ assert_equal ~printer:(String.concat "; ")
+ ["a";"b";"d"]
+ (Aux.list_remove "c" ["a";"c";"b"; "d"; "c"]);
+
+ assert_equal ~printer:(String.concat "; ")
+ ["a";"b";"d"; "c"]
+ (Aux.remove_one "c" ["a";"c";"b"; "d"; "c"]);
+ );
+
+ "insert_nth, find_index" >::
+ (fun () ->
+ assert_equal ~printer:(String.concat "; ")
+ ["a";"c";"e"; "b"; "d"; "c"]
+ (Aux.insert_nth 2 "e" ["a";"c"; "b"; "d"; "c"]);
+
+ assert_equal ~printer:(String.concat "; ")
+ ["a";"c"; "b";"e"]
+ (Aux.insert_nth 3 "e" ["a";"c"; "b"]);
+
+ assert_raises ~msg:"beyond end of list"
+ Not_found
+ (fun () -> Aux.insert_nth 3 "e" ["a"; "b"]);
+
+ assert_equal ~printer:string_of_int
+ 2
+ (Aux.find_index "e" ["a";"c"; "e"; "b"; "d"; "c"]);
+
+ assert_equal ~printer:string_of_int
+ 3
+ (Aux.find_index "e" ["a";"c"; "b"; "e"]);
+
+ assert_raises ~msg:"not in list"
+ Not_found
+ (fun () -> Aux.find_index "e" ["a"; "b"]);
+ );
+
+ "maximal" >::
+ (fun () ->
+ assert_equal ~printer:(String.concat "; ") ~msg:"orto by first char"
+ ["b1";"a3";"c7"]
+ (Aux.maximal (fun a b -> a.[0] = b.[0] && a.[1] <= b.[1])
+ ["a1";"c2"; "b1"; "a3"; "c7"]);
+
+ assert_equal ~printer:(String.concat "; ") ~msg:"incomparable"
+ ["a1";"c2"; "b1"; "a3"; "c7"]
+ (Aux.maximal (fun _ _ -> false)
+ ["a1";"c2"; "b1"; "a3"; "c7"]);
+
+ assert_equal ~printer:(String.concat "; ") ~msg:"linear"
+ ["c7"]
+ (Aux.maximal (<=)
+ ["a1";"c2"; "b1"; "a3"; "c7"]);
+ );
+
+ "unique, take_n" >::
+ (fun () ->
+ assert_equal ~printer:(String.concat "; ")
+ ["a";"c";"b";"d"]
+ (Aux.unique (=) ["a";"c";"b"; "d"; "c"]);
+
+ assert_equal ~printer:(String.concat "; ")
+ ["a";"c";"b"]
+ (Aux.take_n 3 ["a";"c";"b"; "d"; "c"]);
+
+ assert_equal ~printer:(String.concat "; ")
+ ["a";"c";"b"]
+ (Aux.take_n 5 ["a";"c";"b"]);
+ );
+
+ "array_map2, array_combine" >::
+ (fun () ->
+ assert_equal ~printer:(print_alist (fun x->x))
+ ["a","e";"c","d";"b","c"]
+ (Array.to_list
+ (Aux.array_map2 (fun x y->x,y) [|"a";"c";"b"|] [|"e"; "d"; "c"|]));
+
+ assert_raises ~msg:"not equal lengths"
+ (Invalid_argument "Aux.array_map2")
+ (fun ()->
+ Aux.array_map2 (fun x y->x,y) [|"a";"c";"b"|] [|"e"; "d"|]);
+
+ assert_equal ~printer:(print_alist (fun x->x))
+ ["a","e";"c","d";"b","c"]
+ (Array.to_list
+ (Aux.array_combine [|"a";"c";"b"|] [|"e"; "d"; "c"|]));
+
+ assert_raises ~msg:"not equal lengths"
+ (Invalid_argument "Aux.array_map2")
+ (fun ()->
+ Aux.array_combine [|"a";"c";"b"|] [|"e"; "d"|]);
+ );
+
+ "array_existsi, array_mem" >::
+ (fun () ->
+ assert_bool "exists 4th"
+ (Aux.array_existsi (fun i _ -> i = 4)
+ [|"a1";"c2"; "b1"; "a3"; "c7"|]);
+
+ assert_bool "exists same 4th"
+ (Aux.array_existsi (fun i x -> i = 4 && x = "c7")
+ [|"a1";"c2"; "b1"; "a3"; "c7"|]);
+
+ assert_bool "mem c7"
+ (Aux.array_mem "c7"
+ [|"a1";"c2"; "b1"; "a3"; "c7"|]);
+
+ );
+
+ "array_from_assoc, array_map_of_list" >::
+ (fun () ->
+ assert_equal ~printer:(String.concat "; ")
+ ["a"; "c"; "b"; "e"; "d"; "c"]
+ (Array.to_list
+ (Aux.array_from_assoc
+ [0,"a";1,"c"; 4,"d"; 5,"c";2,"b";3,"e"]));
+
+ assert_equal ~printer:(String.concat "; ")
+ ["2"; "3"; "4"; "5"]
+ (Array.to_list
+ (Aux.array_map_of_list (fun i->string_of_int (i+1))
+ [1;2;3;4]));
+ );
+
+
+ "array_argfind, array_find_all, array_argfind_all" >::
+ (fun () ->
+ assert_equal ~printer:string_of_int
+ 2
+ (Aux.array_argfind (fun e->e="e")
+ [|"a";"c"; "e"; "b"; "d"; "c"|]);
+
+ assert_equal ~printer:string_of_int
+ 3
+ (Aux.array_argfind (fun e->e="e")
+ [|"a";"c"; "b"; "e"|]);
+
+ assert_raises ~msg:"not in array"
+ Not_found
+ (fun () -> Aux.array_argfind (fun e->e="e")
+ [|"a"; "b"|]);
+
+ assert_equal ~printer:(String.concat "; ")
+ ["e"; "e2"; "e3"]
+ (Aux.array_find_all (fun e->e.[0]='e')
+ [|"a";"c"; "e"; "b"; "e2"; "d"; "e3"; "c"|]);
+
+ assert_equal ~printer:(String.concat "; ")
+ ["e0"]
+ (Aux.array_find_all (fun e->e.[0]='e')
+ [|"a";"c"; "b"; "e0"|]);
+
+ assert_equal ~printer:(String.concat "; ")
+ []
+ (Aux.array_find_all (fun e->e.[0]='e')
+ [|"a";"c"; "b"|]);
+
+ assert_equal
+ ~printer:(fun l->String.concat "; " (List.map string_of_int l))
+ [2;4;6]
+ (Aux.array_argfind_all (fun e->e.[0]='e')
+ [|"a";"c"; "e"; "b"; "e2"; "d"; "e3"; "c"|]);
+
+ assert_equal
+ ~printer:(fun l->String.concat "; " (List.map string_of_int l))
+ [3]
+ (Aux.array_argfind_all (fun e->e.[0]='e')
+ [|"a";"c"; "b"; "e0"|]);
+
+ assert_equal
+ ~printer:(fun l->String.concat "; " (List.map string_of_int l))
+ []
+ (Aux.array_argfind_all (fun e->e.[0]='e')
+ [|"a";"c"; "b"|]);
+ );
+
+ "array_for_all, array_for_all2" >::
+ (fun () ->
+ assert_bool "all c"
+ (Aux.array_for_all (fun x->x.[0]='c')
+ [|"c1";"c2"; "c1"; "c3"; "c7"|]);
+
+ assert_bool "not all c"
+ (not (Aux.array_for_all (fun x->x.[0]='c')
+ [|"a1";"c2"; "b1"; "a3"; "c7"|]));
+
+ assert_bool "all equal"
+ (Aux.array_for_all2 (fun x y->x=y)
+ [|"a";"c";"b"|] [|"a"; "c"; "b"|]);
+
+ assert_bool "not all equal"
+ (not (Aux.array_for_all2 (fun x y->x=y)
+ [|"a";"c";"b"|] [|"e"; "d"; "c"|]));
+
+ assert_raises ~msg:"not equal lengths"
+ (Invalid_argument "Aux.array_for_all2")
+ (fun ()->
+ Aux.array_for_all2 (fun x y->x=y)
+ [|"a";"c";"b"|] [|"e"; "d"|]);
+ );
+
+ "partition_choice, partition_map" >::
+ (fun () ->
+ assert_equal ~printer:(fun (x,y)->
+ String.concat ", " x^"; "^String.concat ", " y)
+ (["b";"c";"e"],["a";"d"])
+ (Aux.partition_choice
+ [Aux.Right "a";Aux.Left "b";Aux.Left "c";
+ Aux.Right "d";Aux.Left "e"]);
+
+ let f = function `A -> Aux.Right "a" | `B -> Aux.Left "b"
+ | `C -> Aux.Left "c"
+ | `D -> Aux.Right "d" | `E -> Aux.Left "e" in
+ assert_equal ~printer:(fun (x,y)->
+ String.concat ", " x^"; "^String.concat ", " y)
+ (["b";"c";"e"],["a";"d"])
+ (Aux.partition_map f [`A;`B;`C;`D; `E]);
+ );
+
+ "transpose_lists" >::
+ (fun () ->
+ let print_llist l = String.concat "; "
+ (List.map (String.concat ", ") l) in
+
+ assert_equal ~printer:print_llist
+ [["a"; "d"; "f"]; ["b"; "e"; "g"]]
+ (Aux.transpose_lists [["a";"b"]; ["d";"e"]; ["f";"g"]]);
+
+ assert_equal ~printer:print_llist
+ [["a"; "d"]; ["b"; "e"]; ["c"; "f"]]
+ (Aux.transpose_lists [["a";"b"; "c"]; ["d";"e"; "f"]]);
+
+ assert_raises ~msg:"not rectangular"
+ (Invalid_argument "List.map2")
+ (fun ()->
+ Aux.transpose_lists [["a";"b"; "c"]; ["d";"e"]]);
+ );
+
+
+ "not_conflicting_name, not_conflicting_names" >::
+ (fun () ->
+ assert_equal ~printer:(fun x->x)
+ "x1"
+ (Aux.not_conflicting_name
+ (Aux.strings_of_list ["x"; "x0"]) "x");
+
+ assert_equal ~printer:(String.concat "; ")
+ ["x1"; "x2"; "x3"]
+ (Aux.not_conflicting_names "x"
+ (Aux.strings_of_list ["x"; "x0"]) [();();()]);
+
+ assert_equal ~printer:(fun x->x)
+ "y"
+ (Aux.not_conflicting_name
+ (Aux.strings_of_list ["x"; "x0"]) "y");
+
+ assert_equal ~printer:(String.concat "; ")
+ ["y0"; "y1"; "y2"]
+ (Aux.not_conflicting_names "y"
+ (Aux.strings_of_list ["x"; "x0"]) [();();()]);
+ );
+
+]
+
+let a =
+ let file_from_path p =
+ String.sub p (String.rindex p '/'+1)
+ (String.length p - String.rindex p '/' - 1) in
+ let test_fname name =
+ let fname = file_from_path Sys.executable_name in
+ String.length fname >= String.length name &&
+ String.sub fname 0 (String.length name) = name in
+ if test_fname "AuxTest" then
+ ignore (run_test_tt ~verbose:true tests)
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <luk...@us...> - 2010-11-21 21:34:09
|
Revision: 1188
http://toss.svn.sourceforge.net/toss/?rev=1188&view=rev
Author: lukaszkaiser
Date: 2010-11-21 21:34:02 +0000 (Sun, 21 Nov 2010)
Log Message:
-----------
Solver corrections and tests moved to OUnit.
Modified Paths:
--------------
trunk/Toss/Client/SystemDisplay.py
trunk/Toss/Solver/AssignmentSet.ml
trunk/Toss/Solver/AssignmentSet.mli
trunk/Toss/Solver/Solver.ml
trunk/Toss/Solver/Solver.mli
trunk/Toss/Solver/SolverTest.ml
trunk/Toss/TossTest.ml
Modified: trunk/Toss/Client/SystemDisplay.py
===================================================================
--- trunk/Toss/Client/SystemDisplay.py 2010-11-21 20:45:43 UTC (rev 1187)
+++ trunk/Toss/Client/SystemDisplay.py 2010-11-21 21:34:02 UTC (rev 1188)
@@ -43,7 +43,7 @@
suggest_bt = self.toolbar.addAction (QIcon(":/pics/move.svg"),"Hint")
QObject.connect(suggest_bt, SIGNAL("triggered ()"), self.suggest)
- self.__sg_iters = 4
+ self.__sg_iters = 2
self.sg_iters_bt = self.toolbar.addAction ("Depth: " +
str(self.__sg_iters))
QObject.connect(self.sg_iters_bt, SIGNAL("triggered ()"),
Modified: trunk/Toss/Solver/AssignmentSet.ml
===================================================================
--- trunk/Toss/Solver/AssignmentSet.ml 2010-11-21 20:45:43 UTC (rev 1187)
+++ trunk/Toss/Solver/AssignmentSet.ml 2010-11-21 21:34:02 UTC (rev 1188)
@@ -85,14 +85,17 @@
(* List all tuples the first-order assignment [asg] assigns to [vars]
- in order in which [vars] are given. Raise Not_found if the assignment
- is empty. Use [elems] as the set of all elements of the structure. *)
+ in order in which [vars] are given. [elems] are are all elements. *)
let rec tuples elems vars = function
- | Empty -> raise Not_found
+ | Empty -> []
| Any -> List.rev_map Array.of_list
(Aux.product (List.rev_map (fun _ -> Structure.Elems.elements elems) vars))
| FO (`FO v, asg_list) ->
- let (idx, vs) = (Aux.find_index v vars, Aux.remove_one v vars) in
+ let (idx, vs) =
+ try
+ (Aux.find_index v vars, Aux.remove_one v vars)
+ with Not_found ->
+ failwith ("assigned var "^ v ^ " not in "^ (String.concat "," vars)) in
let prolong e asg =
Array.of_list (Aux.insert_nth idx e (Array.to_list asg)) in
List.concat (List.rev_map (fun (e, asg) ->
Modified: trunk/Toss/Solver/AssignmentSet.mli
===================================================================
--- trunk/Toss/Solver/AssignmentSet.mli 2010-11-21 20:45:43 UTC (rev 1187)
+++ trunk/Toss/Solver/AssignmentSet.mli 2010-11-21 21:34:02 UTC (rev 1188)
@@ -33,6 +33,5 @@
(string * int) list -> assignment_set -> (string * int) list
(* List all tuples the first-order assignment [asg] assigns to [vars]
- in order in which [vars] are given. Raise Not_found if the assignment
- is empty. Use [elems] as the set of all elements of the structure. *)
+ in order in which [vars] are given. [elems] are are all elements. *)
val tuples : Structure.Elems.t -> string list -> assignment_set -> int array list
Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml 2010-11-21 20:45:43 UTC (rev 1187)
+++ trunk/Toss/Solver/Solver.ml 2010-11-21 21:34:02 UTC (rev 1188)
@@ -207,15 +207,10 @@
eval_m struc
(RealExpr (Plus (expr, Times (Const (-1.), RVar rvar)), Formula.EQZero))
-let rec remove_dup acc = function
- | [] -> acc
- | [x] -> x :: acc
- | x :: y :: xs when x = y -> remove_dup acc (y :: xs)
- | x :: y :: xs -> remove_dup (x :: acc) (y :: xs)
(* Fast function to get a value of a real expression without free variables
other than those assigned in [asg] explicitely. *)
-let rec get_real_val_a solver asg expr struc =
+let rec get_real_val solver asg expr struc =
let rec check_f = function
Ex (vs, phi) -> check_f phi
| Or (fl) -> List.exists check_f fl
@@ -224,10 +219,10 @@
Char phi -> if check_f phi then 1. else 0.
| Const v -> v
| Times (e1, e2) ->
- (get_real_val_a solver asg e1 struc) *. (get_real_val_a solver asg e2 struc)
+ (get_real_val solver asg e1 struc) *. (get_real_val solver asg e2 struc)
| Plus (e1, e2) ->
- (get_real_val_a solver asg e1 struc) +. (get_real_val_a solver asg e2 struc)
- | Sum (vl, guard, r) -> (* TODO; FIXME; is asg ok down here? *)
+ (get_real_val solver asg e1 struc) +. (get_real_val solver asg e2 struc)
+ | Sum (vl, guard, r) ->
let gd = (
try
let gd_id = List.assoc guard !(solver.reg_formulas) in
@@ -235,13 +230,19 @@
with Not_found ->
Hashtbl.find solver.formulas_eval (register_formula solver guard)
) in
- if !debug_level > 0 then print_endline ("guard " ^ (Formula.str guard));
- let asg = eval_m struc gd in
- let tps = tuples struc.elements (List.map var_str vl) asg in
- let stps = remove_dup [] (List.sort Pervasives.compare tps) in
- let add_val acc tp =
- acc+.(get_real_val_a solver (join asg (asg_of_tuple struc vl tp)) r struc) in
- List.fold_left add_val 0. stps
+ let all_vs = (List.map to_fo (AssignmentSet.assigned_vars [] asg)) @ vl in
+ if !debug_level > 0 then (
+ print_endline ("guard " ^ (Formula.str guard));
+ print_endline ("asg " ^ (AssignmentSet.str asg));
+ print_endline ("sum vars " ^ (Formula.var_list_str vl));
+ print_endline ("all vars " ^ (Formula.var_list_str all_vs));
+ );
+ let asg_gd = join asg (eval_m struc gd) in
+ let tps = tuples struc.elements (List.map var_str all_vs) asg_gd in
+ let add_val acc tp =
+ let tp_asg = asg_of_tuple struc all_vs tp in
+ acc +. (get_real_val solver tp_asg r struc) in
+ List.fold_left add_val 0. tps
| _ ->
let rec get_rval = function
| FO (_, [(_, a)]) -> get_rval a
@@ -258,8 +259,6 @@
AssignmentSet.str ev_assgn) in
get_rval (join asg (evaluate_real "#" expr struc))
-let get_real_val expr struc =
- get_real_val_a (new_solver ()) Any expr struc
(* Evaluate i-th formula on j-th structure. *)
let evaluate solver ~formula struc =
@@ -288,7 +287,7 @@
let evaluate struc formula = evaluate solver ~formula struc
let check_formula struc formula =
check solver ~formula struc
- let get_real_val = get_real_val_a solver Any
+ let get_real_val = get_real_val solver Any
let formula_str phi =
let phi = Hashtbl.find solver.formulas_check phi in
Formula.str phi
Modified: trunk/Toss/Solver/Solver.mli
===================================================================
--- trunk/Toss/Solver/Solver.mli 2010-11-21 20:45:43 UTC (rev 1187)
+++ trunk/Toss/Solver/Solver.mli 2010-11-21 21:34:02 UTC (rev 1188)
@@ -23,7 +23,8 @@
Assignments.assignment_set
(* Fast function to get a value of a real expression without free variables. *)
-val get_real_val : Formula.real_expr -> Structure.structure -> float
+val get_real_val : solver -> Assignments.assignment_set ->
+ Formula.real_expr -> Structure.structure -> float
(* ------------------------- DEBUGGING ------------------------------------- *)
Modified: trunk/Toss/Solver/SolverTest.ml
===================================================================
--- trunk/Toss/Solver/SolverTest.ml 2010-11-21 20:45:43 UTC (rev 1187)
+++ trunk/Toss/Solver/SolverTest.ml 2010-11-21 21:34:02 UTC (rev 1188)
@@ -1,4 +1,5 @@
open Solver ;;
+open OUnit ;;
Solver.set_debug_level 0 ;;
Sat.set_debug_level 0;;
@@ -13,129 +14,144 @@
FormulaParser.parse_real_expr Lexer.lex (Lexing.from_string s)
;;
-let nstruc_of_string s =
+let struc_of_string s =
StructureParser.parse_structure Lexer.lex (Lexing.from_string s)
;;
-let struc_of_string s = let struc = nstruc_of_string s in struc ;;
-let test_eval struc_s phi_s =
+let eval_eq struc_s phi_s aset_s =
let (struc, phi) = (struc_of_string struc_s, formula_of_string phi_s) in
let solver = new_solver () in
let f = register_formula solver phi in
- print_string "Evaluating\n ";
- print_endline (Formula.str phi);
- print_string "on\n ";
- print_endline (Structure.str struc);
- print_string "returns:\n ";
- print_endline (AssignmentSet.str (evaluate solver f struc));
- print_endline ""
+ assert_equal ~printer:(fun x -> x)
+ (AssignmentSet.str (evaluate solver f struc)) aset_s
;;
-let test_eval_real struc_s expr_s =
+let eval_real_eq var_s struc_s expr_s aset_s =
let (struc, expr) = (struc_of_string struc_s, real_expr_of_string expr_s) in
- print_string "Evaluating real expr as r_var\n ";
- print_endline (Formula.real_str expr);
- print_string "on\n ";
- print_endline (Structure.str struc);
- print_string "returns:\n ";
- print_endline (AssignmentSet.str (evaluate_real "r_var" expr struc));
- print_endline ""
+ assert_equal ~printer:(fun x -> x)
+ (AssignmentSet.str (evaluate_real var_s expr struc)) aset_s
;;
-let test_real_val struc_s expr_s =
+let real_val_eq struc_s expr_s x =
let (struc, expr) = (struc_of_string struc_s, real_expr_of_string expr_s) in
- print_string ("Real value of " ^ (Formula.real_str expr) ^ " on\n ");
- print_string ((Structure.str struc) ^ "\nis: ");
- print_endline ((string_of_float (get_real_val expr struc)) ^ "\n");
+ assert_equal ~printer:(fun x -> string_of_float x)
+ (get_real_val (new_solver ()) AssignmentSet.Any expr struc) x
;;
-test_eval "[ | R { (a, b); (a, c) } | ]" "ex x R (x, y)" ;;
-test_eval "[ | R { (a, b); (a, c) } | ]" "x = y" ;;
+let tests = "Solver" >::: [
+ "eval: first-order quantifier free" >::
+ (fun () ->
+ eval_eq "[ | R { (a, b); (a, c) } | ]" "x = y"
+ "{ y->1{ x->1 } , y->2{ x->2 } , y->3{ x->3 } }";
+ eval_eq "[ | R { (a, b); (b, c) }; P { b } | ]" "P(x) and x = y"
+ "{ y->2{ x->2 } }";
+ eval_eq "[ | R { (a, b); (a, c) } | ]" "R(x, y) and x = y"
+ "{}";
+ eval_eq "[ | R { (a, a); (a, b) } | ]" "R(x, y) and x = y"
+ "{ y->1{ x->1 } }";
+ eval_eq "[ | R { (a, b); (a, c) } | ]" "not x = y"
+ "{ y->1{ x->2, x->3 } , y->2{ x->1, x->3 } , y->3{ x->1, x->2 } }";
+ eval_eq "[ | R { (a, a); (a, c) } | ]" "R (x, y) and not x = y"
+ "{ y->2{ x->1 } }";
+ );
-test_eval "[ | R { (a, b); (b, c) }; P { b } | ]" "P(x) and x = y" ;;
+ "eval: first-order with quantifiers" >::
+ (fun () ->
+ eval_eq "[ | R { (a, b); (a, c) } | ]" "ex x R (x, y)"
+ "{ y->2, y->3 }";
+ eval_eq "[ | R { (a, b); (b, c) }; P { b } | ]"
+ "ex x ( P(x) and not (ex y R(x, y)) )"
+ "{}";
+ );
-test_eval "[ | R { (a, b); (a, c) } | ]" "R(x, y) and x = y" ;;
+ "eval: mso quantifier free basic" >::
+ (fun () ->
+ eval_eq "[ | P { a } | ]" "x in X"
+ "{ x->1{ X->(inc {1} excl {}) } }";
+ eval_eq "[ | P { a } | ]" "not (x in X)"
+ "{ x->1{ X->(inc {} excl {1}) } }";
+ eval_eq "[ | P { a } | ]" "x in X and x in Y"
+ "{ x->1{ Y->(inc {1} excl {}){ X->(inc {1} excl {}) } } }";
+ eval_eq "[ | P { a } | ]" "x in X and not (x in Y)"
+ "{ x->1{ Y->(inc {} excl {1}){ X->(inc {1} excl {}) } } }";
+ eval_eq "[ | P { a } | ]" "x in X and x = y and not (x in X)"
+ "{}";
+ eval_eq "[ | P { a } | ]" "x in X and x in Y and (x = y and not (x in Y))"
+ "{}";
+ eval_eq "[ | P { a } | ]" "x in X and (x in X or x in Y)"
+ "{ x->1{ X->(inc {1} excl {}) } }";
+ );
-test_eval "[ | R { (a, a); (a, b) } | ]" "R(x, y) and x = y" ;;
+ "eval: mso quantifier free" >::
+ (fun () ->
+ eval_eq "[ | P { a } | ]" "(t in X2) and ((t in X) or ((t in C)))"
+ ("{ t->1{ X2->(inc {1} excl {}){ X->(inc {} excl {}){ C->(inc {1}" ^
+ " excl {}) }, X->(inc {1} excl {}) } } }");
+ eval_eq "[ | P { a } | ]" "(t in X2) and ((t in X) or ((t in C) or (t in X)))"
+ ("{ t->1{ X2->(inc {1} excl {}){ X->(inc {} excl {}){ C->(inc {1}" ^
+ " excl {}) }, X->(inc {1} excl {}) } } }");
+ eval_eq "[ | P { a } | ]"
+ "(((t in X2) and ((t in X) or (((t in C) or (t in X)) and ((not t in C)
+ or (not (t in X))))) and ((not (t in X)) or ((t in C) and (t in X)) or
+ ((not (t in C)) and (not (t in X))))))"
+ "{ t->1{ X2->(inc {1} excl {}){ C->(inc {1} excl {}) } } }";
+ );
-test_eval "[ | R { (a, b); (b, c) }; P { b } | ]"
- "ex x ( P(x) and not (ex y R(x, y)) )" ;;
+ "eval: mso with only first-order quantifiers" >::
+ (fun () ->
+ eval_eq "[ | P { a } | ]"
+ "(not t in X2) or ((t in X2) and (t in X3)) and
+ all s (s in X3 or not P(s))"
+ ("{ t->1{ X3->(inc {} excl {}){ X2->(inc {} excl {1}) }," ^
+ " X3->(inc {1} excl {}) } }");
+ );
-test_eval "[ | R { (a, b); (a, c) } | ]" "not x = y" ;;
+ "eval: mso with quantifiers" >::
+ (fun () ->
+ let reach_f =
+ "all X (x in X and (all z,v (z in X and R(z,v)-> v in X))-> y in X)" in
+ eval_eq "[ | R { (a, b); (a, c) } | ]" reach_f
+ "{ y->1{ x->1 } , y->2{ x->1, x->2 } , y->3{ x->1, x->3 } }";
+ eval_eq "[ | R { (a, b); (b, c) } | ]" reach_f
+ "{ y->1{ x->1 } , y->2{ x->1, x->2 } , y->3 }";
+ eval_eq "[ | R { (a,b); (b,c); (c,d); (d,e); (e,f); (f,g); (g,h) } | ]"
+ ("x != y and not R(x, y) and " ^ reach_f)
+ ("{ y->3{ x->1 } , y->4{ x->1, x->2 } , y->5{ x->1, x->2, x->3 } ," ^
+ " y->6{ x->1, x->2, x->3, x->4 } , y->7{ x->1, x->2, x->3, x->4," ^
+ " x->5 } , y->8{ x->1, x->2, x->3, x->4, x->5, x->6 } }");
+ );
-test_eval "[ | R { (a, a); (a, c) } | ]" "R (x, y) and not x = y" ;;
+ "eval: with real values" >::
+ (fun () ->
+ eval_eq "[ | P { x } | ] " "ex :x ((:x^2 + 3*:x + 2 < 0) and (:x < 0))"
+ "T";
+ eval_eq "[ | P { x } | f { x -> 1, y -> 2, z -> 3 } ]" ":f(x) > 2"
+ "{ x->3 }";
+ eval_eq "[ | P { x } | f { x -> 1, y -> 2, z -> 3 } ]"
+ "ex :x (:x^2 + :x * :f(x) + 2 < 0)"
+ "{ x->3 }";
+ eval_eq "[ | R { (a, a); (a, b) } | ] " ":(all y (R (x, y))) > 0"
+ "{ x->1 }";
+ );
-test_eval "[ | P { a } | ]" "x in X" ;;
-
-test_eval "[ | P { a } | ]" "not (x in X)" ;;
-
-test_eval "[ | P { a } | ]" "x in X and x in Y" ;;
-
-test_eval "[ | P { a } | ]" "x in X and not (x in Y)" ;;
-
-test_eval "[ | P { a } | ]" "x in X and x = y and not (x in X)" ;;
-
-test_eval "[ | P { a } | ]" "x in X and x in Y and (x = y and not (x in Y))" ;;
-
-test_eval "[ | P { a } | ]" "x in X and (x in X or x in Y)" ;;
-
-test_eval "[ | P { a } | ]" "(t in X2) and ((t in X) or ((t in C)))" ;;
-
-test_eval "[ | P { a } | ]" "(t in X2) and ((t in X) or ((t in C) or (t in X)))" ;;
-
-test_eval "[ | P { a } | ]"
- ("(((t in X2) and ((t in X) or (((t in C) or (t in X)) and ((not (t in C)) or" ^
- " (not (t in X))))) and ((not (t in X)) or ((t in C) and (t in X)) or ((not (t in C)) and (not (t in X))))))") ;;
-
-test_eval "[ | P { a } | ]" "(not t in X2) or ((t in X2) and (t in X3)) and all s (s in X3 or not P(s))" ;;
-
-let reach_f =
- "all X (x in X and ( all z,v (z in X and R (z, v) -> v in X )) -> y in X)" ;;
-
-test_eval "[ | R { (a, b); (a, c) } | ]" reach_f ;;
-
-test_eval "[ | R { (a, b); (b, c) } | ]" reach_f ;;
-
-test_eval "[ | R { (a,b); (b,c); (c,d); (d,e); (e,f); (f,g); (g,h) } | ]"
- ("x != y and not R(x, y) and " ^ reach_f) ;;
-
-test_eval "[ | P { x } | ] " "ex :x ((:x^2 + 3*:x + 2 < 0) and (:x < 0))" ;;
-
-test_eval "[ | P { x } | f { x -> 1, y -> 2, z -> 3 } ]" ":f(x) > 2" ;;
-
-test_eval "[ | P { x } | f { x -> 1, y -> 2, z -> 3 } ]"
- "ex :x (:x^2 + :x * :f(x) + 2 < 0)" ;;
-
-test_eval "[ | R { (a, a); (a, b) } | ] " ":(all y (R (x, y))) > 0" ;;
-
-test_eval_real "[ | R { (a, a); (a, b) } | ] " ":(all y (R (x, y)))" ;;
-
-test_real_val "[ | R { (a, a); (a, b) } | ] " ":(ex x (R (x, x))) + 1" ;;
-
-test_real_val "[ | P { x } | f { x->1, y->2, z->3 } ]" "Sum (x | true : :f(x)^2)" ;;
-
-test_real_val "[ | R { (a, a); (a, b) } | ] " "Sum (x | true : :(all y (R (x, y))))";;
-
-test_real_val "[ | R { (a, a); (a, b) } | ] " "Sum (x | all y (R (x, y)) : 1)";;
-
-test_real_val "[ | P { x } | f { x->1, y->2, z->3 } ]"
- "Sum (x, y | P(x) : :f(x) * :f(y))" ;;
-
-test_real_val "[ | P { x } | f { x->1, y->2, z->3 } ]"
- "Sum (x, y | true : :f(x) * :f(y))" ;;
-
-test_real_val "[ | R { (a, a); (a, b) } | ] " "Sum (x, y | R (x, y) : 1)";;
-
-
-(* Heuristic guard evaluation test. *)
-
-let heur_phi = "(((R(v, w) and R(w, x) and R(x, y) and R(y, z)) or (C(v, w) and C(w, x) and C(x, y) and C(y, z)) or ex r, s, t, u ((C(z, u) and R(y, u) and C(y, t) and R(x, t) and C(x, s) and R(w, s) and C(w, r) and R(v, r))) or ex r, s, t, u ((R(y, u) and R(x, t) and R(w, s) and R(v, r) and C(u, z) and C(t, y) and C(s, x) and C(r, w)))) and (Q(z) or Q(y) or Q(x) or Q(w) or Q(v)) and (not P(v)) and (not P(w)) and (not P(x)) and (not P(y)) and (not P(z))" ^
- "and (not ex v, w, x, y, z ((((C(y, z) and C(x, y) and C(w, x) and C(v, w)) or (R(y, z) and R(x, y) and R(w, x) and R(v, w)) or ex r, s, t, u ((R(y, u) and R(x, t) and R(w, s) and R(v, r) and C(u, z) and C(t, y) and C(s, x) and C(r, w))) or ex r, s, t, u ((C(z, u) and R(y, u) and C(y, t) and R(x, t) and C(x, s) and R(w, s) and C(w, r) and R(v, r)))) and P(z) and P(y) and P(x) and P(w) and P(v)))))" ;;
-
-(* Formula.print (FormulaOps.tnf_fv (formula_of_string heur_phi)) ;; *)
-
-test_eval "[ | | ] \"
+ "eval: game heuristic tests" >::
+ (fun () ->
+ let heur_phi = "(((R(v, w) and R(w, x) and R(x, y) and R(y, z)) or
+ (C(v, w) and C(w, x) and C(x, y) and C(y, z)) or ex r, s, t, u
+ ((C(z, u) and R(y, u) and C(y, t) and R(x, t) and C(x, s) and R(w, s)
+ and C(w, r) and R(v, r))) or ex r, s, t, u ((R(y, u) and R(x, t) and
+ R(w, s) and R(v, r) and C(u, z) and C(t, y) and C(s, x) and C(r, w))))
+ and (Q(z) or Q(y) or Q(x) or Q(w) or Q(v)) and (not P(v)) and (not P(w))
+ and (not P(x)) and (not P(y)) and (not P(z))" ^
+ "and (not ex v, w, x, y, z ((((C(y, z) and C(x, y) and C(w, x) and
+ C(v, w)) or (R(y, z) and R(x, y) and R(w, x) and R(v, w)) or
+ ex r, s, t, u ((R(y, u) and R(x, t) and R(w, s) and R(v, r) and C(u, z)
+ and C(t, y) and C(s, x) and C(r, w))) or ex r, s, t, u ((C(z, u) and
+ R(y, u) and C(y, t) and R(x, t) and C(x, s) and R(w, s) and C(w, r) and
+ R(v, r)))) and P(z) and P(y) and P(x) and P(w) and P(v)))))" in
+ let _ () = Formula.print (FormulaOps.tnf_fv (formula_of_string heur_phi)) in
+ eval_eq "[ | | ] \"
... ... ... ...
P ... ... ... ...
... ... ... ...
@@ -152,10 +168,64 @@
...P ... P.. ...
... ... ... ...
... ... ...Q ...
-\"" heur_phi ;;
+\"" heur_phi
+ ("{ z->5{ y->12{ x->19{ w->26{ v->33 } } } } ," ^
+ " z->6{ y->5{ x->4{ w->3{ v->2 } } } } ," ^
+ " z->7{ y->6{ x->5{ w->4{ v->3 } } } } ," ^
+ " z->8{ y->7{ x->6{ w->5{ v->4 } } } } ," ^
+ " z->32{ y->39{ x->46{ w->53{ v->60 } } } } ," ^
+ " z->48{ y->47{ x->46{ w->45{ v->44 } } } } ," ^
+ " z->53{ y->44{ x->35{ w->26{ v->17 } } } } ," ^
+ " z->58{ y->50{ x->42{ w->34{ v->26 } } } } ," ^
+ " z->62{ y->53{ x->44{ w->35{ v->26 } } } } ," ^
+ " z->63{ y->54{ x->45{ w->36{ v->27 } } } } }");
+ );
+ "eval real: basic" >::
+ (fun () ->
+ eval_real_eq "r" "[ | R { (a, a); (a, b) } | ] " ":(all y (R (x, y)))"
+ "{ x->1{ ((1.) + ((-1.)*r) = 0) } , x->2{ ((0.) + ((-1.)*r) = 0) } }";
+ );
+ "get real val" >::
+ (fun () ->
+ real_val_eq "[ | R { (a, a); (a, b) } | ] "
+ ":(ex x (R (x, x))) + 1" 2.;
+ real_val_eq "[ | P { x } | f { x->1, y->2, z->3 } ]"
+ "Sum (x | true : :f(x)^2)" 14.;
+ real_val_eq "[ | R { (a, a); (a, b) } | ] "
+ "Sum (x | true : :(all y (R (x, y))))" 1.;
+ real_val_eq "[ | R { (a, a); (a, b) } | ] "
+ "Sum (x | all y (R (x, y)) : 1)" 1.;
+ real_val_eq "[ | P { x } | f { x->1, y->2, z->3 } ]"
+ "Sum (x, y | P(x) : :f(x) * :f(y))" 6.;
+ real_val_eq "[ | P { x } | f { x->1, y->2, z->3 } ]"
+ "Sum (x, y | true : :f(x) * :f(y))" 36.;
+ real_val_eq "[ | R { (a, a); (a, b) } | ] "
+ "Sum (x, y | R (x, y) : 1)" 2.;
+ );
+] ;;
+
+let a =
+ let file_from_path p =
+ String.sub p (String.rindex p '/'+1)
+ (String.length p - String.rindex p '/' - 1) in
+ let test_fname name =
+ let fname = file_from_path Sys.executable_name in
+ String.length fname >= String.length name &&
+ String.sub fname 0 (String.length name) = name in
+ (* So that the tests are not run twice while building TossTest. *)
+ if test_fname "SolverTest" then
+ match test_filter [""] tests with
+ | Some tests -> ignore (run_test_tt ~verbose:true tests)
+ | None -> ()
+;;
+
+
+
+
+
(* ----------------------- FOUR POINTS PROBLEM --------------------------- *)
(*
Modified: trunk/Toss/TossTest.ml
===================================================================
--- trunk/Toss/TossTest.ml 2010-11-21 20:45:43 UTC (rev 1187)
+++ trunk/Toss/TossTest.ml 2010-11-21 21:34:02 UTC (rev 1188)
@@ -1,7 +1,7 @@
open OUnit
let formula_tests = "Formula" >::: [
- AuxTest.tests;
+ (* AuxTest.tests; *)
FormulaTest.tests;
FormulaOpsTest.tests;
FFTNFTest.tests;
@@ -10,6 +10,7 @@
let solver_tests = "Solver" >::: [
StructureTest.tests;
FFSolverTest.tests;
+ SolverTest.tests;
]
let arena_tests = "Arena" >::: [
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <luk...@us...> - 2010-11-21 20:45:53
|
Revision: 1187
http://toss.svn.sourceforge.net/toss/?rev=1187&view=rev
Author: lukstafi
Date: 2010-11-21 20:45:43 +0000 (Sun, 21 Nov 2010)
Log Message:
-----------
Cleanup of Aux: removed unused functions, some functions used once moved to their use site. AuxTest test suite.
Modified Paths:
--------------
trunk/Toss/Arena/DiscreteRule.ml
trunk/Toss/Formula/Aux.ml
trunk/Toss/Formula/Aux.mli
trunk/Toss/Formula/BoolFormula.ml
trunk/Toss/Formula/FFTNF.ml
trunk/Toss/Play/Game.ml
trunk/Toss/Play/Heuristic.ml
trunk/Toss/Solver/AssignmentSet.ml
trunk/Toss/Solver/Assignments.ml
trunk/Toss/Solver/FFSolver.ml
trunk/Toss/Solver/Structure.ml
trunk/Toss/TossTest.ml
Modified: trunk/Toss/Arena/DiscreteRule.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRule.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Arena/DiscreteRule.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -209,10 +209,7 @@
let enumerate_matchings model rule matches =
let all_elems = Structure.Elems.elements model.Structure.elements in
let assgns =
- (* Aux.drop_repeating (
- List.sort Pervasives.compare ( *)
- enumerate_assgns all_elems rule.lhs_elem_vars matches
- (* )) *) in
+ enumerate_assgns all_elems rule.lhs_elem_vars matches in
List.map (assignment_to_embedding rule) assgns
(* Helpers for special relations. *)
@@ -228,6 +225,12 @@
Some (String.sub rel 1 (String.index_from rel 1 '_' - 1))
with Not_found -> None
+(* Return the result of the first index [i] that passes the
+ given test, and [i+1]. *)
+let rec first_i n gen test =
+ let res = gen n in
+ if test res then n+1, res else first_i (n+1) gen test
+
(* Rewrite the model [given_model], allowing the elements to be
cloned and deleted. Also change the "trace" of rewritten
elements.
@@ -251,7 +254,7 @@
let _, alloc_elems, rmmap =
List.fold_left (fun (next, alloc_elems, rmmap) evar ->
let next, nelem =
- Aux.first_i next (fun i->i) (fun i-> not (Els.mem i elems)) in
+ first_i next (fun i->i) (fun i-> not (Els.mem i elems)) in
next, nelem::alloc_elems, (evar, nelem)::rmmap)
(1, [], []) rule_obj.rhs_elem_vars in
(* Select a nice name in case elements in the model are named. In
@@ -470,6 +473,44 @@
module STups = Structure.Tuples
+(** Return the nth dimensional "triangle matrix", as the set of [n]
+ element subsets of [l]. *)
+let triang_product n l =
+ let rec mult1 = function
+ | [],[] -> []
+ | [_],[_] -> []
+ | e::es,(_::rs) -> List.map (fun r->e::r) rs::mult1 (es, rs)
+ | _ -> failwith "triang_product: impossible" in
+ let rec mult2 = function
+ (*| [],[] -> []*)
+ | [_],[] -> []
+ | [_;_],[_] -> []
+ | e::es,(_::rs) -> List.map (List.map (fun r->e::r)) rs::mult2 (es, rs)
+ | _ -> failwith "triang_product: impossible" in
+ let rec multn = function
+ | _,[] -> []
+ | _,[_] -> []
+ | _,[_;[[]]] -> []
+ | e::es,(_::rs) ->
+ List.map (concat_map (List.map (fun r->e::r))) rs::multn (es, rs)
+ | _ -> failwith "triang_product: impossible" in
+ let ls = List.map (fun e->[e]) l in
+ match n with
+ | 0 -> []
+ | 1 -> ls
+ | 2 -> List.flatten (mult1 (l,ls))
+ | 3 ->
+ let lls = mult1 (l,ls) in
+ List.flatten (List.flatten (mult2 (l,lls)))
+ | n ->
+ let rec aux n acc =
+ if n=0 then acc
+ else aux (n-1) (multn (l,acc)) in
+ let lls = mult1 (l,ls) in
+ let llls = mult2 (l,lls) in
+ List.flatten (List.flatten (aux (n-3) llls))
+
+
(** Translate a rule specification into a processed form. Note that
when a relation is in $\tau_h$, and is present in the LHS but not
in the RHS, it is still not removed by a rewrite.
@@ -598,8 +639,8 @@
(* check if the map is a total 1-1 onto, if so, [rlmap=None], optimize *)
let rlmap =
let rimg, ldom = List.split rule_src.rule_s in
- let rimg = Aux.drop_repeating (List.sort Pervasives.compare rimg)
- and ldom = Aux.drop_repeating (List.sort Pervasives.compare ldom) in
+ let rimg = Aux.unique (=) rimg
+ and ldom = Aux.unique (=) ldom in
let nimg = List.length rimg and ndom = List.length ldom in
if nimg = Els.cardinal rule_src.rhs_struc.Structure.elements &&
ndom = Els.cardinal rule_src.lhs_struc.Structure.elements &&
Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Formula/Aux.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -30,15 +30,6 @@
in
List.rev (maps_f [] l)
-let rec map_some2 f l1 l2 =
- match (l1, l2) with
- ([], []) -> []
- | (a1::l1, a2::l2) ->
- (match f a1 a2 with
- | None -> map_some2 f l1 l2
- | Some r -> r :: map_some2 f l1 l2)
- | (_, _) -> invalid_arg "map_some2"
-
let map_reduce mapf redf red0 l =
match List.sort (fun x y -> compare (fst x) (fst y))
(List.map mapf l) with
@@ -50,38 +41,19 @@
List.rev (List.map (fun (k,vs) -> k, List.fold_left redf red0 vs)
((k0,vs)::l))
-let rec drop_repeating = function
- | hd::(nk::tl as rest) when hd = nk -> drop_repeating rest
- | hd::tl -> hd::drop_repeating tl
- | tl -> tl
-
-let rec has_repeating = function
- | [] -> false
- | hd::tl when List.mem hd tl -> true
- | hd::tl -> has_repeating tl
-
let list_remove v l = List.filter (fun w->v<>w) l
-let list_existsi p l =
- let rec aux i = function
- | [] -> false
- | a::l -> p i a || aux (i+1) l in
- aux 0 l
-
let rec rev_assoc l x = match l with
[] -> raise Not_found
- | (a,b)::l -> if compare b x = 0 then a else rev_assoc l x
+ | (a,b)::l -> if b = x then a else rev_assoc l x
let rev_assoc_all l x =
let rec aux acc = function
| [] -> acc
| (a,b)::l ->
- if compare b x = 0 then aux (a::acc) l else aux acc l in
+ if b = x then aux (a::acc) l else aux acc l in
aux [] l
-let replace_assoc k v l =
- (k, v)::(List.remove_assoc k l)
-
let rec replace_assoc k v = function
| [] -> [k, v]
| (a, b as pair) :: l ->
@@ -95,53 +67,10 @@
else aux (pair :: acc) l in
aux [] l
-
-let find_max cmp l =
- let rec find acc = function
- | hd::tl ->
- if cmp hd acc <= 0 then find acc tl
- else find hd tl
- | [] -> acc in
- match l with
- | [] -> invalid_arg "find_max: empty list"
- | hd::tl -> find hd tl
-
-let find_all_max cmp l =
- let rec find best acc = function
- | hd::tl ->
- let rel = cmp hd best in
- if rel < 0 then find best acc tl
- else if rel = 0 then find best (hd::acc) tl
- else find hd [hd] tl
- | [] -> acc in
- match l with
- | [] -> invalid_arg "find_all_max: empty list"
- | hd::tl -> find hd [hd] tl
-
-let insert_ordered cmp e l =
- let rec aux = function
- | [] -> [e]
- | hd::_ as l when cmp e hd <= 0 -> e::l
- | hd::tl -> hd::aux tl in
- aux l
-
let unsome = function
| Some v -> v
| None -> raise (Invalid_argument "unsome")
-let rev_map_choose f l =
- let rec rmap_f accu = function
- | [] -> None, accu, []
- | a::tl ->
- match f a with
- | Left r -> rmap_f (r :: accu) tl
- | Right r -> Some r, accu, tl in
- rmap_f [] l
-
-let rec try_find f = function
- | [] -> raise Not_found
- | hd::tl -> try f hd with Not_found -> try_find f tl
-
let rec map_try f = function
| [] -> []
| hd::tl ->
@@ -155,75 +84,21 @@
concat_map (fun el -> List.map (fun tup -> el::tup) prod) set)
l [[]]
-let gproduct f r0 l =
- List.fold_right (fun set prod ->
- concat_map (fun el -> List.map (fun tup -> f el tup) prod) set)
- l [r0]
+let all_tuples_for args elems =
+ List.fold_left (fun tups _ ->
+ concat_map (fun e -> (List.map (fun tup -> e::tup) tups))
+ elems) [[]] args
-let triang_product n l =
- let rec mult1 = function
- | [],[] -> []
- | [_],[_] -> []
- | e::es,(_::rs) -> List.map (fun r->e::r) rs::mult1 (es, rs)
- | _ -> failwith "triang_product: impossible" in
- let rec mult2 = function
- (*| [],[] -> []*)
- | [_],[] -> []
- | [_;_],[_] -> []
- | e::es,(_::rs) -> List.map (List.map (fun r->e::r)) rs::mult2 (es, rs)
- | _ -> failwith "triang_product: impossible" in
- let rec multn = function
- | _,[] -> []
- | _,[_] -> []
- | _,[_;[[]]] -> []
- | e::es,(_::rs) ->
- List.map (concat_map (List.map (fun r->e::r))) rs::multn (es, rs)
- | _ -> failwith "triang_product: impossible" in
- let ls = List.map (fun e->[e]) l in
- match n with
- | 0 -> []
- | 1 -> ls
- | 2 -> List.flatten (mult1 (l,ls))
- | 3 ->
- let lls = mult1 (l,ls) in
- List.flatten (List.flatten (mult2 (l,lls)))
- | n ->
- let rec aux n acc =
- if n=0 then acc
- else aux (n-1) (multn (l,acc)) in
- let lls = mult1 (l,ls) in
- let llls = mult2 (l,lls) in
- List.flatten (List.flatten (aux (n-3) llls))
-
let rec remove_one e = function
| hd::tl when hd = e -> tl
| hd::tl -> hd::(remove_one e tl)
| [] -> []
-let rec remove_nth n = function
- | [] -> invalid_arg "remove_nth"
- | hd::tl when n<=0 -> tl
- | hd::tl -> hd::(remove_nth (n-1) tl)
+let rec insert_nth n e = function
+ | l when n<=0 -> e::l
+ | [] -> raise Not_found
+ | hd::tl -> hd::(insert_nth (n-1) e tl)
-
-let rec extract_nth n = function
- | [] -> invalid_arg "extract_nth"
- | hd::tl when n<=0 -> hd, tl
- | hd::tl ->
- let e, tl = extract_nth (n-1) tl in
- e, hd::tl
-
-let rec replace_nth n e = function
- | [] -> invalid_arg "replace_nth"
- | hd::tl when n<=0 -> e::tl
- | hd::tl -> hd::(replace_nth (n-1) e tl)
-
-
-let rec add_nth n e = function
- | [] -> [e]
- | hd::tl when n<=0 -> e::hd::tl
- | hd::tl -> hd::(add_nth (n-1) e tl)
-
let find_index v l =
let rec aux n = function
| [] -> raise Not_found
@@ -231,20 +106,6 @@
| _::tl -> aux (n+1) tl in
aux 0 l
-let sample n l =
- let s = List.length l in
- let rec samp n =
- if n=0 then []
- else (List.nth l (Random.int s))::samp (n-1) in
- samp n
-
-let rec first_i n gen test =
- let res = gen n in
- if test res then n+1, res else first_i (n+1) gen test
-
-let rec map_for b n f =
- if b < n then (f b)::(map_for (b+1) n f) else []
-
let maximal cmp l =
let rec aux acc = function
| hd::tl when
@@ -257,13 +118,10 @@
(* TODO: that's quadratic, perhaps (sort |> drop_repeating)
would be faster in practice *)
-let unique cmp l =
- let rec aux acc = function
- | hd::tl when not (List.exists (fun x->cmp hd x) acc) ->
- aux (hd::acc) tl
- | hd::tl -> aux acc tl
- | [] -> acc in
- List.rev (aux [] l)
+let rec unique eq = function
+ | [] -> []
+ | x :: xs ->
+ x :: unique eq (List.filter (fun y -> not (eq y x)) xs)
let take_n n l =
let rec aux n acc = function
@@ -272,36 +130,6 @@
| _ -> acc in
List.rev (aux n [] l)
-let take_n_unique n l =
- let rec aux n acc = function
- | hd::tl when n > 0 && not (List.mem hd acc) ->
- aux (n-1) (hd::acc) tl
- | hd::tl when n > 0 -> aux n acc tl
- | _ -> acc in
- List.rev (aux n [] l)
-
-let concat_unique ls =
- let rec conc acc = function
- | [] -> acc
- | []::rest -> conc acc rest
- | (hd::tl)::rest when List.mem hd acc -> conc acc (tl::rest)
- | (hd::tl)::rest -> conc (hd::acc) (tl::rest) in
- List.rev (conc [] ls)
-
-let prefix_free ls =
- let rec prefix = function
- | [],[] -> false
- | [],_ -> true
- | hd1::tl1, hd2::tl2 when hd1=hd2 -> prefix (tl1,tl2)
- | _ -> false in
- let rec aux acc = function
- | hd::tl when not (List.exists (fun x->hd=x) acc) &&
- not (List.exists (fun l2->prefix (l2,hd)) ls) ->
- aux (hd::acc) tl
- | hd::tl -> aux acc tl
- | [] -> acc in
- List.rev (aux [] ls)
-
let array_map2 f a b =
let l = Array.length a in
if l <> Array.length b then
@@ -317,58 +145,9 @@
r
end
-let array_mapi2 f a b =
- let l = Array.length a in
- if l <> Array.length b then
- raise (Invalid_argument "Aux.array_mapi2")
- else
- if l = 0 then [||] else begin
- let r = Array.create l
- (f 0 (Array.unsafe_get a 0) (Array.unsafe_get b 0)) in
- for i = 1 to l - 1 do
- Array.unsafe_set r i
- (f i (Array.unsafe_get a i) (Array.unsafe_get b i))
- done;
- r
- end
-
-let array_fold_map f acc a =
- let l = Array.length a in
- if l = 0 then acc, [||] else begin
- let acc, e = f acc (Array.unsafe_get a 0) in
- let prev = ref acc in
- let r = Array.create l e in
- for i = 1 to l - 1 do
- let acc, e = f !prev (Array.unsafe_get a i) in
- prev := acc;
- Array.unsafe_set r i e
- done;
- !prev, r
- end
-
let array_combine a b =
- let l = Array.length a in
- if l <> Array.length b then
- raise (Invalid_argument "Aux.array_combine")
- else
- if l = 0 then [||] else begin
- let r = Array.create l
- (Array.unsafe_get a 0, Array.unsafe_get b 0) in
- for i = 1 to l - 1 do
- Array.unsafe_set r i
- (Array.unsafe_get a i, Array.unsafe_get b i)
- done;
- r
- end
+ array_map2 (fun x y->x,y) a b
-let array_exists p a =
- let res = ref false in
- let i = ref 0 in
- while !i < Array.length a && not !res do
- res := p (Array.unsafe_get a !i);
- incr i
- done; !res
-
let array_existsi p a =
let res = ref false in
let i = ref 0 in
@@ -378,7 +157,7 @@
done; !res
let array_mem e a =
- array_exists (fun x -> e=x) a
+ array_existsi (fun _ x -> e=x) a
let array_from_assoc l =
match l with
@@ -401,54 +180,6 @@
| hd::tl -> Array.unsafe_set a i (f hd); fill (i+1) tl in
fill 1 tl
-(* Same as [Array.of_list (List.concat (List.map (fun x-> List.map (g
- x) (f x)) l))] *)
-let array_concat_map_of_list f g = function
- [] -> [||]
- | hd::tl as l ->
- let ls = List.map f l in
- let len =
- List.fold_left (fun acc l->acc + List.length l) 0 ls in
- if len = 0 then [||] else
- let org = ref l in
- let rec seek = function
- | [] -> assert false
- | []::tl -> org := List.tl !org; seek tl
- | (hd::_)::_ -> hd in
- let e = seek ls in
- let a = Array.make len (g (List.hd !org) e) in
- let hd = ref (List.hd ls) and tl = ref (List.tl ls) in
- while !hd=[] do
- hd := List.hd !tl; tl := List.tl !tl
- done;
- let e = ref (List.hd !org) in
- hd := List.tl !hd;
- for i=1 to len-1 do
- while !hd=[] do
- hd := List.hd !tl; tl := List.tl !tl;
- org := List.tl !org; e := List.hd !org
- done;
- Array.unsafe_set a i (g !e (List.hd !hd));
- hd := List.tl !hd
- done;
- a
-
-let array_fold_while p f x a =
- let r = ref x and i = ref 0 in
- let n = Array.length a in
- while !i < n && p (Array.unsafe_get a !i) do
- r := f !r (Array.unsafe_get a !i); incr i
- done;
- !r
-
-let array_find f a =
- let i = ref 0 in
- let n = Array.length a in
- while !i < n && not (f (Array.unsafe_get a !i)) do
- incr i done;
- if !i >= n then raise Not_found
- else Array.unsafe_get a !i
-
let array_argfind f a =
let i = ref 0 in
let n = Array.length a in
@@ -473,37 +204,6 @@
done;
!r
-let array_for_all f a =
- try
- for i = 0 to Array.length a - 1 do
- if not (f (Array.unsafe_get a i)) then
- raise Not_found
- done;
- true
- with Not_found -> false
-
-let array_for_all2 f a b =
- let len = min (Array.length a) (Array.length b) in
- try
- for i = 0 to len - 1 do
- if not (f (Array.unsafe_get a i) (Array.unsafe_get b i)) then
- raise Not_found
- done;
- true
- with Not_found -> false
-
-let array_argfind_max cmp a =
- let n = Array.length a in
- if n=0 then failwith "array_argfind_max: empty array"
- else
- let best = ref (Array.unsafe_get a 0)
- and besti = ref 0 in
- for i = 1 to n-1 do
- let e = Array.unsafe_get a i in
- if cmp e !best > 0 then (best := e; besti := i)
- done;
- !besti
-
let array_argfind_all_max cmp a =
let n = Array.length a in
if n=0 then []
@@ -517,12 +217,34 @@
else if res = 0 then besti := i:: !besti
done;
!besti
+
+let array_for_all f a =
+ try
+ for i = 0 to Array.length a - 1 do
+ if not (f (Array.unsafe_get a i)) then
+ raise Not_found
+ done;
+ true
+ with Not_found -> false
+let array_for_all2 f a b =
+ let len = Array.length a in
+ if len <> Array.length b then
+ raise (Invalid_argument "Aux.array_for_all2")
+ else
+ try
+ for i = 0 to len - 1 do
+ if not (f (Array.unsafe_get a i) (Array.unsafe_get b i)) then
+ raise Not_found
+ done;
+ true
+ with Not_found -> false
+
let neg f x = not (f x)
let partition_choice l =
let rec split laux raux = function
- | [] -> laux, raux
+ | [] -> List.rev laux, List.rev raux
| Left e::tl -> split (e::laux) raux tl
| Right e::tl -> split laux (e::raux) tl in
split [] [] l
@@ -536,11 +258,6 @@
| Right e -> split laux (e::raux) tl in
split [] [] l
-let rec split_triples = function
- [] -> ([], [], [])
- | (x,y,z)::l ->
- let (rx, ry, rz) = split_triples l in (x::rx, y::ry, z::rz)
-
let transpose_lists lls =
let rec aux acc = function
| [] -> List.map List.rev acc
@@ -551,28 +268,17 @@
| hd::tl ->
aux (List.map (fun e->[e]) hd) tl
-let all_tuples_for args elems =
- List.fold_left (fun tups _ ->
- concat_map (fun e -> (List.map (fun tup -> e::tup) tups))
- elems) [[]] args
-
let rec fold_n f accu n =
if n <= 0 then accu
else fold_n f (f accu) (n-1)
-let rec foldi_n f accu n =
- let accu = ref accu in
- for i=1 to n do
- accu := f i !accu
- done; !accu
+(* Return the result of the first index [i] that passes the
+ given test, and [i+1]. *)
+let rec first_i n gen test =
+ let res = gen n in
+ if test res then n+1, res else first_i (n+1) gen test
-let all_tuples_n arity elems =
- fold_n (fun tups ->
- concat_map (fun e -> (List.map (fun tup -> e::tup) tups))
- elems) [[]] arity
-
-
let new_filename basename suffix =
if not (Sys.file_exists (basename^suffix))
then basename^suffix else
@@ -585,34 +291,13 @@
snd (first_i 0 (fun i -> s^(string_of_int i))
(fun v -> not (Strings.mem v names)))
-let not_conflicting_name_cands names cands =
- let _ = if cands = [] then
- failwith "not_conflicting_name: no candidates" in
- if List.exists (fun s->not (Strings.mem s names)) cands
- then List.find (fun s->not (Strings.mem s names)) cands
- else
- let ncands = List.map (fun s->
- first_i 0 (fun i -> s^(string_of_int i))
- (fun v -> not (Strings.mem v names))) cands in
- snd (List.hd (List.stable_sort (fun (a,_) (b,_) -> a-b) ncands))
-
let not_conflicting_names s names n =
- snd (List.fold_left (fun (i,res) _ ->
+ List.rev (snd (List.fold_left (fun (i,res) _ ->
let i', v =
first_i i (fun i -> s^(string_of_int i))
(fun v -> not (Strings.mem v names)) in
- i', v::res) (0,[]) n)
+ i', v::res) (0,[]) n))
-let rec split_table columns rows =
- let rec collect = function
- | [], rest -> [], rest
- | hd::tl, e::more ->
- let cols, rest = collect (tl, more) in
- (e::hd)::cols, rest
- | cols, [] -> cols, [] in
- let columns, rest = collect (columns, rows) in
- if rest = [] then columns else split_table columns rest
-
(* Character classes. *)
let is_uppercase c = c >= 'A' && c <= 'Z'
let is_lowercase c = c >= 'a' && c <= 'z'
Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Formula/Aux.mli 2010-11-21 20:45:43 UTC (rev 1187)
@@ -15,109 +15,59 @@
(** Map a list filtering out some elements. *)
val map_some : ('a -> 'b option) -> 'a list -> 'b list
-val map_some2 : ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
-
(** Map elements into key-value pairs, and fold values with the same
- key. *)
+ key. Uses {!List.fold_left}, therefore reverses the order. The
+ resulting keys are sorted in the {!Pervasives.compare} order. *)
val map_reduce :
('a -> 'b * 'c) -> ('d -> 'c -> 'd) -> 'd -> 'a list -> ('b * 'd) list
-(** Return a list of unique elements (using structural equality) for a
- *sorted* input list. *)
-val drop_repeating : 'a list -> 'a list
-
-(** Check if an element of a list repeats, using structural
- equality. *)
-val has_repeating : 'a list -> bool
-
(** Remove all elements equal to the argument, using structural
inequality. *)
val list_remove : 'a -> 'a list -> 'a list
-(** Check if at least one element and its position satisfies the predicate. *)
-val list_existsi : (int -> 'a -> bool) -> 'a list -> bool
-
-(** Return first key with the given value from the key-value pairs. *)
+(** Return first key with the given value from the key-value pairs,
+ using structural equality. *)
val rev_assoc : ('a * 'b) list -> 'b -> 'a
-(** Inverse image of an association: return all keys with a given value. *)
+(** Inverse image of an association: return all keys with a given
+ value (using structural equality). Returns elements in reverse order. *)
val rev_assoc_all : ('a * 'b) list -> 'b -> 'a list
-(** Replace the value of a first occurrence of a key. *)
+(** Replace the value of a first occurrence of a key, or place it at
+ the end of the assoc list. *)
val replace_assoc : 'a -> 'b -> ('a * 'b) list -> ('a * 'b) list
(** Find the value associated with the first occurrence of the key and
remove them from the list. *)
val pop_assoc : 'a -> ('a * 'b) list -> 'b * ('a * 'b) list
-(** Find the first maximal element. Comparison is by [cmp a b <= 0]
- iff [a <= b]. *)
-val find_max : ('a -> 'a -> int) -> 'a list -> 'a
-
-(** Find all maximal elements. *)
-val find_all_max : ('a -> 'a -> int) -> 'a list -> 'a list
-
-(** Insert an element (without repeating it) into an
- increasing-ordered list. *)
-val insert_ordered : ('a -> 'a -> int) -> 'a -> 'a list -> 'a list
-
(** unConstructors. *)
val unsome : 'a option -> 'a
-(** Map a prefix of [Left] elements (returned in reverse order) till
- the first [Right] element (if any), also return the unmapped tail
- of the list. *)
-val rev_map_choose :
- ('a -> ('b, 'c) choice) -> 'a list -> 'c option * 'b list * 'a list
-
-(** Find the first result of [f] on [l] that does not raise [Not_found]. *)
-val try_find : ('a -> 'b) -> 'a list -> 'b
-
(** Map [f] on the list collecting results whose computation does not
raise [Not_found]. Therefore [map_try] call cannot raise [Not_found]. *)
val map_try : ('a -> 'b) -> 'a list -> 'b list
-(** Cartesian product of lists. *)
+(** Cartesian product of lists. Not tail recursive. *)
val product : 'a list list -> 'a list list
-(** Generalized product. [product l = gproduct (fun x y->x::y) [] l]. *)
-val gproduct : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
+(** An [n]th cartesian power of the second list, where [n] is the
+ length of the first list. Tail recursive. *)
+val all_tuples_for : 'a list -> 'b list -> 'b list list
-(** Return the nth dimensional "triangle matrix", as the set of [n]
- element subsets of [l]. *)
-val triang_product : int -> 'a list -> 'a list list
-
(** Remove an occurrence of a value (uses structural equality). *)
val remove_one : 'a -> 'a list -> 'a list
-(** Remove [n+1]th element of a list ([n]th counting from zero). *)
-val remove_nth : int -> 'a list -> 'a list
+(** Insert as [n]th element of a list (counting from zero). Raise
+ [Not_found] if the list has less than [n] elements (e.g. inserting
+ 0th element to empty list is OK). *)
+val insert_nth : int -> 'a -> 'a list -> 'a list
-(** At once access an element as by {!List.nth}, and delete as by
- {!remove_nth}. *)
-val extract_nth : int -> 'a list -> 'a * 'a list
-
-(** Replace [n+1]th element of a list ([n]th counting from zero). *)
-val replace_nth : int -> 'a -> 'a list -> 'a list
-
-(** Add as [n]th element of a list (counting from zero). *)
-val add_nth : int -> 'a -> 'a list -> 'a list
-
(** Find the index of the first occurrence of a value in a list,
counting from zero. *)
val find_index : 'a -> 'a list -> int
-(** Sample from a list with repetitions. *)
-val sample : int -> 'a list -> 'a list
-
-(** Return the result of the first index [i] that passes the
- given test, and [i+1]. *)
-val first_i : int -> (int -> 'a) -> ('a -> bool) -> int * 'a
-
-(** Map the numbers [b..n]. *)
-val map_for : int -> int -> (int -> 'a) -> 'a list
-
(** Return the list of maximal elements, under the given less-or-equal
comparison (the input does not need to be sorted). (Currently, of
equal elements only the last one is preserved.) *)
@@ -126,41 +76,26 @@
(** Return the list of unique elements, under the given comparison
(the input does not need to be sorted). (Currently uses a
straightforward [n^2] algorithm, a sorting-based would reduce it to
- [n log n].) *)
+ [n log n]. Currently not tail-recursive.) *)
val unique : ('a -> 'a -> bool) -> 'a list -> 'a list
(** Take [n] elements of the given list, or less it the list does not
contain enough values. *)
val take_n : int -> 'a list -> 'a list
-(** Take [n] nonrepeating elements of the given list, or less it the
- list does not contain enough values. *)
-val take_n_unique : int -> 'a list -> 'a list
-
-(** Concatenate lists without repeating the elements. *)
-val concat_unique : 'a list list -> 'a list
-
-(** All lists from [l] that are not initial parts of other lists from [l]. *)
-val prefix_free : 'a list list -> 'a list list
-
(** Make an array from an association from indices to values. The
indices must cover the [0..length-1] range; raises
- [Invalid_argument] otherwise. *)
+ [Invalid_argument "Aux.array_from_assoc"] otherwise. *)
val array_from_assoc : (int * 'a) list -> 'a array
(** Map a function over two arrays index-wise. Raises
[Invalid_argument] if the arrays are of different lengths. *)
val array_map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
-val array_mapi2 : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
-(** Map a function over an array threading an accumulator. *)
-val array_fold_map :
- ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
-
-(** Zip two arrays into an array of pairs. *)
+(** Zip two arrays into an array of pairs. Raises [Invalid_argument
+ "Aux.array_map2"] if the arrays are of different lengths. *)
val array_combine : 'a array -> 'b array -> ('a * 'b) array
-val array_exists : ('a -> bool) -> 'a array -> bool
val array_existsi : (int -> 'a -> bool) -> 'a array -> bool
val array_mem : 'a -> 'a array -> bool
@@ -168,20 +103,6 @@
(** Same as [Array.of_list (List.map f l)] *)
val array_map_of_list : ('a -> 'b) -> 'a list -> 'b array
-(** Same as [Array.of_list (List.concat (List.map (fun x-> List.map (g
- x) (f x)) l))]. The first function generates the results and the
- second postprocesses them. *)
-val array_concat_map_of_list
- : ('a -> 'b list) -> ('a -> 'b -> 'c) -> 'a list -> 'c array
-
-(** Like {!Array.fold_left}, but only for the initial elements for
- which the predicate holds. *)
-val array_fold_while :
- ('a -> bool) -> ('b -> 'a -> 'b) -> 'b -> 'a array -> 'b
-
-(** Find the first element that satisfies a predicate. Raises [Not_found]. *)
-val array_find : ('a -> bool) -> 'a array -> 'a
-
val array_argfind : ('a -> bool) -> 'a array -> int
(** Find all elements for which [f] holds. *)
@@ -192,12 +113,11 @@
(** Find if a predicate holds for all elements. *)
val array_for_all : ('a -> bool) -> 'a array -> bool
-(** Find if a predicate holds for all elements of two arrays pointwise. *)
+(** Find if a predicate holds for all elements of two arrays
+ pointwise. Raises [Invalid_argument "Aux.array_for_all2"] if
+ arrays are of different lengths. *)
val array_for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
-(** Find the index of the first maximal element in an array. *)
-val array_argfind_max : ('a -> 'a -> int) -> 'a array -> int
-
(** Find indices of all maximal elements in an array. *)
val array_argfind_all_max : ('a -> 'a -> int) -> 'a array -> int list
@@ -212,42 +132,23 @@
also {!partition_choice}). *)
val partition_map : ('a -> ('b, 'c) choice) -> 'a list -> 'b list * 'c list
-(** Transpose a list of triples into a triple of lists. *)
-val split_triples : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
-
-(** Transpose a rectangular matrix represented by lists. *)
+(** Transpose a rectangular matrix represented by lists. Raises
+ [Invalid_argument "List.map2"] when matrix is not rectangular. *)
val transpose_lists : 'a list list -> 'a list list
-(** An [n]th cartesian power of the second list, where [n] is the
- length of the first list. *)
-val all_tuples_for : 'a list -> 'b list -> 'b list list
-
(** Iterate a function [n] times: [f^n(x)]. *)
val fold_n : ('a -> 'a) -> 'a -> int -> 'a
-(** Fold a function over the [1..n] sequence: [f(n,f(...f(1,x)...))]. *)
-val foldi_n : (int -> 'a -> 'a) -> 'a -> int -> 'a
-
-(** An [n]th cartesian power of a list. *)
-val all_tuples_n : int -> 'a list -> 'a list list
-
(** Generate a fresh filename of the form [base ^ n ^ suffix]. *)
val new_filename : string -> string -> string
(** Returns a string proloning [s] and not appearing in [names]. *)
val not_conflicting_name : Strings.t -> string -> string
-(** Returns a string proloning one of [cands] and not appearing in
- [names]. *)
-val not_conflicting_name_cands : Strings.t -> string list -> string
-
(** Returns [n] strings proloning [s] and not appearing in [names]. *)
val not_conflicting_names :
string -> Strings.t -> 'a list -> string list
-(** Collect columns of a table given by concatenation of rows. *)
-val split_table : 'a list list -> 'a list -> 'a list list
-
(** Character classes. *)
val is_uppercase : char -> bool
val is_lowercase : char -> bool
Modified: trunk/Toss/Formula/BoolFormula.ml
===================================================================
--- trunk/Toss/Formula/BoolFormula.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Formula/BoolFormula.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -261,9 +261,6 @@
then (BOr []) else BAnd (List.map neutral_absorbing filtered) in
let rec singularise unsorted_phi =
let phi = sort unsorted_phi in (* this should be done more elegantly!!! *)
- let rec unique = function (* remove duplicate subformulas *)
- [] -> []
- | x :: xs -> [x] @ (unique (List.filter (fun y -> y<>x) xs)) in
let rec neg_occurrence = function
(* check whether a _sorted_ "uniqued" list contains a pair (phi,not phi)
at the moment this only works for literals due to the implementation of compare! *)
@@ -272,10 +269,10 @@
match phi with
BVar _ -> phi
| BNot psi -> BNot (singularise psi)
- | BOr psis -> let unique_psis = unique psis in
+ | BOr psis -> let unique_psis = Aux.unique (=) psis in
let lits = List.filter is_literal unique_psis in
if neg_occurrence lits then BAnd [] else BOr (List.map singularise unique_psis)
- | BAnd psis -> let unique_psis = unique psis in
+ | BAnd psis -> let unique_psis = Aux.unique (=) psis in
let lits = List.filter is_literal unique_psis in
if neg_occurrence lits then BOr [] else BAnd (List.map singularise unique_psis) in
let rec subsumption phi =
Modified: trunk/Toss/Formula/FFTNF.ml
===================================================================
--- trunk/Toss/Formula/FFTNF.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Formula/FFTNF.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -1073,6 +1073,18 @@
(* build will flatten the formula *)
evs, build false phi
+(* Map a prefix of [Left] elements (returned in reverse order) till
+ the first [Right] element (if any), also return the unmapped tail
+ of the list. *)
+let rev_map_choose f l =
+ let rec rmap_f accu = function
+ | [] -> None, accu, []
+ | a::tl ->
+ match f a with
+ | Left r -> rmap_f (r :: accu) tl
+ | Right r -> Some r, accu, tl in
+ rmap_f [] l
+
(* Step 4. Search depth-first since it's simpler, perhaps results in less
duplication, and there are no clear advantages of breadth-first. *)
let find_active frels evs t =
Modified: trunk/Toss/Play/Game.ml
===================================================================
--- trunk/Toss/Play/Game.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Play/Game.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -477,6 +477,19 @@
v1+.v2) sum table) hd tl in
Array.map (fun v -> v /. n) sum
+(* Find all maximal elements. *)
+let find_all_max cmp l =
+ let rec find best acc = function
+ | hd::tl ->
+ let rel = cmp hd best in
+ if rel < 0 then find best acc tl
+ else if rel = 0 then find best (hd::acc) tl
+ else find hd [hd] tl
+ | [] -> acc in
+ match l with
+ | [] -> invalid_arg "find_all_max: empty list"
+ | hd::tl -> find hd [hd] tl
+
(* Maximaxing: find the best among subtrees for a player. Pick a best
entry in the lexicographic product of: maximal [scores] value for
[player], minimal/maximal sum of [scores] values (resp. competitive
@@ -503,14 +516,14 @@
then fun (_,x) (_,y) -> compare x y
else fun (_,x) (_,y) -> compare y x in
let bestsc =
- Aux.find_all_max cmp_sums sc_sums in
+ find_all_max cmp_sums sc_sums in
match bestsc with
| [] -> failwith "impossible"
| [bestsc,_] -> scores.(bestsc), bestsc
| _ ->
(* pick ones from biggest subtrees *)
let bestsc =
- Aux.find_all_max
+ find_all_max
(fun (b1,_) (b2,_) -> subt_sizes.(b1) - subt_sizes.(b2))
bestsc in
match bestsc with
Modified: trunk/Toss/Play/Heuristic.ml
===================================================================
--- trunk/Toss/Play/Heuristic.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Play/Heuristic.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -307,6 +307,10 @@
List.map (fun v ->
List.map (List.assoc v) substs) vars in
(* TODO: optimizable *)
+ let rec has_repeating = function
+ | [] -> false
+ | hd::tl when List.mem hd tl -> true
+ | hd::tl -> has_repeating tl in
if has_repeating vs_insts
then
[], true, []
@@ -317,6 +321,16 @@
exception Outside_subst of (fo_var * int) list
+let find_max cmp l =
+ let rec find acc = function
+ | hd::tl ->
+ if cmp hd acc <= 0 then find acc tl
+ else find hd tl
+ | [] -> acc in
+ match l with
+ | [] -> invalid_arg "find_max: empty list"
+ | hd::tl -> find hd tl
+
let expanded_descr max_alt_descr elems rels struc
all_vars xvars xsubsts =
let alt_descr = ref 0 in
@@ -633,6 +647,12 @@
(* ********** Heuristic of Payoff Expression ********** *)
+(* Generalized product. [product l = gproduct (fun x y->x::y) [] l]. *)
+let gproduct f r0 l =
+ List.fold_right (fun set prod ->
+ concat_map (fun el -> List.map (fun tup -> f el tup) prod) set)
+ l [r0]
+
let rec limited_dnf neg = function
| (Rel _
| Eq _
@@ -640,7 +660,7 @@
| RealExpr _) as psi -> [[if neg then Not psi else psi]]
| Not psi -> limited_dnf (not neg) psi
| And conjs ->
- Aux.gproduct List.append [] (List.map (limited_dnf neg) conjs)
+ gproduct List.append [] (List.map (limited_dnf neg) conjs)
| Or disjs -> Aux.concat_map (limited_dnf neg) disjs
| Ex (vs, psi) as phi ->
[[if neg then All (vs, Not psi) else phi]]
Modified: trunk/Toss/Solver/AssignmentSet.ml
===================================================================
--- trunk/Toss/Solver/AssignmentSet.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Solver/AssignmentSet.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -93,7 +93,8 @@
(Aux.product (List.rev_map (fun _ -> Structure.Elems.elements elems) vars))
| FO (`FO v, asg_list) ->
let (idx, vs) = (Aux.find_index v vars, Aux.remove_one v vars) in
- let prolong e asg = Array.of_list (Aux.add_nth idx e (Array.to_list asg)) in
+ let prolong e asg =
+ Array.of_list (Aux.insert_nth idx e (Array.to_list asg)) in
List.concat (List.rev_map (fun (e, asg) ->
List.rev_map (prolong e) (tuples elems vs asg)) asg_list)
| _ -> failwith "listing tuples in non first-order assignment set"
Modified: trunk/Toss/Solver/Assignments.ml
===================================================================
--- trunk/Toss/Solver/Assignments.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Solver/Assignments.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -292,24 +292,10 @@
(* ---------------------- UNIVERSAL PROJECTION ------------------------------ *)
-let concat_map f l =
- let rec cmap_f accu = function
- | [] -> accu
- | a::l -> cmap_f (List.rev_append (f a) accu) l
- in
- List.rev (cmap_f [] l)
-
-let product l =
- if List.mem [] l then []
- else
- List.fold_right (fun set prod ->
- concat_map (fun el -> List.map (fun tup -> el::tup) prod) set)
- l [[]]
-
let negate_real_disj poly_disj =
let neg_sign (p, s) = (p, SignTable.neg_sign_op s) in
let ndisj = List.rev_map (fun l -> List.rev_map neg_sign l) poly_disj in
- List.filter RealQuantElim.sat (product ndisj)
+ List.filter RealQuantElim.sat (Aux.product ndisj)
(* Project assignments on a given universal variable. We assume that [elems]
are all elements and are sorted. Corresponds to the for-all v quantifier. *)
Modified: trunk/Toss/Solver/FFSolver.ml
===================================================================
--- trunk/Toss/Solver/FFSolver.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Solver/FFSolver.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -156,6 +156,12 @@
let debug_count = ref 0
+let list_existsi p l =
+ let rec aux i = function
+ | [] -> false
+ | a::l -> p i a || aux (i+1) l in
+ aux 0 l
+
(* We assume that for every "not ex
psi" subformula, "ex psi" is ground, and that every other
occurrence of negation is in a literal (it is guaranteed by
@@ -289,7 +295,7 @@
if List.mem_assoc x sb then 1, y else 0, x in
let oldvars =
List.filter (fun v->List.mem_assoc v sb) vtup in
- let multi_unkn = Aux.list_existsi
+ let multi_unkn = list_existsi
(fun i v->i>nvi && not (List.mem v oldvars)) vtup in
if multi_unkn && (conj_cont <> [] || delayed1 <> [])
then (* delay *)
@@ -401,7 +407,7 @@
if List.mem_assoc x sb then 1, y else 0, x in
let oldvars =
List.filter (fun v->List.mem_assoc v sb) vtup in
- let multi_unkn = Aux.list_existsi
+ let multi_unkn = list_existsi
(fun i v->i>nvi && not (List.mem v oldvars)) vtup in
if multi_unkn && (conj_cont <> [] || delayed1 <> [])
then (* delay *)
Modified: trunk/Toss/Solver/Structure.ml
===================================================================
--- trunk/Toss/Solver/Structure.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Solver/Structure.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -254,6 +254,21 @@
(* ------------ GLOBAL FUNCTIONS TO CREATE STRUCTURES FROM LISTS ------------ *)
+(** Map a function over an array threading an accumulator. *)
+let array_fold_map f acc a =
+ let l = Array.length a in
+ if l = 0 then acc, [||] else begin
+ let acc, e = f acc (Array.unsafe_get a 0) in
+ let prev = ref acc in
+ let r = Array.create l e in
+ for i = 1 to l - 1 do
+ let acc, e = f !prev (Array.unsafe_get a i) in
+ prev := acc;
+ Array.unsafe_set r i e
+ done;
+ !prev, r
+ end
+
(* Add to a named structure elements, relations and functions from the lists. *)
let add_from_lists struc els rels funs =
List.fold_left (fun s (fn, assgns) ->
@@ -271,7 +286,7 @@
| Some ar -> ar in
let s = add_rel_name rn arity s in
List.fold_left (fun s tp ->
- let s, tp = Aux.array_fold_map find_or_new_elem s tp in
+ let s, tp = array_fold_map find_or_new_elem s tp in
add_rel s rn tp) s tps)
(List.fold_left (fun s ne ->
fst (find_or_new_elem s ne)) struc els) rels) funs
@@ -335,31 +350,12 @@
{ del_rels_struc with elements = Elems.remove e del_rels_struc.elements ;
functions = StringMap.map del_fun del_rels_struc.functions ; }
-(* Copied from Server/Aux.ml *)
-let map_reduce mapf redf red0 l =
- match List.sort (fun x y -> Pervasives.compare (fst x) (fst y))
- (List.map mapf l) with
- | [] -> []
- | (k0, v0)::tl ->
- let k0, vs, l = List.fold_left (fun (k0, vs, l) (kn, vn) ->
- if k0 = kn then k0, vn::vs, l else kn, [vn], (k0,vs)::l)
- (k0, [v0], []) tl in
- List.rev (List.map (fun (k,vs) -> k, List.fold_left redf red0 vs)
- ((k0,vs)::l))
-
-let concat_map f l =
- let rec cmap_f accu = function
- | [] -> accu
- | a::l -> cmap_f (List.rev_append (f a) accu) l
- in
- List.rev (cmap_f [] l)
-
(* Remove the elements [es] and all incident relation tuples from
[struc]; return the deleted relation tuples. *)
let del_elems struc es =
let rel_tuples =
- map_reduce (fun x->x) List.rev_append []
- (concat_map (incident struc) es) in
+ Aux.map_reduce (fun x->x) List.rev_append []
+ (Aux.concat_map (incident struc) es) in
let del_rels_struc =
List.fold_left (fun s (rn, tps) -> del_rels s rn tps) struc rel_tuples in
let del_fun fmap =
Modified: trunk/Toss/TossTest.ml
===================================================================
--- trunk/Toss/TossTest.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/TossTest.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -1,6 +1,7 @@
open OUnit
let formula_tests = "Formula" >::: [
+ AuxTest.tests;
FormulaTest.tests;
FormulaOpsTest.tests;
FFTNFTest.tests;
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
