diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/bv/bitblast/eager_bitblaster.cpp | 19 |
1 files changed, 19 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; } |