This commit is contained in:
Naveen Sundar Govindarajulu 2018-06-01 13:43:49 -04:00
parent fc1cbfb5ab
commit 96688ccf2e
16 changed files with 290 additions and 34 deletions

4
learn.lisp Normal file
View file

@ -0,0 +1,4 @@
(defun
)

View file

@ -91,7 +91,7 @@
(snark:initialize :verbose verbose) (snark:initialize :verbose verbose)
(if (not verbose) (snark-deverbose) ) (if (not verbose) (snark-deverbose) )
(temp-sorts) (temp-sorts)
(snark:run-time-limit 0.5) (snark:run-time-limit 5)
(snark:assert-supported t) (snark:assert-supported t)
(snark:assume-supported t) (snark:assume-supported t)
(snark:prove-supported t) (snark:prove-supported t)

View file

@ -23,6 +23,7 @@ public class Action {
private final Set<Formula> additions; private final Set<Formula> additions;
private final Set<Formula> deletions; private final Set<Formula> deletions;
private final List<Variable> freeVariables; private final List<Variable> freeVariables;
private final List<Variable> interestedVars;
private final String name; private final String name;
private final Formula precondition; private final Formula precondition;
@ -32,7 +33,7 @@ public class Action {
private final Compound shorthand; private final Compound shorthand;
public Action(String name, Set<Formula> preconditions, Set<Formula> additions, Set<Formula> deletions, List<Variable> freeVariables) { public Action(String name, Set<Formula> preconditions, Set<Formula> additions, Set<Formula> deletions, List<Variable> freeVariables, List<Variable> interestedVars) {
this.name = name; this.name = name;
this.preconditions = preconditions; this.preconditions = preconditions;
@ -52,10 +53,11 @@ public class Action {
additions.stream().mapToInt(Formula::getWeight).sum() + additions.stream().mapToInt(Formula::getWeight).sum() +
deletions.stream().mapToInt(Formula::getWeight).sum(); deletions.stream().mapToInt(Formula::getWeight).sum();
List<Value> valuesList = freeVariables.stream().collect(Collectors.toList());; List<Value> valuesList = interestedVars.stream().collect(Collectors.toList());;
this.shorthand = new Compound(name, valuesList); this.shorthand = new Compound(name, valuesList);
this.trivial = computeTrivialOrNot(); this.trivial = computeTrivialOrNot();
this.interestedVars = interestedVars;
} }
public Action(String name, Set<Formula> preconditions, Set<Formula> additions, public Action(String name, Set<Formula> preconditions, Set<Formula> additions,
@ -83,6 +85,7 @@ public class Action {
this.shorthand = shorthand; this.shorthand = shorthand;
this.trivial = computeTrivialOrNot(); this.trivial = computeTrivialOrNot();
this.interestedVars = freeVariables;
} }
@ -93,7 +96,17 @@ public class Action {
Set<Formula> deletions, Set<Formula> deletions,
List<Variable> freeVariables) { List<Variable> 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<Formula> preconditions,
Set<Formula> additions,
Set<Formula> deletions,
List<Variable> freeVariables, List<Variable> interestedVars) {
return new Action(name, preconditions, additions, deletions, freeVariables, interestedVars);
} }
@ -148,7 +161,7 @@ public class Action {
} }
} }
List<Value> valuesList = freeVariables.stream().collect(Collectors.toList());; List<Value> valuesList = interestedVars.stream().collect(Collectors.toList());;
Compound shorthand = (Compound)(new Compound(name, valuesList)).apply(binding); Compound shorthand = (Compound)(new Compound(name, valuesList)).apply(binding);
return new Action(name, newPreconditions, newAdditions, newDeletions, newFreeVraibles, shorthand); return new Action(name, newPreconditions, newAdditions, newDeletions, newFreeVraibles, shorthand);
} }

View file

