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
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
|
/********************* */
/*! \file Relations.java
** \verbatim
** Top contributors (to current version):
** Mudathir Mohamed, Andres Noetzli
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 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.\endverbatim
**
** \brief Reasoning about relations with CVC4 via Java API.
**
** A simple demonstration of reasoning about strings with CVC4 via Jave API.
**/
import edu.stanford.CVC4.*;
/*
This file uses the API to make a sat call equivalent to the following benchmark:
(set-logic ALL)
(set-option :finite-model-find true)
(set-option :produce-models true)
(set-option :sets-ext true)
(set-option :output-language "smt2")
(declare-sort Person 0)
(declare-fun people () (Set (Tuple Person)))
(declare-fun males () (Set (Tuple Person)))
(declare-fun females() (Set (Tuple Person)))
(declare-fun father () (Set (Tuple Person Person)))
(declare-fun mother () (Set (Tuple Person Person)))
(declare-fun parent () (Set (Tuple Person Person)))
(declare-fun ancestor () (Set (Tuple Person Person)))
(declare-fun descendant () (Set (Tuple Person Person)))
(assert (= people (as univset (Set (Tuple Person)))))
(assert (not (= males (as emptyset (Set (Tuple Person))))))
(assert (not (= females (as emptyset (Set (Tuple Person))))))
(assert (= (intersection males females) (as emptyset (Set (Tuple Person)))))
; father relation is not empty
(assert (not (= father (as emptyset (Set (Tuple Person Person))))))
; mother relation is not empty
(assert (not (= mother (as emptyset (Set (Tuple Person Person))))))
; fathers are males
(assert (subset (join father people) males))
; mothers are females
(assert (subset (join mother people) females))
; parent
(assert (= parent (union father mother)))
; no self ancestor
(assert (forall ((x Person)) (not (member (mkTuple x x) ancestor))))
; descendant
(assert (= descendant (tclosure parent)))
; ancestor
(assert (= ancestor (transpose descendant)))
(check-sat)
(get-model)
*/
public class Relations {
public static void main(String[] args) {
System.loadLibrary("cvc4jni");
ExprManager manager = new ExprManager();
SmtEngine smtEngine = new SmtEngine(manager);
// Set the logic
smtEngine.setLogic("ALL");
// options
smtEngine.setOption("produce-models", new SExpr(true));
smtEngine.setOption("finite-model-find", new SExpr(true));
smtEngine.setOption("sets-ext", new SExpr(true));
smtEngine.setOption("output-language", new SExpr("smt2"));
// (declare-sort Person 0)
Type personType = manager.mkSort("Person", 0);
vectorType vector1 = new vectorType();
vector1.add(personType);
// (Tuple Person)
Type tupleArity1 = manager.mkTupleType(vector1);
// (Set (Tuple Person))
SetType relationArity1 = manager.mkSetType(tupleArity1);
vectorType vector2 = new vectorType();
vector2.add(personType);
vector2.add(personType);
// (Tuple Person Person)
DatatypeType tupleArity2 = manager.mkTupleType(vector2);
// (Set (Tuple Person Person))
SetType relationArity2 = manager.mkSetType(tupleArity2);
// empty set
EmptySet emptySet = new EmptySet(relationArity1);
Expr emptySetExpr = manager.mkConst(emptySet);
// empty relation
EmptySet emptyRelation = new EmptySet(relationArity2);
Expr emptyRelationExpr = manager.mkConst(emptyRelation);
// universe set
Expr universeSet =
manager.mkNullaryOperator(relationArity1, Kind.UNIVERSE_SET);
// variables
Expr people = manager.mkVar("people", relationArity1);
Expr males = manager.mkVar("males", relationArity1);
Expr females = manager.mkVar("females", relationArity1);
Expr father = manager.mkVar("father", relationArity2);
Expr mother = manager.mkVar("mother", relationArity2);
Expr parent = manager.mkVar("parent", relationArity2);
Expr ancestor = manager.mkVar("ancestor", relationArity2);
Expr descendant = manager.mkVar("descendant", relationArity2);
Expr isEmpty1 = manager.mkExpr(Kind.EQUAL, males, emptySetExpr);
Expr isEmpty2 = manager.mkExpr(Kind.EQUAL, females, emptySetExpr);
// (assert (= people (as univset (Set (Tuple Person)))))
Expr peopleAreTheUniverse = manager.mkExpr(Kind.EQUAL, people, universeSet);
// (assert (not (= males (as emptyset (Set (Tuple Person))))))
Expr maleSetIsNotEmpty = manager.mkExpr(Kind.NOT, isEmpty1);
// (assert (not (= females (as emptyset (Set (Tuple Person))))))
Expr femaleSetIsNotEmpty = manager.mkExpr(Kind.NOT, isEmpty2);
// (assert (= (intersection males females) (as emptyset (Set (Tuple
// Person)))))
Expr malesFemalesIntersection =
manager.mkExpr(Kind.INTERSECTION, males, females);
Expr malesAndFemalesAreDisjoint =
manager.mkExpr(Kind.EQUAL, malesFemalesIntersection, emptySetExpr);
// (assert (not (= father (as emptyset (Set (Tuple Person Person))))))
// (assert (not (= mother (as emptyset (Set (Tuple Person Person))))))
Expr isEmpty3 = manager.mkExpr(Kind.EQUAL, father, emptyRelationExpr);
Expr isEmpty4 = manager.mkExpr(Kind.EQUAL, mother, emptyRelationExpr);
Expr fatherIsNotEmpty = manager.mkExpr(Kind.NOT, isEmpty3);
Expr motherIsNotEmpty = manager.mkExpr(Kind.NOT, isEmpty4);
// fathers are males
// (assert (subset (join father people) males))
Expr fathers = manager.mkExpr(Kind.JOIN, father, people);
Expr fathersAreMales = manager.mkExpr(Kind.SUBSET, fathers, males);
// mothers are females
// (assert (subset (join mother people) females))
Expr mothers = manager.mkExpr(Kind.JOIN, mother, people);
Expr mothersAreFemales = manager.mkExpr(Kind.SUBSET, mothers, females);
// (assert (= parent (union father mother)))
Expr unionFatherMother = manager.mkExpr(Kind.UNION, father, mother);
Expr parentIsFatherOrMother =
manager.mkExpr(Kind.EQUAL, parent, unionFatherMother);
// (assert (= parent (union father mother)))
Expr transitiveClosure = manager.mkExpr(Kind.TCLOSURE, parent);
Expr descendantFormula =
manager.mkExpr(Kind.EQUAL, descendant, transitiveClosure);
// (assert (= parent (union father mother)))
Expr transpose = manager.mkExpr(Kind.TRANSPOSE, descendant);
Expr ancestorFormula = manager.mkExpr(Kind.EQUAL, ancestor, transpose);
// (assert (forall ((x Person)) (not (member (mkTuple x x) ancestor))))
Expr x = manager.mkBoundVar("x", personType);
Expr constructor = tupleArity2.getDatatype().get(0).getConstructor();
Expr xxTuple = manager.mkExpr(Kind.APPLY_CONSTRUCTOR, constructor, x, x);
Expr member = manager.mkExpr(Kind.MEMBER, xxTuple, ancestor);
Expr notMember = manager.mkExpr(Kind.NOT, member);
vectorExpr vectorExpr = new vectorExpr();
vectorExpr.add(x);
Expr quantifiedVariables = manager.mkExpr(Kind.BOUND_VAR_LIST, x);
Expr noSelfAncestor =
manager.mkExpr(Kind.FORALL, quantifiedVariables, notMember);
// formulas
Expr formula1 = manager.mkExpr(Kind.AND,
peopleAreTheUniverse,
maleSetIsNotEmpty,
femaleSetIsNotEmpty,
malesAndFemalesAreDisjoint);
Expr formula2 = manager.mkExpr(Kind.AND,
formula1,
fatherIsNotEmpty,
motherIsNotEmpty,
fathersAreMales,
mothersAreFemales);
Expr formula3 = manager.mkExpr(Kind.AND,
formula2,
parentIsFatherOrMother,
descendantFormula,
ancestorFormula,
noSelfAncestor);
// check sat
Result result = smtEngine.checkSat(formula3);
// output
System.out.println("CVC4 reports: " + formula3 + " is " + result + ".");
System.out.println("people = " + smtEngine.getValue(people));
System.out.println("males = " + smtEngine.getValue(males));
System.out.println("females = " + smtEngine.getValue(females));
System.out.println("father = " + smtEngine.getValue(father));
System.out.println("mother = " + smtEngine.getValue(mother));
System.out.println("parent = " + smtEngine.getValue(parent));
System.out.println("descendant = " + smtEngine.getValue(descendant));
System.out.println("ancestor = " + smtEngine.getValue(ancestor));
}
}
|
