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

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

Revision: 1429
          http://toss.svn.sourceforge.net/toss/?rev=1429&view=rev
Author:   lukaszkaiser
Date:     2011-05-01 23:21:01 +0000 (Sun, 01 May 2011)

Log Message:
-----------
Finishing adding fixed-points to formulas, cleanups in FormulaOps and related corrections.

Modified Paths:
--------------
    trunk/Toss/Arena/Arena.ml
    trunk/Toss/Arena/DiscreteRule.ml
    trunk/Toss/Formula/BoolFunctionTest.ml
    trunk/Toss/Formula/FFTNF.ml
    trunk/Toss/Formula/FFTNFTest.ml
    trunk/Toss/Formula/FormulaOps.ml
    trunk/Toss/Formula/FormulaOps.mli
    trunk/Toss/Formula/FormulaOpsTest.ml
    trunk/Toss/Formula/FormulaParser.mly
    trunk/Toss/GGP/GameSimpl.ml
    trunk/Toss/GGP/Makefile
    trunk/Toss/GGP/tests/breakthrough-simpl.toss
    trunk/Toss/GGP/tests/connect5-simpl.toss
    trunk/Toss/GGP/tests/tictactoe-simpl.toss
    trunk/Toss/Play/Heuristic.ml
    trunk/Toss/Play/HeuristicTest.ml
    trunk/Toss/Solver/ClassTest.ml

Modified: trunk/Toss/Arena/Arena.ml
===================================================================
--- trunk/Toss/Arena/Arena.ml	2011-05-01 16:34:53 UTC (rev 1428)
+++ trunk/Toss/Arena/Arena.ml	2011-05-01 23:21:01 UTC (rev 1429)
@@ -495,11 +495,9 @@
             "At location %d, only the second game has label %s->%d"
             i label.rule dest));
         let poff1 =
-          FormulaOps.map_to_formulas_expr FormulaOps.flatten_formula
-            loc1.payoff in
+          FormulaOps.map_to_formulas_expr Formula.flatten loc1.payoff in
         let poff2 =
-          FormulaOps.map_to_formulas_expr FormulaOps.flatten_formula
-            loc2.payoff in
+          FormulaOps.map_to_formulas_expr Formula.flatten loc2.payoff in
         if poff1 <> poff2 then raise (Diff_result (
           Printf.sprintf
             "At location %d, payffs for player %d differ:\n%s\nvs.\n%s"

Modified: trunk/Toss/Arena/DiscreteRule.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRule.ml	2011-05-01 16:34:53 UTC (rev 1428)
+++ trunk/Toss/Arena/DiscreteRule.ml	2011-05-01 23:21:01 UTC (rev 1429)
@@ -880,7 +880,7 @@
       lhs_neg_tups @
     List.map (function [x;y] -> Not (Eq (`FO x, `FO y))
       | _ -> assert false) lhs_alldif_tups @
-      FormulaOps.flatten_ands precond
+      (FormulaOps.as_conjuncts precond)
   ) in
 
   (* Substitute defined relations, expanding their special variants. *)
@@ -1026,7 +1026,7 @@
   );
   (* }}} *)
   let conjs =
-    FormulaOps.flatten_ands (FormulaOps.remove_redundant precond) in
+    FormulaOps.as_conjuncts (FormulaOps.remove_redundant precond) in
   let posi, conjs = Aux.partition_map (function
     | Formula.Rel (rel, args) when rewritable args ->
       Left (rel,args)
@@ -1253,8 +1253,8 @@
       Structure.compare_diff ~cmp_funs r1.rhs_struc r2.rhs_struc in
     if not eq then raise (Diff_result (
       "Rule RHS structures differ: "^msg));
-    let pre1 = FormulaOps.flatten_formula r1.pre in
-    let pre2 = FormulaOps.flatten_formula r2.pre in
+    let pre1 = Formula.flatten r1.pre in
+    let pre2 = Formula.flatten r2.pre in
     if pre1 <> pre2 then raise (Diff_result (
       Printf.sprintf "Rule preconditions differ:\n%s\n =/=\n%s"
         (Formula.sprint pre1) (Formula.sprint pre2)));

Modified: trunk/Toss/Formula/BoolFunctionTest.ml
===================================================================
--- trunk/Toss/Formula/BoolFunctionTest.ml	2011-05-01 16:34:53 UTC (rev 1428)
+++ trunk/Toss/Formula/BoolFunctionTest.ml	2011-05-01 23:21:01 UTC (rev 1429)
@@ -82,7 +82,7 @@
 	"(R(n) & (exists M m. R(m)))";
       test_mod_subst "R(m) & ex M m (R(m) | R(n))" [("m", "n")] 
 	"(R(n) & (exists M m. (R(m) | R(n))))";
-      test_mod_subst "ex M m R(x)" [("x", "m")] "(exists M m0. R(m))";
+      test_mod_subst "ex M m R(x, m)" [("x", "m")] "(exists M m0. R(m, m0))";
       test_mod_subst "R(m) & ex M m (S(m) | T(x))" [("x", "m"); ("m", "x")]
 	"(R(x) & (exists M m0. (S(m0) | T(m))))";
     );

Modified: trunk/Toss/Formula/FFTNF.ml
===================================================================
--- trunk/Toss/Formula/FFTNF.ml	2011-05-01 16:34:53 UTC (rev 1428)
+++ trunk/Toss/Formula/FFTNF.ml	2011-05-01 23:21:01 UTC (rev 1429)
@@ -197,32 +197,28 @@
 
   let rec nnf ?(neg=false) psi = 
     match psi with
-        Rel _ | Eq _ | In _ | RealExpr _ as atom ->
-          if neg then Not atom else atom
+      | Rel _ | Eq _ | In _ | SO _ | RealExpr _ | Lfp _ | Gfp _ as atom ->
+        if neg then Not atom else atom
       | Not phi -> if neg then nnf ~neg:false phi else nnf ~neg:true phi
       | And (flist) when neg -> Or (List.map (nnf ~neg:true) flist)
       | And (flist) -> And (List.map (nnf ~neg:false) flist)
       | Or (flist) when neg -> And (List.map (nnf ~neg:true) flist)
       | Or (flist) -> Or (List.map (nnf ~neg:false) flist)
-      | Ex (x, _) as phi when neg && FormulaOps.free_vars phi = []
-                         -> Not (pn_nnf phi)
+      | Ex (x, _) as phi when neg && FormulaOps.free_vars phi = [] ->
+	Not (pn_nnf phi)
       | Ex (x, phi) when neg -> All (x, nnf ~neg:true phi)
       | Ex (x, phi) -> Ex (x, nnf ~neg:false phi)
       | All (x, phi) when neg -> Ex (x, nnf ~neg:true phi)
-      | All (x, phi) as sbt when not neg && FormulaOps.free_vars sbt = []
-                            -> Not (pn_nnf (Ex (x, nnf ~neg:true phi)))
+      | All (x, phi) as sbt when not neg && FormulaOps.free_vars sbt = [] ->
+	Not (pn_nnf (Ex (x, nnf ~neg:true phi)))
       | All (x, phi) -> All (x, nnf ~neg:false phi)
 
   and pn_nnf phi =
     let rec pnf ex vars sb = function
-      | (Rel _ 
-            | Eq _
-            | In _ 
-            | RealExpr _) as psi ->
+      | Rel _ | Eq _ | In _ | SO _ | RealExpr _ | Lfp _ | Gfp _ as psi ->
         [], vars, FormulaOps.subst_vars sb psi
-      | Not (Ex _) as phi -> [], vars, phi
-    (* already processed recursively *)
-      | Not psi as phi ->                 (* already reduced to NNF *)
+      | Not (Ex _) as phi -> [], vars, phi (* already processed recursively *)
+      | Not psi as phi ->                  (* already reduced to NNF *)
         [], vars, FormulaOps.subst_vars sb phi
       | And conjs ->
         let (prefs, vars, conjs) =
@@ -454,14 +450,16 @@
 
 (* Useful for debugging. *)
 let rec unpack_flat = function
