[Toss-devel-svn] SF.net SVN: toss:[1197] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1197] trunk/Toss
|
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.
|
