Difference between revisions of "Sets"

From CVC4
Jump to: navigation, search
(→‎Finite Relations)
Line 111: Line 111:
 
<code><nowiki>=</nowiki></code>. For example, <code>A - B | A & C <= D</code> is read as <code>( A - ( B | (A & C) ) ) <= D</code>.
 
<code><nowiki>=</nowiki></code>. For example, <code>A - B | A & C <= D</code> is read as <code>( A - ( B | (A & C) ) ) <= D</code>.
  
 +
==Semantics==
 +
 +
Most of the above operators (e.g. set union, intersection, difference) have semantics that are straightforward. The semantics for the universe set is more subtle and is explained in the following.
 +
 +
The universe set (as univset (Set T)) is not
 +
 +
For all sets X of type (Set T), the complement operator is such that:
 +
  (complement X) = (setminus (as univset (Set T)) X)
 +
holds in all models.
 +
 +
The motivation for these semantics is to ensure that the universe set and applications of set complement can always be interpreted as a finite set in (quantifier-free) inputs.
  
 
=Finite Relations=
 
=Finite Relations=

Revision as of 12:28, 12 March 2019

Finite Sets

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>)
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.

Semantics

Most of the above operators (e.g. set union, intersection, difference) have semantics that are straightforward. The semantics for the universe set is more subtle and is explained in the following.

The universe set (as univset (Set T)) is not

For all sets X of type (Set T), the complement operator is such that: 

 (complement X) = (setminus (as univset (Set T)) X)

holds in all models.

The motivation for these semantics is to ensure that the universe set and applications of set complement can always be interpreted as a finite set in (quantifier-free) inputs.

Finite Relations

CVC language SMTLIB language C++ API
Logic string Not needed (set-logic QF_ALL) smt.setLogic("QF_ALL");
Tuple Sort [<Sort_1>, ..., <Sort_n>] (Tuple <Sort_1>, ..., <Sort_n>) CVC4::ExprManager::mkTupleType(std::vector<CVC4::Type>& types)
t: [INT, INT]; (declare-fun t () (Tuple Int Int)) std::vector<Type> types;

types.push_back(em.mkIntegerType());</br> types.push_back(em.mkIntegerType());</br> em.mkTupleType( types );

Tuple constructor (t1, ..., tn) (mkTuple t1, ..., tn) DatatypeType tt = em.mkTupleType(types);

const Datatype& dt = tt.getDatatype();
Expr c = dt[0].getConstructor();
em.mkExpr(kind::APPLY_CONSTRUCTOR, c, t1, ..., tn);

Tuple selector t.i ((_ tupSel i) t) DatatypeType tt = em.mkTupleType(types);

const Datatype& dt = tt.getDatatype();
Expr s = dt[0][i].getSelector();
em.mkExpr(kind::APPLY_SELECTOR, s, t);

Relation Sort SET OF [<Sort_1>, ..., <Sort_n>] (Set (Tuple <Sort_1>, ..., <Sort_n>)) CVC4::ExprManager::mkSetType(CVC4::Type elementType)
X: SET OF [INT, INT]; (declare-fun X () (Set (Tuple Int Int))) em.mkSetType( em.mkTupleType( em.integerType(), em.integerType() ) );
Transpose TRANSPOSE(X) (transpose X) em.mkExpr(kind::TRANSPOSE, X);
Transitive Closure TCLOSURE(X) (tclosure X) em.mkExpr(kind::TCLOSURE, X);
Join X JOIN Y (join X Y) em.mkExpr(kind::JOIN, X);
Product X PRODUCT Y (product X Y) em.mkExpr(kind::PRODUCT, X);
Retrieved from "http://cvc4.cs.stanford.edu/w/index.php?title=Sets&oldid=5741"