+  | Rel _ | Eq _ | In _ | SO _ | RealExpr _ as atom -> atom
+  | Not phi -> Not (unpack_flat phi)
   | Or [phi] -> Or [Rel ("NOOP", [||]); unpack_flat phi]
   | And [phi] -> And [Rel ("NOOP", [||]); unpack_flat phi]
   | Or fl -> Or (List.map unpack_flat fl)
   | And fl -> And (List.map unpack_flat fl)
   | All (vs, phi) -> All (vs, unpack_flat phi)
   | Ex (vs, phi) -> Ex (vs, unpack_flat phi)
-  | Not phi -> Not (unpack_flat phi)
-  | (Rel _ | Eq _ | In _ | RealExpr _) as atom -> atom
+  | Lfp (v, vs, phi) -> Lfp (v, vs, unpack_flat phi)
+  | Gfp (v, vs, phi) -> Gfp (v, vs, unpack_flat phi)
 
 let location_str loc =
   sprintf "%s#[%s]"
@@ -559,18 +557,17 @@
     | phi -> res, phi in
   let revpref, phi =
     prefix Top (p_pn_nnf ~do_pnf phi) in
-  let phi = FormulaOps.flatten_formula phi in
+  let phi = Formula.flatten phi in
   let protected lit qvs =
     let lit_vs = FormulaOps.all_vars lit in
     List.for_all (fun v->List.mem v lit_vs) qvs in
   let rec to_tree last_qvs = function
     | Not (Ex _ as phi) ->              (* assumes [phi] is ground! *)
       {fvs=Vars.empty; t=TNot_subtask phi}
-    | (Rel _ | Eq _ | In _ | RealExpr _ | Not _) as lit
+    | (Rel _ | Eq _ | In _ | SO _ | RealExpr _ | Not _ | Lfp _ | Gfp _) as lit
         when not do_pnf && protected lit last_qvs ->
       {fvs=vars_of_list (FormulaOps.all_vars lit); t=TProc (0,lit)}
