Remove support for lazy BV extended function reductions and inferences (#6728)

solve-int-as-bv is now the preferred method for solving these benchmarks.

Adds solve-int-as-bv to a regression that became slow in my previous commit.

8 files changed, 11 insertions, 356 deletions

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index fcad51ceb..8d4c2b1de 100644
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -191,22 +191,6 @@ name   = "Bitvector Theory"
   help       = "simplify formula via Gaussian Elimination if applicable"
 
 [[option]]
-  name       = "bvLazyRewriteExtf"
-  category   = "regular"
-  long       = "bv-lazy-rewrite-extf"
-  type       = "bool"
-  default    = "true"
-  help       = "lazily rewrite extended functions like bv2nat and int2bv"
-
-[[option]]
-  name       = "bvLazyReduceExtf"
-  category   = "regular"
-  long       = "bv-lazy-reduce-extf"
-  type       = "bool"
-  default    = "false"
-  help       = "reduce extended functions like bv2nat and int2bv at last call instead of full effort"
-
-[[option]]
   name       = "bvAlgExtf"
   category   = "regular"
   long       = "bv-alg-extf"
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 31d14c569..67c5c5647 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -189,8 +189,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 
   if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
   {
-    // do not rewrite bv2nat eagerly
-    opts.bv.bvLazyRewriteExtf = true;
     if (options::boolToBitvector() != options::BoolToBVMode::OFF)
     {
       throw OptionException(
@@ -215,14 +213,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       logic.lock();
     }
   }
-  else if (options::bvSolver() == options::BVSolver::SIMPLE
-           || options::bvSolver() == options::BVSolver::BITBLAST)
-  {
-    // Only BVSolver::LAZY natively supports int2bv and nat2bv, for other
-    // solvers we need to eagerly eliminate the operators. Note this is only
-    // applied if we are not eliminating BV (e.g. with solveBVAsInt).
-    opts.bv.bvLazyReduceExtf = false;
-  }
 
   // set options about ackermannization
   if (options::ackermann() && options::produceModels()
@@ -1401,22 +1391,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     opts.arrays.arraysOptimizeLinear = false;
   }
 
-  if (!options::bitvectorEqualitySolver())
-  {
-    if (options::bvLazyRewriteExtf())
-    {
-      if (opts.bv.bvLazyRewriteExtfWasSetByUser)
-      {
-        throw OptionException(
-            "--bv-lazy-rewrite-extf requires --bv-eq-solver to be set");
-      }
-    }
-    Trace("smt")
-        << "disabling bvLazyRewriteExtf since equality solver is disabled"
-        << std::endl;
-    opts.bv.bvLazyRewriteExtf = false;
-  }
-
   if (options::stringFMF() && !opts.strings.stringProcessLoopModeWasSetByUser)
   {
     Trace("smt") << "settting stringProcessLoopMode to 'simple' since "
diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index fbd910bee..5210117b8 100644
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -233,18 +233,6 @@ void BVSolverLazy::check(Theory::Effort e)
     return;
   }
 
-  // last call : do reductions on extended bitvector functions
-  if (e == Theory::EFFORT_LAST_CALL)
-  {
-    CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
-    if (core)
-    {
-      // check extended functions at last call effort
-      core->checkExtf(e);
-    }
-    return;
-  }
-
   Debug("bitvector") << "BVSolverLazy::check(" << e << ")" << std::endl;
   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
   // we may be getting new assertions so the model cache may not be sound
@@ -331,27 +319,6 @@ void BVSolverLazy::check(Theory::Effort e)
       break;
     }
   }
