Module SrkSimplify

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