Skip to content

Commit 525472a

Browse files
kfriedbergerkfriedberger
authored
Merge pull request #523 from sosy-lab/yices2-arrays
Add support for arrays in Yices2
2 parents 6971a02 + c410213 commit 525472a

File tree

10 files changed

+306
-49
lines changed

10 files changed

+306
-49
lines changed

‎src/org/sosy_lab/java_smt/solvers/yices2/Yices2ArrayFormulaManager.java‎

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,77 @@
1+
/*
2+
* This file is part of JavaSMT,
3+
* an API wrapper for a collection of SMT solvers:
4+
* https://github.com/sosy-lab/java-smt
5+
*
6+
* SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
7+
*
8+
* SPDX-License-Identifier: Apache-2.0
9+
*/
10+
11+
package org.sosy_lab.java_smt.solvers.yices2;
12+
13+
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_application;
14+
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_eq;
15+
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_function_type;
16+
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_lambda;
17+
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_new_variable;
18+
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_update;
19+
20+
import com.google.common.collect.HashBasedTable;
21+
import com.google.common.collect.Table;
22+
import org.sosy_lab.java_smt.api.Formula;
23+
import org.sosy_lab.java_smt.api.FormulaType;
24+
import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager;
25+
26+
@SuppressWarnings({"ClassTypeParameterName", "MethodTypeParameterName"})
27+
public class Yices2ArrayFormulaManager
28+
extends AbstractArrayFormulaManager<Integer, Integer, Long, Integer> {
29+
30+
/**
31+
* Cache with constant array values.
32+
*
33+
* <p>Used in {@link #internalMakeArray(FormulaType, FormulaType, Integer)} to guarantee that
34+
* existing constant array values are never re-created
35+
*/
36+
private final Table<Integer, Integer, Integer> constCache = HashBasedTable.create();
37+
38+
public Yices2ArrayFormulaManager(Yices2FormulaCreator pCreator) {
39+
super(pCreator);
40+
}
41+
42+
@Override
43+
protected Integer select(Integer pArray, Integer pIndex) {
44+
return yices_application(pArray, 1, new int[] {pIndex});
45+
}
46+
47+
@Override
48+
protected Integer store(Integer pArray, Integer pIndex, Integer pValue) {
49+
return yices_update(pArray, 1, new int[] {pIndex}, pValue);
50+
}
51+
52+
@Override
53+
protected <TI extends Formula, TE extends Formula> Integer internalMakeArray(
54+
String pName, FormulaType<TI> pIndexType, FormulaType<TE> pElementType) {
55+
var yicesFuncType =
56+
yices_function_type(1, new int[] {toSolverType(pIndexType)}, toSolverType(pElementType));
57+
return ((Yices2FormulaCreator) getFormulaCreator()).createNamedVariable(yicesFuncType, pName);
58+
}
59+
60+
@Override
61+
protected <TI extends Formula, TE extends Formula> Integer internalMakeArray(
62+
FormulaType<TI> pIndexType, FormulaType<TE> pElementType, Integer defaultElement) {
63+
var arraySort = toSolverType(FormulaType.getArrayType(pIndexType, pElementType));
64+
var constantArray = constCache.get(arraySort, defaultElement);
65+
if (constantArray == null) {
66+
constantArray =
67+
yices_lambda(1, new int[] {yices_new_variable(toSolverType(pIndexType))}, defaultElement);
68+
constCache.put(arraySort, defaultElement, constantArray);
69+
}
70+
return constantArray;
71+
}
72+
73+
@Override
74+
protected Integer equivalence(Integer pArray1, Integer pArray2) {
75+
return yices_eq(pArray1, pArray2);
76+
}
77+
}

‎src/org/sosy_lab/java_smt/solvers/yices2/Yices2Formula.java‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,12 +8,15 @@
88

99
package org.sosy_lab.java_smt.solvers.yices2;
1010

11+
import static com.google.common.base.Preconditions.checkNotNull;
1112
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_to_string;
1213

1314
import com.google.errorprone.annotations.Immutable;
15+
import org.sosy_lab.java_smt.api.ArrayFormula;
1416
import org.sosy_lab.java_smt.api.BitvectorFormula;
1517
import org.sosy_lab.java_smt.api.BooleanFormula;
1618
import org.sosy_lab.java_smt.api.Formula;
19+
import org.sosy_lab.java_smt.api.FormulaType;
1720
import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
1821
import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
1922

