Theory of Sets
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}
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-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
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 }
95}
examples/api/python/pythonic/sets.py
1from cvc5.pythonic import *
2
3if __name__ == "__main__":
4 A, B, C = [Set(name, IntSort()) for name in "ABC"]
5
6 # holds
7 prove((A | B) & C == (A & C) | (B & C))
8
9 # holds
10 prove(IsSubset(EmptySet(IntSort()), A))
11
12 # x must be 2.
13 x = Int("x")
14 solve(
15 IsMember(
16 x,
17 (Singleton(IntVal(1)) | Singleton(IntVal(2)))
18 & (Singleton(IntVal(2)) | Singleton(IntVal(3))),
19 )
20 )
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-2022 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 slv = cvc5.Solver()
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 integer = slv.getIntegerSort()
33 set_ = slv.mkSetSort(integer)
34
35 # Verify union distributions over intersection
36 # (A union B) intersection C = (A intersection C) union (B intersection C)
37
38 A = slv.mkConst(set_, "A")
39 B = slv.mkConst(set_, "B")
40 C = slv.mkConst(set_, "C")
41
42 unionAB = slv.mkTerm(Kind.SET_UNION, A, B)
43 lhs = slv.mkTerm(Kind.SET_INTER, unionAB, C)
44
45 intersectionAC = slv.mkTerm(Kind.SET_INTER, A, C)
46 intersectionBC = slv.mkTerm(Kind.SET_INTER, B, C)
47 rhs = slv.mkTerm(Kind.SET_UNION, intersectionAC, intersectionBC)
48
49 theorem = slv.mkTerm(Kind.EQUAL, lhs, rhs)
50
51 print("cvc5 reports: {} is {}".format(
52 theorem.notTerm(), slv.checkSatAssuming(theorem.notTerm())))
53
54 # Verify emptset is a subset of any set
55
56 A = slv.mkConst(set_, "A")
57 emptyset = slv.mkEmptySet(set_)
58
59 theorem = slv.mkTerm(Kind.SET_SUBSET, emptyset, A)
60
61 print("cvc5 reports: {} is {}".format(
62 theorem.notTerm(), slv.checkSatAssuming(theorem.notTerm())))
63
64 # Find me an element in 1, 2 intersection 2, 3, if there is one.
65
66 one = slv.mkInteger(1)
67 two = slv.mkInteger(2)
68 three = slv.mkInteger(3)
69
70 singleton_one = slv.mkTerm(Kind.SET_SINGLETON, one)
71 singleton_two = slv.mkTerm(Kind.SET_SINGLETON, two)
72 singleton_three = slv.mkTerm(Kind.SET_SINGLETON, three)
73 one_two = slv.mkTerm(Kind.SET_UNION, singleton_one, singleton_two)
74 two_three = slv.mkTerm(Kind.SET_UNION, singleton_two, singleton_three)
75 intersection = slv.mkTerm(Kind.SET_INTER, one_two, two_three)
76
77 x = slv.mkConst(integer, "x")
78
79 e = slv.mkTerm(Kind.SET_MEMBER, x, intersection)
80
81 result = slv.checkSatAssuming(e)
82
83 print("cvc5 reports: {} is {}".format(e, result))
84
85 if result:
86 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))