Difference between revisions of "Sets"

From CVC4
Jump to: navigation, search
(→‎Relations)
 
(20 intermediate revisions by 2 users not shown)
Line 1: Line 1:
 +
=Finite Sets=
 +
 
As of July 2014 (CVC4 v1.4), we include support for theory of finite sets. The simplest way to get a sense of the syntax is to look at an example:
 
As of July 2014 (CVC4 v1.4), we include support for theory of finite sets. The simplest way to get a sense of the syntax is to look at an example:
 
* [https://github.com/CVC4/CVC4/blob/1.4/test/regress/regress0/sets/cvc-sample.cvc CVC language example]
 
* [https://github.com/CVC4/CVC4/blob/1.4/test/regress/regress0/sets/cvc-sample.cvc CVC language example]
Line 109: Line 111:
 
<code><nowiki>=</nowiki></code>. For example, <code>A - B | A & C <= D</code> is read as <code>( A - ( B | (A & C) ) ) <= D</code>.
 
<code><nowiki>=</nowiki></code>. For example, <code>A - B | A & C <= D</code> is read as <code>( A - ( B | (A & C) ) ) <= D</code>.
  
 +
==Semantics==
  
−
=Relations=
+
The semantics of most of the above operators (e.g. set union, intersection, difference) are straightforward. The semantics for the universe set and complement are more subtle and is explained in the following.
 +
 
 +
The universe set (as univset (Set T)) is *not* interpreted as the set containing all elements of type T. Instead it may be interpreted as any set such that all sets of type (Set T) are interpreted as subsets of it. In other words, it is the union of the interpretation of all (finite) sets in our input. For example:
 +
  (declare-fun x () (Set Int))
 +
  (declare-fun y () (Set Int))
 +
  (declare-fun z () (Set Int))
 +
  (assert (member 0 x))
 +
  (assert (member 1 y))
 +
  (assert (= z (as univset (Set Int))))
 +
  (check-sat)
 +
Here, a possible model is:
 +
  (define-fun x () (singleton 0))
 +
  (define-fun y () (singleton 1))
 +
  (define-fun z () (union (singleton 1) (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 of it.
 +
 
 +
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 type T.  That is, for all sets X of type (Set T), the complement operator is such that:
 +
  (complement X) = (setminus (as univset (Set T)) X)
 +
holds in all models.
 +
 
 +
The motivation for these semantics is to ensure that the universe set for type T and applications of set complement can always be interpreted as a finite set in (quantifier-free) inputs, even if the cardinality of T is infinite. Above, notice that we were able to find a model for the universe set of type (Set Int) that contained two elements only.
 +
 
 +
=Finite Relations=
 +
 
 +
* [https://github.com/CVC4/CVC4/blob/master/test/regress/regress0/rels/rel_join_1_1.cvc CVC language example]
 +
* [https://github.com/CVC4/CVC4/blob/master/test/regress/regress0/rels/relations-ops.smt2 SMT language example]
  
 
{| class="wikitable" cellpadding="5" border="0" style="border-collapse:collapse"
 
{| class="wikitable" cellpadding="5" border="0" style="border-collapse:collapse"
Line 121: Line 149:
 
| Logic string
 
| Logic string
 
| Not needed
 
| Not needed
−
| --
+
| <code>(set-logic QF_'''ALL''')</code>
−
| --
+
| <code>smt.setLogic("QF_'''ALL'''");</code>
 
|-
 
|-
−
|
+
| Tuple Sort
−
|
+
| [<Sort_1>, ..., <Sort_n>]
−
| --
+
| (Tuple <Sort_1>, ..., <Sort_n>)
−
| --
+
| CVC4::ExprManager::mkTupleType(std::vector<CVC4::Type>& types)
 
|-
 
|-
−
| Sort
+
|  
−
| SET OF [ElementSort_1, ..., ElementSort_n]
+
| <code>t: '''[INT, INT]''';</code>
−
| (Set (Tuple ElementSort_1, ..., ElementSort_n))
+
| <code> (declare-fun t () '''(Tuple Int Int)''') </code>
−
| --
+
| <code>std::vector<Type> types;</code><br>
 +
<code>types.push_back(em.mkIntegerType());</code></br>
 +
<code>types.push_back(em.mkIntegerType());</code></br>
 +
<code>em.'''mkTupleType'''( types );</code>
 +
|-
 +
| Tuple constructor
 +
| <code>'''(t1, ..., tn)'''</code>
 +
| <code>('''mkTuple''' t1, ..., tn)</code>
 +
| <code>DatatypeType tt = em.mkTupleType(types);</code>
 +
<code>const Datatype& dt = tt.getDatatype();</code><br>
 +
<code>Expr c = dt[0].getConstructor();</code><br>
 +
<code>em.mkExpr('''kind::APPLY_CONSTRUCTOR''', c, t1, ..., tn);</code>
 +
|-
 +
| Tuple selector
 +
| <code>'''t.i'''</code>
 +
| <code>('''(_ tupSel i)''' t)</code>
 +
| <code>DatatypeType tt = em.mkTupleType(types);</code><br>
 +
<code>const Datatype& dt = tt.getDatatype();</code><br>
 +
<code>Expr s = dt[0][i].getSelector();</code><br>
 +
<code>em.mkExpr('''kind::APPLY_SELECTOR''', s, t);</code>
 +
|-
 +
| Relation Sort
 +
| SET OF [<Sort_1>, ..., <Sort_n>]
 +
| (Set (Tuple <Sort_1>, ..., <Sort_n>))
 +
| CVC4::ExprManager::mkSetType(CVC4::Type elementType)
 
|-
 
|-
 
|  
 
|  
 
| <code>X: '''SET OF [INT, INT]''';</code>
 
| <code>X: '''SET OF [INT, INT]''';</code>
−
| <code> (declare-fun X () (Set (Tuple Int Int))) </code>
+
| <code> (declare-fun X () '''(Set (Tuple Int Int))''') </code>
−
| <code> -- </code>
+
| <code>em.'''mkSetType'''( em.'''mkTupleType'''( em.integerType(), em.integerType() ) );</code>
 
|-
 
|-
 
| Transpose
 
| Transpose
 
| <code>'''<nowiki>TRANSPOSE</nowiki>'''(X) </code>
 
| <code>'''<nowiki>TRANSPOSE</nowiki>'''(X) </code>
 
| <code> ('''transpose''' X) </code>
 
| <code> ('''transpose''' X) </code>
−
| <code> -- </code>
+
| <code> em.mkExpr('''kind::TRANSPOSE''', X); </code>
 
|-
 
|-
 
| Transitive Closure
 
| Transitive Closure
 
| <code>'''<nowiki>TCLOSURE</nowiki>'''(X) </code>
 
| <code>'''<nowiki>TCLOSURE</nowiki>'''(X) </code>
 
| <code> ('''tclosure''' X) </code>
 
| <code> ('''tclosure''' X) </code>
−
| <code> -- </code>
+
| <code> em.mkExpr('''kind::TCLOSURE''', X);  </code>
 
|-
 
|-
 
| Join
 
| Join
 
| <code> X '''<nowiki>JOIN</nowiki>''' Y </code>
 
| <code> X '''<nowiki>JOIN</nowiki>''' Y </code>
 
| <code> ('''join''' X Y) </code>
 
| <code> ('''join''' X Y) </code>
−
| <code> -- </code>
+
| <code> em.mkExpr('''kind::JOIN''', X); </code>
 
|-
 
|-
 
| Product
 
| Product
 
| <code> X '''<nowiki>PRODUCT</nowiki>''' Y </code>
 
| <code> X '''<nowiki>PRODUCT</nowiki>''' Y </code>
 
| <code> ('''product''' X Y) </code>
 
| <code> ('''product''' X Y) </code>
−
| <code> -- </code>
+
| <code> em.mkExpr('''kind::PRODUCT''', X); </code>
 
|-
 
|-
  
−
Note: Currently, we only support encoding relational constraints in CVC4 native language. Support for SMT-LIB language is coming soon.
+
For more details, see our CADE 2017 paper on an extension of the decision procedure for sets, as described in [http://homepage.cs.uiowa.edu/~tinelli/papers/MenEtAl-CADE-17.pdf].

Latest revision as of 06:47, 13 August 2019

Finite Sets

As of July 2014 (CVC4 v1.4), we include support for theory of finite sets. The simplest way to get a sense of the syntax is to look at an example:


For reference, below is a short summary of the sorts, constants, functions and predicates.

CVC language SMTLIB language C++ API
Logic string Not needed append "FS" for finite sets append "FS" for finite sets
(set-logic QF_UFLIAFS) smt.setLogic("QF_UFLIAFS");
Sort SET OF <Element Sort> (Set <Element Sort>) CVC4::ExprManager::mkSetType(CVC4::Type elementType)
X: SET OF INT; (declare-fun X () (Set Int)) em.mkSetType( em.integerType() );
Union X | Y (union X Y) em.mkExpr(kind::UNION, X, Y);
Intersection X & Y (intersection X Y) em.mkExpr(kind::INTERSECTION, X, Y);
Set subtraction X – Y (setminus X Y) em.mkExpr(kind::SETMINUS, X, Y);
Membership x IS_IN X (member x X) em.mkExpr(kind::MEMBER, x, X);
Subset X <= Y (subset X Y) em.mkExpr(kind::SUBSET, X, Y);
Empty set {} :: <Type Ascription> (as emptyset <Type Ascription>) CVC4::EmptySet(CVC4::SetType setType)
{} :: SET OF INT (as emptyset (Set Int)) em.mkConst(EmptySet(em.mkSetType(em.integerType())));
Singleton set {1} (singleton 1) em.mkExpr(kind::SINGLETON, oneExpr);
Cardinality CARD( X ) (card X) em.mkExpr(kind::CARD, X);
Insert/finite sets {1, 2, 3, 4} (insert 1 2 3 (singleton 4)) em.mkExpr(kind::INSERT, c1, c2, c3, sgl4);
Complement ~ X (complement X) em.mkExpr(kind::COMPLEMENT, X);
Universe set UNIVERSE :: <Type Ascription> (as univset <Type Ascription>)
UNIVERSE :: SET OF INT (as univset (Set Int)) em.mkNullaryOperator(em.mkSetType(em.integerType()),kind::UNIVERSE_SET);


Operator precedence for CVC language: & | – IS_IN <= =. For example, A - B | A & C <= D is read as ( A - ( B | (A & C) ) ) <= D.

Semantics

The semantics of most of the above operators (e.g. set union, intersection, difference) are straightforward. The semantics for the universe set and complement are more subtle and is explained in the following.

The universe set (as univset (Set T)) is *not* interpreted as the set containing all elements of type T. Instead it may be interpreted as any set such that all sets of type (Set T) are interpreted as subsets of it. In other words, it is the union of the interpretation of all (finite) sets in our input. For example: 

 (declare-fun x () (Set Int))
 (declare-fun y () (Set Int))
 (declare-fun z () (Set Int))
 (assert (member 0 x))
 (assert (member 1 y))
 (assert (= z (as univset (Set Int))))
 (check-sat)

Here, a possible model is: 

 (define-fun x () (singleton 0))
 (define-fun y () (singleton 1))
 (define-fun z () (union (singleton 1) (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 of it.

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 type T. That is, for all sets X of type (Set T), the complement operator is such that: 

 (complement X) = (setminus (as univset (Set T)) X)

holds in all models.

The motivation for these semantics is to ensure that the universe set for type T and applications of set complement can always be interpreted as a finite set in (quantifier-free) inputs, even if the cardinality of T is infinite. Above, notice that we were able to find a model for the universe set of type (Set Int) that contained two elements only.

Finite Relations

For more details, see our CADE 2017 paper on an extension of the decision procedure for sets, as described in [1].
CVC language SMTLIB language C++ API
Logic string Not needed (set-logic QF_ALL) smt.setLogic("QF_ALL");
Tuple Sort [<Sort_1>, ..., <Sort_n>] (Tuple <Sort_1>, ..., <Sort_n>) CVC4::ExprManager::mkTupleType(std::vector<CVC4::Type>& types)
t: [INT, INT]; (declare-fun t () (Tuple Int Int)) std::vector<Type> types;

types.push_back(em.mkIntegerType());</br> types.push_back(em.mkIntegerType());</br> em.mkTupleType( types );

Tuple constructor (t1, ..., tn) (mkTuple t1, ..., tn) DatatypeType tt = em.mkTupleType(types);

const Datatype& dt = tt.getDatatype();
Expr c = dt[0].getConstructor();
em.mkExpr(kind::APPLY_CONSTRUCTOR, c, t1, ..., tn);

Tuple selector t.i ((_ tupSel i) t) DatatypeType tt = em.mkTupleType(types);

const Datatype& dt = tt.getDatatype();
Expr s = dt[0][i].getSelector();
em.mkExpr(kind::APPLY_SELECTOR, s, t);

Relation Sort SET OF [<Sort_1>, ..., <Sort_n>] (Set (Tuple <Sort_1>, ..., <Sort_n>)) CVC4::ExprManager::mkSetType(CVC4::Type elementType)
X: SET OF [INT, INT]; (declare-fun X () (Set (Tuple Int Int))) em.mkSetType( em.mkTupleType( em.integerType(), em.integerType() ) );
Transpose TRANSPOSE(X) (transpose X) em.mkExpr(kind::TRANSPOSE, X);
Transitive Closure TCLOSURE(X) (tclosure X) em.mkExpr(kind::TCLOSURE, X);
Join X JOIN Y (join X Y) em.mkExpr(kind::JOIN, X);
Product X PRODUCT Y (product X Y) em.mkExpr(kind::PRODUCT, X);
Retrieved from "http://cvc4.cs.stanford.edu/w/index.php?title=Sets&oldid=5746"