diff options
| -rw-r--r-- | src/theory/bv/bitblast/eager_bitblaster.cpp | 19 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/bv/bool-model.smt2 | 7 |
3 files changed, 27 insertions, 0 deletions
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index 77ff6f885..0d3d3b483 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -241,6 +241,9 @@ Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) { bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { + NodeManager* nm = NodeManager::currentNM(); + + // Collect the values for the bit-vector variables TNodeSet::iterator it = d_variables.begin(); for (; it != d_variables.end(); ++it) { TNode var = *it; @@ -262,6 +265,22 @@ bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) } } } + + // Collect the values for the Boolean variables + std::vector<TNode> vars; + d_cnfStream->getBooleanVariables(vars); + for (TNode var : vars) + { + Assert(d_cnfStream->hasLiteral(var)); + prop::SatLiteral bit = d_cnfStream->getLiteral(var); + prop::SatValue value = d_satSolver->value(bit); + Assert(value != prop::SAT_VALUE_UNKNOWN); + if (!m->assertEquality( + var, nm->mkConst(value == prop::SAT_VALUE_TRUE), true)) + { + return false; + } + } return true; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 307906dc3..c3f2bc866 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -159,6 +159,7 @@ set(regress_0_tests regress0/bv/ackermann2.smt2 regress0/bv/ackermann3.smt2 regress0/bv/ackermann4.smt2 + regress0/bv/bool-model.smt2 regress0/bv/bool-to-bv-all.smt2 regress0/bv/bool-to-bv-ite.smt2 regress0/bv/bug260a.smt diff --git a/test/regress/regress0/bv/bool-model.smt2 b/test/regress/regress0/bv/bool-model.smt2 new file mode 100644 index 000000000..30531418c --- /dev/null +++ b/test/regress/regress0/bv/bool-model.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --bitblast=eager +(set-info :status sat) +(set-logic QF_BV) +(declare-fun x () Bool) +(declare-fun y () Bool) +(assert (xor y x)) +(check-sat) |