Caching and new problem.

pom.xml

@@ -35,6 +35,12 @@
             <version>0.5.0</version>
         </dependency>
 
+        <dependency>
+            <groupId>com.google.guava</groupId>
+            <artifactId>guava</artifactId>
+            <version>21.0</version>
+        </dependency>
+
     </dependencies>
     <properties>
         <maven.compiler.source>1.8</maven.compiler.source>

src/main/java/edu/rpi/rair/DepthFirstPlanner.java

@@ -13,7 +13,7 @@ import java.util.stream.Collectors;
 public class DepthFirstPlanner implements Planner {
 
 
-    private static  int MAX_DEPTH = 3;
+    private static  int MAX_DEPTH = 4;
     private static  boolean EXHAUSTIVE_TILL_MAX_DEPTH = false;
 
     public static int getMaxDepth() {

src/main/java/edu/rpi/rair/GoalTracker.java

@@ -31,6 +31,8 @@ public class GoalTracker {
         this.currentGoals = CollectionUtils.newEmptySet();
         this.planner = new DepthFirstPlanner();
         this.actions = actions;
+
+        Operations.reset();
     }
 
 

src/main/java/edu/rpi/rair/Operations.java

@@ -2,7 +2,7 @@ package edu.rpi.rair;
 
 import com.naveensundarg.shadow.prover.core.Prover;
 import com.naveensundarg.shadow.prover.core.SnarkWrapper;
-import com.naveensundarg.shadow.prover.representations.formula.And;
+import com.naveensundarg.shadow.prover.core.proof.Justification;
 import com.naveensundarg.shadow.prover.representations.formula.BiConditional;
 import com.naveensundarg.shadow.prover.representations.formula.Formula;
 import com.naveensundarg.shadow.prover.representations.value.Value;
@@ -11,6 +11,7 @@ import com.naveensundarg.shadow.prover.utils.CollectionUtils;
 import com.naveensundarg.shadow.prover.utils.ImmutablePair;
 import com.naveensundarg.shadow.prover.utils.Pair;
 import com.naveensundarg.shadow.prover.utils.Sets;
+import org.apache.commons.lang3.tuple.Triple;
 
 import java.util.List;
 import java.util.Map;
@@ -31,34 +32,101 @@ public class Operations {
     private static Prover prover;
 
 
-    static{
+    private static final Map<Pair<Set<Formula>, Formula>, Optional<Justification>> proverCache = CollectionUtils.newMap();
+    private static final Map<Triple<Set<Formula>, Formula, List<Variable>>, Optional<Set<Map<Variable, Value>>>> proverBindingsCache = CollectionUtils.newMap();
+    private static final Map<Triple<Set<Formula>, Action, State>, Optional<Set<Pair<State, Action>>> > applyCache = CollectionUtils.newMap();
+
+
+    public static void reset(){
+
+        proverCache.clear();
+        proverBindingsCache.clear();
+        applyCache.clear();
+    }
+    static {
         prover = new SnarkWrapper();
+
     }
 
-    public static synchronized Optional<Map<Variable, Value>> proveAndGetBindings(Set<Formula> givens, Formula goal, List<Variable> variables){
+    public static synchronized Optional<Justification> proveCached(Set<Formula> assumptions, Formula goal) {
 
-        Future<Optional<Map<Variable, Value>>> future = new FutureTask<>(()->{
+        Pair<Set<Formula>, Formula> inputPair = ImmutablePair.from(assumptions, goal);
-                   return prover.proveAndGetBindings(givens, goal, variables);
+
+        if (proverCache.containsKey(inputPair)) {
+
+            return proverCache.get(inputPair);
+
+        }
+
+        Optional<Map.Entry<Pair<Set<Formula>, Formula>, Optional<Justification>>> cachedOptional = proverCache.entrySet().stream().filter(pairOptionalEntry -> {
+
+            Set<Formula> cachedAssumptions = pairOptionalEntry.getKey().first();
+            Formula cachedGoal = pairOptionalEntry.getKey().second();
+
+            return cachedGoal.equals(goal) && Sets.subset(cachedAssumptions, assumptions);
+        }).findAny();
+
+
+        if(cachedOptional.isPresent()){
+
+            return cachedOptional.get().getValue();
+        }
+
+        {
+
+            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);
+
+        if (proverBindingsCache.containsKey(inputTriple)) {
+
+            return proverBindingsCache.get(inputTriple);
+
+        } else {
+
+            Optional<Set<Map<Variable, Value>>> answer = proveAndGetMultipleBindings(givens, 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{
+        try {
 
             answer = future.get(1, TimeUnit.SECONDS);
         } catch (InterruptedException | ExecutionException | TimeoutException e) {
-            answer =   Optional.empty();
+            answer = Optional.empty();
         }
 
         return answer;
     }
 
 
-     public static synchronized Optional<Set<Map<Variable, Value>>> proveAndGetMultipleBindings(Set<Formula> givens, Formula goal, List<Variable> variables){
+    public static synchronized Optional<Set<Map<Variable, Value>>> proveAndGetMultipleBindings(Set<Formula> givens, Formula goal, List<Variable> variables) {
 
-       return prover.proveAndGetMultipleBindings(givens, goal, variables);
+        return prover.proveAndGetMultipleBindings(givens, goal, variables);
 
       /*  Future<Optional<Set<Map<Variable, Value>>>> future = new FutureTask<>(()-> prover.proveAndGetMultipleBindings(givens, goal, variables));
 
@@ -75,58 +143,63 @@ public class Operations {
 */
     }
 
-    public static Optional<Set<Pair<State,Action>>> apply(Set<Formula> background, Action action, State state){
 
+    public static Optional<Set<Pair<State, Action>>> apply(Set<Formula> background, Action action, State state) {
 
+        if(applyCache.containsKey(Triple.of(background, action, state))){
+
+            return applyCache.get(Triple.of(background, action, state));
+        }
 
         Set<Formula> givens = Sets.union(background, state.getFormulae());
 
-        Optional<Set<Map<Variable, Value>>> bindingsOpt = proveAndGetMultipleBindings(givens, action.getPrecondition(), action.openVars());
+        Optional<Set<Map<Variable, Value>>> bindingsOpt = proveAndGetBindingsCached(givens, action.getPrecondition(), action.openVars());
 
         State newState;
 
-        if(!bindingsOpt.isPresent()){
+        if (!bindingsOpt.isPresent()) {
 
 
+            applyCache.put(Triple.of(background, action ,state), Optional.empty());
             return Optional.empty();
 
         }
 
-        Set<Pair<State,Action>> nexts = Sets.newSet();
+        Set<Pair<State, Action>> nexts = Sets.newSet();
-        for(Map<Variable, Value> binding: bindingsOpt.get()){
+        for (Map<Variable, Value> binding : bindingsOpt.get()) {
 
-            if(THROW_AWAY_EMPTY_BINDINGS && binding.values().stream().anyMatch(x-> x instanceof Variable)){
+            if (THROW_AWAY_EMPTY_BINDINGS && binding.values().stream().anyMatch(x -> x instanceof Variable)) {
 
-               continue;
+                continue;
             }
 
-        Set<Formula> instantiatedDeletions =  action.instantiateDeletions(binding);
+            Set<Formula> instantiatedDeletions = action.instantiateDeletions(binding);
 
-        Set<Formula> formulaeToRemove = state.getFormulae().stream().
+            Set<Formula> formulaeToRemove = state.getFormulae().stream().
-                filter(f-> instantiatedDeletions.stream().anyMatch(d-> equivalent(background, f,d))).collect(Collectors.toSet());
+                    filter(f -> instantiatedDeletions.stream().anyMatch(d -> equivalent(background, f, d))).collect(Collectors.toSet());
 
-        Set<Formula> newFormulae = state.getFormulae();
+            Set<Formula> newFormulae = state.getFormulae();
 
-        newFormulae = Sets.union(newFormulae, action.instantiateAdditions(binding));
+            newFormulae = Sets.union(newFormulae, action.instantiateAdditions(binding));
 
 
-        newFormulae = Sets.difference(newFormulae, formulaeToRemove);
+            newFormulae = Sets.difference(newFormulae, formulaeToRemove);
 
 
-        newState = State.initializeWith(newFormulae);
+            newState = State.initializeWith(newFormulae);
 
-        nexts.add(ImmutablePair.from(newState, action.instantiate(binding)));
+            nexts.add(ImmutablePair.from(newState, action.instantiate(binding)));
 
 
         }
 
-        if(nexts.isEmpty()){
+        if (nexts.isEmpty()) {
 
             Map<Variable, Value> emptyBinding = CollectionUtils.newMap();
-            Set<Formula> instantiatedDeletions =  action.instantiateDeletions(emptyBinding);
+            Set<Formula> instantiatedDeletions = action.instantiateDeletions(emptyBinding);
 
             Set<Formula> formulaeToRemove = state.getFormulae().stream().
-                filter(f-> instantiatedDeletions.stream().anyMatch(d-> equivalent(background, f,d))).collect(Collectors.toSet());
+                    filter(f -> instantiatedDeletions.stream().anyMatch(d -> equivalent(background, f, d))).collect(Collectors.toSet());
 
             Set<Formula> newFormulae = state.getFormulae();
 
@@ -136,37 +209,44 @@ public class Operations {
             newFormulae = Sets.difference(newFormulae, formulaeToRemove);
 
 
-        newState = State.initializeWith(newFormulae);
+            newState = State.initializeWith(newFormulae);
 
             nexts.add(ImmutablePair.from(newState, action.instantiate(emptyBinding)));
 
 
         }
 
+        applyCache.put(Triple.of(background, action ,state), Optional.of(nexts));
+
         return Optional.of(nexts);
 
     }
 
-    public static boolean equivalent(Set<Formula> background, Formula f1, Formula f2){
+    public static boolean equivalent(Set<Formula> background, Formula f1, Formula f2) {
 
-        if(!DEEP_EQUIVALENCE){
+        if (!DEEP_EQUIVALENCE) {
             return f1.equals(f2);
         }
 
         BiConditional biConditional = new BiConditional(f1, f2);
-        return prover.prove(background,biConditional).isPresent();
+        return proveCached(background, biConditional).isPresent();
     }
 
-    public static boolean satisfies(Set<Formula> background, State state, State goal){
+    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->prover.prove(Sets.union(background, state.getFormulae()), x).isPresent());
+                allMatch(x -> proveCached(Sets.union(background, state.getFormulae()), x).isPresent());
 
     }
 
-    public static boolean conflicts(Set<Formula> background, State state1, State state2){
+    public static boolean conflicts(Set<Formula> background, State state1, State state2) {
 
-        return prover.prove(Sets.union(background, Sets.union(state1.getFormulae(), state2.getFormulae())), FALSE ).isPresent();
+
+        return proveCached(Sets.union(background, Sets.union(state1.getFormulae(), state2.getFormulae())), FALSE).isPresent();
 
     }
 

src/main/java/edu/rpi/rair/utils/RunDemo.java

@@ -32,7 +32,7 @@ public class RunDemo {
             List<Problem> problems = ProblemReader.readFrom(Sandbox.class.getResourceAsStream("firstorder-completness-tests.clj"));
 
             problems.forEach(problem -> {
-                for (int i = 0; i < 100; i++) {
+                for (int i = 0; i < 10; i++) {
                     prover.prove(problem.getAssumptions(), problem.getGoal());
 
                 }
@@ -53,7 +53,7 @@ public class RunDemo {
 
             System.out.println();
 
-            List<GoalTrackingProblem> goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("goal_management_3.clj")));
+            List<GoalTrackingProblem> goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("goal_management_1.clj")));
 
 
             GoalTrackingProblem goalTrackingProblem = goalTrackingProblemList.get(0);

src/main/resources/edu/rpi/rair/goal_management_1.clj

@@ -79,7 +79,7 @@
                G4  {:priority 1.0
                     :state [(in prisoner room2)
                            (in self room2)]}
-               G5 {:priority 1.0
+               G5 {:priority 3
 
                    :state [(interrogates commander prisoner)]}}
 

src/main/resources/edu/rpi/rair/goal_management_3.clj

@@ -3,7 +3,7 @@
          :background []
          :start      [
 
-                      (forall (?room ?x ?y) (implies (and (in ?x ?room) (and (in ?y ?room) (not (= ?x ?y)))) (sameroom ?x ?y)))
+                      ;   (forall (?room ?x ?y) (implies (and (in ?x ?room) (and (in ?y ?room) (not (= ?x ?y)))) (sameroom ?x ?y)))
                       (not (= prisoner commander))
                       (not (= self prisoner))
                       (in prisoner room1)
@@ -18,7 +18,7 @@
                       (not (= self commander))
                       (not (open (door room1)))
                       (open (door room2))
-                      (forall (?room ?x ?y) (implies (and (sameroom ?x ?y) (in ?x ?room)) (in ?y ?room)))
+                      ;  (forall (?room ?x ?y) (implies (and (sameroom ?x ?y) (in ?x ?room)) (in ?y ?room)))
 
                       ]
 
@@ -96,7 +96,9 @@
              :state    [(in prisoner room1)]}
 
          G3 {:priority 1.0
-             :state    [(sameroom self prisoner)]}
+             :state    [(forall [?room]
+                                      (if (in prisoner ?room)
+                                        (in self ?room)))]}
 
          G4 {:priority 3.0
              :state    [(in prisoner room2)]}

src/main/resources/edu/rpi/rair/goal_management_4.clj

@@ -0,0 +1,127 @@
+{:definitions
+        {:name       "demo 1"
+         :background []
+         :start      [
+                     (person prisoner)
+                     (person commander)
+                     (commander commander)
+                     (robot guard)
+                     (robot guide)
+
+                     (not (= prisoner commander))
+                     (not (= prisoner guard))
+                     (not (= prisoner guide))
+                     (not (= commander guard))
+                     (not (= commander guide))
+                     (not (= guard guide))
+
+                     (room room1)
+                     (room room2)
+                     (not (= room1 room2))
+
+                     (in prisoner room1)
+                     (in commander room2)
+                     (in guard room1)
+                     (in guide room2)
+
+                     (not (open (door room1)))
+                     (open (door room2))
+
+                     (forall (?room ?x ?y) (implies (and (in ?x ?room) (in ?y ?room)) (sameroom ?x ?y)))
+                     (forall (?room2 ?x ?room1) (implies (and (not (= ?room1 ?room2)) (in ?x ?room1)) (not (in ?x ?room2))))
+                     (forall (?room ?x ?y) (implies (and (sameroom ?x ?y) (in ?x ?room)) (in ?y ?room)))
+                      ]
+
+         :goal       []
+
+         :actions
+                     [
+
+                      (define-action move [?actor ?person ?room2 ?room1]
+                                     {:preconditions [(robot ?actor)
+                                                      (person ?person)
+                                                      (room ?room1)
+                                                      (room ?room2)
+                                                      (not (= ?room1 ?room2))
+                                                      (open (door ?room1))
+                                                      (in ?actor ?room2)
+                                                      (in ?person ?room2)
+                                                      (open (door ?room2))]
+                                      :additions     [(in ?person ?room1)]
+                                      :deletions     [(in ?person ?room2)]
+                                      })
+                      (define-action keepDoorClosed [?actor ?room]
+                                     {:preconditions [(robot ?actor)
+                                                      (room ?room)
+                                                      (in ?actor ?room)
+                                                      (not (open (door ?room)))]
+                                      :additions     []
+                                      :deletions     [(open (door ?room))]
+                                      })
+                      (define-action accompany [?actor ?person ?room1 ?room2]
+                                     {:preconditions [(robot ?actor)
+                                                      (person ?person)
+                                                      (room ?room1)
+                                                      (room ?room2)
+                                                      (not (= ?room1 ?room2))
+                                                      (open (door ?room1))
+                                                      (in ?person ?room1)
+                                                      (open (door ?room2))
+                                                      (not (= ?person ?actor))
+                                                      (in ?actor ?room1)]
+                                      :additions     [(in ?actor ?room2)
+                                                      (in ?person ?room2)]
+                                      :deletions     [(in ?person ?room1)
+                                                      (in ?actor ?room1)]
+                                      })
+                      (define-action openDoor [?actor ?room]
+                                     {:preconditions [(robot ?actor)
+                                                      (room ?room)
+                                                      (in ?actor ?room)
+                                                      (not (open (door ?room)))]
+                                      :additions     [(open (door ?room))]
+                                      :deletions     [(not (open (door ?room)))]
+                                      })
+                      (define-action stayInRoom [?actor ?room]
+                                     {:preconditions [(in ?actor ?room)
+                                                      (room ?room)]
+                                      :additions     [(in ?actor ?room)]
+                                      :deletions     []
+                                      })
+                      (define-action interrogate [?actor ?person]
+                                     {:preconditions [(person ?person)
+                                                      (commander ?actor)
+                                                      (in ?actor ?room)
+                                                      (in ?person ?room)
+                                                      (room ?room)]
+                                      :additions     [(interrogates ?actor ?person)]
+                                      :deletions     []
+                                      })
+                      (define-action staySameRoom [?actor ?person]
+                                     {:preconditions [(robot ?actor)
+                                                      (sameroom ?actor ?person)
+                                                      (person ?person)
+                                                      (in ?actor ?room)
+                                                      (in ?person ?room)
+                                                      (room ?room)]
+                                      :additions     [(sameroom ?actor ?person)]
+                                      :deletions     []
+                                      })
+
+                      ]
+         }
+
+ :goals {G1 {:priority 1.0
+             :state    [(not (open (door room1)))]}
+
+         G2 {:priority 1.0
+             :state    [(in prisoner room1)]}
+
+         G3 {:priority 1.0
+             :state    [(sameroom guard prisoner)]}
+
+         G4 {:priority 6.0
+             :state    [(interrogates commander prisoner)]}
+         }
+
+ }

src/main/resources/edu/rpi/rair/goal_management_5.clj

@@ -0,0 +1,141 @@
+{:definitions
+        {:name       "demo 1"
+         :background []
+         :start      [
+                     (person prisoner)
+                     (person commander)
+                     (commander commander)
+                     (robot guard)
+                     (robot guide)
+
+                     (not (= prisoner commander))
+                     (not (= prisoner guard))
+                     (not (= prisoner guide))
+                     (not (= commander guard))
+                     (not (= commander guide))
+                     (not (= guard guide))
+
+                     (room room1)
+                     (room room2)
+                     (room hallway)
+                     (not (= room1 room2))
+                     (not (= room1 hallway))
+                     (not (= room2 hallway))
+
+                     (in prisoner room1)
+                     (in commander room2)
+                     (in guard room1)
+                     (in guide hallway)
+
+                     (not (open (door room1)))
+                     (open (door room2))
+                     (open (door hallway))
+
+                      (forall [?x ?y] (if (accompanies ?x ?y) (accompanies ?y ?x)))
+                      (forall (?room ?x ?y) (implies (and (in ?x ?room) (and (in ?y ?room) (not (= ?x ?y)))) (sameroom ?x ?y)))
+                      (forall (?room2 ?x ?room1) (implies (and (not (= ?room1 ?room2)) (in ?x ?room1)) (not (in ?x ?room2))))
+                      (forall (?room ?x ?y) (implies (and (sameroom ?x ?y) (in ?x ?room)) (in ?y ?room)))
+                      ]
+
+         :goal       []
+
+         :actions
+                     [
+
+                      (define-action move [?actor ?room1 ?room2]
+                                     {:preconditions [(robot ?actor)
+                                                      (room ?room1)
+                                                      (room ?room2)
+                                                      (in ?actor ?room1)
+                                                      (open (door ?room1))
+                                                      (open (door ?room2))
+                                                      (not (= ?room1 ?room2))]
+                                      :additions     [(in ?actor ?room2)]
+                                      :deletions     [(in ?actor ?room1)]
+                                      })
+
+                      (define-action keepDoorClosed [?actor ?room]
+                                     {:preconditions [(robot ?actor)
+                                                      (room ?room)
+                                                      (in ?actor ?room)
+                                                      (not (open (door ?room)))]
+                                      :additions     []
+                                      :deletions     [(open (door ?room))]
+                                      })
+
+                      (define-action accompany [?actor ?person1 ?person2 ?room1 ?room2]
+                                     {:preconditions [(robot ?actor)
+                                                      (person ?person1)
+                                                      (room ?room1)
+                                                      (room ?room2)
+                                                      (in ?actor ?room1)
+                                                      (in ?person1 ?room1)
+                                                      (in ?person2 ?room2)
+                                                      (open (door ?room1))
+                                                      (open (door ?room2))
+                                                      (not (= ?actor ?person1))
+                                                      (not (= ?actor ?person2))
+                                                      (not (= ?room1 ?room2))]
+                                      :additions     [(accompanies ?person1 ?person2)
+                                                      (in ?actor ?room2)
+                                                      (in ?person1 ?room2)]
+                                      :deletions     [(in ?actor ?room1)
+                                                      (in ?person1 ?room1)]
+                                      })
+
+                      (define-action accompany2 [?actor ?person1 ?person2]
+                                     {:preconditions [(robot ?actor)
+                                                      (person ?person1)
+                                                      (person ?person2)
+                                                      (in ?actor ?room)
+                                                      (in ?person1 ?room)
+                                                      (in ?person2 ?room)
+                                                      (not (= ?actor ?person1))
+                                                      (not (= ?actor ?person2))
+                                                      (not (= ?person1 ?person2))]
+                                      :additions     [(accompanies ?actor ?person1 ?person2)]
+                                      :deletions     []
+                                      })
+
+                      (define-action openDoor [?actor ?room]
+                                     {:preconditions [(robot ?actor)
+                                                      (room ?room)
+                                                      (in ?actor ?room)
+                                                      (not (open (door ?room)))]
+                                      :additions     [(open (door ?room))]
+                                      :deletions     [(not (open (door ?room)))]
+                                      })
+                      (define-action stayInRoom [?actor ?room]
+                                     {:preconditions [(in ?actor ?room)
+                                                      (room ?room)]
+                                      :additions     [(in ?actor ?room)]
+                                      :deletions     []
+                                      })
+                      (define-action staySameRoom [?actor ?person]
+                                     {:preconditions [(robot ?actor)
+                                                      (sameroom ?actor ?person)
+                                                      (person ?person)
+                                                      (in ?actor ?room)
+                                                      (in ?person ?room)
+                                                      (room ?room)]
+                                      :additions     [(sameroom ?actor ?person)]
+                                      :deletions     []
+                                      })
+
+                      ]
+         }
+
+ :goals {G1 {:priority 1.0
+             :state    [(not (open (door room1)))]}
+
+         G2 {:priority 1.0
+             :state    [(in prisoner room1)]}
+
+         G3 {:priority 1.0
+             :state    [(sameroom guard prisoner)]}
+
+         G4 {:priority 3.0
+             :state    [(accompanies prisoner commander)]}
+         }
+
+ }