-
-    | (Rel _ | Eq _ | In _ | RealExpr _ | Not _) as lit ->
+    | (Rel _ | Eq _ | In _ | SO _ | RealExpr _ | Not _ | Lfp _ | Gfp _) as lit->
       {fvs=vars_of_list (FormulaOps.all_vars lit); t=TLit lit}
     | And conjs ->
       List.fold_right (fun conj -> function {fvs=vs; t=TAnd conjs} ->
@@ -927,7 +924,7 @@
     match force_parsimony with
       | Some parl -> parl
       | None ->
-        let size = FormulaOps.size phi in
+        let size = Formula.size phi in
         if size < !parsimony_threshold_1 then 0
         else if size < !parsimony_threshold_2 then 1
         else 2 in
@@ -1108,11 +1105,11 @@
       aux neg (add_vars vs evs) phi
     | All (vs, phi) when neg ->
       aux neg (add_vars vs evs) phi
-    | Ex _ | All _ | Or [] | And [] -> evs
+    | Ex _ | All _ | Lfp _ | Gfp _ | Or [] | And [] -> evs
     | Not phi -> aux (not neg) evs phi
     | Or (phi::js) | And (phi::js) ->
       aux neg (aux neg evs phi) (And js)
-    | Rel _ | RealExpr _ | Eq _ | In _ -> evs in
+    | Rel _ | RealExpr _ | Eq _ | In _ | SO _ -> evs in
   let evs = aux false Vars.empty phi in
   let fevs = add_vars fvs evs in
   let is_active neg rel vs =
@@ -1123,8 +1120,9 @@
     | Rel (rel, vs) -> is_active neg rel (Formula.var_tup vs)
     | Not phi -> has_active (not neg) phi
     | And js | Or js -> List.exists (has_active neg) js
-    | Ex (_, phi) | All (_, phi) -> has_active neg phi
-    | Eq _ | In _ | RealExpr _ -> false in
+    | Ex (_, phi) | All (_, phi) | Lfp (_, _, phi) | Gfp (_, _, phi) -> 
+      has_active neg phi
+    | Eq _ | In _ | RealExpr _ | SO _ -> false in
   let rec build neg phi =
     if not (has_active neg phi) then
       {fvs=vars_of_list (FormulaOps.free_vars phi);
@@ -1159,7 +1157,7 @@
           let t = if neg then TAnd js else TOr js in
           {fvs=List.fold_left (fun fvs jt -> Vars.union fvs jt.fvs)
               Vars.empty js; t=t}
-        | RealExpr _ | In _ | Eq _ -> assert false
+        | RealExpr _ | In _ | Eq _ | SO _ | Lfp _ | Gfp _ -> assert false
   and build_and neg phi =
     match build neg phi with
       | {t=TAnd js} when not neg -> js
@@ -1309,6 +1307,6 @@
     let avs = FormulaOps.free_vars (And atoms) in
     let avs = List.map Formula.to_fo
       (List.filter (fun v->not (List.mem v fvs)) avs) in
-    avs, unique (=) atoms, FormulaOps.flatten_formula
+    avs, unique (=) atoms, Formula.flatten
       (erase_qs false (formula_of_tree tree))) forest
 

Modified: trunk/Toss/Formula/FFTNFTest.ml
===================================================================
--- trunk/Toss/Formula/FFTNFTest.ml	2011-05-01 16:34:53 UTC (rev 1428)
+++ trunk/Toss/Formula/FFTNFTest.ml	2011-05-01 23:21:01 UTC (rev 1429)
@@ -259,7 +259,7 @@
 
       (* TODO? simplify the result *)
       assert_eq_str ~msg:"#3"
-        "ex y (C(y, z) and R(x, y)) or ex z (Q(z) and ex y true) or ex x (P(x) and ex y R(x, y))"
+        "ex y (C(y, z) and R(x, y)) or ex z (Q(z) and true) or ex x (P(x) and ex y R(x, y))"
         (Formula.str (
           formula_of_guards (Aux.strings_of_list ["P"; "Q"])
             Aux.Strings.empty

Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml	2011-05-01 16:34:53 UTC (rev 1428)
+++ trunk/Toss/Formula/FormulaOps.ml	2011-05-01 23:21:01 UTC (rev 1429)
@@ -430,27 +430,84 @@
       | `Real s -> `Real (subst_str s)
 
 let fo_var_subst subst (v : fo_var) = to_fo (var_subst subst v)
+let fp_var_subst s (v : [ mso_var | so_var ]) = to_mso_or_so (var_subst s v)
 
+(* Find a substitution for [v] which avoids [avs], string arguments *)
+let subst_name_avoiding_str avs var_s =
+  (* Helper: strip digits from string end if it doesn't start 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 in
+  let v = strip_digits var_s in
+  let rec asubst i =
+    let vi = v ^ (string_of_int i) in
+    if not (List.mem vi avs) then (var_s, vi) else asubst (i+1) in
+  if List.mem var_s avs then asubst 0 else (var_s, var_s)
+
+(* Find a substitution for [v] which avoids [avs]. *)
+let subst_name_avoiding avoidv var =
+  subst_name_avoiding_str (List.rev_map var_str avoidv) (var_str var)
+
 (* Apply substitution [subst] to all free variables in the given
    formula. Preserves order of subformulas. *)
-let rec subst_vars subst = function
-  | Rel (rn, vs) -> Rel (rn, Array.map (fo_var_subst subst) vs)
-  | Eq (x, y) -> Eq (fo_var_subst subst x, fo_var_subst subst y)
-  | In (x, y) -> In (fo_var_subst subst x, to_mso (var_subst subst y))
-  | SO (v, vs) ->
-    SO (to_so (var_subst subst v), Array.map (fo_var_subst subst) vs)
-  | RealExpr (r, sgn) -> RealExpr (subst_vars_expr subst r, sgn)
-  | Not phi -> Not (subst_vars subst phi)
-  | Or flist -> Or (List.map (subst_vars subst) flist)
-  | And flist -> And (List.map (subst_vars subst) flist)
-  | Ex (vs, phi) -> 
-    let in_vs (s, _) = List.exists (fun v -> var_str v = s) vs in
-    let new_vs = List.filter (fun x -> not (in_vs x)) subst in
-    if new_vs = [] then Ex (vs, phi) else Ex (vs, subst_vars new_vs phi)
-  | All (vs, phi) -> 
-    let in_vs (s, _) = List.exists (fun v -> var_str v = s) vs in
-    let new_vs = List.filter (fun x -> not (in_vs x)) subst in
-    if new_vs = [] then All (vs, phi) else All (vs, subst_vars new_vs phi)
+let rec subst_vars subst phi =
+  let splitvs sub vars =
+    let vs = List.rev_map (fun v -> var_str v) vars in
+    let new_sub = List.filter (fun (v, _) -> not (List.mem v vs)) sub in
+    let in_new_sub v = List.exists (fun (_, new_v) -> v = new_v) new_sub in
+    (List.partition (fun v -> in_new_sub (var_str v)) vars, new_sub) in
+  let newnames sub vars =
+    let aviodvs = List.map snd sub in
+    let new_n v = snd (subst_name_avoiding_str aviodvs (var_str v)) in
+    let new_vsub v = let n = new_n v in (var_of_string n, (var_str v, n)) in
+    List.split (List.map new_vsub vars) in
+  match phi with
+    | Rel (rn, vs) -> Rel (rn, Array.map (fo_var_subst subst) vs)
+    | Eq (x, y) -> Eq (fo_var_subst subst x, fo_var_subst subst y)
+    | In (x, y) -> In (fo_var_subst subst x, to_mso (var_subst subst y))
+    | SO (v, vs) ->
+      SO (to_so (var_subst subst v), Array.map (fo_var_subst subst) vs)
+    | RealExpr (r, sgn) -> RealExpr (subst_vars_expr subst r, sgn)
+    | Not phi -> Not (subst_vars subst phi)
+    | Or flist -> Or (List.map (subst_vars subst) flist)
+    | And flist -> And (List.map (subst_vars subst) flist)
+    | Ex (vs, phi) -> 
+      let ((bad_vs, ok_vs), new_subst) = splitvs subst vs in
+      if new_subst = [] then Ex (vs, phi) else if bad_vs = [] then
+	  Ex (vs, subst_vars new_subst phi) 
+	else 
+	  let (new_bad, bad_subst) = newnames new_subst bad_vs in
+	  Ex (new_bad @ ok_vs, subst_vars (bad_subst @ new_subst) phi)
+    | All (vs, phi) ->
+      let ((bad_vs, ok_vs), new_subst) = splitvs subst vs in
+      if new_subst = [] then Ex (vs, phi) else if bad_vs = [] then
+	  All (vs, subst_vars new_subst phi) 
+	else 
+	  let (new_bad, bad_subst) = newnames new_subst bad_vs in
+	  All (new_bad @ ok_vs, subst_vars (bad_subst @ new_subst) phi)
+    | Lfp (v, vs, phi) ->
+      let ((bad_vs,ok_vs),new_subst) = 
+	splitvs subst ((v :> var) :: ((Array.to_list vs) :> var list)) in
+      if new_subst = [] then Lfp (v, vs, phi) else if bad_vs = [] then
+	  Lfp (v, vs, subst_vars new_subst phi) 
+	else
+	  let (_, bad_subst) = newnames new_subst bad_vs in
+	  let nvs = Array.map (fo_var_subst bad_subst) vs in
+	  Lfp (fp_var_subst bad_subst v, nvs,
+	       subst_vars (bad_subst @ new_subst) phi)
+    | Gfp (v, vs, phi) ->
+      let ((bad_vs,ok_vs),new_subst) = 
+	splitvs subst ((v :> var) :: ((Array.to_list vs) :> var list)) in
+      if new_subst = [] then Gfp (v, vs, phi) else if bad_vs = [] then
+	  Gfp (v, vs, subst_vars new_subst phi) 
+	else
+	  let (_, bad_subst) = newnames new_subst bad_vs in
+	  let nvs = Array.map (fo_var_subst bad_subst) vs in
+	  Gfp (fp_var_subst bad_subst v, nvs,
+	       subst_vars (bad_subst @ new_subst) phi)
 
 and subst_vars_expr subst = function
   | Const _ as x -> x
@@ -465,65 +522,19 @@
     if new_vs = [] then Sum(vs, phi, r) else 
       Sum(vs, subst_vars new_vs phi, subst_vars_expr new_vs 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, 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 (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. *)
-let rec rename_quant_avoiding avs = function
-  | Rel _ | Eq _ | In _ | RealExpr _ as x -> x
-  | Not phi -> Not (rename_quant_avoiding avs phi)
-  | Or flist -> Or (List.map (rename_quant_avoiding avs) flist)
-  | And flist -> And (List.map (rename_quant_avoiding avs) flist)
-  | Ex (vs, phi) -> 
-    let (avoidv, okv) = List.partition (fun v -> List.mem v avs) vs in
-    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, 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
-      let subst = List.map (subst_name_avoiding avs) avoidv in
-      let nvs = okv @ (List.map var_of_string (snd (List.split subst))) in
-      All (nvs, subst_vars subst (rename_quant_avoiding (avs @ nvs) 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
-let subst_vars subst phi = subst_vars_check 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 make_mso_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_check [(x, nx); (y, ny)] phi 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)])
@@ -537,18 +548,18 @@
       let (phi1, phi2) = 
 	(make_fo_tc_conj k1 x y phi, make_fo_tc_conj k2 x y phi) in
       let (phi1s, phi2s) = 
-	(subst_vars_check [(y,t)] phi1, subst_vars_check [(x,t)] phi2) in
+	(subst_vars [(y,t)] phi1, subst_vars [(x,t)] phi2) in
       Ex ([var_of_string t], And [phi1s; phi2s])
 
 (* First-order [k]-step refl. transitive closure of [phi], disjunctive form. *)
 let make_fo_tc_disj k x y phi =
   let (fv, xv, yv) = (free_vars phi, fo_var_of_string x, fo_var_of_string y) in
   let (_, t) = subst_name_avoiding fv (var_of_string "t") in
-  let phi_t = subst_vars_check [(y,t)] phi in
+  let phi_t = subst_vars [(y,t)] phi in
   let rec k_step i =
     if i = 0 then [Eq (xv, yv)] else if i = 1 then phi::[Eq (xv, yv)] else
 	let lst = k_step (i-1) in
-	let psi = subst_vars_check [(x,t)] (List.hd lst) in
+	let psi = subst_vars [(x,t)] (List.hd lst) in
 	Ex ([var_of_string t], And [phi_t; psi]) :: lst in
   Or (List.rev (k_step k))
 	
@@ -562,8 +573,6 @@
     try 
       let (dvs, dphi) = List.assoc rn defs in
       let ovs = List.map var_str (Array.to_list vs) in
-      (* not needed any more: let newdphi =
-           rename_quant_avoiding ((Array.to_list vs) :> var list) dphi in *)
       subst_vars (List.combine dvs ovs) dphi
     with Not_found -> Rel (rn, vs) )
   | x -> x
@@ -587,154 +596,124 @@
     else
       fp_n print (n-1) f nx
 
-(* Substitute recursively in [phi] relations defined in [defs] by their definitions. *)
+(* Substitute recursively in [phi] relations defined in [defs]. *)
 let subst_rels defs phi =
   fp_n str (List.length defs) (subst_once_rels defs) phi
 
-(* Substitute recursively in [r] relations defined in [defs] by their definitions. *)
+(* Substitute recursively in [r] relations defined in [defs]. *)
 let subst_rels_expr defs r =
   fp_n real_str (List.length defs) (subst_once_rels_expr defs) r
 
 
-(* ------------------------ CNF TO DNF USING SAT  --------------------------- *)
-
-(* Given a list of list of formulas interpreted as CNF, convert to DNF. *)
-(*let convert ll = 
-  let (ids, rev_ids, free_id) = (Hashtbl.create 7, Hashtbl.create 7, ref 1) in
-  let rec get_id ?(pos=true) = function
-      Not (phi) -> get_id ~pos:(not pos) phi 
-        (* TODO: we could check also: all x not R(x) = not ex x R(x)!*)
-    | phi ->
-        try 
-          let id = Hashtbl.find ids phi in if pos then id else -1 * id
-        with Not_found ->
-          if !debug_level_cnf > 2 then 
-            print_endline ("Added " ^ (str phi) ^ " as " ^ (string_of_int !free_id));
-          Hashtbl.add ids phi (!free_id);
-          Hashtbl.add rev_ids (!free_id) phi;
-          Hashtbl.add rev_ids (-1 * !free_id) (Not phi);
-          free_id := !free_id + 1;
-          if pos then !free_id - 1 else -1 * (!free_id - 1) in
-  let append_formula l i = 
-    try (* SAT DNF conversion might generate new literals. *)
-      (Hashtbl.find rev_ids i) :: l
-    with Not_found -> l in  (* It is safe to skip such literals. *)
-  let cnf = List.rev_map (fun l -> List.rev_map get_id l) ll in
-  let dnf = Sat.convert cnf in
-    List.rev_map (fun l -> List.fold_left append_formula [] l) dnf
-*)
-
-(* Given a CNF formula as list of lists, return negation as DNF (and dually). *)
-let negate_sort ll =
-  let neg_formula = function Not phi -> phi | phi -> Not phi in
-  let neg l = List.sort compare (List.rev_map neg_formula l) in
-    List.rev_map neg ll
-
-(* Given a list or lists, e.g. a disjunction of DNFs, flatten it to DNF. *)
-let rec tail_flatten ?(acc=[]) = function
-    [] -> acc
-  | ls :: rest -> tail_flatten ~acc:(List.rev_append ls acc) rest
-
-
 (* ------------------------------------------------------------------------- *)
 (* Prenex normal form.                                                       *)
 (* ------------------------------------------------------------------------- *)
 
 let mk_and phis = And phis and mk_or phis = Or phis
-and mk_forall (xs,phi) = All(xs,phi) and mk_exists (xs, phi) = Ex(xs,phi);;
+and mk_forall (xs,phi) = All(xs,phi) and mk_exists (xs, phi) = Ex(xs,phi)
 
 let rec variant x vars = 
-  if List.mem x vars then variant (var_of_string ((var_str x)^"_")) vars else x;;
+  if List.mem x vars then variant (var_of_string ((var_str x)^"_")) vars else x
 
-(* Determine if a list of formulas contains an Ex (x, ..) such that x does not occur elsewhere. *)
+(* Determine if a list of formulas contains an Ex (x, ..) such
+   that x does not occur elsewhere. *)
 let rec movable_ex acc_phis acc_vars = function
-    [] -> ([], None)
+  | [] -> ([], None)
   | (Ex (vs, f) as phi) :: phis ->
-      let othervs = List.rev_append acc_vars (all_vars (And phis)) in
-      let singvs = List.filter (fun v -> not (List.mem v othervs)) vs in
-      if singvs <> [] then 
-        (singvs, Some (vs, f, List.rev_append acc_phis phis))
-      else
-        movable_ex (phi::acc_phis) (List.rev_append (all_vars phi) acc_vars) phis
+    let othervs = List.rev_append acc_vars (all_vars (And phis)) in
+    let singvs = List.filter (fun v -> not (List.mem v othervs)) vs in
+    if singvs <> [] then 
+      (singvs, Some (vs, f, List.rev_append acc_phis phis))
+    else
+      movable_ex (phi::acc_phis) (List.rev_append (all_vars phi) acc_vars) phis
   | phi :: phis ->
-      movable_ex (phi::acc_phis) (List.rev_append (all_vars phi) acc_vars) phis
+    movable_ex (phi::acc_phis) (List.rev_append (all_vars phi) acc_vars) phis
 
-(* Determine if a list of formulas contains an All (x, ..) such that x does not occur elsewhere. *)
+(* Determine if a list of formulas contains an All (x, ..) such
+   that x does not occur elsewhere. *)
 let rec movable_all acc_phis acc_vars = function
-    [] -> ([], None)
+  | [] -> ([], None)
   | (All (vs, f) as phi) :: phis ->
-      let othervs = List.rev_append acc_vars (all_vars (Or phis)) in
-      let singvs = List.filter (fun v -> not (List.mem v othervs)) vs in
-      if singvs <> [] then 
-        (singvs, Some (vs, f, List.rev_append acc_phis phis))
-      else
-        movable_all (phi::acc_phis) (List.rev_append (all_vars phi) acc_vars) phis
+    let othervs = List.rev_append acc_vars (all_vars (Or phis)) in
+    let singvs = List.filter (fun v -> not (List.mem v othervs)) vs in
+    if singvs <> [] then 
+      (singvs, Some (vs, f, List.rev_append acc_phis phis))
+    else
+      movable_all (phi::acc_phis) (List.rev_append (all_vars phi) acc_vars) phis
   | phi :: phis ->
-      movable_all (phi::acc_phis) (List.rev_append (all_vars phi) acc_vars) phis
+    movable_all (phi::acc_phis) (List.rev_append (all_vars phi) acc_vars) phis
 
 let rec prenex = function
-    Rel _ | Eq _ | In _ | RealExpr _ as atom -> atom
+  | Rel _ | Eq _ | In _ | SO _ | RealExpr _ as atom -> atom
   | Not phi -> Not phi (* We assume NNF on input *)
   | And (flist) -> (
-      let pfl = List.rev_map prenex flist in
-      match movable_ex [] [] pfl with 
-          (svs, Some (vs, f, fl)) -> 
-            let dvs = List.filter (fun v -> not (List.mem v svs)) vs in
-            if dvs = [] then Ex (svs, prenex (And (f :: fl))) else
-              Ex (svs, prenex (And (Ex (dvs, f) :: fl)))
-        | _ ->
-	    let (alls, atoms) = List.partition (function All _ -> true | _ -> false) pfl in
-            if alls <> [] then
-	      let append_split_alls (vl, fl) = function 
-	          All (xs, f) -> (List.rev_append xs vl, f :: fl)
-                | _ -> failwith "" in
-	      let (allvs, phis) = List.fold_left append_split_alls ([], []) alls in
-              All (remove_dup_vars [] (List.sort compare_vars allvs),
-                   prenex (And (List.rev_append phis atoms)))
-            else
-              let (ex, noex) = List.partition (function Ex _ -> true | _ -> false) pfl in
-              if (ex = []) then And (pfl) else (
-                let vars = all_vars (And (List.rev_append (List.tl ex) noex)) in
-                let new_ex = match List.hd ex with
-                    Ex (vs, f) -> 
-                      let newvs = List.map (fun v -> variant v vars) vs in
-                      let subst = List.map2 (fun v w -> (var_str v, var_str w)) vs newvs in
-                      Ex (newvs, subst_vars subst f)
-                  | _ -> failwith "cex" in
-                prenex (And (new_ex :: (List.rev_append (List.tl ex) noex)))
-              )
-    )
+    let pfl = List.rev_map prenex flist in
+    match movable_ex [] [] pfl with 
+        (svs, Some (vs, f, fl)) -> 
+          let dvs = List.filter (fun v -> not (List.mem v svs)) vs in
+          if dvs = [] then Ex (svs, prenex (And (f :: fl))) else
+            Ex (svs, prenex (And (Ex (dvs, f) :: fl)))
+      | _ ->
+	let (alls, atoms) =
+	  List.partition (function All _ -> true | _ -> false) pfl in
+        if alls <> [] then
+	  let append_split_alls (vl, fl) = function 
+	    | All (xs, f) -> (List.rev_append xs vl, f :: fl)
+            | _ -> failwith "" in
+	  let (allvs, phis) = List.fold_left append_split_alls ([], []) alls in
+          All (remove_dup_vars [] (List.sort compare_vars allvs),
+               prenex (And (List.rev_append phis atoms)))
+        else
+          let (ex, noex) =
+	    List.partition (function Ex _ -> true | _ -> false) pfl in
+          if (ex = []) then And (pfl) else (
+            let vars = all_vars (And (List.rev_append (List.tl ex) noex)) in
+            let new_ex = match List.hd ex with
+              | Ex (vs, f) -> 
+                let newvs = List.map (fun v -> variant v vars) vs in
+                let subst = List.map2 
+		  (fun v w -> (var_str v, var_str w)) vs newvs in
+                Ex (newvs, subst_vars subst f)
+              | _ -> failwith "cex" in
+            prenex (And (new_ex :: (List.rev_append (List.tl ex) noex)))
+          )
+  )
   | Or (flist) -> (
-      let pfl = List.rev_map prenex flist in
-      match movable_all [] [] pfl with
-          (svs, Some (vs, f, fl)) -> 
-            let dvs = List.filter (fun v -> not (List.mem v svs)) vs in
-            if dvs = [] then All (svs, prenex (Or (f :: fl))) else
-              All (svs, prenex (Or (All (dvs, f) :: fl)))
-        | _ ->
-	    let (exs, atoms) = List.partition (function Ex _ -> true | _ -> false) pfl in
-            if exs <> [] then
-	      let append_split_exs (vl, fl) = function 
-	          Ex (xs, f) -> (List.rev_append xs vl, f :: fl)
-                | _ -> failwith "" in
-	      let (exvs, phis) = List.fold_left append_split_exs ([], []) exs in
-              Ex (remove_dup_vars [] (List.sort compare_vars exvs),
-                  prenex (Or (List.rev_append phis atoms)))
-            else
-              let (all, noall) = List.partition (function All _ -> true | _ -> false) pfl in
-              if (all = []) then Or (pfl) else (
-                let vars = all_vars (Or (List.rev_append (List.tl all) noall)) in
-                let new_all = match List.hd all with
-                    All (vs, f) -> 
-                      let newvs = List.map (fun v -> variant v vars) vs in
-                      let subst = List.map2 (fun v w -> (var_str v, var_str w)) vs newvs in
-                      All (newvs, subst_vars subst f)
-                  | _ -> failwith "call" in
-                prenex (Or (new_all :: (List.rev_append (List.tl all) noall)))
-              )
-    )
+    let pfl = List.rev_map prenex flist in
+    match movable_all [] [] pfl with
+        (svs, Some (vs, f, fl)) -> 
+          let dvs = List.filter (fun v -> not (List.mem v svs)) vs in
+          if dvs = [] then All (svs, prenex (Or (f :: fl))) else
+            All (svs, prenex (Or (All (dvs, f) :: fl)))
+      | _ ->
+	let (exs, atoms) =
+	  List.partition (function Ex _ -> true | _ -> false) pfl in
+        if exs <> [] then
+	  let append_split_exs (vl, fl) = function 
+	    | Ex (xs, f) -> (List.rev_append xs vl, f :: fl)
+            | _ -> failwith "" in
+	  let (exvs, phis) = List.fold_left append_split_exs ([], []) exs in
+          Ex (remove_dup_vars [] (List.sort compare_vars exvs),
+              prenex (Or (List.rev_append phis atoms)))
+        else
+          let (all, noall) =
+	    List.partition (function All _ -> true | _ -> false) pfl in
+          if (all = []) then Or (pfl) else (
+            let vars = all_vars (Or (List.rev_append (List.tl all) noall)) in
+            let new_all = match List.hd all with
+              | All (vs, f) -> 
+                let newvs = List.map (fun v -> variant v vars) vs in
+                let subst = List.map2 
+		  (fun v w -> (var_str v, var_str w)) vs newvs in
+                All (newvs, subst_vars subst f)
+              | _ -> failwith "call" in
+            prenex (Or (new_all :: (List.rev_append (List.tl all) noall)))
+          )
+  )
   | Ex (xs, phi) -> Ex (xs, prenex phi)
   | 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 pnf fm = prenex(nnf(fm))
 
@@ -766,7 +745,7 @@
 let univ_subs atom (univ_atom, _) =
   let usubs v uv = (v = uv) || (var_str uv = "u***") || (var_str uv = "U***") in
   match (atom, univ_atom) with
-      Rel (s, vl1), Rel (t, vl2) when s = t -> Aux.array_for_all2 usubs vl1 vl2
+    | Rel (s, vl1), Rel (t, vl2) when s = t -> Aux.array_for_all2 usubs vl1 vl2
     | Eq (v1, w1), Eq (v2, w2) -> usubs v1 v2 && usubs w1 w2
     | In (v1, w1), In (v2, w2) -> usubs v1 v2 && usubs w1 w2
     | _ -> false
@@ -775,43 +754,45 @@
 
 let concreter phi (conc_phi, _) =
   if phi = conc_phi then true else match (phi, conc_phi) with
-      (Or fl, Or cfl) -> List.for_all (fun f -> List.mem f fl) cfl
+    | (Or fl, Or cfl) -> List.for_all (fun f -> List.mem f fl) cfl
     | _ -> false
 
 (* Gather and propagate universally quantified atoms. *)
 let rec propagate_univ acc_atoms acc_formulas = function
   | phi when List.exists (concreter phi) acc_formulas -> 
       let (_, t) = List.find (concreter phi) acc_formulas in t
-  | Rel _ | Eq _ | In _ | RealExpr _ as atom -> (
-      try 
-        let (_, t) = List.find (univ_subs atom) acc_atoms in t
-      with Not_found -> atom
-    )
+  | Rel _ | Eq _ | In _ | SO _ | RealExpr _ as atom -> (
+    try 
+      let (_, t) = List.find (univ_subs atom) acc_atoms in t
+    with Not_found -> atom
+  )
   | Not phi -> Not (propagate_univ acc_atoms acc_formulas 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)
+  | Gfp (v, vs, phi) -> Gfp (v, vs, propagate_univ acc_atoms acc_formulas phi)
   | Or (fl) -> Or (List.map (propagate_univ acc_atoms acc_formulas) fl)
   | And fl ->
-      let pfl = List.rev_map (propagate_univ acc_atoms acc_formulas) fl in
-      let (alls, oth) = List.partition (function All _ -> true | _ -> false) pfl in
-      let (all_atoms, all_fs) = List.partition 
-        (function 
-             All (_, Not f) -> is_atom f 
-           | All (_, f) -> is_atom f 
-           | _ -> false ) alls in
-      let append_univ_atom al = function
-          All (vs, Not f) when is_atom f -> (sub_all vs f, Or []) :: al
-        | All (vs, f) when is_atom f -> (sub_all vs f, And []) :: al
-        | _ -> al in
-      let acc_a = List.fold_left append_univ_atom acc_atoms all_atoms in
-      let acc_fs = List.rev_append (List.map setall all_fs) acc_formulas in
-      let pother = List.rev_map (propagate_univ acc_a acc_fs) oth in
-      let (pallfs, _) = 
-        List.fold_left 
-          (fun (afs, acc_f) phi -> 
-             ((propagate_univ acc_a acc_f phi) :: afs, (setall phi) :: acc_f))
-          ([], acc_formulas) (List.sort Formula.compare all_fs) in
-      And (List.rev_append all_atoms (List.rev_append pallfs pother))
+    let pfl = List.rev_map (propagate_univ acc_atoms acc_formulas) fl in
+    let (alls, oth) = List.partition (function All _-> true | _-> false) pfl in
+    let (all_atoms, all_fs) = List.partition 
+      (function 
+	| All (_, Not f) -> is_atom f 
+        | All (_, f) -> is_atom f 
+        | _ -> false ) alls in
+    let append_univ_atom al = function
+      | All (vs, Not f) when is_atom f -> (sub_all vs f, Or []) :: al
+      | All (vs, f) when is_atom f -> (sub_all vs f, And []) :: al
+      | _ -> al in
+    let acc_a = List.fold_left append_univ_atom acc_atoms all_atoms in
+    let acc_fs = List.rev_append (List.map setall all_fs) acc_formulas in
+    let pother = List.rev_map (propagate_univ acc_a acc_fs) oth in
+    let (pallfs, _) = 
+      List.fold_left 
+        (fun (afs, acc_f) phi -> 
+          ((propagate_univ acc_a acc_f phi) :: afs, (setall phi) :: acc_f))
+        ([], acc_formulas) (List.sort Formula.compare all_fs) in
+    And (List.rev_append all_atoms (List.rev_append pallfs pother))
 
 let simp_prop_univ phi =
   flatten_sort (propagate_univ [] [] (flatten_sort phi))
@@ -820,47 +801,52 @@
 (* Recursively simplify a formula *)
 let rec simplify ?(do_pnf=false) ?(do_re=true) ?(ni=0) phi =
   let do_simplify phi = 
-    let (ids, rev_ids, free_id) = (Hashtbl.create 7, Hashtbl.create 7, ref 1) in    
-    let boolean_phi = BoolFormula.bool_formula_of_formula_arg phi (ids, rev_ids, free_id) in
+    let (ids, rev_ids, free_id) = (Hashtbl.create 7,Hashtbl.create 7,ref 1) in
+    let boolean_phi =
+      BoolFormula.bool_formula_of_formula_arg phi (ids, rev_ids, free_id) in
     let simplified = BoolFormula.simplify boolean_phi in
-    let simplified_phi = BoolFormula.formula_of_bool_formula_arg simplified (ids, rev_ids, free_id) in
-      (*print_endline("Simplified to: " ^ str simplified_phi);*)
-      simplified_phi in
+    let simplified_phi = BoolFormula.formula_of_bool_formula_arg simplified 
+      (ids, rev_ids, free_id) in simplified_phi in
   let rec simplify_subformulas = function
-      Rel _ | Eq _ | In _ as atom -> atom
+    | Rel _ | Eq _ | SO _ | In _ as atom -> atom
     | RealExpr (re, sgn) as rx -> 
       if do_re then 
 	RealExpr (simplify_re ~do_pnf ~do_formula:true ~ni re, sgn) 
       else rx
     | Not psi -> do_simplify (Not (simplify_subformulas psi))
-    | And (flist)  -> do_simplify (And (List.rev_map simplify_subformulas flist))
-    | Or  (flist)  -> do_simplify (Or  (List.rev_map simplify_subformulas flist))
+    | And (flist) -> do_simplify (And (List.rev_map simplify_subformulas flist))
+    | Or  (flist) -> do_simplify (Or  (List.rev_map simplify_subformulas flist))
     | Ex  (x, psi) -> Ex  (x, do_simplify (simplify_subformulas psi))
-    | All (x, psi) -> All (x, do_simplify (simplify_subformulas psi)) in
+    | 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
   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
+    List.exists (fun var -> var.[((String.length var)-1)]='_') vars in
   let rec qfree_size = function
-      All (xs, phi) 
+    | All (xs, phi) 
     | Ex (xs, phi) -> qfree_size phi
     | _ as phi -> Formula.size phi in
-  let prenex_phi = if do_pnf then pnf (simp_prop_univ phi) else simp_prop_univ phi in
+  let prenex_phi =
+    if do_pnf then pnf (simp_prop_univ phi) else simp_prop_univ phi in
   let prenex_size = qfree_size prenex_phi in
   let simplified_prenex_phi = simplify_subformulas prenex_phi in
   let simplified_size = qfree_size simplified_prenex_phi in
-    if (check_for_variants simplified_prenex_phi) then (
-      if !debug_level > 0 then (
-        print_endline("Attention! Variants detected!");
-        print_endline("Size: " ^ (string_of_int prenex_size) ^ " vs. " ^ (string_of_int simplified_size));
-        print_endline(str prenex_phi ^ " vs. " ^ str simplified_prenex_phi);
-      );
-      if (simplified_size >= prenex_size) then (
-        if !debug_level > 0 then print_endline ("Simplification of PNF not successful!");
-        simplify_subformulas phi
-      ) else
-        simplified_prenex_phi 
+  if (check_for_variants simplified_prenex_phi) then (
+    if !debug_level > 0 then (
+      print_endline("Attention! Variants detected!");
+      print_endline("Size: " ^ (string_of_int prenex_size) ^ 
+		       " vs. " ^ (string_of_int simplified_size));
+      print_endline(str prenex_phi ^ " vs. " ^ str simplified_prenex_phi);
+    );
+    if (simplified_size >= prenex_size) then (
+      if !debug_level > 0 then
+	print_endline ("Simplification of PNF not successful!");
+      simplify_subformulas phi
     ) else
-      simplified_prenex_phi        
+      simplified_prenex_phi 
+  ) else
+    simplified_prenex_phi        
   
 and simplify_re ?(do_pnf=false) ?(do_formula=true) ?(ni=0) = function
   | RVar _ | Const _ | Fun _ as atom -> atom
@@ -928,66 +914,39 @@
       simplify_re ~do_pnf ~do_formula ~ni (Times (simp_p, simp_q))
 
 
-(* Flatten "and"s and "or"s in a formula --
-   i.e. associativity. Remove double negation along the way. *)
-let flatten_formula =
-  let flat_and = function And conjs -> conjs | phi -> [phi] in
-  let flat_or = function Or disjs -> disjs | phi -> [phi] in
-  map_formula {identity_map with
-    map_And = (function
-      | [conj] -> conj
-      | conjs -> And (Aux.concat_map flat_and conjs));
-    map_Or = (function
-      | [disj] -> disj
-      | disjs -> Or (Aux.concat_map flat_or disjs));
-    map_Not = (function
-      | Or [] -> And []
-      | And [] -> Or []
-      | Not phi -> phi | phi -> Not phi)}
-
-let rec flatten_or = function
-  | Or disjs -> Aux.concat_map flatten_or disjs
-  | Not (Not phi) | Not (And [Not phi]) | Not (Or [Not phi]) ->
-    flatten_or phi
-  | phi -> [phi]
-
 (* Formula as a list of conjuncts, with one level of distributing
    negation over disjunction and pushing quantifiers inside. *)
-let rec flatten_ands = function
-  | And conjs -> Aux.concat_map flatten_ands conjs
-  | Or [phi] -> flatten_ands phi
-  | Not (And [phi]) -> flatten_ands (Not phi)
-  | Not (Or disjs) ->
-    Aux.concat_map flatten_ands
-      (List.map (fun d -> Not d)
-         (Aux.concat_map flatten_or disjs))
-  | All (vs, phi) ->
-    List.map (fun phi -> All (vs, phi)) (flatten_ands phi)
-  | Ex (vs, phi) as arg ->
-    (match flatten_ands phi with
-      | [] -> [] | [_] -> [arg]
-      | conjs ->
-        let free_conjs, bound_conjs = List.partition (fun conj ->
-          Aux.list_inter vs (free_vars conj) = []) conjs in
-        let bound_phi = match bound_conjs with
-          | [phi] -> phi | _ -> And bound_conjs in
-        free_conjs @ [Ex (vs, bound_phi)])
-  | Not (Not phi) -> flatten_ands phi
-  | phi -> [phi]
+let as_conjuncts phi =
+  let rec conjuncts = function
+    | And fl -> Aux.concat_map conjuncts fl
+    | All (vs, f) -> List.map (fun f -> All (vs, f)) (conjuncts f)
+    | Ex (vs, phi) ->
+      (match conjuncts phi with
+	| [] -> [] | [psi] -> [Ex (vs, psi)]
+	| conjs ->
+          let free_conjs, bound_conjs = List.partition (fun conj ->
+            Aux.list_inter vs (free_vars conj) = []) conjs in
+          let bound_phi = match bound_conjs with
+            | [phi] -> phi | _ -> And bound_conjs in
+          free_conjs @ [Ex (vs, bound_phi)])
+    | phi -> [phi] in
+  conjuncts (Formula.flatten_sort phi)
 
+
 (* Currently, does not go down real expressions. *)
 let remove_subformulas psub phi =
   let rec map_formula subf =
     if psub subf then raise Not_found;    
     match subf with
-      | Rel _ | Eq _ | RealExpr _ | In _ -> subf
+      | Rel _ | Eq _ | In _ | SO _ | RealExpr _ -> subf
       | Not phi -> Not (map_formula phi)
       | And conjs -> And (Aux.map_try map_formula conjs)
       | Or disjs -> Or (Aux.map_try map_formula disjs)
       | Ex (vs, phi) -> Ex (vs, map_formula phi)
-      | All (vs, phi) -> All (vs, map_formula phi) in
-  try flatten_formula (map_formula phi)
-  with Not_found -> And []
+      | 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
+  try Formula.flatten (map_formula phi) with Not_found -> And []
 
 let unused_quants_map = {identity_map with
   map_Ex = (fun vs phi ->
@@ -1007,7 +966,6 @@
    the removal till fixpoint since it can "unpack" literals e.g. from
    conjunctions to disjunctions. Also perform a very basic check for
    satisfiability of disjuncts.
-
    TODO: traverse the real part too. *)
 exception Unsatisfiable
 (* [Unsatisfiable] does not escape the function -- [Or []] is
@@ -1126,6 +1084,8 @@
     | Not phi -> Not (aux posbase negbase (not neg) phi)
     | Ex (vs, phi) -> Ex (vs, aux posbase negbase neg phi)
     | All (vs, phi) -> All (vs, aux posbase negbase neg phi)
+    | Lfp (v, vs, phi) -> Lfp (v, vs, aux posbase negbase neg phi)
+    | Gfp (v, vs, phi) -> Gfp (v, vs, aux posbase negbase neg phi)
     | phi -> phi in
 
   let rec fixpoint phi =
@@ -1135,51 +1095,44 @@
         (Formula.str phi)
     );
     (* }}} *)
