Sets - Revision history

Ajreynol at 14:47, 13 August 2019

2019-08-13T14:47:25Z

Ajreynol at 14:38, 13 August 2019

2019-08-13T14:38:42Z

Ajreynol at 19:36, 12 March 2019

2019-03-12T19:36:40Z

Ajreynol at 19:34, 12 March 2019

2019-03-12T19:34:59Z

Ajreynol at 19:34, 12 March 2019

2019-03-12T19:34:06Z

Ajreynol at 19:28, 12 March 2019

2019-03-12T19:28:32Z

Ajreynol: /* Finite Relations */

2018-05-08T13:56:15Z

‎Finite Relations

Ajreynol: /* Finite Relations */

2018-05-01T19:46:34Z

‎Finite Relations

Ajreynol: /* Finite Relations */

2018-05-01T19:45:15Z

‎Finite Relations

Ajreynol: /* Finite Relations */

2018-04-25T17:52:10Z

‎Finite Relations

← Older revision		Revision as of 14:47, 13 August 2019
Line 211:		Line 211:
	\| <code> em.mkExpr('''kind::PRODUCT''', X); </code>		\| <code> em.mkExpr('''kind::PRODUCT''', X); </code>
	\|-		\|-
		+
		+	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].

← Older revision		Revision as of 14:38, 13 August 2019
Line 136:		Line 136:

	=Finite Relations=		=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 113: / Line 113: @@
 ==Semantics==
-Most of the above operators (e.g. set union, intersection, difference) have semantics that are straightforward. The semantics for the universe set is more subtle and is explained in the following.
+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 is defined as any set such that all sets of type (Set T) are interpreted as subsets of it. For example:
+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))

@@ Line 126: / Line 126: @@
    (define-fun x () (singleton 0))
    (define-fun y () (singleton 1))
-   (define-fun z () (uniont (singleton 1) (singleton 0)))
+   (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.
@@ Line 133: / Line 133: @@
 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.
+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=

@@ Line 115: / Line 115: @@
 Most of the above operators (e.g. set union, intersection, difference) have semantics that are straightforward. The semantics for the universe set is more subtle and is explained in the following.
-The universe set (as univset (Set T)) is not
+The universe set (as univset (Set T)) is *not* interpreted as the set containing all elements of type T. Instead it is defined as any set such that all sets of type (Set T) are interpreted as subsets of it. For example:
-For all sets X of type (Set T), the complement operator is such that:
+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 and applications of set complement can always be interpreted as a finite set in (quantifier-free) inputs.
+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.
 =Finite Relations=

← Older revision		Revision as of 19:28, 12 March 2019
Line 111:		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==
		+
		+	Most of the above operators (e.g. set union, intersection, difference) have semantics that are straightforward. The semantics for the universe set is more subtle and is explained in the following.
		+
		+	The universe set (as univset (Set T)) is not
		+
		+	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 and applications of set complement can always be interpreted as a finite set in (quantifier-free) inputs.

	=Finite Relations=		=Finite Relations=

@@ Line 134: / Line 134: @@
 | <code>t: '''[INT, INT]''';</code>
 | <code> (declare-fun t () '''(Tuple Int Int)''') </code>
-| <code>em.'''mkTupleType'''( em.integerType(), em.integerType() );</code>
+| <code>std::vector<Type> types;</code><br>
 |-
 | Tuple constructor
@@ Line 147: / Line 150: @@
 | <code>'''t.i'''</code>
 | <code>('''(_ tupSel i)''' t)</code>
-| <code>DatatypeType tt = em.mkTupleType(types);</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_CONSTRUCTOR''', s, t);</code>
+<code>em.mkExpr('''kind::APPLY_SELECTOR''', s, t);</code>
 |-
 | Relation Sort

@@ Line 132: / Line 132: @@
 |-
+|
-| <code>X: '''[INT, INT]''';</code>
+| <code>t: '''[INT, INT]''';</code>
-| <code> (declare-fun X () '''(Tuple Int Int)''') </code>
+| <code> (declare-fun t () '''(Tuple Int Int)''') </code>
 | <code>em.'''mkTupleType'''( em.integerType(), em.integerType() );</code>
 |-
 | Tuple constructor
-| <code>'''(X1, ..., Xn)'''</code>
+| <code>'''(t1, ..., tn)'''</code>
-| <code>('''mkTuple''' X1, ..., Xn)</code>
+| <code>('''mkTuple''' t1, ..., tn)</code>
-| <code>DatatypeType t = em.mkTupleType(types);</code>
+| <code>DatatypeType tt = em.mkTupleType(types);</code>
-<code>const Datatype& dt = t.getDatatype();</code><br>
+<code>const Datatype& dt = tt.getDatatype();</code><br>
 <code>Expr c = dt[0].getConstructor();</code><br>
-<code>em.mkExpr('''kind::APPLY_CONSTRUCTOR''', c, X1, ..., Xn);</code>
+<code>em.mkExpr('''kind::APPLY_CONSTRUCTOR''', c, t1, ..., tn);</code>
 |-
 | Tuple selector
-| <code>'''X.i'''</code>
+| <code>'''t.i'''</code>
-| <code>('''(_ tupSel i)''' X)</code>
+| <code>('''(_ tupSel i)''' t)</code>
-| <code>DatatypeType t = em.mkTupleType(types);</code>
+| <code>DatatypeType tt = em.mkTupleType(types);</code>
-<code>const Datatype& dt = t.getDatatype();</code><br>
+<code>const Datatype& dt = tt.getDatatype();</code><br>
 <code>Expr s = dt[0][i].getSelector();</code><br>
-<code>em.mkExpr('''kind::APPLY_CONSTRUCTOR''', s, X);</code>
+<code>em.mkExpr('''kind::APPLY_CONSTRUCTOR''', s, t);</code>
 |-
 | Relation Sort

@@ Line 134: / Line 134: @@
 | <code>X: '''[INT, INT]''';</code>
 | <code> (declare-fun X () '''(Tuple Int Int)''') </code>
-| <code>em.mkTupleType( em.integerType(), em.integerType() );</code>
+| <code>em.'''mkTupleType'''( em.integerType(), em.integerType() );</code>
 |-
 | Tuple constructor
@@ Line 152: / Line 152: @@
 | <code>X: '''SET OF [INT, INT]''';</code>
 | <code> (declare-fun X () '''(Set (Tuple Int Int))''') </code>
-| <code>em.mkSetType( em.mkTupleType( em.integerType(), em.integerType() ) );</code>
+| <code>em.'''mkSetType'''( em.'''mkTupleType'''( em.integerType(), em.integerType() ) );</code>
 |-
 | Transpose