Newer
Older
RDLProofSystem / src / main / java / inference / equivalence / MetaSemanticEquivalenceRelation.java
package inference.equivalence;

import lombok.Getter;

@Getter
public class MetaSemanticEquivalenceRelation {
	
//	private MetaRDLTerm leftSideHand;
//	private MetaRDLTerm rightSideHand;
//	private Expression order;
//	private Variable orderVariable;
//	private int orderConstant = 0;
//	
//	public MetaSemanticEquivalenceRelation(MetaRDLTerm lsh, MetaRDLTerm rsh, Expression order) {
//		leftSideHand = lsh;
//		rightSideHand = rsh;
//		this.order = order;
//		Map<Variable, Integer> coefficients = new HashMap<>(); 
//		orderConstant = ExpressionUitls.getCoefficientAndConstantsFromExpression(order, coefficients, 1);
//		if (coefficients.size() > 1) {
//			// todo: create exception
//			throw new TooManyVariablesException("Too many variables");
//		}
//		if (coefficients.size() == 1) {
//			orderVariable = coefficients.keySet().iterator().next();
//			if (coefficients.get(orderVariable) != 1) {
//				throw new CoefficientNotOneException();
//			}
//		} else {
//			orderVariable = null;
//		}
//	}
//	
//	public boolean isMatchedBy(SemanticEquivalenceRelation relation) {
//		Map<Variable, RDLTerm> binding = new HashMap<>();
//		Map<Variable, OrderVariableConstraint> orderConstraint = new HashMap<>();
//		return isMatchedBy(relation, binding, orderConstraint);
//	}
//	
//	public boolean isMatchedBy(SemanticEquivalenceRelation relation, Map<Variable, RDLTerm> binding, Map<Variable, OrderVariableConstraint> orderConstraint) {
//		return leftSideHand.isMatchedBy(relation.getLeftSideHand(), binding, orderConstraint)
//					&& rightSideHand.isMatchedBy(relation.getRightSideHand(), binding, orderConstraint);
//	}
//	
//	public Set<SemanticEquivalenceRelation> substitute(Map<Variable, RDLTerm> binding, Map<Variable, OrderVariableConstraint> orderConstraint, Collection<RDLTerm> existedTerms) {
//		Set<SemanticEquivalenceRelation> result = new HashSet<>();
//		Map<Variable, MetaVariable> allVariables = new HashMap<>();
//		for(MetaVariable variable : leftSideHand.getAllVariables()) {
//			allVariables.put(variable.getVariableName(), variable);
//		}
//		for(MetaVariable variable : rightSideHand.getAllVariables()) {
//			allVariables.put(variable.getVariableName(), variable);
//		}
//		for (Variable variable : binding.keySet()) {
//			allVariables.remove(variable);
//		}
//		List<Variable> leftVariables = new ArrayList<>(allVariables.keySet());
//		for(List<RDLTerm> useTerms: Permutation.permutation(existedTerms, leftVariables.size())) {
//			Map<Variable, RDLTerm> tempBinding = new HashMap<>();
//			tempBinding.putAll(binding);
//			boolean flg = false;
//			for (int i = 0; i < leftVariables.size(); i++) {
//				if (!allVariables.get(leftVariables.get(i)).isMatchedBy(useTerms.get(i))) {
//					flg = true;
//					break;
//				}
//				tempBinding.put(leftVariables.get(i), useTerms.get(i));
//			}
//			if (flg) {
//				continue;
//			}
//			EvaluatableTerm leftTerm = (EvaluatableTerm) leftSideHand.substitute(tempBinding);
//			EvaluatableTerm rightTerm = (EvaluatableTerm) rightSideHand.substitute(tempBinding);
//			Map<Variable, OrderVariableConstraint> tempOrderConstraint = new HashMap<>();
//			for(Variable key : orderConstraint.keySet()) {
//				tempOrderConstraint.put(key, (OrderVariableConstraint)orderConstraint.get(key).clone());
//			}
//			if (leftSideHand.isMatchedBy(leftTerm, binding, tempOrderConstraint) && rightSideHand.isMatchedBy(rightTerm, binding, tempOrderConstraint)) {
//				if (! tempOrderConstraint.containsKey(orderVariable)) {
//					continue;
//				}
//				int order = tempOrderConstraint.get(this.orderVariable).getOrder();
//				if (order == -1) {
//					continue;
//				}
//				order += orderConstant;
//				result.add(new SemanticEquivalenceRelation(leftTerm, rightTerm, order));
//			}
//			for(Variable variable: leftVariables) {
//				binding.remove(variable);
//			}
//		}
//		return result;
//	}
//	
//	public Set<SemanticEquivalenceRelation> substitute(RDLTerm term, Collection<RDLTerm> existedTerms) {
//		Set<SemanticEquivalenceRelation> result = new HashSet<>();
//		Set<SemanticEquivalenceRelation> leftSub = leftSubstitute(term, existedTerms);
//		if (leftSub != null) {
//			result.addAll(leftSub);
//		}
//		
//		Set<SemanticEquivalenceRelation> rightSub = rightSubstitute(term, existedTerms);
//		if (rightSub != null) {
//			result.addAll(rightSub);
//		}
//		return result;
//	}
//	
//	private Set<SemanticEquivalenceRelation> leftSubstitute(RDLTerm term, Collection<RDLTerm> existedTerms) {
//		Set<SemanticEquivalenceRelation> result = new HashSet<>();
//		Map<Variable, RDLTerm> binding = new HashMap<>();
//		Map<Variable, OrderVariableConstraint> orderConstraint = new HashMap<>();
//		if (! leftSideHand.isMatchedBy(term, binding, orderConstraint)) {
//			return null;
//		}
//		if (! orderConstraint.containsKey(orderVariable)) {
//			return null;
//		}
//		int order = orderConstraint.get(this.orderVariable).getOrder();
//		if (order == -1) {
//			return null;
//		}
//		order += orderConstant;
//		
//		Set<Variable> allVariables = new HashSet<>(rightSideHand.getVariables().values());
//		allVariables.removeAll(binding.keySet());
//		List<Variable> leftVariables = new ArrayList<>(allVariables);
//		for (List<RDLTerm> useVariables: Permutation.permutation(existedTerms, leftVariables.size())) {
//			Map<Variable, RDLTerm> tempBinding = new HashMap<>();
//			tempBinding.putAll(binding);
//			for (int i = 0; i < leftVariables.size(); i++) {
//				tempBinding.put(leftVariables.get(i), useVariables.get(i));
//			}
//			RDLTerm tempTerm = rightSideHand.substitute(tempBinding);
//			if (! rightSideHand.isMatchedBy(tempTerm, binding, orderConstraint)) {
//				continue;
//			}
//			result.add(new SemanticEquivalenceRelation((EvaluatableTerm)leftSideHand.substitute(binding), (EvaluatableTerm) rightSideHand.substitute(binding), order));
//			for (int i = 0; i < leftVariables.size(); i++) {
//				binding.remove(leftVariables.get(i));
//			}
//		}
//		try {
//			result.add(new SemanticEquivalenceRelation((EvaluatableTerm)leftSideHand.substitute(binding), (EvaluatableTerm)rightSideHand.substitute(binding), order));
//		} catch (SubstituteFailedException e){}
//		return result;
//	}
//	
//	private Set<SemanticEquivalenceRelation> rightSubstitute(RDLTerm term, Collection<RDLTerm> existedTerms) {
//		Set<SemanticEquivalenceRelation> result = new HashSet<>();
//		Map<Variable, RDLTerm> binding = new HashMap<>();
//		Map<Variable, OrderVariableConstraint> orderConstraint = new HashMap<>();
//		if (! rightSideHand.isMatchedBy(term, binding, orderConstraint)) {
//			return null;
//		};
//		if (! orderConstraint.containsKey(orderVariable)) {
//			return null;
//		}
//		int order = orderConstraint.get(this.orderVariable).getOrder();
//		if (order == -1) {
//			return null;
//		}
//		order += orderConstant;
//		
//		Set<Variable> allVariables = new HashSet<>();
//		for (MetaVariable vari : leftSideHand.getAllVariables()) {
//			allVariables.add(vari.getVariableName());
//		}
//		allVariables.removeAll(binding.keySet());
//		List<Variable> leftVariables = new ArrayList<>(allVariables);
//		for (List<RDLTerm> useVariables: Permutation.permutation(existedTerms, leftVariables.size())) {
//			Map<Variable, RDLTerm> tempBinding = new HashMap<>();
//			tempBinding.putAll(binding);
//			for (int i = 0; i < leftVariables.size(); i++) {
//				tempBinding.put(leftVariables.get(i), useVariables.get(i));
//			}
//			RDLTerm tempTerm = leftSideHand.substitute(tempBinding);
//			if (! leftSideHand.isMatchedBy(tempTerm, binding, orderConstraint)) {
//				for (int i = 0; i < leftVariables.size(); i++) {
//					binding.remove(leftVariables.get(i));
//				}
//				continue;
//			}
//			result.add(new SemanticEquivalenceRelation((EvaluatableTerm)leftSideHand.substitute(binding), (EvaluatableTerm)rightSideHand.substitute(binding), order));
//			for (int i = 0; i < leftVariables.size(); i++) {
//				binding.remove(leftVariables.get(i));
//			}
//		}
//		try {
//			result.add(new SemanticEquivalenceRelation((EvaluatableTerm)leftSideHand.substitute(binding), (EvaluatableTerm)rightSideHand.substitute(binding), order));
//		} catch (SubstituteFailedException e){}
//		return result;
//		
//	}
//	
//	
//	@Override
//	public String toString() {
//		return leftSideHand.toString() + " ===(" + order + ") " + rightSideHand.toString();
//	}
//	
//	@Override
//	public boolean equals(Object another) {
//		if (! (another instanceof SemanticEquivalenceRelation)) {
//			return false;
//		}
//		SemanticEquivalenceRelation relation = (SemanticEquivalenceRelation) another;
//		return leftSideHand.equals(relation.getLeftSideHand()) && rightSideHand.equals(relation.getRightSideHand());
//	}
//	
//	@Override
//	public int hashCode() {
//		return toString().hashCode();
//	}
	
}