Theory of 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(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}