From: Aina Niemetz Date: Tue, 9 Nov 2021 18:07:11 +0000 (-0800) Subject: sets: Update theory reference and smt2 examples. (#7602) X-Git-Tag: cvc5-1.0.0~849 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=15aa8ebd3acacc9b69a77f1892a7895e444759bb;p=cvc5.git sets: Update theory reference and smt2 examples. (#7602) --- diff --git a/docs/theories/sets-and-relations.rst b/docs/theories/sets-and-relations.rst index 88671a837..423a5d4b1 100644 --- a/docs/theories/sets-and-relations.rst +++ b/docs/theories/sets-and-relations.rst @@ -25,62 +25,62 @@ predicates. More details can be found in :cite:`BansalBRT17`. For the C++ API examples in the table below, we assume that we have created a `cvc5::api::Solver solver` object. -+----------------------+----------------------------------------------+--------------------------------------------------------------------+ -| | SMTLIB language | C++ API | -+----------------------+----------------------------------------------+--------------------------------------------------------------------+ -| Logic String | append `FS` for finite sets | append `FS` for finite sets | -| | | | -| | ``(set-logic QF_UFLIAFS)`` | ``solver.setLogic("QF_UFLIAFS");`` | -+----------------------+----------------------------------------------+--------------------------------------------------------------------+ -| Sort | ``(Set )`` | ``solver.mkSetSort(cvc5::api::Sort elementSort);`` | -+----------------------+----------------------------------------------+--------------------------------------------------------------------+ -| Constants | ``(declare-const X (Set Int)`` | ``Sort s = solver.mkSetSort(solver.getIntegerSort());`` | -| | | | -| | | ``Term X = solver.mkConst(s, "X");`` | -+----------------------+----------------------------------------------+--------------------------------------------------------------------+ -| Union | ``(union X Y)`` | ``Term Y = solver.mkConst(s, "Y");`` | -| | | | -| | | ``Term t = solver.mkTerm(Kind::UNION, X, Y);`` | -+----------------------+----------------------------------------------+--------------------------------------------------------------------+ -| Intersection | ``(setminus X Y)`` | ``Term t = solver.mkTerm(Kind::SETMINUS, X, Y);`` | -+----------------------+----------------------------------------------+--------------------------------------------------------------------+ -| Membership | ``(member x X)`` | ``Term x = solver.mkConst(solver.getIntegerSort(), "x");`` | -| | | | -| | | ``Term t = solver.mkTerm(Kind::MEMBER, x, X);`` | -+----------------------+----------------------------------------------+--------------------------------------------------------------------+ -| Subset | ``(subset X Y)`` | ``Term t = solver.mkTerm(Kind::SUBSET, X, Y);`` | -+----------------------+----------------------------------------------+--------------------------------------------------------------------+ -| Emptyset | ``(as emptyset (Set Int)`` | ``Term t = solver.mkEmptySet(s);`` | -+----------------------+----------------------------------------------+--------------------------------------------------------------------+ -| Singleton Set | ``(singleton 1)`` | ``Term t = solver.mkTerm(Kind::SINGLETON, solver.mkInteger(1));`` | -+----------------------+----------------------------------------------+--------------------------------------------------------------------+ -| Cardinality | ``(card X)`` | ``Term t = solver.mkTerm(Kind::CARD, X);`` | -+----------------------+----------------------------------------------+--------------------------------------------------------------------+ -| Insert / Finite Sets | ``(insert 1 2 3 (singleton 4))`` | ``Term one = solver.mkInteger(1);`` | -| | | | -| | | ``Term two = solver.mkInteger(2);`` | -| | | | -| | | ``Term three = solver.mkInteger(3);`` | -| | | | -| | | ``Term sgl = solver.mkTerm(Kind::SINGLETON, solver.mkInteger(4));``| -| | | | -| | | ``Term t = solver.mkTerm(Kind::INSERT, {one, two, three, sgl});`` | -+----------------------+----------------------------------------------+--------------------------------------------------------------------+ -| Complement | ``(complement X)`` | ``Term t = solver.mkTerm(Kind::COMPLEMENT, X);`` | -+----------------------+----------------------------------------------+--------------------------------------------------------------------+ -| Universe Set | ``(as univset (Set Int))`` | ``Term t = solver.mkUniverseSet(s);`` | -+----------------------+----------------------------------------------+--------------------------------------------------------------------+ ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| | SMTLIB language | C++ API | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Logic String | append `FS` for finite sets | append `FS` for finite sets | +| | | | +| | ``(set-logic QF_UFLIAFS)`` | ``solver.setLogic("QF_UFLIAFS");`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Sort | ``(Set )`` | ``solver.mkSetSort(cvc5::api::Sort elementSort);`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Constants | ``(declare-const X (Set Int)`` | ``Sort s = solver.mkSetSort(solver.getIntegerSort());`` | +| | | | +| | | ``Term X = solver.mkConst(s, "X");`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Union | ``(set.union X Y)`` | ``Term Y = solver.mkConst(s, "Y");`` | +| | | | +| | | ``Term t = solver.mkTerm(Kind::SET_UNION, X, Y);`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Intersection | ``(set.minus X Y)`` | ``Term t = solver.mkTerm(Kind::SET_MINUS, X, Y);`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Membership | ``(set.member x X)`` | ``Term x = solver.mkConst(solver.getIntegerSort(), "x");`` | +| | | | +| | | ``Term t = solver.mkTerm(Kind::SET_MEMBER, x, X);`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Subset | ``(set.subset X Y)`` | ``Term t = solver.mkTerm(Kind::SET_SUBSET, X, Y);`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Emptyset | ``(as set.empty (Set Int)`` | ``Term t = solver.mkEmptySet(s);`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Singleton Set | ``(set.singleton 1)`` | ``Term t = solver.mkTerm(Kind::SET_SINGLETON, solver.mkInteger(1));`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Cardinality | ``(set.card X)`` | ``Term t = solver.mkTerm(Kind::SET_CARD, X);`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Insert / Finite Sets | ``(set.insert 1 2 3 (set.singleton 4))`` | ``Term one = solver.mkInteger(1);`` | +| | | | +| | | ``Term two = solver.mkInteger(2);`` | +| | | | +| | | ``Term three = solver.mkInteger(3);`` | +| | | | +| | | ``Term sgl = solver.mkTerm(Kind::SET_SINGLETON, solver.mkInteger(4));`` | +| | | | +| | | ``Term t = solver.mkTerm(Kind::SET_INSERT, {one, two, three, sgl});`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Complement | ``(set.complement X)`` | ``Term t = solver.mkTerm(Kind::SET_COMPLEMENT, X);`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Universe Set | ``(as set.universe (Set Int))`` | ``Term t = solver.mkUniverseSet(s);`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ Semantics ^^^^^^^^^ -The semantics of most of the above operators (e.g., set union, intersection, -difference) are straightforward. +The semantics of most of the above operators (e.g., ``set.union``, +``set.intersection``, difference) are straightforward. The semantics for the universe set and complement are more subtle and explained in the following. -The universe set ``(as univset (Set T))`` is *not* interpreted as the set +The universe set ``(as set.universe (Set T))`` is *not* interpreted as the set containing all elements of sort ``T``. Instead it may be interpreted as any set such that all sets of sort ``(Set T)`` are interpreted as subsets of it. @@ -96,16 +96,16 @@ For example: (declare-fun z () (Set Int)) (assert (member 0 x)) (assert (member 1 y)) - (assert (= z (as univset (Set Int)))) + (assert (= z (as set.universe (Set Int)))) (check-sat) Here, a possible model is: .. code:: smtlib - (define-fun x () (singleton 0)) - (define-fun y () (singleton 1)) - (define-fun z () (union (singleton 1) (singleton 0))) + (define-fun x () (set.singleton 0)) + (define-fun y () (set.singleton 1)) + (define-fun z () (set.union (set.singleton 1) (set.singleton 0))) Notice that the universe set in this example is interpreted the same as ``z``, and is such that all sets in this example (``x``, ``y``, and ``z``) are subsets @@ -115,7 +115,7 @@ The set complement operator for ``(Set T)`` is interpreted relative to the interpretation of the universe set for ``(Set T)``, and not relative to the set of all elements of sort ``T``. That is, for all sets ``X`` of sort ``(Set T)``, the complement operator is -such that ``(= (complement X) (setminus (as univset (Set T)) X))`` +such that ``(= (set.complement X) (set.minus (as set.universe (Set T)) X))`` holds in all models. The motivation for these semantics is to ensure that the universe set for sort @@ -134,7 +134,7 @@ Above, notice that we were able to find a model for the universe set of sort (set-logic ALL) (declare-fun x () (Set Int)) - (assert (forall ((z Int) (member (* 2 z) x))) + (assert (forall ((z Int) (set.member (* 2 z) x))) (check-sat) The reason for that is that making this formula (and similar ones) `unsat` is @@ -189,11 +189,11 @@ More details can be found in :cite:`MengRTB17`. | | | | | | | ``Term X = solver.mkConst(s, "X");`` | +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ -| Transpose | ``(transpose X)`` | ``Term t = solver.mkTerm(Kind::TRANSPOSE, X);`` | +| Transpose | ``(rel.transpose X)`` | ``Term t = solver.mkTerm(Kind::RELATION_TRANSPOSE, X);`` | +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ -| Transitive Closure | ``(tclosure X)`` | ``Term t = solver.mkTerm(Kind::TCLOSURE, X);`` | +| Transitive Closure | ``(rel.tclosure X)`` | ``Term t = solver.mkTerm(Kind::RELATION_TCLOSURE, X);`` | +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ -| Join | ``(join X Y)`` | ``Term t = solver.mkTerm(Kind::JOIN, X, Y);`` | +| Join | ``(rel.join X Y)`` | ``Term t = solver.mkTerm(Kind::RELATION_JOIN, X, Y);`` | +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ -| Product | ``(product X Y)`` | ``Term t = solver.mkTerm(Kind::PRODUCT, X, Y);`` | +| Product | ``(rel.product X Y)`` | ``Term t = solver.mkTerm(Kind::RELATION_PRODUCT, X, Y);`` | +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ diff --git a/examples/api/smtlib/relations.smt2 b/examples/api/smtlib/relations.smt2 index b663b7f17..c8ece3aa7 100644 --- a/examples/api/smtlib/relations.smt2 +++ b/examples/api/smtlib/relations.smt2 @@ -12,30 +12,30 @@ (assert (= r1 - (insert + (set.insert (tuple "a" 1) (tuple "b" 2) (tuple "c" 3) - (singleton (tuple "d" 4))))) + (set.singleton (tuple "d" 4))))) (assert (= r2 - (insert + (set.insert (tuple 1 "1") (tuple 2 "2") (tuple 3 "3") - (singleton (tuple 17 "17"))))) -(assert (= r (join r1 r2))) -(assert (= s (transpose r))) -(assert (= t (product r1 r2))) + (set.singleton (tuple 17 "17"))))) +(assert (= r (rel.join r1 r2))) +(assert (= s (rel.transpose r))) +(assert (= t (rel.product r1 r2))) (assert (= lt1 - (insert + (set.insert (tuple 1 2) (tuple 2 3) (tuple 3 4) - (singleton (tuple 4 5))))) -(assert (= lt2 (tclosure lt1))) -(assert (= i (card t))) + (set.singleton (tuple 4 5))))) +(assert (= lt2 (rel.tclosure lt1))) +(assert (= i (set.card t))) (check-sat) diff --git a/examples/api/smtlib/sets.smt2 b/examples/api/smtlib/sets.smt2 index 2e4b76b46..f8b30ae47 100644 --- a/examples/api/smtlib/sets.smt2 +++ b/examples/api/smtlib/sets.smt2 @@ -10,28 +10,28 @@ (check-sat-assuming ( (distinct - (intersection (union A B) C) - (union (intersection A C) (intersection B C))) + (set.intersection (set.union A B) C) + (set.union (set.intersection A C) (set.intersection B C))) ) ) ; Verify emptset is a subset of any set (check-sat-assuming ( - (not (subset (as emptyset (Set Int)) A)) + (not (set.subset (as set.empty (Set Int)) A)) ) ) ; Find an element in {1, 2} intersection {2, 3}, if there is one. (check-sat-assuming ( - (member + (set.member x - (intersection - (union (singleton 1) (singleton 2)) - (union (singleton 2) (singleton 3)))) + (set.intersection + (set.union (set.singleton 1) (set.singleton 2)) + (set.union (set.singleton 2) (set.singleton 3)))) ) ) (echo "A member: ") -(get-value (x)) \ No newline at end of file +(get-value (x))