1 /********************* */
2 /*! \file sets-new.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Aina Niemetz, Makai Mann
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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.\endverbatim
11 **
12 ** \brief Reasoning about sets with CVC4.
13 **
14 ** A simple demonstration of reasoning about sets with CVC4.
15 **/
16
17 #include <iostream>
18
19 // #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
20 #include "api/cvc4cpp.h"
21
22 using namespace std;
23 using namespace CVC4::api;
24
main()25 int main()
26 {
27 Solver slv;
28
29 // Optionally, set the logic. We need at least UF for equality predicate,
30 // integers (LIA) and sets (FS).
31 slv.setLogic("QF_UFLIAFS");
32
33 // Produce models
34 slv.setOption("produce-models", "true");
35 slv.setOption("output-language", "smt2");
36
37 Sort integer = slv.getIntegerSort();
38 Sort set = slv.mkSetSort(integer);
39
40 // Verify union distributions over intersection
41 // (A union B) intersection C = (A intersection C) union (B intersection C)
42 {
43 Term A = slv.mkVar(set, "A");
44 Term B = slv.mkVar(set, "B");
45 Term C = slv.mkVar(set, "C");
46
47 Term unionAB = slv.mkTerm(UNION, A, B);
48 Term lhs = slv.mkTerm(INTERSECTION, unionAB, C);
49
50 Term intersectionAC = slv.mkTerm(INTERSECTION, A, C);
51 Term intersectionBC = slv.mkTerm(INTERSECTION, B, C);
52 Term rhs = slv.mkTerm(UNION, intersectionAC, intersectionBC);
53
54 Term theorem = slv.mkTerm(EQUAL, lhs, rhs);
55
56 cout << "CVC4 reports: " << theorem << " is "
57 << slv.checkValidAssuming(theorem) << "." << endl;
58 }
59
60 // Verify emptset is a subset of any set
61 {
62 Term A = slv.mkVar(set, "A");
63 Term emptyset = slv.mkEmptySet(set);
64
65 Term theorem = slv.mkTerm(SUBSET, emptyset, A);
66
67 cout << "CVC4 reports: " << theorem << " is "
68 << slv.checkValidAssuming(theorem) << "." << endl;
69 }
70
71 // Find me an element in {1, 2} intersection {2, 3}, if there is one.
72 {
73 Term one = slv.mkReal(1);
74 Term two = slv.mkReal(2);
75 Term three = slv.mkReal(3);
76
77 Term singleton_one = slv.mkTerm(SINGLETON, one);
78 Term singleton_two = slv.mkTerm(SINGLETON, two);
79 Term singleton_three = slv.mkTerm(SINGLETON, three);
80 Term one_two = slv.mkTerm(UNION, singleton_one, singleton_two);
81 Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three);
82 Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three);
83
84 Term x = slv.mkVar(integer, "x");
85
86 Term e = slv.mkTerm(MEMBER, x, intersection);
87
88 Result result = slv.checkSatAssuming(e);
89 cout << "CVC4 reports: " << e << " is " << result << "." << endl;
90
91 if (result.isSat())
92 {
93 cout << "For instance, " << slv.getValue(x) << " is a member." << endl;
94 }
95 }
96 }
97