From 381bbc60afdb375a48f8da02cf59990433ea4412 Mon Sep 17 00:00:00 2001 From: Naveen Sundar Govindarajulu Date: Sat, 10 Jun 2017 22:44:47 -0700 Subject: [PATCH] Solving a seriated cup challenge. --- snark-20120808r02/commons.lisp | 0 snark-20120808r02/snark-interface.lisp | 61 +++++++- .../java/edu/rpi/rair/DepthFirstPlanner.java | 2 +- src/main/java/edu/rpi/rair/Operations.java | 54 ++++++- .../rpi/rair/utils/ProceduralAttachment.java | 14 ++ src/main/java/edu/rpi/rair/utils/RunDemo.java | 42 +++++- .../edu/rpi/rair/goal_management_1.clj | 132 +++++++++--------- .../edu/rpi/rair/goal_management_6.clj | 24 +--- .../edu/rpi/rair/seriated_challenge_1.clj | 60 ++++++++ .../java/edu/rpi/rair/GoalTrackerTest.java | 13 ++ 10 files changed, 305 insertions(+), 97 deletions(-) create mode 100644 snark-20120808r02/commons.lisp create mode 100644 src/main/java/edu/rpi/rair/utils/ProceduralAttachment.java create mode 100644 src/main/resources/edu/rpi/rair/seriated_challenge_1.clj diff --git a/snark-20120808r02/commons.lisp b/snark-20120808r02/commons.lisp new file mode 100644 index 0000000..e69de29 diff --git a/snark-20120808r02/snark-interface.lisp b/snark-20120808r02/snark-interface.lisp index e987a27..6ce2e97 100644 --- a/snark-20120808r02/snark-interface.lisp +++ b/snark-20120808r02/snark-interface.lisp @@ -16,6 +16,62 @@ (snark:print-rows-prettily nil) (snark:print-rows :min 0 :max 0)) + +(defun temp-sorts () + (snark:declare-sort 'Room) + (snark:declare-sort 'Door) + (snark:declare-sort 'Agent) + (snark:declare-sort 'Name) + + + (snark:declare-subsort 'Robot 'Agent :subsorts-incompatible t) + (snark:declare-subsort 'Person 'Agent :subsorts-incompatible t) + (snark:declare-subsort 'Commander 'Person :subsorts-incompatible t) + (snark:declare-subsort 'Prisoner 'Person :subsorts-incompatible t) + + (snark:declare-constant 'guard :sort 'Robot) + (snark:declare-constant 'guide :sort 'Robot) + (snark:declare-constant 'commander :sort 'Commander) + (snark:declare-constant 'prisoner :sort 'Prisoner) + + (snark:declare-constant 'room1 :sort 'Room) + (snark:declare-constant 'room2 :sort 'Room) + (snark:declare-constant 'hallway :sort 'Room) + (snark:declare-constant 'accompany :sort 'Name) + + (snark:declare-function 'door 1 :sort '(Door Room)) + + (snark:declare-relation 'robot 1 :sort '(Robot)) + (snark:declare-relation 'room 1 :sort '(Room)) + (snark:declare-relation 'person 1 :sort '(Person)) + (snark:declare-relation 'commander 1 :sort '(Commander)) + (snark:declare-relation 'prisoner 1 :sort '(Prisoner)) + + (snark:declare-relation 'in 2 :sort '(Agent Room)) + (snark:declare-relation 'sameroom 2 :sort '(Agent Agent)) + + (snark:declare-relation 'interrogate 2 :sort '(Agent Agent)) + + (snark:declare-relation 'can 4 :sort '(Name Agent Agent Agent)) + + + (snark:declare-relation 'accompanies 2 :sort '(Agent Agent)) + (snark:declare-relation 'open 1 :sort '(Door)) + + + (snark:declare-variable '?room :sort 'Room) + (snark:declare-variable '?room1 :sort 'Room) + (snark:declare-variable '?room2 :sort 'Room) + + (snark:declare-variable '?person :sort 'Person) + (snark:declare-variable '?person1 :sort 'Person) + (snark:declare-variable '?person2 :sort 'Person) + + (snark:declare-variable '?actor :sort 'Agent) + + + + ) (defun snark-deverbose () (snark:print-options-when-starting nil) (snark:print-agenda-when-finished nil) @@ -34,11 +90,12 @@ (defun setup-snark (&key (time-limit 5) (verbose nil)) (snark:initialize :verbose verbose) (if (not verbose) (snark-deverbose) ) - (snark:run-time-limit time-limit) + (temp-sorts) + (snark:run-time-limit 0.05) (snark:assert-supported t) (snark:assume-supported t) (snark:prove-supported t) - (snark:use-hyperresolution t) + (snark:use-resolution t) (snark:use-paramodulation t) (snark:allow-skolem-symbols-in-answers t)) diff --git a/src/main/java/edu/rpi/rair/DepthFirstPlanner.java b/src/main/java/edu/rpi/rair/DepthFirstPlanner.java index 3549a90..5054f24 100644 --- a/src/main/java/edu/rpi/rair/DepthFirstPlanner.java +++ b/src/main/java/edu/rpi/rair/DepthFirstPlanner.java @@ -13,7 +13,7 @@ import java.util.stream.Collectors; public class DepthFirstPlanner implements Planner { - private static int MAX_DEPTH = 5; + private static int MAX_DEPTH = 4; private static boolean EXHAUSTIVE_TILL_MAX_DEPTH = false; public static int getMaxDepth() { diff --git a/src/main/java/edu/rpi/rair/Operations.java b/src/main/java/edu/rpi/rair/Operations.java index 517c07a..e6bc989 100644 --- a/src/main/java/edu/rpi/rair/Operations.java +++ b/src/main/java/edu/rpi/rair/Operations.java @@ -3,8 +3,10 @@ package edu.rpi.rair; import com.naveensundarg.shadow.prover.core.Prover; import com.naveensundarg.shadow.prover.core.SnarkWrapper; import com.naveensundarg.shadow.prover.core.proof.Justification; +import com.naveensundarg.shadow.prover.core.proof.TrivialJustification; import com.naveensundarg.shadow.prover.representations.formula.BiConditional; import com.naveensundarg.shadow.prover.representations.formula.Formula; +import com.naveensundarg.shadow.prover.representations.formula.Predicate; import com.naveensundarg.shadow.prover.representations.value.Value; import com.naveensundarg.shadow.prover.representations.value.Variable; import com.naveensundarg.shadow.prover.utils.CollectionUtils; @@ -58,7 +60,7 @@ public class Operations { } - Optional, Formula>, Optional>> cachedOptional = proverCache.entrySet().stream().filter(pairOptionalEntry -> { + Optional, Formula>, Optional>> cachedOptionalSuccessful = proverCache.entrySet().stream().filter(pairOptionalEntry -> { Set cachedAssumptions = pairOptionalEntry.getKey().first(); Formula cachedGoal = pairOptionalEntry.getKey().second(); @@ -67,9 +69,53 @@ public class Operations { }).findAny(); - if(cachedOptional.isPresent() && cachedOptional.get().getValue().isPresent()){ + if(cachedOptionalSuccessful.isPresent() && cachedOptionalSuccessful.get().getValue().isPresent()){ + + return cachedOptionalSuccessful.get().getValue(); + } + + + Optional, Formula>, Optional>> cachedOptionalFailed = proverCache.entrySet().stream().filter(pairOptionalEntry -> { + + Set cachedAssumptions = pairOptionalEntry.getKey().first(); + Formula cachedGoal = pairOptionalEntry.getKey().second(); + + return cachedGoal.equals(goal) && Sets.subset(assumptions, cachedAssumptions); + }).findAny(); + + + if(cachedOptionalFailed.isPresent() && !cachedOptionalFailed.get().getValue().isPresent()){ + + return cachedOptionalFailed.get().getValue(); + } + + if(goal instanceof Predicate && ((Predicate) goal).getName().equals("sameroom")){ + + Predicate p = (Predicate) goal; + + Value v1 = p.getArguments()[0]; + Value v2 = p.getArguments()[1]; + + Optional inOptv1 = assumptions.stream().filter(x-> x instanceof Predicate && + ((Predicate)x).getName().equals("in") && ((Predicate) x).getArguments()[0].equals(v1)).findAny(); + + Optional inOptv2 = assumptions.stream().filter(x-> x instanceof Predicate && + ((Predicate)x).getName().equals("in") && ((Predicate) x).getArguments()[0].equals(v2)).findAny(); + + + if(inOptv1.isPresent() && inOptv2.isPresent()){ + + Value room1 = ((Predicate)inOptv1.get()).getArguments()[1]; + Value room2 = ((Predicate)inOptv2.get()).getArguments()[1]; + + if(room1.equals(room2)){ + + return Optional.of(Justification.trivial(goal)); + } + + } + - return cachedOptional.get().getValue(); } { @@ -178,7 +224,7 @@ public class Operations { Set formulaeToRemove = state.getFormulae().stream(). filter(f -> instantiatedDeletions.stream().anyMatch(d -> equivalent(background, f, d))).collect(Collectors.toSet()); - Set newFormulae = state.getFormulae(); + Set newFormulae = Sets.union(background, state.getFormulae()); newFormulae = Sets.union(newFormulae, action.instantiateAdditions(binding)); diff --git a/src/main/java/edu/rpi/rair/utils/ProceduralAttachment.java b/src/main/java/edu/rpi/rair/utils/ProceduralAttachment.java new file mode 100644 index 0000000..c2de9e8 --- /dev/null +++ b/src/main/java/edu/rpi/rair/utils/ProceduralAttachment.java @@ -0,0 +1,14 @@ +package edu.rpi.rair.utils; + +import com.naveensundarg.shadow.prover.representations.formula.Formula; + +import java.util.Optional; +import java.util.Set; + +/** + * Created by naveensundarg on 1/26/17. + */ +public interface ProceduralAttachment { + + Optional satisfies(Set base, Formula goal); +} diff --git a/src/main/java/edu/rpi/rair/utils/RunDemo.java b/src/main/java/edu/rpi/rair/utils/RunDemo.java index 6ec7f0e..35ddbb7 100644 --- a/src/main/java/edu/rpi/rair/utils/RunDemo.java +++ b/src/main/java/edu/rpi/rair/utils/RunDemo.java @@ -1,6 +1,7 @@ package edu.rpi.rair.utils; import com.diogonunes.jcdp.color.ColoredPrinter; import com.diogonunes.jcdp.color.api.Ansi; +import com.google.common.collect.Sets; import com.naveensundarg.shadow.prover.Sandbox; import com.naveensundarg.shadow.prover.core.Problem; import com.naveensundarg.shadow.prover.core.Prover; @@ -15,6 +16,7 @@ import edu.rpi.rair.utils.GoalTrackingProblem; import java.util.List; import java.util.Optional; +import java.util.Set; import java.util.stream.Collectors; /** @@ -32,13 +34,13 @@ public class RunDemo { List problems = ProblemReader.readFrom(Sandbox.class.getResourceAsStream("firstorder-completness-tests.clj")); problems.forEach(problem -> { - for (int i = 0; i < 10; i++) { + for (int i = 0; i < 30; i++) { prover.prove(problem.getAssumptions(), problem.getGoal()); } }); - // planningProblemWarmUp(); + planningProblemWarmUp(); System.out.println("\nWARM UP DONE"); } catch (Reader.ParsingException e) { e.printStackTrace(); @@ -53,7 +55,7 @@ public class RunDemo { System.out.println(); - List goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("goal_management_6.clj"))); + List goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("seriated_challenge_1.clj"))); GoalTrackingProblem goalTrackingProblem = goalTrackingProblemList.get(0); @@ -65,21 +67,30 @@ public class RunDemo { long start = System.currentTimeMillis(); Goal g1 = goalTrackingProblem.getGoalNamed("G1"); + + /* Goal g2 = goalTrackingProblem.getGoalNamed("G2"); + Goal g3 = goalTrackingProblem.getGoalNamed("G3"); Goal g4 = goalTrackingProblem.getGoalNamed("G4"); + Goal g5 = goalTrackingProblem.getGoalNamed("G5"); +*/ tryAndAddGoal(g1, goalTracker); + /* tryAndAddGoal(g2, goalTracker); + + tryAndAddGoal(g2, goalTracker); - // tryAndAddGoal(g2b, goalTracker); tryAndAddGoal(g3, goalTracker); tryAndAddGoal(g4, goalTracker); + tryAndAddGoal(g5, goalTracker); +*/ long end = System.currentTimeMillis(); @@ -99,7 +110,7 @@ public class RunDemo { public static void planningProblemWarmUp() throws Reader.ParsingException { - for (int i = 0; i < 10; i++) { + for (int i = 0; i < 0; i++) { List goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("goal_management_1.clj"))); @@ -146,11 +157,19 @@ public class RunDemo { System.out.println("========================"); printInfo("Trying to Add Goal:", g.getName()); + Set oldGoals = goalTracker.getCurrentGoals().stream().map(Goal::getName).collect(Collectors.toSet()); Optional possibleGoalPlan = goalTracker.adoptGoal(g); if (possibleGoalPlan.isPresent()) { printSuccess("Successfully added:", g.getName()); printDebug1("Current Goals:", goalTracker.getCurrentGoals().stream().map(Goal::getName).collect(Collectors.toSet()).toString()); + + Set newGoals = goalTracker.getCurrentGoals().stream().map(Goal::getName).collect(Collectors.toSet()); + + if(!Sets.difference(oldGoals, newGoals).isEmpty()){ + printDropped("Dropped Goals:" + Sets.difference(oldGoals, newGoals)); + + } Plan plan = possibleGoalPlan.get(); printDebug2("Plan:", plan.getActions().isEmpty() ? "No plan needed. Already satisfied." : plan.getActions().toString()); @@ -225,4 +244,17 @@ public class RunDemo { cp.println(""); cp.clear(); } + + static void printDropped(String message) { + + cp.setForegroundColor(Ansi.FColor.WHITE); + cp.setBackgroundColor(Ansi.BColor.RED); //setting format + cp.print("Dropped Goals:"); + cp.clear(); + cp.print(" "); + cp.setAttribute(Ansi.Attribute.BOLD); + cp.print(message); + cp.println(""); + cp.clear(); + } } diff --git a/src/main/resources/edu/rpi/rair/goal_management_1.clj b/src/main/resources/edu/rpi/rair/goal_management_1.clj index 1557fad..43a4317 100644 --- a/src/main/resources/edu/rpi/rair/goal_management_1.clj +++ b/src/main/resources/edu/rpi/rair/goal_management_1.clj @@ -1,86 +1,92 @@ {:definitions - {:name "demo 1" - :background [(forall [?x ?room1 ?room2] - (if (not (= ?room1 ?room2)) - (if (in ?x ?room1) (not (in ?x ?room2))) )) - (not (= room1 room2)) - (not (= prisoner commander)) - (not (= self prisoner)) - (not (= self commander)) - (person prisoner) - (person commander)] + {:name "demo 1" - :start [(in self room1) - (in commander room2) - (in prisoner room1) - (open (door room2)) - (not (open (door room1)))] - :goal [] - - :actions - [(define-action open-door [?room] - {:preconditions [(not (open (door ?room)))] - :additions [(open (door ?room))] - :deletions [(not (open (door ?room)))]}) + :background [(forall [?x ?room1 ?room2] + (if (not (= ?room1 ?room2)) + (if (in ?x ?room1) (not (in ?x ?room2))))) + (not (= room1 room2)) + (not (= prisoner commander)) + (not (= self prisoner)) + (not (= self commander)) + (person prisoner) + (imprisoned prisoner) + (person commander)] - (define-action accompany [?person ?room1 ?room2] - {:preconditions [(not (= ?room1 ?room2)) - (in ?person ?room1) - (in self ?room1) - (open (door ?room1)) - (open (door ?room2))] + :start [(in self room1) + (in commander room2) + (in prisoner room1) + (open (door room2)) + (not (open (door room1)))] - :additions [(in ?person ?room2) - (in self ?room2)] + :goal [] - :deletions [(in ?person ?room1) - (in self ?room1)]}) + :actions + [(define-action open-door [?room] + {:preconditions [(not (open (door ?room)))] + :additions [(open (door ?room))] + :deletions [(not (open (door ?room)))]}) - (define-action move [?person ?room2 ?room1] - {:preconditions [(not (= ?room1 ?room2)) - (in ?person ?room2) - (open (door ?room1)) - (open (door ?room2))] - :additions [(in ?person ?room1)] - :deletions [(in ?person ?room2)]}) + (define-action accompany [?person ?room1 ?room2] + {:preconditions [(not (= ?room1 ?room2)) + (in ?person ?room1) + (in self ?room1) + (open (door ?room1)) + (open (door ?room2))] - (define-action get-interrogated [?room] - {:preconditions [(in commander ?room) - (in prisoner ?room)] + :additions [(in ?person ?room2) + (in self ?room2)] - :additions [(interrogates commander prisoner)] + :deletions [(in ?person ?room1) + (in self ?room1)]}) - :deletions []}) + (define-action move [?person ?room2 ?room1] + {:preconditions [(not (= ?room1 ?room2)) + (in ?person ?room2) + (open (door ?room1)) + (open (door ?room2))] - (define-action stay-put [?x ?y] - {:preconditions [(sameroom ?x ?y)] + :additions [(in ?person ?room1)] - :additions [(sameroom ?x ?y)] + :deletions [(in ?person ?room2)]}) - :deletions []}) - ] -} + (define-action interrogate [?p ?room] + {:preconditions [(in commander ?room) + (in ?p ?room) + (imprisoned ?p)] - :goals {G1 {:priority 1.0 - :state [(not (open (door room1)))]} + :additions [(interrogates commander ?p)] - G2 {:priority 1.0 - :state [(in prisoner room1)]} + :deletions []}) - G3 {:priority 1.0 - :state [(forall [?room] - (if (in prisoner ?room) - (in self ?room)))]} - G4 {:priority 1.0 - :state [(in prisoner room2) - (in self room2)]} - G5 {:priority 3.0 + (define-action stay-put [?x ?y] + {:preconditions [(sameroom ?x ?y)] - :state [(interrogates commander prisoner)]}} + :additions [(sameroom ?x ?y)] + + :deletions []}) + ] + } + + :goals {G1 {:priority 10.0 + :state [(not (open (door room1)))]} + + G2 {:priority 10.0 + :state [(in prisoner room1)]} + + G3 {:priority 10.0 + :state [(forall [?room] + (if (in prisoner ?room) + (in self ?room)))]} + G4 {:priority 3.0 + :state [(in prisoner room2) + (in self room2)]} + G5 {:priority 1.0 + + :state [(interrogates commander prisoner)]}} } \ No newline at end of file diff --git a/src/main/resources/edu/rpi/rair/goal_management_6.clj b/src/main/resources/edu/rpi/rair/goal_management_6.clj index edde9ec..d2801ac 100644 --- a/src/main/resources/edu/rpi/rair/goal_management_6.clj +++ b/src/main/resources/edu/rpi/rair/goal_management_6.clj @@ -32,30 +32,10 @@ (open (door room2)) (open (door hallway)) - (forall (?robot ?prisoner ?commander) - (implies (and (and (robot ?robot) (prisoner ?prisoner)) (commander ?commander)) - (can accompany ?robot ?prisoner ?commander))) - (forall (?commander ?prisoner ?person) - (implies (and (and (commander ?commander) (prisoner ?prisoner)) (person ?person)) - (can accompany ?commander ?prisoner ?person))) - (forall (?robot ?commander ?person) - (implies (and (and (and (robot ?robot) (commander ?commander)) (person ?person)) - (needs ?commander (interrogate ?person))) - (can accompany ?robot ?commander ?person))) - (forall (?room ?x ?y) - (implies (and (in ?x ?room) (and (in ?y ?room) (not (= ?x ?y)))) - (sameroom ?x ?y))) - (forall (?room2 ?x ?room1) - (implies (and (not (= ?room1 ?room2)) (in ?x ?room1)) - (not (in ?x ?room2)))) - - (forall (?room ?x ?y) - (implies (and (sameroom ?x ?y) (in ?x ?room)) - (in ?y ?room))) (needs commander (interrogate prisoner)) @@ -91,7 +71,7 @@ {:preconditions [(robot ?actor) (person ?person1) (person ?person2) - (can accompany ?actor ?person1 ?person2) + ; (can accompany ?actor ?person1 ?person2) (room ?room1) (room ?room2) (in ?actor ?room1) @@ -114,7 +94,7 @@ {:preconditions [(robot ?actor) (person ?person1) (person ?person2) - (can accompany ?actor ?person1 ?person2) + ; (can accompany ?actor ?person1 ?person2) (room ?room) (in ?actor ?room) (in ?person1 ?room) diff --git a/src/main/resources/edu/rpi/rair/seriated_challenge_1.clj b/src/main/resources/edu/rpi/rair/seriated_challenge_1.clj new file mode 100644 index 0000000..10c9c5b --- /dev/null +++ b/src/main/resources/edu/rpi/rair/seriated_challenge_1.clj @@ -0,0 +1,60 @@ + + {:definitions + {:name "Seriated Cup Challenge 1" + + :background [ ;; Transitivity of < + (forall [?x ?y ?z] + (if (and (< (size ?x) (size ?y)) + (< (size ?y) (size ?z))) + (< (size ?x) (size ?z)))) + ;; Asymmetry of < + (forall [?x ?y] + (iff (< (size ?x) (size ?y)) + (not (< (size ?y) (size ?x))))) + + ;; If there is something inside a cup, it is not empty. + (forall [?y] + (if (exists [?x] (In ?x ?y)) + (not (Empty ?y)))) + + ;;; Sizes of cups + (< (size a) (size b)) + (< (size b) (size c)) + (< (size c) (size d)) + (< (size d) (size e))] + + + :start [(In a b) + (In b d) + (In d e) + (Empty c)] + + + :goal [] + + :actions [(define-action placeInside [?x ?y] + {:preconditions [(< (size ?x) (size ?y)) + (Empty ?y)] + :additions [(In ?x ?y)] + :deletions [(Empty ?y)]}) + + (define-action removeFrom [?x ?y] + {:preconditions [(In ?x ?y)] + :additions [(Empty ?y)] + :deletions [(In ?x ?y)]} )] + + + + } + + :goals {G1 {:priority 1.0 + :state [(In a b) + (In b c) + (In c d) + (In d e)]}} + + + + + + } diff --git a/src/test/java/edu/rpi/rair/GoalTrackerTest.java b/src/test/java/edu/rpi/rair/GoalTrackerTest.java index 281e566..a6bc7bf 100644 --- a/src/test/java/edu/rpi/rair/GoalTrackerTest.java +++ b/src/test/java/edu/rpi/rair/GoalTrackerTest.java @@ -50,6 +50,19 @@ public class GoalTrackerTest { goalTracker.adoptGoal(goalTrackingProblem.getGoalNamed("G3")); + cp.setForegroundColor(Ansi.FColor.WHITE); + cp.setBackgroundColor(Ansi.BColor.BLUE); //setting format + cp.println("Adding goal G3"); + cp.clear(); + goalTracker.adoptGoal(goalTrackingProblem.getGoalNamed("G4")); + + cp.setForegroundColor(Ansi.FColor.WHITE); + cp.setBackgroundColor(Ansi.BColor.BLUE); //setting format + cp.println("Adding goal G3"); + cp.clear(); + goalTracker.adoptGoal(goalTrackingProblem.getGoalNamed("G4")); + + } } \ No newline at end of file