diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-20 15:19:40 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-20 15:19:40 -0600 |
| commit | 6beb76055b81510ec38a8b50f5ed35d2f5010139 (patch) | |
| tree | 87c8b09f26091794943bdaf58c502cc0c29f5a60 /test/regress | |
| parent | 798524d033f69153d4bf6604e08c69a571771ae8 (diff) | |
Support nested quantifier elimination for get-qe command (#5490)
Uses new nested-qe utility for eliminating nested quantification before doing quantifier elimination.
Fixes CVC4/cvc4-wishues#26
Fixes #5484.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/issue5484-qe.smt2 | 9 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/issue5484b-qe.smt2 | 18 |
3 files changed, 29 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 7e87c337a..cb37b428e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1616,6 +1616,8 @@ set(regress_1_tests regress1/quantifiers/issue5469-aext.smt2 regress1/quantifiers/issue5470-aext.smt2 regress1/quantifiers/issue5471-aext.smt2 + regress1/quantifiers/issue5484-qe.smt2 + regress1/quantifiers/issue5484b-qe.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lia-witness-div-pp.smt2 diff --git a/test/regress/regress1/quantifiers/issue5484-qe.smt2 b/test/regress/regress1/quantifiers/issue5484-qe.smt2 new file mode 100644 index 000000000..c2499ed16 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5484-qe.smt2 @@ -0,0 +1,9 @@ +; SCRUBBER: sed 's/(.*)/()/g' +; EXPECT: () +; EXIT: 0 +(set-logic LIA) +(declare-fun v9 () Bool) +(declare-fun v18 () Bool) +(declare-fun i2 () Int) +(declare-fun v31 () Bool) +(get-qe (forall ((q23 Int) (q24 Int) (q25 Int) (q26 Int) (q27 Bool) (q28 Int) (q29 Int)) (xor (=> (not (not (distinct 83 407))) (> (- i2 31 722) 319)) (forall ((q23 Int) (q24 Int) (q25 Int) (q26 Int) (q27 Bool) (q28 Int) (q29 Int)) (not (not (not v9)))) v31 (> 665 (+ (mod 83 923) (div i2 850)) 319 (- 939 878)) v18))) diff --git a/test/regress/regress1/quantifiers/issue5484b-qe.smt2 b/test/regress/regress1/quantifiers/issue5484b-qe.smt2 new file mode 100644 index 000000000..86f999504 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5484b-qe.smt2 @@ -0,0 +1,18 @@ +; SCRUBBER: sed 's/(.*)/()/g' +; EXPECT: () +; EXIT: 0 +(set-logic LIA) +(declare-fun v0 () Bool) +(declare-fun v1 () Bool) +(declare-fun v2 () Bool) +(declare-fun v3 () Bool) +(declare-fun v4 () Bool) +(declare-fun v7 () Bool) +(declare-fun v8 () Bool) +(declare-fun i6 () Int) +(declare-fun i9 () Int) +(declare-fun i11 () Int) +(declare-fun i13 () Int) +(declare-fun v9 () Bool) +(declare-fun i16 () Int) +(get-qe (forall ((q75 Bool)) (xor (< i9 52) (forall ((q75 Bool)) (not (and (< i16 37) q75 q75 v1))) v2 (and (distinct v4 v3 v4) v9 v9 (and v7 v0 (>= 24 56 i11 i6 7) v0 v8)) (= (+ (div i13 340) 268 i9) i13)))) |