fix unit test that requires integer logic in the solver.
Boolector fails here.
And some formatting such that all requirements come first in each test case.
@@ -70,8 +70,9 @@ public class UfEliminationTest extends SolverBasedTest0 {
@Test
public void simpleTest() throws SolverException, InterruptedException {
- // f := uf(v1, v3) XOR uf(v2, v4)
requireIntegers();
+
+ // f := uf(v1, v3) XOR uf(v2, v4)
IntegerFormula variable1 = imgr.makeVariable("variable1");
IntegerFormula variable2 = imgr.makeVariable("variable2");
IntegerFormula variable3 = imgr.makeVariable("variable3");
@@ -101,8 +102,9 @@ public class UfEliminationTest extends SolverBasedTest0 {
@Test
public void nestedUfs() throws SolverException, InterruptedException {
- // f := uf2(uf1(v1, v2), v3) XOR uf2(uf1(v2, v1), v4)
requireIntegers();
+
+ // f := uf2(uf1(v1, v2), v3) XOR uf2(uf1(v2, v1), v4)
IntegerFormula variable1 = imgr.makeVariable("variable1");
IntegerFormula variable2 = imgr.makeVariable("variable2");
IntegerFormula variable3 = imgr.makeVariable("variable3");
@@ -137,8 +139,9 @@ public class UfEliminationTest extends SolverBasedTest0 {
@Test
public void nestedUfs2() throws SolverException, InterruptedException {
- // f := uf2(uf1(v1, uf2(v3, v6)), v3) < uf2(uf1(v2, uf2(v4, v5)), v4)
requireIntegers();
+
+ // f := uf2(uf1(v1, uf2(v3, v6)), v3) < uf2(uf1(v2, uf2(v4, v5)), v4)
IntegerFormula variable1 = imgr.makeVariable("variable1");
IntegerFormula variable2 = imgr.makeVariable("variable2");
IntegerFormula variable3 = imgr.makeVariable("variable3");
@@ -180,6 +183,8 @@ public class UfEliminationTest extends SolverBasedTest0 {
@Test
public void nestedUfs3() throws SolverException, InterruptedException {
+ requireIntegers();
+
// f := uf(v1) < uf(v2)
IntegerFormula variable1 = imgr.makeVariable("variable1");
IntegerFormula variable2 = imgr.makeVariable("variable2");
@@ -247,6 +252,7 @@ public class UfEliminationTest extends SolverBasedTest0 {
public void quantifierTest() {
requireQuantifiers();
requireIntegers();
+
// f := exists v1,v2v,v3,v4 : uf(v1, v3) == uf(v2, v4)
IntegerFormula variable1 = imgr.makeVariable("variable1");
IntegerFormula variable2 = imgr.makeVariable("variable2");
@@ -270,8 +276,9 @@ public class UfEliminationTest extends SolverBasedTest0 {
@Test
public void substitutionTest() throws SolverException, InterruptedException {
- // f := uf(v1, v3) \/ NOT(uf(v2, v4)))
requireIntegers();
+
+ // f := uf(v1, v3) \/ NOT(uf(v2, v4)))
IntegerFormula variable1 = imgr.makeVariable("variable1");
IntegerFormula variable2 = imgr.makeVariable("variable2");
IntegerFormula variable3 = imgr.makeVariable("variable3");
