Merge pull request #22 from kbansal/sets-model

Sets model

16 files changed, 121 insertions, 12 deletions

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 32a96ec21..fe53838be 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -53,6 +53,8 @@ TESTS =	\
 	jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 \
 	sets-sample.smt2 \
 	eqtest.smt2 \
+	mar2014/lemmabug-ListElts317minimized.smt2 \
+	mar2014/sharing-preregister.smt2 \
 	emptyset.smt2 \
 	error2.smt2
 
diff --git a/test/regress/regress0/sets/error1.smt2 b/test/regress/regress0/sets/error1.smt2
index c4b3dd551..1241b117f 100644
--- a/test/regress/regress0/sets/error1.smt2
+++ b/test/regress/regress0/sets/error1.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic QF_UFLIA_SETS)
 (set-info :status sat)
diff --git a/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2
index 290ee95d5..7a8661e4d 100644
--- a/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2
+++ b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2
index bcc4c33da..0aa6c88ae 100644
--- a/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2
+++ b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2
index 5a44c0344..35110d831 100644
--- a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2
+++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2
index 67d64bd05..d0fda8b86 100644
--- a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2
+++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2
new file mode 100644
index 000000000..1ea3ea6b5
--- /dev/null
+++ b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2
@@ -0,0 +1,89 @@
+; EXPECT: sat
+
+; Observed behavior:
+;   --check-model failed for set-term (union (z3f69 z3v151) (setenum z3v143))
+; with different set of elements in the model for representative and the node
+; itself.
+;
+; Issue:
+;   The trouble with data structure being mainted to ensure that things
+; for which lemmas have been generated are not generated again. This
+; data structure (d_pendingEverInserted) needs to be user context
+; dependent. The bug was in the sequence of steps from requesting that
+; a lemma be generated to when it actually was. Sequence was:
+; addToPending (and also adds to pending ever inserted) ->
+; isComplete (might remove things from pending if requirment met in other ways) ->
+; getLemma (actually generated the lemma, if requirement not already met)
+;
+; Resolution:
+;   adding terms to d_pendingEverInserted was moved from addToPending()
+; to getLemma().
+
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status sat)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+
+(declare-fun z3v58 () Int)
+(declare-fun z3v59 () Int)
+(assert (distinct z3v58 z3v59))
+
+(declare-fun z3f60 (Int) Bool)
+(declare-fun z3v61 () Int)
+(declare-fun z3f62 (Int) Int)
+(declare-fun z3v63 () Int)
+(declare-fun z3v64 () Int)
+(declare-fun z3v67 () Int)
+(declare-fun z3f68 (Int) Int)
+(declare-fun z3f69 (Int) mySet)
+(declare-fun z3f70 (Int) mySet)
+(declare-fun z3f71 (Int) Bool)
+(declare-fun z3v90 () Int)
+(declare-fun z3v91 () Int)
+(declare-fun z3f92 (Int Int) Int)
+(declare-fun z3v140 () Int)
+(declare-fun z3v141 () Int)
+(declare-fun z3v142 () Int)
+(declare-fun z3v143 () Int)
+(declare-fun z3v144 () Int)
+(declare-fun z3v145 () Int)
+(declare-fun z3v147 () Int)
+(declare-fun z3v150 () Int)
+(declare-fun z3v151 () Int)
+(declare-fun z3v152 () Int)
+
+(assert (not (= (z3f69 z3v152)
+                (z3f69 z3v140))))
+
+(assert (= (z3f69 z3v151)
+           (smt_set_cup (z3f69 z3v141)
+                        (z3f69 z3v140))))
+
+(assert (= (z3f69 z3v152)
+           (smt_set_cup (setenum z3v143) (z3f69 z3v151))))
+
+(assert (= (z3f70 z3v152)
+           (smt_set_cup (setenum z3v143) (z3f70 z3v151))))
+
+(assert (and
+        (= (z3f69 z3v142)
+           (smt_set_cup (setenum z3v143) (z3f69 z3v141)))
+        (= (z3f70 z3v142)
+           (smt_set_cup (setenum z3v143) (z3f70 z3v141)))
+         (= z3v142 (z3f92 z3v143 z3v141))
+         (= z3v142 z3v144)
+         (= (z3f62 z3v61) z3v61)
+         (= (z3f62 z3v63) z3v63)
+         )
+        )
+
+(check-sat)
diff --git a/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2
new file mode 100644
index 000000000..dc42abfa2
--- /dev/null
+++ b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2
@@ -0,0 +1,12 @@
+; EXPECT: unsat
+(set-logic QF_UFLIA_SETS)
+(set-info :status sat)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun x () (Set Int))
+(declare-fun y () (Set Int))
+(assert (= x (setenum a)))
+(assert (= y (setenum b)))
+(assert (not (= x y)))
+(assert (and (< 1 a) (< a 3) (< 1 b) (< b 3)))
+(check-sat)
diff --git a/test/regress/regress0/sets/sets-new.smt2 b/test/regress/regress0/sets/sets-new.smt2
index c85ae4837..accb09799 100644
--- a/test/regress/regress0/sets/sets-new.smt2
+++ b/test/regress/regress0/sets/sets-new.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress0/sets/sets-testlemma-ints.smt2 b/test/regress/regress0/sets/sets-testlemma-ints.smt2
new file mode 100644
index 000000000..9dd257401
--- /dev/null
+++ b/test/regress/regress0/sets/sets-testlemma-ints.smt2
@@ -0,0 +1,7 @@
+; EXPECT: sat
+(set-logic QF_UFLIA_SETS)
+(set-info :status sat)
+(declare-fun x () (Set Int))
+(declare-fun y () (Set Int))
+(assert (not (= x y)))
+(check-sat)
diff --git a/test/regress/regress0/sets/sets-testlemma-reals.smt2 b/test/regress/regress0/sets/sets-testlemma-reals.smt2
new file mode 100644
index 000000000..16e7780b4
--- /dev/null
+++ b/test/regress/regress0/sets/sets-testlemma-reals.smt2
@@ -0,0 +1,7 @@
+; EXPECT: sat
+(set-logic QF_UFLRA_SETS)
+(set-info :status sat)
+(declare-fun x () (Set Real))
+(declare-fun y () (Set Real))
+(assert (not (= x y)))
+(check-sat)
diff --git a/test/regress/regress0/sets/sets-testlemma.smt2 b/test/regress/regress0/sets/sets-testlemma.smt2
index 74ce72747..183f54242 100644
--- a/test/regress/regress0/sets/sets-testlemma.smt2
+++ b/test/regress/regress0/sets/sets-testlemma.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFBV_SETS)
 (set-info :status sat)
 (declare-fun x () (Set (_ BitVec 2)))
 (declare-fun y () (Set (_ BitVec 2)))
