Skip to content

Commit 640085e

Browse files
schuessfschuessf
committed
Workaround: Duplicate ConstantTermNormalizer
Even though this class is present in SMTInterpol, it is only used by Ultimate and it was modified to fix a bug (see ddd1310 and 6d19ff8). Therefore, it was copied to Library-SmtLibUtils and SMTSolverBridge (it has to be duplicated, as there is no matching common import of those and they cannot imported by each other because of cyclic dependenices). But the long term solution should be to fix ConstantTermNormalizer in SMTInterpol, i.e., ultimate-pa/smtinterpol#150 should be revisited and merged.
1 parent 5db40c8 commit 640085e

File tree

5 files changed

+180
-47
lines changed

5 files changed

+180
-47
lines changed

‎trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/transformulatransformers/CommuHashPreprocessor.java‎

Lines changed: 2 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -26,18 +26,13 @@
2626
*/
2727
package de.uni_freiburg.informatik.ultimate.icfgtransformer.transformulatransformers;
2828

29-
import java.math.BigDecimal;
30-
import java.math.BigInteger;
31-
3229
import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider;
3330
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.ModifiableTransFormula;
3431
import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.CommuhashNormalForm;
32+
import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ConstantTermNormalizer;
3533
import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ManagedScript;
36-
import de.uni_freiburg.informatik.ultimate.logic.ConstantTerm;
37-
import de.uni_freiburg.informatik.ultimate.logic.Rational;
3834
import de.uni_freiburg.informatik.ultimate.logic.Script;
3935
import de.uni_freiburg.informatik.ultimate.logic.Term;
40-
import de.uni_freiburg.informatik.ultimate.logic.TermTransformer;
4136

4237
/**
4338
* Use CommuhashNormalForm to simplify TransformulaLR
@@ -67,47 +62,9 @@ public boolean checkSoundness(final Script script, final ModifiableTransFormula
6762
@Override
6863
public ModifiableTransFormula process(final ManagedScript script, final ModifiableTransFormula tf)
6964
throws TermException {
70-
final Term normalized1 = (new ConstantTermNormalizer2()).transform(tf.getFormula());
65+
final Term normalized1 = (new ConstantTermNormalizer()).transform(tf.getFormula());
7166
final Term normalized2 = (new CommuhashNormalForm(mServices, script.getScript())).transform(normalized1);
7267
tf.setFormula(normalized2);
7368
return tf;
7469
}
75-
76-
/*
77-
* This class was copied from the package. de.uni_freiburg.informatik.ultimate.smtinterpol.model FIXME: Proper
78-
* solution.
79-
*
80-
*/
81-
public static class ConstantTermNormalizer2 extends TermTransformer {
82-
83-
@Override
84-
protected void convert(final Term term) {
85-
if (term instanceof ConstantTerm) {
86-
final ConstantTerm ct = (ConstantTerm) term;
87-
if (ct.getValue() instanceof BigInteger) {
88-
final Rational rat = Rational.valueOf((BigInteger) ct.getValue(), BigInteger.ONE);
89-
setResult(rat.toTerm(term.getSort()));
90-
} else if (ct.getValue() instanceof BigDecimal) {
91-
final BigDecimal decimal = (BigDecimal) ct.getValue();
92-
Rational rat;
93-
if (decimal.scale() <= 0) {
94-
final BigInteger num = decimal.toBigInteger();
95-
rat = Rational.valueOf(num, BigInteger.ONE);
96-
} else {
97-
final BigInteger num = decimal.unscaledValue();
98-
final BigInteger denom = BigInteger.TEN.pow(decimal.scale());
99-
rat = Rational.valueOf(num, denom);
100-
}
101-
setResult(rat.toTerm(term.getSort()));
102-
} else if (ct.getValue() instanceof Rational) {
103-
setResult(ct);
104-
} else {
105-
setResult(term);
106-
}
107-
} else {
108-
super.convert(term);
109-
}
110-
}
111-
112-
}
11370
}

‎trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/ConstantTermNormalizer.java‎

