Merge pull request #82 from ftsrg/bitvector-algs

Advanced refinement algorithms supporting bitvectors
ftsrg · Sep 10, 2020 · 949b632 · 949b632
2 parents 9c0395d + 58d62b5
commit 949b632
Show file tree

Hide file tree

Showing 16 changed files with 1,290 additions and 27 deletions.
diff --git a/build.gradle.kts b/build.gradle.kts
@@ -10,7 +10,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.inf.theta"
-    version = "2.3.0"
+    version = "2.4.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

diff --git a/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/BasicExprState.java b/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/BasicExprState.java
@@ -18,6 +18,7 @@
 import static com.google.common.base.Preconditions.checkNotNull;
 import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False;
 
+import hu.bme.mit.theta.common.Utils;
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
 
@@ -43,4 +44,8 @@ public boolean isBottom() {
 		return expr.equals(False());
 	}
 
+	@Override
+	public String toString() {
+		return Utils.lispStringBuilder(getClass().getSimpleName()).body().add(expr).toString();
+	}
 }
diff --git a/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/ExprTraceUtils.java b/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/ExprTraceUtils.java
@@ -33,7 +33,7 @@ public final class ExprTraceUtils {
 	private ExprTraceUtils() {
 	}
 
-	public static Trace<ExprState, ExprAction> traceFrom(final List<? extends ExprAction> actions) {
+	public static <A extends ExprAction> Trace<ExprState, A> traceFrom(final List<? extends A> actions) {
 		checkNotNull(actions);
 		final List<ExprState> states = new ArrayList<>(actions.size() + 1);
 		for (int i = 0; i < actions.size() + 1; i++) {