module SrkSimplify: sig
.. end
Formula and term simplification.
module TermPolynomial: sig
.. end
val simplify_terms_rewriter : 'a Syntax.context -> 'a Syntax.rewriter
val simplify_terms : 'a Syntax.context -> ('a, 'b) Syntax.expr -> ('a, 'b) Syntax.expr
val purify : 'a Syntax.context ->
'a Syntax.formula ->
'a Syntax.formula * ('a, Syntax.typ_fo) Syntax.expr Syntax.Symbol.Map.t
Purify function applications in a ground formula: replace each function
application within a formula with a fresh symbol, and return both the
resulting formula and a mapping from the fresh symbols to the terms they
define.
val partition_implicant : 'a Syntax.formula list -> 'a Syntax.formula list list