diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-24 14:29:12 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-25 13:42:38 -0400 |
commit | 2a734a31217cd17bd1d51abb621b0cb409973285 (patch) | |
tree | e2c814407e992f27f6db54eaafa9b6b77f7f518a /test | |
parent | b8ddf766460bfcf475e08ff52c889246e78f76cc (diff) |
rename subseteq to subset in smtlib, all kinds and smt operator names are now consistent
Diffstat (limited to 'test')
12 files changed, 13 insertions, 13 deletions
diff --git a/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 index 87cb9b73d..7b5294aec 100644 --- a/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 +++ b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 @@ -11,7 +11,7 @@ ;(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)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3v58 () Int) (declare-fun z3v59 () Int) (assert (distinct z3v58 z3v59)) 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 index bc919673d..71bb8a3e6 100644 --- a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 +++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 @@ -10,7 +10,7 @@ (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)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3v58 () Int) (declare-fun z3v59 () Int) (assert (distinct z3v58 z3v59)) 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 index f055a8e1c..eb48b023a 100644 --- a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 +++ b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 @@ -10,7 +10,7 @@ ;(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)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3v54 () Int) (declare-fun z3f55 (Int) Int) (declare-fun z3v56 () Int) 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 index 81b8794e5..3c0ef1dda 100644 --- a/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2 +++ b/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2 @@ -16,7 +16,7 @@ ;(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)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3v56 () Int) (declare-fun z3v57 () Int) (assert (distinct z3v56 z3v57)) diff --git a/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 index 8b84c9153..83dfe41e5 100644 --- a/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 +++ b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 @@ -11,7 +11,7 @@ ;(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)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3v58 () Int) (declare-fun z3v59 () Int) (assert (distinct z3v58 z3v59)) diff --git a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 index ac5fdf48d..282325f14 100644 --- a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 +++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 @@ -11,7 +11,7 @@ ;(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)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3v60 () Int) (declare-fun z3v61 () Int) (assert (distinct z3v60 z3v61)) 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 index e17911327..10ed4be7c 100644 --- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 @@ -8,7 +8,7 @@ (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)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3v66 () Int) (declare-fun z3v67 () Int) (assert (distinct z3v66 z3v67)) 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 index bea016683..6165b98de 100644 --- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 @@ -10,7 +10,7 @@ ;(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)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3v66 () Int) (declare-fun z3v67 () Int) (assert (distinct z3v66 z3v67)) diff --git a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 index 9175a8723..38477c46a 100644 --- a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 +++ b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 @@ -8,7 +8,7 @@ (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)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3v66 () Int) (declare-fun z3v67 () Int) diff --git a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 index 81117134c..e282e446e 100644 --- a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 +++ b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 @@ -8,7 +8,7 @@ (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)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3f70 (Int) mySet) (declare-fun z3f72 (Int) mySet) @@ -177,7 +177,7 @@ (z3f70 z3v270)))) (assert (= z3v242 (z3f77 z3v271 z3v270))) (assert (= z3v242 z3v243)) -(assert (subseteq (z3f70 z3v242) +(assert (subset (z3f70 z3v242) (z3f70 z3v244))) (assert (= (z3f72 z3v243) smt_set_emp)) (assert (= (z3f72 z3v244) diff --git a/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 index 1e848695d..0fc8ca067 100644 --- a/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 +++ b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 @@ -31,7 +31,7 @@ ;(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)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3v58 () Int) (declare-fun z3v59 () Int) diff --git a/test/regress/regress0/sets/sets-sample.smt2 b/test/regress/regress0/sets/sets-sample.smt2 index 4838c6cf2..a040b0bec 100644 --- a/test/regress/regress0/sets/sets-sample.smt2 +++ b/test/regress/regress0/sets/sets-sample.smt2 @@ -16,7 +16,7 @@ (assert (= c (union a b) )) (assert (not (= c (intersection a b) ))) (assert (= c (setminus a b) )) -(assert (subseteq a b)) +(assert (subset a b)) (assert (member e c)) (assert (member e a)) (assert (member e (intersection a b))) |