From 50c26544c83a71e87efa487e4af063b1b5647c0f Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Mon, 9 Sep 2013 14:47:53 -0400 Subject: 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 --- .../rewriterules/set_A_new_fast_tableau-base.smt2 | 68 +++++++++++----------- .../set_A_new_fast_tableau-base_sat.smt2 | 66 ++++++++++----------- 2 files changed, 67 insertions(+), 67 deletions(-) (limited to 'test/regress/regress0/rewriterules') 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) -- cgit v1.2.3