Difference between revisions of "Sets"

From CVC4

Revision as of 11:46, 1 May 2018

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.

	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))`	`em.mkTupleType( em.integerType(), em.integerType() );`
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_CONSTRUCTOR, 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);`

@@ 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