@@ -78,4 +81,27 @@ static final class Yices2BooleanFormula extends Yices2Formula implements Boolean
7881
super(pTerm);
7982
}
8083
}
84+
85+
@SuppressWarnings({"ClassTypeParameterName", "MethodTypeParameterName"})
86+
@Immutable
87+
static final class Yices2ArrayFormula<TI extends Formula, TE extends Formula>
88+
extends Yices2Formula implements ArrayFormula<TI, TE> {
89+
90+
private final FormulaType<TI> indexType;
91+
private final FormulaType<TE> elementType;
92+
93+
Yices2ArrayFormula(Integer info, FormulaType<TI> pIndexType, FormulaType<TE> pElementType) {
94+
super(info);
95+
this.indexType = checkNotNull(pIndexType);
96+
this.elementType = checkNotNull(pElementType);
97+
}
98+
99+
public FormulaType<TI> getIndexType() {
100+
return indexType;
101+
}
102+
103+
public FormulaType<TE> getElementType() {
104+
return elementType;
105+
}
106+
}
81107
}

‎src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java‎

Lines changed: 105 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARITH_CONST;
1616
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARITH_GE_ATOM;
1717
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARITH_SUM;
18+
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARRAY_SELECT;
1819
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_BIT_TERM;
1920
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_BOOL_CONST;
2021
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_BV_ARRAY;
@@ -41,12 +42,14 @@
4142
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_IMOD;
4243
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_IS_INT_ATOM;
4344
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ITE_TERM;
45+
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_LAMBDA_TERM;
4446
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_NOT_TERM;
4547
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_OR_TERM;
4648
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_POWER_PRODUCT;
4749
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_RDIV;
4850
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_SELECT_TERM;
4951
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_UNINTERPRETED_TERM;
52+
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_UPDATE_TERM;
5053
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_VARIABLE;
5154
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_XOR_TERM;
5255
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_abs;
@@ -111,16 +114,19 @@
111114
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_bitsize;
112115
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_child;
113116
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_constructor;
114-
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_is_bitvector;
115-
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_is_bool;
116117
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_is_int;
117-
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_is_real;
118118
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_num_children;
119119
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_to_string;
120120
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_true;
121+
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_child;
121122
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_is_bitvector;
123+
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_is_bool;
124+
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_is_function;
125+
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_is_int;
126+
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_is_real;
122127
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_of_term;
123128
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_to_string;
129+
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_update;
124130
import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_xor;
125131

126132
import com.google.common.base.Joiner;
@@ -136,24 +142,30 @@
136142
import java.math.BigInteger;
137143
import java.util.ArrayList;
138144
import java.util.Arrays;
145+
import java.util.HashSet;
139146
import java.util.List;
147+
import java.util.Set;
140148
import java.util.stream.Collectors;
141149
import org.sosy_lab.common.rationals.Rational;
150+
import org.sosy_lab.java_smt.api.ArrayFormula;
142151
import org.sosy_lab.java_smt.api.BitvectorFormula;
143152
import org.sosy_lab.java_smt.api.BooleanFormula;
144153
import org.sosy_lab.java_smt.api.Formula;
145154
import org.sosy_lab.java_smt.api.FormulaType;
155+
import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType;
146156
import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
147157
import org.sosy_lab.java_smt.api.FunctionDeclarationKind;
148158
import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier;
149159
import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
150160
import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
151161
import org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl;
162+
import org.sosy_lab.java_smt.solvers.yices2.Yices2Formula.Yices2ArrayFormula;
152163
import org.sosy_lab.java_smt.solvers.yices2.Yices2Formula.Yices2BitvectorFormula;
153164
import org.sosy_lab.java_smt.solvers.yices2.Yices2Formula.Yices2BooleanFormula;
154165
import org.sosy_lab.java_smt.solvers.yices2.Yices2Formula.Yices2IntegerFormula;
155166
import org.sosy_lab.java_smt.solvers.yices2.Yices2Formula.Yices2RationalFormula;
156167

