Move expand definition from Theory to TheoryRewriter (#6408)

This is work towards eliminating global calls to getCurrentSmtEngine()->expandDefinition.

The next step will be to add Rewriter::expandDefinition.

1 files changed, 12 insertions, 0 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 83aaaadd8..b8135127d 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -26,6 +26,7 @@
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/normal_form.h"
+#include "theory/arith/operator_elim.h"
 #include "theory/theory.h"
 #include "util/iand.h"
 
@@ -33,6 +34,8 @@ namespace cvc5 {
 namespace theory {
 namespace arith {
 
+ArithRewriter::ArithRewriter(OperatorElim& oe) : d_opElim(oe) {}
+
 bool ArithRewriter::isAtom(TNode n) {
   Kind k = n.getKind();
   return arith::isRelationOperator(k) || k == kind::IS_INTEGER
@@ -893,6 +896,15 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre)
   return RewriteResponse(REWRITE_DONE, t);
 }
 
+TrustNode ArithRewriter::expandDefinition(Node node)
+{
+  // call eliminate operators, to eliminate partial operators only
+  std::vector<SkolemLemma> lems;
+  TrustNode ret = d_opElim.eliminate(node, lems, true);
+  Assert(lems.empty());
+  return ret;
+}
+
 RewriteResponse ArithRewriter::returnRewrite(TNode t, Node ret, Rewrite r)
 {
   Trace("arith-rewrite") << "ArithRewriter : " << t << " == " << ret << " by "