Improving DCEC support

- Time based search algorithm
- Added new variables ?now and ?next

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.
@@ -155,10 +159,37 @@ public class Operations {
         return Optional.of(ans.get().getRight());
     }
 
+    public static Value getTime(int time) {
+        return new Constant("t" + time);
+    }
 
-    public static Optional<Set<Pair<State, Action>>> apply(Set<Formula> background, Action action, State state) {
+    public static int getTime(Value time) {
+        String s = time.getName();
+        String[] ss = s.split("t");
+        if (ss.length != 2) {
+            return -1;
+        }
+        try {
+            int t = Integer.parseInt(ss[1]);
+            return t + 1;
+        } catch (NumberFormatException e) {
+            return -1;
+        }
+    }
 
-        // Get resulting states from cache if computed before
+    // 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<Set<Pair<State, Action>>> apply(Set<Formula> background, Action action, State state, Value t) {
+
+        // // Get resulting states from cache if computed before
         if(applyCache.containsKey(Triple.of(background, action, state))){
             Optional<Set<Pair<State, Action>>>  ans  = applyCache.get(Triple.of(background, action, state));
             if(ans.isPresent()){
@@ -169,7 +200,22 @@ public class Operations {
 
         // Ask theorem prover for witnesses that satisfy the precondition
         Set<Formula> givens = Sets.union(background, state.getFormulae());
-        Optional<Set<Map<Variable, Value>>> bindingsOpt = proveAndGetBindingsCached(givens, action.getPrecondition(), action.openVars());
+
+        // 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<Variable> openVars = action.openVars()
+            .stream()
+            .filter(v -> !v.getName().equals("?now"))
+            .collect(Collectors.toList());
+
+        // TODO: Can likely more intelligently cache considering time...
+        Optional<Set<Map<Variable, Value>>> bindingsOpt = proveAndGetBindingsCached(givens, precondition, openVars);
 
         // If not witnesses found, return nothing
         if (!bindingsOpt.isPresent()) {
@@ -191,9 +237,19 @@ public class Operations {
             // newState = (oldState - Deletions(a)) U Additions(a)
             Action groundedAction = action.instantiate(binding);
 
+            Set<Formula> additions = groundedAction.getAdditions();
+            Set<Formula> 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(), groundedAction.getDeletions()),
+                Sets.difference(state.getFormulae(), deletions),
-                groundedAction.getAdditions()
+                additions
             ));
 
             // If the state progresses, record it as a possible next state
@@ -203,10 +259,102 @@ public class Operations {
         }
 
         applyCache.put(Triple.of(background, action, state), Optional.of(nextStates));
+
         return Optional.of(nextStates);
 
     }
 
+    public static State replaceValue(State s, Value r, Value t) {
+        Set<Formula> newFormulae = replaceValue(s.getFormulae(), r, t);
+        return State.initializeWith(newFormulae);
+    }
+
+    public static Set<Formula> replaceValue(Set<Formula> s, Value r, Value t) {
+        Set<Formula> newFormulae = new HashSet<Formula>();
+        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<Formula> subFormulae = f.getArgs();
+        List<Formula> newArguments = new ArrayList<Formula>();
+        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<Formula> background, Formula f1, Formula f2) {
         if (!DEEP_EQUIVALENCE) {
             return f1.equals(f2);

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<State, List<Action>> seq = new HashMap<State, List<Action>>();
+        seq.put(start, new ArrayList<Action>());
+
         // Current set of plans
         Set<Plan> plansFound = new HashSet<Plan>();
 
@@ -81,7 +86,11 @@ public class AStarPlanner {
             State lastState = currentSearch.getLeft();
             List<Action> previous_actions = currentSearch.getRight();
 
-            // System.out.println("Considering state with heuristic: " + comparator.getValue(currentSearch));
+            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,7 +114,10 @@ public class AStarPlanner {
 
             // Apply the action to the state and add to the search space
             for (Action action : nonTrivialActions) {
-                Optional<Set<Pair<State, Action>>> optNextStateActionPairs = Operations.apply(background, action, lastState);
+                // System.out.println("Considering action: " + action.getName());
+
+                Value currentTime = Operations.getTime(previous_actions.size());
+                Optional<Set<Pair<State, Action>>> optNextStateActionPairs = Operations.apply(background, action, lastState, currentTime);
 
                 // Ignore actions that aren't applicable
                 if (optNextStateActionPairs.isEmpty()) {
@@ -137,6 +149,10 @@ public class AStarPlanner {
                     int heuristicValue = heuristic.apply(nextState);
                     comparator.setValue(futureSearch, planCost + heuristicValue);
                     search.add(futureSearch);
+
+                    // For debugging...
+                    seq.put(nextState, next_actions);
+
                 }
             }
         }

src/main/java/org/rairlab/planner/utils/Runner.java

@@ -46,7 +46,7 @@ public final class Runner {
         }
 
         AStarPlanner astarplanner = new AStarPlanner();
-        astarplanner.setK(2);
+        astarplanner.setK(1);
 
         for (PlanningProblem planningProblem : planningProblemList) {
 

src/main/resources/org/rairlab/planner/problems/conformant/block_tiny.clj

@@ -0,0 +1,108 @@
+; Original problem from Joerg Hoffmann and Ronen Brafman
+{:name "Block-Conformant-Tiny"
+    :background [
+        ; Setting object types
+        (block b1)
+        (block b2)
+
+        ; Unique name axioms
+        (not (= b1 b2))
+
+        ; Block World Axioms
+
+        ; Blocks are never on themselves
+        (forall [x] (not (on x x)))
+        ; on is not symmetric
+        (forall [x y] (if (on x y) (not (on y x))))
+        ; Any block on a table isn't on top of another block
+        (forall [x y] (if (on-table x) (not (on x y))))
+        ; Any block that is cleared does not have another block on top of it
+        (forall [x y] (if (clear x) (not (on y x))))
+
+        ; NOTE: Slow if we use complicated definitions
+        ;; ; A block is on the table if it isn't on top of any other block
+        ;; (forall [x] (iff (on-table x) (forall [y] (not (on x y)))))
+        ;; ; A block is cleared if there is no other block on top of it
+        ;; (forall [x] (iff (clear x) (forall [y] (not (on y x)))))
+    ]
+
+
+    :actions [
+
+        (define-action move-bstack-to-t [?b ?b1] {
+            :preconditions [ 
+                ; Type restriction
+                (block ?b)
+                (block ?b1)
+                ; Arguments unique
+                (not (= ?b ?b1))
+
+                ; Preconditions
+                ;; (not (on-table ?b))
+
+            ]
+            ; TODO: Think hard about the effect
+            ;;   :effect (and (when (on ?b ?bl) 
+            ;;         (and (not (on ?b ?bl)) (on-table ?b) (clear ?bl)))))
+            :additions [
+                ; The following creates a contradiction because
+                ; (on-table ?b) -> (not (on ?b ?b1)) and
+                ; we can't have P -> \neg P
+                ;; (if (on ?b ?b1) (and (on-table ?b) (clear ?b1))) 
+
+            ]
+            :deletions [ ]
+        })
+
+        (define-action move-t-to-b [?bm ?bt ?t] {
+            :preconditions [
+                ; Type restrictions
+                (block ?bm)
+                (block ?bt)
+                ; Arguments unique
+                (not (= ?bm ?bt))
+                ; Primary preconditions
+                (clear ?bm ?t)
+                (clear ?bt ?t)
+                (on-table ?bm ?t)
+            ]
+            :additions [
+                (on ?bm ?bt (s ?t))
+
+                (not (clear ?bt (s ?t)))
+                (not (on-table ?bm (s ?t)))
+            ]
+            :deletions [
+                ;; (not (on ?bm ?bt))
+                
+                ;; (clear ?bt)
+                ;; (on-table ?bm)
+            ]
+        })
+    ]
+    :start [
+        ; Unknown facts don't need to be stated 
+        ; since we don't assume closed world assumption.
+
+        ; Negated predicates in this example is handled by
+        ; the block world axioms
+
+        (or
+            (and 
+                (on b2 b1 t0)
+                (clear b2 t0)
+                (on-table b1 t0)
+            )
+
+            (and
+                (on b1 b2 t0)
+                (clear b1 t0)
+                (on-table b2 t0)
+            )
+        )
+    ]
+    :goal [
+        (exists [x] (on b2 b1 x))
+    ]
+
+}

src/main/resources/org/rairlab/planner/problems/conformant/progression.clj

@@ -0,0 +1,81 @@
+; Original problem from Joerg Hoffmann and Ronen Brafman
+{:name "Block-Conformant-Tiny"
+    :background [
+        ; Setting object types
+        (Believes! a t0 (block b1))
+        (Believes! a t0 (block b2))
+
+        ; Unique name axioms
+        (Believes! a t0 (not (= b1 b2)))
+
+        ; Block World Axioms
+
+        ; Blocks are never on themselves
+        (Believes! a t0 (forall [x] (not (on x x))))
+        ; on is not symmetric
+        (Believes! a t0 (forall [x y] (if (on x y) (not (on y x)))))
+        ; Any block on a table isn't on top of another block
+        (Believes! a t0 (forall [x y] (if (on-table x) (not (on x y)))))
+        ; Any block that is cleared does not have another block on top of it
+        (Believes! a t0 (forall [x y] (if (clear x) (not (on y x)))))
+    ]
+
+
+    :actions [
+
+        (define-action move-t-to-b [?bm ?bt] {
+            :preconditions [
+                (Believes! a ?now (and
+                    ; Type Restrictions
+                    (block ?bm)
+                    (block ?bt)
+                    ; Arguments Unique
+                    (not (= ?bm ?bt))
+                    ; Primary preconditions
+                    (clear ?bm)
+                    (clear ?bt)
+                    (on-table ?bm)
+                ))
+                ; NOTE: QA Algorithm is very barebones,
+                ; currently does not support beliefs under
+                ; binary operations. Example:
+                ;; (and
+                ;;     (Believes! a t0 (block ?bm))
+                ;;     (Believes! a t0 (block ?bt))
+                ;; )
+            ]
+            :additions [
+                ; ShadowProver uses string comparisons to determine 
+                ; ordering on time points.
+                ; Spectra currently hacks around this by replacing
+                ; ?next where the constant
+                ; that represents ?now + 1.
+                ; ShadowProver Limitation: Cannot go beyond 10 time points
+                (Believes! a ?next (on ?bm ?bt))
+
+                ; These below shouldn't be needed but left for posterity
+                ;; (Believes! a ?next (not (clear ?bt)))
+                ;; (Believes! a ?next (not (on-table ?bm)))
+            ]
+            :deletions [ ]
+        })
+    ]
+    :start [
+        ; Unknown facts don't need to be stated 
+        ; since we don't assume closed world assumption.
+
+        ; Negated predicates in this example is handled by
+        ; the block world axioms
+
+        (Believes! a t0 (on-table b2))
+        (Believes! a t0 (on-table b1))
+        (Believes! a t0 (clear b1))
+        (Believes! a t0 (clear b2))
+    ]
+    :goal [
+        ;; (Believes! a t0 (clear ?bm))
+        ; Try a there exists at some point
+        (exists [t] (Believes! a t (on b1 b2)))
+    ]
+
+}