Module FormulaOps

module FormulaOps: sig .. end

Operations on formulas.

NNF

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.

Simplification

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).

TNF

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.

Reals

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.