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