diff options
Diffstat (limited to 'src/theory/bv/eager_bitblaster.h')
-rw-r--r-- | src/theory/bv/eager_bitblaster.h | 73 |
1 files changed, 70 insertions, 3 deletions
diff --git a/src/theory/bv/eager_bitblaster.h b/src/theory/bv/eager_bitblaster.h index da73c7f09..91ef866bd 100644 --- a/src/theory/bv/eager_bitblaster.h +++ b/src/theory/bv/eager_bitblaster.h @@ -20,11 +20,13 @@ #define __CVC4__EAGER__BITBLASTER_H -#include "bitblaster_template.h" #include "theory/theory_registrar.h" +#include "theory/bv/bitblaster_template.h" +#include "theory/bv/options.h" +#include "theory/theory_model.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" -#include "theory/bv/options.h" + namespace CVC4 { namespace theory { @@ -43,9 +45,11 @@ public: };/* class Registrar */ -EagerBitblaster::EagerBitblaster() +EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) : TBitblaster<Node>() + , d_bv(theory_bv) , d_bbAtoms() + , d_variables() { d_bitblastingRegistrar = new BitblastingRegistrar(this); d_nullContext = new context::Context(); @@ -126,6 +130,7 @@ void EagerBitblaster::makeVariable(TNode var, Bits& bits) { for (unsigned i = 0; i < utils::getSize(var); ++i) { bits.push_back(utils::mkBitOf(var, i)); } + d_variables.insert(var); } Node EagerBitblaster::getBBAtom(TNode node) const { @@ -154,6 +159,68 @@ bool EagerBitblaster::solve() { } +/** + * Returns the value a is currently assigned to in the SAT solver + * or null if the value is completely unassigned. + * + * @param a + * @param fullModel whether to create a "full model," i.e., add + * constants to equivalence classes that don't already have them + * + * @return + */ +Node EagerBitblaster::getVarValue(TNode a, bool fullModel) { + if (!hasBBTerm(a)) { + Assert(isSharedTerm(a)); + return Node(); + } + Bits bits; + getBBTerm(a, bits); + Integer value(0); + for (int i = bits.size() -1; i >= 0; --i) { + prop::SatValue bit_value; + if (d_cnfStream->hasLiteral(bits[i])) { + prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]); + bit_value = d_satSolver->value(bit); + Assert (bit_value != prop::SAT_VALUE_UNKNOWN); + } else { + // the bit is unconstrainted so we can give it an arbitrary value + bit_value = prop::SAT_VALUE_FALSE; + } + Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0); + value = value * 2 + bit_int; + } + return utils::mkConst(BitVector(bits.size(), value)); +} + + +void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { + TNodeSet::const_iterator it = d_variables.begin(); + for (; it!= d_variables.end(); ++it) { + TNode var = *it; + if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { + Node const_value = getVarValue(var, fullModel); + if(const_value == Node()) { + if( fullModel ){ + // if the value is unassigned just set it to zero + const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); + } + } + if(const_value != Node()) { + Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= " + << var << " " + << const_value << "))\n"; + m->assertEquality(var, const_value, true); + } + } + } +} + +bool EagerBitblaster::isSharedTerm(TNode node) { + return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); +} + + } /*bv namespace */ } /* theory namespace */ } /* CVC4 namespace*/ |