Skip to content

Commit e697ed6

Browse files
kfriedbergerkfriedberger
committed
#397: extend tests for bitvector rotation.
1 parent 53bbf95 commit e697ed6

File tree

2 files changed

+210
-31
lines changed

2 files changed

+210
-31
lines changed

‎src/org/sosy_lab/java_smt/test/RotationVisitorTest.java‎

Lines changed: 187 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -12,37 +12,210 @@
1212

1313
import static com.google.common.truth.Truth.assertThat;
1414

15+
import org.junit.Before;
1516
import org.junit.Test;
1617
import org.sosy_lab.java_smt.api.BitvectorFormula;
18+
import org.sosy_lab.java_smt.api.FunctionDeclarationKind;
19+
import org.sosy_lab.java_smt.test.SolverVisitorTest.FunctionDeclarationVisitorNoOther;
1720

1821
public class RotationVisitorTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
22+
23+
private BitvectorFormula a;
24+
private BitvectorFormula y;
25+
26+
@Before
27+
public void init() {
28+
requireBitvectors();
29+
requireVisitor();
30+
31+
a = bvmgr.makeVariable(8, "a");
32+
y = bvmgr.makeBitvector(8, 1);
33+
}
34+
1935
@Test
2036
public void rotateLeftTest() {
21-
requireBitvectors();
22-
BitvectorFormula x = bvmgr.makeBitvector(8, 7);
23-
assertThat(mgr.extractVariables(bvmgr.rotateLeft(x, 1))).isEmpty();
37+
BitvectorFormula f = bvmgr.rotateLeft(a, y);
38+
39+
var variables = mgr.extractVariablesAndUFs(f);
40+
assertThat(variables).hasSize(1);
41+
assertThat(variables).containsKey("a");
42+
43+
var functions = mgr.visit(f, new FunctionDeclarationVisitorNoOther(mgr));
44+
switch (solverToUse()) {
45+
case CVC4:
46+
assertThat(functions)
47+
.containsExactly(
48+
FunctionDeclarationKind.BV_OR,
49+
FunctionDeclarationKind.BV_SHL,
50+
FunctionDeclarationKind.ITE,
51+
FunctionDeclarationKind.ITE,
52+
FunctionDeclarationKind.EQ,
53+
FunctionDeclarationKind.EQ,
54+
FunctionDeclarationKind.BV_SMOD,
55+
FunctionDeclarationKind.BV_SMOD,
56+
FunctionDeclarationKind.BV_LSHR,
57+
FunctionDeclarationKind.BV_SUB);
58+
break;
59+
case CVC5:
60+
case PRINCESS:
61+
assertThat(functions)
62+
.containsExactly(
63+
FunctionDeclarationKind.BV_OR,
64+
FunctionDeclarationKind.BV_SHL,
65+
FunctionDeclarationKind.BV_SMOD,
66+
FunctionDeclarationKind.BV_SMOD,
67+
FunctionDeclarationKind.BV_LSHR,
68+
FunctionDeclarationKind.BV_SUB);
69+
break;
70+
case MATHSAT5:
71+
assertThat(functions)
72+
.containsExactly(
73+
FunctionDeclarationKind.BV_OR,
74+
FunctionDeclarationKind.BV_LSHR,
75+
FunctionDeclarationKind.BV_SHL);
76+
break;
77+
case YICES2:
78+
assertThat(functions)
79+
.containsExactly(
80+
FunctionDeclarationKind.BV_CONCAT,
81+
FunctionDeclarationKind.BV_EXTRACT,
82+
FunctionDeclarationKind.BV_EXTRACT,
83+
FunctionDeclarationKind.BV_EXTRACT,
84+
FunctionDeclarationKind.BV_EXTRACT,
85+
FunctionDeclarationKind.BV_EXTRACT,
86+
FunctionDeclarationKind.BV_EXTRACT,
87+
FunctionDeclarationKind.BV_EXTRACT,
88+
FunctionDeclarationKind.BV_EXTRACT);
89+
break;
90+
default:
91+
assertThat(functions).containsExactly(FunctionDeclarationKind.BV_ROTATE_LEFT);
92+
}
93+
94+
// TODO dumpFormula crashes with Princess
95+
// System.out.println(mgr.dumpFormula(bvmgr.equal(a, f)));
2496
}
2597

