Newer
Older
RDLProofSystem / src / main / java / models / formulas / meta / MetaFormula.java
@Sakoda2269 Sakoda2269 6 days ago 1 KB test完了
package models.formulas.meta;

import java.util.HashSet;
import java.util.Map;
import java.util.Set;

import models.algebra.Variable;
import models.formulas.Formula;
import models.terms.RDLTerm;
import models.terms.meta.MatchConstraint;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaVariable;

public abstract class MetaFormula extends Formula {

	public Set<MatchConstraint> isMatchedBy(Formula formula) {
		return isMatchedBy(formula, MatchConstraint.createDefault());
	}
	
	public abstract Set<MatchConstraint> isMatchedBy(Formula formula, MatchConstraint constraint);
	
	
	public Set<MatchConstraint> isMatchedBy(Formula formula, Set<MatchConstraint> constraints) {
		Set<MatchConstraint> result = new HashSet<>();
		for (MatchConstraint constraint: constraints) {
			result.addAll(isMatchedBy(formula, constraint));
		}
		return result;
	}
	
	public abstract Formula substitution(Map<Variable, RDLTerm> binding, Map<Object, Object> context);
	
    public abstract <T extends RDLTerm> Set<T> getSubTerms(Class<T> clazz);
    
    public abstract MetaFormula replace(Map<? extends MetaRDLTerm, ? extends RDLTerm> mapping);
    public abstract Set<MetaVariable> getAllVariables();
	
}