diff --git a/learn.lisp b/learn.lisp new file mode 100644 index 0000000..aa4feaa --- /dev/null +++ b/learn.lisp @@ -0,0 +1,4 @@ + +(defun + + ) diff --git a/snark-20120808r02/snark-interface.lisp b/snark-20120808r02/snark-interface.lisp index 649ab1c..ad9c54c 100644 --- a/snark-20120808r02/snark-interface.lisp +++ b/snark-20120808r02/snark-interface.lisp @@ -91,7 +91,7 @@ (snark:initialize :verbose verbose) (if (not verbose) (snark-deverbose) ) (temp-sorts) - (snark:run-time-limit 0.5) + (snark:run-time-limit 5) (snark:assert-supported t) (snark:assume-supported t) (snark:prove-supported t) diff --git a/src/main/java/com/naveensundarg/planner/Action.java b/src/main/java/com/naveensundarg/planner/Action.java index aa3dbbc..cc61173 100644 --- a/src/main/java/com/naveensundarg/planner/Action.java +++ b/src/main/java/com/naveensundarg/planner/Action.java @@ -23,6 +23,7 @@ public class Action { private final Set additions; private final Set deletions; private final List freeVariables; + private final List interestedVars; private final String name; private final Formula precondition; @@ -32,7 +33,7 @@ public class Action { private final Compound shorthand; - public Action(String name, Set preconditions, Set additions, Set deletions, List freeVariables) { + public Action(String name, Set preconditions, Set additions, Set deletions, List freeVariables, List interestedVars) { this.name = name; this.preconditions = preconditions; @@ -52,10 +53,11 @@ public class Action { additions.stream().mapToInt(Formula::getWeight).sum() + deletions.stream().mapToInt(Formula::getWeight).sum(); - List valuesList = freeVariables.stream().collect(Collectors.toList());; + List valuesList = interestedVars.stream().collect(Collectors.toList());; this.shorthand = new Compound(name, valuesList); this.trivial = computeTrivialOrNot(); + this.interestedVars = interestedVars; } public Action(String name, Set preconditions, Set additions, @@ -83,6 +85,7 @@ public class Action { this.shorthand = shorthand; this.trivial = computeTrivialOrNot(); + this.interestedVars = freeVariables; } @@ -93,7 +96,17 @@ public class Action { Set deletions, List freeVariables) { - return new Action(name, preconditions, additions, deletions, freeVariables); + return new Action(name, preconditions, additions, deletions, freeVariables, freeVariables); + + } + + public static Action buildActionFrom(String name, + Set preconditions, + Set additions, + Set deletions, + List freeVariables, List interestedVars) { + + return new Action(name, preconditions, additions, deletions, freeVariables, interestedVars); } @@ -148,7 +161,7 @@ public class Action { } } - List valuesList = freeVariables.stream().collect(Collectors.toList());; + List valuesList = interestedVars.stream().collect(Collectors.toList());; Compound shorthand = (Compound)(new Compound(name, valuesList)).apply(binding); return new Action(name, newPreconditions, newAdditions, newDeletions, newFreeVraibles, shorthand); } diff --git a/src/main/java/com/naveensundarg/planner/DepthFirstPlanner.java b/src/main/java/com/naveensundarg/planner/DepthFirstPlanner.java index bdd9258..53f5fe5 100644 --- a/src/main/java/com/naveensundarg/planner/DepthFirstPlanner.java +++ b/src/main/java/com/naveensundarg/planner/DepthFirstPlanner.java @@ -20,7 +20,7 @@ public class DepthFirstPlanner implements Planner { private static int MAX_DEPTH = 5; - private static boolean EXHAUSTIVE_TILL_MAX_DEPTH = true; + private static boolean EXHAUSTIVE_TILL_MAX_DEPTH = false; private boolean USE_METHODS, WORK_FROM_SCRATCH; diff --git a/src/main/java/com/naveensundarg/planner/utils/IndefiniteAction.java b/src/main/java/com/naveensundarg/planner/utils/IndefiniteAction.java index 82aed3d..d2087d2 100644 --- a/src/main/java/com/naveensundarg/planner/utils/IndefiniteAction.java +++ b/src/main/java/com/naveensundarg/planner/utils/IndefiniteAction.java @@ -10,6 +10,6 @@ import java.util.Set; public class IndefiniteAction extends Action { private IndefiniteAction(String name, Set preconditions, Set additions, Set deletions, List freeVariables) { - super(name, preconditions, additions, deletions, freeVariables); + super(name, preconditions, additions, deletions, freeVariables, freeVariables); } } diff --git a/src/main/java/com/naveensundarg/planner/utils/PlanningProblem.java b/src/main/java/com/naveensundarg/planner/utils/PlanningProblem.java index d29ad22..9f472b3 100644 --- a/src/main/java/com/naveensundarg/planner/utils/PlanningProblem.java +++ b/src/main/java/com/naveensundarg/planner/utils/PlanningProblem.java @@ -312,7 +312,10 @@ public class PlanningProblem { Set additions = readFrom((List) actionSpec.get(ADDITIONS)); Set deletions = readFrom((List) actionSpec.get(DELETIONS)); - return Action.buildActionFrom(name, preconditions, additions, deletions, vars); + List interestedVars = CollectionUtils.newEmptyList(); + interestedVars.addAll(vars); + vars.addAll(preconditions.stream().map(Formula::variablesPresent).reduce(Sets.newSet(), Sets::union)); + return Action.buildActionFrom(name, preconditions, additions, deletions, vars, interestedVars); } catch (Reader.ParsingException e) { diff --git a/src/main/java/com/naveensundarg/planner/utils/Sandbox.java b/src/main/java/com/naveensundarg/planner/utils/Sandbox.java index f7d1bfb..5cf4d1f 100644 --- a/src/main/java/com/naveensundarg/planner/utils/Sandbox.java +++ b/src/main/java/com/naveensundarg/planner/utils/Sandbox.java @@ -1,6 +1,8 @@ package com.naveensundarg.planner.utils; +import com.naveensundarg.planner.DepthFirstPlanner; import com.naveensundarg.planner.PlanMethod; +import com.naveensundarg.planner.Planner; import java.util.List; @@ -9,9 +11,9 @@ import java.util.List; */ public class Sandbox { - public static void main(String[] args) throws com.naveensundarg.shadow.prover.utils.Reader.ParsingException { + public static void demoPlanMethods(String[] args) throws com.naveensundarg.shadow.prover.utils.Reader.ParsingException { - PlanMethod seriatedPlanMethod = (Reader.readPlanMethodsFrom(Sandbox.class.getResourceAsStream("../problems/seriated/methods.clj"))).get(0); + PlanMethod seriatedPlanMethod = (Reader.readPlanMethodsFrom(Sandbox.class.getResourceAsStream("../problems/learning/dry.clj"))).get(0); List goalTrackingProblemList1 = (GoalTrackingProblem.readFromFile(Sandbox.class.getResourceAsStream("../problems/seriated/seriated_challenge_1.clj"))); @@ -36,5 +38,22 @@ 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/learning/reasoning_5.clj"))); + + Planner depthFirstPlanner = new DepthFirstPlanner(); + + PlanningProblem planningProblem = planningProblemList.stream().filter(problem -> problem.getName().equals("learning")).findFirst().get(); + + + depthFirstPlanner.plan(planningProblem.getBackground(), planningProblem.getActions(), planningProblem.getStart(), planningProblem.getGoal()).ifPresent( + System.out::println + ); + + + } } diff --git a/src/main/resources/com/naveensundarg/planner/completeness_problems.clj b/src/main/resources/com/naveensundarg/planner/completeness_problems.clj index 36724b3..b76840c 100644 --- a/src/main/resources/com/naveensundarg/planner/completeness_problems.clj +++ b/src/main/resources/com/naveensundarg/planner/completeness_problems.clj @@ -146,21 +146,21 @@ :start [] :goal [(Declaration god-exists)] :actions - [(define-action declare-P [?p] - {:preconditions [(Belief ?p)] - :additions [(Declaration ?p)] - :deletions [(Private ?p)]}) + [(define-action declare-P [?p] + {:preconditions [(Belief ?p)] + :additions [(Declaration ?p)] + :deletions [(Private ?p)]}) - (define-action believe-with-support [?p] - {:preconditions [(Proposition ?p) - (HasSupport ?p)] - :additions [(Belief ?p)] - :deletions []}) + (define-action believe-with-support [?p] + {:preconditions [(Proposition ?p) + (HasSupport ?p)] + :additions [(Belief ?p)] + :deletions []}) - (define-action believe-without-support [?p] - {:preconditions [(Proposition ?p)] - :additions [(Belief ?p)] - :deletions []})] + (define-action believe-without-support [?p] + {:preconditions [(Proposition ?p)] + :additions [(Belief ?p)] + :deletions []})] :expected-plans ([believe-P declare-P])} @@ -200,24 +200,24 @@ {:name "reasoning 3" :background [] - :start [(! A) (! B) + :start [(! A) (! B) (Prop S) (! (if (and A B) C)) ] - :goal [(! (if S C) )] + :goal [(! (if S C))] :actions [(define-action and-intro [?p ?q] - {:preconditions [(! ?p) (! ?q)] - :additions [(! (and ?p ?q))] - :deletions []}) + {:preconditions [(! ?p) (! ?q)] + :additions [(! (and ?p ?q))] + :deletions []}) (define-action cond-elim [?p ?q] - {:preconditions [(! (if ?p ?q)) (! ?p)] - :additions [(! ?q)] - :deletions []}) + {:preconditions [(! (if ?p ?q)) (! ?p)] + :additions [(! ?q)] + :deletions []}) (define-action cond-intro [?p ?q] - {:preconditions [ (Prop ?p) (! ?q)] - :additions [(! (if ?p ?q))] - :deletions []})] + {:preconditions [(Prop ?p) (! ?q)] + :additions [(! (if ?p ?q))] + :deletions []})] :expected-plans ([and-intro])} diff --git a/src/main/resources/com/naveensundarg/planner/problems/learning/dry.clj b/src/main/resources/com/naveensundarg/planner/problems/learning/dry.clj new file mode 100644 index 0000000..58ecb33 --- /dev/null +++ b/src/main/resources/com/naveensundarg/planner/problems/learning/dry.clj @@ -0,0 +1,37 @@ +{:name "learning" + :background [(iff dry (not wet)) + (iff umbrella (not coat)) + + + (if was-outside (if (and rain (not umbrella)) wet)) + (if was-outside (if (and snow (not coat)) wet))] + :start [ rain + (at a) + (available b) + ] + + :actions [(define-action walkFromTo [?start ?end] + {:preconditions [(at ?start) + (available ?end) + ] + :additions [(at ?end) + was-outside] + :deletions [(at ?start)]}) + + (define-action useUmbrella [] + {:preconditions [rain] + :additions [umbrella] + :deletions [(not umbrella)]}) + + + (define-action useCoat [] + {:preconditions [snow] + :additions [coat] + :deletions [(not coat)]}) + + ] + + + :goal [(at b) + dry] + } \ No newline at end of file diff --git a/src/main/resources/com/naveensundarg/planner/problems/learning/reasoning_1.clj b/src/main/resources/com/naveensundarg/planner/problems/learning/reasoning_1.clj new file mode 100644 index 0000000..73607a1 --- /dev/null +++ b/src/main/resources/com/naveensundarg/planner/problems/learning/reasoning_1.clj @@ -0,0 +1,21 @@ +{:name "learning" + :background [] + :start [(holds c1 a null)] + + :actions [(define-action resolve [?c1 ?c2] + {:preconditions [(holds ?c1 ?u null) + (holds ?c2 (not ?u) ?w)] + :additions [(holds (comb ?c1 ?c2) null ?w)] + :deletions []}) + + + (define-action resolve [?c1 ?c2] + {:preconditions [(holds ?c1 null ?u ) + (holds ?c2 ?w (not ?u) )] + :additions [(holds (comb ?c1 ?c2) ?w null)] + :deletions []}) + ] + + + :goal [(holds ?id null null)] + } \ No newline at end of file diff --git a/src/main/resources/com/naveensundarg/planner/problems/learning/reasoning_2.clj b/src/main/resources/com/naveensundarg/planner/problems/learning/reasoning_2.clj new file mode 100644 index 0000000..77f64da --- /dev/null +++ b/src/main/resources/com/naveensundarg/planner/problems/learning/reasoning_2.clj @@ -0,0 +1,25 @@ +{:name "learning" + :background [] + + + + :start [(holds c1 a null) + (holds c2 (not a) null)] + + :actions [(define-action resolve [?c1 ?c2] + {:preconditions [(holds ?c1 ?u null) + (holds ?c2 (not ?u) ?w)] + :additions [(holds (comb ?c1 ?c2) null ?w)] + :deletions []}) + + + (define-action resolve [?c1 ?c2] + {:preconditions [(holds ?c1 null ?u ) + (holds ?c2 ?w (not ?u) )] + :additions [(holds (comb ?c1 ?c2) ?w null)] + :deletions []}) + ] + + + :goal [(holds ?id null null)] + } \ No newline at end of file diff --git a/src/main/resources/com/naveensundarg/planner/problems/learning/reasoning_3.clj b/src/main/resources/com/naveensundarg/planner/problems/learning/reasoning_3.clj new file mode 100644 index 0000000..cc9a51b --- /dev/null +++ b/src/main/resources/com/naveensundarg/planner/problems/learning/reasoning_3.clj @@ -0,0 +1,25 @@ +{:name "learning" + :background [] + :start [(holds c1 a null) + (holds c2 (not a) b) + (holds c3 c (not b)) + (holds c3 (not c) null) + ] + + :actions [(define-action resolve [?c1 ?c2] + {:preconditions [(holds ?c1 ?u null) + (holds ?c2 (not ?u) ?w)] + :additions [(holds (comb ?c1 ?c2) null ?w)] + :deletions []}) + + + (define-action resolve [?c1 ?c2] + {:preconditions [(holds ?c1 null ?u ) + (holds ?c2 ?w (not ?u) )] + :additions [(holds (comb ?c1 ?c2) ?w null)] + :deletions []}) + ] + + + :goal [(holds ?id null null)] + } \ No newline at end of file diff --git a/src/main/resources/com/naveensundarg/planner/problems/learning/reasoning_4.clj b/src/main/resources/com/naveensundarg/planner/problems/learning/reasoning_4.clj new file mode 100644 index 0000000..cc9a51b --- /dev/null +++ b/src/main/resources/com/naveensundarg/planner/problems/learning/reasoning_4.clj @@ -0,0 +1,25 @@ +{:name "learning" + :background [] + :start [(holds c1 a null) + (holds c2 (not a) b) + (holds c3 c (not b)) + (holds c3 (not c) null) + ] + + :actions [(define-action resolve [?c1 ?c2] + {:preconditions [(holds ?c1 ?u null) + (holds ?c2 (not ?u) ?w)] + :additions [(holds (comb ?c1 ?c2) null ?w)] + :deletions []}) + + + (define-action resolve [?c1 ?c2] + {:preconditions [(holds ?c1 null ?u ) + (holds ?c2 ?w (not ?u) )] + :additions [(holds (comb ?c1 ?c2) ?w null)] + :deletions []}) + ] + + + :goal [(holds ?id null null)] + } \ No newline at end of file diff --git a/src/main/resources/com/naveensundarg/planner/problems/learning/reasoning_5.clj b/src/main/resources/com/naveensundarg/planner/problems/learning/reasoning_5.clj new file mode 100644 index 0000000..68792d5 --- /dev/null +++ b/src/main/resources/com/naveensundarg/planner/problems/learning/reasoning_5.clj @@ -0,0 +1,35 @@ + + + +{:name "learning" + :background [] + + + :start [(holds c1 a null) + (holds c2 (not a) b) + (holds c3 c (not b)) + (holds c3 (not c) d ) + (holds c4 null (not d))] + + + + :actions [(define-action resolve [?c1 ?c2] + {:preconditions [(holds ?c1 ?u null) + (holds ?c2 (not ?u) ?w)] + :additions [(holds (comb ?c1 ?c2) null ?w)] + :deletions []}) + + + (define-action resolve [?c1 ?c2] + {:preconditions [(holds ?c1 null ?u ) + (holds ?c2 ?w (not ?u) )] + :additions [(holds (comb ?c1 ?c2) ?w null)] + :deletions []}) + ] + + + :goal [(holds ?id null null)] + } + + + diff --git a/src/main/resources/com/naveensundarg/planner/problems/learning/reasoningdiff.clj b/src/main/resources/com/naveensundarg/planner/problems/learning/reasoningdiff.clj new file mode 100644 index 0000000..2d2114b --- /dev/null +++ b/src/main/resources/com/naveensundarg/planner/problems/learning/reasoningdiff.clj @@ -0,0 +1,25 @@ +{:name "learning" + :background [] + :start [(= c1 (clause a null)) + (= c2 (clause (not a) b)) + (= c3 (clause c (not b))) + (= c3 (clause (not c) null)) + ] + + :actions [(define-action resolve1a [?c1 ?c2 ?u ?w] + {:preconditions [(= ?c1 (clause ?u null)) + (= ?c2 (clause (not ?u) ?w))] + :additions [(= (comb ?c1 ?c2) (clause null ?w))] + :deletions []}) + + + (define-action resolve1b [?c1 ?c2 ?u ?w] + {:preconditions [(= ?c1 (clause null ?u) ) + (= ?c2 (clause ?w (not ?u)) )] + :additions [(= (comb ?c1 ?c2) (clause ?w null))] + :deletions []}) + ] + + + :goal [(= ?id (clause null null))] + } diff --git a/src/main/resources/com/naveensundarg/planner/problems/learning/restaurant.clj b/src/main/resources/com/naveensundarg/planner/problems/learning/restaurant.clj new file mode 100644 index 0000000..83c0b0f --- /dev/null +++ b/src/main/resources/com/naveensundarg/planner/problems/learning/restaurant.clj @@ -0,0 +1,24 @@ + + +{:name "toy restaurant example" + :background [ ] + :start [(Believes I (Believes other (= ?something (phone R))))] + + :actions [(define-action call [?entity] + {:preconditions [(Believes I (= ?num (phone ?entity)))] + :additions [(called ?entity)] + :deletions [(not (called ?entity))]}) + + (define-action query [?value] + {:preconditions [(Believes I (Believes ?other (= ?something ?value)))] + :additions [(Believes I (= ?something ?value))] + :deletions [(not (Believes I (= ?something ?value)))]})] + + + :goal [(called ?establishment)]} + + + + + +