@ -20,7 +20,7 @@ public class DepthFirstPlanner implements Planner {
private static int MAX_DEPTH = 5; 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; private boolean USE_METHODS, WORK_FROM_SCRATCH;

View file

@ -10,6 +10,6 @@ import java.util.Set;
public class IndefiniteAction extends Action { public class IndefiniteAction extends Action {
private IndefiniteAction(String name, Set<Formula> preconditions, Set<Formula> additions, Set<Formula> deletions, List<Variable> freeVariables) { private IndefiniteAction(String name, Set<Formula> preconditions, Set<Formula> additions, Set<Formula> deletions, List<Variable> freeVariables) {
super(name, preconditions, additions, deletions, freeVariables); super(name, preconditions, additions, deletions, freeVariables, freeVariables);
} }
} }

View file

@ -312,7 +312,10 @@ public class PlanningProblem {
Set<Formula> additions = readFrom((List<?>) actionSpec.get(ADDITIONS)); Set<Formula> additions = readFrom((List<?>) actionSpec.get(ADDITIONS));
Set<Formula> deletions = readFrom((List<?>) actionSpec.get(DELETIONS)); Set<Formula> deletions = readFrom((List<?>) actionSpec.get(DELETIONS));
return Action.buildActionFrom(name, preconditions, additions, deletions, vars); List<Variable> 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) { } catch (Reader.ParsingException e) {

View file

@ -1,6 +1,8 @@
package com.naveensundarg.planner.utils; package com.naveensundarg.planner.utils;
import com.naveensundarg.planner.DepthFirstPlanner;
import com.naveensundarg.planner.PlanMethod; import com.naveensundarg.planner.PlanMethod;
import com.naveensundarg.planner.Planner;
import java.util.List; import java.util.List;
@ -9,9 +11,9 @@ import java.util.List;
*/ */
public class Sandbox { 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<GoalTrackingProblem> goalTrackingProblemList1 = (GoalTrackingProblem.readFromFile(Sandbox.class.getResourceAsStream("../problems/seriated/seriated_challenge_1.clj"))); List<GoalTrackingProblem> 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<PlanningProblem> 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
);
} }
} }

View file

@ -146,21 +146,21 @@
:start [] :start []
:goal [(Declaration god-exists)] :goal [(Declaration god-exists)]
:actions :actions
[(define-action declare-P [?p] [(define-action declare-P [?p]
{:preconditions [(Belief ?p)] {:preconditions [(Belief ?p)]
:additions [(Declaration ?p)] :additions [(Declaration ?p)]
:deletions [(Private ?p)]}) :deletions [(Private ?p)]})
(define-action believe-with-support [?p] (define-action believe-with-support [?p]
{:preconditions [(Proposition ?p) {:preconditions [(Proposition ?p)
(HasSupport ?p)] (HasSupport ?p)]
:additions [(Belief ?p)] :additions [(Belief ?p)]
:deletions []}) :deletions []})
(define-action believe-without-support [?p] (define-action believe-without-support [?p]
{:preconditions [(Proposition ?p)] {:preconditions [(Proposition ?p)]
:additions [(Belief ?p)] :additions [(Belief ?p)]
:deletions []})] :deletions []})]
:expected-plans ([believe-P declare-P])} :expected-plans ([believe-P declare-P])}
@ -200,24 +200,24 @@
{:name "reasoning 3" {:name "reasoning 3"
:background [] :background []
:start [(! A) (! B) :start [(! A) (! B)
(Prop S) (Prop S)
(! (if (and A B) C)) (! (if (and A B) C))
] ]
:goal [(! (if S C) )] :goal [(! (if S C))]
:actions [(define-action and-intro [?p ?q] :actions [(define-action and-intro [?p ?q]
{:preconditions [(! ?p) (! ?q)] {:preconditions [(! ?p) (! ?q)]
:additions [(! (and ?p ?q))] :additions [(! (and ?p ?q))]
:deletions []}) :deletions []})
(define-action cond-elim [?p ?q] (define-action cond-elim [?p ?q]
{:preconditions [(! (if ?p ?q)) (! ?p)] {:preconditions [(! (if ?p ?q)) (! ?p)]
:additions [(! ?q)] :additions [(! ?q)]
:deletions []}) :deletions []})
(define-action cond-intro [?p ?q] (define-action cond-intro [?p ?q]
{:preconditions [ (Prop ?p) (! ?q)] {:preconditions [(Prop ?p) (! ?q)]
:additions [(! (if ?p ?q))] :additions [(! (if ?p ?q))]
:deletions []})] :deletions []})]
:expected-plans ([and-intro])} :expected-plans ([and-intro])}

View file

@ -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]
}

View file

@ -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)]
}

View file

@ -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)]
}

View file

@ -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)]
}

View file

@ -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)]
}

View file

@ -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)]
}

View file

@ -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))]
}

View file

@ -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)]}