package inference;

import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;

import lombok.Getter;
import models.algebra.Variable;
import models.formulas.Formula;
import models.formulas.meta.MetaFormula;
import models.terms.RDLTerm;
import models.terms.meta.OrderVariableConstraint;

public class InferenceRule {

	@Getter
	private final String name;
	
	private final List<MetaFormula> assumptions;
	private final MetaFormula conclusion;
	private final InferenceOrderConstraint defaultOrderConstraint;
	
	public InferenceRule(String name, List<MetaFormula> assumptions, MetaFormula conclusion, InferenceOrderConstraint constraint) {
		this.name = name;
		this.assumptions = assumptions;
		this.conclusion = conclusion;
		this.defaultOrderConstraint = constraint;
	}
	
	public InferenceRule( List<MetaFormula> assumptions, MetaFormula conclusion, InferenceOrderConstraint constraint) {
		this.name = "undefined";
		this.assumptions = assumptions;
		this.conclusion = conclusion;
		this.defaultOrderConstraint = constraint;
	}
	
	public InferenceRule(String name, List<MetaFormula> assumptions, MetaFormula conclusion) {
		this.assumptions = assumptions;
		this.conclusion = conclusion;
		this.name = name;
		this.defaultOrderConstraint = null;
	}
	
	public InferenceRule(List<MetaFormula> assumptions, MetaFormula conclusion) {
		this.assumptions = assumptions;
		this.conclusion = conclusion;
		this.name = "undefined";
		this.defaultOrderConstraint = null;
	}
	
	public boolean check(Collection<Formula> assumptions, Formula conclusion) {
		
		if (this.assumptions.size() > assumptions.size()) {
			return false;
		}
		
		Map<Variable, RDLTerm> binding = new HashMap<>();
		Map<Variable, OrderVariableConstraint> orderConstraints = new HashMap<>();
		this.conclusion.isMatchedBy(conclusion, binding, orderConstraints);
		Set<Formula> givenAssumptions = new HashSet<>(assumptions);
		
		for (MetaFormula assumption : this.assumptions) {
			boolean flg = false;
			for (Formula given : givenAssumptions) {
				Map<Variable, RDLTerm> tmpBinding = new HashMap<>(binding);
				Map<Variable, OrderVariableConstraint> tmpOrderConstraints = new HashMap<>(orderConstraints);
				if (assumption.isMatchedBy(given, tmpBinding, tmpOrderConstraints)) {
					binding.putAll(tmpBinding);
					orderConstraints.putAll(tmpOrderConstraints);
					flg = true;
					givenAssumptions.remove(given);
					break;
				}
			}
			if (!flg) {
				return false;
			}
		}
		
		if (this.defaultOrderConstraint != null) {
			return defaultOrderConstraint.check(orderConstraints);
		}
		
		return true;
		
//		for(List<Formula> assumption : permutation(assumptions, this.assumptions.size())) {
//			if (check(assumption, conclusion)) {
//				return true;
//			}
//		}
//		return false;
	}
	
	private boolean check(List<Formula> assumptions, Formula conclusion) {
		Map<Variable, RDLTerm> binding = new HashMap<>();
		Map<Variable, OrderVariableConstraint> orderConstraints = new HashMap<>();
		for (int i = 0; i < assumptions.size(); i++) {
			if (! this.assumptions.get(i).isMatchedBy(assumptions.get(i), binding, orderConstraints)) {
				return false;
			}
		}
		if (! this.conclusion.isMatchedBy(conclusion, binding, orderConstraints)) {
			return false;
		}
		if (this.defaultOrderConstraint != null) {
			return defaultOrderConstraint.check(orderConstraints);
		}
		return true;
	}
	
	
	public String toString() {
		StringBuilder sb = new StringBuilder();
		for (int i = 0; i < assumptions.size(); i++) {
			sb.append(assumptions.get(i).toString());
			if (i != assumptions.size() - 1) {
				sb.append(", ");
			}
		}
		String assumpStr = sb.toString();
		String concluStr = conclusion.toString();
		String line = "-".repeat(Math.max(assumpStr.length(), concluStr.length()));
		sb = new StringBuilder();
		sb.append(assumpStr);
		sb.append("\n");
		sb.append(line);
		sb.append("\n");
		sb.append(concluStr);
		return sb.toString();
	}
	
}