-    let res = aux [] [] false (flatten_formula phi) in
+    let res = aux [] [] false (Formula.flatten phi) in
     if res = phi then res else fixpoint res in
   try fixpoint phi
   with Unsatisfiable -> Or []
 
 
-(* Compute size of a formula (currently w/o descending the real part). *)
-let rec size = function
-  | Or js | And js -> List.fold_left (+) 1 (List.map size js)
-  | All (_, phi) | Ex (_, phi) | Not phi -> size phi + 1
-  | Rel _ | Eq _ | In _ | RealExpr _ -> 1
-
 (* -------------------------- TYPE NORMAL FORM  ----------------------------- *)
 
 
 (* Check if [cl] is subsumed by [phi], i.e. if phi implies cl (partial). *)
 let partial_subsumes cl phi =
   if cl = phi then true else match cl with
-      Or fl -> if List.mem phi fl then true else false
+    | Or fl -> if List.mem phi fl then true else false
     | _ -> false
 
 (* Append to [acc] new clauses from [cl]. *)
 let rec append_clauses acc = function
-    [] -> acc
+  | [] -> acc
   | cl :: cls -> 
       if List.exists (partial_subsumes cl) acc then append_clauses acc cls else
         append_clauses (cl :: acc) cls
 
 (* Negate a boolean combination (do not go over quantifiers). *)
 let rec neg_boolean = function
