diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-07-28 14:11:55 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-07-28 14:11:55 -0700 |
commit | 1377cede4b223a5b6a68d7d9194b7e3346a2d51a (patch) | |
tree | face9b6f6b46f663a38115c6ca11fb7415acbd10 /src/theory/bv/theory_bv.cpp | |
parent | 5067dee413caf5f5bda4e666d877841f936d74b0 (diff) | |
parent | e6747735d2074fc2651c5edc11fa8170fc13663e (diff) |
Merge branch 'master' into docsLinkdocsLink
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 103 |
1 files changed, 101 insertions, 2 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 37881f9b2..547d24b23 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -43,6 +43,7 @@ TheoryBV::TheoryBV(context::Context* c, d_state(c, u, valuation), d_im(*this, d_state, nullptr, "theory::bv::"), d_notify(d_im), + d_invalidateModelCache(c, true), d_stats("theory::bv::") { switch (options::bvSolver()) @@ -158,7 +159,11 @@ void TheoryBV::preRegisterTerm(TNode node) bool TheoryBV::preCheck(Effort e) { return d_internal->preCheck(e); } -void TheoryBV::postCheck(Effort e) { d_internal->postCheck(e); } +void TheoryBV::postCheck(Effort e) +{ + d_invalidateModelCache = true; + d_internal->postCheck(e); +} bool TheoryBV::preNotifyFact( TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) @@ -282,7 +287,27 @@ void TheoryBV::presolve() { d_internal->presolve(); } EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) { - return d_internal->getEqualityStatus(a, b); + EqualityStatus status = d_internal->getEqualityStatus(a, b); + + if (status == EqualityStatus::EQUALITY_UNKNOWN) + { + Node value_a = getValue(a); + Node value_b = getValue(b); + + if (value_a.isNull() || value_b.isNull()) + { + return status; + } + + if (value_a == value_b) + { + Debug("theory-bv") << EQUALITY_TRUE_IN_MODEL << std::endl; + return EQUALITY_TRUE_IN_MODEL; + } + Debug("theory-bv") << EQUALITY_FALSE_IN_MODEL << std::endl; + return EQUALITY_FALSE_IN_MODEL; + } + return status; } TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); } @@ -303,6 +328,80 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, return d_internal->applyAbstraction(assertions, new_assertions); } +Node TheoryBV::getValue(TNode node) +{ + if (d_invalidateModelCache.get()) + { + d_modelCache.clear(); + } + d_invalidateModelCache.set(false); + + std::vector<TNode> visit; + + TNode cur; + visit.push_back(node); + do + { + cur = visit.back(); + visit.pop_back(); + + auto it = d_modelCache.find(cur); + if (it != d_modelCache.end() && !it->second.isNull()) + { + continue; + } + + if (cur.isConst()) + { + d_modelCache[cur] = cur; + continue; + } + + Node value = d_internal->getValue(cur, false); + if (value.isConst()) + { + d_modelCache[cur] = value; + continue; + } + + if (Theory::isLeafOf(cur, theory::THEORY_BV)) + { + value = d_internal->getValue(cur, true); + d_modelCache[cur] = value; + continue; + } + + if (it == d_modelCache.end()) + { + visit.push_back(cur); + d_modelCache.emplace(cur, Node()); + visit.insert(visit.end(), cur.begin(), cur.end()); + } + else if (it->second.isNull()) + { + NodeBuilder nb(cur.getKind()); + if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) + { + nb << cur.getOperator(); + } + + std::unordered_map<Node, Node>::iterator iit; + for (const TNode& child : cur) + { + iit = d_modelCache.find(child); + Assert(iit != d_modelCache.end()); + Assert(iit->second.isConst()); + nb << iit->second; + } + it->second = Rewriter::rewrite(nb.constructNode()); + } + } while (!visit.empty()); + + auto it = d_modelCache.find(node); + Assert(it != d_modelCache.end()); + return it->second; +} + TheoryBV::Statistics::Statistics(const std::string& name) : d_solveSubstitutions( smtStatisticsRegistry().registerInt(name + "NumSolveSubstitutions")) |