Sets

From CVC4
Jump to: navigation, search

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.


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