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).

17 files changed, 114 insertions, 21 deletions

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index fe3dbc62b..c2374c6ff 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -130,7 +130,11 @@ bool ProcessAssertions::apply(Assertions& as)
       << "ProcessAssertions::processAssertions() : pre-definition-expansion"
       << endl;
   dumpAssertions("pre-definition-expansion", assertions);
-  d_exDefs.expandAssertions(assertions, false);
+  // Expand definitions, which replaces defined functions with their definition
+  // and does beta reduction. Notice we pass true as the second argument since
+  // we do not want to call theories to expand definitions here, since we want
+  // to give the opportunity to rewrite/preprocess terms before expansion.
+  d_exDefs.expandAssertions(assertions, true);
   Trace("smt-proc")
       << "ProcessAssertions::processAssertions() : post-definition-expansion"
       << endl;
diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp
index 577407c07..142f02eab 100644
--- a/src/theory/arith/arith_preprocess.cpp
+++ b/src/theory/arith/arith_preprocess.cpp
@@ -25,7 +25,10 @@ ArithPreprocess::ArithPreprocess(ArithState& state,
     : d_im(im), d_opElim(pnm, info), d_reduced(state.getUserContext())
 {
 }
-TrustNode ArithPreprocess::eliminate(TNode n) { return d_opElim.eliminate(n); }
+TrustNode ArithPreprocess::eliminate(TNode n, bool partialOnly)
+{
+  return d_opElim.eliminate(n, partialOnly);
+}
 bool ArithPreprocess::reduceAssertion(TNode atom)
 {
   context::CDHashMap<Node, bool, NodeHashFunction>::const_iterator it =
diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h
index 165209bd9..622357e73 100644
--- a/src/theory/arith/arith_preprocess.h
+++ b/src/theory/arith/arith_preprocess.h
@@ -46,8 +46,13 @@ class ArithPreprocess
    * Call eliminate operators on formula n, return the resulting trust node,
    * which is of TrustNodeKind REWRITE and whose node is the result of
    * eliminating extended operators from n.
+   *
+   * @param n The node to eliminate operators from
+   * @param partialOnly Whether we are eliminating partial operators only.
+   * @return the trust node proving (= n nr) where nr is the return of
+   * eliminating operators in n, or the null trust node if n was unchanged.
    */
-  TrustNode eliminate(TNode n);
+  TrustNode eliminate(TNode n, bool partialOnly = false);
   /**
    * Reduce assertion. This sends a lemma via the inference manager if atom
    * contains any extended operators. When applicable, the lemma is of the form:
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())
diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h
index c7b55caf1..bca80ea4d 100644
--- a/src/theory/arith/operator_elim.h
+++ b/src/theory/arith/operator_elim.h
@@ -37,7 +37,7 @@ class OperatorElim : public EagerProofGenerator
     * transcendental functions), then we replace it by a form that eliminates
     * that operator. This may involve the introduction of witness terms.
     */
-  TrustNode eliminate(Node n);
+  TrustNode eliminate(Node n, bool partialOnly = false);
   /**
    * Get axiom for term n. This returns the axiom that this class uses to
    * eliminate the term n, which is determined by its top-most symbol.
@@ -101,7 +101,7 @@ class OperatorElim : public EagerProofGenerator
    * @param n The node to eliminate operators from.
    * @return The (single step) eliminated form of n.
    */
-  Node eliminateOperators(Node n, TConvProofGenerator* tg);
+  Node eliminateOperators(Node n, TConvProofGenerator* tg, bool partialOnly);
   /**
    * Recursively ensure that n has no non-standard operators. This applies
    * the above method on all subterms of n.
@@ -109,7 +109,7 @@ class OperatorElim : public EagerProofGenerator
    * @param n The node to eliminate operators from.
    * @return The eliminated form of n.
    */
-  Node eliminateOperatorsRec(Node n, TConvProofGenerator* tg);
+  Node eliminateOperatorsRec(Node n, TConvProofGenerator* tg, bool partialOnly);
   /** get arithmetic skolem
    *
    * Returns the Skolem in the above map for the given id, creating it if it
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 247772897..b8cead4fc 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -97,6 +97,12 @@ void TheoryArith::preRegisterTerm(TNode n)
   d_internal->preRegisterTerm(n);
 }
 
+TrustNode TheoryArith::expandDefinition(Node node)
+{
+  // call eliminate operators, to eliminate partial operators only
+  return d_arithPreproc.eliminate(node, true);
+}
+
 void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); }
 
 TrustNode TheoryArith::ppRewrite(TNode atom)
@@ -140,8 +146,9 @@ TrustNode TheoryArith::ppRewriteTerms(TNode n)
   // 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_arithPreproc.eliminate(n);
+  // call eliminate operators. In contrast to expandDefinitions, we eliminate
+  // *all* extended arithmetic operators here, including total ones.
+  return d_arithPreproc.eliminate(n, false);
 }
 
 Theory::PPAssertStatus TheoryArith::ppAssert(
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index e6029faef..e26ff51ef 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -68,7 +68,11 @@ class TheoryArith : public Theory {
   /** finish initialization */
   void finishInit() override;
   //--------------------------------- end initialization
-
+  /**
+   * Expand definition, which eliminates extended operators like div/mod in
+   * the given node.
+   */
+  TrustNode expandDefinition(Node node) override;
   /**
    * Does non-context dependent setup for a node connected to a theory.
    */
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 3e59aebe6..4d4ec89b4 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -318,6 +318,12 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck
 
 TrustNode TheoryArrays::ppRewrite(TNode term)
 {
+  // first, see if we need to expand definitions
+  TrustNode texp = expandDefinition(term);
+  if (!texp.isNull())
+  {
+    return texp;
+  }
   if (!d_preprocess)
   {
     return TrustNode::null();
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index d43fa3927..7285b6768 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -200,7 +200,16 @@ Theory::PPAssertStatus TheoryBV::ppAssert(
   return d_internal->ppAssert(tin, outSubstitutions);
 }
 
-TrustNode TheoryBV::ppRewrite(TNode t) { return d_internal->ppRewrite(t); }
+TrustNode TheoryBV::ppRewrite(TNode t)
+{
+  // first, see if we need to expand definitions
+  TrustNode texp = expandDefinition(t);
+  if (!texp.isNull())
+  {
+    return texp;
+  }
+  return d_internal->ppRewrite(t);
+}
 
 void TheoryBV::presolve() { d_internal->presolve(); }
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 74c822215..ff36216c2 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -431,6 +431,8 @@ void TheoryDatatypes::preRegisterTerm(TNode n)
 {
   Trace("datatypes-prereg")
       << "TheoryDatatypes::preRegisterTerm() " << n << endl;
+  // external selectors should be preprocessed away by now
+  Assert(n.getKind() != APPLY_SELECTOR);
   // must ensure the type is well founded and has no nested recursion if
   // the option dtNestedRec is not set to true.
   TypeNode tn = n.getType();
@@ -595,7 +597,12 @@ TrustNode TheoryDatatypes::expandDefinition(Node n)
 TrustNode TheoryDatatypes::ppRewrite(TNode in)
 {
   Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl;
-
+  // first, see if we need to expand definitions
+  TrustNode texp = expandDefinition(in);
+  if (!texp.isNull())
+  {
+    return texp;
+  }
   if( in.getKind()==EQUAL ){
     Node nn;
     std::vector< Node > rew;
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 01fab92c8..ce423a7fe 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -454,6 +454,12 @@ TrustNode TheoryFp::expandDefinition(Node node)
 TrustNode TheoryFp::ppRewrite(TNode node)
 {
   Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): " << node << std::endl;
+  // first, see if we need to expand definitions
+  TrustNode texp = expandDefinition(node);
+  if (!texp.isNull())
+  {
+    return texp;
+  }
 
   Node res = node;
 
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 59666f6fd..aa847d8ea 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -1612,7 +1612,10 @@ void CegInstantiator::registerCounterexampleLemma(Node lem,
       // already processed variable
       continue;
     }
-    if (ces.getType().isBoolean())
+    // must avoid selector symbols, and function skolems introduced by
+    // theory preprocessing
+    TypeNode ct = ces.getType();
+    if (ct.isBoolean() || ct.isFunctionLike())
     {
       // Boolean variables, including the counterexample literal, don't matter
       // since they are always assigned a model value.
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 57778b4c8..615ff987a 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -126,6 +126,7 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
   {
     return;
   }
+  Trace("quant-dsplit") << "QuantDSplit::check" << std::endl;
   NodeManager* nm = NodeManager::currentNM();
   FirstOrderModel* m = d_quantEngine->getModel();
   std::vector<Node> lemmas;
@@ -134,6 +135,7 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
        ++it)
   {
     Node q = it->first;
+    Trace("quant-dsplit") << "- Split quantifier " << q << std::endl;
     if (m->isQuantifierAsserted(q) && m->isQuantifierActive(q)
         && d_added_split.find(q) == d_added_split.end())
     {
@@ -196,5 +198,6 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
     Trace("quant-dsplit") << "QuantDSplit lemma : " << lem << std::endl;
     d_quantEngine->addLemma(lem, false);
   }
+  Trace("quant-dsplit") << "QuantDSplit::check finished" << std::endl;
 }
 
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 0e6ab1b18..e4f281de8 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -68,6 +68,9 @@ void TheorySets::finishInit()
   d_valuation.setUnevaluatedKind(COMPREHENSION);
   // choice is used to eliminate witness
   d_valuation.setUnevaluatedKind(WITNESS);
+  // Universe set is not evaluated. This is moreover important for ensuring that
+  // we do not eliminate terms whose value involves the universe set.
+  d_valuation.setUnevaluatedKind(UNIVERSE_SET);
 
   // functions we are doing congruence over
   d_equalityEngine->addFunctionKind(SINGLETON);
@@ -128,6 +131,11 @@ void TheorySets::preRegisterTerm(TNode node)
 
 TrustNode TheorySets::expandDefinition(Node n)
 {
+  return d_internal->expandDefinition(n);
+}
+
+TrustNode TheorySets::ppRewrite(TNode n)
+{
   Kind nk = n.getKind();
   if (nk == UNIVERSE_SET || nk == COMPLEMENT || nk == JOIN_IMAGE
       || nk == COMPREHENSION)
@@ -150,7 +158,8 @@ TrustNode TheorySets::expandDefinition(Node n)
       throw LogicException(ss.str());
     }
   }
-  return d_internal->expandDefinition(n);
+  // just expand definitions
+  return expandDefinition(n);
 }
 
 Theory::PPAssertStatus TheorySets::ppAssert(
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index a5f8fa4d8..3b95c7e00 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -77,6 +77,7 @@ class TheorySets : public Theory
   std::string identify() const override { return "THEORY_SETS"; }
   void preRegisterTerm(TNode node) override;
   TrustNode expandDefinition(Node n) override;
+  TrustNode ppRewrite(TNode n) override;
   PPAssertStatus ppAssert(TrustNode tin,
                           TrustSubstitutionMap& outSubstitutions) override;
   void presolve() override;
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 110ff9b2d..72a4ae50d 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -997,6 +997,12 @@ void TheoryStrings::checkRegisterTermsNormalForms()
 TrustNode TheoryStrings::ppRewrite(TNode atom)
 {
   Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl;
+  // first, see if we need to expand definitions
+  TrustNode texp = expandDefinition(atom);
+  if (!texp.isNull())
+  {
+    return texp;
+  }
   TrustNode ret;
   Node atomRet = atom;
   if (options::regExpElim() && atom.getKind() == STRING_IN_REGEXP)
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index da0fc8de4..84212fa1b 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1402,7 +1402,8 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
   // get the node
   Node node = tlemma.getNode();
   Node lemma = tlemma.getProven();
-  Trace("te-lemma") << "Lemma, input: " << lemma << std::endl;
+  Trace("te-lemma") << "Lemma, input: " << lemma << ", property = " << p
+                    << std::endl;
 
   Assert(!expr::hasFreeVar(lemma));