diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-10-23 22:46:50 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-23 22:46:50 -0700 |
| commit | 00e75cb0c6aedab34740b7feadb512ea3c0c7f3d (patch) | |
| tree | e046bca9e8f04be0028811682f4c4b0f6dfa475b /src/options | |
| parent | 2f11cfd563ef96402042e9a3b0086712de660ae6 (diff) | |
CBQI BV: Add ULT/SLT inverse handling. (#1268)
This adds inverse handling for ULT(BV), SLT(BV) and disequalities. Rewriting of inequalities and disequalities to equalities with slack can now be disabled with an option (--cbqi-bv-inv-in-dis-eq). Function solve_bv_constraint is now merged into solve_bv_lit.
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 d3f8c9f6a..05c2512cd 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -339,6 +339,8 @@ option cbqiBvInterleaveValue --cbqi-bv-interleave-value bool :read-write :defaul interleave model value instantiation with word-level inversion approach option cbqiBvSlackIneq --cbqi-bv-slack-ineq bool :read-write :default true use model slack values when solving inequalities with word-level inversion approach +option cbqiBvInvInDisEq --cbqi-bv-inv-in-dis-eq bool :read-write :default false + let bv inverter handle (un)signed less than nodes ### local theory extensions options |