package inference;

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

import java.util.Set;

import org.junit.jupiter.api.Test;

import models.formulas.EquationFormula;
import models.terms.DependencyTerm;
import models.terms.Resource;

public class ProofSystemTest {

	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);
	
	@Test
	void AdmissibleTest() {
		DependencyTerm t1 = new DependencyTerm(a, b, c);
		EquationFormula eq1 = new EquationFormula(t1, a);
		assertThrows(IllegalArgumentException.class, () -> new ProofSystem(Set.of(eq1), eq1));
		EquationFormula eq2 = new EquationFormula(a, t1);
		assertThrows(IllegalArgumentException.class, () -> new ProofSystem(Set.of(eq2), eq1));
		
		DependencyTerm t2 = new DependencyTerm(a, a, b);
		EquationFormula eq3 = new EquationFormula(t2, b);
		assertDoesNotThrow(() -> {
				new ProofSystem(Set.of(eq3), eq3);
			}
		);
		
	}
	
}