Lines changed: 87 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,87 @@
1+
/*
2+
* Copyright (C) 2024 Matthias Heizmann ([email protected]>)
3+
* Copyright (C) 2024 University of Freiburg
4+
*
5+
* This file is part of the ULTIMATE ModelCheckerUtils Library.
6+
*
7+
* The ULTIMATE ModelCheckerUtils Library is free software: you can redistribute it and/or modify
8+
* it under the terms of the GNU Lesser General Public License as published
9+
* by the Free Software Foundation, either version 3 of the License, or
10+
* (at your option) any later version.
11+
*
12+
* The ULTIMATE ModelCheckerUtils Library is distributed in the hope that it will be useful,
13+
* but WITHOUT ANY WARRANTY; without even the implied warranty of
14+
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15+
* GNU Lesser General Public License for more details.
16+
*
17+
* You should have received a copy of the GNU Lesser General Public License
18+
* along with the ULTIMATE ModelCheckerUtils Library. If not, see <http://www.gnu.org/licenses/>.
19+
*
20+
* Additional permission under GNU GPL version 3 section 7:
21+
* If you modify the ULTIMATE ModelCheckerUtils Library, or any covered work, by linking
22+
* or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
23+
* containing parts covered by the terms of the Eclipse Public License, the
24+
* licensors of the ULTIMATE ModelCheckerUtils Library grant you additional permission
25+
* to convey the resulting work.
26+
*/
27+
package de.uni_freiburg.informatik.ultimate.lib.smtlibutils;
28+
29+
import java.math.BigDecimal;
30+
import java.math.BigInteger;
31+
32+
import de.uni_freiburg.informatik.ultimate.logic.ConstantTerm;
33+
import de.uni_freiburg.informatik.ultimate.logic.Rational;
34+
import de.uni_freiburg.informatik.ultimate.logic.Term;
35+
import de.uni_freiburg.informatik.ultimate.logic.TermTransformer;
36+
37+
/**
38+
* {@link ConstantTerm}s that have numeric sort (Int, Real) can represent their value either as {@link BigInteger},
39+
* {@link BigDecimal}, or {@link Rational}. This class helps us to establish a normal form in which values are always
40+
* represented by {@link Rational}s.
41+
*
42+
* @author Matthias Heizmann ([email protected]>)
43+
*
44+
*/
45+
public class ConstantTermNormalizer extends TermTransformer {
46+
47+
@Override
48+
protected void convert(final Term term) {
49+
if (term instanceof ConstantTerm) {
50+
final Term res;
51+
final ConstantTerm ct = (ConstantTerm) term;
52+
res = convertConstantTerm(term, ct);
53+
setResult(res);
54+
} else {
55+
super.convert(term);
56+
}
57+
}
58+
59+
private static Term convertConstantTerm(final Term term, final ConstantTerm ct) {
60+
if (!ct.getSort().isNumericSort()) {
61+
// do nothing, only applicable to numeric sorts
62+
return ct;
63+
}
64+
if (ct.getValue() instanceof BigInteger) {
65+
final Rational rat = Rational.valueOf((BigInteger) ct.getValue(), BigInteger.ONE);
66+
return rat.toTerm(term.getSort());
67+
} else if (ct.getValue() instanceof BigDecimal) {
68+
final BigDecimal decimal = (BigDecimal) ct.getValue();
69+
Rational rat;
70+
if (decimal.scale() <= 0) {
71+
final BigInteger num = decimal.toBigInteger();
72+
rat = Rational.valueOf(num, BigInteger.ONE);
73+
} else {
74+
final BigInteger num = decimal.unscaledValue();
75+
final BigInteger denom = BigInteger.TEN.pow(decimal.scale());
76+
rat = Rational.valueOf(num, denom);
77+
}
78+
return rat.toTerm(term.getSort());
79+
} else if (ct.getValue() instanceof Rational) {
80+
// do nothing, already in normal form
81+
return ct;
82+
} else {
83+
throw new AssertionError("Value has to be either BigInteger, Decimal, or Rational");
84+
}
85+
}
86+
87+
}

‎trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/singletracecheck/NestedInterpolantsBuilder.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,7 @@
5252
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IPredicateUnifier;
5353
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.SPredicate;
5454
import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.scripttransfer.TermTransferrer;
55+
import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ConstantTermNormalizer;
5556
import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.DebugMessage;
5657
import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ManagedScript;
5758
import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.SmtUtils;
@@ -72,7 +73,6 @@
7273
import de.uni_freiburg.informatik.ultimate.logic.Term;
7374
import de.uni_freiburg.informatik.ultimate.logic.TermVariable;
7475
import de.uni_freiburg.informatik.ultimate.logic.Util;
75-
import de.uni_freiburg.informatik.ultimate.smtinterpol.model.ConstantTermNormalizer;
7676
import de.uni_freiburg.informatik.ultimate.util.CoreUtil;
7777
import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple;
7878

‎trunk/source/SMTSolverBridge/src/de/uni_freiburg/informatik/ultimate/smtsolver/external/ConstantTermNormalizer.java‎

