diff --git a/src/main/java/at/ac/tuwien/kr/alpha/Util.java b/src/main/java/at/ac/tuwien/kr/alpha/Util.java index 358012221..bab1de70c 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/Util.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/Util.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2016, the Alpha Team. +/* + * Copyright (c) 2016-2020, the Alpha Team. * All rights reserved. * * Additional changes made by Siemens. @@ -33,8 +33,13 @@ import java.nio.channels.ReadableByteChannel; import java.nio.charset.StandardCharsets; import java.util.AbstractMap; +import java.util.Collection; +import java.util.Collections; +import java.util.Comparator; import java.util.Iterator; +import java.util.LinkedHashSet; import java.util.Map; +import java.util.Set; import java.util.SortedSet; import java.util.StringJoiner; import java.util.stream.Collector; @@ -52,6 +57,13 @@ public static Map.Entry entry(K key, V value) { return Collectors.toMap(Map.Entry::getKey, Map.Entry::getValue); } + public static K getKeyWithMaximumValue(Map map) { + if (map.isEmpty()) { + return null; + } + return Collections.max(map.entrySet(), Comparator.comparingInt(Map.Entry::getValue)).getKey(); + } + public static String join(String prefix, Iterable iterable, String suffix) { return join(prefix, iterable, ", ", suffix); } @@ -117,4 +129,22 @@ public static int arrayGrowthSize(int oldSize) { // Growth factor is 1.5. return oldSize + (oldSize >> 1); } + + public static Set intArrayToLinkedHashSet(int[] array) { + final Set set = new LinkedHashSet<>(array.length); + for (int element : array) { + set.add(element); + } + return set; + } + + public static int[] collectionToIntArray(Collection collection) { + final int[] array = new int[collection.size()]; + int i = 0; + for (Integer element : collection) { + array[i++] = element; + } + return array; + } + } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/AtomStore.java b/src/main/java/at/ac/tuwien/kr/alpha/common/AtomStore.java index ec8278b82..02cf91297 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/AtomStore.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/AtomStore.java @@ -94,7 +94,7 @@ default String literalToString(int literal) { * @param noGood the nogood to translate * @return the string representation of the NoGood. */ - default String noGoodToString(T noGood) { + default > String noGoodToString(T noGood) { StringBuilder sb = new StringBuilder(); if (noGood.hasHead()) { diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/Literals.java b/src/main/java/at/ac/tuwien/kr/alpha/common/Literals.java index 8c703a54b..7a260a09b 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/Literals.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/Literals.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2016-2019, the Alpha Team. +/* + * Copyright (c) 2016-2020, the Alpha Team. * All rights reserved. * * Additional changes made by Siemens. @@ -80,4 +80,19 @@ public static int positiveLiteral(int literal) { public static String literalToString(int literal) { return (isPositive(literal) ? "+" : "-") + atomOf(literal); } + + /** + * Returns the index of the first position at which a literal of the given atom occurs in the given array of literals. + * @param atom the atom to look for + * @param literals an array of literals + * @return the first index where the atom occurs, or -1 if it does not occur + */ + public static int findAtomInLiterals(int atom, int[] literals) { + for (int i = 0; i < literals.length; i++) { + if (atomOf(literals[i]) == atom) { + return i; + } + } + return -1; + } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/NoGood.java b/src/main/java/at/ac/tuwien/kr/alpha/common/NoGood.java index cf452fa8f..8bd5c9743 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/NoGood.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/NoGood.java @@ -35,29 +35,36 @@ import java.util.stream.IntStream; import static at.ac.tuwien.kr.alpha.Util.oops; -import static at.ac.tuwien.kr.alpha.common.Literals.*; -import static at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type.*; - -public class NoGood implements NoGoodInterface, Comparable { - public static final int HEAD = 0; +import static at.ac.tuwien.kr.alpha.common.Literals.atomOf; +import static at.ac.tuwien.kr.alpha.common.Literals.isNegated; +import static at.ac.tuwien.kr.alpha.common.Literals.isPositive; +import static at.ac.tuwien.kr.alpha.common.Literals.negateLiteral; +import static at.ac.tuwien.kr.alpha.common.Literals.positiveLiteral; +import static at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type.INTERNAL; +import static at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type.LEARNT; +import static at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type.STATIC; +import static at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type.SUPPORT; + +public class NoGood implements NoGoodInterface, Comparable { public static final NoGood UNSAT = new NoGood(); protected final int[] literals; private final boolean head; private final Type type; + private NonGroundNoGood nonGroundNoGood; public NoGood(int... literals) { this(STATIC, literals, false); } - + public NoGood(Type type, int... literals) { this(type, literals, false); } - + private NoGood(Type type, int[] literals, boolean head) { this.type = type; this.head = head; - if (head && !isNegated(literals[0])) { + if (head && !isNegated(literals[HEAD])) { throw oops("Head is not negative"); } @@ -80,8 +87,9 @@ protected NoGood(NoGood noGood) { this.literals = noGood.literals.clone(); this.head = noGood.head; this.type = noGood.type; + this.nonGroundNoGood = noGood.nonGroundNoGood; } - + public static NoGood learnt(int... literals) { return new NoGood(LEARNT, literals); } @@ -93,7 +101,7 @@ public static NoGood headFirst(int... literals) { public static NoGood headFirstInternal(int... literals) { return headFirst(INTERNAL, literals); } - + public static NoGood headFirst(Type type, int... literals) { return new NoGood(type, literals, true); } @@ -109,11 +117,11 @@ public static NoGood support(int headLiteral, int bodyRepresentingLiteral) { public static NoGood fromConstraint(List posLiterals, List negLiterals) { return new NoGood(addPosNeg(new int[posLiterals.size() + negLiterals.size()], posLiterals, negLiterals, 0)); } - + public static NoGood fromBody(List posLiterals, List negLiterals, int bodyRepresentingLiteral) { return fromBody(STATIC, posLiterals, negLiterals, bodyRepresentingLiteral); } - + public static NoGood fromBodyInternal(List posLiterals, List negLiterals, int bodyRepresentingLiteral) { return fromBody(INTERNAL, posLiterals, negLiterals, bodyRepresentingLiteral); } @@ -144,6 +152,8 @@ public int size() { public Antecedent asAntecedent() { return new Antecedent() { + private final NoGood originalNoGood = NoGood.this; + @Override public int[] getReasonLiterals() { return NoGood.this.literals; // Beware: returned array must not be modified! @@ -156,6 +166,11 @@ public void bumpActivity() { @Override public void decreaseActivity() { } + + @Override + public NoGood getOriginalNoGood() { + return originalNoGood; + } }; } @@ -171,7 +186,7 @@ public int getPositiveLiteral(int index) { } @Override - public int getLiteral(int index) { + public Integer getLiteral(int index) { return literals[index]; } @@ -180,16 +195,19 @@ public boolean hasHead() { return head; } - @Override - public int getHead() { - return getLiteral(HEAD); - } - @Override public Type getType() { return type; } + public NonGroundNoGood getNonGroundNoGood() { + return nonGroundNoGood; + } + + public void setNonGroundNoGood(NonGroundNoGood nonGroundNoGood) { + this.nonGroundNoGood = nonGroundNoGood; + } + @Override public Iterator iterator() { return new Iterator() { @@ -211,6 +229,15 @@ public IntStream stream() { return Arrays.stream(literals); } + public int indexOf(int literal) { + for (int i = 0; i < literals.length; i++) { + if (literals[i] == literal) { + return i; + } + } + return -1; + } + @Override public int compareTo(NoGood o) { if (o == null) { diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/NoGoodInterface.java b/src/main/java/at/ac/tuwien/kr/alpha/common/NoGoodInterface.java index 95157630e..eb43cb575 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/NoGoodInterface.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/NoGoodInterface.java @@ -29,14 +29,16 @@ import at.ac.tuwien.kr.alpha.solver.Antecedent; -public interface NoGoodInterface extends Iterable { +public interface NoGoodInterface extends Iterable { + + int HEAD = 0; /** * Returns the literal at the given index. * @param index the index position within the NoGood. * @return the literal at the index. */ - int getLiteral(int index); + T getLiteral(int index); /** * Returns whether the NoGood has a head. @@ -46,9 +48,11 @@ public interface NoGoodInterface extends Iterable { /** * Returns the head literal of the NoGood, if present. - * @return the head literal if the NoGood has a head, otherwise an arbitrary integer. + * @return the head literal if the NoGood has a head, otherwise an arbitrary literal. */ - int getHead(); + default T getHead() { + return getLiteral(HEAD); + } /** * Returns the size, i.e., number of literals, in the NoGood. diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/NonGroundNoGood.java b/src/main/java/at/ac/tuwien/kr/alpha/common/NonGroundNoGood.java new file mode 100644 index 000000000..e7ba317c5 --- /dev/null +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/NonGroundNoGood.java @@ -0,0 +1,264 @@ +/* + * Copyright (c) 2020 Siemens AG + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * 1) Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * 2) Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +package at.ac.tuwien.kr.alpha.common; + +import at.ac.tuwien.kr.alpha.common.atoms.Atom; +import at.ac.tuwien.kr.alpha.common.atoms.Literal; +import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; +import at.ac.tuwien.kr.alpha.grounder.NoGoodGenerator; +import at.ac.tuwien.kr.alpha.solver.Antecedent; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Collection; +import java.util.HashSet; +import java.util.Iterator; +import java.util.List; +import java.util.Map; +import java.util.Objects; +import java.util.Set; +import java.util.stream.Collectors; + +import static at.ac.tuwien.kr.alpha.Util.join; +import static at.ac.tuwien.kr.alpha.Util.oops; +import static at.ac.tuwien.kr.alpha.common.Literals.atomOf; +import static at.ac.tuwien.kr.alpha.common.Literals.isPositive; +import static at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type.LEARNT; +import static at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type.STATIC; + +/** + * Represents a non-ground nogood that corresponds to several ground nogoods generated from it. + *

+ * This class assumes the following to hold without checking it: + *

    + *
  • no literal appears twice (different variable names are OK, if different literals correspond to different ground literals)
    • + *
  • the non-ground literals here appear in the same order as the corresponding ground literals in the corresponding ground nogood
    • + *
  • any literals not present in the corresponding ground nogood (e.g., arithmetic literals removed by the grounder) + * appear after all literals present in the ground nogood (i.e., if the ground nogood contains N literals, then + * the first N literals in the non-ground nogood correspond directly to ground literals at the same positions in + * the ground nogood, and all positions from N+1 till the end are for literals not present in the ground nogood)
    • + *
+ */ +public class NonGroundNoGood implements NoGoodInterface { + + protected final Literal[] literals; + private final Literal[] sortedLiterals; + private final boolean head; + private final Type type; + + public NonGroundNoGood(Literal... literals) { + this(STATIC, literals, false); + } + + public NonGroundNoGood(Type type, Literal... literals) { + this(type, literals, false); + } + + NonGroundNoGood(Type type, Literal[] literals, boolean head) { + this.type = type; + this.head = head; + if (head && !literals[HEAD].isNegated()) { + throw oops("Head is not negative"); + } + + this.literals = Arrays.copyOf(literals, literals.length); + // note: literals are not sorted here (in contrast to ground NoGood) because of the assumption that the literals + // appear in the same order as in the corresponding ground nogood + // however, we maintain a second array of literals that is sorted for comparison purposes: + // (the following code is duplicated from the constructor of NoGood) + + Arrays.sort(literals, head ? 1 : 0, literals.length); + + int shift = 0; + for (int i = 1; i < literals.length; i++) { + if (literals[i - 1] == literals[i]) { // check for duplicate + shift++; + } + literals[i - shift] = literals[i]; // Remove duplicates in place by shifting remaining literals. + } + + // copy-shrink array if needed. + this.sortedLiterals = shift <= 0 ? literals : Arrays.copyOf(literals, literals.length - shift); + } + + public static NonGroundNoGood forGroundNoGood(NoGood groundNoGood, Map atomMapping) { + return new NonGroundNoGood(groundNoGood.getType(), literalsForGroundNoGood(groundNoGood, atomMapping), groundNoGood.hasHead()); + } + + public static NonGroundNoGood fromBody(NoGood groundNoGood, NoGoodGenerator.CollectedLiterals posLiterals, NoGoodGenerator.CollectedLiterals negLiterals, Map atomMapping) { + final List literals = new ArrayList<>(Arrays.asList(literalsForGroundNoGood(groundNoGood, atomMapping))); + literals.addAll(posLiterals.getSkippedFacts()); + literals.addAll(posLiterals.getSkippedFixedInterpretationLiterals()); + literals.addAll(negLiterals.getSkippedFacts().stream().map(Literal::negate).collect(Collectors.toList())); + literals.addAll(negLiterals.getSkippedFixedInterpretationLiterals().stream().map(Literal::negate).collect(Collectors.toList())); + return new NonGroundNoGood(groundNoGood.getType(), literals.toArray(new Literal[]{}), groundNoGood.hasHead()); + } + + public static NonGroundNoGood learnt(Collection literals) { + return new NonGroundNoGood(LEARNT, literals.toArray(new Literal[]{})); + } + + private static Literal[] literalsForGroundNoGood(NoGood groundNoGood, Map atomMapping) { + final Literal[] literals = new Literal[groundNoGood.size()]; + for (int i = 0; i < groundNoGood.size(); i++) { + final int groundLiteral = groundNoGood.getLiteral(i); + literals[i] = atomMapping.get(atomOf(groundLiteral)).toLiteral(isPositive(groundLiteral)); + } + return literals; + } + + @Override + public Literal getLiteral(int index) { + return literals[index]; + } + + Literal[] getSortedLiterals() { + return sortedLiterals; + } + + @Override + public boolean hasHead() { + return head; + } + + @Override + public int size() { + return literals.length; + } + + public Set getOccurringVariables() { + final Set occurringVariables = new HashSet<>(); + for (Literal literal : literals) { + occurringVariables.addAll(literal.getOccurringVariables()); + } + return occurringVariables; + } + + @Override + public Antecedent asAntecedent() { + throw new UnsupportedOperationException("Non-ground nogood cannot be represented as an antecedent"); + } + + public Rule asConstraint() { + return new Rule(null, Arrays.asList(literals)); + } + + @Override + public Type getType() { + return type; + } + + /** + * Makes variable names more readable by: + *
    + *
  • Substituting variable names containing an underscore by the part before the underscore, if this part alone is not already used
    • + *
  • Replacing different variable names with the same prefix by new variable names with the postfixes 1 and 2, e.g., H and H_1 become H1 and H2
    • + *
+ * @return a unifier that simplifies variable names + */ + public Unifier simplifyVariableNames() { + final Unifier unifier = new Unifier(); + final Set existingVariables = getOccurringVariables(); + final Set allVariables = new HashSet<>(existingVariables); + for (VariableTerm variable : existingVariables) { + final String variableName = variable.toString(); + final int startOfPostfix = variableName.lastIndexOf('_'); + if (startOfPostfix > 0) { + final String variableNameWithoutPostfix = variableName.substring(0, startOfPostfix); + final VariableTerm variableWithoutPostfix = VariableTerm.getInstance(variableNameWithoutPostfix); + if (!allVariables.contains(variableWithoutPostfix) && unifier.eval(variableWithoutPostfix) == null) { + unifier.put(variable, variableWithoutPostfix); + allVariables.add(variableWithoutPostfix); + continue; + } + final VariableTerm variableWithNewPostfix1 = VariableTerm.getInstance(variableNameWithoutPostfix + 1); + final VariableTerm variableWithNewPostfix2 = VariableTerm.getInstance(variableNameWithoutPostfix + 2); + if (!allVariables.contains(variableWithNewPostfix1) && unifier.eval(variableWithNewPostfix1) == null && + !allVariables.contains(variableWithNewPostfix2) && unifier.eval(variableWithNewPostfix2) == null) { + unifier.put(variableWithoutPostfix, variableWithNewPostfix1); + unifier.put(variable, variableWithNewPostfix2); + allVariables.add(variableWithNewPostfix1); + allVariables.add(variableWithNewPostfix2); + } + } + } + return unifier; + } + + public NonGroundNoGood substitute(Substitution substitution) { + return new NonGroundNoGood( + this.type, + Arrays.stream(literals).map(l -> l.substitute(substitution)).collect(Collectors.toList()).toArray(new Literal[]{}), + this.head + ); + } + + @Override + public Iterator iterator() { + return new Iterator() { + private int i; + + @Override + public boolean hasNext() { + return literals.length > i; + } + + @Override + public Literal next() { + return literals[i++]; + } + }; + } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + NonGroundNoGood that = (NonGroundNoGood) o; + return head == that.head && + Arrays.equals(sortedLiterals, that.sortedLiterals) && + type == that.type; + } + + @Override + public int hashCode() { + return Objects.hash(Arrays.hashCode(sortedLiterals), head, type); + } + + @Override + public String toString() { + final List stringLiterals = new ArrayList<>(literals.length); + for (Literal literal : literals) { + stringLiterals.add((literal.isNegated() ? "-" : "+") + "(" + literal.getAtom() + ")"); + } + return (head ? "*" : "") + join("{ ", stringLiterals, ", ", " }"); + } +} diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/Rule.java b/src/main/java/at/ac/tuwien/kr/alpha/common/Rule.java index f1f8943fd..036f619dc 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/Rule.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/Rule.java @@ -30,7 +30,6 @@ import at.ac.tuwien.kr.alpha.common.atoms.Atom; import at.ac.tuwien.kr.alpha.common.atoms.Literal; import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; -import at.ac.tuwien.kr.alpha.grounder.Unifier; import java.util.ArrayList; import java.util.Collections; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/Substitution.java b/src/main/java/at/ac/tuwien/kr/alpha/common/Substitution.java similarity index 71% rename from src/main/java/at/ac/tuwien/kr/alpha/grounder/Substitution.java rename to src/main/java/at/ac/tuwien/kr/alpha/common/Substitution.java index b859cb501..442bc82da 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/Substitution.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/Substitution.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2016-2019, the Alpha Team. +/* + * Copyright (c) 2016-2020, the Alpha Team. * All rights reserved. * * Additional changes made by Siemens. @@ -25,23 +25,17 @@ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */ -package at.ac.tuwien.kr.alpha.grounder; +package at.ac.tuwien.kr.alpha.common; -import at.ac.tuwien.kr.alpha.antlr.ASPCore2Lexer; -import at.ac.tuwien.kr.alpha.antlr.ASPCore2Parser; import at.ac.tuwien.kr.alpha.common.atoms.Atom; import at.ac.tuwien.kr.alpha.common.atoms.Literal; import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm; import at.ac.tuwien.kr.alpha.common.terms.FunctionTerm; import at.ac.tuwien.kr.alpha.common.terms.Term; import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; -import at.ac.tuwien.kr.alpha.grounder.parser.ParseTreeVisitor; -import org.antlr.v4.runtime.CharStreams; -import org.antlr.v4.runtime.CommonTokenStream; -import org.antlr.v4.runtime.RecognitionException; -import org.antlr.v4.runtime.misc.ParseCancellationException; +import at.ac.tuwien.kr.alpha.grounder.Instance; +import at.ac.tuwien.kr.alpha.grounder.parser.ProgramPartParser; -import java.util.Collections; import java.util.Map; import java.util.Objects; import java.util.TreeMap; @@ -49,11 +43,12 @@ import static at.ac.tuwien.kr.alpha.Util.oops; public class Substitution { - private static final ParseTreeVisitor VISITOR = new ParseTreeVisitor(Collections.emptyMap(), false); + + private static final ProgramPartParser PROGRAM_PART_PARSER = new ProgramPartParser(); protected TreeMap substitution; - private Substitution(TreeMap substitution) { + Substitution(TreeMap substitution) { if (substitution == null) { throw oops("Substitution is null."); } @@ -68,7 +63,7 @@ public Substitution(Substitution clone) { this(new TreeMap<>(clone.substitution)); } - static Substitution unify(Literal literal, Instance instance, Substitution substitution) { + public static Substitution unify(Literal literal, Instance instance, Substitution substitution) { return unify(literal.getAtom(), instance, substitution); } @@ -91,34 +86,50 @@ public static Substitution unify(Atom atom, Instance instance, Substitution subs } /** - * Checks if the left possible non-ground term unifies with the ground term. - * @param termNonGround - * @param termGround - * @return + * Checks if the left, possibly non-ground term unifies with the right ground term. + * This substitution is modified to reflect the unification. + * @param termNonGround the left term, possibly non-ground + * @param termGround the right term, must be ground + * @return {@code true} iff the unification succeeds */ public boolean unifyTerms(Term termNonGround, Term termGround) { - if (termNonGround == termGround) { - // Both terms are either the same constant or the same variable term + return unifyTerms(termNonGround, termGround, false); + } + + /** + * Checks if the left, possibly non-ground term unifies with the right, possibly non-ground term. + * This substitution is modified to reflect the unification. + * @param termLeft the left term, possibly non-ground + * @param termRight the right term, may only be non-ground if {@code allowNonGroundTermRight} is {@code true} + * @return {@code true} iff the unification succeeds + */ + public boolean unifyTerms(Term termLeft, Term termRight, boolean allowNonGroundTermRight) { + final boolean isRightTermGround = termRight.isGround(); + if (!allowNonGroundTermRight && !isRightTermGround) { + throw new IllegalArgumentException("Term " + termRight + " is not ground."); + } + if (termLeft == termRight) { return true; - } else if (termNonGround instanceof ConstantTerm) { - // Since right term is ground, both terms differ + } else if (termLeft instanceof ConstantTerm) { return false; - } else if (termNonGround instanceof VariableTerm) { - VariableTerm variableTerm = (VariableTerm)termNonGround; - // Left term is variable, bind it to the right term. - Term bound = eval(variableTerm); - - if (bound != null) { - // Variable is already bound, return true if binding is the same as the current ground term. - return termGround == bound; + } else if (termLeft instanceof VariableTerm) { + // TODO: what do do with anonymous variables? + VariableTerm variableTermLeft = (VariableTerm)termLeft; + if (isRightTermGround) { + // Left term is variable, bind it to the right term. + Term bound = eval(variableTermLeft); + + if (bound != null) { + // Variable is already bound, return true if binding is the same as the current ground term. + return termRight == bound; + } } - - substitution.put(variableTerm, termGround); + put(variableTermLeft, termRight); return true; - } else if (termNonGround instanceof FunctionTerm && termGround instanceof FunctionTerm) { + } else if (termLeft instanceof FunctionTerm && termRight instanceof FunctionTerm) { // Both terms are function terms - FunctionTerm ftNonGround = (FunctionTerm) termNonGround; - FunctionTerm ftGround = (FunctionTerm) termGround; + FunctionTerm ftNonGround = (FunctionTerm) termLeft; + FunctionTerm ftGround = (FunctionTerm) termRight; if (!(ftNonGround.getSymbol().equals(ftGround.getSymbol()))) { return false; @@ -129,7 +140,7 @@ public boolean unifyTerms(Term termNonGround, Term termGround) { // Iterate over all subterms of both function terms for (int i = 0; i < ftNonGround.getTerms().size(); i++) { - if (!unifyTerms(ftNonGround.getTerms().get(i), ftGround.getTerms().get(i))) { + if (!unifyTerms(ftNonGround.getTerms().get(i), ftGround.getTerms().get(i), allowNonGroundTermRight)) { return false; } } @@ -198,24 +209,12 @@ public static Substitution fromString(String substitution) { for (String assignment : assignments) { String keyVal[] = assignment.split("->"); VariableTerm variable = VariableTerm.getInstance(keyVal[0]); - Term assignedTerm = parseTerm(keyVal[1]); + Term assignedTerm = PROGRAM_PART_PARSER.parseTerm(keyVal[1]); ret.put(variable, assignedTerm); } return ret; } - private static Term parseTerm(String s) { - try { - final ASPCore2Parser parser = new ASPCore2Parser(new CommonTokenStream(new ASPCore2Lexer(CharStreams.fromString(s)))); - return (Term)VISITOR.visit(parser.term()); - } catch (RecognitionException | ParseCancellationException e) { - // If there were issues parsing the given string, we - // throw something that suggests that the input string - // is malformed. - throw new IllegalArgumentException("Could not parse term.", e); - } - } - @Override public boolean equals(Object o) { if (this == o) { diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/Unification.java b/src/main/java/at/ac/tuwien/kr/alpha/common/Unification.java similarity index 97% rename from src/main/java/at/ac/tuwien/kr/alpha/grounder/Unification.java rename to src/main/java/at/ac/tuwien/kr/alpha/common/Unification.java index b448dc29f..77c81026d 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/Unification.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/Unification.java @@ -1,19 +1,19 @@ /** * Copyright (c) 2017-2018, the Alpha Team. * All rights reserved. - * + * * Additional changes made by Siemens. - * + * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are met: - * + * * 1) Redistributions of source code must retain the above copyright notice, this * list of conditions and the following disclaimer. - * + * * 2) Redistributions in binary form must reproduce the above copyright notice, * this list of conditions and the following disclaimer in the documentation * and/or other materials provided with the distribution. - * + * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE @@ -25,7 +25,7 @@ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */ -package at.ac.tuwien.kr.alpha.grounder; +package at.ac.tuwien.kr.alpha.common; import at.ac.tuwien.kr.alpha.common.atoms.Atom; import at.ac.tuwien.kr.alpha.common.terms.FunctionTerm; @@ -36,9 +36,6 @@ import static at.ac.tuwien.kr.alpha.Util.oops; -/** - * Copyright (c) 2017, the Alpha Team. - */ public class Unification { public static Unifier unifyAtoms(Atom left, Atom right) { diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/Unifier.java b/src/main/java/at/ac/tuwien/kr/alpha/common/Unifier.java similarity index 60% rename from src/main/java/at/ac/tuwien/kr/alpha/grounder/Unifier.java rename to src/main/java/at/ac/tuwien/kr/alpha/common/Unifier.java index 8d65fa7ca..7769188c5 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/Unifier.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/Unifier.java @@ -1,11 +1,14 @@ -package at.ac.tuwien.kr.alpha.grounder; +package at.ac.tuwien.kr.alpha.common; +import at.ac.tuwien.kr.alpha.common.atoms.Atom; +import at.ac.tuwien.kr.alpha.common.atoms.Literal; import at.ac.tuwien.kr.alpha.common.terms.Term; import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; import java.util.ArrayList; import java.util.List; import java.util.Map; +import java.util.Objects; import java.util.TreeMap; import static at.ac.tuwien.kr.alpha.Util.oops; @@ -47,7 +50,65 @@ public Unifier extendWith(Substitution extension) { return this; } + /** + * Unifies the given atoms if possible. Unification will only substitute variables that occur in {@code modifiableAtom}. + * @param modifiableAtom an atom that can be modified by substitution + * @param unmodifiableAtom an atom that cannot be modified by substitution + * @return {@code true} iff unification was successful + */ + public boolean unify(Atom modifiableAtom, Atom unmodifiableAtom) { + if (modifiableAtom == null || unmodifiableAtom == null) { + throw new IllegalArgumentException("Atom must not be null."); + } + if (!Objects.equals(modifiableAtom.getPredicate(), unmodifiableAtom.getPredicate())) { + throw new IllegalArgumentException("Predicates of two atoms do not match."); + } + int i = 0; + for (Term modifiableTerm : modifiableAtom.getTerms()) { + if (!unifyTerms(modifiableTerm, unmodifiableAtom.getTerms().get(i), true)) { + return false; + } + i++; + } + return true; + } + + /** + * Unifies the given non-ground nogoods if possible. Unification will only substitute variables that occur in {@code modifiableNonGroundNoGood}. + * @param modifiableNonGroundNoGood a non-ground nogood that can be modified by substitution + * @param unmodifiableNonGroundNoGood a non-ground nogood that cannot be modified by substitution + * @return {@code true} iff unification was successful + */ + public boolean unify(NonGroundNoGood modifiableNonGroundNoGood, NonGroundNoGood unmodifiableNonGroundNoGood) { + if (modifiableNonGroundNoGood.hasHead() != unmodifiableNonGroundNoGood.hasHead()) { + return false; + } + final Literal[] modifiableLiterals = modifiableNonGroundNoGood.getSortedLiterals(); + final Literal[] unmodifiableLiterals = unmodifiableNonGroundNoGood.getSortedLiterals(); + if (modifiableLiterals.length != unmodifiableLiterals.length) { + return false; + } + for (int i = 0; i < modifiableLiterals.length; i++) { + final Literal modifiableLiteral = modifiableLiterals[i]; + final Literal unmodifiableLiteral = unmodifiableLiterals[i]; + if (modifiableLiteral.isNegated() != unmodifiableLiteral.isNegated()) { + return false; + } + if (!Objects.equals(modifiableLiteral.getPredicate(), unmodifiableLiteral.getPredicate())) { + return false; + } + if (!unify(modifiableLiteral.getAtom(), unmodifiableLiteral.getAtom())) { + return false; + } + } + return true; + } + + public static boolean canBeUnifiedInBothDirections(NonGroundNoGood nonGroundNoGood1, NonGroundNoGood nonGroundNoGood2) { + return new Unifier().unify(nonGroundNoGood2, nonGroundNoGood1) && new Unifier().unify(nonGroundNoGood1, nonGroundNoGood2); + } + @Override public > Term put(VariableTerm variableTerm, Term term) { // If term is not ground, store it for right-hand side reverse-lookup. if (!term.isGround()) { diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/UniqueVariableNames.java b/src/main/java/at/ac/tuwien/kr/alpha/common/UniqueVariableNames.java new file mode 100644 index 000000000..b6ebb20f4 --- /dev/null +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/UniqueVariableNames.java @@ -0,0 +1,70 @@ +/* + * Copyright (c) 2020 Siemens AG + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * 1) Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * 2) Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +package at.ac.tuwien.kr.alpha.common; + +import at.ac.tuwien.kr.alpha.common.atoms.Literal; +import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; + +import java.util.HashMap; +import java.util.Map; +import java.util.Set; + +public class UniqueVariableNames { + + private final Map variablesToOccurrences = new HashMap<>(); + + public NonGroundNoGood makeVariableNamesUnique(NonGroundNoGood noGood) { + final Unifier unifier = renameVariablesIfAlreadyUsed(noGood.getOccurringVariables()); + if (unifier.isEmpty()) { + return noGood; + } + final Literal[] newLiterals = new Literal[noGood.size()]; + for (int i = 0; i < noGood.size(); i++) { + final Literal literal = noGood.getLiteral(i); + newLiterals[i] = literal.substitute(unifier); + } + return new NonGroundNoGood(noGood.getType(), newLiterals, noGood.hasHead()); + + } + + private Unifier renameVariablesIfAlreadyUsed(Set variables) { + final Unifier unifier = new Unifier(); + for (VariableTerm variable : variables) { + if (variablesToOccurrences.containsKey(variable)) { + VariableTerm newVariable; + do { + newVariable = VariableTerm.getInstance(variable.toString() + "_" + (variablesToOccurrences.computeIfPresent(variable, (v, o) -> o + 1))); + } while (variablesToOccurrences.containsKey(newVariable)); + unifier.put(variable, newVariable); + } else { + variablesToOccurrences.put(variable, 0); + } + } + return unifier; + } + +} diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/AggregateAtom.java b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/AggregateAtom.java index f9108050e..9f453a757 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/AggregateAtom.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/AggregateAtom.java @@ -29,9 +29,9 @@ import at.ac.tuwien.kr.alpha.common.ComparisonOperator; import at.ac.tuwien.kr.alpha.common.Predicate; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.terms.Term; import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; -import at.ac.tuwien.kr.alpha.grounder.Substitution; import java.util.Collections; import java.util.LinkedList; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/AggregateLiteral.java b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/AggregateLiteral.java index 4cdabd179..536828d1b 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/AggregateLiteral.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/AggregateLiteral.java @@ -1,9 +1,9 @@ package at.ac.tuwien.kr.alpha.common.atoms; import at.ac.tuwien.kr.alpha.common.ComparisonOperator; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.terms.Term; import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; -import at.ac.tuwien.kr.alpha.grounder.Substitution; import java.util.HashSet; import java.util.Set; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/Atom.java b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/Atom.java index 5519f3404..2c85d7c78 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/Atom.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/Atom.java @@ -28,10 +28,10 @@ package at.ac.tuwien.kr.alpha.common.atoms; import at.ac.tuwien.kr.alpha.common.Predicate; +import at.ac.tuwien.kr.alpha.common.Substitution; +import at.ac.tuwien.kr.alpha.common.Unifier; import at.ac.tuwien.kr.alpha.common.terms.Term; import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; -import at.ac.tuwien.kr.alpha.grounder.Unifier; -import at.ac.tuwien.kr.alpha.grounder.Substitution; import java.util.List; import java.util.Set; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/BasicAtom.java b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/BasicAtom.java index 172d78587..8cc036609 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/BasicAtom.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/BasicAtom.java @@ -28,10 +28,12 @@ package at.ac.tuwien.kr.alpha.common.atoms; import at.ac.tuwien.kr.alpha.common.Predicate; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.terms.Term; -import at.ac.tuwien.kr.alpha.grounder.Substitution; -import java.util.*; +import java.util.Arrays; +import java.util.Collections; +import java.util.List; import java.util.stream.Collectors; import static at.ac.tuwien.kr.alpha.Util.join; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/BasicLiteral.java b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/BasicLiteral.java index c3a078fd8..ea333e3c0 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/BasicLiteral.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/BasicLiteral.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2017-2018, the Alpha Team. +/* + * Copyright (c) 2017-2018, 2020, the Alpha Team. * All rights reserved. * * Additional changes made by Siemens. @@ -27,18 +27,10 @@ */ package at.ac.tuwien.kr.alpha.common.atoms; -import at.ac.tuwien.kr.alpha.common.terms.Term; -import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; -import at.ac.tuwien.kr.alpha.grounder.Substitution; - -import java.util.Collections; -import java.util.HashSet; -import java.util.Set; +import at.ac.tuwien.kr.alpha.common.Substitution; /** * Contains a potentially negated {@link BasicAtom}. - * - * Copyright (c) 2017-2018, the Alpha Team. */ public class BasicLiteral extends Literal { @@ -66,40 +58,4 @@ public BasicLiteral negate() { public BasicLiteral substitute(Substitution substitution) { return new BasicLiteral(getAtom().substitute(substitution), positive); } - - /** - * Set of all variables occurring in the Atom that are potentially binding, i.e., variables in positive atoms. - * - * @return - */ - @Override - public Set getBindingVariables() { - if (!positive) { - // Negative literal has no binding variables. - return Collections.emptySet(); - } - Set bindingVariables = new HashSet<>(); - for (Term term : atom.getTerms()) { - bindingVariables.addAll(term.getOccurringVariables()); - } - return bindingVariables; - } - - /** - * Set of all variables occurring in the Atom that are never binding, not even in positive atoms, e.g., variables in intervals or built-in atoms. - * - * @return - */ - @Override - public Set getNonBindingVariables() { - if (positive) { - // Positive literal has only binding variables. - return Collections.emptySet(); - } - Set nonbindingVariables = new HashSet<>(); - for (Term term : atom.getTerms()) { - nonbindingVariables.addAll(term.getOccurringVariables()); - } - return nonbindingVariables; - } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ComparisonAtom.java b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ComparisonAtom.java index b19e2a699..6df127d18 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ComparisonAtom.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ComparisonAtom.java @@ -29,8 +29,8 @@ import at.ac.tuwien.kr.alpha.common.ComparisonOperator; import at.ac.tuwien.kr.alpha.common.Predicate; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.terms.Term; -import at.ac.tuwien.kr.alpha.grounder.Substitution; import java.util.Arrays; import java.util.List; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ComparisonLiteral.java b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ComparisonLiteral.java index 91ac679d3..7681059f3 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ComparisonLiteral.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ComparisonLiteral.java @@ -28,13 +28,17 @@ package at.ac.tuwien.kr.alpha.common.atoms; import at.ac.tuwien.kr.alpha.common.ComparisonOperator; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.terms.ArithmeticTerm; import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm; import at.ac.tuwien.kr.alpha.common.terms.Term; import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; -import at.ac.tuwien.kr.alpha.grounder.Substitution; -import java.util.*; +import java.util.Collections; +import java.util.HashSet; +import java.util.LinkedList; +import java.util.List; +import java.util.Set; import static at.ac.tuwien.kr.alpha.common.terms.ArithmeticTerm.evaluateGroundTerm; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ExternalAtom.java b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ExternalAtom.java index 2c9ba2191..43cfddd69 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ExternalAtom.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ExternalAtom.java @@ -27,16 +27,16 @@ */ package at.ac.tuwien.kr.alpha.common.atoms; -import static at.ac.tuwien.kr.alpha.Util.join; +import at.ac.tuwien.kr.alpha.common.Predicate; +import at.ac.tuwien.kr.alpha.common.Substitution; +import at.ac.tuwien.kr.alpha.common.fixedinterpretations.PredicateInterpretation; +import at.ac.tuwien.kr.alpha.common.terms.Term; import java.util.Collections; import java.util.List; import java.util.stream.Collectors; -import at.ac.tuwien.kr.alpha.common.Predicate; -import at.ac.tuwien.kr.alpha.common.fixedinterpretations.PredicateInterpretation; -import at.ac.tuwien.kr.alpha.common.terms.Term; -import at.ac.tuwien.kr.alpha.grounder.Substitution; +import static at.ac.tuwien.kr.alpha.Util.join; public class ExternalAtom implements Atom, VariableNormalizableAtom { diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ExternalLiteral.java b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ExternalLiteral.java index 86a943df5..dbb9e8868 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ExternalLiteral.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ExternalLiteral.java @@ -27,12 +27,16 @@ */ package at.ac.tuwien.kr.alpha.common.atoms; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm; import at.ac.tuwien.kr.alpha.common.terms.Term; import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; -import at.ac.tuwien.kr.alpha.grounder.Substitution; -import java.util.*; +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashSet; +import java.util.List; +import java.util.Set; import static java.util.Collections.emptyList; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/FixedInterpretationLiteral.java b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/FixedInterpretationLiteral.java index 2db2df800..e831835f2 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/FixedInterpretationLiteral.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/FixedInterpretationLiteral.java @@ -27,7 +27,7 @@ */ package at.ac.tuwien.kr.alpha.common.atoms; -import at.ac.tuwien.kr.alpha.grounder.Substitution; +import at.ac.tuwien.kr.alpha.common.Substitution; import java.util.List; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/Literal.java b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/Literal.java index 907a38b04..5a713c796 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/Literal.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/Literal.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2017-2018, the Alpha Team. +/* + * Copyright (c) 2017-2018, 2020, the Alpha Team. * All rights reserved. * * Additional changes made by Siemens. @@ -28,20 +28,20 @@ package at.ac.tuwien.kr.alpha.common.atoms; import at.ac.tuwien.kr.alpha.common.Predicate; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.terms.Term; import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; -import at.ac.tuwien.kr.alpha.grounder.Substitution; import org.apache.commons.collections4.SetUtils; +import java.util.Collections; +import java.util.HashSet; import java.util.List; import java.util.Set; /** * A potentially negated {@link Atom} - * - * Copyright (c) 2017-2018, the Alpha Team. */ -public abstract class Literal { +public abstract class Literal implements Comparable { protected final Atom atom; protected final boolean positive; @@ -62,10 +62,46 @@ public boolean isNegated() { public abstract Literal negate(); public abstract Literal substitute(Substitution substitution); - - public abstract Set getBindingVariables(); - - public abstract Set getNonBindingVariables(); + + /** + * Set of all variables occurring in the Atom that are potentially binding, i.e., variables in positive atoms. + * + * This is the default implementation used by {@link BasicLiteral} and {@link at.ac.tuwien.kr.alpha.grounder.atoms.BodyRepresentingLiteral} + * and may be overridden in implementing classes. + * + * @return the set of binding variables in this literal + */ + public Set getBindingVariables() { + if (!positive) { + // Negative literal has no binding variables. + return Collections.emptySet(); + } + Set bindingVariables = new HashSet<>(); + for (Term term : atom.getTerms()) { + bindingVariables.addAll(term.getOccurringVariables()); + } + return bindingVariables; + } + + /** + * Set of all variables occurring in the Atom that are never binding, not even in positive atoms, e.g., variables in intervals or built-in atoms. + * + * This is the default implementation used by {@link BasicLiteral} and {@link at.ac.tuwien.kr.alpha.grounder.atoms.BodyRepresentingLiteral} + * and may be overridden in implementing classes. + * + * @return the set of non-binding variables in this literal + */ + public Set getNonBindingVariables() { + if (positive) { + // Positive literal has only binding variables. + return Collections.emptySet(); + } + Set nonbindingVariables = new HashSet<>(); + for (Term term : atom.getTerms()) { + nonbindingVariables.addAll(term.getOccurringVariables()); + } + return nonbindingVariables; + } /** * Union of {@link #getBindingVariables()} and {@link #getNonBindingVariables()} @@ -119,4 +155,11 @@ public int hashCode() { return 12 * atom.hashCode() + (positive ? 1 : 0); } + @Override + public int compareTo(Literal o) { + if (this.positive == o.positive) { + return this.getAtom().compareTo(o.getAtom()); + } + return Boolean.compare(this.positive, o.positive); + } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/terms/ArithmeticTerm.java b/src/main/java/at/ac/tuwien/kr/alpha/common/terms/ArithmeticTerm.java index cf01f5f6e..410fc19f2 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/terms/ArithmeticTerm.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/terms/ArithmeticTerm.java @@ -28,7 +28,7 @@ package at.ac.tuwien.kr.alpha.common.terms; import at.ac.tuwien.kr.alpha.common.Interner; -import at.ac.tuwien.kr.alpha.grounder.Substitution; +import at.ac.tuwien.kr.alpha.common.Substitution; import com.google.common.math.IntMath; import java.util.ArrayList; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/terms/ConstantTerm.java b/src/main/java/at/ac/tuwien/kr/alpha/common/terms/ConstantTerm.java index 71c2f524e..aa6514893 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/terms/ConstantTerm.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/terms/ConstantTerm.java @@ -1,7 +1,7 @@ package at.ac.tuwien.kr.alpha.common.terms; import at.ac.tuwien.kr.alpha.common.Interner; -import at.ac.tuwien.kr.alpha.grounder.Substitution; +import at.ac.tuwien.kr.alpha.common.Substitution; import java.util.Collections; import java.util.List; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/terms/FunctionTerm.java b/src/main/java/at/ac/tuwien/kr/alpha/common/terms/FunctionTerm.java index 9e3847ac4..3ec07ed96 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/terms/FunctionTerm.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/terms/FunctionTerm.java @@ -1,9 +1,13 @@ package at.ac.tuwien.kr.alpha.common.terms; import at.ac.tuwien.kr.alpha.common.Interner; -import at.ac.tuwien.kr.alpha.grounder.Substitution; +import at.ac.tuwien.kr.alpha.common.Substitution; -import java.util.*; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Collections; +import java.util.LinkedList; +import java.util.List; import static at.ac.tuwien.kr.alpha.Util.join; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/terms/IntervalTerm.java b/src/main/java/at/ac/tuwien/kr/alpha/common/terms/IntervalTerm.java index 8383b55ca..0e66b75db 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/terms/IntervalTerm.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/terms/IntervalTerm.java @@ -1,7 +1,35 @@ +/* + * Copyright (c) 2017, 2018, 2020, the Alpha Team. + * All rights reserved. + * + * Additional changes made by Siemens. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * 1) Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * 2) Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + package at.ac.tuwien.kr.alpha.common.terms; import at.ac.tuwien.kr.alpha.common.Interner; -import at.ac.tuwien.kr.alpha.grounder.Substitution; +import at.ac.tuwien.kr.alpha.common.Substitution; import java.util.LinkedList; import java.util.List; @@ -11,7 +39,6 @@ /** * An IntervalTerm represents the shorthand notation for a set of rules where all elements in this interval occur once, e.g., fact(2..5). * An IntervalTerm is a meta-term and the grounder must replace it with its corresponding set of facts or rules. - * Copyright (c) 2017, the Alpha Team. */ public class IntervalTerm extends Term { private static final Interner INTERNER = new Interner<>(); @@ -115,7 +142,23 @@ public int hashCode() { @Override public int compareTo(Term o) { - throw new UnsupportedOperationException("Intervals cannot be compared."); + if (this == o) { + return 0; + } + + if (!(o instanceof IntervalTerm)) { + return super.compareTo(o); + } + + IntervalTerm other = (IntervalTerm)o; + + int result = lowerBoundTerm.compareTo(other.lowerBoundTerm); + + if (result != 0) { + return result; + } + + return upperBoundTerm.compareTo(other.upperBoundTerm); } @Override diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/terms/Term.java b/src/main/java/at/ac/tuwien/kr/alpha/common/terms/Term.java index a619a108d..106a1d733 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/terms/Term.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/terms/Term.java @@ -1,6 +1,6 @@ package at.ac.tuwien.kr.alpha.common.terms; -import at.ac.tuwien.kr.alpha.grounder.Substitution; +import at.ac.tuwien.kr.alpha.common.Substitution; import java.util.ArrayList; import java.util.HashMap; @@ -51,8 +51,10 @@ private static int priority(Term term) { return 2; } else if (clazz.equals(VariableTerm.class)) { return 3; + } else if (clazz.equals(ArithmeticTerm.class)) { + return 4; } - throw new UnsupportedOperationException("Can only compare constant term, function terms and variable terms among each other."); + throw new UnsupportedOperationException("Can only compare constant term, function terms, variable terms, and arithmetic terms among each other."); } @Override diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/terms/VariableTerm.java b/src/main/java/at/ac/tuwien/kr/alpha/common/terms/VariableTerm.java index 8396b4102..6a6c09a71 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/terms/VariableTerm.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/terms/VariableTerm.java @@ -1,15 +1,40 @@ +/* + * Copyright (c) 2016-2018, 2020, the Alpha Team. + * All rights reserved. + * + * Additional changes made by Siemens. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * 1) Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * 2) Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + package at.ac.tuwien.kr.alpha.common.terms; import at.ac.tuwien.kr.alpha.common.Interner; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.grounder.IntIdGenerator; -import at.ac.tuwien.kr.alpha.grounder.Substitution; import java.util.Collections; import java.util.List; -/** - * Copyright (c) 2016-2017, the Alpha Team. - */ public class VariableTerm extends Term { private static final Interner INTERNER = new Interner<>(); @@ -23,6 +48,10 @@ private VariableTerm(String variableName) { } public static VariableTerm getInstance(String variableName) { + final char firstChar = variableName.charAt(0); + if (firstChar != ANONYMOUS_VARIABLE_PREFIX.charAt(0) && !Character.isUpperCase(firstChar)) { + throw new IllegalArgumentException("Variable name must start with upper-case letter or " + ANONYMOUS_VARIABLE_PREFIX); + } return INTERNER.intern(new VariableTerm(variableName)); } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java index c379e5f88..4344d44b1 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java @@ -37,6 +37,7 @@ import at.ac.tuwien.kr.alpha.common.Predicate; import at.ac.tuwien.kr.alpha.common.Program; import at.ac.tuwien.kr.alpha.common.Rule; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.atoms.Atom; import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; import at.ac.tuwien.kr.alpha.common.atoms.ComparisonLiteral; @@ -704,31 +705,6 @@ public void forgetAssignment(int[] atomIds) { throw new UnsupportedOperationException("Forgetting assignments is not implemented"); } - public static String groundAndPrintRule(NonGroundRule rule, Substitution substitution) { - StringBuilder ret = new StringBuilder(); - if (!rule.isConstraint()) { - Atom groundHead = rule.getHeadAtom().substitute(substitution); - ret.append(groundHead.toString()); - } - ret.append(" :- "); - boolean isFirst = true; - for (Atom bodyAtom : rule.getBodyAtomsPositive()) { - ret.append(groundLiteralToString(bodyAtom.toLiteral(), substitution, isFirst)); - isFirst = false; - } - for (Atom bodyAtom : rule.getBodyAtomsNegative()) { - ret.append(groundLiteralToString(bodyAtom.toLiteral(false), substitution, isFirst)); - isFirst = false; - } - ret.append("."); - return ret.toString(); - } - - static String groundLiteralToString(Literal literal, Substitution substitution, boolean isFirst) { - Literal groundLiteral = literal.substitute(substitution); - return (isFirst ? "" : ", ") + groundLiteral.toString(); - } - @Override public NonGroundRule getNonGroundRule(Integer ruleId) { return knownNonGroundRules.get(ruleId); diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGenerator.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGenerator.java index 72500f499..541ffad03 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGenerator.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGenerator.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2017-2018, the Alpha Team. +/* + * Copyright (c) 2017-2018, 2020, the Alpha Team. * All rights reserved. * * Additional changes made by Siemens. @@ -29,22 +29,34 @@ import at.ac.tuwien.kr.alpha.common.AtomStore; import at.ac.tuwien.kr.alpha.common.NoGood; +import at.ac.tuwien.kr.alpha.common.NonGroundNoGood; import at.ac.tuwien.kr.alpha.common.Predicate; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.atoms.Atom; import at.ac.tuwien.kr.alpha.common.atoms.FixedInterpretationLiteral; +import at.ac.tuwien.kr.alpha.common.atoms.Literal; import at.ac.tuwien.kr.alpha.grounder.atoms.EnumerationAtom; import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom; import at.ac.tuwien.kr.alpha.grounder.structure.ProgramAnalysis; -import java.util.*; +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashMap; +import java.util.HashSet; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; -import static at.ac.tuwien.kr.alpha.common.Literals.*; +import static at.ac.tuwien.kr.alpha.common.Literals.atomOf; +import static at.ac.tuwien.kr.alpha.common.Literals.atomToLiteral; +import static at.ac.tuwien.kr.alpha.common.Literals.negateLiteral; import static java.util.Collections.emptyList; import static java.util.Collections.singletonList; /** * Class to generate ground NoGoods out of non-ground rules and grounding substitutions. - * Copyright (c) 2017-2018, the Alpha Team. + * Copyright (c) 2017-2018, 2020, the Alpha Team. */ public class NoGoodGenerator { private final AtomStore atomStore; @@ -53,6 +65,8 @@ public class NoGoodGenerator { private final ProgramAnalysis programAnalysis; private final Set uniqueGroundRulePerGroundHead; + private final boolean conflictGeneralisationEnabled = true; // TODO: make parameterisable + NoGoodGenerator(AtomStore atomStore, ChoiceRecorder recorder, Map> factsFromProgram, ProgramAnalysis programAnalysis, Set uniqueGroundRulePerGroundHead) { this.atomStore = atomStore; this.choiceRecorder = recorder; @@ -72,16 +86,27 @@ public class NoGoodGenerator { * @return a list of the NoGoods corresponding to the ground rule. */ List generateNoGoodsFromGroundSubstitution(final NonGroundRule nonGroundRule, final Substitution substitution) { - final List posLiterals = collectPosLiterals(nonGroundRule, substitution); - final List negLiterals = collectNegLiterals(nonGroundRule, substitution); + final CollectedLiterals posLiterals = collectPosLiterals(nonGroundRule, substitution); + final CollectedLiterals negLiterals = collectNegLiterals(nonGroundRule, substitution); if (posLiterals == null || negLiterals == null) { return emptyList(); } + final Map mapGroundToNonGroundAtoms; + if (conflictGeneralisationEnabled) { + mapGroundToNonGroundAtoms = new HashMap<>(); + mapGroundToNonGroundAtoms.putAll(posLiterals.getAtomMapping()); + mapGroundToNonGroundAtoms.putAll(negLiterals.getAtomMapping()); + } + // A constraint is represented by exactly one nogood. if (nonGroundRule.isConstraint()) { - return singletonList(NoGood.fromConstraint(posLiterals, negLiterals)); + final NoGood ngConstraint = NoGood.fromConstraint(posLiterals.collectedGroundLiterals, negLiterals.collectedGroundLiterals); + if (conflictGeneralisationEnabled) { + ngConstraint.setNonGroundNoGood(NonGroundNoGood.fromBody(ngConstraint, posLiterals, negLiterals, mapGroundToNonGroundAtoms)); + } + return singletonList(ngConstraint); } final List result = new ArrayList<>(); @@ -90,7 +115,7 @@ List generateNoGoodsFromGroundSubstitution(final NonGroundRule nonGround final int headId = atomStore.putIfAbsent(groundHeadAtom); // Prepare atom representing the rule body. - final RuleAtom bodyAtom = new RuleAtom(nonGroundRule, substitution); + final RuleAtom bodyAtom = RuleAtom.ground(nonGroundRule, substitution); // Check uniqueness of ground rule by testing whether the // body representing atom already has an id. @@ -100,37 +125,58 @@ List generateNoGoodsFromGroundSubstitution(final NonGroundRule nonGround return emptyList(); } - final int bodyRepresentingLiteral = atomToLiteral(atomStore.putIfAbsent(bodyAtom)); + final int bodyRepresentingAtom = atomStore.putIfAbsent(bodyAtom); + final int bodyRepresentingLiteral = atomToLiteral(bodyRepresentingAtom); final int headLiteral = atomToLiteral(atomStore.putIfAbsent(nonGroundRule.getHeadAtom().substitute(substitution))); + if (conflictGeneralisationEnabled) { + mapGroundToNonGroundAtoms.put(headId, nonGroundRule.getHeadAtom()); + mapGroundToNonGroundAtoms.put(bodyRepresentingAtom, nonGroundRule.getNonGroundRuleAtom()); + } + choiceRecorder.addHeadToBody(headId, atomOf(bodyRepresentingLiteral)); // Create a nogood for the head. - result.add(NoGood.headFirst(negateLiteral(headLiteral), bodyRepresentingLiteral)); + final NoGood ngHead = NoGood.headFirst(negateLiteral(headLiteral), bodyRepresentingLiteral); + result.add(ngHead); + if (conflictGeneralisationEnabled) { + ngHead.setNonGroundNoGood(NonGroundNoGood.forGroundNoGood(ngHead, mapGroundToNonGroundAtoms)); + } - final NoGood ruleBody = NoGood.fromBody(posLiterals, negLiterals, bodyRepresentingLiteral); - result.add(ruleBody); + final NoGood ngWholeBody = NoGood.fromBody(posLiterals.collectedGroundLiterals, negLiterals.collectedGroundLiterals, bodyRepresentingLiteral); + if (conflictGeneralisationEnabled) { + ngWholeBody.setNonGroundNoGood(NonGroundNoGood.fromBody(ngWholeBody, posLiterals, negLiterals, mapGroundToNonGroundAtoms)); + } + result.add(ngWholeBody); // Nogoods such that the atom representing the body is true iff the body is true. - for (int j = 1; j < ruleBody.size(); j++) { - result.add(new NoGood(bodyRepresentingLiteral, negateLiteral(ruleBody.getLiteral(j)))); + for (int j = 1; j < ngWholeBody.size(); j++) { + final NoGood ngOneBodyLiteral = new NoGood(bodyRepresentingLiteral, negateLiteral(ngWholeBody.getLiteral(j))); + result.add(ngOneBodyLiteral); + if (conflictGeneralisationEnabled) { + ngOneBodyLiteral.setNonGroundNoGood(NonGroundNoGood.forGroundNoGood(ngOneBodyLiteral, mapGroundToNonGroundAtoms)); + } } // If the rule head is unique, add support. if (uniqueGroundRulePerGroundHead.contains(nonGroundRule)) { - result.add(NoGood.support(headLiteral, bodyRepresentingLiteral)); + final NoGood ngSupport = NoGood.support(headLiteral, bodyRepresentingLiteral); + if (conflictGeneralisationEnabled) { + ngSupport.setNonGroundNoGood(NonGroundNoGood.forGroundNoGood(ngSupport, mapGroundToNonGroundAtoms)); + } + result.add(ngSupport); } // If the body of the rule contains negation, add choices. - if (!negLiterals.isEmpty()) { - result.addAll(choiceRecorder.generateChoiceNoGoods(posLiterals, negLiterals, bodyRepresentingLiteral)); + if (!negLiterals.collectedGroundLiterals.isEmpty()) { + result.addAll(choiceRecorder.generateChoiceNoGoods(posLiterals.collectedGroundLiterals, negLiterals.collectedGroundLiterals, bodyRepresentingLiteral)); } return result; } - List collectNegLiterals(final NonGroundRule nonGroundRule, final Substitution substitution) { - final List bodyLiteralsNegative = new ArrayList<>(); + CollectedLiterals collectNegLiterals(final NonGroundRule nonGroundRule, final Substitution substitution) { + final CollectedLiterals collectedLiterals = new CollectedLiterals(); for (Atom atom : nonGroundRule.getBodyAtomsNegative()) { Atom groundAtom = atom.substitute(substitution); @@ -146,23 +192,27 @@ List collectNegLiterals(final NonGroundRule nonGroundRule, final Substi continue; } - bodyLiteralsNegative.add(atomToLiteral(atomStore.putIfAbsent(groundAtom))); + collectedLiterals.collectedGroundLiterals.add(atomToLiteral(atomStore.putIfAbsent(groundAtom))); + collectedLiterals.correspondingNonGroundLiterals.add(atom.toLiteral()); } - return bodyLiteralsNegative; + return collectedLiterals; } - private List collectPosLiterals(final NonGroundRule nonGroundRule, final Substitution substitution) { - final List bodyLiteralsPositive = new ArrayList<>(); + private CollectedLiterals collectPosLiterals(final NonGroundRule nonGroundRule, final Substitution substitution) { + final CollectedLiterals collectedLiterals = new CollectedLiterals(); for (Atom atom : nonGroundRule.getBodyAtomsPositive()) { - if (atom.toLiteral() instanceof FixedInterpretationLiteral) { + final Literal literal = atom.toLiteral(); + if (literal instanceof FixedInterpretationLiteral) { // TODO: conversion of atom to literal is ugly. NonGroundRule could manage atoms instead of literals, cf. FIXME there // Atom has fixed interpretation, hence was checked earlier that it // evaluates to true under the given substitution. // FixedInterpretationAtoms need not be shown to the solver, skip it. + collectedLiterals.skippedFixedInterpretationLiterals.add(literal); continue; } // Skip the special enumeration atom. if (atom instanceof EnumerationAtom) { + // TODO: ??? continue; } @@ -173,6 +223,7 @@ private List collectPosLiterals(final NonGroundRule nonGroundRule, fina Set factInstances = factsFromProgram.get(groundAtom.getPredicate()); if (factInstances != null && factInstances.contains(new Instance(groundAtom.getTerms()))) { // Skip positive atoms that are always true. + collectedLiterals.skippedFacts.add(literal); continue; } @@ -181,13 +232,61 @@ private List collectPosLiterals(final NonGroundRule nonGroundRule, fina return null; } - bodyLiteralsPositive.add(atomToLiteral(atomStore.putIfAbsent(groundAtom))); + collectedLiterals.collectedGroundLiterals.add(atomToLiteral(atomStore.putIfAbsent(groundAtom))); + collectedLiterals.correspondingNonGroundLiterals.add(literal); } - return bodyLiteralsPositive; + return collectedLiterals; } private boolean existsRuleWithPredicateInHead(final Predicate predicate) { final HashSet definingRules = programAnalysis.getPredicateDefiningRules().get(predicate); return definingRules != null && !definingRules.isEmpty(); } + + public static class CollectedLiterals { + private final List collectedGroundLiterals = new ArrayList<>(); + private final List correspondingNonGroundLiterals = new ArrayList<>(); + private final List skippedFixedInterpretationLiterals = new ArrayList<>(); + private final List skippedFacts = new ArrayList<>(); + + public CollectedLiterals() { + super(); + } + + public CollectedLiterals( + List collectedGroundLiterals, List correspondingNonGroundLiterals, + List skippedFixedInterpretationLiterals, List skippedFacts) { + this(); + this.collectedGroundLiterals.addAll(collectedGroundLiterals); + this.correspondingNonGroundLiterals.addAll(correspondingNonGroundLiterals); + this.skippedFixedInterpretationLiterals.addAll(skippedFixedInterpretationLiterals); + this.skippedFacts.addAll(skippedFacts); + } + + public List getCollectedGroundLiterals() { + return Collections.unmodifiableList(collectedGroundLiterals); + } + + public List getCorrespondingNonGroundLiterals() { + return Collections.unmodifiableList(correspondingNonGroundLiterals); + } + + public List getSkippedFixedInterpretationLiterals() { + return Collections.unmodifiableList(skippedFixedInterpretationLiterals); + } + + public List getSkippedFacts() { + return Collections.unmodifiableList(skippedFacts); + } + + public Map getAtomMapping() { + final Map atomMapping = new HashMap<>(); + for (int i = 0; i < collectedGroundLiterals.size(); i++) { + final int groundAtom = atomOf(collectedGroundLiterals.get(i)); + final Atom nonGroundAtom = correspondingNonGroundLiterals.get(i).getAtom(); + atomMapping.put(groundAtom, nonGroundAtom); + } + return atomMapping; + } + } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/NonGroundRule.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/NonGroundRule.java index f9cdbdf05..810d8bce4 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/NonGroundRule.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/NonGroundRule.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2016-2019, the Alpha Team. +/* + * Copyright (c) 2016-2020, the Alpha Team. * All rights reserved. * * Additional changes made by Siemens. @@ -32,17 +32,20 @@ import at.ac.tuwien.kr.alpha.common.Rule; import at.ac.tuwien.kr.alpha.common.atoms.Atom; import at.ac.tuwien.kr.alpha.common.atoms.Literal; +import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; +import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom; import java.util.ArrayList; import java.util.Collections; +import java.util.HashSet; import java.util.List; +import java.util.Set; import static at.ac.tuwien.kr.alpha.Util.join; import static at.ac.tuwien.kr.alpha.Util.oops; /** * Represents a non-ground rule or a constraint for the semi-naive grounder. - * Copyright (c) 2017-2018, the Alpha Team. */ public class NonGroundRule { static final IntIdGenerator ID_GENERATOR = new IntIdGenerator(); @@ -53,6 +56,7 @@ public class NonGroundRule { private final List bodyAtomsPositive; private final List bodyAtomsNegative; private final Atom headAtom; + private final RuleAtom nonGroundRuleAtom; final RuleGroundingOrders groundingOrder; @@ -69,6 +73,7 @@ private NonGroundRule(Rule rule, int ruleId, List bodyAtomsPositive, List< this.bodyAtomsNegative = Collections.unmodifiableList(bodyAtomsNegative); this.headAtom = headAtom; + this.nonGroundRuleAtom = RuleAtom.nonGround(this); checkSafety(); this.groundingOrder = new RuleGroundingOrders(this); @@ -120,6 +125,20 @@ public List getOccurringPredicates() { return predicateList; } + public Set getOccurringVariables() { + final Set occurringVariables = new HashSet<>(); + for (Atom posAtom : bodyAtomsPositive) { + occurringVariables.addAll(posAtom.getOccurringVariables()); + } + for (Atom negAtom : bodyAtomsNegative) { + occurringVariables.addAll(negAtom.getOccurringVariables()); + } + if (!isConstraint()) { + occurringVariables.addAll(headAtom.getOccurringVariables()); + } + return occurringVariables; + } + /** * Checks whether a rule is safe. A rule is safe iff all negated variables and all variables occurring in the * head also occur in the positive body). @@ -163,4 +182,8 @@ public List getBodyAtomsNegative() { public Atom getHeadAtom() { return headAtom; } + + public RuleAtom getNonGroundRuleAtom() { + return nonGroundRuleAtom; + } } \ No newline at end of file diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/BodyRepresentingLiteral.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/BodyRepresentingLiteral.java new file mode 100644 index 000000000..db1443891 --- /dev/null +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/BodyRepresentingLiteral.java @@ -0,0 +1,55 @@ +/* + * Copyright (c) 2020 Siemens AG + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * 1) Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * 2) Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +package at.ac.tuwien.kr.alpha.grounder.atoms; + +import at.ac.tuwien.kr.alpha.common.Substitution; +import at.ac.tuwien.kr.alpha.common.atoms.Literal; + +/** + * A literal containing a {@link RuleAtom} (only to be used internally, e.g., in {@link at.ac.tuwien.kr.alpha.common.NonGroundNoGood}s) + */ +public class BodyRepresentingLiteral extends Literal { + + public BodyRepresentingLiteral(RuleAtom atom, boolean positive) { + super(atom, positive); + } + + @Override + public RuleAtom getAtom() { + return (RuleAtom) super.getAtom(); + } + + @Override + public BodyRepresentingLiteral negate() { + return new BodyRepresentingLiteral(getAtom(), !positive); + } + + @Override + public BodyRepresentingLiteral substitute(Substitution substitution) { + return new BodyRepresentingLiteral(getAtom().substitute(substitution), positive); + } +} diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/ChoiceAtom.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/ChoiceAtom.java index bea727e50..6b369dacc 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/ChoiceAtom.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/ChoiceAtom.java @@ -28,11 +28,11 @@ package at.ac.tuwien.kr.alpha.grounder.atoms; import at.ac.tuwien.kr.alpha.common.Predicate; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.atoms.Atom; import at.ac.tuwien.kr.alpha.common.atoms.Literal; import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm; import at.ac.tuwien.kr.alpha.common.terms.Term; -import at.ac.tuwien.kr.alpha.grounder.Substitution; import java.util.Collections; import java.util.List; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/EnumerationAtom.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/EnumerationAtom.java index 8848b2845..7c229e5d2 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/EnumerationAtom.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/EnumerationAtom.java @@ -1,11 +1,11 @@ package at.ac.tuwien.kr.alpha.grounder.atoms; import at.ac.tuwien.kr.alpha.common.Predicate; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm; import at.ac.tuwien.kr.alpha.common.terms.Term; import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; -import at.ac.tuwien.kr.alpha.grounder.Substitution; import java.util.HashMap; import java.util.List; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/EnumerationLiteral.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/EnumerationLiteral.java index 46e82aa2b..be662a4cd 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/EnumerationLiteral.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/EnumerationLiteral.java @@ -1,9 +1,9 @@ package at.ac.tuwien.kr.alpha.grounder.atoms; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.atoms.BasicLiteral; import at.ac.tuwien.kr.alpha.common.terms.Term; import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; -import at.ac.tuwien.kr.alpha.grounder.Substitution; import java.util.Collections; import java.util.HashSet; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/IntervalAtom.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/IntervalAtom.java index 5832fc878..5acc36b55 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/IntervalAtom.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/IntervalAtom.java @@ -28,11 +28,11 @@ package at.ac.tuwien.kr.alpha.grounder.atoms; import at.ac.tuwien.kr.alpha.common.Predicate; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.atoms.Atom; import at.ac.tuwien.kr.alpha.common.atoms.VariableNormalizableAtom; import at.ac.tuwien.kr.alpha.common.terms.IntervalTerm; import at.ac.tuwien.kr.alpha.common.terms.Term; -import at.ac.tuwien.kr.alpha.grounder.Substitution; import java.util.Arrays; import java.util.List; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/IntervalLiteral.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/IntervalLiteral.java index 372594550..4582d6be3 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/IntervalLiteral.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/IntervalLiteral.java @@ -27,12 +27,12 @@ */ package at.ac.tuwien.kr.alpha.grounder.atoms; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.atoms.FixedInterpretationLiteral; import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm; import at.ac.tuwien.kr.alpha.common.terms.IntervalTerm; import at.ac.tuwien.kr.alpha.common.terms.Term; import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; -import at.ac.tuwien.kr.alpha.grounder.Substitution; import com.google.common.collect.Sets; import java.util.ArrayList; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/RuleAtom.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/RuleAtom.java index bd10713d6..2d9c055b6 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/RuleAtom.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/RuleAtom.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2016-2018, the Alpha Team. +/* + * Copyright (c) 2016-2018, 2020, the Alpha Team. * All rights reserved. * * Additional changes made by Siemens. @@ -28,15 +28,19 @@ package at.ac.tuwien.kr.alpha.grounder.atoms; import at.ac.tuwien.kr.alpha.common.Predicate; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.atoms.Atom; -import at.ac.tuwien.kr.alpha.common.atoms.Literal; -import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm; +import at.ac.tuwien.kr.alpha.common.terms.FunctionTerm; import at.ac.tuwien.kr.alpha.common.terms.Term; +import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; import at.ac.tuwien.kr.alpha.grounder.NonGroundRule; -import at.ac.tuwien.kr.alpha.grounder.Substitution; +import java.util.ArrayList; import java.util.Arrays; +import java.util.Collections; import java.util.List; +import java.util.Set; +import java.util.stream.Collectors; import static at.ac.tuwien.kr.alpha.common.terms.ConstantTerm.getInstance; @@ -47,21 +51,44 @@ public class RuleAtom implements Atom { public static final Predicate PREDICATE = Predicate.getInstance("_R_", 2, true, true); - private final List> terms; + private final List terms; + private final boolean ground; - private RuleAtom(List> terms) { + private RuleAtom(List terms, boolean ground) { if (terms.size() != 2) { throw new IllegalArgumentException(); } this.terms = terms; + this.ground = ground; } - public RuleAtom(NonGroundRule nonGroundRule, Substitution substitution) { - this(Arrays.asList( + /** + * Constructs a {@link RuleAtom} representing a ground rule. + * @param nonGroundRule a rule + * @param substitution a substitution that makes the rule ground + * @return a rule atom representing the ground rule + */ + public static RuleAtom ground(NonGroundRule nonGroundRule, Substitution substitution) { + return new RuleAtom(Arrays.asList( getInstance(Integer.toString(nonGroundRule.getRuleId())), getInstance(substitution.toString()) - )); + ), true); + } + + /** + * Constructs a {@link RuleAtom} representing a non-ground rule (to be used in {@link at.ac.tuwien.kr.alpha.common.NonGroundNoGood}s, for example). + * @param nonGroundRule a rule + * @return a rule atom representing the non-ground rule which contains all the variables occurring in the rule + */ + public static RuleAtom nonGround(NonGroundRule nonGroundRule) { + final Set occurringVariables = nonGroundRule.getOccurringVariables(); + final List sortedVariables = new ArrayList<>(occurringVariables); + Collections.sort(sortedVariables); + return new RuleAtom(Arrays.asList( + getInstance(Integer.toString(nonGroundRule.getRuleId())), + FunctionTerm.getInstance("", sortedVariables) + ), false); } @Override @@ -79,18 +106,23 @@ public List getTerms() { @Override public boolean isGround() { - // NOTE: Both terms are ConstantTerms, which are ground by definition. - return true; + return ground; } @Override - public Literal toLiteral(boolean positive) { - throw new UnsupportedOperationException("RuleAtom cannot be literalized"); + public BodyRepresentingLiteral toLiteral(boolean positive) { + return new BodyRepresentingLiteral(this, positive); } @Override - public Atom substitute(Substitution substitution) { - return this; + public RuleAtom substitute(Substitution substitution) { + if (ground) { + return this; + } else { + return new RuleAtom(terms.stream() + .map(t -> t.substitute(substitution)) + .collect(Collectors.toList()), false); + } } @Override diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/parser/ProgramPartParser.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/parser/ProgramPartParser.java new file mode 100644 index 000000000..56593b6a3 --- /dev/null +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/parser/ProgramPartParser.java @@ -0,0 +1,80 @@ +/* + * Copyright (c) 2018-2020, the Alpha Team. + * All rights reserved. + * + * Additional changes made by Siemens. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * 1) Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * 2) Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +package at.ac.tuwien.kr.alpha.grounder.parser; + +import at.ac.tuwien.kr.alpha.antlr.ASPCore2Lexer; +import at.ac.tuwien.kr.alpha.antlr.ASPCore2Parser; +import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; +import at.ac.tuwien.kr.alpha.common.atoms.Literal; +import at.ac.tuwien.kr.alpha.common.terms.Term; +import org.antlr.v4.runtime.CharStreams; +import org.antlr.v4.runtime.CommonTokenStream; +import org.antlr.v4.runtime.ParserRuleContext; +import org.antlr.v4.runtime.RecognitionException; +import org.antlr.v4.runtime.misc.ParseCancellationException; + +import java.util.Collections; + +/** + * A parser that, in contrast to {@link ProgramParser}, does not parse full programs but only program parts like + * atoms, terms and such. + */ +public class ProgramPartParser { + private final ParseTreeVisitor visitor = new ParseTreeVisitor(Collections.emptyMap(), true); + + public Term parseTerm(String s) { + final ASPCore2Parser parser = getASPCore2Parser(s); + return (Term)parse(parser.term()); + } + + public BasicAtom parseBasicAtom(String s) { + final ASPCore2Parser parser = getASPCore2Parser(s); + return (BasicAtom)parse(parser.classical_literal()); + } + + public Literal parseLiteral(String s) { + final ASPCore2Parser parser = getASPCore2Parser(s); + return (Literal)parse(parser.naf_literal()); + } + + private ASPCore2Parser getASPCore2Parser(String s) { + return new ASPCore2Parser(new CommonTokenStream(new ASPCore2Lexer(CharStreams.fromString(s)))); + } + + private Object parse(ParserRuleContext context) { + try { + return visitor.visit(context); + } catch (RecognitionException | ParseCancellationException e) { + // If there were issues parsing the given string, we + // throw something that suggests that the input string + // is malformed. + throw new IllegalArgumentException("Could not parse term.", e); + } + } +} diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustified.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustified.java index 8f17cbe11..eefaa4dc2 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustified.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustified.java @@ -1,19 +1,64 @@ +/* + * Copyright (c) 2018-2020, the Alpha Team. + * All rights reserved. + * + * Additional changes made by Siemens. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * 1) Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * 2) Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + package at.ac.tuwien.kr.alpha.grounder.structure; -import at.ac.tuwien.kr.alpha.common.*; -import at.ac.tuwien.kr.alpha.common.atoms.*; -import at.ac.tuwien.kr.alpha.grounder.*; +import at.ac.tuwien.kr.alpha.common.Assignment; +import at.ac.tuwien.kr.alpha.common.AtomStore; +import at.ac.tuwien.kr.alpha.common.DisjunctiveHead; +import at.ac.tuwien.kr.alpha.common.Predicate; +import at.ac.tuwien.kr.alpha.common.Rule; +import at.ac.tuwien.kr.alpha.common.Unification; +import at.ac.tuwien.kr.alpha.common.Unifier; +import at.ac.tuwien.kr.alpha.common.atoms.Atom; +import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; +import at.ac.tuwien.kr.alpha.common.atoms.ComparisonLiteral; +import at.ac.tuwien.kr.alpha.common.atoms.FixedInterpretationLiteral; +import at.ac.tuwien.kr.alpha.common.atoms.Literal; +import at.ac.tuwien.kr.alpha.grounder.Instance; +import at.ac.tuwien.kr.alpha.grounder.NonGroundRule; import at.ac.tuwien.kr.alpha.solver.ThriceTruth; import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.util.*; +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashSet; +import java.util.Iterator; +import java.util.LinkedHashMap; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Map; +import java.util.NoSuchElementException; +import java.util.Set; import static at.ac.tuwien.kr.alpha.Util.oops; -/** - * Copyright (c) 2018, the Alpha Team. - */ public class AnalyzeUnjustified { private static final Logger LOGGER = LoggerFactory.getLogger(AnalyzeUnjustified.class); private final ProgramAnalysis programAnalysis; @@ -304,7 +349,7 @@ private List rulesHeadUnifyingWith(Atom p) { List rulesWithUnifier = new ArrayList<>(); Predicate predicate = p.getPredicate(); // Check if literal is built-in with a fixed interpretation. - if (p instanceof FixedInterpretationLiteral) { + if (p.toLiteral() instanceof FixedInterpretationLiteral) { return Collections.emptyList(); } ArrayList definingRulesAndFacts = new ArrayList<>(); diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/LitSet.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/LitSet.java index 2e415af08..6c57cebfe 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/LitSet.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/LitSet.java @@ -1,9 +1,9 @@ package at.ac.tuwien.kr.alpha.grounder.structure; +import at.ac.tuwien.kr.alpha.common.Unification; +import at.ac.tuwien.kr.alpha.common.Unifier; import at.ac.tuwien.kr.alpha.common.atoms.Atom; import at.ac.tuwien.kr.alpha.common.atoms.VariableNormalizableAtom; -import at.ac.tuwien.kr.alpha.grounder.Unifier; -import at.ac.tuwien.kr.alpha.grounder.Unification; import java.util.Collections; import java.util.HashSet; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/transformation/CardinalityNormalization.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/transformation/CardinalityNormalization.java index 21b301a5f..dc31f1766 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/transformation/CardinalityNormalization.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/transformation/CardinalityNormalization.java @@ -1,17 +1,28 @@ package at.ac.tuwien.kr.alpha.grounder.transformation; -import at.ac.tuwien.kr.alpha.common.*; -import at.ac.tuwien.kr.alpha.common.atoms.*; +import at.ac.tuwien.kr.alpha.common.DisjunctiveHead; +import at.ac.tuwien.kr.alpha.common.Program; +import at.ac.tuwien.kr.alpha.common.Rule; +import at.ac.tuwien.kr.alpha.common.Substitution; +import at.ac.tuwien.kr.alpha.common.Unifier; +import at.ac.tuwien.kr.alpha.common.atoms.AggregateAtom; +import at.ac.tuwien.kr.alpha.common.atoms.AggregateLiteral; +import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; +import at.ac.tuwien.kr.alpha.common.atoms.Literal; import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm; import at.ac.tuwien.kr.alpha.common.terms.FunctionTerm; import at.ac.tuwien.kr.alpha.common.terms.Term; import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; -import at.ac.tuwien.kr.alpha.grounder.Substitution; -import at.ac.tuwien.kr.alpha.grounder.Unifier; import at.ac.tuwien.kr.alpha.grounder.atoms.EnumerationAtom; import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser; -import java.util.*; +import java.util.ArrayList; +import java.util.Collection; +import java.util.Collections; +import java.util.HashSet; +import java.util.Iterator; +import java.util.LinkedHashSet; +import java.util.List; /** * Copyright (c) 2017, the Alpha Team. diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/transformation/SumNormalization.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/transformation/SumNormalization.java index 3f69906d7..841ad3988 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/transformation/SumNormalization.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/transformation/SumNormalization.java @@ -3,16 +3,23 @@ import at.ac.tuwien.kr.alpha.common.DisjunctiveHead; import at.ac.tuwien.kr.alpha.common.Program; import at.ac.tuwien.kr.alpha.common.Rule; -import at.ac.tuwien.kr.alpha.common.atoms.*; +import at.ac.tuwien.kr.alpha.common.Unifier; +import at.ac.tuwien.kr.alpha.common.atoms.AggregateAtom; +import at.ac.tuwien.kr.alpha.common.atoms.AggregateLiteral; +import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; +import at.ac.tuwien.kr.alpha.common.atoms.Literal; import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm; import at.ac.tuwien.kr.alpha.common.terms.FunctionTerm; import at.ac.tuwien.kr.alpha.common.terms.Term; import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; -import at.ac.tuwien.kr.alpha.grounder.Unifier; import at.ac.tuwien.kr.alpha.grounder.atoms.EnumerationAtom; import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser; -import java.util.*; +import java.util.ArrayList; +import java.util.Collection; +import java.util.Collections; +import java.util.Iterator; +import java.util.List; import static at.ac.tuwien.kr.alpha.grounder.transformation.PredicateInternalizer.makePredicatesInternal; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/transformation/VariableEqualityRemoval.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/transformation/VariableEqualityRemoval.java index 8529f4775..82fd034e4 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/transformation/VariableEqualityRemoval.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/transformation/VariableEqualityRemoval.java @@ -30,14 +30,19 @@ import at.ac.tuwien.kr.alpha.common.DisjunctiveHead; import at.ac.tuwien.kr.alpha.common.Program; import at.ac.tuwien.kr.alpha.common.Rule; +import at.ac.tuwien.kr.alpha.common.Unifier; import at.ac.tuwien.kr.alpha.common.atoms.Atom; import at.ac.tuwien.kr.alpha.common.atoms.ComparisonLiteral; import at.ac.tuwien.kr.alpha.common.atoms.Literal; import at.ac.tuwien.kr.alpha.common.terms.Term; import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; -import at.ac.tuwien.kr.alpha.grounder.Unifier; -import java.util.*; +import java.util.Arrays; +import java.util.HashMap; +import java.util.HashSet; +import java.util.Iterator; +import java.util.LinkedHashSet; +import java.util.Map; /** * Removes variable equalities from rules by replacing one variable with the other. diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/Antecedent.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/Antecedent.java index c841ecc0e..0c8b907b0 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/Antecedent.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/Antecedent.java @@ -1,12 +1,43 @@ +/* + * Copyright (c) 2019-2020, the Alpha Team. + * All rights reserved. + * + * Additional changes made by Siemens. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * 1) Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * 2) Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ package at.ac.tuwien.kr.alpha.solver; +import at.ac.tuwien.kr.alpha.common.NoGood; + +import java.util.Iterator; + /** * An interface to reasons of implications as used internally by the solver. This is a lightweight {@link at.ac.tuwien.kr.alpha.common.NoGood} that only * provides an array of literals (in some order) and has an activity that may change. * - * Copyright (c) 2019, the Alpha Team. + * Copyright (c) 2019-2020, the Alpha Team. */ -public interface Antecedent { +public interface Antecedent extends Iterable { int[] getReasonLiterals(); @@ -14,4 +45,33 @@ public interface Antecedent { void decreaseActivity(); + /** + * Gets the {@link NoGood} from which this Antecedent has been created + * @return the original nogood, if known, else {@code null}. + */ + default NoGood getOriginalNoGood() { + return null; + } + + @Override + default Iterator iterator() { + return new Iterator() { + private int i; + private int[] literals = getReasonLiterals(); + + @Override + public boolean hasNext() { + return literals.length > i; + } + + @Override + public Integer next() { + return literals[i++]; + } + }; + } + + default int size() { + return getReasonLiterals().length; + } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/Atoms.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/Atoms.java index b0d26b58b..d43a08fd9 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/Atoms.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/Atoms.java @@ -1,6 +1,37 @@ +/* + * Copyright (c) 2017, 2020, the Alpha Team. + * All rights reserved. + * + * Additional changes made by Siemens. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * 1) Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * 2) Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + package at.ac.tuwien.kr.alpha.solver; public final class Atoms { + + public static final int FALSUM = 0; + public static boolean isAtom(int atom) { return atom >= 0; } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java index c8e9391da..af94937a3 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2016-2019, the Alpha Team. +/* + * Copyright (c) 2016-2020, the Alpha Team. * All rights reserved. * * Additional changes made by Siemens. @@ -32,6 +32,7 @@ import at.ac.tuwien.kr.alpha.common.AtomStore; import at.ac.tuwien.kr.alpha.common.NoGood; import at.ac.tuwien.kr.alpha.common.Rule; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.atoms.Atom; import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; import at.ac.tuwien.kr.alpha.common.atoms.ComparisonAtom; @@ -41,14 +42,16 @@ import at.ac.tuwien.kr.alpha.grounder.Grounder; import at.ac.tuwien.kr.alpha.grounder.NonGroundRule; import at.ac.tuwien.kr.alpha.grounder.ProgramAnalyzingGrounder; -import at.ac.tuwien.kr.alpha.grounder.Substitution; import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom; import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristic; import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristicFactory; import at.ac.tuwien.kr.alpha.solver.heuristics.ChainedBranchingHeuristics; import at.ac.tuwien.kr.alpha.solver.heuristics.HeuristicsConfiguration; import at.ac.tuwien.kr.alpha.solver.heuristics.NaiveHeuristic; +import at.ac.tuwien.kr.alpha.solver.learning.ConflictAnalysisResult; +import at.ac.tuwien.kr.alpha.solver.learning.ConflictNoGoodLearner; import at.ac.tuwien.kr.alpha.solver.learning.GroundConflictNoGoodLearner; +import at.ac.tuwien.kr.alpha.solver.learning.NonGroundConflictNoGoodLearner; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -71,7 +74,7 @@ import static at.ac.tuwien.kr.alpha.solver.NoGoodStore.LBD_NO_VALUE; import static at.ac.tuwien.kr.alpha.solver.ThriceTruth.MBT; import static at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristic.DEFAULT_CHOICE_LITERAL; -import static at.ac.tuwien.kr.alpha.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult.UNSAT; +import static at.ac.tuwien.kr.alpha.solver.learning.ConflictAnalysisResult.UNSAT; /** * The new default solver employed in Alpha. @@ -85,7 +88,7 @@ public class DefaultSolver extends AbstractSolver implements SolverMaintainingSt private final ChoiceManager choiceManager; private final WritableAssignment assignment; - private final GroundConflictNoGoodLearner learner; + private final ConflictNoGoodLearner learner; private final BranchingHeuristic branchingHeuristic; @@ -97,14 +100,18 @@ public class DefaultSolver extends AbstractSolver implements SolverMaintainingSt private final boolean disableNoGoodDeletion; private final PerformanceLog performanceLog; - + + private final boolean conflictGeneralisationEnabled = true; // TODO: make parameterisable + private static final int STOP_AFTER_BACKJUMPS = 1000; // TODO: make parameterisable + public DefaultSolver(AtomStore atomStore, Grounder grounder, NoGoodStore store, WritableAssignment assignment, Random random, SystemConfig config, HeuristicsConfiguration heuristicsConfiguration) { super(atomStore, grounder); this.assignment = assignment; this.store = store; this.choiceManager = new ChoiceManager(assignment, store); - this.learner = new GroundConflictNoGoodLearner(assignment, atomStore); + final GroundConflictNoGoodLearner groundLearner = new GroundConflictNoGoodLearner(assignment, atomStore); + this.learner = conflictGeneralisationEnabled ? new NonGroundConflictNoGoodLearner(assignment, atomStore, groundLearner) : groundLearner; this.branchingHeuristic = chainFallbackHeuristic(grounder, assignment, random, heuristicsConfiguration); this.disableJustifications = config.isDisableJustificationSearch(); this.disableNoGoodDeletion = config.isDisableNoGoodDeletion(); @@ -179,7 +186,10 @@ protected boolean tryAdvance(Consumer action) { // TODO: The violatedNoGood should not be necessary here, but this requires major type changes in heuristics. branchingHeuristic.violatedNoGood(violatedNoGood); if (!afterAllAtomsAssigned) { - if (!learnBackjumpAddFromConflict(conflictCause)) { + if (getNumberOfBackjumps() >= STOP_AFTER_BACKJUMPS) { + LOGGER.info("Stopping conflict generalisation after {} conflicts", STOP_AFTER_BACKJUMPS); + } + if (getNumberOfBackjumps() >= STOP_AFTER_BACKJUMPS || !learnBackjumpAddFromConflict(conflictCause)) { logStats(); return false; } @@ -253,7 +263,7 @@ private boolean addAndBackjumpIfNecessary(int noGoodId, NoGood noGood, int lbd) * @return false iff the analysis result shows that the set of NoGoods is unsatisfiable. */ private boolean learnBackjumpAddFromConflict(ConflictCause conflictCause) { - GroundConflictNoGoodLearner.ConflictAnalysisResult analysisResult = learner.analyzeConflictingNoGood(conflictCause.getAntecedent()); + ConflictAnalysisResult analysisResult = learner.analyzeConflictingNoGood(conflictCause.getAntecedent()); LOGGER.debug("Analysis result: {}", analysisResult); @@ -496,7 +506,7 @@ private boolean ingest(Map obtained) { private NoGood fixContradiction(Map.Entry noGoodEntry, ConflictCause conflictCause) { LOGGER.debug("Attempting to fix violation of {} caused by {}", noGoodEntry.getValue(), conflictCause); - GroundConflictNoGoodLearner.ConflictAnalysisResult conflictAnalysisResult = learner.analyzeConflictFromAddingNoGood(conflictCause.getAntecedent()); + ConflictAnalysisResult conflictAnalysisResult = learner.analyzeConflictFromAddingNoGood(conflictCause.getAntecedent()); if (conflictAnalysisResult == UNSAT) { return NoGood.UNSAT; } @@ -575,7 +585,7 @@ public int getNumberOfDeletedNoGoods() { } @Override - public NoGoodCounter getNoGoodCounter() { + public NoGoodCounter getNoGoodCounter() { return store.getNoGoodCounter(); } @@ -588,11 +598,18 @@ private void logStats() { LOGGER.debug("{}: {}", heuristicToDecisionCounter.getKey(), heuristicToDecisionCounter.getValue()); } } - NoGoodCounter noGoodCounter = store.getNoGoodCounter(); + final NoGoodCounter noGoodCounter = store.getNoGoodCounter(); LOGGER.debug("Number of NoGoods by type: {}", noGoodCounter.getStatsByType()); LOGGER.debug("Number of NoGoods by cardinality: {}", noGoodCounter.getStatsByCardinality()); AtomCounter atomCounter = atomStore.getAtomCounter(); LOGGER.debug("Number of atoms by type: {}", atomCounter.getStatsByType()); } + logLearnedNonGroundNoGoods(); + } + + private void logLearnedNonGroundNoGoods() { + if (learner instanceof NonGroundConflictNoGoodLearner) { + ((NonGroundConflictNoGoodLearner)learner).logLearnedConstraints(); + } } } \ No newline at end of file diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStore.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStore.java index 28af2719c..57208a832 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStore.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStore.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2017-2019, the Alpha Team. +/* + * Copyright (c) 2017-2020, the Alpha Team. * All rights reserved. * * Additional changes made by Siemens. @@ -33,15 +33,19 @@ import java.util.HashMap; -import static at.ac.tuwien.kr.alpha.common.Literals.*; -import static at.ac.tuwien.kr.alpha.solver.ThriceTruth.*; +import static at.ac.tuwien.kr.alpha.common.Literals.atomOf; +import static at.ac.tuwien.kr.alpha.common.Literals.isNegated; +import static at.ac.tuwien.kr.alpha.common.Literals.isPositive; +import static at.ac.tuwien.kr.alpha.solver.ThriceTruth.FALSE; +import static at.ac.tuwien.kr.alpha.solver.ThriceTruth.MBT; +import static at.ac.tuwien.kr.alpha.solver.ThriceTruth.TRUE; public class NaiveNoGoodStore implements NoGoodStore { private static final Logger LOGGER = LoggerFactory.getLogger(NaiveNoGoodStore.class); private HashMap delegate = new HashMap<>(); private final WritableAssignment assignment; - private final NoGoodCounter counter = new NoGoodCounter(); + private final NoGoodCounter counter = new NoGoodCounter<>(); private boolean hasInferredAssignments; @@ -134,7 +138,7 @@ public void growForMaxAtomId(int maxAtomId) { } @Override - public NoGoodCounter getNoGoodCounter() { + public NoGoodCounter getNoGoodCounter() { return counter; } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodCounter.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodCounter.java index 432419ab1..b3d0c53ef 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodCounter.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodCounter.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2019 Siemens AG +/* + * Copyright (c) 2019-2020 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -26,8 +26,8 @@ package at.ac.tuwien.kr.alpha.solver; import at.ac.tuwien.kr.alpha.common.NoGood; -import at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type; import at.ac.tuwien.kr.alpha.common.NoGoodInterface; +import at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type; import java.util.ArrayList; import java.util.List; @@ -35,7 +35,7 @@ /** * Maintains statistics on numbers of various types of {@link NoGood}s. */ -public class NoGoodCounter { +public class NoGoodCounter { private static final int CARD_NARY = 0; private static final int CARD_UNARY = 1; @@ -48,7 +48,7 @@ public class NoGoodCounter { * Increases counters for the types of the given NoGood * @param noGood */ - void add(NoGoodInterface noGood) { + void add(NoGoodInterface noGood) { countByType[noGood.getType().ordinal()]++; countByCardinality[getAbstractCardinality(noGood)]++; } @@ -57,12 +57,12 @@ void add(NoGoodInterface noGood) { * Decreases counters for the types of the given NoGood * @param noGood */ - void remove(NoGoodInterface noGood) { + void remove(NoGoodInterface noGood) { countByType[noGood.getType().ordinal()]--; countByCardinality[getAbstractCardinality(noGood)]--; } - private int getAbstractCardinality(NoGoodInterface noGood) { + private int getAbstractCardinality(NoGoodInterface noGood) { if (noGood.isUnary()) { return CARD_UNARY; } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java index 7cd516b40..b83922672 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java @@ -1,3 +1,30 @@ +/* + * Copyright (c) 2016-2020, the Alpha Team. + * All rights reserved. + * + * Additional changes made by Siemens. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * 1) Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * 2) Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ package at.ac.tuwien.kr.alpha.solver; import at.ac.tuwien.kr.alpha.common.NoGood; @@ -54,5 +81,5 @@ public interface NoGoodStore { */ void cleanupLearnedNoGoods(); - NoGoodCounter getNoGoodCounter(); + NoGoodCounter getNoGoodCounter(); } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java index e2f256c5d..7f35fd250 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java @@ -83,7 +83,9 @@ public class NoGoodStoreAlphaRoaming implements NoGoodStore, BinaryNoGoodPropaga private boolean didPropagate; private boolean hasBinaryNoGoods; - private final NoGoodCounter counter = new NoGoodCounter(); + private final NoGoodCounter counter = new NoGoodCounter<>(); + + private final boolean conflictGeneralisationEnabled = true; // TODO: make parameterisable public NoGoodStoreAlphaRoaming(WritableAssignment assignment, boolean checksEnabled) { this.assignment = assignment; @@ -149,7 +151,7 @@ public void growForMaxAtomId(int maxAtomId) { } @Override - public NoGoodCounter getNoGoodCounter() { + public NoGoodCounter getNoGoodCounter() { return counter; } @@ -425,13 +427,13 @@ private ConflictCause addAndWatchBinary(final NoGood noGood) { return null; } - private ConflictCause assignWeakComplement(final int literalIndex, final NoGoodInterface impliedBy, int decisionLevel) { + private ConflictCause assignWeakComplement(final int literalIndex, final NoGoodInterface impliedBy, int decisionLevel) { final int literal = impliedBy.getLiteral(literalIndex); ThriceTruth truth = isNegated(literal) ? MBT : FALSE; return assignTruth(atomOf(literal), truth, impliedBy.asAntecedent(), decisionLevel); } - private ConflictCause assignStrongComplement(final NoGoodInterface impliedBy, int decisionLevel) { + private ConflictCause assignStrongComplement(final NoGoodInterface impliedBy, int decisionLevel) { return assignTruth(atomOf(impliedBy.getHead()), TRUE, impliedBy.asAntecedent(), decisionLevel); } @@ -678,6 +680,8 @@ class BinaryWatchList implements ShallowAntecedent { private int noGoodsWithHeadSize; private final int forLiteral; + private final Map originalNoGoods = new HashMap<>(); + private BinaryWatchList(int forLiteral) { this.forLiteral = forLiteral; } @@ -702,6 +706,7 @@ private ConflictCause addHeadedNoGood(NoGood noGood) { throw oops("NoGood has wrong head."); } noGoodsWithHead[noGoodsWithHeadSize++] = otherLiteral; + addOriginalNoGoodIfConflictGeneralisationEnabled(otherLiteral, noGood); // Assign (weakly) otherLiteral if the newly added NoGood is unit. ThriceTruth literalTruth = assignment.getTruth(atomOf(forLiteral)); if (literalTruth != null && literalTruth.toBoolean() == isPositive(forLiteral)) { @@ -725,6 +730,7 @@ private ConflictCause addOrdinaryNoGood(NoGood noGood) { } int otherLiteral = noGood.getLiteral(0) == forLiteral ? noGood.getLiteral(1) : noGood.getLiteral(0); noGoodsWithoutHead[noGoodsWithoutHeadSize++] = otherLiteral; + addOriginalNoGoodIfConflictGeneralisationEnabled(otherLiteral, noGood); // Assign otherLiteral if the newly added NoGood is unit. ThriceTruth literalTruth = assignment.getTruth(atomOf(forLiteral)); if (literalTruth != null && literalTruth.toBoolean() == isPositive(forLiteral)) { @@ -764,6 +770,23 @@ ConflictCause propagateStrongly() { } return null; } + + private void addOriginalNoGoodIfConflictGeneralisationEnabled(int otherLiteral, NoGood noGood) { + if (conflictGeneralisationEnabled) { + final NoGood originalNoGood = originalNoGoods.get(otherLiteral); + if (originalNoGood != null && !originalNoGood.equals(noGood)) { + if (checksEnabled && !originalNoGood.withoutHead().equals(noGood.withoutHead())) { + throw oops("Unexpected nogood for literals " + literalToString(forLiteral) + " and " + literalToString(otherLiteral) + ": " + noGood + " (already stored: " + originalNoGood + ")"); + } + if (noGood.hasHead()) { + // if two nogoods have the same literals, prefer the one with head because it contains more information + originalNoGoods.put(otherLiteral, noGood); + } + } else { + originalNoGoods.put(otherLiteral, noGood); + } + } + } public int size() { return noGoodsWithHeadSize + noGoodsWithoutHeadSize; @@ -800,6 +823,11 @@ public void bumpActivity() { public void decreaseActivity() { } + @Override + public NoGood getOriginalNoGood() { + return originalNoGoods.get(literals[0]); + } + @Override public String toString() { return "{" + literalToString(literals[0]) + ", " + literalToString(literals[1]) + "}"; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverMaintainingStatistics.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverMaintainingStatistics.java index 0c29abef7..2d2fddcff 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverMaintainingStatistics.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverMaintainingStatistics.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2017-2019 Siemens AG +/* + * Copyright (c) 2017-2020 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -46,7 +46,7 @@ public interface SolverMaintainingStatistics { */ int getNumberOfConflictsAfterClosing(); - NoGoodCounter getNoGoodCounter(); + NoGoodCounter getNoGoodCounter(); default String getStatisticsString() { return "g=" + getNumberOfChoices() + ", bt=" + getNumberOfBacktracks() + ", bj=" + getNumberOfBackjumps() + ", bt_within_bj=" diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java index 4395d9ed5..155af2b7f 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java @@ -35,13 +35,14 @@ import static at.ac.tuwien.kr.alpha.Util.oops; import static at.ac.tuwien.kr.alpha.common.Literals.literalToString; -public final class WatchedNoGood implements NoGoodInterface, Antecedent { +public final class WatchedNoGood implements NoGoodInterface, Antecedent { private int activity; private final int[] literals; private int alpha; private int head; private final Type type; private boolean isLbdLessOrEqual2; + private final NoGood originalNoGood; WatchedNoGood(NoGood noGood, int a, int b, int alpha) { if (noGood.size() < 3) { @@ -63,6 +64,7 @@ public final class WatchedNoGood implements NoGoodInterface, Antecedent { swap(1, b); } this.type = noGood.getType(); + this.originalNoGood = noGood; } private void checkPointers(int a, int b, int alpha) { @@ -99,7 +101,7 @@ public boolean hasHead() { } @Override - public int getHead() { + public Integer getHead() { return literals[head]; } @@ -115,7 +117,7 @@ void setWatch(int index, int value) { } @Override - public int getLiteral(int index) { + public Integer getLiteral(int index) { return literals[index]; } @@ -161,6 +163,11 @@ public Integer next() { }; } + @Override + public NoGood getOriginalNoGood() { + return originalNoGood; + } + @Override public String toString() { StringBuilder sb = new StringBuilder(); diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMin.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMin.java index 48e523932..d01f623e5 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMin.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMin.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2016-2019 Siemens AG +/* + * Copyright (c) 2016-2020 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -30,11 +30,16 @@ import at.ac.tuwien.kr.alpha.common.NoGood; import at.ac.tuwien.kr.alpha.solver.ChoiceManager; import at.ac.tuwien.kr.alpha.solver.ThriceTruth; -import at.ac.tuwien.kr.alpha.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult; +import at.ac.tuwien.kr.alpha.solver.learning.ConflictAnalysisResult; import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.util.*; +import java.util.ArrayDeque; +import java.util.Comparator; +import java.util.Deque; +import java.util.LinkedHashMap; +import java.util.Map; +import java.util.Random; import java.util.stream.Stream; import static at.ac.tuwien.kr.alpha.common.Literals.atomOf; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristic.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristic.java index 78be2e6de..8fa3f6f43 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristic.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristic.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2016, 2018-2019 Siemens AG +/* + * Copyright (c) 2016, 2018-2020 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -26,7 +26,7 @@ package at.ac.tuwien.kr.alpha.solver.heuristics; import at.ac.tuwien.kr.alpha.common.NoGood; -import at.ac.tuwien.kr.alpha.solver.learning.GroundConflictNoGoodLearner; +import at.ac.tuwien.kr.alpha.solver.learning.ConflictAnalysisResult; import java.util.Collection; @@ -56,7 +56,7 @@ public interface BranchingHeuristic { * * @param analysisResult */ - void analyzedConflict(GroundConflictNoGoodLearner.ConflictAnalysisResult analysisResult); + void analyzedConflict(ConflictAnalysisResult analysisResult); /** * Stores a newly grounded {@link NoGood} and updates associated activity counters. diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ChainedBranchingHeuristics.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ChainedBranchingHeuristics.java index 6d6eb8761..902f1dc85 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ChainedBranchingHeuristics.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ChainedBranchingHeuristics.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2018-2019 Siemens AG +/* + * Copyright (c) 2018-2020 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -26,9 +26,13 @@ package at.ac.tuwien.kr.alpha.solver.heuristics; import at.ac.tuwien.kr.alpha.common.NoGood; -import at.ac.tuwien.kr.alpha.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult; +import at.ac.tuwien.kr.alpha.solver.learning.ConflictAnalysisResult; -import java.util.*; +import java.util.Arrays; +import java.util.HashMap; +import java.util.LinkedList; +import java.util.List; +import java.util.Map; import static at.ac.tuwien.kr.alpha.Util.oops; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/DependencyDrivenHeuristic.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/DependencyDrivenHeuristic.java index e24f29da0..95739de0d 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/DependencyDrivenHeuristic.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/DependencyDrivenHeuristic.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2017-2019 Siemens AG +/* + * Copyright (c) 2017-2020 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -33,17 +33,28 @@ import at.ac.tuwien.kr.alpha.solver.heuristics.activity.BodyActivityProvider; import at.ac.tuwien.kr.alpha.solver.heuristics.activity.BodyActivityProviderFactory; import at.ac.tuwien.kr.alpha.solver.heuristics.activity.BodyActivityProviderFactory.BodyActivityType; -import at.ac.tuwien.kr.alpha.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult; +import at.ac.tuwien.kr.alpha.solver.learning.ConflictAnalysisResult; import org.apache.commons.collections4.MultiValuedMap; import org.apache.commons.collections4.multimap.HashSetValuedHashMap; import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.util.*; +import java.util.ArrayDeque; +import java.util.Collection; +import java.util.Comparator; +import java.util.Deque; +import java.util.HashMap; +import java.util.HashSet; +import java.util.Map; +import java.util.Optional; +import java.util.Random; +import java.util.Set; import java.util.function.Predicate; import java.util.stream.Stream; -import static at.ac.tuwien.kr.alpha.common.Literals.*; +import static at.ac.tuwien.kr.alpha.common.Literals.atomOf; +import static at.ac.tuwien.kr.alpha.common.Literals.atomToLiteral; +import static at.ac.tuwien.kr.alpha.common.Literals.isNegated; import static at.ac.tuwien.kr.alpha.solver.ThriceTruth.FALSE; import static at.ac.tuwien.kr.alpha.solver.ThriceTruth.TRUE; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/NaiveHeuristic.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/NaiveHeuristic.java index 506cc345c..f2613c186 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/NaiveHeuristic.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/NaiveHeuristic.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2016-2018, the Alpha Team. +/* + * Copyright (c) 2016-2018, 2020, the Alpha Team. * All rights reserved. * * Additional changes made by Siemens. @@ -29,7 +29,7 @@ import at.ac.tuwien.kr.alpha.common.NoGood; import at.ac.tuwien.kr.alpha.solver.ChoiceManager; -import at.ac.tuwien.kr.alpha.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult; +import at.ac.tuwien.kr.alpha.solver.learning.ConflictAnalysisResult; import java.util.Collection; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristic.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristic.java index cda9f35ac..17842b8a5 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristic.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristic.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2019 Siemens AG +/* + * Copyright (c) 2019-2020 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -28,7 +28,7 @@ import at.ac.tuwien.kr.alpha.common.Literals; import at.ac.tuwien.kr.alpha.common.NoGood; import at.ac.tuwien.kr.alpha.solver.ChoiceManager; -import at.ac.tuwien.kr.alpha.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult; +import at.ac.tuwien.kr.alpha.solver.learning.ConflictAnalysisResult; import java.util.Iterator; import java.util.List; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDS.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDS.java index 16b5f0daa..0f30e1fa6 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDS.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDS.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2018-2019 Siemens AG +/* + * Copyright (c) 2018-2020 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -31,7 +31,7 @@ import at.ac.tuwien.kr.alpha.solver.ChoiceManager; import at.ac.tuwien.kr.alpha.solver.ThriceTruth; import at.ac.tuwien.kr.alpha.solver.heuristics.activity.BodyActivityProvider; -import at.ac.tuwien.kr.alpha.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult; +import at.ac.tuwien.kr.alpha.solver.learning.ConflictAnalysisResult; import org.apache.commons.collections4.MultiValuedMap; import org.apache.commons.collections4.multimap.HashSetValuedHashMap; import org.slf4j.Logger; @@ -42,7 +42,9 @@ import java.util.Collection; import static at.ac.tuwien.kr.alpha.Util.arrayGrowthSize; -import static at.ac.tuwien.kr.alpha.common.Literals.*; +import static at.ac.tuwien.kr.alpha.common.Literals.atomOf; +import static at.ac.tuwien.kr.alpha.common.Literals.atomToLiteral; +import static at.ac.tuwien.kr.alpha.common.Literals.isPositive; /** * This implementation is inspired by the VSIDS implementation in clasp. diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/ConflictAnalysisResult.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/ConflictAnalysisResult.java new file mode 100644 index 000000000..eab25fcea --- /dev/null +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/ConflictAnalysisResult.java @@ -0,0 +1,138 @@ +/* + * Copyright (c) 2016-2020, the Alpha Team. + * All rights reserved. + * + * Additional changes made by Siemens. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * 1) Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * 2) Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ +package at.ac.tuwien.kr.alpha.solver.learning; + +import at.ac.tuwien.kr.alpha.common.NoGood; +import at.ac.tuwien.kr.alpha.common.NonGroundNoGood; + +import java.util.Collection; +import java.util.Collections; +import java.util.List; + +import static at.ac.tuwien.kr.alpha.Util.oops; +import static at.ac.tuwien.kr.alpha.solver.NoGoodStore.LBD_NO_VALUE; + +public class ConflictAnalysisResult { + public static final ConflictAnalysisResult UNSAT = new ConflictAnalysisResult(); + + public final NoGood learnedNoGood; + public final int backjumpLevel; + public final Collection resolutionAtoms; + public final int lbd; + + private List additionalLearnedNoGoods; + private NonGroundNoGood learnedNonGroundNoGood; + private List additionalLearnedNonGroundNoGoods; + private NonGroundNoGood exceptionallyLearnedNonGroundNoGood; + + private ConflictAnalysisResult() { + learnedNoGood = null; + backjumpLevel = -1; + resolutionAtoms = null; + lbd = LBD_NO_VALUE; + } + + public ConflictAnalysisResult(NoGood learnedNoGood, int backjumpLevel, Collection resolutionAtoms) { + this(learnedNoGood, backjumpLevel, resolutionAtoms, LBD_NO_VALUE); + } + + public ConflictAnalysisResult(NoGood learnedNoGood, int backjumpLevel, Collection resolutionAtoms, int lbd) { + if (backjumpLevel < 0) { + throw oops("Backjumping level is smaller than 0"); + } + + this.learnedNoGood = learnedNoGood; + this.backjumpLevel = backjumpLevel; + this.resolutionAtoms = resolutionAtoms; + this.lbd = lbd; + } + + /** + * Adds nogoods that have been learned additionally to the primary learned nogood on non-first UIPs. + * @param additionalLearnedNoGoods the nogoods learnt on non-first UIPs + */ + void addLearnedNoGoods(List additionalLearnedNoGoods) { + if (this.additionalLearnedNoGoods == null) { + this.additionalLearnedNoGoods = additionalLearnedNoGoods; + } else { + this.additionalLearnedNoGoods.addAll(additionalLearnedNoGoods); + } + } + + /** + * Gets a list of nogoods that have been learned additionally to the primary learned nogood on non-first UIPs. + * @return a list of additional learned nogoods + */ + List getAdditionalLearnedNoGoods() { + return additionalLearnedNoGoods == null ? Collections.emptyList() : Collections.unmodifiableList(additionalLearnedNoGoods); + } + + /** + * Adds non-ground nogoods that have been learned additionally to the primary learned nogood on non-first UIPs. + * @param additionalLearnedNonGroundNoGoods the non-ground nogoods learnt on non-first UIPs + */ + void addLearnedNonGroundNoGoods(List additionalLearnedNonGroundNoGoods) { + if (this.additionalLearnedNonGroundNoGoods == null) { + this.additionalLearnedNonGroundNoGoods = additionalLearnedNonGroundNoGoods; + } else { + this.additionalLearnedNonGroundNoGoods.addAll(additionalLearnedNonGroundNoGoods); + } + } + + /** + * Gets a list of non-ground nogoods that have been learned additionally to the primary learned nogood on non-first UIPs. + * @return a list of additional learned non-ground nogoods + */ + List getAdditionalLearnedNonGroundNoGoods() { + return additionalLearnedNonGroundNoGoods == null ? Collections.emptyList() : Collections.unmodifiableList(additionalLearnedNonGroundNoGoods); + } + + void setLearnedNonGroundNoGood(NonGroundNoGood learnedNonGroundNoGood) { + this.learnedNonGroundNoGood = learnedNonGroundNoGood; + } + + public NonGroundNoGood getLearnedNonGroundNoGood() { + return learnedNonGroundNoGood; + } + + public void setLearnedNonGroundGoodFromNonUIP(NonGroundNoGood exceptionallyLearnedNonGroundNoGood) { + this.exceptionallyLearnedNonGroundNoGood = exceptionallyLearnedNonGroundNoGood; + } + + public NonGroundNoGood getLearnedNonGroundGoodFromNonUIP() { + return exceptionallyLearnedNonGroundNoGood; + } + + @Override + public String toString() { + if (this == UNSAT) { + return "UNSATISFIABLE"; + } + return learnedNoGood + "@" + backjumpLevel; + } +} diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/ConflictNoGoodLearner.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/ConflictNoGoodLearner.java new file mode 100644 index 000000000..78327ddaf --- /dev/null +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/ConflictNoGoodLearner.java @@ -0,0 +1,40 @@ +/* + * Copyright (c) 2016-2020, the Alpha Team. + * All rights reserved. + * + * Additional changes made by Siemens. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * 1) Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * 2) Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ +package at.ac.tuwien.kr.alpha.solver.learning; + +import at.ac.tuwien.kr.alpha.common.NoGood; +import at.ac.tuwien.kr.alpha.solver.Antecedent; + +public interface ConflictNoGoodLearner { + + int computeConflictFreeBackjumpingLevel(NoGood noGood); + + ConflictAnalysisResult analyzeConflictingNoGood(Antecedent violatedNoGood); + + ConflictAnalysisResult analyzeConflictFromAddingNoGood(Antecedent antecedent); +} diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java index 00a822541..f42518f57 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2016-2018, the Alpha Team. +/* + * Copyright (c) 2016-2020, the Alpha Team. * All rights reserved. * * Additional changes made by Siemens. @@ -35,12 +35,20 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.util.*; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Collection; +import java.util.Collections; +import java.util.HashSet; +import java.util.List; +import java.util.Set; import java.util.stream.Collectors; import java.util.stream.IntStream; import static at.ac.tuwien.kr.alpha.Util.oops; -import static at.ac.tuwien.kr.alpha.common.Literals.*; +import static at.ac.tuwien.kr.alpha.common.Literals.atomOf; +import static at.ac.tuwien.kr.alpha.common.Literals.atomToLiteral; +import static at.ac.tuwien.kr.alpha.common.Literals.isPositive; import static at.ac.tuwien.kr.alpha.solver.NoGoodStore.LBD_NO_VALUE; /** @@ -48,12 +56,13 @@ * * Copyright (c) 2016-2020, the Alpha Team. */ -public class GroundConflictNoGoodLearner { +public class GroundConflictNoGoodLearner implements ConflictNoGoodLearner { private static final Logger LOGGER = LoggerFactory.getLogger(GroundConflictNoGoodLearner.class); private final Assignment assignment; private final AtomStore atomStore; + @Override public int computeConflictFreeBackjumpingLevel(NoGood violatedNoGood) { int highestDecisionLevel = -1; int secondHighestDecisionLevel = -1; @@ -77,55 +86,18 @@ public int computeConflictFreeBackjumpingLevel(NoGood violatedNoGood) { return highestDecisionLevel - 1; } - public static class ConflictAnalysisResult { - public static final ConflictAnalysisResult UNSAT = new ConflictAnalysisResult(); - - public final NoGood learnedNoGood; - public final int backjumpLevel; - public final Collection resolutionAtoms; - public final int lbd; - - private ConflictAnalysisResult() { - learnedNoGood = null; - backjumpLevel = -1; - resolutionAtoms = null; - lbd = LBD_NO_VALUE; - } - - public ConflictAnalysisResult(NoGood learnedNoGood, int backjumpLevel, Collection resolutionAtoms) { - this(learnedNoGood, backjumpLevel, resolutionAtoms, LBD_NO_VALUE); - } - - public ConflictAnalysisResult(NoGood learnedNoGood, int backjumpLevel, Collection resolutionAtoms, int lbd) { - if (backjumpLevel < 0) { - throw oops("Backjumping level is smaller than 0"); - } - - this.learnedNoGood = learnedNoGood; - this.backjumpLevel = backjumpLevel; - this.resolutionAtoms = resolutionAtoms; - this.lbd = lbd; - } - - @Override - public String toString() { - if (this == UNSAT) { - return "UNSATISFIABLE"; - } - return learnedNoGood + "@" + backjumpLevel; - } - } - public GroundConflictNoGoodLearner(Assignment assignment, AtomStore atomStore) { this.assignment = assignment; this.atomStore = atomStore; } + @Override public ConflictAnalysisResult analyzeConflictingNoGood(Antecedent violatedNoGood) { LOGGER.trace("Analyzing violated nogood: {}", violatedNoGood); return analyzeTrailBased(violatedNoGood); } + @Override public ConflictAnalysisResult analyzeConflictFromAddingNoGood(Antecedent violatedNoGood) { LOGGER.trace("Analyzing conflict caused by adding the (violated) nogood: {}", violatedNoGood); // Simply compute appropriate backjumping level. @@ -165,6 +137,21 @@ private String reasonsToString(int[] reasons) { } private ConflictAnalysisResult analyzeTrailBased(Antecedent conflictReason) { + return analyzeTrailBased(conflictReason, true); + } + + /** + * Analyzes a conflict based on the trail assignment. + * @param conflictReason the violated nogood + * @param optimizeAnalysisResult if {@code true}, the analysis result will be optimized in two ways: + *
    + *
  1. if the learned nogood is not assigning due to out-of-order assigned literals + * and thus the program can be proven to be UNSAT, UNSAT will be returned
    2. + *
  2. the learned nogood will be minimized by local clause minimization
    3. + *
+ * @return an instance of {@link ConflictAnalysisResult} that may contain a learned nogood or the information that the problem is UNSAT. + */ + ConflictAnalysisResult analyzeTrailBased(Antecedent conflictReason, boolean optimizeAnalysisResult) { LOGGER.trace("Analyzing trail based."); if (assignment.getDecisionLevel() == 0) { LOGGER.trace("Conflict on decision level 0."); @@ -229,7 +216,16 @@ private ConflictAnalysisResult analyzeTrailBased(Antecedent conflictReason) { // Add the 1UIP literal. resolutionLiterals.add(atomToLiteral(nextAtom, assignment.getTruth(nextAtom).toBoolean())); - int[] learnedLiterals = minimizeLearnedLiterals(resolutionLiterals, seenAtoms); + final int[] learnedLiterals; + if (optimizeAnalysisResult) { + learnedLiterals = minimizeLearnedLiterals(resolutionLiterals, seenAtoms); + } else { + learnedLiterals = new int[resolutionLiterals.size()]; + int i = 0; + for (Integer resolutionLiteral : resolutionLiterals) { + learnedLiterals[i++] = resolutionLiteral; + } + } NoGood learnedNoGood = NoGood.learnt(learnedLiterals); if (LOGGER.isTraceEnabled()) { @@ -238,10 +234,14 @@ private ConflictAnalysisResult analyzeTrailBased(Antecedent conflictReason) { int backjumpingDecisionLevel = computeBackjumpingDecisionLevel(learnedNoGood); if (backjumpingDecisionLevel < 0) { - // Due to out-of-order assigned literals, the learned nogood may be not assigning. - backjumpingDecisionLevel = computeConflictFreeBackjumpingLevel(learnedNoGood); - if (backjumpingDecisionLevel < 0) { - return ConflictAnalysisResult.UNSAT; + if (optimizeAnalysisResult) { + // Due to out-of-order assigned literals, the learned nogood may be not assigning. + backjumpingDecisionLevel = computeConflictFreeBackjumpingLevel(learnedNoGood); + if (backjumpingDecisionLevel < 0) { + return ConflictAnalysisResult.UNSAT; + } + } else { + backjumpingDecisionLevel = 0; } } if (LOGGER.isTraceEnabled()) { diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/NonGroundConflictNoGoodLearner.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/NonGroundConflictNoGoodLearner.java new file mode 100644 index 000000000..6a231d3c4 --- /dev/null +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/NonGroundConflictNoGoodLearner.java @@ -0,0 +1,444 @@ +/* + * Copyright (c) 2020 Siemens AG + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * 1) Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * 2) Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ +package at.ac.tuwien.kr.alpha.solver.learning; + +import at.ac.tuwien.kr.alpha.Util; +import at.ac.tuwien.kr.alpha.common.Assignment; +import at.ac.tuwien.kr.alpha.common.AtomStore; +import at.ac.tuwien.kr.alpha.common.NoGood; +import at.ac.tuwien.kr.alpha.common.NonGroundNoGood; +import at.ac.tuwien.kr.alpha.common.Unifier; +import at.ac.tuwien.kr.alpha.common.UniqueVariableNames; +import at.ac.tuwien.kr.alpha.common.atoms.Atom; +import at.ac.tuwien.kr.alpha.common.atoms.Literal; +import at.ac.tuwien.kr.alpha.solver.Antecedent; +import at.ac.tuwien.kr.alpha.solver.TrailAssignment; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.HashSet; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.stream.Collectors; + +import static at.ac.tuwien.kr.alpha.Util.collectionToIntArray; +import static at.ac.tuwien.kr.alpha.Util.intArrayToLinkedHashSet; +import static at.ac.tuwien.kr.alpha.Util.oops; +import static at.ac.tuwien.kr.alpha.common.Literals.atomOf; +import static at.ac.tuwien.kr.alpha.common.Literals.atomToLiteral; +import static at.ac.tuwien.kr.alpha.common.Literals.isPositive; +import static at.ac.tuwien.kr.alpha.common.Literals.negateLiteral; +import static at.ac.tuwien.kr.alpha.solver.Atoms.FALSUM; + +/** + * Conflict-driven learning on ground clauses that also learns non-ground nogoods. + *

+ * This class builds upon an underlying {@link GroundConflictNoGoodLearner}, to which it acts as a proxy for all operations + * not implemented on the non-ground level. + * The non-ground learning capabilities implemented here are not designed for efficiency (yet), so this class should only + * be used in an "offline" conflict generalisation mode. + */ +public class NonGroundConflictNoGoodLearner implements ConflictNoGoodLearner { + private static final Logger LOGGER = LoggerFactory.getLogger(NonGroundConflictNoGoodLearner.class); + private static final int RESOLUTION_DL_LIMIT = 1; // how many DLs below the current DL shall be used to resolve literals (originally 0, TODO: make configurable) + + private final Assignment assignment; + private final AtomStore atomStore; + private final GroundConflictNoGoodLearner groundLearner; + + private Map nonGroundNoGoodViolationCounter = new HashMap<>(); + private Map> learnedOnFirstUIP = new HashMap<>(); + private Map> learnedOnLastUIP = new HashMap<>(); + private Map> learnedOnOtherUIPs = new HashMap<>(); + private Map> learnedOnNonUIPs = new HashMap<>(); + + public NonGroundConflictNoGoodLearner(Assignment assignment, AtomStore atomStore, GroundConflictNoGoodLearner groundLearner) { + this.assignment = assignment; + this.atomStore = atomStore; + this.groundLearner = groundLearner; + } + + @Override + public int computeConflictFreeBackjumpingLevel(NoGood noGood) { + return groundLearner.computeConflictFreeBackjumpingLevel(noGood); + } + + @Override + public ConflictAnalysisResult analyzeConflictFromAddingNoGood(Antecedent antecedent) { + return groundLearner.analyzeConflictFromAddingNoGood(antecedent); + } + + @Override + public ConflictAnalysisResult analyzeConflictingNoGood(Antecedent violatedNoGood) { + LOGGER.trace("Analyzing violated nogood: {}", violatedNoGood); + return analyzeConflictingNoGoodAndGeneraliseConflict(violatedNoGood); + } + + /** + * Analyzes a conflict and learns both a ground nogood (if possible) and one or more non-ground nogoods (if possible). + *

+ * This method also contains an implementation of first UIP learning that is redundant to the one in + * {@link GroundConflictNoGoodLearner#analyzeTrailBased(Antecedent, boolean)} on purpose: + * While the other implementation is designed for efficiency, this one is designed to be easily understood such that + * the connection to conflict generalisation (non-ground conflict learning) becomes apparent. + * This implementation also uses the other one internally to check the correctness of learned ground nogoods. + * + * @param violatedNoGood the violated nogood to start analysis from + * @return an analysis result, possibly including a learned ground nogood and one or more learned non-ground nogoods + */ + ConflictAnalysisResult analyzeConflictingNoGoodAndGeneraliseConflict(Antecedent violatedNoGood) { + if (assignment.getDecisionLevel() == 0) { + LOGGER.trace("Conflict on decision level 0."); + return ConflictAnalysisResult.UNSAT; + } + + final TrailAssignment.TrailBackwardsWalker trailWalker = ((TrailAssignment) assignment).getTrailBackwardsWalker(); + NoGood firstLearnedNoGood = null; + NonGroundNoGood firstLearnedNonGroundNoGood = null; + List additionalLearnedNoGoods = new ArrayList<>(); + List additionalLearnedNonGroundNoGoods = new ArrayList<>(); + NonGroundNoGood exceptionallyLearnedNonGroundNoGood = null; + GroundAndNonGroundNoGood currentNoGood = new GroundAndNonGroundNoGood(violatedNoGood); + boolean wasAbleToLearn = currentNoGood.canLearnNonGround; + NonGroundNoGood learntNonGroundNoGood = null; + while (makeOneResolutionStep(currentNoGood, trailWalker)) { + if (wasAbleToLearn && !currentNoGood.canLearnNonGround) { + // learn current non-ground nogood if we stopped being able to learn with the last resolution step (e.g., because no non-ground nogood is known for the last antecedent) + assert exceptionallyLearnedNonGroundNoGood == null; + exceptionallyLearnedNonGroundNoGood = learntNonGroundNoGood; + } + wasAbleToLearn = currentNoGood.canLearnNonGround; + learntNonGroundNoGood = currentNoGood.toNonGroundNoGood(); + if (containsUIP(currentNoGood)) { + final NoGood learntNoGood = createLearntNoGood(currentNoGood); + learntNoGood.setNonGroundNoGood(learntNonGroundNoGood); + if (firstLearnedNoGood == null) { + firstLearnedNoGood = learntNoGood; + firstLearnedNonGroundNoGood = learntNonGroundNoGood; + } else { + additionalLearnedNoGoods.add(learntNoGood); + if (learntNonGroundNoGood != null) { + additionalLearnedNonGroundNoGoods.add(learntNonGroundNoGood); + } + } + } + } + final ConflictAnalysisResult groundAnalysisResultNotMinimized = groundLearner.analyzeTrailBased(violatedNoGood, false); +// if (!Objects.equals(groundAnalysisResultNotMinimized.learnedNoGood, firstLearnedNoGood)) { + //throw oops("Learned nogood is not the same as the one computed by ground analysis"); + // TODO: re-introduce check +// } + final ConflictAnalysisResult analysisResult = groundLearner.analyzeConflictingNoGood(violatedNoGood); + if (analysisResult.backjumpLevel >= 0) { + // if backJumpLevel < 0, then problem is UNSAT (ground analysis result does additional checks for this) + analysisResult.setLearnedNonGroundNoGood(firstLearnedNonGroundNoGood); + LOGGER.info("Learned non-ground nogood for ground conflict {}: {}", violatedNoGood, firstLearnedNonGroundNoGood); + if (!additionalLearnedNoGoods.isEmpty()) { + analysisResult.addLearnedNoGoods(additionalLearnedNoGoods); + analysisResult.addLearnedNonGroundNoGoods(additionalLearnedNonGroundNoGoods); + LOGGER.info("Additionally learned non-ground nogoods: {}", additionalLearnedNonGroundNoGoods); + } + if (exceptionallyLearnedNonGroundNoGood != null) { + analysisResult.setLearnedNonGroundGoodFromNonUIP(exceptionallyLearnedNonGroundNoGood); + LOGGER.info("Non-ground nogood learned at non-UIP: {}", exceptionallyLearnedNonGroundNoGood); + } + countAndRememberLearnedNonGroundNoGoods(violatedNoGood, analysisResult); + } + return analysisResult; + } + + /** + * Resolves the current nogood with the antecedent of one of its literals assigned on the current decision level. + * The given {@code currentNoGood} is modified in situ. + * + * @param currentNoGood the nogood to resolve with the antecedent of one of its literals + * @param trailWalker a backwards-walker on the trail + * @return {@code true} if resolution succeeded, or {@code false} if no further resolution step is possible + */ + private boolean makeOneResolutionStep(GroundAndNonGroundNoGood currentNoGood, TrailAssignment.TrailBackwardsWalker trailWalker) { + if (!containsLiteralForResolution(currentNoGood)) { + return false; + } + final int literal = findNextLiteralToResolve(currentNoGood, trailWalker); + resolve(currentNoGood, literal); + return true; + } + + private Integer findNextLiteralToResolve(GroundAndNonGroundNoGood noGood, TrailAssignment.TrailBackwardsWalker trailWalker) { + final int currentDecisionLevel = assignment.getDecisionLevel(); + int literal; + int atom; + do { + literal = trailWalker.getNextLowerLiteral(); + atom = atomOf(literal); + } while (assignment.getWeakDecisionLevel(atom) < currentDecisionLevel - RESOLUTION_DL_LIMIT || assignment.getImpliedBy(atom) == null || !noGood.groundNoGood.contains(literal)); + return literal; + } + + private void resolve(GroundAndNonGroundNoGood noGood1, int literal1) { + final Antecedent antecedentOfLiteral = assignment.getImpliedBy(atomOf(literal1)); + noGood1.resolveWith(antecedentOfLiteral, literal1); + } + + private boolean containsLiteralForResolution(GroundAndNonGroundNoGood noGood) { + final int currentDecisionLevel = assignment.getDecisionLevel(); + for (Integer literal : noGood.groundNoGood) { + final int atom = atomOf(literal); + if (assignment.getWeakDecisionLevel(atom) >= currentDecisionLevel - RESOLUTION_DL_LIMIT && assignment.getImpliedBy(atom) != null) { + return true; + } + } + return false; + } + + private boolean containsUIP(GroundAndNonGroundNoGood resolvent) { + final int currentDecisionLevel = assignment.getDecisionLevel(); + boolean containsLiteralOnCurrentDecisionLevel = false; + for (int literal : resolvent.groundNoGood) { + if (assignment.getWeakDecisionLevel(atomOf(literal)) == currentDecisionLevel) { + if (containsLiteralOnCurrentDecisionLevel) { + return false; + } else { + containsLiteralOnCurrentDecisionLevel = true; + } + } + } + // TODO: is it problematic if containsLiteralOnCurrentDecisionLevel == false? + return containsLiteralOnCurrentDecisionLevel; + } + + private NoGood createLearntNoGood(GroundAndNonGroundNoGood resolvent) { + return NoGood.learnt(collectionToIntArray(resolvent.groundNoGood)); + } + + private static List getAdditionalLiterals(NonGroundNoGood nonGroundNoGood, int numberOfAlreadyConsideredLiterals) { + final List result = new ArrayList<>(nonGroundNoGood.size() - numberOfAlreadyConsideredLiterals); + for (int i = numberOfAlreadyConsideredLiterals; i < nonGroundNoGood.size(); i++) { + result.add(nonGroundNoGood.getLiteral(i)); + } + return result; + } + + private void countAndRememberLearnedNonGroundNoGoods(Antecedent violatedNoGood, ConflictAnalysisResult analysisResult) { + if (violatedNoGood.getOriginalNoGood() == null) { + return; + } + final NonGroundNoGood violatedNonGroundNoGood = violatedNoGood.getOriginalNoGood().getNonGroundNoGood(); + if (violatedNonGroundNoGood == null) { + return; + } + final NonGroundNoGood learnedNonGroundNoGood = analysisResult.getLearnedNonGroundNoGood(); + final List additionalLearnedNonGroundNoGoods = analysisResult.getAdditionalLearnedNonGroundNoGoods(); + final NonGroundNoGood learnedNonGroundGoodFromNonUIP = analysisResult.getLearnedNonGroundGoodFromNonUIP(); + if (!nonGroundNoGoodViolationCounter.containsKey(violatedNonGroundNoGood)) { + nonGroundNoGoodViolationCounter.put(violatedNonGroundNoGood, 0); + learnedOnFirstUIP.put(violatedNonGroundNoGood, new HashSet<>()); + learnedOnLastUIP.put(violatedNonGroundNoGood, new HashSet<>()); + learnedOnOtherUIPs.put(violatedNonGroundNoGood, new HashSet<>()); + learnedOnNonUIPs.put(violatedNonGroundNoGood, new HashSet<>()); + } + nonGroundNoGoodViolationCounter.computeIfPresent(violatedNonGroundNoGood, (n, c) -> c + 1); + if (learnedNonGroundNoGood != null) { + rememberNonGroundNoGoodIfNotAlreadyPresent(learnedNonGroundNoGood, learnedOnFirstUIP.get(violatedNonGroundNoGood)); + } + if (!additionalLearnedNonGroundNoGoods.isEmpty()) { + rememberNonGroundNoGoodIfNotAlreadyPresent(additionalLearnedNonGroundNoGoods.get(additionalLearnedNonGroundNoGoods.size() - 1), learnedOnLastUIP.get(violatedNonGroundNoGood)); + for (int i = 0; i < additionalLearnedNonGroundNoGoods.size() - 1; i++) { + rememberNonGroundNoGoodIfNotAlreadyPresent(additionalLearnedNonGroundNoGoods.get(i), learnedOnOtherUIPs.get(violatedNonGroundNoGood)); + } + } + if (learnedNonGroundGoodFromNonUIP != null) { + rememberNonGroundNoGoodIfNotAlreadyPresent(learnedNonGroundGoodFromNonUIP, learnedOnNonUIPs.get(violatedNonGroundNoGood)); + } + } + + /** + * Adds {@code learnedNonGroundNoGood} to the set {@code nonGroundNoGoods} only if the set does not already contain + * another nogood that is equivalent to the given one under unification. + * @param learnedNonGroundNoGood the nogood to add + * @param nonGroundNoGoods the set of existing nogoods + * @return true iff the nogood is added + */ + private boolean rememberNonGroundNoGoodIfNotAlreadyPresent(NonGroundNoGood learnedNonGroundNoGood, Set nonGroundNoGoods) { + for (NonGroundNoGood existingNoGood : nonGroundNoGoods) { + if (existingNoGood.equals(learnedNonGroundNoGood) || Unifier.canBeUnifiedInBothDirections(learnedNonGroundNoGood, existingNoGood)) { + return false; + } + } + final NonGroundNoGood simplifiedLearnedNoGood = learnedNonGroundNoGood.substitute(learnedNonGroundNoGood.simplifyVariableNames()); + nonGroundNoGoods.add(simplifiedLearnedNoGood); + return true; + } + + public void logLearnedConstraints() { + LOGGER.info("LEARNED NON-GROUND CONSTRAINTS:"); + List> nonGroundViolationCounterEntries = new ArrayList<>(nonGroundNoGoodViolationCounter.entrySet()); + nonGroundViolationCounterEntries.sort(Map.Entry.comparingByValue().reversed()); + for (Map.Entry nonGroundViolationCounterEntry : nonGroundViolationCounterEntries) { + final NonGroundNoGood violatedNonGroundNoGood = nonGroundViolationCounterEntry.getKey(); + LOGGER.info("Violated {} times: {}", nonGroundViolationCounterEntry.getValue(), violatedNonGroundNoGood); + for (NonGroundNoGood learnedNoGood : learnedOnFirstUIP.get(violatedNonGroundNoGood)) { + LOGGER.info("Learned on first UIP: {}", learnedNoGood.asConstraint()); + } + for (NonGroundNoGood learnedNoGood : learnedOnLastUIP.get(violatedNonGroundNoGood)) { + LOGGER.info("Learned on last UIP: {}", learnedNoGood.asConstraint()); + } + for (NonGroundNoGood learnedNoGood : learnedOnOtherUIPs.get(violatedNonGroundNoGood)) { + LOGGER.info("Learned on other UIPs: {}", learnedNoGood.asConstraint()); + } + for (NonGroundNoGood learnedNoGood : learnedOnNonUIPs.get(violatedNonGroundNoGood)) { + LOGGER.info("Learned on non-UIPs: {}", learnedNoGood.asConstraint()); + } + } + } + + public NonGroundNoGood getNoGoodViolatedMostOften() { + // TODO: if more than one nogood has been violated the same maximum number of times, only one of them is returned + return Util.getKeyWithMaximumValue(nonGroundNoGoodViolationCounter); + } + + class GroundAndNonGroundNoGood { + + final UniqueVariableNames uniqueVariableNames = new UniqueVariableNames(); + + Set groundNoGood; + Map mapToNonGroundAtoms = new HashMap<>(); + Set additionalNonGroundLiterals = new LinkedHashSet<>(); + + boolean canLearnNonGround; + + public GroundAndNonGroundNoGood(Antecedent antecedent) { + this.groundNoGood = intArrayToLinkedHashSet(antecedent.getReasonLiterals()); + canLearnNonGround = digestOriginalNonGroundNoGood(antecedent, atomToLiteral(FALSUM)); + } + + private boolean digestOriginalNonGroundNoGood(Antecedent antecedent, int impliedLiteral) { + final NoGood originalNoGood = antecedent.getOriginalNoGood(); + if (originalNoGood == null) { + LOGGER.warn("Cannot generalise conflict because original nogood unknown for " + antecedent); + return false; + } + NonGroundNoGood nonGroundNoGood = originalNoGood.getNonGroundNoGood(); + if (nonGroundNoGood == null) { + LOGGER.warn("Cannot generalise conflict because non-ground nogood unknown for " + atomStore.noGoodToString(originalNoGood)); + return false; + } + + nonGroundNoGood = uniqueVariableNames.makeVariableNamesUnique(nonGroundNoGood); + final Unifier unifier = new Unifier(); + assert (impliedLiteral == atomToLiteral(FALSUM)) == mapToNonGroundAtoms.isEmpty(); // impliedLiteral is only FALSUM for violated nogood + if (!mapToNonGroundAtoms.isEmpty()) { + // if we already have atoms stored, we need to unify conflicting non-ground atoms: + final Unifier conflictUnifier = new Unifier(); + for (int literal : antecedent) { + final Literal nonGroundLiteral = findNonGroundLiteral(literal, originalNoGood, nonGroundNoGood); + final Atom nonGroundAtom = nonGroundLiteral.getAtom(); + final Atom existingNonGroundAtom = mapToNonGroundAtoms.get(atomOf(literal)); + if (literal == negateLiteral(impliedLiteral)) { + // this is the literal used for resolution + assert existingNonGroundAtom != null; + if (!unifier.unify(nonGroundAtom, existingNonGroundAtom)) { + // try unification in other direction (this time with conflictUnifier, because this will be applied to original nogood): + if (!conflictUnifier.unify(existingNonGroundAtom, nonGroundAtom)) { + throw new IllegalArgumentException("Cannot unify existing non-ground atom " + existingNonGroundAtom + " with new atom " + nonGroundAtom); + } + } + } else if (existingNonGroundAtom != null) { + // this is another atom that already exists in the current nogood. It may be that because of this, + // the current nogood uses two variable names for what should be the same variable. + // Therefore, additional unification may be necessary in the current nogood: + // all atoms that are substituted in the conflicting atom must also be substituted in the existing atom + if (!conflictUnifier.unify(existingNonGroundAtom, nonGroundAtom)) { + throw new IllegalArgumentException("Cannot unify existing non-ground atom " + existingNonGroundAtom + " with conflicting atom " + nonGroundAtom); + } + } + } + final Unifier mergedUnifier = Unifier.mergeIntoLeft(conflictUnifier, unifier); + mapToNonGroundAtoms.replaceAll((a, n) -> n.substitute(mergedUnifier)); + additionalNonGroundLiterals = additionalNonGroundLiterals.stream().map(n -> n.substitute(mergedUnifier)).collect(Collectors.toCollection(LinkedHashSet::new)); + } + for (int literal : antecedent) { + final Atom unifiedNonGroundAtom = findNonGroundLiteral(literal, originalNoGood, nonGroundNoGood).getAtom().substitute(unifier); + final Atom existingNonGroundAtom = mapToNonGroundAtoms.get(atomOf(literal)); + if (existingNonGroundAtom != null) { + if (!existingNonGroundAtom.equals(unifiedNonGroundAtom)) { + throw oops("Existing non-ground atom " + existingNonGroundAtom + " for " + atomOf(literal) + " does not match unified atom " + unifiedNonGroundAtom); + } + } else { + mapToNonGroundAtoms.put(atomOf(literal), unifiedNonGroundAtom); + } + } + + for (Literal additionalLiteral : getAdditionalLiterals(nonGroundNoGood, antecedent.size())) { + additionalNonGroundLiterals.add(additionalLiteral.substitute(unifier)); + } + return true; + } + + private Literal findNonGroundLiteral(int literal, NoGood originalNoGood, NonGroundNoGood nonGroundNoGood) { + // index must be looked up because literals may have different order in antecedent than in original nogood: + final int indexOfLiteralInOriginalNogood = originalNoGood.indexOf(literal); + final Literal nonGroundLiteral = nonGroundNoGood.getLiteral(indexOfLiteralInOriginalNogood); + if (!nonGroundLiteral.getPredicate().equals(atomStore.get(atomOf(literal)).getPredicate())) { + throw oops("Wrong non-ground literal assigned to ground literal"); + // TODO: execute this and other checks only if internal checks enabled (?) + } + return nonGroundLiteral; + } + + void resolveWith(Antecedent antecedent, int literalInThisNoGood) { + canLearnNonGround = canLearnNonGround && digestOriginalNonGroundNoGood(antecedent, literalInThisNoGood); + this.groundNoGood.remove(literalInThisNoGood); + for (int literal : antecedent.getReasonLiterals()) { + if (literal != negateLiteral(literalInThisNoGood)) { + this.groundNoGood.add(literal); + } + } + } + + NonGroundNoGood toNonGroundNoGood() { + if (!canLearnNonGround) { + return null; + } + final List literals = new ArrayList<>(); + for (int literal : groundNoGood) { + literals.add(mapToNonGroundAtoms.get(atomOf(literal)).toLiteral(isPositive(literal))); + } + literals.addAll(additionalNonGroundLiterals); + return NonGroundNoGood.learnt(literals); + } + + @Override + public String toString() { + return String.valueOf(toNonGroundNoGood()); + } + } + +} diff --git a/src/test/java/at/ac/tuwien/kr/alpha/TestUtil.java b/src/test/java/at/ac/tuwien/kr/alpha/TestUtil.java index 1fa27b4a2..ac8eb6e2a 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/TestUtil.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/TestUtil.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2019 Siemens AG +/* + * Copyright (c) 2019-2020 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -30,7 +30,6 @@ import at.ac.tuwien.kr.alpha.common.Predicate; import at.ac.tuwien.kr.alpha.common.atoms.Atom; import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; -import at.ac.tuwien.kr.alpha.common.atoms.Literal; import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm; import at.ac.tuwien.kr.alpha.common.terms.Term; import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; @@ -65,14 +64,6 @@ public static Atom atom(String predicateName, int... termInts) { } return new BasicAtom(Predicate.getInstance(predicateName, terms.length), terms); } - - public static Literal literal(String predicateName, String... termStrings) { - return atom(predicateName, termStrings).toLiteral(); - } - - public static Literal literal(String predicateName, int... termInts) { - return atom(predicateName, termInts).toLiteral(); - } public static void printNoGoods(AtomStore atomStore, Collection noGoods) { System.out.println(noGoods.stream().map(atomStore::noGoodToString).collect(Collectors.toSet())); diff --git a/src/test/java/at/ac/tuwien/kr/alpha/common/NoGoodTest.java b/src/test/java/at/ac/tuwien/kr/alpha/common/NoGoodTest.java index b8262aa55..1f7eb9588 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/common/NoGoodTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/common/NoGoodTest.java @@ -1,3 +1,30 @@ +/* + * Copyright (c) 2016-2020, the Alpha Team. + * All rights reserved. + * + * Additional changes made by Siemens. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * 1) Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * 2) Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ package at.ac.tuwien.kr.alpha.common; import org.junit.Test; @@ -8,7 +35,9 @@ import static at.ac.tuwien.kr.alpha.common.Literals.atomToLiteral; import static at.ac.tuwien.kr.alpha.common.Literals.atomToNegatedLiteral; -import static org.junit.Assert.*; +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertFalse; +import static org.junit.Assert.assertTrue; public class NoGoodTest { /** @@ -26,7 +55,7 @@ public static int[] fromOldLiterals(int... literals) { return newLiterals; } - public static int fromOldLiterals(int literal) { + public static Integer fromOldLiterals(int literal) { return literal >= 0 ? atomToLiteral(literal) : atomToNegatedLiteral(-literal); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/common/NonGroundNoGoodTest.java b/src/test/java/at/ac/tuwien/kr/alpha/common/NonGroundNoGoodTest.java new file mode 100644 index 000000000..33f7b3c23 --- /dev/null +++ b/src/test/java/at/ac/tuwien/kr/alpha/common/NonGroundNoGoodTest.java @@ -0,0 +1,55 @@ +/* + * Copyright (c) 2020 Siemens AG + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * 1) Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * 2) Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +package at.ac.tuwien.kr.alpha.common; + +import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; +import at.ac.tuwien.kr.alpha.common.atoms.Literal; +import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; +import org.junit.Test; + +import static org.junit.Assert.assertEquals; + +/** + * Tests {@link NonGroundNoGood} + */ +public class NonGroundNoGoodTest { + + @Test + public void testEqualsIgnoreOrderOfLiterals() { + final Predicate predA = Predicate.getInstance("a", 1); + final Predicate predB = Predicate.getInstance("b", 1); + final VariableTerm varX = VariableTerm.getInstance("X"); + final VariableTerm varY = VariableTerm.getInstance("Y"); + final Literal literalAX = new BasicAtom(predA, varX).toLiteral(); + final Literal literalBY = new BasicAtom(predB, varY).toLiteral(); + final NonGroundNoGood ng1 = new NonGroundNoGood(literalAX, literalBY); + final NonGroundNoGood ng2 = new NonGroundNoGood(literalBY, literalAX); + assertEquals(ng1, ng2); + assertEquals(ng1.hashCode(), ng2.hashCode()); + } + +} diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/SubstitutionTest.java b/src/test/java/at/ac/tuwien/kr/alpha/common/SubstitutionTest.java similarity index 91% rename from src/test/java/at/ac/tuwien/kr/alpha/grounder/SubstitutionTest.java rename to src/test/java/at/ac/tuwien/kr/alpha/common/SubstitutionTest.java index 89093c149..7280ff601 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/grounder/SubstitutionTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/common/SubstitutionTest.java @@ -1,19 +1,19 @@ -/** - * Copyright (c) 2016-2018, the Alpha Team. +/* + * Copyright (c) 2016-2018, 2020, the Alpha Team. * All rights reserved. - * + * * Additional changes made by Siemens. - * + * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are met: - * + * * 1) Redistributions of source code must retain the above copyright notice, this * list of conditions and the following disclaimer. - * + * * 2) Redistributions in binary form must reproduce the above copyright notice, * this list of conditions and the following disclaimer in the documentation * and/or other materials provided with the distribution. - * + * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE @@ -25,10 +25,8 @@ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */ -package at.ac.tuwien.kr.alpha.grounder; +package at.ac.tuwien.kr.alpha.common; -import at.ac.tuwien.kr.alpha.common.Predicate; -import at.ac.tuwien.kr.alpha.common.Rule; import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; import at.ac.tuwien.kr.alpha.common.atoms.BasicLiteral; import at.ac.tuwien.kr.alpha.common.atoms.Literal; @@ -36,6 +34,7 @@ import at.ac.tuwien.kr.alpha.common.terms.FunctionTerm; import at.ac.tuwien.kr.alpha.common.terms.Term; import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; +import at.ac.tuwien.kr.alpha.grounder.NonGroundRule; import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom; import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser; import org.junit.Test; @@ -45,9 +44,6 @@ import static org.junit.Assert.assertEquals; import static org.junit.Assert.assertTrue; -/** - * Copyright (c) 2016-2018, the Alpha Team. - */ public class SubstitutionTest { static final ProgramParser PARSER = new ProgramParser(); @@ -96,7 +92,7 @@ public void groundAndPrintRule() { Substitution substitution = new Substitution(); substitution.unifyTerms(X, A); substitution.unifyTerms(Y, B); - String printedString = NaiveGrounder.groundAndPrintRule(nonGroundRule, substitution); + String printedString = SubstitutionTestUtil.groundAndPrintRule(nonGroundRule, substitution); assertEquals("x :- p(a, b), not q(a, b).", printedString); } @@ -130,7 +126,7 @@ private void groundLiteralToString(boolean negated) { Substitution substitution = new Substitution(); substitution.unifyTerms(X, A); substitution.unifyTerms(Y, B); - String printedString = NaiveGrounder.groundLiteralToString(atom.toLiteral(!negated), substitution, true); + String printedString = SubstitutionTestUtil.groundLiteralToString(atom.toLiteral(!negated), substitution, true); assertEquals((negated ? "not " : "") + "p(a, b)", printedString); } @@ -141,7 +137,7 @@ public void substitutionFromString() { Substitution substitution = new Substitution(); substitution.unifyTerms(X, A); substitution.unifyTerms(Y, B); - RuleAtom ruleAtom = new RuleAtom(nonGroundRule, substitution); + RuleAtom ruleAtom = RuleAtom.ground(nonGroundRule, substitution); String substitutionString = (String) ((ConstantTerm) ruleAtom.getTerms().get(1)).getObject(); Substitution fromString = Substitution.fromString(substitutionString); assertTrue(substitution.equals(fromString)); diff --git a/src/test/java/at/ac/tuwien/kr/alpha/common/SubstitutionTestUtil.java b/src/test/java/at/ac/tuwien/kr/alpha/common/SubstitutionTestUtil.java new file mode 100644 index 000000000..d6eec37ca --- /dev/null +++ b/src/test/java/at/ac/tuwien/kr/alpha/common/SubstitutionTestUtil.java @@ -0,0 +1,61 @@ +/** + * Copyright (c) 2016-2020, the Alpha Team. + * All rights reserved. + * + * Additional changes made by Siemens. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * 1) Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * 2) Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +package at.ac.tuwien.kr.alpha.common; + +import at.ac.tuwien.kr.alpha.common.atoms.Atom; +import at.ac.tuwien.kr.alpha.common.atoms.Literal; +import at.ac.tuwien.kr.alpha.grounder.NonGroundRule; + +public class SubstitutionTestUtil { + + static String groundAndPrintRule(NonGroundRule rule, Substitution substitution) { + StringBuilder ret = new StringBuilder(); + if (!rule.isConstraint()) { + Atom groundHead = rule.getHeadAtom().substitute(substitution); + ret.append(groundHead.toString()); + } + ret.append(" :- "); + boolean isFirst = true; + for (Atom bodyAtom : rule.getBodyAtomsPositive()) { + ret.append(groundLiteralToString(bodyAtom.toLiteral(), substitution, isFirst)); + isFirst = false; + } + for (Atom bodyAtom : rule.getBodyAtomsNegative()) { + ret.append(groundLiteralToString(bodyAtom.toLiteral(false), substitution, isFirst)); + isFirst = false; + } + ret.append("."); + return ret.toString(); + } + + static String groundLiteralToString(Literal literal, Substitution substitution, boolean isFirst) { + Literal groundLiteral = literal.substitute(substitution); + return (isFirst ? "" : ", ") + groundLiteral.toString(); + } +} diff --git a/src/test/java/at/ac/tuwien/kr/alpha/common/UnifierTest.java b/src/test/java/at/ac/tuwien/kr/alpha/common/UnifierTest.java new file mode 100644 index 000000000..291b16c0a --- /dev/null +++ b/src/test/java/at/ac/tuwien/kr/alpha/common/UnifierTest.java @@ -0,0 +1,245 @@ +/* + * Copyright (c) 2018, 2020, the Alpha Team. + * All rights reserved. + * + * Additional changes made by Siemens. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * 1) Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * 2) Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +package at.ac.tuwien.kr.alpha.common; + +import at.ac.tuwien.kr.alpha.common.atoms.Atom; +import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; +import at.ac.tuwien.kr.alpha.common.atoms.BasicLiteral; +import at.ac.tuwien.kr.alpha.common.atoms.Literal; +import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm; +import at.ac.tuwien.kr.alpha.common.terms.FunctionTerm; +import at.ac.tuwien.kr.alpha.common.terms.Term; +import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; +import at.ac.tuwien.kr.alpha.grounder.NonGroundRule; +import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser; +import at.ac.tuwien.kr.alpha.grounder.parser.ProgramPartParser; +import org.junit.Test; + +import java.util.Arrays; + +import static at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type.STATIC; +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertFalse; +import static org.junit.Assert.assertTrue; + +public class UnifierTest extends SubstitutionTest { + + private static final ProgramPartParser PROGRAM_PART_PARSER = new ProgramPartParser(); + + @Test + public void extendUnifier() { + VariableTerm varX = VariableTerm.getInstance("X"); + VariableTerm varY = VariableTerm.getInstance("Y"); + Unifier sub1 = new Unifier(); + sub1.put(varX, varY); + Unifier sub2 = new Unifier(); + sub2.put(varY, ConstantTerm.getInstance("a")); + + sub1.extendWith(sub2); + BasicAtom atom1 = parseAtom("p(X)"); + + Atom atomSubstituted = atom1.substitute(sub1); + assertEquals(ConstantTerm.getInstance("a"), atomSubstituted.getTerms().get(0)); + } + + @Test + public void mergeUnifierIntoLeft() { + VariableTerm varX = VariableTerm.getInstance("X"); + VariableTerm varY = VariableTerm.getInstance("Y"); + VariableTerm varZ = VariableTerm.getInstance("Z"); + Term constA = ConstantTerm.getInstance("a"); + Unifier left = new Unifier(); + left.put(varX, varY); + left.put(varZ, varY); + Unifier right = new Unifier(); + right.put(varX, constA); + Unifier merged = Unifier.mergeIntoLeft(left, right); + assertEquals(constA, merged.eval(varY)); + assertEquals(constA, merged.eval(varZ)); + } + + private BasicAtom parseAtom(String atom) { + ProgramParser programParser = new ProgramParser(); + Program program = programParser.parse(atom + "."); + return (BasicAtom) program.getFacts().get(0); + } + + @Test + public void unifyTermsSimpleBinding() throws Exception { + Substitution substitution = new Unifier(); + substitution.unifyTerms(Y, A); + assertEquals(A, substitution.eval(Y)); + } + + @Test + public void unifyTermsFunctionTermBinding() throws Exception { + Substitution substitution = new Unifier(); + substitution.put(Y, A); + + FunctionTerm groundFunctionTerm = FunctionTerm.getInstance("f", B, C); + Term nongroundFunctionTerm = FunctionTerm.getInstance("f", B, X); + + substitution.unifyTerms(nongroundFunctionTerm, groundFunctionTerm); + + assertEquals(C, substitution.eval(X)); + assertEquals(A, substitution.eval(Y)); + } + + @Test + public void substitutePositiveBasicAtom() { + substituteBasicAtomLiteral(false); + } + + @Test + public void substituteNegativeBasicAtom() { + substituteBasicAtomLiteral(true); + } + + @Test + public void groundAndPrintRule() { + Rule rule = PARSER.parse("x :- p(X,Y), not q(X,Y).").getRules().get(0); + NonGroundRule nonGroundRule = NonGroundRule.constructNonGroundRule(rule); + Substitution substitution = new Unifier(); + substitution.unifyTerms(X, A); + substitution.unifyTerms(Y, B); + String printedString = SubstitutionTestUtil.groundAndPrintRule(nonGroundRule, substitution); + assertEquals("x :- p(a, b), not q(a, b).", printedString); + } + + private void substituteBasicAtomLiteral(boolean negated) { + Predicate p = Predicate.getInstance("p", 2); + BasicAtom atom = new BasicAtom(p, Arrays.asList(X, Y)); + Literal literal = new BasicLiteral(atom, !negated); + Substitution substitution = new Unifier(); + substitution.unifyTerms(X, A); + substitution.unifyTerms(Y, B); + literal = literal.substitute(substitution); + assertEquals(p, literal.getPredicate()); + assertEquals(A, literal.getTerms().get(0)); + assertEquals(B, literal.getTerms().get(1)); + assertEquals(negated, literal.isNegated()); + } + + @Test + public void groundLiteralToString_PositiveBasicAtom() { + groundLiteralToString(false); + } + + @Test + public void groundLiteralToString_NegativeBasicAtom() { + groundLiteralToString(true); + } + + private void groundLiteralToString(boolean negated) { + Predicate p = Predicate.getInstance("p", 2); + BasicAtom atom = new BasicAtom(p, Arrays.asList(X, Y)); + Substitution substitution = new Unifier(); + substitution.unifyTerms(X, A); + substitution.unifyTerms(Y, B); + String printedString = SubstitutionTestUtil.groundLiteralToString(atom.toLiteral(!negated), substitution, true); + assertEquals((negated ? "not " : "") + "p(a, b)", printedString); + } + + @Test + public void unsuccessfullyUnifyNonGroundNoGoodsMismatchingHead() { + final Literal lit1 = PROGRAM_PART_PARSER.parseLiteral("not a(X)"); + final Literal lit2 = PROGRAM_PART_PARSER.parseLiteral("b(X)"); + final Literal[] literals = new Literal[]{lit1, lit2}; + final NonGroundNoGood nonGroundNoGood1 = new NonGroundNoGood(STATIC, literals, true); + final NonGroundNoGood nonGroundNoGood2 = new NonGroundNoGood(STATIC, literals, false); + assertFalse(new Unifier().unify(nonGroundNoGood1, nonGroundNoGood2)); + assertFalse(new Unifier().unify(nonGroundNoGood2, nonGroundNoGood1)); + } + + @Test + public void unsuccessfullyUnifyNonGroundNoGoodsMismatchingPredicate() { + final Literal lit1a = PROGRAM_PART_PARSER.parseLiteral("a(X)"); + final Literal lit1b = PROGRAM_PART_PARSER.parseLiteral("b(X)"); + final Literal lit2 = PROGRAM_PART_PARSER.parseLiteral("not c(X)"); + final NonGroundNoGood nonGroundNoGood1 = new NonGroundNoGood(lit1a, lit2); + final NonGroundNoGood nonGroundNoGood2 = new NonGroundNoGood(lit1b, lit2); + assertFalse(new Unifier().unify(nonGroundNoGood1, nonGroundNoGood2)); + assertFalse(new Unifier().unify(nonGroundNoGood2, nonGroundNoGood1)); + } + + @Test + public void unsuccessfullyUnifyNonGroundNoGoodsAdditionalLiteral() { + final Literal lit1 = PROGRAM_PART_PARSER.parseLiteral("a(X,Y)"); + final Literal lit2 = PROGRAM_PART_PARSER.parseLiteral("b(X)"); + final Literal lit3 = PROGRAM_PART_PARSER.parseLiteral("X < Y"); + final NonGroundNoGood nonGroundNoGood1 = new NonGroundNoGood(lit1, lit2); + final NonGroundNoGood nonGroundNoGood2 = new NonGroundNoGood(lit1, lit2, lit3); + assertFalse(new Unifier().unify(nonGroundNoGood1, nonGroundNoGood2)); + assertFalse(new Unifier().unify(nonGroundNoGood2, nonGroundNoGood1)); + } + + @Test + public void successfullyUnifyNonGroundNoGoods() { + final Literal lit1 = PROGRAM_PART_PARSER.parseLiteral("a(X,Y)"); + final Literal lit2 = PROGRAM_PART_PARSER.parseLiteral("b(X)"); + final Literal lit3 = PROGRAM_PART_PARSER.parseLiteral("X < Y"); + final Unifier substitution = new Unifier(); + substitution.put(VariableTerm.getInstance("X"), VariableTerm.getInstance("X1")); + substitution.put(VariableTerm.getInstance("Y"), VariableTerm.getInstance("Z")); + final NonGroundNoGood nonGroundNoGood1 = new NonGroundNoGood(lit1, lit2, lit3); + final NonGroundNoGood nonGroundNoGood2 = new NonGroundNoGood( + lit1.substitute(substitution), lit2.substitute(substitution), lit3.substitute(substitution)); + assertTrue(new Unifier().unify(nonGroundNoGood1, nonGroundNoGood2)); + assertTrue(new Unifier().unify(nonGroundNoGood2, nonGroundNoGood1)); + } + + @Test + public void successfullyUnifyNonGroundNoGoodsOneIsPartiallyGround() { + final Literal lit1 = PROGRAM_PART_PARSER.parseLiteral("a(X,Y)"); + final Literal lit2 = PROGRAM_PART_PARSER.parseLiteral("b(X)"); + final Literal lit3 = PROGRAM_PART_PARSER.parseLiteral("X < Y"); + final Unifier substitution = new Unifier(); + substitution.put(VariableTerm.getInstance("X"), VariableTerm.getInstance("X1")); + substitution.put(VariableTerm.getInstance("Y"), ConstantTerm.getInstance("y")); + final NonGroundNoGood nonGroundNoGood1 = new NonGroundNoGood(lit1, lit2, lit3); + final NonGroundNoGood nonGroundNoGood2 = new NonGroundNoGood( + lit1.substitute(substitution), lit2.substitute(substitution), lit3.substitute(substitution)); + assertTrue(new Unifier().unify(nonGroundNoGood1, nonGroundNoGood2)); + assertFalse(new Unifier().unify(nonGroundNoGood2, nonGroundNoGood1)); + } + + @Test + public void unsuccessfullyUnifyPartiallyGroundNonGroundNoGoods() { + final Literal lit1a = PROGRAM_PART_PARSER.parseLiteral("a(1,Y)"); + final Literal lit2a = PROGRAM_PART_PARSER.parseLiteral("b(1)"); + final Literal lit3a = PROGRAM_PART_PARSER.parseLiteral("1 < Y"); + final Literal lit1b = PROGRAM_PART_PARSER.parseLiteral("a(X,2)"); + final Literal lit2b = PROGRAM_PART_PARSER.parseLiteral("b(X)"); + final Literal lit3b = PROGRAM_PART_PARSER.parseLiteral("X < 2"); + final NonGroundNoGood nonGroundNoGood1 = new NonGroundNoGood(lit1a, lit2a, lit3a); + final NonGroundNoGood nonGroundNoGood2 = new NonGroundNoGood(lit1b, lit2b, lit3b); + assertFalse(new Unifier().unify(nonGroundNoGood1, nonGroundNoGood2)); + assertFalse(new Unifier().unify(nonGroundNoGood2, nonGroundNoGood1)); + } +} \ No newline at end of file diff --git a/src/test/java/at/ac/tuwien/kr/alpha/common/UniqueVariableNamesTest.java b/src/test/java/at/ac/tuwien/kr/alpha/common/UniqueVariableNamesTest.java new file mode 100644 index 000000000..abf703ed4 --- /dev/null +++ b/src/test/java/at/ac/tuwien/kr/alpha/common/UniqueVariableNamesTest.java @@ -0,0 +1,106 @@ +/* + * Copyright (c) 2020 Siemens AG + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * 1) Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * 2) Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +package at.ac.tuwien.kr.alpha.common; + +import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; +import at.ac.tuwien.kr.alpha.common.atoms.BasicLiteral; +import at.ac.tuwien.kr.alpha.common.atoms.ComparisonAtom; +import at.ac.tuwien.kr.alpha.common.atoms.ComparisonLiteral; +import at.ac.tuwien.kr.alpha.common.atoms.Literal; +import at.ac.tuwien.kr.alpha.common.terms.ArithmeticTerm; +import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm; +import at.ac.tuwien.kr.alpha.common.terms.Term; +import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; +import org.junit.Before; +import org.junit.Test; + +import static at.ac.tuwien.kr.alpha.common.ComparisonOperator.EQ; +import static at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type.LEARNT; +import static at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type.STATIC; +import static at.ac.tuwien.kr.alpha.common.terms.ArithmeticTerm.ArithmeticOperator.PLUS; +import static org.junit.Assert.assertEquals; + +/** + * Tests {@link UniqueVariableNames} + */ +public class UniqueVariableNamesTest { + + private UniqueVariableNames uniqueVariableNames; + + @Before + public void setUp() { + this.uniqueVariableNames = new UniqueVariableNames(); + } + + @Test + public void testRenameInSecondNoGood() { + final Predicate predA = Predicate.getInstance("a", 2); + final Predicate predB = Predicate.getInstance("b", 2); + final VariableTerm varX = VariableTerm.getInstance("X"); + final VariableTerm varY = VariableTerm.getInstance("Y"); + final VariableTerm varY1 = VariableTerm.getInstance("Y_1"); + final VariableTerm varY2 = VariableTerm.getInstance("Y_2"); + final VariableTerm varZ = VariableTerm.getInstance("Z"); + + final Literal[] literals1 = new Literal[]{ + lit(true, predA, varX, varY), + lit(false, predA, varX, varY1), + comp(varY1, plus(varY, ConstantTerm.getInstance(1)), EQ) + }; + + final Literal[] literals2 = new Literal[]{ + lit(true, predB, varY, varZ) + }; + + final Literal[] expectedModifiedLiterals2 = new Literal[]{ + lit(true, predB, varY2, varZ) + }; + + final NonGroundNoGood noGood1 = new NonGroundNoGood(LEARNT, literals1, false); + final NonGroundNoGood noGood2 = new NonGroundNoGood(STATIC, literals2, false); + final NonGroundNoGood expectedModifiedNoGood2 = new NonGroundNoGood(STATIC, expectedModifiedLiterals2, false); + + final NonGroundNoGood modifiedNoGood1 = uniqueVariableNames.makeVariableNamesUnique(noGood1); + final NonGroundNoGood modifiedNoGood2 = uniqueVariableNames.makeVariableNamesUnique(noGood2); + + assertEquals(noGood1, modifiedNoGood1); + assertEquals(expectedModifiedNoGood2, modifiedNoGood2); + } + + private BasicLiteral lit(boolean positive, Predicate predicate, Term... terms) { + return new BasicAtom(predicate, terms).toLiteral(positive); + } + + private ComparisonLiteral comp(Term term1, Term term2, ComparisonOperator operator) { + return new ComparisonAtom(term1, term2, operator).toLiteral(true); + } + + private Term plus(VariableTerm term1, Term term2) { + return ArithmeticTerm.getInstance(term1, PLUS, term2); + } + +} diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/ChoiceGrounder.java b/src/test/java/at/ac/tuwien/kr/alpha/grounder/ChoiceGrounder.java index 2270c16b2..72c35339c 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/grounder/ChoiceGrounder.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/grounder/ChoiceGrounder.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2016-2019, the Alpha Team. +/* + * Copyright (c) 2016-2020, the Alpha Team. * All rights reserved. * * Additional changes made by Siemens. @@ -27,7 +27,17 @@ */ package at.ac.tuwien.kr.alpha.grounder; -import at.ac.tuwien.kr.alpha.common.*; +import at.ac.tuwien.kr.alpha.common.AnswerSet; +import at.ac.tuwien.kr.alpha.common.AnswerSetBuilder; +import at.ac.tuwien.kr.alpha.common.Assignment; +import at.ac.tuwien.kr.alpha.common.AtomStore; +import at.ac.tuwien.kr.alpha.common.BasicAnswerSet; +import at.ac.tuwien.kr.alpha.common.DisjunctiveHead; +import at.ac.tuwien.kr.alpha.common.IntIterator; +import at.ac.tuwien.kr.alpha.common.NoGood; +import at.ac.tuwien.kr.alpha.common.Predicate; +import at.ac.tuwien.kr.alpha.common.Rule; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.atoms.Atom; import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; import at.ac.tuwien.kr.alpha.grounder.atoms.ChoiceAtom; @@ -35,7 +45,14 @@ import org.apache.commons.lang3.tuple.ImmutablePair; import org.apache.commons.lang3.tuple.Pair; -import java.util.*; +import java.util.Arrays; +import java.util.Collections; +import java.util.HashMap; +import java.util.HashSet; +import java.util.Map; +import java.util.Set; +import java.util.SortedSet; +import java.util.TreeSet; import java.util.stream.Stream; import static at.ac.tuwien.kr.alpha.Util.entriesToMap; @@ -96,8 +113,8 @@ public class ChoiceGrounder implements Grounder { private static Atom atomBB = new BasicAtom(Predicate.getInstance("bb", 0)); private static Rule ruleAA = new Rule(new DisjunctiveHead(Collections.singletonList(atomAA)), Collections.singletonList(new BasicAtom(Predicate.getInstance("bb", 0)).toLiteral(false))); private static Rule ruleBB = new Rule(new DisjunctiveHead(Collections.singletonList(atomBB)), Collections.singletonList(new BasicAtom(Predicate.getInstance("aa", 0)).toLiteral(false))); - private static Atom rule1 = new RuleAtom(NonGroundRule.constructNonGroundRule(ruleAA), new Substitution()); - private static Atom rule2 = new RuleAtom(NonGroundRule.constructNonGroundRule(ruleBB), new Substitution()); + private static Atom rule1 = RuleAtom.ground(NonGroundRule.constructNonGroundRule(ruleAA), new Substitution()); + private static Atom rule2 = RuleAtom.ground(NonGroundRule.constructNonGroundRule(ruleBB), new Substitution()); private static Atom atomEnBR1 = ChoiceAtom.on(1); private static Atom atomEnBR2 = ChoiceAtom.on(2); private static Atom atomDisBR1 = ChoiceAtom.off(3); diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/DummyGrounder.java b/src/test/java/at/ac/tuwien/kr/alpha/grounder/DummyGrounder.java index e9fad2622..cf5f70cec 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/grounder/DummyGrounder.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/grounder/DummyGrounder.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2016-2019, the Alpha Team. +/* + * Copyright (c) 2016-2020, the Alpha Team. * All rights reserved. * * Additional changes made by Siemens. @@ -27,14 +27,31 @@ */ package at.ac.tuwien.kr.alpha.grounder; -import at.ac.tuwien.kr.alpha.common.*; +import at.ac.tuwien.kr.alpha.common.AnswerSet; +import at.ac.tuwien.kr.alpha.common.AnswerSetBuilder; +import at.ac.tuwien.kr.alpha.common.Assignment; +import at.ac.tuwien.kr.alpha.common.AtomStore; +import at.ac.tuwien.kr.alpha.common.BasicAnswerSet; +import at.ac.tuwien.kr.alpha.common.DisjunctiveHead; +import at.ac.tuwien.kr.alpha.common.IntIterator; +import at.ac.tuwien.kr.alpha.common.NoGood; +import at.ac.tuwien.kr.alpha.common.Predicate; +import at.ac.tuwien.kr.alpha.common.Rule; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.atoms.Atom; import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom; import org.apache.commons.lang3.tuple.ImmutablePair; import org.apache.commons.lang3.tuple.Pair; -import java.util.*; +import java.util.Arrays; +import java.util.Collections; +import java.util.HashMap; +import java.util.HashSet; +import java.util.Map; +import java.util.Set; +import java.util.SortedSet; +import java.util.TreeSet; import java.util.stream.Stream; import static at.ac.tuwien.kr.alpha.Util.entriesToMap; @@ -73,7 +90,7 @@ public class DummyGrounder implements Grounder { private static Atom atomBB = new BasicAtom(Predicate.getInstance("b", 0)); private static Atom atomCC = new BasicAtom(Predicate.getInstance("c", 0)); private static Rule ruleABC = new Rule(new DisjunctiveHead(Collections.singletonList(atomCC)), Arrays.asList(atomAA.toLiteral(), atomBB.toLiteral())); - private static Atom rule1 = new RuleAtom(NonGroundRule.constructNonGroundRule(ruleABC), new Substitution()); + private static Atom rule1 = RuleAtom.ground(NonGroundRule.constructNonGroundRule(ruleABC), new Substitution()); private Set returnedNogoods = new HashSet<>(); public DummyGrounder(AtomStore atomStore) { diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java b/src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java index f2aeda83f..40e4be5c3 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2018-2019 Siemens AG +/* + * Copyright (c) 2018-2020 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -30,13 +30,13 @@ import at.ac.tuwien.kr.alpha.common.AtomStoreImpl; import at.ac.tuwien.kr.alpha.common.Literals; import at.ac.tuwien.kr.alpha.common.NoGood; -import at.ac.tuwien.kr.alpha.common.Predicate; import at.ac.tuwien.kr.alpha.common.Program; -import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.atoms.Literal; import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm; import at.ac.tuwien.kr.alpha.grounder.heuristics.GrounderHeuristicsConfiguration; import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser; +import at.ac.tuwien.kr.alpha.grounder.parser.ProgramPartParser; import at.ac.tuwien.kr.alpha.solver.ThriceTruth; import at.ac.tuwien.kr.alpha.solver.TrailAssignment; import org.junit.Before; @@ -50,7 +50,6 @@ import java.util.Map; import static at.ac.tuwien.kr.alpha.TestUtil.atom; -import static at.ac.tuwien.kr.alpha.TestUtil.literal; import static at.ac.tuwien.kr.alpha.solver.ThriceTruth.TRUE; import static org.junit.Assert.assertEquals; import static org.junit.Assert.assertTrue; @@ -65,7 +64,15 @@ * If unit tests in this class begin to fail due to such improvements to preprocessing, this issue must be addressed. */ public class NaiveGrounderTest { - private static final ProgramParser PARSER = new ProgramParser(); + private static final ProgramParser PROGRAM_PARSER = new ProgramParser(); + private static final ProgramPartParser PROGRAM_PART_PARSER = new ProgramPartParser(); + + final Literal litP1X = PROGRAM_PART_PARSER.parseLiteral("p1(X)"); + final Literal litP2X = PROGRAM_PART_PARSER.parseLiteral("p2(X)"); + final Literal litQ2Y = PROGRAM_PART_PARSER.parseLiteral("q2(Y)"); + final Literal litQ1Y = PROGRAM_PART_PARSER.parseLiteral("q1(Y)"); + final Literal litAX = PROGRAM_PART_PARSER.parseLiteral("a(X)"); + final Literal litA1 = PROGRAM_PART_PARSER.parseLiteral("a(1)"); @Before public void resetRuleIdGenerator() { @@ -78,15 +85,15 @@ public void resetRuleIdGenerator() { */ @Test public void groundRuleAlreadyGround() { - Program program = PARSER.parse("a :- not b. " + Program program = PROGRAM_PARSER.parse("a :- not b. " + "b :- not a. " + "c :- b."); AtomStore atomStore = new AtomStoreImpl(); Grounder grounder = GrounderFactory.getInstance("naive", program, atomStore, true); Map noGoods = grounder.getNoGoods(new TrailAssignment(atomStore)); - int litCNeg = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("c", 0))), false); - int litB = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("b", 0)))); + int litCNeg = Literals.atomToLiteral(atomStore.get(PROGRAM_PART_PARSER.parseBasicAtom("c")), false); + int litB = Literals.atomToLiteral(atomStore.get(PROGRAM_PART_PARSER.parseBasicAtom("b"))); assertExistsNoGoodContaining(noGoods.values(), litCNeg); assertExistsNoGoodContaining(noGoods.values(), litB); } @@ -97,7 +104,7 @@ public void groundRuleAlreadyGround() { */ @Test public void groundRuleWithLongerBodyAlreadyGround() { - Program program = PARSER.parse("a :- not b. " + Program program = PROGRAM_PARSER.parse("a :- not b. " + "b :- not a. " + "c :- b. " + "d :- b, c. "); @@ -105,10 +112,10 @@ public void groundRuleWithLongerBodyAlreadyGround() { AtomStore atomStore = new AtomStoreImpl(); Grounder grounder = GrounderFactory.getInstance("naive", program, atomStore, true); Map noGoods = grounder.getNoGoods(new TrailAssignment(atomStore)); - int litANeg = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("a", 0))), false); - int litBNeg = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("b", 0))), false); - int litCNeg = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("c", 0))), false); - int litDNeg = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("d", 0))), false); + int litANeg = Literals.atomToLiteral(atomStore.get(PROGRAM_PART_PARSER.parseBasicAtom("a")), false); + int litBNeg = Literals.atomToLiteral(atomStore.get(PROGRAM_PART_PARSER.parseBasicAtom("b")), false); + int litCNeg = Literals.atomToLiteral(atomStore.get(PROGRAM_PART_PARSER.parseBasicAtom("c")), false); + int litDNeg = Literals.atomToLiteral(atomStore.get(PROGRAM_PART_PARSER.parseBasicAtom("d")), false); assertExistsNoGoodContaining(noGoods.values(), litANeg); assertExistsNoGoodContaining(noGoods.values(), litBNeg); assertExistsNoGoodContaining(noGoods.values(), litCNeg); @@ -121,42 +128,42 @@ public void groundRuleWithLongerBodyAlreadyGround() { */ @Test public void groundConstraintAlreadyGround() { - Program program = PARSER.parse("a :- not b. " + Program program = PROGRAM_PARSER.parse("a :- not b. " + "b :- not a. " + ":- b."); AtomStore atomStore = new AtomStoreImpl(); Grounder grounder = GrounderFactory.getInstance("naive", program, atomStore, true); Map noGoods = grounder.getNoGoods(new TrailAssignment(atomStore)); - int litB = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("b", 0)))); + int litB = Literals.atomToLiteral(atomStore.get(PROGRAM_PART_PARSER.parseBasicAtom("b"))); assertTrue(noGoods.containsValue(NoGood.fromConstraint(Collections.singletonList(litB), Collections.emptyList()))); } @Test public void avoidDeadEndsWithPermissiveGrounderHeuristicForP1() { - RuleGroundingOrder groundingOrderP1 = new RuleGroundingOrder(literal("p1", "X"), - Arrays.asList(literal("p2", "X"), literal("q2", "Y"), literal("q1", "Y")), -1, false); + RuleGroundingOrder groundingOrderP1 = new RuleGroundingOrder(litP1X, + Arrays.asList(litP2X, litQ2Y, litQ1Y), -1, false); testDeadEnd("p1", groundingOrderP1, true); } @Test public void avoidDeadEndsWithPermissiveGrounderHeuristicForQ1() { - RuleGroundingOrder groundingOrderQ1 = new RuleGroundingOrder(literal("q1", "Y"), - Arrays.asList(literal("q2", "Y"), literal("p2", "X"), literal("p1", "X")), -1, false); + RuleGroundingOrder groundingOrderQ1 = new RuleGroundingOrder(litQ1Y, + Arrays.asList(litQ2Y, litP2X, litP1X), -1, false); testDeadEnd("q1", groundingOrderQ1, true); } @Test public void noDeadEndWithPermissiveGrounderHeuristicForP1() { - RuleGroundingOrder groundingOrderP1 = new RuleGroundingOrder(literal("p1", "X"), - Arrays.asList(literal("p2", "X"), literal("q1", "Y"), literal("q2", "Y")), -1, false); + RuleGroundingOrder groundingOrderP1 = new RuleGroundingOrder(litP1X, + Arrays.asList(litP2X, litQ1Y, litQ2Y), -1, false); testDeadEnd("p1", groundingOrderP1, true); } @Test public void noDeadEndWithPermissiveGrounderHeuristicForQ1() { - RuleGroundingOrder groundingOrderQ1 = new RuleGroundingOrder(literal("q1", "Y"), - Arrays.asList(literal("q2", "Y"), literal("p1", "X"), literal("p2", "X")), -1, false); + RuleGroundingOrder groundingOrderQ1 = new RuleGroundingOrder(litQ1Y, + Arrays.asList(litQ2Y, litP1X, litP2X), -1, false); testDeadEnd("q1", groundingOrderQ1, true); } @@ -180,7 +187,7 @@ public void noDeadEndWithPermissiveGrounderHeuristicForQ1() { * described above. */ private void testDeadEnd(String predicateNameOfStartingLiteral, RuleGroundingOrder groundingOrder, boolean expectNoGoods) { - Program program = PARSER.parse("p1(1). q1(1). " + Program program = PROGRAM_PARSER.parse("p1(1). q1(1). " + "x :- p1(X), p2(X), q1(Y), q2(Y). " + "p2(X) :- something(X). " + "q2(X) :- something(X). "); @@ -189,8 +196,8 @@ private void testDeadEnd(String predicateNameOfStartingLiteral, RuleGroundingOrd NaiveGrounder grounder = (NaiveGrounder) GrounderFactory.getInstance("naive", program, atomStore, p -> true, GrounderHeuristicsConfiguration.permissive(), true); NonGroundRule nonGroundRule = grounder.getNonGroundRule(0); - String varName = "p1".equals(predicateNameOfStartingLiteral) ? "X" : "Y"; - final Literal startingLiteral = literal("p1", varName); + String strLiteral = "p1".equals(predicateNameOfStartingLiteral) ? "p1(X)" : "p1(Y)"; + final Literal startingLiteral = PROGRAM_PART_PARSER.parseLiteral(strLiteral); nonGroundRule.groundingOrder.groundingOrders.put(startingLiteral, groundingOrder); grounder.bootstrap(); @@ -203,36 +210,36 @@ private void testDeadEnd(String predicateNameOfStartingLiteral, RuleGroundingOrd @Test public void testGroundingOfRuleSwitchedOffByFalsePositiveBody() { - Program program = PARSER.parse("a(1). " + Program program = PROGRAM_PARSER.parse("a(1). " + "c(X) :- a(X), b(X). " + "b(X) :- something(X). "); - testIfGrounderGroundsRule(program, 0, literal("a", "X"), 1, ThriceTruth.FALSE, false); + testIfGrounderGroundsRule(program, 0, litAX, 1, ThriceTruth.FALSE, false); } @Test public void testGroundingOfRuleNotSwitchedOffByTruePositiveBody() { - Program program = PARSER.parse("a(1). " + Program program = PROGRAM_PARSER.parse("a(1). " + "c(X) :- a(X), b(X). " + "b(X) :- something(X). "); - testIfGrounderGroundsRule(program, 0, literal("a", "X"), 1, ThriceTruth.TRUE, true); + testIfGrounderGroundsRule(program, 0, litAX, 1, ThriceTruth.TRUE, true); } @Test @Ignore("Currently, rule grounding is not switched off by a true negative body atom") public void testGroundingOfRuleSwitchedOffByTrueNegativeBody() { - Program program = PARSER.parse("a(1). " + Program program = PROGRAM_PARSER.parse("a(1). " + "c(X) :- a(X), not b(X). " + "b(X) :- something(X). "); - testIfGrounderGroundsRule(program, 0, literal("a", "X"), 1, ThriceTruth.TRUE, false); + testIfGrounderGroundsRule(program, 0, litAX, 1, ThriceTruth.TRUE, false); } @Test public void testGroundingOfRuleNotSwitchedOffByFalseNegativeBody() { - Program program = PARSER.parse("a(1). " + Program program = PROGRAM_PARSER.parse("a(1). " + "c(X) :- a(X), not b(X). " + "b(X) :- something(X). "); - testIfGrounderGroundsRule(program, 0, literal("a", "X"), 1, ThriceTruth.FALSE, true); + testIfGrounderGroundsRule(program, 0, litAX, 1, ThriceTruth.FALSE, true); } /** @@ -260,66 +267,66 @@ private void testIfGrounderGroundsRule(Program program, int ruleID, Literal star @Test public void testPermissiveGrounderHeuristicTolerance_0_reject() { - Program program = PARSER.parse("a(1). " + Program program = PROGRAM_PARSER.parse("a(1). " + "c(X) :- a(X), b(X). " + "b(X) :- something(X)."); - testPermissiveGrounderHeuristicTolerance(program, 0, literal("a", "X"), 1, 0, false, Arrays.asList(1)); + testPermissiveGrounderHeuristicTolerance(program, 0, litAX, 1, 0, false, Arrays.asList(1)); } @Test public void testPermissiveGrounderHeuristicTolerance_1_accept() { - Program program = PARSER.parse("a(1). " + Program program = PROGRAM_PARSER.parse("a(1). " + "c(X) :- a(X), b(X). " + "b(X) :- something(X)."); - testPermissiveGrounderHeuristicTolerance(program, 0, literal("a", "X"), 1, 1, true, Arrays.asList(1)); + testPermissiveGrounderHeuristicTolerance(program, 0, litAX, 1, 1, true, Arrays.asList(1)); } @Test public void testPermissiveGrounderHeuristicTolerance_1_reject() { - Program program = PARSER.parse("a(1). " + Program program = PROGRAM_PARSER.parse("a(1). " + "c(X) :- a(X), b(X), b(X+1). " + "b(X) :- something(X)."); - testPermissiveGrounderHeuristicTolerance(program, 0, literal("a", "X"), 1, 1, false, Arrays.asList(2)); + testPermissiveGrounderHeuristicTolerance(program, 0, litAX, 1, 1, false, Arrays.asList(2)); } @Test public void testPermissiveGrounderHeuristicTolerance_2_accept() { - Program program = PARSER.parse("a(1). " + Program program = PROGRAM_PARSER.parse("a(1). " + "c(X) :- a(X), b(X), b(X+1). " + "b(X) :- something(X)."); - testPermissiveGrounderHeuristicTolerance(program, 0, literal("a", "X"), 1, 2, true, Arrays.asList(2)); + testPermissiveGrounderHeuristicTolerance(program, 0, litAX, 1, 2, true, Arrays.asList(2)); } @Test public void testPermissiveGrounderHeuristicTolerance_1_accept_two_substitutions() { - Program program = PARSER.parse("a(1). " + Program program = PROGRAM_PARSER.parse("a(1). " + "c(X) :- a(X), b(X,Y). " + "b(X,Y) :- something(X,Y)."); - testPermissiveGrounderHeuristicTolerance(program, 0, literal("a", "X"), 1, 1, new ThriceTruth[] {TRUE, TRUE}, 2, true, Arrays.asList(0, 0)); + testPermissiveGrounderHeuristicTolerance(program, 0, litAX, 1, 1, new ThriceTruth[] {TRUE, TRUE}, 2, true, Arrays.asList(0, 0)); } @Test public void testPermissiveGrounderHeuristicTolerance_1_accept_accept_two_substitutions_with_different_remaining_tolerances() { - Program program = PARSER.parse("a(1). " + Program program = PROGRAM_PARSER.parse("a(1). " + "c(X) :- a(1), b(X,Y). " + "b(X,Y) :- something(X,Y)."); - testPermissiveGrounderHeuristicTolerance(program, 0, literal("a", 1), 1, 1, new ThriceTruth[] {null, null}, 2, true, Arrays.asList(1, 1)); + testPermissiveGrounderHeuristicTolerance(program, 0, litA1, 1, 1, new ThriceTruth[] {null, null}, 2, true, Arrays.asList(1, 1)); } @Test public void testPermissiveGrounderHeuristicTolerance_2_reject() { - Program program = PARSER.parse("a(1). " + Program program = PROGRAM_PARSER.parse("a(1). " + "c(X) :- a(X), b(X), b(X+1), b(X+2). " + "b(X) :- something(X)."); - testPermissiveGrounderHeuristicTolerance(program, 0, literal("a", "X"), 1, 2, false, Arrays.asList(3)); + testPermissiveGrounderHeuristicTolerance(program, 0, litAX, 1, 2, false, Arrays.asList(3)); } @Test public void testPermissiveGrounderHeuristicTolerance_2_accept_multiple_facts_of_same_variable() { - Program program = PARSER.parse("a(1). b(1). " + Program program = PROGRAM_PARSER.parse("a(1). b(1). " + "c(X) :- a(X), b(X), b(X+1), b(X+2). " + "b(X) :- something(X)."); - testPermissiveGrounderHeuristicTolerance(program, 0, literal("a", "X"), 1, 2, true, Arrays.asList(2)); + testPermissiveGrounderHeuristicTolerance(program, 0, litAX, 1, 2, true, Arrays.asList(2)); } private void testPermissiveGrounderHeuristicTolerance(Program program, int ruleID, Literal startingLiteral, int startingInstance, int tolerance, boolean expectNoGoods, List expectedNumbersOfUnassignedPositiveBodyAtoms) { diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGeneratorTest.java b/src/test/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGeneratorTest.java index 14ee4374d..ab9867789 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGeneratorTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGeneratorTest.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2018 Siemens AG +/* + * Copyright (c) 2018, 2020 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -27,16 +27,22 @@ import at.ac.tuwien.kr.alpha.common.AtomStore; import at.ac.tuwien.kr.alpha.common.AtomStoreImpl; +import at.ac.tuwien.kr.alpha.common.NoGood; import at.ac.tuwien.kr.alpha.common.Program; import at.ac.tuwien.kr.alpha.common.Rule; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm; import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; +import at.ac.tuwien.kr.alpha.grounder.atoms.ChoiceAtom; +import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom; import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser; +import org.junit.Before; import org.junit.Test; import java.util.List; import static at.ac.tuwien.kr.alpha.common.Literals.atomOf; +import static at.ac.tuwien.kr.alpha.common.Literals.isNegated; import static org.junit.Assert.assertEquals; /** @@ -50,6 +56,11 @@ public class NoGoodGeneratorTest { private static final VariableTerm X = VariableTerm.getInstance("X"); private static final VariableTerm Y = VariableTerm.getInstance("Y"); + + @Before + public void setUp() { + NonGroundRule.ID_GENERATOR.resetGenerator(); + } /** * Calls {@link NoGoodGenerator#collectNegLiterals(NonGroundRule, Substitution)}, @@ -70,10 +81,89 @@ public void collectNeg_ContainsOnlyPositiveLiterals() { Substitution substitution = new Substitution(); substitution.unifyTerms(X, A); substitution.unifyTerms(Y, B); - List collectedNeg = noGoodGenerator.collectNegLiterals(nonGroundRule, substitution); + List collectedNeg = noGoodGenerator.collectNegLiterals(nonGroundRule, substitution).getCollectedGroundLiterals(); assertEquals(1, collectedNeg.size()); String negAtomString = atomStore.atomToString(atomOf(collectedNeg.get(0))); assertEquals("q(a, b)", negAtomString); } + @Test + public void testNonGroundNoGoods_normalRuleWithArithmetics() { + final Program program = PARSER.parse("p(1,1). " + + "{ p(X1,Y) } :- p(X,Y), X1=X+1. " + + "q(X,Y) :- p(X,Y), X1=X+1, not p(X1,Y)."); + final Rule rule = program.getRules().get(1); + final AtomStore atomStore = new AtomStoreImpl(); + final Grounder grounder = GrounderFactory.getInstance("naive", program, atomStore, true); + final NoGoodGenerator noGoodGenerator = ((NaiveGrounder)grounder).noGoodGenerator; + final NonGroundRule nonGroundRule = NonGroundRule.constructNonGroundRule(rule); + final Substitution substitution = new Substitution(); + + substitution.put(VariableTerm.getInstance("X"), ConstantTerm.getInstance(2)); + substitution.put(VariableTerm.getInstance("X1"), ConstantTerm.getInstance(3)); + substitution.put(VariableTerm.getInstance("Y"), ConstantTerm.getInstance(1)); + final List noGoods = noGoodGenerator.generateNoGoodsFromGroundSubstitution(nonGroundRule, substitution); + + assertEquals(6, noGoods.size()); + int seenExpected = 0; + for (NoGood noGood : noGoods) { + final boolean hasHead = noGood.hasHead(); + final int headAtom = atomOf(noGood.getHead()); + final Integer firstLiteral = noGood.getLiteral(0); + final String groundNoGoodToString = atomStore.noGoodToString(noGood); + final String nonGroundNoGoodToString = noGood.getNonGroundNoGood() == null ? null : noGood.getNonGroundNoGood().toString(); + if (hasHead && atomStore.get(headAtom).getPredicate().getName().equals("q")) { + // head to body + expectNonGroundNoGoodForGroundNoGood(groundNoGoodToString, "*{ -(q(X, Y)), +(_R_(\"3\",(X, X1, Y))) }", nonGroundNoGoodToString); + } else if (hasHead && atomStore.get(headAtom) instanceof RuleAtom) { + // body-representing atom to full body + expectNonGroundNoGoodForGroundNoGood(groundNoGoodToString, "*{ -(_R_(\"3\",(X, X1, Y))), +(p(X, Y)), -(p(X1, Y)), +(X1 = X + 1) }", nonGroundNoGoodToString); + } else if (!hasHead && isNegated(firstLiteral)) { + // positive body atom to body-representing atom + expectNonGroundNoGoodForGroundNoGood(groundNoGoodToString, "{ -(p(X, Y)), +(_R_(\"3\",(X, X1, Y))) }", nonGroundNoGoodToString); + } else if (!hasHead && !isNegated(firstLiteral)) { + // negative body atom to body-representing atom + expectNonGroundNoGoodForGroundNoGood(groundNoGoodToString, "{ +(p(X1, Y)), +(_R_(\"3\",(X, X1, Y))) }", nonGroundNoGoodToString); + } else if (hasHead && atomStore.get(atomOf(firstLiteral)).getPredicate().equals(ChoiceAtom.OFF)) { + // ChoiceOff + expectNonGroundNoGoodForGroundNoGood(groundNoGoodToString, null, nonGroundNoGoodToString); + } else if (hasHead && atomStore.get(atomOf(firstLiteral)).getPredicate().equals(ChoiceAtom.ON)) { + // ChoiceOn + expectNonGroundNoGoodForGroundNoGood(groundNoGoodToString, null, nonGroundNoGoodToString); + } else { + continue; + } + seenExpected++; + } + assertEquals(6, seenExpected); + } + + @Test + public void testNonGroundNoGoods_constraint() { + final Program program = PARSER.parse("p(1,1). " + + "{ p(X1,Y) } :- p(X,Y), X1=X+1. " + + ":- p(X,Y), X1=X+1, not p(X1,Y)."); + final Rule rule = program.getRules().get(1); + final AtomStore atomStore = new AtomStoreImpl(); + final Grounder grounder = GrounderFactory.getInstance("naive", program, atomStore, true); + final NoGoodGenerator noGoodGenerator = ((NaiveGrounder)grounder).noGoodGenerator; + final NonGroundRule nonGroundRule = NonGroundRule.constructNonGroundRule(rule); + final Substitution substitution = new Substitution(); + + substitution.put(VariableTerm.getInstance("X"), ConstantTerm.getInstance(2)); + substitution.put(VariableTerm.getInstance("X1"), ConstantTerm.getInstance(3)); + substitution.put(VariableTerm.getInstance("Y"), ConstantTerm.getInstance(1)); + final List noGoods = noGoodGenerator.generateNoGoodsFromGroundSubstitution(nonGroundRule, substitution); + + assertEquals(1, noGoods.size()); + final NoGood noGood = noGoods.get(0); + final String groundNoGoodToString = atomStore.noGoodToString(noGood); + final String nonGroundNoGoodToString = noGood.getNonGroundNoGood() == null ? null : noGood.getNonGroundNoGood().toString(); + expectNonGroundNoGoodForGroundNoGood(groundNoGoodToString, "{ +(p(X, Y)), -(p(X1, Y)), +(X1 = X + 1) }", nonGroundNoGoodToString); + } + + private void expectNonGroundNoGoodForGroundNoGood(String groundNoGoodToString, String expectedNonGroundNoGoodToString, String nonGroundNoGoodToString) { + assertEquals("Unexpected non-ground nogood for ground nogood " + groundNoGoodToString, expectedNonGroundNoGoodToString, nonGroundNoGoodToString); + } + } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/RuleGroundingOrderTest.java b/src/test/java/at/ac/tuwien/kr/alpha/grounder/RuleGroundingOrderTest.java index 8c6b53c41..5d0b5f1a8 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/grounder/RuleGroundingOrderTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/grounder/RuleGroundingOrderTest.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2017-2019, the Alpha Team. +/* + * Copyright (c) 2017-2020, the Alpha Team. * All rights reserved. * * Additional changes made by Siemens. @@ -31,25 +31,27 @@ import at.ac.tuwien.kr.alpha.common.Rule; import at.ac.tuwien.kr.alpha.common.atoms.Literal; import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser; +import at.ac.tuwien.kr.alpha.grounder.parser.ProgramPartParser; import at.ac.tuwien.kr.alpha.grounder.transformation.VariableEqualityRemoval; import org.junit.Test; import java.io.IOException; -import static at.ac.tuwien.kr.alpha.TestUtil.literal; -import static org.junit.Assert.*; +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertTrue; +import static org.junit.Assert.fail; /** * Copyright (c) 2017-2019, the Alpha Team. */ public class RuleGroundingOrderTest { - - private final ProgramParser parser = new ProgramParser(); + private static final ProgramParser PROGRAM_PARSER = new ProgramParser(); + private static final ProgramPartParser PROGRAM_PART_PARSER = new ProgramPartParser(); @Test public void groundingOrder() throws IOException { - Program program = parser.parse("h(X,C) :- p(X,Y), q(A,B), r(Y,A), s(C)." + + Program program = PROGRAM_PARSER.parse("h(X,C) :- p(X,Y), q(A,B), r(Y,A), s(C)." + "j(A,B,X,Y) :- r1(A,B), r1(X,Y), r1(A,X), r1(B,Y), A = B." + "p(a) :- b = a."); new VariableEqualityRemoval().transform(program); @@ -74,21 +76,21 @@ public void groundingOrder() throws IOException { @Test(expected = RuntimeException.class) public void groundingOrderUnsafe() throws IOException { - Program program = parser.parse("h(X,C) :- X = Y, Y = C .. 3, C = X."); + Program program = PROGRAM_PARSER.parse("h(X,C) :- X = Y, Y = C .. 3, C = X."); new VariableEqualityRemoval().transform(program); computeGroundingOrdersForRule(program, 0); } @Test public void testPositionFromWhichAllVarsAreBound_ground() { - Program program = parser.parse("a :- b, not c."); + Program program = PROGRAM_PARSER.parse("a :- b, not c."); RuleGroundingOrders rgo0 = computeGroundingOrdersForRule(program, 0); assertEquals(0, rgo0.getFixedGroundingOrder().getPositionFromWhichAllVarsAreBound()); } @Test public void testPositionFromWhichAllVarsAreBound_simpleNonGround() { - Program program = parser.parse("a(X) :- b(X), not c(X)."); + Program program = PROGRAM_PARSER.parse("a(X) :- b(X), not c(X)."); RuleGroundingOrders rgo0 = computeGroundingOrdersForRule(program, 0); assertEquals(1, rgo0.getStartingLiterals().size()); for (Literal startingLiteral : rgo0.getStartingLiterals()) { @@ -98,7 +100,7 @@ public void testPositionFromWhichAllVarsAreBound_simpleNonGround() { @Test public void testPositionFromWhichAllVarsAreBound_longerSimpleNonGround() { - Program program = parser.parse("a(X) :- b(X), c(X), d(X), not e(X)."); + Program program = PROGRAM_PARSER.parse("a(X) :- b(X), c(X), d(X), not e(X)."); RuleGroundingOrders rgo0 = computeGroundingOrdersForRule(program, 0); assertEquals(3, rgo0.getStartingLiterals().size()); for (Literal startingLiteral : rgo0.getStartingLiterals()) { @@ -108,7 +110,7 @@ public void testPositionFromWhichAllVarsAreBound_longerSimpleNonGround() { @Test public void testToString_longerSimpleNonGround() { - Program program = parser.parse("a(X) :- b(X), c(X), d(X), not e(X)."); + Program program = PROGRAM_PARSER.parse("a(X) :- b(X), c(X), d(X), not e(X)."); RuleGroundingOrders rgo0 = computeGroundingOrdersForRule(program, 0); assertEquals(3, rgo0.getStartingLiterals().size()); for (Literal startingLiteral : rgo0.getStartingLiterals()) { @@ -123,16 +125,20 @@ public void testToString_longerSimpleNonGround() { @Test public void testPositionFromWhichAllVarsAreBound_joinedNonGround() { - Program program = parser.parse("a(X) :- b(X), c(X,Y), d(X,Z), not e(X)."); + Program program = PROGRAM_PARSER.parse("a(X) :- b(X), c(X,Y), d(X,Z), not e(X)."); RuleGroundingOrders rgo0 = computeGroundingOrdersForRule(program, 0); - assertTrue(2 <= rgo0.orderStartingFrom(literal("b", "X")).getPositionFromWhichAllVarsAreBound()); - assertTrue(1 <= rgo0.orderStartingFrom(literal("c", "X", "Y")).getPositionFromWhichAllVarsAreBound()); - assertTrue(1 <= rgo0.orderStartingFrom(literal("d", "X", "Z")).getPositionFromWhichAllVarsAreBound()); + final Literal litBX = PROGRAM_PART_PARSER.parseLiteral("b(X)"); + final Literal litCXY = PROGRAM_PART_PARSER.parseLiteral("c(X,Y)"); + final Literal litDXZ = PROGRAM_PART_PARSER.parseLiteral("d(X,Z)"); + assertTrue(2 <= rgo0.orderStartingFrom(litBX).getPositionFromWhichAllVarsAreBound()); + assertTrue(1 <= rgo0.orderStartingFrom(litCXY).getPositionFromWhichAllVarsAreBound()); + assertTrue(1 <= rgo0.orderStartingFrom(litDXZ).getPositionFromWhichAllVarsAreBound()); } private RuleGroundingOrders computeGroundingOrdersForRule(Program program, int ruleIndex) { Rule rule = program.getRules().get(ruleIndex); - NonGroundRule nonGroundRule = NonGroundRule.constructNonGroundRule(rule); + final NonGroundRule nonGroundRule1 = NonGroundRule.constructNonGroundRule(rule); + NonGroundRule nonGroundRule = nonGroundRule1; RuleGroundingOrders rgo = new RuleGroundingOrders(nonGroundRule); rgo.computeGroundingOrders(); return rgo; diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/UnifierTest.java b/src/test/java/at/ac/tuwien/kr/alpha/grounder/UnifierTest.java deleted file mode 100644 index 4ea4dd92c..000000000 --- a/src/test/java/at/ac/tuwien/kr/alpha/grounder/UnifierTest.java +++ /dev/null @@ -1,139 +0,0 @@ -package at.ac.tuwien.kr.alpha.grounder; - -import at.ac.tuwien.kr.alpha.common.Predicate; -import at.ac.tuwien.kr.alpha.common.Program; -import at.ac.tuwien.kr.alpha.common.Rule; -import at.ac.tuwien.kr.alpha.common.atoms.Atom; -import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; -import at.ac.tuwien.kr.alpha.common.atoms.BasicLiteral; -import at.ac.tuwien.kr.alpha.common.atoms.Literal; -import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm; -import at.ac.tuwien.kr.alpha.common.terms.FunctionTerm; -import at.ac.tuwien.kr.alpha.common.terms.Term; -import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; -import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser; -import org.junit.Test; - -import java.util.Arrays; - -import static org.junit.Assert.assertEquals; - -/** - * Copyright (c) 2018, the Alpha Team. - */ -public class UnifierTest extends SubstitutionTest { - - @Test - public void extendUnifier() { - VariableTerm varX = VariableTerm.getInstance("X"); - VariableTerm varY = VariableTerm.getInstance("Y"); - Unifier sub1 = new Unifier(); - sub1.put(varX, varY); - Unifier sub2 = new Unifier(); - sub2.put(varY, ConstantTerm.getInstance("a")); - - sub1.extendWith(sub2); - BasicAtom atom1 = parseAtom("p(X)"); - - Atom atomSubstituted = atom1.substitute(sub1); - assertEquals(ConstantTerm.getInstance("a"), atomSubstituted.getTerms().get(0)); - } - - @Test - public void mergeUnifierIntoLeft() { - VariableTerm varX = VariableTerm.getInstance("X"); - VariableTerm varY = VariableTerm.getInstance("Y"); - VariableTerm varZ = VariableTerm.getInstance("Z"); - Term constA = ConstantTerm.getInstance("a"); - Unifier left = new Unifier(); - left.put(varX, varY); - left.put(varZ, varY); - Unifier right = new Unifier(); - right.put(varX, constA); - Unifier merged = Unifier.mergeIntoLeft(left, right); - assertEquals(constA, merged.eval(varY)); - assertEquals(constA, merged.eval(varZ)); - } - - private BasicAtom parseAtom(String atom) { - ProgramParser programParser = new ProgramParser(); - Program program = programParser.parse(atom + "."); - return (BasicAtom) program.getFacts().get(0); - } - - @Test - public void unifyTermsSimpleBinding() throws Exception { - Substitution substitution = new Unifier(); - substitution.unifyTerms(Y, A); - assertEquals(A, substitution.eval(Y)); - } - - @Test - public void unifyTermsFunctionTermBinding() throws Exception { - Substitution substitution = new Unifier(); - substitution.put(Y, A); - - FunctionTerm groundFunctionTerm = FunctionTerm.getInstance("f", B, C); - Term nongroundFunctionTerm = FunctionTerm.getInstance("f", B, X); - - substitution.unifyTerms(nongroundFunctionTerm, groundFunctionTerm); - - assertEquals(C, substitution.eval(X)); - assertEquals(A, substitution.eval(Y)); - } - - @Test - public void substitutePositiveBasicAtom() { - substituteBasicAtomLiteral(false); - } - - @Test - public void substituteNegativeBasicAtom() { - substituteBasicAtomLiteral(true); - } - - @Test - public void groundAndPrintRule() { - Rule rule = PARSER.parse("x :- p(X,Y), not q(X,Y).").getRules().get(0); - NonGroundRule nonGroundRule = NonGroundRule.constructNonGroundRule(rule); - Substitution substitution = new Unifier(); - substitution.unifyTerms(X, A); - substitution.unifyTerms(Y, B); - String printedString = NaiveGrounder.groundAndPrintRule(nonGroundRule, substitution); - assertEquals("x :- p(a, b), not q(a, b).", printedString); - } - - private void substituteBasicAtomLiteral(boolean negated) { - Predicate p = Predicate.getInstance("p", 2); - BasicAtom atom = new BasicAtom(p, Arrays.asList(X, Y)); - Literal literal = new BasicLiteral(atom, !negated); - Substitution substitution = new Unifier(); - substitution.unifyTerms(X, A); - substitution.unifyTerms(Y, B); - literal = literal.substitute(substitution); - assertEquals(p, literal.getPredicate()); - assertEquals(A, literal.getTerms().get(0)); - assertEquals(B, literal.getTerms().get(1)); - assertEquals(negated, literal.isNegated()); - } - - @Test - public void groundLiteralToString_PositiveBasicAtom() { - groundLiteralToString(false); - } - - @Test - public void groundLiteralToString_NegativeBasicAtom() { - groundLiteralToString(true); - } - - private void groundLiteralToString(boolean negated) { - Predicate p = Predicate.getInstance("p", 2); - BasicAtom atom = new BasicAtom(p, Arrays.asList(X, Y)); - Substitution substitution = new Unifier(); - substitution.unifyTerms(X, A); - substitution.unifyTerms(Y, B); - String printedString = NaiveGrounder.groundLiteralToString(atom.toLiteral(!negated), substitution, true); - assertEquals((negated ? "not " : "") + "p(a, b)", printedString); - } -} \ No newline at end of file diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/AtomCounterTests.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/AtomCounterTests.java index d3729a8ad..ad20f2352 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/AtomCounterTests.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/AtomCounterTests.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2019 Siemens AG +/* + * Copyright (c) 2019-2020 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -31,13 +31,13 @@ import at.ac.tuwien.kr.alpha.common.DisjunctiveHead; import at.ac.tuwien.kr.alpha.common.Predicate; import at.ac.tuwien.kr.alpha.common.Rule; +import at.ac.tuwien.kr.alpha.common.Substitution; import at.ac.tuwien.kr.alpha.common.atoms.AggregateAtom; import at.ac.tuwien.kr.alpha.common.atoms.Atom; import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm; import at.ac.tuwien.kr.alpha.common.terms.Term; import at.ac.tuwien.kr.alpha.grounder.NonGroundRule; -import at.ac.tuwien.kr.alpha.grounder.Substitution; import at.ac.tuwien.kr.alpha.grounder.atoms.ChoiceAtom; import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom; import org.junit.Before; @@ -120,7 +120,7 @@ private void createChoiceAtom() { private void createRuleAtom() { Atom atomAA = new BasicAtom(Predicate.getInstance("aa", 0)); Rule ruleAA = new Rule(new DisjunctiveHead(Collections.singletonList(atomAA)), Collections.singletonList(new BasicAtom(Predicate.getInstance("bb", 0)).toLiteral(false))); - atomStore.putIfAbsent(new RuleAtom(NonGroundRule.constructNonGroundRule(ruleAA), new Substitution())); + atomStore.putIfAbsent(RuleAtom.ground(NonGroundRule.constructNonGroundRule(ruleAA), new Substitution())); } private void expectGetNumberOfAtoms(AtomCounter atomCounter, Class classOfAtoms, int expectedNumber) { diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletionTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletionTest.java index ab6afb5eb..eb45ac662 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletionTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletionTest.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2019, the Alpha Team. +/* + * Copyright (c) 2019-2020, the Alpha Team. * All rights reserved. * * Additional changes made by Siemens. @@ -27,18 +27,23 @@ */ package at.ac.tuwien.kr.alpha.solver; -import at.ac.tuwien.kr.alpha.common.*; +import at.ac.tuwien.kr.alpha.common.AtomStore; +import at.ac.tuwien.kr.alpha.common.AtomStoreImpl; +import at.ac.tuwien.kr.alpha.common.AtomStoreTest; +import at.ac.tuwien.kr.alpha.common.NoGood; +import at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type; import org.junit.Before; import org.junit.Test; -import at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type; - import java.util.HashMap; import java.util.List; import java.util.Map; import static at.ac.tuwien.kr.alpha.common.NoGoodTest.fromOldLiterals; -import static org.junit.Assert.*; +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertFalse; +import static org.junit.Assert.assertNull; +import static org.junit.Assert.assertTrue; public class LearnedNoGoodDeletionTest { @@ -140,7 +145,7 @@ public void testDeletionReducesNumberOfLearntNoGoods() { private Map countNoGoodsByType(NoGoodStore store) { final Map counters = new HashMap<>(); - final NoGoodCounter noGoodCounter = store.getNoGoodCounter(); + final NoGoodCounter noGoodCounter = store.getNoGoodCounter(); for (Type type : Type.values()) { counters.put(type, noGoodCounter.getNumberOfNoGoods(type)); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/SolverStatisticsTests.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/SolverStatisticsTests.java index a5f9df004..92ab83905 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/SolverStatisticsTests.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/SolverStatisticsTests.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2017-2019 Siemens AG +/* + * Copyright (c) 2017-2020 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -88,14 +88,14 @@ private void collectAnswerSetsAndCheckStats(Solver solver, int expectedNumberOfA private void collectAnswerSetsAndCheckNoGoodCounterStatsByType(Solver solver, int expectedNumberOfStaticNoGoods, int expectedNumberOfSupportNoGoods, int expectedNumberOfLearntNoGoods, int expectedNumberOfInternalNoGoods) { solver.collectSet(); SolverMaintainingStatistics solverMaintainingStatistics = (SolverMaintainingStatistics) solver; - final NoGoodCounter noGoodCounter = solverMaintainingStatistics.getNoGoodCounter(); + final NoGoodCounter noGoodCounter = solverMaintainingStatistics.getNoGoodCounter(); assertEquals("STATIC: " + expectedNumberOfStaticNoGoods + " SUPPORT: " + expectedNumberOfSupportNoGoods + " LEARNT: " + expectedNumberOfLearntNoGoods + " INTERNAL: " + expectedNumberOfInternalNoGoods, noGoodCounter.getStatsByType()); } private void collectAnswerSetsAndCheckNoGoodCounterStatsByCardinality(Solver solver, int expectedNumberOfUnaryNoGoods, int expectedNumberOfBinaryNoGoods, int expectedNumberOfNAryNoGoods) { solver.collectSet(); SolverMaintainingStatistics solverMaintainingStatistics = (SolverMaintainingStatistics) solver; - final NoGoodCounter noGoodCounter = solverMaintainingStatistics.getNoGoodCounter(); + final NoGoodCounter noGoodCounter = solverMaintainingStatistics.getNoGoodCounter(); assertEquals("unary: " + expectedNumberOfUnaryNoGoods + " binary: " + expectedNumberOfBinaryNoGoods + " larger: " + expectedNumberOfNAryNoGoods, noGoodCounter.getStatsByCardinality()); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMinTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMinTest.java index 29227058f..6a32d0638 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMinTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMinTest.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2016-2018 Siemens AG +/* + * Copyright (c) 2016-2020 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -32,7 +32,7 @@ import at.ac.tuwien.kr.alpha.solver.NaiveNoGoodStore; import at.ac.tuwien.kr.alpha.solver.TrailAssignment; import at.ac.tuwien.kr.alpha.solver.WritableAssignment; -import at.ac.tuwien.kr.alpha.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult; +import at.ac.tuwien.kr.alpha.solver.learning.ConflictAnalysisResult; import org.junit.Before; import org.junit.Test; @@ -45,8 +45,6 @@ /** * Tests {@link BerkMin}. - * - * Copyright (c) 2016 Siemens AG * */ public class BerkMinTest { diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSTest.java index e4f4f714f..8e1e60261 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSTest.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2018-2019 Siemens AG +/* + * Copyright (c) 2018-2020 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -25,11 +25,15 @@ */ package at.ac.tuwien.kr.alpha.solver.heuristics; -import at.ac.tuwien.kr.alpha.common.*; +import at.ac.tuwien.kr.alpha.common.AtomStore; +import at.ac.tuwien.kr.alpha.common.AtomStoreImpl; +import at.ac.tuwien.kr.alpha.common.AtomStoreTest; +import at.ac.tuwien.kr.alpha.common.Literals; +import at.ac.tuwien.kr.alpha.common.NoGood; import at.ac.tuwien.kr.alpha.solver.NoGoodStoreAlphaRoaming; import at.ac.tuwien.kr.alpha.solver.TrailAssignment; import at.ac.tuwien.kr.alpha.solver.WritableAssignment; -import at.ac.tuwien.kr.alpha.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult; +import at.ac.tuwien.kr.alpha.solver.learning.ConflictAnalysisResult; import org.junit.Before; import org.junit.Test; diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearnerTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearnerTest.java index 238894bbd..3d1e93242 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearnerTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearnerTest.java @@ -4,13 +4,23 @@ import at.ac.tuwien.kr.alpha.common.AtomStoreImpl; import at.ac.tuwien.kr.alpha.common.AtomStoreTest; import at.ac.tuwien.kr.alpha.common.NoGood; -import at.ac.tuwien.kr.alpha.solver.*; +import at.ac.tuwien.kr.alpha.solver.Antecedent; +import at.ac.tuwien.kr.alpha.solver.ConflictCause; +import at.ac.tuwien.kr.alpha.solver.NoGoodStore; +import at.ac.tuwien.kr.alpha.solver.NoGoodStoreAlphaRoaming; +import at.ac.tuwien.kr.alpha.solver.ThriceTruth; +import at.ac.tuwien.kr.alpha.solver.TrailAssignment; +import at.ac.tuwien.kr.alpha.solver.WritableAssignment; import org.junit.Ignore; import org.junit.Test; import static at.ac.tuwien.kr.alpha.common.NoGoodTest.fromOldLiterals; import static at.ac.tuwien.kr.alpha.solver.AntecedentTest.antecedentsEquals; -import static org.junit.Assert.*; +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertFalse; +import static org.junit.Assert.assertNotNull; +import static org.junit.Assert.assertNull; +import static org.junit.Assert.assertTrue; /** * Copyright (c) 2016-2019, the Alpha Team. @@ -61,7 +71,7 @@ public void smallConflictNonTrivial1UIP() { Antecedent violatedNoGood = conflictCause.getAntecedent(); assertNotNull(violatedNoGood); assertTrue(antecedentsEquals(violatedNoGood, n5.asAntecedent()) || antecedentsEquals(violatedNoGood, n7.asAntecedent())); - GroundConflictNoGoodLearner.ConflictAnalysisResult analysisResult = learner.analyzeConflictingNoGood(conflictCause.getAntecedent()); + ConflictAnalysisResult analysisResult = learner.analyzeConflictingNoGood(conflictCause.getAntecedent()); NoGood learnedNoGood = analysisResult.learnedNoGood; assertEquals(new NoGood(fromOldLiterals(1, -8)), learnedNoGood); int backjumpingDecisionLevel = analysisResult.backjumpLevel; @@ -83,7 +93,7 @@ public void subCurrentDLPropagationWithChoiceCauseOfConflict() { ConflictCause conflictCause = store.add(11, n2); assertNotNull(conflictCause); assertNotNull(conflictCause.getAntecedent()); - GroundConflictNoGoodLearner.ConflictAnalysisResult conflictAnalysisResult = learner.analyzeConflictingNoGood(conflictCause.getAntecedent()); + ConflictAnalysisResult conflictAnalysisResult = learner.analyzeConflictingNoGood(conflictCause.getAntecedent()); assertNull(conflictAnalysisResult.learnedNoGood); assertEquals(2, conflictAnalysisResult.backjumpLevel); diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/NonGroundConflictNoGoodLearnerTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/NonGroundConflictNoGoodLearnerTest.java new file mode 100644 index 000000000..f64508396 --- /dev/null +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/NonGroundConflictNoGoodLearnerTest.java @@ -0,0 +1,318 @@ +/* + * Copyright (c) 2020 Siemens AG + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * 1) Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * 2) Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ +package at.ac.tuwien.kr.alpha.solver.learning; + +import at.ac.tuwien.kr.alpha.common.AtomStore; +import at.ac.tuwien.kr.alpha.common.AtomStoreImpl; +import at.ac.tuwien.kr.alpha.common.DisjunctiveHead; +import at.ac.tuwien.kr.alpha.common.NoGood; +import at.ac.tuwien.kr.alpha.common.NonGroundNoGood; +import at.ac.tuwien.kr.alpha.common.Predicate; +import at.ac.tuwien.kr.alpha.common.Rule; +import at.ac.tuwien.kr.alpha.common.Substitution; +import at.ac.tuwien.kr.alpha.common.Unifier; +import at.ac.tuwien.kr.alpha.common.atoms.Atom; +import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; +import at.ac.tuwien.kr.alpha.common.atoms.ComparisonAtom; +import at.ac.tuwien.kr.alpha.common.atoms.Literal; +import at.ac.tuwien.kr.alpha.common.terms.ArithmeticTerm; +import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm; +import at.ac.tuwien.kr.alpha.common.terms.VariableTerm; +import at.ac.tuwien.kr.alpha.grounder.NoGoodGenerator; +import at.ac.tuwien.kr.alpha.grounder.NonGroundRule; +import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom; +import at.ac.tuwien.kr.alpha.solver.Antecedent; +import at.ac.tuwien.kr.alpha.solver.ConflictCause; +import at.ac.tuwien.kr.alpha.solver.NoGoodStore; +import at.ac.tuwien.kr.alpha.solver.NoGoodStoreAlphaRoaming; +import at.ac.tuwien.kr.alpha.solver.TrailAssignment; +import at.ac.tuwien.kr.alpha.solver.WritableAssignment; +import org.junit.Before; +import org.junit.Test; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.HashSet; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import static at.ac.tuwien.kr.alpha.Util.intArrayToLinkedHashSet; +import static at.ac.tuwien.kr.alpha.common.ComparisonOperator.EQ; +import static at.ac.tuwien.kr.alpha.common.ComparisonOperator.LT; +import static at.ac.tuwien.kr.alpha.common.Literals.atomToLiteral; +import static at.ac.tuwien.kr.alpha.common.terms.ArithmeticTerm.ArithmeticOperator.MINUS; +import static at.ac.tuwien.kr.alpha.solver.ThriceTruth.FALSE; +import static at.ac.tuwien.kr.alpha.solver.ThriceTruth.MBT; +import static at.ac.tuwien.kr.alpha.solver.ThriceTruth.TRUE; +import static java.util.Arrays.asList; +import static java.util.Collections.emptyList; +import static java.util.Collections.singletonList; +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertNotNull; +import static org.junit.Assert.assertNull; + +/** + * Tests {@link NonGroundConflictNoGoodLearner}. + */ +public class NonGroundConflictNoGoodLearnerTest { + + private WritableAssignment assignment; + private NoGoodStore store; + private AtomStore atomStore; + + @Before + public void setUp() { + atomStore = new AtomStoreImpl(); + this.assignment = new TrailAssignment(atomStore); + this.store = new NoGoodStoreAlphaRoaming(assignment); + } + + /** + * This is example 4.2.4 from: + * Joao Marques-Silva, Ines Lynce and Sharad Malik: Conflict-Driven Clause Learning SAT Solvers + * in: Armin Biere, Marijn Heule, Hans van Maaren and Toby Walsh (Eds.): Handbook of Satisfiability + */ + @Test + public void groundExampleFromSatisfiabilityHandbook() { + final GroundConflictNoGoodLearner groundLearner = new GroundConflictNoGoodLearner(assignment, atomStore); + final NonGroundConflictNoGoodLearner learner = new NonGroundConflictNoGoodLearner(assignment, atomStore, groundLearner); + int x1 = atomStore.putIfAbsent(new BasicAtom(Predicate.getInstance("x1", 0))); + int x2 = atomStore.putIfAbsent(new BasicAtom(Predicate.getInstance("x2", 0))); + int x3 = atomStore.putIfAbsent(new BasicAtom(Predicate.getInstance("x3", 0))); + int x4 = atomStore.putIfAbsent(new BasicAtom(Predicate.getInstance("x4", 0))); + int x5 = atomStore.putIfAbsent(new BasicAtom(Predicate.getInstance("x5", 0))); + int x6 = atomStore.putIfAbsent(new BasicAtom(Predicate.getInstance("x6", 0))); + int x21 = atomStore.putIfAbsent(new BasicAtom(Predicate.getInstance("x21", 0))); + int x31 = atomStore.putIfAbsent(new BasicAtom(Predicate.getInstance("x31", 0))); + int unrelated1 = atomStore.putIfAbsent(new BasicAtom(Predicate.getInstance("unrelated1", 0))); + int unrelated4 = atomStore.putIfAbsent(new BasicAtom(Predicate.getInstance("unrelated4", 0))); + final NoGood ng1 = new NoGood(atomToLiteral(x1, false), atomToLiteral(x31, false), atomToLiteral(x2, true)); + final NoGood ng2 = new NoGood(atomToLiteral(x1, false), atomToLiteral(x3, true)); + final NoGood ng3 = NoGood.headFirst(atomToLiteral(x4, false), atomToLiteral(x2, false), atomToLiteral(x3, false)); + final NoGood ng4 = new NoGood(atomToLiteral(x4, true), atomToLiteral(x5, true)); + final NoGood ng5 = new NoGood(atomToLiteral(x21, false), atomToLiteral(x4, true), atomToLiteral(x6, true)); + final NoGood ng6 = new NoGood(atomToLiteral(x5, false), atomToLiteral(x6, false)); + + store.growForMaxAtomId(atomStore.getMaxAtomId()); + this.assignment.growForMaxAtomId(); + + store.add(1, ng1); + store.add(2, ng2); + store.add(3, ng3); + store.add(4, ng4); + store.add(5, ng5); + store.add(6, ng6); + + assertEquals(0, assignment.getDecisionLevel()); + assignment.choose(unrelated1, TRUE); + ConflictCause conflictCause = store.propagate(); + assertNull(conflictCause); + assertEquals(1, assignment.getDecisionLevel()); + assignment.choose(x21, FALSE); + conflictCause = store.propagate(); + assertNull(conflictCause); + assertEquals(2, assignment.getDecisionLevel()); + assignment.choose(x31, FALSE); + conflictCause = store.propagate(); + assertNull(conflictCause); + assertEquals(3, assignment.getDecisionLevel()); + assignment.choose(unrelated4, TRUE); + conflictCause = store.propagate(); + assertNull(conflictCause); + assertEquals(4, assignment.getDecisionLevel()); + assignment.choose(x1, FALSE); + assertEquals(5, assignment.getDecisionLevel()); + conflictCause = store.propagate(); + assertEquals(FALSE, assignment.get(x2).getTruth()); + assertEquals(FALSE, assignment.get(x3).getTruth()); + assertEquals(TRUE, assignment.get(x4).getTruth()); + assertEquals(FALSE, assignment.get(x5).getTruth()); + assertEquals(FALSE, assignment.get(x6).getTruth()); + assertNotNull(conflictCause); + final Antecedent antecedent = conflictCause.getAntecedent(); + assertEquals(ng6, antecedent.getOriginalNoGood()); + + final ConflictAnalysisResult conflictAnalysisResult = learner.analyzeConflictingNoGoodAndGeneraliseConflict(antecedent); + Set expectedLearnedNoGood = new HashSet<>(); + expectedLearnedNoGood.add(atomToLiteral(x4, true)); + expectedLearnedNoGood.add(atomToLiteral(x21, false)); + assert conflictAnalysisResult.learnedNoGood != null; + assertEquals(expectedLearnedNoGood, intArrayToLinkedHashSet(conflictAnalysisResult.learnedNoGood.asAntecedent().getReasonLiterals())); + + final List additionalLearnedNoGoods = conflictAnalysisResult.getAdditionalLearnedNoGoods(); + assertEquals(1, additionalLearnedNoGoods.size()); + expectedLearnedNoGood = new HashSet<>(); + expectedLearnedNoGood.add(atomToLiteral(x1, false)); + expectedLearnedNoGood.add(atomToLiteral(x21, false)); + expectedLearnedNoGood.add(atomToLiteral(x31, false)); + System.out.println(atomStore.noGoodToString(additionalLearnedNoGoods.get(0))); + assertEquals(expectedLearnedNoGood, intArrayToLinkedHashSet(additionalLearnedNoGoods.get(0).asAntecedent().getReasonLiterals())); + } + + /** + * Tests non-ground learning on the following example:
+ * Nogood 1: { -(col(1,g), +(_R_("0", "{X->1,Col->g}") }, non-ground: { -(col(X,Col), +(_R_("0", (X,Col)) }
+ * Nogood 2: { -(col(0,g)), +(col(1,g)) }, non-ground: { -(col(Y,Col)), +(col(X,Col)), +(Y=X-1) }
+ * Nogood 3: { +(col(1,g)), +(col(0,g)) }, non-ground: { +(col(N,C)), +(col(M,C)), +(M + * When nogood 3 is violated, it is first resolved with nogood 2, learning a nogood at the first UIP, + * and then with nogood 1, learning another nogood at the second UIP. + */ + @Test + public void smallNonGroundExample() { + final GroundConflictNoGoodLearner groundLearner = new GroundConflictNoGoodLearner(assignment, atomStore); + final NonGroundConflictNoGoodLearner learner = new NonGroundConflictNoGoodLearner(assignment, atomStore, groundLearner); + + final Predicate predCol = Predicate.getInstance("col", 2); + final Predicate predUnrelated = Predicate.getInstance("unrelated", 2); + + final ConstantTerm const0 = ConstantTerm.getInstance(0); + final ConstantTerm const1 = ConstantTerm.getInstance(1); + final ConstantTerm constG = ConstantTerm.getInstance("g"); + + final int groundAtomCol0g = atomStore.putIfAbsent(new BasicAtom(predCol, const0, constG)); + final int groundAtomCol1g = atomStore.putIfAbsent(new BasicAtom(predCol, const1, constG)); + final int groundAtomUnrelated = atomStore.putIfAbsent(new BasicAtom(predUnrelated, const1, constG)); + + final VariableTerm varX = VariableTerm.getInstance("X"); + final VariableTerm varY = VariableTerm.getInstance("Y"); + final VariableTerm varC = VariableTerm.getInstance("C"); + final VariableTerm varM = VariableTerm.getInstance("M"); + final VariableTerm varN = VariableTerm.getInstance("N"); + final VariableTerm varCol = VariableTerm.getInstance("Col"); + + final Atom nonGroundAtomColXCol = new BasicAtom(predCol, varX, varCol); + final Atom nonGroundAtomColYCol = new BasicAtom(predCol, varY, varCol); + final Atom nonGroundAtomColMC = new BasicAtom(predCol, varM, varC); + final Atom nonGroundAtomColNC = new BasicAtom(predCol, varN, varC); + final Atom nonGroundAtomColXC = new BasicAtom(predCol, varX, varC); + final Atom unrelated = new BasicAtom(predUnrelated, varX, varCol); + + final Rule rule = new Rule(new DisjunctiveHead(singletonList(nonGroundAtomColXCol)), singletonList(unrelated.toLiteral())); + final NonGroundRule nonGroundRule = NonGroundRule.constructNonGroundRule(rule); + final Substitution substitution = new Substitution(); + substitution.put(varX, const1); + substitution.put(varCol, constG); + final int groundAtomR = atomStore.putIfAbsent(RuleAtom.ground(nonGroundRule, substitution)); + final RuleAtom nonGroundAtomR = RuleAtom.nonGround(nonGroundRule); + + final NoGood ng1 = NoGood.headFirst(atomToLiteral(groundAtomCol1g, false), atomToLiteral(groundAtomR)); + final Map atomMapping1 = new HashMap<>(); + atomMapping1.put(groundAtomCol1g, nonGroundAtomColXCol); + atomMapping1.put(groundAtomR, nonGroundAtomR); + ng1.setNonGroundNoGood(NonGroundNoGood.forGroundNoGood(ng1, atomMapping1)); + + final NoGood ng2 = NoGood.learnt(atomToLiteral(groundAtomCol0g, false), atomToLiteral(groundAtomCol1g)); + final Literal nonGroundComparisonLiteralYEqualsXMinus1 = new ComparisonAtom(varY, ArithmeticTerm.getInstance(varX, MINUS, const1), EQ).toLiteral(); + final NoGoodGenerator.CollectedLiterals positiveCollectedLiterals2 = new NoGoodGenerator.CollectedLiterals( + asList(atomToLiteral(groundAtomCol0g, false), atomToLiteral(groundAtomCol1g)), + asList(nonGroundAtomColYCol.toLiteral(false), nonGroundAtomColXCol.toLiteral()), + singletonList(nonGroundComparisonLiteralYEqualsXMinus1), + emptyList() + ); + final NoGoodGenerator.CollectedLiterals negativeCollectedLiterals2 = new NoGoodGenerator.CollectedLiterals(); + ng2.setNonGroundNoGood(NonGroundNoGood.fromBody(ng2, positiveCollectedLiterals2, negativeCollectedLiterals2, positiveCollectedLiterals2.getAtomMapping())); + + final List groundLiteralsInNoGood3 = asList(atomToLiteral(groundAtomCol1g), atomToLiteral(groundAtomCol0g)); + final NoGood ng3 = NoGood.fromConstraint(groundLiteralsInNoGood3, emptyList()); + final Literal nonGroundComparisonLiteralMLessThanN = new ComparisonAtom(varM, varN, LT).toLiteral(); + final NoGoodGenerator.CollectedLiterals positiveCollectedLiterals3 = new NoGoodGenerator.CollectedLiterals( + groundLiteralsInNoGood3, + asList(nonGroundAtomColNC.toLiteral(), nonGroundAtomColMC.toLiteral()), + singletonList(nonGroundComparisonLiteralMLessThanN), + emptyList() + ); + final NoGoodGenerator.CollectedLiterals negativeCollectedLiterals3 = new NoGoodGenerator.CollectedLiterals(); + ng3.setNonGroundNoGood(NonGroundNoGood.fromBody(ng3, positiveCollectedLiterals3, negativeCollectedLiterals3, positiveCollectedLiterals3.getAtomMapping())); + + store.growForMaxAtomId(atomStore.getMaxAtomId()); + this.assignment.growForMaxAtomId(); + + store.add(1, ng1); + store.add(2, ng2); + store.add(3, ng3); + + assertEquals(0, assignment.getDecisionLevel()); + ConflictCause conflictCause = assignment.choose(groundAtomUnrelated, TRUE); + assertNull(conflictCause); + conflictCause = store.propagate(); + assertNull(conflictCause); + assertEquals(1, assignment.getDecisionLevel()); + conflictCause = assignment.choose(groundAtomR, TRUE); + assertNull(conflictCause); + conflictCause = store.propagate(); + assertEquals(2, assignment.getDecisionLevel()); + assertEquals(TRUE, assignment.get(groundAtomCol1g).getTruth()); + assertEquals(MBT, assignment.get(groundAtomCol0g).getTruth()); + + assertNotNull(conflictCause); + final Antecedent antecedent = conflictCause.getAntecedent(); + assertEquals(ng3, antecedent.getOriginalNoGood()); + + final ConflictAnalysisResult conflictAnalysisResult = learner.analyzeConflictingNoGoodAndGeneraliseConflict(antecedent); + Set expectedLearnedNoGood1 = new LinkedHashSet<>(); + expectedLearnedNoGood1.add(atomToLiteral(groundAtomCol1g, true)); + assert conflictAnalysisResult.learnedNoGood != null; + assertEquals(expectedLearnedNoGood1, intArrayToLinkedHashSet(conflictAnalysisResult.learnedNoGood.asAntecedent().getReasonLiterals())); + + final Literal nonGroundComparisonLiteralMLessThanX = new ComparisonAtom(varM, varX, LT).toLiteral(); + final Literal nonGroundComparisonLiteralMEqualsXMinus1 = new ComparisonAtom(varM, ArithmeticTerm.getInstance(varX, MINUS, const1), EQ).toLiteral(); + + final NoGoodGenerator.CollectedLiterals positiveCollectedLiteralsLearned1 = new NoGoodGenerator.CollectedLiterals( + new ArrayList<>(expectedLearnedNoGood1), + singletonList(nonGroundAtomColXC.toLiteral()), + asList(nonGroundComparisonLiteralMLessThanX, nonGroundComparisonLiteralMEqualsXMinus1), + // TODO: comparison literals could be removed by learning algorithm because they involve variables that are not used anywhere else + emptyList() + ); + final NoGoodGenerator.CollectedLiterals negativeCollectedLiteralsLearned1 = new NoGoodGenerator.CollectedLiterals(); + final NonGroundNoGood expectedLearnedNonGroundNoGood1 = NonGroundNoGood.fromBody(conflictAnalysisResult.learnedNoGood, positiveCollectedLiteralsLearned1, negativeCollectedLiteralsLearned1, positiveCollectedLiteralsLearned1.getAtomMapping()); + assertEquals(expectedLearnedNonGroundNoGood1, conflictAnalysisResult.getLearnedNonGroundNoGood()); + + assertEquals(1, conflictAnalysisResult.getAdditionalLearnedNoGoods().size()); + assertEquals(1, conflictAnalysisResult.getAdditionalLearnedNonGroundNoGoods().size()); + + Set expectedLearnedNoGood2 = new LinkedHashSet<>(); + expectedLearnedNoGood2.add(atomToLiteral(groundAtomR, true)); + final NoGood learnedNoGood2 = conflictAnalysisResult.getAdditionalLearnedNoGoods().get(0); + assertEquals(expectedLearnedNoGood2, intArrayToLinkedHashSet(learnedNoGood2.asAntecedent().getReasonLiterals())); + + final Unifier ruleUnifier = new Unifier(); + ruleUnifier.put(varCol, varC); + final RuleAtom nonGroundAtomRenamedRule = nonGroundAtomR.substitute(ruleUnifier); + + final NoGoodGenerator.CollectedLiterals positiveCollectedLiteralsLearned2 = new NoGoodGenerator.CollectedLiterals( + new ArrayList<>(expectedLearnedNoGood2), + singletonList(nonGroundAtomRenamedRule.toLiteral()), + asList(nonGroundComparisonLiteralMLessThanX, nonGroundComparisonLiteralMEqualsXMinus1), + emptyList() + ); + final NoGoodGenerator.CollectedLiterals negativeCollectedLiteralsLearned2 = new NoGoodGenerator.CollectedLiterals(); + final NonGroundNoGood expectedLearnedNonGroundNoGood2 = NonGroundNoGood.fromBody(learnedNoGood2, positiveCollectedLiteralsLearned2, negativeCollectedLiteralsLearned2, positiveCollectedLiteralsLearned2.getAtomMapping()); + assertEquals(expectedLearnedNonGroundNoGood2, conflictAnalysisResult.getAdditionalLearnedNonGroundNoGoods().get(0)); + } +} \ No newline at end of file