Skip to content

Mirror bvugt/bvuge/bvsgt/bvsge onto bvult/bvule/bvslt/bvsle #799

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
the-mr-dave wants to merge 3 commits into
base: dev
Choose a base branch
from
+85 −10
Open

Mirror bvugt/bvuge/bvsgt/bvsge onto bvult/bvule/bvslt/bvsle #799

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
a84ec80
Mirror bvugt/bvuge/bvsgt/bvsge onto their bvult/bvule/bvslt/bvsle form
the-mr-dave Aug 16, 2026
60995f0
Add tests for mirroring bvugt/bvuge/bvsgt/bvsge
the-mr-dave Aug 16, 2026
c677116
Move operator-mirroring tests into UltimateNormalFormTest
the-mr-dave Aug 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
62 changes: 62 additions & 0 deletions ...src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/UltimateNormalFormTest.java
View file
Open in desktop

@the-mr-dave the-mr-dave Aug 26, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Changes are here

Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down
33 changes: 23 additions & 10 deletions ...y-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/BitvectorUtils.java
View file
Open in desktop

@the-mr-dave the-mr-dave Aug 26, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Changes are here

Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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))
Expand All @@ -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)) {
Expand All @@ -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,
Expand Down