From: Kshitij Bansal Date: Tue, 24 Jun 2014 18:29:12 +0000 (-0400) Subject: rename subseteq to subset in smtlib, all kinds and smt operator names are now consistent X-Git-Tag: cvc5-1.0.0~6712^2~7 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2a734a31217cd17bd1d51abb621b0cb409973285;p=cvc5.git rename subseteq to subset in smtlib, all kinds and smt operator names are now consistent --- diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp index 5257915b0..14df2fac0 100644 --- a/examples/sets-translate/sets_translate.cpp +++ b/examples/sets-translate/sets_translate.cpp @@ -44,37 +44,37 @@ const bool enableAxioms = false; #endif string setaxioms[] = { - "(declare-fun inHOLDA (HOLDB (Set HOLDB)) Bool)", + "(declare-fun memberHOLDA (HOLDB (Set HOLDB)) Bool)", "", "(declare-fun unionHOLDA ((Set HOLDB) (Set HOLDB)) (Set HOLDB))", "(assert (forall ((?X (Set HOLDB)) (?Y (Set HOLDB)) (?x HOLDB))", - " (= (inHOLDA ?x (unionHOLDA ?X ?Y))", - " (or (inHOLDA ?x ?X) (inHOLDA ?x ?Y))", + " (= (memberHOLDA ?x (unionHOLDA ?X ?Y))", + " (or (memberHOLDA ?x ?X) (memberHOLDA ?x ?Y))", " ) ) )", "", "", "(declare-fun intersectionHOLDA ((Set HOLDB) (Set HOLDB)) (Set HOLDB))", "(assert (forall ((?X (Set HOLDB)) (?Y (Set HOLDB)) (?x HOLDB))", - " (= (inHOLDA ?x (intersectionHOLDA ?X ?Y))", - " (and (inHOLDA ?x ?X) (inHOLDA ?x ?Y))", + " (= (memberHOLDA ?x (intersectionHOLDA ?X ?Y))", + " (and (memberHOLDA ?x ?X) (memberHOLDA ?x ?Y))", " ) ) )", "", "(declare-fun setminusHOLDA ((Set HOLDB) (Set HOLDB)) (Set HOLDB))", "(assert (forall ((?X (Set HOLDB)) (?Y (Set HOLDB)) (?x HOLDB))", - " (= (inHOLDA ?x (setminusHOLDA ?X ?Y))", - " (and (inHOLDA ?x ?X) (not (inHOLDA ?x ?Y)))", + " (= (memberHOLDA ?x (setminusHOLDA ?X ?Y))", + " (and (memberHOLDA ?x ?X) (not (memberHOLDA ?x ?Y)))", " ) ) )", "", - "(declare-fun setenumHOLDA (HOLDB) (Set HOLDB))", + "(declare-fun singletonHOLDA (HOLDB) (Set HOLDB))", "(assert (forall ((?x HOLDB) (?y HOLDB))", - " (= (inHOLDA ?x (setenumHOLDA ?y))", + " (= (memberHOLDA ?x (singletonHOLDA ?y))", " (= ?x ?y)", " ) ) )", "", "(declare-fun emptysetHOLDA () (Set HOLDB))", - "(assert (forall ((?x HOLDB)) (not (inHOLDA ?x emptysetHOLDA)) ) )", + "(assert (forall ((?x HOLDB)) (not (memberHOLDA ?x emptysetHOLDA)) ) )", "", - "(define-fun subseteqHOLDA ((X (Set HOLDB)) (Y (Set HOLDB))) Bool (= (unionHOLDA X Y) Y))", + "(define-fun subsetHOLDA ((X (Set HOLDB)) (Y (Set HOLDB))) Bool (= (unionHOLDA X Y) Y))", "" }; @@ -123,12 +123,12 @@ class Mapper { t); if(!enableAxioms) - sout << "(define-fun setenum" << elementTypeAsString << " " + sout << "(define-fun singleton" << elementTypeAsString << " " << " ( (x " << elementType << ") )" << " " << name << "" << " (store emptyset" << elementTypeAsString << " x true) )" << endl; setoperators[ make_pair(t, kind::SINGLETON) ] = - em->mkVar( std::string("setenum") + elementTypeAsString, + em->mkVar( std::string("singleton") + elementTypeAsString, em->mkFunctionType( elementType, t ) ); if(!enableAxioms) @@ -164,16 +164,16 @@ class Mapper { << " Bool" << " (select s x) )" << endl; setoperators[ make_pair(t, kind::MEMBER) ] = - em->mkVar( std::string("in") + elementTypeAsString, + em->mkVar( std::string("member") + elementTypeAsString, em->mkPredicateType( elet_t ) ); if(!enableAxioms) - sout << "(define-fun subseteq" << elementTypeAsString << " " + sout << "(define-fun subset" << elementTypeAsString << " " << " ( (s1 " << name << ") (s2 " << name << ") )" << " Bool" <<" (= emptyset" << elementTypeAsString << " (setminus" << elementTypeAsString << " s1 s2)) )" << endl; setoperators[ make_pair(t, kind::SUBSET) ] = - em->mkVar( std::string("subseteq") + elementTypeAsString, + em->mkVar( std::string("subset") + elementTypeAsString, em->mkPredicateType( t_t ) ); if(enableAxioms) { diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index a0d759cc2..3f1e59e6d 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -149,7 +149,7 @@ void Smt2::addTheory(Theory theory) { addOperator(kind::UNION, "union"); addOperator(kind::INTERSECTION, "intersection"); addOperator(kind::SETMINUS, "setminus"); - addOperator(kind::SUBSET, "subseteq"); + addOperator(kind::SUBSET, "subset"); addOperator(kind::MEMBER, "member"); addOperator(kind::SINGLETON, "singleton"); break; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index dbdc65ba9..3c0f4ebc5 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -609,7 +609,7 @@ static string smtKindString(Kind k) throw() { case kind::UNION: return "union"; case kind::INTERSECTION: return "intersection"; case kind::SETMINUS: return "setminus"; - case kind::SUBSET: return "subseteq"; + case kind::SUBSET: return "subset"; case kind::MEMBER: return "member"; case kind::SET_TYPE: return "Set"; case kind::SINGLETON: return "singleton"; 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)))