Make ExtTheory independent of Theory (#5010)

This makes it so that ExtTheory uses a generic callback instead of relying on Theory.

The primary purpose of this commit is to eliminate the connection of TheoryBV and ExtTheory. This commit moves all things related to ExtTheory in BV into CoreSolver.

It also refactors the use of ExtTheory in strings and arithmetic.

4 files changed, 278 insertions, 215 deletions

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 38c5cb482..b341b0671 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -31,7 +31,65 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
 using namespace CVC4::theory::bv::utils;
 
-CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv, ExtTheory* extt)
+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, TheoryBV* bv)
     : SubtheorySolver(c, bv),
       d_notify(*this),
       d_isComplete(c, true),
@@ -39,9 +97,18 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv, ExtTheory* extt)
       d_preregisterCalled(false),
       d_checkCalled(false),
       d_bv(bv),
-      d_extTheory(extt),
-      d_reasons(c)
+      d_extTheoryCb(),
+      d_extTheory(new ExtTheory(d_extTheoryCb,
+                                bv->getSatContext(),
+                                bv->getUserContext(),
+                                bv->getOutputChannel())),
+      d_reasons(c),
+      d_needsLastCallCheck(false),
+      d_extf_range_infer(bv->getUserContext()),
+      d_extf_collapse_infer(bv->getUserContext())
 {
+  d_extTheory->addFunctionKind(kind::BITVECTOR_TO_NAT);
+  d_extTheory->addFunctionKind(kind::INT_TO_BITVECTOR);
 }
 
 CoreSolver::~CoreSolver() {}
