package performance;

import static org.junit.Assert.assertEquals;

import java.util.Arrays;

import org.junit.Test;

import dev.civl.sarl.SARL;
import dev.civl.sarl.IF.SymbolicUniverse;
import dev.civl.sarl.IF.expr.BooleanExpression;
import dev.civl.sarl.IF.expr.NumericExpression;
import dev.civl.sarl.IF.expr.NumericSymbolicConstant;
import dev.civl.sarl.IF.expr.SymbolicConstant;
import dev.civl.sarl.IF.type.SymbolicArrayType;
import dev.civl.sarl.IF.type.SymbolicFunctionType;
import dev.civl.sarl.IF.type.SymbolicType;

public class PerformanceTest {

	static public BooleanExpression slowNegationFormula(boolean unsat,
			SymbolicUniverse u) {
		// types:
		SymbolicType intType = u.integerType();
		SymbolicArrayType arrayType = u.arrayType(intType);
		SymbolicFunctionType funcType = u.functionType(
				Arrays.asList(arrayType, intType, intType, intType, intType),
				u.booleanType());
		// constants:
		NumericSymbolicConstant X_N = (NumericSymbolicConstant) u
				.symbolicConstant(u.stringObject("X_N"), u.integerType());
		NumericSymbolicConstant Y0 = (NumericSymbolicConstant) u
				.symbolicConstant(u.stringObject("Y0"), intType);
		NumericSymbolicConstant Y1 = (NumericSymbolicConstant) u
				.symbolicConstant(u.stringObject("Y1"), intType);
		NumericSymbolicConstant Y2 = (NumericSymbolicConstant) u
				.symbolicConstant(u.stringObject("Y2"), intType);
		NumericSymbolicConstant Y3 = (NumericSymbolicConstant) u
				.symbolicConstant(u.stringObject("Y3"), intType);
		BooleanExpression Y4 = (BooleanExpression) u
				.symbolicConstant(u.stringObject("Y4"), u.booleanType());
		BooleanExpression Y5 = (BooleanExpression) u
				.symbolicConstant(u.stringObject("Y5"), u.booleanType());
		NumericSymbolicConstant Y6 = (NumericSymbolicConstant) u
				.symbolicConstant(u.stringObject("Y6"), intType);
		NumericSymbolicConstant Y7 = (NumericSymbolicConstant) u
				.symbolicConstant(u.stringObject("Y7"), intType);
		SymbolicConstant array = u.symbolicConstant(u.stringObject("X_a"),
				arrayType);
		SymbolicConstant isDuplet = u
				.symbolicConstant(u.stringObject("is_duplet"), funcType);
		// clauses:
		BooleanExpression clauses[] = new BooleanExpression[17];

		clauses[0] = u.lessThan(u.oneInt(), X_N);
		clauses[1] = u.or(u.equals(u.oneInt(), u.subtract(X_N, Y7)), Y5);
		clauses[2] = u.or(u.equals(Y6, u.add(Y0, u.oneInt())), u.not(Y4));
		clauses[3] = u.or(u.equals(Y7, u.add(Y2, u.oneInt())), u.not(Y5));
		clauses[4] = u.or(u.equals(Y0, u.zeroInt()), Y4);
		clauses[5] = u.or(u.equals(Y2, u.zeroInt()), Y5);
		clauses[6] = u.or(u.lessThanEquals(u.add(Y0, u.oneInt()), Y1),
				u.not(Y4));
		clauses[7] = u.or(u.lessThanEquals(u.add(Y2, u.oneInt()), Y3),
				u.not(Y5));
		clauses[8] = u.or(u.lessThanEquals(Y1, u.subtract(X_N, u.oneInt())),
				u.not(Y4));
		clauses[9] = u.or(u.lessThanEquals(Y3, u.subtract(X_N, u.oneInt())),
				u.not(Y5));
		clauses[10] = u.or(u.lessThanEquals(u.oneInt(), Y6), u.not(Y4));
		clauses[11] = u.or(u.lessThanEquals(u.oneInt(), Y7), u.not(Y5));
		clauses[12] = u.or(
				u.neq(u.zeroInt(),
						u.subtract((NumericExpression) u.arrayRead(array, Y0),
								(NumericExpression) u.arrayRead(array, Y2))),
				u.not(Y5));
		clauses[13] = u.or(
				(BooleanExpression) u.apply(isDuplet,
						Arrays.asList(array, u.zeroInt(), X_N, Y0, Y1)),
				u.not(Y4));
		clauses[14] = u.or(
				(BooleanExpression) u.apply(isDuplet,
						Arrays.asList(array, u.zeroInt(), X_N, Y2, Y3)),
				u.not(Y5));
		clauses[15] = u.or(u.equals(u.oneInt(), u.subtract(X_N, Y6)), Y4);
		if (unsat)
			clauses[16] = u.lessThan(X_N, u.zeroInt());
		else
			clauses[16] = u.trueExpression();
		// ret:
		return u.and(Arrays.asList(clauses));
	}

	/**
	 * The negation of <code>
	 * 0 <= X_N - 1*Y7 - 1 &&
	 * 0 <= X_N - 3 &&
	 * 0 <= Y6 &&
	 * 0 <= Y7 &&
	 * (is_duplet(X_a,0,X_N,Y0,Y1) || (!Y4)) &&
	 * (is_duplet(X_a,0,X_N,Y2,Y3) || (!Y5)) &&
	 * ((0 == X_N - 1*Y6 - 1) || Y4) &&
	 * ((0 == X_N - 1*Y7 - 1) || Y5) &&
	 * ((0 == Y0 - 1*Y6 + 1) || (!Y4)) &&
	 * ((0 == Y2 - 1*Y7 + 1) || (!Y5)) &&
	 * ((0 == Y0) || Y4) &&
	 * ((0 == Y2) || Y5) &&
	 * ((Y0 - 1*Y1 + 1 <= 0) || (!Y4)) &&
	 * ((Y2 - 1*Y3 + 1 <= 0) || (!Y5)) &&
	 * ((0 <= X_N - 1*Y1 - 1) || (!Y4)) &&
	 * ((0 <= X_N - 1*Y3 - 1) || (!Y5)) &&
	 * ((0 <= Y6 - 1) || (!Y4)) &&
	 * ((0 <= Y7 - 1) || (!Y5)) &&
	 * ((0 != X_a[Y0] - 1*X_a[Y2]) || (!Y5)) &&
	 * 0 <= X_N - 1*Y6 - 1 &&
	 * X_N <= 0
	 * </code>
	 */
	@Test
	public void slowNegation() {
		SymbolicUniverse u = SARL.newStandardUniverse();
		// test:
		BooleanExpression negation = u.not(slowNegationFormula(true, u));

		assertEquals(u.trueExpression(),
				u.reasoner(u.trueExpression()).simplify(negation));
	}
}