-    And fl -> Or (List.rev_map neg_boolean fl)
+  | And fl -> Or (List.rev_map neg_boolean fl)
   | Or fl -> And (List.rev_map neg_boolean fl)
   | Not f -> f
   | f -> Not f
 
 (* Compute NNF but do not go over quantifiers. *)
-let rec bool_nnf ?(neg=false) psi =
-  match psi with
-      Not phi -> if neg then bool_nnf ~neg:false phi else bool_nnf ~neg:true phi
-    | And [f] | Or [f] -> bool_nnf ~neg f
-    | And (flist) when neg -> Or (List.rev_map (bool_nnf ~neg:true) flist)
-    | And (flist) -> And (List.rev_map (bool_nnf ~neg:false) flist)
-    | Or (flist) when neg -> And (List.rev_map (bool_nnf ~neg:true) flist)
-    | Or (flist) -> Or (List.rev_map (bool_nnf ~neg:false) flist)
-    | phi -> if neg then Not phi else phi
+let rec bool_nnf ?(neg=false) = function
+  | Not phi -> if neg then bool_nnf ~neg:false phi else bool_nnf ~neg:true phi
+  | And [f] | Or [f] -> bool_nnf ~neg f
+  | And (flist) when neg -> Or (List.rev_map (bool_nnf ~neg:true) flist)
+  | And (flist) -> And (List.rev_map (bool_nnf ~neg:false) flist)
+  | Or (flist) when neg -> And (List.rev_map (bool_nnf ~neg:true) flist)
+  | Or (flist) -> Or (List.rev_map (bool_nnf ~neg:false) flist)
+  | phi -> if neg then Not phi else phi
 
 
 (* Convert an arbitrary boolean combination to CNF. *)
