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.

8 files changed, 115 insertions, 167 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 7c22b880a..3ca20e8dc 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -395,7 +395,6 @@ libcvc4_add_sources(
   theory/arith/theory_arith.h
   theory/arith/theory_arith_private.cpp
   theory/arith/theory_arith_private.h
-  theory/arith/theory_arith_private_forward.h
   theory/arith/theory_arith_type_rules.h
   theory/arith/type_enumerator.h
   theory/arrays/array_info.cpp
diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
index d9d9708a8..1ce61f46f 100644
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -22,13 +22,14 @@
 #include "theory/arith/arithvar.h"
 #include "theory/arith/bound_counts.h"
 #include "theory/arith/constraint_forward.h"
-#include "theory/arith/theory_arith_private_forward.h"
 #include "util/rational.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
+class TheoryArithPrivate;
+
 /**
  * ArithVarCallBack provides a mechanism for agreeing on callbacks while
  * breaking mutual recursion inclusion order problems.
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 67df9237c..6115fec8a 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -38,11 +38,6 @@
 
 namespace CVC4 {
 namespace theory {
-
-namespace quantifiers {
-class EqualityInference;
-}
-
 namespace arith {
 
 class ArithCongruenceManager {
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(
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index f05dee38b..8555156a5 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -18,16 +18,19 @@
 #pragma once
 
 #include "expr/node.h"
+#include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_state.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nonlinear_extension.h"
-#include "theory/arith/theory_arith_private_forward.h"
+#include "theory/arith/operator_elim.h"
 #include "theory/theory.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
+class TheoryArithPrivate;
+
 /**
  * Implementation of linear and non-linear integer and real arithmetic.
  * The linear arithmetic solver is based upon:
@@ -120,6 +123,15 @@ class TheoryArith : public Theory {
   }
 
  private:
+  /**
+   * Preprocess rewrite terms, return the trust node encapsulating the
+   * preprocessed form of n, and the proof generator that can provide the
+   * proof for the equivalence of n and this term.
+   *
+   * This calls the operator elimination utility to eliminate extended
+   * symbols.
+   */
+  TrustNode ppRewriteTerms(TNode n);
   /** Get the proof equality engine */
   eq::ProofEqEngine* getProofEqEngine();
   /** The state object wrapping TheoryArithPrivate  */
@@ -132,6 +144,10 @@ class TheoryArith : public Theory {
    * arithmetic.
    */
   std::unique_ptr<nl::NonlinearExtension> d_nonlinearExtension;
+  /** The operator elimination utility */
+  OperatorElim d_opElim;
+  /** The theory rewriter for this theory. */
+  ArithRewriter d_rewriter;
 };/* class TheoryArith */
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 1a13f44fa..557072319 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -92,7 +92,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
                                        const LogicInfo& logicInfo,
                                        ProofNodeManager* pnm)
     : d_containing(containing),
-      d_nlIncomplete(false),
+      d_foundNl(false),
       d_rowTracking(),
       d_pnm(pnm),
       d_checker(),
@@ -147,7 +147,6 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
           d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
       d_attemptSolSimplex(
           d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
-      d_nonlinearExtension(nullptr),
       d_pass1SDP(NULL),
       d_otherSDP(NULL),
       d_lastContextIntegerAttempted(c, -1),
@@ -171,8 +170,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
       d_solveIntAttempts(0u),
       d_newFacts(false),
       d_previousStatus(Result::SAT_UNKNOWN),
-      d_statistics(),
-      d_opElim(pnm, logicInfo)
+      d_statistics()
 {
   ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
   if (pc != nullptr)
@@ -186,7 +184,6 @@ TheoryArithPrivate::~TheoryArithPrivate(){
   if(d_approxStats != NULL) { delete d_approxStats; }
 }
 
-TheoryRewriter* TheoryArithPrivate::getTheoryRewriter() { return &d_rewriter; }
 bool TheoryArithPrivate::needsEqualityEngine(EeSetupInfo& esi)
 {
   return d_congruenceManager.needsEqualityEngine(esi);
@@ -197,7 +194,6 @@ void TheoryArithPrivate::finishInit()
   eq::ProofEqEngine* pfee = d_containing.getProofEqEngine();
   Assert(ee != nullptr);
   d_congruenceManager.finishInit(ee, pfee);
-  d_nonlinearExtension = d_containing.d_nonlinearExtension.get();
 }
 
 static bool contains(const ConstraintCPVec& v, ConstraintP con){
@@ -1107,49 +1103,6 @@ Node TheoryArithPrivate::getModelValue(TNode term) {
   }
 }
 
-TrustNode TheoryArithPrivate::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);
-}
-
-TrustNode TheoryArithPrivate::ppRewrite(TNode 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);
-}
-
 Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
   TimerStat::CodeTimer codeTimer(d_statistics.d_simplifyTimer);
   Debug("simplify") << "TheoryArithPrivate::solve(" << in << ")" << endl;
