diff --git a/coverage/pom.xml b/coverage/pom.xml index cd9c75339..db9c33e4f 100644 --- a/coverage/pom.xml +++ b/coverage/pom.xml @@ -14,46 +14,51 @@ coverage - - ${project.groupId} - rulewerk-core - ${project.version} - - - ${project.groupId} - rulewerk-vlog - ${project.version} - - - ${project.groupId} - rulewerk-rdf - ${project.version} - - - ${project.groupId} - rulewerk-owlapi - ${project.version} - - - ${project.groupId} - rulewerk-graal - ${project.version} - - - ${project.groupId} - rulewerk-parser - ${project.version} - - - ${project.groupId} - rulewerk-commands - ${project.version} - - - ${project.groupId} - rulewerk-client - ${project.version} - + + ${project.groupId} + rulewerk-core + ${project.version} + + + ${project.groupId} + rulewerk-vlog + ${project.version} + + + ${project.groupId} + rulewerk-rdf + ${project.version} + + + ${project.groupId} + rulewerk-owlapi + ${project.version} + + + ${project.groupId} + rulewerk-graal + ${project.version} + + + ${project.groupId} + rulewerk-parser + ${project.version} + + + ${project.groupId} + rulewerk-commands + ${project.version} + + + ${project.groupId} + rulewerk-client + ${project.version} + + + ${project.groupId} + rulewerk-reliances + ${project.version} + diff --git a/pom.xml b/pom.xml index 10123a1c3..6b866ed2b 100644 --- a/pom.xml +++ b/pom.xml @@ -1,5 +1,7 @@ - + 4.0.0 @@ -13,7 +15,7 @@ https://github.com/knowsys/rulewerk - rulewerk-core rulewerk-vlog @@ -24,8 +26,9 @@ rulewerk-commands rulewerk-examples rulewerk-client + rulewerk-reliances coverage - + @@ -131,7 +134,7 @@ org.codehaus.mojo license-maven-plugin 1.14 - + first @@ -155,7 +158,7 @@ - org.eclipse.m2e lifecycle-mapping @@ -174,7 +177,7 @@ - + @@ -189,7 +192,7 @@ - + @@ -231,7 +234,7 @@ license-maven-plugin - org.apache.maven.plugins maven-compiler-plugin @@ -294,8 +297,8 @@ test - ${project.reporting.outputDirectory}/jacoco-ut @@ -303,7 +306,7 @@ - **/javacc/JavaCCParser.class **/javacc/JavaCCParserConstants.class @@ -317,7 +320,7 @@ - org.apache.maven.plugins maven-javadoc-plugin diff --git a/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/api/Literal.java b/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/api/Literal.java index b345b070d..69ca7a8c8 100644 --- a/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/api/Literal.java +++ b/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/api/Literal.java @@ -33,6 +33,11 @@ */ public interface Literal extends SyntaxObject { + /** + * + * @return true if the literal is a NegativeLiteral, or false if it is a + * PositiveLiteral + */ boolean isNegated(); /** diff --git a/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/api/Piece.java b/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/api/Piece.java new file mode 100644 index 000000000..d40e579d7 --- /dev/null +++ b/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/api/Piece.java @@ -0,0 +1,50 @@ +package org.semanticweb.rulewerk.core.model.api; + +/*- + * #%L + * Rulewerk Core Components + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +/** + * Interface for classes representing a rule. This implementation assumes that + * rules are defined by their head and body literals, without explicitly + * specifying quantifiers. All variables in the body are considered universally + * quantified; all variables in the head that do not occur in the body are + * considered existentially quantified. + * + * @author Larry Gonzalez + * + */ +public interface Piece extends SyntaxObject { + + /** + * Returns the conjunction of head literals (the consequence of the rule). + * + * @return conjunction of literals + */ + Conjunction getLiterals(); + + /** + * An unconnected piece is a piece s.t. no universally quantified variable + * occurs into it. + * + * @return True if the piece is unconnected + */ + boolean isUnconnected(); + +} diff --git a/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/api/PositiveLiteral.java b/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/api/PositiveLiteral.java index 6c4598a77..f9b573fa2 100644 --- a/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/api/PositiveLiteral.java +++ b/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/api/PositiveLiteral.java @@ -26,4 +26,12 @@ public interface PositiveLiteral extends Literal { default boolean isNegated() { return false; } + + /** + * + * @return true if the literal contain at least one existential quantified + * variable. + */ + boolean containsExistentialVariables(); + } diff --git a/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/api/Rule.java b/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/api/Rule.java index 9187282eb..6c2e50ba3 100644 --- a/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/api/Rule.java +++ b/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/api/Rule.java @@ -1,5 +1,7 @@ package org.semanticweb.rulewerk.core.model.api; +import java.util.Set; + /*- * #%L * Rulewerk Core Components @@ -28,6 +30,7 @@ * considered existentially quantified. * * @author Markus Krötzsch + * @author Larry González * */ public interface Rule extends SyntaxObject, Statement { @@ -46,4 +49,32 @@ public interface Rule extends SyntaxObject, Statement { */ Conjunction getBody(); + /** + * Returns the conjunction of positive body literals. + * + * @return conjunction of literals + */ + Conjunction getPositiveBodyLiterals(); + + /** + * Returns the conjunction of negative body literals. + * + * @return conjunction of literals + */ + Conjunction getNegativeBodyLiterals(); + + /** + * Returns the list of pieces in the head of the rule. + * + * @return List of Piece + */ + Set getPieces(); + + /** + * @see {@code Piece.isUnconnected} + * + * @return True if the rule contains an unconnected piece. + */ + boolean containsUnconnectedPieces(); + } diff --git a/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/api/Term.java b/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/api/Term.java index 3bbabcfe4..8c760e987 100644 --- a/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/api/Term.java +++ b/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/api/Term.java @@ -54,6 +54,15 @@ default boolean isConstant() { || this.getType() == TermType.LANGSTRING_CONSTANT; } + /** + * Returns true if the term represents some kind of a null. + * + * @return true if term is null + */ + default boolean isNull() { + return this.getType() == TermType.NAMED_NULL; + } + /** * Returns true if the term represents some kind of variable. * @@ -63,6 +72,24 @@ default boolean isVariable() { return this.getType() == TermType.UNIVERSAL_VARIABLE || this.getType() == TermType.EXISTENTIAL_VARIABLE; } + /** + * Returns true if the term represents an existential variable. + * + * @return true if term is an instance of {@code ExistentialVariable} + */ + default boolean isExistentialVariable() { + return this.getType() == TermType.EXISTENTIAL_VARIABLE; + } + + /** + * Returns true if the term represents an universal variable. + * + * @return true if term is an instance of {@code UniversalVariable} + */ + default boolean isUniversalVariable() { + return this.getType() == TermType.UNIVERSAL_VARIABLE; + } + /** * Accept a {@link TermVisitor} and return its output. * diff --git a/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/implementation/PieceImpl.java b/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/implementation/PieceImpl.java new file mode 100644 index 000000000..d9c7167eb --- /dev/null +++ b/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/implementation/PieceImpl.java @@ -0,0 +1,110 @@ +package org.semanticweb.rulewerk.core.model.implementation; + +/*- + * #%L + * Rulewerk Core Components + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import java.util.stream.Stream; + +import org.apache.commons.lang3.Validate; +import org.semanticweb.rulewerk.core.model.api.Conjunction; +import org.semanticweb.rulewerk.core.model.api.Piece; +import org.semanticweb.rulewerk.core.model.api.PositiveLiteral; +import org.semanticweb.rulewerk.core.model.api.Term; + +/** + * Implementation for {@link Piece}. + * + * @author Larry Gonzalez + * + */ +public class PieceImpl implements Piece { + + final Conjunction literals; + + /** + * Creates a Rule with a non-empty body and an non-empty head. All variables in + * the body must be universally quantified; all variables in the head that do + * not occur in the body must be existentially quantified. + * + * @param head list of Literals (negated or non-negated) representing the rule + * body conjuncts. + * @param body list of positive (non-negated) Literals representing the rule + * head conjuncts. + */ + public PieceImpl(final Conjunction literals) { + Validate.notNull(literals); + Validate.notEmpty(literals.getLiterals()); + + this.literals = literals; + + } + + @Override + public int hashCode() { + final int prime = 31; + int result = 1; + result = prime * result + ((literals == null) ? 0 : literals.hashCode()); + return result; + } + + @Override + public boolean equals(Object obj) { + if (this == obj) { + return true; + } + if (obj == null) { + return false; + } + if (!(obj instanceof Piece)) { + return false; + } + + final Piece other = (Piece) obj; + + return this.literals.equals(other.getLiterals()); + } + + @Override + public String toString() { + return Serializer.getSerialization(serializer -> serializer.writeLiteralConjunction(this.literals)); + } + + @Override + public Conjunction getLiterals() { + return this.literals; + } + + @Override + public Stream getTerms() { + return this.literals.getTerms().distinct(); + } + + @Override + public boolean isUnconnected() { + for (PositiveLiteral literal : this.literals) { + if (literal.getUniversalVariables().count() > 0) { + return false; + } + } + // TODO Auto-generated method stub + return true; + } + +} diff --git a/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/implementation/PositiveLiteralImpl.java b/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/implementation/PositiveLiteralImpl.java index dc0892e78..9b6f4a984 100644 --- a/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/implementation/PositiveLiteralImpl.java +++ b/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/implementation/PositiveLiteralImpl.java @@ -25,10 +25,22 @@ import org.semanticweb.rulewerk.core.model.api.PositiveLiteral; import org.semanticweb.rulewerk.core.model.api.Predicate; import org.semanticweb.rulewerk.core.model.api.Term; +import org.semanticweb.rulewerk.core.model.api.TermType; public class PositiveLiteralImpl extends AbstractLiteralImpl implements PositiveLiteral { public PositiveLiteralImpl(final Predicate predicate, final List terms) { super(predicate, terms); } + + @Override + public boolean containsExistentialVariables() { + for (Term term : getArguments()) { + if (term.getType() == TermType.EXISTENTIAL_VARIABLE) { + return true; + } + } + return false; + } + } diff --git a/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/implementation/RuleImpl.java b/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/implementation/RuleImpl.java index 15f35d27e..23fc6845b 100644 --- a/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/implementation/RuleImpl.java +++ b/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/model/implementation/RuleImpl.java @@ -1,5 +1,8 @@ package org.semanticweb.rulewerk.core.model.implementation; +import java.util.ArrayList; +import java.util.HashSet; +import java.util.List; import java.util.Set; import java.util.stream.Collectors; @@ -27,18 +30,22 @@ import org.apache.commons.lang3.Validate; import org.semanticweb.rulewerk.core.model.api.Conjunction; +import org.semanticweb.rulewerk.core.model.api.ExistentialVariable; import org.semanticweb.rulewerk.core.model.api.Literal; +import org.semanticweb.rulewerk.core.model.api.Piece; import org.semanticweb.rulewerk.core.model.api.PositiveLiteral; import org.semanticweb.rulewerk.core.model.api.Rule; import org.semanticweb.rulewerk.core.model.api.StatementVisitor; import org.semanticweb.rulewerk.core.model.api.Term; import org.semanticweb.rulewerk.core.model.api.UniversalVariable; +import org.semanticweb.rulewerk.core.utils.Graph; /** * Implementation for {@link Rule}. Represents rules with non-empty heads and * bodies. * * @author Irina Dragoste + * @author Larry Gonzalez * */ public class RuleImpl implements Rule { @@ -128,4 +135,65 @@ public Stream getTerms() { return Stream.concat(this.body.getTerms(), this.head.getTerms()).distinct(); } + @Override + public Conjunction getPositiveBodyLiterals() { + return new ConjunctionImpl(this.getBody().getLiterals().stream() + .filter(lit -> !lit.isNegated()).map(lit -> (PositiveLiteral) lit).collect(Collectors.toList())); + } + + @Override + public Conjunction getNegativeBodyLiterals() { + return new ConjunctionImpl( + this.getBody().getLiterals().stream().filter(lit -> lit.isNegated()).collect(Collectors.toList())); + } + + @Override + public Set getPieces() { + + List literals = getHead().getLiterals(); + + Graph g = new Graph<>(); + for (int i = 0; i < literals.size() - 1; i++) { + for (int j = i + 1; j < literals.size(); j++) { + PositiveLiteral first = literals.get(i); + PositiveLiteral second = literals.get(j); + + Set existentialVariablesInFirst = first.getExistentialVariables() + .collect(Collectors.toCollection(HashSet::new)); + Set existentialVariablesInSecond = second.getExistentialVariables() + .collect(Collectors.toCollection(HashSet::new)); + + existentialVariablesInFirst.retainAll(existentialVariablesInSecond); + if (existentialVariablesInFirst.size() > 0) { + g.addEdge(i, j); + } + } + } + + Set result = new HashSet<>(); + Set visitedLiterals = new HashSet<>(); + + for (int i = 0; i < literals.size(); i++) { + if (!visitedLiterals.contains(i)) { + List reachableNodes = g.getReachableNodes(i).stream().sorted().collect(Collectors.toList()); + List reachableLiterals = new ArrayList<>(); + reachableNodes.forEach(idx -> reachableLiterals.add(literals.get(idx))); + + result.add(new PieceImpl(new ConjunctionImpl(reachableLiterals))); + visitedLiterals.addAll(reachableNodes); + } + } + return result; + } + + @Override + public boolean containsUnconnectedPieces() { + for (Piece p : getPieces()) { + if (p.isUnconnected()) { + return true; + } + } + return false; + } + } diff --git a/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/utils/Graph.java b/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/utils/Graph.java new file mode 100644 index 000000000..0bd43fe10 --- /dev/null +++ b/rulewerk-core/src/main/java/org/semanticweb/rulewerk/core/utils/Graph.java @@ -0,0 +1,74 @@ +package org.semanticweb.rulewerk.core.utils; + +/*- + * #%L + * rulewerk-utils + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +public class Graph { + + private Map> edges; + + public Graph() { + edges = new HashMap<>(); + } + + public void addEdge(T origin, T destination) { + doAddEdge(origin, destination); + doAddEdge(destination, origin); + } + + public Set getReachableNodes(T node) { + Set result = new HashSet<>(); + result.add(node); + List toVisit = new ArrayList<>(); + toVisit.add(node); + Set visited = new HashSet<>(); + + while (!toVisit.isEmpty()) { + T current = toVisit.remove(toVisit.size() - 1); + if (edges.containsKey(current)) { + for (T next : edges.get(current)) { + result.add(next); + if (!visited.contains(next)) { + toVisit.add(next); + } + } + } + visited.add(current); + } + return result; + } + + private void doAddEdge(T origin, T destination) { + if (edges.containsKey(origin)) { + this.edges.get(origin).add(destination); + } else { + Set newSet = new HashSet<>(); + newSet.add(destination); + this.edges.put(origin, newSet); + } + } +} diff --git a/rulewerk-core/src/test/java/org/semanticweb/rulewerk/core/model/implementation/RuleImplTest.java b/rulewerk-core/src/test/java/org/semanticweb/rulewerk/core/model/implementation/RuleImplTest.java index 6d234958c..401a834e3 100644 --- a/rulewerk-core/src/test/java/org/semanticweb/rulewerk/core/model/implementation/RuleImplTest.java +++ b/rulewerk-core/src/test/java/org/semanticweb/rulewerk/core/model/implementation/RuleImplTest.java @@ -20,17 +20,21 @@ * #L% */ import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertTrue; import static org.junit.Assert.assertFalse; import static org.junit.Assert.assertNotEquals; import java.util.Arrays; import java.util.List; +import java.util.Set; import org.junit.Test; import org.semanticweb.rulewerk.core.model.api.Conjunction; import org.semanticweb.rulewerk.core.model.api.Constant; +import org.semanticweb.rulewerk.core.model.api.Fact; import org.semanticweb.rulewerk.core.model.api.Literal; import org.semanticweb.rulewerk.core.model.api.NegativeLiteral; +import org.semanticweb.rulewerk.core.model.api.Piece; import org.semanticweb.rulewerk.core.model.api.PositiveLiteral; import org.semanticweb.rulewerk.core.model.api.Rule; import org.semanticweb.rulewerk.core.model.api.Variable; @@ -41,19 +45,45 @@ public class RuleImplTest { + final Variable uniX = Expressions.makeUniversalVariable("X"); + final Variable uniY = Expressions.makeUniversalVariable("Y"); + final Variable uniZ = Expressions.makeUniversalVariable("Z"); + + final Variable extY = Expressions.makeExistentialVariable("Y"); + final Variable extZ = Expressions.makeExistentialVariable("Z"); + + final Constant absConC = Expressions.makeAbstractConstant("c"); + final Constant absConD = Expressions.makeAbstractConstant("d"); + + final LanguageStringConstantImpl strConTen = new LanguageStringConstantImpl("T", "en"); + + final PositiveLiteral posLitPUniX = Expressions.makePositiveLiteral("p", uniX); + final PositiveLiteral posLitQUniX = Expressions.makePositiveLiteral("q", uniX); + final PositiveLiteral posLitQUniY = Expressions.makePositiveLiteral("q", uniY); + final PositiveLiteral posLitRUniX = Expressions.makePositiveLiteral("r", uniX); + + final PositiveLiteral posLitPExtY = Expressions.makePositiveLiteral("p", extY); + final PositiveLiteral posLitRUniY = Expressions.makePositiveLiteral("r", uniY); + + final PositiveLiteral posLitPUniXUniZ = Expressions.makePositiveLiteral("p", uniX, uniZ); + final PositiveLiteral posLitPUniYUniX = Expressions.makePositiveLiteral("p", uniY, uniX); + final PositiveLiteral posLitPUniXExtY = Expressions.makePositiveLiteral("p", uniX, extY); + final PositiveLiteral posLitPUniXExtZ = Expressions.makePositiveLiteral("p", uniX, extZ); + final PositiveLiteral posLitQUniXExtY = Expressions.makePositiveLiteral("q", uniX, extY); + + final PositiveLiteral posLitPUniXAbsConC = Expressions.makePositiveLiteral("p", uniX, absConC); + final PositiveLiteral posLitQUniXAbsConD = Expressions.makePositiveLiteral("q", uniX, absConD); + final PositiveLiteral posLitRUniXAbsConD = Expressions.makePositiveLiteral("r", uniX, absConD); + + final NegativeLiteral negLitRUniXAbsConD = Expressions.makeNegativeLiteral("r", uniX, absConD); + + final Fact factSAbsConCStrConTen = Expressions.makeFact("s", absConC, strConTen); + @Test public void testGetters() { - final Variable x = Expressions.makeUniversalVariable("X"); - final Variable y = Expressions.makeExistentialVariable("Y"); - final Variable z = Expressions.makeUniversalVariable("Z"); - final Constant c = Expressions.makeAbstractConstant("c"); - final Constant d = Expressions.makeAbstractConstant("d"); - final Literal atom1 = Expressions.makePositiveLiteral("p", x, c); - final Literal atom2 = Expressions.makePositiveLiteral("p", x, z); - final PositiveLiteral atom3 = Expressions.makePositiveLiteral("q", x, y); - final PositiveLiteral atom4 = Expressions.makePositiveLiteral("r", x, d); - final Conjunction body = Expressions.makeConjunction(atom1, atom2); - final Conjunction head = Expressions.makePositiveConjunction(atom3, atom4); + final Conjunction body = Expressions.makeConjunction(posLitPUniXAbsConC, posLitPUniXUniZ); + final Conjunction head = Expressions.makePositiveConjunction(posLitQUniXExtY, + posLitRUniXAbsConD); final Rule rule = Expressions.makeRule(head, body); assertEquals(body, rule.getBody()); @@ -62,25 +92,16 @@ public void testGetters() { @Test public void testEquals() { - final Variable x = Expressions.makeUniversalVariable("X"); - final Variable y = Expressions.makeExistentialVariable("Y"); - final Variable z = Expressions.makeUniversalVariable("Z"); - final Constant c = Expressions.makeAbstractConstant("c"); - - final PositiveLiteral atom1 = Expressions.makePositiveLiteral("p", x, c); - final PositiveLiteral atom2 = Expressions.makePositiveLiteral("p", x, z); - final PositiveLiteral headAtom1 = Expressions.makePositiveLiteral("q", x, y); - - final Conjunction bodyLiterals = Expressions.makeConjunction(atom1, atom2); - final Conjunction headPositiveLiterals = Expressions.makePositiveConjunction(headAtom1); + final Conjunction bodyLiterals = Expressions.makeConjunction(posLitPUniXAbsConC, posLitPUniXUniZ); + final Conjunction headPositiveLiterals = Expressions.makePositiveConjunction(posLitQUniXExtY); - final Conjunction bodyPositiveLiterals = Expressions.makePositiveConjunction(atom1, atom2); + final Conjunction bodyPositiveLiterals = Expressions + .makePositiveConjunction(posLitPUniXAbsConC, posLitPUniXUniZ); final Rule rule1 = new RuleImpl(headPositiveLiterals, bodyLiterals); - final Rule rule2 = Expressions.makeRule(headAtom1, atom1, atom2); - - final Rule rule6 = Expressions.makeRule(headAtom1, atom1, atom2); - final Rule rule7 = Expressions.makeRule(headAtom1, atom1, atom2); + final Rule rule2 = Expressions.makeRule(posLitQUniXExtY, posLitPUniXAbsConC, posLitPUniXUniZ); + final Rule rule6 = Expressions.makeRule(posLitQUniXExtY, posLitPUniXAbsConC, posLitPUniXUniZ); + final Rule rule7 = Expressions.makeRule(posLitQUniXExtY, posLitPUniXAbsConC, posLitPUniXUniZ); final Rule rule8 = Expressions.makePositiveLiteralsRule(headPositiveLiterals, bodyPositiveLiterals); assertEquals(rule1, rule1); @@ -100,77 +121,141 @@ public void testEquals() { assertNotEquals(rule4, rule1); assertNotEquals(rule5, rule1); assertFalse(rule1.equals(null)); - assertFalse(rule1.equals(c)); + assertFalse(rule1.equals(absConC)); } @Test(expected = IllegalArgumentException.class) public void bodyNonEmpty() { - Expressions.makeRule(Expressions.makePositiveLiteral("p", Expressions.makeUniversalVariable("X"))); + Expressions.makeRule(posLitPUniX); } @Test(expected = NullPointerException.class) public void bodyNotNull() { - final Conjunction head = Expressions - .makePositiveConjunction(Expressions.makePositiveLiteral("p", Expressions.makeUniversalVariable("X"))); + final Conjunction head = Expressions.makePositiveConjunction(posLitPUniX); Expressions.makeRule(head, null); } @Test(expected = IllegalArgumentException.class) public void headNonEmpty() { - final Literal literal = Expressions.makePositiveLiteral("p", Expressions.makeUniversalVariable("X")); - final Conjunction body = Expressions.makeConjunction(literal); + final Conjunction body = Expressions.makeConjunction(posLitPUniX); Expressions.makeRule(Expressions.makePositiveConjunction(), body); } @Test(expected = NullPointerException.class) public void headNotNull() { - final Literal literal = Expressions.makePositiveLiteral("p", Expressions.makeUniversalVariable("X")); - final Conjunction body = Expressions.makeConjunction(literal); + final Conjunction body = Expressions.makeConjunction(posLitPUniX); Expressions.makeRule(null, body); } @Test(expected = IllegalArgumentException.class) public void noExistentialInBody() { - final Literal literal1 = Expressions.makePositiveLiteral("p", Expressions.makeExistentialVariable("X")); - final PositiveLiteral literal2 = Expressions.makePositiveLiteral("q", Expressions.makeUniversalVariable("Y")); - Expressions.makeRule(literal2, literal1); + Expressions.makeRule(posLitQUniY, posLitPUniX); } @Test(expected = IllegalArgumentException.class) public void noUnsafeVariables() { - final PositiveLiteral literal1 = Expressions.makePositiveLiteral("p", Expressions.makeUniversalVariable("X")); - final Literal literal2 = Expressions.makePositiveLiteral("q", Expressions.makeUniversalVariable("Y")); - Expressions.makeRule(literal1, literal2); + Expressions.makeRule(posLitPUniX, posLitQUniY); } @Test public void ruleToStringTest() { - final Variable x = Expressions.makeUniversalVariable("X"); - final Variable y = Expressions.makeExistentialVariable("Y"); - final Variable z = Expressions.makeUniversalVariable("Z"); - final Variable y2 = Expressions.makeUniversalVariable("Y"); - final Constant d = Expressions.makeAbstractConstant("d"); - final Constant c = Expressions.makeAbstractConstant("c"); - final LanguageStringConstantImpl s = new LanguageStringConstantImpl("Test", "en"); - final PositiveLiteral atom1 = Expressions.makePositiveLiteral("p", x, c); - final PositiveLiteral atom2 = Expressions.makePositiveLiteral("p", x, z); - final PositiveLiteral headAtom1 = Expressions.makePositiveLiteral("q", x, y); - final PositiveLiteral positiveLiteral1 = Expressions.makePositiveLiteral("p", x, c); - final PositiveLiteral positiveLiteral2 = Expressions.makePositiveLiteral("p", y2, x); - final PositiveLiteral positiveLiteral3 = Expressions.makePositiveLiteral("q", x, d); - final NegativeLiteral NegativeLiteral = Expressions.makeNegativeLiteral("r", x, d); - final PositiveLiteral PositiveLiteral4 = Expressions.makePositiveLiteral("s", c, s); - final List LiteralList = Arrays.asList(positiveLiteral1, positiveLiteral2, positiveLiteral3, - NegativeLiteral, PositiveLiteral4); - final Conjunction bodyLiterals = Expressions.makeConjunction(atom1, atom2); - final Conjunction headPositiveLiterals = Expressions.makePositiveConjunction(headAtom1); + final List LiteralList = Arrays.asList(posLitPUniXAbsConC, posLitPUniYUniX, posLitQUniXAbsConD, + negLitRUniXAbsConD, factSAbsConCStrConTen); + final Conjunction bodyLiterals = Expressions.makeConjunction(posLitPUniXAbsConC, posLitPUniXUniZ); + final Conjunction headPositiveLiterals = Expressions.makePositiveConjunction(posLitQUniXExtY); final Conjunction bodyConjunction = new ConjunctionImpl<>(LiteralList); final Rule rule1 = new RuleImpl(headPositiveLiterals, bodyLiterals); final Rule rule2 = new RuleImpl(headPositiveLiterals, bodyConjunction); assertEquals("q(?X, !Y) :- p(?X, c), p(?X, ?Z) .", rule1.toString()); - assertEquals("q(?X, !Y) :- p(?X, c), p(?Y, ?X), q(?X, d), ~r(?X, d), s(c, \"Test\"@en) .", rule2.toString()); + assertEquals("q(?X, !Y) :- p(?X, c), p(?Y, ?X), q(?X, d), ~r(?X, d), s(c, \"T\"@en) .", rule2.toString()); + } + + @Test + public void getPieces00() { + // q(?X):- p(?X) . + final Conjunction head = Expressions.makePositiveConjunction(posLitQUniX); + final Conjunction body = Expressions.makeConjunction(posLitPUniX); + + final Rule rule = new RuleImpl(head, body); + + Set pieces = rule.getPieces(); + assertEquals(pieces.size(), 1); + assertTrue(pieces.contains(new PieceImpl(head))); + } + + @Test + public void getPieces01() { + // p(?X,!Y),q(?X,!Y):- r(?X) . + final Conjunction head = Expressions.makePositiveConjunction(posLitPUniXExtY, posLitQUniXExtY); + final Conjunction body = Expressions.makeConjunction(posLitRUniX); + + final Rule rule = new RuleImpl(head, body); + + Set pieces = rule.getPieces(); + + assertEquals(pieces.size(), 1); + assertTrue(pieces.contains(new PieceImpl(head))); + } + + @Test + public void getPieces02() { + // p(?X,!Y),q(?X,!Z):- r(?X) . + final Conjunction head = Expressions.makePositiveConjunction(posLitPUniXExtY, posLitPUniXExtZ); + final Conjunction body = Expressions.makeConjunction(posLitRUniX); + + final Rule rule = new RuleImpl(head, body); + + Piece piece1 = new PieceImpl(Expressions.makePositiveConjunction(posLitPUniXExtY)); + Piece piece2 = new PieceImpl(Expressions.makePositiveConjunction(posLitPUniXExtZ)); + + Set pieces = rule.getPieces(); + assertEquals(pieces.size(), 2); + assertTrue(pieces.contains(piece1)); + assertTrue(pieces.contains(piece2)); + } + + @Test + public void unconnectedPiece01() { + // q(?X):- p(?X) . + final Conjunction head = Expressions.makePositiveConjunction(posLitQUniX); + final Conjunction body = Expressions.makeConjunction(posLitPUniX); + + final Rule rule = new RuleImpl(head, body); + + assertFalse(rule.containsUnconnectedPieces()); + } + @Test + public void unconnectedPiece02() { + // p(?X,!Y),q(?X,!Y):- r(?X) . + final Conjunction head = Expressions.makePositiveConjunction(posLitPUniXExtY, posLitQUniXExtY); + final Conjunction body = Expressions.makeConjunction(posLitRUniX); + + final Rule rule = new RuleImpl(head, body); + + assertFalse(rule.containsUnconnectedPieces()); + } + + @Test + public void unconnectedPiece03() { + // p(!Y):- p(?X) . + final Conjunction head = Expressions.makePositiveConjunction(posLitPExtY); + final Conjunction body = Expressions.makeConjunction(posLitPUniX); + + final Rule rule = new RuleImpl(head, body); + + assertTrue(rule.containsUnconnectedPieces()); } + @Test + public void unconnectedPiece04() { + // q(?X,!Y), r(!Y):- p(?X) . + final Conjunction head = Expressions.makePositiveConjunction(posLitQUniXExtY, posLitRUniX); + final Conjunction body = Expressions.makeConjunction(posLitPUniX); + + final Rule rule = new RuleImpl(head, body); + + assertFalse(rule.containsUnconnectedPieces()); + } } diff --git a/rulewerk-core/src/test/java/org/semanticweb/rulewerk/core/utils/GraphTest.java b/rulewerk-core/src/test/java/org/semanticweb/rulewerk/core/utils/GraphTest.java new file mode 100644 index 000000000..fbccce010 --- /dev/null +++ b/rulewerk-core/src/test/java/org/semanticweb/rulewerk/core/utils/GraphTest.java @@ -0,0 +1,96 @@ +package org.semanticweb.rulewerk.core.utils; + +/*- + * #%L + * rulewerk-utils + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import static org.junit.Assert.assertEquals; + +import java.util.Set; + +import org.junit.Test; +import org.mockito.internal.util.collections.Sets; +import org.semanticweb.rulewerk.core.utils.Graph; + +public class GraphTest { + + @Test + public void getReachableNodesSimpleGraphTest() { + final Graph g = new Graph<>(); + g.addEdge(1, 1); + + assertEquals(Sets.newSet(1), g.getReachableNodes(1)); + } + + @Test + public void getReachableNodesCyclicGraphTest() { + + final Graph g = new Graph<>(); + final Set s = Sets.newSet(1, 2, 3); + g.addEdge(1, 2); + g.addEdge(2, 3); + g.addEdge(3, 1); + + assertEquals(s, g.getReachableNodes(1)); + assertEquals(s, g.getReachableNodes(2)); + assertEquals(s, g.getReachableNodes(3)); + } + + @Test + public void getReachableNodesTreeGraphTest() { + + final Graph g = new Graph<>(); + final Set s = Sets.newSet(1, 2, 3, 4, 5, 6, 7); + g.addEdge(1, 2); + g.addEdge(1, 3); + g.addEdge(2, 4); + g.addEdge(2, 5); + g.addEdge(1, 6); + g.addEdge(1, 7); + + assertEquals(s, g.getReachableNodes(1)); + assertEquals(s, g.getReachableNodes(2)); + assertEquals(s, g.getReachableNodes(3)); + assertEquals(s, g.getReachableNodes(4)); + assertEquals(s, g.getReachableNodes(5)); + assertEquals(s, g.getReachableNodes(6)); + assertEquals(s, g.getReachableNodes(7)); + } + + @Test + public void getReachableNodesUnconnectedGraphTest() { + + final Graph g = new Graph<>(); + final Set s1 = Sets.newSet(1, 2, 3); + final Set s2 = Sets.newSet(4, 5, 6); + g.addEdge(1, 2); + g.addEdge(1, 3); + g.addEdge(4, 5); + g.addEdge(5, 6); + g.addEdge(6, 4); + + assertEquals(s1, g.getReachableNodes(1)); + assertEquals(s1, g.getReachableNodes(2)); + assertEquals(s1, g.getReachableNodes(3)); + assertEquals(s2, g.getReachableNodes(4)); + assertEquals(s2, g.getReachableNodes(5)); + assertEquals(s2, g.getReachableNodes(6)); + } + +} diff --git a/rulewerk-examples/pom.xml b/rulewerk-examples/pom.xml index 341378aec..7746028dd 100644 --- a/rulewerk-examples/pom.xml +++ b/rulewerk-examples/pom.xml @@ -1,5 +1,6 @@ - 4.0.0 @@ -42,6 +43,11 @@ rulewerk-parser ${project.version} + + ${project.groupId} + rulewerk-reliances + ${project.version} + ${project.groupId} rulewerk-vlog @@ -62,7 +68,8 @@ org.openrdf.sesame sesame-rio-turtle - + ${openrdf.sesame.version} @@ -70,15 +77,16 @@ org.openrdf.sesame sesame-rio-rdfxml - + ${openrdf.sesame.version} - - fr.lirmm.graphik - graal-io-dlgp - ${graal.version} - + + fr.lirmm.graphik + graal-io-dlgp + ${graal.version} + diff --git a/rulewerk-examples/src/main/data/input/doid-local-positive-reliance.rls b/rulewerk-examples/src/main/data/input/doid-local-positive-reliance.rls new file mode 100644 index 000000000..c87b07676 --- /dev/null +++ b/rulewerk-examples/src/main/data/input/doid-local-positive-reliance.rls @@ -0,0 +1,40 @@ +@prefix rdfs: . +@prefix wdqs: . + +@source doidTriple[3]: load-rdf("src/main/data/input/doid.nt.gz") . + +@source diseaseId[2]: load-csv("src/main/data/input/wd-doid-diseaseId.csv.gz") . + +@source recentDeaths[1]: load-csv("src/main/data/input/wd-doid-recentDeadths.csv.gz") . + +@source recentDeathsCause[2]: load-csv("src/main/data/input/wd-doid-recentDeathsCause.csv.gz") . + +p1(1) . +p2(1) . +p3(1) . +p4(1) . +p5(1) . +p6(1) . +p7(1) . + +% Combine recent death data (infer "unknown" cause if no cause given): +deathCause(?X, ?Z), p1(1) :- recentDeathsCause(?X, ?Z) . +deathCause(?X, !Z), p2(1) :- recentDeaths(?X) . + +% Mark Wikidata diseases that have a DOID: +hasDoid(?X) :- diseaseId(?X, ?DoidId) . + +% Relate DOID string ID (used on Wikidata) to DOID IRI (used in DOID ontology) +doid(?Iri, ?DoidId), p3(1) :- doidTriple(?Iri, ,?DoidId) . + +% Compute transitive closure of DOID subclass hierarchy +diseaseHierarchy(?X, ?Y), p4(1) :- doidTriple(?X, rdfs:subClassOf, ?Y) . +diseaseHierarchy(?X, ?Z), p5(1) :- diseaseHierarchy(?X, ?Y), doidTriple(?Y, rdfs:subClassOf, ?Z), ~p4(2) . + +% Find DOID ids for all subclasses of cancer: +cancerDisease(?Xdoid), p6(1) :- diseaseHierarchy(?X, ?Y), doid(?Y, "DOID:162"), doid(?X, ?Xdoid), ~p3(2), ~p4(2), ~p5(2) . + +% Compute who died of cancer and who died of something else (including diseases unknown to DOID): +humansWhoDiedOfCancer(?X) :- deathCause(?X, ?Y), diseaseId(?Y, ?Z), cancerDisease(?Z), ~p1(2), ~p6(2) . +humansWhoDiedOfNoncancer(?X) :- deathCause(?X, ?Y), diseaseId(?Y, ?Z), ~cancerDisease(?Z), ~p1(2) . +humansWhoDiedOfNoncancer(?X) :- deathCause(?X, ?Y), ~hasDoid(?Y), ~p1(2), ~p2(2) . \ No newline at end of file diff --git a/rulewerk-examples/src/main/data/input/doid-local.rls b/rulewerk-examples/src/main/data/input/doid-local.rls new file mode 100644 index 000000000..a4cd84953 --- /dev/null +++ b/rulewerk-examples/src/main/data/input/doid-local.rls @@ -0,0 +1,32 @@ +@prefix rdfs: . +@prefix wdqs: . + +@source doidTriple[3]: load-rdf("src/main/data/input/doid.nt.gz") . + +@source diseaseId[2]: load-csv("src/main/data/input/wd-doid-diseaseId.csv.gz") . + +@source recentDeaths[1]: load-csv("src/main/data/input/wd-doid-recentDeadths.csv.gz") . + +@source recentDeathsCause[2]: load-csv("src/main/data/input/wd-doid-recentDeathsCause.csv.gz") . + +% Combine recent death data (infer "unknown" cause if no cause given): +deathCause(?X, ?Z) :- recentDeathsCause(?X, ?Z) . +deathCause(?X, !Z) :- recentDeaths(?X) . + +% Mark Wikidata diseases that have a DOID: +hasDoid(?X) :- diseaseId(?X, ?DoidId) . + +% Relate DOID string ID (used on Wikidata) to DOID IRI (used in DOID ontology) +doid(?Iri, ?DoidId) :- doidTriple(?Iri, ,?DoidId) . + +% Compute transitive closure of DOID subclass hierarchy +diseaseHierarchy(?X, ?Y) :- doidTriple(?X, rdfs:subClassOf, ?Y) . +diseaseHierarchy(?X, ?Z) :- diseaseHierarchy(?X, ?Y), doidTriple(?Y, rdfs:subClassOf, ?Z) . + +% Find DOID ids for all subclasses of cancer: +cancerDisease(?Xdoid) :- diseaseHierarchy(?X, ?Y), doid(?Y, "DOID:162"), doid(?X, ?Xdoid) . + +% Compute who died of cancer and who died of something else (including diseases unknown to DOID): +humansWhoDiedOfCancer(?X) :- deathCause(?X, ?Y), diseaseId(?Y, ?Z), cancerDisease(?Z) . +humansWhoDiedOfNoncancer(?X) :- deathCause(?X, ?Y), diseaseId(?Y, ?Z), ~cancerDisease(?Z) . +humansWhoDiedOfNoncancer(?X) :- deathCause(?X, ?Y), ~hasDoid(?Y) . diff --git a/rulewerk-examples/src/main/data/input/doid.rls b/rulewerk-examples/src/main/data/input/doid.rls index e50e4e3ef..041f32519 100644 --- a/rulewerk-examples/src/main/data/input/doid.rls +++ b/rulewerk-examples/src/main/data/input/doid.rls @@ -2,11 +2,14 @@ @prefix wdqs: . @source doidTriple[3]: load-rdf("src/main/data/input/doid.nt.gz") . + @source diseaseId[2]: sparql(wdqs:sparql, "disease,doid", "?disease wdt:P699 ?doid .") . + @source recentDeaths[1]: sparql(wdqs:sparql, "human", '''?human wdt:P31 wd:Q5; wdt:P570 ?deathDate . FILTER (YEAR(?deathDate) = 2018)''') . + @source recentDeathsCause[2]: sparql(wdqs:sparql, "human,causeOfDeath", '''?human wdt:P31 wd:Q5; wdt:P570 ?deathDate ; diff --git a/rulewerk-examples/src/main/data/input/wd-doid-diseaseId.csv.gz b/rulewerk-examples/src/main/data/input/wd-doid-diseaseId.csv.gz new file mode 100644 index 000000000..c42201c05 Binary files /dev/null and b/rulewerk-examples/src/main/data/input/wd-doid-diseaseId.csv.gz differ diff --git a/rulewerk-examples/src/main/data/input/wd-doid-recentDeadths.csv.gz b/rulewerk-examples/src/main/data/input/wd-doid-recentDeadths.csv.gz new file mode 100644 index 000000000..74bde1c03 Binary files /dev/null and b/rulewerk-examples/src/main/data/input/wd-doid-recentDeadths.csv.gz differ diff --git a/rulewerk-examples/src/main/data/input/wd-doid-recentDeathsCause.csv.gz b/rulewerk-examples/src/main/data/input/wd-doid-recentDeathsCause.csv.gz new file mode 100644 index 000000000..fa9bfd22c Binary files /dev/null and b/rulewerk-examples/src/main/data/input/wd-doid-recentDeathsCause.csv.gz differ diff --git a/rulewerk-examples/src/main/java/org/semanticweb/rulewerk/examples/reliances/DoidPerformance.java b/rulewerk-examples/src/main/java/org/semanticweb/rulewerk/examples/reliances/DoidPerformance.java new file mode 100644 index 000000000..648ad54d7 --- /dev/null +++ b/rulewerk-examples/src/main/java/org/semanticweb/rulewerk/examples/reliances/DoidPerformance.java @@ -0,0 +1,114 @@ +package org.semanticweb.rulewerk.examples.reliances; + +/*- + * #%L + * Rulewerk Examples + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import java.io.FileInputStream; +import java.io.IOException; +import java.util.Arrays; +import java.util.List; + +import org.semanticweb.rulewerk.core.reasoner.KnowledgeBase; +import org.semanticweb.rulewerk.core.reasoner.LogLevel; +import org.semanticweb.rulewerk.core.reasoner.Reasoner; +import org.semanticweb.rulewerk.examples.ExamplesUtils; +import org.semanticweb.rulewerk.reasoner.vlog.VLogReasoner; +import org.semanticweb.rulewerk.parser.ParsingException; +import org.semanticweb.rulewerk.parser.RuleParser; + +/** + * This example reasons about human diseases, based on information from the + * Disease Ontology (DOID) and Wikidata. It illustrates how to load data from + * different sources (RDF file, SPARQL), and reason about these inputs using + * rules that are loaded from a file. The rules used here employ existential + * quantifiers and stratified negation. + * + * @author Markus Kroetzsch + * @author Larry Gonzalez + */ +public class DoidPerformance { + + static private void meterialize(String ruleFile, String kind, int i) throws IOException, ParsingException { +// ExamplesUtils.configureLogging(); + + /* Configure rules */ + KnowledgeBase kb; + try { + kb = RuleParser.parse(new FileInputStream(ExamplesUtils.INPUT_FOLDER + ruleFile)); // THIS SHOULD BE + // CHANGED + } catch (final ParsingException e) { + System.out.println("Failed to parse rules: " + e.getMessage()); + return; + } + + try (Reasoner reasoner = new VLogReasoner(kb)) { + reasoner.setLogFile(ExamplesUtils.OUTPUT_FOLDER + "vlog-" + kind + "-" + i + ".log"); + reasoner.setLogLevel(LogLevel.DEBUG); + + /* Initialise reasoner and compute inferences */ + reasoner.reason(); + + /* Execute some queries */ + final List queries = Arrays.asList("humansWhoDiedOfCancer(?X)", "humansWhoDiedOfNoncancer(?X)", + "deathCause(?X,?Y)", "hasDoid(?X)", "doid(?X, ?Y)", "diseaseHierarchy(?X, ?Y)", + "cancerDisease(?X)"); + System.out.println("\nNumber of inferred tuples for selected query atoms:"); + for (final String queryString : queries) { + double answersCount = reasoner.countQueryAnswers(RuleParser.parsePositiveLiteral(queryString)) + .getCount(); + System.out.println(" " + queryString + ": " + answersCount); + } + } + + } + + static private void print(long[] array) { + String content = "["; + for (int i = 0; i < array.length; i++) { + content += array[i] + ", "; + } + content += "]"; + System.out.println(content); + } + + public static void main(final String[] args) throws IOException, ParsingException { + // normal + long startTime, endTime; + long first[] = new long[10]; + for (int i = 0; i < 10; i++) { + startTime = System.currentTimeMillis(); + meterialize("/doid-local.rls", "ori", i); + endTime = System.currentTimeMillis(); + first[i] = endTime - startTime; + } + + long second[] = new long[10]; + for (int i = 0; i < 10; i++) { + startTime = System.currentTimeMillis(); + meterialize("/doid-local-positive-reliance.rls", "mod", i); + endTime = System.currentTimeMillis(); + second[i] = endTime - startTime; + } + + print(first); + print(second); + } + +} diff --git a/rulewerk-examples/src/main/java/org/semanticweb/rulewerk/examples/reliances/DoidPositiveReliance.java b/rulewerk-examples/src/main/java/org/semanticweb/rulewerk/examples/reliances/DoidPositiveReliance.java new file mode 100644 index 000000000..8186c0955 --- /dev/null +++ b/rulewerk-examples/src/main/java/org/semanticweb/rulewerk/examples/reliances/DoidPositiveReliance.java @@ -0,0 +1,100 @@ +package org.semanticweb.rulewerk.examples.reliances; + +/*- + * #%L + * Rulewerk Examples + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import java.io.FileInputStream; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; + +import org.semanticweb.rulewerk.core.model.api.Fact; +import org.semanticweb.rulewerk.core.model.api.Literal; +import org.semanticweb.rulewerk.core.model.api.PositiveLiteral; +import org.semanticweb.rulewerk.core.model.api.Rule; +import org.semanticweb.rulewerk.core.model.implementation.ConjunctionImpl; +import org.semanticweb.rulewerk.core.model.implementation.RuleImpl; +import org.semanticweb.rulewerk.core.reasoner.KnowledgeBase; +import org.semanticweb.rulewerk.examples.ExamplesUtils; +import org.semanticweb.rulewerk.parser.RuleParser; +import org.semanticweb.rulewerk.reliances.Reliance; + +public class DoidPositiveReliance { + + static private Rule addHeadAtom(Rule rule, PositiveLiteral literal) { + List head = new ArrayList<>(); + rule.getHead().getLiterals().forEach(pl -> head.add(pl)); + head.add(literal); + return new RuleImpl(new ConjunctionImpl(head), rule.getBody()); + } + + static private Rule addBodyAtom(Rule rule, Literal literal) { + List body = new ArrayList<>(); + rule.getBody().getLiterals().forEach(l -> body.add(l)); + body.add(literal); + return new RuleImpl(rule.getHead(), new ConjunctionImpl(body)); + } + + static public void main(String args[]) throws Exception { + KnowledgeBase kb = RuleParser.parse(new FileInputStream(ExamplesUtils.INPUT_FOLDER + "/doid.rls")); + + HashMap rules = new HashMap<>(); + kb.getRules().forEach(rule -> rules.put(rules.size(), rule)); + + System.out.println("Rules used in this example:"); + for (int i = 0; i < rules.size(); i++) { + System.out.println(i + ": " + rules.get(i)); + } + + List positiveDependency = new ArrayList<>(); + for (int i = 0; i < rules.size(); i++) { + for (int j = 0; j < rules.size(); j++) { + if (Reliance.positively(rules.get(i), rules.get(j))) { + positiveDependency.add(new int[] { i, j }); + } + } + } + + KnowledgeBase kb2 = new KnowledgeBase(); + for (int i = 0; i < positiveDependency.size(); i++) { + String name = "newPredicateName"; + Fact fact = RuleParser.parseFact(name + i + "(1)."); + PositiveLiteral literal1 = RuleParser.parsePositiveLiteral(name + i + "(1)"); + Literal literal2 = RuleParser.parseLiteral("~" + name + i + "(2)"); + + int[] pair = positiveDependency.get(i); + if (pair[0] != pair[1]) { + kb2.addStatement(fact); + Rule r1 = addHeadAtom(rules.get(pair[0]), literal1); + System.out.println(r1); + rules.replace(pair[0], addHeadAtom(rules.get(pair[0]), literal1)); + rules.replace(pair[1], addBodyAtom(rules.get(pair[1]), literal2)); + } + } + + for (int i = 0; i < rules.size(); i++) { + kb2.addStatement(rules.get(i)); + } + + System.out.println("XXXXXXXXXXXXXXXXXXXXXXXXXXXXXX"); + kb2.getFacts().forEach(System.out::println); + kb2.getRules().forEach(System.out::println); + } +} diff --git a/rulewerk-parser/src/main/java/org/semanticweb/rulewerk/parser/javacc/JavaCCParser.jj b/rulewerk-parser/src/main/java/org/semanticweb/rulewerk/parser/javacc/JavaCCParser.jj index cc7568888..c17911950 100644 --- a/rulewerk-parser/src/main/java/org/semanticweb/rulewerk/parser/javacc/JavaCCParser.jj +++ b/rulewerk-parser/src/main/java/org/semanticweb/rulewerk/parser/javacc/JavaCCParser.jj @@ -321,16 +321,24 @@ Term term(FormulaContext context) throws PrefixDeclarationException : { | c = RDFLiteral() { return c; } | t = < UNIVAR > { s = t.image.substring(1); - if (context == FormulaContext.HEAD) + if (context == FormulaContext.HEAD) { + if (headExiVars.contains(s)) { + throw new ParseException("Universal variables can not appear as Existential variable. Line: " + t.beginLine + ", Column: "+ t.beginColumn); + } headUniVars.add(s); + } else if (context == FormulaContext.BODY) bodyVars.add(s); return createUniversalVariable(s); } | t = < EXIVAR > { s = t.image.substring(1); - if (context == FormulaContext.HEAD) + if (context == FormulaContext.HEAD) { + if (headUniVars.contains(s)) { + throw new ParseException("Existential variables can not appear as Universal variable. Line: " + t.beginLine + ", Column: "+ t.beginColumn); + } headExiVars.add(s); + } if (context == FormulaContext.BODY) throw new ParseException("Existentialy quantified variables can not appear in the body. Line: " + t.beginLine + ", Column: "+ t.beginColumn); return createExistentialVariable(s); diff --git a/rulewerk-parser/src/main/java/org/semanticweb/rulewerk/parser/javacc/JavaCCParserBase.java b/rulewerk-parser/src/main/java/org/semanticweb/rulewerk/parser/javacc/JavaCCParserBase.java index 981632edf..9ff6a1df9 100644 --- a/rulewerk-parser/src/main/java/org/semanticweb/rulewerk/parser/javacc/JavaCCParserBase.java +++ b/rulewerk-parser/src/main/java/org/semanticweb/rulewerk/parser/javacc/JavaCCParserBase.java @@ -22,6 +22,7 @@ import java.util.HashSet; import java.util.List; +import java.util.Set; import org.semanticweb.rulewerk.core.exceptions.PrefixDeclarationException; import org.semanticweb.rulewerk.core.model.api.AbstractConstant; @@ -72,15 +73,15 @@ public class JavaCCParserBase { /** * "Local" variable to remember (universal) body variables during parsing. */ - protected final HashSet bodyVars = new HashSet(); + protected final Set bodyVars = new HashSet(); /** * "Local" variable to remember existential head variables during parsing. */ - protected final HashSet headExiVars = new HashSet(); + protected final Set headExiVars = new HashSet(); /** * "Local" variable to remember universal head variables during parsing. */ - protected final HashSet headUniVars = new HashSet(); + protected final Set headUniVars = new HashSet(); /** * Defines the context for parsing sub-formulas. diff --git a/rulewerk-parser/src/test/java/org/semanticweb/rulewerk/parser/LiteralParserTest.java b/rulewerk-parser/src/test/java/org/semanticweb/rulewerk/parser/LiteralParserTest.java new file mode 100644 index 000000000..e13df2df3 --- /dev/null +++ b/rulewerk-parser/src/test/java/org/semanticweb/rulewerk/parser/LiteralParserTest.java @@ -0,0 +1,48 @@ +package org.semanticweb.rulewerk.parser; + +/*- + * #%L + * Rulewerk Parser + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import org.junit.Assert; +import org.junit.Test; +import org.semanticweb.rulewerk.core.model.api.ExistentialVariable; +import org.semanticweb.rulewerk.core.model.api.Literal; +import org.semanticweb.rulewerk.core.model.api.UniversalVariable; +import org.semanticweb.rulewerk.core.model.implementation.Expressions; + +public class LiteralParserTest implements ParserTestUtils { + + private final UniversalVariable uX = Expressions.makeUniversalVariable("X"); + private final ExistentialVariable eX = Expressions.makeExistentialVariable("X"); + private final Literal puXeX = Expressions.makePositiveLiteral("p", uX, eX); + private final Literal peXuX = Expressions.makePositiveLiteral("p", eX, uX); + + @Test(expected = ParsingException.class) + public void pX1() throws ParsingException { + Literal literal = RuleParser.parseLiteral("p(?X, !X)"); + Assert.assertEquals(literal, puXeX); + } + + @Test(expected = ParsingException.class) + public void pX2() throws ParsingException { + Literal literal = RuleParser.parseLiteral("p(!X, ?X)"); + Assert.assertEquals(literal, peXuX); + } +} diff --git a/rulewerk-reliances/LICENSE.txt b/rulewerk-reliances/LICENSE.txt new file mode 100644 index 000000000..261eeb9e9 --- /dev/null +++ b/rulewerk-reliances/LICENSE.txt @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/rulewerk-reliances/pom.xml b/rulewerk-reliances/pom.xml new file mode 100644 index 000000000..667917c73 --- /dev/null +++ b/rulewerk-reliances/pom.xml @@ -0,0 +1,42 @@ + + + 4.0.0 + + + org.semanticweb.rulewerk + rulewerk-parent + 0.8.0-SNAPSHOT + + + rulewerk-reliances + jar + + Rulewerk Reliances + Contains code to compute positive reliances, negative reliances, and restrains between rules + + + + ${project.groupId} + rulewerk-core + ${project.version} + + + ${project.groupId} + rulewerk-parser + ${project.version} + + + ${project.groupId} + rulewerk-vlog + ${project.version} + + + org.slf4j + slf4j-log4j12 + ${slf4j.version} + + + + \ No newline at end of file diff --git a/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/logic/MartelliMontanariUnifier.java b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/logic/MartelliMontanariUnifier.java new file mode 100644 index 000000000..fc1ae0daa --- /dev/null +++ b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/logic/MartelliMontanariUnifier.java @@ -0,0 +1,116 @@ +package org.semanticweb.rulewerk.logic; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import java.util.List; +import java.util.Map; + +import org.semanticweb.rulewerk.core.model.api.Literal; +import org.semanticweb.rulewerk.core.model.api.Term; +import org.semanticweb.rulewerk.core.model.api.UniversalVariable; + +/** + * An implementation of the Martelli & Montanari unification algorithm for + * predicate logic without function symbols. + * + * @author Larry González + * + */ +public class MartelliMontanariUnifier implements Unifier { + final private Substitution substitution; + private boolean success; + + /** + * An implementation of the Martelli & Montanari unification algorithm for + * predicate logic without function symbols. + * + * It will unify pair-wise every pair key-value in {@code mapping} + */ + public MartelliMontanariUnifier(Map mapping) { + substitution = new Substitution(); + success = true; + mapping.forEach((key, value) -> { + if (success) { + unify(key, value); + } + }); + } + + private void unify(Literal first, Literal second) { + if (!first.getPredicate().equals(second.getPredicate()) || first.isNegated() != second.isNegated()) { + + success = false; + } else { + List terms1 = first.getArguments(); + List terms2 = second.getArguments(); + for (int i = 0; i < terms1.size(); i++) { + unify(terms1.get(i), terms2.get(i)); + } + } + } + + private void unify(Term first, Term second) { + Term rep1 = substitution.getValue(first); + Term rep2 = substitution.getValue(second); + if (first.isExistentialVariable() || second.isExistentialVariable() || rep1.isExistentialVariable() + || rep2.isExistentialVariable()) { + throw new IllegalArgumentException("Unification is not defined for Existential Variables"); + } + + if (rep1.isConstant()) { + if (rep2.isConstant()) { + success &= rep1.equals(rep2); + } else if (rep2.isNull()) { + success = false; + } else { + substitution.add((UniversalVariable) rep2, rep1); + } + } else if (rep1.isNull()) { + if (rep2.isConstant()) { + success = false; + } else if (rep2.isNull()) { + success &= rep1.equals(rep2); + } else { + substitution.add((UniversalVariable) rep2, rep1); + } + } else { + if (!rep1.equals(rep2)) { + substitution.add((UniversalVariable) rep1, rep2); + } + } + } + + + @Override + public boolean isSuccessful() { + return success; + } + + @Override + public Substitution getSubstitution() { + return substitution; + } + + @Override + public String toString() { + return "{"+success+", "+substitution+"}"; + } +} diff --git a/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/logic/Substitute.java b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/logic/Substitute.java new file mode 100644 index 000000000..1226d2e28 --- /dev/null +++ b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/logic/Substitute.java @@ -0,0 +1,53 @@ +package org.semanticweb.rulewerk.logic; + +import java.util.List; +import java.util.stream.Collectors; + +import org.semanticweb.rulewerk.core.model.api.Literal; +import org.semanticweb.rulewerk.core.model.api.NegativeLiteral; +import org.semanticweb.rulewerk.core.model.api.PositiveLiteral; +import org.semanticweb.rulewerk.core.model.api.Rule; +import org.semanticweb.rulewerk.core.model.api.Term; +import org.semanticweb.rulewerk.core.model.implementation.Expressions; + +public class Substitute { + + static public Term term(Substitution subst, Term term) { + return subst.contains(term) ? subst.getValue(term) : term; + } + + static public PositiveLiteral positiveLiteral(Substitution subst, PositiveLiteral literal) { + return Expressions.makePositiveLiteral(literal.getPredicate(), terms(subst, literal.getArguments())); + } + + static public NegativeLiteral negativeLiteral(Substitution subst, NegativeLiteral literal) { + return Expressions.makeNegativeLiteral(literal.getPredicate(), terms(subst, literal.getArguments())); + } + + static public Literal literal(Substitution subst, Literal literal) { + return literal.isNegated() ? negativeLiteral(subst, (NegativeLiteral) literal) + : positiveLiteral(subst, (PositiveLiteral) literal); + } + + static public List terms(Substitution subst, List terms) { + return terms.stream().map(term -> term(subst, term)).collect(Collectors.toList()); + } + + static public List positiveLiterals(Substitution subst, List literals) { + return literals.stream().map(literal -> positiveLiteral(subst, literal)).collect(Collectors.toList()); + } + + static public List negativeLiterals(Substitution subst, List literals) { + return literals.stream().map(literal -> negativeLiteral(subst, literal)).collect(Collectors.toList()); + } + + static public List literals(Substitution subst, List literals) { + return literals.stream().map(literal -> literal(subst, literal)).collect(Collectors.toList()); + } + + static public Rule rule(Substitution subst, Rule rule) { + List newBody = literals(subst, rule.getBody().getLiterals()); + List newHead = positiveLiterals(subst, rule.getHead().getLiterals()); + return Expressions.makeRule(Expressions.makeConjunction(newHead), Expressions.makeConjunction(newBody)); + } +} diff --git a/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/logic/Substitution.java b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/logic/Substitution.java new file mode 100644 index 000000000..92e15041b --- /dev/null +++ b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/logic/Substitution.java @@ -0,0 +1,57 @@ +package org.semanticweb.rulewerk.logic; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2021 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import java.util.HashMap; +import java.util.Map; +import java.util.stream.Collectors; + +import org.semanticweb.rulewerk.core.model.api.Term; +import org.semanticweb.rulewerk.core.model.api.Variable; + +public class Substitution { + final private Map substitution; + + public Substitution() { + substitution = new HashMap<>(); + } + + public void add(Variable key, Term value) { + if (key.equals(value)) { + throw new IllegalArgumentException("Pairs key-value should be different in Substutions"); + } + substitution.put(key, value); + } + + public boolean contains(Term key) { + return substitution.containsKey(key); + } + + public Term getValue(Term key) { + return substitution.containsKey(key) ? getValue(substitution.get(key)) : key; + } + + @Override + public String toString() { + return substitution.keySet().stream().map(k -> k + ":" + substitution.get(k)).collect(Collectors.joining(",")); + } + +} diff --git a/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/logic/Unifier.java b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/logic/Unifier.java new file mode 100644 index 000000000..69825db5c --- /dev/null +++ b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/logic/Unifier.java @@ -0,0 +1,39 @@ +package org.semanticweb.rulewerk.logic; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2021 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +public interface Unifier { + + /* + * Getter for Success + */ + public boolean isSuccessful(); + + /* + * Getter for Substitution + */ + public Substitution getSubstitution(); + + /* + * toString method + */ + public String toString(); +} diff --git a/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/math/permutation/KOverNIterable.java b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/math/permutation/KOverNIterable.java new file mode 100644 index 000000000..9f704cb89 --- /dev/null +++ b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/math/permutation/KOverNIterable.java @@ -0,0 +1,47 @@ +package org.semanticweb.rulewerk.math.permutation; + +import java.util.BitSet; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2021 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import java.util.Iterator; + +/** + * A class to iterate over all combinations of choosing k elements from n, + * represented as set indexes in a BitSet, over an Iterable. + * + * @author Larry González + * + */ +public class KOverNIterable implements Iterable { + + KOverNIterator kOverNIterator; + + public KOverNIterable(int n, int k) { + kOverNIterator = new KOverNIterator(n, k); + } + + @Override + public Iterator iterator() { + return kOverNIterator; + } + +} diff --git a/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/math/permutation/KOverNIterator.java b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/math/permutation/KOverNIterator.java new file mode 100644 index 000000000..e0829d75d --- /dev/null +++ b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/math/permutation/KOverNIterator.java @@ -0,0 +1,134 @@ +package org.semanticweb.rulewerk.math.permutation; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2021 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import java.util.BitSet; +import java.util.Iterator; + +/** + * A class to iterate over all combinations of choosing k elements from n, + * represented as set indexes in a BitSet, over an Iterator. + * + * @author Larry González + * + */ +public class KOverNIterator implements Iterator { + int k; + int n; + BitSet combination; + BitSet end; + + /** + * {@code KOverNIterator} constructor. + * + * @note The bit {@value n} is used as a flag. If true then the iteration has + * finished. + * + * @param n total number of set elements + * @param k number of elements to choose over n + * @return + * @return + */ + public KOverNIterator(int n, int k) { + this.n = n; + this.k = k; + this.combination = new BitSet(n + 1); + this.end = new BitSet(n + 1); + this.combination.set(0, k, true); + this.combination.set(k, n, false); + this.end.set(0, n - k, false); + this.end.set(n - k, n, true); + } + + @Override + public boolean hasNext() { + return !combination.get(n); + } + + @Override + public BitSet next() { + BitSet helper = (BitSet) combination.clone(); + work(); + if (helper.equals(end)) { + combination.set(n); + end.set(n); + } + return helper; + } + + /** + * Change the representation of combination in such a way that the next valid + * combination is computed + */ + private void work() { + int toMove; + if (n > 0) { + if (!combination.get(n - 1)) { + toMove = combination.previousSetBit(n - 1); + if (toMove > -1) { + swap(toMove, toMove + 1); + } + } else { + toMove = getLeftOfFirstClearGroup(); + if (toMove > 0) { + swap(toMove, toMove - 1); + if (getLeftOfFirstClearGroup() > toMove) { + while (combination.get(n - 1)) { + swap(getLeftOfFirstSetGroup(), getLeftOfFirstClearGroup()); + } + } + } + } + } else { + combination.set(n); + end.set(n); + } + + } + + /** + * @return the index of the left most bit in the first set group from left to + * right. + */ + private int getLeftOfFirstSetGroup() { + return combination.previousClearBit(combination.previousSetBit(n - 1)) + 1; + } + + /** + * @return the index of the left most bit in the first clear group from left to + * right. + */ + private int getLeftOfFirstClearGroup() { + return combination.previousSetBit(combination.previousClearBit(n - 1)) + 1; + } + + /** + * Swap the values of indexes {@code i} and {@code j}. + * + * @param i index to be swapped + * @param j index to be swapped + */ + private void swap(int i, int j) { + boolean helper = combination.get(i); + combination.set(i, combination.get(j)); + combination.set(j, helper); + } +} diff --git a/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/math/powerset/SubSetIndexIterable.java b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/math/powerset/SubSetIndexIterable.java new file mode 100644 index 000000000..c9b053aa3 --- /dev/null +++ b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/math/powerset/SubSetIndexIterable.java @@ -0,0 +1,46 @@ +package org.semanticweb.rulewerk.math.powerset; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import java.util.Iterator; +import java.util.List; + +/** + * Given a set, iterate over all subsets in its power set, represented by a list + * of indexes, over an Iterable. + * + * @author Larry González + * + */ +public class SubSetIndexIterable implements Iterable> { + + SubSetIndexIterator iter; + + public SubSetIndexIterable(int n) { + iter = new SubSetIndexIterator(n); + } + + @Override + public Iterator> iterator() { + return iter; + } + +} diff --git a/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/math/powerset/SubSetIndexIterator.java b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/math/powerset/SubSetIndexIterator.java new file mode 100644 index 000000000..020c4bf0a --- /dev/null +++ b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/math/powerset/SubSetIndexIterator.java @@ -0,0 +1,72 @@ +package org.semanticweb.rulewerk.math.powerset; + +import java.util.ArrayList; +import java.util.BitSet; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import java.util.Iterator; +import java.util.List; + +import org.semanticweb.rulewerk.math.permutation.KOverNIterator; + +/** + * Given a set, iterate over all subsets in its power set, represented by a list + * of indexes, over an Iterator. + * + * @author Larry González + * + */ +public class SubSetIndexIterator implements Iterator> { + int n; + int i; + KOverNIterator iter; + + public SubSetIndexIterator(int n) { + this.n = n; + this.i = 0; + this.iter = new KOverNIterator(n, i); + } + + @Override + public boolean hasNext() { + return iter.hasNext() || i < n; + } + + @Override + public List next() { + if (!iter.hasNext()) { + i++; + iter = new KOverNIterator(n, i); + } + return getSubSet(iter.next()); + } + + private List getSubSet(BitSet bs) { + List subset = new ArrayList<>(); + for (int j = 0; j < n; j++) { + if (bs.get(j)) { + subset.add(j); + } + } + return subset; + } +} \ No newline at end of file diff --git a/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/math/powerset/SubSetIterable.java b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/math/powerset/SubSetIterable.java new file mode 100644 index 000000000..3fa8f0899 --- /dev/null +++ b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/math/powerset/SubSetIterable.java @@ -0,0 +1,46 @@ +package org.semanticweb.rulewerk.math.powerset; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import java.util.Iterator; +import java.util.List; + +/** + * Given a set, iterate over all subsets in its power set over an Iterable. + * + * @author Larry González + * + */ +public class SubSetIterable implements Iterable> { + + SubSetIterator subsetIterator; + + public SubSetIterable(List elements) { + subsetIterator = new SubSetIterator(elements); + + } + + @Override + public Iterator> iterator() { + return subsetIterator; + } + +} diff --git a/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/math/powerset/SubSetIterator.java b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/math/powerset/SubSetIterator.java new file mode 100644 index 000000000..4f539904a --- /dev/null +++ b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/math/powerset/SubSetIterator.java @@ -0,0 +1,55 @@ +package org.semanticweb.rulewerk.math.powerset; + +import java.util.ArrayList; +import java.util.Iterator; +import java.util.List; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +/** + * Given a set, iterate over all subsets in its power set over an Iterator. + * + * @author Larry González + * + */ +public class SubSetIterator implements Iterator> { + List elements; + SubSetIndexIterator iter; + + public SubSetIterator(List elements) { + this.elements = elements; + iter = new SubSetIndexIterator(elements.size()); + } + + @Override + public boolean hasNext() { + return iter.hasNext(); + } + + @Override + public List next() { + List subset = new ArrayList<>(); + for (int i : iter.next()) { + subset.add(elements.get(i)); + } + return subset; + } +} \ No newline at end of file diff --git a/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/reliances/Reliance.java b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/reliances/Reliance.java new file mode 100644 index 000000000..e2187a784 --- /dev/null +++ b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/reliances/Reliance.java @@ -0,0 +1,212 @@ +package org.semanticweb.rulewerk.reliances; + +import java.io.IOException; +import java.util.ArrayList; +import java.util.HashMap; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import java.util.List; +import java.util.Map; +import java.util.stream.Collectors; + +import org.apache.log4j.ConsoleAppender; +import org.apache.log4j.Level; +import org.apache.log4j.Logger; +import org.apache.log4j.PatternLayout; +import org.semanticweb.rulewerk.core.model.api.Fact; +import org.semanticweb.rulewerk.core.model.api.PositiveLiteral; +import org.semanticweb.rulewerk.core.model.api.Rule; +import org.semanticweb.rulewerk.logic.MartelliMontanariUnifier; +import org.semanticweb.rulewerk.logic.Substitute; +import org.semanticweb.rulewerk.logic.Unifier; +import org.semanticweb.rulewerk.parser.ParsingException; +import org.semanticweb.rulewerk.utils.BCQA; +import org.semanticweb.rulewerk.utils.LiteralList; +import org.semanticweb.rulewerk.utils.RuleUtil; +import org.semanticweb.rulewerk.utils.Transform; + +public class Reliance { + + final private static Logger logger = Logger.getLogger(Reliance.class); + + /** + * Defines how messages should be logged. This method can be modified to + * restrict the logging messages that are shown on the console or to change + * their formatting. See the documentation of Log4J for details on how to do + * this. + * + * Note: The VLog C++ backend performs its own logging. The log-level for this + * can be configured using + * {@link Reasoner#setLogLevel(org.semanticweb.rulewerk.core.reasoner.LogLevel)}. + * It is also possible to specify a separate log file for this part of the logs. + */ + public static void configureLogging() { + // Create the appender that will write log messages to the console. + final ConsoleAppender consoleAppender = new ConsoleAppender(); + // Define the pattern of log messages. + // Insert the string "%c{1}:%L" to also show class name and line. + final String pattern = "%d{yyyy-MM-dd HH:mm:ss} %-5p - %m%n"; + consoleAppender.setLayout(new PatternLayout(pattern)); + // Change to Level.ERROR for fewer messages: + consoleAppender.setThreshold(Level.DEBUG); + + consoleAppender.activateOptions(); + Logger.getRootLogger().addAppender(consoleAppender); + } + + /** + * Checker for positive reliance relation. + * + * @param rule1 + * @param rule2 + * @return True if rule2 positively relies on rule1. + * @throws IOException + * @throws ParsingException + */ + static public boolean positively(Rule first, Rule second) throws ParsingException, IOException { + configureLogging(); + if (RuleUtil.containsRepeatedAtoms(first)) { + logger.debug("RPOS: Illegal argument exception: Rule first contains duplicated atoms"); + throw new IllegalArgumentException("Rule first can not contain dupplicated atoms: " + first); + } + if (RuleUtil.containsRepeatedAtoms(second)) { + logger.debug("RPOS: Illegal argument exception: Rule second contains duplicated atoms"); + throw new IllegalArgumentException("Rule second can not contain dupplicated atoms: " + second); + } + if (!RuleUtil.isApplicable(first)) { + logger.debug("RPOS: Rule first is not applicable"); + return false; + } + if (!RuleUtil.isApplicable(second)) { + logger.debug("RPOS: Rule second is not applicable"); + return false; + } + logger.debug("RPOS: Rules are well written"); + + Rule rule1 = Transform.exi2null(RuleUtil.renameVariablesWithSufix(first, 1)); + Rule rule2 = Transform.exi2null(RuleUtil.renameVariablesWithSufix(second, 2)); + + logger.debug("RPOS: rule1: " + rule1); + logger.debug("RPOS: rule2: " + rule2); + + List varphi1 = rule1.getPositiveBodyLiterals().getLiterals(); + List psi1 = Transform.exi2null(rule1.getHead().getLiterals()).stream() + .map(e -> (PositiveLiteral) e).collect(Collectors.toList()); + List varphi2 = rule2.getPositiveBodyLiterals().getLiterals(); + List psi2 = Transform.exi2null(rule2.getHead().getLiterals()).stream() + .map(e -> (PositiveLiteral) e).collect(Collectors.toList()); + + return extend(varphi1, psi1, varphi2, psi2, new HashMap(), 0); + } + + private static boolean extend(List varphi1, List psi1, + List varphi2, List psi2, Map m, int idx) + throws ParsingException, IOException { + logger.debug("RPOS: starting extend with:\n\tvarphi1:\t" + varphi1 + "\n\tpsi1 :\t" + psi1 + "\n\tvarphi2:\t" + + varphi2 + "\n\tpsi2 :\t" + psi2 + "\n\tmapping:\t" + m + "\n\tindex :\t" + idx); + for (int i = idx; i < psi1.size(); i++) { + for (int j = 0; j < varphi2.size(); j++) { + if (varphi2.get(j).getPredicate().equals(psi1.get(i).getPredicate())) { + Map helper = new HashMap<>(m); + helper.put(psi1.get(i), varphi2.get(j)); + if (worker(varphi1, psi1, varphi2, psi2, helper, (idx + 1))) { + return true; + } + } + } + } + return false; // should this be in the previous line? + } + + private static boolean worker(List varphi1, List psi1, + List varphi2, List psi2, Map m, int idx) + throws ParsingException, IOException { + logger.debug("RPOS: starting worker with:\n\tvarphi1:\t" + varphi1 + "\n\tpsi1 :\t" + psi1 + "\n\tvarphi2:\t" + + varphi2 + "\n\tpsi2 :\t" + psi2 + "\n\tmapping:\t" + m + "\n\tindex :\t" + idx); + + Unifier sigma = new MartelliMontanariUnifier(m); + if (!sigma.isSuccessful()) { + logger.debug("RPOS: ending worker with false (not unifiable)"); + return false; + } + logger.debug("RPOS: sigma:\t" + sigma); + List varphi21 = new ArrayList<>(); + List varphi22 = new ArrayList<>(); + + m.forEach((key, value) -> varphi21.add(value)); + varphi2.forEach(e -> { + if (!varphi21.contains(e)) + varphi22.add(e); + }); + logger.debug("RPOS: varphi21:\t" + varphi21); + logger.debug("RPOS: varphi22:\t" + varphi22); + + List varphi1sigma = Substitute.positiveLiterals(sigma.getSubstitution(), varphi1); + List varphi22sigma = Substitute.positiveLiterals(sigma.getSubstitution(), varphi22); + if (!LiteralList.getExistentialVariables(varphi1sigma).isEmpty()) { + logger.debug("RPOS: ending worker with false (existentials in varphi1sigma)"); + return false; + } + if (!LiteralList.getExistentialVariables(varphi22sigma).isEmpty()) { + logger.debug("RPOS: recursive call to extend"); + return extend(varphi1, psi1, varphi2, psi2, m, (idx + 1)); + } + + List psi1sigmaforall = Transform + .intoPositiveLiterals(Transform.uni2cons(Substitute.positiveLiterals(sigma.getSubstitution(), psi1))); + List InstA = Transform.intoFacts(Transform.uni2cons(varphi1sigma)); + logger.debug("RPOS: Inst A:\t" + InstA); + + if (BCQA.query2(InstA, psi1sigmaforall)) { + System.out.println("extending"); + return extend(varphi1, psi1, varphi2, psi2, m, (idx + 1)); + } + + logger.debug("RPOS: HERE"); + logger.debug("RPOS: HERE: "+sigma.getSubstitution()); + logger.debug("RPOS: HERE: "+varphi2); + List varphi2sigmaforall = Transform + .intoFacts(Transform.uni2cons(Substitute.positiveLiterals(sigma.getSubstitution(), varphi2))); + logger.debug("RPOS: varphi2sigmaforall:\t" + varphi2sigmaforall); + logger.debug("RPOS: HERE2"); + if (BCQA.query1(InstA, varphi2sigmaforall)) { + logger.debug("RPOS: ending worker with false (InstA models varphi2sigmaforall)"); + return false; + } + + List InstB = new ArrayList<>(InstA); + InstB.addAll(Transform.intoFacts(psi1sigmaforall)); + logger.debug("RPOS: Inst B:\t" + InstB); + + List psi2sigmaforall = Transform + .intoPositiveLiterals(Transform.uni2cons(Substitute.positiveLiterals(sigma.getSubstitution(), psi2))); + logger.debug("RPOS: psi2sigmaforall:\t" + psi2sigmaforall); + + if (!BCQA.query2(InstB, psi2sigmaforall)) { + logger.debug("RPOS: ending worker with true"); + return true; + } + logger.debug("RPOS: ending worker with false (last case)"); + return false; + } + +} diff --git a/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/reliances/Restraint.java b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/reliances/Restraint.java new file mode 100644 index 000000000..3d36f7d58 --- /dev/null +++ b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/reliances/Restraint.java @@ -0,0 +1,236 @@ +package org.semanticweb.rulewerk.reliances; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.stream.Collectors; + +import org.semanticweb.rulewerk.core.model.api.ExistentialVariable; +import org.semanticweb.rulewerk.core.model.api.Literal; +import org.semanticweb.rulewerk.core.model.api.PositiveLiteral; +import org.semanticweb.rulewerk.core.model.api.Rule; +import org.semanticweb.rulewerk.core.model.api.Term; +import org.semanticweb.rulewerk.core.model.api.TermType; +import org.semanticweb.rulewerk.math.mapping.Pair; +import org.semanticweb.rulewerk.math.mapping.PartialMappingIdx; +import org.semanticweb.rulewerk.math.mapping.PartialMappingIterable; +import org.semanticweb.rulewerk.math.powerset.SubSetIterable; +import org.semanticweb.rulewerk.utils.Filter; +import org.semanticweb.rulewerk.utils.LiteralList; +import org.semanticweb.rulewerk.utils.RuleUtil; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +public class Restraint { + + /** + * + * @return true if an universal variable occurring in a literal in head21 is + * being mapped into an existential variable occurring in its mapped + * literal from head11, which makes the alternative match invalid. + */ + static private boolean mappingUniversalintoExistential(List headAtomsRule2, + List headAtomsRule1, PartialMappingIdx assignment) { + + for (Pair match : assignment.getImages()) { + List fromHead2 = headAtomsRule2.get(match.getX()).getArguments(); + List fromHead1 = headAtomsRule1.get(match.getY()).getArguments(); + + for (int i = 0; i < fromHead2.size(); i++) { + if (fromHead2.get(i).getType() == TermType.UNIVERSAL_VARIABLE + && fromHead1.get(i).getType() == TermType.EXISTENTIAL_VARIABLE) { + return true; + } + } + } + return false; + } + + /** + * If we map an extVar (occurring in a literal in head21) into another extVar + * (occurring in a literal in head11), that first extVar can not occur in + * head22. If it occurs in head22, we don't have an alternative match because we + * can not drop all occurrences of the extVar, nor instantiate it with a + * constant. + * + * @param headAtomsRule2 rule2.head (renamed, unified, and renamed again) + * @param headAtomsRule1 rule1.head (renamed, unified, and renamed again) + * @param headAtoms22 atoms from rule2.head that were not unified, but + * renamed + * @param assignment see {@code Assignment} + * @return true if the alternative match is still a valid candidate + */ + static private boolean mapExt2ExtOrExt2Uni(List headAtomsRule2, List headAtomsRule1, + List headAtoms22, PartialMappingIdx assignment) { + Set extVarsIn22 = LiteralList.getExistentialVariables(headAtoms22); + for (Pair match : assignment.getImages()) { + List origin = headAtomsRule2.get(match.getX()).getArguments(); + List destination = headAtomsRule1.get(match.getY()).getArguments(); + + for (int i = 0; i < origin.size(); i++) { + if (origin.get(i).getType() == TermType.EXISTENTIAL_VARIABLE + && destination.get(i).getType() == TermType.EXISTENTIAL_VARIABLE + && extVarsIn22.contains(origin.get(i))) { + return false; + } + } + } + return true; + } + + /** + * Check that the existentially quantified variables occurring in mapping + * literals from head2 are mapped to the same. Consider the following atoms + * p(a,b), and p(!X,!X). We can not unify it. This is a shortcoming of the + * application of Martelli & Montanari unification algorithm to our case, + * specially when we unify existential variables. + * + * If its value is false, then the alternative match is not valid anymore. + * + * @note we are not renaming the existentially quantified variables in the rules + * + * @param headRule2 rule2.head (renamed, unified, and renamed again) + * @param headRule1 rule1.head (renamed, unified, and renamed again) + * @param assignment see {@code Assignment} + * @return true if the alternative match is still a valid candidate + */ + static private boolean mapExistentialsToTheSame(List headRule2, List headRule1, + PartialMappingIdx assignment) { + Map map = new HashMap<>(); + for (Pair match : assignment.getImages()) { + List origin = headRule2.get(match.getX()).getArguments(); + List destination = headRule1.get(match.getY()).getArguments(); + for (int i = 0; i < origin.size(); i++) { + if (origin.get(i).getType() == TermType.EXISTENTIAL_VARIABLE) { + if (map.containsKey(origin.get(i))) { + if (!map.get(origin.get(i)).equals(destination.get(i))) { + return false; + } + } else { + map.put((ExistentialVariable) origin.get(i), destination.get(i)); + } + } + } + } + return true; + } + + /** + * Checker for restraining relation. + * + * @param rule1 + * @param rule2 + * @return True if rule1 restraints rule2. + */ + static public boolean restraint(Rule rule1, Rule rule2) { + // if rule2 is Datalog, it can not be restrained + if (rule2.getExistentialVariables().count() == 0) { + return false; + } + + if (!RuleUtil.isRuleApplicable(rule1)) { + return false; + } + + if (!RuleUtil.isRuleApplicable(rule2)) { + return false; + } + + if (rule1.equals(rule2)) { + return SelfRestraint.restraint(rule1); + } + + Rule renamedRule1 = SuffixBasedVariableRenamer.rename(rule1, rule2.hashCode() + 1); + Rule renamedRule2 = SuffixBasedVariableRenamer.rename(rule2, rule1.hashCode() + 2); + + List headAtomsRule1 = renamedRule1.getHead().getLiterals(); + List headAtomsRule2 = renamedRule2.getHead().getLiterals(); + + List existentialVariables = renamedRule2.getExistentialVariables() + .collect(Collectors.toList()); + + // to avoid duplicate computation + Set testedAssignment = new HashSet<>(); + + // Iterate over all subsets of existentialVariables + for (List extVarComb : new SubSetIterable(existentialVariables)) { + + if (extVarComb.size() > 0) { + List literalsContainingExtVarsIdxs = LiteralList + .idxOfLiteralsContainingExistentialVariables(headAtomsRule2, extVarComb); + // Iterate over all subsets of literalsContainingExtVarsIdxs. Because it could + // be that we need to match only one of the literals + for (List literaltoUnifyIdx : new SubSetIterable(literalsContainingExtVarsIdxs)) { + + if (literaltoUnifyIdx.size() > 0) { + PartialMappingIterable assignmentIterable = new PartialMappingIterable(literaltoUnifyIdx.size(), + headAtomsRule1.size()); + // Iterate over all possible assignments of those Literals + for (PartialMappingIdx assignment : assignmentIterable) { + + // We transform the assignment to keep the old indexes + PartialMappingIdx transformed = new PartialMappingIdx(assignment, literaltoUnifyIdx, + headAtomsRule2.size()); + + if (!testedAssignment.contains(transformed)) { + testedAssignment.add(transformed); + + List headAtoms22Idx = transformed.inactiveDomain(); + MartelliMontanariUnifier unifier = new MartelliMontanariUnifier(headAtomsRule2, + headAtomsRule1, transformed); + if (unifier.getSuccess()) { + UnifierBasedVariableRenamer renamer = new UnifierBasedVariableRenamer(unifier, + false); + // rename universal variables (RWU = renamed with unifier) + Rule rule1RWU = renamer.rename(renamedRule1); + Rule rule2RWU = renamer.rename(renamedRule2); + + List headAtomsRule1RWU = new ArrayList<>(); + headAtomsRule1.forEach(literal -> headAtomsRule1RWU.add(renamer.rename(literal))); + + List headAtomsRule2RWU = new ArrayList<>(); + headAtomsRule2.forEach(literal -> headAtomsRule2RWU.add(renamer.rename(literal))); + + List headAtoms22 = Filter.indexBased(headAtomsRule2RWU, headAtoms22Idx); + + if (RuleUtil.isRule1Applicable(rule1RWU, rule2RWU) + && !mappingUniversalintoExistential(headAtomsRule2, headAtomsRule1, + transformed) + && mapExt2ExtOrExt2Uni(headAtomsRule2RWU, headAtomsRule1RWU, headAtoms22, + transformed) + && mapExistentialsToTheSame(headAtomsRule2RWU, headAtomsRule1RWU, + transformed)) { + return true; + } + } + } + } + } + } + } + } + return false; + } + +} diff --git a/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/reliances/SelfRestraint.java b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/reliances/SelfRestraint.java new file mode 100644 index 000000000..b438d0120 --- /dev/null +++ b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/reliances/SelfRestraint.java @@ -0,0 +1,103 @@ +package org.semanticweb.rulewerk.reliances; + +import java.util.List; +import java.util.Map; + +import org.semanticweb.rulewerk.core.model.api.Conjunction; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import org.semanticweb.rulewerk.core.model.api.PositiveLiteral; +import org.semanticweb.rulewerk.core.model.api.Predicate; +import org.semanticweb.rulewerk.core.model.api.Rule; +import org.semanticweb.rulewerk.core.model.implementation.Expressions; +import org.semanticweb.rulewerk.core.model.implementation.RuleImpl; +import org.semanticweb.rulewerk.math.powerset.SubSetIterable; +import org.semanticweb.rulewerk.utils.Filter; +import org.semanticweb.rulewerk.utils.LiteralList; +import org.semanticweb.rulewerk.utils.RuleUtil; + +public class SelfRestraint { + + /** + * + * @param rule + * @return True if the rule restraints itself. + */ + static public boolean restraint(Rule rule) { + // if rule2 is Datalog, it can not be restrained + if (rule.getExistentialVariables().count() == 0) { + return false; + } + + if (!RuleUtil.isRuleApplicable(rule)) { + return false; + } + + if (rule.containsUnconnectedPieces()) { + return true; + } + + Rule renamedRule = SuffixBasedVariableRenamer.rename(rule, rule.hashCode() + 1); + if (Restraint.restraint(rule, renamedRule)) { + return true; + } + + List headAtoms = rule.getHead().getLiterals(); + int headSize = headAtoms.size(); + + Map> predToLiterals = LiteralList.getPredicate2Literals(headAtoms); + + for (Predicate pred : predToLiterals.keySet()) { + + List positions = predToLiterals.get(pred); + + List rest = Filter.complement(positions, headSize); + + if (positions.size() > 0) { + SubSetIterable subsetIterable = new SubSetIterable<>(positions); + + for (List subset : subsetIterable) { + List complement = Filter.complement(positions, subset); + + if (subset.size() > 0 && complement.size() > 0) { + List head1Idx = Filter.join(rest, subset); + List head2Idx = Filter.join(rest, complement); + + List headAtoms1 = Filter.indexBased(headAtoms, head1Idx); + List headAtoms2 = Filter.indexBased(headAtoms, head2Idx); + + Conjunction head1 = Expressions.makeConjunction(headAtoms1); + Conjunction head2 = Expressions.makeConjunction(headAtoms2); + + Rule rule1 = new RuleImpl(head1, rule.getBody()); + Rule rule2 = new RuleImpl(head2, rule.getBody()); + + if (Restraint.restraint(rule1, rule2)) { + return true; + } + } + } + } + } + return false; + } +} diff --git a/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/utils/BCQA.java b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/utils/BCQA.java new file mode 100644 index 000000000..474dccf84 --- /dev/null +++ b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/utils/BCQA.java @@ -0,0 +1,54 @@ +package org.semanticweb.rulewerk.utils; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import java.util.List; + +import org.apache.commons.lang3.Validate; +import org.semanticweb.rulewerk.core.model.api.Literal; +import org.semanticweb.rulewerk.logic.MartelliMontanariUnifier; +import org.semanticweb.rulewerk.math.mapping.PartialMapping; +import org.semanticweb.rulewerk.math.mapping.PartialMappingIterable; + +/** + * A class to implement a (very simple) boolean conjunctive query. + * + * @author Larry González + */ +public class BCQ { + + // TODO explore other unifiers. + static boolean query(List instance, List query) { + Validate.isTrue(LiteralList.getVariables(instance).isEmpty()); + + for (PartialMapping partialMapping : new PartialMappingIterable(query.size(), instance.size())) { + + if (!partialMapping.isEmpty() && partialMapping.getDomineSize() == query.size()) { + MartelliMontanariUnifier unifier = new MartelliMontanariUnifier(query, instance, partialMapping); + + if (unifier.getSuccess()) { + return true; + } + } + } + return false; + } +} diff --git a/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/utils/Filter.java b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/utils/Filter.java new file mode 100644 index 000000000..1e1fb535a --- /dev/null +++ b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/utils/Filter.java @@ -0,0 +1,76 @@ +package org.semanticweb.rulewerk.utils; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import java.util.ArrayList; +import java.util.List; +import java.util.stream.Collectors; + +public class Filter { + static public List combinationBased(List original, int[] combination) { + List result = new ArrayList<>(); + for (int i = 0; i < combination.length; i++) { + if (combination[i] == 1) { + result.add(original.get(i)); + } + } + return result; + } + + static public List indexBased(List original, List positions) { + List result = new ArrayList<>(); + for (int index : positions) { + result.add(original.get(index)); + } + return result; + } + + static public List complement(List indexes, int length) { + List result = new ArrayList<>(); + for (int i = 0; i < length; i++) { + if (!indexes.contains(i)) { + result.add(i); + } + } + return result; + } + + static public List complement(List set, List subset) { + + List result = new ArrayList<>(); + for (int element : set) { + if (!subset.contains(element)) { + result.add(element); + } + } + return result; + } + + static public List join(List first, List second) { + + List result = new ArrayList<>(); + result.addAll(first); + result.addAll(second); + + List sorted = result.stream().sorted().collect(Collectors.toList()); + return sorted; + } +} diff --git a/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/utils/LiteralList.java b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/utils/LiteralList.java new file mode 100644 index 000000000..2d13a8a49 --- /dev/null +++ b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/utils/LiteralList.java @@ -0,0 +1,112 @@ +package org.semanticweb.rulewerk.utils; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.stream.Collectors; + +import org.semanticweb.rulewerk.core.model.api.ExistentialVariable; +import org.semanticweb.rulewerk.core.model.api.Literal; +import org.semanticweb.rulewerk.core.model.api.PositiveLiteral; +import org.semanticweb.rulewerk.core.model.api.Predicate; +import org.semanticweb.rulewerk.core.model.api.UniversalVariable; +import org.semanticweb.rulewerk.core.model.api.Variable; + +public class LiteralList { + + static public List getExistentialVariables(List literals) { + List result = new ArrayList<>(); + literals.forEach(lit -> result.addAll(((Literal) lit).getExistentialVariables().collect(Collectors.toList()))); + return result; + } + + static public List getUniversalVariables(List literals) { + List result = new ArrayList<>(); + literals.forEach(literal -> result.addAll(literal.getUniversalVariables().collect(Collectors.toList()))); + return result; + } + + static public List getVariables(List literals) { + List result = new ArrayList<>(); + literals.forEach(literal -> result.addAll(literal.getVariables().collect(Collectors.toList()))); + return result; + } + + @Deprecated + static public List filterLiteralsByExistentialVariables(List literals, + List existentialVariables) { + List result = new ArrayList<>(); + + for (PositiveLiteral literal : literals) { + for (ExistentialVariable extVar : existentialVariables) { + if (((Literal) literal).getExistentialVariables() + .anyMatch(containedVar -> containedVar.equals(extVar))) { + result.add(literal); + break; + } + } + } + return result; + } + + @Deprecated + static public List idxOfLiteralsContainingExistentialVariables(List literals, + List existentialVariables) { + List result = new ArrayList<>(); + + for (int i = 0; i < literals.size(); i++) { + for (ExistentialVariable extVar : existentialVariables) { + if (literals.get(i).getExistentialVariables().anyMatch(containedVar -> containedVar.equals(extVar))) { + result.add(i); + break; + } + } + } + return result; + } + + /** + * Returns a map from predicate to literals having that predicate. + * + * @param literals List of literals + * @return map {predicate -> [literals]} + */ + @Deprecated + static public Map> getPredicate2Literals(List literals) { + Map> result = new HashMap<>(); + + for (int i = 0; i < literals.size(); i++) { + Predicate pred = literals.get(i).getPredicate(); + if (result.containsKey(pred)) { + result.get(pred).add(i); + } else { + List helper = new ArrayList<>(); + helper.add(i); + result.put(pred, helper); + } + } + return result; + } + +} diff --git a/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/utils/RuleUtil.java b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/utils/RuleUtil.java new file mode 100644 index 000000000..2a9b83e64 --- /dev/null +++ b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/utils/RuleUtil.java @@ -0,0 +1,88 @@ +package org.semanticweb.rulewerk.utils; + +import java.io.IOException; +import java.util.HashSet; +import java.util.List; +import java.util.Set; + +import org.semanticweb.rulewerk.core.model.api.Fact; +import org.semanticweb.rulewerk.core.model.api.Literal; +import org.semanticweb.rulewerk.core.model.api.PositiveLiteral; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import org.semanticweb.rulewerk.core.model.api.Rule; +import org.semanticweb.rulewerk.core.model.implementation.Expressions; +import org.semanticweb.rulewerk.logic.Substitution; +import org.semanticweb.rulewerk.parser.ParsingException; +import org.semanticweb.rulewerk.logic.Substitute; + +public class RuleUtil { + + static public boolean isApplicable(Rule rule) throws ParsingException, IOException { + List instance = Transform.intoFacts(Transform.uni2cons(rule.getPositiveBodyLiterals().getLiterals())); + List query = Transform + .intoPositiveLiterals(Transform.exi2uni(Transform.uni2cons(rule.getHead().getLiterals()))); + return !BCQA.query2(instance, query); + } + + /* + * True if a rule contains any repeated literal + * + * TODO This should be in RuleImpl and/or RuleParser. + */ + static public boolean containsRepeatedAtoms(Rule rule) { + Set literals = new HashSet<>(); + + for (Literal l : rule.getBody().getLiterals()) { + if (literals.contains(l)) { + return true; + } else { + literals.add(l); + } + } + + for (Literal l : rule.getHead().getLiterals()) { + if (literals.contains(l)) { + return true; + } else { + literals.add(l); + } + } + return false; + } + + /* + * Append a suffix to every variable name. The suffix is a dash and the hashCode + * of the Rule. + */ + static public Rule renameVariablesWithSufix(Rule rule, int n) { + String suffix = "-" + n; + Substitution s = new Substitution(); + rule.getVariables().forEach(var -> { + String newName = var.getName() + suffix; + s.add(var, var.isExistentialVariable() ? Expressions.makeExistentialVariable(newName) + : Expressions.makeUniversalVariable(newName)); + }); + return Substitute.rule(s, rule); + } + +} diff --git a/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/utils/Transform.java b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/utils/Transform.java new file mode 100644 index 000000000..5db79f7f2 --- /dev/null +++ b/rulewerk-reliances/src/main/java/org/semanticweb/rulewerk/utils/Transform.java @@ -0,0 +1,207 @@ +package org.semanticweb.rulewerk.utils; + +import java.util.List; +import java.util.stream.Collectors; + +import org.apache.commons.lang3.Validate; +import org.semanticweb.rulewerk.core.model.api.Fact; +import org.semanticweb.rulewerk.core.model.api.Literal; +import org.semanticweb.rulewerk.core.model.api.PositiveLiteral; +import org.semanticweb.rulewerk.core.model.api.Predicate; +import org.semanticweb.rulewerk.core.model.api.Rule; +import org.semanticweb.rulewerk.core.model.api.Term; +import org.semanticweb.rulewerk.core.model.implementation.ConjunctionImpl; +import org.semanticweb.rulewerk.core.model.implementation.ExistentialVariableImpl; +import org.semanticweb.rulewerk.core.model.implementation.Expressions; +import org.semanticweb.rulewerk.core.model.implementation.NamedNullImpl; +import org.semanticweb.rulewerk.core.model.implementation.NegativeLiteralImpl; +import org.semanticweb.rulewerk.core.model.implementation.PositiveLiteralImpl; +import org.semanticweb.rulewerk.core.model.implementation.UniversalVariableImpl; + +public class Transform { + + /* + * Return an named null when the term is an existentially quantified variable + */ + static public Term exi2null(Term term) { + return term.isExistentialVariable() ? new NamedNullImpl(term.getName()) : term; + } + + /* + * Replace existentially quantified variables with named nulls having the same + * name in a literal + */ + static public Literal exi2null(Literal literal) { + Predicate p = literal.getPredicate(); + List terms = literal.getArguments().stream().map(t -> exi2null(t)).collect(Collectors.toList()); + return literal.isNegated() ? new NegativeLiteralImpl(p, terms) : new PositiveLiteralImpl(p, terms); + } + + /* + * Replace existentially quantified variables with named nulls having the same + * name in a list of literal + */ + static public List exi2null(List literals) { + return literals.stream().map(l -> exi2null(l)).collect(Collectors.toList()); + } + + /* + * Replace existentially quantified variables with named nulls having the same + * name as the existentially quantified variable in a rule + */ + static public Rule exi2null(Rule rule) { + return Expressions.makeRule( + new ConjunctionImpl<>(Transform.intoPositiveLiterals(Transform.exi2null(rule.getHead().getLiterals()))), + new ConjunctionImpl<>(Transform.exi2null(rule.getBody().getLiterals()))); + } + + /* + * If {@code term} is a named null, then it returns an existentially quantified + * variable having the same name. It returns {@code term} in the contrary case + */ + static public Term null2exi(Term term) { + return term.isNull() ? new ExistentialVariableImpl(term.getName()) : term; + } + + /* + * Replace named nulls with existentially quantified variables having the same + * name in a literal + */ + static public Literal null2exi(Literal literal) { + Predicate p = literal.getPredicate(); + List terms = literal.getArguments().stream().map(t -> null2exi(t)).collect(Collectors.toList()); + return literal.isNegated() ? new NegativeLiteralImpl(p, terms) : new PositiveLiteralImpl(p, terms); + } + + /* + * Replace named nulls with existentially quantified variables having the same + * name in a list of literals + */ + static public List null2exi(List literals) { + return literals.stream().map(l -> null2exi(l)).collect(Collectors.toList()); + } + + /* + * If {@code term} is a named null, then it returns aconstant having the same + * name. It returns {@code term} in the contrary case + */ + static public Term null2cons(Term term) { + return term.isNull() ? Expressions.makeAbstractConstant(term.getName()) : term; + } + + /* + * Replace named nulls with constants having the same name in a literal + */ + static public Literal null2cons(Literal literal) { + Predicate p = literal.getPredicate(); + List terms = literal.getArguments().stream().map(t -> null2cons(t)).collect(Collectors.toList()); + return literal.isNegated() ? new NegativeLiteralImpl(p, terms) : new PositiveLiteralImpl(p, terms); + } + + /* + * Replace named nulls with constants having the same name in a list of literals + */ + static public List null2cons(List literals) { + return literals.stream().map(l -> null2cons(l)).collect(Collectors.toList()); + } + + /* + * Return an universally quantified variables when the term is a constant + */ + static public Term uni2cons(Term term) { + return term.isUniversalVariable() ? Expressions.makeAbstractConstant(term.getName()) : term; + } + + /* + * Replace universally quantified variables with constants having the same name + * in a literal + */ + static public Literal uni2cons(Literal literal) { + Predicate p = literal.getPredicate(); + List terms = literal.getArguments().stream().map(t -> uni2cons(t)).collect(Collectors.toList()); + return literal.isNegated() ? new NegativeLiteralImpl(p, terms) : new PositiveLiteralImpl(p, terms); + } + + /* + * Replace universally quantified variables with constants having the same name + * in a list of literals + */ + static public List uni2cons(List literals) { + return literals.stream().map(l -> uni2cons(l)).collect(Collectors.toList()); + } + + /* + * If {@code term} is a named null, then it returns an universally quantified + * variable having the same name. It returns {@code term} in the contrart case + */ + static public Term null2uni(Term term) { + return term.isNull() ? new UniversalVariableImpl(term.getName()) : term; + } + + /* + * Replace named nulls with universally quantified variables having the same + * name in a literal + */ + static public Literal null2uni(Literal literal) { + Predicate p = literal.getPredicate(); + List terms = literal.getArguments().stream().map(t -> null2uni(t)).collect(Collectors.toList()); + return literal.isNegated() ? new NegativeLiteralImpl(p, terms) : new PositiveLiteralImpl(p, terms); + } + + /* + * Replace named nulls with universally quantified variables having the same + * name in a list of literals + */ + static public List null2uni(List literals) { + return literals.stream().map(l -> null2uni(l)).collect(Collectors.toList()); + } + + /* + * If {@code term} is an existentially quantified variable, then returns an + * universally quantified variable having the same name. It returns {@code term} + * in the contrary case + */ + static public Term exi2uni(Term term) { + return term.isExistentialVariable() ? new UniversalVariableImpl(term.getName()) : term; + } + + /* + * Replace existentially quantified variables with universally quantified + * variables having the same name in a literal + */ + static public Literal exi2uni(Literal literal) { + Predicate p = literal.getPredicate(); + List terms = literal.getArguments().stream().map(t -> exi2uni(t)).collect(Collectors.toList()); + return literal.isNegated() ? new NegativeLiteralImpl(p, terms) : new PositiveLiteralImpl(p, terms); + } + + /* + * Replace existentially quantified variables with universally quantified + * variables having the same name in a list of literals + */ + static public List exi2uni(List literals) { + return literals.stream().map(l -> exi2uni(l)).collect(Collectors.toList()); + } + + /* + * @param literals list of (positive) literals that don't contains existentially + * quantified variables + */ + static public Fact intoFact(Literal literal) { + Validate.isTrue(!literal.isNegated()); + return Expressions.makeFact(literal.getPredicate(), + literal.getArguments().stream().map(t -> uni2cons(t)).collect(Collectors.toList())); + } + + /* + * Transform a list of PositiveLiterals into a list of Facts + */ + static public List intoFacts(List literals) { + return literals.stream().map(l -> intoFact(l)).collect(Collectors.toList()); + } + + static public List intoPositiveLiterals(List literals) { + return literals.stream().map(l -> (PositiveLiteral) l).collect(Collectors.toList()); + } + +} diff --git a/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/logic/MartelliMontanariUnifierTest.java b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/logic/MartelliMontanariUnifierTest.java new file mode 100644 index 000000000..ebcac87d0 --- /dev/null +++ b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/logic/MartelliMontanariUnifierTest.java @@ -0,0 +1,138 @@ +package org.semanticweb.rulewerk.logic; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import static org.junit.Assert.assertTrue; +import static org.junit.Assert.assertFalse; + +import java.util.HashMap; +import java.util.Map; + +import org.junit.Test; +import org.semanticweb.rulewerk.core.model.api.Literal; +import org.semanticweb.rulewerk.parser.RuleParser; + +public class MartelliMontanariUnifierTest { + + Map m = new HashMap<>(); + MartelliMontanariUnifier unifier; + + @Test(expected = IllegalArgumentException.class) + public void test01() throws Exception { + m.clear(); + m.put(RuleParser.parseLiteral("q(?X1,?X1)"), RuleParser.parseLiteral("q(!X2,!X2)")); + + unifier = new MartelliMontanariUnifier(m); + assertTrue(unifier.isSuccessful()); + } + + @Test + public void test02() throws Exception { + m.clear(); + m.put(RuleParser.parseLiteral("q(?X1,?X1)"), RuleParser.parseLiteral("q(?X2,c)")); + + unifier = new MartelliMontanariUnifier(m); + assertTrue(unifier.isSuccessful()); + } + + @Test(expected = IllegalArgumentException.class) + public void test03() throws Exception { + m.clear(); + m.put(RuleParser.parseLiteral("r(?X10001, !Y10001, !Z10001)"), + RuleParser.parseLiteral("r(c, ?X20002, ?Y20002)")); + + unifier = new MartelliMontanariUnifier(m); + assertTrue(unifier.isSuccessful()); + } + + @Test + public void test04() throws Exception { + m.clear(); + m.put(RuleParser.parseLiteral("p(?X)"), RuleParser.parseLiteral("q(?X)")); + + unifier = new MartelliMontanariUnifier(m); + assertFalse(unifier.isSuccessful()); + } + + @Test + public void test05() throws Exception { + m.clear(); + m.put(RuleParser.parseLiteral("p(?Y,?X)"), RuleParser.parseLiteral("p(?X,?Y)")); + + unifier = new MartelliMontanariUnifier(m); + assertTrue(unifier.isSuccessful()); + } + + @Test(expected = IllegalArgumentException.class) + public void test06() throws Exception { + m.clear(); + m.put(RuleParser.parseLiteral("p(!Y,!X)"), RuleParser.parseLiteral("p(!X,!Y)")); + + unifier = new MartelliMontanariUnifier(m); + assertTrue(unifier.isSuccessful()); + } + + @Test + public void test07() throws Exception { + m.clear(); + m.put(RuleParser.parseLiteral("p(?x1,?x1,?x1)"), RuleParser.parseLiteral("p(?x2,c1,c2)")); + + unifier = new MartelliMontanariUnifier(m); + assertFalse(unifier.isSuccessful()); + } + + @Test + public void test08() throws Exception { + m.clear(); + m.put(RuleParser.parseLiteral("p(c)"), RuleParser.parseLiteral("p(c)")); + + unifier = new MartelliMontanariUnifier(m); + assertTrue(unifier.isSuccessful()); + } + + @Test + public void test09() throws Exception { + m.clear(); + m.put(RuleParser.parseLiteral("p(c)"), RuleParser.parseLiteral("p(d)")); + + unifier = new MartelliMontanariUnifier(m); + assertFalse(unifier.isSuccessful()); + } + + @Test + public void test10() throws Exception { + m.clear(); + m.put(RuleParser.parseLiteral("p(?Y,?X)"), RuleParser.parseLiteral("p(?X,?Y)")); + + unifier = new MartelliMontanariUnifier(m); + assertTrue(unifier.isSuccessful()); + } + + @Test + public void test11() throws Exception { + m.clear(); + m.put(RuleParser.parseLiteral("r(?X1, ?Y1, ?Z1)"), + RuleParser.parseLiteral("r(c, ?X2, ?Y2)")); + + unifier = new MartelliMontanariUnifier(m); + assertTrue(unifier.isSuccessful()); + } +} diff --git a/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/logic/SubstituteTest.java b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/logic/SubstituteTest.java new file mode 100644 index 000000000..28c32e4b4 --- /dev/null +++ b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/logic/SubstituteTest.java @@ -0,0 +1,6 @@ +package org.semanticweb.rulewerk.logic; + +// TODO +public class SubstitutionTest { + +} diff --git a/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/mapping/PairTest.java b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/mapping/PairTest.java new file mode 100644 index 000000000..cbb42a743 --- /dev/null +++ b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/mapping/PairTest.java @@ -0,0 +1,25 @@ +package org.semanticweb.rulewerk.math.mapping; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2021 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +public class PairTest { + // TODO +} diff --git a/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/mapping/PartialMappingIdxTest.java b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/mapping/PartialMappingIdxTest.java new file mode 100644 index 000000000..b4a9ef58a --- /dev/null +++ b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/mapping/PartialMappingIdxTest.java @@ -0,0 +1,25 @@ +package org.semanticweb.rulewerk.math.mapping; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2021 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +public class PartialMappingIdxTest { + // TODO +} diff --git a/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/permutation/KOverNIterableTest.java b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/permutation/KOverNIterableTest.java new file mode 100644 index 000000000..ed93c0829 --- /dev/null +++ b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/permutation/KOverNIterableTest.java @@ -0,0 +1,25 @@ +package org.semanticweb.rulewerk.math.permutation; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2021 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +public class KOverNIterableTest { + // TODO +} diff --git a/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/permutation/KOverNIteratorTest.java b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/permutation/KOverNIteratorTest.java new file mode 100644 index 000000000..fff91f8aa --- /dev/null +++ b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/permutation/KOverNIteratorTest.java @@ -0,0 +1,25 @@ +package org.semanticweb.rulewerk.math.permutation; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2021 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +public class KOverNIteratorTest { + // TODO +} diff --git a/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/powerset/SubSetIndexIterableTest.java b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/powerset/SubSetIndexIterableTest.java new file mode 100644 index 000000000..a22e64336 --- /dev/null +++ b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/powerset/SubSetIndexIterableTest.java @@ -0,0 +1,25 @@ +package org.semanticweb.rulewerk.math.powerset; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2021 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +public class SubSetIndexIterableTest { + // TODO +} diff --git a/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/powerset/SubSetIndexIteratorTest.java b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/powerset/SubSetIndexIteratorTest.java new file mode 100644 index 000000000..8731a6e6d --- /dev/null +++ b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/powerset/SubSetIndexIteratorTest.java @@ -0,0 +1,25 @@ +package org.semanticweb.rulewerk.math.powerset; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2021 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +public class SubSetIndexIteratorTest { + // TODO +} diff --git a/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/powerset/SubSetIterableTest.java b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/powerset/SubSetIterableTest.java new file mode 100644 index 000000000..297eea500 --- /dev/null +++ b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/powerset/SubSetIterableTest.java @@ -0,0 +1,25 @@ +package org.semanticweb.rulewerk.math.powerset; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2021 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +public class SubSetIterableTest { + // TODO +} diff --git a/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/powerset/SubSetIteratorTest.java b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/powerset/SubSetIteratorTest.java new file mode 100644 index 000000000..9b5b8e234 --- /dev/null +++ b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/math/powerset/SubSetIteratorTest.java @@ -0,0 +1,25 @@ +package org.semanticweb.rulewerk.math.powerset; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2021 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +public class SubSetIteratorTest { + // TODO +} diff --git a/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/reliances/RelianceTest.java b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/reliances/RelianceTest.java new file mode 100644 index 000000000..dbf5d1596 --- /dev/null +++ b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/reliances/RelianceTest.java @@ -0,0 +1,356 @@ +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +package org.semanticweb.rulewerk.reliances; + +import static org.junit.Assert.assertFalse; +import static org.junit.Assert.assertTrue; + +import org.junit.Test; +import org.semanticweb.rulewerk.core.model.api.Rule; +import org.semanticweb.rulewerk.parser.RuleParser; + +public class RelianceTest { + + @Test + public void noMatchingAtomsTest() throws Exception { + Rule px_qx = RuleParser.parseRule("q(?X) :- p(?X) ."); + + assertFalse(Reliance.positively(px_qx, px_qx)); + } + + @Test + public void chainUni2UniTest() throws Exception { + Rule px_qx = RuleParser.parseRule("q(?X) :- p(?X) ."); + Rule qx_rx = RuleParser.parseRule("r(?X) :- q(?X) ."); + + assertTrue(Reliance.positively(px_qx, qx_rx)); + } + + @Test + public void chainUni2ExiTest() throws Exception { + Rule px_qy = RuleParser.parseRule("q(!Y) :- p(?X) ."); + Rule qx_rx = RuleParser.parseRule("r(?X) :- q(?X) ."); + + assertTrue(Reliance.positively(px_qy, qx_rx)); + } + + @Test + public void chainUni2ConTest() throws Exception { + Rule px_qc = RuleParser.parseRule("q(c) :- p(?X) ."); + Rule qx_rx = RuleParser.parseRule("r(?X) :- q(?X) ."); + + assertTrue(Reliance.positively(px_qc, qx_rx)); + } + + @Test + public void chainCon2UniTest() throws Exception { + Rule px_qx = RuleParser.parseRule("q(?X) :- p(?X) ."); + Rule qc_rx = RuleParser.parseRule("r(!X) :- q(c) ."); + + assertTrue(Reliance.positively(px_qx, qc_rx)); + } + + @Test + public void chainCon2ExiTest() throws Exception { + Rule px_qy = RuleParser.parseRule("q(!Y) :- p(?X) ."); + Rule qc_rx = RuleParser.parseRule("r(!X) :- q(c) ."); + + assertFalse(Reliance.positively(px_qy, qc_rx)); + } + + @Test + public void chainCon2ConTest() throws Exception { + Rule px_qc = RuleParser.parseRule("q(c) :- p(?X) ."); + Rule qc_rx = RuleParser.parseRule("r(!X) :- q(c) ."); + Rule qd_rx = RuleParser.parseRule("r(!X) :- q(d) ."); + + assertTrue(Reliance.positively(px_qc, qc_rx)); + assertFalse(Reliance.positively(px_qc, qd_rx)); + } + + @Test + public void cyclicUni2UniTest() throws Exception { + Rule px_qx = RuleParser.parseRule("q(?X) :- p(?X) ."); + Rule qx_px = RuleParser.parseRule("p(?X) :- q(?X) ."); + + assertFalse(Reliance.positively(px_qx, qx_px)); + } + + @Test + public void cyclicUni2ExiTest() throws Exception { + Rule px_qy = RuleParser.parseRule("q(!Y) :- p(?X) ."); + Rule qx_px = RuleParser.parseRule("p(?X) :- q(?X) ."); + + assertFalse(Reliance.positively(px_qy, qx_px)); + assertFalse(Reliance.positively(qx_px, px_qy)); + } + + @Test + public void cyclicUni2ConTest() throws Exception { + Rule px_qc = RuleParser.parseRule("q(c) :- p(?X) ."); + Rule qx_px = RuleParser.parseRule("p(?X) :- q(?X) ."); + + assertTrue(Reliance.positively(px_qc, qx_px)); + assertTrue(Reliance.positively(qx_px, px_qc)); + } + + @Test + public void cyclicCon2UniTest() throws Exception { + Rule px_qx = RuleParser.parseRule("q(?X) :- p(?X) ."); + Rule qc_px = RuleParser.parseRule("p(!X) :- q(c) ."); + + assertFalse(Reliance.positively(px_qx, qc_px)); + } + + @Test + public void cyclicCon2ExiTest() throws Exception { + Rule px_qy = RuleParser.parseRule("q(!Y) :- p(?X) ."); + Rule qc_px = RuleParser.parseRule("p(!X) :- q(c) ."); + + assertFalse(Reliance.positively(px_qy, qc_px)); + } + + @Test + public void cyclicCon2ConTest() throws Exception { + Rule px_qc = RuleParser.parseRule("q(c) :- p(?X) ."); + Rule qc_px = RuleParser.parseRule("p(!X) :- q(c) ."); + Rule qd_px = RuleParser.parseRule("p(!X) :- q(d) ."); + + assertFalse(Reliance.positively(px_qc, qc_px)); + assertFalse(Reliance.positively(px_qc, qd_px)); + } + + @Test + public void complexExistentialRuleTest() throws Exception { + Rule rule1 = RuleParser.parseRule("r(?X1,!Y1,!Z1) :- a(?X1) ."); + Rule rule2 = RuleParser.parseRule("b(?X2,?X3) :- r(c,?X2, ?Y2), r(c,?X3, ?Y3) ."); + + assertFalse(Reliance.positively(rule1, rule1)); + assertTrue(Reliance.positively(rule1, rule2)); + assertFalse(Reliance.positively(rule2, rule1)); + assertFalse(Reliance.positively(rule2, rule2)); + } + + @Test + public void test01() throws Exception { + Rule rule1 = RuleParser.parseRule("q(?X,?Y) :- p(?X,?Y) ."); + Rule rule2 = RuleParser.parseRule("r(?X,!Z) :- q(?X,?Y), q(?Y,?X) ."); + + assertFalse(Reliance.positively(rule1, rule1)); + assertTrue(Reliance.positively(rule1, rule2)); + assertFalse(Reliance.positively(rule2, rule1)); + assertFalse(Reliance.positively(rule2, rule2)); + } + + @Test + public void test02() throws Exception { + Rule rule1 = RuleParser.parseRule("cd(?Xdoid) :- dh(?X, ?Y), doid(?Y, \"DOID:162\"), doid(?X, ?Xdoid) ."); + Rule rule2 = RuleParser.parseRule("hwdonc(?X) :- dc(?X, ?Y), id(?Y, ?Z), ~cD(?Z) ."); + + assertFalse(Reliance.positively(rule1, rule1)); + assertFalse(Reliance.positively(rule1, rule2)); + assertFalse(Reliance.positively(rule2, rule1)); + assertFalse(Reliance.positively(rule2, rule2)); + } + + @Test + public void test03() throws Exception { + Rule rule1 = RuleParser.parseRule("S(?Y,?X) :- R(?X,?Y) ."); + Rule rule2 = RuleParser.parseRule("R(?Y,?X) :- S(?X,?Y) ."); + + assertFalse(Reliance.positively(rule1, rule1)); + assertFalse(Reliance.positively(rule1, rule2)); + assertFalse(Reliance.positively(rule2, rule1)); + assertFalse(Reliance.positively(rule2, rule2)); + } + + @Test + public void test04() throws Exception { + Rule rule1 = RuleParser.parseRule("S(?Y,?X), P(?X) :- R(?X,?Y) ."); + Rule rule2 = RuleParser.parseRule("R(?X,?Y) :- S(?Y,?X) ."); + + assertFalse(Reliance.positively(rule1, rule1)); + assertFalse(Reliance.positively(rule1, rule2)); + assertTrue(Reliance.positively(rule2, rule1)); + assertFalse(Reliance.positively(rule2, rule2)); + } + + @Test + public void recursiveRuleTest() throws Exception { + Rule rule1 = RuleParser.parseRule("p(?Y,!Z) :- p(?X,?Y) ."); + Rule rule2 = RuleParser.parseRule("p(?X,!Z) :- p(?X,?Y) ."); + + assertFalse(Reliance.positively(rule1, rule1)); + assertFalse(Reliance.positively(rule2, rule2)); + } + + @Test + public void transitiveClosure1Test() throws Exception { + Rule rule1 = RuleParser.parseRule("Q(?X,?Y) :- P(?X,?Y) ."); + Rule rule2 = RuleParser.parseRule("Q(?X,?Z) :- Q(?X,?Y), Q(?Y,?Z) ."); + + assertFalse(Reliance.positively(rule1, rule1)); + assertTrue(Reliance.positively(rule1, rule2)); + assertFalse(Reliance.positively(rule2, rule1)); + assertTrue(Reliance.positively(rule2, rule2)); + } + + @Test + public void transitiveClosure2Test() throws Exception { + Rule rule1 = RuleParser.parseRule("Q(?X,?Y) :- P(?X,?Y) ."); + Rule rule2 = RuleParser.parseRule("Q(?X,?Z) :- P(?X,?Y), Q(?Y,?Z) ."); + + assertFalse(Reliance.positively(rule1, rule1)); + assertTrue(Reliance.positively(rule1, rule2)); + assertFalse(Reliance.positively(rule2, rule1)); + assertTrue(Reliance.positively(rule2, rule2)); + } + + @Test(expected = IllegalArgumentException.class) + public void test05a() throws Exception { + Rule rule1 = RuleParser.parseRule("Q(?X,?Y) :- Q(?X,?Y) ."); + + Reliance.positively(rule1, rule1); + } + + @Test(expected = IllegalArgumentException.class) + public void test05b() throws Exception { + Rule rule1 = RuleParser.parseRule("Q(?X,?Y) :- Q(?X,?Y) ."); + Rule rule2 = RuleParser.parseRule("Q(?Y,?Y) :- Q(?X,?Y) ."); + + Reliance.positively(rule2, rule1); + } + + @Test + public void test06() throws Exception { + Rule rule1 = RuleParser.parseRule("Q(?X,?Y) :- P(?X,?Y) ."); + Rule rule2 = RuleParser.parseRule("P(?X,!Z) :- Q(?X,?Y) ."); + + assertFalse(Reliance.positively(rule1, rule1)); + assertFalse(Reliance.positively(rule1, rule2)); + assertFalse(Reliance.positively(rule2, rule1)); + assertFalse(Reliance.positively(rule2, rule2)); + } + + @Test + public void test07() throws Exception { + Rule rule1 = RuleParser.parseRule("P(?X,!Z) :- P(?X,?Y) ."); + + assertFalse(Reliance.positively(rule1, rule1)); + } + + @Test + public void test08() throws Exception { + Rule rule1 = RuleParser.parseRule("P(?X,!U), P(!U,!V) :- P(?X,?Y) ."); + Rule rule2 = RuleParser.parseRule("P(?X,!U), P(!U,!V) :- Q(?X,?Y) ."); + + assertFalse(Reliance.positively(rule1, rule1)); + assertFalse(Reliance.positively(rule1, rule2)); + assertFalse(Reliance.positively(rule2, rule1)); + assertFalse(Reliance.positively(rule2, rule2)); + } + + @Test + public void test09() throws Exception { + Rule rule1 = RuleParser.parseRule("P(!U,?Y,?Z) :- P(?X,?Y,?Z) ."); + Rule rule2 = RuleParser.parseRule("P(?X,!U,?Z) :- P(?X,?Y,?Z) ."); + Rule rule3 = RuleParser.parseRule("P(?X,?Y,!U) :- P(?X,?Y,?Z) ."); + + assertFalse(Reliance.positively(rule1, rule1)); + assertFalse(Reliance.positively(rule1, rule2)); + assertFalse(Reliance.positively(rule1, rule3)); + assertFalse(Reliance.positively(rule2, rule1)); + assertFalse(Reliance.positively(rule2, rule2)); + assertFalse(Reliance.positively(rule2, rule3)); + assertFalse(Reliance.positively(rule3, rule1)); + assertFalse(Reliance.positively(rule3, rule2)); + assertFalse(Reliance.positively(rule3, rule3)); + } + + @Test + public void test10() throws Exception { + Rule rule1 = RuleParser.parseRule("P(?Y,?X) :- P(?X,?Y) ."); + + assertFalse(Reliance.positively(rule1, rule1)); + } + + @Test + public void test11() throws Exception { + Rule rule1 = RuleParser.parseRule("q(?X,!U,!V), q(?Y,!V,!U), q(?Z,!V,!W) :- q(?X,?Y,?Z) ."); + + assertTrue(Reliance.positively(rule1, rule1)); + } + + @Test + public void test12() throws Exception { + Rule rule1 = RuleParser.parseRule("q(!U,!V,!W) :- q(?X,?Y,?Z) ."); + + assertFalse(Reliance.positively(rule1, rule1)); + } + + @Test + public void test13() throws Exception { + Rule rule1 = RuleParser.parseRule("q(!Y) :- q(?X) ."); + + assertFalse(Reliance.positively(rule1, rule1)); + } + + @Test + public void test14() throws Exception { + Rule rule1 = RuleParser.parseRule("q(?X) :- p(?X) ."); + Rule rule2 = RuleParser.parseRule("r(!Y) :- q(c) ."); + + assertFalse(Reliance.positively(rule1, rule1)); + assertTrue(Reliance.positively(rule1, rule2)); + assertFalse(Reliance.positively(rule2, rule1)); + assertFalse(Reliance.positively(rule2, rule2)); + } + + @Test + public void test15() throws Exception { + Rule rule1 = RuleParser.parseRule("P(!U,?Z,?Y) :- P(?X,?Y,?Z) ."); + Rule rule2 = RuleParser.parseRule("P(?Z,!U,?X) :- P(?X,?Y,?Z) ."); + Rule rule3 = RuleParser.parseRule("P(?Y,?X,!U) :- P(?X,?Y,?Z) ."); + + assertFalse(Reliance.positively(rule1, rule1)); + assertTrue(Reliance.positively(rule1, rule2)); + assertTrue(Reliance.positively(rule1, rule3)); + assertTrue(Reliance.positively(rule2, rule1)); + assertFalse(Reliance.positively(rule2, rule2)); + assertTrue(Reliance.positively(rule2, rule3)); + assertTrue(Reliance.positively(rule3, rule1)); + assertTrue(Reliance.positively(rule3, rule2)); + assertFalse(Reliance.positively(rule3, rule3)); + } + + @Test + public void rulesNotApplicable() throws Exception { + Rule rule1 = RuleParser.parseRule("P(!U,?Y) :- P(?X,?Y) ."); + Rule rule2 = RuleParser.parseRule("P(?Y,?Y) :- P(?X,?Y) ."); + + assertFalse(Reliance.positively(rule1, rule1)); + assertFalse(Reliance.positively(rule1, rule2)); + assertFalse(Reliance.positively(rule2, rule1)); + assertFalse(Reliance.positively(rule2, rule2)); + } + +} + diff --git a/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/reliances/RestraintTest.java b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/reliances/RestraintTest.java new file mode 100644 index 000000000..cd59812ce --- /dev/null +++ b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/reliances/RestraintTest.java @@ -0,0 +1,185 @@ +package org.semanticweb.rulewerk.reliances; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import static org.junit.Assert.assertFalse; +import static org.junit.Assert.assertTrue; + +import org.junit.Test; + +import org.semanticweb.rulewerk.core.model.api.Rule; +import org.semanticweb.rulewerk.parser.RuleParser; + +public class RestraintTest { + + @Test + public void falseDueToBlockingTest() throws Exception { + Rule rule1 = RuleParser.parseRule("q(?X,!Y) :- p(?X) ."); + Rule rule2 = RuleParser.parseRule("q(?X,!Y) :- r(?X) ."); + + assertFalse(Restraint.restraint(rule1, rule2)); + assertFalse(Restraint.restraint(rule2, rule1)); + } + + @Test + public void singleAtomPiece() throws Exception { + Rule rule1 = RuleParser.parseRule("q(?X,?Y) :- p(?X,?Y) ."); + Rule rule2 = RuleParser.parseRule("q(?X,!Y) :- r(?X) ."); + + assertTrue(Restraint.restraint(rule1, rule2)); + assertFalse(Restraint.restraint(rule2, rule1)); + } + + @Test + public void twoVariablesIntoOneTest() throws Exception { + Rule rule1 = RuleParser.parseRule("b(?X,!Y,!Y) :- a(?X) ."); + Rule rule2 = RuleParser.parseRule("b(?X,!Y,!Z) :- a(?X) ."); + + assertTrue(Restraint.restraint(rule1, rule2)); + assertFalse(Restraint.restraint(rule2, rule1)); + } + + @Test + public void successorPredecesorTest() throws Exception { + Rule rule1 = RuleParser.parseRule("q(!Y,?X), q(?X,!Z) :- p(?X) ."); + Rule rule2 = RuleParser.parseRule("q(?X,!Y) :- r(?X) ."); + + assertTrue(Restraint.restraint(rule1, rule2)); + assertFalse(Restraint.restraint(rule2, rule1)); + } + + @Test + public void successorPredecesorWithExtraAtomTest() throws Exception { + Rule rule1 = RuleParser.parseRule("q(!Y,?X), q(?X,!Z) :- p(?X) ."); + Rule rule2 = RuleParser.parseRule("q(?X,!Y), s(!Y) :- r(?X) ."); + + assertFalse(Restraint.restraint(rule1, rule2)); + assertTrue(Restraint.restraint(rule2, rule1)); + } + + @Test + public void successorPredecesorWithExtraAtomToUniversalVarTest() throws Exception { + Rule rule1 = RuleParser.parseRule("q(!Y,?X), q(?X,?Z) :- p(?X,?Z) ."); + Rule rule2 = RuleParser.parseRule("q(?X,!Y), s(!Y) :- r(?X) ."); + + assertTrue(Restraint.restraint(rule1, rule2)); + assertFalse(Restraint.restraint(rule2, rule1)); + } + + @Test + public void unifyTwoAtomsIntoOneTest() throws Exception { + Rule rule1 = RuleParser.parseRule("q(?X,!Y) :- r(?X) ."); + Rule rule2 = RuleParser.parseRule("q(?X,!Z), q(?Y,!Z) :- p(?X,?Y) ."); + + assertFalse(Restraint.restraint(rule1, rule2)); + assertTrue(Restraint.restraint(rule2, rule1)); + } + + @Test + public void unifyTwoAtomsIntoOneTest02() throws Exception { + Rule rule1 = RuleParser.parseRule("q(?X,!U), q(?Y,!U) :- p(?X,?Y) ."); + Rule rule2 = RuleParser.parseRule("q(?X,!Z), q(?Y,!Z) :- p(?X,?Y) ."); + + assertTrue(Restraint.restraint(rule1, rule2)); + assertTrue(Restraint.restraint(rule2, rule1)); + } + + @Test + public void blockingRestraintTest() throws Exception { + Rule rule1 = RuleParser.parseRule("b(?X,!Y,!Y),c(!Y,!Z) :- a(?X) ."); + Rule rule2 = RuleParser.parseRule("b(?X,!Y,!Z),c(!Z,!Z) :- a(?X) ."); + + assertFalse(Restraint.restraint(rule1, rule2)); + assertFalse(Restraint.restraint(rule2, rule1)); + } + + @Test + public void freeInstantiationofExistentialVariableInHead22() throws Exception { + Rule rule1 = RuleParser.parseRule("b(?X,!Y), c(!Y) :- a(?X) ."); + Rule rule2 = RuleParser.parseRule("b(?X,?X) :- a(?X) ."); + + assertFalse(Restraint.restraint(rule1, rule2)); + assertTrue(Restraint.restraint(rule2, rule1)); + } + + @Test + public void freeInstantiationofExistentialVariableInHead22_02() throws Exception { + Rule rule1 = RuleParser.parseRule("b(?X,?Y,?Y) :- a(?X,?Y) ."); + Rule rule2 = RuleParser.parseRule("b(?X,!Y,!Z), d(!Z) :- c(?X) ."); + + assertTrue(Restraint.restraint(rule1, rule2)); + assertFalse(Restraint.restraint(rule2, rule1)); + } + + @Test + public void fromSelfRestraintExtRule08() throws Exception { + Rule rule1 = RuleParser.parseRule("q(?X,?Z) :- p(?X,?Z) ."); + Rule rule2 = RuleParser.parseRule("q(!Y,?X) :- p(?X,?Z) ."); + + assertTrue(Restraint.restraint(rule1, rule2)); + assertFalse(Restraint.restraint(rule2, rule1)); + } + + @Test + public void fromSelfRestraintExtRule15() throws Exception { + Rule rule1 = RuleParser.parseRule("r(?X, !W, !V), s(!U, !V, !W) :- b(?X) ."); + Rule rule2 = RuleParser.parseRule("r(?X, !U, !V), s(!U, !V, !W) :- b(?X) ."); + + assertFalse(Restraint.restraint(rule1, rule2)); + assertFalse(Restraint.restraint(rule2, rule1)); + } + + @Test + public void fromSelfRestraintExtRule16() throws Exception { + Rule rule1 = RuleParser.parseRule("q(?X,!U,!V), q(?Y,!V,!U), q(?Z,!V,!W) :- p(?X,?Y,?Z) ."); + Rule rule2 = RuleParser.parseRule("q(?X,!U,!H), q(?Y,!H,!U), q(?Z,!H,!W) :- p(?X,?Y,?Z) ."); + + assertTrue(Restraint.restraint(rule1, rule2)); + assertTrue(Restraint.restraint(rule2, rule1)); + } + + @Test + public void latest01() throws Exception { + Rule rule1 = RuleParser.parseRule("q(?X,!Y,!Y), r(?X) :- p(?X) ."); + Rule rule2 = RuleParser.parseRule("q(?X,!Y,!Z) :- p(?X) ."); + + assertTrue(Restraint.restraint(rule1, rule2)); + assertFalse(Restraint.restraint(rule2, rule1)); + } + + @Test + public void latest02() throws Exception { + Rule rule1 = RuleParser.parseRule("q(?X,!Y,!Z), r(?X) :- p(?X) ."); + Rule rule2 = RuleParser.parseRule("q(?X,!Y,!Y) :- p(?X) ."); + + assertFalse(Restraint.restraint(rule1, rule2)); + assertTrue(Restraint.restraint(rule2, rule1)); + } + + @Test + public void trueNegativeTest() throws Exception { + Rule rule1 = RuleParser.parseRule("q(?X,!Y), r(?X) :- p(?X) ."); + Rule rule2 = RuleParser.parseRule("r(?X), s(?X,!Y) :- p(?X) ."); + + assertFalse(Restraint.restraint(rule1, rule2)); + assertFalse(Restraint.restraint(rule2, rule1)); + } +} diff --git a/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/reliances/SelfRestraintTest.java b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/reliances/SelfRestraintTest.java new file mode 100644 index 000000000..3088ada74 --- /dev/null +++ b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/reliances/SelfRestraintTest.java @@ -0,0 +1,243 @@ +package org.semanticweb.rulewerk.reliances; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2020 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import static org.junit.Assert.assertFalse; +import static org.junit.Assert.assertTrue; + +import org.junit.Test; + +import org.semanticweb.rulewerk.core.model.api.Rule; +import org.semanticweb.rulewerk.parser.RuleParser; + +public class SelfRestraintTest { + + // TODO add tests with constants + @Test + public void datalogRule01() throws Exception { + Rule rule = RuleParser.parseRule("q(?X) :- p(?X) ."); + + assertFalse(SelfRestraint.restraint(rule)); + } + + @Test + public void datalogRule02() throws Exception { + Rule rule = RuleParser.parseRule("q(?X,?X) :- p(?X) ."); + + assertFalse(SelfRestraint.restraint(rule)); + } + + @Test + public void datalogRule03() throws Exception { + Rule rule = RuleParser.parseRule("q(?X,?Y) :- p(?X,?Y) ."); + + assertFalse(SelfRestraint.restraint(rule)); + } + + @Test + public void datalogRule04() throws Exception { + Rule rule = RuleParser.parseRule("q(?X,?Y), q(?Y,?Z) :- p(?X,?Y,?Z) ."); + + assertFalse(SelfRestraint.restraint(rule)); + } + + @Test + public void datalogRule05() throws Exception { + Rule rule = RuleParser.parseRule("r(?X,?Y), r(?Y,?Z) :- p(?X,?Y), q(?Y,?Z) ."); + + assertFalse(SelfRestraint.restraint(rule)); + } + + @Test + public void datalogRule06() throws Exception { + Rule rule = RuleParser.parseRule("r(?X,?Y,?Z), s(?X,?Y,?Z) :- p(?X,?Y), q(?Y,?Z) ."); + + assertFalse(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule01() throws Exception { + Rule rule = RuleParser.parseRule("q(?X,!Y) :- r(?X) ."); + + assertFalse(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule02() throws Exception { + Rule rule = RuleParser.parseRule("b(?X,!Y,!Y) :- a(?X) ."); + + assertFalse(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule03() throws Exception { + Rule rule = RuleParser.parseRule("b(?X,!Y,!Z) :- a(?X) ."); + + assertFalse(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule04() throws Exception { + Rule rule = RuleParser.parseRule("b(!Y) :- a(?X) ."); + + assertTrue(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule05() throws Exception { + Rule rule = RuleParser.parseRule("b(?X),c(!Y) :- a(?X) ."); + + assertTrue(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule06() throws Exception { + Rule rule = RuleParser.parseRule("q(!Y,?X), q(?X,!Z) :- p(?X) ."); + + assertFalse(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule07() throws Exception { + Rule rule = RuleParser.parseRule("q(?X,!Y), s(!Y) :- r(?X) ."); + + assertFalse(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule08() throws Exception { + Rule rule = RuleParser.parseRule("q(!Y,?X), q(?X,?Z) :- p(?X,?Z) ."); + + assertTrue(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule09() throws Exception { + Rule rule = RuleParser.parseRule("q(?X,!Z), q(?Y,!Z) :- p(?X,?Y) ."); + + assertTrue(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule10() throws Exception { + Rule rule = RuleParser.parseRule("b(?X,!Y,!Y),c(!Y,!Z) :- a(?X) ."); + + assertFalse(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule11() throws Exception { + Rule rule = RuleParser.parseRule("b(?X,!Y,!Z),c(!Z,!Z) :- a(?X) ."); + + assertFalse(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule12() throws Exception { + Rule rule = RuleParser.parseRule("r(?X,!V,!W), r(?X,?X,!W), a(!V) :- b(?X) ."); + + assertTrue(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule13() throws Exception { + Rule rule = RuleParser.parseRule("b(?X,!Y), c(!Y) :- a(?X) ."); + + assertFalse(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule14() throws Exception { + Rule rule = RuleParser.parseRule("r(?X, ?Y, !Z), r(?X, !Z, ?Y) :- b(?X,?Y) ."); + + assertFalse(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule15() throws Exception { + Rule rule = RuleParser.parseRule("r(?X, !U, !V), r(?X, !W, !V), s(!U, !V, !W) :- b(?X) ."); + + assertFalse(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule16() throws Exception { + Rule rule = RuleParser.parseRule("q(?X,!U,!V), q(?Y,!V,!U), q(?Z,!V,!W) :- p(?X,?Y,?Z) ."); + + assertTrue(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule17() throws Exception { + Rule rule = RuleParser.parseRule("q(?X,?Y), q(?X,!U), q(?Y,!U) :- p(?X,?Y) ."); + + assertTrue(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule18() throws Exception { + Rule rule = RuleParser.parseRule("p(!U,!V) :- p(?X,?Y) ."); + + assertFalse(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule19() throws Exception { + Rule rule = RuleParser.parseRule("p(?X,!Z) :- p(?X,?Y) ."); + + assertFalse(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule20() throws Exception { + Rule rule = RuleParser.parseRule("p(?X,!U), q(?Y) :- p(?X,?Y) ."); + + assertTrue(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule21() throws Exception { + Rule rule = RuleParser.parseRule("p(!U,!V), q(?X) :- p(?X,?Y) ."); + + assertTrue(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule22() throws Exception { + Rule rule = RuleParser.parseRule("q(?X,!U), q(?Y,!U), q(?Z,!U) :- p(?X,?Y,?Z) ."); + + assertTrue(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule23() throws Exception { + Rule rule = RuleParser.parseRule("q(?Y,!Z),r(?X,?Y),r(?Y,?X) :- p(?X,?Y) ."); + + assertTrue(SelfRestraint.restraint(rule)); + } + + @Test + public void existentialRule24() throws Exception { + Rule rule = RuleParser.parseRule("q(?Y,!Z),r(?X,?X),r(?X,?Y),r(?Y,?X),r(?Y,?Y) :- p(?X,?Y) ."); + + assertTrue(SelfRestraint.restraint(rule)); + } +} diff --git a/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/utils/BCQATest.java b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/utils/BCQATest.java new file mode 100644 index 000000000..17367f26d --- /dev/null +++ b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/utils/BCQATest.java @@ -0,0 +1,111 @@ +package org.semanticweb.rulewerk.utils; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2021 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ +import static org.junit.Assert.assertTrue; +import static org.junit.Assert.assertFalse; + +import java.util.ArrayList; +import java.util.List; + +import org.junit.Test; +import org.semanticweb.rulewerk.parser.ParsingException; +import org.semanticweb.rulewerk.parser.RuleParser; +import org.semanticweb.rulewerk.core.model.api.Literal; + +// TODO add more complex tests +public class BCQTest { + + @Test + public void test001() throws ParsingException { + List instance = new ArrayList<>(); + List query = new ArrayList<>(); + + instance.add(RuleParser.parseLiteral("p(a)")); + query.add(RuleParser.parseLiteral("p(?X)")); + assertTrue(BCQ.query(instance, query)); + } + + @Test + public void test002() throws ParsingException { + List instance = new ArrayList<>(); + List query = new ArrayList<>(); + + instance.add(RuleParser.parseLiteral("p(a)")); + query.add(RuleParser.parseLiteral("p(!X)")); + assertTrue(BCQ.query(instance, query)); + } + + @Test + public void test003() throws ParsingException { + List instance = new ArrayList<>(); + List query = new ArrayList<>(); + + instance.add(RuleParser.parseLiteral("p(a)")); + query.add(RuleParser.parseLiteral("q(?X)")); + assertFalse(BCQ.query(instance, query)); + } + + @Test + public void test004() throws ParsingException { + List instance = new ArrayList<>(); + List query = new ArrayList<>(); + + instance.add(RuleParser.parseLiteral("p(a)")); + query.add(RuleParser.parseLiteral("q(!X)")); + assertFalse(BCQ.query(instance, query)); + } + + @Test + public void test_005() throws ParsingException { + List instance = new ArrayList<>(); + List query = new ArrayList<>(); + + instance.add(RuleParser.parseLiteral("p(a)")); + query.add(RuleParser.parseLiteral("q(a)")); + + assertFalse(BCQ.query(instance, query)); + } + + @Test + public void test_006() throws ParsingException { + List instance = new ArrayList<>(); + List query = new ArrayList<>(); + + instance.add(RuleParser.parseLiteral("p(a)")); + instance.add(RuleParser.parseLiteral("p(b)")); + query.add(RuleParser.parseLiteral("q(a)")); + + assertFalse(BCQ.query(instance, query)); + } + + @Test + public void test_007() throws ParsingException { + List instance = new ArrayList<>(); + List query = new ArrayList<>(); + + instance.add(RuleParser.parseLiteral("p(a)")); + instance.add(RuleParser.parseLiteral("p(b)")); + instance.add(RuleParser.parseLiteral("p(c)")); + query.add(RuleParser.parseLiteral("q(a)")); + + assertFalse(BCQ.query(instance, query)); + } +} diff --git a/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/utils/RuleUtilTest.java b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/utils/RuleUtilTest.java new file mode 100644 index 000000000..f5699422c --- /dev/null +++ b/rulewerk-reliances/src/test/java/org/semanticweb/rulewerk/utils/RuleUtilTest.java @@ -0,0 +1,133 @@ +package org.semanticweb.rulewerk.utils; + +/*- + * #%L + * Rulewerk Reliances + * %% + * Copyright (C) 2018 - 2021 Rulewerk Developers + * %% + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * #L% + */ + +import static org.junit.Assert.assertTrue; + +import java.io.IOException; + +import static org.junit.Assert.assertFalse; + +import org.junit.Test; +import org.semanticweb.rulewerk.core.model.api.Rule; +import org.semanticweb.rulewerk.parser.ParsingException; +import org.semanticweb.rulewerk.parser.RuleParser; + +//TODO add more tests +public class RuleUtilTest { + + @Test + public void isApplicable_001() throws ParsingException, IOException { + Rule qy_px = RuleParser.parseRule("q(!Y) :- p(?X) ."); + assertTrue(RuleUtil.isApplicable(qy_px)); + } + + @Test + public void isApplicable_002() throws ParsingException, IOException { + Rule qc_qc = RuleParser.parseRule("q(c) :- q(c) ."); + assertFalse(RuleUtil.isApplicable(qc_qc)); + } + + @Test + public void isApplicable_003() throws ParsingException, IOException { + Rule qy_qc = RuleParser.parseRule("q(!Y) :- q(c) ."); + assertFalse(RuleUtil.isApplicable(qy_qc)); + } + + @Test + public void isApplicable_004() throws ParsingException, IOException { + Rule qc_qx = RuleParser.parseRule("q(c) :- q(?X) ."); + assertTrue(RuleUtil.isApplicable(qc_qx)); + } + + @Test + public void isApplicable_005() throws ParsingException, IOException { + Rule qy_qx = RuleParser.parseRule("q(!Y) :- q(?X) ."); + assertFalse(RuleUtil.isApplicable(qy_qx)); + } + + @Test + public void isApplicable_006() throws ParsingException, IOException { + Rule qx_qx = RuleParser.parseRule("q(?X) :- q(?X) ."); + assertFalse(RuleUtil.isApplicable(qx_qx)); + } + + @Test + public void isApplicable_007() throws ParsingException, IOException { + Rule pxz_pxy = RuleParser.parseRule("p(?X,!Z) :- p(?X,?Y) ."); + assertFalse(RuleUtil.isApplicable(pxz_pxy)); + } + + @Test + public void isApplicable_008() throws ParsingException, IOException { + Rule qxy_pxy = RuleParser.parseRule("q(?X,?Y) :- p(?X,?Y) ."); + assertTrue(RuleUtil.isApplicable(qxy_pxy)); + } + + @Test + public void isApplicable_009() throws ParsingException, IOException { + Rule pxz_qxy = RuleParser.parseRule("p(?X,!Z) :- q(?X,?Y) ."); + assertTrue(RuleUtil.isApplicable(pxz_qxy)); + } + + @Test + public void containsRepeatedAtoms_001() throws ParsingException, IOException { + Rule qy_px = RuleParser.parseRule("q(!Y) :- p(?X) ."); + assertFalse(RuleUtil.containsRepeatedAtoms(qy_px)); + } + + @Test + public void containsRepeatedAtoms_002() throws ParsingException, IOException { + Rule qc_qc = RuleParser.parseRule("q(c) :- q(c) ."); + assertTrue(RuleUtil.containsRepeatedAtoms(qc_qc)); + } + + @Test + public void containsRepeatedAtoms_003() throws ParsingException, IOException { + Rule qy_qc = RuleParser.parseRule("q(!Y) :- q(c) ."); + assertFalse(RuleUtil.containsRepeatedAtoms(qy_qc)); + } + + @Test + public void containsRepeatedAtoms_004() throws ParsingException, IOException { + Rule qc_qx = RuleParser.parseRule("q(c) :- q(?X) ."); + assertFalse(RuleUtil.containsRepeatedAtoms(qc_qx)); + } + + @Test + public void containsRepeatedAtoms_005() throws ParsingException, IOException { + Rule qy_qx = RuleParser.parseRule("q(!Y) :- q(?X) ."); + assertFalse(RuleUtil.containsRepeatedAtoms(qy_qx)); + } + + @Test + public void containsRepeatedAtoms_006() throws ParsingException, IOException { + Rule qx_qx = RuleParser.parseRule("q(?X) :- q(?X) ."); + assertTrue(RuleUtil.containsRepeatedAtoms(qx_qx)); + } + + @Test + public void containsRepeatedAtoms_007() throws ParsingException, IOException { + Rule pxz_pxy = RuleParser.parseRule("p(?X,!Z) :- p(?X,?Y) ."); + assertFalse(RuleUtil.containsRepeatedAtoms(pxz_pxy)); + } + +}