Sets

2017-12-10T02:03:30Z

Arjunvish: /* Relations */

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:
* [https://github.com/CVC4/CVC4/blob/1.4/test/regress/regress0/sets/cvc-sample.cvc CVC language example]
* [https://github.com/CVC4/CVC4/blob/1.4/test/regress/regress0/sets/sets-sample.smt2 SMT language example]
* API example: [[Tutorials#Sets|tutorial]], [https://github.com/CVC4/CVC4/blob/1.4/examples/api/sets.cpp source code]

For reference, below is a short summary of the sorts, constants, functions and predicates.

{| 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>)
|
|-
|
| <code>'''UNIVERSE''' :: SET OF INT</code>
| <code>(as '''univset''' (Set Int))</code>
| <code>em.mkNullaryOperator(em.mkSetType(em.integerType()),'''kind::UNIVERSE_SET''');</code>
|}

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

=Relations=

{| class="wikitable" cellpadding="5" border="0" style="border-collapse:collapse"
|-
!
! CVC language
! SMTLIB language
! C++ API
|-
| Logic string
| Not needed
| --
| --
|-
|
|
| --
| --
|-
| Sort
| SET OF [ElementSort_1, ..., ElementSort_n]
| (Set (Tuple ElementSort_1, ..., ElementSort_n))
| --
|-
|
| <code>X: '''SET OF [INT, INT]''';</code>
| <code> (declare-fun X () (Set (Tuple Int Int))) </code>
| <code> -- </code>
|-
| Transpose
| <code>'''<nowiki>TRANSPOSE</nowiki>'''(X) </code>
| <code> ('''transpose''' X) </code>
| <code> -- </code>
|-
| Transitive Closure
| <code>'''<nowiki>TCLOSURE</nowiki>'''(X) </code>
| <code> ('''tclosure''' X) </code>
| <code> -- </code>
|-
| Join
| <code> X '''<nowiki>JOIN</nowiki>''' Y </code>
| <code> ('''join''' X Y) </code>
| <code> -- </code>
|-
| Product
| <code> X '''<nowiki>PRODUCT</nowiki>''' Y </code>
| <code> ('''product''' X Y) </code>
| <code> -- </code>
|-

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

CVC4 - User contributions [en]

Sets