diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-19 16:53:48 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-19 16:53:48 -0600 |
| commit | f2ed7b1aebc175b971e3cebf4c0b2fff6e4e895f (patch) | |
| tree | 9d67467344399282909475f3cf891639f8abbaf8 /test/regress/regress1 | |
| parent | 7191e58e5561a159c0cd3b81fddbe311ba70a45b (diff) | |
Enable new implementation of CEGQI based on nested quantifier elimination (#5477)
This replaces the old implementation of CEGQI based on nested quantifier elimination (--cegqi-nested-qe) with the new implementation.
The previous implementation used some convoluted internal attributes to manage dependencies between quantified formulas, the new implementation is much simpler: it simply eliminates nested quantification eagerly.
Fixes #5365, fixes #5279, fixes #4849, fixes #4433.
This PR also required fixes related to how quantifier elimination is computed.
Diffstat (limited to 'test/regress/regress1')
4 files changed, 35 insertions, 0 deletions
diff --git a/test/regress/regress1/quantifiers/issue4433-nqe.smt2 b/test/regress/regress1/quantifiers/issue4433-nqe.smt2 new file mode 100644 index 000000000..1ab35a43f --- /dev/null +++ b/test/regress/regress1/quantifiers/issue4433-nqe.smt2 @@ -0,0 +1,9 @@ +(set-logic LIA) +(set-option :cegqi-nested-qe true) +(set-info :status unsat) +(assert + (forall ((a Int) (b Int)) + (xor (xor (= a 0) (= b 0)) + (forall ((c Int)) + (= (ite (= a 0) 0 1) (ite (= c 0) 0 1)))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue4849-nqe.smt2 b/test/regress/regress1/quantifiers/issue4849-nqe.smt2 new file mode 100644 index 000000000..dd7a22e39 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue4849-nqe.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --cegqi-nested-qe -q +; EXPECT: sat +(set-logic LIA) +(set-option :cegqi-nested-qe true) +(set-info :status sat) +(assert (forall ((a Int)) (exists ((b Int)) (= (ite (= a 0) 0 1) (ite (= b 0) 0 1))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue5279-nqe.smt2 b/test/regress/regress1/quantifiers/issue5279-nqe.smt2 new file mode 100644 index 000000000..b87f36ebe --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5279-nqe.smt2 @@ -0,0 +1,5 @@ +(set-logic LIA) +(set-option :cegqi-nested-qe true) +(set-info :status unsat) +(assert (forall ((a Int) (b Bool)) (= a (ite b 0 1)))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue5365-nqe.smt2 b/test/regress/regress1/quantifiers/issue5365-nqe.smt2 new file mode 100644 index 000000000..c19cb6a3f --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5365-nqe.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --cegqi-nested-qe -q +; EXPECT: sat +(set-logic BV) +(set-option :cegqi-nested-qe true) +(set-info :status sat) +(assert + (exists ((a (_ BitVec 32))) + (forall ((b (_ BitVec 32)) (c (_ BitVec 32))) + (exists ((d (_ BitVec 32)) (e (_ BitVec 32))) + (forall ((g (_ BitVec 32))) + (exists ((f (_ BitVec 32))) + (=> (= (_ bv0 32) a) + (= (bvadd e g) (bvand d f) b c)))))))) +(check-sat) |