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, 6 insertions, 1 deletions

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: