Skip to content

Commit e6a45ac

Browse files
kfriedbergerkfriedberger
authored
Merge pull request #466 from sosy-lab/461-z3-fails-when-given-mixed-integer-real-arguments-for-division
Add explicit cast in mixed integer-real term
2 parents c9b34d4 + a26e5dc commit e6a45ac

11 files changed

+418
-68
lines changed

‎src/org/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager.java

+19-8
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
// an API wrapper for a collection of SMT solvers:
33
// https://github.com/sosy-lab/java-smt
44
//
5-
// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
5+
// SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
66
//
77
// SPDX-License-Identifier: Apache-2.0
88

@@ -17,6 +17,7 @@
1717
import java.math.BigDecimal;
1818
import java.math.BigInteger;
1919
import java.util.List;
20+
import java.util.stream.Collectors;
2021
import org.sosy_lab.common.rationals.Rational;
2122
import org.sosy_lab.java_smt.api.BooleanFormula;
2223
import org.sosy_lab.java_smt.api.Formula;
@@ -180,7 +181,7 @@ public ResultFormulaType makeVariable(String pVar) {
180181
@Override
181182
public ResultFormulaType negate(ParamFormulaType pNumber) {
182183
TFormulaInfo param1 = extractInfo(pNumber);
183-
return wrap(negate(param1));
184+
return wrap(negate(toType(param1)));
184185
}
185186

186187
protected abstract TFormulaInfo negate(TFormulaInfo pParam1);
@@ -190,14 +191,19 @@ public ResultFormulaType add(ParamFormulaType pNumber1, ParamFormulaType pNumber
190191
TFormulaInfo param1 = extractInfo(pNumber1);
191192
TFormulaInfo param2 = extractInfo(pNumber2);
192193

193-
return wrap(add(param1, param2));
194+
return wrap(add(toType(param1), toType(param2)));
194195
}
195196

196197
protected abstract TFormulaInfo add(TFormulaInfo pParam1, TFormulaInfo pParam2);
197198

198199
@Override
199200
public ResultFormulaType sum(List<ParamFormulaType> operands) {
200-
return wrap(sumImpl(Lists.transform(operands, this::extractInfo)));
201+
return wrap(
202+
sumImpl(
203+
operands.stream()
204+
.map(this::extractInfo)
205+
.map(this::toType)
206+
.collect(Collectors.toList())));
201207
}
202208

203209
protected TFormulaInfo sumImpl(List<TFormulaInfo> operands) {
@@ -213,7 +219,7 @@ public ResultFormulaType subtract(ParamFormulaType pNumber1, ParamFormulaType pN
213219
TFormulaInfo param1 = extractInfo(pNumber1);
214220
TFormulaInfo param2 = extractInfo(pNumber2);
215221

216-
return wrap(subtract(param1, param2));
222+
return wrap(subtract(toType(param1), toType(param2)));
217223
}
218224

219225
protected abstract TFormulaInfo subtract(TFormulaInfo pParam1, TFormulaInfo pParam2);
@@ -231,7 +237,7 @@ public ResultFormulaType divide(ParamFormulaType pNumber1, ParamFormulaType pNum
231237
result = makeUf(divUfDecl, param1, param2);
232238
} else {
233239
try {
234-
result = divide(param1, param2);
240+
result = divide(toType(param1), toType(param2));
235241
} catch (UnsupportedOperationException e) {
236242
if (nonLinearArithmetic == NonLinearArithmetic.APPROXIMATE_FALLBACK) {
237243
result = makeUf(divUfDecl, param1, param2);
@@ -263,7 +269,7 @@ public ResultFormulaType modulo(ParamFormulaType pNumber1, ParamFormulaType pNum
263269
result = makeUf(modUfDecl, param1, param2);
264270
} else {
265271
try {
266-
result = modulo(param1, param2);
272+
result = modulo(toType(param1), toType(param2));
267273
} catch (UnsupportedOperationException e) {
268274
if (nonLinearArithmetic == NonLinearArithmetic.APPROXIMATE_FALLBACK) {
269275
result = makeUf(modUfDecl, param1, param2);
@@ -337,7 +343,7 @@ public ResultFormulaType multiply(ParamFormulaType pNumber1, ParamFormulaType pN
337343
result = makeUf(multUfDecl, param1, param2);
338344
} else {
339345
try {
340-
result = multiply(param1, param2);
346+
result = multiply(toType(param1), toType(param2));
341347
} catch (UnsupportedOperationException e) {
342348
if (nonLinearArithmetic == NonLinearArithmetic.APPROXIMATE_FALLBACK) {
343349
result = makeUf(multUfDecl, param1, param2);
@@ -434,4 +440,9 @@ protected TFormulaInfo floor(TFormulaInfo number) {
434440
"method should only be called for RationalFormulae, but type is "
435441
+ getFormulaCreator().getFormulaType(number));
436442
}
443+
444+
/** Make sure the value is of correct type (Int vs. Real) and add a cast if necessary. */
445+
protected TFormulaInfo toType(TFormulaInfo param) {
446+
return param;
447+
}
437448
}

‎src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NumeralFormulaManager.java

+3-2
Original file line numberDiff line numberDiff line change
@@ -163,7 +163,7 @@ protected Term subtract(Term pParam1, Term pParam2) {
163163

164164
@Override
165165
protected Term equal(Term pParam1, Term pParam2) {
166-
return termManager.mkTerm(Kind.EQUAL, pParam1, pParam2);
166+
return termManager.mkTerm(Kind.EQUAL, toType(pParam1), toType(pParam2));
167167
}
168168

169169
@Override
@@ -191,7 +191,8 @@ protected Term distinctImpl(List<Term> pParam) {
191191
if (pParam.size() < 2) {
192192
return termManager.mkTrue();
193193
} else {
194-
return termManager.mkTerm(Kind.DISTINCT, pParam.toArray(new Term[0]));
194+
return termManager.mkTerm(
195+
Kind.DISTINCT, pParam.stream().map(this::toType).toArray(Term[]::new));
195196
}
196197
}
197198
}

‎src/org/sosy_lab/java_smt/solvers/cvc5/CVC5RationalFormulaManager.java

+6-1
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
// an API wrapper for a collection of SMT solvers:
33
// https://github.com/sosy-lab/java-smt
44
//
5-
// SPDX-FileCopyrightText: 2022 Dirk Beyer <https://www.sosy-lab.org>
5+
// SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
66
//
77
// SPDX-License-Identifier: Apache-2.0
88

@@ -40,6 +40,11 @@ protected Term makeNumberImpl(BigDecimal pNumber) {
4040
return makeNumberImpl(pNumber.toPlainString());
4141
}
4242

43+
@Override
44+
protected Term toType(Term pNumber) {
45+
return pNumber.getSort().isInteger() ? termManager.mkTerm(Kind.TO_REAL, pNumber) : pNumber;
46+
}
47+
4348
@Override
4449
public Term divide(Term pParam1, Term pParam2) {
4550
return termManager.mkTerm(Kind.DIVISION, pParam1, pParam2);

‎src/org/sosy_lab/java_smt/solvers/princess/PrincessIntegerFormulaManager.java

+36
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@
1010

1111
import ap.basetypes.IdealInt;
1212
import ap.parser.IExpression;
13+
import ap.parser.IFormula;
1314
import ap.parser.IIntLit;
1415
import ap.parser.ITerm;
1516
import ap.theories.nia.GroebnerMultiplication;
@@ -105,4 +106,39 @@ protected boolean isNumeral(IExpression val) {
105106
protected IExpression floor(IExpression pNumber) {
106107
return pNumber; // identity for integers
107108
}
109+
110+
@Override
111+
protected ITerm negate(IExpression pNumber) {
112+
return ((ITerm) pNumber).unary_$minus();
113+
}
114+
115+
@Override
116+
protected ITerm add(IExpression pNumber1, IExpression pNumber2) {
117+
return ((ITerm) pNumber1).$plus((ITerm) pNumber2);
118+
}
119+
120+
@Override
121+
protected ITerm subtract(IExpression pNumber1, IExpression pNumber2) {
122+
return ((ITerm) pNumber1).$minus((ITerm) pNumber2);
123+
}
124+
125+
@Override
126+
protected IFormula greaterThan(IExpression pNumber1, IExpression pNumber2) {
127+
return ((ITerm) pNumber1).$greater((ITerm) pNumber2);
128+
}
129+
130+
@Override
131+
protected IFormula greaterOrEquals(IExpression pNumber1, IExpression pNumber2) {
132+
return ((ITerm) pNumber1).$greater$eq((ITerm) pNumber2);
133+
}
134+
135+
@Override
136+
protected IFormula lessThan(IExpression pNumber1, IExpression pNumber2) {
137+
return ((ITerm) pNumber1).$less((ITerm) pNumber2);
138+
}
139+
140+
@Override
141+
protected IFormula lessOrEquals(IExpression pNumber1, IExpression pNumber2) {
142+
return ((ITerm) pNumber1).$less$eq((ITerm) pNumber2);
143+
}
108144
}

‎src/org/sosy_lab/java_smt/solvers/princess/PrincessNumeralFormulaManager.java

-35
Original file line numberDiff line numberDiff line change
@@ -35,21 +35,6 @@ abstract class PrincessNumeralFormulaManager<
3535
super(pCreator, pNonLinearArithmetic);
3636
}
3737

38-
@Override
39-
protected ITerm negate(IExpression pNumber) {
40-
return ((ITerm) pNumber).unary_$minus();
41-
}
42-
43-
@Override
44-
protected ITerm add(IExpression pNumber1, IExpression pNumber2) {
45-
return ((ITerm) pNumber1).$plus((ITerm) pNumber2);
46-
}
47-
48-
@Override
49-
protected ITerm subtract(IExpression pNumber1, IExpression pNumber2) {
50-
return ((ITerm) pNumber1).$minus((ITerm) pNumber2);
51-
}
52-
5338
@Override
5439
protected IFormula equal(IExpression pNumber1, IExpression pNumber2) {
5540
return ((ITerm) pNumber1).$eq$eq$eq((ITerm) pNumber2);
@@ -59,24 +44,4 @@ protected IFormula equal(IExpression pNumber1, IExpression pNumber2) {
5944
protected IExpression distinctImpl(List<IExpression> pNumbers) {
6045
return IExpression.distinct(asScala(Iterables.filter(pNumbers, ITerm.class)));
6146
}
62-
63-
@Override
64-
protected IFormula greaterThan(IExpression pNumber1, IExpression pNumber2) {
65-
return ((ITerm) pNumber1).$greater((ITerm) pNumber2);
66-
}
67-
68-
@Override
69-
protected IFormula greaterOrEquals(IExpression pNumber1, IExpression pNumber2) {
70-
return ((ITerm) pNumber1).$greater$eq((ITerm) pNumber2);
71-
}
72-
73-
@Override
74-
protected IFormula lessThan(IExpression pNumber1, IExpression pNumber2) {
75-
return ((ITerm) pNumber1).$less((ITerm) pNumber2);
76-
}
77-
78-
@Override
79-
protected IFormula lessOrEquals(IExpression pNumber1, IExpression pNumber2) {
80-
return ((ITerm) pNumber1).$less$eq((ITerm) pNumber2);
81-
}
8247
}

‎src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java

+58-16
Original file line numberDiff line numberDiff line change
@@ -8,17 +8,17 @@
88

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

11-
import ap.basetypes.IdealInt;
1211
import ap.parser.IExpression;
12+
import ap.parser.IFormula;
1313
import ap.parser.IFunApp;
14-
import ap.parser.IIntLit;
1514
import ap.parser.ITerm;
15+
import ap.theories.rationals.Rationals;
1616
import com.google.common.collect.ImmutableList;
1717
import java.math.BigDecimal;
1818
import java.math.BigInteger;
1919
import java.util.List;
20+
import java.util.stream.Collectors;
2021
import org.sosy_lab.common.rationals.Rational;
21-
import org.sosy_lab.java_smt.api.FormulaType;
2222
import org.sosy_lab.java_smt.api.NumeralFormula;
2323
import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
2424
import org.sosy_lab.java_smt.api.RationalFormulaManager;
@@ -107,30 +107,72 @@ protected IExpression makeVariableImpl(String varName) {
107107
return getFormulaCreator().makeVariable(PrincessEnvironment.FRACTION_SORT, varName);
108108
}
109109

110+
@Override
111+
protected ITerm toType(IExpression param) {
112+
ITerm number = (ITerm) param;
113+
return formulaCreator.getFormulaType(number).isIntegerType()
114+
? Rationals.int2ring(number)
115+
: number;
116+
}
117+
110118
@Override
111119
protected IExpression floor(IExpression number) {
112120
throw new UnsupportedOperationException("floor is not supported in Princess");
113121
}
114122

115123
@Override
116-
protected IExpression multiply(IExpression number1, IExpression number2) {
117-
FormulaType<?> sort1 = getFormulaCreator().getFormulaType(number1);
118-
FormulaType<?> sort2 = getFormulaCreator().getFormulaType(number1);
124+
protected ITerm negate(IExpression number) {
125+
return Rationals.minus(toType(number));
126+
}
119127

120-
IExpression result = PrincessEnvironment.rationalTheory.mul((ITerm) number1, (ITerm) number2);
128+
@Override
129+
protected ITerm add(IExpression number1, IExpression number2) {
130+
return Rationals.plus(toType(number1), toType(number2));
131+
}
121132

122-
if (result instanceof IIntLit && ((IIntLit) result).value().equals(IdealInt.apply(0))) {
123-
// If the result is (integer) zero we may have lost our type
124-
// Check the type of both arguments and convert the result back to rational if needed
125-
if (sort1.isRationalType() || sort2.isRationalType()) {
126-
result = PrincessEnvironment.rationalTheory.int2ring((IIntLit) result);
127-
}
128-
}
129-
return result;
133+
@Override
134+
protected ITerm subtract(IExpression number1, IExpression number2) {
135+
return Rationals.minus(toType(number1), toType(number2));
136+
}
137+
138+
@Override
139+
protected IExpression multiply(IExpression number1, IExpression number2) {
140+
return Rationals.mul(toType(number1), toType(number2));
130141
}
131142

132143
@Override
133144
protected IExpression divide(IExpression number1, IExpression number2) {
134-
return PrincessEnvironment.rationalTheory.div((ITerm) number1, (ITerm) number2);
145+
return Rationals.div(toType(number1), toType(number2));
146+
}
147+
148+
@Override
149+
protected IFormula equal(IExpression number1, IExpression number2) {
150+
return super.equal(toType(number1), toType(number2));
151+
}
152+
153+
@Override
154+
protected IExpression distinctImpl(List<IExpression> operands) {
155+
List<IExpression> castedOps = operands.stream().map(this::toType).collect(Collectors.toList());
156+
return super.distinctImpl(castedOps);
157+
}
158+
159+
@Override
160+
protected IFormula greaterThan(IExpression number1, IExpression number2) {
161+
return Rationals.gt(toType(number1), toType(number2));
162+
}
163+
164+
@Override
165+
protected IFormula greaterOrEquals(IExpression number1, IExpression number2) {
166+
return Rationals.geq(toType(number1), toType(number2));
167+
}
168+
169+
@Override
170+
protected IFormula lessThan(IExpression number1, IExpression number2) {
171+
return Rationals.lt(toType(number1), toType(number2));
172+
}
173+
174+
@Override
175+
protected IFormula lessOrEquals(IExpression number1, IExpression number2) {
176+
return Rationals.leq(toType(number1), toType(number2));
135177
}
136178
}

‎src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolNumeralFormulaManager.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ abstract class SmtInterpolNumeralFormulaManager<
3333

3434
/** Operators for arithmetic functions that return a numeric value. */
3535
private static final ImmutableSet<String> NUMERIC_FUNCTIONS =
36-
ImmutableSet.of("+", "-", "*", "/", "div", "mod");
36+
ImmutableSet.of("+", "-", "*", "/", "div", "mod", "to_real");
3737

3838
protected final Script env;
3939

‎src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolRationalFormulaManager.java

+6-4
Original file line numberDiff line numberDiff line change
@@ -65,13 +65,15 @@ protected Term makeVariableImpl(String varName) {
6565
return getFormulaCreator().makeVariable(t, varName);
6666
}
6767

68+
@Override
69+
protected Term toType(Term pNumber) {
70+
Sort intSort = pNumber.getTheory().getNumericSort();
71+
return pNumber.getSort().equals(intSort) ? env.term("to_real", pNumber) : pNumber;
72+
}
73+
6874
@Override
6975
public Term divide(Term pNumber1, Term pNumber2) {
7076
if (consistsOfNumerals(pNumber2)) {
71-
Sort intSort = pNumber1.getTheory().getNumericSort();
72-
Sort realSort = pNumber1.getTheory().getRealSort();
73-
assert intSort.equals(pNumber1.getSort()) || realSort.equals(pNumber1.getSort());
74-
assert intSort.equals(pNumber2.getSort()) || realSort.equals(pNumber2.getSort());
7577
return env.term("/", pNumber1, pNumber2);
7678
} else {
7779
return super.divide(pNumber1, pNumber2);

‎src/org/sosy_lab/java_smt/solvers/z3/Z3RationalFormulaManager.java

+11
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,17 @@ protected Long makeNumberImpl(BigDecimal pNumber) {
3636
return makeNumberImpl(pNumber.toPlainString());
3737
}
3838

39+
@Override
40+
protected Long toType(Long pNumber) {
41+
if (Native.getSort(z3context, pNumber) == formulaCreator.getIntegerType()) {
42+
long castedNumber = Native.mkInt2real(z3context, pNumber);
43+
Native.incRef(z3context, castedNumber);
44+
return castedNumber;
45+
} else {
46+
return pNumber;
47+
}
48+
}
49+
3950
@Override
4051
protected Long floor(Long pNumber) {
4152
return Native.mkReal2int(z3context, pNumber);

0 commit comments

Comments
 (0)