package de.bmoth.backend.translator;

import static org.junit.Assert.assertEquals;

import java.math.BigInteger;
import java.util.ArrayList;
import java.util.Arrays;

import org.junit.Test;
import org.sosy_lab.common.ShutdownManager;
import org.sosy_lab.common.configuration.Configuration;
import org.sosy_lab.common.configuration.InvalidConfigurationException;
import org.sosy_lab.common.log.BasicLogManager;
import org.sosy_lab.common.log.LogManager;
import org.sosy_lab.java_smt.SolverContextFactory;
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
import org.sosy_lab.java_smt.api.BooleanFormula;
import org.sosy_lab.java_smt.api.BooleanFormulaManager;
import org.sosy_lab.java_smt.api.FormulaManager;
import org.sosy_lab.java_smt.api.IntegerFormulaManager;
import org.sosy_lab.java_smt.api.Model;
import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
import org.sosy_lab.java_smt.api.ProverEnvironment;
import org.sosy_lab.java_smt.api.QuantifiedFormulaManager;
import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier;
import org.sosy_lab.java_smt.api.SolverContext;
import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
import org.sosy_lab.java_smt.api.SolverException;

public class SMTSolverConnectionTest {

	@Test
	public void testSimpleCallToSMTINTERPOL()
			throws InvalidConfigurationException, SolverException, InterruptedException {
		Configuration config = Configuration.defaultConfiguration();
		LogManager logger = BasicLogManager.create(config);
		ShutdownManager shutdown = ShutdownManager.create();

		SolverContext context = SolverContextFactory.createSolverContext(config, logger, shutdown.getNotifier(),
				Solvers.SMTINTERPOL);
		FormulaManager fmgr = context.getFormulaManager();

		BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager();
		IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager();

		IntegerFormula a = imgr.makeVariable("a"), b = imgr.makeVariable("b");
		BooleanFormula constraint = bmgr.and(imgr.equal(a, b), imgr.equal(a, imgr.makeNumber(5)));

		try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
			prover.addConstraint(constraint);
			boolean isUnsat = prover.isUnsat();
			if (!isUnsat) {
				Model model = prover.getModel();
				assertEquals(BigInteger.valueOf(5), model.evaluate(b));
			}
		}
	}

	@Test(expected = UnsupportedOperationException.class)
	public void testNoQuantifiersInSMTINTERPOL()
			throws InvalidConfigurationException, SolverException, InterruptedException {
		Configuration config = Configuration.defaultConfiguration();
		LogManager logger = BasicLogManager.create(config);
		ShutdownManager shutdown = ShutdownManager.create();

		SolverContext context = SolverContextFactory.createSolverContext(config, logger, shutdown.getNotifier(),
				Solvers.SMTINTERPOL);
		FormulaManager fmgr = context.getFormulaManager();

		BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager();
		IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager();
		QuantifiedFormulaManager qmgr = fmgr.getQuantifiedFormulaManager();

		IntegerFormula a = imgr.makeVariable("a"), b = imgr.makeVariable("b");
		BooleanFormula constraint = bmgr.and(imgr.equal(a, b), imgr.equal(a, imgr.makeNumber(5)));
		BooleanFormula quantified = qmgr.mkQuantifier(Quantifier.EXISTS,
				new ArrayList<IntegerFormula>(Arrays.asList(a, b)), constraint);

		try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
			prover.addConstraint(quantified);
			boolean isUnsat = prover.isUnsat();
			if (!isUnsat) {
				Model model = prover.getModel();
				assertEquals(BigInteger.valueOf(5), model.evaluate(b));
			}
		}
	}

	@Test
	public void testSimpleCallToZ3() throws InvalidConfigurationException, SolverException, InterruptedException {
		Configuration config = Configuration.defaultConfiguration();
		LogManager logger = BasicLogManager.create(config);
		ShutdownManager shutdown = ShutdownManager.create();

		SolverContext context = SolverContextFactory.createSolverContext(config, logger, shutdown.getNotifier(),
				Solvers.Z3);
		FormulaManager fmgr = context.getFormulaManager();

		BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager();
		IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager();

		IntegerFormula a = imgr.makeVariable("a"), b = imgr.makeVariable("b");
		BooleanFormula constraint = bmgr.and(imgr.equal(a, b), imgr.equal(a, imgr.makeNumber(5)));

		try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
			prover.addConstraint(constraint);
			boolean isUnsat = prover.isUnsat();
			if (!isUnsat) {
				Model model = prover.getModel();
				assertEquals(BigInteger.valueOf(5), model.evaluate(b));
			}
		}
	}

}

@@ -75,16 +75,60 @@
 tEquals;
+%0Aimport static org.junit.Assert.assertFalse;
 %0A%0Aimport
@@ -258,242 +258,51 @@
 mon.
-ShutdownManager;%0Aimport org.sosy_lab.common.configuration.Configuration;%0Aimport org.sosy_lab.common.configuration.InvalidConfigurationException;%0Aimport org.sosy_lab.common.log.BasicLogManager;%0Aimport org.sosy_lab.common.log.LogManager
+configuration.InvalidConfigurationException
 ;%0Aim
@@ -1065,16 +1065,65 @@
 ption;%0A%0A
+import com.google.common.collect.ImmutableList;%0A%0A
 public c
@@ -1289,181 +1289,8 @@
 n %7B%0A
-%09%09Configuration config = Configuration.defaultConfiguration();%0A%09%09LogManager logger = BasicLogManager.create(config);%0A%09%09ShutdownManager shutdown = ShutdownManager.create();%0A%0A
 %09%09So
@@ -1356,52 +1356,8 @@
 ext(
-config, logger, shutdown.getNotifier(),%0A%09%09%09%09
 Solv
@@ -2212,181 +2212,8 @@
 n %7B%0A
-%09%09Configuration config = Configuration.defaultConfiguration();%0A%09%09LogManager logger = BasicLogManager.create(config);%0A%09%09ShutdownManager shutdown = ShutdownManager.create();%0A%0A
 %09%09So
@@ -2279,52 +2279,8 @@
 ext(
-config, logger, shutdown.getNotifier(),%0A%09%09%09%09
 Solv
@@ -3278,181 +3278,8 @@
 n %7B%0A
-%09%09Configuration config = Configuration.defaultConfiguration();%0A%09%09LogManager logger = BasicLogManager.create(config);%0A%09%09ShutdownManager shutdown = ShutdownManager.create();%0A%0A
 %09%09So
@@ -3345,52 +3345,8 @@
 ext(
-config, logger, shutdown.getNotifier(),%0A%09%09%09%09
 Solv
@@ -3869,32 +3869,57 @@
 over.isUnsat();%0A
+%09%09%09assertFalse(isUnsat);%0A
 %09%09%09if (!isUnsat)
@@ -3950,32 +3950,92 @@
 ver.getModel();%0A
+%09%09%09%09assertEquals(BigInteger.valueOf(5), model.evaluate(a));%0A
 %09%09%09%09assertEquals

simplify test cases