package inference;

import java.util.List;
import java.util.Set;

import exceptions.SubstituteFailedException;
import models.formulas.Formula;
import models.formulas.meta.MetaEquationFormula;
import models.formulas.meta.MetaFormula;
import models.terms.RDLTerm;
import models.terms.meta.MatchConstraint;
import utils.Permutation;

public class EquationAxiom extends InferenceRule{
	
	public EquationAxiom(String name) {
		super(name);
	}
	
	public EquationAxiom(
			String name,
			List<MetaFormula> assumptions, 
			List<MetaFormula> repetitionAssumptions, 
			MetaFormula conclusion, 
			InferenceOrderConstraint constraint,
			ConclusionSizeCalculator conclusionMaxIndexCalculator,
			ConclusionSizeCalculator conclusionMaxDepthCalculator,
			AssumptionSizeCalculator assumptionSizeCalculator
	) {
		super(name, assumptions, repetitionAssumptions, conclusion, constraint, conclusionMaxIndexCalculator, conclusionMaxDepthCalculator, assumptionSizeCalculator);
	}
	
	public RDLTerm generateRightSideHand(List<Formula> assumptions, RDLTerm leftSideHand) {
		if (! (this.conclusion instanceof MetaEquationFormula)) return null;
		if (this.assumptions.size()  > assumptions.size()) return null;
		MetaEquationFormula metaFormula = (MetaEquationFormula) this.conclusion;
		Set<MatchConstraint> constraints = metaFormula.getLeftSideHand().isMatchedBy(leftSideHand);
		for (List<Formula> assumptionList: Permutation.permutation(assumptions, assumptions.size())) {
			for (int i = 0; i < getAssumptionSize(); i++) {
				constraints = this.assumptions.get(i).isMatchedBy(assumptionList.get(i), constraints);
			}
			for (MatchConstraint constraint: constraints) {
				try {
					return metaFormula.getRightSideHand().substitute(constraint.getBinding());
				} catch (SubstituteFailedException e) {
					continue;
				}
			}
		}
		return null;
	}
	
}