Decouple modules from TheoryArithPrivate (#5184)

This decouples the arithmetic rewriter, the operator eliminator and the non-linear extension from TheoryArithPrivate and performs some minor cleanup.

This is in preparation for further refactoring of (lazy) arithmetic operator elimination.

1 files changed, 63 insertions, 8 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 93c8d87fc..434d2e1c8 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -44,7 +44,8 @@ TheoryArith::TheoryArith(context::Context* c,
       d_ppRewriteTimer("theory::arith::ppRewriteTimer"),
       d_astate(*d_internal, c, u, valuation),
       d_inferenceManager(*this, d_astate, pnm),
-      d_nonlinearExtension(nullptr)
+      d_nonlinearExtension(nullptr),
+      d_opElim(pnm, logicInfo)
 {
   smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
 
@@ -58,10 +59,7 @@ TheoryArith::~TheoryArith(){
   delete d_internal;
 }
 
-TheoryRewriter* TheoryArith::getTheoryRewriter()
-{
-  return d_internal->getTheoryRewriter();
-}
+TheoryRewriter* TheoryArith::getTheoryRewriter() { return &d_rewriter; }
 
 bool TheoryArith::needsEqualityEngine(EeSetupInfo& esi)
 {
@@ -101,7 +99,8 @@ void TheoryArith::preRegisterTerm(TNode n)
 
 TrustNode TheoryArith::expandDefinition(Node node)
 {
-  return d_internal->expandDefinition(node);
+  // call eliminate operators
+  return d_opElim.eliminate(node);
 }
 
 void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); }
@@ -109,7 +108,46 @@ void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); }
 TrustNode TheoryArith::ppRewrite(TNode atom)
 {
   CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true);
-  return d_internal->ppRewrite(atom);
+  Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
+
+  if (options::arithRewriteEq())
+  {
+    if (atom.getKind() == kind::EQUAL && atom[0].getType().isReal())
+    {
+      Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
+      Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
+      TrustNode tleq = ppRewriteTerms(leq);
+      TrustNode tgeq = ppRewriteTerms(geq);
+      if (!tleq.isNull())
+      {
+        leq = tleq.getNode();
+      }
+      if (!tgeq.isNull())
+      {
+        geq = tgeq.getNode();
+      }
+      Node rewritten = Rewriter::rewrite(leq.andNode(geq));
+      Debug("arith::preprocess")
+          << "arith::preprocess() : returning " << rewritten << endl;
+      // don't need to rewrite terms since rewritten is not a non-standard op
+      return TrustNode::mkTrustRewrite(atom, rewritten, nullptr);
+    }
+  }
+  return ppRewriteTerms(atom);
+}
+
+TrustNode TheoryArith::ppRewriteTerms(TNode n)
+{
+  if (Theory::theoryOf(n) != THEORY_ARITH)
+  {
+    return TrustNode::null();
+  }
+  // Eliminate operators recursively. Notice we must do this here since other
+  // theories may generate lemmas that involve non-standard operators. For
+  // example, quantifier instantiation may use TO_INTEGER terms; SyGuS may
+  // introduce non-standard arithmetic terms appearing in grammars.
+  // call eliminate operators
+  return d_opElim.eliminate(n);
 }
 
 Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
@@ -134,7 +172,24 @@ void TheoryArith::postCheck(Effort level)
     return;
   }
   // otherwise, check with the linear solver
-  d_internal->postCheck(level);
+  if (d_internal->postCheck(level))
+  {
+    // linear solver emitted a conflict or lemma, return
+    return;
+  }
+
+  if (Theory::fullEffort(level))
+  {
+    if (d_nonlinearExtension != nullptr)
+    {
+      d_nonlinearExtension->check(level);
+    }
+    else if (d_internal->foundNonlinear())
+    {
+      // set incomplete
+      d_inferenceManager.setIncomplete();
+    }
+  }
 }
 
 bool TheoryArith::preNotifyFact(