Theory of Sets
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of reasoning about sets via the C++ API.
11 */
12
13#include <cvc5/cvc5.h>
14
15#include <iostream>
16
17using namespace std;
18using namespace cvc5;
19
20int main()
21{
22 TermManager tm;
23 Solver slv(tm);
24
25 // Optionally, set the logic. We need at least UF for equality predicate,
26 // integers (LIA) and sets (FS).
27 slv.setLogic("QF_UFLIAFS");
28
29 // Produce models
30 slv.setOption("produce-models", "true");
31
32 Sort integer = tm.getIntegerSort();
33 Sort set = tm.mkSetSort(integer);
34
35 // Verify union distributions over intersection
36 // (A union B) intersection C = (A intersection C) union (B intersection C)
37 {
38 Term A = tm.mkConst(set, "A");
39 Term B = tm.mkConst(set, "B");
40 Term C = tm.mkConst(set, "C");
41
42 Term unionAB = tm.mkTerm(Kind::SET_UNION, {A, B});
43 Term lhs = tm.mkTerm(Kind::SET_INTER, {unionAB, C});
44
45 Term intersectionAC = tm.mkTerm(Kind::SET_INTER, {A, C});
46 Term intersectionBC = tm.mkTerm(Kind::SET_INTER, {B, C});
47 Term rhs = tm.mkTerm(Kind::SET_UNION, {intersectionAC, intersectionBC});
48
49 Term theorem = tm.mkTerm(Kind::EQUAL, {lhs, rhs});
50
51 cout << "cvc5 reports: " << theorem << " is "
52 << slv.checkSatAssuming(theorem.notTerm()) << "." << endl;
53 }
54
55 // Verify emptset is a subset of any set
56 {
57 Term A = tm.mkConst(set, "A");
58 Term emptyset = tm.mkEmptySet(set);
59
60 Term theorem = tm.mkTerm(Kind::SET_SUBSET, {emptyset, A});
61
62 cout << "cvc5 reports: " << theorem << " is "
63 << slv.checkSatAssuming(theorem.notTerm()) << "." << endl;
64 }
65
66 // Find me an element in {1, 2} intersection {2, 3}, if there is one.
67 {
68 Term one = tm.mkInteger(1);
69 Term two = tm.mkInteger(2);
70 Term three = tm.mkInteger(3);
71
72 Term singleton_one = tm.mkTerm(Kind::SET_SINGLETON, {one});
73 Term singleton_two = tm.mkTerm(Kind::SET_SINGLETON, {two});
74 Term singleton_three = tm.mkTerm(Kind::SET_SINGLETON, {three});
75 Term one_two = tm.mkTerm(Kind::SET_UNION, {singleton_one, singleton_two});
76 Term two_three =
77 tm.mkTerm(Kind::SET_UNION, {singleton_two, singleton_three});
78 Term intersection = tm.mkTerm(Kind::SET_INTER, {one_two, two_three});
79
80 Term x = tm.mkConst(integer, "x");
81
82 Term e = tm.mkTerm(Kind::SET_MEMBER, {x, intersection});
83
84 Result result = slv.checkSatAssuming(e);
85 cout << "cvc5 reports: " << e << " is " << result << "." << endl;
86
87 if (result.isSat())
88 {
89 cout << "For instance, " << slv.getValue(x) << " is a member." << endl;
90 }
91 }
92}
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of reasoning about sets via the C API.
11 */
12
13#include <cvc5/c/cvc5.h>
14#include <stdio.h>
15
16int main()
17{
18 Cvc5TermManager* tm = cvc5_term_manager_new();
19 Cvc5* slv = cvc5_new(tm);
20
21 // Optionally, set the logic. We need at least UF for equality predicate,
22 // integers (LIA) and sets (FS).
23 cvc5_set_logic(slv, "QF_UFLIAFS");
24
25 // Produce models
26 cvc5_set_option(slv, "produce-models", "true");
27
28 Cvc5Sort int_sort = cvc5_get_integer_sort(tm);
29 Cvc5Sort set_sort = cvc5_mk_set_sort(tm, int_sort);
30
31 // Verify union distributions over intersection
32 // (A union B) intersection C = (A intersection C) union (B intersection C)
33 {
34 Cvc5Term A = cvc5_mk_const(tm, set_sort, "A");
35 Cvc5Term B = cvc5_mk_const(tm, set_sort, "B");
36 Cvc5Term C = cvc5_mk_const(tm, set_sort, "C");
37
38 Cvc5Term args2[2] = {A, B};
39 Cvc5Term union_AB = cvc5_mk_term(tm, CVC5_KIND_SET_UNION, 2, args2);
40 args2[0] = union_AB;
41 args2[1] = C;
42 Cvc5Term lhs = cvc5_mk_term(tm, CVC5_KIND_SET_INTER, 2, args2);
43
44 args2[0] = A;
45 args2[1] = C;
46 Cvc5Term inter_AC = cvc5_mk_term(tm, CVC5_KIND_SET_INTER, 2, args2);
47 args2[0] = B;
48 args2[1] = C;
49 Cvc5Term inter_BC = cvc5_mk_term(tm, CVC5_KIND_SET_INTER, 2, args2);
50 args2[0] = inter_AC;
51 args2[1] = inter_BC;
52 Cvc5Term rhs = cvc5_mk_term(tm, CVC5_KIND_SET_UNION, 2, args2);
53
54 args2[0] = lhs;
55 args2[1] = rhs;
56 Cvc5Term theorem = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
57
58 Cvc5Term args1[1] = {theorem};
59 Cvc5Term assumptions[1] = {cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args1)};
60 printf("cvc5 reports: %s is %s.\n",
61 cvc5_term_to_string(theorem),
62 cvc5_result_to_string(cvc5_check_sat_assuming(slv, 1, assumptions)));
63 // optional, not needed anymore so we can release
64 cvc5_term_release(A);
65 cvc5_term_release(B);
66 cvc5_term_release(C);
67 cvc5_term_release(union_AB);
68 cvc5_term_release(inter_AC);
69 cvc5_term_release(inter_BC);
70 cvc5_term_release(lhs);
71 cvc5_term_release(rhs);
72 cvc5_term_release(theorem);
73 }
74
75 // Verify emptset is a subset of any set
76 {
77 Cvc5Term A = cvc5_mk_const(tm, set_sort, "A");
78 Cvc5Term empty_set = cvc5_mk_empty_set(tm, set_sort);
79
80 Cvc5Term args2[2] = {empty_set, A};
81 Cvc5Term theorem = cvc5_mk_term(tm, CVC5_KIND_SET_SUBSET, 2, args2);
82
83 Cvc5Term args1[1] = {theorem};
84 Cvc5Term assumptions[1] = {cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args1)};
85 printf("cvc5 reports: %s is %s.\n",
86 cvc5_term_to_string(theorem),
87 cvc5_result_to_string(cvc5_check_sat_assuming(slv, 1, assumptions)));
88 // optional, not needed anymore so we can release
89 cvc5_term_release(A);
90 cvc5_term_release(theorem);
91 }
92
93 // Find me an element in {1, 2} intersection {2, 3}, if there is one.
94 {
95 Cvc5Term one = cvc5_mk_integer_int64(tm, 1);
96 Cvc5Term two = cvc5_mk_integer_int64(tm, 2);
97 Cvc5Term three = cvc5_mk_integer_int64(tm, 3);
98
99 Cvc5Term args1[1] = {one};
100 Cvc5Term sing_one = cvc5_mk_term(tm, CVC5_KIND_SET_SINGLETON, 1, args1);
101 args1[0] = two;
102 Cvc5Term sing_two = cvc5_mk_term(tm, CVC5_KIND_SET_SINGLETON, 1, args1);
103 args1[0] = three;
104 Cvc5Term sing_three = cvc5_mk_term(tm, CVC5_KIND_SET_SINGLETON, 1, args1);
105 Cvc5Term args2[2] = {sing_one, sing_two};
106 Cvc5Term one_two = cvc5_mk_term(tm, CVC5_KIND_SET_UNION, 2, args2);
107 args2[0] = sing_two;
108 args2[1] = sing_three;
109 Cvc5Term two_three = cvc5_mk_term(tm, CVC5_KIND_SET_UNION, 2, args2);
110 args2[0] = one_two;
111 args2[1] = two_three;
112 Cvc5Term inter = cvc5_mk_term(tm, CVC5_KIND_SET_INTER, 2, args2);
113
114 Cvc5Term x = cvc5_mk_const(tm, int_sort, "x");
115 args2[0] = x;
116 args2[1] = inter;
117 Cvc5Term e = cvc5_mk_term(tm, CVC5_KIND_SET_MEMBER, 2, args2);
118
119 Cvc5Term assumptions[1] = {e};
120 Cvc5Result result = cvc5_check_sat_assuming(slv, 1, assumptions);
121 printf("cvc5 reports: %s is %s.\n",
122 cvc5_term_to_string(e),
123 cvc5_result_to_string(result));
124
125 if (cvc5_result_is_sat(result))
126 {
127 printf("For instance, %s is a member.\n",
128 cvc5_term_to_string(cvc5_get_value(slv, x)));
129 }
130 }
131 cvc5_delete(slv);
132 cvc5_term_manager_delete(tm);
133}
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of reasoning about sets with cvc5.
11 */
12
13import static io.github.cvc5.Kind.*;
14
15import io.github.cvc5.*;
16
17public class Sets
18{
19 public static void main(String args[]) throws CVC5ApiException
20 {
21 TermManager tm = new TermManager();
22 Solver slv = new Solver(tm);
23 {
24 // Optionally, set the logic. We need at least UF for equality predicate,
25 // integers (LIA) and sets (FS).
26 slv.setLogic("QF_UFLIAFS");
27
28 // Produce models
29 slv.setOption("produce-models", "true");
30 slv.setOption("output-language", "smt2");
31
32 Sort integer = tm.getIntegerSort();
33 Sort set = tm.mkSetSort(integer);
34
35 // Verify union distributions over intersection
36 // (A union B) intersection C = (A intersection C) union (B intersection C)
37 {
38 Term A = tm.mkConst(set, "A");
39 Term B = tm.mkConst(set, "B");
40 Term C = tm.mkConst(set, "C");
41
42 Term unionAB = tm.mkTerm(SET_UNION, A, B);
43 Term lhs = tm.mkTerm(SET_INTER, unionAB, C);
44
45 Term intersectionAC = tm.mkTerm(SET_INTER, A, C);
46 Term intersectionBC = tm.mkTerm(SET_INTER, B, C);
47 Term rhs = tm.mkTerm(SET_UNION, intersectionAC, intersectionBC);
48
49 Term theorem = tm.mkTerm(EQUAL, lhs, rhs);
50
51 System.out.println(
52 "cvc5 reports: " + theorem + " is " + slv.checkSatAssuming(theorem.notTerm()) + ".");
53 }
54
55 // Verify set.empty is a subset of any set
56 {
57 Term A = tm.mkConst(set, "A");
58 Term emptyset = tm.mkEmptySet(set);
59
60 Term theorem = tm.mkTerm(SET_SUBSET, emptyset, A);
61
62 System.out.println(
63 "cvc5 reports: " + theorem + " is " + slv.checkSatAssuming(theorem.notTerm()) + ".");
64 }
65
66 // Find me an element in {1, 2} intersection {2, 3}, if there is one.
67 {
68 Term one = tm.mkInteger(1);
69 Term two = tm.mkInteger(2);
70 Term three = tm.mkInteger(3);
71
72 Term singleton_one = tm.mkTerm(SET_SINGLETON, one);
73 Term singleton_two = tm.mkTerm(SET_SINGLETON, two);
74 Term singleton_three = tm.mkTerm(SET_SINGLETON, three);
75 Term one_two = tm.mkTerm(SET_UNION, singleton_one, singleton_two);
76 Term two_three = tm.mkTerm(SET_UNION, singleton_two, singleton_three);
77 Term intersection = tm.mkTerm(SET_INTER, one_two, two_three);
78
79 Term x = tm.mkConst(integer, "x");
80
81 Term e = tm.mkTerm(SET_MEMBER, x, intersection);
82
83 Result result = slv.checkSatAssuming(e);
84 System.out.println("cvc5 reports: " + e + " is " + result + ".");
85
86 if (result.isSat())
87 {
88 System.out.println("For instance, " + slv.getValue(x) + " is a member.");
89 }
90 }
91 }
92 Context.deletePointers();
93 }
94}
examples/api/python/pythonic/sets.py
1###############################################################################
2# This file is part of the cvc5 project.
3#
4# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5# in the top-level source directory and their institutional affiliations.
6# All rights reserved. See the file COPYING in the top-level source
7# directory for licensing information.
8# #############################################################################
9#
10# A simple demonstration of reasoning about sets with cvc5.
11##
12from cvc5.pythonic import *
13
14if __name__ == "__main__":
15 A, B, C = [Set(name, IntSort()) for name in "ABC"]
16
17 # holds
18 prove((A | B) & C == (A & C) | (B & C))
19
20 # holds
21 prove(IsSubset(EmptySet(IntSort()), A))
22
23 # x must be 2.
24 x = Int("x")
25 solve(
26 IsMember(
27 x,
28 (Singleton(IntVal(1)) | Singleton(IntVal(2)))
29 & (Singleton(IntVal(2)) | Singleton(IntVal(3))),
30 )
31 )
1#!/usr/bin/env python
2###############################################################################
3# This file is part of the cvc5 project.
4#
5# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
6# in the top-level source directory and their institutional affiliations.
7# All rights reserved. See the file COPYING in the top-level source
8# directory for licensing information.
9# #############################################################################
10#
11# A simple demonstration of the solving capabilities of the cvc5 sets solver
12# through the Python API. This is a direct translation of sets.cpp.
13##
14
15import cvc5
16from cvc5 import Kind
17
18if __name__ == "__main__":
19 tm = cvc5.TermManager()
20 slv = cvc5.Solver(tm)
21
22 # Optionally, set the logic. We need at least UF for equality predicate,
23 # integers (LIA) and sets (FS).
24 slv.setLogic("QF_UFLIAFS")
25
26 # Produce models
27 slv.setOption("produce-models", "true")
28 slv.setOption("output-language", "smt2")
29
30 integer = tm.getIntegerSort()
31 set_ = tm.mkSetSort(integer)
32
33 # Verify union distributions over intersection
34 # (A union B) intersection C = (A intersection C) union (B intersection C)
35
36 A = tm.mkConst(set_, "A")
37 B = tm.mkConst(set_, "B")
38 C = tm.mkConst(set_, "C")
39
40 unionAB = tm.mkTerm(Kind.SET_UNION, A, B)
41 lhs = tm.mkTerm(Kind.SET_INTER, unionAB, C)
42
43 intersectionAC = tm.mkTerm(Kind.SET_INTER, A, C)
44 intersectionBC = tm.mkTerm(Kind.SET_INTER, B, C)
45 rhs = tm.mkTerm(Kind.SET_UNION, intersectionAC, intersectionBC)
46
47 theorem = tm.mkTerm(Kind.EQUAL, lhs, rhs)
48
49 print("cvc5 reports: {} is {}".format(
50 theorem.notTerm(), slv.checkSatAssuming(theorem.notTerm())))
51
52 # Verify emptset is a subset of any set
53
54 A = tm.mkConst(set_, "A")
55 emptyset = tm.mkEmptySet(set_)
56
57 theorem = tm.mkTerm(Kind.SET_SUBSET, emptyset, A)
58
59 print("cvc5 reports: {} is {}".format(
60 theorem.notTerm(), slv.checkSatAssuming(theorem.notTerm())))
61
62 # Find me an element in 1, 2 intersection 2, 3, if there is one.
63
64 one = tm.mkInteger(1)
65 two = tm.mkInteger(2)
66 three = tm.mkInteger(3)
67
68 singleton_one = tm.mkTerm(Kind.SET_SINGLETON, one)
69 singleton_two = tm.mkTerm(Kind.SET_SINGLETON, two)
70 singleton_three = tm.mkTerm(Kind.SET_SINGLETON, three)
71 one_two = tm.mkTerm(Kind.SET_UNION, singleton_one, singleton_two)
72 two_three = tm.mkTerm(Kind.SET_UNION, singleton_two, singleton_three)
73 intersection = tm.mkTerm(Kind.SET_INTER, one_two, two_three)
74
75 x = tm.mkConst(integer, "x")
76
77 e = tm.mkTerm(Kind.SET_MEMBER, x, intersection)
78
79 result = slv.checkSatAssuming(e)
80
81 print("cvc5 reports: {} is {}".format(e, result))
82
83 if result:
84 print("For instance, {} is a member".format(slv.getValue(x)))
1(set-logic QF_UFLIAFS)
2(set-option :produce-models true)
3(set-option :incremental true)
4(declare-const A (Set Int))
5(declare-const B (Set Int))
6(declare-const C (Set Int))
7(declare-const x Int)
8
9; Verify union distributions over intersection
10(check-sat-assuming
11 (
12 (distinct
13 (set.inter (set.union A B) C)
14 (set.union (set.inter A C) (set.inter B C)))
15 )
16)
17
18; Verify emptset is a subset of any set
19(check-sat-assuming
20 (
21 (not (set.subset (as set.empty (Set Int)) A))
22 )
23)
24
25; Find an element in {1, 2} intersection {2, 3}, if there is one.
26(check-sat-assuming
27 (
28 (set.member
29 x
30 (set.inter
31 (set.union (set.singleton 1) (set.singleton 2))
32 (set.union (set.singleton 2) (set.singleton 3))))
33 )
34)
35
36(echo "A member: ")
37(get-value (x))