Completion

src/main/java/at/ac/tuwien/kr/alpha/api/Alpha.java

@@ -182,7 +182,7 @@ public Stream<AnswerSet> solve(InternalProgram program) {
 
 	/**
 	 * Solves the given program and filters answer sets based on the passed predicate.
-	 * 
+	 *
 	 * @param program an {@link InternalProgram} to solve
 	 * @param filter       {@link Predicate} filtering {@at.ac.tuwien.kr.alpha.common.Predicate}s in the returned answer sets
 	 * @return a Stream of answer sets representing stable models of the given program
@@ -195,7 +195,7 @@ public Stream<AnswerSet> solve(InternalProgram program, java.util.function.Predi
 	/**
 	 * Prepares a solver (and accompanying grounder) instance pre-loaded with the given program. Use this if the
 	 * solver is needed after reading answer sets (e.g. for obtaining statistics).
-	 * 
+	 *
 	 * @param program the program to solve.
 	 * @param filter  a (java util) predicate that filters (asp-)predicates which should be contained in the answer
 	 *                set stream from the solver.
@@ -210,7 +210,7 @@ public Solver prepareSolverFor(InternalProgram program, java.util.function.Predi
 		grounderHeuristicConfiguration.setAccumulatorEnabled(config.isGrounderAccumulatorEnabled());
 
 		AtomStore atomStore = new AtomStoreImpl();
-		Grounder grounder = GrounderFactory.getInstance(grounderName, program, atomStore, filter, grounderHeuristicConfiguration, doDebugChecks);
+		Grounder grounder = GrounderFactory.getInstance(grounderName, program, atomStore, filter, grounderHeuristicConfiguration, this.config.getCompletionConfiguration(), doDebugChecks);
 
 		return SolverFactory.getInstance(config, atomStore, grounder);
 	}

src/main/java/at/ac/tuwien/kr/alpha/api/mapper/AnswerSetToWorkbookMapper.java

@@ -25,8 +25,10 @@
  */
 package at.ac.tuwien.kr.alpha.api.mapper;
 
-import java.util.List;
-
+import at.ac.tuwien.kr.alpha.common.AnswerSet;
+import at.ac.tuwien.kr.alpha.common.Predicate;
+import at.ac.tuwien.kr.alpha.common.atoms.Atom;
+import at.ac.tuwien.kr.alpha.common.terms.Term;
 import org.apache.poi.ss.usermodel.Cell;
 import org.apache.poi.ss.usermodel.CellStyle;
 import org.apache.poi.ss.usermodel.FillPatternType;
@@ -39,10 +41,7 @@
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
-import at.ac.tuwien.kr.alpha.common.AnswerSet;
-import at.ac.tuwien.kr.alpha.common.Predicate;
-import at.ac.tuwien.kr.alpha.common.atoms.Atom;
-import at.ac.tuwien.kr.alpha.common.terms.Term;
+import java.util.List;
 
 /**
  * Implementation of {@link AnswerSetToObjectMapper} that generates an office open xml workbook ("excel file") from a given answer set.

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

@@ -172,9 +172,10 @@ default boolean violates(NoGood noGood) {
 
 	/**
 	 * Obtain a BasicAtom that is currently assigned MBT (but not TRUE).
-	 * @return some BasicAtom that is assigned MBT.
+	 * @param excludedAtoms a set of atoms not to return.
+	 * @return some BasicAtom that is assigned MBT or -1 if none such exists.
 	 */
-	int getBasicAtomAssignedMBT();
+	int getBasicAtomAssignedMBT(Set<Integer> excludedAtoms);
 
 	/**
 	 * Assigns all unassigned atoms to FALSE.

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

@@ -106,6 +106,15 @@ public static NoGood support(int headLiteral, int bodyRepresentingLiteral) {
 		return new NoGood(SUPPORT, headLiteral, negateLiteral(bodyRepresentingLiteral));
 	}
 
+	public static NoGood support(int headLiteral, int... bodyRepresentingLiterals) {
+		int[] literals = new int[bodyRepresentingLiterals.length + 1];
+		literals[0] = headLiteral;
+		for (int i = 0; i < bodyRepresentingLiterals.length; i++) {
+			literals[i + 1] = negateLiteral(bodyRepresentingLiterals[i]);
+		}
+		return new NoGood(SUPPORT, literals);
+	}
+
 	public static NoGood fromConstraint(List<Integer> posLiterals, List<Integer> negLiterals) {
 		return new NoGood(addPosNeg(new int[posLiterals.size() + negLiterals.size()], posLiterals, negLiterals, 0));
 	}

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.fixedinterpretations.PredicateInterpretation;
+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;
 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 extends Atom implements VariableNormalizableAtom {
 

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

@@ -27,17 +27,17 @@
  */
 package at.ac.tuwien.kr.alpha.common.atoms;
 
+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.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;
-
 /**
  * Contains a potentially negated {@link ExternalAtom}.
  */

src/main/java/at/ac/tuwien/kr/alpha/common/program/InternalProgram.java

@@ -6,14 +6,18 @@
 import at.ac.tuwien.kr.alpha.common.rule.NormalRule;
 import at.ac.tuwien.kr.alpha.grounder.FactIntervalEvaluator;
 import at.ac.tuwien.kr.alpha.grounder.Instance;
+import at.ac.tuwien.kr.alpha.grounder.Substitution;
 import org.apache.commons.lang3.tuple.ImmutablePair;
 
 import java.util.ArrayList;
 import java.util.Collections;
+import java.util.HashSet;
 import java.util.LinkedHashMap;
 import java.util.LinkedHashSet;
 import java.util.List;
 import java.util.Map;
+import java.util.Set;
+import java.util.TreeMap;
 
 /**
  * A program in the internal representation needed for grounder and solver, i.e.: rules must have normal heads, all
@@ -27,6 +31,8 @@ public class InternalProgram extends AbstractProgram<InternalRule> {
 	private final Map<Predicate, LinkedHashSet<InternalRule>> predicateDefiningRules = new LinkedHashMap<>();
 	private final Map<Predicate, LinkedHashSet<Instance>> factsByPredicate = new LinkedHashMap<>();
 	private final Map<Integer, InternalRule> rulesById = new LinkedHashMap<>();
+	private TreeMap<Atom, Set<InternalRule>> rulesUnifyingWithHead = new TreeMap<>();
+	private Set<InternalRule> isFullyNonProjective = new HashSet<>();
 
 	public InternalProgram(List<InternalRule> rules, List<Atom> facts) {
 		super(rules, facts, null);
@@ -90,4 +96,61 @@ public Map<Integer, InternalRule> getRulesById() {
 		return Collections.unmodifiableMap(rulesById);
 	}
 
+	/**
+	 * Runs program analysis after all defining rules have been recorded.
+	 */
+	public void runProgramAnalysis() {
+		computeRulesDerivingSameHeadBasedOnPredicate();
+	}
+
+	private void computeRulesDerivingSameHeadBasedOnPredicate() {
+		// Iterate all rules having the same predicate in the head.
+		boolean isCompletable;
+		for (Map.Entry<Predicate, LinkedHashSet<InternalRule>> definingRules : predicateDefiningRules.entrySet()) {
+			isCompletable = true;
+			LinkedHashSet<InternalRule> rules = definingRules.getValue();
+			for (InternalRule rule : rules) {
+				if (!rule.isNonProjective() && !rule.isFunctionallyDependent()) {
+					isCompletable = false;
+				}
+			}
+			if (isCompletable) {
+				this.isFullyNonProjective.addAll(rules);
+			}
+		}
+	}
+
+	public boolean isRuleFullyNonProjective(InternalRule nonGroundRule) {
+		return isFullyNonProjective.contains(nonGroundRule);
+	}
+
+	public Set<InternalRule> getRulesUnifyingWithGroundHead(Atom groundHeadAtom) {
+		// Check if we already computed all rules unifying with the given head atom.
+		Set<InternalRule> ret = rulesUnifyingWithHead.get(groundHeadAtom);
+		if (ret != null) {
+			return ret;
+		}
+		// Construct rules unifying with the given head.
+		return computeRulesHeadUnifyingWithGroundAtom(groundHeadAtom);
+	}
+
+	private Set<InternalRule> computeRulesHeadUnifyingWithGroundAtom(Atom groundAtom) {
+		HashSet<InternalRule> nonGroundRules = getPredicateDefiningRules().get(groundAtom.getPredicate());
+		if (nonGroundRules.isEmpty()) {
+			return Collections.emptySet();
+		}
+		Set<InternalRule> ret = new LinkedHashSet<>();
+		for (InternalRule nonGroundRule : nonGroundRules) {
+			if (Substitution.specializeSubstitution(nonGroundRule.getHeadAtom(), new Instance(groundAtom.getTerms()), new Substitution()) != null) {
+				// Rule head does unify with current atom.
+				ret.add(nonGroundRule);
+			}
+		}
+		if (nonGroundRules.size() != 1) {
+			// Only store the head-rules association if it likely will be used again.
+			rulesUnifyingWithHead.put(groundAtom, ret);
+		}
+		return ret;
+	}
+
 }