@@ -1208,8 +1161,6 @@
 (* A bit hacky way to protect (by empty exists) parts of a boolean combination
    in which all atoms already contain one of the variables [vs] as free. *)
 let rec protect_full mlen vs = function
-    Rel _ | Eq _ | In _ | RealExpr _ | Ex _ | All _ as phi -> 
-      if has_free vs phi then Ex ([], phi) else phi
   | And fl when List.length fl < 2 || List.length fl > mlen -> 
       let pfl = List.rev_map (protect_full mlen vs) fl in
       if List.for_all (function Ex ([], _) -> true | _ -> false) pfl then
@@ -1227,7 +1178,9 @@
     )
   | And fl -> And (List.rev_map (protect_full mlen vs) fl)
   | Or fl -> Or (List.rev_map (protect_full mlen vs) fl)
+  | phi -> if has_free vs phi then Ex ([], phi) else phi
 
+
 (* Protect parts which do not contain any of the variables [vs] at all. *)
 let rec protect_empty mlen vs = function
     And fl when List.length fl > mlen ->
@@ -1280,7 +1233,7 @@
    in Ex (x, BC (tau's)) and All (x, BC (tau's))) it must hold that
    the free variables of *each* of the tau's contain x. *)
 let rec tnf_fun = function
-    Rel _ | Eq _ | In _ as phi -> phi
+  | Rel _ | Eq _ | In _ | SO _ as phi -> phi
   | RealExpr (re, sg) -> RealExpr (tnf_re_fun re, sg)
   | Not phi -> Not (tnf_fun phi)
   | Or flist -> Or (List.rev_map tnf_fun flist)
