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

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

Revision: 1556
          http://toss.svn.sourceforge.net/toss/?rev=1556&view=rev
Author:   lukaszkaiser
Date:     2011-09-03 00:16:24 +0000 (Sat, 03 Sep 2011)
Log Message:
-----------
Formula and real expr (Let and RLet) expansion, correcting compilation warnings.

Modified Paths:
--------------
    trunk/Toss/Formula/FormulaOps.ml
    trunk/Toss/Formula/FormulaOpsTest.ml
    trunk/Toss/Formula/FormulaSubst.ml
    trunk/Toss/Formula/FormulaSubst.mli
    trunk/Toss/GGP/GameSimpl.ml
    trunk/Toss/Play/Heuristic.ml
    trunk/Toss/Solver/Solver.ml

Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml	2011-09-02 13:37:14 UTC (rev 1555)
+++ trunk/Toss/Formula/FormulaOps.ml	2011-09-03 00:16:24 UTC (rev 1556)
@@ -50,8 +50,7 @@
     | Gfp (r, vs, phi) when neg ->
       Lfp (r, vs, nnf ~neg:true ~rev:((var_str r) :: rev) phi)
     | Gfp (r, vs, phi) -> Gfp (r, vs, nnf ~neg:false ~rev phi)
-    | Let (r, args, body, phi) -> (* subst_rels [(rel, (args, body))] phi *)
-      Let (r, args, nnf body, nnf phi)
+    | Let _ -> nnf ~neg ~rev (expand_formula psi)
 
 
 (* -- Delete quantified variables. --- *)
@@ -64,6 +63,7 @@
       match compare_vars v1 v2 with
           0 -> remove_dup_vars acc (v2::vs)
         | _ -> remove_dup_vars (v1::acc) (v2::vs)
+
 (* Delete all quantification over [vs] in the formula. *)
 let rec del_vars_quant vs = function
   | Eq _ | Rel _ | In _ | SO _ | RealExpr _ as f -> f
@@ -81,6 +81,7 @@
     else All (vr, del_vars_quant vs phi)
   | Lfp (r, xs, phi) -> Lfp (r, xs, del_vars_quant vs phi)
   | Gfp (r, xs, phi) -> Gfp (r, xs, del_vars_quant vs phi)
+  | Let _ as phi -> del_vars_quant vs (expand_formula phi)
 
 
 (* --- Signs of rels --- *)
@@ -262,6 +263,7 @@
   | All (xs, phi) -> All (xs, prenex phi)
   | Lfp (v, vs, phi) -> Lfp (v, vs, prenex phi)
   | Gfp (v, vs, phi) -> Gfp (v, vs, prenex phi)
+  | Let _ as phi -> prenex (expand_formula phi)
 
 let pnf fm = prenex(nnf(fm))
 
@@ -315,6 +317,7 @@
     with Not_found -> atom
   )
   | Not phi -> Not (propagate_univ acc_atoms acc_formulas phi)
+  | Let _ as phi -> propagate_univ acc_atoms acc_formulas (expand_formula phi)
   | Ex (vs, phi) -> Ex (vs, propagate_univ acc_atoms acc_formulas phi)
   | All (vs, phi) -> All (vs, propagate_univ acc_atoms acc_formulas phi)
   | Lfp (v, vs, phi) -> Lfp (v, vs, propagate_univ acc_atoms acc_formulas phi)
@@ -367,7 +370,8 @@
     | Ex  (x, psi) -> Ex  (x, do_simplify (simplify_subformulas psi))
     | All (x, psi) -> All (x, do_simplify (simplify_subformulas psi))
     | Lfp (x, xs, psi) -> Lfp (x, xs, do_simplify (simplify_subformulas psi))
-    | Gfp (x, xs, psi) -> Gfp (x, xs, do_simplify (simplify_subformulas psi)) in
+    | Gfp (x, xs, psi) -> Gfp (x, xs, do_simplify (simplify_subformulas psi))
+    | Let _ as psi -> simplify_subformulas (expand_formula psi) in
   let check_for_variants phi =
     let vars = List.map var_str (all_vars phi) in
     List.exists (fun var -> var.[((String.length var)-1)]='_') vars in
