diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index 8d1b7be..57bfc69 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -12,584 +12,575 @@ 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.InFormula; -import models.formulas.meta.MetaDependencyFormula; -import models.formulas.meta.MetaEquationFormula; -import models.formulas.meta.MetaInFormula; 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.OrderConstraint; import utils.Product; public class ProofSystem { //======================Equality Axioms============================= - private static final InferenceRule reflexivity = new InferenceRule( - "Reflexivity", - List.of(), - new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ); - - private 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")) - ) - ); - - private 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")) - ) - ); - - private 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 MetaResource(new Variable("r")) - ), - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaRDLTerm(new MetaResource(new Variable("r"))) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")), - new MetaEvaluatableTermVariable(new Variable("te")) - ), - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ) - ); - - private 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 MetaResource(new Variable("r")) - ), - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("ue")), - new MetaRDLTerm(new MetaResource(new Variable("r"))) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ), - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResource(new Variable("r")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ) - ); - - private static final InferenceRule identity = new InferenceRule( - "Identity", - List.of( - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaRDLTerm(new MetaResource(new Variable("r"))) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaResource(new Variable("r")), - new MetaResource(new Variable("r")), - new MetaEvaluatableTermVariable(new Variable("te")) - ), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ); - - private static final InferenceRule mapComposition = new InferenceRule( - "Map Composition", - List.of( - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")) - ), - new MetaDependencyFormula( - new MetaResource(new Variable("r")), - new MetaResource(new Variable("p")) - ), - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaRDLTerm(new MetaResource(new Variable("p"))) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")), - new MetaRDLTerm( - new MetaResource(new Variable("r")), - new MetaResource(new Variable("p")), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ), - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("p")), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ) - ); - - private static final InferenceRule constantness = new InferenceRule( - "Constantness", - List.of( - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("t1")), - new MetaRDLTerm(new MetaResource(new Variable("r1"), new Variable("m"))) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), - new MetaResource(new Variable("r1"), new Variable("m")), - new MetaEvaluatableTermVariable(new Variable("t1")) - ), - new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) - ), - new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) - ); - - private static final InferenceRule rightNormalization = new InferenceRule( - "Right Normalization", - List.of( - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResource(new Variable("r"), new Variable("n")) - ) - ), - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("q"), new Variable("n")) - ) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResource(new Variable("r"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("se")) - ), - new MetaResource(new Variable("q"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ), - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResource(new Variable("r"), new Variable("n")), - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("q"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ) - ), - new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) - ); - - private static final InferenceRule pseudoConstantness = new InferenceRule( - "Pseudo-Constantness", - List.of( - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), - new MetaResource(new Variable("r"), new Variable("n")) - ) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), - new MetaResource(new Variable("r"), new Variable("n")), - new MetaResource(new Variable("r"), new Variable("n")) - ), - new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")) - ), - new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) - ); - - //======================Dependency Axioms============================= - - private 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")) - ) - ); - - private static final InferenceRule compositeMapping = new InferenceRule( - "Composite Mapping", - List.of( - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResource(new Variable("r")) - ), - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("r")), - new MetaResource(new Variable("q")) - ) - ), - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResource(new Variable("q")) - ) - ); - - private 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")) - ); - - private 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")) - ) - ); - - //======================Set-Theoretic Axioms============================= - - private static final InferenceRule memberSubstitution = new InferenceRule( - "Member Substitution", - List.of( - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ), - new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ), - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ); - - private static final InferenceRule membershipChain = new InferenceRule( - "Membership Chain", - List.of( - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("te")) - ), - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ), - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ); - - private static final InferenceRule collectionSubstitution = new InferenceRule( - "Collection Substitution", - List.of( - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("te")) - ), - new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ), - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ); - - private static final InferenceRule setEquivelence = new InferenceRule( - "Set Equivelence", - List.of( - new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))), - new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))) - ), - new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) - ); - - private static final InferenceRule setHomomorphism = new InferenceRule( - "Set Homomorphism", - List.of( - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")), - new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"))) - ), - new MetaRDLTerm( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ) - ) - ); - - private static final InferenceRule leftProjection = new InferenceRule( - "Left Projection", - List.of( - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), - new MetaResource(new Variable("r"), new Variable("m")) - ), - new MetaResource(new Variable("q"), new Variable("l")) - ) - ), - new MetaDependencyFormula( - new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))), - new MetaResource(new Variable("q"), new Variable("l")) - ) - ); - - private static final InferenceRule rightProjection = new InferenceRule( - "Right Projection", - List.of( - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), - new MetaResource(new Variable("r"), new Variable("m")) - ), - new MetaResource(new Variable("q"), new Variable("l")) - ) - ), - new MetaDependencyFormula( - new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("r"), new Variable("m"))), - new MetaResource(new Variable("q"), new Variable("l")) - ) - ); - - private static final InferenceRule domainMembership = new InferenceRule( - "Domain Membership", - List.of( - new MetaEquationFormula( - new MetaRDLTerm( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r1")), - new MetaEvaluatableTermVariable(new Variable("t1")) - ), - new MetaResource(new Variable("r2")), - new MetaEvaluatableTermVariable(new Variable("t2")) - ), - new MetaResource(new Variable("c")) - ) - ), - new MetaInFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("t1")), - new MetaResource(new Variable("r2")), - new MetaEvaluatableTermVariable(new Variable("t2")) - ), - new MetaRDLTerm( - new MetaRDLTerm(new MetaResource(new Variable("r1"))), - new MetaResource(new Variable("r2")), - new MetaEvaluatableTermVariable(new Variable("t2")) - ) - ) - ); - - private static final InferenceRule codomainMembership = new InferenceRule( - "Codomain Membership", - List.of( - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r1")), - new MetaEvaluatableTermVariable(new Variable("t1")) - ), - new MetaResource(new Variable("r2")) - ), - new MetaInFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("t1")), - new MetaResource(new Variable("r2")), - new MetaEvaluatableTermVariable(new Variable("t2")) - ), - new MetaRDLTerm( - new MetaRDLTerm( - new MetaResource(new Variable("r1")) - ), - new MetaResource(new Variable("r2")), - new MetaEvaluatableTermVariable(new Variable("t2")) - ) - ) - ), - new MetaInFormula( - new MetaRDLTerm( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r1")), - new MetaEvaluatableTermVariable(new Variable("t1")) - ), - new MetaResource(new Variable("r2")), - new MetaEvaluatableTermVariable(new Variable("t2")) - ), - new MetaRDLTerm( - new MetaRDLTerm( - new MetaResource(new Variable("se")) - ), - new MetaResource(new Variable("r2")), - new MetaEvaluatableTermVariable(new Variable("t2")) - ) - ) - ); - - private static final InferenceRule codomainMembership2 = new InferenceRule( - "Codomain Membership2", - List.of( - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r1")) - ), - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("t1")), - new MetaRDLTerm( - new MetaResource(new Variable("r1")) - ) - ) - ), - new MetaInFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r1")), - new MetaEvaluatableTermVariable(new Variable("t1")) - ), - new MetaRDLTerm( - new MetaResource(new Variable("se")) - ) - ) - ); +// private static final InferenceRule reflexivity = new InferenceRule( +// "Reflexivity", +// List.of(), +// new MetaEquationFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ) +// ); +// +// private 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")) +// ) +// ); +// +// private 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")) +// ) +// ); +// +// private 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 MetaResource(new Variable("r")) +// ), +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaRDLTerm(new MetaResource(new Variable("r"))) +// ) +// ), +// new MetaEquationFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ), +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ) +// ) +// ); +// +// private 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 MetaResource(new Variable("r")) +// ), +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("ue")), +// new MetaRDLTerm(new MetaResource(new Variable("r"))) +// ) +// ), +// new MetaEquationFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ), +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaResource(new Variable("r")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ) +// ) +// ); +// +// private static final InferenceRule identity = new InferenceRule( +// "Identity", +// List.of( +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaRDLTerm(new MetaResource(new Variable("r"))) +// ) +// ), +// new MetaEquationFormula( +// new MetaRDLTerm( +// new MetaResource(new Variable("r")), +// new MetaResource(new Variable("r")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ) +// ); +// +// private static final InferenceRule mapComposition = new InferenceRule( +// "Map Composition", +// List.of( +// new MetaDependencyFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r")) +// ), +// new MetaDependencyFormula( +// new MetaResource(new Variable("r")), +// new MetaResource(new Variable("p")) +// ), +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaRDLTerm(new MetaResource(new Variable("p"))) +// ) +// ), +// new MetaEquationFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r")), +// new MetaRDLTerm( +// new MetaResource(new Variable("r")), +// new MetaResource(new Variable("p")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ) +// ), +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("p")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ) +// ) +// ); +// +// private static final InferenceRule constantness = new InferenceRule( +// "Constantness", +// List.of( +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("t1")), +// new MetaRDLTerm(new MetaResource(new Variable("r1"), new Variable("m"))) +// ) +// ), +// new MetaEquationFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), +// new MetaResource(new Variable("r1"), new Variable("m")), +// new MetaEvaluatableTermVariable(new Variable("t1")) +// ), +// new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) +// ), +// new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) +// ); +// +// private static final InferenceRule rightNormalization = new InferenceRule( +// "Right Normalization", +// List.of( +// new MetaDependencyFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaResource(new Variable("r"), new Variable("n")) +// ) +// ), +// new MetaDependencyFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("q"), new Variable("n")) +// ) +// ) +// ), +// new MetaEquationFormula( +// new MetaRDLTerm( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaResource(new Variable("r"), new Variable("n")), +// new MetaEvaluatableTermVariable(new Variable("se")) +// ), +// new MetaResource(new Variable("q"), new Variable("n")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ), +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaResource(new Variable("r"), new Variable("n")), +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("q"), new Variable("n")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ) +// ) +// ), +// new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) +// ); +// +// private static final InferenceRule pseudoConstantness = new InferenceRule( +// "Pseudo-Constantness", +// List.of( +// new MetaDependencyFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), +// new MetaResource(new Variable("r"), new Variable("n")) +// ) +// ) +// ), +// new MetaEquationFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), +// new MetaResource(new Variable("r"), new Variable("n")), +// new MetaResource(new Variable("r"), new Variable("n")) +// ), +// new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")) +// ), +// new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) +// ); +// +// //======================Dependency Axioms============================= +// +// private 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")) +// ) +// ); +// +// private static final InferenceRule compositeMapping = new InferenceRule( +// "Composite Mapping", +// List.of( +// new MetaDependencyFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaResource(new Variable("r")) +// ), +// new MetaDependencyFormula( +// new MetaEvaluatableTermVariable(new Variable("r")), +// new MetaResource(new Variable("q")) +// ) +// ), +// new MetaDependencyFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaResource(new Variable("q")) +// ) +// ); +// +// private 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")) +// ); +// +// private 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")) +// ) +// ); +// +// //======================Set-Theoretic Axioms============================= +// +// private static final InferenceRule memberSubstitution = new InferenceRule( +// "Member Substitution", +// List.of( +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ), +// new MetaEquationFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ) +// ), +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ) +// ); +// +// private static final InferenceRule membershipChain = new InferenceRule( +// "Membership Chain", +// List.of( +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ), +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ) +// ), +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ) +// ); +// +// private static final InferenceRule collectionSubstitution = new InferenceRule( +// "Collection Substitution", +// List.of( +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ), +// new MetaEquationFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ) +// ), +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ) +// ); +// +// private static final InferenceRule setEquivelence = new InferenceRule( +// "Set Equivelence", +// List.of( +// new MetaEquationFormula( +// new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), +// new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")) +// ) +// ), +// new MetaEquationFormula( +// new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))), +// new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))) +// ), +// new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) +// ); +// +// private static final InferenceRule setHomomorphism = new InferenceRule( +// "Set Homomorphism", +// List.of( +// new MetaDependencyFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r")) +// ) +// ), +// new MetaEquationFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r")), +// new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"))) +// ), +// new MetaRDLTerm( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ) +// ) +// ) +// ); +// +// private static final InferenceRule leftProjection = new InferenceRule( +// "Left Projection", +// List.of( +// new MetaDependencyFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), +// new MetaResource(new Variable("r"), new Variable("m")) +// ), +// new MetaResource(new Variable("q"), new Variable("l")) +// ) +// ), +// new MetaDependencyFormula( +// new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))), +// new MetaResource(new Variable("q"), new Variable("l")) +// ) +// ); +// +// private static final InferenceRule rightProjection = new InferenceRule( +// "Right Projection", +// List.of( +// new MetaDependencyFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), +// new MetaResource(new Variable("r"), new Variable("m")) +// ), +// new MetaResource(new Variable("q"), new Variable("l")) +// ) +// ), +// new MetaDependencyFormula( +// new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("r"), new Variable("m"))), +// new MetaResource(new Variable("q"), new Variable("l")) +// ) +// ); +// +// private static final InferenceRule domainMembership = new InferenceRule( +// "Domain Membership", +// List.of( +// new MetaEquationFormula( +// new MetaRDLTerm( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r1")), +// new MetaEvaluatableTermVariable(new Variable("t1")) +// ), +// new MetaResource(new Variable("r2")), +// new MetaEvaluatableTermVariable(new Variable("t2")) +// ), +// new MetaResource(new Variable("c")) +// ) +// ), +// new MetaInFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("t1")), +// new MetaResource(new Variable("r2")), +// new MetaEvaluatableTermVariable(new Variable("t2")) +// ), +// new MetaRDLTerm( +// new MetaRDLTerm(new MetaResource(new Variable("r1"))), +// new MetaResource(new Variable("r2")), +// new MetaEvaluatableTermVariable(new Variable("t2")) +// ) +// ) +// ); +// +// private static final InferenceRule codomainMembership = new InferenceRule( +// "Codomain Membership", +// List.of( +// new MetaDependencyFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r1")), +// new MetaEvaluatableTermVariable(new Variable("t1")) +// ), +// new MetaResource(new Variable("r2")) +// ), +// new MetaInFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("t1")), +// new MetaResource(new Variable("r2")), +// new MetaEvaluatableTermVariable(new Variable("t2")) +// ), +// new MetaRDLTerm( +// new MetaRDLTerm( +// new MetaResource(new Variable("r1")) +// ), +// new MetaResource(new Variable("r2")), +// new MetaEvaluatableTermVariable(new Variable("t2")) +// ) +// ) +// ), +// new MetaInFormula( +// new MetaRDLTerm( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r1")), +// new MetaEvaluatableTermVariable(new Variable("t1")) +// ), +// new MetaResource(new Variable("r2")), +// new MetaEvaluatableTermVariable(new Variable("t2")) +// ), +// new MetaRDLTerm( +// new MetaRDLTerm( +// new MetaResource(new Variable("se")) +// ), +// new MetaResource(new Variable("r2")), +// new MetaEvaluatableTermVariable(new Variable("t2")) +// ) +// ) +// ); +// +// private static final InferenceRule codomainMembership2 = new InferenceRule( +// "Codomain Membership2", +// List.of( +// new MetaDependencyFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r1")) +// ), +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("t1")), +// new MetaRDLTerm( +// new MetaResource(new Variable("r1")) +// ) +// ) +// ), +// new MetaInFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r1")), +// new MetaEvaluatableTermVariable(new Variable("t1")) +// ), +// new MetaRDLTerm( +// new MetaResource(new Variable("se")) +// ) +// ) +// ); private static final List 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 +// 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() { diff --git a/src/main/java/models/terms/DependencyTerm.java b/src/main/java/models/terms/DependencyTerm.java index 20c6882..201d109 100644 --- a/src/main/java/models/terms/DependencyTerm.java +++ b/src/main/java/models/terms/DependencyTerm.java @@ -47,8 +47,6 @@ termPairs.put(dependedTerm, argTerm); this.size += dependedTerm.getSize(); this.size += argTerm.getSize(); - addChild(dependedTerm); - addChild(argTerm); if (argOrderType) { if (argTerm.getOrder() != getOrder()) { throw new SyntaxException("order not same"); @@ -65,6 +63,10 @@ } } } + for (EvaluatableTerm dependedTerm : termPairs.keySet()) { + addChild(dependedTerm); + addChild(termPairs.get(dependedTerm)); + } } public DependencyTerm(EvaluatableTerm dependingTerm, EvaluatableTerm ...terms) { @@ -85,14 +87,20 @@ @Override public void selfLinearRightNormalize() { - } private boolean isLinearRightNormaled(int depth) { - return false; } + public List getDependedTerms() { + return new ArrayList<>(termPairs.keySet()); + } + + public List getArgumentTerms() { + return new ArrayList<>(termPairs.values()); + } + @Override public String toString() { diff --git a/src/main/java/models/terms/meta/MetaRDLTerm.java b/src/main/java/models/terms/meta/MetaRDLTerm.java index 3353cb2..39e8b1e 100644 --- a/src/main/java/models/terms/meta/MetaRDLTerm.java +++ b/src/main/java/models/terms/meta/MetaRDLTerm.java @@ -9,11 +9,14 @@ import java.util.Set; import java.util.TreeMap; import java.util.TreeSet; +import java.util.stream.Collectors; +import java.util.stream.IntStream; import exceptions.IllegalTypeException; import exceptions.SubstituteFailedException; import exceptions.SyntaxException; import lombok.Getter; +import models.algebra.Expression; import models.algebra.Symbol; import models.algebra.Variable; import models.terms.Dependency; @@ -22,6 +25,7 @@ import models.terms.LinearRightNormalizedType; import models.terms.RDLTerm; import models.terms.Resource; +import utils.Permutation; @Getter public class MetaRDLTerm extends RDLTerm { @@ -38,11 +42,11 @@ } //dependency - public MetaRDLTerm(MetaRDLTerm dependingTerm, TreeSet dependedTerms) { + public MetaRDLTerm(MetaRDLTerm dependingTerm, Set dependedTerms) { super(new Symbol(":", 1 + dependedTerms.size()), -1, -1); int size = dependingTerm.getSize(); addChild(dependingTerm); - for (MetaRDLTerm dependedTerm: dependedTerms) { + for (MetaRDLTerm dependedTerm: new TreeSet<>(dependedTerms)) { addChild(dependedTerm); size += dependedTerm.getSize(); } @@ -79,12 +83,12 @@ } sortedTerms.put(dependedTerm, argTerm); } + this.size = size; for (MetaRDLTerm dependedTerm: sortedTerms.keySet()) { MetaRDLTerm argTerm = sortedTerms.get(dependedTerm); addChild(dependedTerm); addChild(argTerm); } - this.size = size; this.termType = TermType.META_DEPENDENCY_TERM; } @@ -107,19 +111,6 @@ } } else if (isDependencyTerm()) { -// RDLTerm dependingTerm = (RDLTerm) getChild(0); -// RDLTerm dependedVariable = (RDLTerm) getChild(1); -// RDLTerm argumentTerm = (RDLTerm) getChild(2); -// if (dependingTerm instanceof MetaRDLTerm) { -// dependingTerm = ((MetaRDLTerm) dependingTerm).substitute(binding); -// } -// if (dependedVariable instanceof MetaRDLTerm) { -// dependedVariable = ((MetaRDLTerm) dependedVariable).substitute(binding); -// } -// if (argumentTerm instanceof MetaRDLTerm) { -// argumentTerm = ((MetaRDLTerm) argumentTerm).substitute(binding); -// } -// return new DependencyTerm((EvaluatableTerm) dependingTerm, (Resource) dependedVariable, (EvaluatableTerm) argumentTerm); RDLTerm dependingTerm = (RDLTerm) getChild(0); if (dependingTerm instanceof MetaRDLTerm metaDependingTerm) { dependingTerm = metaDependingTerm.substitute(binding); @@ -155,21 +146,127 @@ if (isDependencyTerm() && (! islinearRightNormalizedMatchedBy(another))) { return false; } - for (int i = 0; i < this.getChildren().size(); i++) { - RDLTerm child = (RDLTerm) this.getChild(i); - RDLTerm anotherChild = (RDLTerm) another.getChild(i); - if (child instanceof MetaRDLTerm) { - MetaRDLTerm metaChild = (MetaRDLTerm) child; - if (! metaChild.isMatchedBy(anotherChild, binding, orderConstraint)) { + if (isDependencyTerm() && !isVariable()) { + RDLTerm dependingChild = (RDLTerm) this.getChild(0); + RDLTerm anotherDependingChild = (RDLTerm) another.getChild(0); + if (dependingChild instanceof MetaRDLTerm) { + MetaRDLTerm metaChild = (MetaRDLTerm) dependingChild; + if (! metaChild.isMatchedBy(anotherDependingChild, binding, orderConstraint)) { return false; } } else { - if (!(child.equals(anotherChild))) { + if (!(dependingChild.equals(anotherDependingChild))) { return false; } } + for (List perm : Permutation.permutation((getChildren().size() - 1) / 2)) { + Map binding2 = new HashMap<>(binding); + Map orderConstraint2 = new HashMap<>(orderConstraint); + boolean flg = true; + for (int i = 0; i < (getChildren().size() - 1) / 2; i++) { + int j = perm.get(i); + RDLTerm dependedChild = (RDLTerm) this.getChild(j * 2 + 1); + RDLTerm anotherDependedChild = (RDLTerm) another.getChild(i * 2 + 1); + RDLTerm argChild = (RDLTerm) this.getChild(j * 2 + 2); + RDLTerm anotherArgChild = (RDLTerm) another.getChild(i * 2 + 2); + if (dependedChild instanceof MetaRDLTerm) { + MetaRDLTerm metaChild = (MetaRDLTerm) dependedChild; + if (! metaChild.isMatchedBy(anotherDependedChild, binding2, orderConstraint2)) { + flg = false; + break; + } + } else { + if (!(dependedChild.equals(anotherDependedChild))) { + flg = false; + break; + } + } + if (argChild instanceof MetaRDLTerm) { + MetaRDLTerm metaChild = (MetaRDLTerm) argChild; + if (! metaChild.isMatchedBy(anotherArgChild, binding2, orderConstraint2)) { + flg = false; + break; + } + } else { + if (!(argChild.equals(anotherArgChild))) { + flg = false; + break; + } + } + } + if (flg) { + for (var key: binding2.keySet()) { + binding.put(key, binding2.get(key)); + } + for (var key : orderConstraint2.keySet()) { + orderConstraint.put(key, orderConstraint2.get(key)); + } + return true; + } + } + return false; + } else if (isDependency() && !isVariable()) { + RDLTerm dependingChild = (RDLTerm) this.getChild(0); + RDLTerm anotherDependingChild = (RDLTerm) another.getChild(0); + if (dependingChild instanceof MetaRDLTerm) { + MetaRDLTerm metaChild = (MetaRDLTerm) dependingChild; + if (! metaChild.isMatchedBy(anotherDependingChild, binding, orderConstraint)) { + return false; + } + } else { + if (!(dependingChild.equals(anotherDependingChild))) { + return false; + } + } + for (List perm : Permutation.permutation(getChildren().size() - 1)) { + Map binding2 = new HashMap<>(binding); + Map orderConstraint2 = new HashMap<>(orderConstraint); + boolean flg = true; + for (int i = 0; i < getChildren().size() - 1; i++) { + int j = perm.get(i); + RDLTerm dependedChild = (RDLTerm) this.getChild(j + 1); + RDLTerm anotherDependedChild = (RDLTerm) another.getChild(i + 1); + if (dependedChild instanceof MetaRDLTerm) { + MetaRDLTerm metaChild = (MetaRDLTerm) dependedChild; + if (! metaChild.isMatchedBy(anotherDependedChild, binding2, orderConstraint2)) { + flg = false; + break; + } + } else { + if (!(dependedChild.equals(anotherDependedChild))) { + flg = false; + break; + } + } + } + if (flg) { + for (var key: binding2.keySet()) { + binding.put(key, binding2.get(key)); + } + for (var key : orderConstraint2.keySet()) { + orderConstraint.put(key, orderConstraint2.get(key)); + } + return true; + } + } + return false; + } else { + for (int i = 0; i < this.getChildren().size(); i++) { + RDLTerm child = (RDLTerm) this.getChild(i); + RDLTerm anotherChild = (RDLTerm) another.getChild(i); + if (child instanceof MetaRDLTerm) { + MetaRDLTerm metaChild = (MetaRDLTerm) child; + if (! metaChild.isMatchedBy(anotherChild, binding, orderConstraint)) { + return false; + } + } else { + if (!(child.equals(anotherChild))) { + return false; + } + } + } + return true; } - return true; } public boolean checkTermType(Class clazz) { @@ -223,11 +320,10 @@ public String toString() { switch(termType) { case META_DEPENDENCY: - return "[" + getChild(0).toString() + " : " + getChild(1).toString() + "]"; - case META_DEPENDENCY_LIST: - return "[" + getChild(0).toString() + "]"; + return "[" + getChild(0).toString() + " : " + getChildren().stream().skip(1).map(Expression::toString).collect(Collectors.joining(",")) + "]"; case META_DEPENDENCY_TERM: - return "[" + getChild(0).toString() + " : " + getChild(1).toString() + " -> " + getChild(2).toString() + "]"; + return "[" + getChild(0).toString() + " : " + IntStream.range(0, (getChildren().size() - 1) / 2) + .mapToObj(i -> getChild(i * 2 + 1).toString() + " -> " + getChild(i * 2 + 2)).collect(Collectors.joining(",")) + "]"; default: return ""; } diff --git a/src/main/java/utils/Permutation.java b/src/main/java/utils/Permutation.java index 039b9f9..f52227f 100644 --- a/src/main/java/utils/Permutation.java +++ b/src/main/java/utils/Permutation.java @@ -14,6 +14,18 @@ return res; } + public static List> permutation(int i) { + return permutation(0, i); + } + + public static List> permutation(int i, int j) { + List perms = new ArrayList<>(); + for (int ii = i; ii < j; ii++) { + perms.add(ii); + } + return permutation(perms, j - i); + } + private static void permutation(Collection all, int n, List current, Set used, List> result) { if (current.size() == n) { result.add(new ArrayList<>(current)); diff --git a/src/test/java/terms/DependencyTermTest.java b/src/test/java/terms/DependencyTermTest.java new file mode 100644 index 0000000..bd673a0 --- /dev/null +++ b/src/test/java/terms/DependencyTermTest.java @@ -0,0 +1,86 @@ +package terms; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.jupiter.api.Test; + +import java.util.HashMap; +import java.util.Map; + +import models.algebra.Variable; +import models.terms.DependencyTerm; +import models.terms.RDLTerm; +import models.terms.Resource; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaResource; +import models.terms.meta.OrderVariableConstraint; +import utils.Utils; + +public class DependencyTermTest { + + Resource a = new Resource("a", Utils.INT, 1); + Resource b = new Resource("b", Utils.INT, 1); + Resource c = new Resource("c", Utils.INT, 1); + Resource d = new Resource("d", Utils.INT, 1); + Resource e = new Resource("e", Utils.INT, 1); + Resource f = new Resource("f", Utils.INT, 1); + Resource g = new Resource("g", Utils.INT, 1); + + @Test + void EqualsTest() { + DependencyTerm t1 = new DependencyTerm(a, b, c); + DependencyTerm t2 = new DependencyTerm(a, b, c); + assertEquals(t1, t2); + + DependencyTerm t3 = new DependencyTerm(a, b, c, b, c); + assertEquals(t1, t3); + + DependencyTerm t4 = new DependencyTerm(a, c, b); + assertFalse(t1.equals(t4)); + + DependencyTerm t5 = new DependencyTerm(a, b, c, d, e); + DependencyTerm t6 = new DependencyTerm(a, d, e, b, c); + DependencyTerm t7 = new DependencyTerm(a, b, e, d, c); + assertEquals(t5, t6); + assertFalse(t5.equals(t7)); + + DependencyTerm t8 = new DependencyTerm(t1, t5, t6); + DependencyTerm t9 = new DependencyTerm(t1, t6, t5); + assertEquals(t8, t9); + + } + + @Test + void MatchTest() { + DependencyTerm t1 = new DependencyTerm(a, b, c, d, e); + DependencyTerm t2 = new DependencyTerm(a, g, f, b, c); + MetaResource x = new MetaResource(new Variable("x")); + MetaResource y = new MetaResource(new Variable("y")); + MetaResource z = new MetaResource(new Variable("z")); + MetaResource w = new MetaResource(new Variable("w")); + MetaResource p = new MetaResource(new Variable("p")); + MetaResource o = new MetaResource(new Variable("o")); + MetaResource n = new MetaResource(new Variable("n")); + MetaRDLTerm mt1 = new MetaRDLTerm(x, y, z, w, p); + MetaRDLTerm mt2 = new MetaRDLTerm(x, w, p, y, z); + MetaRDLTerm mt3 = new MetaRDLTerm(x, p, w, y, z); + MetaRDLTerm mt4 = new MetaRDLTerm(x, n, o, w, p); + Map binding = new HashMap<>(); + Map orderConstraint = new HashMap<>(); + Map correctBinding = new HashMap<>(); + correctBinding.put(x.getVariableName(), a); + correctBinding.put(y.getVariableName(), d); + correctBinding.put(z.getVariableName(), e); + correctBinding.put(w.getVariableName(), b); + correctBinding.put(p.getVariableName(), c); + mt4.toString(); + assertTrue(mt1.isMatchedBy(t1, binding, orderConstraint)); + assertTrue(mt2.isMatchedBy(t1, binding, orderConstraint)); + assertFalse(mt3.isMatchedBy(t1, binding, orderConstraint)); + assertEquals(correctBinding, binding); + assertTrue(mt4.isMatchedBy(t2, binding, orderConstraint)); + RDLTerm t = mt1.substitute(binding); + assertEquals(t, t1); + System.out.println(binding); + } +} diff --git a/src/test/java/terms/DependencyTest.java b/src/test/java/terms/DependencyTest.java index c940eab..bc2c60e 100644 --- a/src/test/java/terms/DependencyTest.java +++ b/src/test/java/terms/DependencyTest.java @@ -3,9 +3,18 @@ import org.junit.jupiter.api.Test; +import java.util.HashMap; +import java.util.Map; +import java.util.Set; + import exceptions.SyntaxException; +import models.algebra.Variable; import models.terms.Dependency; +import models.terms.RDLTerm; import models.terms.Resource; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaResource; +import models.terms.meta.OrderVariableConstraint; import utils.Utils; public class DependencyTest { @@ -14,6 +23,8 @@ Resource b = new Resource("b", Utils.INT, 1); Resource c = new Resource("c", Utils.INT, 1); Resource d = new Resource("d", Utils.INT, 2); + Resource e = new Resource("e", Utils.INT, 1); + Resource f = new Resource("f", Utils.INT, 1); @Test void EqualsTest() { @@ -68,4 +79,38 @@ assertEquals(d3.toString(), "a : b, c"); } + @Test + void MatchTest() { + MetaResource p = new MetaResource(new Variable("p")); + MetaResource q = new MetaResource(new Variable("q")); + MetaResource r = new MetaResource(new Variable("r")); + MetaResource s = new MetaResource(new Variable("s")); + MetaResource t = new MetaResource(new Variable("t")); + + MetaRDLTerm mt1 = new MetaRDLTerm(p, q); + MetaRDLTerm mt2 = new MetaRDLTerm(p, Set.of(q, r, s)); + MetaRDLTerm mt3 = new MetaRDLTerm(p, Set.of(r, q, s)); + MetaRDLTerm mt4 = new MetaRDLTerm(p, Set.of(s, r, q)); + MetaRDLTerm mt5 = new MetaRDLTerm(p, Set.of(s, t, q)); + + Dependency d1 = new Dependency(a, b); + Dependency d2 = new Dependency(a, b, c, f); + Dependency d3 = new Dependency(a, f, c, b); + Dependency d4 = new Dependency(a, b, f, c); + Dependency d5 = new Dependency(a, b, e, f); + + + Map binding = new HashMap<>(); + Map orderConst = new HashMap<>(); + assertTrue(mt1.isMatchedBy(d1, binding, orderConst)); + assertEquals(binding.get(p.getVariableName()), a); + assertEquals(binding.get(q.getVariableName()), b); + binding.clear(); + assertTrue(mt2.isMatchedBy(d2, binding, orderConst)); + assertTrue(mt3.isMatchedBy(d2, binding, orderConst)); + assertTrue(mt4.isMatchedBy(d2, binding, orderConst)); + assertFalse(mt4.isMatchedBy(d5, binding, orderConst)); + + } + } diff --git a/src/test/java/terms/meta/DependencyTermTest.java b/src/test/java/terms/meta/DependencyTermTest.java deleted file mode 100644 index a97bd9f..0000000 --- a/src/test/java/terms/meta/DependencyTermTest.java +++ /dev/null @@ -1,70 +0,0 @@ -package terms.meta; - -import static org.junit.jupiter.api.Assertions.*; - -import org.junit.jupiter.api.Test; - -import java.util.HashMap; -import java.util.Map; - -import models.algebra.Variable; -import models.terms.DependencyTerm; -import models.terms.RDLTerm; -import models.terms.Resource; -import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaResource; -import models.terms.meta.OrderVariableConstraint; -import utils.Utils; - -public class DependencyTermTest { - - Resource a = new Resource("a", Utils.INT, 1); - Resource b = new Resource("b", Utils.INT, 1); - Resource c = new Resource("c", Utils.INT, 1); - Resource d = new Resource("d", Utils.INT, 1); - Resource e = new Resource("e", Utils.INT, 1); - - @Test - void EqualsTest() { - DependencyTerm t1 = new DependencyTerm(a, b, c); - DependencyTerm t2 = new DependencyTerm(a, b, c); - assertEquals(t1, t2); - - DependencyTerm t3 = new DependencyTerm(a, b, c, b, c); - assertEquals(t1, t3); - - DependencyTerm t4 = new DependencyTerm(a, c, b); - assertFalse(t1.equals(t4)); - - DependencyTerm t5 = new DependencyTerm(a, b, c, d, e); - DependencyTerm t6 = new DependencyTerm(a, d, e, b, c); - DependencyTerm t7 = new DependencyTerm(a, b, e, d, c); - assertEquals(t5, t6); - assertFalse(t5.equals(t7)); - - DependencyTerm t8 = new DependencyTerm(t1, t5, t6); - DependencyTerm t9 = new DependencyTerm(t1, t6, t5); - assertEquals(t8, t9); - - } - - @Test - void MatchTest() { - DependencyTerm t1 = new DependencyTerm(a, b, c, d, e); - MetaResource x = new MetaResource(new Variable("x")); - MetaResource y = new MetaResource(new Variable("y")); - MetaResource z = new MetaResource(new Variable("z")); - MetaResource w = new MetaResource(new Variable("w")); - MetaResource p = new MetaResource(new Variable("p")); - MetaRDLTerm mt1 = new MetaRDLTerm(x, y, z, w, p); - MetaRDLTerm mt2 = new MetaRDLTerm(x, w, p, y, z); - MetaRDLTerm mt3 = new MetaRDLTerm(x, p, w, y, z); - Map binding = new HashMap<>(); - Map orderConstraint = new HashMap<>(); - assertTrue(mt1.isMatchedBy(t1, binding, orderConstraint)); - assertTrue(mt2.isMatchedBy(t1, binding, orderConstraint)); - assertFalse(mt3.isMatchedBy(t1, binding, orderConstraint)); - RDLTerm t = mt1.substitute(binding); - assertEquals(t, t1); - } -}