-
-  // check extended functions
-  if (Theory::fullEffort(e))
-  {
-    CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
-    if (core)
-    {
-      // check extended functions at full effort
-      core->checkExtf(e);
-    }
-  }
-}
-
-bool BVSolverLazy::needsCheckLastEffort()
-{
-  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
-  if (core)
-  {
-    return core->needsCheckLastEffort();
-  }
-  return false;
 }
 
 bool BVSolverLazy::collectModelValues(TheoryModel* m,
diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h
index 9b3a2f1fa..4f73354bc 100644
--- a/src/theory/bv/bv_solver_lazy.h
+++ b/src/theory/bv/bv_solver_lazy.h
@@ -82,8 +82,6 @@ class BVSolverLazy : public BVSolver
 
   bool preCheck(Theory::Effort e) override;
 
-  bool needsCheckLastEffort() override;
-
   void propagate(Theory::Effort e) override;
 
   TrustNode explain(TNode n) override;
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 2589418cc..fa71641ad 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -32,64 +32,6 @@ using namespace cvc5::theory;
 using namespace cvc5::theory::bv;
 using namespace cvc5::theory::bv::utils;
 
-bool CoreSolverExtTheoryCallback::getCurrentSubstitution(
-    int effort,
-    const std::vector<Node>& vars,
-    std::vector<Node>& subs,
-    std::map<Node, std::vector<Node> >& exp)
-{
-  if (d_equalityEngine == nullptr)
-  {
-    return false;
-  }
-  // get the constant equivalence classes
-  bool retVal = false;
-  for (const Node& n : vars)
-  {
-    if (d_equalityEngine->hasTerm(n))
-    {
-      Node nr = d_equalityEngine->getRepresentative(n);
-      if (nr.isConst())
-      {
-        subs.push_back(nr);
-        exp[n].push_back(n.eqNode(nr));
-        retVal = true;
-      }
-      else
-      {
-        subs.push_back(n);
-      }
-    }
-    else
-    {
-      subs.push_back(n);
-    }
-  }
-  // return true if the substitution is non-trivial
-  return retVal;
-}
-
-bool CoreSolverExtTheoryCallback::getReduction(int effort,
-                                               Node n,
-                                               Node& nr,
-                                               bool& satDep)
-{
-  Trace("bv-ext") << "TheoryBV::checkExt : non-reduced : " << n << std::endl;
-  if (n.getKind() == kind::BITVECTOR_TO_NAT)
-  {
-    nr = utils::eliminateBv2Nat(n);
-    satDep = false;
-    return true;
-  }
-  else if (n.getKind() == kind::INT_TO_BITVECTOR)
-  {
-    nr = utils::eliminateInt2Bv(n);
-    satDep = false;
-    return true;
-  }
-  return false;
-}
-
 CoreSolver::CoreSolver(context::Context* c, BVSolverLazy* bv)
     : SubtheorySolver(c, bv),
       d_notify(*this),
@@ -98,18 +40,8 @@ CoreSolver::CoreSolver(context::Context* c, BVSolverLazy* bv)
       d_preregisterCalled(false),
       d_checkCalled(false),
       d_bv(bv),
-      d_extTheoryCb(),
-      d_extTheory(new ExtTheory(d_extTheoryCb,
-                                bv->d_bv.getSatContext(),
-                                bv->d_bv.getUserContext(),
-                                bv->d_bv.getOutputChannel())),
-      d_reasons(c),
-      d_needsLastCallCheck(false),
-      d_extf_range_infer(bv->d_bv.getUserContext()),
-      d_extf_collapse_infer(bv->d_bv.getUserContext())
+      d_reasons(c)
 {
-  d_extTheory->addFunctionKind(kind::BITVECTOR_TO_NAT);
-  d_extTheory->addFunctionKind(kind::INT_TO_BITVECTOR);
 }
 
 CoreSolver::~CoreSolver() {}
@@ -167,11 +99,6 @@ void CoreSolver::preRegister(TNode node) {
     d_equalityEngine->addTriggerPredicate(node);
   } else {
     d_equalityEngine->addTerm(node);
-    // Register with the extended theory, for context-dependent simplification.
-    // Notice we do this for registered terms but not internally generated
-    // equivalence classes. The two should roughly cooincide. Since ExtTheory is
-    // being used as a heuristic, it is good enough to be registered here.
-    d_extTheory->registerTerm(node);
   }
 }
 
@@ -489,142 +416,3 @@ CoreSolver::Statistics::Statistics()
         "theory::bv::CoreSolver::NumCallsToCheck"))
 {
 }
