diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-28 21:43:49 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-28 21:43:49 -0600 |
| commit | 940a25255469bbeea95df14ef25036e6c0565c3e (patch) | |
| tree | 5d00490debcd9c96de307810daf2aa5d8935a233 /test/regress/regress0/quantifiers | |
| parent | a975f3af51a3730f5b848d2b55f9c6d4027fe763 (diff) | |
Replace conditional rewrite pass in quantifiers with the extended rewriter (#3841)
Fixes #3839.
Previously, the quantifiers rewriter had a rewriting step that was an ad-hoc version of some of the rewrites that have been incorporated into the extended rewriter. Moreover, the code for that pass was buggy.
This eliminates the previous conditional rewriting step from the "term process" rewrite pass in quantifiers. It additional adds an optional (disabled by default) rewriting pass that calls the extended rewriter on the body of quantified formulas. This subsumes the previous behavior and should not be buggy.
Notice that the indentation in computeProcessTerms changed and subsequently has been updated to the new coding standards.
This PR relies on #3840.
Diffstat (limited to 'test/regress/regress0/quantifiers')
| -rw-r--r-- | test/regress/regress0/quantifiers/agg-rew-test-cf.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/agg-rew-test.smt2 | 2 |
2 files changed, 4 insertions, 0 deletions
diff --git a/test/regress/regress0/quantifiers/agg-rew-test-cf.smt2 b/test/regress/regress0/quantifiers/agg-rew-test-cf.smt2 index 44f475d83..f46147d7b 100644 --- a/test/regress/regress0/quantifiers/agg-rew-test-cf.smt2 +++ b/test/regress/regress0/quantifiers/agg-rew-test-cf.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --ext-rewrite-quant +; EXPECT: sat (set-logic UFLIA) (set-info :status sat) (declare-fun Q (Int Int) Bool) diff --git a/test/regress/regress0/quantifiers/agg-rew-test.smt2 b/test/regress/regress0/quantifiers/agg-rew-test.smt2 index d1159278e..7dfb1430e 100644 --- a/test/regress/regress0/quantifiers/agg-rew-test.smt2 +++ b/test/regress/regress0/quantifiers/agg-rew-test.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --ext-rewrite-quant +; EXPECT: sat (set-logic UFLIA) (set-info :status sat) (declare-fun Q (Int Int) Bool) |