package de.bmoth.backend.translator;

import static org.junit.Assert.assertEquals;

import java.math.BigInteger;

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.SolverContext;
import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
import org.sosy_lab.java_smt.api.SolverException;

public class SMTSolverConnectionTest {

	@Test
	public void testSimpleSMTCall() 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));
			}
		}
	}

}

@@ -1104,15 +1104,1105 @@
 mple
-SMT
 Call
+ToSMTINTERPOL()%0A%09%09%09throws InvalidConfigurationException, SolverException, InterruptedException %7B%0A%09%09Configuration config = Configuration.defaultConfiguration();%0A%09%09LogManager logger = BasicLogManager.create(config);%0A%09%09ShutdownManager shutdown = ShutdownManager.create();%0A%0A%09%09SolverContext context = SolverContextFactory.createSolverContext(config, logger, shutdown.getNotifier(),%0A%09%09%09%09Solvers.SMTINTERPOL);%0A%09%09FormulaManager fmgr = context.getFormulaManager();%0A%0A%09%09BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager();%0A%09%09IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager();%0A%0A%09%09IntegerFormula a = imgr.makeVariable(%22a%22), b = imgr.makeVariable(%22b%22);%0A%09%09BooleanFormula constraint = bmgr.and(imgr.equal(a, b), imgr.equal(a, imgr.makeNumber(5)));%0A%0A%09%09try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) %7B%0A%09%09%09prover.addConstraint(constraint);%0A%09%09%09boolean isUnsat = prover.isUnsat();%0A%09%09%09if (!isUnsat) %7B%0A%09%09%09%09Model model = prover.getModel();%0A%09%09%09%09assertEquals(BigInteger.valueOf(5), model.evaluate(b));%0A%09%09%09%7D%0A%09%09%7D%0A%09%7D%0A%0A%09@Test%0A%09public void testSimpleCallToZ3
 () t
@@ -2566,35 +2566,26 @@
 %09%09%09%09Solvers.
-SMTINTERPOL
+Z3
 );%0A%09%09Formula

add z3 test