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.meta.MetaDependencyFormula;
import models.formulas.meta.MetaEquationFormula;
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.MetaTermGenerator;
import models.terms.meta.OrderConstraint;
import utils.ExpressionUitls;
import utils.Product;

public class ProofSystem {

	//======================Equality Axioms=============================
	
	public static final InferenceRule reflexivity = new InferenceRule(
			"Reflexivity",
			List.of(),
			new MetaEquationFormula(
					new MetaEvaluatableTermVariable(new Variable("te")),
					new MetaEvaluatableTermVariable(new Variable("te"))
			)
	);
	
	public 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"))
			)
	);
	
	public 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"))
			)
	);
	
	public 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 MetaEvaluatableTermVariable(new Variable("re"))
					),
					new MetaEquationFormula(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("re")), 
									new MetaEvaluatableTermVariable(new Variable("x")), 
									new MetaEvaluatableTermVariable(new Variable("y"))
							),
							new MetaEvaluatableTermVariable(new Variable("te"))
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("re")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					),
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("re")),
							new MetaEvaluatableTermVariable(new Variable("ue"))
					)
			)
	);
	
	public 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 MetaEvaluatableTermVariable(new Variable("re"))
					),
					new MetaEquationFormula(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("re")), 
									new MetaEvaluatableTermVariable(new Variable("x")), 
									new MetaEvaluatableTermVariable(new Variable("y"))
							),
							new MetaEvaluatableTermVariable(new Variable("ue"))
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("re")),
							new MetaEvaluatableTermVariable(new Variable("ue"))
					),
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaEvaluatableTermVariable(new Variable("re")),
							new MetaEvaluatableTermVariable(new Variable("ue"))
					)
			)
	);
	
	public static final InferenceRule identity = new InferenceRule(
			"Identity",
			List.of(
					new MetaEquationFormula(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaEvaluatableTermVariable(new Variable("x")),
									new MetaEvaluatableTermVariable(new Variable("y"))
							),
							new MetaEvaluatableTermVariable(new Variable("te"))
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					),
					new MetaEvaluatableTermVariable(new Variable("te"))
			)
	);
	
	public static final InferenceRule mapComposition = new InferenceRule(
			"Map Composition",
			List.of(
					new MetaDependencyFormula(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("re"))
					),
					new MetaDependencyFormula(
							new MetaEvaluatableTermVariable(new Variable("re")),
							new MetaEvaluatableTermVariable(new Variable("pe"))
					),
					new MetaEquationFormula(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("pe")),
									new MetaEvaluatableTermVariable(new Variable("x")),
									new MetaEvaluatableTermVariable(new Variable("y"))
							),
							new MetaEvaluatableTermVariable(new Variable("te"))
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("re")),
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("re")),
									new MetaEvaluatableTermVariable(new Variable("pe")),
									new MetaEvaluatableTermVariable(new Variable("te"))
							)
					),
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("pe")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					)
			)
	);
	
	//todo
