diff --git a/.idea/libraries/Maven__com_diogonunes_JCDP_2_0_1.xml b/.idea/libraries/Maven__com_diogonunes_JCDP_2_0_1.xml
new file mode 100644
index 0000000..574defc
--- /dev/null
+++ b/.idea/libraries/Maven__com_diogonunes_JCDP_2_0_1.xml
@@ -0,0 +1,13 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/.idea/libraries/Maven__org_fusesource_jansi_jansi_1_11.xml b/.idea/libraries/Maven__org_fusesource_jansi_jansi_1_11.xml
new file mode 100644
index 0000000..2ab51a7
--- /dev/null
+++ b/.idea/libraries/Maven__org_fusesource_jansi_jansi_1_11.xml
@@ -0,0 +1,13 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/.idea/vcs.xml b/.idea/vcs.xml
new file mode 100644
index 0000000..35eb1dd
--- /dev/null
+++ b/.idea/vcs.xml
@@ -0,0 +1,6 @@
+
+
+
+
+
+
\ No newline at end of file
diff --git a/pom.xml b/pom.xml
index d7191e8..ebdc119 100644
--- a/pom.xml
+++ b/pom.xml
@@ -24,6 +24,11 @@
test
+
+ com.diogonunes
+ JCDP
+ 2.0.1
+
us.bpsm
edn-java
diff --git a/snark-20120808r02/snark-interface.lisp b/snark-20120808r02/snark-interface.lisp
index 8771762..6149fb0 100644
--- a/snark-20120808r02/snark-interface.lisp
+++ b/snark-20120808r02/snark-interface.lisp
@@ -40,6 +40,7 @@
(snark:prove-supported t)
(snark:use-hyperresolution t)
(snark:use-paramodulation t)
+
(snark:allow-skolem-symbols-in-answers nil))
(defun row-formula (name))
@@ -135,6 +136,9 @@
"")))))
+(defun get-answer-string (proof)
+ (string-downcase (princ-to-string (@! (rest (snark:answer proof))))))
+
(defun prove-from-axioms-and-get-answers (all-axioms f vars
&key
(time-limit 5)
@@ -157,9 +161,39 @@
(let ((proof (snark:prove (!@ f) :answer (!@ (cons 'ans vars)) )))
(if (equalp :PROOF-FOUND proof)
- (string-downcase (princ-to-string (@! (rest (snark:answer proof) ))))
+ (get-answer-string proof)
"")))))
+(defun prove-from-axioms-and-get-multiple-answers (all-axioms f vars
+ &key
+ (time-limit 5)
+ (verbose nil)
+ sortal-setup-fn)
+ (let ((axioms (remove-duplicates all-axioms :test #'equalp)))
+ (setup-snark :time-limit time-limit :verbose verbose)
+ (if sortal-setup-fn (funcall sortal-setup-fn))
+ (let* ((n-a (make-hash-table :test #'equalp))
+ (a-n (make-hash-table :test #'equalp)))
+ (mapcar (lambda (axiom)
+ (let ((name (gensym)))
+ (setf (gethash (princ-to-string axiom) a-n) name)
+ (setf (gethash (princ-to-string name) n-a) axiom))) axioms)
+ (mapcar (lambda (axiom)
+ (snark::assert axiom :name (gethash (princ-to-string axiom) a-n)
+ ))
+ (mapcar #'!@ axioms))
+
+ (let ((proof (snark:prove (!@ f) :answer (!@ (cons 'ans vars)) )))
+
+ (if (equalp :PROOF-FOUND proof)
+ (princ-to-string (cons (get-answer-string proof) (call)))
+ "")))))
+
+(defun call ()
+ (let ((proof (snark:closure)))
+ (if (equalp :PROOF-FOUND proof)
+ (cons (get-answer-string proof) (call))
+ ())))
(defun proved? (ans) (first ans))
(defun used-premises (ans) (second ans))
diff --git a/src/main/java/edu/rpi/rair/DepthFirstPlanner.java b/src/main/java/edu/rpi/rair/DepthFirstPlanner.java
index 97c4639..fa32817 100644
--- a/src/main/java/edu/rpi/rair/DepthFirstPlanner.java
+++ b/src/main/java/edu/rpi/rair/DepthFirstPlanner.java
@@ -14,10 +14,26 @@ import java.util.stream.Collectors;
public class DepthFirstPlanner implements Planner {
+ private static final int MAX_DEPTH = 4;
+
+
@Override
public Optional> plan(Set background, Set actions, State start, State goal) {
+ return planInternal(Sets.newSet(), 0, background, actions, start, goal);
+
+
+ }
+
+
+
+ private Optional> planInternal(Set> history, int currentDepth, Set background, Set actions, State start, State goal) {
+
+ if(currentDepth>=MAX_DEPTH){
+ return Optional.empty();
+ }
+
if (Operations.satisfies(background, start, goal)) {
//Already satisfied. Do nothing. Return a set with an empty plan.
return Optional.of(Sets.with(Plan.newEmptyPlan(goal, background)));
@@ -29,29 +45,38 @@ public class DepthFirstPlanner implements Planner {
for (Action action : actions) {
- Optional> nextStateActionPair = Operations.apply(background, action, start);
+ Optional>> nextStateActionPairs = Operations.apply(background, action, start);
- if (nextStateActionPair.isPresent()) {
+ if (nextStateActionPairs.isPresent()) {
- Optional> planOpt = plan(background, actions, nextStateActionPair.get().first(), goal);
+ for (Pair stateActionPair : nextStateActionPairs.get()) {
- if (planOpt.isPresent()) {
- atleastOnePlanFound = true;
- Set nextPlans = planOpt.get();
- State nextSate = nextStateActionPair.get().first();
- Action instantiatedAction = nextStateActionPair.get().second();
+ Optional> planOpt = planInternal(history, currentDepth+1, background, actions, stateActionPair.first(), goal);
- Set augmentedPlans = nextPlans.stream().
- map(plan -> plan.getPlanByStartingWith(instantiatedAction, nextSate)).
- collect(Collectors.toSet());
+ if (planOpt.isPresent()) {
- allPlans.addAll(augmentedPlans);
- //TODO: store different plans and return the best plan.
+ atleastOnePlanFound = true;
+ Set nextPlans = planOpt.get();
+
+ State nextSate = stateActionPair.first();
+ Action instantiatedAction = stateActionPair.second();
+
+ Set augmentedPlans = nextPlans.stream().
+ map(plan -> plan.getPlanByStartingWith(instantiatedAction, nextSate)).
+ collect(Collectors.toSet());
+
+ allPlans.addAll(augmentedPlans);
+
+ //TODO: store different plans and return the best plan.
+ }
}
+
+
}
+
}
if (atleastOnePlanFound) {
@@ -67,4 +92,5 @@ public class DepthFirstPlanner implements Planner {
}
+
}
diff --git a/src/main/java/edu/rpi/rair/Goal.java b/src/main/java/edu/rpi/rair/Goal.java
index f8cdd50..bc4c36e 100644
--- a/src/main/java/edu/rpi/rair/Goal.java
+++ b/src/main/java/edu/rpi/rair/Goal.java
@@ -1,5 +1,7 @@
package edu.rpi.rair;
+import java.util.concurrent.atomic.AtomicInteger;
+
/**
* Created by naveensundarg on 1/14/17.
*/
@@ -7,18 +9,36 @@ public class Goal {
private final State goalState;
private final int priority;
+ private final String name;
+ private static final AtomicInteger nameCounter;
+ static {
+ nameCounter = new AtomicInteger(0);
+ }
private Goal(State goalState, int priority) {
this.goalState = goalState;
this.priority = priority;
+ this.name = "G" + nameCounter.incrementAndGet();
}
+ private Goal(State goalState, int priority, String name) {
+ this.goalState = goalState;
+ this.priority = priority;
+ this.name = name;
+ }
public static Goal makeGoal(State goalState, int priority){
return new Goal(goalState, priority);
}
+ public static Goal makeGoal(State goalState, int priority, String name){
+
+ return new Goal(goalState, priority, name);
+
+ }
+
+
public State getGoalState() {
return goalState;
}
@@ -27,11 +47,16 @@ public class Goal {
return priority;
}
+ public String getName() {
+ return name;
+ }
+
@Override
public String toString() {
return "Goal{" +
"goalState=" + goalState +
", priority=" + priority +
+ ", name='" + name + '\'' +
'}';
}
diff --git a/src/main/java/edu/rpi/rair/GoalTracker.java b/src/main/java/edu/rpi/rair/GoalTracker.java
index 8bd84a5..e979c8f 100644
--- a/src/main/java/edu/rpi/rair/GoalTracker.java
+++ b/src/main/java/edu/rpi/rair/GoalTracker.java
@@ -14,6 +14,9 @@ import java.util.Set;
public class GoalTracker {
+
+
+
private final Set background;
private State currentState;
private final Set currentGoals;
@@ -32,6 +35,7 @@ public class GoalTracker {
public boolean adoptGoal(Goal goal) {
+
Optional> possiblePlans = planner.plan(background, actions, currentState, goal.getGoalState());
if (!possiblePlans.isPresent()) {
diff --git a/src/main/java/edu/rpi/rair/Operations.java b/src/main/java/edu/rpi/rair/Operations.java
index 326d4a7..81575cf 100644
--- a/src/main/java/edu/rpi/rair/Operations.java
+++ b/src/main/java/edu/rpi/rair/Operations.java
@@ -3,9 +3,11 @@ package edu.rpi.rair;
import com.naveensundarg.shadow.prover.core.Prover;
import com.naveensundarg.shadow.prover.core.SnarkWrapper;
import com.naveensundarg.shadow.prover.representations.formula.And;
+import com.naveensundarg.shadow.prover.representations.formula.BiConditional;
import com.naveensundarg.shadow.prover.representations.formula.Formula;
import com.naveensundarg.shadow.prover.representations.value.Value;
import com.naveensundarg.shadow.prover.representations.value.Variable;
+import com.naveensundarg.shadow.prover.utils.CollectionUtils;
import com.naveensundarg.shadow.prover.utils.ImmutablePair;
import com.naveensundarg.shadow.prover.utils.Pair;
import com.naveensundarg.shadow.prover.utils.Sets;
@@ -14,6 +16,7 @@ import java.util.List;
import java.util.Map;
import java.util.Optional;
import java.util.Set;
+import java.util.concurrent.*;
import java.util.stream.Collectors;
import static edu.rpi.rair.State.FALSE;
@@ -23,6 +26,7 @@ import static edu.rpi.rair.State.FALSE;
*/
public class Operations {
+ private static boolean DEEP_EQUIVALENCE = false;
private static Prover prover;
static{
@@ -31,38 +35,125 @@ public class Operations {
public static synchronized Optional