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-2024 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * A simple demonstration of reasoning about sets with cvc5.
14 */
15
16#include <cvc5/cvc5.h>
17
18#include <iostream>
19
20using namespace std;
21using namespace cvc5;
22
23int main()
24{
25 TermManager tm;
26 Solver slv(tm);
27
28 // Optionally, set the logic. We need at least UF for equality predicate,
29 // integers (LIA) and sets (FS).
30 slv.setLogic("QF_UFLIAFS");
31
32 // Produce models
33 slv.setOption("produce-models", "true");
34 slv.setOption("output-language", "smt2");
35
36 Sort integer = tm.getIntegerSort();
37 Sort set = tm.mkSetSort(integer);
38
39 // Verify union distributions over intersection
40 // (A union B) intersection C = (A intersection C) union (B intersection C)
41 {
42 Term A = tm.mkConst(set, "A");
43 Term B = tm.mkConst(set, "B");
44 Term C = tm.mkConst(set, "C");
45
46 Term unionAB = tm.mkTerm(Kind::SET_UNION, {A, B});
47 Term lhs = tm.mkTerm(Kind::SET_INTER, {unionAB, C});
48
49 Term intersectionAC = tm.mkTerm(Kind::SET_INTER, {A, C});
50 Term intersectionBC = tm.mkTerm(Kind::SET_INTER, {B, C});
51 Term rhs = tm.mkTerm(Kind::SET_UNION, {intersectionAC, intersectionBC});
52
53 Term theorem = tm.mkTerm(Kind::EQUAL, {lhs, rhs});
54
55 cout << "cvc5 reports: " << theorem << " is "
56 << slv.checkSatAssuming(theorem.notTerm()) << "." << endl;
57 }
58
59 // Verify emptset is a subset of any set
60 {
61 Term A = tm.mkConst(set, "A");
62 Term emptyset = tm.mkEmptySet(set);
63
64 Term theorem = tm.mkTerm(Kind::SET_SUBSET, {emptyset, A});
65
66 cout << "cvc5 reports: " << theorem << " is "
67 << slv.checkSatAssuming(theorem.notTerm()) << "." << endl;
68 }
69
70 // Find me an element in {1, 2} intersection {2, 3}, if there is one.
71 {
72 Term one = tm.mkInteger(1);
73 Term two = tm.mkInteger(2);
74 Term three = tm.mkInteger(3);
75
76 Term singleton_one = tm.mkTerm(Kind::SET_SINGLETON, {one});
77 Term singleton_two = tm.mkTerm(Kind::SET_SINGLETON, {two});
78 Term singleton_three = tm.mkTerm(Kind::SET_SINGLETON, {three});
79 Term one_two = tm.mkTerm(Kind::SET_UNION, {singleton_one, singleton_two});
80 Term two_three =
81 tm.mkTerm(Kind::SET_UNION, {singleton_two, singleton_three});
82 Term intersection = tm.mkTerm(Kind::SET_INTER, {one_two, two_three});
83
84 Term x = tm.mkConst(integer, "x");
85
86 Term e = tm.mkTerm(Kind::SET_MEMBER, {x, intersection});
87
88 Result result = slv.checkSatAssuming(e);
89 cout << "cvc5 reports: " << e << " is " << result << "." << endl;
90
91 if (result.isSat())
92 {
93 cout << "For instance, " << slv.getValue(x) << " is a member." << endl;
94 }
95 }
96}
1/******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Andres Noetzli
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * A simple demonstration of reasoning about sets with cvc5.
14 */
15
16import static io.github.cvc5.Kind.*;
17
18import io.github.cvc5.*;
19
20public class Sets
21{
22 public static void main(String args[]) throws CVC5ApiException
23 {
24 Solver slv = new Solver();
25 {
26 // Optionally, set the logic. We need at least UF for equality predicate,
27 // integers (LIA) and sets (FS).
28 slv.setLogic("QF_UFLIAFS");
29
30 // Produce models
31 slv.setOption("produce-models", "true");
32 slv.setOption("output-language", "smt2");
33
34 Sort integer = slv.getIntegerSort();
35 Sort set = slv.mkSetSort(integer);
36
37 // Verify union distributions over intersection
38 // (A union B) intersection C = (A intersection C) union (B intersection C)
39 {
40 Term A = slv.mkConst(set, "A");
41 Term B = slv.mkConst(set, "B");
42 Term C = slv.mkConst(set, "C");
43
44 Term unionAB = slv.mkTerm(SET_UNION, A, B);
45 Term lhs = slv.mkTerm(SET_INTER, unionAB, C);
46
47 Term intersectionAC = slv.mkTerm(SET_INTER, A, C);
48 Term intersectionBC = slv.mkTerm(SET_INTER, B, C);
49 Term rhs = slv.mkTerm(SET_UNION, intersectionAC, intersectionBC);
50
51 Term theorem = slv.mkTerm(EQUAL, lhs, rhs);
52
53 System.out.println(
54 "cvc5 reports: " + theorem + " is " + slv.checkSatAssuming(theorem.notTerm()) + ".");
55 }
56
57 // Verify set.empty is a subset of any set
58 {
59 Term A = slv.mkConst(set, "A");
60 Term emptyset = slv.mkEmptySet(set);
61
62 Term theorem = slv.mkTerm(SET_SUBSET, emptyset, A);
63
64 System.out.println(
65 "cvc5 reports: " + theorem + " is " + slv.checkSatAssuming(theorem.notTerm()) + ".");
66 }
67
68 // Find me an element in {1, 2} intersection {2, 3}, if there is one.
69 {
70 Term one = slv.mkInteger(1);
71 Term two = slv.mkInteger(2);
72 Term three = slv.mkInteger(3);
73
74 Term singleton_one = slv.mkTerm(SET_SINGLETON, one);
75 Term singleton_two = slv.mkTerm(SET_SINGLETON, two);
76 Term singleton_three = slv.mkTerm(SET_SINGLETON, three);
77 Term one_two = slv.mkTerm(SET_UNION, singleton_one, singleton_two);
78 Term two_three = slv.mkTerm(SET_UNION, singleton_two, singleton_three);
79 Term intersection = slv.mkTerm(SET_INTER, one_two, two_three);
80
81 Term x = slv.mkConst(integer, "x");
82
83 Term e = slv.mkTerm(SET_MEMBER, x, intersection);
84
85 Result result = slv.checkSatAssuming(e);
86 System.out.println("cvc5 reports: " + e + " is " + result + ".");
87
88 if (result.isSat())
89 {
90 System.out.println("For instance, " + slv.getValue(x) + " is a member.");
91 }
92 }
93 }
94 Context.deletePointers();
95 }
96}
1#!/usr/bin/env python
2###############################################################################
3# Top contributors (to current version):
4# Makai Mann, Aina Niemetz, Mudathir Mohamed
5#
6# This file is part of the cvc5 project.
7#
8# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
9# in the top-level source directory and their institutional affiliations.
10# All rights reserved. See the file COPYING in the top-level source
11# directory for licensing information.
12# #############################################################################
13#
14# A simple demonstration of the solving capabilities of the cvc5 sets solver
15# through the Python API. This is a direct translation of sets.cpp.
16##
17
18import cvc5
19from cvc5 import Kind
20
21if __name__ == "__main__":
22 tm = cvc5.TermManager()
23 slv = cvc5.Solver(tm)
24
25 # Optionally, set the logic. We need at least UF for equality predicate,
26 # integers (LIA) and sets (FS).
27 slv.setLogic("QF_UFLIAFS")
28
29 # Produce models
30 slv.setOption("produce-models", "true")
31 slv.setOption("output-language", "smt2")
32
33 integer = tm.getIntegerSort()
34 set_ = tm.mkSetSort(integer)
35
36 # Verify union distributions over intersection
37 # (A union B) intersection C = (A intersection C) union (B intersection C)
38
39 A = tm.mkConst(set_, "A")
40 B = tm.mkConst(set_, "B")
41 C = tm.mkConst(set_, "C")
42
43 unionAB = tm.mkTerm(Kind.SET_UNION, A, B)
44 lhs = tm.mkTerm(Kind.SET_INTER, unionAB, C)
45
46 intersectionAC = tm.mkTerm(Kind.SET_INTER, A, C)
47 intersectionBC = tm.mkTerm(Kind.SET_INTER, B, C)
48 rhs = tm.mkTerm(Kind.SET_UNION, intersectionAC, intersectionBC)
49
50 theorem = tm.mkTerm(Kind.EQUAL, lhs, rhs)
51
52 print("cvc5 reports: {} is {}".format(
53 theorem.notTerm(), slv.checkSatAssuming(theorem.notTerm())))
54
55 # Verify emptset is a subset of any set
56
57 A = tm.mkConst(set_, "A")
58 emptyset = tm.mkEmptySet(set_)
59
60 theorem = tm.mkTerm(Kind.SET_SUBSET, emptyset, A)
61
62 print("cvc5 reports: {} is {}".format(
63 theorem.notTerm(), slv.checkSatAssuming(theorem.notTerm())))
64
65 # Find me an element in 1, 2 intersection 2, 3, if there is one.
66
67 one = tm.mkInteger(1)
68 two = tm.mkInteger(2)
69 three = tm.mkInteger(3)
70
71 singleton_one = tm.mkTerm(Kind.SET_SINGLETON, one)
72 singleton_two = tm.mkTerm(Kind.SET_SINGLETON, two)
73 singleton_three = tm.mkTerm(Kind.SET_SINGLETON, three)
74 one_two = tm.mkTerm(Kind.SET_UNION, singleton_one, singleton_two)
75 two_three = tm.mkTerm(Kind.SET_UNION, singleton_two, singleton_three)
76 intersection = tm.mkTerm(Kind.SET_INTER, one_two, two_three)
77
78 x = tm.mkConst(integer, "x")
79
80 e = tm.mkTerm(Kind.SET_MEMBER, x, intersection)
81
82 result = slv.checkSatAssuming(e)
83
84 print("cvc5 reports: {} is {}".format(e, result))
85
86 if result:
87 print("For instance, {} is a member".format(slv.getValue(x)))
1(set-logic QF_UFLIAFS)
2(set-option :produce-models true)
3(set-option :incremental true)
4(declare-const A (Set Int))
5(declare-const B (Set Int))
6(declare-const C (Set Int))
7(declare-const x Int)
8
9; Verify union distributions over intersection
10(check-sat-assuming
11 (
12 (distinct
13 (set.inter (set.union A B) C)
14 (set.union (set.inter A C) (set.inter B C)))
15 )
16)
17
18; Verify emptset is a subset of any set
19(check-sat-assuming
20 (
21 (not (set.subset (as set.empty (Set Int)) A))
22 )
23)
24
25; Find an element in {1, 2} intersection {2, 3}, if there is one.
26(check-sat-assuming
27 (
28 (set.member
29 x
30 (set.inter
31 (set.union (set.singleton 1) (set.singleton 2))
32 (set.union (set.singleton 2) (set.singleton 3))))
33 )
34)
35
36(echo "A member: ")
37(get-value (x))
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-2024 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * A simple demonstration of reasoning about relations with cvc5 via 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-ext", "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}
examples/api/java/Relations.java
1/******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Andres Noetzli, Andrew Reynolds
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * A simple demonstration of reasoning about 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 Solver solver = new Solver();
25 {
26 // Set the logic
27 solver.setLogic("ALL");
28
29 // options
30 solver.setOption("produce-models", "true");
31 // we need finite model finding to answer sat problems with universal
32 // quantified formulas
33 solver.setOption("finite-model-find", "true");
34 // we need sets extension to support set.universe operator
35 solver.setOption("sets-ext", "true");
36
37 // (declare-sort Person 0)
38 Sort personSort = solver.mkUninterpretedSort("Person");
39
40 // (Tuple Person)
41 Sort tupleArity1 = solver.mkTupleSort(new Sort[] {personSort});
42 // (Relation Person)
43 Sort relationArity1 = solver.mkSetSort(tupleArity1);
44
45 // (Tuple Person Person)
46 Sort tupleArity2 = solver.mkTupleSort(new Sort[] {personSort, personSort});
47 // (Relation Person Person)
48 Sort relationArity2 = solver.mkSetSort(tupleArity2);
49
50 // empty set
51 Term emptySetTerm = solver.mkEmptySet(relationArity1);
52
53 // empty relation
54 Term emptyRelationTerm = solver.mkEmptySet(relationArity2);
55
56 // universe set
57 Term universeSet = solver.mkUniverseSet(relationArity1);
58
59 // variables
60 Term people = solver.mkConst(relationArity1, "people");
61 Term males = solver.mkConst(relationArity1, "males");
62 Term females = solver.mkConst(relationArity1, "females");
63 Term father = solver.mkConst(relationArity2, "father");
64 Term mother = solver.mkConst(relationArity2, "mother");
65 Term parent = solver.mkConst(relationArity2, "parent");
66 Term ancestor = solver.mkConst(relationArity2, "ancestor");
67 Term descendant = solver.mkConst(relationArity2, "descendant");
68
69 Term isEmpty1 = solver.mkTerm(EQUAL, males, emptySetTerm);
70 Term isEmpty2 = solver.mkTerm(EQUAL, females, emptySetTerm);
71
72 // (assert (= people (as set.universe (Relation Person))))
73 Term peopleAreTheUniverse = solver.mkTerm(EQUAL, people, universeSet);
74 // (assert (not (= males (as set.empty (Relation Person)))))
75 Term maleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty1);
76 // (assert (not (= females (as set.empty (Relation Person)))))
77 Term femaleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty2);
78
79 // (assert (= (set.inter males females)
80 // (as set.empty (Relation Person))))
81 Term malesFemalesIntersection = solver.mkTerm(SET_INTER, males, females);
82 Term malesAndFemalesAreDisjoint =
83 solver.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 = solver.mkTerm(EQUAL, father, emptyRelationTerm);
88 Term isEmpty4 = solver.mkTerm(EQUAL, mother, emptyRelationTerm);
89 Term fatherIsNotEmpty = solver.mkTerm(NOT, isEmpty3);
90 Term motherIsNotEmpty = solver.mkTerm(NOT, isEmpty4);
91
92 // fathers are males
93 // (assert (set.subset (rel.join father people) males))
94 Term fathers = solver.mkTerm(RELATION_JOIN, father, people);
95 Term fathersAreMales = solver.mkTerm(SET_SUBSET, fathers, males);
96
97 // mothers are females
98 // (assert (set.subset (rel.join mother people) females))
99 Term mothers = solver.mkTerm(RELATION_JOIN, mother, people);
100 Term mothersAreFemales = solver.mkTerm(SET_SUBSET, mothers, females);
101
102 // (assert (= parent (set.union father mother)))
103 Term unionFatherMother = solver.mkTerm(SET_UNION, father, mother);
104 Term parentIsFatherOrMother = solver.mkTerm(EQUAL, parent, unionFatherMother);
105
106 // (assert (= ancestor (rel.tclosure parent)))
107 Term transitiveClosure = solver.mkTerm(RELATION_TCLOSURE, parent);
108 Term ancestorFormula = solver.mkTerm(EQUAL, ancestor, transitiveClosure);
109
110 // (assert (= descendant (rel.transpose ancestor)))
111 Term transpose = solver.mkTerm(RELATION_TRANSPOSE, ancestor);
112 Term descendantFormula = solver.mkTerm(EQUAL, descendant, transpose);
113
114 // (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
115 Term x = solver.mkVar(personSort, "x");
116 Term xxTuple = solver.mkTuple(new Term[] {x, x});
117 Term member = solver.mkTerm(SET_MEMBER, xxTuple, ancestor);
118 Term notMember = solver.mkTerm(NOT, member);
119
120 Term quantifiedVariables = solver.mkTerm(VARIABLE_LIST, x);
121 Term noSelfAncestor = solver.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, Alex Ozdemir
5#
6# This file is part of the cvc5 project.
7#
8# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
9# in the top-level source directory and their institutional affiliations.
10# All rights reserved. See the file COPYING in the top-level source
11# directory for licensing information.
12# #############################################################################
13#
14# A simple demonstration of the solving capabilities of the cvc5 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-ext", "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-ext 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)