diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-12 10:13:45 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-12 10:13:45 -0500 |
commit | 4ff2946e1338d3f500b7e6bababee50fadad68d6 (patch) | |
tree | 6f1306e4476e3f7496d7a4e045e63d942802a392 /test/regress | |
parent | 1b2e6c81be2a8ab0656ff2ee3938ef4587e24e25 (diff) |
Optimizations for QCF to check relevant domain of variable argument positions eagerly, global ordering mechanism for quantified formulas within check. Refactoring of term database.
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 | 45 |
2 files changed, 47 insertions, 1 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 784eaf677..b51313deb 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -77,7 +77,8 @@ TESTS = \ anti-sk-simp.smt2 \ pure_dt_cbqi.smt2 \ florian-case-ax.smt2 \ - double-pattern.smt2 + double-pattern.smt2 \ + qcf-rel-dom-opt.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 b/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 new file mode 100644 index 000000000..539f181af --- /dev/null +++ b/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 @@ -0,0 +1,45 @@ +(set-logic UFLIA) +(set-info :status unsat) +(declare-fun P (Int) Bool) + +(assert (P 0)) +(assert (P 1)) +(assert (P 2)) +(assert (P 3)) +(assert (P 4)) +(assert (P 5)) +(assert (P 6)) +(assert (P 7)) +(assert (P 8)) +(assert (P 9)) + +(assert (P 10)) +(assert (P 11)) +(assert (P 12)) +(assert (P 13)) +(assert (P 14)) +(assert (P 15)) +(assert (P 16)) +(assert (P 17)) +(assert (P 18)) +(assert (P 19)) + +(assert (P 20)) +(assert (P 21)) +(assert (P 22)) +(assert (P 23)) +(assert (P 24)) +(assert (P 25)) +(assert (P 26)) +(assert (P 27)) +(assert (P 28)) +(assert (P 29)) + +(declare-fun Q (Int Int Int Int Int) Bool) +(assert (forall ((x Int) (y Int) (z Int) (w Int) (q Int)) (or (not (P x)) (not (P y)) (not (P z)) (not (P w)) (not (P q)) (Q x y z w q)))) + +(declare-fun R (Int) Bool) +(assert (R 0)) +(assert (forall ((x Int)) (not (R x)))) + +(check-sat) |