Revision as of 13:51, 12 April 2017 (view source) Ajreynol (Talk | contribs) ← Older edit		Revision as of 18:03, 9 December 2017 (view source) Arjunvish (Talk | contribs) (→‎Relations) Newer edit →
Line 131:		Line 131:
	| Sort		| Sort
	| SET OF [ElementSort_1, ..., ElementSort_n]		| SET OF [ElementSort_1, ..., ElementSort_n]
−	| --	+	| (Set (Tuple ElementSort_1, ..., ElementSort_n))
	| --		| --
	|-		|-
	|		|
	| <code>X: '''SET OF [INT, INT]''';</code>		| <code>X: '''SET OF [INT, INT]''';</code>
−	| <code> -- </code>	+	| <code> (declare-fun X () (Set (Tuple Int Int))) </code>
	| <code> -- </code>		| <code> -- </code>
	|-		|-
	| Transpose		| Transpose
	| <code>'''<nowiki>TRANSPOSE</nowiki>'''(X) </code>		| <code>'''<nowiki>TRANSPOSE</nowiki>'''(X) </code>
−	| <code> -- </code>	+	| <code> ('''transpose''' X) </code>
	| <code> -- </code>		| <code> -- </code>
	|-		|-
	| Transitive Closure		| Transitive Closure
	| <code>'''<nowiki>TCLOSURE</nowiki>'''(X) </code>		| <code>'''<nowiki>TCLOSURE</nowiki>'''(X) </code>
−	| <code> -- </code>	+	| <code> ('''tclosure''' X) </code>
	| <code> -- </code>		| <code> -- </code>
	|-		|-
	| Join		| Join
	| <code> X '''<nowiki>JOIN</nowiki>''' Y </code>		| <code> X '''<nowiki>JOIN</nowiki>''' Y </code>
−	| <code> -- </code>	+	| <code> ('''join''' X Y) </code>
	| <code> -- </code>		| <code> -- </code>
	|-		|-
	| Product		| Product
	| <code> X '''<nowiki>PRODUCT</nowiki>''' Y </code>		| <code> X '''<nowiki>PRODUCT</nowiki>''' Y </code>
−	| <code> -- </code>	+	| <code> ('''product''' X Y) </code>
	| <code> -- </code>		| <code> -- </code>
	|-		|-
	Note: Currently, we only support encoding relational constraints in CVC4 native language. Support for SMT-LIB language is coming soon.		Note: Currently, we only support encoding relational constraints in CVC4 native language. Support for SMT-LIB language is coming soon.

---

Revision as of 18:03, 9 December 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:

• CVC language example
• SMT language example
• API example: tutorial, source code

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.

Relations

Note: Currently, we only support encoding relational constraints in CVC4 native language. Support for SMT-LIB language is coming soon.

	CVC language	SMTLIB language	C++ API
Logic string	Not needed	--	--
		--	--
Sort	SET OF [ElementSort_1, ..., ElementSort_n]	(Set (Tuple ElementSort_1, ..., ElementSort_n))	--
	X: SET OF [INT, INT];	(declare-fun X () (Set (Tuple Int Int)))	--
Transpose	TRANSPOSE(X)	(transpose X)	--
Transitive Closure	TCLOSURE(X)	(tclosure X)	--
Join	X JOIN Y	(join X Y)	--
Product	X PRODUCT Y	(product X Y)	--