Lazy load Z3 in CLI tools, fixes #50

build.gradle.kts

@@ -10,7 +10,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.inf.theta"
-    version = "2.6.0"
+    version = "2.6.1"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

doc/Development.md

@@ -20,6 +20,7 @@ We usually develop on separate branches and increment the version number just be
 As the main repository is read-only, we suggest you to create your own [fork](https://help.github.com/articles/fork-a-repo/). Within your fork, we also recommend to create new _branches_ for your development. This enables us later on to easily integrate your work into the main repository by using [pull requests](https://help.github.com/articles/about-pull-requests/).
 
 As the framework is under development, we suggest you to [sync your fork](https://help.github.com/articles/syncing-a-fork/) often and merge the master branch into your development branch(es).
+If you are confident that only you are working on your branch, you can also [rebase instead of merge](https://www.atlassian.com/git/tutorials/merging-vs-rebasing), but be careful.
 
 ## Building
 

subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java

@@ -16,10 +16,6 @@
 package hu.bme.mit.theta.cfa.cli;
 
 import java.io.*;
-import java.util.HashSet;
-import java.util.LinkedList;
-import java.util.Queue;
-import java.util.Set;
 import java.util.concurrent.TimeUnit;
 import java.util.stream.Stream;
 
@@ -58,16 +54,6 @@
 import hu.bme.mit.theta.common.table.TableWriter;
 import hu.bme.mit.theta.common.visualization.Graph;
 import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter;
-import hu.bme.mit.theta.core.stmt.AssignStmt;
-import hu.bme.mit.theta.core.stmt.AssumeStmt;
-import hu.bme.mit.theta.core.stmt.HavocStmt;
-import hu.bme.mit.theta.core.type.arraytype.ArrayType;
-import hu.bme.mit.theta.core.type.booltype.BoolExprs;
-import hu.bme.mit.theta.core.type.booltype.BoolType;
-import hu.bme.mit.theta.core.type.bvtype.BvExprs;
-import hu.bme.mit.theta.core.type.bvtype.BvType;
-import hu.bme.mit.theta.core.type.inttype.IntExprs;
-import hu.bme.mit.theta.core.type.inttype.IntType;
 import hu.bme.mit.theta.solver.*;
 import hu.bme.mit.theta.solver.z3.*;
 
@@ -76,7 +62,6 @@
  */
 public class CfaCli {
 	private static final String JAR_NAME = "theta-cfa-cli.jar";
-	private final SolverFactory solverFactory = Z3SolverFactory.getInstance();
 	private final String[] args;
 	private final TableWriter writer;
 
@@ -213,7 +198,8 @@ private CFA loadModel() throws Exception {
 
 	private CfaConfig<?, ?, ?> buildConfiguration(final CFA cfa) throws Exception {
 		try {
-			return new CfaConfigBuilder(domain, refinement, solverFactory).precGranularity(precGranularity).search(search)
+			return new CfaConfigBuilder(domain, refinement, Z3SolverFactory.getInstance())
+					.precGranularity(precGranularity).search(search)
 					.predSplit(predSplit).encoding(encoding).maxEnum(maxEnum).initPrec(initPrec)
 					.pruneStrategy(pruneStrategy).logger(logger).build(cfa);
 		} catch (final Exception ex) {
@@ -267,16 +253,14 @@ private void printError(final Throwable ex) {
 		}
 	}
 
-	private void writeCex(final Unsafe<?, ?> status) {
+	private void writeCex(final Unsafe<?, ?> status) throws FileNotFoundException {
 		@SuppressWarnings("unchecked") final Trace<CfaState<?>, CfaAction> trace = (Trace<CfaState<?>, CfaAction>) status.getTrace();
-		final Trace<CfaState<ExplState>, CfaAction> concrTrace = CfaTraceConcretizer.concretize(trace, solverFactory);
+		final Trace<CfaState<ExplState>, CfaAction> concrTrace = CfaTraceConcretizer.concretize(trace, Z3SolverFactory.getInstance());
 		final File file = new File(cexfile);
 		PrintWriter printWriter = null;
 		try {
 			printWriter = new PrintWriter(file);
 			printWriter.write(concrTrace.toString());
-		} catch (final FileNotFoundException e) {
-			printError(e);
 		} finally {
 			if (printWriter != null) {
 				printWriter.close();

subprojects/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java

@@ -65,7 +65,6 @@
  */
 public class StsCli {
 	private static final String JAR_NAME = "theta-sts-cli.jar";
-	private final SolverFactory solverFactory = Z3SolverFactory.getInstance();
 	private final String[] args;
 	private final TableWriter writer;
 
@@ -193,7 +192,8 @@ private STS loadModel() throws Exception {
 
 	private StsConfig<?, ?, ?> buildConfiguration(final STS sts) throws Exception {
 		try {
-			return new StsConfigBuilder(domain, refinement, solverFactory).initPrec(initPrec).search(search)
+			return new StsConfigBuilder(domain, refinement, Z3SolverFactory.getInstance())
+					.initPrec(initPrec).search(search)
 					.predSplit(predSplit).pruneStrategy(pruneStrategy).logger(logger).build(sts);
 		} catch (final Exception ex) {
 			throw new Exception("Could not create configuration: " + ex.getMessage(), ex);
@@ -240,18 +240,16 @@ private void printError(final Throwable ex) {
 		}
 	}
 
-	private void writeCex(final STS sts, final SafetyResult.Unsafe<?, ?> status) {
+	private void writeCex(final STS sts, final SafetyResult.Unsafe<?, ?> status) throws FileNotFoundException {
 		@SuppressWarnings("unchecked") final Trace<ExprState, StsAction> trace = (Trace<ExprState, StsAction>) status.getTrace();
-		final Trace<Valuation, StsAction> concrTrace = StsTraceConcretizer.concretize(sts, trace, solverFactory);
+		final Trace<Valuation, StsAction> concrTrace = StsTraceConcretizer.concretize(sts, trace, Z3SolverFactory.getInstance());
 		final File file = new File(cexfile);
 		PrintWriter printWriter = null;
 		try {
 			printWriter = new PrintWriter(file);
 			for (Valuation state : concrTrace.getStates()) {
 				printWriter.println(state.toString());
 			}
-		} catch (final FileNotFoundException e) {
-			printError(e);
 		} finally {
 			if (printWriter != null) {
 				printWriter.close();

subprojects/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java

@@ -45,7 +45,6 @@
 public class XstsCli {
 
 	private static final String JAR_NAME = "theta-xsts-cli.jar";
-	private final SolverFactory solverFactory = Z3SolverFactory.getInstance();
 	private final String[] args;
 	private final TableWriter writer;
 
@@ -174,8 +173,9 @@ private XSTS loadModel() throws Exception {
 
 	private XstsConfig<?, ?, ?> buildConfiguration(final XSTS xsts) throws Exception {
 		try {
-			return new XstsConfigBuilder(domain, refinement, solverFactory).maxEnum(maxEnum).initPrec(initPrec)
-					.pruneStrategy(pruneStrategy).search(search).predSplit(predSplit).logger(logger).build(xsts);
+			return new XstsConfigBuilder(domain, refinement, Z3SolverFactory.getInstance())
+					.maxEnum(maxEnum).initPrec(initPrec).pruneStrategy(pruneStrategy)
+					.search(search).predSplit(predSplit).logger(logger).build(xsts);
 		} catch (final Exception ex) {
 			throw new Exception("Could not create configuration: " + ex.getMessage(), ex);
 		}
@@ -220,18 +220,16 @@ private void printError(final Throwable ex) {
 		}
 	}
 
-	private void writeCex(final SafetyResult.Unsafe<?, ?> status, final XSTS xsts) {
+	private void writeCex(final SafetyResult.Unsafe<?, ?> status, final XSTS xsts) throws FileNotFoundException {
 		//TODO remove temp vars, replace int values with literals
 
 		@SuppressWarnings("unchecked") final Trace<XstsState<?>, XstsAction> trace = (Trace<XstsState<?>, XstsAction>) status.getTrace();
-		final XstsStateSequence concrTrace = XstsTraceConcretizerUtil.concretize(trace, solverFactory, xsts);
+		final XstsStateSequence concrTrace = XstsTraceConcretizerUtil.concretize(trace, Z3SolverFactory.getInstance(), xsts);
 		final File file = new File(cexfile);
 		PrintWriter printWriter = null;
 		try {
 			printWriter = new PrintWriter(file);
 			printWriter.write(concrTrace.toString());
-		} catch (final FileNotFoundException e) {
-			printError(e);
 		} finally {
 			if (printWriter != null) {
 				printWriter.close();