2698
@Test
2799
public void rotateRightTest() {
28-
requireBitvectors();
29-
BitvectorFormula x = bvmgr.makeBitvector(8, 7);
30-
assertThat(mgr.extractVariables(bvmgr.rotateRight(x, 1))).isEmpty();
100+
BitvectorFormula f = bvmgr.rotateRight(a, y);
101+
102+
var variables = mgr.extractVariablesAndUFs(f);
103+
assertThat(variables).hasSize(1);
104+
assertThat(variables).containsKey("a");
105+
106+
var functions = mgr.visit(f, new FunctionDeclarationVisitorNoOther(mgr));
107+
switch (solverToUse()) {
108+
case CVC4:
109+
assertThat(functions)
110+
.containsExactly(
111+
FunctionDeclarationKind.BV_OR,
112+
FunctionDeclarationKind.BV_LSHR,
113+
FunctionDeclarationKind.ITE,
114+
FunctionDeclarationKind.ITE,
115+
FunctionDeclarationKind.EQ,
116+
FunctionDeclarationKind.EQ,
117+
FunctionDeclarationKind.BV_SMOD,
118+
FunctionDeclarationKind.BV_SMOD,
119+
FunctionDeclarationKind.BV_SHL,
120+
FunctionDeclarationKind.BV_SUB);
121+
break;
122+
case CVC5:
123+
case PRINCESS:
124+
assertThat(functions)
125+
.containsExactly(
126+
FunctionDeclarationKind.BV_OR,
127+
FunctionDeclarationKind.BV_SHL,
128+
FunctionDeclarationKind.BV_SMOD,
129+
FunctionDeclarationKind.BV_SMOD,
130+
FunctionDeclarationKind.BV_LSHR,
131+
FunctionDeclarationKind.BV_SUB);
132+
break;
133+
case MATHSAT5:
134+
assertThat(functions)
135+
.containsExactly(
136+
FunctionDeclarationKind.BV_OR,
137+
FunctionDeclarationKind.BV_LSHR,
138+
FunctionDeclarationKind.BV_SHL);
139+
break;
140+
case YICES2:
141+
assertThat(functions)
142+
.containsExactly(
143+
FunctionDeclarationKind.BV_CONCAT,
144+
FunctionDeclarationKind.BV_EXTRACT,
145+
FunctionDeclarationKind.BV_EXTRACT,
146+
FunctionDeclarationKind.BV_EXTRACT,
147+
FunctionDeclarationKind.BV_EXTRACT,
148+
FunctionDeclarationKind.BV_EXTRACT,
149+
FunctionDeclarationKind.BV_EXTRACT,
150+
FunctionDeclarationKind.BV_EXTRACT,
151+
FunctionDeclarationKind.BV_EXTRACT);
152+
break;
153+
default:
154+
assertThat(functions).containsExactly(FunctionDeclarationKind.BV_ROTATE_RIGHT);
155+
}
31156
}
32157

33158
@Test
34159
public void rotateLeftIntegerTest() {
35-
requireBitvectors();
36-
BitvectorFormula x = bvmgr.makeBitvector(8, 7);
37-
BitvectorFormula y = bvmgr.makeBitvector(8, 1);
38-
assertThat(mgr.extractVariables(bvmgr.rotateLeft(x, y))).isEmpty();
160+
BitvectorFormula f = bvmgr.rotateLeft(a, 1);
161+
162+
var variables = mgr.extractVariablesAndUFs(f);
163+
assertThat(variables).hasSize(1);
164+
assertThat(variables).containsKey("a");
165+
166+
var functions = mgr.visit(f, new FunctionDeclarationVisitorNoOther(mgr));
167+
switch (solverToUse()) {
168+
case PRINCESS:
169+
assertThat(functions)
170+
.containsExactly(FunctionDeclarationKind.BV_EXTRACT, FunctionDeclarationKind.BV_CONCAT);
171+
break;
172+
case YICES2:
173+
assertThat(functions)
174+
.containsExactly(
175+
FunctionDeclarationKind.BV_CONCAT,
176+
FunctionDeclarationKind.BV_EXTRACT,
177+
FunctionDeclarationKind.BV_EXTRACT,
178+
FunctionDeclarationKind.BV_EXTRACT,
179+
FunctionDeclarationKind.BV_EXTRACT,
180+
FunctionDeclarationKind.BV_EXTRACT,
181+
FunctionDeclarationKind.BV_EXTRACT,
182+
FunctionDeclarationKind.BV_EXTRACT,
183+
FunctionDeclarationKind.BV_EXTRACT);
184+
break;
185+
default:
186+
assertThat(functions).containsExactly(FunctionDeclarationKind.BV_ROTATE_LEFT_BY_INT);
187+
}
39188
}
40189

