Difference between revisions of "Sets"

From CVC4
Jump to: navigation, search
Line 111: Line 111:
  
 
=Relations=
 
=Relations=
 +
 +
{| class="wikitable" cellpadding="5" border="0" style="border-collapse:collapse"
 +
|-
 +
!
 +
! CVC language
 +
! SMTLIB language
 +
! C++ API
 +
|-
 +
| Logic string
 +
| Not needed
 +
| append "FS" for finite sets
 +
| append "FS" for finite sets
 +
|-
 +
|
 +
|
 +
| <code>(set-logic QF_UFLIA'''FS''')</code>
 +
| <code>smt.setLogic("QF_UFLIA'''FS'''");</code>
 +
|-
 +
| Sort
 +
| SET OF <Element Sort>
 +
| (Set <Element Sort>)
 +
| CVC4::ExprManager::mkSetType(CVC4::Type elementType)
 +
|-
 +
|
 +
| <code>X: '''SET OF INT''';</code>
 +
| <code>(declare-fun X () '''(Set Int)''')</code>
 +
| <code>em.'''mkSetType'''( em.integerType() );</code>
 +
|-
 +
| Union
 +
| <code>X '''<nowiki>|</nowiki>''' Y</code>
 +
| <code>('''union''' X Y)</code>
 +
| <code>em.mkExpr('''kind::UNION''', X, Y);</code>
 +
|-
 +
| Intersection
 +
| <code>X '''<nowiki>&</nowiki>''' Y</code>
 +
| <code>('''intersection''' X Y)</code>
 +
| <code>em.mkExpr('''kind::INTERSECTION''', X, Y);</code>
 +
|-
 +
| Set subtraction
 +
| <code>X '''<nowiki>–</nowiki>''' Y</code>
 +
| <code>('''setminus''' X Y)</code>
 +
| <code>em.mkExpr('''kind::SETMINUS''', X, Y);</code>
 +
|-
 +
| Membership
 +
| <code>x '''<nowiki>IS_IN</nowiki>''' X</code>
 +
| <code>('''member''' x X)</code>
 +
| <code>em.mkExpr('''kind::MEMBER''', x, X);</code>
 +
|-
 +
| Subset
 +
| <code>X '''<nowiki><=</nowiki>''' Y</code>
 +
| <code>('''subset''' X Y)</code>
 +
| <code>em.mkExpr('''kind::SUBSET''', X, Y);</code>
 +
|-
 +
| Empty set
 +
| {} :: <Type Ascription>
 +
| (as emptyset <Type Ascription>)
 +
| CVC4::EmptySet(CVC4::SetType setType)
 +
|-
 +
|
 +
| <code>'''{}''' :: SET OF INT</code>
 +
| <code>(as '''emptyset''' (Set Int))</code>
 +
| <code>em.mkConst('''EmptySet'''(em.mkSetType(em.integerType())));</code>
 +
|-
 +
| Singleton set
 +
| <code>'''{1}'''</code>
 +
| <code>('''singleton''' 1)</code>
 +
| <code>em.mkExpr('''kind::SINGLETON''', oneExpr);</code>
 +
|-
 +
| Cardinality
 +
| <code>'''<nowiki>CARD</nowiki>'''( X )</code>
 +
| <code>('''card''' X)</code>
 +
| <code>em.mkExpr('''kind::CARD''', X);</code>
 +
|-
 +
| Insert/finite sets
 +
| <code>'''{1, 2, 3, 4}'''</code>
 +
| <code>('''insert''' 1 2 3 (singleton 4))</code>
 +
| <code>em.mkExpr('''kind::INSERT''', c1, c2, c3, sgl4);</code>
 +
|-
 +
| Complement
 +
| <code>'''<nowiki>~</nowiki>''' X</code>
 +
| <code>('''complement''' X)</code>
 +
| <code>em.mkExpr('''kind::COMPLEMENT''', X);</code>
 +
|-
 +
| Universe set
 +
| UNIVERSE :: <Type Ascription>
 +
| (as univset <Type Ascription>)
 +
| mkUniqueVar(CVC4::SetType setType,kind::UNIVERSE_SET)
 +
|-
  
  
 
(Coming soon)
 
(Coming soon)

Revision as of 14:53, 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:


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

(Coming soon)
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)
Retrieved from "http://cvc4.stanford.edu/w/index.php?title=Sets&oldid=5539"