Skip to content

Commit

Permalink
Improved caching of operations
Browse files Browse the repository at this point in the history
  • Loading branch information
@Brandon-Rozek
Brandon-Rozek committed Oct 31, 2023
1 parent 61ae5a5 commit 0e3895d
Showing 1 changed file with 70 additions and 102 deletions.
172 changes: 70 additions & 102 deletions src/main/java/com/naveensundarg/planner/Operations.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,11 @@
import org.rairlab.shadow.prover.core.Prover;
import org.rairlab.shadow.prover.core.SnarkWrapper;
import org.rairlab.shadow.prover.core.proof.Justification;
import org.rairlab.planner.utils.Commons;
import org.rairlab.shadow.prover.representations.formula.BiConditional;
import org.rairlab.shadow.prover.representations.formula.Formula;
import org.rairlab.shadow.prover.representations.formula.Predicate;

import org.rairlab.shadow.prover.representations.value.Value;
import org.rairlab.shadow.prover.representations.value.Variable;
import org.rairlab.shadow.prover.utils.CollectionUtils;
Expand Down Expand Up @@ -52,115 +54,92 @@ public static void reset(){

public static synchronized Optional<Justification> proveCached(Set<Formula> assumptions, Formula goal) {

// (1) If we've asked to prove this exact goal from assumptions before
// then return the previous result
Pair<Set<Formula>, Formula> inputPair = ImmutablePair.of(assumptions, goal);

if (proverCache.containsKey(inputPair)) {

return proverCache.get(inputPair);

}

Optional<Map.Entry<Pair<Set<Formula>, Formula>, Optional<Justification>>> cachedOptionalSuccessful = proverCache.entrySet().stream().filter(pairOptionalEntry -> {

Set<Formula> cachedAssumptions = pairOptionalEntry.getKey().getLeft();
Formula cachedGoal = pairOptionalEntry.getKey().getRight();

return cachedGoal.equals(goal) && Sets.subset(cachedAssumptions, assumptions);
}).findAny();


if(cachedOptionalSuccessful.isPresent() && cachedOptionalSuccessful.get().getValue().isPresent()){

return cachedOptionalSuccessful.get().getValue();
}


Optional<Map.Entry<Pair<Set<Formula>, Formula>, Optional<Justification>>> cachedOptionalFailed = proverCache.entrySet().stream().filter(pairOptionalEntry -> {

Set<Formula> cachedAssumptions = pairOptionalEntry.getKey().getLeft();
Formula cachedGoal = pairOptionalEntry.getKey().getRight();

return cachedGoal.equals(goal) && Sets.subset(assumptions, cachedAssumptions);
}).findAny();


if(cachedOptionalFailed.isPresent() && !cachedOptionalFailed.get().getValue().isPresent()){

return cachedOptionalFailed.get().getValue();
}

if(goal instanceof Predicate && ((Predicate) goal).getName().equals("sameroom")){

Predicate p = (Predicate) goal;

Value v1 = p.getArguments()[0];
Value v2 = p.getArguments()[1];

Optional<Formula> inOptv1 = assumptions.stream().filter(x-> x instanceof Predicate &&
((Predicate)x).getName().equals("in") && ((Predicate) x).getArguments()[0].equals(v1)).findAny();

Optional<Formula> inOptv2 = assumptions.stream().filter(x-> x instanceof Predicate &&
((Predicate)x).getName().equals("in") && ((Predicate) x).getArguments()[0].equals(v2)).findAny();


if(inOptv1.isPresent() && inOptv2.isPresent()){

Value room1 = ((Predicate)inOptv1.get()).getArguments()[1];
Value room2 = ((Predicate)inOptv2.get()).getArguments()[1];

if(room1.equals(room2)){

return Optional.of(Justification.trivial(assumptions, goal));
}

}

// Iterate through the cache
for (Map.Entry<Pair<Set<Formula>, Formula>, Optional<Justification>> entry : proverCache.entrySet()) {
Set<Formula> cachedAssumptions = entry.getKey().getLeft();
Formula cachedGoal = entry.getKey().getRight();
Optional<Justification> optJust = entry.getValue();

// (2) Return the cached justification if:
// - Goals are the same
// - The cached assumptions are a subset of the current ones
// - A justification was found
if (optJust.isPresent() && cachedGoal.equals(goal) && Sets.subset(cachedAssumptions, assumptions)) {
return optJust;
}

// (3) Return cached failure if:
// - Goals are the same
// - Assumptions are a subset of cached assumptions
// - No justification was found
if (optJust.isEmpty() && cachedGoal.equals(goal) && Sets.subset(assumptions, cachedAssumptions)) {
return optJust;
}
}

{

Optional<Justification> answer = prover.prove(assumptions, goal);

proverCache.put(inputPair, answer);

return answer;
}
// Otherwise create a new call to the theorem prover
Optional<Justification> answer = prover.prove(assumptions, goal);
proverCache.put(inputPair, answer);
return answer;

}

public static synchronized Optional<Set<Map<Variable, Value>>> proveAndGetBindingsCached(Set<Formula> givens, Formula goal, List<Variable> variables) {


Triple<Set<Formula>, Formula, List<Variable>> inputTriple = Triple.of(givens, goal, variables);
public static synchronized Optional<Set<Map<Variable, Value>>> proveAndGetBindingsCached(Set<Formula> assumptions, Formula goal, List<Variable> variables) {

// (1) If we've asked to find the variables that satisfy this exact goal from assumptions before
// then return the previous result
Triple<Set<Formula>, Formula, List<Variable>> inputTriple = Triple.of(assumptions, goal, variables);
if (proverBindingsCache.containsKey(inputTriple)) {

return proverBindingsCache.get(inputTriple);
}

} else {

Optional<Set<Map<Variable, Value>>> answer = proveAndGetMultipleBindings(givens, goal, variables);

proverBindingsCache.put(inputTriple, answer);
for (Map.Entry<Triple<Set<Formula>, Formula, List<Variable>>, Optional<Set<Map<Variable, Value>>>> entry : proverBindingsCache.entrySet()) {
Set<Formula> cachedAssumptions = entry.getKey().getLeft();
Formula cachedGoal = entry.getKey().getMiddle();
List<Variable> cachedVars = entry.getKey().getRight();
Optional<Set<Map<Variable, Value>>> optMapping = entry.getValue();

// (2) Return the cached justification if:
// - Goals are the same
// - The variable list requested is the same
// - The cached assumptions are a subset of the current ones
// - A justification was found
if (optMapping.isPresent() && cachedGoal.equals(goal) && cachedVars.equals(variables) && Sets.subset(cachedAssumptions, assumptions)) {
return optMapping;
}

return answer;
// (3) Return cached failure if:
// - Goals are the same
// - The variable list requested is the same
// - Assumptions are a subset of cached assumptions
// - No justification was found
if (optMapping.isEmpty() && cachedGoal.equals(goal) && cachedVars.equals(variables) && Sets.subset(assumptions, cachedAssumptions)) {
return optMapping;
}
}

// Otherwise create a new call to the theorem prover
Optional<Set<Map<Variable, Value>>> answer = proveAndGetMultipleBindings(assumptions, goal, variables);
proverBindingsCache.put(inputTriple, answer);
return answer;
}

public static synchronized Optional<Map<Variable, Value>> proveAndGetBindings(Set<Formula> givens, Formula goal, List<Variable> variables) {

Future<Optional<Map<Variable, Value>>> future = new FutureTask<>(() -> {
return prover.proveAndGetBindings(givens, goal, variables);


});

Optional<Map<Variable, Value>> answer;

try {

answer = future.get(1, TimeUnit.SECONDS);
} catch (InterruptedException | ExecutionException | TimeoutException e) {
answer = Optional.empty();
Expand All @@ -174,26 +153,11 @@ public static synchronized Optional<Set<Map<Variable, Value>>> proveAndGetMultip

Optional<org.apache.commons.lang3.tuple.Pair<Justification, Set<Map<Variable, Value>>>> ans = prover.proveAndGetMultipleBindings(givens, goal, variables);

if(ans.isPresent()){

return Optional.of(ans.get().getRight());

}else {
if (ans.isEmpty()) {
return Optional.empty();
}
/* Future<Optional<Set<Map<Variable, Value>>>> future = new FutureTask<>(()-> prover.proveAndGetMultipleBindings(givens, goal, variables));

Optional<Set<Map<Variable, Value>>> answer;
try{
answer = future.get(50, TimeUnit.SECONDS);
} catch (InterruptedException | ExecutionException | TimeoutException e ) {
answer = Optional.empty();
}
return answer;
*/
return Optional.of(ans.get().getRight());
}


Expand Down Expand Up @@ -301,18 +265,22 @@ public static boolean equivalent(Set<Formula> background, Formula f1, Formula f2
public static boolean satisfies(Set<Formula> background, State state, State goal) {

if ((Sets.union(background, state.getFormulae()).containsAll(goal.getFormulae()))) {

return true;
}
return goal.getFormulae().stream().
allMatch(x -> proveCached(Sets.union(background, state.getFormulae()), x).isPresent());

return proveCached(
Sets.union(background, state.getFormulae()),
Commons.makeAnd(goal.getFormulae())
).isPresent();

}

public static boolean conflicts(Set<Formula> background, State state1, State state2) {


return proveCached(Sets.union(background, Sets.union(state1.getFormulae(), state2.getFormulae())), State.FALSE).isPresent();
return proveCached(
Sets.union(background, Sets.union(state1.getFormulae(), state2.getFormulae())),
State.FALSE
).isPresent();

}

Expand Down

0 comments on commit 0e3895d

Please sign in to comment.