Theory Reference: Sets and Relations

Finite Sets

cvc5 supports the theory of finite sets using the following sorts, constants, functions and predicates. More details can be found in [ BBRT17 ] .

For the C++ API examples in the table below, we assume that we have created a cvc5::Solver solver object.

SMTLIB language

C++ API

Logic String

append FS for finite sets

(set-logic QF_UFLIAFS)

append FS for finite sets

solver.setLogic("QF_UFLIAFS");

Sort

(Set <Sort>)

solver.mkSetSort(cvc5::Sort elementSort);

Constants

(declare-const X (Set Int)

Sort s = solver.mkSetSort(solver.getIntegerSort());

Term X = solver.mkConst(s, "X");

Union

(set.union X Y)

Term Y = solver.mkConst(s, "Y");

Term t = solver.mkTerm(Kind::SET_UNION, {X, Y});

Intersection

(set.inter X Y)

Term t = solver.mkTerm(Kind::SET_INTER, {X, Y});

Minus

(set.minus X Y)

Term t = solver.mkTerm(Kind::SET_MINUS, {X, Y});

Membership

(set.member x X)

Term x = solver.mkConst(solver.getIntegerSort(), "x");

Term t = solver.mkTerm(Kind::SET_MEMBER, {x, X});

Subset

(set.subset X Y)

Term t = solver.mkTerm(Kind::SET_SUBSET, {X, Y});

Emptyset

(as set.empty (Set Int)

Term t = solver.mkEmptySet(s);

Singleton Set

(set.singleton 1)

Term t = solver.mkTerm(Kind::SET_SINGLETON, {solver.mkInteger(1)});

Cardinality

(set.card X)

Term t = solver.mkTerm(Kind::SET_CARD, {X});

Insert / Finite Sets

(set.insert 1 2 3 (set.singleton 4))

Term one = solver.mkInteger(1);

Term two = solver.mkInteger(2);

Term three = solver.mkInteger(3);

Term sgl = solver.mkTerm(Kind::SET_SINGLETON, {solver.mkInteger(4)});

Term t = solver.mkTerm(Kind::SET_INSERT, {one, two, three, sgl});

Complement

(set.complement X)

Term t = solver.mkTerm(Kind::SET_COMPLEMENT, {X});

Universe Set

(as set.universe (Set Int))

Term t = solver.mkUniverseSet(s);

Semantics

The semantics of most of the above operators (e.g., set.union , set.inter , difference) are straightforward. The semantics for the universe set and complement are more subtle and explained in the following.

The universe set (as set.universe (Set T)) is not interpreted as the set containing all elements of sort T . Instead it may be interpreted as any set such that all sets of sort (Set T) are interpreted as subsets of it. In other words, it is the union of the interpretations of all (finite) sets in our input.

For example: 

(declare-fun x () (Set Int))
(declare-fun y () (Set Int))
(declare-fun z () (Set Int))
(assert (set.member 0 x))
(assert (set.member 1 y))
(assert (= z (as set.universe (Set Int))))
(check-sat)

Here, a possible model is: 

(define-fun x () (set.singleton 0))
(define-fun y () (set.singleton 1))
(define-fun z () (set.union (set.singleton 1) (set.singleton 0)))

Notice that the universe set in this example is interpreted the same as z , and is such that all sets in this example ( x , y , and z ) are subsets of it.

The set complement operator for (Set T) is interpreted relative to the interpretation of the universe set for (Set T) , and not relative to the set of all elements of sort T . That is, for all sets X of sort (Set T) , the complement operator is such that (= (set.complement X) (set.minus (as set.universe (Set T)) X)) holds in all models.

The motivation for these semantics is to ensure that the universe set for sort T and applications of set complement can always be interpreted as a finite set in (quantifier-free) inputs, even if the cardinality of T is infinite. Above, notice that we were able to find a model for the universe set of sort (Set Int) that contained two elements only.

Note

In the presence of quantifiers, cvc5’s implementation of the above theory allows infinite sets. In particular, the following formula is SAT (even though cvc5 is not able to say this): 

(set-logic ALL)
(declare-fun x () (Set Int))
(assert (forall ((z Int) (set.member (* 2 z) x)))
(check-sat)

The reason for that is that making this formula (and similar ones) unsat is counter-intuitive when quantifiers are present.

Below is a more extensive example on how to use finite sets:

examples/api/cpp/sets.cpp 

 1 /******************************************************************************
 2  * Top contributors (to current version):
 3  *   Aina Niemetz, Kshitij Bansal, Mathias Preiner
 4  *
 5  * This file is part of the cvc5 project.
 6  *
 7  * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
 8  * in the top-level source directory and their institutional affiliations.
 9  * All rights reserved.  See the file COPYING in the top-level source
10  * directory for licensing information.
11  * ****************************************************************************
12  *
13  * A simple demonstration of reasoning about sets with cvc5.
14  */
15 
16 #include <cvc5/cvc5.h>
17 
18 #include <iostream>
19 
20 using namespace std;
21 using namespace cvc5;
22 
23 int main()
24 {
25   Solver slv;
26 
27   // Optionally, set the logic. We need at least UF for equality predicate,
28   // integers (LIA) and sets (FS).
29   slv.setLogic("QF_UFLIAFS");
30 
31   // Produce models
32   slv.setOption("produce-models", "true");
33   slv.setOption("output-language", "smt2");
34 
35   Sort integer = slv.getIntegerSort();
36   Sort set = slv.mkSetSort(integer);
37 
38   // Verify union distributions over intersection
39   // (A union B) intersection C = (A intersection C) union (B intersection C)
40   {
41     Term A = slv.mkConst(set, "A");
42     Term B = slv.mkConst(set, "B");
43     Term C = slv.mkConst(set, "C");
44 
45     Term unionAB = slv.mkTerm(SET_UNION, {A, B});
46     Term lhs = slv.mkTerm(SET_INTER, {unionAB, C});
47 
48     Term intersectionAC = slv.mkTerm(SET_INTER, {A, C});
49     Term intersectionBC = slv.mkTerm(SET_INTER, {B, C});
50     Term rhs = slv.mkTerm(SET_UNION, {intersectionAC, intersectionBC});
51 
52     Term theorem = slv.mkTerm(EQUAL, {lhs, rhs});
53 
54     cout << "cvc5 reports: " << theorem << " is "
55          << slv.checkSatAssuming(theorem.notTerm()) << "." << endl;
56   }
57 
58   // Verify emptset is a subset of any set
59   {
60     Term A = slv.mkConst(set, "A");
61     Term emptyset = slv.mkEmptySet(set);
62 
63     Term theorem = slv.mkTerm(SET_SUBSET, {emptyset, A});
64 
65     cout << "cvc5 reports: " << theorem << " is "
66          << slv.checkSatAssuming(theorem.notTerm()) << "." << endl;
67   }
68 
69   // Find me an element in {1, 2} intersection {2, 3}, if there is one.
70   {
71     Term one = slv.mkInteger(1);
72     Term two = slv.mkInteger(2);
73     Term three = slv.mkInteger(3);
74 
75     Term singleton_one = slv.mkTerm(SET_SINGLETON, {one});
76     Term singleton_two = slv.mkTerm(SET_SINGLETON, {two});
77     Term singleton_three = slv.mkTerm(SET_SINGLETON, {three});
78     Term one_two = slv.mkTerm(SET_UNION, {singleton_one, singleton_two});
79     Term two_three = slv.mkTerm(SET_UNION, {singleton_two, singleton_three});
80     Term intersection = slv.mkTerm(SET_INTER, {one_two, two_three});
81 
82     Term x = slv.mkConst(integer, "x");
83 
84     Term e = slv.mkTerm(SET_MEMBER, {x, intersection});
85 
86     Result result = slv.checkSatAssuming(e);
87     cout << "cvc5 reports: " << e << " is " << result << "." << endl;
88 
89     if (result.isSat())
90     {
91       cout << "For instance, " << slv.getValue(x) << " is a member." << endl;
92     }
93   }
94 }

Finite Relations

cvc5 also supports the theory of finite relations, using the following sorts, constants, functions and predicates. More details can be found in [ MRTB17 ] .

SMTLIB language

C++ API

Logic String

(set-logic QF_ALL)

solver.setLogic("QF_ALL");

Tuple Sort

(Tuple <Sort_1>, ..., <Sort_n>)

std::vector<cvc5::Sort> sorts = { ... };

Sort s = solver.mkTupleSort(sorts);

(declare-const t (Tuple Int Int))

Sort s_int = solver.getIntegerSort();

Sort s = solver.mkTupleSort({s_int, s_int});

Term t = solver.mkConst(s, "t");

Tuple Constructor

(tuple <Term_1>, ..., <Term_n>)

Term t = solver.mkTuple({<Sort_1>, ..., <Sort_n>}, {Term_1>, ..., <Term_n>});

Tuple Selector

((_ tuple_select i) t)

Sort s = solver.mkTupleSort(sorts);

Datatype dt = s.getDatatype();

Term c = dt[0].getSelector();

Term t = solver.mkTerm(Kind::APPLY_SELECTOR, {s, t});

Relation Sort

(Set (Tuple <Sort_1>, ..., <Sort_n>))

Sort s = solver.mkSetSort(cvc5::Sort tupleSort);

Constants

(declare-const X (Set (Tuple Int Int)

Sort s = solver.mkSetSort(solver.mkTupleSort({s_int, s_int});

Term X = solver.mkConst(s, "X");

Transpose

(rel.transpose X)

Term t = solver.mkTerm(Kind::RELATION_TRANSPOSE, X);

Transitive Closure

(rel.tclosure X)

Term t = solver.mkTerm(Kind::RELATION_TCLOSURE, X);

Join

(rel.join X Y)

Term t = solver.mkTerm(Kind::RELATION_JOIN, X, Y);

Product

(rel.product X Y)

Term t = solver.mkTerm(Kind::RELATION_PRODUCT, X, Y);

Example:

examples/api/cpp/relations.cpp 

  1 /******************************************************************************
  2  * Top contributors (to current version):
  3  *   Mudathir Mohamed, Mathias Preiner
  4  *
  5  * This file is part of the cvc5 project.
  6  *
  7  * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
  8  * in the top-level source directory and their institutional affiliations.
  9  * All rights reserved.  See the file COPYING in the top-level source
 10  * directory for licensing information.
 11  * ****************************************************************************
 12  *
 13  * A simple demonstration of reasoning about relations with cvc5 via C++ API.
 14  */
 15 
 16 #include <cvc5/cvc5.h>
 17 
 18 #include <iostream>
 19 
 20 using namespace cvc5;
 21 
 22 int main()
 23 {
 24   Solver solver;
 25 
 26   // Set the logic
 27   solver.setLogic("ALL");
 28 
 29   // options
 30   solver.setOption("produce-models", "true");
 31   // we need finite model finding to answer sat problems with universal
 32   // quantified formulas
 33   solver.setOption("finite-model-find", "true");
 34   // we need sets extension to support set.universe operator
 35   solver.setOption("sets-ext", "true");
 36 
 37   // (declare-sort Person 0)
 38   Sort personSort = solver.mkUninterpretedSort("Person");
 39 
 40   // (Tuple Person)
 41   Sort tupleArity1 = solver.mkTupleSort({personSort});
 42   // (Set (Tuple Person))
 43   Sort relationArity1 = solver.mkSetSort(tupleArity1);
 44 
 45   // (Tuple Person Person)
 46   Sort tupleArity2 = solver.mkTupleSort({personSort, personSort});
 47   // (Set (Tuple Person Person))
 48   Sort relationArity2 = solver.mkSetSort(tupleArity2);
 49 
 50   // empty set
 51   Term emptySetTerm = solver.mkEmptySet(relationArity1);
 52 
 53   // empty relation
 54   Term emptyRelationTerm = solver.mkEmptySet(relationArity2);
 55 
 56   // universe set
 57   Term universeSet = solver.mkUniverseSet(relationArity1);
 58 
 59   // variables
 60   Term people = solver.mkConst(relationArity1, "people");
 61   Term males = solver.mkConst(relationArity1, "males");
 62   Term females = solver.mkConst(relationArity1, "females");
 63   Term father = solver.mkConst(relationArity2, "father");
 64   Term mother = solver.mkConst(relationArity2, "mother");
 65   Term parent = solver.mkConst(relationArity2, "parent");
 66   Term ancestor = solver.mkConst(relationArity2, "ancestor");
 67   Term descendant = solver.mkConst(relationArity2, "descendant");
 68 
 69   Term isEmpty1 = solver.mkTerm(EQUAL, {males, emptySetTerm});
 70   Term isEmpty2 = solver.mkTerm(EQUAL, {females, emptySetTerm});
 71 
 72   // (assert (= people (as set.universe (Set (Tuple Person)))))
 73   Term peopleAreTheUniverse = solver.mkTerm(EQUAL, {people, universeSet});
 74   // (assert (not (= males (as set.empty (Set (Tuple Person))))))
 75   Term maleSetIsNotEmpty = solver.mkTerm(NOT, {isEmpty1});
 76   // (assert (not (= females (as set.empty (Set (Tuple Person))))))
 77   Term femaleSetIsNotEmpty = solver.mkTerm(NOT, {isEmpty2});
 78 
 79   // (assert (= (set.inter males females)
 80   //            (as set.empty (Set (Tuple Person)))))
 81   Term malesFemalesIntersection = solver.mkTerm(SET_INTER, {males, females});
 82   Term malesAndFemalesAreDisjoint =
 83       solver.mkTerm(EQUAL, {malesFemalesIntersection, emptySetTerm});
 84 
 85   // (assert (not (= father (as set.empty (Set (Tuple Person Person))))))
 86   // (assert (not (= mother (as set.empty (Set (Tuple Person Person))))))
 87   Term isEmpty3 = solver.mkTerm(EQUAL, {father, emptyRelationTerm});
 88   Term isEmpty4 = solver.mkTerm(EQUAL, {mother, emptyRelationTerm});
 89   Term fatherIsNotEmpty = solver.mkTerm(NOT, {isEmpty3});
 90   Term motherIsNotEmpty = solver.mkTerm(NOT, {isEmpty4});
 91 
 92   // fathers are males
 93   // (assert (set.subset (rel.join father people) males))
 94   Term fathers = solver.mkTerm(RELATION_JOIN, {father, people});
 95   Term fathersAreMales = solver.mkTerm(SET_SUBSET, {fathers, males});
 96 
 97   // mothers are females
 98   // (assert (set.subset (rel.join mother people) females))
 99   Term mothers = solver.mkTerm(RELATION_JOIN, {mother, people});
100   Term mothersAreFemales = solver.mkTerm(SET_SUBSET, {mothers, females});
101 
102   // (assert (= parent (set.union father mother)))
103   Term unionFatherMother = solver.mkTerm(SET_UNION, {father, mother});
104   Term parentIsFatherOrMother =
105       solver.mkTerm(EQUAL, {parent, unionFatherMother});
106 
107   // (assert (= ancestor (rel.tclosure parent)))
108   Term transitiveClosure = solver.mkTerm(RELATION_TCLOSURE, {parent});
109   Term ancestorFormula = solver.mkTerm(EQUAL, {ancestor, transitiveClosure});
110 
111   // (assert (= descendant (rel.transpose descendant)))
112   Term transpose = solver.mkTerm(RELATION_TRANSPOSE, {ancestor});
113   Term descendantFormula = solver.mkTerm(EQUAL, {descendant, transpose});
114 
115   // (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
116   Term x = solver.mkVar(personSort, "x");
117   Term xxTuple = solver.mkTuple({personSort, personSort}, {x, x});
118   Term member = solver.mkTerm(SET_MEMBER, {xxTuple, ancestor});
119   Term notMember = solver.mkTerm(NOT, {member});
120 
121   Term quantifiedVariables = solver.mkTerm(VARIABLE_LIST, {x});
122   Term noSelfAncestor = solver.mkTerm(FORALL, {quantifiedVariables, notMember});
123 
124   // formulas
125   solver.assertFormula(peopleAreTheUniverse);
126   solver.assertFormula(maleSetIsNotEmpty);
127   solver.assertFormula(femaleSetIsNotEmpty);
128   solver.assertFormula(malesAndFemalesAreDisjoint);
129   solver.assertFormula(fatherIsNotEmpty);
130   solver.assertFormula(motherIsNotEmpty);
131   solver.assertFormula(fathersAreMales);
132   solver.assertFormula(mothersAreFemales);
133   solver.assertFormula(parentIsFatherOrMother);
134   solver.assertFormula(descendantFormula);
135   solver.assertFormula(ancestorFormula);
136   solver.assertFormula(noSelfAncestor);
137 
138   // check sat
139   Result result = solver.checkSat();
140 
141   // output
142   std::cout << "Result     = " << result << std::endl;
143   std::cout << "people     = " << solver.getValue(people) << std::endl;
144   std::cout << "males      = " << solver.getValue(males) << std::endl;
145   std::cout << "females    = " << solver.getValue(females) << std::endl;
146   std::cout << "father     = " << solver.getValue(father) << std::endl;
147   std::cout << "mother     = " << solver.getValue(mother) << std::endl;
148   std::cout << "parent     = " << solver.getValue(parent) << std::endl;
149   std::cout << "descendant = " << solver.getValue(descendant) << std::endl;
150   std::cout << "ancestor   = " << solver.getValue(ancestor) << std::endl;
151 }