@@ -1296,11 +1249,7 @@ void TheoryArithPrivate::setupVariableList(const VarList& vl){
     if(getLogicInfo().isLinear()){
       throw LogicException("A non-linear fact was asserted to arithmetic in a linear logic.");
     }
-
-    if (d_nonlinearExtension == nullptr)
-    {
-      d_nlIncomplete = true;
-    }
+    d_foundNl = true;
 
     ++(d_statistics.d_statUserVariables);
     requestArithVar(vlNode, false, false);
@@ -1308,16 +1257,12 @@ void TheoryArithPrivate::setupVariableList(const VarList& vl){
     //setupInitialValue(av);
 
     markSetup(vlNode);
-  }else{
-    if (d_nonlinearExtension == nullptr)
-    {
-      if (vlNode.getKind() == kind::EXPONENTIAL
-          || vlNode.getKind() == kind::SINE || vlNode.getKind() == kind::COSINE
-          || vlNode.getKind() == kind::TANGENT)
-      {
-        d_nlIncomplete = true;
-      }
-    }
+  }
+  else if (vlNode.getKind() == kind::EXPONENTIAL
+           || vlNode.getKind() == kind::SINE || vlNode.getKind() == kind::COSINE
+           || vlNode.getKind() == kind::TANGENT)
+  {
+    d_foundNl = true;
   }
 
   /* Note:
@@ -3332,7 +3277,7 @@ void TheoryArithPrivate::preNotifyFact(TNode atom, bool pol, TNode fact)
   }
 }
 
-void TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
+bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
 {
   if(!anyConflict()){
     while(!d_learnedBounds.empty()){
@@ -3368,7 +3313,7 @@ void TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
     }
     outputConflicts();
     //cout << "unate conflict 1 " << effortLevel << std::endl;
-    return;
+    return true;
   }
 
 
@@ -3403,7 +3348,7 @@ void TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
       revertOutOfConflict();
       d_errorSet.clear();
       outputConflicts();
-      return;
+      return true;
     }
   }
 
@@ -3641,24 +3586,10 @@ void TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
     }
   }//if !emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()
 
-  if(!emmittedConflictOrSplit && effortLevel>=Theory::EFFORT_FULL){
-    if (d_nonlinearExtension != nullptr)
-    {
-      d_nonlinearExtension->check( effortLevel );
-    }
-  }
-
-  if(Theory::fullEffort(effortLevel) && d_nlIncomplete){
-    setIncomplete();
-  }
-
   if(Theory::fullEffort(effortLevel)){
     if(Debug.isOn("arith::consistency::final")){
       entireStateIsConsistent("arith::consistency::final");
     }
-    // cout << "fulleffort" << getSatContext()->getLevel() << endl;
-    // entireStateIsConsistent("arith::consistency::final");
-    // cout << "emmittedConflictOrSplit" << emmittedConflictOrSplit << endl;
   }
 
   if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
@@ -3666,8 +3597,11 @@ void TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
     debugPrintModel(Debug("arith::print_model"));
   }
   Debug("arith") << "TheoryArithPrivate::check end" << std::endl;
+  return emmittedConflictOrSplit;
 }
 
+bool TheoryArithPrivate::foundNonlinear() const { return d_foundNl; }
+
 Node TheoryArithPrivate::branchIntegerVariable(ArithVar x) const {
   const DeltaRational& d = d_partialModel.getAssignment(x);
   Assert(!d.isIntegral());
@@ -4075,7 +4009,6 @@ void TheoryArithPrivate::collectModelValues(const std::set<Node>& termSet,
                                             std::map<Node, Node>& arithModel)
 {
   AlwaysAssert(d_qflraStatus == Result::SAT);
-  //AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints");
 
   if(Debug.isOn("arith::collectModelInfo")){
     debugPrintFacts();
@@ -4687,12 +4620,6 @@ const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{
   return d_rowTracking[ridx];
 }
 
-TrustNode TheoryArithPrivate::expandDefinition(Node node)
-{
-  // call eliminate operators
-  return d_opElim.eliminate(node);
-}
-
 std::pair<bool, Node> TheoryArithPrivate::entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){
   using namespace inferbounds;
 
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 71bada17d..1d840a81f 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -35,7 +35,6 @@
 #include "options/arith_options.h"
 #include "smt/logic_exception.h"
 #include "smt_util/boolean_simplification.h"
-#include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_static_learner.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/arithvar.h"
@@ -50,13 +49,11 @@
 #include "theory/arith/linear_equality.h"
 #include "theory/arith/matrix.h"
 #include "theory/arith/normal_form.h"
-#include "theory/arith/operator_elim.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/proof_checker.h"
 #include "theory/arith/simplex.h"
 #include "theory/arith/soi_simplex.h"
 #include "theory/arith/theory_arith.h"
-#include "theory/arith/theory_arith_private_forward.h"
 #include "theory/eager_proof_generator.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
@@ -82,10 +79,6 @@ namespace inferbounds {
 }
 class InferBoundsResult;
 
-namespace nl {
-class NonlinearExtension;
-}
-
 /**
  * Implementation of QF_LRA.
  * Based upon:
@@ -98,9 +91,10 @@ private:
 
   TheoryArith& d_containing;
 
-  bool d_nlIncomplete;
-  // TODO A better would be:
-  //context::CDO<bool> d_nlIncomplete;
+  /**
+   * Whether we encountered non-linear arithmetic at any time during solving.
+   */
+  bool d_foundNl;
 
   BoundInfoMap d_rowTracking;
 
@@ -382,9 +376,6 @@ private:
   SumOfInfeasibilitiesSPD d_soiSimplex;
   AttemptSolutionSDP d_attemptSolSimplex;
 
-  /** non-linear algebraic approach */
-  nl::NonlinearExtension* d_nonlinearExtension;
-
   bool solveRealRelaxation(Theory::Effort effortLevel);
 
   /* Returns true if this is heuristically a good time to try
@@ -426,10 +417,6 @@ private:
 
   Node axiomIteForTotalDivision(Node div_tot);
   Node axiomIteForTotalIntDivision(Node int_div_like);
-
-  // handle linear /, div, mod, and also is_int, to_int
-  TrustNode ppRewriteTerms(TNode atom);
-
  public:
   TheoryArithPrivate(TheoryArith& containing,
                      context::Context* c,
@@ -441,8 +428,6 @@ private:
   ~TheoryArithPrivate();
 
   //--------------------------------- initialization
-  /** get the official theory rewriter of this theory */
-  TheoryRewriter* getTheoryRewriter();
   /**
    * Returns true if we need an equality engine, see
    * Theory::needsEqualityEngine.
@@ -456,7 +441,6 @@ private:
    * Does non-context dependent setup for a node connected to a theory.
    */
   void preRegisterTerm(TNode n);
-  TrustNode expandDefinition(Node node);
 
   void propagate(Theory::Effort e);
   Node explain(TNode n);
@@ -482,7 +466,6 @@ private:
   void presolve();
   void notifyRestart();
   Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
-  TrustNode ppRewrite(TNode atom);
   void ppStaticLearn(TNode in, NodeBuilder<>& learned);
 
   std::string identify() const { return std::string("TheoryArith"); }
@@ -502,9 +485,21 @@ private:
   bool preCheck(Theory::Effort level);
   /** Pre-notify fact. */
   void preNotifyFact(TNode atom, bool pol, TNode fact);
-  /** Post-check, called after the fact queue of the theory is processed. */
-  void postCheck(Theory::Effort level);
+  /**
+   * Post-check, called after the fact queue of the theory is processed. Returns
+   * true if a conflict or lemma was emitted.
+   */
+  bool postCheck(Theory::Effort level);
   //--------------------------------- end standard check
+  /**
+   * Found non-linear? This returns true if this solver ever encountered
+   * any non-linear terms that were unhandled. Note that this class is not
+   * responsible for handling non-linear arithmetic. If the owner of this
+   * class does not handle non-linear arithmetic in another way, then
+   * setIncomplete should be called on the output channel of TheoryArith.
+   */
+  bool foundNonlinear() const;
+
  private:
   /** The constant zero. */
   DeltaRational d_DELTA_ZERO;
@@ -692,10 +687,6 @@ private:
   inline TheoryId theoryOf(TNode x) const { return d_containing.theoryOf(x); }
   inline void debugPrintFacts() const { d_containing.debugPrintFacts(); }
   inline context::Context* getSatContext() const { return d_containing.getSatContext(); }
-  inline void setIncomplete() {
-    (d_containing.d_out)->setIncomplete();
-    d_nlIncomplete = true;
-  }
   void outputLemma(TNode lem);
   void outputConflict(TNode lit);
   void outputPropagate(TNode lit);
@@ -877,11 +868,6 @@ private:
 
 
   Statistics d_statistics;
-
-  /** The theory rewriter for this theory. */
-  ArithRewriter d_rewriter;
-  /** The operator elimination utility */
-  OperatorElim d_opElim;
 };/* class TheoryArithPrivate */
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/theory_arith_private_forward.h b/src/theory/arith/theory_arith_private_forward.h
deleted file mode 100644
index 6668e0386..000000000
--- a/src/theory/arith/theory_arith_private_forward.h
+++ /dev/null
@@ -1,31 +0,0 @@
-/*********************                                                        */
-/*! \file theory_arith_private_forward.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-
-#include "cvc4_private.h"
-
-#pragma once
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-class TheoryArithPrivate;
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */