module FormulaSubst: sig .. end
Substitutions in formulas and real-valued expressions.
Basic Substitution Functions
val var_subst : (string * string) list -> [< Formula.var ] -> Formula.var
Helper function: apply subsutitution subst to the variable v.
val subst_name_avoiding_str : string list -> string -> string * string
Find a substitution for v which avoids avs, string arguments.
val subst_name_prefix : string Pervasives.ref
Prefix for variable name replacements. Default (empty) = derived from var.
val subst_name_avoiding : [< Formula.var ] list -> [< Formula.var ] -> string * string
Find a substitution for v which avoids avs.
val subst_vars : (string * string) list -> Formula.formula -> Formula.formula
Apply substitution subst to all free variables in the given formula
checking for and preventing name clashes with quantified variables.
val subst_vars_expr : (string * string) list -> Formula.real_expr -> Formula.real_expr
val subst_real : (string * Formula.real_expr) list -> Formula.real_expr -> Formula.real_expr
Substitute a real variable with a subexpression.
val subst_once_rels : (string * (string list * Formula.formula)) list ->
Formula.formula -> Formula.formula
Substitute once relations in defs by corresponding subformulas
(with instantiated parameters).
val subst_once_rels_expr : (string * (string list * Formula.formula)) list ->
Formula.real_expr -> Formula.real_expr
val subst_rels : (string * (string list * Formula.formula)) list ->
Formula.formula -> Formula.formula
Substitute recursively relations defined in defs by their definitions.
val subst_rels_expr : (string * (string list * Formula.formula)) list ->
Formula.real_expr -> Formula.real_expr
val expand_formula : ?defs:(string * (string list * Formula.formula)) list ->
Formula.formula -> Formula.formula
Expand Let's and RLet's in formula. *
val expand_real_expr : ?defs:(string * (string list * Formula.formula)) list ->
Formula.real_expr -> Formula.real_expr
Auxiliary Functions
val range : ?estimates:(string * (float * float)) list ->
?pred_est:((string * int) * float) list ->
int -> Formula.real_expr -> float * float
Rough estimate of the range of a real-valued expression given structure
size and function, real-variable value and predicate size estimates.
val assign_emptyset : string -> Formula.formula -> Formula.formula
Assign emptyset to an MSO-variable.
Variables
val all_vars : Formula.formula -> Formula.var list
All variables in a formula.
val free_vars : Formula.formula -> Formula.var list
Free variables in a formula.
val quantified_vars : Formula.formula -> Formula.var list
Quantified variables in a formula.
val push_quant : Formula.formula -> Formula.formula
Basic pushing of quantifiers inside a formula
Transitive Closure
val make_lfp_tc : string -> string -> Formula.formula -> Formula.formula
Transitive closure of phi(x, y, z) over x and y, an LFP formula.
val make_mso_tc : string -> string -> Formula.formula -> Formula.formula
Transitive closure of phi(x, y, z) over x and y, an MSO formula.
val make_fo_tc_conj : ?reflexive:bool ->
int -> string -> string -> Formula.formula -> Formula.formula
First-order k-step refl. transitive closure of phi over x and y.
val make_fo_tc_disj : ?reflexive:bool ->
int -> string -> string -> Formula.formula -> Formula.formula
val fo_tc_param : int Pervasives.ref
Parameter governing whether to use LFP or FO TC when parsing.
val make_standard_tc : string -> string -> Formula.formula -> Formula.formula
The default TC syntax: LFP if fo_tc_param = 0 else FO with fo_tc_param.