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
20using namespace std;
21using namespace cvc5;
22
23int 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(Kind::SET_UNION, {A, B});
46    Term lhs = slv.mkTerm(Kind::SET_INTER, {unionAB, C});
47
48    Term intersectionAC = slv.mkTerm(Kind::SET_INTER, {A, C});
49    Term intersectionBC = slv.mkTerm(Kind::SET_INTER, {B, C});
50    Term rhs = slv.mkTerm(Kind::SET_UNION, {intersectionAC, intersectionBC});
51
52    Term theorem = slv.mkTerm(Kind::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(Kind::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(Kind::SET_SINGLETON, {one});
76    Term singleton_two = slv.mkTerm(Kind::SET_SINGLETON, {two});
77    Term singleton_three = slv.mkTerm(Kind::SET_SINGLETON, {three});
78    Term one_two = slv.mkTerm(Kind::SET_UNION, {singleton_one, singleton_two});
79    Term two_three =
80        slv.mkTerm(Kind::SET_UNION, {singleton_two, singleton_three});
81    Term intersection = slv.mkTerm(Kind::SET_INTER, {one_two, two_three});
82
83    Term x = slv.mkConst(integer, "x");
84
85    Term e = slv.mkTerm(Kind::SET_MEMBER, {x, intersection});
86
87    Result result = slv.checkSatAssuming(e);
88    cout << "cvc5 reports: " << e << " is " << result << "." << endl;
89
90    if (result.isSat())
91    {
92      cout << "For instance, " << slv.getValue(x) << " is a member." << endl;
93    }
94  }
95}

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

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

which is a syntax sugar for

(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
 20using namespace cvc5;
 21
 22int 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  // (Relation Person)
 43  Sort relationArity1 = solver.mkSetSort(tupleArity1);
 44
 45  // (Tuple Person Person)
 46  Sort tupleArity2 = solver.mkTupleSort({personSort, personSort});
 47  // (Relation 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(Kind::EQUAL, {males, emptySetTerm});
 70  Term isEmpty2 = solver.mkTerm(Kind::EQUAL, {females, emptySetTerm});
 71
 72  // (assert (= people (as set.universe (Relation Person))))
 73  Term peopleAreTheUniverse = solver.mkTerm(Kind::EQUAL, {people, universeSet});
 74  // (assert (not (= males (as set.empty (Relation Person)))))
 75  Term maleSetIsNotEmpty = solver.mkTerm(Kind::NOT, {isEmpty1});
 76  // (assert (not (= females (as set.empty (Relation Person)))))
 77  Term femaleSetIsNotEmpty = solver.mkTerm(Kind::NOT, {isEmpty2});
 78
 79  // (assert (= (set.inter males females)
 80  //            (as set.empty (Relation Person))))
 81  Term malesFemalesIntersection =
 82      solver.mkTerm(Kind::SET_INTER, {males, females});
 83  Term malesAndFemalesAreDisjoint =
 84      solver.mkTerm(Kind::EQUAL, {malesFemalesIntersection, emptySetTerm});
 85
 86  // (assert (not (= father (as set.empty (Relation Person Person)))))
 87  // (assert (not (= mother (as set.empty (Relation Person Person)))))
 88  Term isEmpty3 = solver.mkTerm(Kind::EQUAL, {father, emptyRelationTerm});
 89  Term isEmpty4 = solver.mkTerm(Kind::EQUAL, {mother, emptyRelationTerm});
 90  Term fatherIsNotEmpty = solver.mkTerm(Kind::NOT, {isEmpty3});
 91  Term motherIsNotEmpty = solver.mkTerm(Kind::NOT, {isEmpty4});
 92
 93  // fathers are males
 94  // (assert (set.subset (rel.join father people) males))
 95  Term fathers = solver.mkTerm(Kind::RELATION_JOIN, {father, people});
 96  Term fathersAreMales = solver.mkTerm(Kind::SET_SUBSET, {fathers, males});
 97
 98  // mothers are females
 99  // (assert (set.subset (rel.join mother people) females))
100  Term mothers = solver.mkTerm(Kind::RELATION_JOIN, {mother, people});
101  Term mothersAreFemales = solver.mkTerm(Kind::SET_SUBSET, {mothers, females});
102
103  // (assert (= parent (set.union father mother)))
104  Term unionFatherMother = solver.mkTerm(Kind::SET_UNION, {father, mother});
105  Term parentIsFatherOrMother =
106      solver.mkTerm(Kind::EQUAL, {parent, unionFatherMother});
107
108  // (assert (= ancestor (rel.tclosure parent)))
109  Term transitiveClosure = solver.mkTerm(Kind::RELATION_TCLOSURE, {parent});
110  Term ancestorFormula =
111      solver.mkTerm(Kind::EQUAL, {ancestor, transitiveClosure});
112
113  // (assert (= descendant (rel.transpose descendant)))
114  Term transpose = solver.mkTerm(Kind::RELATION_TRANSPOSE, {ancestor});
115  Term descendantFormula = solver.mkTerm(Kind::EQUAL, {descendant, transpose});
116
117  // (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
118  Term x = solver.mkVar(personSort, "x");
119  Term xxTuple = solver.mkTuple({x, x});
120  Term member = solver.mkTerm(Kind::SET_MEMBER, {xxTuple, ancestor});
121  Term notMember = solver.mkTerm(Kind::NOT, {member});
122
123  Term quantifiedVariables = solver.mkTerm(Kind::VARIABLE_LIST, {x});
124  Term noSelfAncestor =
125      solver.mkTerm(Kind::FORALL, {quantifiedVariables, notMember});
126
127  // formulas
128  solver.assertFormula(peopleAreTheUniverse);
129  solver.assertFormula(maleSetIsNotEmpty);
130  solver.assertFormula(femaleSetIsNotEmpty);
131  solver.assertFormula(malesAndFemalesAreDisjoint);
132  solver.assertFormula(fatherIsNotEmpty);
133  solver.assertFormula(motherIsNotEmpty);
134  solver.assertFormula(fathersAreMales);
135  solver.assertFormula(mothersAreFemales);
136  solver.assertFormula(parentIsFatherOrMother);
137  solver.assertFormula(descendantFormula);
138  solver.assertFormula(ancestorFormula);
139  solver.assertFormula(noSelfAncestor);
140
141  // check sat
142  Result result = solver.checkSat();
143
144  // output
145  std::cout << "Result     = " << result << std::endl;
146  std::cout << "people     = " << solver.getValue(people) << std::endl;
147  std::cout << "males      = " << solver.getValue(males) << std::endl;
148  std::cout << "females    = " << solver.getValue(females) << std::endl;
149  std::cout << "father     = " << solver.getValue(father) << std::endl;
150  std::cout << "mother     = " << solver.getValue(mother) << std::endl;
151  std::cout << "parent     = " << solver.getValue(parent) << std::endl;
152  std::cout << "descendant = " << solver.getValue(descendant) << std::endl;
153  std::cout << "ancestor   = " << solver.getValue(ancestor) << std::endl;
154}