Module FormulaMap

module FormulaMap: sig .. end

Maps, iterators and folds over formulas and real-valued expressions.

Basic maps - to literals and atoms.

val get_atoms : Formula.formula -> Formula.formula list

All atoms in a formula.

val get_relations_constants : Formula.formula -> (string * int) list * string list

All relations in a formula, with arities, and constants that appear.

val map_to_literals : ?save_rels:string list ->
       ?save_rvars:string list ->
       (Formula.formula -> Formula.formula) ->
       (Formula.real_expr -> Formula.real_expr) ->
       (Formula.formula -> Formula.formula) -> Formula.formula -> Formula.formula

Map f to all literals (i.e. atoms or not(atom)'s) in the given formula. Do not touch save_rels or save_rvars. Preserves order of subformulas. The last function is forced and applied to saved relations.

val map_to_literals_expr : ?save_rels:string list ->
       ?save_rvars:string list ->
       (Formula.formula -> Formula.formula) ->
       (Formula.real_expr -> Formula.real_expr) ->
       (Formula.formula -> Formula.formula) ->
       Formula.real_expr -> Formula.real_expr

val map_to_atoms_full : (Formula.formula -> Formula.formula) ->
       (Formula.real_expr -> Formula.real_expr) ->
       (Formula.formula -> Formula.formula) -> Formula.formula -> Formula.formula

Map f to all atoms in the given formula.

val map_to_atoms_full_re : (Formula.formula -> Formula.formula) ->
       (Formula.real_expr -> Formula.real_expr) ->
       (Formula.formula -> Formula.formula) ->
       Formula.real_expr -> Formula.real_expr

val map_to_atoms : (Formula.formula -> Formula.formula) -> Formula.formula -> Formula.formula

val map_to_atoms_expr : (Formula.formula -> Formula.formula) ->
       Formula.real_expr -> Formula.real_expr

Generalized maps

type formula_and_expr_map = {

	`map_Rel :string -> Formula.const_or_fo_var array -> Formula.formula;`
	`map_Eq :Formula.const_or_fo_var -> Formula.const_or_fo_var -> Formula.formula;`
	`map_SO :Formula.so_var -> Formula.const_or_fo_var array -> Formula.formula;`
	`map_RealExpr :Formula.real_expr -> Formula.sign_op -> Formula.formula;`
	`map_Not :Formula.formula -> Formula.formula;`
	`map_And :Formula.formula list -> Formula.formula;`
	`map_Or :Formula.formula list -> Formula.formula;`
	`map_Ex :Formula.var list -> Formula.formula -> Formula.formula;`
	`map_All :Formula.var list -> Formula.formula -> Formula.formula;`
	`map_Lfp :Formula.so_var -> Formula.fo_var array -> Formula.formula -> Formula.formula;`
	`map_Gfp :Formula.so_var -> Formula.fo_var array -> Formula.formula -> Formula.formula;`
	`map_Let :string -> string list -> Formula.formula -> Formula.formula -> Formula.formula;`
	`map_RVar :string -> Formula.real_expr;`
	`map_Const :float -> Formula.real_expr;`
	`map_Plus :Formula.real_expr -> Formula.real_expr -> Formula.real_expr;`
	`map_Times :Formula.real_expr -> Formula.real_expr -> Formula.real_expr;`
	`map_Pow :Formula.real_expr -> Formula.real_expr -> Formula.real_expr;`
	`map_Fun :string -> Formula.const_or_fo_var -> Formula.real_expr;`
	`map_Char :Formula.formula -> Formula.real_expr;`
	`map_Sum :Formula.fo_var list -> Formula.formula -> Formula.real_expr -> Formula.real_expr;`
	`map_RLet :string -> Formula.real_expr -> Formula.real_expr -> Formula.real_expr;`

}

Generalized map over formula and real expression types.

val identity_map : formula_and_expr_map

Identity map to be refined using the with syntax.

val map_formula : formula_and_expr_map -> Formula.formula -> Formula.formula

Map through the structure adjusting subformulas/subexpressions.

val map_real_expr : formula_and_expr_map -> Formula.real_expr -> Formula.real_expr

type 'a formula_and_expr_fold = {

	`fold_Rel :string -> Formula.const_or_fo_var array -> 'a;`
	`fold_Eq :Formula.const_or_fo_var -> Formula.const_or_fo_var -> 'a;`
	`fold_SO :Formula.so_var -> Formula.const_or_fo_var array -> 'a;`
	`fold_RealExpr :'a -> Formula.sign_op -> 'a;`
	`fold_Not :'a -> 'a;`
	`fold_And :'a -> 'a -> 'a;`
	`fold_Or :'a -> 'a -> 'a;`
	`fold_Ex :Formula.var list -> 'a -> 'a;`
	`fold_All :Formula.var list -> 'a -> 'a;`
	`fold_Lfp :Formula.so_var -> Formula.fo_var array -> 'a -> 'a;`
	`fold_Gfp :Formula.so_var -> Formula.fo_var array -> 'a -> 'a;`
	`fold_Let :string -> string list -> 'a -> 'a -> 'a;`
	`fold_RVar :string -> 'a;`
	`fold_Const :float -> 'a;`
	`fold_Plus :'a -> 'a -> 'a;`
	`fold_Times :'a -> 'a -> 'a;`
	`fold_Pow :'a -> 'a -> 'a;`
	`fold_Fun :string -> Formula.const_or_fo_var -> 'a;`
	`fold_Char :'a -> 'a;`
	`fold_Sum :Formula.fo_var list -> 'a -> 'a -> 'a;`
	`fold_RLet :string -> 'a -> 'a -> 'a;`

}

Generalized fold over formula and real expression types.

val make_fold : ('a -> 'a -> 'a) -> 'a -> 'a formula_and_expr_fold

val fold_formula : 'a formula_and_expr_fold -> Formula.formula -> 'a

Fold the structure using the operations. (Not tail-recursive.)

val fold_real_expr : 'a formula_and_expr_fold -> Formula.real_expr -> 'a

val map_to_formulas_expr : (Formula.formula -> Formula.formula) ->
       Formula.real_expr -> Formula.real_expr

Map f to top-level formulas in the real expression (Chars and Sum guards).

val fold_over_formulas_expr : (Formula.formula -> 'a -> 'a) -> Formula.real_expr -> 'a -> 'a

val fold_over_literals : (Formula.formula -> 'a -> 'a) -> Formula.formula -> 'a -> 'a

val fold_over_atoms : (Formula.formula -> 'a -> 'a) -> Formula.formula -> 'a -> 'a

val map_to_all_vars : (Formula.var -> Formula.var) -> Formula.formula -> Formula.formula

Map