Theory of Sets

examples/api/cpp/sets.cpp

 1/******************************************************************************
 2 * Top contributors (to current version):
 3 *   Aina Niemetz, Kshitij Bansal, Andrew Reynolds
 4 *
 5 * This file is part of the cvc5 project.
 6 *
 7 * Copyright (c) 2009-2024 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 via the C++ API.
14 */
15
16#include <cvc5/cvc5.h>
17
18#include <iostream>
19
20using namespace std;
21using namespace cvc5;
22
23int main()
24{
25  TermManager tm;
26  Solver slv(tm);
27
28  // Optionally, set the logic. We need at least UF for equality predicate,
29  // integers (LIA) and sets (FS).
30  slv.setLogic("QF_UFLIAFS");
31
32  // Produce models
33  slv.setOption("produce-models", "true");
34
35  Sort integer = tm.getIntegerSort();
36  Sort set = tm.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 = tm.mkConst(set, "A");
42    Term B = tm.mkConst(set, "B");
43    Term C = tm.mkConst(set, "C");
44
45    Term unionAB = tm.mkTerm(Kind::SET_UNION, {A, B});
46    Term lhs = tm.mkTerm(Kind::SET_INTER, {unionAB, C});
47
48    Term intersectionAC = tm.mkTerm(Kind::SET_INTER, {A, C});
49    Term intersectionBC = tm.mkTerm(Kind::SET_INTER, {B, C});
50    Term rhs = tm.mkTerm(Kind::SET_UNION, {intersectionAC, intersectionBC});
51
52    Term theorem = tm.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 = tm.mkConst(set, "A");
61    Term emptyset = tm.mkEmptySet(set);
62
63    Term theorem = tm.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 = tm.mkInteger(1);
72    Term two = tm.mkInteger(2);
73    Term three = tm.mkInteger(3);
74
75    Term singleton_one = tm.mkTerm(Kind::SET_SINGLETON, {one});
76    Term singleton_two = tm.mkTerm(Kind::SET_SINGLETON, {two});
77    Term singleton_three = tm.mkTerm(Kind::SET_SINGLETON, {three});
78    Term one_two = tm.mkTerm(Kind::SET_UNION, {singleton_one, singleton_two});
79    Term two_three =
80        tm.mkTerm(Kind::SET_UNION, {singleton_two, singleton_three});
81    Term intersection = tm.mkTerm(Kind::SET_INTER, {one_two, two_three});
82
83    Term x = tm.mkConst(integer, "x");
84
85    Term e = tm.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}