From: Liana Hadarean Date: Wed, 3 Oct 2012 22:38:37 +0000 (+0000) Subject: implemented collectModelInfo for TheoryBV X-Git-Tag: cvc5-1.0.0~7743 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c7d04993e8d73105d091e0b732ddb63131b431a3;p=cvc5.git implemented collectModelInfo for TheoryBV --- diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index 80b689b8c..08bd3475a 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -338,9 +338,7 @@ void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb) { } void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) { - // Assert (node.getKind() == kind::VARIABLE); Assert(bits.size() == 0); - for (unsigned i = 0; i < utils::getSize(node); ++i) { bits.push_back(utils::mkBitOf(node, i)); } @@ -349,6 +347,10 @@ void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) { BVDebug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting " << node << "\n"; BVDebug("bitvector-bb") << " with bits " << toString(bits); } + // this is not necessairily a variable, but it is a term the theory of bitvectors treads as one + // e.g. a select over a bv array + bb->storeVariable(node); + } void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) { 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::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*/ diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h index ada9802bd..3aee0ee1a 100644 --- a/src/theory/bv/bitblaster.h +++ b/src/theory/bv/bitblaster.h @@ -51,6 +51,7 @@ class BVSatSolverInterface; namespace theory { class OutputChannel; +class TheoryModel; namespace bv { @@ -82,7 +83,8 @@ class Bitblaster { }; typedef __gnu_cxx::hash_map TermDefMap; - typedef __gnu_cxx::hash_set AtomSet; + typedef __gnu_cxx::hash_set AtomSet; + typedef __gnu_cxx::hash_set VarSet; typedef void (*TermBBStrategy) (TNode, Bits&, Bitblaster*); typedef Node (*AtomBBStrategy) (TNode, Bitblaster*); @@ -95,7 +97,7 @@ class Bitblaster { // caches and mappings TermDefMap d_termCache; AtomSet d_bitblastedAtoms; - + VarSet d_variables; context::CDList d_assertedAtoms; /**< context dependent list storing the atoms currently asserted by the DPLL SAT solver. */ @@ -136,7 +138,29 @@ public: void explain(TNode atom, std::vector& explanation); EqualityStatus getEqualityStatus(TNode a, TNode b); - + /** + * Return a constant Node representing the value of a variable + * in the current model. + * @param a + * + * @return + */ + Node getVarValue(TNode a); + /** + * Adds a constant value for each bit-blasted variable in the model. + * + * @param m the model + */ + void collectModelInfo(TheoryModel* m); + /** + * Stores the variable (or non-bv term) and its corresponding bits. + * + * @param var + * @param bits + */ + void storeVariable(TNode var) { + d_variables.insert(var); + } private: diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index f8c763e3f..98b809d85 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -28,6 +28,9 @@ namespace CVC4 { namespace theory { + +class TheoryModel; + namespace bv { enum SubTheory { @@ -82,7 +85,7 @@ public: virtual bool addAssertions(const std::vector& assertions, Theory::Effort e) = 0; virtual void explain(TNode literal, std::vector& assumptions) = 0; virtual void preRegister(TNode node) {} - + virtual void collectModelInfo(TheoryModel* m) = 0; }; } diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index b0d04f952..e28ec188d 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -125,3 +125,7 @@ bool BitblastSolver::addAssertions(const std::vector& assertions, Theory: EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) { return d_bitblaster->getEqualityStatus(a, b); } + +void BitblastSolver::collectModelInfo(TheoryModel* m) { + return d_bitblaster->collectModelInfo(m); +} diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 33ae5d2ff..a2c77c9f5 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -47,6 +47,7 @@ public: bool addAssertions(const std::vector& assertions, Theory::Effort e); void explain(TNode literal, std::vector& assumptions); EqualityStatus getEqualityStatus(TNode a, TNode b); + void collectModelInfo(TheoryModel* m); }; } diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp index cb08a1ad8..56a490747 100644 --- a/src/theory/bv/bv_subtheory_eq.cpp +++ b/src/theory/bv/bv_subtheory_eq.cpp @@ -19,7 +19,7 @@ #include "theory/bv/bv_subtheory_eq.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" - +#include "theory/model.h" using namespace std; using namespace CVC4; using namespace CVC4::context; @@ -165,3 +165,6 @@ void EqualitySolver::conflict(TNode a, TNode b) { d_bv->setConflict(mkAnd(assumptions)); } +void EqualitySolver::collectModelInfo(TheoryModel* m) { + m->assertEqualityEngine(&d_equalityEngine); +} diff --git a/src/theory/bv/bv_subtheory_eq.h b/src/theory/bv/bv_subtheory_eq.h index d0ba8abca..24d9669db 100644 --- a/src/theory/bv/bv_subtheory_eq.h +++ b/src/theory/bv/bv_subtheory_eq.h @@ -19,7 +19,6 @@ #pragma once #include "cvc4_private.h" - #include "theory/bv/bv_subtheory.h" namespace CVC4 { @@ -68,6 +67,7 @@ public: void preRegister(TNode node); bool addAssertions(const std::vector& assertions, Theory::Effort e); void explain(TNode literal, std::vector& assumptions); + void collectModelInfo(TheoryModel* m); void addSharedTerm(TNode t) { d_equalityEngine.addTriggerTerm(t, THEORY_BV); } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index aa5281d2f..51e09ee5a 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -23,7 +23,7 @@ #include "theory/bv/bitblaster.h" #include "theory/bv/options.h" #include "theory/bv/theory_bv_rewrite_rules_normalization.h" - +#include "theory/model.h" using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::bv; @@ -126,7 +126,11 @@ void TheoryBV::check(Effort e) } void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){ - + Assert(!inConflict()); + Assert (fullModel); // can only query full model + d_equalitySolver.collectModelInfo(m); + d_bitblastSolver.collectModelInfo(m); + } void TheoryBV::propagate(Effort e) {