Simplifiers Summary
Simplifier bit-blast
Description
reduce bit-vector expressions into SAT.
Simplifier bit2int
Description
simplify bit2int expressions.
Simplifier blast-term-ite
Description
blast term if-then-else by hoisting them.
Simplifier bv-divrem-bounds
Description
add range lemmas for bit-vector division/remainder terms with a symbolic divisor.
Simplifier bv-slice
Description
simplify using bit-vector slices.
Simplifier bv1-blast
Description
reduce bit-vector expressions into bit-vectors of size 1 (notes: only equality, extract and concat are supported).
Simplifier bvarray2uf
Description
Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.
Simplifier card2bv
Description
convert pseudo-boolean constraints to bit-vectors.
Simplifier cheap-fourier-motzkin
Description
eliminate variables from quantifiers using partial Fourier-Motzkin elimination.
Simplifier cofactor-term-ite
Description
eliminate term if-then-else using cofactors.
Simplifier demodulator
Description
extracts equalities from quantifiers and applies them to simplify.
Simplifier der
Description
destructive equality resolution.
Simplifier distribute-forall
Description
distribute forall over conjunctions.
Simplifier dom-simplify
Description
apply dominator simplification rules.
Simplifier elim-predicates
Description
eliminate predicates, macros and implicit definitions.
Simplifier elim-term-ite
Description
eliminate if-then-else term by hoisting them top top-level.
Simplifier elim-unconstrained
Description
eliminate unconstrained variables.
Simplifier euf-completion
Description
simplify modulo congruence closure.
Simplifier factor
Description
polynomial factorization.
Simplifier fold-unfold
Description
solve for variables.
Simplifier injectivity
Description
Identifies and applies injectivity axioms.
Simplifier max-bv-sharing
Description
use heuristics to maximize the sharing of bit-vector expressions such as adders and multipliers.
Simplifier propagate-bv-bounds
Description
propagate bit-vector bounds by simplifying implied or contradictory bounds.
Simplifier propagate-ineqs
Description
propagate ineqs/bounds, remove subsumed inequalities.
Simplifier propagate-values
Description
propagate constants.
Simplifier pull-nested-quantifiers
Description
pull nested quantifiers to top-level.
Simplifier push-app-ite-conservative
Description
Push functions over if-then else.
Simplifier push-app-ite
Description
Push functions over if-then else.
Simplifier ng-push-app-ite-conservative
Description
Push functions over if-then-else within non-ground terms only.
Simplifier ng-push-app-ite
Description
Push functions over if-then-else within non-ground terms only.
Simplifier qe-light
Description
apply light-weight quantifier elimination.
Simplifier randomizer
Description
shuffle assertions and rename uninterpreted functions.
Simplifier reduce-args
Description
reduce the number of arguments of function applications, when for all occurrences of a function f the i-th is a value.
Simplifier refine-injectivity
Description
refine injectivity axioms.
Simplifier simplify
Description
apply simplification rules.
Simplifier solve-eqs
Description
solve for variables.
Simplifier special-relations
Description
detect and replace by special relations.