Skip to content

Commit f452b34

Browse files
daniel-rafflerdaniel-raffler
committed
Merge remote-tracking branch 'origin/master' into 371-better-performance-in-floatingpointmanagertest
2 parents 9718a18 + e697ed6 commit f452b34

File tree

8 files changed

+294
-19
lines changed

8 files changed

+294
-19
lines changed

‎src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -181,6 +181,24 @@ public enum FunctionDeclarationKind {
181181
/** Arithmetic right-shift over bitvectors (fill from left with value of first bit). */
182182
BV_ASHR,
183183

184+
/** Performs a circular left rotation on the bitvector. */
185+
BV_ROTATE_LEFT,
186+
187+
/** Performs a circular right rotation on the bitvector. */
188+
BV_ROTATE_RIGHT,
189+
190+
/**
191+
* Performs a circular left rotation on the bitvector by a specified number of positions,
192+
* determined by an integer value.
193+
*/
194+
BV_ROTATE_LEFT_BY_INT,
195+
196+
/**
197+
* Performs a circular right rotation on the bitvector by a specified number of positions,
198+
* determined by an integer value.
199+
*/
200+
BV_ROTATE_RIGHT_BY_INT,
201+
184202
/** Cast an unsigned bitvector to a floating-point number. */
185203
BV_UCASTTO_FP,
186204

‎src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -326,8 +326,16 @@ private FunctionDeclarationKind getDeclarationKind(Term term) {
326326
return FunctionDeclarationKind.FP_CASTTO_UBV;
327327
} else if (kind.equals(Kind.BV_XOR)) {
328328
return FunctionDeclarationKind.BV_XOR;
329+
} else if (kind.equals(Kind.BV_ROL)) {
330+
return FunctionDeclarationKind.BV_ROTATE_LEFT;
331+
} else if (kind.equals(Kind.BV_ROR)) {
332+
return FunctionDeclarationKind.BV_ROTATE_RIGHT;
333+
} else if (kind.equals(Kind.BV_ROLI)) {
334+
return FunctionDeclarationKind.BV_ROTATE_LEFT_BY_INT;
335+
} else if (kind.equals(Kind.BV_RORI)) {
336+
return FunctionDeclarationKind.BV_ROTATE_RIGHT_BY_INT;
329337
}
330-
throw new UnsupportedOperationException("Can not discern formula kind " + kind);
338+
return FunctionDeclarationKind.OTHER;
331339
}
332340

333341
@SuppressWarnings("unchecked")

‎src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -458,6 +458,8 @@ private Expr normalize(Expr operator) {
458458
.put(Kind.BITVECTOR_SHL, FunctionDeclarationKind.BV_SHL)
459459
.put(Kind.BITVECTOR_ASHR, FunctionDeclarationKind.BV_ASHR)
460460
.put(Kind.BITVECTOR_LSHR, FunctionDeclarationKind.BV_LSHR)
461+
.put(Kind.BITVECTOR_ROTATE_LEFT, FunctionDeclarationKind.BV_ROTATE_LEFT_BY_INT)
462+
.put(Kind.BITVECTOR_ROTATE_RIGHT, FunctionDeclarationKind.BV_ROTATE_RIGHT_BY_INT)
461463
.put(Kind.BITVECTOR_NOT, FunctionDeclarationKind.BV_NOT)
462464
.put(Kind.BITVECTOR_NEG, FunctionDeclarationKind.BV_NEG)
463465
.put(Kind.BITVECTOR_EXTRACT, FunctionDeclarationKind.BV_EXTRACT)

‎src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -578,6 +578,8 @@ private Term normalize(Term operator) {
578578
.put(Kind.BITVECTOR_SHL, FunctionDeclarationKind.BV_SHL)
579579
.put(Kind.BITVECTOR_ASHR, FunctionDeclarationKind.BV_ASHR)
580580
.put(Kind.BITVECTOR_LSHR, FunctionDeclarationKind.BV_LSHR)
581+
.put(Kind.BITVECTOR_ROTATE_LEFT, FunctionDeclarationKind.BV_ROTATE_LEFT_BY_INT)
582+
.put(Kind.BITVECTOR_ROTATE_RIGHT, FunctionDeclarationKind.BV_ROTATE_RIGHT_BY_INT)
581583
// Floating-point theory
582584
.put(Kind.TO_INTEGER, FunctionDeclarationKind.FLOOR)
583585
.put(Kind.TO_REAL, FunctionDeclarationKind.TO_REAL)

‎src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,8 @@
2323
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_NEG;
2424
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_NOT;
2525
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_OR;
26+
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_ROL;
27+
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_ROR;
2628
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_SDIV;
2729
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_SEXT;
2830
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_SLE;
@@ -458,6 +460,10 @@ private FunctionDeclarationKind getDeclarationKind(long pF) {
458460
return FunctionDeclarationKind.BV_SIGN_EXTENSION;
459461
case MSAT_TAG_BV_ZEXT:
460462
return FunctionDeclarationKind.BV_ZERO_EXTENSION;
463+
case MSAT_TAG_BV_ROL:
464+
return FunctionDeclarationKind.BV_ROTATE_LEFT_BY_INT;
465+
case MSAT_TAG_BV_ROR:
466+
return FunctionDeclarationKind.BV_ROTATE_RIGHT_BY_INT;
461467

462468
case MSAT_TAG_FP_NEG:
463469
return FunctionDeclarationKind.FP_NEG;

‎src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -707,6 +707,14 @@ private FunctionDeclarationKind getDeclarationKind(long f) {
707707
return FunctionDeclarationKind.BV_SIGN_EXTENSION;
708708
case Z3_OP_ZERO_EXT:
709709
return FunctionDeclarationKind.BV_ZERO_EXTENSION;
710+
case Z3_OP_ROTATE_LEFT:
711+
return FunctionDeclarationKind.BV_ROTATE_LEFT_BY_INT;
712+
case Z3_OP_ROTATE_RIGHT:
713+
return FunctionDeclarationKind.BV_ROTATE_RIGHT_BY_INT;
714+
case Z3_OP_EXT_ROTATE_LEFT:
715+
return FunctionDeclarationKind.BV_ROTATE_LEFT;
716+
case Z3_OP_EXT_ROTATE_RIGHT:
717+
return FunctionDeclarationKind.BV_ROTATE_RIGHT;
710718

711719
case Z3_OP_FPA_NEG:
712720
return FunctionDeclarationKind.FP_NEG;

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

Lines changed: 221 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,221 @@
1+
/*
2+
* This file is part of JavaSMT,
3+
* an API wrapper for a collection of SMT solvers:
4+
* https://github.com/sosy-lab/java-smt
5+
*
6+
* SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
7+
*
8+
* SPDX-License-Identifier: Apache-2.0
9+
*/
10+
11+
package org.sosy_lab.java_smt.test;
12+
13+
import static com.google.common.truth.Truth.assertThat;
14+
15+
import org.junit.Before;
16+
import org.junit.Test;
17+
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;
20+
21+
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+
35+
@Test
36+
public void rotateLeftTest() {
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)));
96+
}
97+
98+
@Test
99+
public void rotateRightTest() {
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+
}
156+
}
157+
158+
@Test
159+
public void rotateLeftIntegerTest() {
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+
}
188+
}
189+
190+
@Test
191+
public void rotateRightIntegerTest() {
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+
}
220+
}
221+
}

0 commit comments

Comments
 (0)