diff options
author | lianah <lianahady@gmail.com> | 2013-04-18 19:09:44 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-04-18 19:09:44 -0400 |
commit | c863478fd87b4ff7d97d00a4a63a4c5e9bac2b4b (patch) | |
tree | a4417d4a56733f660a8e410db35addda1f0cacfe /src/theory/bv | |
parent | eaa9f9af40941ef1aeb93367884e692301b60280 (diff) | |
parent | 8d56bb7184d573448fd16242afda2e4224e8641d (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.cpp | 48 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.h | 8 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 19 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_inequality.cpp | 11 |
4 files changed, 73 insertions, 13 deletions
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index d8a784544..997244c40 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -31,7 +31,8 @@ BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv) : SubtheorySolver(c, bv), d_bitblaster(new Bitblaster(c, bv)), d_bitblastQueue(c), - d_statistics() + d_statistics(), + d_validModelCache(c, true) {} BitblastSolver::~BitblastSolver() { @@ -87,6 +88,7 @@ bool BitblastSolver::check(Theory::Effort e) { // Processing assertions while (!done()) { TNode fact = get(); + d_validModelCache = false; Debug("bv-bitblast") << " fact " << fact << ")\n"; if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) { // Some atoms have not been bit-blasted yet @@ -138,8 +140,46 @@ void BitblastSolver::collectModelInfo(TheoryModel* m) { return d_bitblaster->collectModelInfo(m); } -Node BitblastSolver::getModelValue(TNode node) { - Node val = d_bitblaster->getVarValue(node); - Assert (val != Node() || d_bv->isSharedTerm(node)); +Node BitblastSolver::getModelValue(TNode node) +{ + if (!d_validModelCache) { + d_modelCache.clear(); + d_validModelCache = true; + } + return getModelValueRec(node); +} + +Node BitblastSolver::getModelValueRec(TNode node) +{ + Node val; + if (node.isConst()) { + return node; + } + NodeMap::iterator it = d_modelCache.find(node); + if (it != d_modelCache.end()) { + val = (*it).second; + Debug("bitvector-model") << node << " => (cached) " << val <<"\n"; + return val; + } + if (d_bv->isLeaf(node)) { + val = d_bitblaster->getVarValue(node); + if (val == Node()) { + // If no value in model, just set to 0 + val = utils::mkConst(utils::getSize(node), (unsigned)0); + } + } else { + NodeBuilder<> valBuilder(node.getKind()); + if (node.getMetaKind() == kind::metakind::PARAMETERIZED) { + valBuilder << node.getOperator(); + } + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + valBuilder << getModelValueRec(node[i]); + } + val = valBuilder; + val = Rewriter::rewrite(val); + } + Assert(val.isConst()); + d_modelCache[node] = val; + Debug("bitvector-model") << node << " => " << val <<"\n"; return val; } diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 1fab621cd..819b3d62c 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -19,7 +19,7 @@ #pragma once #include "theory/bv/bv_subtheory.h" - +#include "theory/substitutions.h" namespace CVC4 { namespace theory { namespace bv { @@ -41,6 +41,12 @@ class BitblastSolver : public SubtheorySolver { /** Nodes that still need to be bit-blasted */ context::CDQueue<TNode> d_bitblastQueue; Statistics d_statistics; + + typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + NodeMap d_modelCache; + context::CDO<bool> d_validModelCache; + Node getModelValueRec(TNode node); + public: BitblastSolver(context::Context* c, TheoryBV* bv); ~BitblastSolver(); diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index a1c8f0e9a..c0546f892 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -387,17 +387,26 @@ void CoreSolver::collectModelInfo(TheoryModel* m) { } Node CoreSolver::getModelValue(TNode var) { + // we don't need to evaluate bv expressions and only look at variable values + // because this only gets called when the core theory is complete (i.e. no other bv + // function symbols are currently asserted) + Assert (d_slicer->isCoreTerm(var)); + + Debug("bitvector-model") << "CoreSolver::getModelValue (" << var <<")"; Assert (isComplete()); TNode repr = d_equalityEngine.getRepresentative(var); + Node result = Node(); if (repr.getKind() == kind::CONST_BITVECTOR) { - return repr; - } - if (d_modelValues.find(repr) == d_modelValues.end()) { + result = repr; + } else if (d_modelValues.find(repr) == d_modelValues.end()) { // it may be a shared term that never gets asserted + // result is just Null Assert(d_bv->isSharedTerm(var)); - return Node(); + } else { + result = d_modelValues[repr]; } - return d_modelValues[repr]; + Debug("bitvector-model") << " => " << result <<"\n"; + return result; } CoreSolver::Statistics::Statistics() diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 40093f070..f45250f5b 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -178,13 +178,18 @@ void InequalitySolver::collectModelInfo(TheoryModel* m) { } Node InequalitySolver::getModelValue(TNode var) { + Assert (isInequalityOnly(var)); + Debug("bitvector-model") << "InequalitySolver::getModelValue (" << var <<")"; Assert (isComplete()); + Node result = Node(); if (!d_inequalityGraph.hasValueInModel(var)) { Assert (d_bv->isSharedTerm(var)); - return Node(); + } else { + BitVector val = d_inequalityGraph.getValueInModel(var); + result = utils::mkConst(val); } - BitVector val = d_inequalityGraph.getValueInModel(var); - return utils::mkConst(val); + Debug("bitvector-model") << " => " << result <<"\n"; + return result; } InequalitySolver::Statistics::Statistics() |