Merge pull request #252 from alpha-asp/negated_externals

Fix evaluation of negated external atoms (Issue #234)

src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ComparisonLiteral.java

@@ -121,7 +121,7 @@ public Set<VariableTerm> getNonBindingVariables() {
 	}
 
 	@Override
-	public List<Substitution> getSubstitutions(Substitution partialSubstitution) {
+	public List<Substitution> getSatisfyingSubstitutions(Substitution partialSubstitution) {
 		// Treat case where this is just comparison with all variables bound by partialSubstitution.
 		final Term left = getAtom().getTerms().get(0).substitute(partialSubstitution);
 		final Term right = getAtom().getTerms().get(1).substitute(partialSubstitution);

src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ExternalLiteral.java

@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2017-2018, the Alpha Team.
+ * Copyright (c) 2017-2020, the Alpha Team.
  * All rights reserved.
  * 
  * Additional changes made by Siemens.
@@ -27,15 +27,17 @@
  */
 package at.ac.tuwien.kr.alpha.common.atoms;
 
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
+
 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 static java.util.Collections.emptyList;
-
 /**
  * Contains a potentially negated {@link ExternalAtom}.
  */
@@ -44,14 +46,15 @@ public class ExternalLiteral extends FixedInterpretationLiteral {
 	public ExternalLiteral(ExternalAtom atom, boolean positive) {
 		super(atom, positive);
 	}
-	
+
 	@Override
 	public ExternalAtom getAtom() {
-		return (ExternalAtom)atom;
+		return (ExternalAtom) atom;
 	}
 
 	/**
-	 * Returns a new copy of this literal whose {@link Literal#isNegated()} status is inverted
+	 * Returns a new copy of this literal whose {@link Literal#isNegated()} status
+	 * is inverted
 	 */
 	@Override
 	public ExternalLiteral negate() {
@@ -75,7 +78,7 @@ public Set<VariableTerm> getBindingVariables() {
 		if (!positive) {
 			return Collections.emptySet();
 		}
-		
+
 		List<Term> output = getAtom().getOutput();
 
 		Set<VariableTerm> binding = new HashSet<>(output.size());
@@ -93,15 +96,16 @@ public Set<VariableTerm> getBindingVariables() {
 	public Set<VariableTerm> getNonBindingVariables() {
 		List<Term> input = getAtom().getInput();
 		List<Term> output = getAtom().getOutput();
-		
+
 		// External atoms have their input always non-binding, since they cannot
 		// be queried without some concrete input.
 		Set<VariableTerm> nonbindingVariables = new HashSet<>();
 		for (Term term : input) {
 			nonbindingVariables.addAll(term.getOccurringVariables());
 		}
 
-		// If the external atom is negative, then all variables of input and output are non-binding.
+		// If the external atom is negative, then all variables of input and output are
+		// non-binding.
 		if (!positive) {
 			for (Term out : output) {
 				if (out instanceof VariableTerm) {
@@ -114,35 +118,83 @@ public Set<VariableTerm> getNonBindingVariables() {
 	}
 
 	@Override
-	public List<Substitution> getSubstitutions(Substitution partialSubstitution) {
+	public List<Substitution> getSatisfyingSubstitutions(Substitution partialSubstitution) {
 		List<Term> input = getAtom().getInput();
-		List<Term> output = getAtom().getOutput();
-		List<Substitution> substitutions = new ArrayList<>();
 		List<Term> substitutes = new ArrayList<>(input.size());
 
+		// In preparation for evaluating the external atom, set the input values according
+		// to the partial substitution supplied by the grounder.
 		for (Term t : input) {
 			substitutes.add(t.substitute(partialSubstitution));
 		}
-
 		Set<List<ConstantTerm<?>>> results = getAtom().getInterpretation().evaluate(substitutes);
-
 		if (results == null) {
 			throw new NullPointerException("Predicate " + getPredicate().getName() + " returned null. It must return a Set.");
 		}
 
-		if (results.isEmpty()) {
-			return emptyList();
+		if (this.isNegated()) {
+			return this.isNegatedLiteralSatisfied(results) ? Collections.singletonList(partialSubstitution) : Collections.emptyList();
+		} else {
+			return this.buildSubstitutionsForOutputs(partialSubstitution, results);
 		}
+	}
 
-		for (List<ConstantTerm<?>> bindings : results) {
-			if (bindings.size() < output.size()) {
-				throw new RuntimeException("Predicate " + getPredicate().getName() + " returned " + bindings.size() + " terms when at least " + output.size() + " were expected.");
+	/**
+	 * Checks whether this negated external literal is satisfied.
+	 * 
+	 * Note that this method must only be called on negated external literals.
+	 * In that case, the literal itself does not bind any output variables,
+	 * i.e. the underlying atom is satisfied iff the output terms obtained by
+	 * evaluating the underlying external atom match the values to which
+	 * the respective output variables are bound. The result of this method assumes
+	 * that the literal is negated, i.e. for the underlying atom AT, it represents
+	 * the truth value !AT.
+	 * Furthermore, this method assumes that the output terms of the underlying atom
+	 * are {@link ConstantTerm}s, i.e. that the grounder's current partial
+	 * substitution has already been applied to them. That assumption is safe since
+	 * in case of a negated external literal, the output variables are always
+	 * non-binding.
+	 * 
+	 * @param externalMethodResult The term lists obtained from evaluating the external atom
+	 *                (i.e. calling the java method) encapsulated by this literal
+	 * @return true iff no list in externalMethodResult equals the external atom's output term
+	 *         list as substituted by the grounder, false otherwise
+	 */
+	private boolean isNegatedLiteralSatisfied(Set<List<ConstantTerm<?>>> externalMethodResult) {
+		List<Term> externalAtomOutTerms = this.getAtom().getOutput();
+		boolean outputMatches;
+		for (List<ConstantTerm<?>> resultTerms : externalMethodResult) {
+			outputMatches = true;
+			for (int i = 0; i < externalAtomOutTerms.size(); i++) {
+				if (!resultTerms.get(i).equals(externalAtomOutTerms.get(i))) {
+					outputMatches = false;
+					break;
+				}
 			}
+			if (outputMatches) {
+				// We found one term list where all terms match the ground output terms of the
+				// external atom, therefore the atom is true and the (negative) literal false.
+				return false;
+			}
+		}
+		// We checked all term list and none matches the ground output terms, therefore
+		// the external atom is false, making the literal true.
+		return true;
+	}
 
+	private List<Substitution> buildSubstitutionsForOutputs(Substitution partialSubstitution, Set<List<ConstantTerm<?>>> outputs) {
+		List<Substitution> retVal = new ArrayList<>();
+		List<Term> externalAtomOutputTerms = this.getAtom().getOutput();
+		for (List<ConstantTerm<?>> bindings : outputs) {
+			if (bindings.size() < externalAtomOutputTerms.size()) {
+				throw new RuntimeException(
+						"Predicate " + getPredicate().getName() + " returned " + bindings.size() + " terms when at least " + externalAtomOutputTerms.size()
+								+ " were expected.");
+			}
 			Substitution ith = new Substitution(partialSubstitution);
 			boolean skip = false;
-			for (int i = 0; i < output.size(); i++) {
-				Term out = output.get(i);
+			for (int i = 0; i < externalAtomOutputTerms.size(); i++) {
+				Term out = externalAtomOutputTerms.get(i);
 
 				if (out instanceof VariableTerm) {
 					ith.put((VariableTerm) out, bindings.get(i));
@@ -153,13 +205,11 @@ public List<Substitution> getSubstitutions(Substitution partialSubstitution) {
 					}
 				}
 			}
-
 			if (!skip) {
-				substitutions.add(ith);
+				retVal.add(ith);
 			}
 		}
-
-		return substitutions;
+		return retVal;
 	}
 
 }

src/main/java/at/ac/tuwien/kr/alpha/common/atoms/FixedInterpretationLiteral.java

@@ -32,15 +32,31 @@
 import java.util.List;
 
 /**
- * Represents a literal whose ground truth value(s) are independent of the current assignment.
- * Examples of atoms underlying such literals are builtin atoms and external atoms.
+ * Represents a literal whose ground truth value(s) are independent of the
+ * current assignment.
+ * Examples of atoms underlying such literals are builtin atoms and external
+ * atoms.
  * Copyright (c) 2017-2018, the Alpha Team.
  */
 public abstract class FixedInterpretationLiteral extends Literal {
-	
+
 	public FixedInterpretationLiteral(Atom atom, boolean positive) {
 		super(atom, positive);
 	}
-
-	public abstract List<Substitution> getSubstitutions(Substitution partialSubstitution);
+
+	/**
+	 * Creates a list of {@link Substitution}s based on the given partial
+	 * substitution, such that
+	 * this {@link FixedInterpretationLiteral} is true in every returned
+	 * substitution.
+	 * In cases where this is not possible (because of conflicting variable
+	 * assignments in the partial substitution), getSatisfyingSubstitutions is
+	 * required to return an empty list
+	 * 
+	 * @param partialSubstitution a partial substitution that is required to bind
+	 *                            all variables that are non-binding in this literal
+	 * @return a list of substitutions, in each of which this literal is true, or an
+	 *         empty list if no such substitution exists
+	 */
+	public abstract List<Substitution> getSatisfyingSubstitutions(Substitution partialSubstitution);
 }

src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java

@@ -485,7 +485,7 @@ private BindingResult bindNextAtomInRule(RuleGroundingOrder groundingOrder, int
 			if (shallPushBackFixedInterpretationLiteral(substitutedLiteral)) {
 				return pushBackAndBindNextAtomInRule(groundingOrder, orderPosition, originalTolerance, remainingTolerance, partialSubstitution, currentAssignment);
 			}
-			final List<Substitution> substitutions = substitutedLiteral.getSubstitutions(partialSubstitution);
+			final List<Substitution> substitutions = substitutedLiteral.getSatisfyingSubstitutions(partialSubstitution);
 
 			if (substitutions.isEmpty()) {
 				// if FixedInterpretationLiteral cannot be satisfied now, it will never be

src/main/java/at/ac/tuwien/kr/alpha/grounder/atoms/IntervalLiteral.java

@@ -103,7 +103,7 @@ public Set<VariableTerm> getNonBindingVariables() {
 	}
 
 	@Override
-	public List<Substitution> getSubstitutions(Substitution partialSubstitution) {
+	public List<Substitution> getSatisfyingSubstitutions(Substitution partialSubstitution) {
 		// Substitute variables occurring in the interval itself.
 		IntervalLiteral groundInterval = substitute(partialSubstitution);
 		// Generate all substitutions for the interval representing variable.

src/test/java/at/ac/tuwien/kr/alpha/api/externals/stdlib/AspStandardLibraryTest.java

@@ -7,6 +7,8 @@
 
 import org.junit.Assert;
 import org.junit.Test;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
 
 import at.ac.tuwien.kr.alpha.api.Alpha;
 import at.ac.tuwien.kr.alpha.common.AnswerSet;
@@ -18,6 +20,8 @@
 
 public class AspStandardLibraryTest {
 
+	private static final Logger LOGGER = LoggerFactory.getLogger(AspStandardLibrary.class);
+
 	//@formatter:off
 	private static final String STRINGSTUFF_ASP =
 			"string(\"bla\")."
@@ -31,6 +35,19 @@ public class AspStandardLibraryTest {
 			+ ":- resultstring(S), not containsFoo(S)."
 			+ "has_resultstring :- resultstring(_)."
 			+ ":- not has_resultstring.";
+
+	// same as stringstuff asp, but without the "containsFoo" intermediate predicate
+	private static final String NEGATED_EXTERNAL_ASP =
+			"string(\"bla\")."
+			+ "string(\"blubb\")."
+			+ "string(\"foo\")."
+			+ "string(\"bar\")."
+			+ "{ strcat(S1, S2) } :- string(S1), string(S2)."
+			+ "resultstring(SCAT) :- strcat(S1, S2), &stdlib_string_concat[S1, S2](SCAT)."
+			+ ":- resultstring(S), &stdlib_string_length[S](LEN), LEN != 6."
+			+ ":- resultstring(S), not &stdlib_string_matches_regex[S, \".*foo.*\"]."
+			+ "has_resultstring :- resultstring(_)."
+			+ ":- not has_resultstring.";
 	//@formatter:on
 
 	@Test
@@ -82,21 +99,21 @@ public void datetimeBefore() {
 		Assert.assertFalse(AspStandardLibrary.datetimeIsBefore(2015, 5, 13, 12, 1, 33, 2003, 1, 1, 0, 0, 1));
 		Assert.assertFalse(AspStandardLibrary.datetimeIsBefore(2022, 2, 22, 22, 22, 22, 2022, 2, 22, 22, 22, 22));
 	}
-	
+
 	@Test
 	public void datetimeEqual() {
 		Assert.assertTrue(AspStandardLibrary.datetimeIsEqual(1990, 2, 14, 15, 16, 17, 1990, 2, 14, 15, 16, 17));
 		Assert.assertFalse(AspStandardLibrary.datetimeIsEqual(2015, 5, 13, 12, 1, 33, 2003, 1, 1, 0, 0, 1));
-	}	
+	}
 
 	@Test
 	public void datetimeBeforeOrEqual() {
 		Assert.assertTrue(AspStandardLibrary.datetimeIsBeforeOrEqual(1990, 2, 14, 15, 16, 17, 1990, 3, 1, 0, 59, 1));
 		Assert.assertFalse(AspStandardLibrary.datetimeIsBeforeOrEqual(2015, 5, 13, 12, 1, 33, 2003, 1, 1, 0, 0, 1));
 		Assert.assertTrue(AspStandardLibrary.datetimeIsBeforeOrEqual(2022, 2, 22, 22, 22, 22, 2022, 2, 22, 22, 22, 22));
-		
+
 	}
-	
+
 	@Test
 	public void matchesRegex() {
 		Assert.assertTrue(AspStandardLibrary.stringMatchesRegex("Blaaaaa Blubbb!!", "Bla+ Blub+!!"));
@@ -139,4 +156,22 @@ public void programWithStringStuff() throws IOException {
 		}
 	}
 
+	@Test
+	@SuppressWarnings("unchecked")
+	public void negatedExternal() throws IOException {
+		Alpha alpha = new Alpha();
+		Program prog = alpha.readProgram(InputConfig.forString(NEGATED_EXTERNAL_ASP));
+		Set<AnswerSet> answerSets = alpha.solve(prog).collect(Collectors.toSet());
+		Assert.assertEquals(31, answerSets.size());
+		// Verify every result string has length 6 and contains "foo"
+		for (AnswerSet as : answerSets) {
+			for (Atom atom : as.getPredicateInstances(Predicate.getInstance("resultstring", 1))) {
+				String resultstring = ((ConstantTerm<String>) atom.getTerms().get(0)).getObject();
+				LOGGER.debug("ResultString is {}", resultstring);
+				Assert.assertEquals(6, resultstring.length());
+				Assert.assertTrue(resultstring.contains("foo"));
+			}
+		}
+	}
+
 }