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 * 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}
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))
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 * 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 relations via the C++ API.
11 */
12
13#include <cvc5/cvc5.h>
14
15#include <iostream>
16
17using namespace cvc5;
18
19int main()
20{
21 TermManager tm;
22 Solver solver(tm);
23
24 // Set the logic
25 solver.setLogic("ALL");
26
27 // options
28 solver.setOption("produce-models", "true");
29 // we need finite model finding to answer sat problems with universal
30 // quantified formulas
31 solver.setOption("finite-model-find", "true");
32 // we need sets extension to support set.universe operator
33 solver.setOption("sets-exp", "true");
34
35 // (declare-sort Person 0)
36 Sort personSort = tm.mkUninterpretedSort("Person");
37
38 // (Tuple Person)
39 Sort tupleArity1 = tm.mkTupleSort({personSort});
40 // (Relation Person)
41 Sort relationArity1 = tm.mkSetSort(tupleArity1);
42
43 // (Tuple Person Person)
44 Sort tupleArity2 = tm.mkTupleSort({personSort, personSort});
45 // (Relation Person Person)
46 Sort relationArity2 = tm.mkSetSort(tupleArity2);
47
48 // empty set
49 Term emptySetTerm = tm.mkEmptySet(relationArity1);
50
51 // empty relation
52 Term emptyRelationTerm = tm.mkEmptySet(relationArity2);
53
54 // universe set
55 Term universeSet = tm.mkUniverseSet(relationArity1);
56
57 // variables
58 Term people = tm.mkConst(relationArity1, "people");
59 Term males = tm.mkConst(relationArity1, "males");
60 Term females = tm.mkConst(relationArity1, "females");
61 Term father = tm.mkConst(relationArity2, "father");
62 Term mother = tm.mkConst(relationArity2, "mother");
63 Term parent = tm.mkConst(relationArity2, "parent");
64 Term ancestor = tm.mkConst(relationArity2, "ancestor");
65 Term descendant = tm.mkConst(relationArity2, "descendant");
66
67 Term isEmpty1 = tm.mkTerm(Kind::EQUAL, {males, emptySetTerm});
68 Term isEmpty2 = tm.mkTerm(Kind::EQUAL, {females, emptySetTerm});
69
70 // (assert (= people (as set.universe (Relation Person))))
71 Term peopleAreTheUniverse = tm.mkTerm(Kind::EQUAL, {people, universeSet});
72 // (assert (not (= males (as set.empty (Relation Person)))))
73 Term maleSetIsNotEmpty = tm.mkTerm(Kind::NOT, {isEmpty1});
74 // (assert (not (= females (as set.empty (Relation Person)))))
75 Term femaleSetIsNotEmpty = tm.mkTerm(Kind::NOT, {isEmpty2});
76
77 // (assert (= (set.inter males females)
78 // (as set.empty (Relation Person))))
79 Term malesFemalesIntersection = tm.mkTerm(Kind::SET_INTER, {males, females});
80 Term malesAndFemalesAreDisjoint =
81 tm.mkTerm(Kind::EQUAL, {malesFemalesIntersection, emptySetTerm});
82
83 // (assert (not (= father (as set.empty (Relation Person Person)))))
84 // (assert (not (= mother (as set.empty (Relation Person Person)))))
85 Term isEmpty3 = tm.mkTerm(Kind::EQUAL, {father, emptyRelationTerm});
86 Term isEmpty4 = tm.mkTerm(Kind::EQUAL, {mother, emptyRelationTerm});
87 Term fatherIsNotEmpty = tm.mkTerm(Kind::NOT, {isEmpty3});
88 Term motherIsNotEmpty = tm.mkTerm(Kind::NOT, {isEmpty4});
89
90 // fathers are males
91 // (assert (set.subset (rel.join father people) males))
92 Term fathers = tm.mkTerm(Kind::RELATION_JOIN, {father, people});
93 Term fathersAreMales = tm.mkTerm(Kind::SET_SUBSET, {fathers, males});
94
95 // mothers are females
96 // (assert (set.subset (rel.join mother people) females))
97 Term mothers = tm.mkTerm(Kind::RELATION_JOIN, {mother, people});
98 Term mothersAreFemales = tm.mkTerm(Kind::SET_SUBSET, {mothers, females});
99
100 // (assert (= parent (set.union father mother)))
101 Term unionFatherMother = tm.mkTerm(Kind::SET_UNION, {father, mother});
102 Term parentIsFatherOrMother =
103 tm.mkTerm(Kind::EQUAL, {parent, unionFatherMother});
104
105 // (assert (= ancestor (rel.tclosure parent)))
106 Term transitiveClosure = tm.mkTerm(Kind::RELATION_TCLOSURE, {parent});
107 Term ancestorFormula = tm.mkTerm(Kind::EQUAL, {ancestor, transitiveClosure});
108
109 // (assert (= descendant (rel.transpose descendant)))
110 Term transpose = tm.mkTerm(Kind::RELATION_TRANSPOSE, {ancestor});
111 Term descendantFormula = tm.mkTerm(Kind::EQUAL, {descendant, transpose});
112
113 // (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
114 Term x = tm.mkVar(personSort, "x");
115 Term xxTuple = tm.mkTuple({x, x});
116 Term member = tm.mkTerm(Kind::SET_MEMBER, {xxTuple, ancestor});
117 Term notMember = tm.mkTerm(Kind::NOT, {member});
118
119 Term quantifiedVariables = tm.mkTerm(Kind::VARIABLE_LIST, {x});
120 Term noSelfAncestor =
121 tm.mkTerm(Kind::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 std::cout << "Result = " << result << std::endl;
142 std::cout << "people = " << solver.getValue(people) << std::endl;
143 std::cout << "males = " << solver.getValue(males) << std::endl;
144 std::cout << "females = " << solver.getValue(females) << std::endl;
145 std::cout << "father = " << solver.getValue(father) << std::endl;
146 std::cout << "mother = " << solver.getValue(mother) << std::endl;
147 std::cout << "parent = " << solver.getValue(parent) << std::endl;
148 std::cout << "descendant = " << solver.getValue(descendant) << std::endl;
149 std::cout << "ancestor = " << solver.getValue(ancestor) << std::endl;
150}
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 relations 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 // Set the logic
22 cvc5_set_logic(slv, "ALL");
23
24 // options
25 cvc5_set_option(slv, "produce-models", "true");
26 // we need finite model finding to answer sat problems with universal
27 // quantified formulas
28 cvc5_set_option(slv, "finite-model-find", "true");
29 // we need sets extension to support set.universe operator
30 cvc5_set_option(slv, "sets-exp", "true");
31
32 // (declare-sort Person 0)
33 Cvc5Sort person_sort = cvc5_mk_uninterpreted_sort(tm, "Person");
34
35 // (Tuple Person)
36 Cvc5Sort sorts1[1] = {person_sort};
37 Cvc5Sort tuple_arity1 = cvc5_mk_tuple_sort(tm, 1, sorts1);
38 // (Relation Person)
39 Cvc5Sort rel_arity1 = cvc5_mk_set_sort(tm, tuple_arity1);
40
41 // (Tuple Person Person)
42 Cvc5Sort sorts2[2] = {person_sort, person_sort};
43 Cvc5Sort tuple_arity2 = cvc5_mk_tuple_sort(tm, 2, sorts2);
44 // (Relation Person Person)
45 Cvc5Sort rel_arity2 = cvc5_mk_set_sort(tm, tuple_arity2);
46
47 // empty set
48 Cvc5Term empty_set = cvc5_mk_empty_set(tm, rel_arity1);
49
50 // empty relation
51 Cvc5Term empty_rel = cvc5_mk_empty_set(tm, rel_arity2);
52
53 // universe set
54 Cvc5Term universe_set = cvc5_mk_universe_set(tm, rel_arity1);
55
56 // variables
57 Cvc5Term people = cvc5_mk_const(tm, rel_arity1, "people");
58 Cvc5Term males = cvc5_mk_const(tm, rel_arity1, "males");
59 Cvc5Term females = cvc5_mk_const(tm, rel_arity1, "females");
60 Cvc5Term father = cvc5_mk_const(tm, rel_arity2, "father");
61 Cvc5Term mother = cvc5_mk_const(tm, rel_arity2, "mother");
62 Cvc5Term parent = cvc5_mk_const(tm, rel_arity2, "parent");
63 Cvc5Term ancestor = cvc5_mk_const(tm, rel_arity2, "ancestor");
64 Cvc5Term descendant = cvc5_mk_const(tm, rel_arity2, "descendant");
65
66 Cvc5Term args2[2] = {males, empty_set};
67 Cvc5Term is_empty1 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
68 args2[0] = females;
69 Cvc5Term is_empty2 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
70
71 // (assert (= people (as set.universe (Relation Person))))
72 args2[0] = people;
73 args2[1] = universe_set;
74 Cvc5Term people_universe = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
75 // (assert (not (= males (as set.empty (Relation Person)))))
76 Cvc5Term args1[1] = {is_empty1};
77 Cvc5Term male_not_empty = cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args1);
78 // (assert (not (= females (as set.empty (Relation Person)))))
79 args1[0] = is_empty2;
80 Cvc5Term female_not_empty = cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args1);
81
82 // (assert (= (set.inter males females)
83 // (as set.empty (Relation Person))))
84 args2[0] = males;
85 args2[1] = females;
86 Cvc5Term inter_males_females =
87 cvc5_mk_term(tm, CVC5_KIND_SET_INTER, 2, args2);
88 args2[0] = inter_males_females;
89 args2[1] = empty_set;
90 Cvc5Term disjoint_males_females = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
91
92 // (assert (not (= father (as set.empty (Relation Person Person)))))
93 // (assert (not (= mother (as set.empty (Relation Person Person)))))
94 args2[0] = father;
95 args2[1] = empty_rel;
96 Cvc5Term is_empty3 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
97 args2[0] = mother;
98 args2[1] = empty_rel;
99 Cvc5Term is_empty4 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
100 args1[0] = is_empty3;
101 Cvc5Term father_not_empty = cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args1);
102 args1[0] = is_empty4;
103 Cvc5Term mother_not_empty = cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args1);
104
105 // fathers are males
106 // (assert (set.subset (rel.join father people) males))
107 args2[0] = father;
108 args2[1] = people;
109 Cvc5Term fathers = cvc5_mk_term(tm, CVC5_KIND_RELATION_JOIN, 2, args2);
110 args2[0] = fathers;
111 args2[1] = males;
112 Cvc5Term fathers_are_males = cvc5_mk_term(tm, CVC5_KIND_SET_SUBSET, 2, args2);
113
114 // mothers are females
115 // (assert (set.subset (rel.join mother people) females))
116 args2[0] = mother;
117 args2[1] = people;
118 Cvc5Term mothers = cvc5_mk_term(tm, CVC5_KIND_RELATION_JOIN, 2, args2);
119 args2[0] = mothers;
120 args2[1] = females;
121 Cvc5Term mothers_are_females =
122 cvc5_mk_term(tm, CVC5_KIND_SET_SUBSET, 2, args2);
123
124 // (assert (= parent (set.union father mother)))
125 args2[0] = father;
126 args2[1] = mother;
127 Cvc5Term union_father_mother =
128 cvc5_mk_term(tm, CVC5_KIND_SET_UNION, 2, args2);
129 args2[0] = parent;
130 args2[1] = union_father_mother;
131 Cvc5Term parent_is_father_or_mother =
132 cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
133
134 // (assert (= ancestor (rel.tclosure parent)))
135 args1[0] = parent;
136 Cvc5Term trans_closure =
137 cvc5_mk_term(tm, CVC5_KIND_RELATION_TCLOSURE, 1, args1);
138 args2[0] = ancestor;
139 args2[1] = trans_closure;
140 Cvc5Term ancestor_formula = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
141
142 // (assert (= descendant (rel.transpose descendant)))
143 args1[0] = ancestor;
144 Cvc5Term transpose = cvc5_mk_term(tm, CVC5_KIND_RELATION_TRANSPOSE, 1, args1);
145 args2[0] = descendant;
146 args2[1] = transpose;
147 Cvc5Term descendant_formula = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
148
149 // (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
150 Cvc5Term x = cvc5_mk_var(tm, person_sort, "x");
151 args2[0] = x;
152 args2[1] = x;
153 Cvc5Term xx_tuple = cvc5_mk_tuple(tm, 2, args2);
154 args2[0] = xx_tuple;
155 args2[1] = ancestor;
156 Cvc5Term member = cvc5_mk_term(tm, CVC5_KIND_SET_MEMBER, 2, args2);
157 args1[0] = member;
158 Cvc5Term not_member = cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args1);
159
160 args1[0] = x;
161 Cvc5Term vars = cvc5_mk_term(tm, CVC5_KIND_VARIABLE_LIST, 1, args1);
162 args2[0] = vars;
163 args2[1] = not_member;
164 Cvc5Term not_self_ancestor = cvc5_mk_term(tm, CVC5_KIND_FORALL, 2, args2);
165
166 // formulas
167 cvc5_assert_formula(slv, people_universe);
168 cvc5_assert_formula(slv, male_not_empty);
169 cvc5_assert_formula(slv, female_not_empty);
170 cvc5_assert_formula(slv, disjoint_males_females);
171 cvc5_assert_formula(slv, father_not_empty);
172 cvc5_assert_formula(slv, mother_not_empty);
173 cvc5_assert_formula(slv, fathers_are_males);
174 cvc5_assert_formula(slv, mothers_are_females);
175 cvc5_assert_formula(slv, parent_is_father_or_mother);
176 cvc5_assert_formula(slv, descendant_formula);
177 cvc5_assert_formula(slv, ancestor_formula);
178 cvc5_assert_formula(slv, not_self_ancestor);
179
180 // check sat
181 Cvc5Result result = cvc5_check_sat(slv);
182
183 // output
184 printf("Result = %s\n", cvc5_result_to_string(result));
185 printf("people = %s\n", cvc5_term_to_string(cvc5_get_value(slv, people)));
186 printf("males = %s\n", cvc5_term_to_string(cvc5_get_value(slv, males)));
187 printf("females = %s\n",
188 cvc5_term_to_string(cvc5_get_value(slv, females)));
189 printf("father = %s\n", cvc5_term_to_string(cvc5_get_value(slv, father)));
190 printf("mother = %s\n", cvc5_term_to_string(cvc5_get_value(slv, mother)));
191 printf("parent = %s\n", cvc5_term_to_string(cvc5_get_value(slv, parent)));
192 printf("descendant = %s\n",
193 cvc5_term_to_string(cvc5_get_value(slv, descendant)));
194 printf("ancestor = %s\n",
195 cvc5_term_to_string(cvc5_get_value(slv, ancestor)));
196
197 cvc5_delete(slv);
198 cvc5_term_manager_delete(tm);
199}
examples/api/java/Relations.java
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 relations with cvc5 via Java API.
11 */
12
13import static io.github.cvc5.Kind.*;
14
15import io.github.cvc5.*;
16
17public class Relations
18{
19 public static void main(String[] args) throws CVC5ApiException
20 {
21 TermManager tm = new TermManager();
22 Solver solver = new Solver(tm);
23 {
24 // Set the logic
25 solver.setLogic("ALL");
26
27 // options
28 solver.setOption("produce-models", "true");
29 // we need finite model finding to answer sat problems with universal
30 // quantified formulas
31 solver.setOption("finite-model-find", "true");
32 // we need sets extension to support set.universe operator
33 solver.setOption("sets-exp", "true");
34
35 // (declare-sort Person 0)
36 Sort personSort = tm.mkUninterpretedSort("Person");
37
38 // (Tuple Person)
39 Sort tupleArity1 = tm.mkTupleSort(new Sort[] {personSort});
40 // (Relation Person)
41 Sort relationArity1 = tm.mkSetSort(tupleArity1);
42
43 // (Tuple Person Person)
44 Sort tupleArity2 = tm.mkTupleSort(new Sort[] {personSort, personSort});
45 // (Relation Person Person)
46 Sort relationArity2 = tm.mkSetSort(tupleArity2);
47
48 // empty set
49 Term emptySetTerm = tm.mkEmptySet(relationArity1);
50
51 // empty relation
52 Term emptyRelationTerm = tm.mkEmptySet(relationArity2);
53
54 // universe set
55 Term universeSet = tm.mkUniverseSet(relationArity1);
56
57 // variables
58 Term people = tm.mkConst(relationArity1, "people");
59 Term males = tm.mkConst(relationArity1, "males");
60 Term females = tm.mkConst(relationArity1, "females");
61 Term father = tm.mkConst(relationArity2, "father");
62 Term mother = tm.mkConst(relationArity2, "mother");
63 Term parent = tm.mkConst(relationArity2, "parent");
64 Term ancestor = tm.mkConst(relationArity2, "ancestor");
65 Term descendant = tm.mkConst(relationArity2, "descendant");
66
67 Term isEmpty1 = tm.mkTerm(EQUAL, males, emptySetTerm);
68 Term isEmpty2 = tm.mkTerm(EQUAL, females, emptySetTerm);
69
70 // (assert (= people (as set.universe (Relation Person))))
71 Term peopleAreTheUniverse = tm.mkTerm(EQUAL, people, universeSet);
72 // (assert (not (= males (as set.empty (Relation Person)))))
73 Term maleSetIsNotEmpty = tm.mkTerm(NOT, isEmpty1);
74 // (assert (not (= females (as set.empty (Relation Person)))))
75 Term femaleSetIsNotEmpty = tm.mkTerm(NOT, isEmpty2);
76
77 // (assert (= (set.inter males females)
78 // (as set.empty (Relation Person))))
79 Term malesFemalesIntersection = tm.mkTerm(SET_INTER, males, females);
80 Term malesAndFemalesAreDisjoint = tm.mkTerm(EQUAL, malesFemalesIntersection, emptySetTerm);
81
82 // (assert (not (= father (as set.empty (Relation Person Person)))))
83 // (assert (not (= mother (as set.empty (Relation Person Person)))))
84 Term isEmpty3 = tm.mkTerm(EQUAL, father, emptyRelationTerm);
85 Term isEmpty4 = tm.mkTerm(EQUAL, mother, emptyRelationTerm);
86 Term fatherIsNotEmpty = tm.mkTerm(NOT, isEmpty3);
87 Term motherIsNotEmpty = tm.mkTerm(NOT, isEmpty4);
88
89 // fathers are males
90 // (assert (set.subset (rel.join father people) males))
91 Term fathers = tm.mkTerm(RELATION_JOIN, father, people);
92 Term fathersAreMales = tm.mkTerm(SET_SUBSET, fathers, males);
93
94 // mothers are females
95 // (assert (set.subset (rel.join mother people) females))
96 Term mothers = tm.mkTerm(RELATION_JOIN, mother, people);
97 Term mothersAreFemales = tm.mkTerm(SET_SUBSET, mothers, females);
98
99 // (assert (= parent (set.union father mother)))
100 Term unionFatherMother = tm.mkTerm(SET_UNION, father, mother);
101 Term parentIsFatherOrMother = tm.mkTerm(EQUAL, parent, unionFatherMother);
102
103 // (assert (= ancestor (rel.tclosure parent)))
104 Term transitiveClosure = tm.mkTerm(RELATION_TCLOSURE, parent);
105 Term ancestorFormula = tm.mkTerm(EQUAL, ancestor, transitiveClosure);
106
107 // (assert (= descendant (rel.transpose ancestor)))
108 Term transpose = tm.mkTerm(RELATION_TRANSPOSE, ancestor);
109 Term descendantFormula = tm.mkTerm(EQUAL, descendant, transpose);
110
111 // (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
112 Term x = tm.mkVar(personSort, "x");
113 Term xxTuple = tm.mkTuple(new Term[] {x, x});
114 Term member = tm.mkTerm(SET_MEMBER, xxTuple, ancestor);
115 Term notMember = tm.mkTerm(NOT, member);
116
117 Term quantifiedVariables = tm.mkTerm(VARIABLE_LIST, x);
118 Term noSelfAncestor = tm.mkTerm(FORALL, quantifiedVariables, notMember);
119
120 // formulas
121 solver.assertFormula(peopleAreTheUniverse);
122 solver.assertFormula(maleSetIsNotEmpty);
123 solver.assertFormula(femaleSetIsNotEmpty);
124 solver.assertFormula(malesAndFemalesAreDisjoint);
125 solver.assertFormula(fatherIsNotEmpty);
126 solver.assertFormula(motherIsNotEmpty);
127 solver.assertFormula(fathersAreMales);
128 solver.assertFormula(mothersAreFemales);
129 solver.assertFormula(parentIsFatherOrMother);
130 solver.assertFormula(descendantFormula);
131 solver.assertFormula(ancestorFormula);
132 solver.assertFormula(noSelfAncestor);
133
134 // check sat
135 Result result = solver.checkSat();
136
137 // output
138 System.out.println("Result = " + result);
139 System.out.println("people = " + solver.getValue(people));
140 System.out.println("males = " + solver.getValue(males));
141 System.out.println("females = " + solver.getValue(females));
142 System.out.println("father = " + solver.getValue(father));
143 System.out.println("mother = " + solver.getValue(mother));
144 System.out.println("parent = " + solver.getValue(parent));
145 System.out.println("descendant = " + solver.getValue(descendant));
146 System.out.println("ancestor = " + solver.getValue(ancestor));
147 }
148 Context.deletePointers();
149 }
150}
examples/api/python/relations.py
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 relations solver
12# through the Python API. This is a direct translation of relations.cpp.
13##
14
15import cvc5
16from cvc5 import Kind
17
18if __name__ == "__main__":
19 tm = cvc5.TermManager()
20 solver = cvc5.Solver(tm)
21
22 # Set the logic
23 solver.setLogic("ALL")
24
25 # options
26 solver.setOption("produce-models", "true")
27 # we need finite model finding to answer sat problems with universal
28 # quantified formulas
29 solver.setOption("finite-model-find", "true")
30 # we need sets extension to support set.universe operator
31 solver.setOption("sets-exp", "true")
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 # (declare-sort Person 0)
40 personSort = tm.mkUninterpretedSort("Person")
41
42 # (Tuple Person)
43 tupleArity1 = tm.mkTupleSort(personSort)
44 # (Relation Person)
45 relationArity1 = tm.mkSetSort(tupleArity1)
46
47 # (Tuple Person Person)
48 tupleArity2 = tm.mkTupleSort(personSort, personSort)
49 # (Relation Person Person)
50 relationArity2 = tm.mkSetSort(tupleArity2)
51
52 # empty set
53 emptySetTerm = tm.mkEmptySet(relationArity1)
54
55 # empty relation
56 emptyRelationTerm = tm.mkEmptySet(relationArity2)
57
58 # universe set
59 universeSet = tm.mkUniverseSet(relationArity1)
60
61 # variables
62 people = tm.mkConst(relationArity1, "people")
63 males = tm.mkConst(relationArity1, "males")
64 females = tm.mkConst(relationArity1, "females")
65 father = tm.mkConst(relationArity2, "father")
66 mother = tm.mkConst(relationArity2, "mother")
67 parent = tm.mkConst(relationArity2, "parent")
68 ancestor = tm.mkConst(relationArity2, "ancestor")
69 descendant = tm.mkConst(relationArity2, "descendant")
70
71 isEmpty1 = tm.mkTerm(Kind.EQUAL, males, emptySetTerm)
72 isEmpty2 = tm.mkTerm(Kind.EQUAL, females, emptySetTerm)
73
74 # (assert (= people (as set.universe (Relation Person))))
75 peopleAreTheUniverse = tm.mkTerm(Kind.EQUAL, people, universeSet)
76 # (assert (not (= males (as set.empty (Relation Person)))))
77 maleSetIsNotEmpty = tm.mkTerm(Kind.NOT, isEmpty1)
78 # (assert (not (= females (as set.empty (Relation Person)))))
79 femaleSetIsNotEmpty = tm.mkTerm(Kind.NOT, isEmpty2)
80
81 # (assert (= (set.inter males females)
82 # (as set.empty (Relation Person))))
83 malesFemalesIntersection = tm.mkTerm(Kind.SET_INTER, males, females)
84 malesAndFemalesAreDisjoint = \
85 tm.mkTerm(Kind.EQUAL, malesFemalesIntersection, emptySetTerm)
86
87 # (assert (not (= father (as set.empty (Relation Person Person)))))
88 # (assert (not (= mother (as set.empty (Relation Person Person)))))
89 isEmpty3 = tm.mkTerm(Kind.EQUAL, father, emptyRelationTerm)
90 isEmpty4 = tm.mkTerm(Kind.EQUAL, mother, emptyRelationTerm)
91 fatherIsNotEmpty = tm.mkTerm(Kind.NOT, isEmpty3)
92 motherIsNotEmpty = tm.mkTerm(Kind.NOT, isEmpty4)
93
94 # fathers are males
95 # (assert (set.subset (rel.join father people) males))
96 fathers = tm.mkTerm(Kind.RELATION_JOIN, father, people)
97 fathersAreMales = tm.mkTerm(Kind.SET_SUBSET, fathers, males)
98
99 # mothers are females
100 # (assert (set.subset (rel.join mother people) females))
101 mothers = tm.mkTerm(Kind.RELATION_JOIN, mother, people)
102 mothersAreFemales = tm.mkTerm(Kind.SET_SUBSET, mothers, females)
103
104 # (assert (= parent (set.union father mother)))
105 unionFatherMother = tm.mkTerm(Kind.SET_UNION, father, mother)
106 parentIsFatherOrMother = \
107 tm.mkTerm(Kind.EQUAL, parent, unionFatherMother)
108
109 # (assert (= ancestor (rel.tclosure parent)))
110 transitiveClosure = tm.mkTerm(Kind.RELATION_TCLOSURE, parent)
111 ancestorFormula = tm.mkTerm(Kind.EQUAL, ancestor, transitiveClosure)
112
113 # (assert (= descendant (rel.transpose ancestor)))
114 transpose = tm.mkTerm(Kind.RELATION_TRANSPOSE, ancestor)
115 descendantFormula = tm.mkTerm(Kind.EQUAL, descendant, transpose)
116
117 # (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
118 x = tm.mkVar(personSort, "x")
119 xxTuple = tm.mkTuple([x, x])
120 member = tm.mkTerm(Kind.SET_MEMBER, xxTuple, ancestor)
121 notMember = tm.mkTerm(Kind.NOT, member)
122
123 quantifiedVariables = tm.mkTerm(Kind.VARIABLE_LIST, x)
124 noSelfAncestor = 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 = solver.checkSat()
142
143 # output
144 print("Result = {}".format(result))
145 print("people = {}".format(solver.getValue(people)))
146 print("males = {}".format(solver.getValue(males)))
147 print("females = {}".format(solver.getValue(females)))
148 print("father = {}".format(solver.getValue(father)))
149 print("mother = {}".format(solver.getValue(mother)))
150 print("parent = {}".format(solver.getValue(parent)))
151 print("descendant = {}".format(solver.getValue(descendant)))
152 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)