diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-09-09 14:47:53 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-02-21 07:25:13 -0500 |
| commit | 50c26544c83a71e87efa487e4af063b1b5647c0f (patch) | |
| tree | 82d4f3b2632a2cf06aff70550f37f80dc80d9543 /test | |
| parent | 53b8499f48a00dc876d56c76fbc79aafe5803529 (diff) | |
add new theory (sets)
Specification (smt2) -- as per this commit, subject to change
- Parameterized sort Set, e.g. (Set Int)
- Empty set constant (typed), use with "as" to specify the type, e.g.
(as emptyset (Set Int))
- Create a singleton set
(setenum X (Set X)) : creates singleton set
- Functions/operators
(union (Set X) (Set X) (Set X))
(intersection (Set X) (Set X) (Set X))
(setminus (Set X) (Set X) (Set X))
- Predicates
(in X (Set X) Bool) : membership
(subseteq (Set X) (Set X) Bool) : set containment
Diffstat (limited to 'test')
42 files changed, 3080 insertions, 88 deletions
diff --git a/test/Makefile.am b/test/Makefile.am index 8a7a5a0a7..1da15dc43 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -56,6 +56,7 @@ subdirs_to_check = \ regress/regress0/decision \ regress/regress0/fmf \ regress/regress0/strings \ + regress/regress0/sets \ regress/regress1 \ regress/regress1/arith \ regress/regress2 \ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index d7663e298..067b5d381 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,5 +1,5 @@ -SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings -DIST_SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings +SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets +DIST_SUBDIRS = $(SUBDIRS) #. arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets # don't override a BINARY imported from a personal.mk @mk_if@eq ($(BINARY),) diff --git a/test/regress/regress0/quantifiers/set8.smt2 b/test/regress/regress0/quantifiers/set8.smt2 index 684d94b7a..6e4a84672 100644 --- a/test/regress/regress0/quantifiers/set8.smt2 +++ b/test/regress/regress0/quantifiers/set8.smt2 @@ -1,26 +1,26 @@ (set-logic AUFLIA) -(set-info :source | Set theory. |) +(set-info :source | mySet theory. |) (set-info :smt-lib-version 2.0) (set-info :category "crafted") (set-info :status unsat) -(declare-sort Set 0) +(declare-sort mySet 0) (declare-sort Elem 0) -(declare-fun member (Elem Set) Bool) -(declare-fun subset (Set Set) Bool) -(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (=> (and (member ?x ?s1) (subset ?s1 ?s2)) (member ?x ?s2)))) -(assert (forall ((?s1 Set) (?s2 Set)) (=> (not (subset ?s1 ?s2)) (exists ((?x Elem)) (and (member ?x ?s1) (not (member ?x ?s2))))))) -(assert (forall ((?s1 Set) (?s2 Set)) (=> (forall ((?x Elem)) (=> (member ?x ?s1) (member ?x ?s2))) (subset ?s1 ?s2)))) -(declare-fun seteq (Set Set) Bool) -(assert (forall ((?s1 Set) (?s2 Set)) (= (seteq ?s1 ?s2) (= ?s1 ?s2)))) -(assert (forall ((?s1 Set) (?s2 Set)) (= (seteq ?s1 ?s2) (and (subset ?s1 ?s2) (subset ?s2 ?s1))))) -(declare-fun union (Set Set) Set) -(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (member ?x (union ?s1 ?s2)) (or (member ?x ?s1) (member ?x ?s2))))) -(declare-fun intersection (Set Set) Set) -(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (member ?x (intersection ?s1 ?s2)) (and (member ?x ?s1) (member ?x ?s2))))) -(declare-fun difference (Set Set) Set) -(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (member ?x (difference ?s1 ?s2)) (and (member ?x ?s1) (not (member ?x ?s2)))))) -(declare-fun a () Set) -(declare-fun b () Set) -(assert (not (seteq (intersection a b) (intersection b a)))) +(declare-fun member (Elem mySet) Bool) +(declare-fun subset (mySet mySet) Bool) +(assert (forall ((?x Elem) (?s1 mySet) (?s2 mySet)) (=> (and (member ?x ?s1) (subset ?s1 ?s2)) (member ?x ?s2)))) +(assert (forall ((?s1 mySet) (?s2 mySet)) (=> (not (subset ?s1 ?s2)) (exists ((?x Elem)) (and (member ?x ?s1) (not (member ?x ?s2))))))) +(assert (forall ((?s1 mySet) (?s2 mySet)) (=> (forall ((?x Elem)) (=> (member ?x ?s1) (member ?x ?s2))) (subset ?s1 ?s2)))) +(declare-fun seteq (mySet mySet) Bool) +(assert (forall ((?s1 mySet) (?s2 mySet)) (= (seteq ?s1 ?s2) (= ?s1 ?s2)))) +(assert (forall ((?s1 mySet) (?s2 mySet)) (= (seteq ?s1 ?s2) (and (subset ?s1 ?s2) (subset ?s2 ?s1))))) +(declare-fun myunion (mySet mySet) mySet) +(assert (forall ((?x Elem) (?s1 mySet) (?s2 mySet)) (= (member ?x (myunion ?s1 ?s2)) (or (member ?x ?s1) (member ?x ?s2))))) +(declare-fun myintersection (mySet mySet) mySet) +(assert (forall ((?x Elem) (?s1 mySet) (?s2 mySet)) (= (member ?x (myintersection ?s1 ?s2)) (and (member ?x ?s1) (member ?x ?s2))))) +(declare-fun difference (mySet mySet) mySet) +(assert (forall ((?x Elem) (?s1 mySet) (?s2 mySet)) (= (member ?x (difference ?s1 ?s2)) (and (member ?x ?s1) (not (member ?x ?s2)))))) +(declare-fun a () mySet) +(declare-fun b () mySet) +(assert (not (seteq (myintersection a b) (myintersection b a)))) (check-sat) (exit) diff --git a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 index 9bd49f714..56228e082 100644 --- a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 +++ b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 @@ -2,124 +2,124 @@ (set-logic AUFLIA) (set-info :status unsat) -;; don't use a datatypes for currently focusing in uf +;; don't use a datatypes for currently focusing my_in uf (declare-sort elt 0) (declare-sort set 0) -(declare-fun in (elt set) Bool) +(declare-fun my_in (elt set) Bool) ;;;;;;;;;;;;;;;;;;;; ;; inter (declare-fun inter (set set) set) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) () () - ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2))) + ((my_in ?s (inter ?t1 ?t2))) (and (my_in ?s ?t1) (my_in ?s ?t2))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) ) + (((inter ?t1 ?t2))) () ((not (my_in ?s ?t1))) (not (my_in ?s (inter ?t1 ?t2))) ) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) ) + (((inter ?t1 ?t2))) () ((not (my_in ?s ?t2))) (not (my_in ?s (inter ?t1 ?t2))) ) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) ) + () () ((not (my_in ?s (inter ?t1 ?t2))) (my_in ?s ?t1)) (not (my_in ?s ?t2)) ) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1))) + () () ((not (my_in ?s (inter ?t1 ?t2))) (my_in ?s ?t2)) (not (my_in ?s ?t1))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) ) + (((inter ?t1 ?t2))) () ((my_in ?s ?t1) (my_in ?s ?t2)) (my_in ?s (inter ?t1 ?t2)) ) ;;;;;;;;;;;;;;;;; ;; union -(declare-fun union (set set) set) +(declare-fun my_union (set set) set) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2)))) + () () ((not (my_in ?s (my_union ?t1 ?t2)))) (and (not (my_in ?s ?t1)) (not (my_in ?s ?t2)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((union ?t1 ?t2))) () ((in ?s ?t1)) (in ?s (union ?t1 ?t2))) + (((my_union ?t1 ?t2))) () ((my_in ?s ?t1)) (my_in ?s (my_union ?t1 ?t2))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((union ?t1 ?t2))) () ((in ?s ?t2)) (in ?s (union ?t1 ?t2))) + (((my_union ?t1 ?t2))) () ((my_in ?s ?t2)) (my_in ?s (my_union ?t1 ?t2))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2)) + () () ((my_in ?s (my_union ?t1 ?t2)) (not (my_in ?s ?t1))) (my_in ?s ?t2)) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1)) + () () ((my_in ?s (my_union ?t1 ?t2)) (not (my_in ?s ?t2))) (my_in ?s ?t1)) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((union ?t1 ?t2))) () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2)))) + (((my_union ?t1 ?t2))) () ((not (my_in ?s ?t1)) (not (my_in ?s ?t2))) (not (my_in ?s (my_union ?t1 ?t2)))) ;;;;;;;;;;;;;;;;;;;; ;; diff (declare-fun diff (set set) set) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2)))) + () () ((my_in ?s (diff ?t1 ?t2))) (and (my_in ?s ?t1) (not (my_in ?s ?t2)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((diff ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) ) + (((diff ?t1 ?t2))) () ((not (my_in ?s ?t1))) (not (my_in ?s (diff ?t1 ?t2))) ) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((diff ?t1 ?t2))) () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2)))) + (((diff ?t1 ?t2))) () ((my_in ?s ?t2)) (not (my_in ?s (diff ?t1 ?t2)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2)) + () () ((not (my_in ?s (diff ?t1 ?t2))) (my_in ?s ?t1)) (my_in ?s ?t2)) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1))) + () () ((not (my_in ?s (diff ?t1 ?t2))) (not (my_in ?s ?t2))) (not (my_in ?s ?t1))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((diff ?t1 ?t2))) () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) ) + (((diff ?t1 ?t2))) () ((my_in ?s ?t1) (not (my_in ?s ?t2))) (my_in ?s (diff ?t1 ?t2)) ) ;;;;;;;;;;;;;;;; ;;sing (declare-fun sing (elt) set) (assert-propagation ((?s elt)) - (((sing ?s))) () () (in ?s (sing ?s)) ) + (((sing ?s))) () () (my_in ?s (sing ?s)) ) (assert-propagation ((?s elt) (?t1 elt)) - () () ((in ?s (sing ?t1))) (= ?s ?t1)) + () () ((my_in ?s (sing ?t1))) (= ?s ?t1)) (assert-propagation ((?s elt) (?t1 elt)) - () () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1))) + () () ((not (my_in ?s (sing ?t1)))) (not (= ?s ?t1))) ;;;;;;;;;;;;;;;;;;; ;; fullfiling runned at Full effort (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1)))) + () () ((my_in ?s (my_union ?t1 ?t2))) (or (my_in ?s ?t1) (not (my_in ?s ?t1)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2)))) + (((inter ?t1 ?t2))) () ((my_in ?s ?t1)) (or (my_in ?s ?t2) (not (my_in ?s ?t2)))) (assert-propagation ((?t1 set) (?t2 set)) - () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2))))) + () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (my_in ?e ?t1) (not (my_in ?e ?t2))) (and (not (my_in ?e ?t1)) (my_in ?e ?t2))))) ;;;;;;;;;;;;;;;;;;; ;; shortcut (declare-fun subset (set set) Bool) (assert-reduction ((?t1 set) (?t2 set)) - () () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2)) + () () ((subset ?t1 ?t2)) (= (my_union ?t1 ?t2) ?t2)) (declare-fun e () elt) (declare-fun t1 () set) (declare-fun t2 () set) (declare-fun t3 () set) -;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e (union t1 t1))))) -;;(assert (not (=> (in e (union t1 t1)) (in e t1)))) +;;(assert (not (=> (my_in e (inter (my_union t1 t2) (my_union t1 t1))) (my_in e (my_union t1 t1))))) +;;(assert (not (=> (my_in e (my_union t1 t1)) (my_in e t1)))) ;; hyp -;;(assert (=> (in e (union t1 t1)) (in e t1))) +;;(assert (=> (my_in e (my_union t1 t1)) (my_in e t1))) -;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e t1)))) +;;(assert (not (=> (my_in e (inter (my_union t1 t2) (my_union t1 t1))) (my_in e t1)))) -;;(assert (or (and (not (in e (union t1 (union t2 t3)))) (in e (union (union t1 t2) t3))) (and (in e (union t1 (union t2 t3))) (not (in e (union (union t1 t2) t3))))) ) -(assert (not (= (union t1 (union t2 t3)) (union (union t1 t2) t3))) ) +;;(assert (or (and (not (my_in e (my_union t1 (my_union t2 t3)))) (my_in e (my_union (my_union t1 t2) t3))) (and (my_in e (my_union t1 (my_union t2 t3))) (not (my_in e (my_union (my_union t1 t2) t3))))) ) +(assert (not (= (my_union t1 (my_union t2 t3)) (my_union (my_union t1 t2) t3))) ) (check-sat) diff --git a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 index 4d65ffac5..2a7e59d6e 100644 --- a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 +++ b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 @@ -2,11 +2,11 @@ (set-logic AUFLIA) (set-info :status sat) -;; don't use a datatypes for currently focusing in uf +;; don't use a datatypes for currently focusing my_in uf (declare-sort elt 0) (declare-sort set 0) -(declare-fun in (elt set) Bool) +(declare-fun my_in (elt set) Bool) ;;;;;;;;;;;;;;;;;;;; @@ -14,112 +14,112 @@ (declare-fun inter (set set) set) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) () () - ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2))) + ((my_in ?s (inter ?t1 ?t2))) (and (my_in ?s ?t1) (my_in ?s ?t2))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) ) + (((inter ?t1 ?t2))) () ((not (my_in ?s ?t1))) (not (my_in ?s (inter ?t1 ?t2))) ) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) ) + (((inter ?t1 ?t2))) () ((not (my_in ?s ?t2))) (not (my_in ?s (inter ?t1 ?t2))) ) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) ) + () () ((not (my_in ?s (inter ?t1 ?t2))) (my_in ?s ?t1)) (not (my_in ?s ?t2)) ) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1))) + () () ((not (my_in ?s (inter ?t1 ?t2))) (my_in ?s ?t2)) (not (my_in ?s ?t1))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) ) + (((inter ?t1 ?t2))) () ((my_in ?s ?t1) (my_in ?s ?t2)) (my_in ?s (inter ?t1 ?t2)) ) ;;;;;;;;;;;;;;;;; ;; union -(declare-fun union (set set) set) +(declare-fun my_union (set set) set) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2)))) + () () ((not (my_in ?s (my_union ?t1 ?t2)))) (and (not (my_in ?s ?t1)) (not (my_in ?s ?t2)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((union ?t1 ?t2))) () ((in ?s ?t1)) (in ?s (union ?t1 ?t2))) + (((my_union ?t1 ?t2))) () ((my_in ?s ?t1)) (my_in ?s (my_union ?t1 ?t2))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((union ?t1 ?t2))) () ((in ?s ?t2)) (in ?s (union ?t1 ?t2))) + (((my_union ?t1 ?t2))) () ((my_in ?s ?t2)) (my_in ?s (my_union ?t1 ?t2))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2)) + () () ((my_in ?s (my_union ?t1 ?t2)) (not (my_in ?s ?t1))) (my_in ?s ?t2)) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1)) + () () ((my_in ?s (my_union ?t1 ?t2)) (not (my_in ?s ?t2))) (my_in ?s ?t1)) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((union ?t1 ?t2))) () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2)))) + (((my_union ?t1 ?t2))) () ((not (my_in ?s ?t1)) (not (my_in ?s ?t2))) (not (my_in ?s (my_union ?t1 ?t2)))) ;;;;;;;;;;;;;;;;;;;; ;; diff (declare-fun diff (set set) set) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2)))) + () () ((my_in ?s (diff ?t1 ?t2))) (and (my_in ?s ?t1) (not (my_in ?s ?t2)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((diff ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) ) + (((diff ?t1 ?t2))) () ((not (my_in ?s ?t1))) (not (my_in ?s (diff ?t1 ?t2))) ) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((diff ?t1 ?t2))) () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2)))) + (((diff ?t1 ?t2))) () ((my_in ?s ?t2)) (not (my_in ?s (diff ?t1 ?t2)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2)) + () () ((not (my_in ?s (diff ?t1 ?t2))) (my_in ?s ?t1)) (my_in ?s ?t2)) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1))) + () () ((not (my_in ?s (diff ?t1 ?t2))) (not (my_in ?s ?t2))) (not (my_in ?s ?t1))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((diff ?t1 ?t2))) () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) ) + (((diff ?t1 ?t2))) () ((my_in ?s ?t1) (not (my_in ?s ?t2))) (my_in ?s (diff ?t1 ?t2)) ) ;;;;;;;;;;;;;;;; ;;sing (declare-fun sing (elt) set) (assert-propagation ((?s elt)) - (((sing ?s))) () () (in ?s (sing ?s)) ) + (((sing ?s))) () () (my_in ?s (sing ?s)) ) (assert-propagation ((?s elt) (?t1 elt)) - () () ((in ?s (sing ?t1))) (= ?s ?t1)) + () () ((my_in ?s (sing ?t1))) (= ?s ?t1)) (assert-propagation ((?s elt) (?t1 elt)) - () () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1))) + () () ((not (my_in ?s (sing ?t1)))) (not (= ?s ?t1))) ;;;;;;;;;;;;;;;;;;; ;; fullfiling runned at Full effort (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1)))) + () () ((my_in ?s (my_union ?t1 ?t2))) (or (my_in ?s ?t1) (not (my_in ?s ?t1)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2)))) + (((inter ?t1 ?t2))) () ((my_in ?s ?t1)) (or (my_in ?s ?t2) (not (my_in ?s ?t2)))) (assert-propagation ((?t1 set) (?t2 set)) - () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2))))) + () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (my_in ?e ?t1) (not (my_in ?e ?t2))) (and (not (my_in ?e ?t1)) (my_in ?e ?t2))))) ;;;;;;;;;;;;;;;;;;; ;; shortcut (declare-fun subset (set set) Bool) (assert-reduction ((?t1 set) (?t2 set)) - () () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2)) + () () ((subset ?t1 ?t2)) (= (my_union ?t1 ?t2) ?t2)) (declare-fun e () elt) (declare-fun t1 () set) (declare-fun t2 () set) (declare-fun t3 () set) -;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e (union t1 t1))))) -;;(assert (not (=> (in e (union t1 t1)) (in e t1)))) +;;(assert (not (=> (my_in e (inter (my_union t1 t2) (my_union t1 t1))) (my_in e (my_union t1 t1))))) +;;(assert (not (=> (my_in e (my_union t1 t1)) (my_in e t1)))) ;; hyp -;;(assert (=> (in e (union t1 t1)) (in e t1))) +;;(assert (=> (my_in e (my_union t1 t1)) (my_in e t1))) -;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e t1)))) +;;(assert (not (=> (my_in e (inter (my_union t1 t2) (my_union t1 t1))) (my_in e t1)))) -(assert (or (and (not (in e (union t1 (union t2 t3)))) (in e (union (union t1 t2) t3))) (and (in e (union t1 (union t2 t3))) (not (in e (union (union t2 t2) t3))))) ) +(assert (or (and (not (my_in e (my_union t1 (my_union t2 t3)))) (my_in e (my_union (my_union t1 t2) t3))) (and (my_in e (my_union t1 (my_union t2 t3))) (not (my_in e (my_union (my_union t2 t2) t3))))) ) (check-sat) diff --git a/test/regress/regress0/sets/Makefile b/test/regress/regress0/sets/Makefile new file mode 100644 index 000000000..67ae35206 --- /dev/null +++ b/test/regress/regress0/sets/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../.. +srcdir = test/regress/regress0/sets + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am new file mode 100644 index 000000000..f040a6cd0 --- /dev/null +++ b/test/regress/regress0/sets/Makefile.am @@ -0,0 +1,75 @@ +# don't override a BINARY imported from a personal.mk +@mk_if@eq ($(BINARY),) +@mk_empty@BINARY = cvc4 +end@mk_if@ + +LOG_COMPILER = @srcdir@/../../run_regression +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) + +if AUTOMAKE_1_11 +# old-style (pre-automake 1.12) test harness +TESTS_ENVIRONMENT = \ + $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) +endif + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" +TESTS = \ + union-1b-flip.smt2 \ + sets-sharing.smt2 \ + union-1a-flip.smt2 \ + copy_check_heap_access_33_4.smt2 \ + rec_copy_loop_check_heap_access_43_4.smt2 \ + sets-testlemma.smt2 \ + jan24/insert_invariant_37_2.smt2 \ + jan24/deepmeas0.hs.fqout.cvc4.47.smt2 \ + jan24/deepmeas0.hs.fqout.small.smt2 \ + jan24/remove_check_free_31_6.smt2 \ + sets-inter.smt2 \ + sets-equal.smt2 \ + union-2.smt2 \ + jan27/deepmeas0.hs.fqout.cvc4.41.smt2 \ + jan27/ListConcat.hs.fqout.cvc4.177.smt2 \ + jan27/ListConcat.hs.fqout.177minimized.smt2 \ + jan27/ListElem.hs.fqout.cvc4.38.smt2 \ + feb3/ListElts.hs.fqout.cvc4.317.smt2 \ + setel-eq.smt2 \ + sets-new.smt2 \ + jan30/UniqueZipper.hs.fqout.minimized10.smt2 \ + jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 \ + jan30/UniqueZipper.hs.fqout.minimized1832.smt2 \ + jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 \ + emptyset.smt2 \ + sets-union.smt2 \ + error2.smt2 \ + union-1b.smt2 \ + union-1a.smt2 \ + error1.smt2 \ + jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 \ + jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 \ + sets-sample.smt2 \ + eqtest.smt2 \ + emptyset.smt2 \ + error2.smt2 + +EXTRA_DIST = $(TESTS) + +#if CVC4_BUILD_PROFILE_COMPETITION +#else +#TESTS += \ +# error.cvc +#endif +# +# and make sure to distribute it +#EXTRA_DIST += \ +# error.cvc + +# synonyms for "check" +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 b/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 new file mode 100644 index 000000000..a8eccf4ad --- /dev/null +++ b/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 @@ -0,0 +1,133 @@ +(set-option :print-success false) +(set-logic AUFLIA_SETS) +(set-info :status unsat) +(declare-sort Loc 0) +(define-sort SetLoc () (Set Loc)) +(define-sort SetInt () (Set Int)) +(declare-sort FldLoc 0) +(declare-sort FldInt 0) +(declare-fun null$0 () Loc) +(declare-fun read$0 (FldInt Loc) Int) +(declare-fun read$1 (FldLoc Loc) Loc) +(declare-fun Btwn$0 (FldLoc Loc Loc Loc) Bool) +(declare-fun Alloc$0 () SetLoc) +(declare-fun Alloc_1$0 () SetLoc) +(declare-fun Axiom_1$0 () Bool) +(declare-fun FP$0 () SetLoc) +(declare-fun FP_1$0 () SetLoc) +(declare-fun FP_Caller$0 () SetLoc) +(declare-fun FP_Caller_1$0 () SetLoc) +(declare-fun cp_2$0 () Loc) +(declare-fun curr_2$0 () Loc) +(declare-fun data$0 () FldInt) +(declare-fun lst$0 () Loc) +(declare-fun next$0 () FldLoc) +(declare-fun res_1$0 () Loc) +(declare-fun sk_?X_4$0 () SetLoc) +(declare-fun slseg_domain$0 (FldInt FldLoc Loc Loc) SetLoc) +(declare-fun slseg_struct$0 (SetLoc FldInt FldLoc Loc Loc) Bool) +(declare-fun tmp_2$0 () Loc) + +(assert (! (forall ((?y Loc)) + (or (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y) + (Btwn$0 next$0 null$0 (read$1 next$0 null$0) ?y))) + :named btwn_reach_1)) + +(assert (! (forall ((?y Loc)) + (or (not (= (read$1 next$0 null$0) null$0)) + (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y))) + :named btwn_cycl_1)) + +(assert (! (Btwn$0 next$0 null$0 (read$1 next$0 null$0) (read$1 next$0 null$0)) + :named btwn_step_1)) + +(assert (! (forall ((l1 Loc) (l2 Loc)) + (or (not Axiom_1$0) + (or (<= (read$0 data$0 l1) (read$0 data$0 l2)) + (not (Btwn$0 next$0 l1 l2 null$0)) (not (in l1 sk_?X_4$0)) + (not (in l2 sk_?X_4$0))))) + :named sortedness_3)) + +(assert (! (= (read$1 next$0 null$0) null$0) :named read_null_1)) + +(assert (! (not (in tmp_2$0 Alloc$0)) :named new_31_11)) + +(assert (! (not (in null$0 Alloc$0)) :named initial_footprint_of_copy_23_11_2)) + +(assert (! (not (= lst$0 null$0)) :named if_else_26_6)) + +(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0)) + :named precondition_of_copy_23_11_4)) + +(assert (! (= sk_?X_4$0 FP$0) :named precondition_of_copy_23_11_5)) + +(assert (! (= res_1$0 tmp_2$0) :named assign_31_4)) + +(assert (! (= cp_2$0 res_1$0) :named assign_32_4)) + +(assert (! (= FP_1$0 (union FP$0 (setenum tmp_2$0))) :named assign_31_11)) + +(assert (! (or (and (Btwn$0 next$0 lst$0 null$0 null$0) Axiom_1$0) + (not (slseg_struct$0 sk_?X_4$0 data$0 next$0 lst$0 null$0))) + :named unnamed_3)) + +(assert (! (forall ((l1 Loc)) + (or + (and (Btwn$0 next$0 lst$0 l1 null$0) + (in l1 (slseg_domain$0 data$0 next$0 lst$0 null$0)) + (not (= l1 null$0))) + (and (or (= l1 null$0) (not (Btwn$0 next$0 lst$0 l1 null$0))) + (not (in l1 (slseg_domain$0 data$0 next$0 lst$0 null$0)))))) + :named slseg_footprint_2)) + +(assert (! (not (in curr_2$0 FP_1$0)) :named check_heap_access_33_4)) + +(assert (! (not (= tmp_2$0 null$0)) :named new_31_11_1)) + +(assert (! (slseg_struct$0 sk_?X_4$0 data$0 next$0 lst$0 null$0) + :named precondition_of_copy_23_11_6)) + +(assert (! (= sk_?X_4$0 (slseg_domain$0 data$0 next$0 lst$0 null$0)) + :named precondition_of_copy_23_11_7)) + +(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0)) + :named initial_footprint_of_copy_23_11_3)) + +(assert (! (= curr_2$0 lst$0) :named assign_30_4)) + +(assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_26_2_1)) + +(assert (! (= Alloc_1$0 (union Alloc$0 (setenum tmp_2$0))) :named assign_31_11_1)) + +(assert (! (forall ((?x Loc)) (Btwn$0 next$0 ?x ?x ?x)) :named btwn_refl_1)) + +(assert (! (forall ((?x Loc) (?y Loc)) (or (not (Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y))) + :named btwn_sndw_1)) + +(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) + (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?x ?z ?z)) + (Btwn$0 next$0 ?x ?y ?z) (Btwn$0 next$0 ?x ?z ?y))) + :named btwn_ord1_1)) + +(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) + (or (not (Btwn$0 next$0 ?x ?y ?z)) + (and (Btwn$0 next$0 ?x ?y ?y) (Btwn$0 next$0 ?y ?z ?z)))) + :named btwn_ord2_1)) + +(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) + (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?y ?z ?z)) + (Btwn$0 next$0 ?x ?z ?z))) + :named btwn_trn1_1)) + +(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc)) + (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?y ?u ?z)) + (and (Btwn$0 next$0 ?x ?y ?u) (Btwn$0 next$0 ?x ?u ?z)))) + :named btwn_trn2_1)) + +(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc)) + (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?x ?u ?y)) + (and (Btwn$0 next$0 ?x ?u ?z) (Btwn$0 next$0 ?u ?y ?z)))) + :named btwn_trn3_1)) + +(check-sat) +(exit) diff --git a/test/regress/regress0/sets/emptyset.smt2 b/test/regress/regress0/sets/emptyset.smt2 new file mode 100644 index 000000000..47fc25661 --- /dev/null +++ b/test/regress/regress0/sets/emptyset.smt2 @@ -0,0 +1,4 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(assert (in 5 (as emptyset (Set Int) ))) +(check-sat) diff --git a/test/regress/regress0/sets/eqtest.smt2 b/test/regress/regress0/sets/eqtest.smt2 new file mode 100644 index 000000000..02577b00a --- /dev/null +++ b/test/regress/regress0/sets/eqtest.smt2 @@ -0,0 +1,18 @@ +(set-logic QF_ALL_SUPPORTED) +(set-info :status unsat) +(declare-fun A () (Set Int) ) +(declare-fun B () (Set Int) ) +(declare-fun C () (Set Int) ) +(declare-fun D () (Set Int) ) +(declare-fun E () (Set Int) ) +(declare-fun F () (Set Int) ) +(declare-fun G () (Set Int) ) +(declare-fun H () (Set Int) ) +(declare-fun I () (Set Int) ) +(declare-fun x () Int) +(assert (in x (intersection (union A B) C))) +(assert (not (in x G))) +(assert (= (union A B) D)) +(assert (= C (intersection E F))) +(assert (and (= F H) (= G H) (= H I))) +(check-sat) diff --git a/test/regress/regress0/sets/error1.smt2 b/test/regress/regress0/sets/error1.smt2 new file mode 100644 index 000000000..c4b3dd551 --- /dev/null +++ b/test/regress/regress0/sets/error1.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic QF_UFLIA_SETS) +(set-info :status sat) +(declare-fun A () (Set Int)) +(declare-fun C () (Set Int)) +(declare-fun D () (Set Int)) +(declare-fun E () (Set Int)) +(set-info :status sat) + +(assert (= A (union D C))) +(assert (not (= A (union E A)))) + +(check-sat) diff --git a/test/regress/regress0/sets/error2.smt2 b/test/regress/regress0/sets/error2.smt2 new file mode 100644 index 000000000..ac678c552 --- /dev/null +++ b/test/regress/regress0/sets/error2.smt2 @@ -0,0 +1,4 @@ +(set-logic QF_ALL_SUPPORTED) +(set-info :status unsat) +(assert (= (as emptyset (Set Int)) (setenum 5))) +(check-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 new file mode 100644 index 000000000..290ee95d5 --- /dev/null +++ b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 @@ -0,0 +1,99 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(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 z3v73 () Int) +(declare-fun z3v76 () Int) +(declare-fun z3v79 () Int) +(declare-fun z3v82 () Int) +(declare-fun z3v84 () Int) +(declare-fun z3v85 () Int) +(declare-fun z3v86 () Int) +(declare-fun z3v89 () Int) +(declare-fun z3v90 () Int) +(declare-fun z3v91 () Int) +(declare-fun z3f92 (Int Int) Int) +(declare-fun z3v93 () Int) +(declare-fun z3v94 () Int) +(declare-fun z3f96 () Int) +(declare-fun z3v97 () Int) +(declare-fun z3v98 () Int) +(declare-fun z3v99 () Int) +(declare-fun z3v100 () Int) +(declare-fun z3v101 () Int) +(declare-fun z3v102 () Int) +(declare-fun z3v104 () Int) +(declare-fun z3v107 () Int) +(declare-fun z3v110 () Int) +(declare-fun z3v113 () Int) +(declare-fun z3v116 () Int) +(declare-fun z3v117 () Int) +(declare-fun z3v118 () Int) +(declare-fun z3v119 () Int) +(declare-fun z3v120 () Int) +(declare-fun z3v121 () Int) +(declare-fun z3v122 () Int) +(declare-fun z3v123 () Int) +(declare-fun z3v124 () Int) +(declare-fun z3v125 () Int) +(declare-fun z3v127 () Int) +(declare-fun z3v130 () Int) +(declare-fun z3v133 () Int) +(declare-fun z3v134 () Int) +(declare-fun z3v135 () Int) +(declare-fun z3v136 () Int) +(declare-fun z3v137 () 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 (= (z3f69 z3v152) (smt_set_cup (smt_set_add smt_set_emp z3v143) (z3f69 z3v151)))) +(assert (= (z3f70 z3v152) (smt_set_cup (smt_set_add smt_set_emp z3v143) (z3f70 z3v151)))) +(assert (= (z3f68 z3v152) (+ 1 (z3f68 z3v151)))) +(assert (= (z3f71 z3v152) false)) +(assert (and (>= (z3f68 z3v140) 0) (>= (z3f68 z3v141) 0) (>= (z3f68 z3v151) 0) (>= (z3f68 z3v142) 0) (= (z3f69 z3v142) (smt_set_cup (smt_set_add smt_set_emp z3v143) (z3f69 z3v141))) (= (z3f70 z3v142) (smt_set_cup (smt_set_add smt_set_emp z3v143) (z3f70 z3v141))) (= (z3f68 z3v142) (+ 1 (z3f68 z3v141))) (= (z3f71 z3v142) false) (= z3v142 (z3f92 z3v143 z3v141)) (>= (z3f68 z3v142) 0) (= z3v142 z3v144) (>= (z3f68 z3v142) 0) (>= (z3f68 z3v144) 0) (z3f60 z3v58) (= (z3f62 z3v61) z3v61) (= (z3f62 z3v63) z3v63) (not (z3f60 z3v59)) (= (z3f62 z3v64) z3v64))) +(assert (= (z3f69 z3v151) (smt_set_cup (z3f69 z3v140) (z3f69 z3v141)))) +(assert (= (z3f69 z3v151) (smt_set_cup (z3f69 z3v140) (z3f69 z3v140)))) +(assert (= (z3f69 z3v151) (smt_set_cup (z3f69 z3v141) (z3f69 z3v140)))) +(assert (smt_set_sub (z3f69 z3v151) (z3f69 z3v140))) +(assert (= (z3f69 z3v151) (z3f69 z3v140))) +(assert (<= z3v151 z3v140)) +(assert (>= z3v151 z3v140)) +(assert (<= (z3f68 z3v151) (z3f68 z3v140))) +(assert (>= (z3f68 z3v151) (z3f68 z3v141))) +(assert (>= (z3f68 z3v151) (z3f68 z3v140))) +(assert (= (z3f68 z3v151) (z3f68 z3v140))) +(assert (= z3v151 z3v140)) +(assert (>= (z3f68 z3v151) 0)) +(assert (not (= (z3f69 z3v152) (smt_set_cup (z3f69 z3v140) (z3f69 z3v140))))) +(check-sat) diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 new file mode 100644 index 000000000..b90563199 --- /dev/null +++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 @@ -0,0 +1,75 @@ +(set-logic QF_ALL_SUPPORTED) +(set-info :status unsat) +(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_dif ((s1 mySet) (s2 mySet)) mySet (setminus 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 z3v65 () Int) +(declare-fun z3v66 () Int) +(declare-fun z3f67 (Int) mySet) +(declare-fun z3v69 () Int) +(declare-fun z3f70 (Int) Int) +(declare-fun z3v76 () Int) +(declare-fun z3v77 () Int) +(declare-fun z3v78 () Int) +(declare-fun z3v79 () Int) +(declare-fun z3v80 () Int) +(declare-fun z3v81 () Int) +(declare-fun z3v82 () Int) +(declare-fun z3f83 (Int) Int) +(declare-fun z3f84 (Int) Int) +(declare-fun z3v85 () Int) +(declare-fun z3f86 (Int) Int) +(declare-fun z3f87 (Int Int) Int) +(declare-fun z3v88 () Int) +(declare-fun z3v89 () Int) +(declare-fun z3f90 (Int) mySet) +(declare-fun z3f91 (Int) Bool) +(declare-fun z3f92 (Int Int) Int) +(declare-fun z3v93 () Int) +(declare-fun z3v94 () Int) +(declare-fun z3v95 () Int) +(declare-fun z3v96 () Int) +(declare-fun z3v97 () Int) +(declare-fun z3v99 () Int) + +(assert (= z3v99 z3v89)) +(assert (>= (z3f70 z3v99) 0)) + +(assert (and (not (z3f60 z3v79)) + (not (z3f60 z3v79)) + (= z3v79 z3v80) + (= (z3f60 z3v79) + (= z3v76 z3v81)) + (= (z3f60 z3v80) + (= z3v76 z3v81)) + (= (z3f83 z3v82) z3v81) + (= (z3f91 z3v78) false) + (= z3v78 (z3f92 z3v88 z3v89)) + (= z3v82 z3v88) + (= (z3f67 z3v78) + (smt_set_cup (smt_set_add smt_set_emp (z3f83 z3v88)) + (z3f67 z3v89))) + (= (z3f62 z3v64) z3v64))) + +(assert (smt_set_mem z3v76 (z3f67 z3v78))) +(assert (<= z3v95 z3v93)) +(assert (>= z3v95 z3v93)) +(assert (not (smt_set_mem z3v76 (z3f67 z3v99)))) +(check-sat) diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 new file mode 100644 index 000000000..204af2f2d --- /dev/null +++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 @@ -0,0 +1,18 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-fun x () Int) +(declare-fun y () Int) + +(declare-fun S () (Set Int)) +(declare-fun T () (Set Int)) + +(assert (in x S)) + +(assert (= S (union T (setenum y)))) + +(assert (not (= x y))) + +(assert (not (in x T))) + +(check-sat) diff --git a/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2 b/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2 new file mode 100644 index 000000000..ad0a7e464 --- /dev/null +++ b/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2 @@ -0,0 +1,812 @@ +(set-option :print-success false) +(set-logic AUFLIA_SETS) +(set-info :status unsat) +(declare-sort Loc 0) +(define-sort SetLoc () (Set Loc)) +(define-sort SetInt () (Set Int)) +(declare-sort FldLoc 0) +(declare-sort FldInt 0) +(declare-fun null$0 () Loc) +(declare-fun read$0 (FldInt Loc) Int) +(declare-fun read$1 (FldLoc Loc) Loc) +(declare-fun Btwn$0 (FldLoc Loc Loc Loc) Bool) +(declare-fun Alloc$0 () SetLoc) +(declare-fun Axiom$0 () Bool) +(declare-fun FP$0 () SetLoc) +(declare-fun FP_Caller$0 () SetLoc) +(declare-fun FP_Caller_1$0 () SetLoc) +(declare-fun c1_2$0 () SetInt) +(declare-fun c2_2$0 () SetInt) +(declare-fun content$0 () SetInt) +(declare-fun curr_2$0 () Loc) +(declare-fun data$0 () FldInt) +(declare-fun lst$0 () Loc) +(declare-fun next$0 () FldLoc) +(declare-fun prev_2$0 () Loc) +(declare-fun sk_?X$0 () SetLoc) +(declare-fun sk_?X_1$0 () SetLoc) +(declare-fun sk_?X_2$0 () SetLoc) +(declare-fun sk_?X_3$0 () SetLoc) +(declare-fun sk_?X_4$0 () SetLoc) +(declare-fun sk_?X_5$0 () SetLoc) +(declare-fun sk_?e$0 () Int) +(declare-fun sk_?e_1$0 () Loc) +(declare-fun sk_?e_2$0 () Loc) +(declare-fun sk_?e_3$0 () Int) +(declare-fun sk_FP$0 () SetLoc) +(declare-fun sk_FP_1$0 () SetLoc) +(declare-fun sk_l1$0 () Loc) +(declare-fun sk_l1_1$0 () Loc) +(declare-fun sk_l2$0 () Loc) +(declare-fun sk_l2_1$0 () Loc) +(declare-fun sorted_set_c$0 (FldInt FldLoc Loc Loc) SetInt) +(declare-fun sorted_set_domain$0 (FldInt FldLoc Loc Loc) SetLoc) +(declare-fun sorted_set_struct$0 (SetLoc FldInt FldLoc Loc Loc SetInt) Bool) +(declare-fun val$0 () Int) +(declare-fun witness$0 (Int SetInt) Loc) + +(assert (! (forall ((?y Loc)) + (or (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y) + (Btwn$0 next$0 null$0 (read$1 next$0 null$0) ?y))) + :named btwn_reach)) + +(assert (! (forall ((?y Loc)) + (or (not (= (read$1 next$0 null$0) null$0)) + (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y))) + :named btwn_cycl)) + +(assert (! (Btwn$0 next$0 null$0 (read$1 next$0 null$0) (read$1 next$0 null$0)) + :named btwn_step)) + +(assert (! (forall ((l1 Loc) (l2 Loc)) + (or (not Axiom$0) + (or (= l1 l2) (< (read$0 data$0 l1) (read$0 data$0 l2)) + (not (Btwn$0 next$0 l1 l2 null$0)) (not (in l1 sk_?X$0)) + (not (in l2 sk_?X$0))))) + :named strict_sortedness)) + +(assert (! (forall ((l1 Loc)) + (or (= l1 null$0) + (in (read$0 data$0 l1) + (sorted_set_c$0 data$0 next$0 lst$0 null$0)) + (not (Btwn$0 next$0 lst$0 l1 null$0)))) + :named sorted_set_1)) + +(assert (! (and + (or + (= + (witness$0 (read$0 data$0 curr_2$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0)) + null$0) + (in (read$0 data$0 curr_2$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0))) + (or + (and + (= (read$0 data$0 curr_2$0) + (read$0 data$0 + (witness$0 (read$0 data$0 curr_2$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) + (in + (witness$0 (read$0 data$0 curr_2$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0)) + (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) + (not + (in (read$0 data$0 curr_2$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) + :named sorted_set_2)) + +(assert (! (and + (or + (= + (witness$0 (read$0 data$0 prev_2$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0)) + null$0) + (in (read$0 data$0 prev_2$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0))) + (or + (and + (= (read$0 data$0 prev_2$0) + (read$0 data$0 + (witness$0 (read$0 data$0 prev_2$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) + (in + (witness$0 (read$0 data$0 prev_2$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0)) + (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) + (not + (in (read$0 data$0 prev_2$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) + :named sorted_set_2_1)) + +(assert (! (and + (or + (= + (witness$0 (read$0 data$0 sk_l1$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0)) + null$0) + (in (read$0 data$0 sk_l1$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0))) + (or + (and + (= (read$0 data$0 sk_l1$0) + (read$0 data$0 + (witness$0 (read$0 data$0 sk_l1$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) + (in + (witness$0 (read$0 data$0 sk_l1$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0)) + (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) + (not + (in (read$0 data$0 sk_l1$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) + :named sorted_set_2_2)) + +(assert (! (and + (or + (= + (witness$0 (read$0 data$0 sk_l1_1$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0)) + null$0) + (in (read$0 data$0 sk_l1_1$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0))) + (or + (and + (= (read$0 data$0 sk_l1_1$0) + (read$0 data$0 + (witness$0 (read$0 data$0 sk_l1_1$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) + (in + (witness$0 (read$0 data$0 sk_l1_1$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0)) + (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) + (not + (in (read$0 data$0 sk_l1_1$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) + :named sorted_set_2_3)) + +(assert (! (and + (or + (= + (witness$0 (read$0 data$0 sk_l2$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0)) + null$0) + (in (read$0 data$0 sk_l2$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0))) + (or + (and + (= (read$0 data$0 sk_l2$0) + (read$0 data$0 + (witness$0 (read$0 data$0 sk_l2$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) + (in + (witness$0 (read$0 data$0 sk_l2$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0)) + (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) + (not + (in (read$0 data$0 sk_l2$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) + :named sorted_set_2_4)) + +(assert (! (and + (or + (= + (witness$0 (read$0 data$0 sk_l2_1$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0)) + null$0) + (in (read$0 data$0 sk_l2_1$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0))) + (or + (and + (= (read$0 data$0 sk_l2_1$0) + (read$0 data$0 + (witness$0 (read$0 data$0 sk_l2_1$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) + (in + (witness$0 (read$0 data$0 sk_l2_1$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0)) + (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) + (not + (in (read$0 data$0 sk_l2_1$0) + (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) + :named sorted_set_2_5)) + +(assert (! (and + (or + (= + (witness$0 sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0)) + null$0) + (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))) + (or + (and + (= sk_?e$0 + (read$0 data$0 + (witness$0 sk_?e$0 + (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) + (in + (witness$0 sk_?e$0 + (sorted_set_c$0 data$0 next$0 lst$0 null$0)) + (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) + (not (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) + :named sorted_set_2_6)) + +(assert (! (and + (or + (= + (witness$0 sk_?e_3$0 + (sorted_set_c$0 data$0 next$0 lst$0 null$0)) + null$0) + (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))) + (or + (and + (= sk_?e_3$0 + (read$0 data$0 + (witness$0 sk_?e_3$0 + (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) + (in + (witness$0 sk_?e_3$0 + (sorted_set_c$0 data$0 next$0 lst$0 null$0)) + (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) + (not (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) + :named sorted_set_2_7)) + +(assert (! (forall ((l1 Loc)) + (or (= l1 null$0) + (in (read$0 data$0 l1) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + (not (Btwn$0 next$0 curr_2$0 l1 null$0)))) + :named sorted_set_1_1)) + +(assert (! (forall ((l1 Loc)) + (or (= l1 curr_2$0) + (in (read$0 data$0 l1) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) + (not (Btwn$0 next$0 lst$0 l1 curr_2$0)))) + :named sorted_set_1_2)) + +(assert (! (and + (or + (= + (witness$0 (read$0 data$0 curr_2$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + null$0) + (in (read$0 data$0 curr_2$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) + (or + (and + (= (read$0 data$0 curr_2$0) + (read$0 data$0 + (witness$0 (read$0 data$0 curr_2$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) + (in + (witness$0 (read$0 data$0 curr_2$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) + (not + (in (read$0 data$0 curr_2$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) + :named sorted_set_2_8)) + +(assert (! (and + (or + (= + (witness$0 (read$0 data$0 prev_2$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + null$0) + (in (read$0 data$0 prev_2$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) + (or + (and + (= (read$0 data$0 prev_2$0) + (read$0 data$0 + (witness$0 (read$0 data$0 prev_2$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) + (in + (witness$0 (read$0 data$0 prev_2$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) + (not + (in (read$0 data$0 prev_2$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) + :named sorted_set_2_9)) + +(assert (! (and + (or + (= + (witness$0 (read$0 data$0 sk_l1$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + null$0) + (in (read$0 data$0 sk_l1$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) + (or + (and + (= (read$0 data$0 sk_l1$0) + (read$0 data$0 + (witness$0 (read$0 data$0 sk_l1$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) + (in + (witness$0 (read$0 data$0 sk_l1$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) + (not + (in (read$0 data$0 sk_l1$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) + :named sorted_set_2_10)) + +(assert (! (and + (or + (= + (witness$0 (read$0 data$0 sk_l1_1$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + null$0) + (in (read$0 data$0 sk_l1_1$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) + (or + (and + (= (read$0 data$0 sk_l1_1$0) + (read$0 data$0 + (witness$0 (read$0 data$0 sk_l1_1$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) + (in + (witness$0 (read$0 data$0 sk_l1_1$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) + (not + (in (read$0 data$0 sk_l1_1$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) + :named sorted_set_2_11)) + +(assert (! (and + (or + (= + (witness$0 (read$0 data$0 sk_l2$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + null$0) + (in (read$0 data$0 sk_l2$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) + (or + (and + (= (read$0 data$0 sk_l2$0) + (read$0 data$0 + (witness$0 (read$0 data$0 sk_l2$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) + (in + (witness$0 (read$0 data$0 sk_l2$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) + (not + (in (read$0 data$0 sk_l2$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) + :named sorted_set_2_12)) + +(assert (! (and + (or + (= + (witness$0 (read$0 data$0 sk_l2_1$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + null$0) + (in (read$0 data$0 sk_l2_1$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) + (or + (and + (= (read$0 data$0 sk_l2_1$0) + (read$0 data$0 + (witness$0 (read$0 data$0 sk_l2_1$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) + (in + (witness$0 (read$0 data$0 sk_l2_1$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) + (not + (in (read$0 data$0 sk_l2_1$0) + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) + :named sorted_set_2_13)) + +(assert (! (and + (or + (= + (witness$0 sk_?e$0 + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + null$0) + (in sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) + (or + (and + (= sk_?e$0 + (read$0 data$0 + (witness$0 sk_?e$0 + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) + (in + (witness$0 sk_?e$0 + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) + (not (in sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) + :named sorted_set_2_14)) + +(assert (! (and + (or + (= + (witness$0 sk_?e_3$0 + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + null$0) + (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) + (or + (and + (= sk_?e_3$0 + (read$0 data$0 + (witness$0 sk_?e_3$0 + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) + (in + (witness$0 sk_?e_3$0 + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) + (not + (in sk_?e_3$0 + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) + :named sorted_set_2_15)) + +(assert (! (and + (or + (= + (witness$0 (read$0 data$0 curr_2$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) + null$0) + (in (read$0 data$0 curr_2$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) + (or + (and + (= (read$0 data$0 curr_2$0) + (read$0 data$0 + (witness$0 (read$0 data$0 curr_2$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) + (in + (witness$0 (read$0 data$0 curr_2$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) + (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) + (not + (in (read$0 data$0 curr_2$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) + :named sorted_set_2_16)) + +(assert (! (and + (or + (= + (witness$0 (read$0 data$0 prev_2$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) + null$0) + (in (read$0 data$0 prev_2$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) + (or + (and + (= (read$0 data$0 prev_2$0) + (read$0 data$0 + (witness$0 (read$0 data$0 prev_2$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) + (in + (witness$0 (read$0 data$0 prev_2$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) + (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) + (not + (in (read$0 data$0 prev_2$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) + :named sorted_set_2_17)) + +(assert (! (and + (or + (= + (witness$0 (read$0 data$0 sk_l1$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) + null$0) + (in (read$0 data$0 sk_l1$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) + (or + (and + (= (read$0 data$0 sk_l1$0) + (read$0 data$0 + (witness$0 (read$0 data$0 sk_l1$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) + (in + (witness$0 (read$0 data$0 sk_l1$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) + (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) + (not + (in (read$0 data$0 sk_l1$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) + :named sorted_set_2_18)) + +(assert (! (and + (or + (= + (witness$0 (read$0 data$0 sk_l1_1$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) + null$0) + (in (read$0 data$0 sk_l1_1$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) + (or + (and + (= (read$0 data$0 sk_l1_1$0) + (read$0 data$0 + (witness$0 (read$0 data$0 sk_l1_1$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) + (in + (witness$0 (read$0 data$0 sk_l1_1$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) + (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) + (not + (in (read$0 data$0 sk_l1_1$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) + :named sorted_set_2_19)) + +(assert (! (and + (or + (= + (witness$0 (read$0 data$0 sk_l2$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) + null$0) + (in (read$0 data$0 sk_l2$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) + (or + (and + (= (read$0 data$0 sk_l2$0) + (read$0 data$0 + (witness$0 (read$0 data$0 sk_l2$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) + (in + (witness$0 (read$0 data$0 sk_l2$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) + (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) + (not + (in (read$0 data$0 sk_l2$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) + :named sorted_set_2_20)) + +(assert (! (and + (or + (= + (witness$0 (read$0 data$0 sk_l2_1$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) + null$0) + (in (read$0 data$0 sk_l2_1$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) + (or + (and + (= (read$0 data$0 sk_l2_1$0) + (read$0 data$0 + (witness$0 (read$0 data$0 sk_l2_1$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) + (in + (witness$0 (read$0 data$0 sk_l2_1$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) + (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) + (not + (in (read$0 data$0 sk_l2_1$0) + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) + :named sorted_set_2_21)) + +(assert (! (and + (or + (= + (witness$0 sk_?e$0 + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) + null$0) + (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) + (or + (and + (= sk_?e$0 + (read$0 data$0 + (witness$0 sk_?e$0 + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) + (in + (witness$0 sk_?e$0 + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) + (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) + (not (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) + :named sorted_set_2_22)) + +(assert (! (and + (or + (= + (witness$0 sk_?e_3$0 + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) + null$0) + (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) + (or + (and + (= sk_?e_3$0 + (read$0 data$0 + (witness$0 sk_?e_3$0 + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) + (in + (witness$0 sk_?e_3$0 + (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) + (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) + (not + (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) + :named sorted_set_2_23)) + +(assert (! (= (read$1 next$0 null$0) null$0) :named read_null)) + +(assert (! (forall ((l1 Loc)) + (or + (and (Btwn$0 next$0 lst$0 l1 null$0) + (in l1 (sorted_set_domain$0 data$0 next$0 lst$0 null$0)) + (not (= l1 null$0))) + (and (or (= l1 null$0) (not (Btwn$0 next$0 lst$0 l1 null$0))) + (not + (in l1 + (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))))) + :named sorted_set_footprint)) + +(assert (! (or (in sk_?e_3$0 c2_2$0) + (and (in sk_?e_2$0 sk_FP_1$0) (not (in sk_?e_2$0 FP$0))) + (and (in sk_?e_3$0 (union c1_2$0 c2_2$0)) + (not (in sk_?e_3$0 content$0))) + (and (in sk_?e_3$0 c1_2$0) + (not + (in sk_?e_3$0 + (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) + (and (in sk_?e_3$0 content$0) + (not (in sk_?e_3$0 (union c1_2$0 c2_2$0)))) + (and (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + (not (in sk_?e_3$0 c1_2$0))) + (and (not (= curr_2$0 null$0)) (not (= prev_2$0 null$0)) + (not (< (read$0 data$0 prev_2$0) (read$0 data$0 curr_2$0)))) + (not (= curr_2$0 lst$0)) (not (= prev_2$0 null$0)) + (not + (sorted_set_struct$0 sk_?X_3$0 data$0 next$0 curr_2$0 null$0 + c1_2$0))) + :named invariant_37_2)) + +(assert (! (= sk_FP_1$0 sk_?X_2$0) :named invariant_37_2_1)) + +(assert (! (= sk_?X_5$0 (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)) + :named invariant_37_2_2)) + +(assert (! (= sk_?X_3$0 (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)) + :named invariant_37_2_3)) + +(assert (! (= sk_?X_1$0 (union sk_?X_3$0 sk_?X_4$0)) :named invariant_37_2_4)) + +(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0)) + :named precondition_of_insert_27_11)) + +(assert (! (= sk_?X$0 FP$0) :named precondition_of_insert_27_11_1)) + +(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0)) + :named initial_footprint_of_insert_27_11)) + +(assert (! (= curr_2$0 lst$0) :named assign_31_2)) + +(assert (! (= c1_2$0 content$0) :named assign_34_2)) + +(assert (! (or (and (Btwn$0 next$0 lst$0 null$0 null$0) Axiom$0) + (not + (sorted_set_struct$0 sk_?X$0 data$0 next$0 lst$0 null$0 + content$0))) + :named unnamed)) + +(assert (! (or (sorted_set_struct$0 sk_?X_3$0 data$0 next$0 curr_2$0 null$0 c1_2$0) + (not (Btwn$0 next$0 curr_2$0 null$0 null$0)) + (! (and (Btwn$0 next$0 sk_l1$0 sk_l2$0 null$0) (in sk_l1$0 sk_?X_3$0) + (in sk_l2$0 sk_?X_3$0) (not (= sk_l1$0 sk_l2$0)) + (not (< (read$0 data$0 sk_l1$0) (read$0 data$0 sk_l2$0)))) + :named strict_sortedness_1)) + :named unnamed_1)) + +(assert (! (forall ((l1 Loc)) + (or + (and (Btwn$0 next$0 lst$0 l1 curr_2$0) + (in l1 + (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)) + (not (= l1 curr_2$0))) + (and + (or (= l1 curr_2$0) + (not (Btwn$0 next$0 lst$0 l1 curr_2$0))) + (not + (in l1 + (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)))))) + :named sorted_set_footprint_1)) + +(assert (! (forall ((l1 Loc)) + (or + (and (Btwn$0 next$0 curr_2$0 l1 null$0) + (in l1 + (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)) + (not (= l1 null$0))) + (and + (or (= l1 null$0) + (not (Btwn$0 next$0 curr_2$0 l1 null$0))) + (not + (in l1 + (sorted_set_domain$0 data$0 next$0 curr_2$0 + null$0)))))) + :named sorted_set_footprint_2)) + +(assert (! (not (in null$0 Alloc$0)) :named initial_footprint_of_insert_27_11_1)) + +(assert (! (or (= prev_2$0 curr_2$0) + (in sk_?e_1$0 (intersection sk_?X_4$0 sk_?X_3$0)) + (and (in sk_?e_1$0 sk_FP$0) (not (in sk_?e_1$0 FP$0))) + (and (in sk_?e$0 (union c1_2$0 c2_2$0)) (not (in sk_?e$0 content$0))) + (and (in sk_?e$0 c1_2$0) + (not (in sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) + (and (in sk_?e$0 c2_2$0) + (not (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) + (and (in sk_?e$0 content$0) (not (in sk_?e$0 (union c1_2$0 c2_2$0)))) + (and (in sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + (not (in sk_?e$0 c1_2$0))) + (and (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) + (not (in sk_?e$0 c2_2$0))) + (and (not (= curr_2$0 null$0)) (not (= prev_2$0 null$0)) + (not (< (read$0 data$0 prev_2$0) (read$0 data$0 curr_2$0)))) + (not (= (read$1 next$0 prev_2$0) curr_2$0)) + (not (> val$0 (read$0 data$0 prev_2$0))) + (not (Btwn$0 next$0 lst$0 prev_2$0 curr_2$0)) + (not + (sorted_set_struct$0 sk_?X_3$0 data$0 next$0 curr_2$0 null$0 + c1_2$0)) + (not + (sorted_set_struct$0 sk_?X_5$0 data$0 next$0 lst$0 curr_2$0 + c2_2$0))) + :named invariant_37_2_5)) + +(assert (! (= sk_FP$0 sk_?X_1$0) :named invariant_37_2_6)) + +(assert (! (= sk_?X_4$0 sk_?X_5$0) :named invariant_37_2_7)) + +(assert (! (= sk_?X_2$0 sk_?X_3$0) :named invariant_37_2_8)) + +(assert (! (sorted_set_struct$0 sk_?X$0 data$0 next$0 lst$0 null$0 content$0) + :named precondition_of_insert_27_11_2)) + +(assert (! (= sk_?X$0 (sorted_set_domain$0 data$0 next$0 lst$0 null$0)) + :named precondition_of_insert_27_11_3)) + +(assert (! (= content$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0)) + :named precondition_of_insert_27_11_4)) + +(assert (! (= prev_2$0 null$0) :named assign_32_2)) + +(assert (! (= c2_2$0 (as emptyset SetInt)) :named assign_35_2)) + +(assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_29_0)) + +(assert (! (or (sorted_set_struct$0 sk_?X_5$0 data$0 next$0 lst$0 curr_2$0 c2_2$0) + (not (Btwn$0 next$0 lst$0 curr_2$0 curr_2$0)) + (! (and (Btwn$0 next$0 sk_l1_1$0 sk_l2_1$0 curr_2$0) + (in sk_l1_1$0 sk_?X_5$0) (in sk_l2_1$0 sk_?X_5$0) + (not (= sk_l1_1$0 sk_l2_1$0)) + (not (< (read$0 data$0 sk_l1_1$0) (read$0 data$0 sk_l2_1$0)))) + :named strict_sortedness_2)) + :named unnamed_2)) + +(assert (! (forall ((?x Loc)) (Btwn$0 next$0 ?x ?x ?x)) :named btwn_refl)) + +(assert (! (forall ((?x Loc) (?y Loc)) (or (not (Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y))) + :named btwn_sndw)) + +(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) + (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?x ?z ?z)) + (Btwn$0 next$0 ?x ?y ?z) (Btwn$0 next$0 ?x ?z ?y))) + :named btwn_ord1)) + +(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) + (or (not (Btwn$0 next$0 ?x ?y ?z)) + (and (Btwn$0 next$0 ?x ?y ?y) (Btwn$0 next$0 ?y ?z ?z)))) + :named btwn_ord2)) + +(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) + (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?y ?z ?z)) + (Btwn$0 next$0 ?x ?z ?z))) + :named btwn_trn1)) + +(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc)) + (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?y ?u ?z)) + (and (Btwn$0 next$0 ?x ?y ?u) (Btwn$0 next$0 ?x ?u ?z)))) + :named btwn_trn2)) + +(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc)) + (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?x ?u ?y)) + (and (Btwn$0 next$0 ?x ?u ?z) (Btwn$0 next$0 ?u ?y ?z)))) + :named btwn_trn3)) + +(check-sat) +(exit) diff --git a/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2 b/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2 new file mode 100644 index 000000000..c1c65cea5 --- /dev/null +++ b/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2 @@ -0,0 +1,470 @@ +(set-option :print-success false) +(set-logic AUFLIA_SETS) +(set-info :status unsat) +(declare-sort Loc 0) +(define-sort SetLoc () (Set Loc)) +(define-sort SetInt () (Set Int)) +(declare-sort FldLoc 0) +(declare-sort FldInt 0) +(declare-fun null$0 () Loc) +(declare-fun read$0 (FldLoc Loc) Loc) +(declare-fun write$0 (FldLoc Loc Loc) FldLoc) +(declare-fun ep$0 (FldLoc SetLoc Loc) Loc) +(declare-fun Btwn$0 (FldLoc Loc Loc Loc) Bool) +(declare-fun Frame$0 (SetLoc SetLoc FldLoc FldLoc) Bool) +(declare-fun Alloc$0 () SetLoc) +(declare-fun FP$0 () SetLoc) +(declare-fun FP_1$0 () SetLoc) +(declare-fun FP_2$0 () SetLoc) +(declare-fun FP_Caller$0 () SetLoc) +(declare-fun FP_Caller_1$0 () SetLoc) +(declare-fun curr_2$0 () Loc) +(declare-fun curr_3$0 () Loc) +(declare-fun lseg_domain$0 (FldLoc Loc Loc) SetLoc) +(declare-fun lseg_struct$0 (SetLoc FldLoc Loc Loc) Bool) +(declare-fun lst$0 () Loc) +(declare-fun lst_1$0 () Loc) +(declare-fun next$0 () FldLoc) +(declare-fun next_1$0 () FldLoc) +(declare-fun nondet_2$0 () Bool) +(declare-fun sk_?X_27$0 () SetLoc) +(declare-fun sk_?X_28$0 () SetLoc) +(declare-fun sk_?X_29$0 () SetLoc) +(declare-fun sk_?X_30$0 () SetLoc) +(declare-fun sk_?X_31$0 () SetLoc) +(declare-fun sk_?X_32$0 () SetLoc) +(declare-fun sk_?X_33$0 () SetLoc) +(declare-fun tmp_2$0 () Loc) + +(assert (! (forall ((?y Loc)) + (or (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y) + (Btwn$0 next$0 null$0 (read$0 next$0 null$0) ?y))) + :named btwn_reach_8)) + +(assert (! (forall ((?y Loc)) + (or (not (Btwn$0 next$0 tmp_2$0 ?y ?y)) (= tmp_2$0 ?y) + (Btwn$0 next$0 tmp_2$0 (read$0 next$0 tmp_2$0) ?y))) + :named btwn_reach_9)) + +(assert (! (forall ((?y Loc)) + (or (not (Btwn$0 next$0 curr_3$0 ?y ?y)) (= curr_3$0 ?y) + (Btwn$0 next$0 curr_3$0 (read$0 next$0 curr_3$0) ?y))) + :named btwn_reach_10)) + +(assert (! (forall ((?y Loc)) + (or (not (= (read$0 next$0 null$0) null$0)) + (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y))) + :named btwn_cycl_8)) + +(assert (! (forall ((?y Loc)) + (or (not (= (read$0 next$0 tmp_2$0) tmp_2$0)) + (not (Btwn$0 next$0 tmp_2$0 ?y ?y)) (= tmp_2$0 ?y))) + :named btwn_cycl_9)) + +(assert (! (forall ((?y Loc)) + (or (not (= (read$0 next$0 curr_3$0) curr_3$0)) + (not (Btwn$0 next$0 curr_3$0 ?y ?y)) (= curr_3$0 ?y))) + :named btwn_cycl_10)) + +(assert (! (Btwn$0 next$0 null$0 (read$0 next$0 null$0) (read$0 next$0 null$0)) + :named btwn_step_8)) + +(assert (! (Btwn$0 next$0 tmp_2$0 (read$0 next$0 tmp_2$0) (read$0 next$0 tmp_2$0)) + :named btwn_step_9)) + +(assert (! (Btwn$0 next$0 curr_3$0 (read$0 next$0 curr_3$0) (read$0 next$0 curr_3$0)) + :named btwn_step_10)) + +(assert (! (forall ((?f FldLoc)) + (or (in (ep$0 ?f sk_?X_30$0 null$0) sk_?X_30$0) + (= null$0 (ep$0 ?f sk_?X_30$0 null$0)))) + :named entry-point3_10)) + +(assert (! (forall ((?f FldLoc)) + (or (in (ep$0 ?f sk_?X_30$0 lst_1$0) sk_?X_30$0) + (= lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0)))) + :named entry-point3_11)) + +(assert (! (forall ((?f FldLoc)) + (or (in (ep$0 ?f sk_?X_30$0 curr_3$0) sk_?X_30$0) + (= curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0)))) + :named entry-point3_12)) + +(assert (! (forall ((?f FldLoc)) + (or (in (ep$0 ?f sk_?X_30$0 tmp_2$0) sk_?X_30$0) + (= tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0)))) + :named entry-point3_13)) + +(assert (! (forall ((?f FldLoc)) + (Btwn$0 ?f null$0 (ep$0 ?f sk_?X_30$0 null$0) + (ep$0 ?f sk_?X_30$0 null$0))) + :named entry-point1_10)) + +(assert (! (forall ((?f FldLoc)) + (Btwn$0 ?f lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0) + (ep$0 ?f sk_?X_30$0 lst_1$0))) + :named entry-point1_11)) + +(assert (! (forall ((?f FldLoc)) + (Btwn$0 ?f curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0) + (ep$0 ?f sk_?X_30$0 curr_3$0))) + :named entry-point1_12)) + +(assert (! (forall ((?f FldLoc)) + (Btwn$0 ?f tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0) + (ep$0 ?f sk_?X_30$0 tmp_2$0))) + :named entry-point1_13)) + +(assert (! (forall ((?f FldLoc) (?y Loc)) + (or (Btwn$0 ?f null$0 (ep$0 ?f sk_?X_30$0 null$0) ?y) + (not (Btwn$0 ?f null$0 ?y ?y)) (not (in ?y sk_?X_30$0)))) + :named entry-point4_10)) + +(assert (! (forall ((?f FldLoc) (?y Loc)) + (or (Btwn$0 ?f lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0) ?y) + (not (Btwn$0 ?f lst_1$0 ?y ?y)) (not (in ?y sk_?X_30$0)))) + :named entry-point4_11)) + +(assert (! (forall ((?f FldLoc) (?y Loc)) + (or (Btwn$0 ?f curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0) ?y) + (not (Btwn$0 ?f curr_3$0 ?y ?y)) (not (in ?y sk_?X_30$0)))) + :named entry-point4_12)) + +(assert (! (forall ((?f FldLoc) (?y Loc)) + (or (Btwn$0 ?f tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0) ?y) + (not (Btwn$0 ?f tmp_2$0 ?y ?y)) (not (in ?y sk_?X_30$0)))) + :named entry-point4_13)) + +(assert (! (forall ((?f FldLoc) (?y Loc)) + (or (not (Btwn$0 ?f null$0 ?y ?y)) (not (in ?y sk_?X_30$0)) + (in (ep$0 ?f sk_?X_30$0 null$0) sk_?X_30$0))) + :named entry-point2_10)) + +(assert (! (forall ((?f FldLoc) (?y Loc)) + (or (not (Btwn$0 ?f lst_1$0 ?y ?y)) (not (in ?y sk_?X_30$0)) + (in (ep$0 ?f sk_?X_30$0 lst_1$0) sk_?X_30$0))) + :named entry-point2_11)) + +(assert (! (forall ((?f FldLoc) (?y Loc)) + (or (not (Btwn$0 ?f curr_3$0 ?y ?y)) (not (in ?y sk_?X_30$0)) + (in (ep$0 ?f sk_?X_30$0 curr_3$0) sk_?X_30$0))) + :named entry-point2_12)) + +(assert (! (forall ((?f FldLoc) (?y Loc)) + (or (not (Btwn$0 ?f tmp_2$0 ?y ?y)) (not (in ?y sk_?X_30$0)) + (in (ep$0 ?f sk_?X_30$0 tmp_2$0) sk_?X_30$0))) + :named entry-point2_13)) + +(assert (! (= (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) curr_3$0) + (read$0 next$0 tmp_2$0)) + :named read_write2)) + +(assert (! (or (= null$0 curr_3$0) + (= (read$0 next$0 null$0) + (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) null$0))) + :named read_write1)) + +(assert (! (or (= tmp_2$0 curr_3$0) + (= (read$0 next$0 tmp_2$0) + (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) tmp_2$0))) + :named read_write1_1)) + +(assert (! (or (= curr_3$0 curr_3$0) + (= (read$0 next$0 curr_3$0) + (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) curr_3$0))) + :named read_write1_2)) + +(assert (! (= (read$0 next$0 null$0) null$0) :named read_null_5)) + +(assert (! (= (read$0 next_1$0 null$0) null$0) :named read_null_6)) + +(assert (! (forall ((l1 Loc)) + (or + (and (Btwn$0 next$0 lst$0 l1 curr_2$0) + (in l1 (lseg_domain$0 next$0 lst$0 curr_2$0)) + (not (= l1 curr_2$0))) + (and + (or (= l1 curr_2$0) + (not (Btwn$0 next$0 lst$0 l1 curr_2$0))) + (not (in l1 (lseg_domain$0 next$0 lst$0 curr_2$0)))))) + :named lseg_footprint_20)) + +(assert (! (forall ((l1 Loc)) + (or + (and (Btwn$0 next$0 curr_3$0 l1 null$0) + (in l1 (lseg_domain$0 next$0 curr_3$0 null$0)) + (not (= l1 null$0))) + (and + (or (= l1 null$0) + (not (Btwn$0 next$0 curr_3$0 l1 null$0))) + (not (in l1 (lseg_domain$0 next$0 curr_3$0 null$0)))))) + :named lseg_footprint_21)) + +(assert (! (not (in tmp_2$0 FP_2$0)) :named check_free_31_6)) + +(assert (! (not (in null$0 Alloc$0)) :named framecondition_of_remove_loop_18_4_15)) + +(assert (! (not (= lst$0 null$0)) :named if_else_13_6_4)) + +(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0)) + :named precondition_of_remove_10_11_20)) + +(assert (! (= sk_?X_33$0 FP$0) :named precondition_of_remove_10_11_21)) + +(assert (! (lseg_struct$0 sk_?X_32$0 next$0 lst$0 curr_2$0) :named invariant_18_4_62)) + +(assert (! (= FP$0 (union FP_1$0 FP$0)) :named invariant_18_4_63)) + +(assert (! (= sk_?X_31$0 (lseg_domain$0 next$0 curr_2$0 null$0)) + :named invariant_18_4_64)) + +(assert (! (= sk_?X_30$0 (union sk_?X_31$0 sk_?X_32$0)) :named invariant_18_4_65)) + +(assert (! (= (as emptyset SetLoc) (as emptyset SetLoc)) :named invariant_18_4_66)) + +(assert (! (lseg_struct$0 sk_?X_28$0 next$0 curr_3$0 null$0) + :named invariant_18_4_67)) + +(assert (! (= sk_?X_29$0 (union sk_?X_28$0 sk_?X_27$0)) :named invariant_18_4_68)) + +(assert (! (= sk_?X_28$0 (lseg_domain$0 next$0 curr_3$0 null$0)) + :named invariant_18_4_69)) + +(assert (! (= (as emptyset SetLoc) (intersection sk_?X_27$0 sk_?X_28$0)) + :named invariant_18_4_70)) + +(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0)) + :named initial_footprint_of_remove_10_11_10)) + +(assert (! (Frame$0 FP_1$0 Alloc$0 next$0 next$0) + :named framecondition_of_remove_loop_18_4_16)) + +(assert (! (= next_1$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0))) + :named assign_30_6)) + +(assert (! (= curr_2$0 lst$0) :named assign_17_4_4)) + +(assert (! (= FP_2$0 + (union (setminus FP$0 FP_1$0) + (union (intersection Alloc$0 FP_1$0) (setminus Alloc$0 Alloc$0)))) + :named framecondition_of_remove_loop_18_4_17)) + +(assert (! (or (Btwn$0 next$0 lst$0 curr_2$0 curr_2$0) + (not (lseg_struct$0 sk_?X_32$0 next$0 lst$0 curr_2$0))) + :named unnamed_23)) + +(assert (! (or (Btwn$0 next$0 curr_3$0 null$0 null$0) + (not (lseg_struct$0 sk_?X_28$0 next$0 curr_3$0 null$0))) + :named unnamed_24)) + +(assert (! (or (= (read$0 next$0 curr_3$0) null$0) (not nondet_2$0)) + :named unnamed_25)) + +(assert (! (forall ((l1 Loc)) + (or + (and (Btwn$0 next$0 lst_1$0 l1 curr_3$0) + (in l1 (lseg_domain$0 next$0 lst_1$0 curr_3$0)) + (not (= l1 curr_3$0))) + (and + (or (= l1 curr_3$0) + (not (Btwn$0 next$0 lst_1$0 l1 curr_3$0))) + (not (in l1 (lseg_domain$0 next$0 lst_1$0 curr_3$0)))))) + :named lseg_footprint_22)) + +(assert (! (forall ((l1 Loc)) + (or + (and (Btwn$0 next$0 lst$0 l1 null$0) + (in l1 (lseg_domain$0 next$0 lst$0 null$0)) + (not (= l1 null$0))) + (and (or (= l1 null$0) (not (Btwn$0 next$0 lst$0 l1 null$0))) + (not (in l1 (lseg_domain$0 next$0 lst$0 null$0)))))) + :named lseg_footprint_23)) + +(assert (! (forall ((l1 Loc)) + (or + (and (Btwn$0 next$0 curr_2$0 l1 null$0) + (in l1 (lseg_domain$0 next$0 curr_2$0 null$0)) + (not (= l1 null$0))) + (and + (or (= l1 null$0) + (not (Btwn$0 next$0 curr_2$0 l1 null$0))) + (not (in l1 (lseg_domain$0 next$0 curr_2$0 null$0)))))) + :named lseg_footprint_24)) + +(assert (! (not (in null$0 Alloc$0)) :named initial_footprint_of_remove_10_11_11)) + +(assert (! (not (= tmp_2$0 null$0)) :named if_else_28_8_2)) + +(assert (! (lseg_struct$0 sk_?X_33$0 next$0 lst$0 null$0) + :named precondition_of_remove_10_11_22)) + +(assert (! (= sk_?X_33$0 (lseg_domain$0 next$0 lst$0 null$0)) + :named precondition_of_remove_10_11_23)) + +(assert (! (not (= curr_2$0 null$0)) :named invariant_18_4_71)) + +(assert (! (lseg_struct$0 sk_?X_31$0 next$0 curr_2$0 null$0) + :named invariant_18_4_72)) + +(assert (! (= sk_?X_32$0 (lseg_domain$0 next$0 lst$0 curr_2$0)) + :named invariant_18_4_73)) + +(assert (! (= sk_?X_30$0 FP_1$0) :named invariant_18_4_74)) + +(assert (! (= (as emptyset SetLoc) (intersection sk_?X_32$0 sk_?X_31$0)) + :named invariant_18_4_75)) + +(assert (! (not (= curr_3$0 null$0)) :named invariant_18_4_76)) + +(assert (! (lseg_struct$0 sk_?X_27$0 next$0 lst_1$0 curr_3$0) + :named invariant_18_4_77)) + +(assert (! (= sk_?X_29$0 + (union (intersection Alloc$0 FP_1$0) (setminus Alloc$0 Alloc$0))) + :named invariant_18_4_78)) + +(assert (! (= sk_?X_27$0 (lseg_domain$0 next$0 lst_1$0 curr_3$0)) + :named invariant_18_4_79)) + +(assert (! (= (as emptyset SetLoc) (as emptyset SetLoc)) :named invariant_18_4_80)) + +(assert (! (= Alloc$0 (union FP_2$0 Alloc$0)) + :named framecondition_of_remove_loop_18_4_18)) + +(assert (! (= tmp_2$0 (read$0 next$0 curr_3$0)) :named assign_27_4_2)) + +(assert (! (= lst_1$0 lst$0) :named framecondition_of_remove_loop_18_4_19)) + +(assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_13_2_5)) + +(assert (! (or (Btwn$0 next$0 lst_1$0 curr_3$0 curr_3$0) + (not (lseg_struct$0 sk_?X_27$0 next$0 lst_1$0 curr_3$0))) + :named unnamed_26)) + +(assert (! (or (Btwn$0 next$0 lst$0 null$0 null$0) + (not (lseg_struct$0 sk_?X_33$0 next$0 lst$0 null$0))) + :named unnamed_27)) + +(assert (! (or (Btwn$0 next$0 curr_2$0 null$0 null$0) + (not (lseg_struct$0 sk_?X_31$0 next$0 curr_2$0 null$0))) + :named unnamed_28)) + +(assert (! (forall ((?u Loc) (?v Loc) (?z Loc)) + (and + (or + (Btwn$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) + ?z ?u ?v) + (not + (or + (and (Btwn$0 next$0 ?z ?u ?v) + (or (Btwn$0 next$0 ?z ?v curr_3$0) + (and (Btwn$0 next$0 ?z ?v ?v) + (not + (Btwn$0 next$0 ?z curr_3$0 + curr_3$0))))) + (and (not (= curr_3$0 ?v)) + (or (Btwn$0 next$0 ?z curr_3$0 ?v) + (and + (Btwn$0 next$0 ?z curr_3$0 + curr_3$0) + (not (Btwn$0 next$0 ?z ?v ?v)))) + (Btwn$0 next$0 ?z ?u curr_3$0) + (or + (Btwn$0 next$0 (read$0 next$0 tmp_2$0) + ?v curr_3$0) + (and + (Btwn$0 next$0 + (read$0 next$0 tmp_2$0) ?v ?v) + (not + (Btwn$0 next$0 + (read$0 next$0 tmp_2$0) + curr_3$0 curr_3$0))))) + (and (not (= curr_3$0 ?v)) + (or (Btwn$0 next$0 ?z curr_3$0 ?v) + (and + (Btwn$0 next$0 ?z curr_3$0 + curr_3$0) + (not (Btwn$0 next$0 ?z ?v ?v)))) + (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?u + ?v) + (or + (Btwn$0 next$0 (read$0 next$0 tmp_2$0) + ?v curr_3$0) + (and + (Btwn$0 next$0 + (read$0 next$0 tmp_2$0) ?v ?v) + (not + (Btwn$0 next$0 + (read$0 next$0 tmp_2$0) + curr_3$0 curr_3$0)))))))) + (or + (and (Btwn$0 next$0 ?z ?u ?v) + (or (Btwn$0 next$0 ?z ?v curr_3$0) + (and (Btwn$0 next$0 ?z ?v ?v) + (not (Btwn$0 next$0 ?z curr_3$0 curr_3$0))))) + (and (not (= curr_3$0 ?v)) + (or (Btwn$0 next$0 ?z curr_3$0 ?v) + (and (Btwn$0 next$0 ?z curr_3$0 curr_3$0) + (not (Btwn$0 next$0 ?z ?v ?v)))) + (Btwn$0 next$0 ?z ?u curr_3$0) + (or + (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v + curr_3$0) + (and + (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v + ?v) + (not + (Btwn$0 next$0 (read$0 next$0 tmp_2$0) + curr_3$0 curr_3$0))))) + (and (not (= curr_3$0 ?v)) + (or (Btwn$0 next$0 ?z curr_3$0 ?v) + (and (Btwn$0 next$0 ?z curr_3$0 curr_3$0) + (not (Btwn$0 next$0 ?z ?v ?v)))) + (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?u ?v) + (or + (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v + curr_3$0) + (and + (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v + ?v) + (not + (Btwn$0 next$0 (read$0 next$0 tmp_2$0) + curr_3$0 curr_3$0))))) + (not + (Btwn$0 + (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) + ?z ?u ?v))))) + :named btwn_write)) + +(assert (! (forall ((?x Loc)) (Btwn$0 next$0 ?x ?x ?x)) :named btwn_refl_5)) + +(assert (! (forall ((?x Loc) (?y Loc)) (or (not (Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y))) + :named btwn_sndw_5)) + +(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) + (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?x ?z ?z)) + (Btwn$0 next$0 ?x ?y ?z) (Btwn$0 next$0 ?x ?z ?y))) + :named btwn_ord1_5)) + +(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) + (or (not (Btwn$0 next$0 ?x ?y ?z)) + (and (Btwn$0 next$0 ?x ?y ?y) (Btwn$0 next$0 ?y ?z ?z)))) + :named btwn_ord2_5)) + +(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) + (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?y ?z ?z)) + (Btwn$0 next$0 ?x ?z ?z))) + :named btwn_trn1_5)) + +(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc)) + (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?y ?u ?z)) + (and (Btwn$0 next$0 ?x ?y ?u) (Btwn$0 next$0 ?x ?u ?z)))) + :named btwn_trn2_5)) + +(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc)) + (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?x ?u ?y)) + (and (Btwn$0 next$0 ?x ?u ?z) (Btwn$0 next$0 ?u ?y ?z)))) + :named btwn_trn3_5)) + +(check-sat) +(exit) diff --git a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 new file mode 100644 index 000000000..c4ee3b710 --- /dev/null +++ b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 @@ -0,0 +1,18 @@ +(set-logic QF_ALL_SUPPORTED) +(set-info :status unsat) +(define-sort Elt () Int) +(define-sort mySet () (Set Elt )) +(define-fun smt_set_emp () mySet (as emptyset mySet)) + +(declare-fun S () (Set Int)) +(declare-fun T () (Set Int)) + +(assert (not (= S T))) +(assert (= T (union smt_set_emp S))) +(check-sat) + +; What was the bug? +; +; When two sets were disequal, the corresponding lemma +; was not being generated (stating there in an element +; in one, but not in the other). diff --git a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 new file mode 100644 index 000000000..7fea3435e --- /dev/null +++ b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 @@ -0,0 +1,49 @@ +(set-logic QF_ALL_SUPPORTED) +(set-info :status unsat) +(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 z3v54 () Int) +(declare-fun z3f55 (Int) Int) +(declare-fun z3v56 () Int) +(declare-fun z3v57 () Int) +(declare-fun z3v58 () Int) +(declare-fun z3v59 () Int) +(declare-fun z3f60 (Int) mySet) +(declare-fun z3f61 (Int) Bool) +(declare-fun z3f62 (Int Int) Int) +(declare-fun z3v63 () Int) +(declare-fun z3v64 () Int) +(declare-fun z3f65 (Int) mySet) +(declare-fun z3v66 () Int) +(declare-fun z3v67 () Int) +(declare-fun z3v68 () Int) +(declare-fun z3v69 () Int) +(declare-fun z3f70 (Int) Int) +(declare-fun z3v71 () Int) +(declare-fun z3v72 () Int) +(declare-fun z3v74 () Int) +(declare-fun z3v76 () Int) +(declare-fun z3v77 () Int) +(declare-fun z3v78 () Int) +(declare-fun z3v82 () Int) +(declare-fun z3v85 () Int) +(declare-fun z3v86 () Int) +(declare-fun z3v87 () Int) +(declare-fun z3f90 () Int) +(declare-fun z3v91 () Int) +(declare-fun z3v92 () Int) +(declare-fun z3v93 () Int) +(declare-fun z3v94 () Int) +(assert (= (z3f60 z3v94) (z3f65 z3v56))) +(assert (and (>= (z3f55 z3v56) 0) (>= (z3f55 z3v58) 0) (= (z3f60 z3v58) smt_set_emp) (= (z3f55 z3v58) 0) (= (z3f61 z3v58) true) (= z3v58 z3f90) (>= (z3f55 z3v58) 0) (= z3v58 z3v63) (>= (z3f55 z3v58) 0) (>= (z3f55 z3v64) 0) (= (z3f65 z3v64) (smt_set_cup (z3f60 z3v63) (z3f65 z3v56))) (= (z3f60 z3v64) (smt_set_cup (smt_set_add smt_set_emp z3v63) (z3f60 z3v56))) (= (z3f55 z3v64) (+ 1 (z3f55 z3v56))) (= (z3f61 z3v64) false) (= z3v64 (z3f62 z3v63 z3v56)) (>= (z3f55 z3v64) 0) (= z3v64 z3v66) (>= (z3f55 z3v64) 0) (>= (z3f55 z3v63) 0) (>= (z3f55 z3v66) 0) (= (z3f70 z3v69) z3v69) (= (z3f70 z3v71) z3v71) (= (z3f70 z3v72) z3v72))) +(assert (not (= (z3f60 z3v94) (z3f65 z3v66)))) +(check-sat) diff --git a/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2 b/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2 new file mode 100644 index 000000000..6c32bb578 --- /dev/null +++ b/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2 @@ -0,0 +1,59 @@ +(set-logic QF_ALL_SUPPORTED) +(set-info :status unsat) + +; What was the bug? +; +; When asserting equality to equality engine, correct reason +; was not being sent (the fact itself was being sent as reason) + +(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 z3v56 () Int) +(declare-fun z3v57 () Int) +(assert (distinct z3v56 z3v57)) +(declare-fun z3v58 () Int) +(declare-fun z3f59 (Int) Int) +(declare-fun z3v60 () Int) +(declare-fun z3f61 (Int) Bool) +(declare-fun z3v62 () Int) +(declare-fun z3v63 () Int) +(declare-fun z3v64 () Int) +(declare-fun z3v65 () Int) +(declare-fun z3f66 (Int) mySet) +(declare-fun z3f67 (Int) Bool) +(declare-fun z3f68 (Int Int) Int) +(declare-fun z3v69 () Int) +(declare-fun z3v70 () Int) +(declare-fun z3f71 (Int) Int) +(declare-fun z3v72 () Int) +(declare-fun z3v73 () Int) +(declare-fun z3v74 () Int) +(declare-fun z3v75 () Int) +(declare-fun z3v76 () Int) +(declare-fun z3v77 () Int) +(declare-fun z3v78 () Int) +(declare-fun z3v80 () Int) +(declare-fun z3v81 () Int) +(declare-fun z3f82 () Int) +(declare-fun z3v83 () Int) +(declare-fun z3v84 () Int) +(declare-fun z3v85 () Int) +(declare-fun z3v86 () Int) +(declare-fun z3v87 () Int) +(declare-fun z3v88 () Int) +(declare-fun z3v89 () Int) +(declare-fun z3v90 () Int) +(assert (= z3v90 z3v56)) +(assert (z3f61 z3v90)) +(assert (and (>= (z3f59 z3v58) 0) (z3f61 z3v60) (z3f61 z3v60) (= z3v60 z3v62) (= (z3f61 z3v60) (= z3v64 z3v63)) (= (z3f61 z3v62) (= z3v64 z3v63)) (>= (z3f59 z3v65) 0) (= (z3f66 z3v65) (smt_set_cup (smt_set_add smt_set_emp z3v64) (z3f66 z3v58))) (= (z3f59 z3v65) (+ 1 (z3f59 z3v58))) (= (z3f67 z3v65) false) (= z3v65 (z3f68 z3v64 z3v58)) (>= (z3f59 z3v65) 0) (= z3v65 z3v69) (>= (z3f59 z3v65) 0) (>= (z3f59 z3v69) 0) (z3f61 z3v56) (= (z3f71 z3v70) z3v70) (= (z3f71 z3v72) z3v72) (not (z3f61 z3v57)) (= (z3f71 z3v73) z3v73))) +(assert (not (= (z3f61 z3v90) (smt_set_mem z3v63 (z3f66 z3v69))))) +(check-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 new file mode 100644 index 000000000..bcc4c33da --- /dev/null +++ b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 @@ -0,0 +1,59 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(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 z3v65 () Int) +(declare-fun z3v66 () Int) +(declare-fun z3f67 (Int) mySet) +(declare-fun z3v69 () Int) +(declare-fun z3f70 (Int) Int) +(declare-fun z3v76 () Int) +(declare-fun z3v77 () Int) +(declare-fun z3v78 () Int) +(declare-fun z3v79 () Int) +(declare-fun z3v80 () Int) +(declare-fun z3v81 () Int) +(declare-fun z3v82 () Int) +(declare-fun z3f83 (Int) Int) +(declare-fun z3f84 (Int) Int) +(declare-fun z3v85 () Int) +(declare-fun z3f86 (Int) Int) +(declare-fun z3f87 (Int Int) Int) +(declare-fun z3v88 () Int) +(declare-fun z3v89 () Int) +(declare-fun z3f90 (Int) mySet) +(declare-fun z3f91 (Int) Bool) +(declare-fun z3f92 (Int Int) Int) +(declare-fun z3v93 () Int) +(declare-fun z3v94 () Int) +(declare-fun z3v95 () Int) +(declare-fun z3v96 () Int) +(declare-fun z3v97 () Int) +(assert (and (not (z3f60 z3v79)) (not (z3f60 z3v79)) (= z3v79 z3v80) (= (z3f60 z3v79) (= z3v76 z3v81)) (= (z3f60 z3v80) (= z3v76 z3v81)) (= (z3f83 z3v82) z3v81) (= (z3f84 z3v82) z3v81) (= (z3f86 z3v82) z3v85) (= z3v82 (z3f87 z3v81 z3v85)) (= z3v82 z3v88) (>= (z3f70 z3v78) 0) (= (z3f67 z3v78) (smt_set_cup (smt_set_add smt_set_emp (z3f83 z3v88)) (z3f67 z3v89))) (= (z3f90 z3v78) (smt_set_cup (smt_set_add smt_set_emp z3v88) (z3f90 z3v89))) (= (z3f70 z3v78) (+ 1 (z3f70 z3v89))) (= (z3f91 z3v78) false) (= z3v78 (z3f92 z3v88 z3v89)) (>= (z3f70 z3v78) 0) (= z3v78 z3v77) (>= (z3f70 z3v78) 0) (>= (z3f70 z3v89) 0) (>= (z3f70 z3v77) 0) (>= (z3f70 z3v97) 0) (= z3v97 z3v89) (>= (z3f70 z3v97) 0) (z3f60 z3v58) (= (z3f62 z3v61) z3v61) (= (z3f62 z3v63) z3v63) (not (z3f60 z3v59)) (= (z3f62 z3v64) z3v64))) +(assert (smt_set_mem z3v76 (z3f67 z3v78))) +(assert (<= z3v95 z3v93)) +(assert (>= z3v95 z3v93)) +(assert (= z3v95 z3v93)) +(assert (smt_set_mem z3v76 (z3f67 z3v77))) +(declare-fun z3v98 () Int) +(assert (not (< z3v98 z3v85))) +(check-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 new file mode 100644 index 000000000..5a44c0344 --- /dev/null +++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 @@ -0,0 +1,34 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic QF_ALL_SUPPORTED) +(set-info :status sat) + +; Observed behavior +; +; Benchmark taking too long. Lemmas being generated indefinitely with +; skolems due to the "two sets not being equal" axiom. +; +; What was the bug? +; +; + +(define-sort Elt () Int) +(define-sort mySet () (Set Elt)) + +(declare-fun f (Int) mySet) +(declare-fun x () Int) +(declare-fun y () Int) + +(declare-fun S () mySet) +(declare-fun T () mySet) + +(assert (= (f x) + (union S T))) + +(assert (= (f x) + (union T (f y)))) + +(assert (not (= (f y) + (union T (f y))))) + +(check-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 new file mode 100644 index 000000000..67d64bd05 --- /dev/null +++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 @@ -0,0 +1,287 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(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 z3v60 () Int) +(declare-fun z3v61 () Int) +(assert (distinct z3v60 z3v61)) +(declare-fun z3f62 (Int) Bool) +(declare-fun z3v63 () Int) +(declare-fun z3f64 (Int) Int) +(declare-fun z3v65 () Int) +(declare-fun z3v66 () Int) +(declare-fun z3v69 () mySet) +(declare-fun z3v70 () mySet) +(declare-fun z3v72 () mySet) +(declare-fun z3v73 () mySet) +(declare-fun z3v75 () Int) +(declare-fun z3f76 (Int) Int) +(declare-fun z3v79 () Int) +(declare-fun z3v80 () Int) +(declare-fun z3v84 () Int) +(declare-fun z3v87 () mySet) +(declare-fun z3v88 () mySet) +(declare-fun z3v90 () mySet) +(declare-fun z3v91 () mySet) +(declare-fun z3v93 () mySet) +(declare-fun z3v94 () mySet) +(declare-fun z3v96 () Int) +(declare-fun z3f97 (Int) mySet) +(declare-fun z3f98 (Int) Bool) +(declare-fun z3v99 () Int) +(declare-fun z3v102 () Int) +(declare-fun z3v105 () mySet) +(declare-fun z3v107 () mySet) +(declare-fun z3v108 () mySet) +(declare-fun z3v109 () Int) +(declare-fun z3v110 () Int) +(declare-fun z3v111 () Int) +(declare-fun z3v112 () Int) +(declare-fun z3v113 () mySet) +(declare-fun z3v114 () mySet) +(declare-fun z3v117 () mySet) +(declare-fun z3v118 () mySet) +(declare-fun z3v121 () mySet) +(declare-fun z3v123 () mySet) +(declare-fun z3v124 () mySet) +(declare-fun z3v126 () mySet) +(declare-fun z3v128 () Int) +(declare-fun z3v132 () Int) +(declare-fun z3v135 () mySet) +(declare-fun z3v136 () mySet) +(declare-fun z3v138 () mySet) +(declare-fun z3v140 () Int) +(declare-fun z3v143 () mySet) +(declare-fun z3v144 () mySet) +(declare-fun z3v145 () mySet) +(declare-fun z3v146 () Int) +(declare-fun z3v147 () Int) +(declare-fun z3v148 () mySet) +(declare-fun z3v149 () mySet) +(declare-fun z3v155 () mySet) +(declare-fun z3v156 () mySet) +(declare-fun z3v157 () mySet) +(declare-fun z3v160 () Int) +(declare-fun z3v161 () Int) +(declare-fun z3v162 () Int) +(declare-fun z3v163 () Int) +(declare-fun z3v164 () mySet) +(declare-fun z3v165 () mySet) +(declare-fun z3v169 () Int) +(declare-fun z3v172 () mySet) +(declare-fun z3v173 () mySet) +(declare-fun z3v175 () Int) +(declare-fun z3v176 () Int) +(declare-fun z3v177 () Int) +(declare-fun z3v178 () Int) +(declare-fun z3f179 (Int Int) Int) +(declare-fun z3v180 () Int) +(declare-fun z3v181 () Int) +(declare-fun z3f183 () Int) +(declare-fun z3v184 () Int) +(declare-fun z3v185 () Int) +(declare-fun z3v186 () Int) +(declare-fun z3v187 () Int) +(declare-fun z3v188 () Int) +(declare-fun z3v189 () Int) +(declare-fun z3v192 () Int) +(declare-fun z3v193 () Int) +(declare-fun z3v197 () Int) +(declare-fun z3v198 () mySet) +(declare-fun z3v200 () Int) +(declare-fun z3v201 () Int) +(declare-fun z3v202 () Int) +(declare-fun z3v203 () Int) +(declare-fun z3v204 () Int) +(declare-fun z3v206 () Int) +(declare-fun z3v207 () Int) +(declare-fun z3v208 () Int) +(declare-fun z3v209 () Int) +(declare-fun z3v210 () Int) +(declare-fun z3v211 () Int) +(declare-fun z3f212 (Int) Int) +(declare-fun z3f213 (Int) Int) +(declare-fun z3v214 () Int) +(declare-fun z3v215 () Int) +(declare-fun z3v217 () Int) +(declare-fun z3v218 () Int) +(declare-fun z3v219 () Int) +(declare-fun z3v220 () Int) +(declare-fun z3f221 (Int Int) Int) +(declare-fun z3v222 () Int) +(declare-fun z3v223 () Int) +(declare-fun z3v224 () Int) +(declare-fun z3v225 () Int) +(declare-fun z3v226 () Int) +(declare-fun z3v227 () Int) +(declare-fun z3v228 () Int) +(declare-fun z3v229 () Int) +(declare-fun z3v230 () Int) +(declare-fun z3v231 () Int) +(declare-fun z3v232 () Int) +(declare-fun z3v233 () Int) +(declare-fun z3v234 () Int) +(declare-fun z3v235 () Int) +(declare-fun z3v236 () Int) +(declare-fun z3v237 () Int) +(declare-fun z3v238 () Int) +(declare-fun z3v239 () Int) +(declare-fun z3v240 () Int) +(declare-fun z3v241 () Int) +(declare-fun z3v242 () Int) +(declare-fun z3v243 () Int) +(declare-fun z3v244 () Int) +(declare-fun z3v245 () Int) +(declare-fun z3v246 () Int) +(declare-fun z3v247 () Int) +(declare-fun z3v248 () Int) +(declare-fun z3v249 () Int) +(declare-fun z3v250 () Int) +(declare-fun z3v251 () Int) +(declare-fun z3v252 () Int) +(declare-fun z3v253 () Int) +(declare-fun z3v254 () Int) +(declare-fun z3v255 () Int) +(declare-fun z3v256 () Int) +(declare-fun z3v257 () Int) +(declare-fun z3v258 () Int) +(declare-fun z3v259 () Int) +(declare-fun z3v260 () Int) +(declare-fun z3v261 () Int) +(declare-fun z3v262 () Int) +(declare-fun z3v263 () Int) +(declare-fun z3v264 () Int) +(declare-fun z3v265 () Int) +(declare-fun z3v266 () Int) +(declare-fun z3v267 () Int) +(declare-fun z3v268 () Int) +(declare-fun z3v269 () Int) +(declare-fun z3v271 () Int) +(declare-fun z3v273 () Int) +(declare-fun z3v275 () Int) +(declare-fun z3v277 () Int) +(declare-fun z3v279 () Int) +(declare-fun z3v281 () Int) +(declare-fun z3v283 () Int) +(declare-fun z3v286 () Int) +(declare-fun z3v289 () Int) +(declare-fun z3v290 () Int) +(declare-fun z3v291 () Int) +(declare-fun z3v292 () mySet) +(declare-fun z3v295 () mySet) +(declare-fun z3v297 () Int) +(declare-fun z3v301 () Int) +(declare-fun z3v302 () Int) +(declare-fun z3v303 () Int) +(declare-fun z3v304 () Int) +(declare-fun z3v305 () Int) +(declare-fun z3v306 () Int) +(declare-fun z3v307 () Int) +(declare-fun z3v308 () Int) +(declare-fun z3v309 () Int) +(declare-fun z3v310 () Int) +(declare-fun z3v312 () Int) +(declare-fun z3v314 () Int) +(declare-fun z3v315 () Int) +(declare-fun z3v316 () Int) +(declare-fun z3v317 () Int) +(declare-fun z3v318 () Int) +(declare-fun z3v319 () Int) +(declare-fun z3v320 () Int) +(declare-fun z3v321 () Int) +(declare-fun z3v322 () Int) +(declare-fun z3v324 () Int) +(declare-fun z3v327 () Int) +(declare-fun z3v328 () Int) +(declare-fun z3v329 () Int) +(declare-fun z3v330 () Int) +(declare-fun z3v331 () Int) +(declare-fun z3v332 () Int) +(declare-fun z3v333 () Int) +(declare-fun z3v334 () Int) +(declare-fun z3v335 () Int) +(declare-fun z3v336 () Int) +(declare-fun z3v337 () Int) +(declare-fun z3v338 () Int) +(declare-fun z3v339 () Int) +(declare-fun z3v340 () Int) +(declare-fun z3v341 () Int) +(declare-fun z3v342 () Int) +(declare-fun z3v343 () Int) +(declare-fun z3v345 () Int) +(declare-fun z3v349 () Int) +(declare-fun z3v350 () Int) +(declare-fun z3v351 () Int) +(declare-fun z3v352 () Int) +(declare-fun z3v353 () Int) +(declare-fun z3v354 () Int) +(declare-fun z3v355 () Int) +(declare-fun z3v359 () Int) +(declare-fun z3v361 () Int) +(declare-fun z3v362 () Int) +(declare-fun z3v363 () Int) +(declare-fun z3v364 () Int) +(declare-fun z3v366 () Int) +(declare-fun z3v367 () Int) +(declare-fun z3v368 () Int) +(declare-fun z3v369 () Int) +(declare-fun z3v370 () Int) +(declare-fun z3v375 () Int) +(assert (= (z3f97 z3v328) (smt_set_cup (z3f97 z3v331) (z3f97 z3v375)))) +(assert (= (z3f97 z3v328) (smt_set_cup (z3f97 z3v330) (z3f97 z3v375)))) +(assert (= (z3f97 z3v328) (smt_set_cup (z3f97 z3v328) (z3f97 z3v375)))) +(assert (= (z3f97 z3v328) (smt_set_cup (z3f97 z3v327) (z3f97 z3v375)))) +(assert (= (z3f97 z3v331) (smt_set_cup (z3f97 z3v331) (z3f97 z3v375)))) +(assert (= (z3f97 z3v331) (smt_set_cup (z3f97 z3v330) (z3f97 z3v375)))) +(assert (= (z3f97 z3v331) (smt_set_cup (z3f97 z3v328) (z3f97 z3v375)))) +(assert (= (z3f97 z3v331) (smt_set_cup (z3f97 z3v327) (z3f97 z3v375)))) +(assert (= (z3f97 z3v375) (z3f97 z3v331))) +(assert (= (z3f97 z3v375) (z3f97 z3v328))) +(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v327) (z3f97 z3v331)))) +(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v327) (z3f97 z3v328)))) +(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v328) (z3f97 z3v331)))) +(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v328) (z3f97 z3v330)))) +(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v328) (z3f97 z3v328)))) +(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v328) (z3f97 z3v327)))) +(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v330) (z3f97 z3v331)))) +(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v330) (z3f97 z3v328)))) +(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v331) (z3f97 z3v331)))) +(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v331) (z3f97 z3v330)))) +(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v331) (z3f97 z3v328)))) +(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v331) (z3f97 z3v327)))) +(assert (smt_set_sub (z3f97 z3v375) (z3f97 z3v331))) +(assert (smt_set_sub (z3f97 z3v375) (z3f97 z3v328))) +(assert (<= z3v375 z3v331)) +(assert (<= z3v375 z3v328)) +(assert (= z3v375 z3v328)) +(assert (>= z3v375 z3v331)) +(assert (>= z3v375 z3v328)) +(assert (not (= z3v375 z3v330))) +(assert (not (= z3v375 z3v327))) +(assert (<= (z3f76 z3v375) (z3f76 z3v331))) +(assert (<= (z3f76 z3v375) (z3f76 z3v328))) +(assert (> (z3f76 z3v375) (z3f76 z3v330))) +(assert (> (z3f76 z3v375) (z3f76 z3v327))) +(assert (>= (z3f76 z3v375) (z3f76 z3v331))) +(assert (>= (z3f76 z3v375) (z3f76 z3v330))) +(assert (>= (z3f76 z3v375) (z3f76 z3v328))) +(assert (>= (z3f76 z3v375) (z3f76 z3v327))) +(assert (= (z3f76 z3v375) (z3f76 z3v331))) +(assert (= (z3f76 z3v375) (z3f76 z3v328))) +(assert (> (z3f76 z3v375) 0)) +(assert (= z3v375 z3v331)) +(assert (>= (z3f76 z3v375) 0)) +(assert (and (>= (z3f76 z3v327) 0) (>= (z3f76 z3v328) 0) (= (z3f97 z3v328) (smt_set_cup (smt_set_add smt_set_emp z3v329) (z3f97 z3v330))) (= (z3f76 z3v328) (+ 1 (z3f76 z3v330))) (= (z3f98 z3v328) false) (= z3v328 (z3f179 z3v329 z3v330)) (>= (z3f76 z3v328) 0) (= z3v328 z3v331) (>= (z3f76 z3v328) 0) (>= (z3f76 z3v330) 0) (>= (z3f76 z3v331) 0) (z3f62 z3v60) (= (z3f64 z3v63) z3v63) (= (z3f64 z3v65) z3v65) (not (z3f62 z3v61)) (= (z3f64 z3v66) z3v66))) +(assert (not (= (z3f97 z3v327) (smt_set_cup (z3f97 z3v327) (z3f97 z3v375))))) +(check-sat) diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 new file mode 100644 index 000000000..f37a8ccfe --- /dev/null +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 @@ -0,0 +1,106 @@ +(set-logic QF_ALL_SUPPORTED) +(set-info :status unsat) +(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_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2)) +(declare-fun z3v66 () Int) +(declare-fun z3v67 () Int) +(assert (distinct z3v66 z3v67)) +(declare-fun z3v68 () Int) +(declare-fun z3f69 (Int) Int) +(declare-fun z3f70 (Int) mySet) +(declare-fun z3v71 () Int) +(declare-fun z3f72 (Int) mySet) +(declare-fun z3v73 () Int) +(declare-fun z3v74 () Int) +(declare-fun z3v75 () Int) +(declare-fun z3f76 (Int) Bool) +(declare-fun z3f77 (Int Int) Int) +(declare-fun z3v78 () Int) +(declare-fun z3f79 (Int) Bool) +(declare-fun z3v80 () Int) +(declare-fun z3f81 (Int) Int) +(declare-fun z3v82 () Int) +(declare-fun z3v83 () Int) +(declare-fun z3v85 () Int) +(declare-fun z3v86 () Int) +(declare-fun z3v87 () Int) +(declare-fun z3f88 () Int) +(declare-fun z3v89 () Int) +(declare-fun z3v90 () Int) +(declare-fun z3v91 () Int) +(declare-fun z3v92 () Int) +(declare-fun z3v93 () Int) +(declare-fun z3f94 (Int) Int) +(declare-fun z3f95 (Int) Int) +(declare-fun z3f96 (Int Int Int) Int) +(declare-fun z3v97 () Int) +(declare-fun z3v98 () Int) +(declare-fun z3v99 () Int) +(assert (= z3v99 z3v98)) +(assert (and (>= (z3f69 z3v85) 0) + (not (smt_set_mem z3v86 (z3f70 z3v85))) + (= (z3f72 z3v85) smt_set_emp) + (>= (z3f69 z3v87) 0) + (= (z3f72 z3v87) smt_set_emp) + (= (z3f70 z3v87) smt_set_emp) + (= (z3f69 z3v87) 0) + (= (z3f76 z3v87) true) + (= z3v87 z3f88) + (>= (z3f69 z3v87) 0) + (= z3v87 z3v89) + (>= (z3f69 z3v87) 0) + (= (z3f70 z3v87) + (z3f70 z3v90)) + (= (z3f72 z3v87) smt_set_emp) + (>= (z3f69 z3v89) 0) + (= (z3f70 z3v89) + (z3f70 z3v90)) + (= (z3f72 z3v89) smt_set_emp) + (>= (z3f69 z3v90) 0) + (= (z3f72 z3v90) + (ite (smt_set_mem z3v86 (z3f70 z3v85)) + (smt_set_cup (smt_set_add smt_set_emp z3v86) + (z3f72 z3v85)) + (z3f72 z3v85))) + (= (z3f70 z3v90) + (smt_set_cup (smt_set_add smt_set_emp z3v86) + (z3f70 z3v85))) + (= (z3f69 z3v90) + (+ 1 (z3f69 z3v85))) + (= (z3f76 z3v90) false) + (>= (z3f69 z3v91) 0) + (= (z3f72 z3v91) smt_set_emp) + (= (z3f70 z3v91) smt_set_emp) + (= (z3f69 z3v91) 0) + (= (z3f76 z3v91) true) + (= z3v91 z3f88) + (>= (z3f69 z3v91) 0) + (= z3v91 z3v92) + (>= (z3f69 z3v91) 0) + (not (smt_set_mem z3v86 (z3f70 z3v91))) + (= (z3f72 z3v91) smt_set_emp) + (= (z3f94 z3v93) z3v92) + (= (z3f95 z3v93) z3v85) + (= z3v93 (z3f96 z3v86 z3v92 z3v85)) + (= z3v93 z3v97) + (= (smt_set_cap (z3f70 (z3f94 z3v93)) + (z3f70 (z3f95 z3v93))) smt_set_emp) + (>= (z3f69 z3v92) 0) + (not (smt_set_mem z3v86 (z3f70 z3v92))) + (= (z3f72 z3v92) smt_set_emp) + (= (smt_set_cap (z3f70 (z3f94 z3v97)) + (z3f70 (z3f95 z3v97))) smt_set_emp) + (z3f79 z3v66) + (= (z3f81 z3v80) z3v80) + (= (z3f81 z3v82) z3v82) + (not (z3f79 z3v67)) + (= (z3f81 z3v83) z3v83))) +(assert (not (> z3v99 z3v98))) +(check-sat) diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 new file mode 100644 index 000000000..59cc1a00e --- /dev/null +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 @@ -0,0 +1,227 @@ +(set-logic QF_ALL_SUPPORTED) +(set-info :status unsat) +(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 z3v66 () Int) +(declare-fun z3v67 () Int) +(assert (distinct z3v66 z3v67)) +(declare-fun z3v68 () Int) +(declare-fun z3f69 (Int) Int) +(declare-fun z3f70 (Int) mySet) +(declare-fun z3v71 () Int) +(declare-fun z3f72 (Int) mySet) +(declare-fun z3v73 () Int) +(declare-fun z3v74 () Int) +(declare-fun z3v75 () Int) +(declare-fun z3f76 (Int) Bool) +(declare-fun z3f77 (Int Int) Int) +(declare-fun z3v78 () Int) +(declare-fun z3f79 (Int) Bool) +(declare-fun z3v80 () Int) +(declare-fun z3f81 (Int) Int) +(declare-fun z3v82 () Int) +(declare-fun z3v83 () Int) +(declare-fun z3v85 () Int) +(declare-fun z3v86 () Int) +(declare-fun z3v87 () Int) +(declare-fun z3f88 () Int) +(declare-fun z3v89 () Int) +(declare-fun z3v90 () Int) +(declare-fun z3v91 () Int) +(declare-fun z3v92 () Int) +(declare-fun z3v93 () Int) +(declare-fun z3f94 (Int) Int) +(declare-fun z3f95 (Int) Int) +(declare-fun z3f96 (Int Int Int) Int) +(declare-fun z3v97 () Int) +(declare-fun z3v98 () Int) +(declare-fun z3v99 () Int) +(declare-fun z3v100 () Int) +(declare-fun z3v101 () Int) +(declare-fun z3v102 () Int) +(declare-fun z3v103 () Int) +(declare-fun z3v104 () Int) +(declare-fun z3v105 () Int) +(declare-fun z3v106 () Int) +(declare-fun z3v107 () Int) +(declare-fun z3v108 () Int) +(declare-fun z3v109 () Int) +(declare-fun z3v110 () Int) +(declare-fun z3v113 () Int) +(declare-fun z3v114 () Int) +(declare-fun z3v115 () Int) +(declare-fun z3v116 () Int) +(declare-fun z3v117 () Int) +(declare-fun z3v118 () Int) +(declare-fun z3v120 () Int) +(declare-fun z3v121 () Int) +(declare-fun z3v122 () Int) +(declare-fun z3v124 () Int) +(declare-fun z3v125 () Int) +(declare-fun z3v126 () Int) +(declare-fun z3v127 () Int) +(declare-fun z3v128 () Int) +(declare-fun z3v129 () Int) +(declare-fun z3v131 () Int) +(declare-fun z3v132 () Int) +(declare-fun z3v133 () Int) +(declare-fun z3v134 () Int) +(declare-fun z3v135 () Int) +(declare-fun z3v136 () Int) +(declare-fun z3v137 () Int) +(declare-fun z3v138 () Int) +(declare-fun z3v139 () Int) +(declare-fun z3v140 () Int) +(declare-fun z3v141 () Int) +(declare-fun z3v142 () Int) +(declare-fun z3v144 () Int) +(declare-fun z3v145 () Int) +(declare-fun z3v146 () Int) +(declare-fun z3v149 () Int) +(declare-fun z3v151 () Int) +(declare-fun z3v154 () Int) +(declare-fun z3v155 () Int) +(declare-fun z3v156 () Int) +(declare-fun z3v157 () Int) +(declare-fun z3v158 () Int) +(declare-fun z3v159 () Int) +(declare-fun z3v161 () Int) +(declare-fun z3v163 () Int) +(declare-fun z3v164 () Int) +(declare-fun z3v165 () Int) +(declare-fun z3v167 () Int) +(declare-fun z3v170 () Int) +(declare-fun z3v174 () Int) +(declare-fun z3v175 () Int) +(declare-fun z3v176 () Int) +(declare-fun z3v179 () Int) +(declare-fun z3v181 () Int) +(declare-fun z3v182 () Int) +(declare-fun z3v183 () Int) +(declare-fun z3v184 () Int) +(declare-fun z3v187 () Int) +(declare-fun z3v188 () Int) +(declare-fun z3v189 () Int) +(declare-fun z3v190 () Int) +(declare-fun z3f191 (Int) Int) +(declare-fun z3f192 (Int) Int) +(declare-fun z3v195 () Int) +(declare-fun z3v196 () Int) +(declare-fun z3v199 () Int) +(declare-fun z3v200 () Int) +(declare-fun z3v201 () Int) +(declare-fun z3v202 () Int) +(declare-fun z3v203 () Int) +(declare-fun z3v206 () Int) +(declare-fun z3v207 () Int) +(declare-fun z3v208 () Int) +(declare-fun z3v210 () Int) +(declare-fun z3v211 () Int) +(declare-fun z3v212 () Int) +(declare-fun z3f213 (Int) Bool) +(declare-fun z3f214 (Int) Int) +(declare-fun z3v215 () Int) +(declare-fun z3v216 () Int) +(declare-fun z3v218 () Int) +(declare-fun z3v220 () Int) +(declare-fun z3v221 () Int) +(declare-fun z3v222 () Int) +(declare-fun z3v223 () Int) +(declare-fun z3v224 () Int) +(declare-fun z3v225 () Int) +(declare-fun z3v226 () Int) +(declare-fun z3v227 () Int) +(declare-fun z3v228 () Int) +(declare-fun z3v229 () Int) +(declare-fun z3v230 () Int) +(declare-fun z3v231 () Int) +(declare-fun z3v233 () Int) +(declare-fun z3v236 () Int) +(declare-fun z3v242 () Int) +(declare-fun z3v243 () Int) +(declare-fun z3v244 () Int) +(declare-fun z3v245 () Int) +(declare-fun z3v247 () Int) +(declare-fun z3v248 () Int) +(declare-fun z3v249 () Int) +(declare-fun z3v250 () Int) +(declare-fun z3v251 () Int) +(declare-fun z3v252 () Int) +(declare-fun z3v253 () Int) +(declare-fun z3v255 () Int) +(declare-fun z3v256 () Int) +(declare-fun z3v258 () Int) +(declare-fun z3v259 () Int) +(declare-fun z3v261 () Int) +(declare-fun z3v262 () Int) +(declare-fun z3v263 () Int) +(declare-fun z3v264 () Int) +(declare-fun z3v266 () Int) +(declare-fun z3v268 () Int) +(declare-fun z3v270 () Int) +(declare-fun z3v271 () Int) +(declare-fun z3v272 () Int) +(declare-fun z3v274 () Int) +(declare-fun z3v275 () Int) +(declare-fun z3v276 () Int) +(declare-fun z3v278 () Int) +(declare-fun z3v279 () Int) +(declare-fun z3v281 () Int) +(declare-fun z3v282 () Int) +(declare-fun z3v283 () Int) +(declare-fun z3v284 () Int) +(declare-fun z3v285 () Int) +(declare-fun z3v287 () Int) +(declare-fun z3v289 () Int) +(declare-fun z3v290 () Int) +(declare-fun z3v291 () Int) +(declare-fun z3v292 () Int) +(declare-fun z3v293 () Int) +(declare-fun z3v296 () Int) +(declare-fun z3v298 () Int) +(declare-fun z3v299 () Int) +(declare-fun z3f300 (Int Int) Int) +(declare-fun z3v301 () Int) +(declare-fun z3v302 () Int) +(declare-fun z3v303 () Int) +(declare-fun z3v304 () Int) +(declare-fun z3v308 () Int) +(declare-fun z3v309 () Int) +(declare-fun z3v310 () Int) +(declare-fun z3v314 () Int) +(declare-fun z3v315 () Int) +(declare-fun z3v316 () Int) +(declare-fun z3v317 () Int) +(declare-fun z3v318 () Int) +(declare-fun z3v319 () Int) +(declare-fun z3v320 () Int) +(declare-fun z3v324 () Int) +(declare-fun z3v325 () Int) +(declare-fun z3v326 () Int) +(declare-fun z3v327 () Int) +(declare-fun z3v328 () Int) +(declare-fun z3v330 () Int) +(declare-fun z3v332 () Int) +(declare-fun z3v333 () Int) +(declare-fun z3v334 () Int) +(declare-fun z3v335 () Int) +(declare-fun z3v336 () Int) +(declare-fun z3v337 () Int) +(declare-fun z3v339 () Int) +(declare-fun z3v340 () Int) +(declare-fun z3v341 () Int) +(declare-fun z3v342 () Int) +(assert (= z3v342 z3v113)) +(assert (>= (z3f69 z3v342) 0)) +(assert (and (>= (z3f69 z3v113) 0) (>= (z3f69 z3v114) 0) (= (z3f72 z3v114) smt_set_emp) (= (z3f70 z3v114) smt_set_emp) (= (z3f69 z3v114) 0) (= (z3f76 z3v114) true) (>= (z3f69 z3v115) 0) (= (z3f72 z3v115) (ite (smt_set_mem z3v116 (z3f70 z3v113)) (smt_set_cup (smt_set_add smt_set_emp z3v116) (z3f72 z3v113)) (z3f72 z3v113))) (= (z3f70 z3v115) (smt_set_cup (smt_set_add smt_set_emp z3v116) (z3f70 z3v113))) (= (z3f69 z3v115) (+ 1 (z3f69 z3v113))) (= (z3f76 z3v115) false) (= z3v115 (z3f77 z3v116 z3v113)) (>= (z3f69 z3v115) 0) (= z3v115 z3v117) (>= (z3f69 z3v115) 0) (= (z3f72 z3v115) smt_set_emp) (>= (z3f69 z3v117) 0) (= (z3f72 z3v117) smt_set_emp) (z3f79 z3v66) (= (z3f81 z3v80) z3v80) (= (z3f81 z3v82) z3v82) (not (z3f79 z3v67)) (= (z3f81 z3v83) z3v83))) +(assert (not (and (= (z3f72 z3v342) smt_set_emp) (not (smt_set_mem z3v116 (z3f70 z3v342)))))) +(check-sat) diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 new file mode 100644 index 000000000..5fa5101f0 --- /dev/null +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 @@ -0,0 +1,27 @@ +(set-logic QF_ALL_SUPPORTED) +(set-info :status unsat) + +; Observed +; +; sat as output instead of unsat +; +; What was going on? +; +; The solver was unable to reason that (emptyset) cannot equal +; (setenum 0). There were no membership predicates anywhere, just +; equalities. +; +; Fix +; +; Add the propagation rule: (true) => (in x (setenum x)) + +(declare-fun z3f70 (Int) (Set Int)) +(declare-fun z3v85 () Int) +(declare-fun z3v86 () Int) +(declare-fun z3v87 () Int) +(declare-fun z3v90 () Int) + +(assert (= (z3f70 z3v90) (union (z3f70 z3v85) (union (as emptyset (Set Int)) (setenum z3v86))))) +(assert (= (z3f70 z3v90) (z3f70 z3v87))) +(assert (= (as emptyset (Set Int)) (z3f70 z3v87))) +(check-sat) diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 new file mode 100644 index 000000000..d01b7468e --- /dev/null +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 @@ -0,0 +1,18 @@ +(set-logic QF_ALL_SUPPORTED) +(set-info :status unsat) +(define-sort Elt () Int) +(define-sort mySet () + (Set Elt )) +(define-fun smt_set_emp () mySet (as emptyset mySet)) + +(declare-fun S () (Set Int)) +(declare-fun T () (Set Int)) +(declare-fun x () Int) + +(assert (or (not (= S smt_set_emp)) (in x T))) + +(assert (= smt_set_emp + (ite (in x T) + (union (union smt_set_emp (setenum x)) S) + S))) +(check-sat) diff --git a/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 new file mode 100644 index 000000000..57d5d72ca --- /dev/null +++ b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 @@ -0,0 +1,149 @@ +(set-option :print-success false) +(set-logic AUFLIA_SETS) +(set-info :status unsat) +(declare-sort Loc 0) +(define-sort SetLoc () (Set Loc)) +(define-sort SetInt () (Set Int)) +(declare-sort FldLoc 0) +(declare-sort FldInt 0) +(declare-fun null$0 () Loc) +(declare-fun read$0 (FldLoc Loc) Loc) +(declare-fun Btwn$0 (FldLoc Loc Loc Loc) Bool) +(declare-fun Alloc$0 () SetLoc) +(declare-fun Alloc_2$0 () SetLoc) +(declare-fun FP$0 () SetLoc) +(declare-fun FP_3$0 () SetLoc) +(declare-fun FP_Caller$0 () SetLoc) +(declare-fun FP_Caller_2$0 () SetLoc) +(declare-fun cp$0 () Loc) +(declare-fun cp_1$0 () Loc) +(declare-fun curr$0 () Loc) +(declare-fun lseg_domain$0 (FldLoc Loc Loc) SetLoc) +(declare-fun lseg_struct$0 (SetLoc FldLoc Loc Loc) Bool) +(declare-fun next$0 () FldLoc) +(declare-fun old_cp_2$0 () Loc) +(declare-fun sk_?X_36$0 () SetLoc) +(declare-fun sk_?X_37$0 () SetLoc) +(declare-fun sk_?X_38$0 () SetLoc) +(declare-fun tmp_1$0 () Loc) + +(assert (! (forall ((?y Loc)) + (or (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y) + (Btwn$0 next$0 null$0 (read$0 next$0 null$0) ?y))) + :named btwn_reach_6)) + +(assert (! (forall ((?y Loc)) + (or (not (= (read$0 next$0 null$0) null$0)) + (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y))) + :named btwn_cycl_6)) + +(assert (! (Btwn$0 next$0 null$0 (read$0 next$0 null$0) (read$0 next$0 null$0)) + :named btwn_step_6)) + +(assert (! (= (read$0 next$0 null$0) null$0) :named read_null_6)) + +(assert (! (forall ((l1 Loc)) + (or + (and (Btwn$0 next$0 curr$0 l1 null$0) + (in l1 (lseg_domain$0 next$0 curr$0 null$0)) + (not (= l1 null$0))) + (and (or (= l1 null$0) (not (Btwn$0 next$0 curr$0 l1 null$0))) + (not (in l1 (lseg_domain$0 next$0 curr$0 null$0)))))) + :named lseg_footprint_14)) + +(assert (! (not (in tmp_1$0 Alloc$0)) :named new_42_10)) + +(assert (! (not (in null$0 Alloc$0)) + :named initial_footprint_of_rec_copy_loop_34_11_4)) + +(assert (! (not (= curr$0 null$0)) :named if_else_37_6)) + +(assert (! (lseg_struct$0 sk_?X_37$0 next$0 curr$0 null$0) + :named precondition_of_rec_copy_loop_34_11_16)) + +(assert (! (= sk_?X_38$0 (lseg_domain$0 next$0 cp$0 null$0)) + :named precondition_of_rec_copy_loop_34_11_17)) + +(assert (! (= sk_?X_36$0 FP$0) :named precondition_of_rec_copy_loop_34_11_18)) + +(assert (! (= (as emptyset SetLoc) (intersection sk_?X_38$0 sk_?X_37$0)) + :named precondition_of_rec_copy_loop_34_11_19)) + +(assert (! (= old_cp_2$0 cp$0) :named assign_41_4)) + +(assert (! (= FP_Caller_2$0 (setminus FP_Caller$0 FP$0)) :named assign_37_2_2)) + +(assert (! (= Alloc_2$0 (union Alloc$0 (setenum tmp_1$0))) :named assign_42_10)) + +(assert (! (or (Btwn$0 next$0 cp$0 null$0 null$0) + (not (lseg_struct$0 sk_?X_38$0 next$0 cp$0 null$0))) + :named unnamed_22)) + +(assert (! (forall ((l1 Loc)) + (or + (and (Btwn$0 next$0 cp$0 l1 null$0) + (in l1 (lseg_domain$0 next$0 cp$0 null$0)) + (not (= l1 null$0))) + (and (or (= l1 null$0) (not (Btwn$0 next$0 cp$0 l1 null$0))) + (not (in l1 (lseg_domain$0 next$0 cp$0 null$0)))))) + :named lseg_footprint_15)) + +(assert (! (not (in cp_1$0 FP_3$0)) :named check_heap_access_43_4)) + +(assert (! (not (= tmp_1$0 null$0)) :named new_42_10_1)) + +(assert (! (lseg_struct$0 sk_?X_38$0 next$0 cp$0 null$0) + :named precondition_of_rec_copy_loop_34_11_20)) + +(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0)) + :named precondition_of_rec_copy_loop_34_11_21)) + +(assert (! (= sk_?X_37$0 (lseg_domain$0 next$0 curr$0 null$0)) + :named precondition_of_rec_copy_loop_34_11_22)) + +(assert (! (= sk_?X_36$0 (union sk_?X_37$0 sk_?X_38$0)) + :named precondition_of_rec_copy_loop_34_11_23)) + +(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0)) + :named initial_footprint_of_rec_copy_loop_34_11_5)) + +(assert (! (= cp_1$0 tmp_1$0) :named assign_42_4)) + +(assert (! (= FP_3$0 (union FP$0 (setenum tmp_1$0))) :named assign_42_10_1)) + +(assert (! (or (Btwn$0 next$0 curr$0 null$0 null$0) + (not (lseg_struct$0 sk_?X_37$0 next$0 curr$0 null$0))) + :named unnamed_23)) + +(assert (! (forall ((?x Loc)) (Btwn$0 next$0 ?x ?x ?x)) :named btwn_refl_6)) + +(assert (! (forall ((?x Loc) (?y Loc)) (or (not (Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y))) + :named btwn_sndw_6)) + +(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) + (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?x ?z ?z)) + (Btwn$0 next$0 ?x ?y ?z) (Btwn$0 next$0 ?x ?z ?y))) + :named btwn_ord1_6)) + +(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) + (or (not (Btwn$0 next$0 ?x ?y ?z)) + (and (Btwn$0 next$0 ?x ?y ?y) (Btwn$0 next$0 ?y ?z ?z)))) + :named btwn_ord2_6)) + +(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) + (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?y ?z ?z)) + (Btwn$0 next$0 ?x ?z ?z))) + :named btwn_trn1_6)) + +(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc)) + (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?y ?u ?z)) + (and (Btwn$0 next$0 ?x ?y ?u) (Btwn$0 next$0 ?x ?u ?z)))) + :named btwn_trn2_6)) + +(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc)) + (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?x ?u ?y)) + (and (Btwn$0 next$0 ?x ?u ?z) (Btwn$0 next$0 ?u ?y ?z)))) + :named btwn_trn3_6)) + +(check-sat) +(exit) diff --git a/test/regress/regress0/sets/setel-eq.smt2 b/test/regress/regress0/sets/setel-eq.smt2 new file mode 100644 index 000000000..8ed9a2e57 --- /dev/null +++ b/test/regress/regress0/sets/setel-eq.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-fun S () (Set Int)) +(declare-fun T () (Set Int)) +(declare-fun x () Int) +(declare-fun y () Int) +(assert (in y S)) +(assert (not (in x (union S T)))) +(assert (= x y)) +(check-sat) diff --git a/test/regress/regress0/sets/sets-equal.smt2 b/test/regress/regress0/sets/sets-equal.smt2 new file mode 100644 index 000000000..a2ce4b3c2 --- /dev/null +++ b/test/regress/regress0/sets/sets-equal.smt2 @@ -0,0 +1,14 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun z () Int) +(assert (= x y)) +(declare-fun a () (Set Int)) +(declare-fun b () (Set Int)) +(assert (not (in x a))) +(assert (in y (union a b))) +(assert (= x z)) +(assert (not (in z a))) +(assert (= a b)) +(check-sat) diff --git a/test/regress/regress0/sets/sets-inter.smt2 b/test/regress/regress0/sets/sets-inter.smt2 new file mode 100644 index 000000000..0f5e41864 --- /dev/null +++ b/test/regress/regress0/sets/sets-inter.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(define-sort SetInt () (Set Int)) +(declare-fun a () (Set Int)) +(declare-fun b () (Set Int)) +(declare-fun x () Int) +;(assert (not (in x a))) +(assert (in x (intersection a b))) +(assert (not (in x b))) +(check-sat) +(exit) diff --git a/test/regress/regress0/sets/sets-new.smt2 b/test/regress/regress0/sets/sets-new.smt2 new file mode 100644 index 000000000..c85ae4837 --- /dev/null +++ b/test/regress/regress0/sets/sets-new.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(define-sort SetInt () (Set Int)) + +(declare-fun A () SetInt) +(declare-fun B () SetInt) +(declare-fun x () Int) +(assert (in x (union A B))) + +(assert (not (in x (intersection A B)))) +(assert (not (in x (setminus A B)))) +;(assert (not (in x (setminus B A)))) +;(assert (in x B)) + +(check-sat) diff --git a/test/regress/regress0/sets/sets-sample.smt2 b/test/regress/regress0/sets/sets-sample.smt2 new file mode 100644 index 000000000..1bd0eb396 --- /dev/null +++ b/test/regress/regress0/sets/sets-sample.smt2 @@ -0,0 +1,64 @@ +; COMMAND-LINE: --incremental +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(define-sort SetInt () (Set Int)) + +; Something simple to test parsing +(push 1) +(declare-fun a () (Set Int)) +(declare-fun b () (Set Int)) +(declare-fun c () (Set Int)) +(declare-fun e () Int) +(assert (= a (setenum 5))) +(assert (= c (union a b) )) +(assert (not (= c (intersection a b) ))) +(assert (= c (setminus a b) )) +(assert (subseteq a b)) +(assert (in e c)) +(assert (in e a)) +(assert (in e (intersection a b))) +(check-sat) +(pop 1) + +; UF can tell that this is UNSAT (union) +(push 1) +(declare-fun x () (Set Int)) +(declare-fun y () (Set Int)) +(declare-fun z () (Set Int)) +(assert (= x y)) +(assert (not (= (union x z) (union y z)))) +(check-sat) +(pop 1) + +; UF can tell that this is UNSAT (containment) +(push 1) +(declare-fun x () (Set Int)) +(declare-fun y () (Set Int)) +(declare-fun e1 () Int) +(declare-fun e2 () Int) +(assert (= x y)) +(assert (= e1 e2)) +(assert (in e1 x)) +(assert (not (in e2 y))) +(check-sat) +(pop 1) + +; UF can tell that this is UNSAT (merge union + containment examples) +(push 1) +(declare-fun x () (Set Int)) +(declare-fun y () (Set Int)) +(declare-fun z () (Set Int)) +(declare-fun e1 () Int) +(declare-fun e2 () Int) +(assert (= x y)) +(assert (= e1 e2)) +(assert (in e1 (union x z))) +(assert (not (in e2 (union y z)))) +(check-sat) +(pop 1) + +(exit) +(exit) diff --git a/test/regress/regress0/sets/sets-sharing.smt2 b/test/regress/regress0/sets/sets-sharing.smt2 new file mode 100644 index 000000000..d2a94fdf4 --- /dev/null +++ b/test/regress/regress0/sets/sets-sharing.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-fun S () (Set Int)) +(declare-fun x () Int) + +(assert (in (+ 5 x) S)) +(assert (not (in 9 S))) +(assert (= x 4)) + +(check-sat) diff --git a/test/regress/regress0/sets/sets-testlemma.smt2 b/test/regress/regress0/sets/sets-testlemma.smt2 new file mode 100644 index 000000000..74ce72747 --- /dev/null +++ b/test/regress/regress0/sets/sets-testlemma.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic QF_UFLIA_SETS) +(set-info :status sat) +(declare-fun x () (Set (_ BitVec 2))) +(declare-fun y () (Set (_ BitVec 2))) +(assert (not (= x y))) +(check-sat) diff --git a/test/regress/regress0/sets/sets-union.smt2 b/test/regress/regress0/sets/sets-union.smt2 new file mode 100644 index 000000000..6f6d3e019 --- /dev/null +++ b/test/regress/regress0/sets/sets-union.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --incremental --no-check-model +; EXPECT: sat +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(define-sort SetInt () (Set Int)) +(declare-fun a () (Set Int)) +(declare-fun b () (Set Int)) +(declare-fun x () Int) +(assert (not (in x a))) +(assert (in x (union a b))) +(check-sat) +;(get-model) +(assert (not (in x b))) +(check-sat) +(exit) diff --git a/test/regress/regress0/sets/union-1a-flip.smt2 b/test/regress/regress0/sets/union-1a-flip.smt2 new file mode 100644 index 000000000..59c2a2024 --- /dev/null +++ b/test/regress/regress0/sets/union-1a-flip.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --incremental --no-check-models +; EXPECT: unsat +; EXPECT: sat + +; x not in A U B => x not in A +(set-logic ALL_SUPPORTED) +(define-sort SetInt () (Set Int)) +(declare-fun A () (Set Int)) +(declare-fun B () (Set Int)) +(declare-fun x () Int) +(assert (in x A)) +(push 1) +(assert (not (in x (union A B)))) +(check-sat) +(pop 1) +(check-sat) diff --git a/test/regress/regress0/sets/union-1a.smt2 b/test/regress/regress0/sets/union-1a.smt2 new file mode 100644 index 000000000..b594ac74d --- /dev/null +++ b/test/regress/regress0/sets/union-1a.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --incremental +; EXPECT: unsat +; EXPECT: sat + +; x not in A U B => x not in A +(set-logic ALL_SUPPORTED) +(define-sort SetInt () (Set Int)) +(declare-fun A () (Set Int)) +(declare-fun B () (Set Int)) +(declare-fun x () Int) +(assert (not (in x (union A B)))) +(push 1) +(assert (in x A)) +(check-sat) +(pop 1) +(check-sat) diff --git a/test/regress/regress0/sets/union-1b-flip.smt2 b/test/regress/regress0/sets/union-1b-flip.smt2 new file mode 100644 index 000000000..86fed459b --- /dev/null +++ b/test/regress/regress0/sets/union-1b-flip.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --incremental --no-check-models +; EXPECT: unsat +; EXPECT: sat + +; x not in A U B => x not in A +(set-logic ALL_SUPPORTED) +(define-sort SetInt () (Set Int)) +(declare-fun A () (Set Int)) +(declare-fun B () (Set Int)) +(declare-fun x () Int) +(assert (in x B)) +(push 1) +(assert (not (in x (union A B)))) +(check-sat) +(pop 1) +(check-sat) diff --git a/test/regress/regress0/sets/union-1b.smt2 b/test/regress/regress0/sets/union-1b.smt2 new file mode 100644 index 000000000..85fce759c --- /dev/null +++ b/test/regress/regress0/sets/union-1b.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --incremental +; EXPECT: unsat +; EXPECT: sat + +; x not in A U B => x not in A +(set-logic ALL_SUPPORTED) +(define-sort SetInt () (Set Int)) +(declare-fun A () (Set Int)) +(declare-fun B () (Set Int)) +(declare-fun x () Int) +(assert (not (in x (union A B)))) +(push 1) +(assert (in x B)) +(check-sat) +(pop 1) +(check-sat) diff --git a/test/regress/regress0/sets/union-2.smt2 b/test/regress/regress0/sets/union-2.smt2 new file mode 100644 index 000000000..32d949a53 --- /dev/null +++ b/test/regress/regress0/sets/union-2.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(define-sort SetInt () (Set Int)) +(declare-fun A () (Set Int)) +(declare-fun B () (Set Int)) +(declare-fun x () Int) +(declare-fun y () Int) +(assert (in x (union A B))) +(assert (not (in y A))) +(assert (not (in y B))) +(check-sat) diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h index 5f6a93ae7..f569d6389 100644 --- a/test/unit/theory/logic_info_white.h +++ b/test/unit/theory/logic_info_white.h @@ -512,6 +512,7 @@ public: info = info.getUnlockedCopy(); TS_ASSERT( !info.isLocked() ); info.disableTheory(THEORY_STRINGS); + info.disableTheory(THEORY_SETS); info.arithOnlyLinear(); info.disableIntegers(); info.lock(); |