From 839b3e3172c3c44e17070fa75184f1a822ff155f Mon Sep 17 00:00:00 2001 From: Naveen Sundar Govindarajulu Date: Mon, 18 Jun 2018 22:05:40 -0700 Subject: [PATCH] Adding a simplifier. --- snark-20120808r02/snark-interface.lisp | 6 +- .../planner/DepthFirstPlanner.java | 7 +- .../com/naveensundarg/planner/Operations.java | 2 +- .../com/naveensundarg/planner/Simplifier.java | 85 +++++++++++++++++++ .../naveensundarg/planner/utils/Sandbox.java | 16 ++-- .../planner/problems/tora/attend.clj | 5 +- 6 files changed, 107 insertions(+), 14 deletions(-) create mode 100644 src/main/java/com/naveensundarg/planner/Simplifier.java diff --git a/snark-20120808r02/snark-interface.lisp b/snark-20120808r02/snark-interface.lisp index 853d2c7..f22da0c 100644 --- a/snark-20120808r02/snark-interface.lisp +++ b/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)) diff --git a/src/main/java/com/naveensundarg/planner/DepthFirstPlanner.java b/src/main/java/com/naveensundarg/planner/DepthFirstPlanner.java index 53f5fe5..d8a7d81 100644 --- a/src/main/java/com/naveensundarg/planner/DepthFirstPlanner.java +++ b/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 { diff --git a/src/main/java/com/naveensundarg/planner/Operations.java b/src/main/java/com/naveensundarg/planner/Operations.java index fa47ea2..06d03db 100644 --- a/src/main/java/com/naveensundarg/planner/Operations.java +++ b/src/main/java/com/naveensundarg/planner/Operations.java @@ -241,7 +241,7 @@ public class Operations { Set 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); diff --git a/src/main/java/com/naveensundarg/planner/Simplifier.java b/src/main/java/com/naveensundarg/planner/Simplifier.java new file mode 100644 index 0000000..cd221dd --- /dev/null +++ b/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; + + + }; + + +} diff --git a/src/main/java/com/naveensundarg/planner/utils/Sandbox.java b/src/main/java/com/naveensundarg/planner/utils/Sandbox.java index 1d96500..cf611aa 100644 --- a/src/main/java/com/naveensundarg/planner/utils/Sandbox.java +++ b/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 planningProblemList = (PlanningProblem.readFromFile(Sandbox.class.getResourceAsStream("../problems/tora/attend.clj"))); + + + List 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( - y->{ + depthFirstPlanner.plan(planningProblem.getBackground(), planningProblem.getActions(), planningProblem.getStart(), planningProblem.getGoal()).ifPresent(plans-> { - System.out.println(y); - } - ); + plans.stream().forEach(System.out::println); + }); diff --git a/src/main/resources/com/naveensundarg/planner/problems/tora/attend.clj b/src/main/resources/com/naveensundarg/planner/problems/tora/attend.clj index 46bfe06..4305641 100644 --- a/src/main/resources/com/naveensundarg/planner/problems/tora/attend.clj +++ b/src/main/resources/com/naveensundarg/planner/problems/tora/attend.clj @@ -34,9 +34,8 @@ (attend c)] :actions [;; checkbehind an object - (define-action attend [?item] - {:preconditions [(member ?item ?list) - (state ?list)] + (define-action attend [?item ?list] + {:preconditions [(and (state ?list) (member ?item ?list))] :additions [(attend ?item) (state (remove ?item ?list))] :deletions [(state ?list)]})]}