package inference;

import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Collection;
import java.util.Deque;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Queue;
import java.util.Set;
import java.util.stream.Collectors;

import models.algebra.Constant;
import models.algebra.Variable;
import models.formulas.DependencyFormula;
import models.formulas.EquationFormula;
import models.formulas.Formula;
import models.formulas.InFormula;
import models.formulas.meta.MetaDependencyFormula;
import models.formulas.meta.MetaEquationFormula;
import models.formulas.meta.MetaInFormula;
import models.terms.EvaluatableTerm;
import models.terms.RDLTerm;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaResource;
import models.terms.meta.OrderConstraint;
import utils.Product;

public class ProofSystem {

	//======================Equality Axioms=============================
	
	private static final InferenceRule reflexivity = new InferenceRule(
			"Reflexivity",
			List.of(),
			new MetaEquationFormula(
					new MetaEvaluatableTermVariable(new Variable("te")),
					new MetaEvaluatableTermVariable(new Variable("te"))
			)
	);
	
	private static final InferenceRule symmetry = new InferenceRule(
			"Symmetry",
			List.of(
					new MetaEquationFormula(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaEvaluatableTermVariable(new Variable("se"))
					)
			),
			new MetaEquationFormula(
					new MetaEvaluatableTermVariable(new Variable("se")),
					new MetaEvaluatableTermVariable(new Variable("te"))
			)
	);
	
	private static final InferenceRule transitivity = new InferenceRule(
			"Transitivity",
			List.of(
					new MetaEquationFormula(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					),
					new MetaEquationFormula(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaEvaluatableTermVariable(new Variable("ue"))
					)
			),
			new MetaEquationFormula(
					new MetaEvaluatableTermVariable(new Variable("se")),
					new MetaEvaluatableTermVariable(new Variable("ue"))
			)
	);
	
	private static final InferenceRule rightSubstitution = new InferenceRule(
			"Right Substitution",
			List.of(
					new MetaEquationFormula(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaEvaluatableTermVariable(new Variable("ue"))
					),
					new MetaDependencyFormula(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResource(new Variable("r"))
					),
					new MetaInFormula(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaRDLTerm(new MetaResource(new Variable("r")))
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResource(new Variable("r")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					),
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResource(new Variable("r")),
							new MetaEvaluatableTermVariable(new Variable("ue"))
					)
			)
	);
	