//	public static final InferenceRule constantness = new InferenceRule(
//			"Constantness",
//			List.of(),
//			(i) -> new MetaEquationFormula(
//					new MetaRDLTerm(
//							new MetaEvaluatableTermVariable(new Variable("r" + (i + 1)), new Variable("m+" + i)),
//							new MetaEvaluatableTermVariable(new Variable("x" + (i + 1))),
//							new MetaEvaluatableTermVariable(new Variable("y" + (i + 1)))
//					),
//					new MetaEvaluatableTermVariable(new Variable("t" + (i + 1)))
//			),
//			new MetaEquationFormula(
//					new MetaDynamicTerm(
//							new MetaTermGenerator() {
//								@Override
//								public MetaRDLTerm generate(int index, int depth, boolean isLast) {
//									if (isLast) {
//										return new MetaResource(new Variable("se"), new Variable("n"));
//									} 
//									return new MetaDynamicTerm(this, new MetaResource(new Variable("r" + (depth + 1)), new Variable("n+" + depth)), new MetaResource(new Variable("t" + (depth + 1))));
//								}
//								
//							},
//							new MetaResource(new Variable("r1")),
//							new MetaResource(new Variable("t1"))
//					),
//					new MetaResource(new Variable("se"), new Variable("n"))
//			),
//			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m"))
//	);
//	
	public static final InferenceRule rightNormalization = new InferenceRule(
			"Right Normalization",
			List.of(
					new MetaDependencyFormula(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n"))
							)
					),
					new MetaDependencyFormula(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("te")),
									new MetaEvaluatableTermVariable(new Variable("qe"), new Variable("n"))
							)
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")),
									new MetaEvaluatableTermVariable(new Variable("te"))
							),
							new MetaEvaluatableTermVariable(new Variable("qe"), new Variable("n")),
							new MetaEvaluatableTermVariable(new Variable("ue"))
					),
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")),
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("te")),
									new MetaEvaluatableTermVariable(new Variable("qe"), new Variable("n")),
									new MetaEvaluatableTermVariable(new Variable("ue"))
							)
					)
			),
			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
	);
	
	public static final InferenceRule pseudoConstantness = new InferenceRule(
			"Pseudo-Constantness",
			List.of(
					new MetaDependencyFormula(
							new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")),
							new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n"))
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")),
							new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")),
							new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n"))
					),
					new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))
			),
			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
	);
	
	public static final InferenceRule uncurrying = new InferenceRule(
		"Uncurrying",
		List.of(
				new MetaDependencyFormula(
						new MetaRDLTerm(
								new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")),
								new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n"))
						),
						new MetaEvaluatableTermVariable(new Variable("pe"), ExpressionUitls.parse("n-1"))
				),
				new MetaEquationFormula(
						new MetaRDLTerm(
								new MetaEvaluatableTermVariable(new Variable("pe"), ExpressionUitls.parse("n-1")),
								new MetaEvaluatableTermVariable(new Variable("x")),
								new MetaEvaluatableTermVariable(new Variable("y"))
						),
						new MetaEvaluatableTermVariable(new Variable("te"))
				),
				new MetaEquationFormula(
						new MetaRDLTerm(
								new MetaEvaluatableTermVariable(new Variable("qe"), ExpressionUitls.parse("n-1")),
								new MetaEvaluatableTermVariable(new Variable("x2")),
								new MetaEvaluatableTermVariable(new Variable("y2"))
						),
						new MetaEvaluatableTermVariable(new Variable("ue"))
				)
		),
		new MetaEquationFormula(
				new MetaRDLTerm(
						new MetaRDLTerm(
								new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")),
								new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")),
								new MetaEvaluatableTermVariable(new Variable("ue"))
						),
						new MetaEvaluatableTermVariable(new Variable("pe"), ExpressionUitls.parse("n-1")),
						new MetaEvaluatableTermVariable(new Variable("te"))
				),
				new MetaRDLTerm(
						new MetaRDLTerm(
								new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")),
								new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")),
								new MetaEvaluatableTermVariable(new Variable("qe"), ExpressionUitls.parse("n-1"))
						),
						new MetaEvaluatableTermVariable(new Variable("pe"), ExpressionUitls.parse("n-1")),
						new MetaEvaluatableTermVariable(new Variable("te")),
						new MetaEvaluatableTermVariable(new Variable("qe"), ExpressionUitls.parse("n-1")),
						new MetaEvaluatableTermVariable(new Variable("ue"))
				)
		)
	);
	
//	
//	//======================Dependency Axioms=============================
//	
	public 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"))
			)
	);
	
	public static final InferenceRule compositeMapping = new InferenceRule(
			"Composite Mapping",
			List.of(
					new MetaDependencyFormula(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaTermGenerator() {
								@Override
								public MetaRDLTerm generate(int i, int depth, boolean isLast) {
									if (i == 0) {
										return new MetaResource(new Variable("r"));
									} else {
										return new MetaResource(new Variable("r" + i));
									}
								}}
					),
					new MetaDependencyFormula(
							new MetaEvaluatableTermVariable(new Variable("r")),
							new MetaResource(new Variable("q"))
					)
			),
			new MetaDependencyFormula(
					new MetaEvaluatableTermVariable(new Variable("te")),
					new MetaTermGenerator() {
						@Override
						public MetaRDLTerm generate(int i, int depth, boolean isLast) {
							if (i == 0) {
								return new MetaResource(new Variable("q"));
							} else {
								return new MetaResource(new Variable("r" + i));
							}
						}}
			)
	);
	
	public 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"))
	);
	
	public 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"))
			)
	);
	
	public static final InferenceRule uncurriedMapping = new InferenceRule(
			"Uncurried Mapping",
			List.of(
					new MetaDependencyFormula(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaEvaluatableTermVariable(new Variable("re"))
							),
							new MetaEvaluatableTermVariable(new Variable("pe"), ExpressionUitls.parse("n-1"))
					)
			),
			new MetaDependencyFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("re")),
							new MetaEvaluatableTermVariable(new Variable("te"), ExpressionUitls.parse("n-1"))
					),
					new MetaEvaluatableTermVariable(new Variable("pe"), ExpressionUitls.parse("n-1")),
					new MetaEvaluatableTermVariable(new Variable("te"), ExpressionUitls.parse("n-1"))
			)
	);


	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).isEmpty()) {
					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());
		} 
	}
	
	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;
	}
}