Simplifiers Summary
Simplifier bit-blast
Description
reduce bit-vector expressions into SAT.
Simplifier bit2int
Description
simplify bit2int expressions.
Simplifier bound-simplifier
Description
Simplify arithmetical expressions modulo bounds.
Simplifier bv-slice
Description
simplify using bit-vector slices.
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 demodulator
Description
extracts equalities from quantifiers and applies them to simplify.
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 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 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.