Module FormulaOps

module FormulaOps: sig .. end
Operations on formulas.


val nnf : ?neg:bool -> ?rev:string list -> Formula.formula -> Formula.formula
Convert formula to NNF and additionally negate if neg is set.
val make_fp_inductive : int -> Formula.formula -> Formula.formula
Replace fixed-points by their inductive evaluation for given size.
val del_vars_quant : Formula.var list -> Formula.formula -> Formula.formula
Delete top-most quantification of vs in the formula.
val rename_quant_avoiding : Formula.var list -> Formula.formula -> Formula.formula
Rename quantified variables avoiding the ones from avs, and the above-quantified ones. Does not go into real_expr.

Relation sign

val rels_signs : Formula.formula -> Aux.Strings.t * Aux.Strings.t
Find all positively and negatively occurring relations.
val rels_signs_expr : Formula.real_expr -> Aux.Strings.t * Aux.Strings.t

Type generating functions.

val atoms : ?repetitions:bool ->
(string * int) list -> string list -> Formula.formula list
All atoms over given signature and variables.
val atp : (string * int) list -> string list -> Formula.formula list
AType with variables over given relations, no repetition, equality.
val mintp : (Formula.formula -> bool) ->
(string * int) list -> string list -> Formula.formula list
Minimal type satisfying f over rels extending vars.


val simplify : ?do_pnf:bool -> ?do_re:bool -> ?ni:int -> Formula.formula -> Formula.formula
Recursively simplify a formula
val simplify_re : ?do_pnf:bool ->
?do_formula:bool -> ?ni:int -> Formula.real_expr -> Formula.real_expr
Recursively simplify a real expr
val pnf : Formula.formula -> Formula.formula
Prenex normal form.
val as_conjuncts : Formula.formula -> Formula.formula list
Formula as a list of conjuncts, with one level of distributing negation over disjunction and pushing quantifiers inside.
val remove_subformulas : (Formula.formula -> bool) -> Formula.formula -> Formula.formula
"Erase" indicated subformulas from the formula.
val prune_unused_quants : Formula.formula -> Formula.formula
Remove quantifiers that bind only variables not occurring freely in the body.
val remove_redundant : ?implies:(Formula.formula -> Formula.formula -> bool) ->
Formula.formula -> Formula.formula
Simplify the formula by removing relational literals, depending on what literals they are conjoined with up the tree, whether they are in a disjunction and what literals they are disjoined with, keeping track of the sign (variance) of a position. (Does not descend the real part currently.) implies is applied to atoms only. Repeat the removal till fixpoint since it can "unpack" literals e.g. from conjunctions to disjunctions. Also perform a very basic check for satisfiability. Returns Or [] if the formula is obviously unsatisfiable (does not do any unification).


val tnf : Formula.formula -> Formula.formula
Convert formula to TNF; or negTNF when neg is set. Type normal form in a NNF form which pushes quantifiers inside as strongly as possible.
val tnf_re : Formula.real_expr -> Formula.real_expr
val tnf_fv : ?sizes:(string * int) list -> Formula.formula -> Formula.formula
first existentially quantifies free vars

Convert to CNF or DNF

val to_dnf : Formula.formula -> Formula.formula list
Convert an arbitrary boolean combination to DNF.
val to_cnf : Formula.formula -> Formula.formula list
Convert an arbitrary boolean combination to CNF.

Multi-dimensional Formulas

val dimension_vars : int -> string list -> string list
Make the list of FO variable names n-dimensional.
val dimension : int -> size:int -> Formula.formula -> Formula.formula
Create a n-dimensional formula for structures of given size.


val piecewise_linear : Formula.real_expr -> (float * float) list -> Formula.real_expr
Generate a piecewise-linear function of a given argument from a graph. Raise Failure "piecewise_linear" if first elements of the graph are not unique or graph is empty.
val rk4_step_symb : string ->
Formula.real_expr ->
Formula.real_expr ->
Formula.eq_sys -> Formula.real_expr list -> Formula.real_expr list
Perform a Runge-Kutta (RK4) step for vars with vals_init and right-hand side eq_terms. Time variable tvar starts at tinit and moves tstep.