From 59b6845107c08b8857f88c070ff477b3069a87c8 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 29 Mar 2024 17:30:45 -0400 Subject: [PATCH] Removed dead code --- .../java/org/rairlab/planner/Operations.java | 176 ++++-------------- .../rairlab/planner/search/AStarPlanner.java | 13 +- 2 files changed, 38 insertions(+), 151 deletions(-) diff --git a/src/main/java/org/rairlab/planner/Operations.java b/src/main/java/org/rairlab/planner/Operations.java index 2435404..183a7f3 100644 --- a/src/main/java/org/rairlab/planner/Operations.java +++ b/src/main/java/org/rairlab/planner/Operations.java @@ -33,6 +33,7 @@ public class Operations { private static boolean DEEP_EQUIVALENCE = false; private static boolean THROW_AWAY_EMPTY_BINDINGS = true; + private static boolean MONOTONIC = true; private static Prover prover; @@ -52,40 +53,44 @@ public class Operations { } public static synchronized Optional proveCached(Set assumptions, Formula goal) { - - // (1) If we've asked to prove this exact goal from assumptions before - // then return the previous result Pair, Formula> inputPair = ImmutablePair.of(assumptions, goal); - if (proverCache.containsKey(inputPair)) { - return proverCache.get(inputPair); - } - // Iterate through the cache - for (Map.Entry, Formula>, Optional> entry : proverCache.entrySet()) { - Set cachedAssumptions = entry.getKey().getLeft(); - Formula cachedGoal = entry.getKey().getRight(); - Optional 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; + if (MONOTONIC) { + // (1) If we've asked to prove this exact goal from assumptions before + // then return the previous result + if (proverCache.containsKey(inputPair)) { + return proverCache.get(inputPair); } - // (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; + // Iterate through the cache + for (Map.Entry, Formula>, Optional> entry : proverCache.entrySet()) { + Set cachedAssumptions = entry.getKey().getLeft(); + Formula cachedGoal = entry.getKey().getRight(); + Optional 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; + } } - } + } // Otherwise create a new call to the theorem prover Optional answer = prover.prove(assumptions, goal); - proverCache.put(inputPair, answer); + if (MONOTONIC) { + proverCache.put(inputPair, answer); + } return answer; } @@ -176,18 +181,7 @@ public class Operations { return -1; } } - - // Take a time value, get the integer number out and - // increment by 1 - public static Value incrementTime(Value time) { - int t = getTime(time); - if (t < 0) { - return new Constant("ERROR"); - } - return new Constant("t" + (t + 1)); - } - - public static Optional>> apply(Set background, Action action, State state, Value t) { + public static Optional>> apply(Set background, Action action, State state) { // // Get resulting states from cache if computed before if(applyCache.containsKey(Triple.of(background, action, state))){ @@ -201,20 +195,12 @@ public class Operations { // Ask theorem prover for witnesses that satisfy the precondition Set givens = Sets.union(background, state.getFormulae()); - // TODO: Have all this ?now and (next ?now) code within Action.java - - // Replace ?now with current time within preconditions Formula precondition = action.getPrecondition(); - Value now = new Variable("?now"); - precondition = replaceValue(precondition, now, t); - // We already replaced the ?now List openVars = action.openVars() .stream() - .filter(v -> !v.getName().equals("?now")) .collect(Collectors.toList()); - // TODO: Can likely more intelligently cache considering time... Optional>> bindingsOpt = proveAndGetBindingsCached(givens, precondition, openVars); // If not witnesses found, return nothing @@ -240,13 +226,6 @@ public class Operations { Set additions = groundedAction.getAdditions(); Set deletions = groundedAction.getDeletions(); - // Replace (next ?now) with appropriate time - Value nextTime = incrementTime(t); - Value nextTimeVar = new Variable("?next"); - additions = replaceValue(additions, nextTimeVar, nextTime); - deletions = replaceValue(deletions, nextTimeVar, nextTime); - - State newState = State.initializeWith(Sets.union( Sets.difference(state.getFormulae(), deletions), additions @@ -264,97 +243,6 @@ public class Operations { } - public static State replaceValue(State s, Value r, Value t) { - Set newFormulae = replaceValue(s.getFormulae(), r, t); - return State.initializeWith(newFormulae); - } - - public static Set replaceValue(Set s, Value r, Value t) { - Set newFormulae = new HashSet(); - for (Formula f : s) { - newFormulae.add(replaceValue(f, r, t)); - } - return newFormulae; - } - - public static Value replaceValue(Value v, Value r, Value t) { - if (v.getName().equals(r.getName())) { - return t; - } - return v; - } - - // Everywhere where there's a ?now replace with value t - public static Formula replaceValue(Formula f, Value r, Value t) { - // Base Cases: - - // Bottom of Formula graph wouldn't have any time points under it - if (f instanceof Predicate || f instanceof Atom) { - return f; - } - - // Check if these quantifiers contain our bound varialbe - if (f instanceof UnaryModalFormula) { - UnaryModalFormula uf = (UnaryModalFormula) f; - - Value agent = uf.getAgent(); - Value time = uf.getTime(); - Value newTime = replaceValue(time, r, t); - Formula uf_sub = uf.getFormula(); - Formula new_uf_sub = replaceValue(uf_sub, r, t); - - if (f instanceof Belief) { - return new Belief(agent, newTime, new_uf_sub); - } else if (f instanceof Intends) { - return new Intends(agent, newTime, new_uf_sub); - } else if (f instanceof Knowledge) { - return new Knowledge(agent, newTime, new_uf_sub); - } - // Assumes Perception - if (! (f instanceof Perception)) { - System.out.println("[fixTimepoints:Operations.java] Doesn't account for new modal operator"); - } - return new Perception(agent, newTime, new_uf_sub); - } - - // Recusive Case: Iterate over each subformula and replace - - if (f instanceof Not) { - Formula subFormula = ((Not) f).getArgument(); - return new Not(replaceValue(subFormula, r, t)); - } else if (f instanceof Universal) { - Formula subFormula = ((Universal) f).getArgument(); - return new Universal(((Universal) f).vars(), replaceValue(subFormula, r, t)); - } else if (f instanceof Existential) { - Formula subFormula = ((Existential) f).getArgument(); - return new Universal(((Existential) f).vars(), replaceValue(subFormula, r, t)); - } else if (f instanceof Implication) { - Formula antecedant = ((Implication) f).getAntecedent(); - Formula consequent = ((Implication) f).getConsequent(); - return new Implication(replaceValue(antecedant, r, t), replaceValue(consequent, r, t)); - } else if (f instanceof BiConditional) { - Formula left = ((BiConditional) f).getLeft(); - Formula right = ((BiConditional) f).getRight(); - return new BiConditional(replaceValue(left, r, t), replaceValue(right, r, t)); - } - - List subFormulae = f.getArgs(); - List newArguments = new ArrayList(); - for (Formula sf : subFormulae) { - newArguments.add(replaceValue(sf, r, t)); - } - - if (f instanceof And) { - return new And(newArguments); - } - - // Assume Or - if (! (f instanceof Or)) { - System.out.println("[fixTimepoints:Operations.java] Not accounting for formula type in recursive case"); - } - return new Or(newArguments); - } - public static boolean equivalent(Set background, Formula f1, Formula f2) { if (!DEEP_EQUIVALENCE) { return f1.equals(f2); diff --git a/src/main/java/org/rairlab/planner/search/AStarPlanner.java b/src/main/java/org/rairlab/planner/search/AStarPlanner.java index 4799748..6212d9d 100644 --- a/src/main/java/org/rairlab/planner/search/AStarPlanner.java +++ b/src/main/java/org/rairlab/planner/search/AStarPlanner.java @@ -86,11 +86,11 @@ public class AStarPlanner { State lastState = currentSearch.getLeft(); List previous_actions = currentSearch.getRight(); - System.out.println("--------------------"); - System.out.println("Considering state with heuristic: " + comparator.getValue(currentSearch)); - System.out.println("Current Plan: " + seq.get(lastState).toString()); - System.out.println("Current State: " + lastState.toString()); - System.out.println("--------------------"); + // System.out.println("--------------------"); + // System.out.println("Considering state with heuristic: " + comparator.getValue(currentSearch)); + // System.out.println("Current Plan: " + seq.get(lastState).toString()); + // System.out.println("Current State: " + lastState.toString()); + // System.out.println("--------------------"); // Exit loop if we've passed the depth limit int currentDepth = previous_actions.size(); @@ -116,8 +116,7 @@ public class AStarPlanner { for (Action action : nonTrivialActions) { // System.out.println("Considering action: " + action.getName()); - Value currentTime = Operations.getTime(previous_actions.size()); - Optional>> optNextStateActionPairs = Operations.apply(background, action, lastState, currentTime); + Optional>> optNextStateActionPairs = Operations.apply(background, action, lastState); // Ignore actions that aren't applicable if (optNextStateActionPairs.isEmpty()) {