diff --git a/pom.xml b/pom.xml index 12694c2..52044d9 100644 --- a/pom.xml +++ b/pom.xml @@ -16,17 +16,17 @@ 2.4 - sandbox + runner - org.rairlab.planner.Py4JServer + org.rairlab.planner.utils.Runner jar-with-dependencies - sandbox + runner package diff --git a/src/main/java/org/rairlab/planner/Action.java b/src/main/java/org/rairlab/planner/Action.java index 7d4d0f0..057de89 100644 --- a/src/main/java/org/rairlab/planner/Action.java +++ b/src/main/java/org/rairlab/planner/Action.java @@ -49,7 +49,14 @@ public class Action { this.freeVariables = freeVariables; - this.precondition = new And(preconditions.stream().collect(Collectors.toList())); + if (preconditions.size() > 1) { + this.precondition = new And(preconditions.stream().collect(Collectors.toList())); + } else if (preconditions.size() == 1) { + this.precondition = preconditions.iterator().next(); + } else { + this.precondition = State.TRUE; + } + this.weight = preconditions.stream().mapToInt(Formula::getWeight).sum() + additions.stream().mapToInt(Formula::getWeight).sum() + diff --git a/src/main/java/org/rairlab/planner/Operations.java b/src/main/java/org/rairlab/planner/Operations.java index 7f90582..c3999ed 100644 --- a/src/main/java/org/rairlab/planner/Operations.java +++ b/src/main/java/org/rairlab/planner/Operations.java @@ -4,11 +4,12 @@ import org.rairlab.planner.utils.Visualizer; import org.rairlab.shadow.prover.core.Prover; import org.rairlab.shadow.prover.core.ccprovers.CognitiveCalculusProver; import org.rairlab.shadow.prover.core.proof.Justification; -import org.rairlab.shadow.prover.representations.formula.BiConditional; -import org.rairlab.shadow.prover.representations.formula.Formula; - import org.rairlab.shadow.prover.representations.value.Value; import org.rairlab.shadow.prover.representations.value.Variable; +import org.rairlab.shadow.prover.representations.formula.*; +import org.rairlab.shadow.prover.representations.value.Constant; + + import org.rairlab.shadow.prover.utils.CollectionUtils; import org.rairlab.shadow.prover.utils.Sets; @@ -16,11 +17,14 @@ import org.apache.commons.lang3.tuple.Pair; import org.apache.commons.lang3.tuple.ImmutablePair; import org.apache.commons.lang3.tuple.Triple; +import java.util.ArrayList; +import java.util.HashSet; import java.util.List; import java.util.Map; import java.util.Optional; import java.util.Set; import java.util.concurrent.*; +import java.util.stream.Collectors; /** * Created by naveensundarg on 1/13/17. @@ -29,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; @@ -48,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; } @@ -155,10 +164,9 @@ public class Operations { return Optional.of(ans.get().getRight()); } - public static Optional>> apply(Set background, Action action, State state) { - // Get resulting states from cache if computed before + // // Get resulting states from cache if computed before if(applyCache.containsKey(Triple.of(background, action, state))){ Optional>> ans = applyCache.get(Triple.of(background, action, state)); if(ans.isPresent()){ @@ -169,7 +177,14 @@ public class Operations { // Ask theorem prover for witnesses that satisfy the precondition Set givens = Sets.union(background, state.getFormulae()); - Optional>> bindingsOpt = proveAndGetBindingsCached(givens, action.getPrecondition(), action.openVars()); + + Formula precondition = action.getPrecondition(); + + List openVars = action.openVars() + .stream() + .collect(Collectors.toList()); + + Optional>> bindingsOpt = proveAndGetBindingsCached(givens, precondition, openVars); // If not witnesses found, return nothing if (!bindingsOpt.isPresent()) { @@ -191,9 +206,12 @@ public class Operations { // newState = (oldState - Deletions(a)) U Additions(a) Action groundedAction = action.instantiate(binding); + Set additions = groundedAction.getAdditions(); + Set deletions = groundedAction.getDeletions(); + State newState = State.initializeWith(Sets.union( - Sets.difference(state.getFormulae(), groundedAction.getDeletions()), - groundedAction.getAdditions() + Sets.difference(state.getFormulae(), deletions), + additions )); // If the state progresses, record it as a possible next state @@ -203,6 +221,7 @@ public class Operations { } applyCache.put(Triple.of(background, action, state), Optional.of(nextStates)); + return Optional.of(nextStates); } diff --git a/src/main/java/org/rairlab/planner/State.java b/src/main/java/org/rairlab/planner/State.java index 38de048..cbc9697 100644 --- a/src/main/java/org/rairlab/planner/State.java +++ b/src/main/java/org/rairlab/planner/State.java @@ -12,14 +12,17 @@ import java.util.Set; public class State { final Set formulae; + static Formula TRUE; static Formula FALSE; static{ try { + TRUE = Reader.readFormulaFromString("(or P (not P))"); FALSE = Reader.readFormulaFromString("(and P (not P))"); } catch (Reader.ParsingException e) { e.printStackTrace(); + TRUE = null; FALSE = null; } diff --git a/src/main/java/org/rairlab/planner/search/AStarPlanner.java b/src/main/java/org/rairlab/planner/search/AStarPlanner.java index ec79e63..bbed1ba 100644 --- a/src/main/java/org/rairlab/planner/search/AStarPlanner.java +++ b/src/main/java/org/rairlab/planner/search/AStarPlanner.java @@ -6,6 +6,7 @@ import org.rairlab.planner.State; import org.rairlab.planner.Action; import org.rairlab.planner.Plan; import org.rairlab.planner.Operations; +import org.rairlab.shadow.prover.representations.value.Value; import java.util.*; import java.util.function.Function; @@ -67,6 +68,10 @@ public class AStarPlanner { comparator.setValue(searchStart, 0); search.add(searchStart); + // For debugging... + // Map> seq = new HashMap>(); + // seq.put(start, new ArrayList()); + // Current set of plans Set plansFound = new HashSet(); @@ -81,7 +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("--------------------"); // Exit loop if we've passed the depth limit int currentDepth = previous_actions.size(); @@ -105,6 +114,8 @@ public class AStarPlanner { // Apply the action to the state and add to the search space for (Action action : nonTrivialActions) { + // System.out.println("Considering action: " + action.getName()); + Optional>> optNextStateActionPairs = Operations.apply(background, action, lastState); // Ignore actions that aren't applicable @@ -137,6 +148,10 @@ public class AStarPlanner { int heuristicValue = heuristic.apply(nextState); comparator.setValue(futureSearch, planCost + heuristicValue); search.add(futureSearch); + + // For debugging... + // seq.put(nextState, next_actions); + } } } diff --git a/src/main/java/org/rairlab/planner/utils/Runner.java b/src/main/java/org/rairlab/planner/utils/Runner.java index c540233..a95b46a 100644 --- a/src/main/java/org/rairlab/planner/utils/Runner.java +++ b/src/main/java/org/rairlab/planner/utils/Runner.java @@ -46,10 +46,11 @@ public final class Runner { } AStarPlanner astarplanner = new AStarPlanner(); - astarplanner.setK(2); + astarplanner.setK(1); for (PlanningProblem planningProblem : planningProblemList) { + long start = System.currentTimeMillis(); Set plans = astarplanner.plan( planningProblem.getBackground(), planningProblem.getActions(), @@ -57,9 +58,11 @@ public final class Runner { planningProblem.getGoal(), ConstantHeuristic::h ); + long end = System.currentTimeMillis(); if(plans.size() > 0) { System.out.println(plans.toString()); + System.out.println("Time (ms): " + (end - start)); } else { System.out.println("FAILED"); diff --git a/src/main/resources/org/rairlab/planner/problems/epistemic/grapevine.clj b/src/main/resources/org/rairlab/planner/problems/epistemic/grapevine.clj index ecded3f..3cce961 100644 --- a/src/main/resources/org/rairlab/planner/problems/epistemic/grapevine.clj +++ b/src/main/resources/org/rairlab/planner/problems/epistemic/grapevine.clj @@ -61,16 +61,17 @@ ] :additions [ (Believes! ?a2 (the ?a1)) - (Believes ?a3 (the ?a1)) - (Believes ?a1 (Believes! ?a2 (the ?a1))) - (Believes ?a1 (Believes! ?a3 (the ?a1))) + (Believes! ?a3 (the ?a1)) + (Believes! ?a1 (Believes! ?a2 (the ?a1))) + (Believes! ?a1 (Believes! ?a3 (the ?a1))) ] :deletions [ (not (Believes! ?a2 (the ?a1))) (not (Believes! ?a3 (the ?a1))) - (not (Believes ?a1 (Believes! ?a2 (the ?a1)))) - (not (Believes ?a1 (Believes! ?a3 (the ?a1)))) + (not (Believes! ?a1 (Believes! ?a2 (the ?a1)))) + (not (Believes! ?a1 (Believes! ?a3 (the ?a1)))) ] + :cost 2 }) (define-action share-single [?a1 ?a2 ?a3 ?r] { @@ -96,6 +97,7 @@ (not (Believes! ?a2 (the ?a1))) (not (Believes! ?a1 (Believes! ?a2 (the ?a1)))) ] + :cost 2 }) ]