Difference between revisions of "Sets"
From CVC4
Baoluo-meng (Talk | contribs) |
Baoluo-meng (Talk | contribs) |
||
| Line 135: | Line 135: | ||
|- | |- | ||
| | | | ||
| − | | <code>X: '''SET OF INT''';</code> | + | | <code>X: '''SET OF [INT, INT]''';</code> |
| − | | <code> | + | | <code> -- </code> |
| − | | <code> | + | | <code> -- </code> |
|- | |- | ||
| − | | | + | | TRANSPOSE |
| <code>X '''<nowiki>|</nowiki>''' Y</code> | | <code>X '''<nowiki>|</nowiki>''' Y</code> | ||
| <code>('''union''' X Y)</code> | | <code>('''union''' X Y)</code> | ||
| Line 174: | Line 174: | ||
| <code>em.mkConst('''EmptySet'''(em.mkSetType(em.integerType())));</code> | | <code>em.mkConst('''EmptySet'''(em.mkSetType(em.integerType())));</code> | ||
|- | |- | ||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
Revision as of 13:55, 21 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:
- 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>) | mkUniqueVar(CVC4::SetType setType,kind::UNIVERSE_SET) |
UNIVERSE :: SET OF INT
|
(as univset (Set Int))
|
em.mkUniqueVar(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
| 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] | -- | -- |
X: SET OF [INT, INT];
|
--
|
--
| |
| TRANSPOSE | 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())));
|
