7 files changed, 22 insertions, 63 deletions
diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp
index 008e9c015..4b0c17bee 100644
--- a/src/theory/datatypes/sygus_datatype_utils.cpp
+++ b/src/theory/datatypes/sygus_datatype_utils.cpp
@@ -21,6 +21,7 @@
 #include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "expr/sygus_datatype.h"
+#include "smt/env.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/evaluator.h"
@@ -138,60 +139,6 @@ Kind getEliminateKind(Kind ok)
   return nk;
 }
 
-Node eliminatePartialOperators(Node n)
-{
-  NodeManager* nm = NodeManager::currentNM();
-  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
-  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
-  std::vector<TNode> visit;
-  TNode cur;
-  visit.push_back(n);
-  do
-  {
-    cur = visit.back();
-    visit.pop_back();
-    it = visited.find(cur);
-
-    if (it == visited.end())
-    {
-      visited[cur] = Node::null();
-      visit.push_back(cur);
-      for (const Node& cn : cur)
-      {
-        visit.push_back(cn);
-      }
-    }
-    else if (it->second.isNull())
-    {
-      Node ret = cur;
-      bool childChanged = false;
-      std::vector<Node> children;
-      if (cur.getMetaKind() == metakind::PARAMETERIZED)
-      {
-        children.push_back(cur.getOperator());
-      }
-      for (const Node& cn : cur)
-      {
-        it = visited.find(cn);
-        Assert(it != visited.end());
-        Assert(!it->second.isNull());
-        childChanged = childChanged || cn != it->second;
-        children.push_back(it->second);
-      }
-      Kind ok = cur.getKind();
-      Kind nk = getEliminateKind(ok);
-      if (nk != ok || childChanged)
-      {
-        ret = nm->mkNode(nk, children);
-      }
-      visited[cur] = ret;
-    }
-  } while (!visit.empty());
-  Assert(visited.find(n) != visited.end());
-  Assert(!visited.find(n)->second.isNull());
-  return visited[n];
-}
-
 Node mkSygusTerm(const DType& dt,
                  unsigned i,
                  const std::vector<Node>& children,
@@ -235,7 +182,6 @@ Node mkSygusTerm(const DType& dt,
         // expandDefinitions.
         opn = smt::currentSmtEngine()->expandDefinitions(op);
         opn = Rewriter::rewrite(opn);
-        opn = eliminatePartialOperators(opn);
         SygusOpRewrittenAttribute sora;
         op.setAttribute(sora, opn);
       }
diff --git a/src/theory/datatypes/sygus_datatype_utils.h b/src/theory/datatypes/sygus_datatype_utils.h
index 77aa7ac54..63e8a057a 100644
--- a/src/theory/datatypes/sygus_datatype_utils.h
+++ b/src/theory/datatypes/sygus_datatype_utils.h
@@ -86,11 +86,6 @@ Kind getOperatorKindForSygusBuiltin(Node op);
  * otherwise k itself.
  */
 Kind getEliminateKind(Kind k);
-/**
- * Returns a version of n where all partial functions such as bvudiv
- * have been replaced by their total versions like bvudiv_total.
- */
-Node eliminatePartialOperators(Node n);
 /** make sygus term
  *
  * This function returns a builtin term f( children[0], ..., children[n] )
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 93ef072fa..5295302c4 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -289,7 +289,10 @@ CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersState& qs,
 {
   Trace("sel-trigger") << "Selector trigger: " << mpat << std::endl;
   Assert(mpat.getKind() == APPLY_SELECTOR);
-  Node mpatExp = smt::currentSmtEngine()->expandDefinitions(mpat, false);
+  // NOTE: could use qs.getValuation().getPreprocessedTerm(mpat); when
+  // expand definitions is eliminated, however, this also requires avoiding
+  // term formula removal.
+  Node mpatExp = smt::currentSmtEngine()->expandDefinitions(mpat);
   Trace("sel-trigger") << "Expands to: " << mpatExp << std::endl;
   if (mpatExp.getKind() == ITE)
   {
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 5cea6592c..2b2604593 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -179,6 +179,11 @@ void Rewriter::registerPostRewriteEqual(
   d_postRewritersEqual[tid] = fn;
 }
 
+TheoryRewriter* Rewriter::getTheoryRewriter(theory::TheoryId theoryId)
+{
+  return d_theoryRewriters[theoryId];
+}
+
 Rewriter* Rewriter::getInstance()
 {
   return smt::currentSmtEngine()->getRewriter();
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index 3f4676fa0..b3ea3b542 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -147,6 +147,9 @@ class Rewriter {
       theory::TheoryId tid,
       std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
 
+  /** Get the theory rewriter for the given id */
+  TheoryRewriter* getTheoryRewriter(theory::TheoryId theoryId);
+
  private:
   /**
    * Get the rewriter associated with the SmtEngine in scope.
diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp
index 47507bfe0..7a2fb19bd 100644
--- a/src/theory/trust_substitutions.cpp
+++ b/src/theory/trust_substitutions.cpp
@@ -146,7 +146,7 @@ void TrustSubstitutionMap::addSubstitutions(TrustSubstitutionMap& t)
   }
 }
 
-TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite)
+TrustNode TrustSubstitutionMap::applyTrusted(Node n, bool doRewrite)
 {
   Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: apply " << n
                       << std::endl;
@@ -169,6 +169,11 @@ TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite)
   return TrustNode::mkTrustRewrite(n, ns, this);
 }
 
+Node TrustSubstitutionMap::apply(Node n, bool doRewrite)
+{
+  return d_subs.apply(n, doRewrite);
+}
+
 std::shared_ptr<ProofNode> TrustSubstitutionMap::getProofFor(Node eq)
 {
   Assert(eq.getKind() == kind::EQUAL);
diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h
index ec5b2ffb5..b7b526205 100644
--- a/src/theory/trust_substitutions.h
+++ b/src/theory/trust_substitutions.h
@@ -89,7 +89,9 @@ class TrustSubstitutionMap : public ProofGenerator
    * proving n = n*sigma, where the proof generator is provided by this class
    * (when proofs are enabled).
    */
-  TrustNode apply(Node n, bool doRewrite = true);
+  TrustNode applyTrusted(Node n, bool doRewrite = true);
+  /** Same as above, without proofs */
+  Node apply(Node n, bool doRewrite = true);
 
   /** Get the proof for formula f */
   std::shared_ptr<ProofNode> getProofFor(Node f) override;