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/theory/quantifiers/bv_inverter.h | |
| 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/theory/quantifiers/bv_inverter.h')
| -rw-r--r-- | src/theory/quantifiers/bv_inverter.h | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index 724b3b7a7..861331170 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -85,19 +85,11 @@ class BvInverter { */ Node eliminateSkolemFunctions(TNode n, std::vector<Node>& side_conditions); - /** solve_bv_constraint - * solve for sv in constraint ( (pol ? _ : not) sv_t <rk> t ), where sv_t.path - * = sv status accumulates side conditions - */ - Node solve_bv_constraint(Node sv, Node sv_t, Node t, Kind rk, bool pol, - std::vector<unsigned>& path, BvInverterModelQuery* m, - BvInverterStatus& status); - /** solve_bv_lit * solve for sv in lit, where lit.path = sv * status accumulates side conditions */ - Node solve_bv_lit(Node sv, Node lit, bool pol, std::vector<unsigned>& path, + Node solve_bv_lit(Node sv, Node lit, std::vector<unsigned>& path, BvInverterModelQuery* m, BvInverterStatus& status); private: |