Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Substitution lazy cloning #270

Merged
merged 4 commits into from
Oct 7, 2020
Merged

Substitution lazy cloning #270

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
690d1f8
Clone Substitutions only if necessary.
AntoniusW Oct 1, 2020
ecffafe
Clone Substitutions only if necessary also for StratifiedEvaluation.
AntoniusW Oct 1, 2020
0308839
Better name Substitution specialization/unify.
AntoniusW Oct 4, 2020
af66c5a
Improve comments.
AntoniusW Oct 6, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
144 changes: 84 additions & 60 deletions src/main/java/at/ac/tuwien/kr/alpha/grounder/Substitution.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;

Expand All @@ -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) {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note that this is a matter of personal taste, but I'm not sure I agree with the return types here..
I think it might make sense if unifyTerms returned something other than boolean, thereby getting rid of the side-effects of potentially modifying the given partialSubstitution. Instead, unifyTerms could return a Substitution that may be either a new (cloned) one, or the one passed in in case nothing changed. Alternatively, we could also use an Optional<Substitution> here, where the presence of a value would indicate that a new variable got bound. The version with Optional could also be used for Substitution::unify as an alternative to returning null.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Letting unifyTerms return a Substitution is a good idea. I would not want to return an Optional however, since substitutions are used at the core of grounding and Optional is likely slower and creates more objects.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually, I decided to remove unifyTerms as it was only ever used in unit tests. These unit tests have been adapted to now test the new/renamed specializeSubstitution.

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) {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems wrong (or at least really confusing) to me that we now have UnificationHelper::unifyTerms(Term, Term, Substitution) as well as Substitution::unifyTerms(Term, Term). The only difference seems to be that the one in Substitution always operates on this and modifying the substitution it's called on, while the other one operates on the given partialSubstitution. I think the version in UnificationHelper should be adapted so that the other one isn't needed.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Agreed, the Substitution::unifyTerms(Term, Term) is only ever needed in unit tests, while the new one is not tested. Will adapt the tests to run on the real thing and get rid of the other.

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);
}

/**
Expand Down Expand Up @@ -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);
Expand Down
2 changes: 1 addition & 1 deletion ...va/at/ac/tuwien/kr/alpha/grounder/instantiation/AbstractLiteralInstantiationStrategy.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
33 changes: 16 additions & 17 deletions src/main/java/at/ac/tuwien/kr/alpha/grounder/transformation/StratifiedEvaluation.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
Expand All @@ -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.
Expand Down Expand Up @@ -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);
}
Expand Down
43 changes: 21 additions & 22 deletions src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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}
Expand Down Expand Up @@ -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/>
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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}.
Expand All @@ -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);
}
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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) {
Expand Down
6 changes: 3 additions & 3 deletions src/test/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGeneratorTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)));
Expand Down
Loading