From 32e7a8fe4c354dc08da9546b330e227f46895865 Mon Sep 17 00:00:00 2001 From: Naveen Sundar Govindarajulu Date: Mon, 18 Jun 2018 18:29:40 -0700 Subject: [PATCH] TORA example --- .gitignore | 1 + snark-20120808r02/snark-interface.lisp | 8 ++-- .../com/naveensundarg/planner/Action.java | 9 +++- .../naveensundarg/planner/utils/Sandbox.java | 9 ++-- .../planner/problems/tora/attend.clj | 42 +++++++++++++++++++ .../planner/problems/tora/trial2.clj | 27 ++++++++++++ 6 files changed, 88 insertions(+), 8 deletions(-) create mode 100644 src/main/resources/com/naveensundarg/planner/problems/tora/attend.clj create mode 100644 src/main/resources/com/naveensundarg/planner/problems/tora/trial2.clj diff --git a/.gitignore b/.gitignore index f9a7b09..f565ff0 100644 --- a/.gitignore +++ b/.gitignore @@ -23,3 +23,4 @@ planner.iml .idea/libraries/Maven__us_bpsm_edn_java_0_5_0.xml target/* +*.fasl diff --git a/snark-20120808r02/snark-interface.lisp b/snark-20120808r02/snark-interface.lisp index ad9c54c..853d2c7 100644 --- a/snark-20120808r02/snark-interface.lisp +++ b/snark-20120808r02/snark-interface.lisp @@ -90,15 +90,15 @@ (defun setup-snark (&key (time-limit 5) (verbose nil)) (snark:initialize :verbose verbose) (if (not verbose) (snark-deverbose) ) - (temp-sorts) - (snark:run-time-limit 5) + (snark:run-time-limit 0.5) (snark:assert-supported t) (snark:assume-supported t) (snark:prove-supported t) - (snark:use-resolution t) + (snark:use-hyperresolution t) (snark:use-paramodulation t) - (snark:allow-skolem-symbols-in-answers 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/Action.java b/src/main/java/com/naveensundarg/planner/Action.java index cc61173..4aab872 100644 --- a/src/main/java/com/naveensundarg/planner/Action.java +++ b/src/main/java/com/naveensundarg/planner/Action.java @@ -132,7 +132,14 @@ public class Action { public List openVars() { - return freeVariables; + Set variables = Sets.newSet(); + + variables.addAll(freeVariables); + + List variablesList = CollectionUtils.newEmptyList(); + + variablesList.addAll(variables); + return variablesList; } diff --git a/src/main/java/com/naveensundarg/planner/utils/Sandbox.java b/src/main/java/com/naveensundarg/planner/utils/Sandbox.java index 568a49b..1d96500 100644 --- a/src/main/java/com/naveensundarg/planner/utils/Sandbox.java +++ b/src/main/java/com/naveensundarg/planner/utils/Sandbox.java @@ -42,15 +42,18 @@ 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/sodacan.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")).findFirst().get(); + 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( - System.out::println + y->{ + + System.out.println(y); + } ); diff --git a/src/main/resources/com/naveensundarg/planner/problems/tora/attend.clj b/src/main/resources/com/naveensundarg/planner/problems/tora/attend.clj new file mode 100644 index 0000000..46bfe06 --- /dev/null +++ b/src/main/resources/com/naveensundarg/planner/problems/tora/attend.clj @@ -0,0 +1,42 @@ +{:name "soda can challenge 2" + :background [ ;; Membership in a list + (forall [?u ?l] + (iff (member ?u ?l) + (exists [?v ?rest] + (and (= ?l (cons ?v ?rest)) + (or (= ?u ?v) + (member ?u ?rest)))))) + ;; Empty list + (forall ?x (not (member ?x el))) + ;; Removal clause 1 + (forall [?item] (= (remove ?item el) el)) + ;; Removal clause 2 + (forall [?item ?rest] + (= (remove ?item (cons ?item ?rest)) + (remove ?item ?rest))) + ;; Remove clause 3 + (forall [?item ?head ?rest] + (if + (not (= ?head ?item)) + (= (remove ?item (cons ?head ?rest)) + (cons ?head (remove ?item ?rest)))))] + + :start [(state (cons a (cons b (cons c el)))) + (and (not (= a b)) + (not (= b c)) + (not (= c a)) + (not (= a el)) + (not (= b el)) + (not (= c el)))] + + :goal [(attend a) + (attend b) + (attend c)] + + :actions [;; checkbehind an object + (define-action attend [?item] + {:preconditions [(member ?item ?list) + (state ?list)] + :additions [(attend ?item) + (state (remove ?item ?list))] + :deletions [(state ?list)]})]} diff --git a/src/main/resources/com/naveensundarg/planner/problems/tora/trial2.clj b/src/main/resources/com/naveensundarg/planner/problems/tora/trial2.clj new file mode 100644 index 0000000..d6cbfe2 --- /dev/null +++ b/src/main/resources/com/naveensundarg/planner/problems/tora/trial2.clj @@ -0,0 +1,27 @@ +{:name "soda can challenge 2" + :background [;; Checks if something is an element of a list + (forall [?thing ?w ?list] (iff (Elem ?thing ?list) (Elem ?thing (Cons ?w ?list)))) + (forall [?thing] (Elem ?thing (Cons ?thing el))) + ;; Removes an element from a list + (forall [?u ?l1 ?l2] + (if + (and + (not (Elem ?u ?l2)) + (forall [?x] + (if + (Elem ?x ?l1) + (or (= ?x ?u) (Elem ?x ?l2))))) + (Removed ?u ?l1 ?l2)))] + + :start [(Cons a (Cons b (Cons f el)))] + + :goal [(Cons a el) + (Cons b el) + (Cons f el)] + + :actions [;; Checkbehind an object + (define-action attend [?q ?l] + {:preconditions [(Elem ?q ?l) + (Removed ?q ?l ?l2)] + :additions [(Cons ?q el)] + :deletions []})]}