[Toss-devel-svn] SF.net SVN: toss:[1554] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1554] trunk/Toss
|
From: <luk...@us...> - 2011-08-31 23:11:19
|
Revision: 1554
http://toss.svn.sourceforge.net/toss/?rev=1554&view=rev
Author: lukaszkaiser
Date: 2011-08-31 23:11:10 +0000 (Wed, 31 Aug 2011)
Log Message:
-----------
Splitting FormulaOps - creating FormulaMap and FormulaSubst to handle let-in before other FormulaOps parts.
Modified Paths:
--------------
trunk/Toss/Arena/Arena.ml
trunk/Toss/Arena/ContinuousRule.ml
trunk/Toss/Arena/DiscreteRule.ml
trunk/Toss/Formula/FFTNF.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/TranslateFormula.ml
trunk/Toss/GGP/TranslateGame.ml
trunk/Toss/Play/Heuristic.ml
trunk/Toss/Server/Picture.ml
trunk/Toss/Server/Tests.ml
trunk/Toss/Solver/Class.ml
trunk/Toss/Solver/Solver.ml
Added Paths:
-----------
trunk/Toss/Formula/FormulaMap.ml
trunk/Toss/Formula/FormulaMap.mli
trunk/Toss/Formula/FormulaMapTest.ml
trunk/Toss/Formula/FormulaSubst.ml
trunk/Toss/Formula/FormulaSubst.mli
trunk/Toss/Formula/FormulaSubstTest.ml
Modified: trunk/Toss/Arena/Arena.ml
===================================================================
--- trunk/Toss/Arena/Arena.ml 2011-08-31 22:51:22 UTC (rev 1553)
+++ trunk/Toss/Arena/Arena.ml 2011-08-31 23:11:10 UTC (rev 1554)
@@ -263,7 +263,7 @@
List.map add_more old_locs in
let add_def_rel loc =
let sub_p l =
- { l with payoff = FormulaOps.subst_rels_expr def_rels_pure l.payoff } in
+ { l with payoff = FormulaSubst.subst_rels_expr def_rels_pure l.payoff } in
Array.map sub_p loc in
(* {{{ log entry *)
if !debug_level > 2 then (
@@ -279,7 +279,7 @@
(* }}} *)
let graph = Array.of_list (List.rev locations) in
(* TODO; FIXME; JUST THIS List.rev ABOVE WILL NOT ALWAYS BE GOOD, OR?!! *)
- let pats = List.rev_map (FormulaOps.subst_rels_expr def_rels_pure) patterns in
+ let pats=List.rev_map (FormulaSubst.subst_rels_expr def_rels_pure) patterns in
{
rules = rules;
patterns = pats;
@@ -417,7 +417,7 @@
rn, ContinuousRule.map_to_formulas f r
) game.rules;
graph = Array.map (fun la -> Array.map (fun loc ->
- {loc with payoff = FormulaOps.map_to_formulas_expr f loc.payoff;
+ {loc with payoff = FormulaMap.map_to_formulas_expr f loc.payoff;
}) la) game.graph;
defined_rels = List.map (fun (drel, (args, def)) ->
drel, (args, f def)) game.defined_rels;
@@ -430,7 +430,7 @@
) game.rules acc in
let acc =
Array.fold_right (fun la -> Array.fold_right
- (fun loc -> FormulaOps.fold_over_formulas_expr f loc.payoff) la)
+ (fun loc -> FormulaMap.fold_over_formulas_expr f loc.payoff) la)
game.graph acc in
let acc =
if include_defined_rels then
@@ -517,9 +517,9 @@
"At location %d, only the second game has label %s->%d"
i label.lb_rule dest));
let poff1 =
- FormulaOps.map_to_formulas_expr Formula.flatten loc1.payoff in
+ FormulaMap.map_to_formulas_expr Formula.flatten loc1.payoff in
let poff2 =
- FormulaOps.map_to_formulas_expr Formula.flatten loc2.payoff in
+ FormulaMap.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/ContinuousRule.ml
===================================================================
--- trunk/Toss/Arena/ContinuousRule.ml 2011-08-31 22:51:22 UTC (rev 1553)
+++ trunk/Toss/Arena/ContinuousRule.ml 2011-08-31 23:11:10 UTC (rev 1554)
@@ -24,9 +24,9 @@
let make_rule signat defs discr dynamics update ?(pre=Formula.And [])
?(inv=Formula.And []) ?(post=Formula.And []) () =
(* note that replacing not required for [pre]: [compile_rule] does it *)
- let cpre = FormulaOps.subst_rels defs pre in
- let cinv = FormulaOps.subst_rels defs inv in
- let cpost = FormulaOps.subst_rels defs post in
+ let cpre = FormulaSubst.subst_rels defs pre in
+ let cinv = FormulaSubst.subst_rels defs inv in
+ let cpost = FormulaSubst.subst_rels defs post in
let discrete = { discr with DiscreteRule.pre = cpre } in
(* we use [discrete] instead of [discr] because parser does not
insert precondition into discr! *)
Modified: trunk/Toss/Arena/DiscreteRule.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRule.ml 2011-08-31 22:51:22 UTC (rev 1553)
+++ trunk/Toss/Arena/DiscreteRule.ml 2011-08-31 23:11:10 UTC (rev 1554)
@@ -116,12 +116,12 @@
all added and deleted tuples be removed? *)
let fluent_preconds rules signature posi_frels nega_frels indef_frels =
let indef_vars_fold =
- {FormulaOps.make_fold Aux.unique_append [] with
- FormulaOps.fold_Rel = (fun rel args ->
+ {FormulaMap.make_fold Aux.unique_append [] with
+ FormulaMap.fold_Rel = (fun rel args ->
if Aux.Strings.mem rel indef_frels
then Array.to_list args else [])} in
let collect_indef_vars phi =
- FormulaOps.fold_formula indef_vars_fold phi in
+ FormulaMap.fold_formula indef_vars_fold phi in
let rem_closed indef_vars = function
| Formula.Eq (x, y) ->
List.mem x indef_vars || List.mem y indef_vars
@@ -130,7 +130,7 @@
Aux.Strings.mem rel indef_frels ||
( !prune_indef_vars &&
Aux.array_existsi (fun _ v -> List.mem v indef_vars) args)
- | phi -> FormulaOps.free_vars phi = [] in
+ | phi -> FormulaSubst.free_vars phi = [] in
let fluent_precond is_posi rel =
(* rules that produce a fluent, together with its args *)
let rel_prods =
@@ -168,13 +168,13 @@
(* }}} *)
(* remove potential condition for absence/presence of the
fluent being just added / deleted *)
- let body = FormulaOps.map_formula
- {FormulaOps.identity_map with
+ let body = FormulaMap.map_formula
+ {FormulaMap.identity_map with
(* remove the absence/presence condition of added/deleted
tuple (TODO: see header comment); we know by [rel \in
nega_frels/posi_frels] that the occurrence is
positive/negative *)
- FormulaOps.map_Rel = (fun b_rel b_args ->
+ FormulaMap.map_Rel = (fun b_rel b_args ->
let b = rel = b_rel && lhs_args =
Array.map Formula.var_str b_args in
if b && Aux.Strings.mem rel nega_frels then Formula.And []
@@ -202,7 +202,7 @@
| None -> (* LHS and RHS vars are the same *)
let numap = List.combine args nu_args in
(* TODO: (?) could capture if someone uses av__N in precond *)
- FormulaOps.subst_vars numap body,
+ FormulaSubst.subst_vars numap body,
List.filter
(fun v->not (List.mem v args)) r.lhs_elem_vars, []
| Some rlmap ->
@@ -814,7 +814,7 @@
let subst =
List.map (fun (re,le) ->
lhs_name_of le, rhs_name_of re) rule_src.rule_s in
- FormulaOps.subst_vars subst rule_src.pre
+ FormulaSubst.subst_vars subst rule_src.pre
else rule_src.pre in
(* now we are ready to forget LHS names if optimizing *)
let lhs_name_of =
@@ -920,14 +920,14 @@
| atom -> atom in
let defined_new_rels =
List.map (fun (drel, (args,body)) ->
- "_new_"^drel, (args, FormulaOps.map_to_atoms transform_new_rel body))
+ "_new_"^drel, (args, FormulaMap.map_to_atoms transform_new_rel body))
defined_rels in
let defined_del_rels =
List.map (fun (drel, (args,body)) ->
- "_del_"^drel, (args, FormulaOps.map_to_atoms transform_del_rel body))
+ "_del_"^drel, (args, FormulaMap.map_to_atoms transform_del_rel body))
defined_rels in
let defs = defined_rels @ defined_new_rels @ defined_del_rels in
- let emb = FormulaOps.subst_rels defs emb in
+ let emb = FormulaSubst.subst_rels defs emb in
(* RHS *)
let rhs_rels =
@@ -1076,7 +1076,7 @@
);
(* }}} *)
let precond = Formula.And conjs in
- let fvars = FormulaOps.free_vars precond in
+ let fvars = FormulaSubst.free_vars precond in
let local_vars =
List.filter (fun v->
not (List.mem (Formula.var_str v) struc_elems)) fvars in
Modified: trunk/Toss/Formula/FFTNF.ml
===================================================================
--- trunk/Toss/Formula/FFTNF.ml 2011-08-31 22:51:22 UTC (rev 1553)
+++ trunk/Toss/Formula/FFTNF.ml 2011-08-31 23:11:10 UTC (rev 1554)
@@ -204,22 +204,22 @@
| 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 = [] ->
+ | Ex (x, _) as phi when neg && FormulaSubst.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 = [] ->
+ | All (x, phi) as sbt when not neg && FormulaSubst.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 _ | SO _ | RealExpr _ | Lfp _ | Gfp _ as psi ->
- [], vars, FormulaOps.subst_vars sb psi
+ [], vars, FormulaSubst.subst_vars sb psi
| Not (Ex _) as phi -> [], vars, phi (* already processed recursively *)
| Not psi as phi -> (* already reduced to NNF *)
- [], vars, FormulaOps.subst_vars sb phi
+ [], vars, FormulaSubst.subst_vars sb phi
| And conjs ->
let (prefs, vars, conjs) =
List.fold_right (fun conj (prefs, vars, conjs) ->
@@ -559,16 +559,16 @@
prefix Top (p_pn_nnf ~do_pnf phi) in
let phi = Formula.flatten phi in
let protected lit qvs =
- let lit_vs = FormulaOps.all_vars lit in
+ let lit_vs = FormulaSubst.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 _ | 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)}
+ {fvs=vars_of_list (FormulaSubst.all_vars lit); t=TProc (0,lit)}
| (Rel _ | Eq _ | In _ | SO _ | RealExpr _ | Not _ | Lfp _ | Gfp _) as lit->
- {fvs=vars_of_list (FormulaOps.all_vars lit); t=TLit lit}
+ {fvs=vars_of_list (FormulaSubst.all_vars lit); t=TLit lit}
| And conjs ->
List.fold_right (fun conj -> function {fvs=vs; t=TAnd conjs} ->
let conj = to_tree last_qvs conj in
@@ -1099,7 +1099,7 @@
flatten formula, build the tree while pushing negation inside
(flatten if possible) if the subformula contains active atoms. *)
let ffsep_init posi_frels nega_frels phi =
- let fvs = FormulaOps.free_vars phi in
+ let fvs = FormulaSubst.free_vars phi in
let rec aux neg evs = function
| Ex (vs, phi) when not neg ->
aux neg (add_vars vs evs) phi
@@ -1125,13 +1125,13 @@
| 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);
+ {fvs=vars_of_list (FormulaSubst.free_vars phi);
t=TProc (0, if neg then Not phi else phi)}
else
match phi with
| Rel _ as atom ->
(* the atom is actually a literal, negative if [rel \in NF] *)
- {fvs=vars_of_list (FormulaOps.free_vars atom); t=TLit atom}
+ {fvs=vars_of_list (FormulaSubst.free_vars atom); t=TLit atom}
| Not phi -> build (not neg) phi
| Ex (vs, phi) ->
let ({fvs=fvs} as subt) = build neg phi in
@@ -1286,7 +1286,7 @@
| _ -> assert false in
let forest = loop [] [[], tree] in
(* step 6 *)
- let all_avs = FormulaOps.free_vars (And (concat_map fst forest)) in
+ let all_avs = FormulaSubst.free_vars (And (concat_map fst forest)) in
let all_avs = List.filter (fun v->not (List.mem v fvs)) all_avs in
(* does not descend alternations, only erases "real" [evs] *)
let rec erase_qs neg = function
@@ -1304,7 +1304,7 @@
| phi -> phi in
List.map (fun (atoms, tree) ->
let atoms = List.rev atoms in
- let avs = FormulaOps.free_vars (And atoms) in
+ let avs = FormulaSubst.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, Formula.flatten
Added: trunk/Toss/Formula/FormulaMap.ml
===================================================================
--- trunk/Toss/Formula/FormulaMap.ml (rev 0)
+++ trunk/Toss/Formula/FormulaMap.ml 2011-08-31 23:11:10 UTC (rev 1554)
@@ -0,0 +1,273 @@
+open Formula
+
+(* ----- Most basic literals / atoms map. --- *)
+
+(* Map [f] to all literals (i.e. atoms or not(atom)'s) in the given
+ formula. Preserves order of subformulas. *)
+let rec map_to_literals f g = function
+ | Rel _ | Eq _ | In _ | SO _ as x -> f x
+ | RealExpr (r, s) -> RealExpr (map_to_literals_expr f g r, s)
+ | Not (Rel _) | Not (Eq _) | Not (In _) as x -> f x
+ | Not (RealExpr (r, s)) -> Not (RealExpr (map_to_literals_expr f g r, s))
+ | Not phi -> Not (map_to_literals f g phi)
+ | Or flist -> Or (List.map (map_to_literals f g) flist)
+ | And flist -> And (List.map (map_to_literals f g) flist)
+ | Ex (vs, phi) -> Ex (vs, map_to_literals f g phi)
+ | All (vs, phi) -> All (vs, map_to_literals f g phi)
+ | Lfp (v, vs, phi) -> Lfp (v, vs, map_to_literals f g phi)
+ | Gfp (v, vs, phi) -> Gfp (v, vs, map_to_literals f g phi)
+
+and map_to_literals_expr f g = function
+ | RVar _ | Const _ | Fun _ as x -> g x
+ | Times (r1, r2) ->
+ Times (map_to_literals_expr f g r1, map_to_literals_expr f g r2)
+ | Plus (r1, r2) ->
+ Plus (map_to_literals_expr f g r1, map_to_literals_expr f g r2)
+ | Char (phi) -> Char (map_to_literals f g phi)
+ | Sum (vs, phi, r) ->
+ Sum (vs, map_to_literals f g phi, map_to_literals_expr f g r)
+
+(* Map [f] to all atoms in the given formula. *)
+let map_to_atoms_full f g phi =
+ map_to_literals (function Not (x) -> Not (f x) | x -> f x) g phi
+
+let map_to_atoms_full_re f g re =
+ map_to_literals_expr (function Not (x) -> Not (f x) | x -> f x) g re
+
+let map_to_atoms f phi =
+ map_to_literals (function Not (x) -> Not (f x) | x -> f x) (fun x -> x) phi
+
+let map_to_atoms_expr f r =
+ map_to_literals_expr (function Not (x) -> Not (f x) | x -> f x) (fun x -> x) r
+
+let get_atoms phi =
+ let atoms = ref [] in
+ let add_atom x = atoms := x :: !atoms; x in
+ ignore (map_to_atoms add_atom phi);
+ Aux.unique_sorted !atoms
+
+
+(* ---- Generalized maps --- *)
+
+(* Generalized map over formula and real expression types. *)
+type formula_and_expr_map = {
+ map_Rel : string -> fo_var array -> formula;
+ map_Eq : fo_var -> fo_var -> formula;
+ map_In : fo_var -> mso_var -> formula;
+ map_SO : so_var -> fo_var array -> formula;
+ map_RealExpr : real_expr -> sign_op -> formula;
+ map_Not : formula -> formula;
+ map_And : formula list -> formula;
+ map_Or : formula list -> formula;
+ map_Ex : var list -> formula -> formula;
+ map_All : var list -> formula -> formula;
+ map_Lfp : [ mso_var | so_var ] -> fo_var array -> formula -> formula;
+ map_Gfp : [ mso_var | so_var ] -> fo_var array -> formula -> formula;
+
+ map_RVar : string -> real_expr;
+ map_Const : float -> real_expr;
+ map_Times : real_expr -> real_expr -> real_expr;
+ map_Plus : real_expr -> real_expr -> real_expr;
+ map_Fun : string -> fo_var -> real_expr;
+ map_Char : formula -> real_expr;
+ map_Sum : fo_var list -> formula -> real_expr -> real_expr
+}
+
+let identity_map = {
+ map_Rel = (fun rel args -> Rel (rel, args));
+ map_Eq = (fun x y -> Eq (x, y));
+ map_In = (fun x ys -> In (x, ys));
+ map_SO = (fun v vs -> SO (v, vs));
+ map_RealExpr = (fun expr sign -> RealExpr (expr, sign));
+ map_Not = (fun phi -> Not phi);
+ map_And = (fun conjs -> And conjs);
+ map_Or = (fun disjs -> Or disjs);
+ map_Ex = (fun vs phi -> Ex (vs, phi));
+ map_All = (fun vs phi -> All (vs, phi));
+ map_Lfp = (fun v vs phi -> Lfp (v, vs, phi));
+ map_Gfp = (fun v vs phi -> Gfp (v, vs, phi));
+
+ map_RVar = (fun v -> RVar v);
+ map_Const = (fun c -> Const c);
+ map_Times = (fun expr1 expr2 -> Times (expr1, expr2));
+ map_Plus = (fun expr1 expr2 -> Plus (expr1, expr2));
+ map_Fun = (fun f v -> Fun (f, v));
+ map_Char = (fun phi -> Char phi);
+ map_Sum = (fun vs guard expr -> Sum (vs, guard, expr))
+}
+
+let rec map_formula gmap = function
+ | Rel (rel, args) -> gmap.map_Rel rel args
+ | Eq (x, y) -> gmap.map_Eq x y
+ | In (x, ys) -> gmap.map_In x ys
+ | SO (v, vs) -> gmap.map_SO v vs
+ | RealExpr (expr, sign) ->
+ gmap.map_RealExpr (map_real_expr gmap expr) sign
+ | Not phi -> gmap.map_Not (map_formula gmap phi)
+ | And conjs -> gmap.map_And (List.map (map_formula gmap) conjs)
+ | Or disjs -> gmap.map_Or (List.map (map_formula gmap) disjs)
+ | Ex (vs, phi) -> gmap.map_Ex vs (map_formula gmap phi)
+ | All (vs, phi) -> gmap.map_All vs (map_formula gmap phi)
+ | Lfp (v, vs, phi) -> gmap.map_Lfp v vs (map_formula gmap phi)
+ | Gfp (v, vs, phi) -> gmap.map_Gfp v vs (map_formula gmap phi)
+
+and map_real_expr gmap = function
+ | RVar v -> gmap.map_RVar v
+ | Const c -> gmap.map_Const c
+ | Times (expr1, expr2) ->
+ gmap.map_Times (map_real_expr gmap expr1) (map_real_expr gmap expr2)
+ | Plus (expr1, expr2) ->
+ gmap.map_Plus (map_real_expr gmap expr1) (map_real_expr gmap expr2)
+ | Fun (f, v) -> gmap.map_Fun f v
+ | Char phi -> gmap.map_Char (map_formula gmap phi)
+ | Sum (vs, guard, expr) ->
+ gmap.map_Sum vs (map_formula gmap guard) (map_real_expr gmap expr)
+
+
+(* Generalized fold over formula and real expression types. *)
+type 'a formula_and_expr_fold = {
+ fold_Rel : string -> fo_var array -> 'a;
+ fold_Eq : fo_var -> fo_var -> 'a;
+ fold_In : fo_var -> mso_var -> 'a;
+ fold_SO : so_var -> fo_var array -> 'a;
+ fold_RealExpr : 'a -> sign_op -> 'a;
+ fold_Not : 'a -> 'a;
+ fold_And : 'a -> 'a -> 'a;
+ fold_Or : 'a -> 'a -> 'a;
+ fold_Ex : var list -> 'a -> 'a;
+ fold_All : var list -> 'a -> 'a;
+ fold_Lfp : [ mso_var | so_var ] -> fo_var array -> 'a -> 'a;
+ fold_Gfp : [ mso_var | so_var ] -> fo_var array -> 'a -> 'a;
+
+ fold_RVar : string -> 'a;
+ fold_Const : float -> 'a;
+ fold_Times : 'a -> 'a -> 'a;
+ fold_Plus : 'a -> 'a -> 'a;
+ fold_Fun : string -> fo_var -> 'a;
+ fold_Char : 'a -> 'a;
+ fold_Sum : fo_var list -> 'a -> 'a -> 'a
+}
+
+let make_fold union empty = {
+ fold_Rel = (fun _ _ -> empty);
+ fold_Eq = (fun _ _ -> empty);
+ fold_In = (fun _ _ -> empty);
+ fold_SO = (fun _ _ -> empty);
+ fold_RealExpr = (fun expr _ -> expr);
+ fold_Not = (fun phi -> phi);
+ fold_And = union;
+ fold_Or = union;
+ fold_Ex = (fun _ phi -> phi);
+ fold_All = (fun _ phi -> phi);
+ fold_Lfp = (fun _ _ phi -> phi);
+ fold_Gfp = (fun _ _ phi -> phi);
+
+ fold_RVar = (fun _ -> empty);
+ fold_Const = (fun _ -> empty);
+ fold_Times = union;
+ fold_Plus = union;
+ fold_Fun = (fun _ _ -> empty);
+ fold_Char = (fun phi -> phi);
+ fold_Sum = (fun _ guard expr -> union guard expr)
+}
+
+open Aux.BasicOperators
+
+let rec fold_formula gfold = function
+ | Rel (rel, args) -> gfold.fold_Rel rel args
+ | Eq (x, y) -> gfold.fold_Eq x y
+ | In (x, ys) -> gfold.fold_In x ys
+ | SO (v, vs) -> gfold.fold_SO v vs
+ | RealExpr (expr, sign) ->
+ gfold.fold_RealExpr (fold_real_expr gfold expr) sign
+ | Not phi -> gfold.fold_Not (fold_formula gfold phi)
+ | And [] ->
+ gfold.fold_RealExpr (fold_real_expr gfold (Const 1.)) GZero
+ | And [conj] -> fold_formula gfold conj
+ | And (conj::conjs) ->
+ List.fold_right (gfold.fold_And -| fold_formula gfold) conjs
+ (fold_formula gfold conj)
+ | Or [] ->
+ gfold.fold_RealExpr (fold_real_expr gfold (Const 1.)) LZero
+ | Or [disj] -> fold_formula gfold disj
+ | Or (disj::disjs) ->
+ List.fold_right (gfold.fold_Or -| fold_formula gfold) disjs
+ (fold_formula gfold disj)
+ | Ex (vs, phi) -> gfold.fold_Ex vs (fold_formula gfold phi)
+ | All (vs, phi) -> gfold.fold_All vs (fold_formula gfold phi)
+ | Lfp (v, vs, phi) -> gfold.fold_Lfp v vs (fold_formula gfold phi)
+ | Gfp (v, vs, phi) -> gfold.fold_Gfp v vs (fold_formula gfold phi)
+
+and fold_real_expr gfold = function
+ | RVar v -> gfold.fold_RVar v
+ | Const c -> gfold.fold_Const c
+ | Times (expr1, expr2) ->
+ gfold.fold_Times (fold_real_expr gfold expr1) (fold_real_expr gfold expr2)
+ | Plus (expr1, expr2) ->
+ gfold.fold_Plus (fold_real_expr gfold expr1) (fold_real_expr gfold expr2)
+ | Fun (f, v) -> gfold.fold_Fun f v
+ | Char phi -> gfold.fold_Char (fold_formula gfold phi)
+ | Sum (vs, guard, expr) ->
+ gfold.fold_Sum vs (fold_formula gfold guard) (fold_real_expr gfold expr)
+
+(* Map [f] to top-level formulas in the real expression ([Char]s and
+ [Sum] guards). *)
+let rec map_to_formulas_expr f = function
+ | RVar _ | Const _ | Fun _ as x -> x
+ | Times (r1, r2) ->
+ Times (map_to_formulas_expr f r1, map_to_formulas_expr f r2)
+ | Plus (r1, r2) ->
+ Plus (map_to_formulas_expr f r1, map_to_formulas_expr f r2)
+ | Char (phi) -> Char (f phi)
+ | Sum (vs, phi, r) ->
+ Sum (vs, f phi, map_to_formulas_expr f r)
+
+let rec fold_over_formulas_expr f r acc =
+ match r with
+ | RVar _ | Const _ | Fun _ -> acc
+ | Times (r1, r2)
+ | Plus (r1, r2) ->
+ fold_over_formulas_expr f r1 (fold_over_formulas_expr f r2 acc)
+ | Char (phi) -> f phi acc
+ | Sum (vs, phi, r) ->
+ fold_over_formulas_expr f r (f phi acc)
+
+let rec fold_over_literals f phi acc =
+ match phi with
+ | Rel _ | Eq _ | In _ | SO _ as x -> f x acc
+ | RealExpr (r, _) -> fold_over_literals_expr f r acc
+ | Not (Rel _) | Not (Eq _) | Not (In _) as x -> f x acc
+ | Not phi -> fold_over_literals f phi acc
+ | Or flist
+ | And flist -> List.fold_right (fold_over_literals f) flist acc
+ | Ex (_, phi) | All (_, phi) -> fold_over_literals f phi acc
+ | Lfp (_, _, phi) | Gfp (_, _, phi) -> fold_over_literals f phi acc
+
+and fold_over_literals_expr f =
+ fold_over_formulas_expr (fold_over_literals f)
+
+let fold_over_atoms f phi =
+ fold_over_literals
+ (function Not x -> f x | x -> f x) phi
+
+(* Map [f] to all variables occurring in the formula. Preserves order
+ of subformulas. *)
+let rec map_to_all_vars (f : var -> var) phi =
+ let foaf va = Array.map (fun x -> to_fo (f (x :> var))) va in
+ match phi with
+ | Rel (rn, vl) -> Rel (rn, foaf vl)
+ | Eq (x, y) -> Eq (to_fo (f (x :> var)), to_fo (f (y :> var)))
+ | In (x, y) -> In (to_fo (f (x :> var)), to_mso (f (y :> var)))
+ | SO (v, vs) -> SO (to_so (f (v :> var)), foaf vs)
+ | RealExpr _ -> failwith "re"(* TODO: implement var map for realexprs. *)
+ | Not phi -> Not (map_to_all_vars f phi)
+ | Or flist -> Or (List.map (map_to_all_vars f) flist)
+ | And flist -> And (List.map (map_to_all_vars f) flist)
+ | Ex (vs, phi) -> Ex (List.map f vs, map_to_all_vars f phi)
+ | All (vs, phi) -> All (List.map f vs, map_to_all_vars f phi)
+ | Lfp (v, vs, phi) ->
+ Lfp (to_mso_or_so (f (v :> var)), foaf vs, map_to_all_vars f phi)
+ | Gfp (v, vs, phi) ->
+ Gfp (to_mso_or_so (f (v :> var)), foaf vs, map_to_all_vars f phi)
+
+
Added: trunk/Toss/Formula/FormulaMap.mli
===================================================================
--- trunk/Toss/Formula/FormulaMap.mli (rev 0)
+++ trunk/Toss/Formula/FormulaMap.mli 2011-08-31 23:11:10 UTC (rev 1554)
@@ -0,0 +1,99 @@
+open Formula
+
+(** {2 Basic maps - to literals and atoms.} *)
+
+val get_atoms : formula -> formula list
+
+(** Map [f] to all literals (i.e. atoms or not(atom)'s) in the given
+ formula. Preserves order of subformulas. *)
+val map_to_literals : (formula -> formula) -> (real_expr -> real_expr) ->
+ formula -> formula
+val map_to_literals_expr : (formula -> formula) -> (real_expr -> real_expr) ->
+ real_expr -> real_expr
+
+(** Map [f] to all atoms in the given formula. *)
+val map_to_atoms_full : (formula -> formula) -> (real_expr -> real_expr) ->
+ formula -> formula
+val map_to_atoms_full_re : (formula -> formula) -> (real_expr -> real_expr) ->
+ real_expr -> real_expr
+val map_to_atoms : (formula -> formula) -> formula -> formula
+val map_to_atoms_expr : (formula -> formula) -> real_expr -> real_expr
+
+(** {2 Generalized maps} *)
+
+(** Generalized map over formula and real expression types. *)
+type formula_and_expr_map = {
+ map_Rel : string -> fo_var array -> formula;
+ map_Eq : fo_var -> fo_var -> formula;
+ map_In : fo_var -> mso_var -> formula;
+ map_SO : so_var -> fo_var array -> formula;
+ map_RealExpr : real_expr -> sign_op -> formula;
+ map_Not : formula -> formula;
+ map_And : formula list -> formula;
+ map_Or : formula list -> formula;
+ map_Ex : var list -> formula -> formula;
+ map_All : var list -> formula -> formula;
+ map_Lfp : [ mso_var | so_var ] -> fo_var array -> formula -> formula;
+ map_Gfp : [ mso_var | so_var ] -> fo_var array -> formula -> formula;
+
+ map_RVar : string -> real_expr;
+ map_Const : float -> real_expr;
+ map_Times : real_expr -> real_expr -> real_expr;
+ map_Plus : real_expr -> real_expr -> real_expr;
+ map_Fun : string -> fo_var -> real_expr;
+ map_Char : formula -> real_expr;
+ map_Sum : fo_var list -> formula -> real_expr -> real_expr
+}
+
+(** Identity map to be refined using the [with] syntax. *)
+val identity_map : formula_and_expr_map
+
+(** Map through the structure adjusting subformulas/subexpressions. *)
+val map_formula : formula_and_expr_map -> formula -> formula
+val map_real_expr : formula_and_expr_map -> real_expr -> real_expr
+
+(** Generalized fold over formula and real expression types. *)
+type 'a formula_and_expr_fold = {
+ fold_Rel : string -> fo_var array -> 'a;
+ fold_Eq : fo_var -> fo_var -> 'a;
+ fold_In : fo_var -> mso_var -> 'a;
+ fold_SO : so_var -> fo_var array -> 'a;
+ fold_RealExpr : 'a -> sign_op -> 'a;
+ fold_Not : 'a -> 'a;
+ fold_And : 'a -> 'a -> 'a;
+ fold_Or : 'a -> 'a -> 'a;
+ fold_Ex : var list -> 'a -> 'a;
+ fold_All : var list -> 'a -> 'a;
+ fold_Lfp : [ mso_var | so_var ] -> fo_var array -> 'a -> 'a;
+ fold_Gfp : [ mso_var | so_var ] -> fo_var array -> 'a -> 'a;
+
+ fold_RVar : string -> 'a;
+ fold_Const : float -> 'a;
+ fold_Times : 'a -> 'a -> 'a;
+ fold_Plus : 'a -> 'a -> 'a;
+ fold_Fun : string -> fo_var -> 'a;
+ fold_Char : 'a -> 'a;
+ fold_Sum : fo_var list -> 'a -> 'a -> 'a
+}
+
+val make_fold : ('a -> 'a -> 'a) -> 'a -> 'a formula_and_expr_fold
+
+(** Fold the structure using the operations. (Not tail-recursive.) *)
+val fold_formula : 'a formula_and_expr_fold -> formula -> 'a
+val fold_real_expr : 'a formula_and_expr_fold -> real_expr -> 'a
+
+(** Map [f] to top-level formulas in the real expression ([Char]s and
+ [Sum] guards). *)
+val map_to_formulas_expr : (formula -> formula) -> real_expr -> real_expr
+
+val fold_over_formulas_expr :
+ (formula -> 'a -> 'a) -> real_expr -> 'a -> 'a
+
+val fold_over_literals :
+ (formula -> 'a -> 'a) -> formula -> 'a -> 'a
+val fold_over_atoms :
+ (formula -> 'a -> 'a) -> formula -> 'a -> 'a
+
+(** Map @param f to all variables occurring in the formula.
+ Preserves order of subformulas. @param phi The formula to substitute in. *)
+val map_to_all_vars : (var -> var) -> formula -> formula
Added: trunk/Toss/Formula/FormulaMapTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaMapTest.ml (rev 0)
+++ trunk/Toss/Formula/FormulaMapTest.ml 2011-08-31 23:11:10 UTC (rev 1554)
@@ -0,0 +1,45 @@
+open OUnit
+open Formula
+
+FormulaOps.set_debug_level 0
+
+let formula_of_string s =
+ FormulaParser.parse_formula Lexer.lex (Lexing.from_string s)
+
+let real_expr_of_string s =
+ FormulaParser.parse_real_expr Lexer.lex (Lexing.from_string s)
+
+
+let formula_eq ?(flatten=true) f1 phi1 f2 phi2 =
+ if flatten then
+ assert_equal ~printer:(fun x -> Formula.sprint x)
+ (Formula.flatten (f1 (formula_of_string phi1)))
+ (Formula.flatten (f2 (formula_of_string phi2)))
+ else
+ assert_equal ~printer:(fun x -> Formula.sprint x)
+ (f1 (formula_of_string phi1)) (f2 (formula_of_string phi2))
+
+let id x = x
+
+let tests = "FormulaMap" >::: [
+ "subst all" >::
+ (fun () ->
+ let var_subst subst v =
+ let subst_str s = try List.assoc s subst with Not_found -> s in
+ match v with
+ | `FO s -> `FO (subst_str s)
+ | `MSO s -> `MSO (subst_str s)
+ | `SO s -> `SO (subst_str s)
+ | `Real s -> `Real (subst_str s) in
+ let fo_var_subst subst (v : fo_var) = to_fo (var_subst subst v) in
+ let subst_atom subst = function
+ | Rel (rn, vs) -> Rel (rn, Array.map (fo_var_subst subst) vs)
+ | _ -> failwith "not atom" in
+ let subst_all_eq ?(sub=[("x", "a"); ("y", "b")]) phi1 phi2 =
+ formula_eq id phi2 (FormulaMap.map_to_atoms (subst_atom sub)) phi1 in
+ subst_all_eq "ex x (P(x) and (not R(x, y)))"
+ "ex x (P(a) and (not R(a, b)))";
+ );
+]
+
+let exec = Aux.run_test_if_target "FormulaMapTest" tests
Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml 2011-08-31 22:51:22 UTC (rev 1553)
+++ trunk/Toss/Formula/FormulaOps.ml 2011-08-31 23:11:10 UTC (rev 1554)
@@ -1,6 +1,8 @@
(* Operations on formulas.*)
open Formula
+open FormulaMap
+open FormulaSubst
let debug_level = ref 0
let debug_level_cnf = ref 0
@@ -14,6 +16,7 @@
(* Sat.set_debug_level (i-1);*)
Sat.set_debug_level ((i land 48) lsr 4);
(debug_level := i);
+ (FormulaSubst.set_debug_level i);
(debug_level_cnf := (i land 3));
(debug_level_tnf := (i land 12) lsr 2)
(* print_endline ("Debug level (CNF): " ^ string_of_int !debug_level_cnf);
@@ -50,8 +53,9 @@
| Let (r, args, body, phi) -> (* subst_rels [(rel, (args, body))] phi *)
Let (r, args, nnf body, nnf phi)
-(* -------------------------- FREE VARIABLES -------------------------------- *)
+(* -- Delete quantified variables. --- *)
+
(* Helper function: remove duplicates from sorted list of variables. *)
let rec remove_dup_vars acc = function
[] -> acc
@@ -60,71 +64,6 @@
match compare_vars v1 v2 with
0 -> remove_dup_vars acc (v2::vs)
| _ -> remove_dup_vars (v1::acc) (v2::vs)
-
-let rec all_vars_acc acc = function
- | Eq (x, y) -> (x :> var) :: (y :> var) :: acc
- | Rel (r, vs) -> List.rev_append ((Array.to_list vs) :> var list) acc
- | In (x, y) -> (x :> var) :: (y :> var) :: acc
- | SO (v, vs) ->
- (v :> var) :: List.rev_append ((Array.to_list vs) :> var list) acc
- | RealExpr (p, _) ->
- List.rev_append (List.map(fun v -> var_of_string v) (all_vars_real p)) acc
- | Not phi -> all_vars_acc acc phi
- | And (flist) | Or (flist) ->
- List.fold_left (fun vs phi -> all_vars_acc vs phi) acc flist
- | Ex (vs, phi) | All (vs, phi) ->
- all_vars_acc (List.rev_append (vs :> var list) acc) phi
- | Lfp (r, vs, phi) | Gfp (r, vs, phi) ->
- all_vars_acc
- ((r :> var):: (List.rev_append ((Array.to_list vs) :> var list) acc)) phi
-
-and all_vars_real = function
- | RVar s -> [s]
- | Const _ -> []
- | Times (r1, r2) -> List.rev_append (all_vars_real r1) (all_vars_real r2)
- | Plus (r1, r2) -> List.rev_append (all_vars_real r1) (all_vars_real r2)
- | Fun (s, v) -> [var_str v]
- | 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)
-
-let all_vars phi =
- remove_dup_vars [] (List.sort compare_vars (all_vars_acc [] phi))
-
-let rec free_vars_acc acc = function
- | Eq (x, y) -> (x :> var) :: (y :> var) :: acc
- | Rel (r, vs) -> List.rev_append (Array.to_list vs :> var list) acc
- | In (x, y) -> (x :> var) :: (y :> var) :: acc
- | SO (v, vs) ->
- (v :> var) :: List.rev_append ((Array.to_list vs) :> var list) acc
- | RealExpr (p, _) ->
- List.rev_append (List.map (fun v->var_of_string v) (free_vars_real p)) acc
- | Not phi -> free_vars_acc acc phi
- | And (flist) | Or (flist) ->
- List.fold_left (fun vs phi -> free_vars_acc vs phi) acc flist
- | Ex (vs, phi) | All (vs, phi) ->
- let fv_phi = free_vars_acc [] phi in
- List.rev_append (List.filter (fun v -> not (List.mem v vs)) fv_phi) acc
- | Lfp (r, xs, phi) | Gfp (r, xs, phi) ->
- let vs = (r :> var) :: ((Array.to_list xs) :> var list) in
- 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)
-
-and free_vars_real = function
- | RVar s -> [s]
- | Const _ -> []
- | Times (r1, r2) -> List.rev_append (all_vars_real r1) (all_vars_real r2)
- | Plus (r1, r2) -> List.rev_append (all_vars_real r1) (all_vars_real r2)
- | Fun (s, v) -> [var_str v]
- | Char phi -> List.rev_map var_str (free_vars_acc [] phi)
- | Sum (vl, _, r) ->
- let vs = List.map var_str vl in
- List.filter (fun w -> not (List.mem w vs)) (free_vars_real r)
-
-let free_vars phi =
- remove_dup_vars [] (List.sort compare_vars (free_vars_acc [] phi))
-
(* Delete all quantification over [vs] in the formula. *)
let rec del_vars_quant vs = function
| Eq _ | Rel _ | In _ | SO _ | RealExpr _ as f -> f
@@ -144,173 +83,8 @@
| Gfp (r, xs, phi) -> Gfp (r, xs, del_vars_quant vs phi)
-(* ----------------- MAPPING TO ATOMS AND VAR SUBSTITUTION ------------------ *)
+(* --- Signs of rels --- *)
-let is_atom = function
- | Rel _ | Eq _ | In _ -> true
- | _ -> false
-
-(* Generalized map over formula and real expression types. *)
-type formula_and_expr_map = {
- map_Rel : string -> fo_var array -> formula;
- map_Eq : fo_var -> fo_var -> formula;
- map_In : fo_var -> mso_var -> formula;
- map_SO : so_var -> fo_var array -> formula;
- map_RealExpr : real_expr -> sign_op -> formula;
- map_Not : formula -> formula;
- map_And : formula list -> formula;
- map_Or : formula list -> formula;
- map_Ex : var list -> formula -> formula;
- map_All : var list -> formula -> formula;
- map_Lfp : [ mso_var | so_var ] -> fo_var array -> formula -> formula;
- map_Gfp : [ mso_var | so_var ] -> fo_var array -> formula -> formula;
-
- map_RVar : string -> real_expr;
- map_Const : float -> real_expr;
- map_Times : real_expr -> real_expr -> real_expr;
- map_Plus : real_expr -> real_expr -> real_expr;
- map_Fun : string -> fo_var -> real_expr;
- map_Char : formula -> real_expr;
- map_Sum : fo_var list -> formula -> real_expr -> real_expr
-}
-
-let identity_map = {
- map_Rel = (fun rel args -> Rel (rel, args));
- map_Eq = (fun x y -> Eq (x, y));
- map_In = (fun x ys -> In (x, ys));
- map_SO = (fun v vs -> SO (v, vs));
- map_RealExpr = (fun expr sign -> RealExpr (expr, sign));
- map_Not = (fun phi -> Not phi);
- map_And = (fun conjs -> And conjs);
- map_Or = (fun disjs -> Or disjs);
- map_Ex = (fun vs phi -> Ex (vs, phi));
- map_All = (fun vs phi -> All (vs, phi));
- map_Lfp = (fun v vs phi -> Lfp (v, vs, phi));
- map_Gfp = (fun v vs phi -> Gfp (v, vs, phi));
-
- map_RVar = (fun v -> RVar v);
- map_Const = (fun c -> Const c);
- map_Times = (fun expr1 expr2 -> Times (expr1, expr2));
- map_Plus = (fun expr1 expr2 -> Plus (expr1, expr2));
- map_Fun = (fun f v -> Fun (f, v));
- map_Char = (fun phi -> Char phi);
- map_Sum = (fun vs guard expr -> Sum (vs, guard, expr))
-}
-
-let rec map_formula gmap = function
- | Rel (rel, args) -> gmap.map_Rel rel args
- | Eq (x, y) -> gmap.map_Eq x y
- | In (x, ys) -> gmap.map_In x ys
- | SO (v, vs) -> gmap.map_SO v vs
- | RealExpr (expr, sign) ->
- gmap.map_RealExpr (map_real_expr gmap expr) sign
- | Not phi -> gmap.map_Not (map_formula gmap phi)
- | And conjs -> gmap.map_And (List.map (map_formula gmap) conjs)
- | Or disjs -> gmap.map_Or (List.map (map_formula gmap) disjs)
- | Ex (vs, phi) -> gmap.map_Ex vs (map_formula gmap phi)
- | All (vs, phi) -> gmap.map_All vs (map_formula gmap phi)
- | Lfp (v, vs, phi) -> gmap.map_Lfp v vs (map_formula gmap phi)
- | Gfp (v, vs, phi) -> gmap.map_Gfp v vs (map_formula gmap phi)
-
-and map_real_expr gmap = function
- | RVar v -> gmap.map_RVar v
- | Const c -> gmap.map_Const c
- | Times (expr1, expr2) ->
- gmap.map_Times (map_real_expr gmap expr1) (map_real_expr gmap expr2)
- | Plus (expr1, expr2) ->
- gmap.map_Plus (map_real_expr gmap expr1) (map_real_expr gmap expr2)
- | Fun (f, v) -> gmap.map_Fun f v
- | Char phi -> gmap.map_Char (map_formula gmap phi)
- | Sum (vs, guard, expr) ->
- gmap.map_Sum vs (map_formula gmap guard) (map_real_expr gmap expr)
-
-
-(* Generalized fold over formula and real expression types. *)
-type 'a formula_and_expr_fold = {
- fold_Rel : string -> fo_var array -> 'a;
- fold_Eq : fo_var -> fo_var -> 'a;
- fold_In : fo_var -> mso_var -> 'a;
- fold_SO : so_var -> fo_var array -> 'a;
- fold_RealExpr : 'a -> sign_op -> 'a;
- fold_Not : 'a -> 'a;
- fold_And : 'a -> 'a -> 'a;
- fold_Or : 'a -> 'a -> 'a;
- fold_Ex : var list -> 'a -> 'a;
- fold_All : var list -> 'a -> 'a;
- fold_Lfp : [ mso_var | so_var ] -> fo_var array -> 'a -> 'a;
- fold_Gfp : [ mso_var | so_var ] -> fo_var array -> 'a -> 'a;
-
- fold_RVar : string -> 'a;
- fold_Const : float -> 'a;
- fold_Times : 'a -> 'a -> 'a;
- fold_Plus : 'a -> 'a -> 'a;
- fold_Fun : string -> fo_var -> 'a;
- fold_Char : 'a -> 'a;
- fold_Sum : fo_var list -> 'a -> 'a -> 'a
-}
-
-let make_fold union empty = {
- fold_Rel = (fun _ _ -> empty);
- fold_Eq = (fun _ _ -> empty);
- fold_In = (fun _ _ -> empty);
- fold_SO = (fun _ _ -> empty);
- fold_RealExpr = (fun expr _ -> expr);
- fold_Not = (fun phi -> phi);
- fold_And = union;
- fold_Or = union;
- fold_Ex = (fun _ phi -> phi);
- fold_All = (fun _ phi -> phi);
- fold_Lfp = (fun _ _ phi -> phi);
- fold_Gfp = (fun _ _ phi -> phi);
-
- fold_RVar = (fun _ -> empty);
- fold_Const = (fun _ -> empty);
- fold_Times = union;
- fold_Plus = union;
- fold_Fun = (fun _ _ -> empty);
- fold_Char = (fun phi -> phi);
- fold_Sum = (fun _ guard expr -> union guard expr)
-}
-
-open Aux.BasicOperators
-
-let rec fold_formula gfold = function
- | Rel (rel, args) -> gfold.fold_Rel rel args
- | Eq (x, y) -> gfold.fold_Eq x y
- | In (x, ys) -> gfold.fold_In x ys
- | SO (v, vs) -> gfold.fold_SO v vs
- | RealExpr (expr, sign) ->
- gfold.fold_RealExpr (fold_real_expr gfold expr) sign
- | Not phi -> gfold.fold_Not (fold_formula gfold phi)
- | And [] ->
- gfold.fold_RealExpr (fold_real_expr gfold (Const 1.)) GZero
- | And [conj] -> fold_formula gfold conj
- | And (conj::conjs) ->
- List.fold_right (gfold.fold_And -| fold_formula gfold) conjs
- (fold_formula gfold conj)
- | Or [] ->
- gfold.fold_RealExpr (fold_real_expr gfold (Const 1.)) LZero
- | Or [disj] -> fold_formula gfold disj
- | Or (disj::disjs) ->
- List.fold_right (gfold.fold_Or -| fold_formula gfold) disjs
- (fold_formula gfold disj)
- | Ex (vs, phi) -> gfold.fold_Ex vs (fold_formula gfold phi)
- | All (vs, phi) -> gfold.fold_All vs (fold_formula gfold phi)
- | Lfp (v, vs, phi) -> gfold.fold_Lfp v vs (fold_formula gfold phi)
- | Gfp (v, vs, phi) -> gfold.fold_Gfp v vs (fold_formula gfold phi)
-
-and fold_real_expr gfold = function
- | RVar v -> gfold.fold_RVar v
- | Const c -> gfold.fold_Const c
- | Times (expr1, expr2) ->
- gfold.fold_Times (fold_real_expr gfold expr1) (fold_real_expr gfold expr2)
- | Plus (expr1, expr2) ->
- gfold.fold_Plus (fold_real_expr gfold expr1) (fold_real_expr gfold expr2)
- | Fun (f, v) -> gfold.fold_Fun f v
- | Char phi -> gfold.fold_Char (fold_formula gfold phi)
- | Sum (vs, guard, expr) ->
- gfold.fold_Sum vs (fold_formula gfold guard) (fold_real_expr gfold expr)
-
let rels_signs_fold =
{make_fold
(fun (posi1,nega1) (posi2,nega2) ->
@@ -324,367 +98,7 @@
let rels_signs = fold_formula rels_signs_fold
let rels_signs_expr = fold_real_expr rels_signs_fold
-(* Map [f] to all literals (i.e. atoms or not(atom)'s) in the given
- formula. Preserves order of subformulas. *)
-let rec map_to_literals f g = function
- | Rel _ | Eq _ | In _ | SO _ as x -> f x
- | RealExpr (r, s) -> RealExpr (map_to_literals_expr f g r, s)
- | Not (Rel _) | Not (Eq _) | Not (In _) as x -> f x
- | Not (RealExpr (r, s)) -> Not (RealExpr (map_to_literals_expr f g r, s))
- | Not phi -> Not (map_to_literals f g phi)
- | Or flist -> Or (List.map (map_to_literals f g) flist)
- | And flist -> And (List.map (map_to_literals f g) flist)
- | Ex (vs, phi) -> Ex (vs, map_to_literals f g phi)
- | All (vs, phi) -> All (vs, map_to_literals f g phi)
- | Lfp (v, vs, phi) -> Lfp (v, vs, map_to_literals f g phi)
- | Gfp (v, vs, phi) -> Gfp (v, vs, map_to_literals f g phi)
-and map_to_literals_expr f g = function
- | RVar _ | Const _ | Fun _ as x -> g x
- | Times (r1, r2) ->
- Times (map_to_literals_expr f g r1, map_to_literals_expr f g r2)
- | Plus (r1, r2) ->
- Plus (map_to_literals_expr f g r1, map_to_literals_expr f g r2)
- | Char (phi) -> Char (map_to_literals f g phi)
- | Sum (vs, phi, r) ->
- Sum (vs, map_to_literals f g phi, map_to_literals_expr f g r)
-
-(* Map [f] to top-level formulas in the real expression ([Char]s and
- [Sum] guards). *)
-let rec map_to_formulas_expr f = function
- | RVar _ | Const _ | Fun _ as x -> x
- | Times (r1, r2) ->
- Times (map_to_formulas_expr f r1, map_to_formulas_expr f r2)
- | Plus (r1, r2) ->
- Plus (map_to_formulas_expr f r1, map_to_formulas_expr f r2)
- | Char (phi) -> Char (f phi)
- | Sum (vs, phi, r) ->
- Sum (vs, f phi, map_to_formulas_expr f r)
-
-let rec fold_over_formulas_expr f r acc =
- match r with
- | RVar _ | Const _ | Fun _ -> acc
- | Times (r1, r2)
- | Plus (r1, r2) ->
- fold_over_formulas_expr f r1 (fold_over_formulas_expr f r2 acc)
- | Char (phi) -> f phi acc
- | Sum (vs, phi, r) ->
- fold_over_formulas_expr f r (f phi acc)
-
-
-(* Map [f] to all atoms in the given formula. *)
-let map_to_atoms_full f g phi =
- map_to_literals (function Not (x) -> Not (f x) | x -> f x) g phi
-
-let map_to_atoms_full_re f g re =
- map_to_literals_expr (function Not (x) -> Not (f x) | x -> f x) g re
-
-let map_to_atoms f phi =
- map_to_literals (function Not (x) -> Not (f x) | x -> f x) (fun x -> x) phi
-
-let map_to_atoms_expr f r =
- map_to_literals_expr (function Not (x) -> Not (f x) | x -> f x) (fun x -> x) r
-
-let get_atoms phi =
- let atoms = ref [] in
- let add_atom x = atoms := x :: !atoms; x in
- ignore (map_to_atoms add_atom phi);
- Aux.unique_sorted !atoms
-
-
-let rec fold_over_literals f phi acc =
- match phi with
- | Rel _ | Eq _ | In _ | SO _ as x -> f x acc
- | RealExpr (r, _) -> fold_over_literals_expr f r acc
- | Not (Rel _) | Not (Eq _) | Not (In _) as x -> f x acc
- | Not phi -> fold_over_literals f phi acc
- | Or flist
- | And flist -> List.fold_right (fold_over_literals f) flist acc
- | Ex (_, phi) | All (_, phi) -> fold_over_literals f phi acc
- | Lfp (_, _, phi) | Gfp (_, _, phi) -> fold_over_literals f phi acc
-
-and fold_over_literals_expr f =
- fold_over_formulas_expr (fold_over_literals f)
-
-let fold_over_atoms f phi =
- fold_over_literals
- (function Not x -> f x | x -> f x) phi
-
-(* Map [f] to all variables occurring in the formula. Preserves order
- of subformulas. *)
-let rec map_to_all_vars (f : var -> var) phi =
- let foaf va = Array.map (fun x -> to_fo (f (x :> var))) va in
- match phi with
- | Rel (rn, vl) -> Rel (rn, foaf vl)
- | Eq (x, y) -> Eq (to_fo (f (x :> var)), to_fo (f (y :> var)))
- | In (x, y) -> In (to_fo (f (x :> var)), to_mso (f (y :> var)))
- | SO (v, vs) -> SO (to_so (f (v :> var)), foaf vs)
- | RealExpr _ -> failwith "re"(* TODO: implement var map for realexprs. *)
- | Not phi -> Not (map_to_all_vars f phi)
- | Or flist -> Or (List.map (map_to_all_vars f) flist)
- | And flist -> And (List.map (map_to_all_vars f) flist)
- | Ex (vs, phi) -> Ex (List.map f vs, map_to_all_vars f phi)
- | All (vs, phi) -> All (List.map f vs, map_to_all_vars f phi)
- | Lfp (v, vs, phi) ->
- Lfp (to_mso_or_so (f (v :> var)), foaf vs, map_to_all_vars f phi)
- | Gfp (v, vs, phi) ->
- Gfp (to_mso_or_so (f (v :> var)), foaf vs, map_to_all_vars f phi)
-
-(* Helper function: apply subsutitution [subst] to the variable [v]. *)
-let var_subst subst v =
- let subst_str s = try List.assoc s subst with Not_found -> s in
- match v with
- | `FO s -> `FO (subst_str s)
- | `MSO s -> `MSO (subst_str s)
- | `SO s -> `SO (subst_str s)
- | `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 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 subvs = Array.map (fo_var_subst subst) vs in
- let ((bad_vs,ok_vs),new_subst) = splitvs subst [(v :> var)] in
- if new_subst = [] then Lfp (v, subvs, phi) else if bad_vs = [] then
- Lfp (v, subvs, subst_vars new_subst phi)
- else
- let (_, bad_subst) = newnames new_subst bad_vs in
- Lfp (fp_var_subst bad_subst v, subvs,
- subst_vars (bad_subst @ new_subst) phi)
- | Gfp (v, vs, phi) ->
- let subvs = Array.map (fo_var_subst subst) vs in
- let ((bad_vs,ok_vs),new_subst) = splitvs subst [(v :> var)] in
- if new_subst = [] then Gfp (v, subvs, phi) else if bad_vs = [] then
- Gfp (v, subvs, subst_vars new_subst phi)
- else
- let (_, bad_subst) = newnames new_subst bad_vs in
- Gfp (fp_var_subst bad_subst v, subvs,
- subst_vars (bad_subst @ new_subst) phi)
-
-and subst_vars_expr subst = function
- | Const _ as x -> x
- | Fun (s, v) -> Fun (s, fo_var_subst subst v)
- | RVar s -> RVar (try List.assoc s subst with Not_found -> s)
- | Times (r1, r2) -> Times (subst_vars_expr subst r1,subst_vars_expr subst r2)
- | Plus (r1, r2) -> Plus (subst_vars_expr subst r1, subst_vars_expr subst r2)
- | Char (phi) -> Char (subst_vars subst phi)
- | Sum (vs, phi, r) ->
- 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 Sum(vs, phi, r) else
- Sum(vs, subst_vars new_vs phi, subst_vars_expr new_vs r)
-
-
-(* --------------------------- TRANSITIVE CLOSURE --------------------------- *)
-
-(* We construct the lfp transitive closure of phi(x, y, z) over x, y as
- "x = y or lfp T(y) = (phi(x, y, z) or ex n (n in T and phi (n, y, z)))" *)
-let make_lfp_tc x y phi =
- let (fv, xv, yv) = (free_vars phi, fo_var_of_string x, fo_var_of_string y) in
- let (_, nn) = subst_name_avoiding fv (fo_var_of_string "n") in
- let nnv = fo_var_of_string nn in
- let frT = mso_var_of_string(snd(subst_name_avoiding fv(var_of_string "T"))) in
- let nphi = subst_vars [(x, nn)] phi in
- let fpphi = Or [phi; Ex([(nnv :> var)], And [In (nnv, frT); nphi])] in
- Or [Eq (xv, yv); Lfp ((frT :> [ mso_var | so_var ]), [|yv|], fpphi)]
-
-(* We construct the mso 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_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 [(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_conj 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_conj k1 x y phi, make_fo_tc_conj k2 x y phi) in
- let (phi1s, phi2s) =
- (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 [(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 [(x,t)] (List.hd lst) in
- Ex ([var_of_string t], And [phi_t; psi]) :: lst in
- Or (List.rev (k_step k))
-
-
-
-(* --------- SUBSTITUTE DEFINED RELATIONS ------------ *)
-
-(* Substitute in relations defined in [defs] by their definitions. *)
-let subst_r defs = function (* Helper function for atoms. *)
- | Rel (rn, vs) -> (
- try
- let (_, dvs, dphi) = List.assoc rn defs in
- let ovs = List.map var_str (Array.to_list vs) in
- subst_vars (List.combine dvs ovs) dphi
- with Not_found -> Rel (rn, vs) )
- | x -> x
-
-(* Substitute once in [phi] relations in [defs] by corresponding
- subformulas (with instantiated parameters). *)
-let subst_once_rels defs phi =
- let cdefs = List.map (fun (n, (v, f)) -> (n, ([], v, f))) defs in
- map_to_atoms (subst_r cdefs) phi
-
-(* Substitute once in [r] relations defined in [defs] by their definitions. *)
-let subst_once_rels_expr defs r =
- let cdefs = List.map (fun (n, (v, f)) -> (n, ([], v, f))) defs in
- map_to_atoms_expr (subst_r cdefs) r
-
-
-(* Substitute recursively in [phi] relations defined in [defs]. *)
-let subst_rels defs phi =
- let rels f =
- Aux.map_some (function Rel (r, _) -> Some r | _ -> None) (get_atoms f) in
- let rels_def defs f = List.filter (fun r -> List.mem_assoc r defs) (rels f) in
- let cdefs = List.map (fun (n, (vs,f)) -> (n, (rels_def defs f, vs,f))) defs in
- let cdfstr (n, (rs, _, _)) =
- Printf.sprintf "rel %s calls %s" n
- (if (List.length rs) = 0 then "nothing" else
- let rstr = String.concat ", " rs in
- if List.mem n rs then "self, " ^ rstr else rstr) in
- if !debug_level > 1 then
- Printf.printf "Subst:\n %s\n" (String.concat "\n " (List.map cdfstr cdefs));
- let is_basic (_, (rs, _, _)) = List.length rs = 0 in
- let self_calls (n, (rs, _, _)) = List.mem n rs in
- let subst_once_fm defs phi = map_to_atoms (subst_r defs) phi in
- let subst_once rdefs defs (n, (rs, v, f)) =
- let nf = subst_once_fm defs f in
- (n, (rels_def rdefs nf, v, nf)) in
- let subst_once_defs defs lst = List.map (subst_once lst defs) lst in
- let rec rec_subst_rels cdefs phi =
- if cdefs = [] then phi else
- let (basic, other) = List.partition is_basic cdefs in
- if basic <> [] then
- rec_subst_rels (subst_once_defs basic other) (subst_once_fm basic phi)
- else
- let cdefss = List.sort Pervasives.compare cdefs in (* repeatability *)
- let (selfc, otherc) = List.partition self_calls cdefss in
- if otherc <> [] then
- let (d, ds) = (List.hd otherc, (List.tl otherc) @ selfc) in
- rec_subst_rels (subst_once_defs [d] ds) (subst_once_fm [d] phi)
- else
- (* Here we must replace a simultaneous least fixed-point with
- single ones. In the future we should probably add simultaneous
- fixed-points to our logic. For now we use the Bekic principle, cf
- "Finite Model Theory and Descriptive Complexity", Lemma 3.3.41,
- at www.logic.rwth-aachen.de/pub/graedel/FMTbook-Chapter3.pdf *)
- let sovar vs n =
- let m = if Array.length vs = 1 then n else "|" ^ n in
- mso_or_so_var_of_string m in
- let sorels rels = function
- | Rel (m, rvs) when List.mem m rels ->
- let mv = (sovar rvs m :> var) in
- if Array.length rvs = 1 then In (rvs.(0), to_mso mv) else
- SO (to_so mv, rvs)
- | x -> x in
- let do_lfp (n, (calls, vs, f)) =
- let va = Array.of_list (List.map fo_var_of_string vs) in
- let nf = map_to_atoms (sorels [n]) f in
- (n, ([], vs, Lfp (sovar va n, va, nf))) in
- let (d, ds) = do_lfp (List.hd selfc), List.tl selfc in
- rec_subst_rels (subst_once_defs [d] ds) (subst_once_fm [d] phi) in
- let res_phi = rec_subst_rels cdefs phi in
- if syntax_ok res_phi then
- let simpfpvars = (* TODO: is it ok to simplify all these? name clashes? *)
- List.concat (List.map (fun (n, _) -> [n; "|" ^ n]) cdefs) in
- let rec simp_def_lfp acc fpvar fpvs fpdef =
- if List.mem fpvar acc && List.mem (var_str fpvar) simpfpvars then
- match mso_or_so_var_of_string (var_str fpvar) with
- | `MSO v -> In (fpvs.(0), `MSO v)
- | `SO v -> SO (`SO v, fpvs)
- else
- let smap = { identity_map with map_Lfp = simp_def_lfp (fpvar::acc) } in
- Lfp (fpvar, fpvs, map_formula smap fpdef) in
- map_formula { identity_map with map_Lfp = simp_def_lfp []} res_phi
- else failwith ("subst_defs: non-stratified recursion?\n" ^ (str res_phi))
-
-
-(* Substitute recursively in [r] relations defined in [defs]. *)
-let rec subst_rels_expr defs = function
- | RVar _ | Const _ | Fun _ as x -> x
- | Times (r1, r2) -> Times (subst_rels_expr defs r1, subst_rels_expr defs r2)
- | 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)
-
-
(* --- AType with variables over given relations, no repetition, equality --- *)
let atp rels vars_in =
@@ -1445,6 +859,8 @@
(* ------------ TNF with variable pushing --------- *)
+let fp_var_subst s (v : [ mso_var | so_var ]) = to_mso_or_so (var_subst s 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
@@ -1595,11 +1011,3 @@
let tnf_lfp fprel fpvs fpdef = Lfp (fprel, fpvs, tnf_fv_nofp ?sizes fpdef) in
let psi = map_formula { identity_map with map_Lfp = tnf_lfp } phi in
tnf_fv_nofp ?sizes psi
-
-
-(* Assign emptyset to the MSO-variable v by replacing "x in X" with "false". *)
-let assign_emptyset v phi =
- let replace_by_emptyset v = function
- In (fo_v, `MSO w) when w = v -> Or []
- | phi -> phi in
- flatten (map_to_atoms (replace_by_emptyset v) phi)
Modified: trunk/Toss/Formula/FormulaOps.mli
===================================================================
--- trunk/Toss/Formula/FormulaOps.mli 2011-08-31 22:51:22 UTC (rev 1553)
+++ trunk/Toss/Formula/FormulaOps.mli 2011-08-31 23:11:10 UTC (rev 1554)
@@ -9,132 +9,19 @@
val nnf : ?neg: bool -> ?rev: string list -> formula -> formula
-(** {2 Vars} *)
-
-val all_vars : formula -> var list
-val free_vars : formula -> var list
-
(** Delete top-most quantification of [vs] in the formula. *)
val del_vars_quant : var list -> formula -> formula
-(** {2 Mapping to atoms and variable substitution.} *)
-(** Generalized map over formula and real expression types. *)
-type formula_and_expr_map = {
- map_Rel : string -> fo_var array -> formula;
- map_Eq : fo_var -> fo_var -> formula;
- map_In : fo_var -> mso_var -> formula;
- map_SO : so_var -> fo_var array -> formula;
- map_RealExpr : real_expr -> sign_op -> formula;
- map_Not : formula -> formula;
- map_And : formula list -> formula;
- map_Or : formula list -> formula;
- map_Ex : var list -> formula -> formula;
- map_All : var list -> formula -> formula;
- map_Lfp : [ mso_var | so_var ] -> fo_var array -> formula -> formula;
- map_Gfp : [ mso_var | so_var ] -> fo_var array -> formula -> formula;
+(** {2 Relation sign} *)
- map_RVar : string -> real_expr;
- map_Const : float -> real_expr;
- map_Times : real_expr -> real_expr -> real_expr;
- map_Plus : real_expr -> real_expr -> real_expr;
- map_Fun : string -> fo_var -> real_expr;
- map_Char : formula -> real_expr;
- map_Sum : fo_var list -> formula -> real_expr -> real_expr
-}
-
-(** Identity map to be refined using the [with] syntax. *)
-val identity_map : formula_and_expr_map
-
-(** Map through the structure adjusting subformulas/subexpressions. *)
-val map_formula : formula_and_expr_map -> formula -> formula
-val map_real_expr : formula_and_expr_map -> real_expr -> real_expr
-
-(** Generalized fold over formula and real expression types. *)
-type 'a formula_and_expr_fold = {
- fold_Rel : string -> fo_var array -> 'a;
- fold_Eq : fo_var -> fo_var -> 'a;
- fold_In : fo_var -> mso_var -> 'a;
- fold_SO : so_var -> fo_var array -> 'a;
- fold_RealExpr : 'a -> sign_op -> 'a;
- fold_Not : 'a -> 'a;
- fold_And : 'a -> 'a -> 'a;
- fold_Or : 'a -> 'a -> 'a;
- fold_Ex : var list -> 'a -> 'a;
- fold_All : var list -> 'a -> 'a;
- fold_Lfp : [ mso_var | so_var ] -> fo_var array -> 'a -> 'a;
- fold_Gfp : [ mso_var | so_var ] -> fo_var array -> 'a -> 'a;
-
- fold_RVar : string -> 'a;
- fold_Const : float -> 'a;
- fold_Times : 'a -> 'a -> 'a;
- fold_Plus : 'a -> 'a -> 'a;
- fold_Fun : string -> fo_v...
[truncated message content] |
