Update z3 solver docs, fix typo

subprojects/analysis/src/test/java/hu/bme/mit/theta/analysis/expl/ExplInitFuncTest.java

@@ -37,7 +37,7 @@
 public class ExplInitFuncTest {
 	private final VarDecl<IntType> x = Var("x", Int());
 	private final VarDecl<IntType> y = Var("y", Int());
-	private final Solver solver = Z3SolverFactory.getInstace().createSolver();
+	private final Solver solver = Z3SolverFactory.getInstance().createSolver();
 
 	@Test
 	public void test1() {

subprojects/analysis/src/test/java/hu/bme/mit/theta/analysis/expl/ExplStatePredicateTest.java

@@ -44,7 +44,7 @@
 public class ExplStatePredicateTest {
 
 	private static final VarDecl<IntType> x = Var("x", Int());
-	private final Solver solver = Z3SolverFactory.getInstace().createSolver();
+	private final Solver solver = Z3SolverFactory.getInstance().createSolver();
 
 	@Parameter(value = 0)
 	public Expr<BoolType> expr;

subprojects/analysis/src/test/java/hu/bme/mit/theta/analysis/expl/ExplStmtTransFuncTest.java

@@ -49,7 +49,7 @@
 import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
 
 public class ExplStmtTransFuncTest {
-	private final Solver solver = Z3SolverFactory.getInstace().createSolver();
+	private final Solver solver = Z3SolverFactory.getInstance().createSolver();
 	private final VarDecl<IntType> x = Var("x", Int());
 	private final VarDecl<IntType> y = Var("y", Int());
 

subprojects/analysis/src/test/java/hu/bme/mit/theta/analysis/expl/ExplTransFuncTest.java

@@ -44,7 +44,7 @@ public class ExplTransFuncTest {
 	private final ExplPrec prec = ExplPrec.of(ImmutableList.of(x));
 	private final ExplState state = ExplState.of(ImmutableValuation.builder().put(x, Int(1)).build());
 
-	ExplTransFunc transFunc = ExplTransFunc.create(Z3SolverFactory.getInstace().createSolver());
+	ExplTransFunc transFunc = ExplTransFunc.create(Z3SolverFactory.getInstance().createSolver());
 
 	@Test
 	public void testNormal() {

subprojects/analysis/src/test/java/hu/bme/mit/theta/analysis/expr/ExprOrdLeqTest.java

@@ -72,7 +72,7 @@ public static Collection<Object[]> data() {
 
 	@Test
 	public void testIsTop() {
-		final Solver solver = Z3SolverFactory.getInstace().createSolver();
+		final Solver solver = Z3SolverFactory.getInstance().createSolver();
 		final PartialOrd<ExprState> ord = ExprOrd.create(solver);
 		assertEquals(ord.isLeq(state1, state2), leq);
 	}

subprojects/analysis/src/test/java/hu/bme/mit/theta/analysis/expr/ExprStatesTest.java

@@ -38,7 +38,7 @@ public class ExprStatesTest {
 
 	private final VarDecl<IntType> vx = Var("x", Int());
 	private final ExplPrec prec = ExplPrec.of(Collections.singleton(vx));
-	private final Solver solver = Z3SolverFactory.getInstace().createSolver();
+	private final Solver solver = Z3SolverFactory.getInstance().createSolver();
 
 	@Test
 	public void test1() {

subprojects/analysis/src/test/java/hu/bme/mit/theta/analysis/expr/ExprTraceCheckersTest.java

@@ -55,7 +55,7 @@ public final class ExprTraceCheckersTest {
 
 	@Before
 	public void before() {
-		final ItpSolver solver = Z3SolverFactory.getInstace().createItpSolver();
+		final ItpSolver solver = Z3SolverFactory.getInstance().createItpSolver();
 		traceCheckers = new ArrayList<>();
 		traceCheckers.add(ExprTraceSeqItpChecker.create(True(), True(), solver));
 		traceCheckers.add(ExprTraceFwBinItpChecker.create(True(), True(), solver));

subprojects/analysis/src/test/java/hu/bme/mit/theta/analysis/pred/PredInitFuncTest.java

@@ -41,7 +41,7 @@ public class PredInitFuncTest {
 
 	private final VarDecl<IntType> x = Var("x", Int());
 	private final VarDecl<IntType> y = Var("y", Int());
-	private final Solver solver = Z3SolverFactory.getInstace().createSolver();
+	private final Solver solver = Z3SolverFactory.getInstance().createSolver();
 	private final PredAbstractor predAbstractor = PredAbstractors.booleanSplitAbstractor(solver);
 
 	@Test

subprojects/analysis/src/test/java/hu/bme/mit/theta/analysis/pred/PredOrdTest.java

@@ -31,7 +31,7 @@
 public class PredOrdTest {
 	private final VarDecl<IntType> VX = Decls.Var("x", Int());
 
-	private final PredOrd ord = PredOrd.create(Z3SolverFactory.getInstace().createSolver());
+	private final PredOrd ord = PredOrd.create(Z3SolverFactory.getInstance().createSolver());
 
 	PredState sb = PredState.of(False());
 	PredState s1 = PredState.of(Gt(VX.getRef(), Int(1)));

subprojects/analysis/src/test/java/hu/bme/mit/theta/analysis/pred/PredTransFuncTest.java

@@ -44,7 +44,7 @@
 public class PredTransFuncTest {
 	private final VarDecl<IntType> x = Var("x", Int());
 	private final VarDecl<IntType> y = Var("y", Int());
-	private final Solver solver = Z3SolverFactory.getInstace().createSolver();
+	private final Solver solver = Z3SolverFactory.getInstance().createSolver();
 	private final PredTransFunc transFunc = PredTransFunc.create(PredAbstractors.booleanSplitAbstractor(solver));
 
 	@Test

subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java

@@ -31,7 +31,6 @@
 import hu.bme.mit.theta.analysis.unit.UnitPrec;
 import hu.bme.mit.theta.analysis.utils.ArgVisualizer;
 import hu.bme.mit.theta.cfa.CFA;
-import hu.bme.mit.theta.cfa.analysis.impact.PredImpactChecker;
 import hu.bme.mit.theta.cfa.analysis.lts.CfaLbeLts;
 import hu.bme.mit.theta.cfa.dsl.CfaDslManager;
 import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter;
@@ -46,7 +45,7 @@ public void test() throws FileNotFoundException, IOException {
 		// Arrange
 		final CFA cfa = CfaDslManager.createCfa(new FileInputStream("src/test/resources/counter5_true.cfa"));
 
-		final ItpSolver solver = Z3SolverFactory.getInstace().createItpSolver();
+		final ItpSolver solver = Z3SolverFactory.getInstance().createItpSolver();
 
 		final PredImpactChecker checker = PredImpactChecker.create(CfaLbeLts.getInstance(), cfa.getInitLoc(),
 				l -> l.equals(cfa.getErrorLoc()), solver);

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

@@ -56,7 +56,7 @@
  */
 public class CfaCli {
 	private static final String JAR_NAME = "theta-cfa-cli.jar";
-	private final SolverFactory solverFactory = Z3SolverFactory.getInstace();
+	private final SolverFactory solverFactory = Z3SolverFactory.getInstance();
 	private final String[] args;
 	private final TableWriter writer;
 

subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3SolverFactory.java

@@ -24,18 +24,18 @@
 
 public final class Z3SolverFactory implements SolverFactory {
 
-	private static final Z3SolverFactory INSTACE;
+	private static final Z3SolverFactory INSTANCE;
 
 	static {
 		loadLibraries();
-		INSTACE = new Z3SolverFactory();
+		INSTANCE = new Z3SolverFactory();
 	}
 
 	private Z3SolverFactory() {
 	}
 
-	public static Z3SolverFactory getInstace() {
-		return INSTACE;
+	public static Z3SolverFactory getInstance() {
+		return INSTANCE;
 	}
 
 	private static void loadLibraries() {

subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/package-info.java

@@ -1,8 +1,8 @@
 /**
  * This package contains the wrapper classes for Z3. Normally, only
- * {@link Z3SolverFactory} should be used from this project to create solver
- * instances. Then, the common interfaces should be preferred (e.g.,
- * {@link hu.bme.mit.theta.solver.Solver}).
+ * {@link hu.bme.mit.theta.solver.z3.Z3SolverFactory} should be used
+ * from this project to create solver instances. Then, the common
+ * interfaces should be preferred (e.g., {@link hu.bme.mit.theta.solver.Solver}).
  */
 
 package hu.bme.mit.theta.solver.z3;

subprojects/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/SolverUtilsTest.java

@@ -36,7 +36,7 @@ public class SolverUtilsTest {
 	@Test
 	public void testModels() {
 		// Arrange
-		final SolverFactory factory = Z3SolverFactory.getInstace();
+		final SolverFactory factory = Z3SolverFactory.getInstance();
 
 		final ConstDecl<IntType> cx = Const("x", Int());
 		final ConstDecl<IntType> cy = Const("y", Int());

subprojects/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3ItpSolverTest.java

@@ -59,7 +59,7 @@ public final class Z3ItpSolverTest {
 
 	@Before
 	public void initialize() {
-		solver = Z3SolverFactory.getInstace().createItpSolver();
+		solver = Z3SolverFactory.getInstance().createItpSolver();
 
 		final ConstDecl<IntType> ad = Const("a", Int());
 		final ConstDecl<IntType> bd = Const("b", Int());

subprojects/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3ModelTest.java

@@ -25,7 +25,7 @@
 public final class Z3ModelTest {
 
 	static {
-		Z3SolverFactory.getInstace();
+		Z3SolverFactory.getInstance();
 	}
 
 	@Test

subprojects/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3SolverTest.java

@@ -43,7 +43,7 @@ public final class Z3SolverTest {
 
 	@Test
 	public void testSimple() {
-		final Solver solver = Z3SolverFactory.getInstace().createSolver();
+		final Solver solver = Z3SolverFactory.getInstance().createSolver();
 
 		// Create two integer constants x and y
 		final ConstDecl<IntType> cx = Const("x", Int());
@@ -66,7 +66,7 @@ public void testSimple() {
 
 	@Test
 	public void testTrack() {
-		final Solver solver = Z3SolverFactory.getInstace().createSolver();
+		final Solver solver = Z3SolverFactory.getInstance().createSolver();
 
 		final ConstDecl<BoolType> ca = Const("a", Bool());
 		final Expr<BoolType> expr = And(ca.getRef(), True());
@@ -88,7 +88,7 @@ public void testTrack() {
 	@Test
 	public void testFunc() {
 		// Arrange
-		final Solver solver = Z3SolverFactory.getInstace().createSolver();
+		final Solver solver = Z3SolverFactory.getInstance().createSolver();
 		final ConstDecl<FuncType<IntType, IntType>> ca = Const("a", Func(Int(), Int()));
 		final Expr<FuncType<IntType, IntType>> a = ca.getRef();
 		final ParamDecl<IntType> px = Param("x", Int());

subprojects/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java

@@ -67,8 +67,6 @@
 import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
 import hu.bme.mit.theta.sts.STS;
 import hu.bme.mit.theta.sts.STS.Builder;
-import hu.bme.mit.theta.sts.analysis.StsAction;
-import hu.bme.mit.theta.sts.analysis.StsLts;
 
 public class StsExplTest {
 
@@ -95,7 +93,7 @@ public void test() {
 
 		final STS sts = builder.build();
 
-		final ItpSolver solver = Z3SolverFactory.getInstace().createItpSolver();
+		final ItpSolver solver = Z3SolverFactory.getInstance().createItpSolver();
 
 		final Analysis<ExplState, ExprAction, ExplPrec> analysis = ExplAnalysis.create(solver, sts.getInit());
 		final Predicate<ExprState> target = new ExprStatePredicate(Not(sts.getProp()), solver);

subprojects/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java

@@ -67,12 +67,10 @@
 import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
 import hu.bme.mit.theta.sts.STS;
 import hu.bme.mit.theta.sts.STS.Builder;
-import hu.bme.mit.theta.sts.analysis.StsAction;
-import hu.bme.mit.theta.sts.analysis.StsLts;
 
 public class StsPredTest {
 	final Logger logger = new ConsoleLogger(Level.VERBOSE);
-	final ItpSolver solver = Z3SolverFactory.getInstace().createItpSolver();
+	final ItpSolver solver = Z3SolverFactory.getInstance().createItpSolver();
 	STS sts = null;
 
 	@Before

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

@@ -67,7 +67,7 @@
  */
 public class StsCli {
 	private static final String JAR_NAME = "theta-sts-cli.jar";
-	private final SolverFactory solverFactory = Z3SolverFactory.getInstace();
+	private final SolverFactory solverFactory = Z3SolverFactory.getInstance();
 	private final String[] args;
 	private final TableWriter writer;
 

subprojects/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/LazyXtaCheckerTest.java

@@ -99,7 +99,7 @@ public void test() {
 		final SafetyResult<? extends XtaState<?>, XtaAction> status = checker.check(UnitPrec.getInstance());
 
 		// Assert
-		final ArgChecker argChecker = ArgChecker.create(Z3SolverFactory.getInstace().createSolver());
+		final ArgChecker argChecker = ArgChecker.create(Z3SolverFactory.getInstance().createSolver());
 		final boolean argCheckResult = argChecker.isWellLabeled(status.getArg());
 		assertTrue(argCheckResult);
 	}