From 56b5ebfed26283db73c55bbcc9391d2e06897727 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Tue, 27 Jul 2021 13:23:32 -0700
Subject: bv: Refactor getEqualityStatus and use for both bitblasting solvers.
 (#6933)

This commit refactors the getEqualityStatus handling for bitblast and bitblast-internal.
---
 src/theory/bv/theory_bv.cpp | 103 +++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 101 insertions(+), 2 deletions(-)

(limited to 'src/theory/bv/theory_bv.cpp')

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"))
-- 
cgit v1.2.3