From f8335c26707920b6afc26a9038f29674bd8c5003 Mon Sep 17 00:00:00 2001 From: Matthias Heizmann Date: Sun, 23 Jun 2024 17:41:33 +0200 Subject: [PATCH 1/2] Move ConstantTermNormalizer * Move class ConstantTermNormalizer from SMTInterpol to Library-SMTLIB * Extract method * Add support for new representation of bitvector constants (ConstantTerm with BigInteger value) * Add documentation This class is currently not used by SMTInterpol. However, this class is used by several projects of Ultimate, e.g., by the SMTSolverBridge. Ultimate's projects should not depend on SMTInterpol or the SMTSolverBridge. Hence Ultimate currently duplicates this class to make the code available to its projects. --- .../ultimate/util/ConstantTermNormalizer.java | 80 +++++++++++++++++++ .../model/ConstantTermNormalizer.java | 61 -------------- 2 files changed, 80 insertions(+), 61 deletions(-) create mode 100644 Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/util/ConstantTermNormalizer.java delete mode 100644 SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/model/ConstantTermNormalizer.java diff --git a/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/util/ConstantTermNormalizer.java b/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/util/ConstantTermNormalizer.java new file mode 100644 index 000000000..924ded1d0 --- /dev/null +++ b/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/util/ConstantTermNormalizer.java @@ -0,0 +1,80 @@ +/* + * Copyright (C) 2009-2012 University of Freiburg + * + * This file is part of SMTInterpol. + * + * SMTInterpol is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * SMTInterpol is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with SMTInterpol. If not, see . + */ +package de.uni_freiburg.informatik.ultimate.util; + +import java.math.BigDecimal; +import java.math.BigInteger; + +import de.uni_freiburg.informatik.ultimate.logic.ConstantTerm; +import de.uni_freiburg.informatik.ultimate.logic.Rational; +import de.uni_freiburg.informatik.ultimate.logic.Term; +import de.uni_freiburg.informatik.ultimate.logic.TermTransformer; + +/** + * {@link ConstantTerm}s that have numeric sort (Int, Real) can represent their + * value either as {@link BigInteger}, {@link BigDecimal}, or {@link Rational}. + * This class helps us to establish a normal form in which values are always + * represented by {@link Rational}s. + * + * @author Matthias Heizmann (matthias.heizmann@iste.uni-stuttgart.de>) + * + */ +public class ConstantTermNormalizer extends TermTransformer { + + @Override + protected void convert(final Term term) { + if (term instanceof ConstantTerm) { + final Term res; + final ConstantTerm ct = (ConstantTerm) term; + res = convertConstantTerm(term, ct); + setResult(res); + } else { + super.convert(term); + } + } + + private static Term convertConstantTerm(final Term term, final ConstantTerm ct) { + if (!ct.getSort().isNumericSort()) { + // do nothing, only applicable to numeric sorts + return ct; + } + if (ct.getValue() instanceof BigInteger) { + final Rational rat = Rational.valueOf((BigInteger) ct.getValue(), BigInteger.ONE); + return rat.toTerm(term.getSort()); + } else if (ct.getValue() instanceof BigDecimal) { + final BigDecimal decimal = (BigDecimal) ct.getValue(); + Rational rat; + if (decimal.scale() <= 0) { + final BigInteger num = decimal.toBigInteger(); + rat = Rational.valueOf(num, BigInteger.ONE); + } else { + final BigInteger num = decimal.unscaledValue(); + final BigInteger denom = BigInteger.TEN.pow(decimal.scale()); + rat = Rational.valueOf(num, denom); + } + return rat.toTerm(term.getSort()); + } else if (ct.getValue() instanceof Rational) { + // do nothing, already in normal form + return ct; + } else { + throw new AssertionError("Value has to be either BigInteger, Decimal, or Rational"); + } + } + +} diff --git a/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/model/ConstantTermNormalizer.java b/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/model/ConstantTermNormalizer.java deleted file mode 100644 index 6d28b7183..000000000 --- a/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/model/ConstantTermNormalizer.java +++ /dev/null @@ -1,61 +0,0 @@ -/* - * Copyright (C) 2009-2012 University of Freiburg - * - * This file is part of SMTInterpol. - * - * SMTInterpol is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as published - * by the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * SMTInterpol is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU Lesser General Public License for more details. - * - * You should have received a copy of the GNU Lesser General Public License - * along with SMTInterpol. If not, see . - */ -package de.uni_freiburg.informatik.ultimate.smtinterpol.model; - -import java.math.BigDecimal; -import java.math.BigInteger; - -import de.uni_freiburg.informatik.ultimate.logic.ConstantTerm; -import de.uni_freiburg.informatik.ultimate.logic.Rational; -import de.uni_freiburg.informatik.ultimate.logic.Term; -import de.uni_freiburg.informatik.ultimate.logic.TermTransformer; - -public class ConstantTermNormalizer extends TermTransformer { - - @Override - protected void convert(Term term) { - if (term instanceof ConstantTerm) { - final ConstantTerm ct = (ConstantTerm) term; - if (ct.getValue() instanceof BigInteger) { - final Rational rat = Rational.valueOf( - (BigInteger) ct.getValue(), BigInteger.ONE); - setResult(rat.toTerm(term.getSort())); - } else if (ct.getValue() instanceof BigDecimal) { - final BigDecimal decimal = (BigDecimal) ct.getValue(); - Rational rat; - if (decimal.scale() <= 0) { - final BigInteger num = decimal.toBigInteger(); - rat = Rational.valueOf(num, BigInteger.ONE); - } else { - final BigInteger num = decimal.unscaledValue(); - final BigInteger denom = BigInteger.TEN.pow(decimal.scale()); - rat = Rational.valueOf(num, denom); - } - setResult(rat.toTerm(term.getSort())); - } else if (ct.getValue() instanceof Rational) { - setResult(ct); - } else { - setResult(term); - } - } else { - super.convert(term); - } - } - -} From 4bbdaf91a2209617989b351a873a2524fbaba21c Mon Sep 17 00:00:00 2001 From: Matthias Heizmann Date: Sun, 23 Jun 2024 19:51:44 +0200 Subject: [PATCH 2/2] Reduce number of params --- .../informatik/ultimate/util/ConstantTermNormalizer.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/util/ConstantTermNormalizer.java b/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/util/ConstantTermNormalizer.java index 924ded1d0..38701756d 100644 --- a/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/util/ConstantTermNormalizer.java +++ b/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/util/ConstantTermNormalizer.java @@ -42,21 +42,21 @@ protected void convert(final Term term) { if (term instanceof ConstantTerm) { final Term res; final ConstantTerm ct = (ConstantTerm) term; - res = convertConstantTerm(term, ct); + res = convertConstantTerm(ct); setResult(res); } else { super.convert(term); } } - private static Term convertConstantTerm(final Term term, final ConstantTerm ct) { + private static Term convertConstantTerm(final ConstantTerm ct) { if (!ct.getSort().isNumericSort()) { // do nothing, only applicable to numeric sorts return ct; } if (ct.getValue() instanceof BigInteger) { final Rational rat = Rational.valueOf((BigInteger) ct.getValue(), BigInteger.ONE); - return rat.toTerm(term.getSort()); + return rat.toTerm(ct.getSort()); } else if (ct.getValue() instanceof BigDecimal) { final BigDecimal decimal = (BigDecimal) ct.getValue(); Rational rat; @@ -68,7 +68,7 @@ private static Term convertConstantTerm(final Term term, final ConstantTerm ct) final BigInteger denom = BigInteger.TEN.pow(decimal.scale()); rat = Rational.valueOf(num, denom); } - return rat.toTerm(term.getSort()); + return rat.toTerm(ct.getSort()); } else if (ct.getValue() instanceof Rational) { // do nothing, already in normal form return ct;