Additional ground nogoods generated for choice rules

src/main/java/at/ac/tuwien/kr/alpha/common/NegativeChoicePredicate.java

@@ -0,0 +1,46 @@
+/*
+ * Copyright (c) 2020, the Alpha Team.
+ * 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;
+
+public class NegativeChoicePredicate extends Predicate {
+
+	private final static String PREDICATE_NEGATION_PREFIX = "_n";
+
+	private final Predicate originalChoicePredicate;
+
+	protected NegativeChoicePredicate(Predicate originalChoicePredicate) {
+		super(PREDICATE_NEGATION_PREFIX + originalChoicePredicate.getName(), originalChoicePredicate.getArity() + 1, true, false);
+		this.originalChoicePredicate = originalChoicePredicate;
+	}
+
+	public static NegativeChoicePredicate getInstance(Predicate choicePredicate) {
+		return new NegativeChoicePredicate(choicePredicate);
+	}
+
+	public Predicate getOriginalChoicePredicate() {
+		return originalChoicePredicate;
+	}
+}

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-2020, the Alpha Team.
  * All rights reserved.
  * 
  * Additional changes made by Siemens.
@@ -27,30 +27,33 @@
  */
 package at.ac.tuwien.kr.alpha.grounder;
 
-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;
-
-import java.util.ArrayList;
-import java.util.HashSet;
-import java.util.LinkedHashSet;
-import java.util.List;
-import java.util.Map;
-import java.util.Set;
-
 import at.ac.tuwien.kr.alpha.common.AtomStore;
+import at.ac.tuwien.kr.alpha.common.NegativeChoicePredicate;
 import at.ac.tuwien.kr.alpha.common.NoGood;
 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.FixedInterpretationLiteral;
 import at.ac.tuwien.kr.alpha.common.atoms.Literal;
 import at.ac.tuwien.kr.alpha.common.program.InternalProgram;
 import at.ac.tuwien.kr.alpha.common.rule.InternalRule;
+import at.ac.tuwien.kr.alpha.common.terms.Term;
 import at.ac.tuwien.kr.alpha.grounder.atoms.EnumerationAtom;
 import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom;
 
+import java.util.ArrayList;
+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.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.
@@ -72,7 +75,7 @@ public class NoGoodGenerator {
 
 	/**
 	 * Generates all NoGoods resulting from a non-ground rule and a variable substitution.
-	 * 
+	 *
 	 * @param nonGroundRule
 	 *          the non-ground rule.
 	 * @param substitution
@@ -97,7 +100,7 @@ List<NoGood> generateNoGoodsFromGroundSubstitution(final InternalRule nonGroundR
 
 		final Atom groundHeadAtom = nonGroundRule.getHeadAtom().substitute(substitution);
 		final int headId = atomStore.putIfAbsent(groundHeadAtom);
-		
+
 		// Prepare atom representing the rule body.
 		final RuleAtom bodyAtom = new RuleAtom(nonGroundRule, substitution);
 
@@ -113,7 +116,7 @@ List<NoGood> generateNoGoodsFromGroundSubstitution(final InternalRule nonGroundR
 		final int headLiteral = atomToLiteral(atomStore.putIfAbsent(nonGroundRule.getHeadAtom().substitute(substitution)));
 
 		choiceRecorder.addHeadToBody(headId, atomOf(bodyRepresentingLiteral));
-		
+
 		// Create a nogood for the head.
 		result.add(NoGood.headFirst(negateLiteral(headLiteral), bodyRepresentingLiteral));
 
@@ -135,6 +138,16 @@ List<NoGood> generateNoGoodsFromGroundSubstitution(final InternalRule nonGroundR
 			result.addAll(choiceRecorder.generateChoiceNoGoods(posLiterals, negLiterals, bodyRepresentingLiteral));
 		}
 
+		// If this is a choice rule, add nogood that prevents both positive and negative head to be true at the same time.
+		if (groundHeadAtom.getPredicate() instanceof NegativeChoicePredicate) {
+			// TODO: clean up
+			// TODO: should we find the original atom instead of constructing a new one?
+			final List<Term> terms = groundHeadAtom.getTerms().subList(1, groundHeadAtom.getTerms().size());
+			BasicAtom complement = new BasicAtom(((NegativeChoicePredicate) groundHeadAtom.getPredicate()).getOriginalChoicePredicate(), terms);
+			final int complementId = atomStore.putIfAbsent(complement);
+			result.add(new NoGood(atomToLiteral(complementId), headLiteral));
+		}
+
 		return result;
 	}
 

src/main/java/at/ac/tuwien/kr/alpha/grounder/transformation/ChoiceHeadToNormal.java

@@ -27,6 +27,7 @@
  */
 package at.ac.tuwien.kr.alpha.grounder.transformation;
 
+import at.ac.tuwien.kr.alpha.common.NegativeChoicePredicate;
 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;
@@ -48,7 +49,6 @@
  * Copyright (c) 2017-2020, the Alpha Team.
  */
 public class ChoiceHeadToNormal extends ProgramTransformation<InputProgram, InputProgram> {
-	private final static String PREDICATE_NEGATION_PREFIX = "_n";
 
 	@Override
 	public InputProgram apply(InputProgram inputProgram) {
@@ -91,7 +91,7 @@ public InputProgram apply(InputProgram inputProgram) {
 				// Construct head atom for the choice.
 				Predicate headPredicate = head.getPredicate();
 
-				Predicate negPredicate = Predicate.getInstance(PREDICATE_NEGATION_PREFIX + headPredicate.getName(), headPredicate.getArity() + 1, true);
+				Predicate negPredicate = NegativeChoicePredicate.getInstance(headPredicate);
 				List<Term> headTerms = new ArrayList<>(head.getTerms());
 				headTerms.add(0, ConstantTerm.getInstance("1")); // FIXME: when introducing classical negation, this is 1 for classical positive atoms and 0 for
 																	// classical negative atoms.