Skip to content

Tests: more tests for dumping SMTLIB for quantified formulas. #573

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
kfriedberger wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Tests: more tests for dumping SMTLIB for quantified formulas. #573

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
116 changes: 115 additions & 1 deletion src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
// an API wrapper for a collection of SMT solvers:
// https://github.com/sosy-lab/java-smt
//
// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
// SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
//
// SPDX-License-Identifier: Apache-2.0

Expand Down Expand Up @@ -576,4 +576,118 @@ private BooleanFormula functionExprGen() {
BooleanFormula res1 = fmgr.callUF(funA, arg);
return bmgr.and(res1, bmgr.makeBoolean(true));
}

@Test
public void quantifierIntegerDumpTest() {
requireIntegers();
requireQuantifiers();

// build formula: (FORALL (x Int) (= 1 x))
IntegerFormula int1 = imgr.makeNumber(1);
IntegerFormula var = imgr.makeVariable("x");
BooleanFormula body = imgr.equal(int1, var);
BooleanFormula formula = qmgr.forall(var, body);

final String formDump = mgr.dumpFormula(formula).toString();

final String expected;
switch (solverToUse()) {
case Z3:
expected = "forall ((x Int)) (! (= 1 x) :weight 0)"; // with weight
break;
case PRINCESS:
expected = "forall ((var0 Int)) (= 1 var0)"; // renamed symbols
break;
case CVC4:
expected = "forall ((x Int)) (= 1 x) "; // with trailing space
break;
case YICES2:
expected = "forall (x::int) (= 1 x)"; // special type annotation
break;
default:
expected = "forall ((x Int)) (= 1 x)"; // normal
break;
}

assertThat(formDump).isEqualTo("(assert (" + expected + "))\n");
checkThatAssertIsInLastLine(formDump);
checkThatDumpIsParseable(formDump);
}

@Test
public void quantifierBitvectorDumpTest() {
requireBitvectors();
requireQuantifiers();

// build formula: (FORALL (x (_ BitVec 8)) (= #b00000001 x))
BitvectorFormula int1 = bvmgr.makeBitvector(8, 1);
BitvectorFormula var = bvmgr.makeVariable(8, "x");
BooleanFormula body = bvmgr.equal(int1, var);
BooleanFormula formula = qmgr.forall(var, body);

final String formDump = mgr.dumpFormula(formula).toString();

final String expected;
switch (solverToUse()) {
case Z3:
expected = "forall ((x (_ BitVec 8))) (! (= #x01 x) :weight 0)"; // with weight
break;
case PRINCESS:
expected = "forall ((var0 (_ BitVec 8))) (= (_ bv1 8) var0)"; // renamed symbols
break;
case CVC4:
expected = "forall ((x (_ BitVec 8))) (= #b00000001 x) "; // with trailing space
break;
case YICES2:
expected = "forall (x::(bitvector 8)) (= 0b00000001 x)"; // special type annotation
break;
default:
expected = "forall ((x (_ BitVec 8))) (= #b00000001 x)"; // normal
break;
}

// check that function is dumped correctly + necessary assert that has to be there
assertThat(formDump).isEqualTo("(assert (" + expected + "))\n");
checkThatAssertIsInLastLine(formDump);
checkThatDumpIsParseable(formDump);
}

@Test
public void quantifierBitvectorDumpTest_withSize6() {
// bitvector size 6 does not allow solvers like Z3 to use hexadecimal notation for numbers
requireBitvectors();
requireQuantifiers();

// build formula: (FORALL (x (_ BitVec 6)) (= #b000001 x))
BitvectorFormula int1 = bvmgr.makeBitvector(6, 1);
BitvectorFormula var = bvmgr.makeVariable(6, "x");
BooleanFormula body = bvmgr.equal(int1, var);
BooleanFormula formula = qmgr.forall(var, body);

final String formDump = mgr.dumpFormula(formula).toString();

final String expected;
switch (solverToUse()) {
case Z3:
expected = "forall ((x (_ BitVec 6))) (! (= #b000001 x) :weight 0)"; // with weight
break;
case PRINCESS:
expected = "forall ((var0 (_ BitVec 6))) (= (_ bv1 6) var0)"; // renamed symbols
break;
case CVC4:
expected = "forall ((x (_ BitVec 6))) (= #b000001 x) "; // with trailing space
break;
case YICES2:
expected = "forall (x::(bitvector 6)) (= 0b000001 x)"; // special type annotation
break;
default:
expected = "forall ((x (_ BitVec 6))) (= #b000001 x)"; // normal
break;
}

// check that function is dumped correctly + necessary assert that has to be there
assertThat(formDump).isEqualTo("(assert (" + expected + "))\n");
checkThatAssertIsInLastLine(formDump);
checkThatDumpIsParseable(formDump);
}
}