diff --git a/test/regress/regress0/sets/sets-union.smt2 b/test/regress/regress0/sets/sets-union.smt2
index 6f6d3e019..656a0bc88 100644
--- a/test/regress/regress0/sets/sets-union.smt2
+++ b/test/regress/regress0/sets/sets-union.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --no-check-model
+; COMMAND-LINE: --incremental
 ; EXPECT: sat
 ; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
diff --git a/test/regress/regress0/sets/union-1a-flip.smt2 b/test/regress/regress0/sets/union-1a-flip.smt2
index 59c2a2024..7bbe442e1 100644
--- a/test/regress/regress0/sets/union-1a-flip.smt2
+++ b/test/regress/regress0/sets/union-1a-flip.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --no-check-models
+; COMMAND-LINE: --incremental
 ; EXPECT: unsat
 ; EXPECT: sat
 
diff --git a/test/regress/regress0/sets/union-1b-flip.smt2 b/test/regress/regress0/sets/union-1b-flip.smt2
index 86fed459b..72c544553 100644
--- a/test/regress/regress0/sets/union-1b-flip.smt2
+++ b/test/regress/regress0/sets/union-1b-flip.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --no-check-models
+; COMMAND-LINE: --incremental
 ; EXPECT: unsat
 ; EXPECT: sat
 
diff --git a/test/regress/regress0/sets/union-2.smt2 b/test/regress/regress0/sets/union-2.smt2
index 32d949a53..e5e96be5a 100644
--- a/test/regress/regress0/sets/union-2.smt2
+++ b/test/regress/regress0/sets/union-2.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)