diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-09-10 08:12:34 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-09-10 08:12:34 +0200 |
commit | d5b0866bd2a2551143caf591d453993ab5a48840 (patch) | |
tree | 71d9bf61a8134be3ca13596ab0d8f278a2021eb9 /test/regress/regress0 | |
parent | 8a68cca2f9cf76b42187c39d09a4a40bd19622c1 (diff) |
Ensure that expand definitions is called on all non-variable expressi… (#1070)
* Ensure that expand definitions is called on all non-variable expressions. In particular, it is necessary that the sets theory is notified when a set universe term occurs in the input to ensure options are set correctly. The commit moves this check from within check() to expandDefinitions(), and also adds the check for join image which relies on universe set. This fixes a bug reported by Arjun. Add and update regressions.
* Add comments concerning expandDefinitions
* Expand comment, move to .h
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/fmf/quant_real_univ.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_0.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_0_1.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_1.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_1_1.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_2.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_2_1.cvc | 3 | ||||
-rw-r--r-- | test/regress/regress0/sets/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/sets/arjun-set-univ.cvc | 8 | ||||
-rw-r--r-- | test/regress/regress0/sets/univ-set-uf-elim.smt2 | 16 |
10 files changed, 35 insertions, 2 deletions
diff --git a/test/regress/regress0/fmf/quant_real_univ.cvc b/test/regress/regress0/fmf/quant_real_univ.cvc index c3cefd767..c3dbb2cd6 100644 --- a/test/regress/regress0/fmf/quant_real_univ.cvc +++ b/test/regress/regress0/fmf/quant_real_univ.cvc @@ -1,5 +1,6 @@ % EXPECT: sat
OPTION "fmf-bound";
+OPTION "sets-ext";
Atom : TYPE;
REAL_UNIVERSE : SET OF [REAL];
ATOM_UNIVERSE : SET OF [Atom];
diff --git a/test/regress/regress0/rels/joinImg_0.cvc b/test/regress/regress0/rels/joinImg_0.cvc index e36c6a647..297898a81 100644 --- a/test/regress/regress0/rels/joinImg_0.cvc +++ b/test/regress/regress0/rels/joinImg_0.cvc @@ -1,5 +1,6 @@ % EXPECT: unsat OPTION "logic" "ALL_SUPPORTED"; +OPTION "sets-ext"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/joinImg_0_1.cvc b/test/regress/regress0/rels/joinImg_0_1.cvc index 602c4fe3f..4e69394bd 100644 --- a/test/regress/regress0/rels/joinImg_0_1.cvc +++ b/test/regress/regress0/rels/joinImg_0_1.cvc @@ -1,5 +1,6 @@ % EXPECT: sat OPTION "logic" "ALL_SUPPORTED"; +OPTION "sets-ext"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/joinImg_1.cvc b/test/regress/regress0/rels/joinImg_1.cvc index 47e57c1fb..81f208fc4 100644 --- a/test/regress/regress0/rels/joinImg_1.cvc +++ b/test/regress/regress0/rels/joinImg_1.cvc @@ -1,5 +1,6 @@ % EXPECT: unsat OPTION "logic" "ALL_SUPPORTED"; +OPTION "sets-ext"; Atom: TYPE; x : SET OF [Atom, Atom]; y : SET OF [Atom, Atom]; diff --git a/test/regress/regress0/rels/joinImg_1_1.cvc b/test/regress/regress0/rels/joinImg_1_1.cvc index a7927f7e2..003770a1b 100644 --- a/test/regress/regress0/rels/joinImg_1_1.cvc +++ b/test/regress/regress0/rels/joinImg_1_1.cvc @@ -1,5 +1,6 @@ % EXPECT: sat OPTION "logic" "ALL_SUPPORTED"; +OPTION "sets-ext"; Atom: TYPE; x : SET OF [Atom, Atom]; y : SET OF [Atom, Atom]; diff --git a/test/regress/regress0/rels/joinImg_2.cvc b/test/regress/regress0/rels/joinImg_2.cvc index bbf57629b..a4acfe6c6 100644 --- a/test/regress/regress0/rels/joinImg_2.cvc +++ b/test/regress/regress0/rels/joinImg_2.cvc @@ -1,5 +1,6 @@ % EXPECT: unsat OPTION "logic" "ALL_SUPPORTED"; +OPTION "sets-ext"; Atom: TYPE; x : SET OF [Atom, Atom]; y : SET OF [Atom, Atom]; diff --git a/test/regress/regress0/rels/joinImg_2_1.cvc b/test/regress/regress0/rels/joinImg_2_1.cvc index b38bfab06..03f88be37 100644 --- a/test/regress/regress0/rels/joinImg_2_1.cvc +++ b/test/regress/regress0/rels/joinImg_2_1.cvc @@ -1,5 +1,6 @@ % EXPECT: sat OPTION "logic" "ALL_SUPPORTED"; +OPTION "sets-ext"; Atom: TYPE; x : SET OF [Atom, Atom]; y : SET OF [Atom, Atom]; @@ -21,4 +22,4 @@ ASSERT y = {(f, g), (b, c), (d, e), (c, e)}; ASSERT x = {(f, g), (b, c), (d, e), (c, e)}; ASSERT (NOT(a = b)) OR (NOT(a = f)); -CHECKSAT;
\ No newline at end of file +CHECKSAT; diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index c8e416a42..de2170768 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -86,7 +86,9 @@ TESTS = \ sets-poly-nonint.smt2 \ int-real-univ.smt2 \ int-real-univ-unsat.smt2 \ - sets-tuple-poly.cvc + sets-tuple-poly.cvc \ + arjun-set-univ.cvc \ + univ-set-uf-elim.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/sets/arjun-set-univ.cvc b/test/regress/regress0/sets/arjun-set-univ.cvc new file mode 100644 index 000000000..3c35a62a5 --- /dev/null +++ b/test/regress/regress0/sets/arjun-set-univ.cvc @@ -0,0 +1,8 @@ +% EXPECT: Extended set operators are not supported in default mode, try --sets-ext. +% EXIT: 1 +OPTION "produce-models" true; +x,y,z : SET OF BOOLEAN; +ASSERT x = {TRUE}; +ASSERT y = {FALSE}; +CHECKSAT z = ~ y; +COUNTERMODEL; diff --git a/test/regress/regress0/sets/univ-set-uf-elim.smt2 b/test/regress/regress0/sets/univ-set-uf-elim.smt2 new file mode 100644 index 000000000..a22f2a44f --- /dev/null +++ b/test/regress/regress0/sets/univ-set-uf-elim.smt2 @@ -0,0 +1,16 @@ +; EXPECT: (error "Extended set operators are not supported in default mode, try --sets-ext.") +; EXIT: 1 +(set-logic ALL) +(declare-fun a () Int) +(declare-fun f ((Set Bool)) Int) +(declare-fun s () (Set Bool)) + +(assert (member true s)) +(assert (member false s)) +(assert (= a (f (as univset (Set Bool))))) + +(assert (= (f (as emptyset (Set Bool))) 1)) +(assert (= (f (singleton true)) 2)) +(assert (= (f (singleton false)) 3)) +(assert (= (f (union (singleton true) (singleton false))) 4)) +(check-sat) |