package de.bmoth.backend.translator;

import static org.junit.Assert.assertEquals;

import org.junit.After;
import org.junit.Before;
import org.junit.Test;

import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Context;
import com.microsoft.z3.Expr;
import com.microsoft.z3.Solver;
import com.microsoft.z3.Status;

import de.bmoth.backend.FormulaTranslator;

public class FormulaEvaluationTest {

	private Context ctx;
	private Solver s;

	@Before
	public void setup() {
		ctx = new Context();
		s = ctx.mkSolver();
	}

	@After
	public void cleanup() {
		ctx.close();
	}

	@Test
	public void testExpressionFormula() throws Exception {
		String formula = "x = 2 + 3";
		// getting the translated z3 representation of the formula
		BoolExpr constraint = FormulaTranslator.translatePredicate(formula, ctx);

		s.add(constraint);
		Status check = s.check();

		Expr x = ctx.mkIntConst("x");

		assertEquals(Status.SATISFIABLE, check);
		assertEquals(ctx.mkInt(5), s.getModel().eval(x, true));
	}
}

@@ -126,16 +126,41 @@
 Before;%0A
+import org.junit.Ignore;%0A
 import o
@@ -174,16 +174,16 @@
 t.Test;%0A
-
 %0Aimport 
@@ -622,15 +622,13 @@
 test
-Express
+Addit
 ionF
@@ -951,16 +951,16 @@
 check);%0A
-
 %09%09assert
@@ -1011,11 +1011,443 @@
 ue));%0A%09%7D
+%0A%0A%09@Test%0A%09@Ignore%0A%09public void testSubtractionFormula() throws Exception %7B%0A%09%09String formula = %22x = 2 - 3%22;%0A%09%09// getting the translated z3 representation of the formula%0A%09%09BoolExpr constraint = FormulaTranslator.translatePredicate(formula, ctx);%0A%0A%09%09s.add(constraint);%0A%09%09Status check = s.check();%0A%0A%09%09Expr x = ctx.mkIntConst(%22x%22);%0A%0A%09%09assertEquals(Status.SATISFIABLE, check);%0A%09%09assertEquals(ctx.mkInt(-1), s.getModel().eval(x, true));%0A%09%7D
 %0A%7D%0A

add (currently failing) test for subtraction