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