diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2017-12-08 17:36:15 -0800 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2017-12-08 17:36:15 -0800 |
| commit | 99fb7d9e0b963222574c01e0362d3720c62b825f (patch) | |
| tree | d0792c0d93e44db226c5c619f1b611cbfb2b67bb /src/options | |
| parent | 707571c8b4a572b9554f9068df796f1257cb587d (diff) | |
Add CEGQI BV linearization of additions and equalities over additions. (#1417)
Adds support for linearizing additions w.r.t. to a variable.
For example,
a * x + b + c * d * -x = e + x
is rewritten to
x * (a - c * d - 1) = e - b.
This also adds an additional rewriting rule x * x = x --> x < 2.
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/quantifiers_options | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index ef20881db..c3091a131 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -349,6 +349,8 @@ option cbqiBvIneqMode --cbqi-bv-ineq=MODE CVC4::theory::quantifiers::CbqiBvIneqM choose mode for handling bit-vector inequalities with counterexample-guided instantiation option cbqiBvRmExtract --cbqi-bv-rm-extract bool :read-write :default true replaces extract terms with variables for counterexample-guided instantiation for bit-vectors +option cbqiBvLinearize --cbqi-bv-linear bool :read-write :default true + linearize adder chains for variables ### local theory extensions options |