@@ -460,6 +464,7 @@
     let simp_q = simplify_re ~do_pnf ~do_formula ~ni q in
     if simp_p = p && simp_q = q then Times (p, q) else 
       simplify_re ~do_pnf ~do_formula ~ni (Times (simp_p, simp_q))
+  | RLet _ as re -> simplify_re ~do_pnf ~do_formula ~ni (expand_real_expr re)
 
 
 (* Formula as a list of conjuncts, with one level of distributing
@@ -496,7 +501,8 @@
       | Ex (vs, phi) -> Ex (vs, map_formula phi)
       | All (vs, phi) -> All (vs, map_formula phi)
       | Lfp (v, vs, phi) -> Lfp (v, vs, map_formula phi)
-      | Gfp (v, vs, phi) -> Gfp (v, vs, map_formula phi) in
+      | Gfp (v, vs, phi) -> Gfp (v, vs, map_formula phi)
+      | Let _ as phi -> map_formula (expand_formula phi) in
   try Formula.flatten (map_formula phi) with Not_found -> And []
 
 let unused_quants_map = {identity_map with
@@ -825,6 +831,7 @@
     tnf_fun (All ([x], All (xs, phi)))
   | Lfp (v, vs, phi) -> Lfp (v, vs, tnf_fun phi)
   | Gfp (v, vs, phi) -> Gfp (v, vs, tnf_fun phi)
+  | Let _ as phi -> tnf_fun (expand_formula phi)
 
 and tnf_re_fun = function
   | RVar _ | Const _ | Fun _ as x -> x
@@ -832,6 +839,7 @@
   | Plus (re1, re2) -> Plus (tnf_re_fun re1, tnf_re_fun re2)
   | Char (phi) -> Char (flatten_sort (tnf_fun (flatten_sort phi)))
   | Sum (vl, f, r) -> Sum (vl, tnf_fun f, tnf_re_fun r)
+  | RLet _ as re -> tnf_re_fun (expand_real_expr re)
 
 and append_quant vs ~universal flist =
   let (have_v, no_v) = List.partition (has_free vs) flist in
@@ -894,6 +902,7 @@
       let subst = List.map (subst_name_avoiding avs) avoidv in
       let nv = fp_var_subst subst v in
       Gfp (nv, vs, rename_quant_avoiding ((nv :> var) ::  avs) phi)
+  | Let _ as phi -> rename_quant_avoiding avs (expand_formula phi)
 
 
 let rec has_mso = function
@@ -902,6 +911,7 @@
   | Not phi | Ex (_, phi) | All (_, phi) | Lfp (_,_, phi) | Gfp (_,_, phi) ->
     has_mso phi
   | And flist | Or flist -> List.exists has_mso flist
+  | Let _ as phi -> has_mso (expand_formula phi)
 
 let rec has_fo = function
   | In _ -> false
@@ -909,6 +919,7 @@
   | Not phi | Ex (_, phi) | All (_, phi) | Lfp (_,_, phi) | Gfp (_,_, phi) ->
     has_fo phi
   | And flist | Or flist -> List.exists has_fo flist
+  | Let _ as phi -> has_fo (expand_formula phi)
 
 let rec mso_last = function
   | Rel _ | Eq _ | In _ | SO _ | RealExpr _ as phi -> phi
@@ -997,6 +1008,7 @@
     | All (vs, f) -> All (vs, push_in_quant f)
     | Lfp (v, vs, f) -> Lfp (v, vs, push_in_quant f)
     | Gfp (v, vs, f) -> Gfp (v, vs, push_in_quant f)
+    | Let _ -> push_in_quant (expand_formula phi)
 
 let rec push_quant f = push_in_quant (flatten_sort (f))
 

Modified: trunk/Toss/Formula/FormulaOpsTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaOpsTest.ml	2011-09-02 13:37:14 UTC (rev 1555)
+++ trunk/Toss/Formula/FormulaOpsTest.ml	2011-09-03 00:16:24 UTC (rev 1556)
@@ -42,7 +42,7 @@
       nnf_eq "ex x :(all y (R (x, y))) > 0"
 	"ex x :(all y (R (x, y))) > 0";
       nnf_eq "let R(x) = not ex y C(x, y) in not (P(x) or R(x))"
-	"let R(x) = all y not C(x, y) in not P(x) and not R(x)";
+	"not P(x) and ex y C(x, y)";
       nnf_eq "not lfp T(x) = (P(x) or ex y (E(x, y) and y in T))"
 	"gfp T(x) = (not P(x) and all y (not E(x, y) or y in T))";
       nnf_eq "not lfp |R(x, y) = (P(x, y) or ex z (E(x, z) and |R(y, z)))"

Modified: trunk/Toss/Formula/FormulaSubst.ml
===================================================================
--- trunk/Toss/Formula/FormulaSubst.ml	2011-09-02 13:37:14 UTC (rev 1555)
+++ trunk/Toss/Formula/FormulaSubst.ml	2011-09-03 00:16:24 UTC (rev 1556)
@@ -91,6 +91,7 @@
 	  let (_, bad_subst) = newnames new_subst bad_vs in
 	  Gfp (fp_var_subst bad_subst v, subvs,
 	       subst_vars (bad_subst @ new_subst) phi)
+    | Let _ -> failwith "FormulaSubst:subst_vars: let substitution"
 
 and subst_vars_expr subst = function
   | Const _ as x -> x
@@ -104,9 +105,9 @@
     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, subst_vars_expr new_vs r)
+  | RLet _ -> failwith "FormulaSubst:subst_vars_expr: rlet substitution"
 
 
-
 (* --------- SUBSTITUTE DEFINED RELATIONS ------------ *)
 
 (* Substitute in relations defined in [defs] by their definitions. *)
@@ -208,6 +209,7 @@
   | Plus (r1, r2) -> Plus (subst_rels_expr defs r1, subst_rels_expr defs r2)
   | Char (phi) -> Char (subst_rels defs phi)
   | Sum (vs, phi, r) -> Sum (vs, subst_rels defs phi, subst_rels_expr defs r)
+  | RLet _ -> failwith "FormulaSubst:subst_rels_expr: rlet substitution"
 
 (* Assign emptyset to the MSO-variable v by replacing "x in X" with "false".  *)
 let assign_emptyset v phi =
@@ -216,7 +218,30 @@
     | phi -> phi in
   flatten (FormulaMap.map_to_atoms (replace_by_emptyset v) phi)
 
+(* Expand Let's and RLet's in formula. TODO!! FIXME!! add RLet expand
+   and allow recursively defined relations in let-series. *)
+let rec expand_formula = function
+  | Rel _ | Eq _ | In _ | SO _ as phi -> phi
+  | RealExpr (r, sgn) -> RealExpr (expand_real_expr r, sgn)
+  | Not phi -> Not (expand_formula phi)
+  | Or flist -> Or (List.map expand_formula flist)
+  | And flist -> And (List.map expand_formula flist)
+  | Ex (vs, phi) -> Ex (vs, expand_formula phi)
+  | All (vs, phi) -> All (vs, expand_formula phi)
+  | Lfp (v, vs, phi) -> Lfp (v, vs, expand_formula phi)
+  | Gfp (v, vs, phi) -> Gfp (v, vs, expand_formula phi)
+  | Let (rel, args, def, phi) ->
+    let exp = expand_formula phi in subst_rels [(rel, (args, def))] exp
 
+and expand_real_expr = function
+  | RVar _ | Const _ | Fun _ as x -> x
+  | Times (r1, r2) -> Times (expand_real_expr r1, expand_real_expr r2)
+  | Plus (r1, r2) -> Plus (expand_real_expr r1, expand_real_expr r2)
+  | Char (phi) -> Char (expand_formula phi)
+  | Sum (vs, phi, r) -> Sum (vs, expand_formula phi, expand_real_expr r)
+  | RLet _ -> failwith "FormulaSubst:expand real_expr RLet not implemented yet"
+
+
 (* -------------------------- FREE VARIABLES -------------------------------- *)
 
 (* Helper function: remove duplicates from sorted list of variables. *)
@@ -244,6 +269,7 @@
   | Lfp (r, vs, phi) | Gfp (r, vs, phi) -> 
     all_vars_acc 
       ((r :> var):: (List.rev_append ((Array.to_list vs) :> var list) acc)) phi
+  | Let (_, _, def, phi) -> all_vars_acc (all_vars_acc acc def) phi
 
 and all_vars_real = function
   | RVar s -> [s]
@@ -254,6 +280,7 @@
   | Char phi -> List.rev_map var_str (all_vars_acc [] phi)
   | Sum (_, f, r) -> 
     List.rev_append (List.rev_map var_str (all_vars_acc [] f)) (all_vars_real r)
+  | RLet (_, def, re) -> List.rev_append (all_vars_real def) (all_vars_real re)
 
 let all_vars phi =
   remove_dup_vars [] (List.sort compare_vars (all_vars_acc [] phi))
@@ -277,6 +304,7 @@
     let fv_phi = free_vars_acc [] phi in
     List.rev_append ((Array.to_list xs) :> var list) (List.rev_append (
       List.filter (fun v -> not (List.mem v vs)) fv_phi) acc)
+  | Let _ as phi -> free_vars_acc acc (expand_formula phi)
 
 and free_vars_real = function
   | RVar s -> [s]
@@ -288,6 +316,7 @@
   | Sum (vl, _, r) -> 
       let vs = List.map var_str vl in
       List.filter (fun w -> not (List.mem w vs)) (free_vars_real r)
+  | RLet _ as r -> free_vars_real (expand_real_expr r)
 
 let free_vars phi =
   remove_dup_vars [] (List.sort compare_vars (free_vars_acc [] phi))

Modified: trunk/Toss/Formula/FormulaSubst.mli
===================================================================
--- trunk/Toss/Formula/FormulaSubst.mli	2011-09-02 13:37:14 UTC (rev 1555)
+++ trunk/Toss/Formula/FormulaSubst.mli	2011-09-03 00:16:24 UTC (rev 1556)
@@ -28,7 +28,11 @@
 val subst_rels_expr : 
   (string * (string list * formula)) list -> real_expr -> real_expr
 
+(** Expand Let's and RLet's in formula. **)
+val expand_formula : formula -> formula
+val expand_real_expr : real_expr -> real_expr
 
+
 (** {2 MSO empty set assignment} *)
 
 (** Assign emptyset to an MSO-variable. *)

Modified: trunk/Toss/GGP/GameSimpl.ml
===================================================================
--- trunk/Toss/GGP/GameSimpl.ml	2011-09-02 13:37:14 UTC (rev 1555)
+++ trunk/Toss/GGP/GameSimpl.ml	2011-09-03 00:16:24 UTC (rev 1556)
@@ -152,6 +152,7 @@
     | Ex (_, phi) ->
       if not neg then aux neg phi else 0, [phi]
     | Not phi -> aux (not neg) phi
+    | Let _ as phi -> aux neg (FormulaSubst.expand_formula phi)
     | Rel _ | Eq _ | In _ | SO _ | RealExpr _ | Lfp _ | Gfp _ -> 1, [] in
   aux false phi
 

Modified: trunk/Toss/Play/Heuristic.ml
===================================================================
--- trunk/Toss/Play/Heuristic.ml	2011-09-02 13:37:14 UTC (rev 1555)
+++ trunk/Toss/Play/Heuristic.ml	2011-09-03 00:16:24 UTC (rev 1556)
@@ -285,6 +285,7 @@
   | Ex (_,phi) | All (_,phi) | Not phi | Lfp (_, _, phi) | Gfp (_, _, phi) ->
     has_rels frels phi
   | Eq _ | In _ | RealExpr _ | SO _ -> false
+  | Let _ as phi -> has_rels frels (FormulaSubst.expand_formula phi)
 
 let add_tuples nts ts =
   List.fold_left (fun ts nt -> Structure.Tuples.add nt ts) ts nts
@@ -797,11 +798,14 @@
     [[if neg then Not phi else phi]]
   | All (vs, psi) as phi ->
       [[if neg then Ex (vs, Not psi) else phi]]
+  | Let _ as phi -> limited_dnf neg (FormulaSubst.expand_formula phi)
 
 let rec has_pos_existential ?(neg=false) = function
   | Not phi -> has_pos_existential ~neg:(not neg) phi
   | And phs | Or phs -> List.exists (has_pos_existential ~neg) phs
-  | Ex _ -> not neg | All _ -> neg | _ -> false
+  | Ex _ -> not neg | All _ -> neg
+  | Let _ as phi -> has_pos_existential ~neg (FormulaSubst.expand_formula phi)
+  | _ -> false
 
 
 let rec map_constants f = function
@@ -813,6 +817,7 @@
   | Sum (vs, phi, es) ->
       Sum (vs, phi, map_constants f es)
   | RVar _ | Fun _ | Char _ as expr -> expr
+  | RLet _ as re -> map_constants f (FormulaSubst.expand_real_expr re)
 
 let normalized_mult coefs =
   let n = List.length coefs in
@@ -941,6 +946,7 @@
     | RVar _ 
     | Const _
     | Fun _ as expr -> expr
+    | RLet _ as re -> aux gds (FormulaSubst.expand_real_expr re)
     | Times (a, b) -> Times (aux gds a, aux gds b)
     | Plus (a, b) -> Plus (aux gds a, aux gds b)
     | Char phi ->

Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml	2011-09-02 13:37:14 UTC (rev 1555)
+++ trunk/Toss/Solver/Solver.ml	2011-09-03 00:16:24 UTC (rev 1556)
@@ -204,21 +204,23 @@
 	let a0 = eval ((v, alltps)::fp) model elems asg0 phi in
 	let fp_res = if a0 = Any then Any else fixpnt v vll phi a0 in
 	report (simp (join aset fp_res))
+      | Let _ -> eval fp model elems aset (FormulaSubst.expand_formula phi)
 
 and assignment_of_real_expr fp ?(check=true) model elems (p, sgn) =
   let rec fo_vars_r_rec = function
-      RVar s -> []
+    | RVar s -> []
     | Const _ -> []
     | Times (r1, r2) -> List.rev_append (fo_vars_r_rec r1) (fo_vars_r_rec r2)
     | Plus (r1, r2) -> List.rev_append (fo_vars_r_rec r1) (fo_vars_r_rec r2)
     | Fun (s, v) -> [v] 
     | Char phi ->
-        let fv = FormulaSubst.free_vars phi in
-        if List.exists (function `FO _ -> false | _ -> true) fv then
-          failwith "non first-order free vars in real_expr not yet supported"
-        else List.rev_map to_fo fv
+      let fv = FormulaSubst.free_vars phi in
+      if List.exists (function `FO _ -> false | _ -> true) fv then
+        failwith "non first-order free vars in real_expr not yet supported"
+      else List.rev_map to_fo fv
     | Sum (vl, _, r) ->
-        List.filter (fun w -> not (List.mem w vl)) (fo_vars_r_rec r) in
+      List.filter (fun w -> not (List.mem w vl)) (fo_vars_r_rec r)
+    | RLet _ as re -> fo_vars_r_rec (FormulaSubst.expand_real_expr re) in
   let fo_vars_real re = 
     remove_dup_vars [] (List.sort compare_vars (fo_vars_r_rec re)) in
   let rec sum_polys = function
@@ -231,7 +233,7 @@
     | Real [[(poly, _)]] -> poly
     | Real _ -> failwith "too many polynomials in assignement to sum over" in
   let rec poly_of assgn = function
-      RVar s -> Poly.Var s
+    | RVar s -> Poly.Var s
     | Const f -> Poly.Const f
     | Times (r1, r2) -> Poly.Times (poly_of assgn r1, poly_of assgn r2)
     | Plus (r1, r2) -> Poly.Plus (poly_of assgn r1, poly_of assgn r2)
@@ -250,7 +252,8 @@
         let fo_aset = List.fold_left make_fo_asg Any assgn in
         let r_a = assignment_of_real_expr fp ~check:false model elems (r,sgn) in
         let asg = join (eval fp model elems fo_aset guard) r_a in
-        sum_polys asg (* Note: above "sgn" is irrelevant! *) in
+        sum_polys asg (* Note: above "sgn" is irrelevant! *)
+    | RLet _ as re -> poly_of assgn (FormulaSubst.expand_real_expr re) in
   let rec process_vars assgn = function
     | [] -> 
       let poly = poly_of assgn p in

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