src/main/java/at/ac/tuwien/kr/alpha/common/rule/InternalRule.java

@@ -27,11 +27,6 @@
  */
 package at.ac.tuwien.kr.alpha.common.rule;
 
-import com.google.common.annotations.VisibleForTesting;
-
-import java.util.ArrayList;
-import java.util.List;
-
 import at.ac.tuwien.kr.alpha.common.Predicate;
 import at.ac.tuwien.kr.alpha.common.atoms.AggregateLiteral;
 import at.ac.tuwien.kr.alpha.common.atoms.Atom;
@@ -41,6 +36,14 @@
 import at.ac.tuwien.kr.alpha.grounder.IntIdGenerator;
 import at.ac.tuwien.kr.alpha.grounder.RuleGroundingOrders;
 import at.ac.tuwien.kr.alpha.grounder.Unifier;
+import at.ac.tuwien.kr.alpha.grounder.structure.DirectFunctionalDependency;
+import com.google.common.annotations.VisibleForTesting;
+
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.List;
+
+import static at.ac.tuwien.kr.alpha.grounder.structure.DirectFunctionalDependency.computeDirectFunctionalDependencies;
 
 /**
  * Represents a normal rule or a constraint for the semi-naive grounder.
@@ -55,6 +58,8 @@ public class InternalRule extends NormalRule {
 	private final List<Predicate> occurringPredicates;
 
 	private final RuleGroundingOrders groundingOrders;
+	private final boolean isNonProjective;
+	private final DirectFunctionalDependency functionalDependency;
 
 	public InternalRule(NormalHead head, List<Literal> body) {
 		super(head, body);
@@ -76,6 +81,9 @@ public InternalRule(NormalHead head, List<Literal> body) {
 			this.occurringPredicates.add(literal.getPredicate());
 		}
 
+		this.isNonProjective = getHeadAtom() != null && checkIsNonProjective();
+		this.functionalDependency = getHeadAtom() == null ? null : computeDirectFunctionalDependencies(this);
+
 		// not needed, done in AbstractRule! Leaving it commented out for future reference since this might actually be the
 		// proper place to put it
 		// this.checkSafety();
@@ -84,6 +92,19 @@ public InternalRule(NormalHead head, List<Literal> body) {
 		this.groundingOrders.computeGroundingOrders();
 	}
 
+	private boolean checkIsNonProjective() {
+		// Collect head and body variables.
+		HashSet<VariableTerm> occurringVariablesHead = new HashSet<>(getHeadAtom().getOccurringVariables());
+		HashSet<VariableTerm> occurringVariablesBody = new HashSet<>();
+		for (Literal literal : getBody()) {
+			occurringVariablesBody.addAll(literal.getBindingVariables());
+		}
+		// Check that all variables of the body also occur in the head (otherwise grounding is not unique).
+		occurringVariablesBody.removeAll(occurringVariablesHead);
+		// Check if ever body variables occurs in the head.
+		return occurringVariablesBody.isEmpty();
+	}
+
 	@VisibleForTesting
 	public static void resetIdGenerator() {
 		InternalRule.ID_GENERATOR.resetGenerator();
@@ -136,4 +157,16 @@ public int getRuleId() {
 		return this.ruleId;
 	}
 
+	public boolean isNonProjective() {
+		return isNonProjective;
+	}
+
+	public boolean isFunctionallyDependent() {
+		return functionalDependency != null;
+	}
+
+	public DirectFunctionalDependency getFunctionalDependency() {
+		return functionalDependency;
+	}
+
 }

src/main/java/at/ac/tuwien/kr/alpha/common/terms/ArithmeticTerm.java

@@ -66,6 +66,18 @@ public boolean isGround() {
 		return left.isGround() && right.isGround();
 	}
 
+	public Term getLeft() {
+		return left;
+	}
+
+	public Term getRight() {
+		return right;
+	}
+
+	public ArithmeticOperator getArithmeticOperator() {
+		return arithmeticOperator;
+	}
+
 	@Override
 	public List<VariableTerm> getOccurringVariables() {
 		LinkedHashSet<VariableTerm> occurringVariables = new LinkedHashSet<>(left.getOccurringVariables());
@@ -192,6 +204,20 @@ public Integer eval(Integer left, Integer right) {
 
 			}
 		}
+
+		public ArithmeticOperator inverseOperator() {
+			switch (this) {
+				case PLUS:
+					return MINUS;
+				case MINUS:
+					return PLUS;
+				case TIMES:
+					return DIV;
+				case DIV:
+					return TIMES;
+			}
+			return null;
+		}
 	}
 
 	public static class MinusTerm extends ArithmeticTerm {