bv: Refactor ppAssert and move to TheoryBV. (#6470)

This PR refactors ppAssert from the lazy BV solver and moves it to TheoryBV.

7 files changed, 91 insertions, 107 deletions

diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h
index 282be6bfc..8ff4318c0 100644
--- a/src/theory/bv/bv_solver.h
+++ b/src/theory/bv/bv_solver.h
@@ -86,9 +86,6 @@ class BVSolver
 
   virtual std::string identify() const = 0;
 
-  virtual Theory::PPAssertStatus ppAssert(
-      TrustNode in, TrustSubstitutionMap& outSubstitutions) = 0;
-
   virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); };
 
   virtual void ppStaticLearn(TNode in, NodeBuilder& learned){};
diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h
index 8d6b8304e..384017f5f 100644
--- a/src/theory/bv/bv_solver_bitblast.h
+++ b/src/theory/bv/bv_solver_bitblast.h
@@ -60,12 +60,6 @@ class BVSolverBitblast : public BVSolver
 
   std::string identify() const override { return "BVSolverBitblast"; };
 
-  Theory::PPAssertStatus ppAssert(
-      TrustNode in, TrustSubstitutionMap& outSubstitutions) override
-  {
-    return Theory::PPAssertStatus::PP_ASSERT_STATUS_UNSOLVED;
-  }
-
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
 
   bool collectModelValues(TheoryModel* m,
diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index a8670e1a6..06ecea701 100644
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -30,7 +30,6 @@
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory_model.h"
-#include "theory/trust_substitutions.h"
 
 using namespace cvc5::theory::bv::utils;
 
@@ -126,8 +125,6 @@ void BVSolverLazy::spendResource(Resource r)
 BVSolverLazy::Statistics::Statistics()
     : d_avgConflictSize(smtStatisticsRegistry().registerAverage(
         "theory::bv::lazy::AvgBVConflictSize")),
-      d_solveSubstitutions(smtStatisticsRegistry().registerInt(
-          "theory::bv::lazy::NumSolveSubstitutions")),
       d_solveTimer(smtStatisticsRegistry().registerTimer(
           "theory::bv::lazy::solveTimer")),
       d_numCallsToCheckFullEffort(smtStatisticsRegistry().registerInt(
@@ -428,89 +425,6 @@ void BVSolverLazy::propagate(Theory::Effort e)
   }
 }
 
-Theory::PPAssertStatus BVSolverLazy::ppAssert(
-    TrustNode tin, TrustSubstitutionMap& outSubstitutions)
-{
-  TNode in = tin.getNode();
-  switch (in.getKind())
-  {
-    case kind::EQUAL:
-    {
-      if (in[0].isVar() && d_bv.isLegalElimination(in[0], in[1]))
-      {
-        ++(d_statistics.d_solveSubstitutions);
-        outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
-        return Theory::PP_ASSERT_STATUS_SOLVED;
-      }
-      if (in[1].isVar() && d_bv.isLegalElimination(in[1], in[0]))
-      {
-        ++(d_statistics.d_solveSubstitutions);
-        outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
-        return Theory::PP_ASSERT_STATUS_SOLVED;
-      }
-      Node node = Rewriter::rewrite(in);
-      if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst())
-          || (node[1].getKind() == kind::BITVECTOR_EXTRACT
-              && node[0].isConst()))
-      {
-        Node extract = node[0].isConst() ? node[1] : node[0];
-        if (extract[0].isVar())
-        {
-          Node c = node[0].isConst() ? node[0] : node[1];
-
-          unsigned high = utils::getExtractHigh(extract);
-          unsigned low = utils::getExtractLow(extract);
-          unsigned var_bitwidth = utils::getSize(extract[0]);
-          std::vector<Node> children;
-
-          if (low == 0)
-          {
-            Assert(high != var_bitwidth - 1);
-            unsigned skolem_size = var_bitwidth - high - 1;
-            Node skolem = utils::mkVar(skolem_size);
-            children.push_back(skolem);
-            children.push_back(c);
-          }
-          else if (high == var_bitwidth - 1)
-          {
-            unsigned skolem_size = low;
-            Node skolem = utils::mkVar(skolem_size);
-            children.push_back(c);
-            children.push_back(skolem);
-          }
-          else
-          {
-            unsigned skolem1_size = low;
-            unsigned skolem2_size = var_bitwidth - high - 1;
-            Node skolem1 = utils::mkVar(skolem1_size);
-            Node skolem2 = utils::mkVar(skolem2_size);
-            children.push_back(skolem2);
-            children.push_back(c);
-            children.push_back(skolem1);
-          }
-          Node concat = utils::mkConcat(children);
-          Assert(utils::getSize(concat) == utils::getSize(extract[0]));
-          if (d_bv.isLegalElimination(extract[0], concat))
-          {
-            outSubstitutions.addSubstitutionSolved(extract[0], concat, tin);
-            return Theory::PP_ASSERT_STATUS_SOLVED;
-          }
-        }
-      }
-    }
-    break;
-    case kind::BITVECTOR_ULT:
-    case kind::BITVECTOR_SLT:
-    case kind::BITVECTOR_ULE:
-    case kind::BITVECTOR_SLE:
-
-    default:
-      // TODO other predicates
-      break;
-  }
-  return Theory::PP_ASSERT_STATUS_UNSOLVED;
-}
-
 TrustNode BVSolverLazy::ppRewrite(TNode t)
 {
   Debug("bv-pp-rewrite") << "BVSolverLazy::ppRewrite " << t << "\n";
diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h
index e11f525f3..57b3e0a08 100644
--- a/src/theory/bv/bv_solver_lazy.h
+++ b/src/theory/bv/bv_solver_lazy.h
@@ -93,9 +93,6 @@ class BVSolverLazy : public BVSolver
 
   std::string identify() const override { return std::string("BVSolverLazy"); }
 
-  Theory::PPAssertStatus ppAssert(
-      TrustNode tin, TrustSubstitutionMap& outSubstitutions) override;
-
   TrustNode ppRewrite(TNode t) override;
 
   void ppStaticLearn(TNode in, NodeBuilder& learned) override;
@@ -112,7 +109,6 @@ class BVSolverLazy : public BVSolver
   {
    public:
     AverageStat d_avgConflictSize;
-    IntStat d_solveSubstitutions;
     TimerStat d_solveTimer;
     IntStat d_numCallsToCheckFullEffort;
     IntStat d_numCallsToCheckStandardEffort;
diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h
index 106a473d9..2c23189db 100644
--- a/src/theory/bv/bv_solver_simple.h
+++ b/src/theory/bv/bv_solver_simple.h
@@ -54,12 +54,6 @@ class BVSolverSimple : public BVSolver
 
   std::string identify() const override { return "BVSolverSimple"; };
 
-  Theory::PPAssertStatus ppAssert(
-      TrustNode in, TrustSubstitutionMap& outSubstitutions) override
-  {
-    return Theory::PPAssertStatus::PP_ASSERT_STATUS_UNSOLVED;
-  }
-
   bool collectModelValues(TheoryModel* m,
                           const std::set<Node>& termSet) override;
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index a0f3f28f7..296fca2c0 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -18,11 +18,13 @@
 #include "expr/proof_checker.h"
 #include "options/bv_options.h"
 #include "options/smt_options.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/bv/bv_solver_bitblast.h"
 #include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/bv_solver_simple.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/ee_setup_info.h"
+#include "theory/trust_substitutions.h"
 
 namespace cvc5 {
 namespace theory {
@@ -40,7 +42,8 @@ TheoryBV::TheoryBV(context::Context* c,
       d_rewriter(),
       d_state(c, u, valuation),
       d_im(*this, d_state, nullptr, "theory::bv::"),
-      d_notify(d_im)
+      d_notify(d_im),
+      d_stats("theory::bv::")
 {
   switch (options::bvSolver())
   {
@@ -182,7 +185,80 @@ void TheoryBV::propagate(Effort e) { return d_internal->propagate(e); }
 Theory::PPAssertStatus TheoryBV::ppAssert(
     TrustNode tin, TrustSubstitutionMap& outSubstitutions)
 {
-  return d_internal->ppAssert(tin, outSubstitutions);
+  TNode in = tin.getNode();
+  Kind k = in.getKind();
+  if (k == kind::EQUAL)
+  {
+    // Substitute variables
+    if (in[0].isVar() && isLegalElimination(in[0], in[1]))
+    {
+      ++d_stats.d_solveSubstitutions;
+      outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
+      return Theory::PP_ASSERT_STATUS_SOLVED;
+    }
+    if (in[1].isVar() && isLegalElimination(in[1], in[0]))
+    {
+      ++d_stats.d_solveSubstitutions;
+      outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
+      return Theory::PP_ASSERT_STATUS_SOLVED;
+    }
+    /**
+     * Eliminate extract over bit-vector variables.
+     *
+     * Given x[h:l] = c, where c is a constant and x is a variable.
+     *
+     * We rewrite to:
+     *
+     * x = sk1::c       if l == 0, where bw(sk1) = bw(x)-1-h
+     * x = c::sk2       if h == bw(x)-1, where bw(sk2) = l
+     * x = sk1::c::sk2  otherwise, where bw(sk1) = bw(x)-1-h and bw(sk2) = l
+     */
+    Node node = Rewriter::rewrite(in);
+    if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst())
+        || (node[1].getKind() == kind::BITVECTOR_EXTRACT
+            && node[0].isConst()))
+    {
+      Node extract = node[0].isConst() ? node[1] : node[0];
+      if (extract[0].isVar())
+      {
+        Node c = node[0].isConst() ? node[0] : node[1];
+
+        uint32_t high = utils::getExtractHigh(extract);
+        uint32_t low = utils::getExtractLow(extract);
+        uint32_t var_bw = utils::getSize(extract[0]);
+        std::vector<Node> children;
+
+        // create sk1 with size bw(x)-1-h
+        if (low == 0 || high != var_bw - 1)
+        {
+          Assert(high != var_bw - 1);
+          uint32_t skolem_size = var_bw - high - 1;
+          Node skolem = utils::mkVar(skolem_size);
+          children.push_back(skolem);
+        }
+
+        children.push_back(c);
+
+        // create sk2 with size l
+        if (high == var_bw - 1 || low != 0)
+        {
+          Assert(low != 0);
+          uint32_t skolem_size = low;
+          Node skolem = utils::mkVar(skolem_size);
+          children.push_back(skolem);
+        }
+
+        Node concat = utils::mkConcat(children);
+        Assert(utils::getSize(concat) == utils::getSize(extract[0]));
+        if (isLegalElimination(extract[0], concat))
+        {
+          outSubstitutions.addSubstitutionSolved(extract[0], concat, tin);
+          return Theory::PP_ASSERT_STATUS_SOLVED;
+        }
+      }
+    }
+  }
+  return Theory::PP_ASSERT_STATUS_UNSOLVED;
 }
 
 TrustNode TheoryBV::ppRewrite(TNode t, std::vector<SkolemLemma>& lems)
@@ -221,6 +297,12 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions,
   return d_internal->applyAbstraction(assertions, new_assertions);
 }
 
+TheoryBV::Statistics::Statistics(const std::string& name)
+    : d_solveSubstitutions(
+        smtStatisticsRegistry().registerInt(name + "NumSolveSubstitutions"))
+{
+}
+
 }  // namespace bv
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 1f14f05b0..4b3a1f3b2 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -122,6 +122,13 @@ class TheoryBV : public Theory
   /** The notify class for equality engine. */
   TheoryEqNotifyClass d_notify;
 
+  /** TheoryBV statistics. */
+  struct Statistics
+  {
+    Statistics(const std::string& name);
+    IntStat d_solveSubstitutions;
+  } d_stats;
+
 }; /* class TheoryBV */
 
 }  // namespace bv