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 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 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 slv.setOption("output-language", "smt2");
35
36 Sort integer = tm.getIntegerSort();
37 Sort set = tm.mkSetSort(integer);
38
39 // Verify union distributions over intersection
40 // (A union B) intersection C = (A intersection C) union (B intersection C)
41 {
42 Term A = tm.mkConst(set, "A");
43 Term B = tm.mkConst(set, "B");
44 Term C = tm.mkConst(set, "C");
45
46 Term unionAB = tm.mkTerm(Kind::SET_UNION, {A, B});
47 Term lhs = tm.mkTerm(Kind::SET_INTER, {unionAB, C});
48
49 Term intersectionAC = tm.mkTerm(Kind::SET_INTER, {A, C});
50 Term intersectionBC = tm.mkTerm(Kind::SET_INTER, {B, C});
51 Term rhs = tm.mkTerm(Kind::SET_UNION, {intersectionAC, intersectionBC});
52
53 Term theorem = tm.mkTerm(Kind::EQUAL, {lhs, rhs});
54
55 cout << "cvc5 reports: " << theorem << " is "
56 << slv.checkSatAssuming(theorem.notTerm()) << "." << endl;
57 }
58
59 // Verify emptset is a subset of any set
60 {
61 Term A = tm.mkConst(set, "A");
62 Term emptyset = tm.mkEmptySet(set);
63
64 Term theorem = tm.mkTerm(Kind::SET_SUBSET, {emptyset, A});
65
66 cout << "cvc5 reports: " << theorem << " is "
67 << slv.checkSatAssuming(theorem.notTerm()) << "." << endl;
68 }
69
70 // Find me an element in {1, 2} intersection {2, 3}, if there is one.
71 {
72 Term one = tm.mkInteger(1);
73 Term two = tm.mkInteger(2);
74 Term three = tm.mkInteger(3);
75
76 Term singleton_one = tm.mkTerm(Kind::SET_SINGLETON, {one});
77 Term singleton_two = tm.mkTerm(Kind::SET_SINGLETON, {two});
78 Term singleton_three = tm.mkTerm(Kind::SET_SINGLETON, {three});
79 Term one_two = tm.mkTerm(Kind::SET_UNION, {singleton_one, singleton_two});
80 Term two_three =
81 tm.mkTerm(Kind::SET_UNION, {singleton_two, singleton_three});
82 Term intersection = tm.mkTerm(Kind::SET_INTER, {one_two, two_three});
83
84 Term x = tm.mkConst(integer, "x");
85
86 Term e = tm.mkTerm(Kind::SET_MEMBER, {x, intersection});
87
88 Result result = slv.checkSatAssuming(e);
89 cout << "cvc5 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}
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 Solver slv = new Solver();
25 {
26 // Optionally, set the logic. We need at least UF for equality predicate,
27 // integers (LIA) and sets (FS).
28 slv.setLogic("QF_UFLIAFS");
29
30 // Produce models
31 slv.setOption("produce-models", "true");
32 slv.setOption("output-language", "smt2");
33
34 Sort integer = slv.getIntegerSort();
35 Sort set = slv.mkSetSort(integer);
36
37 // Verify union distributions over intersection
38 // (A union B) intersection C = (A intersection C) union (B intersection C)
39 {
40 Term A = slv.mkConst(set, "A");
41 Term B = slv.mkConst(set, "B");
42 Term C = slv.mkConst(set, "C");
43
44 Term unionAB = slv.mkTerm(SET_UNION, A, B);
45 Term lhs = slv.mkTerm(SET_INTER, unionAB, C);
46
47 Term intersectionAC = slv.mkTerm(SET_INTER, A, C);
48 Term intersectionBC = slv.mkTerm(SET_INTER, B, C);
49 Term rhs = slv.mkTerm(SET_UNION, intersectionAC, intersectionBC);
50
51 Term theorem = slv.mkTerm(EQUAL, lhs, rhs);
52
53 System.out.println(
54 "cvc5 reports: " + theorem + " is " + slv.checkSatAssuming(theorem.notTerm()) + ".");
55 }
56
57 // Verify set.empty is a subset of any set
58 {
59 Term A = slv.mkConst(set, "A");
60 Term emptyset = slv.mkEmptySet(set);
61
62 Term theorem = slv.mkTerm(SET_SUBSET, emptyset, A);
63
64 System.out.println(
65 "cvc5 reports: " + theorem + " is " + slv.checkSatAssuming(theorem.notTerm()) + ".");
66 }
67
68 // Find me an element in {1, 2} intersection {2, 3}, if there is one.
69 {
70 Term one = slv.mkInteger(1);
71 Term two = slv.mkInteger(2);
72 Term three = slv.mkInteger(3);
73
74 Term singleton_one = slv.mkTerm(SET_SINGLETON, one);
75 Term singleton_two = slv.mkTerm(SET_SINGLETON, two);
76 Term singleton_three = slv.mkTerm(SET_SINGLETON, three);
77 Term one_two = slv.mkTerm(SET_UNION, singleton_one, singleton_two);
78 Term two_three = slv.mkTerm(SET_UNION, singleton_two, singleton_three);
79 Term intersection = slv.mkTerm(SET_INTER, one_two, two_three);
80
81 Term x = slv.mkConst(integer, "x");
82
83 Term e = slv.mkTerm(SET_MEMBER, x, intersection);
84
85 Result result = slv.checkSatAssuming(e);
86 System.out.println("cvc5 reports: " + e + " is " + result + ".");
87
88 if (result.isSat())
89 {
90 System.out.println("For instance, " + slv.getValue(x) + " is a member.");
91 }
92 }
93 }
94 Context.deletePointers();
95 }
96}
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))