@@ -1288,38 +1241,42 @@
   | Ex ([], phi) -> failwith "empty existential when computing TNF"
   | Ex (xs, Or fl) -> Or (List.rev_map (fun f -> tnf_fun (Ex (xs, f))) fl)
   | Ex ([x], phi) ->
-      let protected_phi = protect [x] (tnf_fun phi) in
-      if !debug_level_tnf > 0 then (
-        print_endline ("TNF for (protected) "); print protected_phi; print_endline ("");
-      );
-      if !debug_level_tnf > 0 then print_endline ("TNF for var "^(var_str x));
-      let unand = function And fl -> fl | psi -> [psi] in
-      let conv_phi = List.rev_map unprotect (to_dnf protected_phi) in
-      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)
+    let protected_phi = protect [x] (tnf_fun phi) in
+    if !debug_level_tnf > 0 then (
+      print_endline "TNF for (protected) ";
+      print protected_phi; print_endline "";
+    );
+    if !debug_level_tnf > 0 then print_endline ("TNF for var "^(var_str x));
+    let unand = function And fl -> fl | psi -> [psi] in
+    let conv_phi = List.rev_map unprotect (to_dnf protected_phi) in
+    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 (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) ->
-      let protected_phi = protect [x] (tnf_fun phi) in
-      if !debug_level_tnf > 0 then (
-        print_endline ("TNF for (protected) "); print protected_phi; print_endline ("");
-      );
-      if !debug_level_tnf > 0 then print_endline ("TNF for var "^(var_str x));
-      let unor = function Or fl -> fl | psi -> [psi] in
-      let conv_phi = List.rev_map unprotect (to_cnf protected_phi) in
-      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)
+    let protected_phi = protect [x] (tnf_fun phi) in
+    if !debug_level_tnf > 0 then (
+      print_endline "TNF for (protected) ";
+      print protected_phi; print_endline "";
+    );
+    if !debug_level_tnf > 0 then print_endline ("TNF for var "^(var_str x));
+    let unor = function Or fl -> fl | psi -> [psi] in
+    let conv_phi = List.rev_map unprotect (to_cnf protected_phi) in
+    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 (vs, phi) -> 
     let (x, xs) = pick_var phi vs in
     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)
 
 and tnf_re_fun = function
-    RVar _ | Const _ | Fun _ as x -> x
+  | RVar _ | Const _ | Fun _ as x -> x
   | Times (re1, re2) -> Times (tnf_re_fun re1, tnf_re_fun re2)
   | Plus (re1, re2) -> Plus (tnf_re_fun re1, tnf_re_fun re2)
   | Char (phi) -> Char (flatten_sort (tnf_fun (flatten_sort phi)))
@@ -1331,7 +1288,7 @@
     | [x] -> x
     | lst -> if universal then Or lst else And lst in
   match have_v with
-      [] -> res no_v
+    | [] -> res no_v
     | [phi] -> 
         let psi = if universal then All (vs, phi) else Ex (vs, phi) in
         res (psi :: no_v)
@@ -1349,24 +1306,66 @@
   if !debug_level_tnf > 0 then print_endline ("TNF re of " ^ (real_str re));
   tnf_re_fun re
 
+(* ------------ TNF with variable pushing --------- *)
 
