package inferencerule;

import static org.junit.jupiter.api.Assertions.*;

import java.util.Set;

import org.junit.jupiter.api.Test;

import inference.In;
import models.algebra.Constant;
import models.algebra.Variable;
import models.formulas.meta.MetaEquationFormula;
import models.terms.DependencyTerm;
import models.terms.Resource;
import models.terms.meta.MetaDependencyTerm;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaResource;

public class InTest {

	Resource a = new Resource("a", 1);
	Resource b = new Resource("b", 1);
	Resource c = new Resource("c", 1);
	Resource d = new Resource("d", 1);
	Resource e = new Resource("e", 1);
	Resource f = new Resource("f", 1);
	Resource g = new Resource("g", 1);
	Resource h = new Resource("h", 1);
	Resource i = new Resource("i", 1);
	Resource j = new Resource("j", 1);
	
	
	@Test
	void DomainMemberShipDeriveTest() {
		DependencyTerm t1 = new DependencyTerm(a, b, c);
		DependencyTerm t2 = new DependencyTerm(d, b, c);
		In in1 = new In(t1, t2);
		Set<MetaEquationFormula> res1 =  in1.deriveRule();
		assertFalse(res1.isEmpty());
		MetaEvaluatableTermVariable se = new MetaEvaluatableTermVariable(new Variable("se"));
		MetaResource C = new MetaResource(new Variable("c"), new Constant("0"));
		MetaDependencyTerm mt1 = new MetaDependencyTerm(se, d, a);
		MetaDependencyTerm mt2 = new MetaDependencyTerm(mt1, b, c);
		MetaEquationFormula eq1 = new MetaEquationFormula(mt2, C);
		//domain membership
		assertTrue(res1.contains(eq1));
		
		
		In in2 = new In(a, b);
		Set<MetaEquationFormula> res2 = in2.deriveRule();
		assertFalse(res2.isEmpty());
		MetaDependencyTerm mt3 = new MetaDependencyTerm(se, b, a);
		assertTrue(res2.contains(new MetaEquationFormula(mt3, C)));
		
		DependencyTerm t3 = new DependencyTerm(a, b, c);
		DependencyTerm t4 = new DependencyTerm(d, e, f);
		DependencyTerm t5 = new DependencyTerm(t3, g, h);
		DependencyTerm t6 = new DependencyTerm(t4, g, h);
		In in3 = new In(t5, t6);
		Set<MetaEquationFormula> res3 = in3.deriveRule();
		assertFalse(res3.isEmpty());
		MetaDependencyTerm mt4 = new MetaDependencyTerm(new MetaDependencyTerm(se, t4, t3), g, h);
		assertTrue(res3.contains(new MetaEquationFormula(mt4, C)));
		
		DependencyTerm t7 = new DependencyTerm(a, b, c, d, e);
		DependencyTerm t8 = new DependencyTerm(f, b, c, d, e);
		In in4 = new In(t7, t8);
		Set<MetaEquationFormula> res4 = in4.deriveRule();
		assertFalse(res4.isEmpty());
		MetaDependencyTerm mt5 = new MetaDependencyTerm(new MetaDependencyTerm(se, f, a), b, c, d, e);
		assertTrue(res4.contains(new MetaEquationFormula(mt5, C)));
		
		DependencyTerm t9 = new DependencyTerm(new DependencyTerm(a, b, c, d, e), f, g, h, i);
		DependencyTerm t10 = new DependencyTerm(new DependencyTerm(j, b, c, d, e), f, g, h, i);
		In in5 = new In(t9, t10);
		Set<MetaEquationFormula> res5 = in5.deriveRule();
		assertFalse(res5.isEmpty());
		MetaDependencyTerm mt6 = new MetaDependencyTerm(new MetaDependencyTerm(new MetaDependencyTerm(se, j, a), b, c, d, e), f, g, h, i);
		assertTrue(res5.contains(new MetaEquationFormula(mt6, C)));
	}
	
}