-
-void CoreSolver::checkExtf(Theory::Effort e)
-{
-  if (e == Theory::EFFORT_LAST_CALL)
-  {
-    std::vector<Node> nred = d_extTheory->getActive();
-    doExtfReductions(nred);
-  }
-  Assert(e == Theory::EFFORT_FULL);
-  // do inferences (adds external lemmas)  TODO: this can be improved to add
-  // internal inferences
-  std::vector<Node> nred;
-  if (d_extTheory->doInferences(0, nred))
-  {
-    return;
-  }
-  d_needsLastCallCheck = false;
-  if (!nred.empty())
-  {
-    // other inferences involving bv2nat, int2bv
-    if (options::bvAlgExtf())
-    {
-      if (doExtfInferences(nred))
-      {
-        return;
-      }
-    }
-    if (!options::bvLazyReduceExtf())
-    {
-      if (doExtfReductions(nred))
-      {
-        return;
-      }
-    }
-    else
-    {
-      d_needsLastCallCheck = true;
-    }
-  }
-}
-
-bool CoreSolver::needsCheckLastEffort() const { return d_needsLastCallCheck; }
-
-bool CoreSolver::doExtfInferences(std::vector<Node>& terms)
-{
-  NodeManager* nm = NodeManager::currentNM();
-  SkolemManager* sm = nm->getSkolemManager();
-  bool sentLemma = false;
-  eq::EqualityEngine* ee = d_equalityEngine;
-  std::map<Node, Node> op_map;
-  for (unsigned j = 0; j < terms.size(); j++)
-  {
-    TNode n = terms[j];
-    Assert(n.getKind() == kind::BITVECTOR_TO_NAT
-           || n.getKind() == kind::INT_TO_BITVECTOR);
-    if (n.getKind() == kind::BITVECTOR_TO_NAT)
-    {
-      // range lemmas
-      if (d_extf_range_infer.find(n) == d_extf_range_infer.end())
-      {
-        d_extf_range_infer.insert(n);
-        unsigned bvs = n[0].getType().getBitVectorSize();
-        Node min = nm->mkConst(Rational(0));
-        Node max = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
-        Node lem = nm->mkNode(kind::AND,
-                              nm->mkNode(kind::GEQ, n, min),
-                              nm->mkNode(kind::LT, n, max));
-        Trace("bv-extf-lemma")
-            << "BV extf lemma (range) : " << lem << std::endl;
-        d_bv->d_im.lemma(lem, InferenceId::BV_EXTF_LEMMA);
-        sentLemma = true;
-      }
-    }
-    Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n[0]) : n[0];
-    op_map[r] = n;
-  }
-  for (unsigned j = 0; j < terms.size(); j++)
-  {
-    TNode n = terms[j];
-    Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n) : n;
-    std::map<Node, Node>::iterator it = op_map.find(r);
-    if (it != op_map.end())
-    {
-      Node parent = it->second;
-      // Node cterm = parent[0]==n ? parent : nm->mkNode( parent.getOperator(),
-      // n );
-      Node cterm = parent[0].eqNode(n);
-      Trace("bv-extf-lemma-debug")
-          << "BV extf collapse based on : " << cterm << std::endl;
-      if (d_extf_collapse_infer.find(cterm) == d_extf_collapse_infer.end())
-      {
-        d_extf_collapse_infer.insert(cterm);
-
-        Node t = n[0];
-        if (t.getType() == parent.getType())
-        {
-          if (n.getKind() == kind::INT_TO_BITVECTOR)
-          {
-            Assert(t.getType().isInteger());
-            // congruent modulo 2^( bv width )
-            unsigned bvs = n.getType().getBitVectorSize();
-            Node coeff = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
-            Node k = sm->mkDummySkolem(
-                "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence");
-            t = nm->mkNode(kind::PLUS, t, nm->mkNode(kind::MULT, coeff, k));
-          }
-          Node lem = parent.eqNode(t);
-
-          if (parent[0] != n)
-          {
-            Assert(ee->areEqual(parent[0], n));
-            lem = nm->mkNode(kind::IMPLIES, parent[0].eqNode(n), lem);
-          }
-          // this handles inferences of the form, e.g.:
-          //   ((_ int2bv w) (bv2nat x)) == x (if x is bit-width w)
-          //   (bv2nat ((_ int2bv w) x)) == x + k*2^w for some k
-          Trace("bv-extf-lemma")
-              << "BV extf lemma (collapse) : " << lem << std::endl;
-          d_bv->d_im.lemma(lem, InferenceId::BV_EXTF_COLLAPSE);
-          sentLemma = true;
-        }
-      }
-      Trace("bv-extf-lemma-debug")
-          << "BV extf f collapse based on : " << cterm << std::endl;
-    }
-  }
-  return sentLemma;
-}
-
-bool CoreSolver::doExtfReductions(std::vector<Node>& terms)
-{
-  std::vector<Node> nredr;
-  if (d_extTheory->doReductions(0, terms, nredr))
-  {
-    return true;
-  }
-  Assert(nredr.empty());
-  return false;
-}
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 0dfcfdde4..46c4559ea 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -22,30 +22,11 @@
 
 #include "context/cdhashset.h"
 #include "theory/bv/bv_subtheory.h"