+(* Rename quantified variables avoiding the ones from [avs],
+    and the above-quantified ones. Does not go into real_expr. *)
+let rec rename_quant_avoiding avs = function
+  | Rel _ | Eq _ | In _ | SO _ | RealExpr _ as x -> x
+  | Not phi -> Not (rename_quant_avoiding avs phi)
+  | Or flist -> Or (List.map (rename_quant_avoiding avs) flist)
+  | And flist -> And (List.map (rename_quant_avoiding avs) flist)
+  | Ex (vs, phi) -> 
+    let (avoidv, okv) = List.partition (fun v -> List.mem v avs) vs in
+    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, 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
+      let subst = List.map (subst_name_avoiding avs) avoidv in
+      let nvs = okv @ (List.map var_of_string (snd (List.split subst))) in
+      All (nvs, subst_vars subst (rename_quant_avoiding (avs @ nvs) phi))
+  | Lfp (v, vs, phi) ->
+    let vars = (v :> var) :: ((Array.to_list vs) :> var list) in
+    let (avoidv, okv) = List.partition (fun v -> List.mem v avs) vars in
+    if avoidv=[] then Lfp (v, vs, rename_quant_avoiding (avs @ vars) phi) else
+      let subst = List.map (subst_name_avoiding avs) avoidv in
+      let nvs, nv = Array.map (fo_var_subst subst) vs, fp_var_subst subst v in
+      let nvars = (nv :> var) :: ((Array.to_list nvs) :> var list) in
+      Lfp (nv, nvs, rename_quant_avoiding (avs @ nvars) phi)
+  | Gfp (v, vs, phi) ->
+    let vars = (v :> var) :: ((Array.to_list vs) :> var list) in
+    let (avoidv, okv) = List.partition (fun v -> List.mem v avs) vars in
+    if avoidv=[] then Gfp (v, vs, rename_quant_avoiding (avs @ vars) phi) else
+      let subst = List.map (subst_name_avoiding avs) avoidv in
+      let nvs, nv = Array.map (fo_var_subst subst) vs, fp_var_subst subst v in
+      let nvars = (nv :> var) :: ((Array.to_list nvs) :> var list) in
+      Gfp (nv, nvs, rename_quant_avoiding (avs @ nvars) phi)
+
+
 let rec has_mso = function
   | In _ -> true
-  | Rel _ | Eq _ | RealExpr _ -> false
-  | Not phi | Ex (_, phi) | All (_, phi) -> has_mso phi
+  | Rel _ | Eq _ | RealExpr _ | SO _ -> false
+  | Not phi | Ex (_, phi) | All (_, phi) | Lfp (_,_, phi) | Gfp (_,_, phi) ->
+    has_mso phi
   | And flist | Or flist -> List.exists has_mso flist
 
 let rec has_fo = function
   | In _ -> false
-  | Rel _ | Eq _ | RealExpr _ -> true
-  | Not phi | Ex (_, phi) | All (_, phi) -> has_fo phi
+  | Rel _ | Eq _ | RealExpr _ | SO _ -> true
+  | Not phi | Ex (_, phi) | All (_, phi) | Lfp (_,_, phi) | Gfp (_,_, phi) ->
+    has_fo phi
   | And flist | Or flist -> List.exists has_fo flist
 
 let rec mso_last = function
-  | Rel _ | Eq _ | In _ | RealExpr _ as phi -> phi
+  | Rel _ | Eq _ | In _ | SO _ | RealExpr _ as phi -> phi
   | Not phi -> Not (mso_last phi)
   | Ex (vs, phi) -> Ex (vs, mso_last phi)
   | All (vs, phi) -> All (vs, mso_last phi)
+  | Lfp (v, vs, phi) -> Lfp (v, vs, mso_last phi)
+  | Gfp (v, vs, phi) -> Gfp (v, vs, mso_last phi)
   | And flist ->
     let (msos, fos) = List.partition has_mso (List.map mso_last flist) in
     let (somefo, nofo) = List.partition has_fo msos in
@@ -1426,7 +1425,7 @@
 
 let rec push_in_quant phi =
   match phi with
-    | In _ | Rel _ | Eq _ | RealExpr _ -> phi
+    | In _ | Rel _ | Eq _ | SO _ | RealExpr _ -> phi
     | Not (Or fl) -> push_in_quant (And (List.map (fun f -> Not f) fl))
     | Not (And fl) -> push_in_quant (Or (List.map (fun f -> Not f) fl))
     | Not f -> Not (push_in_quant f)
@@ -1445,6 +1444,8 @@
       push_in_quant (All ([List.hd vs], push_in_quant (All (List.tl vs,Or fl))))
     | Ex (vs, f) -> Ex (vs, push_in_quant f)
     | 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 rec push_quant f = push_in_quant (flatten_sort (f))
 

Modified: trunk/Toss/Formula/FormulaOps.mli
===================================================================
--- trunk/Toss/Formula/FormulaOps.mli	2011-05-01 16:34:53 UTC (rev 1428)
+++ trunk/Toss/Formula/FormulaOps.mli	2011-05-01 23:21:01 UTC (rev 1429)
@@ -118,20 +118,18 @@
 (** 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
 
-(** 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
-
 (** Substitute once relations in [defs] by corresponding subformulas
    (with instantiated parameters). *)
-val subst_once_rels : (string * (string list * formula)) list -> formula -> formula
-val subst_once_rels_expr : (string * (string list * formula)) list -> real_expr -> real_expr
+val subst_once_rels : 
+  (string * (string list * formula)) list -> formula -> formula
+val subst_once_rels_expr : 
+  (string * (string list * formula)) list -> real_expr -> real_expr
 
 (** Substitute recursively relations defined in [defs] by their definitions. *)
 val subst_rels : (string * (string list * formula)) list -> formula -> formula
-val subst_rels_expr : (string * (string list * formula)) list -> real_expr -> real_expr
+val subst_rels_expr : 
+  (string * (string list * formula)) list -> real_expr -> real_expr
 
 (** Assign emptyset to an MSO-variable. *)
 val assign_emptyset : string -> formula -> formula
@@ -140,7 +138,7 @@
 (** {2 Transitive Closure} *)
 
 (** Transitive closure of phi(x, y, z) over x and y, an MSO formula. *)
-val make_tc : string -> string -> formula -> formula
+val make_mso_tc : string -> string -> formula -> formula
 
 (** First-order [k]-step refl. transitive closure of [phi] over [x] and [y]. *)
 val make_fo_tc_conj : int -> string -> string -> formula -> formula
@@ -156,16 +154,12 @@
 val simplify_re : ?do_pnf: bool -> ?do_formula: bool -> ?ni:int ->
   real_expr -> real_expr
 
-
+(** Prenex normal form. *)
 val pnf : formula -> formula
 
-(** Flatten "and"s and "or"s in a formula --
-    i.e. associativity. Remove double negation along the way. *)
-val flatten_formula : formula -> formula
-
 (** Formula as a list of conjuncts, with one level of distributing
     negation over disjunction and pushing quantifiers inside. *)
-val flatten_ands : formula -> formula list
+val as_conjuncts : formula -> formula list
 
 (** "Erase" indicated subformulas from the formula. *)
 val remove_subformulas : (formula -> bool) -> formula -> formula
@@ -186,8 +180,6 @@
 val remove_redundant :
   ?implies:(formula -> formula -> bool) -> formula -> formula
 
-(** Compute size of a formula (currently w/o descending the real part). *)
-val size : formula -> int
 
 (** {2 TNF} *)
 

Modified: trunk/Toss/Formula/FormulaOpsTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaOpsTest.ml	2011-05-01 16:34:53 UTC (rev 1428)
+++ trunk/Toss/Formula/FormulaOpsTest.ml	2011-05-01 23:21:01 UTC (rev 1429)
@@ -135,17 +135,26 @@
 
    "subst free and all" >::
      (fun () ->
-       let subst phi = FormulaOps.subst_vars [("x", "a"); ("y", "b")] phi in
-       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
+       let subst s phi = FormulaOps.subst_vars s phi in
+       let subst_free_eq ?(sub=[("x", "a"); ("y", "b")]) phi1 phi2 =
+	 formula_eq id phi2 (subst sub) phi1 in
+       let subst_all_eq ?(sub=[("x", "a"); ("y", "b")]) phi1 phi2 =
+	 formula_eq id phi2 (FormulaOps.map_to_atoms (subst sub)) 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_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)";
+       subst_free_eq "R(x) and ex x R(x)" "R(a) and ex x R(x)";
+       subst_free_eq "R(x) and ex x (R(x) or R(a))" 
+	 "R(a) and ex x (R(x) or R(a))";
+       subst_free_eq ~sub:[("x", "m"); ("m", "x")]
+	 "R(m) and ex m (S(m) or T(x))" "R(x) and (ex m0 (S(m0) or T(m)))";
...
 
[truncated message content]