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