-#include "theory/ext_theory.h"
 
 namespace cvc5 {
 namespace theory {
 namespace bv {
 
-class Base;
-
-/** An extended theory callback used by the core solver */
-class CoreSolverExtTheoryCallback : public ExtTheoryCallback
-{
- public:
-  CoreSolverExtTheoryCallback() : d_equalityEngine(nullptr) {}
-  /** Get current substitution based on the underlying equality engine. */
-  bool getCurrentSubstitution(int effort,
-                              const std::vector<Node>& vars,
-                              std::vector<Node>& subs,
-                              std::map<Node, std::vector<Node> >& exp) override;
-  /** Get reduction. */
-  bool getReduction(int effort, Node n, Node& nr, bool& satDep) override;
-  /** The underlying equality engine */
-  eq::EqualityEngine* d_equalityEngine;
-};
-
 /**
  * Bitvector equality solver
  */
@@ -96,10 +77,6 @@ class CoreSolver : public SubtheorySolver {
   BVSolverLazy* d_bv;
   /** Pointer to the equality engine of the parent */
   eq::EqualityEngine* d_equalityEngine;
-  /** The extended theory callback */
-  CoreSolverExtTheoryCallback d_extTheoryCb;
-  /** Extended theory module, for context-dependent simplification. */
-  std::unique_ptr<ExtTheory> d_extTheory;
 
   /** To make sure we keep the explanations */
   context::CDHashSet<Node> d_reasons;
@@ -109,36 +86,6 @@ class CoreSolver : public SubtheorySolver {
   bool isCompleteForTerm(TNode term, TNodeBoolMap& seen);
   Statistics d_statistics;
 
-  /** Whether we need a last call effort check */
-  bool d_needsLastCallCheck;
-  /** For extended functions */
-  context::CDHashSet<Node> d_extf_range_infer;
-  context::CDHashSet<Node> d_extf_collapse_infer;
-
-  /** do extended function inferences
-   *
-   * This method adds lemmas on the output channel of TheoryBV based on
-   * reasoning about extended functions, such as bv2nat and int2bv. Examples
-   * of lemmas added by this method include:
-   *   0 <= ((_ int2bv w) x) < 2^w
-   *   ((_ int2bv w) (bv2nat x)) = x
-   *   (bv2nat ((_ int2bv w) x)) == x + k*2^w
-   * The purpose of these lemmas is to recognize easy conflicts before fully
-   * reducing extended functions based on their full semantics.
-   */
-  bool doExtfInferences(std::vector<Node>& terms);
-  /** do extended function reductions
-   *
-   * This method adds lemmas on the output channel of TheoryBV based on
-   * reducing all extended function applications that are preregistered to
-   * this theory and have not already been reduced by context-dependent
-   * simplification (see theory/ext_theory.h). Examples of lemmas added by
-   * this method include:
-   *   (bv2nat x) = (ite ((_ extract w w-1) x) 2^{w-1} 0) + ... +
-   *                (ite ((_ extract 1 0) x) 1 0)
-   */
-  bool doExtfReductions(std::vector<Node>& terms);
-
  public:
   CoreSolver(context::Context* c, BVSolverLazy* bv);
   ~CoreSolver();
@@ -154,9 +101,6 @@ class CoreSolver : public SubtheorySolver {
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
   bool hasTerm(TNode node) const;
   void addTermToEqualityEngine(TNode node);
-  /** check extended functions at the given effort */
-  void checkExtf(Theory::Effort e);
-  bool needsCheckLastEffort() const;
 };
 
 }
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 4e1076763..97ca24437 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -65,16 +65,14 @@ TrustNode TheoryBVRewriter::expandDefinition(Node node)
     case kind::BITVECTOR_SREM:
     case kind::BITVECTOR_SMOD: ret = eliminateBVSDiv(node); break;
     case kind::BITVECTOR_TO_NAT:
-      if (!options::bvLazyReduceExtf())
-      {
+
         ret = utils::eliminateBv2Nat(node);
-      }
+      
       break;
     case kind::INT_TO_BITVECTOR:
-      if (!options::bvLazyReduceExtf())
-      {
+
         ret = utils::eliminateInt2Bv(node);
-      }
+      
       break;
     default: break;
   }
@@ -646,8 +644,8 @@ RewriteResponse TheoryBVRewriter::RewriteRedand(TNode node, bool prerewrite){
 }
 
 RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) {
-  //do not use lazy rewrite strategy if equality solver is disabled
-  if( node[0].isConst() || !options::bvLazyRewriteExtf() ){
+  if (node[0].isConst())
+  {
     Node resultNode = LinearRewriteStrategy
       < RewriteRule<BVToNatEliminate>
       >::apply(node);
@@ -658,8 +656,8 @@ RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) {
 }
 
 RewriteResponse TheoryBVRewriter::RewriteIntToBV(TNode node, bool prerewrite) {
-  //do not use lazy rewrite strategy if equality solver is disabled
-  if( node[0].isConst() || !options::bvLazyRewriteExtf() ){
+  if (node[0].isConst())
+  {
     Node resultNode = LinearRewriteStrategy
       < RewriteRule<IntToBVEliminate>
       >::apply(node);
diff --git a/test/regress/regress1/bv/bv2nat-simp-range-sat.smt2 b/test/regress/regress1/bv/bv2nat-simp-range-sat.smt2
index 9da8d4ca8..66b286da1 100644
--- a/test/regress/regress1/bv/bv2nat-simp-range-sat.smt2
+++ b/test/regress/regress1/bv/bv2nat-simp-range-sat.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --solve-bv-as-int=sum
+; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
 (declare-fun t () (_ BitVec 16))