diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-19 16:59:35 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-19 21:59:35 +0000 |
| commit | 14ee76f0737bcd0ad6711c4ab4ff9bf53a29a705 (patch) | |
| tree | 1ecb2ec9968443adfb37f7f9128a1c4107254907 /test/regress/regress0/quantifiers | |
| parent | a06ec9eb224c437523f3bff0ac6f6437d924f36a (diff) | |
Fully incorporate quantifiers macros into ppAssert / non-clausal simplification (#6394)
This PR removes the quantifiers macro preprocessing pass, which had several shortcomings, both in terms of performance and features.
This makes it so that quantifier macros are the (optional) implementation of TheoryQuantifiers::ppAssert.
In other words, quantifiers can now be put into "solved form", forall x. P(x) ---> P = lambda x. true.
This is part of an effort to improve proofs for preprocessing, as well as centralizing our reason about substitutions for the sake of efficiency.
Diffstat (limited to 'test/regress/regress0/quantifiers')
| -rw-r--r-- | test/regress/regress0/quantifiers/issue2033-macro-arith.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/macro-back-subs-sat.smt2 | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2 b/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2 index 7993910fd..d65a92aa5 100644 --- a/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2 +++ b/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --macros-quant +; COMMAND-LINE: --macros-quant -q ; EXPECT: sat (set-logic AUFNIRA) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/macro-back-subs-sat.smt2 b/test/regress/regress0/quantifiers/macro-back-subs-sat.smt2 index 34b7422a5..bdb389a63 100644 --- a/test/regress/regress0/quantifiers/macro-back-subs-sat.smt2 +++ b/test/regress/regress0/quantifiers/macro-back-subs-sat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --macros-quant +; COMMAND-LINE: --macros-quant -q ; EXPECT: sat (set-logic UFLIA) (declare-fun A (Int) Int) |