	private static final InferenceRule leftSubstitution = new InferenceRule(
			"Left Substitution",
			List.of(
					new MetaEquationFormula(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					),
					new MetaDependencyFormula(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResource(new Variable("r"))
					),
					new MetaInFormula(
							new MetaEvaluatableTermVariable(new Variable("ue")),
							new MetaRDLTerm(new MetaResource(new Variable("r")))
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResource(new Variable("r")),
							new MetaEvaluatableTermVariable(new Variable("ue"))
					),
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaResource(new Variable("r")),
							new MetaEvaluatableTermVariable(new Variable("ue"))
					)
			)
	);
	
	private static final InferenceRule identity = new InferenceRule(
			"Identity",
			List.of(
					new MetaInFormula(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaRDLTerm(new MetaResource(new Variable("r")))
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaResource(new Variable("r")),
							new MetaResource(new Variable("r")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					),
					new MetaEvaluatableTermVariable(new Variable("te"))
			)
	);
	
	private static final InferenceRule mapComposition = new InferenceRule(
			"Map Composition",
			List.of(
					new MetaDependencyFormula(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResource(new Variable("r"))
					),
					new MetaDependencyFormula(
							new MetaResource(new Variable("r")),
							new MetaResource(new Variable("p"))
					),
					new MetaInFormula(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaRDLTerm(new MetaResource(new Variable("p")))
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResource(new Variable("r")),
							new MetaRDLTerm(
									new MetaResource(new Variable("r")),
									new MetaResource(new Variable("p")),
									new MetaEvaluatableTermVariable(new Variable("te"))
							)
					),
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResource(new Variable("p")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					)
			)
	);
	
	private static final InferenceRule constantness = new InferenceRule(
			"Constantness",
			List.of(
					new MetaInFormula(
							new MetaEvaluatableTermVariable(new Variable("t1")), 
							new MetaRDLTerm(new MetaResource(new Variable("r1"), new Variable("m")))
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")),
							new MetaResource(new Variable("r1"), new Variable("m")),
							new MetaEvaluatableTermVariable(new Variable("t1"))
					),
					new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))
			),
			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m"))
	);
	
	private static final InferenceRule rightNormalization = new InferenceRule(
			"Right Normalization",
			List.of(
					new MetaDependencyFormula(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("te")),
									new MetaResource(new Variable("r"), new Variable("n"))
							)
					),
					new MetaDependencyFormula(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaResource(new Variable("q"), new Variable("n"))
							)
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("te")),
									new MetaResource(new Variable("r"), new Variable("n")),
									new MetaEvaluatableTermVariable(new Variable("se"))
							),
							new MetaResource(new Variable("q"), new Variable("n")),
							new MetaEvaluatableTermVariable(new Variable("ue"))
					),
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaResource(new Variable("r"), new Variable("n")),
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaResource(new Variable("q"), new Variable("n")),
									new MetaEvaluatableTermVariable(new Variable("ue"))
							)
					)
			),
			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
	);
	
	private static final InferenceRule pseudoConstantness = new InferenceRule(
			"Pseudo-Constantness",
			List.of(
					new MetaDependencyFormula(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
									new MetaResource(new Variable("r"), new Variable("n"))
							)
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
							new MetaResource(new Variable("r"), new Variable("n")),
							new MetaResource(new Variable("r"), new Variable("n"))
					),
					new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))
			),
			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
	);
	
	//======================Dependency Axioms=============================
	
	private static final InferenceRule identityMapping = new InferenceRule(
			"Identity Mapping",
			List.of(
					new MetaEquationFormula(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaResource(new Variable("r"))
					)
			),
			new MetaDependencyFormula(
					new MetaEvaluatableTermVariable(new Variable("te")),
					new MetaResource(new Variable("r"))
			)
	);
	
	private static final InferenceRule compositeMapping = new InferenceRule(
			"Composite Mapping",
			List.of(
					new MetaDependencyFormula(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaResource(new Variable("r"))
					),
					new MetaDependencyFormula(
							new MetaEvaluatableTermVariable(new Variable("r")),
							new MetaResource(new Variable("q"))
					)
			),
			new MetaDependencyFormula(
					new MetaEvaluatableTermVariable(new Variable("te")),
					new MetaResource(new Variable("q"))
			)
	);
	
	private static final InferenceRule constantMapping = new InferenceRule(
			"Constant Mapping",
			List.of(),
			new MetaDependencyFormula(
					new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
					new MetaResource(new Variable("r"), new Variable("m"))
			),
			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m"))
	);
	
	private static final InferenceRule slicedMapping = new InferenceRule(
			"Sliced Mapping",
			List.of(
					new MetaDependencyFormula(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaResource(new Variable("r"))
							),
							new MetaResource(new Variable("p"))
					),
					new MetaDependencyFormula(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaResource(new Variable("p"))
					)
			),
			new MetaDependencyFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResource(new Variable("r")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					),
					new MetaResource(new Variable("p"))
			)
	);
	
	//======================Set-Theoretic Axioms=============================
	
	private static final InferenceRule memberSubstitution = new InferenceRule(
			"Member Substitution",
			List.of(
					new MetaInFormula(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("ue"))
					),
					new MetaEquationFormula(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					)
			),
			new MetaInFormula(
					new MetaEvaluatableTermVariable(new Variable("te")),
					new MetaEvaluatableTermVariable(new Variable("ue"))
			)
	);
	
	private static final InferenceRule membershipChain = new InferenceRule(
			"Membership Chain",
			List.of(
					new MetaInFormula(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					),
					new MetaInFormula(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaEvaluatableTermVariable(new Variable("ue"))
					)
			),
			new MetaInFormula(
					new MetaEvaluatableTermVariable(new Variable("se")),
					new MetaEvaluatableTermVariable(new Variable("ue"))
			)
	);
	
	private static final InferenceRule collectionSubstitution = new InferenceRule(
			"Collection Substitution",
			List.of(
					new MetaInFormula(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					),
					new MetaEquationFormula(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaEvaluatableTermVariable(new Variable("ue"))
					)
			),
			new MetaInFormula(
					new MetaEvaluatableTermVariable(new Variable("se")),
					new MetaEvaluatableTermVariable(new Variable("ue"))
			)
	);
	
	private static final InferenceRule setEquivelence = new InferenceRule(
			"Set Equivelence",
			List.of(
					new MetaEquationFormula(
							new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")),
							new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))),
					new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")))
			),
			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
	);

	private static final InferenceRule setHomomorphism = new InferenceRule(
			"Set Homomorphism",
			List.of(
					new MetaDependencyFormula(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResource(new Variable("r"))
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResource(new Variable("r")),
							new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te")))
					),
					new MetaRDLTerm(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaResource(new Variable("r")),
									new MetaEvaluatableTermVariable(new Variable("te"))
							)
					)
			)
	);
	
	private static final InferenceRule leftProjection = new InferenceRule(
			"Left Projection",
			List.of(
					new MetaDependencyFormula(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
									new MetaResource(new Variable("r"), new Variable("m"))
							),
							new MetaResource(new Variable("q"), new Variable("l"))
					)
			),
			new MetaDependencyFormula(
					new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))),
					new MetaResource(new Variable("q"), new Variable("l"))
			)
	);
	
	private static final InferenceRule rightProjection = new InferenceRule(
			"Right Projection",
			List.of(
					new MetaDependencyFormula(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
									new MetaResource(new Variable("r"), new Variable("m"))
							),
							new MetaResource(new Variable("q"), new Variable("l"))
					)
			),
			new MetaDependencyFormula(
					new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("r"), new Variable("m"))),
					new MetaResource(new Variable("q"), new Variable("l"))
			)
	);
	
	private static final InferenceRule domainMembership = new InferenceRule(
			"Domain Membership",
			List.of(
					new MetaEquationFormula(
							new MetaRDLTerm(
								new MetaRDLTerm(
										new MetaEvaluatableTermVariable(new Variable("se")),
										new MetaResource(new Variable("r1")),
										new MetaEvaluatableTermVariable(new Variable("t1"))
								),
								new MetaResource(new Variable("r2")),
								new MetaEvaluatableTermVariable(new Variable("t2"))
							),
							new MetaResource(new Variable("c"))
					)
			),
			new MetaInFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("t1")),
							new MetaResource(new Variable("r2")),
							new MetaEvaluatableTermVariable(new Variable("t2"))
					),
					new MetaRDLTerm(
							new MetaRDLTerm(new MetaResource(new Variable("r1"))),
							new MetaResource(new Variable("r2")),
							new MetaEvaluatableTermVariable(new Variable("t2"))
					)
			)
	);

	private static final InferenceRule codomainMembership = new InferenceRule(
			"Codomain Membership",
			List.of(
					new MetaDependencyFormula(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaResource(new Variable("r1")),
									new MetaEvaluatableTermVariable(new Variable("t1"))
							),
							new MetaResource(new Variable("r2"))
					),
					new MetaInFormula(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("t1")),
									new MetaResource(new Variable("r2")),
									new MetaEvaluatableTermVariable(new Variable("t2"))
							),
							new MetaRDLTerm(
									new MetaRDLTerm(
											new MetaResource(new Variable("r1"))
									),
									new MetaResource(new Variable("r2")),
									new MetaEvaluatableTermVariable(new Variable("t2"))
							)
					)
			),
			new MetaInFormula(
					new MetaRDLTerm(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaResource(new Variable("r1")),
									new MetaEvaluatableTermVariable(new Variable("t1"))
							),
							new MetaResource(new Variable("r2")),
							new MetaEvaluatableTermVariable(new Variable("t2"))
					),
					new MetaRDLTerm(
							new MetaRDLTerm(
									new MetaResource(new Variable("se"))
							),
							new MetaResource(new Variable("r2")),
							new MetaEvaluatableTermVariable(new Variable("t2"))
					)
			)
	);
	
	private static final InferenceRule codomainMembership2 = new InferenceRule(
			"Codomain Membership2",
			List.of(
					new MetaDependencyFormula(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResource(new Variable("r1"))
					),
					new MetaInFormula(
							new MetaEvaluatableTermVariable(new Variable("t1")),
							new MetaRDLTerm(
									new MetaResource(new Variable("r1"))
							)
					)
			),
			new MetaInFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResource(new Variable("r1")),
							new MetaEvaluatableTermVariable(new Variable("t1"))
					),
					new MetaRDLTerm(
							new MetaResource(new Variable("se"))
					)
			)
	);

	private static final List<InferenceRule> axioms = List.of(
//			reflexivity, 
			symmetry, 
			transitivity,
			rightSubstitution, 
			leftSubstitution, 
			identity, 
			mapComposition, 
			constantness,
			rightNormalization,
			pseudoConstantness,
			identityMapping,
			compositeMapping,
			constantMapping,
			slicedMapping,
			memberSubstitution, 
			membershipChain, 
			collectionSubstitution,
			setEquivelence,
			setHomomorphism,
			leftProjection,
			rightProjection,
			domainMembership,
			codomainMembership,
			codomainMembership2
	);
	
	public static void debug() {
		for (var axiom : axioms) {
			System.out.println(axiom);
			System.out.println("==================================================================================================");
		}
	}
	
	record AxiomResult(InferenceRule axiom, List<Formula> formulas) {}
	
	public static boolean check(Collection<Formula> assumptions, Formula conclusion) {
		
		Map<Formula, AxiomResult> proofGraph = new HashMap<>();
		Map<InferenceRule, Set<List<Formula>>> appliedFormulas = new HashMap<>(); 
		
		for (InferenceRule axiom : axioms) {
			appliedFormulas.put(axiom, new HashSet<>());
		}
		
		Set<Formula> appearFormulas = new HashSet<>(assumptions);
		Set<RDLTerm> existTerms = new HashSet<>();
		for (Formula assumption : assumptions) {
			addExistTerms(assumption, existTerms);
		}
		int prevAppearFormulasSize = appearFormulas.size();
		while (! appearFormulas.contains(conclusion)) {
			Set<Formula> derivedFormulas = new HashSet<>();
			for(InferenceRule axiom : axioms) {
				derivedFormulas.addAll(applyAxiom(axiom, appearFormulas, appliedFormulas.get(axiom), existTerms, proofGraph));
			}
			if (derivedFormulas.size() == 0) {
				return false;
			}
			appearFormulas.addAll(derivedFormulas);
			if (appearFormulas.size() == prevAppearFormulasSize) {
				return false;
			}
			prevAppearFormulasSize = appearFormulas.size();
		}
		
		Queue<Formula> formulaQueue = new ArrayDeque<>();
		Queue<Integer> depthQueue = new ArrayDeque<>();
		List<Formula> formulaResult = new ArrayList<>();
		List<Integer> depthResult = new ArrayList<>();
		Set<Formula> used = new HashSet<>();
		Map<Integer, Set<InferenceRule>> usedAxioms = new HashMap<>();
		
		formulaQueue.add(conclusion);
		depthQueue.add(0);
		
		System.out.println("proof finish");
		System.out.println();
		
		while (formulaQueue.size() != 0) {
			Formula currentFormula = formulaQueue.poll();
//			if (used.contains(currentFormula)) {
//				continue;
//			}
			used.add(currentFormula);
			int currentDepth = depthQueue.poll();
			formulaResult.add(currentFormula);
			depthResult.add(currentDepth);
			if (! proofGraph.containsKey(currentFormula)) continue;
			for (Formula nextFormula : proofGraph.get(currentFormula).formulas) {
//				if (used.contains(nextFormula)) {
//					continue;
//				}
				formulaQueue.add(nextFormula);
				depthQueue.add(currentDepth + 1);
				if (! usedAxioms.containsKey(currentDepth + 1)) {
					usedAxioms.put(currentDepth + 1, new HashSet<>());
				}
				usedAxioms.get(currentDepth + 1).add(proofGraph.get(currentFormula).axiom);
			}
		}
		int prevDepth = depthResult.get(depthResult.size() - 1);
		Set<Formula> sameDepthFormulas = new HashSet<>();
		for (int i = formulaResult.size() - 1; i >= 0; i--) {
			int currentDepth = depthResult.get(i);
			Formula currentFormula = formulaResult.get(i);
			if (currentDepth != prevDepth) {
				String out = sameDepthFormulas.stream().map(String::valueOf).collect(Collectors.joining(", "));
				String axioms = usedAxioms.get(prevDepth).stream().map(InferenceRule::getName).collect(Collectors.joining(", "));
				System.out.println(out);
				System.out.println("==============================================================(" + axioms + ")");
				sameDepthFormulas.clear();
			}
			prevDepth = currentDepth;
			sameDepthFormulas.add(currentFormula);
			
		}
		String out = sameDepthFormulas.stream().map(String::valueOf).collect(Collectors.joining(","));
		System.out.println(out);
		return true;
	}
	
	private static Set<Formula> applyAxiom(InferenceRule axiom, Set<Formula> formulas, Set<List<Formula>> appliedFormulas,  Set<RDLTerm> existTerms, Map<Formula, AxiomResult> proofGraph) {
		Set<Formula> result = new HashSet<>();
		List<List<Formula>> matchedFormulas = new ArrayList<>();
		for (int i = 0; i < axiom.getAssumptionSize(); i++) {
			matchedFormulas.add(new ArrayList<>());
			for (Formula formula : formulas) {
				if (axiom.getAssumptions().get(i).isMatchedBy(formula)) {
					matchedFormulas.get(i).add(formula);
				}
			}
		}
		for(List<Formula> applyFormulas : Product.product(matchedFormulas)) {
			if (appliedFormulas.contains(applyFormulas)) continue;
			Set<Formula> applied = axiom.apply(applyFormulas, existTerms);
			if (applied != null) {
				for (Formula formula : applied) {
					if (! formulas.contains(formula)) {
						addExistTerms(formula, existTerms);
						proofGraph.put(formula, new AxiomResult(axiom, applyFormulas));
					}
				}
				result.addAll(applied);
				appliedFormulas.add(applyFormulas);
			}
		}
		return result;
	}
	
	private static void addExistTerms(Formula formula, Set<RDLTerm> existTerms) {
		if (formula instanceof EquationFormula) {
			RDLTerm leftSideHand = ((EquationFormula) formula).getLeftSideHand();
			RDLTerm rightSideHand = ((EquationFormula) formula).getRightSideHand();
			existTerms.addAll(leftSideHand.getSubTerms(RDLTerm.class).values());
			existTerms.addAll(rightSideHand.getSubTerms(RDLTerm.class).values());
		} else if (formula instanceof DependencyFormula) {
			RDLTerm dependency = ((DependencyFormula) formula).getDependency();
			existTerms.addAll(dependency.getSubTerms(RDLTerm.class).values());
		} else if (formula instanceof InFormula){
			RDLTerm leftSideHand = ((InFormula) formula).getLeftSideHand();
			RDLTerm rightSideHand = ((InFormula) formula).getRightSideHand();
			existTerms.addAll(leftSideHand.getSubTerms(RDLTerm.class).values());
			existTerms.addAll(rightSideHand.getSubTerms(RDLTerm.class).values());
		}
	}
	
	private static boolean equationTransitionCheck(Collection<Formula> assumptions, Formula conclusion) {
		if (! (conclusion instanceof EquationFormula)) {
			return false;
		}
		EquationFormula equationConclusion = (EquationFormula) conclusion;
		Map<EvaluatableTerm, List<EvaluatableTerm>> graph = constructEquationGraph(assumptions);
		Deque<EvaluatableTerm> que = new ArrayDeque<>();
		Set<EvaluatableTerm> visited = new HashSet<>();
		que.add(equationConclusion.getLeftSideHand());
		while (! que.isEmpty()) {
			EvaluatableTerm curNode = que.pollFirst();
			if (curNode.equals(equationConclusion.getRightSideHand())) {
				return true;
			}
			for (EvaluatableTerm nextNode : graph.getOrDefault(curNode, new ArrayList<>())) {
				if (visited.contains(nextNode)) {
					continue;
				}
				visited.add(nextNode);
				que.add(nextNode);
			}
		}
		return false;
	}
	
	private static Map<EvaluatableTerm, List<EvaluatableTerm>> constructEquationGraph(Collection<Formula> assumptions) {
		List<EquationFormula> equations = new ArrayList<>();
		for (Formula assumption : assumptions) {
			if (assumption instanceof EquationFormula) {
				equations.add((EquationFormula) assumption);
			}
		}
		
		Map<EvaluatableTerm, List<EvaluatableTerm>> graph = new HashMap<>();
		for (EquationFormula equation : equations) {
			EvaluatableTerm lsh = equation.getLeftSideHand();
			EvaluatableTerm rsh = equation.getRightSideHand();
			if (! graph.containsKey(lsh)) {
				graph.put(lsh, new ArrayList<>());
			}
			if (! graph.containsKey(rsh)) {
				graph.put(rsh, new ArrayList<>());
			}
			graph.get(lsh).add(rsh);
			graph.get(rsh).add(lsh);
		}
		return graph;
	}
}