Theory Reference: Sets and Relations
Finite Sets
cvc5 supports the theory of finite sets using the following sorts, constants, functions and predicates. More details can be found in [BBRT17].
For the C++ API examples in the table below, we assume that we have created a cvc5::Solver solver object.
SMTLIB language |
C++ API |
|
Logic String |
append FS for finite sets
|
append FS for finite sets
|
Sort |
|
|
Constants |
|
|
Union |
|
|
Intersection |
|
|
Minus |
|
|
Membership |
|
|
Subset |
|
|
Emptyset |
|
|
Singleton Set |
|
|
Emptyset tester |
|
|
Singleton tester |
|
|
Cardinality |
|
|
Insert / Finite Sets |
|
|
Complement |
|
|
Universe Set |
|
|
Semantics
The semantics of most of the above operators (e.g., set.union,
set.inter, difference) are straightforward.
The semantics for the universe set and complement are more subtle and explained
in the following.
The universe set (as set.universe (Set T)) is not interpreted as the set
containing all elements of sort T.
Instead it may be interpreted as any set such that all sets of sort (Set T)
are interpreted as subsets of it.
In other words, it is the union of the interpretations of all (finite) sets in
our input.
For example:
(declare-fun x () (Set Int))
(declare-fun y () (Set Int))
(declare-fun z () (Set Int))
(assert (set.member 0 x))
(assert (set.member 1 y))
(assert (= z (as set.universe (Set Int))))
(check-sat)
Here, a possible model is:
(define-fun x () (set.singleton 0))
(define-fun y () (set.singleton 1))
(define-fun z () (set.union (set.singleton 1) (set.singleton 0)))
Notice that the universe set in this example is interpreted the same as z,
and is such that all sets in this example (x, y, and z) are subsets
of it.
The set complement operator for (Set T) is interpreted relative to the
interpretation of the universe set for (Set T), and not relative to the set
of all elements of sort T.
That is, for all sets X of sort (Set T), the complement operator is
such that (= (set.complement X) (set.minus (as set.universe (Set T)) X))
holds in all models.
The motivation for these semantics is to ensure that the universe set for sort
T and applications of set complement can always be interpreted as a finite
set in (quantifier-free) inputs, even if the cardinality of T is infinite.
Above, notice that we were able to find a model for the universe set of sort
(Set Int) that contained two elements only.
Note
In the presence of quantifiers, cvc5’s implementation of the above theory allows infinite sets. In particular, the following formula is SAT (even though cvc5 is not able to say this):
(set-logic ALL)
(declare-fun x () (Set Int))
(assert (forall ((z Int) (set.member (* 2 z) x)))
(check-sat)
The reason for that is that making this formula (and similar ones) unsat is counter-intuitive when quantifiers are present.
Below is a more extensive example on how to use finite 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-2025 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, Kshitij Bansal
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2025 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, Daniel Larraz, Andres Noetzli
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2025 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}
1#!/usr/bin/env python
2###############################################################################
3# Top contributors (to current version):
4# Aina Niemetz, Makai Mann, Alex Ozdemir
5#
6# This file is part of the cvc5 project.
7#
8# Copyright (c) 2009-2025 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))
Finite Relations
cvc5 also supports the theory of finite relations, using the following sorts, constants, functions and predicates. More details can be found in [MRTB17].
SMTLIB language |
C++ API |
|
Logic String |
|
|
Tuple Sort |
|
|
|
|
|
Tuple Constructor |
|
|
Unit Tuple Sort |
|
|
Unit Tuple |
|
|
Tuple Selector |
|
|
Relation Sort |
which is a syntax sugar for
|
|
Constants |
|
|
Transpose |
|
|
Transitive Closure |
|
|
Join |
|
|
Product |
|
|
Example:
examples/api/cpp/relations.cpp
1/******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Aina Niemetz, Mathias Preiner
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2025 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 relations via the C++ API.
14 */
15
16#include <cvc5/cvc5.h>
17
18#include <iostream>
19
20using namespace cvc5;
21
22int main()
23{
24 TermManager tm;
25 Solver solver(tm);
26
27 // Set the logic
28 solver.setLogic("ALL");
29
30 // options
31 solver.setOption("produce-models", "true");
32 // we need finite model finding to answer sat problems with universal
33 // quantified formulas
34 solver.setOption("finite-model-find", "true");
35 // we need sets extension to support set.universe operator
36 solver.setOption("sets-exp", "true");
37
38 // (declare-sort Person 0)
39 Sort personSort = tm.mkUninterpretedSort("Person");
40
41 // (Tuple Person)
42 Sort tupleArity1 = tm.mkTupleSort({personSort});
43 // (Relation Person)
44 Sort relationArity1 = tm.mkSetSort(tupleArity1);
45
46 // (Tuple Person Person)
47 Sort tupleArity2 = tm.mkTupleSort({personSort, personSort});
48 // (Relation Person Person)
49 Sort relationArity2 = tm.mkSetSort(tupleArity2);
50
51 // empty set
52 Term emptySetTerm = tm.mkEmptySet(relationArity1);
53
54 // empty relation
55 Term emptyRelationTerm = tm.mkEmptySet(relationArity2);
56
57 // universe set
58 Term universeSet = tm.mkUniverseSet(relationArity1);
59
60 // variables
61 Term people = tm.mkConst(relationArity1, "people");
62 Term males = tm.mkConst(relationArity1, "males");
63 Term females = tm.mkConst(relationArity1, "females");
64 Term father = tm.mkConst(relationArity2, "father");
65 Term mother = tm.mkConst(relationArity2, "mother");
66 Term parent = tm.mkConst(relationArity2, "parent");
67 Term ancestor = tm.mkConst(relationArity2, "ancestor");
68 Term descendant = tm.mkConst(relationArity2, "descendant");
69
70 Term isEmpty1 = tm.mkTerm(Kind::EQUAL, {males, emptySetTerm});
71 Term isEmpty2 = tm.mkTerm(Kind::EQUAL, {females, emptySetTerm});
72
73 // (assert (= people (as set.universe (Relation Person))))
74 Term peopleAreTheUniverse = tm.mkTerm(Kind::EQUAL, {people, universeSet});
75 // (assert (not (= males (as set.empty (Relation Person)))))
76 Term maleSetIsNotEmpty = tm.mkTerm(Kind::NOT, {isEmpty1});
77 // (assert (not (= females (as set.empty (Relation Person)))))
78 Term femaleSetIsNotEmpty = tm.mkTerm(Kind::NOT, {isEmpty2});
79
80 // (assert (= (set.inter males females)
81 // (as set.empty (Relation Person))))
82 Term malesFemalesIntersection = tm.mkTerm(Kind::SET_INTER, {males, females});
83 Term malesAndFemalesAreDisjoint =
84 tm.mkTerm(Kind::EQUAL, {malesFemalesIntersection, emptySetTerm});
85
86 // (assert (not (= father (as set.empty (Relation Person Person)))))
87 // (assert (not (= mother (as set.empty (Relation Person Person)))))
88 Term isEmpty3 = tm.mkTerm(Kind::EQUAL, {father, emptyRelationTerm});
89 Term isEmpty4 = tm.mkTerm(Kind::EQUAL, {mother, emptyRelationTerm});
90 Term fatherIsNotEmpty = tm.mkTerm(Kind::NOT, {isEmpty3});
91 Term motherIsNotEmpty = tm.mkTerm(Kind::NOT, {isEmpty4});
92
93 // fathers are males
94 // (assert (set.subset (rel.join father people) males))
95 Term fathers = tm.mkTerm(Kind::RELATION_JOIN, {father, people});
96 Term fathersAreMales = tm.mkTerm(Kind::SET_SUBSET, {fathers, males});
97
98 // mothers are females
99 // (assert (set.subset (rel.join mother people) females))
100 Term mothers = tm.mkTerm(Kind::RELATION_JOIN, {mother, people});
101 Term mothersAreFemales = tm.mkTerm(Kind::SET_SUBSET, {mothers, females});
102
103 // (assert (= parent (set.union father mother)))
104 Term unionFatherMother = tm.mkTerm(Kind::SET_UNION, {father, mother});
105 Term parentIsFatherOrMother =
106 tm.mkTerm(Kind::EQUAL, {parent, unionFatherMother});
107
108 // (assert (= ancestor (rel.tclosure parent)))
109 Term transitiveClosure = tm.mkTerm(Kind::RELATION_TCLOSURE, {parent});
110 Term ancestorFormula = tm.mkTerm(Kind::EQUAL, {ancestor, transitiveClosure});
111
112 // (assert (= descendant (rel.transpose descendant)))
113 Term transpose = tm.mkTerm(Kind::RELATION_TRANSPOSE, {ancestor});
114 Term descendantFormula = tm.mkTerm(Kind::EQUAL, {descendant, transpose});
115
116 // (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
117 Term x = tm.mkVar(personSort, "x");
118 Term xxTuple = tm.mkTuple({x, x});
119 Term member = tm.mkTerm(Kind::SET_MEMBER, {xxTuple, ancestor});
120 Term notMember = tm.mkTerm(Kind::NOT, {member});
121
122 Term quantifiedVariables = tm.mkTerm(Kind::VARIABLE_LIST, {x});
123 Term noSelfAncestor =
124 tm.mkTerm(Kind::FORALL, {quantifiedVariables, notMember});
125
126 // formulas
127 solver.assertFormula(peopleAreTheUniverse);
128 solver.assertFormula(maleSetIsNotEmpty);
129 solver.assertFormula(femaleSetIsNotEmpty);
130 solver.assertFormula(malesAndFemalesAreDisjoint);
131 solver.assertFormula(fatherIsNotEmpty);
132 solver.assertFormula(motherIsNotEmpty);
133 solver.assertFormula(fathersAreMales);
134 solver.assertFormula(mothersAreFemales);
135 solver.assertFormula(parentIsFatherOrMother);
136 solver.assertFormula(descendantFormula);
137 solver.assertFormula(ancestorFormula);
138 solver.assertFormula(noSelfAncestor);
139
140 // check sat
141 Result result = solver.checkSat();
142
143 // output
144 std::cout << "Result = " << result << std::endl;
145 std::cout << "people = " << solver.getValue(people) << std::endl;
146 std::cout << "males = " << solver.getValue(males) << std::endl;
147 std::cout << "females = " << solver.getValue(females) << std::endl;
148 std::cout << "father = " << solver.getValue(father) << std::endl;
149 std::cout << "mother = " << solver.getValue(mother) << std::endl;
150 std::cout << "parent = " << solver.getValue(parent) << std::endl;
151 std::cout << "descendant = " << solver.getValue(descendant) << std::endl;
152 std::cout << "ancestor = " << solver.getValue(ancestor) << std::endl;
153}
1/******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz, Mudathir Mohamed, Andrew Reynolds
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2025 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 relations 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 // Set the logic
25 cvc5_set_logic(slv, "ALL");
26
27 // options
28 cvc5_set_option(slv, "produce-models", "true");
29 // we need finite model finding to answer sat problems with universal
30 // quantified formulas
31 cvc5_set_option(slv, "finite-model-find", "true");
32 // we need sets extension to support set.universe operator
33 cvc5_set_option(slv, "sets-exp", "true");
34
35 // (declare-sort Person 0)
36 Cvc5Sort person_sort = cvc5_mk_uninterpreted_sort(tm, "Person");
37
38 // (Tuple Person)
39 Cvc5Sort sorts1[1] = {person_sort};
40 Cvc5Sort tuple_arity1 = cvc5_mk_tuple_sort(tm, 1, sorts1);
41 // (Relation Person)
42 Cvc5Sort rel_arity1 = cvc5_mk_set_sort(tm, tuple_arity1);
43
44 // (Tuple Person Person)
45 Cvc5Sort sorts2[2] = {person_sort, person_sort};
46 Cvc5Sort tuple_arity2 = cvc5_mk_tuple_sort(tm, 2, sorts2);
47 // (Relation Person Person)
48 Cvc5Sort rel_arity2 = cvc5_mk_set_sort(tm, tuple_arity2);
49
50 // empty set
51 Cvc5Term empty_set = cvc5_mk_empty_set(tm, rel_arity1);
52
53 // empty relation
54 Cvc5Term empty_rel = cvc5_mk_empty_set(tm, rel_arity2);
55
56 // universe set
57 Cvc5Term universe_set = cvc5_mk_universe_set(tm, rel_arity1);
58
59 // variables
60 Cvc5Term people = cvc5_mk_const(tm, rel_arity1, "people");
61 Cvc5Term males = cvc5_mk_const(tm, rel_arity1, "males");
62 Cvc5Term females = cvc5_mk_const(tm, rel_arity1, "females");
63 Cvc5Term father = cvc5_mk_const(tm, rel_arity2, "father");
64 Cvc5Term mother = cvc5_mk_const(tm, rel_arity2, "mother");
65 Cvc5Term parent = cvc5_mk_const(tm, rel_arity2, "parent");
66 Cvc5Term ancestor = cvc5_mk_const(tm, rel_arity2, "ancestor");
67 Cvc5Term descendant = cvc5_mk_const(tm, rel_arity2, "descendant");
68
69 Cvc5Term args2[2] = {males, empty_set};
70 Cvc5Term is_empty1 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
71 args2[0] = females;
72 Cvc5Term is_empty2 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
73
74 // (assert (= people (as set.universe (Relation Person))))
75 args2[0] = people;
76 args2[1] = universe_set;
77 Cvc5Term people_universe = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
78 // (assert (not (= males (as set.empty (Relation Person)))))
79 Cvc5Term args1[1] = {is_empty1};
80 Cvc5Term male_not_empty = cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args1);
81 // (assert (not (= females (as set.empty (Relation Person)))))
82 args1[0] = is_empty2;
83 Cvc5Term female_not_empty = cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args1);
84
85 // (assert (= (set.inter males females)
86 // (as set.empty (Relation Person))))
87 args2[0] = males;
88 args2[1] = females;
89 Cvc5Term inter_males_females =
90 cvc5_mk_term(tm, CVC5_KIND_SET_INTER, 2, args2);
91 args2[0] = inter_males_females;
92 args2[1] = empty_set;
93 Cvc5Term disjoint_males_females = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
94
95 // (assert (not (= father (as set.empty (Relation Person Person)))))
96 // (assert (not (= mother (as set.empty (Relation Person Person)))))
97 args2[0] = father;
98 args2[1] = empty_rel;
99 Cvc5Term is_empty3 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
100 args2[0] = mother;
101 args2[1] = empty_rel;
102 Cvc5Term is_empty4 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
103 args1[0] = is_empty3;
104 Cvc5Term father_not_empty = cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args1);
105 args1[0] = is_empty4;
106 Cvc5Term mother_not_empty = cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args1);
107
108 // fathers are males
109 // (assert (set.subset (rel.join father people) males))
110 args2[0] = father;
111 args2[1] = people;
112 Cvc5Term fathers = cvc5_mk_term(tm, CVC5_KIND_RELATION_JOIN, 2, args2);
113 args2[0] = fathers;
114 args2[1] = males;
115 Cvc5Term fathers_are_males = cvc5_mk_term(tm, CVC5_KIND_SET_SUBSET, 2, args2);
116
117 // mothers are females
118 // (assert (set.subset (rel.join mother people) females))
119 args2[0] = mother;
120 args2[1] = people;
121 Cvc5Term mothers = cvc5_mk_term(tm, CVC5_KIND_RELATION_JOIN, 2, args2);
122 args2[0] = mothers;
123 args2[1] = females;
124 Cvc5Term mothers_are_females =
125 cvc5_mk_term(tm, CVC5_KIND_SET_SUBSET, 2, args2);
126
127 // (assert (= parent (set.union father mother)))
128 args2[0] = father;
129 args2[1] = mother;
130 Cvc5Term union_father_mother =
131 cvc5_mk_term(tm, CVC5_KIND_SET_UNION, 2, args2);
132 args2[0] = parent;
133 args2[1] = union_father_mother;
134 Cvc5Term parent_is_father_or_mother =
135 cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
136
137 // (assert (= ancestor (rel.tclosure parent)))
138 args1[0] = parent;
139 Cvc5Term trans_closure =
140 cvc5_mk_term(tm, CVC5_KIND_RELATION_TCLOSURE, 1, args1);
141 args2[0] = ancestor;
142 args2[1] = trans_closure;
143 Cvc5Term ancestor_formula = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
144
145 // (assert (= descendant (rel.transpose descendant)))
146 args1[0] = ancestor;
147 Cvc5Term transpose = cvc5_mk_term(tm, CVC5_KIND_RELATION_TRANSPOSE, 1, args1);
148 args2[0] = descendant;
149 args2[1] = transpose;
150 Cvc5Term descendant_formula = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
151
152 // (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
153 Cvc5Term x = cvc5_mk_var(tm, person_sort, "x");
154 args2[0] = x;
155 args2[1] = x;
156 Cvc5Term xx_tuple = cvc5_mk_tuple(tm, 2, args2);
157 args2[0] = xx_tuple;
158 args2[1] = ancestor;
159 Cvc5Term member = cvc5_mk_term(tm, CVC5_KIND_SET_MEMBER, 2, args2);
160 args1[0] = member;
161 Cvc5Term not_member = cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args1);
162
163 args1[0] = x;
164 Cvc5Term vars = cvc5_mk_term(tm, CVC5_KIND_VARIABLE_LIST, 1, args1);
165 args2[0] = vars;
166 args2[1] = not_member;
167 Cvc5Term not_self_ancestor = cvc5_mk_term(tm, CVC5_KIND_FORALL, 2, args2);
168
169 // formulas
170 cvc5_assert_formula(slv, people_universe);
171 cvc5_assert_formula(slv, male_not_empty);
172 cvc5_assert_formula(slv, female_not_empty);
173 cvc5_assert_formula(slv, disjoint_males_females);
174 cvc5_assert_formula(slv, father_not_empty);
175 cvc5_assert_formula(slv, mother_not_empty);
176 cvc5_assert_formula(slv, fathers_are_males);
177 cvc5_assert_formula(slv, mothers_are_females);
178 cvc5_assert_formula(slv, parent_is_father_or_mother);
179 cvc5_assert_formula(slv, descendant_formula);
180 cvc5_assert_formula(slv, ancestor_formula);
181 cvc5_assert_formula(slv, not_self_ancestor);
182
183 // check sat
184 Cvc5Result result = cvc5_check_sat(slv);
185
186 // output
187 printf("Result = %s\n", cvc5_result_to_string(result));
188 printf("people = %s\n", cvc5_term_to_string(cvc5_get_value(slv, people)));
189 printf("males = %s\n", cvc5_term_to_string(cvc5_get_value(slv, males)));
190 printf("females = %s\n",
191 cvc5_term_to_string(cvc5_get_value(slv, females)));
192 printf("father = %s\n", cvc5_term_to_string(cvc5_get_value(slv, father)));
193 printf("mother = %s\n", cvc5_term_to_string(cvc5_get_value(slv, mother)));
194 printf("parent = %s\n", cvc5_term_to_string(cvc5_get_value(slv, parent)));
195 printf("descendant = %s\n",
196 cvc5_term_to_string(cvc5_get_value(slv, descendant)));
197 printf("ancestor = %s\n",
198 cvc5_term_to_string(cvc5_get_value(slv, ancestor)));
199
200 cvc5_delete(slv);
201 cvc5_term_manager_delete(tm);
202}
examples/api/java/Relations.java
1/******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Daniel Larraz, Andres Noetzli
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2025 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 relations with cvc5 via Java API.
14 */
15
16import static io.github.cvc5.Kind.*;
17
18import io.github.cvc5.*;
19
20public class Relations
21{
22 public static void main(String[] args) throws CVC5ApiException
23 {
24 TermManager tm = new TermManager();
25 Solver solver = new Solver(tm);
26 {
27 // Set the logic
28 solver.setLogic("ALL");
29
30 // options
31 solver.setOption("produce-models", "true");
32 // we need finite model finding to answer sat problems with universal
33 // quantified formulas
34 solver.setOption("finite-model-find", "true");
35 // we need sets extension to support set.universe operator
36 solver.setOption("sets-exp", "true");
37
38 // (declare-sort Person 0)
39 Sort personSort = tm.mkUninterpretedSort("Person");
40
41 // (Tuple Person)
42 Sort tupleArity1 = tm.mkTupleSort(new Sort[] {personSort});
43 // (Relation Person)
44 Sort relationArity1 = tm.mkSetSort(tupleArity1);
45
46 // (Tuple Person Person)
47 Sort tupleArity2 = tm.mkTupleSort(new Sort[] {personSort, personSort});
48 // (Relation Person Person)
49 Sort relationArity2 = tm.mkSetSort(tupleArity2);
50
51 // empty set
52 Term emptySetTerm = tm.mkEmptySet(relationArity1);
53
54 // empty relation
55 Term emptyRelationTerm = tm.mkEmptySet(relationArity2);
56
57 // universe set
58 Term universeSet = tm.mkUniverseSet(relationArity1);
59
60 // variables
61 Term people = tm.mkConst(relationArity1, "people");
62 Term males = tm.mkConst(relationArity1, "males");
63 Term females = tm.mkConst(relationArity1, "females");
64 Term father = tm.mkConst(relationArity2, "father");
65 Term mother = tm.mkConst(relationArity2, "mother");
66 Term parent = tm.mkConst(relationArity2, "parent");
67 Term ancestor = tm.mkConst(relationArity2, "ancestor");
68 Term descendant = tm.mkConst(relationArity2, "descendant");
69
70 Term isEmpty1 = tm.mkTerm(EQUAL, males, emptySetTerm);
71 Term isEmpty2 = tm.mkTerm(EQUAL, females, emptySetTerm);
72
73 // (assert (= people (as set.universe (Relation Person))))
74 Term peopleAreTheUniverse = tm.mkTerm(EQUAL, people, universeSet);
75 // (assert (not (= males (as set.empty (Relation Person)))))
76 Term maleSetIsNotEmpty = tm.mkTerm(NOT, isEmpty1);
77 // (assert (not (= females (as set.empty (Relation Person)))))
78 Term femaleSetIsNotEmpty = tm.mkTerm(NOT, isEmpty2);
79
80 // (assert (= (set.inter males females)
81 // (as set.empty (Relation Person))))
82 Term malesFemalesIntersection = tm.mkTerm(SET_INTER, males, females);
83 Term malesAndFemalesAreDisjoint = tm.mkTerm(EQUAL, malesFemalesIntersection, emptySetTerm);
84
85 // (assert (not (= father (as set.empty (Relation Person Person)))))
86 // (assert (not (= mother (as set.empty (Relation Person Person)))))
87 Term isEmpty3 = tm.mkTerm(EQUAL, father, emptyRelationTerm);
88 Term isEmpty4 = tm.mkTerm(EQUAL, mother, emptyRelationTerm);
89 Term fatherIsNotEmpty = tm.mkTerm(NOT, isEmpty3);
90 Term motherIsNotEmpty = tm.mkTerm(NOT, isEmpty4);
91
92 // fathers are males
93 // (assert (set.subset (rel.join father people) males))
94 Term fathers = tm.mkTerm(RELATION_JOIN, father, people);
95 Term fathersAreMales = tm.mkTerm(SET_SUBSET, fathers, males);
96
97 // mothers are females
98 // (assert (set.subset (rel.join mother people) females))
99 Term mothers = tm.mkTerm(RELATION_JOIN, mother, people);
100 Term mothersAreFemales = tm.mkTerm(SET_SUBSET, mothers, females);
101
102 // (assert (= parent (set.union father mother)))
103 Term unionFatherMother = tm.mkTerm(SET_UNION, father, mother);
104 Term parentIsFatherOrMother = tm.mkTerm(EQUAL, parent, unionFatherMother);
105
106 // (assert (= ancestor (rel.tclosure parent)))
107 Term transitiveClosure = tm.mkTerm(RELATION_TCLOSURE, parent);
108 Term ancestorFormula = tm.mkTerm(EQUAL, ancestor, transitiveClosure);
109
110 // (assert (= descendant (rel.transpose ancestor)))
111 Term transpose = tm.mkTerm(RELATION_TRANSPOSE, ancestor);
112 Term descendantFormula = tm.mkTerm(EQUAL, descendant, transpose);
113
114 // (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
115 Term x = tm.mkVar(personSort, "x");
116 Term xxTuple = tm.mkTuple(new Term[] {x, x});
117 Term member = tm.mkTerm(SET_MEMBER, xxTuple, ancestor);
118 Term notMember = tm.mkTerm(NOT, member);
119
120 Term quantifiedVariables = tm.mkTerm(VARIABLE_LIST, x);
121 Term noSelfAncestor = tm.mkTerm(FORALL, quantifiedVariables, notMember);
122
123 // formulas
124 solver.assertFormula(peopleAreTheUniverse);
125 solver.assertFormula(maleSetIsNotEmpty);
126 solver.assertFormula(femaleSetIsNotEmpty);
127 solver.assertFormula(malesAndFemalesAreDisjoint);
128 solver.assertFormula(fatherIsNotEmpty);
129 solver.assertFormula(motherIsNotEmpty);
130 solver.assertFormula(fathersAreMales);
131 solver.assertFormula(mothersAreFemales);
132 solver.assertFormula(parentIsFatherOrMother);
133 solver.assertFormula(descendantFormula);
134 solver.assertFormula(ancestorFormula);
135 solver.assertFormula(noSelfAncestor);
136
137 // check sat
138 Result result = solver.checkSat();
139
140 // output
141 System.out.println("Result = " + result);
142 System.out.println("people = " + solver.getValue(people));
143 System.out.println("males = " + solver.getValue(males));
144 System.out.println("females = " + solver.getValue(females));
145 System.out.println("father = " + solver.getValue(father));
146 System.out.println("mother = " + solver.getValue(mother));
147 System.out.println("parent = " + solver.getValue(parent));
148 System.out.println("descendant = " + solver.getValue(descendant));
149 System.out.println("ancestor = " + solver.getValue(ancestor));
150 }
151 Context.deletePointers();
152 }
153}
examples/api/python/relations.py
1#!/usr/bin/env python
2###############################################################################
3# Top contributors (to current version):
4# Mudathir Mohamed, Aina Niemetz, Makai Mann
5#
6# This file is part of the cvc5 project.
7#
8# Copyright (c) 2009-2025 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 relations solver
15# through the Python API. This is a direct translation of relations.cpp.
16##
17
18import cvc5
19from cvc5 import Kind
20
21if __name__ == "__main__":
22 tm = cvc5.TermManager()
23 solver = cvc5.Solver(tm)
24
25 # Set the logic
26 solver.setLogic("ALL")
27
28 # options
29 solver.setOption("produce-models", "true")
30 # we need finite model finding to answer sat problems with universal
31 # quantified formulas
32 solver.setOption("finite-model-find", "true")
33 # we need sets extension to support set.universe operator
34 solver.setOption("sets-exp", "true")
35
36 integer = tm.getIntegerSort()
37 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 # (declare-sort Person 0)
43 personSort = tm.mkUninterpretedSort("Person")
44
45 # (Tuple Person)
46 tupleArity1 = tm.mkTupleSort(personSort)
47 # (Relation Person)
48 relationArity1 = tm.mkSetSort(tupleArity1)
49
50 # (Tuple Person Person)
51 tupleArity2 = tm.mkTupleSort(personSort, personSort)
52 # (Relation Person Person)
53 relationArity2 = tm.mkSetSort(tupleArity2)
54
55 # empty set
56 emptySetTerm = tm.mkEmptySet(relationArity1)
57
58 # empty relation
59 emptyRelationTerm = tm.mkEmptySet(relationArity2)
60
61 # universe set
62 universeSet = tm.mkUniverseSet(relationArity1)
63
64 # variables
65 people = tm.mkConst(relationArity1, "people")
66 males = tm.mkConst(relationArity1, "males")
67 females = tm.mkConst(relationArity1, "females")
68 father = tm.mkConst(relationArity2, "father")
69 mother = tm.mkConst(relationArity2, "mother")
70 parent = tm.mkConst(relationArity2, "parent")
71 ancestor = tm.mkConst(relationArity2, "ancestor")
72 descendant = tm.mkConst(relationArity2, "descendant")
73
74 isEmpty1 = tm.mkTerm(Kind.EQUAL, males, emptySetTerm)
75 isEmpty2 = tm.mkTerm(Kind.EQUAL, females, emptySetTerm)
76
77 # (assert (= people (as set.universe (Relation Person))))
78 peopleAreTheUniverse = tm.mkTerm(Kind.EQUAL, people, universeSet)
79 # (assert (not (= males (as set.empty (Relation Person)))))
80 maleSetIsNotEmpty = tm.mkTerm(Kind.NOT, isEmpty1)
81 # (assert (not (= females (as set.empty (Relation Person)))))
82 femaleSetIsNotEmpty = tm.mkTerm(Kind.NOT, isEmpty2)
83
84 # (assert (= (set.inter males females)
85 # (as set.empty (Relation Person))))
86 malesFemalesIntersection = tm.mkTerm(Kind.SET_INTER, males, females)
87 malesAndFemalesAreDisjoint = \
88 tm.mkTerm(Kind.EQUAL, malesFemalesIntersection, emptySetTerm)
89
90 # (assert (not (= father (as set.empty (Relation Person Person)))))
91 # (assert (not (= mother (as set.empty (Relation Person Person)))))
92 isEmpty3 = tm.mkTerm(Kind.EQUAL, father, emptyRelationTerm)
93 isEmpty4 = tm.mkTerm(Kind.EQUAL, mother, emptyRelationTerm)
94 fatherIsNotEmpty = tm.mkTerm(Kind.NOT, isEmpty3)
95 motherIsNotEmpty = tm.mkTerm(Kind.NOT, isEmpty4)
96
97 # fathers are males
98 # (assert (set.subset (rel.join father people) males))
99 fathers = tm.mkTerm(Kind.RELATION_JOIN, father, people)
100 fathersAreMales = tm.mkTerm(Kind.SET_SUBSET, fathers, males)
101
102 # mothers are females
103 # (assert (set.subset (rel.join mother people) females))
104 mothers = tm.mkTerm(Kind.RELATION_JOIN, mother, people)
105 mothersAreFemales = tm.mkTerm(Kind.SET_SUBSET, mothers, females)
106
107 # (assert (= parent (set.union father mother)))
108 unionFatherMother = tm.mkTerm(Kind.SET_UNION, father, mother)
109 parentIsFatherOrMother = \
110 tm.mkTerm(Kind.EQUAL, parent, unionFatherMother)
111
112 # (assert (= ancestor (rel.tclosure parent)))
113 transitiveClosure = tm.mkTerm(Kind.RELATION_TCLOSURE, parent)
114 ancestorFormula = tm.mkTerm(Kind.EQUAL, ancestor, transitiveClosure)
115
116 # (assert (= descendant (rel.transpose ancestor)))
117 transpose = tm.mkTerm(Kind.RELATION_TRANSPOSE, ancestor)
118 descendantFormula = tm.mkTerm(Kind.EQUAL, descendant, transpose)
119
120 # (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
121 x = tm.mkVar(personSort, "x")
122 xxTuple = tm.mkTuple([x, x])
123 member = tm.mkTerm(Kind.SET_MEMBER, xxTuple, ancestor)
124 notMember = tm.mkTerm(Kind.NOT, member)
125
126 quantifiedVariables = tm.mkTerm(Kind.VARIABLE_LIST, x)
127 noSelfAncestor = tm.mkTerm(Kind.FORALL, quantifiedVariables, notMember)
128
129 # formulas
130 solver.assertFormula(peopleAreTheUniverse)
131 solver.assertFormula(maleSetIsNotEmpty)
132 solver.assertFormula(femaleSetIsNotEmpty)
133 solver.assertFormula(malesAndFemalesAreDisjoint)
134 solver.assertFormula(fatherIsNotEmpty)
135 solver.assertFormula(motherIsNotEmpty)
136 solver.assertFormula(fathersAreMales)
137 solver.assertFormula(mothersAreFemales)
138 solver.assertFormula(parentIsFatherOrMother)
139 solver.assertFormula(descendantFormula)
140 solver.assertFormula(ancestorFormula)
141 solver.assertFormula(noSelfAncestor)
142
143 # check sat
144 result = solver.checkSat()
145
146 # output
147 print("Result = {}".format(result))
148 print("people = {}".format(solver.getValue(people)))
149 print("males = {}".format(solver.getValue(males)))
150 print("females = {}".format(solver.getValue(females)))
151 print("father = {}".format(solver.getValue(father)))
152 print("mother = {}".format(solver.getValue(mother)))
153 print("parent = {}".format(solver.getValue(parent)))
154 print("descendant = {}".format(solver.getValue(descendant)))
155 print("ancestor = {}".format(solver.getValue(ancestor)))
examples/api/smtlib/relations.smt2
1(set-logic ALL)
2
3(set-option :produce-models true)
4; we need finite model finding to answer sat problems with universal
5; quantified formulas
6(set-option :finite-model-find true)
7; we need sets extension to support set.universe operator
8(set-option :sets-exp true)
9
10(declare-sort Person 0)
11
12(declare-fun people () (Relation Person))
13(declare-fun males () (Relation Person))
14(declare-fun females () (Relation Person))
15(declare-fun father () (Relation Person Person))
16(declare-fun mother () (Relation Person Person))
17(declare-fun parent () (Relation Person Person))
18(declare-fun ancestor () (Relation Person Person))
19(declare-fun descendant () (Relation Person Person))
20
21(assert (= people (as set.universe (Relation Person))))
22(assert (not (= males (as set.empty (Relation Person)))))
23(assert (not (= females (as set.empty (Relation Person)))))
24(assert (= (set.inter males females) (as set.empty (Relation Person))))
25
26; father relation is not empty
27(assert (not (= father (as set.empty (Relation Person Person)))))
28; mother relation is not empty
29(assert (not (= mother (as set.empty (Relation Person Person)))))
30; fathers are males
31(assert (set.subset (rel.join father people) males))
32; mothers are females
33(assert (set.subset (rel.join mother people) females))
34; parent
35(assert (= parent (set.union father mother)))
36; no self ancestor
37(assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
38; ancestor
39(assert (= ancestor (rel.tclosure parent)))
40; ancestor
41(assert (= descendant (rel.transpose ancestor)))
42
43(check-sat)
44(get-model)