Merge pull request #270 from alpha-asp/substitution_lazy_cloning

Substitution lazy cloning

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

@@ -333,7 +333,7 @@ public Map<Integer, NoGood> getNoGoods(Assignment currentAssignment) {
 				for (Instance instance : modifiedWorkingMemory.getRecentlyAddedInstances()) {
 					// Check instance if it matches with the atom.
 
-					final Substitution unifier = Substitution.unify(firstBindingAtom.startingLiteral, instance, new Substitution());
+					final Substitution unifier = Substitution.specializeSubstitution(firstBindingAtom.startingLiteral, instance, Substitution.EMPTY_SUBSTITUTION);
 
 					if (unifier == null) {
 						continue;

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

@@ -35,6 +35,7 @@
 import at.ac.tuwien.kr.alpha.common.terms.VariableTerm;
 import at.ac.tuwien.kr.alpha.grounder.parser.ProgramPartParser;
 
+import java.util.List;
 import java.util.Map;
 import java.util.Objects;
 import java.util.Set;
@@ -45,6 +46,12 @@
 public class Substitution {
 
 	private static final ProgramPartParser PROGRAM_PART_PARSER = new ProgramPartParser();
+	public static final Substitution EMPTY_SUBSTITUTION = new Substitution() {
+		@Override
+		public <T extends Comparable<T>> Term put(VariableTerm variableTerm, Term groundTerm) {
+			throw oops("Should not be called on EMPTY_SUBSTITUTION");
+		}
+	};
 
 	protected TreeMap<VariableTerm, Term> substitution;
 
@@ -63,76 +70,93 @@ public Substitution(Substitution clone) {
 		this(new TreeMap<>(clone.substitution));
 	}
 
-	public static Substitution unify(Literal literal, Instance instance, Substitution substitution) {
-		return unify(literal.getAtom(), instance, substitution);
+	public static Substitution specializeSubstitution(Literal literal, Instance instance, Substitution substitution) {
+		return specializeSubstitution(literal.getAtom(), instance, substitution);
 	}
 
 	/**
-	 * Computes the unifier of the atom and the instance and stores it in the variable substitution.
-	 * 
-	 * @param atom         the body atom to unify
-	 * @param instance     the ground instance
-	 * @param substitution if the atom does not unify, this is left unchanged.
-	 * @return true if the atom and the instance unify. False otherwise
+	 * Helper class to lazily clone the input substitution of Substitution.specializeSubstitution only when needed.
 	 */
-	public static Substitution unify(Atom atom, Instance instance, Substitution substitution) {
-		for (int i = 0; i < instance.terms.size(); i++) {
-			if (instance.terms.get(i) == atom.getTerms().get(i) || substitution.unifyTerms(atom.getTerms().get(i), instance.terms.get(i))) {
-				continue;
-			}
-			return null;
-		}
-		return substitution;
-	}
+	private static class SpecializationHelper {
+		Substitution updatedSubstitution;	// Is null for as long as the given partial substitution is not extended, afterwards holds the updated/extended/specialized substitution.
 
-	/**
-	 * Checks if the left possible non-ground term unifies with the ground term.
-	 * 
-	 * @param termNonGround
-	 * @param termGround
-	 * @return
-	 */
-	public boolean unifyTerms(Term termNonGround, Term termGround) {
-		if (termNonGround == termGround) {
-			// Both terms are either the same constant or the same variable term
-			return true;
-		} else if (termNonGround instanceof ConstantTerm) {
-			// Since right term is ground, both terms differ
-			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;
-			}
-
-			substitution.put(variableTerm, termGround);
-			return true;
-		} else if (termNonGround instanceof FunctionTerm && termGround instanceof FunctionTerm) {
-			// Both terms are function terms
-			FunctionTerm ftNonGround = (FunctionTerm) termNonGround;
-			FunctionTerm ftGround = (FunctionTerm) termGround;
-
-			if (!(ftNonGround.getSymbol().equals(ftGround.getSymbol()))) {
-				return false;
+		Substitution unify(List<Term> termList, Instance instance, Substitution partialSubstitution) {
+			for (int i = 0; i < termList.size(); i++) {
+				if (!unifyTerms(termList.get(i), instance.terms.get(i), partialSubstitution)) {
+					return null;
+				}
 			}
-			if (ftNonGround.getTerms().size() != ftGround.getTerms().size()) {
-				return false;
+			if (updatedSubstitution == null) {
+				// All terms unify but there was no need to assign a new variable, return the input substitution.
+				return partialSubstitution;
 			}
+			return updatedSubstitution;
+		}
 
-			// 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))) {
+		boolean unifyTerms(Term termNonGround, Term termGround, Substitution partialSubstitution) {
+			if (termNonGround == termGround) {
+				// Both terms are either the same constant or the same variable term
+				return true;
+			} else if (termNonGround instanceof ConstantTerm) {
+				// Since right term is ground, both terms differ
+				return false;
+			} else if (termNonGround instanceof VariableTerm) {
+				VariableTerm variableTerm = (VariableTerm) termNonGround;
+				// Left term is variable, bind it to the right term. Use original substitution if it has
+				// not been cloned yet.
+				Term bound = (updatedSubstitution == null ? partialSubstitution : updatedSubstitution).eval(variableTerm); // Get variable binding, either from input substitution if it has not been updated yet, or from the cloned/updated substitution.
+				if (bound != null) {
+					// Variable is already bound, return true if binding is the same as the current ground term.
+					return termGround == bound;
+				}
+				// Record new variable binding.
+				if (updatedSubstitution == null) {
+					// Clone substitution if it was not yet updated.
+					updatedSubstitution = new Substitution(partialSubstitution);
+				}
+				updatedSubstitution.put(variableTerm, termGround);
+				return true;
+			} else if (termNonGround instanceof FunctionTerm && termGround instanceof FunctionTerm) {
+				// Both terms are function terms
+				FunctionTerm ftNonGround = (FunctionTerm) termNonGround;
+				FunctionTerm ftGround = (FunctionTerm) termGround;
+
+				if (!(ftNonGround.getSymbol().equals(ftGround.getSymbol()))) {
+					return false;
+				}
+				if (ftNonGround.getTerms().size() != ftGround.getTerms().size()) {
 					return false;
 				}
-			}
 
-			return true;
+				// 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), partialSubstitution)) {
+						return false;
+					}
+				}
+
+				return true;
+			}
+			return false;
 		}
-		return false;
+	}
+
+	/**
+	 * Specializes a given substitution such that applying the specialized substitution on the given atom yields the
+	 * given instance (if such a specialized substitution exists). Computes the unifier of the (nonground) atom and
+	 * the given ground instance such that the unifier is an extension of the given partial substitution. If
+	 * specialization succeeds the unifying substitution is returned, if no such unifier exists null is returned. In
+	 * any case the partial substitution is left unchanged.
+	 *
+	 * @param atom         the (potentially nonground) atom to unify.
+	 * @param instance     the ground instance to unify the atom with.
+	 * @param substitution the (partial) substitution for the atom. This is left unchanged in all cases.
+	 * @return null if the unification/specialization fails, otherwise it is a unifying substitution. If the
+	 * 	parameter substitution already is a unifier, it is returned. If the unifying substitution is an
+	 * 	extension of the input substitution, a new substitution will be returned.
+	 */
+	public static Substitution specializeSubstitution(Atom atom, Instance instance, Substitution substitution) {
+		return new SpecializationHelper().unify(atom.getTerms(), instance, substitution);
 	}
 
 	/**
@@ -192,10 +216,10 @@ public String toString() {
 
 	public static Substitution fromString(String substitution) {
 		String bare = substitution.substring(1, substitution.length() - 1);
-		String assignments[] = bare.split(",");
+		String[] assignments = bare.split(",");
 		Substitution ret = new Substitution();
 		for (String assignment : assignments) {
-			String keyVal[] = assignment.split("->");
+			String[] keyVal = assignment.split("->");
 			VariableTerm variable = VariableTerm.getInstance(keyVal[0]);
 			Term assignedTerm = PROGRAM_PART_PARSER.parseTerm(keyVal[1]);
 			ret.put(variable, assignedTerm);

src/main/java/at/ac/tuwien/kr/alpha/grounder/instantiation/AbstractLiteralInstantiationStrategy.java

@@ -105,7 +105,7 @@ protected final List<ImmutablePair<Substitution, AssignmentStatus>> buildSubstit
 		Substitution currentInstanceSubstitution;
 		Atom atomForCurrentInstance;
 		for (Instance instance : candidateInstances) {
-			currentInstanceSubstitution = Substitution.unify(atomToSubstitute, instance, new Substitution(partialSubstitution));
+			currentInstanceSubstitution = Substitution.specializeSubstitution(atomToSubstitute, instance, partialSubstitution);
 			if (currentInstanceSubstitution == null) {
 				// Instance does not unify with partialSubstitution, move on to the next instance.
 				continue;

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

@@ -1,21 +1,5 @@
 package at.ac.tuwien.kr.alpha.grounder.transformation;
 
-import org.apache.commons.collections4.SetUtils;
-import org.apache.commons.lang3.tuple.ImmutablePair;
-import org.slf4j.Logger;
-import org.slf4j.LoggerFactory;
-
-import java.util.ArrayList;
-import java.util.Collections;
-import java.util.HashMap;
-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.Stack;
-
 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;
@@ -37,6 +21,21 @@
 import at.ac.tuwien.kr.alpha.grounder.instantiation.LiteralInstantiationResult;
 import at.ac.tuwien.kr.alpha.grounder.instantiation.LiteralInstantiator;
 import at.ac.tuwien.kr.alpha.grounder.instantiation.WorkingMemoryBasedInstantiationStrategy;
+import org.apache.commons.collections4.SetUtils;
+import org.apache.commons.lang3.tuple.ImmutablePair;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.HashMap;
+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.Stack;
 
 /**
  * Evaluates the stratifiable part of a given (analyzed) ASP program.
@@ -237,7 +236,7 @@ private List<Substitution> substituteFromRecentlyAddedInstances(Literal lit) {
 			return Collections.emptyList();
 		}
 		for (Instance instance : instances) {
-			Substitution unifyingSubstitution = Substitution.unify(lit, instance, new Substitution());
+			Substitution unifyingSubstitution = Substitution.specializeSubstitution(lit, instance, Substitution.EMPTY_SUBSTITUTION);
 			if (unifyingSubstitution != null) {
 				retVal.add(unifyingSubstitution);
 			}

src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java

@@ -25,22 +25,6 @@
  */
 package at.ac.tuwien.kr.alpha.grounder;
 
-import static at.ac.tuwien.kr.alpha.TestUtil.atom;
-import static at.ac.tuwien.kr.alpha.solver.ThriceTruth.TRUE;
-import static org.junit.Assert.assertEquals;
-import static org.junit.Assert.assertTrue;
-import static org.junit.Assert.fail;
-
-import org.junit.Before;
-import org.junit.Ignore;
-import org.junit.Test;
-
-import java.util.Arrays;
-import java.util.Collection;
-import java.util.Collections;
-import java.util.List;
-import java.util.Map;
-
 import at.ac.tuwien.kr.alpha.api.Alpha;
 import at.ac.tuwien.kr.alpha.common.Assignment;
 import at.ac.tuwien.kr.alpha.common.AtomStore;
@@ -59,6 +43,21 @@
 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;
+import org.junit.Ignore;
+import org.junit.Test;
+
+import java.util.Arrays;
+import java.util.Collection;
+import java.util.Collections;
+import java.util.List;
+import java.util.Map;
+
+import static at.ac.tuwien.kr.alpha.TestUtil.atom;
+import static at.ac.tuwien.kr.alpha.solver.ThriceTruth.TRUE;
+import static org.junit.Assert.assertEquals;
+import static org.junit.Assert.assertTrue;
+import static org.junit.Assert.fail;
 
 /**
  * Tests {@link NaiveGrounder}
@@ -182,7 +181,7 @@ public void noDeadEndWithPermissiveGrounderHeuristicForQ1() {
 	}
 
 	/**
-	 * Tests the method {@link NaiveGrounder#getGroundInstantiations(NonGroundRule, RuleGroundingOrder, Substitution, Assignment)} on a predefined program:
+	 * Tests the method {@link NaiveGrounder#getGroundInstantiations(InternalRule, RuleGroundingOrder, Substitution, Assignment)} on a predefined program:
 	 * <code>
 	 *  p1(1). q1(1). <br/>
 	 * 	x :- p1(X), p2(X), q1(Y), q2(Y). <br/>
@@ -223,7 +222,7 @@ private void testDeadEnd(String predicateNameOfStartingLiteral, RuleGroundingOrd
 
 		grounder.bootstrap();
 		TrailAssignment currentAssignment = new TrailAssignment(atomStore);
-		final Substitution subst1 = Substitution.unify(startingLiteral, new Instance(ConstantTerm.getInstance(1)), new Substitution());
+		final Substitution subst1 = Substitution.specializeSubstitution(startingLiteral, new Instance(ConstantTerm.getInstance(1)), Substitution.EMPTY_SUBSTITUTION);
 		final BindingResult bindingResult = grounder.getGroundInstantiations(nonGroundRule, groundingOrder, subst1, currentAssignment);
 
 		assertEquals(expectNoGoods, bindingResult.size() > 0);
@@ -264,7 +263,7 @@ public void testGroundingOfRuleNotSwitchedOffByFalseNegativeBody() {
 	}
 
 	/**
-	 * Tests if {@link NaiveGrounder#getGroundInstantiations(NonGroundRule, RuleGroundingOrder, Substitution, Assignment)}
+	 * Tests if {@link NaiveGrounder#getGroundInstantiations(InternalRule, RuleGroundingOrder, Substitution, Assignment)}
 	 * produces ground instantiations for the rule with ID {@code ruleID} in {@code program} when {@code startingLiteral}
 	 * unified with the numeric instance {@code startingInstance} is used as starting literal and {@code b(1)} is assigned
 	 * {@code bTruth}.
@@ -284,7 +283,7 @@ private void testIfGrounderGroundsRule(InputProgram program, int ruleID, Literal
 
 		grounder.bootstrap();
 		final InternalRule nonGroundRule = grounder.getNonGroundRule(ruleID);
-		final Substitution substStartingLiteral = Substitution.unify(startingLiteral, new Instance(ConstantTerm.getInstance(startingInstance)), new Substitution());
+		final Substitution substStartingLiteral = Substitution.specializeSubstitution(startingLiteral, new Instance(ConstantTerm.getInstance(startingInstance)), Substitution.EMPTY_SUBSTITUTION);
 		final BindingResult bindingResult = grounder.getGroundInstantiations(nonGroundRule, nonGroundRule.getGroundingOrders().groundingOrders.get(startingLiteral), substStartingLiteral, currentAssignment);
 		assertEquals(expectNoGoods, bindingResult.size() > 0);
 	}
@@ -358,7 +357,7 @@ private void testPermissiveGrounderHeuristicTolerance(InputProgram program, int
 	}
 
 	/**
-	 * Tests if {@link NaiveGrounder#getGroundInstantiations(NonGroundRule, RuleGroundingOrder, Substitution, Assignment)}
+	 * Tests if {@link NaiveGrounder#getGroundInstantiations(InternalRule, RuleGroundingOrder, Substitution, Assignment)}
 	 * produces ground instantiations for the rule with ID {@code ruleID} in {@code program} when {@code startingLiteral}
 	 * unified with the numeric instance {@code startingInstance} is used as starting literal and the following
 	 * additional conditions are established:
@@ -397,7 +396,7 @@ private void testPermissiveGrounderHeuristicTolerance(InputProgram program, int
 
 		grounder.bootstrap();
 		final InternalRule nonGroundRule = grounder.getNonGroundRule(ruleID);
-		final Substitution substStartingLiteral = Substitution.unify(startingLiteral, new Instance(ConstantTerm.getInstance(startingInstance)), new Substitution());
+		final Substitution substStartingLiteral = Substitution.specializeSubstitution(startingLiteral, new Instance(ConstantTerm.getInstance(startingInstance)), Substitution.EMPTY_SUBSTITUTION);
 		final BindingResult bindingResult = grounder.getGroundInstantiations(nonGroundRule, nonGroundRule.getGroundingOrders().groundingOrders.get(startingLiteral), substStartingLiteral, currentAssignment);
 		assertEquals(expectNoGoods, bindingResult.size() > 0);
 		if (bindingResult.size() > 0) {

src/test/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGeneratorTest.java

@@ -56,7 +56,7 @@ public class NoGoodGeneratorTest {
 	private static final VariableTerm Y = VariableTerm.getInstance("Y");
 
 	/**
-	 * Calls {@link NoGoodGenerator#collectNegLiterals(NonGroundRule, Substitution)}, which puts the atom occurring
+	 * Calls {@link NoGoodGenerator#collectNegLiterals(InternalRule, Substitution)}, which puts the atom occurring
 	 * negatively in a rule into the atom store. It is then checked whether the atom in the atom store is positive.
 	 */
 	@Test
@@ -73,8 +73,8 @@ public void collectNeg_ContainsOnlyPositiveLiterals() {
 		Grounder grounder = GrounderFactory.getInstance("naive", program, atomStore, true);
 		NoGoodGenerator noGoodGenerator = ((NaiveGrounder) grounder).noGoodGenerator;
 		Substitution substitution = new Substitution();
-		substitution.unifyTerms(X, A);
-		substitution.unifyTerms(Y, B);
+		substitution.put(X, A);
+		substitution.put(Y, B);
 		List<Integer> collectedNeg = noGoodGenerator.collectNegLiterals(rule, substitution);
 		assertEquals(1, collectedNeg.size());
 		String negAtomString = atomStore.atomToString(atomOf(collectedNeg.get(0)));