diff options
Diffstat (limited to 'src/theory/bv/bitblaster.cpp')
-rw-r--r-- | src/theory/bv/bitblaster.cpp | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index 3beb7c229..4aa52e24c 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -26,6 +26,7 @@ #include "theory/bv/theory_bv_rewrite_rules_simplification.h" #include "theory/bv/theory_bv.h" #include "theory/bv/options.h" +#include "theory/model.h" using namespace std; @@ -398,6 +399,35 @@ EqualityStatus Bitblaster::getEqualityStatus(TNode a, TNode b) { } } +Node Bitblaster::getVarValue(TNode a) { + Assert (d_termCache.find(a) != d_termCache.end()); + Bits bits = d_termCache[a]; + Integer value(0); + for (int i = bits.size() -1; i >= 0; --i) { + SatValue bit_value; + if (d_cnfStream->hasLiteral(bits[i])) { + SatLiteral bit = d_cnfStream->getLiteral(bits[i]); + bit_value = d_satSolver->value(bit); + Assert (bit_value != SAT_VALUE_UNKNOWN); + } else { + // the bit is unconstrainted so we can give it an arbitrary value + bit_value = SAT_VALUE_FALSE; + } + Integer bit_int = bit_value == SAT_VALUE_TRUE ? Integer(1) : Integer(0); + value = value * 2 + bit_int; + } + return utils::mkConst(BitVector(bits.size(), value)); +} + +void Bitblaster::collectModelInfo(TheoryModel* m) { + __gnu_cxx::hash_set<TNode, TNodeHashFunction>::iterator it = d_variables.begin(); + for (; it!= d_variables.end(); ++it) { + TNode var = *it; + Node const_value = getVarValue(var); + m->assertEquality(var, const_value, true); + } +} + } /*bv namespace */ } /* theory namespace */ } /* CVC4 namespace*/ |