Lines changed: 90 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
/*
2+
* Copyright (C) 2024 Matthias Heizmann ([email protected]>)
3+
* Copyright (C) 2024 University of Freiburg
4+
*
5+
* This file is part of the ULTIMATE ModelCheckerUtils Library.
6+
*
7+
* The ULTIMATE ModelCheckerUtils Library is free software: you can redistribute it and/or modify
8+
* it under the terms of the GNU Lesser General Public License as published
9+
* by the Free Software Foundation, either version 3 of the License, or
10+
* (at your option) any later version.
11+
*
12+
* The ULTIMATE ModelCheckerUtils Library is distributed in the hope that it will be useful,
13+
* but WITHOUT ANY WARRANTY; without even the implied warranty of
14+
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15+
* GNU Lesser General Public License for more details.
16+
*
17+
* You should have received a copy of the GNU Lesser General Public License
18+
* along with the ULTIMATE ModelCheckerUtils Library. If not, see <http://www.gnu.org/licenses/>.
19+
*
20+
* Additional permission under GNU GPL version 3 section 7:
21+
* If you modify the ULTIMATE ModelCheckerUtils Library, or any covered work, by linking
22+
* or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
23+
* containing parts covered by the terms of the Eclipse Public License, the
24+
* licensors of the ULTIMATE ModelCheckerUtils Library grant you additional permission
25+
* to convey the resulting work.
26+
*/
27+
package de.uni_freiburg.informatik.ultimate.smtsolver.external;
28+
29+
import java.math.BigDecimal;
30+
import java.math.BigInteger;
31+
32+
import de.uni_freiburg.informatik.ultimate.logic.ConstantTerm;
33+
import de.uni_freiburg.informatik.ultimate.logic.Rational;
34+
import de.uni_freiburg.informatik.ultimate.logic.Term;
35+
import de.uni_freiburg.informatik.ultimate.logic.TermTransformer;
36+
37+
/**
38+
* {@link ConstantTerm}s that have numeric sort (Int, Real) can represent their value either as {@link BigInteger},
39+
* {@link BigDecimal}, or {@link Rational}. This class helps us to establish a normal form in which values are always
40+
* represented by {@link Rational}s.
41+
*
42+
* @author Matthias Heizmann ([email protected]>)
43+
*
44+
*/
45+
46+
// TODO: This class is just a copy from Library-SmtLibUtils, as it cannot be imported here!
47+
// Instead, this class should be fixed in SMTInterpol and removed from Ultimate.
48+
public class ConstantTermNormalizer extends TermTransformer {
49+
50+
@Override
51+
protected void convert(final Term term) {
52+
if (term instanceof ConstantTerm) {
53+
final Term res;
54+
final ConstantTerm ct = (ConstantTerm) term;
55+
res = convertConstantTerm(term, ct);
56+
setResult(res);
57+
} else {
58+
super.convert(term);
59+
}
60+
}
61+
62+
private static Term convertConstantTerm(final Term term, final ConstantTerm ct) {
63+
if (!ct.getSort().isNumericSort()) {
64+
// do nothing, only applicable to numeric sorts
65+
return ct;
66+
}
67+
if (ct.getValue() instanceof BigInteger) {
68+
final Rational rat = Rational.valueOf((BigInteger) ct.getValue(), BigInteger.ONE);
69+
return rat.toTerm(term.getSort());
70+
} else if (ct.getValue() instanceof BigDecimal) {
71+
final BigDecimal decimal = (BigDecimal) ct.getValue();
72+
Rational rat;
73+
if (decimal.scale() <= 0) {
74+
final BigInteger num = decimal.toBigInteger();
75+
rat = Rational.valueOf(num, BigInteger.ONE);
76+
} else {
77+
final BigInteger num = decimal.unscaledValue();
78+
final BigInteger denom = BigInteger.TEN.pow(decimal.scale());
79+
rat = Rational.valueOf(num, denom);
80+
}
81+
return rat.toTerm(term.getSort());
82+
} else if (ct.getValue() instanceof Rational) {
83+
// do nothing, already in normal form
84+
return ct;
85+
} else {
86+
throw new AssertionError("Value has to be either BigInteger, Decimal, or Rational");
87+
}
88+
}
89+
90+
}

‎trunk/source/SMTSolverBridge/src/de/uni_freiburg/informatik/ultimate/smtsolver/external/TermParseUtils.java‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,6 @@
3737
import de.uni_freiburg.informatik.ultimate.logic.Script;
3838
import de.uni_freiburg.informatik.ultimate.logic.Term;
3939
import de.uni_freiburg.informatik.ultimate.logic.TermVariable;
40-
import de.uni_freiburg.informatik.ultimate.smtinterpol.model.ConstantTermNormalizer;
4140

4241
/**
4342
* Class that provides auxiliary methods for transforming Strings into SMT- {@link Term}s.

0 commit comments

Comments
 (0)