1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
|
/******************************************************************************
* Top contributors (to current version):
* Aina Niemetz, Mudathir Mohamed, Andrew Reynolds
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
* in the top-level source directory and their institutional affiliations.
* All rights reserved. See the file COPYING in the top-level source
* directory for licensing information.
* ****************************************************************************
*
* A simple demonstration of reasoning about relations via the C API.
*/
#include <cvc5/c/cvc5.h>
#include <stdio.h>
int main()
{
Cvc5TermManager* tm = cvc5_term_manager_new();
Cvc5* slv = cvc5_new(tm);
// Set the logic
cvc5_set_logic(slv, "ALL");
// options
cvc5_set_option(slv, "produce-models", "true");
// we need finite model finding to answer sat problems with universal
// quantified formulas
cvc5_set_option(slv, "finite-model-find", "true");
// we need sets extension to support set.universe operator
cvc5_set_option(slv, "sets-exp", "true");
// (declare-sort Person 0)
Cvc5Sort person_sort = cvc5_mk_uninterpreted_sort(tm, "Person");
// (Tuple Person)
Cvc5Sort sorts1[1] = {person_sort};
Cvc5Sort tuple_arity1 = cvc5_mk_tuple_sort(tm, 1, sorts1);
// (Relation Person)
Cvc5Sort rel_arity1 = cvc5_mk_set_sort(tm, tuple_arity1);
// (Tuple Person Person)
Cvc5Sort sorts2[2] = {person_sort, person_sort};
Cvc5Sort tuple_arity2 = cvc5_mk_tuple_sort(tm, 2, sorts2);
// (Relation Person Person)
Cvc5Sort rel_arity2 = cvc5_mk_set_sort(tm, tuple_arity2);
// empty set
Cvc5Term empty_set = cvc5_mk_empty_set(tm, rel_arity1);
// empty relation
Cvc5Term empty_rel = cvc5_mk_empty_set(tm, rel_arity2);
// universe set
Cvc5Term universe_set = cvc5_mk_universe_set(tm, rel_arity1);
// variables
Cvc5Term people = cvc5_mk_const(tm, rel_arity1, "people");
Cvc5Term males = cvc5_mk_const(tm, rel_arity1, "males");
Cvc5Term females = cvc5_mk_const(tm, rel_arity1, "females");
Cvc5Term father = cvc5_mk_const(tm, rel_arity2, "father");
Cvc5Term mother = cvc5_mk_const(tm, rel_arity2, "mother");
Cvc5Term parent = cvc5_mk_const(tm, rel_arity2, "parent");
Cvc5Term ancestor = cvc5_mk_const(tm, rel_arity2, "ancestor");
Cvc5Term descendant = cvc5_mk_const(tm, rel_arity2, "descendant");
Cvc5Term args2[2] = {males, empty_set};
Cvc5Term is_empty1 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
args2[0] = females;
Cvc5Term is_empty2 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
// (assert (= people (as set.universe (Relation Person))))
args2[0] = people;
args2[1] = universe_set;
Cvc5Term people_universe = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
// (assert (not (= males (as set.empty (Relation Person)))))
Cvc5Term args1[1] = {is_empty1};
Cvc5Term male_not_empty = cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args1);
// (assert (not (= females (as set.empty (Relation Person)))))
args1[0] = is_empty2;
Cvc5Term female_not_empty = cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args1);
// (assert (= (set.inter males females)
// (as set.empty (Relation Person))))
args2[0] = males;
args2[1] = females;
Cvc5Term inter_males_females =
cvc5_mk_term(tm, CVC5_KIND_SET_INTER, 2, args2);
args2[0] = inter_males_females;
args2[1] = empty_set;
Cvc5Term disjoint_males_females = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
// (assert (not (= father (as set.empty (Relation Person Person)))))
// (assert (not (= mother (as set.empty (Relation Person Person)))))
args2[0] = father;
args2[1] = empty_rel;
Cvc5Term is_empty3 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
args2[0] = mother;
args2[1] = empty_rel;
Cvc5Term is_empty4 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
args1[0] = is_empty3;
Cvc5Term father_not_empty = cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args1);
args1[0] = is_empty4;
Cvc5Term mother_not_empty = cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args1);
// fathers are males
// (assert (set.subset (rel.join father people) males))
args2[0] = father;
args2[1] = people;
Cvc5Term fathers = cvc5_mk_term(tm, CVC5_KIND_RELATION_JOIN, 2, args2);
args2[0] = fathers;
args2[1] = males;
Cvc5Term fathers_are_males = cvc5_mk_term(tm, CVC5_KIND_SET_SUBSET, 2, args2);
// mothers are females
// (assert (set.subset (rel.join mother people) females))
args2[0] = mother;
args2[1] = people;
Cvc5Term mothers = cvc5_mk_term(tm, CVC5_KIND_RELATION_JOIN, 2, args2);
args2[0] = mothers;
args2[1] = females;
Cvc5Term mothers_are_females =
cvc5_mk_term(tm, CVC5_KIND_SET_SUBSET, 2, args2);
// (assert (= parent (set.union father mother)))
args2[0] = father;
args2[1] = mother;
Cvc5Term union_father_mother =
cvc5_mk_term(tm, CVC5_KIND_SET_UNION, 2, args2);
args2[0] = parent;
args2[1] = union_father_mother;
Cvc5Term parent_is_father_or_mother =
cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
// (assert (= ancestor (rel.tclosure parent)))
args1[0] = parent;
Cvc5Term trans_closure =
cvc5_mk_term(tm, CVC5_KIND_RELATION_TCLOSURE, 1, args1);
args2[0] = ancestor;
args2[1] = trans_closure;
Cvc5Term ancestor_formula = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
// (assert (= descendant (rel.transpose descendant)))
args1[0] = ancestor;
Cvc5Term transpose = cvc5_mk_term(tm, CVC5_KIND_RELATION_TRANSPOSE, 1, args1);
args2[0] = descendant;
args2[1] = transpose;
Cvc5Term descendant_formula = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
// (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
Cvc5Term x = cvc5_mk_var(tm, person_sort, "x");
args2[0] = x;
args2[1] = x;
Cvc5Term xx_tuple = cvc5_mk_tuple(tm, 2, args2);
args2[0] = xx_tuple;
args2[1] = ancestor;
Cvc5Term member = cvc5_mk_term(tm, CVC5_KIND_SET_MEMBER, 2, args2);
args1[0] = member;
Cvc5Term not_member = cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args1);
args1[0] = x;
Cvc5Term vars = cvc5_mk_term(tm, CVC5_KIND_VARIABLE_LIST, 1, args1);
args2[0] = vars;
args2[1] = not_member;
Cvc5Term not_self_ancestor = cvc5_mk_term(tm, CVC5_KIND_FORALL, 2, args2);
// formulas
cvc5_assert_formula(slv, people_universe);
cvc5_assert_formula(slv, male_not_empty);
cvc5_assert_formula(slv, female_not_empty);
cvc5_assert_formula(slv, disjoint_males_females);
cvc5_assert_formula(slv, father_not_empty);
cvc5_assert_formula(slv, mother_not_empty);
cvc5_assert_formula(slv, fathers_are_males);
cvc5_assert_formula(slv, mothers_are_females);
cvc5_assert_formula(slv, parent_is_father_or_mother);
cvc5_assert_formula(slv, descendant_formula);
cvc5_assert_formula(slv, ancestor_formula);
cvc5_assert_formula(slv, not_self_ancestor);
// check sat
Cvc5Result result = cvc5_check_sat(slv);
// output
printf("Result = %s\n", cvc5_result_to_string(result));
printf("people = %s\n", cvc5_term_to_string(cvc5_get_value(slv, people)));
printf("males = %s\n", cvc5_term_to_string(cvc5_get_value(slv, males)));
printf("females = %s\n",
cvc5_term_to_string(cvc5_get_value(slv, females)));
printf("father = %s\n", cvc5_term_to_string(cvc5_get_value(slv, father)));
printf("mother = %s\n", cvc5_term_to_string(cvc5_get_value(slv, mother)));
printf("parent = %s\n", cvc5_term_to_string(cvc5_get_value(slv, parent)));
printf("descendant = %s\n",
cvc5_term_to_string(cvc5_get_value(slv, descendant)));
printf("ancestor = %s\n",
cvc5_term_to_string(cvc5_get_value(slv, ancestor)));
cvc5_delete(slv);
cvc5_term_manager_delete(tm);
}
|
