diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-16 17:30:59 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-16 17:30:59 -0500 |
commit | 246fffffafba07aaeadd0d0c99a2e1c4b589a63c (patch) | |
tree | 5d2b41e264fc2039da115556befa7fe487a12bb7 /src/theory/bv | |
parent | f58c881034d3b0193dfee8fabf451cc0e9ea20ab (diff) |
Enable --sygus-direct-eval by default, limit to terms that do not induce Boolean structure. Minor fixes for bitvectors: rewrite SDIV to total operators when options::bitvectorDivByZeroConst is true, fix collectModelInfo when fullModel=false. Lift ITEs in sygus search. Fix sygus initialization related to cbqi.
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 2 | ||||
-rw-r--r-- | src/theory/bv/eager_bitblaster.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h | 4 |
4 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index cfbadbf32..5fdc549d0 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -459,7 +459,7 @@ Node TBitblaster<T>::getTermModel(TNode node, bool fullModel) { if (Theory::isLeafOf(node, theory::THEORY_BV)) { // if it is a leaf may ask for fullModel - value = getModelFromSatSolver(node, fullModel); + value = getModelFromSatSolver(node, true); Debug("bv-equality-status")<< "TLazyBitblaster::getTermModel from VarValue" << node <<" => " << value <<"\n"; Assert ((fullModel && !value.isNull() && value.isConst()) || !fullModel); if (!value.isNull()) { diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index 3b54e3794..a103d1f63 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -216,7 +216,7 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { // only shared terms could not have been bit-blasted Assert (hasBBTerm(var) || isSharedTerm(var)); - Node const_value = getModelFromSatSolver(var, fullModel); + Node const_value = getModelFromSatSolver(var, true); if(const_value != Node()) { Debug("bitvector-model") << "EagerBitblaster::collectModelInfo (assert (= " diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index c821b50cd..b549c329a 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -491,7 +491,7 @@ void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { // only shared terms could not have been bit-blasted Assert (hasBBTerm(var) || isSharedTerm(var)); - Node const_value = getModelFromSatSolver(var, fullModel); + Node const_value = getModelFromSatSolver(var, true); Assert (const_value.isNull() || const_value.isConst()); if(const_value != Node()) { Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= " diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 152a335a5..2bcb6ca1b 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -349,7 +349,7 @@ Node RewriteRule<SdivEliminate>::apply(TNode node) { Node abs_a = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a); Node abs_b = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b); - Node a_udiv_b = utils::mkNode(kind::BITVECTOR_UDIV, abs_a, abs_b); + Node a_udiv_b = utils::mkNode(options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UDIV, abs_a, abs_b); Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_udiv_b); Node condition = utils::mkNode(kind::XOR, a_lt_0, b_lt_0); @@ -377,7 +377,7 @@ Node RewriteRule<SremEliminate>::apply(TNode node) { Node abs_a = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a); Node abs_b = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b); - Node a_urem_b = utils::mkNode(kind::BITVECTOR_UREM, abs_a, abs_b); + Node a_urem_b = utils::mkNode( options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UREM_TOTAL : kind::BITVECTOR_UREM, abs_a, abs_b); Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_urem_b); Node result = utils::mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b); |