41190
@Test
42191
public void rotateRightIntegerTest() {
43-
requireBitvectors();
44-
BitvectorFormula x = bvmgr.makeBitvector(8, 7);
45-
BitvectorFormula y = bvmgr.makeBitvector(8, 1);
46-
assertThat(mgr.extractVariables(bvmgr.rotateRight(x, y))).isEmpty();
192+
BitvectorFormula f = bvmgr.rotateRight(a, 1);
193+
194+
var variables = mgr.extractVariablesAndUFs(f);
195+
assertThat(variables).hasSize(1);
196+
assertThat(variables).containsKey("a");
197+
198+
var functions = mgr.visit(f, new FunctionDeclarationVisitorNoOther(mgr));
199+
switch (solverToUse()) {
200+
case PRINCESS:
201+
assertThat(functions)
202+
.containsExactly(FunctionDeclarationKind.BV_EXTRACT, FunctionDeclarationKind.BV_CONCAT);
203+
break;
204+
case YICES2:
205+
assertThat(functions)
206+
.containsExactly(
207+
FunctionDeclarationKind.BV_CONCAT,
208+
FunctionDeclarationKind.BV_EXTRACT,
209+
FunctionDeclarationKind.BV_EXTRACT,
210+
FunctionDeclarationKind.BV_EXTRACT,
211+
FunctionDeclarationKind.BV_EXTRACT,
212+
FunctionDeclarationKind.BV_EXTRACT,
213+
FunctionDeclarationKind.BV_EXTRACT,
214+
FunctionDeclarationKind.BV_EXTRACT,
215+
FunctionDeclarationKind.BV_EXTRACT);
216+
break;
217+
default:
218+
assertThat(functions).containsExactly(FunctionDeclarationKind.BV_ROTATE_RIGHT_BY_INT);
219+
}
47220
}
48221
}

‎src/org/sosy_lab/java_smt/test/SolverVisitorTest.java‎

Lines changed: 23 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,7 @@
4040
import org.sosy_lab.java_smt.api.FloatingPointNumber;
4141
import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
4242
import org.sosy_lab.java_smt.api.Formula;
43+
import org.sosy_lab.java_smt.api.FormulaManager;
4344
import org.sosy_lab.java_smt.api.FormulaType;
4445
import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType;
4546
import org.sosy_lab.java_smt.api.FormulaType.BitvectorType;
@@ -61,10 +62,15 @@
6162
public class SolverVisitorTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
6263

