Difference between revisions of "Sets"

From CVC4

Revision as of 07:53, 6 March 2017

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);`
Compliment	`NOT X`	`(compliment X)`	`em.mkExpr(kind::COMPLIMENT, X);`
Universe set	UNIVERSE :: <Type Ascription>	(as univset <Type Ascription>)	mkUniqueVar(kind::UNIVERSE_SET,CVC4::SetType setType)
	`UNIVERSE :: SET OF INT`	`(as univset (Set Int))`	`em.mkUniqueVar(kind::UNIVERSE_SET,em.mkSetType(em.integerType())));`

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

@@ Line 83: / Line 83: @@
 | <code>('''insert''' 1 2 3 (singleton 4))</code>
 | <code>em.mkExpr('''kind::INSERT''', c1, c2, c3, sgl4);</code>
+|-
+| Compliment
+| <code>'''<nowiki>NOT</nowiki>''' X</code>
+| <code>('''compliment''' X)</code>
+| <code>em.mkExpr('''kind::COMPLIMENT''', X);</code>
+|-
+| Universe set
+| UNIVERSE :: <Type Ascription>
+| (as univset <Type Ascription>)
+| mkUniqueVar(kind::UNIVERSE_SET,CVC4::SetType setType)
+|-
+|
+| <code>'''UNIVERSE''' :: SET OF INT</code>
+| <code>(as '''univset''' (Set Int))</code>
+| <code>em.mkUniqueVar(kind::UNIVERSE_SET,em.mkSetType(em.integerType())));</code>
 |}
 Operator precedence for CVC language: