Adding a simplifier.

snark-20120808r02/snark-interface.lisp

@@ -90,14 +90,16 @@
 (defun setup-snark (&key (time-limit 5) (verbose nil))
   (snark:initialize :verbose  verbose)
   (if (not verbose) (snark-deverbose) )
-  (snark:run-time-limit 0.5)
+  (snark:run-time-limit 1)
   (snark:assert-supported t)
   (snark:assume-supported t)
   (snark:prove-supported t)
   (snark:use-hyperresolution t)
   (snark:use-paramodulation t)
-
+  (snark:use-term-ordering :recursive-path)
+  (snark:use-simplification-by-equalities t)
   (snark::declare-code-for-lists)
+
   (snark:allow-skolem-symbols-in-answers nil))
 
 (defun row-formula (name))

src/main/java/com/naveensundarg/planner/DepthFirstPlanner.java

@@ -19,7 +19,7 @@ import java.util.stream.Collectors;
 public class DepthFirstPlanner implements Planner {
 
 
-    private static  int MAX_DEPTH = 5;
+    private static  int MAX_DEPTH = 6;
     private static  boolean EXHAUSTIVE_TILL_MAX_DEPTH = false;
 
     private  boolean USE_METHODS, WORK_FROM_SCRATCH;
@@ -200,8 +200,11 @@ public class DepthFirstPlanner implements Planner {
 
             if(optPrecond.isPresent()){
 
-                current.addAll(additions);
+
+                current.removeAll(current.stream().filter(u-> deletions.stream().anyMatch(d-> Operations.equivalent(background, d, u))).collect(Collectors.toSet()));
                 current.removeAll(deletions);
+                current.addAll(additions.stream().map(Simplifier::simplify).collect(Collectors.toSet()));
+
                 expectedStates.add(State.initializeWith(current));
 
             } else {

src/main/java/com/naveensundarg/planner/Operations.java

@@ -241,7 +241,7 @@ public class Operations {
 
             Set<Formula> newFormulae = Sets.union(background, state.getFormulae());
 
-            newFormulae = Sets.union(newFormulae, action.instantiateAdditions(binding));
+            newFormulae = Sets.union(newFormulae, action.instantiateAdditions(binding).stream().map(Simplifier::simplify).collect(Collectors.toSet()));
 
 
             newFormulae = Sets.difference(newFormulae, formulaeToRemove);

src/main/java/com/naveensundarg/planner/Simplifier.java

@@ -0,0 +1,85 @@
+package com.naveensundarg.planner;
+
+import com.naveensundarg.shadow.prover.representations.formula.Formula;
+import com.naveensundarg.shadow.prover.representations.formula.Predicate;
+import com.naveensundarg.shadow.prover.representations.value.Compound;
+import com.naveensundarg.shadow.prover.representations.value.Constant;
+import com.naveensundarg.shadow.prover.representations.value.Value;
+
+import java.util.Arrays;
+import java.util.function.Function;
+
+public class Simplifier {
+
+
+    public static Formula simplify(Formula input){
+
+        if(input instanceof Predicate){
+
+            Value[] args = ((Predicate) input).getArguments();
+            Value[] outputArgs = new Value[args.length];
+
+            for(int i = 0; i < args.length; i++){
+
+                outputArgs[i] = simplify(args[i]);
+            }
+
+            return new Predicate(((Predicate) input).getName(), outputArgs);
+
+        }
+
+        return input;
+    }
+
+    public static Value simplify(Value input){
+
+
+        if(input instanceof Compound && input.getName().equals("remove")){
+
+
+            Value item = input.getArguments()[0];
+            Value list = input.getArguments()[1];
+
+
+
+            Value answer = removeFromCons(item, list);
+
+            return answer;
+
+
+
+        } else {
+
+            return input;
+        }
+
+    }
+
+    private static Value removeFromCons(Value item, Value list) {
+
+
+        if(list.equals(new Constant("el"))){
+
+            return new Constant("el");
+        }
+        else if (list instanceof Compound && list.getName().equals("cons")) {
+
+            if(list.getArguments()[0].equals(item)){
+
+                return removeFromCons(item, list.getArguments()[1]);
+
+            } else {
+
+
+                return new Compound("cons", new Value[]{list.getArguments()[0], removeFromCons(item, list.getArguments()[1])});
+
+            }
+        }
+
+        return list;
+
+
+    };
+
+
+}

src/main/java/com/naveensundarg/planner/utils/Sandbox.java

@@ -3,9 +3,13 @@ package com.naveensundarg.planner.utils;
 import com.naveensundarg.planner.DepthFirstPlanner;
 import com.naveensundarg.planner.PlanMethod;
 import com.naveensundarg.planner.Planner;
+import com.naveensundarg.planner.Simplifier;
+import com.naveensundarg.shadow.prover.representations.formula.Predicate;
 
 import java.util.List;
 
+import static com.naveensundarg.shadow.prover.utils.Reader.readFormulaFromString;
+
 /**
  * Created by naveensundarg on 12/22/17.
  */
@@ -42,19 +46,19 @@ public class Sandbox {
 
     public static void main(String[] args) throws com.naveensundarg.shadow.prover.utils.Reader.ParsingException {
 
-        List<PlanningProblem> planningProblemList = (PlanningProblem.readFromFile(Sandbox.class.getResourceAsStream("../problems/tora/attend.clj")));
+
+
+         List<PlanningProblem> planningProblemList = (PlanningProblem.readFromFile(Sandbox.class.getResourceAsStream("../problems/tora/attend.clj")));
 
         Planner depthFirstPlanner = new DepthFirstPlanner();
 
         PlanningProblem planningProblem = planningProblemList.stream().filter(problem -> problem.getName().equals("soda can challenge 2")).findFirst().get();
 
 
-        depthFirstPlanner.plan(planningProblem.getBackground(), planningProblem.getActions(), planningProblem.getStart(), planningProblem.getGoal()).ifPresent(
+        depthFirstPlanner.plan(planningProblem.getBackground(), planningProblem.getActions(), planningProblem.getStart(), planningProblem.getGoal()).ifPresent(plans-> {
-                y->{
 
-                    System.out.println(y);
+                    plans.stream().forEach(System.out::println);
-                }
+                });
-        );
 
 
 

src/main/resources/com/naveensundarg/planner/problems/tora/attend.clj

@@ -34,9 +34,8 @@
               (attend c)]
 
  :actions    [;; checkbehind an object
-               (define-action attend [?item]
+               (define-action attend [?item ?list]
-                 {:preconditions [(member ?item ?list)
+                 {:preconditions [(and (state ?list) (member ?item ?list))]
-                                  (state ?list)]
                   :additions     [(attend ?item)
                                   (state (remove ?item ?list))]
                   :deletions     [(state ?list)]})]}