6364
/** visit a formula and fail on OTHER, i.e., unexpected function declaration type. */
64-
private final class FunctionDeclarationVisitorNoOther
65+
public static final class FunctionDeclarationVisitorNoOther
6566
extends DefaultFormulaVisitor<List<FunctionDeclarationKind>> {
6667

6768
private final List<FunctionDeclarationKind> found = new ArrayList<>();
69+
private final FormulaManager manager;
70+
71+
FunctionDeclarationVisitorNoOther(FormulaManager pMgr) {
72+
manager = pMgr;
73+
}
6874

6975
@Override
7076
public List<FunctionDeclarationKind> visitFunction(
@@ -77,7 +83,7 @@ public List<FunctionDeclarationKind> visitFunction(
7783
.that(functionDeclaration.getKind())
7884
.isNotEqualTo(FunctionDeclarationKind.OTHER);
7985
for (Formula arg : args) {
80-
mgr.visit(arg, this);
86+
manager.visit(arg, this);
8187
}
8288
return visitDefault(f);
8389
}
@@ -207,7 +213,7 @@ public void bitvectorIdVisit() throws SolverException, InterruptedException {
207213
if (Solvers.PRINCESS != solver) {
208214
// Princess models BV theory with intervals, such as "mod_cast(lower, upper , value)".
209215
// The interval function is of FunctionDeclarationKind.OTHER and thus we cannot check it.
210-
mgr.visit(f, new FunctionDeclarationVisitorNoOther());
216+
mgr.visit(f, new FunctionDeclarationVisitorNoOther(mgr));
211217
}
212218
BooleanFormula f2 = mgr.transformRecursively(f, new FormulaTransformationVisitor(mgr) {});
213219
assertThat(f2).isEqualTo(f);
@@ -239,7 +245,7 @@ public void bitvectorIdVisit() throws SolverException, InterruptedException {
239245
if (Solvers.PRINCESS != solver) {
240246
// Princess models BV theory with intervals, such as "mod_cast(lower, upper , value)".
241247
// The interval function is of FunctionDeclarationKind.OTHER and thus we cannot check it.
242-
mgr.visit(f, new FunctionDeclarationVisitorNoOther());
248+
mgr.visit(f, new FunctionDeclarationVisitorNoOther(mgr));
243249
}
244250
BitvectorFormula f2 = mgr.transformRecursively(f, new FormulaTransformationVisitor(mgr) {});
245251
assertThat(f2).isEqualTo(f);
@@ -258,7 +264,7 @@ public void bitvectorIdVisit2() throws SolverException, InterruptedException {
258264
if (Solvers.PRINCESS != solver) {
259265
// Princess models BV theory with intervals, such as "mod_cast(lower, upper , value)".
260266
// The interval function is of FunctionDeclarationKind.OTHER and thus we cannot check it.
261-
mgr.visit(f, new FunctionDeclarationVisitorNoOther());
267+
mgr.visit(f, new FunctionDeclarationVisitorNoOther(mgr));
262268
}
263269
BitvectorFormula f2 = mgr.transformRecursively(f, new FormulaTransformationVisitor(mgr) {});
264270
assertThat(f2).isEqualTo(f);
@@ -315,13 +321,13 @@ public void arrayVisit() {
315321

316322
ArrayFormula<IntegerFormula, IntegerFormula> arr = amgr.makeArray("some_array", arrayType);
317323
IntegerFormula selectedElem = amgr.select(arr, index);
318-
assertThat(mgr.visit(selectedElem, new FunctionDeclarationVisitorNoOther()))
324+
assertThat(mgr.visit(selectedElem, new FunctionDeclarationVisitorNoOther(mgr)))
319325
.containsExactly(FunctionDeclarationKind.SELECT);
320326
assertThat(mgr.visit(selectedElem, new ConstantsVisitor(true)))
321327
.containsExactly(BigInteger.valueOf(1));
322328

323329
ArrayFormula<IntegerFormula, IntegerFormula> store = amgr.store(arr, index, elem);
324-
assertThat(mgr.visit(store, new FunctionDeclarationVisitorNoOther()))
330+
assertThat(mgr.visit(store, new FunctionDeclarationVisitorNoOther(mgr)))
325331
.containsExactly(FunctionDeclarationKind.STORE);
326332
assertThat(mgr.visit(store, new ConstantsVisitor(true)))
327333
.containsExactly(BigInteger.valueOf(1), BigInteger.valueOf(123));
@@ -332,7 +338,7 @@ public void arrayVisit() {
332338
.isNotEqualTo(Solvers.OPENSMT);
333339

334340
ArrayFormula<IntegerFormula, IntegerFormula> initializedArr = amgr.makeArray(arrayType, elem);
335-
assertThat(mgr.visit(initializedArr, new FunctionDeclarationVisitorNoOther()))
341+
assertThat(mgr.visit(initializedArr, new FunctionDeclarationVisitorNoOther(mgr)))
336342
.containsExactly(FunctionDeclarationKind.CONST);
337343
assertThat(mgr.visit(initializedArr, new ConstantsVisitor(true)))
338344
.containsExactly(BigInteger.valueOf(123));
@@ -351,13 +357,13 @@ public void arrayVisitBitvector() {
351357

352358
var arr = amgr.makeArray("some_array", arrayType);
353359
BitvectorFormula selectedElem = amgr.select(arr, index);
354-
assertThat(mgr.visit(selectedElem, new FunctionDeclarationVisitorNoOther()))
360+
assertThat(mgr.visit(selectedElem, new FunctionDeclarationVisitorNoOther(mgr)))
355361
.containsExactly(FunctionDeclarationKind.SELECT);
356362
assertThat(mgr.visit(selectedElem, new ConstantsVisitor(true)))
357363
.containsExactly(BigInteger.valueOf(17));
358364

359365
var store = amgr.store(arr, index, elem);
360-
assertThat(mgr.visit(store, new FunctionDeclarationVisitorNoOther()))
366+
assertThat(mgr.visit(store, new FunctionDeclarationVisitorNoOther(mgr)))
361367
.containsExactly(FunctionDeclarationKind.STORE);
362368
assertThat(mgr.visit(store, new ConstantsVisitor(true)))
363369
.containsExactly(BigInteger.valueOf(17), BigInteger.valueOf(2));
@@ -368,7 +374,7 @@ public void arrayVisitBitvector() {
368374
.isNotEqualTo(Solvers.OPENSMT);
369375

370376
var initializedArr = amgr.makeArray(arrayType, elem);
371-
assertThat(mgr.visit(initializedArr, new FunctionDeclarationVisitorNoOther()))
377+
assertThat(mgr.visit(initializedArr, new FunctionDeclarationVisitorNoOther(mgr)))
372378
.containsExactly(FunctionDeclarationKind.CONST);
373379
assertThat(mgr.visit(initializedArr, new ConstantsVisitor(true)))
374380
.containsExactly(BigInteger.valueOf(2));
@@ -510,7 +516,7 @@ public void floatIdVisit() {
510516
fpmgr.round(x, FloatingPointRoundingMode.TOWARD_POSITIVE),
511517
fpmgr.round(x, FloatingPointRoundingMode.TOWARD_NEGATIVE),
512518
fpmgr.round(x, FloatingPointRoundingMode.TOWARD_ZERO))) {
513-
mgr.visit(f, new FunctionDeclarationVisitorNoOther());
519+
mgr.visit(f, new FunctionDeclarationVisitorNoOther(mgr));
514520
mgr.visit(f, new FunctionDeclarationVisitorNoUF());
515521
Formula f2 = mgr.transformRecursively(f, new FormulaTransformationVisitor(mgr) {});
516522
assertThat(f2).isEqualTo(f);
@@ -715,7 +721,7 @@ public void stringInBooleanFormulaIdVisit() throws SolverException, InterruptedE
715721
smgr.suffix(x, y),
716722
smgr.in(x, r))) {
717723
mgr.visit(f, new FunctionDeclarationVisitorNoUF());
718-
mgr.visit(f, new FunctionDeclarationVisitorNoOther());
724+
mgr.visit(f, new FunctionDeclarationVisitorNoOther(mgr));
719725
BooleanFormula f2 = mgr.transformRecursively(f, new FormulaTransformationVisitor(mgr) {});
720726
assertThat(f2).isEqualTo(f);
721727
assertThatFormula(f).isEquivalentTo(f2);
@@ -743,7 +749,7 @@ public void stringInStringFormulaVisit() throws SolverException, InterruptedExce
743749
}
744750
for (StringFormula f : formulas.build()) {
745751
mgr.visit(f, new FunctionDeclarationVisitorNoUF());
746-
mgr.visit(f, new FunctionDeclarationVisitorNoOther());
752+
mgr.visit(f, new FunctionDeclarationVisitorNoOther(mgr));
747753
StringFormula f2 = mgr.transformRecursively(f, new FormulaTransformationVisitor(mgr) {});
748754
assertThat(f2).isEqualTo(f);
749755
assertThatFormula(bmgr.not(smgr.equal(f, f2))).isUnsatisfiable();
@@ -768,7 +774,7 @@ public void stringInRegexFormulaVisit() {
768774
}
769775
for (RegexFormula f : formulas.build()) {
770776
mgr.visit(f, new FunctionDeclarationVisitorNoUF());
771-
mgr.visit(f, new FunctionDeclarationVisitorNoOther());
777+
mgr.visit(f, new FunctionDeclarationVisitorNoOther(mgr));
772778
RegexFormula f2 = mgr.transformRecursively(f, new FormulaTransformationVisitor(mgr) {});
773779
assertThat(f2).isEqualTo(f);
774780
}
@@ -784,15 +790,15 @@ public void stringInIntegerFormulaVisit() throws SolverException, InterruptedExc
784790
for (IntegerFormula f :
785791
ImmutableList.of(smgr.indexOf(x, y, offset), smgr.length(x), smgr.toIntegerFormula(x))) {
786792
mgr.visit(f, new FunctionDeclarationVisitorNoUF());
787-
mgr.visit(f, new FunctionDeclarationVisitorNoOther());
793+
mgr.visit(f, new FunctionDeclarationVisitorNoOther(mgr));
788794
IntegerFormula f2 = mgr.transformRecursively(f, new FormulaTransformationVisitor(mgr) {});
789795
assertThat(f2).isEqualTo(f);
790796
assertThatFormula(bmgr.not(imgr.equal(f, f2))).isUnsatisfiable();
791797
}
792798
}
793799

794800
private void checkKind(Formula f, FunctionDeclarationKind expected) {
795-
FunctionDeclarationVisitorNoOther visitor = new FunctionDeclarationVisitorNoOther();
801+
FunctionDeclarationVisitorNoOther visitor = new FunctionDeclarationVisitorNoOther(mgr);
796802
mgr.visit(f, visitor);
797803
Truth.assert_()
798804
.withMessage(

0 commit comments

Comments
 (0)