diff --git a/pom.xml b/pom.xml
index d54d1be..c8473ea 100644
--- a/pom.xml
+++ b/pom.xml
@@ -35,6 +35,12 @@
0.5.0
+
+ com.google.guava
+ guava
+ 21.0
+
+
1.8
diff --git a/src/main/java/edu/rpi/rair/DepthFirstPlanner.java b/src/main/java/edu/rpi/rair/DepthFirstPlanner.java
index 605345e..5054f24 100644
--- a/src/main/java/edu/rpi/rair/DepthFirstPlanner.java
+++ b/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() {
diff --git a/src/main/java/edu/rpi/rair/GoalTracker.java b/src/main/java/edu/rpi/rair/GoalTracker.java
index 5b2bccd..3972294 100644
--- a/src/main/java/edu/rpi/rair/GoalTracker.java
+++ b/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();
}
diff --git a/src/main/java/edu/rpi/rair/Operations.java b/src/main/java/edu/rpi/rair/Operations.java
index c1a1bdf..90aa7bd 100644
--- a/src/main/java/edu/rpi/rair/Operations.java
+++ b/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, Formula>, Optional> proverCache = CollectionUtils.newMap();
+ private static final Map, Formula, List>, Optional>>> proverBindingsCache = CollectionUtils.newMap();
+ private static final Map, Action, State>, Optional>> > applyCache = CollectionUtils.newMap();
+
+
+ public static void reset(){
+
+ proverCache.clear();
+ proverBindingsCache.clear();
+ applyCache.clear();
+ }
+ static {
prover = new SnarkWrapper();
+
}
- public static synchronized Optional> proveAndGetBindings(Set givens, Formula goal, List variables){
+ public static synchronized Optional proveCached(Set assumptions, Formula goal) {
- Future>> future = new FutureTask<>(()->{
- return prover.proveAndGetBindings(givens, goal, variables);
+ Pair, Formula> inputPair = ImmutablePair.from(assumptions, goal);
+
+ if (proverCache.containsKey(inputPair)) {
+
+ return proverCache.get(inputPair);
+
+ }
+
+ Optional, Formula>, Optional>> cachedOptional = proverCache.entrySet().stream().filter(pairOptionalEntry -> {
+
+ Set 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 answer = prover.prove(assumptions, goal);
+
+ proverCache.put(inputPair, answer);
+
+ return answer;
+ }
+
+ }
+
+ public static synchronized Optional>> proveAndGetBindingsCached(Set givens, Formula goal, List variables) {
+
+
+ Triple, Formula, List> inputTriple = Triple.of(givens, goal, variables);
+
+ if (proverBindingsCache.containsKey(inputTriple)) {
+
+ return proverBindingsCache.get(inputTriple);
+
+ } else {
+
+ Optional>> answer = proveAndGetMultipleBindings(givens, goal, variables);
+
+ proverBindingsCache.put(inputTriple, answer);
+
+ return answer;
+ }
+
+ }
+
+ public static synchronized Optional> proveAndGetBindings(Set givens, Formula goal, List variables) {
+
+ Future>> future = new FutureTask<>(() -> {
+ return prover.proveAndGetBindings(givens, goal, variables);
});
Optional> 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>> proveAndGetMultipleBindings(Set givens, Formula goal, List variables){
+ public static synchronized Optional>> proveAndGetMultipleBindings(Set givens, Formula goal, List variables) {
- return prover.proveAndGetMultipleBindings(givens, goal, variables);
+ return prover.proveAndGetMultipleBindings(givens, goal, variables);
/* Future>>> future = new FutureTask<>(()-> prover.proveAndGetMultipleBindings(givens, goal, variables));
@@ -75,58 +143,63 @@ public class Operations {
*/
}
- public static Optional>> apply(Set background, Action action, State state){
+ public static Optional>> apply(Set background, Action action, State state) {
+ if(applyCache.containsKey(Triple.of(background, action, state))){
+
+ return applyCache.get(Triple.of(background, action, state));
+ }
Set givens = Sets.union(background, state.getFormulae());
- Optional>> bindingsOpt = proveAndGetMultipleBindings(givens, action.getPrecondition(), action.openVars());
+ Optional>> 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> nexts = Sets.newSet();
- for(Map binding: bindingsOpt.get()){
+ Set> nexts = Sets.newSet();
+ for (Map 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 instantiatedDeletions = action.instantiateDeletions(binding);
+ Set instantiatedDeletions = action.instantiateDeletions(binding);
- Set formulaeToRemove = state.getFormulae().stream().
- filter(f-> instantiatedDeletions.stream().anyMatch(d-> equivalent(background, f,d))).collect(Collectors.toSet());
+ Set formulaeToRemove = state.getFormulae().stream().
+ filter(f -> instantiatedDeletions.stream().anyMatch(d -> equivalent(background, f, d))).collect(Collectors.toSet());
- Set newFormulae = state.getFormulae();
+ Set 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 emptyBinding = CollectionUtils.newMap();
- Set instantiatedDeletions = action.instantiateDeletions(emptyBinding);
+ Set instantiatedDeletions = action.instantiateDeletions(emptyBinding);
Set 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 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 background, Formula f1, Formula f2){
+ public static boolean equivalent(Set 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 background, State state, State goal){
+ public static boolean satisfies(Set 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 background, State state1, State state2){
+ public static boolean conflicts(Set 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();
}
diff --git a/src/main/java/edu/rpi/rair/utils/RunDemo.java b/src/main/java/edu/rpi/rair/utils/RunDemo.java
index 673ad4a..89f5d58 100644
--- a/src/main/java/edu/rpi/rair/utils/RunDemo.java
+++ b/src/main/java/edu/rpi/rair/utils/RunDemo.java
@@ -32,7 +32,7 @@ public class RunDemo {
List 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 goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("goal_management_3.clj")));
+ List goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("goal_management_1.clj")));
GoalTrackingProblem goalTrackingProblem = goalTrackingProblemList.get(0);
diff --git a/src/main/resources/edu/rpi/rair/goal_management_1.clj b/src/main/resources/edu/rpi/rair/goal_management_1.clj
index c0b7469..8790842 100644
--- a/src/main/resources/edu/rpi/rair/goal_management_1.clj
+++ b/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)]}}
diff --git a/src/main/resources/edu/rpi/rair/goal_management_3.clj b/src/main/resources/edu/rpi/rair/goal_management_3.clj
index 576ec29..f0e335d 100644
--- a/src/main/resources/edu/rpi/rair/goal_management_3.clj
+++ b/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)]}
diff --git a/src/main/resources/edu/rpi/rair/goal_management_4.clj b/src/main/resources/edu/rpi/rair/goal_management_4.clj
new file mode 100644
index 0000000..40eb96c
--- /dev/null
+++ b/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)]}
+ }
+
+ }
\ No newline at end of file
diff --git a/src/main/resources/edu/rpi/rair/goal_management_5.clj b/src/main/resources/edu/rpi/rair/goal_management_5.clj
new file mode 100644
index 0000000..3b599d6
--- /dev/null
+++ b/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)]}
+ }
+
+ }
\ No newline at end of file