From a84ec807b6defec1bb3a7f2a9b6b6881df4394f6 Mon Sep 17 00:00:00 2001 From: David Enoghama Date: Sun, 16 Aug 2026 18:59:57 +0200 Subject: [PATCH 1/3] Mirror bvugt/bvuge/bvsgt/bvsge onto their bvult/bvule/bvslt/bvsle form Rewrites the four "greater than" comparisons into their swapped "less than" counterpart instead of implementing constant folding for both directions separately, e.g. (bvugt a b) -> (bvult b a). Halves the number of comparison operators that need their own normal form. Co-authored-by: rvinton --- .../lib/smtlibutils/BitvectorUtils.java | 33 +++++++++++++------ 1 file changed, 23 insertions(+), 10 deletions(-) diff --git a/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/BitvectorUtils.java b/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/BitvectorUtils.java index 887688de095..994c14366c0 100644 --- a/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/BitvectorUtils.java +++ b/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/BitvectorUtils.java @@ -34,6 +34,7 @@ import java.util.function.Function; import java.util.function.Predicate; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.binaryrelation.RelationSymbol; import de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm; import de.uni_freiburg.informatik.ultimate.logic.ConstantTerm; import de.uni_freiburg.informatik.ultimate.logic.FunctionSymbol; @@ -236,12 +237,9 @@ public static Term unfTerm(final Script script, final String funcname, final Big .simplifiedResult(script, funcname, indices, params); break; case bvugt: - result = new RegularBitvectorOperation_BooleanResult(funcname, x -> y -> BitvectorConstant.bvugt(x, y)) - .simplifiedResult(script, funcname, indices, params); - break; case bvuge: - result = new RegularBitvectorOperation_BooleanResult(funcname, x -> y -> BitvectorConstant.bvuge(x, y)) - .simplifiedResult(script, funcname, indices, params); + // Mirror to the "less" form instead of folding these separately, e.g. (bvugt a b) -> (bvult b a). + result = mirrorGreaterOperator(script, funcname, indices, params); break; case bvslt: result = new RegularBitvectorOperation_BooleanResult(funcname, x -> y -> BitvectorConstant.bvslt(x, y)) @@ -252,12 +250,9 @@ public static Term unfTerm(final Script script, final String funcname, final Big .simplifiedResult(script, funcname, indices, params); break; case bvsgt: - result = new RegularBitvectorOperation_BooleanResult(funcname, x -> y -> BitvectorConstant.bvsgt(x, y)) - .simplifiedResult(script, funcname, indices, params); - break; case bvsge: - result = new RegularBitvectorOperation_BooleanResult(funcname, x -> y -> BitvectorConstant.bvsge(x, y)) - .simplifiedResult(script, funcname, indices, params); + // Same mirroring for the signed "greater" operators, e.g. (bvsge a b) -> (bvsle b a). + result = mirrorGreaterOperator(script, funcname, indices, params); break; default: if (BitvectorUtils.allTermsAreBitvectorConstants(params)) { @@ -269,6 +264,24 @@ public static Term unfTerm(final Script script, final String funcname, final Big return result; } + /** + * Rewrites a "greater than" comparison ({@code bvugt}, {@code bvuge}, {@code bvsgt}, {@code bvsge}) into its + * mirrored "less than" form by swapping the two operands, e.g. {@code (bvugt a b)} becomes {@code (bvult b a)}. + * This keeps only 4 comparison operators in normal form instead of 8. The mirrored operator name comes from + * {@link RelationSymbol#swapParameters()}; the actual term is then built by dispatching back into {@link #unfTerm}, + * so the existing bvult/bvule/bvslt/bvsle handling (including constant folding) is reused as-is instead of being + * duplicated here. + * + * @param params + * the two operands of the "greater than" comparison, in their original (unswapped) order + * @return the term constructed for the mirrored "less than" comparison + */ + private static Term mirrorGreaterOperator(final Script script, final String funcname, final BigInteger[] indices, + final Term... params) { + final String mirroredFuncname = RelationSymbol.convert(funcname).swapParameters().toString(); + return unfTerm(script, mirroredFuncname, indices, params[1], params[0]); + } + private static abstract class BitvectorOperation { public final Term simplifiedResult(final Script script, final String funcname, final BigInteger[] indices, From 60995f0f0c04b55aa5a1c5fab90f459f246b39d7 Mon Sep 17 00:00:00 2001 From: David Enoghama Date: Sun, 16 Aug 2026 19:12:17 +0200 Subject: [PATCH 2/3] Add tests for mirroring bvugt/bvuge/bvsgt/bvsge Covers each of the four "greater than" comparisons being swapped into its "less than" counterpart, plus two guards confirming that constant folding still triggers correctly after the operand swap instead of just rewriting the operator syntactically. Co-authored-by: rvinton --- .../smt/BitvectorUtilsTest.java | 193 ++++++++++++++++++ 1 file changed, 193 insertions(+) create mode 100644 trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/BitvectorUtilsTest.java diff --git a/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/BitvectorUtilsTest.java b/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/BitvectorUtilsTest.java new file mode 100644 index 00000000000..472ede728fa --- /dev/null +++ b/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/BitvectorUtilsTest.java @@ -0,0 +1,193 @@ +/* + * Copyright (C) 2017 Matthias Heizmann (heizmann@informatik.uni-freiburg.de) + * Copyright (C) 2017 University of Freiburg + * + * This file is part of the ULTIMATE ModelCheckerUtilsTest Library. + * + * The ULTIMATE ModelCheckerUtilsTest Library 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. + * + * The ULTIMATE ModelCheckerUtilsTest Library 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 the ULTIMATE ModelCheckerUtilsTest Library. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE ModelCheckerUtilsTest Library, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE ModelCheckerUtilsTest Library grant you additional permission + * to convey the resulting work. + */ +package de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt; + +import java.io.IOException; + +import org.hamcrest.MatcherAssert; +import org.hamcrest.core.IsEqual; +import org.junit.After; +import org.junit.AfterClass; +import org.junit.Before; +import org.junit.BeforeClass; +import org.junit.Test; + +import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; +import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger.LogLevel; +import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.scripttransfer.HistoryRecordingScript; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ManagedScript; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.SmtUtils.SimplificationTechnique; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.StatisticsScript; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.normalforms.UnfTransformer; +import de.uni_freiburg.informatik.ultimate.logic.FormulaUnLet; +import de.uni_freiburg.informatik.ultimate.logic.LoggingScript; +import de.uni_freiburg.informatik.ultimate.logic.Logics; +import de.uni_freiburg.informatik.ultimate.logic.Script; +import de.uni_freiburg.informatik.ultimate.logic.Term; +import de.uni_freiburg.informatik.ultimate.smtsolver.external.TermParseUtils; +import de.uni_freiburg.informatik.ultimate.test.mocks.UltimateMocks; + +/** + * Tests for mirroring the "greater than" bitvector comparisons ({@code bvugt}, {@code bvuge}, {@code bvsgt}, + * {@code bvsge}) onto their swapped "less than" counterpart in + * {@link de.uni_freiburg.informatik.ultimate.lib.smtlibutils.BitvectorUtils}, and for confirming that constant + * folding still applies after the swap. + * + * Extracted from {@link SimplificationTest} into its own file; reuses {@link SimplificationTest#runSimplificationTest} + * so the test-running/-checking logic is not duplicated. + * + * @author Roman Vintonyak + * @author David Enoghama + * + */ +public class BitvectorUtilsTest { + + /** + * Warning: each test will overwrite the SMT script of the preceding test. + */ + private static final boolean WRITE_SMT_SCRIPTS_TO_FILE = false; + private static final boolean WRITE_BENCHMARK_RESULTS_TO_WORKING_DIRECTORY = false; + private static final long TEST_TIMEOUT_MILLISECONDS = 20_000; + private static final LogLevel LOG_LEVEL = LogLevel.INFO; + private static final String SOLVER_COMMAND = "cvc4 --incremental --lang smt"; + + private IUltimateServiceProvider mServices; + private Script mScript; + private ManagedScript mMgdScript; + private ILogger mLogger; + private static QuantifierEliminationTestCsvWriter mCsvWriter; + + @BeforeClass + public static void beforeAllTests() { + mCsvWriter = new QuantifierEliminationTestCsvWriter(BitvectorUtilsTest.class.getSimpleName()); + } + + @AfterClass + public static void afterAllTests() { + if (WRITE_BENCHMARK_RESULTS_TO_WORKING_DIRECTORY) { + try { + mCsvWriter.writeCsv(); + } catch (final IOException e) { + throw new AssertionError(e); + } + } + } + + @Before + public void setUp() throws IOException { + mServices = UltimateMocks.createUltimateServiceProviderMock(LOG_LEVEL); + mServices.getProgressMonitorService().setDeadline(System.currentTimeMillis() + TEST_TIMEOUT_MILLISECONDS); + mLogger = mServices.getLoggingService().getLogger("lol"); + + final Script solverInstance = new HistoryRecordingScript(UltimateMocks.createSolver(SOLVER_COMMAND, LOG_LEVEL)); + if (WRITE_SMT_SCRIPTS_TO_FILE) { + mScript = new LoggingScript(solverInstance, "BitvectorUtilsTest.smt2", true); + } else { + mScript = solverInstance; + } + mScript = new StatisticsScript(mScript); + + mMgdScript = new ManagedScript(mServices, mScript); + mScript.setLogic(Logics.ALL); + } + + @After + public void tearDown() { + mScript.exit(); + mCsvWriter.reportTestFinished(); + } + + // --- Operator mirroring (bvugt/bvuge/bvsgt/bvsge -> bvult/bvule/bvslt/bvsle) --- + + @Test + public void bvugtMirroredToBvult() { + // Unsigned "greater than" is eliminated by swapping operands into "less than": (x bvugt 1) -> (1 bvult x). + final FunDecl[] funDecls = { new FunDecl(QuantifierEliminationTest::getBitvectorSort8, "x") }; + final String formulaAsString = "(bvugt x (_ bv1 8))"; + final String expected = "(bvult (_ bv1 8) x)"; + + SimplificationTest.runSimplificationTest(funDecls, formulaAsString, expected, SimplificationTechnique.POLY_PAC, + mServices, mLogger, mMgdScript, mCsvWriter); + } + + @Test + public void bvugeMirroredToBvule() { + // Same mirroring for the non-strict unsigned variant: (x bvuge 1) -> (1 bvule x). + final FunDecl[] funDecls = { new FunDecl(QuantifierEliminationTest::getBitvectorSort8, "x") }; + final String formulaAsString = "(bvuge x (_ bv1 8))"; + final String expected = "(bvule (_ bv1 8) x)"; + + SimplificationTest.runSimplificationTest(funDecls, formulaAsString, expected, SimplificationTechnique.POLY_PAC, + mServices, mLogger, mMgdScript, mCsvWriter); + } + + @Test + public void bvsgtMirroredToBvslt() { + // Signed "greater than" is mirrored the same way as the unsigned case: (x bvsgt 1) -> (1 bvslt x). + final FunDecl[] funDecls = { new FunDecl(QuantifierEliminationTest::getBitvectorSort8, "x") }; + final String formulaAsString = "(bvsgt x (_ bv1 8))"; + final String expected = "(bvslt (_ bv1 8) x)"; + + SimplificationTest.runSimplificationTest(funDecls, formulaAsString, expected, SimplificationTechnique.POLY_PAC, + mServices, mLogger, mMgdScript, mCsvWriter); + } + + @Test + public void bvsgeMirroredToBvsle() { + // Same mirroring for the non-strict signed variant: (x bvsge 1) -> (1 bvsle x). + final FunDecl[] funDecls = { new FunDecl(QuantifierEliminationTest::getBitvectorSort8, "x") }; + final String formulaAsString = "(bvsge x (_ bv1 8))"; + final String expected = "(bvsle (_ bv1 8) x)"; + + SimplificationTest.runSimplificationTest(funDecls, formulaAsString, expected, SimplificationTechnique.POLY_PAC, + mServices, mLogger, mMgdScript, mCsvWriter); + } + + @Test + public void bvugtConstantFoldingAfterMirroring() { + // Guards against a purely syntactic swap: mirroring to bvult must still trigger the existing constant + // folding, not just rewrite the operator. Both operands are literals here, so the result must be "true", + // not an unevaluated (bvult (_ bv3 8) (_ bv5 8)) term. + final String formulaAsString = "(bvugt (_ bv5 8) (_ bv3 8))"; + final String expected = "true"; + + SimplificationTest.runSimplificationTest(new FunDecl[0], formulaAsString, expected, + SimplificationTechnique.POLY_PAC, mServices, mLogger, mMgdScript, mCsvWriter); + } + + @Test + public void bvsgtConstantFoldingAfterMirroring() { + // Same guard for the signed variant, to confirm signed constant folding also still works after mirroring. + final String formulaAsString = "(bvsgt (_ bv5 8) (_ bv3 8))"; + final String expected = "true"; + + SimplificationTest.runSimplificationTest(new FunDecl[0], formulaAsString, expected, + SimplificationTechnique.POLY_PAC, mServices, mLogger, mMgdScript, mCsvWriter); + } + +} From c67711646d7248baae211e96867053ed8fc16bf4 Mon Sep 17 00:00:00 2001 From: David Enoghama Date: Wed, 26 Aug 2026 12:25:33 +0200 Subject: [PATCH 3/3] Move operator-mirroring tests into UltimateNormalFormTest Uses runUnfTest (UnfTransformer directly) instead of SimplificationTest.runSimplificationTest, matching the workflow already used for the other UnfTransformer-level tests in this class. Co-authored-by: rvinton --- .../smt/BitvectorUtilsTest.java | 193 ------------------ .../smt/UltimateNormalFormTest.java | 62 ++++++ 2 files changed, 62 insertions(+), 193 deletions(-) delete mode 100644 trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/BitvectorUtilsTest.java diff --git a/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/BitvectorUtilsTest.java b/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/BitvectorUtilsTest.java deleted file mode 100644 index 472ede728fa..00000000000 --- a/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/BitvectorUtilsTest.java +++ /dev/null @@ -1,193 +0,0 @@ -/* - * Copyright (C) 2017 Matthias Heizmann (heizmann@informatik.uni-freiburg.de) - * Copyright (C) 2017 University of Freiburg - * - * This file is part of the ULTIMATE ModelCheckerUtilsTest Library. - * - * The ULTIMATE ModelCheckerUtilsTest Library 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. - * - * The ULTIMATE ModelCheckerUtilsTest Library 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 the ULTIMATE ModelCheckerUtilsTest Library. If not, see . - * - * Additional permission under GNU GPL version 3 section 7: - * If you modify the ULTIMATE ModelCheckerUtilsTest Library, or any covered work, by linking - * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), - * containing parts covered by the terms of the Eclipse Public License, the - * licensors of the ULTIMATE ModelCheckerUtilsTest Library grant you additional permission - * to convey the resulting work. - */ -package de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt; - -import java.io.IOException; - -import org.hamcrest.MatcherAssert; -import org.hamcrest.core.IsEqual; -import org.junit.After; -import org.junit.AfterClass; -import org.junit.Before; -import org.junit.BeforeClass; -import org.junit.Test; - -import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; -import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger.LogLevel; -import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider; -import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.scripttransfer.HistoryRecordingScript; -import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ManagedScript; -import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.SmtUtils.SimplificationTechnique; -import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.StatisticsScript; -import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.normalforms.UnfTransformer; -import de.uni_freiburg.informatik.ultimate.logic.FormulaUnLet; -import de.uni_freiburg.informatik.ultimate.logic.LoggingScript; -import de.uni_freiburg.informatik.ultimate.logic.Logics; -import de.uni_freiburg.informatik.ultimate.logic.Script; -import de.uni_freiburg.informatik.ultimate.logic.Term; -import de.uni_freiburg.informatik.ultimate.smtsolver.external.TermParseUtils; -import de.uni_freiburg.informatik.ultimate.test.mocks.UltimateMocks; - -/** - * Tests for mirroring the "greater than" bitvector comparisons ({@code bvugt}, {@code bvuge}, {@code bvsgt}, - * {@code bvsge}) onto their swapped "less than" counterpart in - * {@link de.uni_freiburg.informatik.ultimate.lib.smtlibutils.BitvectorUtils}, and for confirming that constant - * folding still applies after the swap. - * - * Extracted from {@link SimplificationTest} into its own file; reuses {@link SimplificationTest#runSimplificationTest} - * so the test-running/-checking logic is not duplicated. - * - * @author Roman Vintonyak - * @author David Enoghama - * - */ -public class BitvectorUtilsTest { - - /** - * Warning: each test will overwrite the SMT script of the preceding test. - */ - private static final boolean WRITE_SMT_SCRIPTS_TO_FILE = false; - private static final boolean WRITE_BENCHMARK_RESULTS_TO_WORKING_DIRECTORY = false; - private static final long TEST_TIMEOUT_MILLISECONDS = 20_000; - private static final LogLevel LOG_LEVEL = LogLevel.INFO; - private static final String SOLVER_COMMAND = "cvc4 --incremental --lang smt"; - - private IUltimateServiceProvider mServices; - private Script mScript; - private ManagedScript mMgdScript; - private ILogger mLogger; - private static QuantifierEliminationTestCsvWriter mCsvWriter; - - @BeforeClass - public static void beforeAllTests() { - mCsvWriter = new QuantifierEliminationTestCsvWriter(BitvectorUtilsTest.class.getSimpleName()); - } - - @AfterClass - public static void afterAllTests() { - if (WRITE_BENCHMARK_RESULTS_TO_WORKING_DIRECTORY) { - try { - mCsvWriter.writeCsv(); - } catch (final IOException e) { - throw new AssertionError(e); - } - } - } - - @Before - public void setUp() throws IOException { - mServices = UltimateMocks.createUltimateServiceProviderMock(LOG_LEVEL); - mServices.getProgressMonitorService().setDeadline(System.currentTimeMillis() + TEST_TIMEOUT_MILLISECONDS); - mLogger = mServices.getLoggingService().getLogger("lol"); - - final Script solverInstance = new HistoryRecordingScript(UltimateMocks.createSolver(SOLVER_COMMAND, LOG_LEVEL)); - if (WRITE_SMT_SCRIPTS_TO_FILE) { - mScript = new LoggingScript(solverInstance, "BitvectorUtilsTest.smt2", true); - } else { - mScript = solverInstance; - } - mScript = new StatisticsScript(mScript); - - mMgdScript = new ManagedScript(mServices, mScript); - mScript.setLogic(Logics.ALL); - } - - @After - public void tearDown() { - mScript.exit(); - mCsvWriter.reportTestFinished(); - } - - // --- Operator mirroring (bvugt/bvuge/bvsgt/bvsge -> bvult/bvule/bvslt/bvsle) --- - - @Test - public void bvugtMirroredToBvult() { - // Unsigned "greater than" is eliminated by swapping operands into "less than": (x bvugt 1) -> (1 bvult x). - final FunDecl[] funDecls = { new FunDecl(QuantifierEliminationTest::getBitvectorSort8, "x") }; - final String formulaAsString = "(bvugt x (_ bv1 8))"; - final String expected = "(bvult (_ bv1 8) x)"; - - SimplificationTest.runSimplificationTest(funDecls, formulaAsString, expected, SimplificationTechnique.POLY_PAC, - mServices, mLogger, mMgdScript, mCsvWriter); - } - - @Test - public void bvugeMirroredToBvule() { - // Same mirroring for the non-strict unsigned variant: (x bvuge 1) -> (1 bvule x). - final FunDecl[] funDecls = { new FunDecl(QuantifierEliminationTest::getBitvectorSort8, "x") }; - final String formulaAsString = "(bvuge x (_ bv1 8))"; - final String expected = "(bvule (_ bv1 8) x)"; - - SimplificationTest.runSimplificationTest(funDecls, formulaAsString, expected, SimplificationTechnique.POLY_PAC, - mServices, mLogger, mMgdScript, mCsvWriter); - } - - @Test - public void bvsgtMirroredToBvslt() { - // Signed "greater than" is mirrored the same way as the unsigned case: (x bvsgt 1) -> (1 bvslt x). - final FunDecl[] funDecls = { new FunDecl(QuantifierEliminationTest::getBitvectorSort8, "x") }; - final String formulaAsString = "(bvsgt x (_ bv1 8))"; - final String expected = "(bvslt (_ bv1 8) x)"; - - SimplificationTest.runSimplificationTest(funDecls, formulaAsString, expected, SimplificationTechnique.POLY_PAC, - mServices, mLogger, mMgdScript, mCsvWriter); - } - - @Test - public void bvsgeMirroredToBvsle() { - // Same mirroring for the non-strict signed variant: (x bvsge 1) -> (1 bvsle x). - final FunDecl[] funDecls = { new FunDecl(QuantifierEliminationTest::getBitvectorSort8, "x") }; - final String formulaAsString = "(bvsge x (_ bv1 8))"; - final String expected = "(bvsle (_ bv1 8) x)"; - - SimplificationTest.runSimplificationTest(funDecls, formulaAsString, expected, SimplificationTechnique.POLY_PAC, - mServices, mLogger, mMgdScript, mCsvWriter); - } - - @Test - public void bvugtConstantFoldingAfterMirroring() { - // Guards against a purely syntactic swap: mirroring to bvult must still trigger the existing constant - // folding, not just rewrite the operator. Both operands are literals here, so the result must be "true", - // not an unevaluated (bvult (_ bv3 8) (_ bv5 8)) term. - final String formulaAsString = "(bvugt (_ bv5 8) (_ bv3 8))"; - final String expected = "true"; - - SimplificationTest.runSimplificationTest(new FunDecl[0], formulaAsString, expected, - SimplificationTechnique.POLY_PAC, mServices, mLogger, mMgdScript, mCsvWriter); - } - - @Test - public void bvsgtConstantFoldingAfterMirroring() { - // Same guard for the signed variant, to confirm signed constant folding also still works after mirroring. - final String formulaAsString = "(bvsgt (_ bv5 8) (_ bv3 8))"; - final String expected = "true"; - - SimplificationTest.runSimplificationTest(new FunDecl[0], formulaAsString, expected, - SimplificationTechnique.POLY_PAC, mServices, mLogger, mMgdScript, mCsvWriter); - } - -} diff --git a/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/UltimateNormalFormTest.java b/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/UltimateNormalFormTest.java index 6540007bbd1..9621f33483e 100644 --- a/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/UltimateNormalFormTest.java +++ b/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/UltimateNormalFormTest.java @@ -574,6 +574,68 @@ public void bvConstantsCase() { runUnfTest(new FunDecl[0], formulaAsString, expected, mMgdScript); } + // --- Operator mirroring (bvugt/bvuge/bvsgt/bvsge -> bvult/bvule/bvslt/bvsle) --- + + @Test + public void bvugtMirroredToBvult() { + // Unsigned "greater than" is eliminated by swapping operands into "less than": (x bvugt 1) -> (1 bvult x). + final FunDecl[] funDecls = { new FunDecl(QuantifierEliminationTest::getBitvectorSort8, "x") }; + final String formulaAsString = "(bvugt x (_ bv1 8))"; + final String expected = "(bvult (_ bv1 8) x)"; + + runUnfTest(funDecls, formulaAsString, expected, mMgdScript); + } + + @Test + public void bvugeMirroredToBvule() { + // Same mirroring for the non-strict unsigned variant: (x bvuge 1) -> (1 bvule x). + final FunDecl[] funDecls = { new FunDecl(QuantifierEliminationTest::getBitvectorSort8, "x") }; + final String formulaAsString = "(bvuge x (_ bv1 8))"; + final String expected = "(bvule (_ bv1 8) x)"; + + runUnfTest(funDecls, formulaAsString, expected, mMgdScript); + } + + @Test + public void bvsgtMirroredToBvslt() { + // Signed "greater than" is mirrored the same way as the unsigned case: (x bvsgt 1) -> (1 bvslt x). + final FunDecl[] funDecls = { new FunDecl(QuantifierEliminationTest::getBitvectorSort8, "x") }; + final String formulaAsString = "(bvsgt x (_ bv1 8))"; + final String expected = "(bvslt (_ bv1 8) x)"; + + runUnfTest(funDecls, formulaAsString, expected, mMgdScript); + } + + @Test + public void bvsgeMirroredToBvsle() { + // Same mirroring for the non-strict signed variant: (x bvsge 1) -> (1 bvsle x). + final FunDecl[] funDecls = { new FunDecl(QuantifierEliminationTest::getBitvectorSort8, "x") }; + final String formulaAsString = "(bvsge x (_ bv1 8))"; + final String expected = "(bvsle (_ bv1 8) x)"; + + runUnfTest(funDecls, formulaAsString, expected, mMgdScript); + } + + @Test + public void bvugtConstantFoldingAfterMirroring() { + // Guards against a purely syntactic swap: mirroring to bvult must still trigger the existing constant + // folding, not just rewrite the operator. Both operands are literals here, so the result must be "true", + // not an unevaluated (bvult (_ bv3 8) (_ bv5 8)) term. + final String formulaAsString = "(bvugt (_ bv5 8) (_ bv3 8))"; + final String expected = "true"; + + runUnfTest(new FunDecl[0], formulaAsString, expected, mMgdScript); + } + + @Test + public void bvsgtConstantFoldingAfterMirroring() { + // Same guard for the signed variant, to confirm signed constant folding also still works after mirroring. + final String formulaAsString = "(bvsgt (_ bv5 8) (_ bv3 8))"; + final String expected = "true"; + + runUnfTest(new FunDecl[0], formulaAsString, expected, mMgdScript); + } + static void runUnfTest(final FunDecl[] funDecls, final String eliminationInputAsString, final String expectedResultAsString, final ManagedScript mgdScript) { for (final FunDecl funDecl : funDecls) {