Do not expand theory definitions at the beginning of preprocessing (#5544)

This updates the preprocessor so that expand definitions does not expand theory symbols at the beginning of preprocessing.

This also restores the previous expandDefinitions method in arithmetic, which is required for correctly interpreting division by zero in models, but should not be applied at the beginning of preprocessing. Moreover it ensures that only partial operators are eliminated in arithmetic expandDefinitions, which required an additional argument partialOnly to arith::OperatorElim.

This adds -q to suppress warnings for many quantified regressions which now emit warnings with --check-model. This will be addressed later as part of CVC4/cvc4-wishues#43.

The purpose of this PR is two-fold:
(1) Currently our responses to get-value are incorrect for partial operators like div, mod, seq.nth since partial operators can be left unevaluated.
(2) The preprocessor should have the opportunity to rewrite and eliminate extended operators before they are expanded. This is required for addressing performance issues for non-linear arithmetic. It is also required for ensuring that trigger selection can be done properly for datatype selectors (to be addressed on a later PR).

1 files changed, 26 insertions, 7 deletions

diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
index 4d4c4a6f5..fbd1798cd 100644
--- a/src/theory/arith/operator_elim.cpp
+++ b/src/theory/arith/operator_elim.cpp
@@ -46,21 +46,23 @@ void OperatorElim::checkNonLinearLogic(Node term)
   }
 }
 
-TrustNode OperatorElim::eliminate(Node n)
+TrustNode OperatorElim::eliminate(Node n, bool partialOnly)
 {
   TConvProofGenerator* tg = nullptr;
-  Node nn = eliminateOperators(n, tg);
+  Node nn = eliminateOperators(n, tg, partialOnly);
   if (nn != n)
   {
     // since elimination may introduce new operators to eliminate, we must
     // recursively eliminate result
-    Node nnr = eliminateOperatorsRec(nn, tg);
+    Node nnr = eliminateOperatorsRec(nn, tg, partialOnly);
     return TrustNode::mkTrustRewrite(n, nnr, nullptr);
   }
   return TrustNode::null();
 }
 
-Node OperatorElim::eliminateOperatorsRec(Node n, TConvProofGenerator* tg)
+Node OperatorElim::eliminateOperatorsRec(Node n,
+                                         TConvProofGenerator* tg,
+                                         bool partialOnly)
 {
   Trace("arith-elim") << "Begin elim: " << n << std::endl;
   NodeManager* nm = NodeManager::currentNM();
@@ -108,12 +110,12 @@ Node OperatorElim::eliminateOperatorsRec(Node n, TConvProofGenerator* tg)
       {
         ret = nm->mkNode(cur.getKind(), children);
       }
-      Node retElim = eliminateOperators(ret, tg);
+      Node retElim = eliminateOperators(ret, tg, partialOnly);
       if (retElim != ret)
       {
         // recursively eliminate operators in result, since some eliminations
         // are defined in terms of other non-standard operators.
-        ret = eliminateOperatorsRec(retElim, tg);
+        ret = eliminateOperatorsRec(retElim, tg, partialOnly);
       }
       visited[cur] = ret;
     }
@@ -123,7 +125,9 @@ Node OperatorElim::eliminateOperatorsRec(Node n, TConvProofGenerator* tg)
   return visited[n];
 }
 
-Node OperatorElim::eliminateOperators(Node node, TConvProofGenerator* tg)
+Node OperatorElim::eliminateOperators(Node node,
+                                      TConvProofGenerator* tg,
+                                      bool partialOnly)
 {
   NodeManager* nm = NodeManager::currentNM();
   SkolemManager* sm = nm->getSkolemManager();
@@ -143,6 +147,11 @@ Node OperatorElim::eliminateOperators(Node node, TConvProofGenerator* tg)
     case TO_INTEGER:
     case IS_INTEGER:
     {
+      if (partialOnly)
+      {
+        // not eliminating total operators
+        return node;
+      }
       Node toIntSkolem;
       std::map<Node, Node>::const_iterator it = d_to_int_skolem.find(node[0]);
       if (it == d_to_int_skolem.end())
@@ -180,6 +189,11 @@ Node OperatorElim::eliminateOperators(Node node, TConvProofGenerator* tg)
     case INTS_DIVISION_TOTAL:
     case INTS_MODULUS_TOTAL:
     {
+      if (partialOnly)
+      {
+        // not eliminating total operators
+        return node;
+      }
       Node den = Rewriter::rewrite(node[1]);
       Node num = Rewriter::rewrite(node[0]);
       Node intVar;
@@ -283,6 +297,11 @@ Node OperatorElim::eliminateOperators(Node node, TConvProofGenerator* tg)
     }
     case DIVISION_TOTAL:
     {
+      if (partialOnly)
+      {
+        // not eliminating total operators
+        return node;
+      }
       Node num = Rewriter::rewrite(node[0]);
       Node den = Rewriter::rewrite(node[1]);
       if (den.isConst())