@@ -431,3 +498,141 @@ CoreSolver::Statistics::Statistics()
 CoreSolver::Statistics::~Statistics() {
   smtStatisticsRegistry()->unregisterStat(&d_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();
+  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->getOutputChannel().lemma(lem);
+        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 = nm->mkSkolem(
+                "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->getOutputChannel().lemma(lem);
+          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 381804681..32bc36164 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -31,6 +31,23 @@ 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
  */
@@ -83,8 +100,10 @@ class CoreSolver : public SubtheorySolver {
   TheoryBV* d_bv;
   /** Pointer to the equality engine of the parent */
   eq::EqualityEngine* d_equalityEngine;
-  /** Pointer to the extended theory module. */
-  ExtTheory* d_extTheory;
+  /** 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, NodeHashFunction> d_reasons;
@@ -96,8 +115,38 @@ 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, NodeHashFunction> d_extf_range_infer;
+  context::CDHashSet<Node, NodeHashFunction> 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, TheoryBV* bv, ExtTheory* extt);
+  CoreSolver(context::Context* c, TheoryBV* bv);
   ~CoreSolver();
   bool needsEqualityEngine(EeSetupInfo& esi);
   void finishInit();
@@ -111,9 +160,11 @@ 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.cpp b/src/theory/bv/theory_bv.cpp
index d6492f177..815656d8f 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -29,7 +29,6 @@
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/bv/theory_bv_utils.h"
-#include "theory/ext_theory.h"
 #include "theory/theory_model.h"
 #include "theory/valuation.h"
 
@@ -63,18 +62,12 @@ TheoryBV::TheoryBV(context::Context* c,
       d_invalidateModelCache(c, true),
       d_literalsToPropagate(c),
       d_literalsToPropagateIndex(c, 0),
-      d_extTheory(new ExtTheory(this)),
       d_propagatedBy(c),
       d_eagerSolver(),
       d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
       d_calledPreregister(false),
-      d_needsLastCallCheck(false),
-      d_extf_range_infer(u),
-      d_extf_collapse_infer(u),
       d_state(c, u, valuation)
 {
-  d_extTheory->addFunctionKind(kind::BITVECTOR_TO_NAT);
-  d_extTheory->addFunctionKind(kind::INT_TO_BITVECTOR);
   if (options::bitblastMode() == options::BitblastMode::EAGER)
   {
     d_eagerSolver.reset(new EagerBitblastSolver(c, this));
@@ -83,7 +76,7 @@ TheoryBV::TheoryBV(context::Context* c,
 
   if (options::bitvectorEqualitySolver())
   {
-    d_subtheories.emplace_back(new CoreSolver(c, this, d_extTheory.get()));
+    d_subtheories.emplace_back(new CoreSolver(c, this));
     d_subtheoryMap[SUB_CORE] = d_subtheories.back().get();
   }
 
@@ -331,8 +324,12 @@ void TheoryBV::check(Effort e)
 
   //last call : do reductions on extended bitvector functions
   if (e == Theory::EFFORT_LAST_CALL) {
-    std::vector<Node> nred = d_extTheory->getActive();
-    doExtfReductions(nred);
+    CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+    if (core)
+    {
+      // check extended functions at last call effort
+      core->checkExtf(e);
+    }
     return;
   }
 
@@ -414,131 +411,24 @@ void TheoryBV::check(Effort e)
 
   //check extended functions
   if (Theory::fullEffort(e)) {
-    //do inferences (adds external lemmas)  TODO: this can be improved to add internal inferences
-    std::vector< Node > nred;
-    if (d_extTheory->doInferences(0, nred))
+    CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+    if (core)
     {
-      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;
-      }
+      // check extended functions at full effort
+      core->checkExtf(e);
     }
   }
 }
 
-bool TheoryBV::doExtfInferences(std::vector<Node>& terms)
+bool TheoryBV::needsCheckLastEffort()
 {
-  NodeManager* nm = NodeManager::currentNM();
-  bool sentLemma = false;
-  eq::EqualityEngine* ee = getEqualityEngine();
-  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_out->lemma(lem);
-        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 = nm->mkSkolem(
-                "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_out->lemma(lem);
-          sentLemma = true;
-        }
-      }
-      Trace("bv-extf-lemma-debug")
-          << "BV extf f collapse based on : " << cterm << std::endl;
-    }
-  }
-  return sentLemma;
-}
-
-bool TheoryBV::doExtfReductions( std::vector< Node >& terms ) {
-  std::vector< Node > nredr;
-  if (d_extTheory->doReductions(0, terms, nredr))
+  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+  if (core)
   {
-    return true;
+    return core->needsCheckLastEffort();
   }
-  Assert(nredr.empty());
   return false;
 }
-
-bool TheoryBV::needsCheckLastEffort() {
-  return d_needsLastCallCheck;
-}
 bool TheoryBV::collectModelInfo(TheoryModel* m)
 {
   Assert(!inConflict());
@@ -595,48 +485,6 @@ void TheoryBV::propagate(Effort e) {
   }
 }
 
-bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) {
-  eq::EqualityEngine * ee = getEqualityEngine();
-  if( ee ){
-    //get the constant equivalence classes
-    bool retVal = false;
-    for( unsigned i=0; i<vars.size(); i++ ){
-      Node n = vars[i];
-      if( ee->hasTerm( n ) ){
-        Node nr = ee->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;
-  }
-  return false;
-}
-
-int TheoryBV::getReduction(int effort, Node n, Node& nr)
-{
-  Trace("bv-ext") << "TheoryBV::checkExt : non-reduced : " << n << std::endl;
-  if (n.getKind() == kind::BITVECTOR_TO_NAT)
-  {
-    nr = utils::eliminateBv2Nat(n);
-    return -1;
-  }
-  else if (n.getKind() == kind::INT_TO_BITVECTOR)
-  {
-    nr = utils::eliminateInt2Bv(n);
-    return -1;
-  }
-  return 0;
-}
-
 Theory::PPAssertStatus TheoryBV::ppAssert(TNode in,
                                           SubstitutionMap& outSubstitutions)
 {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 2f63f1a52..7475feccc 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -33,11 +33,7 @@
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
-
 namespace theory {
-
-class ExtTheory;
-
 namespace bv {
 
 class CoreSolver;
@@ -101,12 +97,6 @@ class TheoryBV : public Theory {
 
   std::string identify() const override { return std::string("TheoryBV"); }
 
-  bool getCurrentSubstitution(int effort,
-                              std::vector<Node>& vars,
-                              std::vector<Node>& subs,
-                              std::map<Node, std::vector<Node>>& exp) override;
-  int getReduction(int effort, Node n, Node& nr) override;
-
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
 
   TrustNode ppRewrite(TNode t) override;
@@ -177,9 +167,6 @@ class TheoryBV : public Theory {
   /** Index of the next literal to propagate */
   context::CDO<unsigned> d_literalsToPropagateIndex;
 
-  /** Extended theory module, for context-dependent simplification. */
-  std::unique_ptr<ExtTheory> d_extTheory;
-
   /**
    * Keeps a map from nodes to the subtheory that propagated it so that we can explain it
    * properly.
@@ -191,34 +178,6 @@ class TheoryBV : public Theory {
   std::unique_ptr<AbstractionModule> d_abstractionModule;
   bool d_calledPreregister;
 
-  //for extended functions
-  bool d_needsLastCallCheck;
-  context::CDHashSet<Node, NodeHashFunction> d_extf_range_infer;
-  context::CDHashSet<Node, NodeHashFunction> 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 );
-
   bool wasPropagatedBySubtheory(TNode literal) const {
     return d_propagatedBy.find(literal) != d_propagatedBy.end();
   }