diff options
author | Andres Noetzli <noetzli@stanford.edu> | 2019-05-15 17:38:04 +0000 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2019-05-15 10:38:04 -0700 |
commit | f2d113cf3cbb0f4966a7c909b9cd2c14aa753eb1 (patch) | |
tree | df20d8af54d7d7d33d5ab41e7f2401c51a10d2dc /src | |
parent | bc550fa115401256616042ccb7a559ec252e319b (diff) |
Fix model of Boolean vars with eager bit-blaster (#2998)
When bit-blasting eagerly, we were not assigning values to the Boolean
variables in the `TheoryModel`. With eager bit-blasting, the BV SAT
solver gets all (converted) terms, including the Boolean ones, so
`EagerBitblaster::collectModelInfo()` is responsible for assigning
values to Boolean variables. However, it has only been assigning values
to bit-vector variables, which lead to wrong models. This commit fixes
the issue by asking the `CnfStream` for the Boolean variables, querying
the SAT solver for their value, and assigning them in the `TheoryModel`.
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; } |