168+
@SuppressWarnings({"ClassTypeParameterName", "MethodTypeParameterName"})
157169
public class Yices2FormulaCreator extends FormulaCreator<Integer, Integer, Long, Integer> {
158170

159171
private static final ImmutableSet<Integer> CONSTANT_AND_VARIABLE_CONSTRUCTORS =
@@ -170,6 +182,14 @@ public class Yices2FormulaCreator extends FormulaCreator<Integer, Integer, Long,
170182
*/
171183
private final Table<String, Integer, Integer> formulaCache = HashBasedTable.create();
172184

185+
/**
186+
* List of all UF function declarations.
187+
*
188+
* <p>We need this in the visitor to tell the difference between functions and arrays. Both are
189+
* modeled internally by function terms.
190+
*/
191+
private final Set<Integer> ufSymbols = new HashSet<>();
192+
173193
protected Yices2FormulaCreator() {
174194
super(null, yices_bool_type(), yices_int_type(), yices_real_type(), null, null);
175195
}
@@ -186,7 +206,7 @@ public Integer getFloatingPointType(FloatingPointType pType) {
186206

187207
@Override
188208
public Integer getArrayType(Integer pIndexType, Integer pElementType) {
189-
throw new UnsupportedOperationException();
209+
return yices_function_type(1, new int[] {pIndexType}, pElementType);
190210
}
191211

192212
@Override
@@ -199,6 +219,20 @@ public Integer extractInfo(Formula pT) {
199219
return Yices2FormulaManager.getYicesTerm(pT);
200220
}
201221

222+
@Override
223+
@SuppressWarnings("unchecked")
224+
protected <TI extends Formula, TE extends Formula> FormulaType<TE> getArrayFormulaElementType(
225+
ArrayFormula<TI, TE> pArray) {
226+
return ((Yices2ArrayFormula<TI, TE>) pArray).getElementType();
227+
}
228+
229+
@Override
230+
@SuppressWarnings("unchecked")
231+
protected <TI extends Formula, TE extends Formula> FormulaType<TI> getArrayFormulaIndexType(
232+
ArrayFormula<TI, TE> pArray) {
233+
return ((Yices2ArrayFormula<TI, TE>) pArray).getIndexType();
234+
}
235+
202236
@SuppressWarnings("unchecked")
203237
@Override
204238
public <T extends Formula> T encapsulate(FormulaType<T> pType, Integer pTerm) {
@@ -219,6 +253,10 @@ public <T extends Formula> T encapsulate(FormulaType<T> pType, Integer pTerm) {
219253
return (T) new Yices2RationalFormula(pTerm);
220254
} else if (pType.isBitvectorType()) {
221255
return (T) new Yices2BitvectorFormula(pTerm);
256+
} else if (pType.isArrayType()) {
257+
var range = ((ArrayFormulaType<?, ?>) pType).getElementType();
258+
var dom = ((ArrayFormulaType<?, ?>) pType).getIndexType();
259+
return (T) encapsulateArray(pTerm, dom, range);
222260
}
223261
throw new IllegalArgumentException("Cannot create formulas of type " + pType + " in Yices");
224262
}
@@ -235,32 +273,51 @@ public BitvectorFormula encapsulateBitvector(Integer pTerm) {
235273
return new Yices2BitvectorFormula(pTerm);
236274
}
237275

276+
@Override
277+
protected <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> encapsulateArray(
278+
Integer pTerm, FormulaType<TI> pIndexType, FormulaType<TE> pElementType) {
279+
checkArgument(
280+
getFormulaType(pTerm).equals(FormulaType.getArrayType(pIndexType, pElementType)),
281+
"Array formula has unexpected type: %s",
282+
getFormulaType(pTerm));
283+
return new Yices2Formula.Yices2ArrayFormula<>(pTerm, pIndexType, pElementType);
284+
}
285+
238286
@SuppressWarnings("unchecked")
239287
@Override
240288
public <T extends Formula> FormulaType<T> getFormulaType(T pFormula) {
241289
if (pFormula instanceof BitvectorFormula) {
242290
int type = yices_type_of_term(extractInfo(pFormula));
243291
return (FormulaType<T>) FormulaType.getBitvectorTypeWithSize(yices_bvtype_size(type));
292+
} else if (pFormula instanceof ArrayFormula) {
293+
return (FormulaType<T>) convertType(yices_type_of_term(extractInfo(pFormula)));
244294
} else {
245295
return super.getFormulaType(pFormula);
246296
}
247297
}
248298

249299
@Override
250300
public FormulaType<?> getFormulaType(Integer pFormula) {
251-
if (yices_term_is_bool(pFormula)) {
301+
return convertType(yices_type_of_term(pFormula));
302+
}
303+
304+
/** Convert from Yices2 types to JavaSMT FormulaTypes. */
305+
private FormulaType<?> convertType(Integer pType) {
306+
if (yices_type_is_bool(pType)) {
252307
return FormulaType.BooleanType;
253-
} else if (yices_term_is_int(pFormula)) {
308+
} else if (yices_type_is_int(pType)) {
254309
return FormulaType.IntegerType;
255-
} else if (yices_term_is_real(pFormula)) {
310+
} else if (yices_type_is_real(pType)) {
256311
return FormulaType.RationalType;
257-
} else if (yices_term_is_bitvector(pFormula)) {
258-
return FormulaType.getBitvectorTypeWithSize(yices_term_bitsize(pFormula));
312+
} else if (yices_type_is_bitvector(pType)) {
313+
return FormulaType.getBitvectorTypeWithSize(yices_bvtype_size(pType));
314+
} else if (yices_type_is_function(pType)) {
315+
var domain = yices_type_child(pType, 0);
316+
var range = yices_type_child(pType, 1);
317+
return FormulaType.getArrayType(convertType(domain), convertType(range));
259318
}
260319
throw new IllegalArgumentException(
261-
String.format(
262-
"Unknown formula type '%s' for formula '%s'",
263-
yices_type_to_string(yices_type_of_term(pFormula)), yices_term_to_string(pFormula)));
320+
String.format("Unknown formula type '%s'", yices_type_to_string(pType)));
264321
}
265322

266323
/** Creates a named, free variable. Might retrieve it from the cache if created prior. */
@@ -335,6 +392,17 @@ public <R> R visit(FormulaVisitor<R> pVisitor, Formula pFormula, Integer pF) {
335392
return pVisitor.visitConstant(pFormula, convertValue(pF, pF));
336393
case YICES_BV_CONST:
337394
return pVisitor.visitConstant(pFormula, convertValue(pF, pF));
395+
case YICES_LAMBDA_TERM:
396+
// We use lambda terms as array constants
397+
return pVisitor.visitFunction(
398+
pFormula,
399+
ImmutableList.of(encapsulateWithTypeOf(yices_term_child(pF, 1))),
400+
FunctionDeclarationImpl.of(
401+
"const",
402+
FunctionDeclarationKind.CONST,
403+
ImmutableList.of(getFormulaType(yices_term_child(pF, 1))),
404+
getFormulaType(pF),
405+
0));
338406
case YICES_UNINTERPRETED_TERM:
339407
return pVisitor.visitFreeVariable(pFormula, yices_get_term_name(pF));
340408
case YICES_VARIABLE:
@@ -398,11 +466,26 @@ private <R> R visitFunctionApplication(
398466
functionKind = FunctionDeclarationKind.ITE;
399467
break;
400468
case YICES_APP_TERM:
401-
functionKind = FunctionDeclarationKind.UF;
402-
functionArgs = getArgs(pF);
403-
functionName = yices_term_to_string(functionArgs.get(0));
404-
functionDeclaration = functionArgs.get(0);
405-
functionArgs.remove(0);
469+
var fun = yices_term_child(pF, 0);
470+
if (ufSymbols.contains(fun)) {
471+
functionKind = FunctionDeclarationKind.UF;
472+
functionArgs = getArgs(pF);
473+
functionName = yices_get_term_name(functionArgs.get(0));
474+
functionDeclaration = functionArgs.get(0);
475+
functionArgs.remove(0);
476+
} else {
477+
functionKind = FunctionDeclarationKind.SELECT;
478+
functionArgs = getArgs(pF);
479+
functionName = "select";
480+
functionDeclaration = -YICES_ARRAY_SELECT;
481+
}
482+
break;
483+
case YICES_UPDATE_TERM:
484+
functionKind = FunctionDeclarationKind.STORE;
485+
functionArgs =
486+
ImmutableList.of(
487+
yices_term_child(pF, 0), yices_term_child(pF, 1), yices_term_child(pF, 2));
488+
functionDeclaration = -YICES_UPDATE_TERM;
406489
break;
407490
case YICES_EQ_TERM:
408491
functionKind = FunctionDeclarationKind.EQ; // Covers all equivalences
@@ -760,6 +843,10 @@ public Integer callFunctionImpl(Integer pDeclaration, List<Integer> pArgs) {
760843
return yices_bvproduct(pArgs.size(), Ints.toArray(pArgs));
761844
case YICES_AND:
762845
return yices_and(pArgs.size(), Ints.toArray(pArgs));
846+
case YICES_ARRAY_SELECT:
847+
return yices_application(pArgs.get(0), 1, new int[] {pArgs.get(1)});
848+
case YICES_UPDATE_TERM:
849+
return yices_update(pArgs.get(0), 1, new int[] {pArgs.get(1)}, pArgs.get(2));
763850
default:
764851
// TODO add more cases
765852
// if something bad happens here,
@@ -808,6 +895,7 @@ public Integer declareUFImpl(String pName, Integer pReturnType, List<Integer> pA
808895
yicesFuncType = yices_function_type(size, argTypeArray, pReturnType);
809896
}
810897
int uf = createNamedVariable(yicesFuncType, pName);
898+
ufSymbols.add(uf);
811899
return uf;
812900
}
813901

0 commit comments

Comments
 (0)