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

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(); }