mirror of
https://github.com/RAIRLab/Spectra.git
synced 2024-11-09 11:10:34 -05:00
Removed dead code
This commit is contained in:
parent
8692700b8f
commit
59b6845107
2 changed files with 38 additions and 151 deletions
|
@ -33,6 +33,7 @@ public class Operations {
|
||||||
|
|
||||||
private static boolean DEEP_EQUIVALENCE = false;
|
private static boolean DEEP_EQUIVALENCE = false;
|
||||||
private static boolean THROW_AWAY_EMPTY_BINDINGS = true;
|
private static boolean THROW_AWAY_EMPTY_BINDINGS = true;
|
||||||
|
private static boolean MONOTONIC = true;
|
||||||
private static Prover prover;
|
private static Prover prover;
|
||||||
|
|
||||||
|
|
||||||
|
@ -52,40 +53,44 @@ public class Operations {
|
||||||
}
|
}
|
||||||
|
|
||||||
public static synchronized Optional<Justification> proveCached(Set<Formula> assumptions, Formula goal) {
|
public static synchronized Optional<Justification> proveCached(Set<Formula> assumptions, Formula goal) {
|
||||||
|
|
||||||
// (1) If we've asked to prove this exact goal from assumptions before
|
|
||||||
// then return the previous result
|
|
||||||
Pair<Set<Formula>, Formula> inputPair = ImmutablePair.of(assumptions, goal);
|
Pair<Set<Formula>, Formula> inputPair = ImmutablePair.of(assumptions, goal);
|
||||||
if (proverCache.containsKey(inputPair)) {
|
|
||||||
return proverCache.get(inputPair);
|
|
||||||
}
|
|
||||||
|
|
||||||
// Iterate through the cache
|
if (MONOTONIC) {
|
||||||
for (Map.Entry<Pair<Set<Formula>, Formula>, Optional<Justification>> entry : proverCache.entrySet()) {
|
// (1) If we've asked to prove this exact goal from assumptions before
|
||||||
Set<Formula> cachedAssumptions = entry.getKey().getLeft();
|
// then return the previous result
|
||||||
Formula cachedGoal = entry.getKey().getRight();
|
if (proverCache.containsKey(inputPair)) {
|
||||||
Optional<Justification> optJust = entry.getValue();
|
return proverCache.get(inputPair);
|
||||||
|
|
||||||
// (2) Return the cached justification if:
|
|
||||||
// - Goals are the same
|
|
||||||
// - The cached assumptions are a subset of the current ones
|
|
||||||
// - A justification was found
|
|
||||||
if (optJust.isPresent() && cachedGoal.equals(goal) && Sets.subset(cachedAssumptions, assumptions)) {
|
|
||||||
return optJust;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
// (3) Return cached failure if:
|
// Iterate through the cache
|
||||||
// - Goals are the same
|
for (Map.Entry<Pair<Set<Formula>, Formula>, Optional<Justification>> entry : proverCache.entrySet()) {
|
||||||
// - Assumptions are a subset of cached assumptions
|
Set<Formula> cachedAssumptions = entry.getKey().getLeft();
|
||||||
// - No justification was found
|
Formula cachedGoal = entry.getKey().getRight();
|
||||||
if (optJust.isEmpty() && cachedGoal.equals(goal) && Sets.subset(assumptions, cachedAssumptions)) {
|
Optional<Justification> optJust = entry.getValue();
|
||||||
return optJust;
|
|
||||||
|
// (2) Return the cached justification if:
|
||||||
|
// - Goals are the same
|
||||||
|
// - The cached assumptions are a subset of the current ones
|
||||||
|
// - A justification was found
|
||||||
|
if (optJust.isPresent() && cachedGoal.equals(goal) && Sets.subset(cachedAssumptions, assumptions)) {
|
||||||
|
return optJust;
|
||||||
|
}
|
||||||
|
|
||||||
|
// (3) Return cached failure if:
|
||||||
|
// - Goals are the same
|
||||||
|
// - Assumptions are a subset of cached assumptions
|
||||||
|
// - No justification was found
|
||||||
|
if (optJust.isEmpty() && cachedGoal.equals(goal) && Sets.subset(assumptions, cachedAssumptions)) {
|
||||||
|
return optJust;
|
||||||
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
// Otherwise create a new call to the theorem prover
|
// Otherwise create a new call to the theorem prover
|
||||||
Optional<Justification> answer = prover.prove(assumptions, goal);
|
Optional<Justification> answer = prover.prove(assumptions, goal);
|
||||||
proverCache.put(inputPair, answer);
|
if (MONOTONIC) {
|
||||||
|
proverCache.put(inputPair, answer);
|
||||||
|
}
|
||||||
return answer;
|
return answer;
|
||||||
|
|
||||||
}
|
}
|
||||||
|
@ -176,18 +181,7 @@ public class Operations {
|
||||||
return -1;
|
return -1;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
public static Optional<Set<Pair<State, Action>>> apply(Set<Formula> background, Action action, State state) {
|
||||||
// Take a time value, get the integer number out and
|
|
||||||
// increment by 1
|
|
||||||
public static Value incrementTime(Value time) {
|
|
||||||
int t = getTime(time);
|
|
||||||
if (t < 0) {
|
|
||||||
return new Constant("ERROR");
|
|
||||||
}
|
|
||||||
return new Constant("t" + (t + 1));
|
|
||||||
}
|
|
||||||
|
|
||||||
public static Optional<Set<Pair<State, Action>>> apply(Set<Formula> background, Action action, State state, Value t) {
|
|
||||||
|
|
||||||
// // Get resulting states from cache if computed before
|
// // Get resulting states from cache if computed before
|
||||||
if(applyCache.containsKey(Triple.of(background, action, state))){
|
if(applyCache.containsKey(Triple.of(background, action, state))){
|
||||||
|
@ -201,20 +195,12 @@ public class Operations {
|
||||||
// Ask theorem prover for witnesses that satisfy the precondition
|
// Ask theorem prover for witnesses that satisfy the precondition
|
||||||
Set<Formula> givens = Sets.union(background, state.getFormulae());
|
Set<Formula> givens = Sets.union(background, state.getFormulae());
|
||||||
|
|
||||||
// TODO: Have all this ?now and (next ?now) code within Action.java
|
|
||||||
|
|
||||||
// Replace ?now with current time within preconditions
|
|
||||||
Formula precondition = action.getPrecondition();
|
Formula precondition = action.getPrecondition();
|
||||||
Value now = new Variable("?now");
|
|
||||||
precondition = replaceValue(precondition, now, t);
|
|
||||||
|
|
||||||
// We already replaced the ?now
|
|
||||||
List<Variable> openVars = action.openVars()
|
List<Variable> openVars = action.openVars()
|
||||||
.stream()
|
.stream()
|
||||||
.filter(v -> !v.getName().equals("?now"))
|
|
||||||
.collect(Collectors.toList());
|
.collect(Collectors.toList());
|
||||||
|
|
||||||
// TODO: Can likely more intelligently cache considering time...
|
|
||||||
Optional<Set<Map<Variable, Value>>> bindingsOpt = proveAndGetBindingsCached(givens, precondition, openVars);
|
Optional<Set<Map<Variable, Value>>> bindingsOpt = proveAndGetBindingsCached(givens, precondition, openVars);
|
||||||
|
|
||||||
// If not witnesses found, return nothing
|
// If not witnesses found, return nothing
|
||||||
|
@ -240,13 +226,6 @@ public class Operations {
|
||||||
Set<Formula> additions = groundedAction.getAdditions();
|
Set<Formula> additions = groundedAction.getAdditions();
|
||||||
Set<Formula> deletions = groundedAction.getDeletions();
|
Set<Formula> deletions = groundedAction.getDeletions();
|
||||||
|
|
||||||
// Replace (next ?now) with appropriate time
|
|
||||||
Value nextTime = incrementTime(t);
|
|
||||||
Value nextTimeVar = new Variable("?next");
|
|
||||||
additions = replaceValue(additions, nextTimeVar, nextTime);
|
|
||||||
deletions = replaceValue(deletions, nextTimeVar, nextTime);
|
|
||||||
|
|
||||||
|
|
||||||
State newState = State.initializeWith(Sets.union(
|
State newState = State.initializeWith(Sets.union(
|
||||||
Sets.difference(state.getFormulae(), deletions),
|
Sets.difference(state.getFormulae(), deletions),
|
||||||
additions
|
additions
|
||||||
|
@ -264,97 +243,6 @@ public class Operations {
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
public static State replaceValue(State s, Value r, Value t) {
|
|
||||||
Set<Formula> newFormulae = replaceValue(s.getFormulae(), r, t);
|
|
||||||
return State.initializeWith(newFormulae);
|
|
||||||
}
|
|
||||||
|
|
||||||
public static Set<Formula> replaceValue(Set<Formula> s, Value r, Value t) {
|
|
||||||
Set<Formula> newFormulae = new HashSet<Formula>();
|
|
||||||
for (Formula f : s) {
|
|
||||||
newFormulae.add(replaceValue(f, r, t));
|
|
||||||
}
|
|
||||||
return newFormulae;
|
|
||||||
}
|
|
||||||
|
|
||||||
public static Value replaceValue(Value v, Value r, Value t) {
|
|
||||||
if (v.getName().equals(r.getName())) {
|
|
||||||
return t;
|
|
||||||
}
|
|
||||||
return v;
|
|
||||||
}
|
|
||||||
|
|
||||||
// Everywhere where there's a ?now replace with value t
|
|
||||||
public static Formula replaceValue(Formula f, Value r, Value t) {
|
|
||||||
// Base Cases:
|
|
||||||
|
|
||||||
// Bottom of Formula graph wouldn't have any time points under it
|
|
||||||
if (f instanceof Predicate || f instanceof Atom) {
|
|
||||||
return f;
|
|
||||||
}
|
|
||||||
|
|
||||||
// Check if these quantifiers contain our bound varialbe
|
|
||||||
if (f instanceof UnaryModalFormula) {
|
|
||||||
UnaryModalFormula uf = (UnaryModalFormula) f;
|
|
||||||
|
|
||||||
Value agent = uf.getAgent();
|
|
||||||
Value time = uf.getTime();
|
|
||||||
Value newTime = replaceValue(time, r, t);
|
|
||||||
Formula uf_sub = uf.getFormula();
|
|
||||||
Formula new_uf_sub = replaceValue(uf_sub, r, t);
|
|
||||||
|
|
||||||
if (f instanceof Belief) {
|
|
||||||
return new Belief(agent, newTime, new_uf_sub);
|
|
||||||
} else if (f instanceof Intends) {
|
|
||||||
return new Intends(agent, newTime, new_uf_sub);
|
|
||||||
} else if (f instanceof Knowledge) {
|
|
||||||
return new Knowledge(agent, newTime, new_uf_sub);
|
|
||||||
}
|
|
||||||
// Assumes Perception
|
|
||||||
if (! (f instanceof Perception)) {
|
|
||||||
System.out.println("[fixTimepoints:Operations.java] Doesn't account for new modal operator");
|
|
||||||
}
|
|
||||||
return new Perception(agent, newTime, new_uf_sub);
|
|
||||||
}
|
|
||||||
|
|
||||||
// Recusive Case: Iterate over each subformula and replace
|
|
||||||
|
|
||||||
if (f instanceof Not) {
|
|
||||||
Formula subFormula = ((Not) f).getArgument();
|
|
||||||
return new Not(replaceValue(subFormula, r, t));
|
|
||||||
} else if (f instanceof Universal) {
|
|
||||||
Formula subFormula = ((Universal) f).getArgument();
|
|
||||||
return new Universal(((Universal) f).vars(), replaceValue(subFormula, r, t));
|
|
||||||
} else if (f instanceof Existential) {
|
|
||||||
Formula subFormula = ((Existential) f).getArgument();
|
|
||||||
return new Universal(((Existential) f).vars(), replaceValue(subFormula, r, t));
|
|
||||||
} else if (f instanceof Implication) {
|
|
||||||
Formula antecedant = ((Implication) f).getAntecedent();
|
|
||||||
Formula consequent = ((Implication) f).getConsequent();
|
|
||||||
return new Implication(replaceValue(antecedant, r, t), replaceValue(consequent, r, t));
|
|
||||||
} else if (f instanceof BiConditional) {
|
|
||||||
Formula left = ((BiConditional) f).getLeft();
|
|
||||||
Formula right = ((BiConditional) f).getRight();
|
|
||||||
return new BiConditional(replaceValue(left, r, t), replaceValue(right, r, t));
|
|
||||||
}
|
|
||||||
|
|
||||||
List<Formula> subFormulae = f.getArgs();
|
|
||||||
List<Formula> newArguments = new ArrayList<Formula>();
|
|
||||||
for (Formula sf : subFormulae) {
|
|
||||||
newArguments.add(replaceValue(sf, r, t));
|
|
||||||
}
|
|
||||||
|
|
||||||
if (f instanceof And) {
|
|
||||||
return new And(newArguments);
|
|
||||||
}
|
|
||||||
|
|
||||||
// Assume Or
|
|
||||||
if (! (f instanceof Or)) {
|
|
||||||
System.out.println("[fixTimepoints:Operations.java] Not accounting for formula type in recursive case");
|
|
||||||
}
|
|
||||||
return new Or(newArguments);
|
|
||||||
}
|
|
||||||
|
|
||||||
public static boolean equivalent(Set<Formula> background, Formula f1, Formula f2) {
|
public static boolean equivalent(Set<Formula> background, Formula f1, Formula f2) {
|
||||||
if (!DEEP_EQUIVALENCE) {
|
if (!DEEP_EQUIVALENCE) {
|
||||||
return f1.equals(f2);
|
return f1.equals(f2);
|
||||||
|
|
|
@ -86,11 +86,11 @@ public class AStarPlanner {
|
||||||
State lastState = currentSearch.getLeft();
|
State lastState = currentSearch.getLeft();
|
||||||
List<Action> previous_actions = currentSearch.getRight();
|
List<Action> previous_actions = currentSearch.getRight();
|
||||||
|
|
||||||
System.out.println("--------------------");
|
// System.out.println("--------------------");
|
||||||
System.out.println("Considering state with heuristic: " + comparator.getValue(currentSearch));
|
// System.out.println("Considering state with heuristic: " + comparator.getValue(currentSearch));
|
||||||
System.out.println("Current Plan: " + seq.get(lastState).toString());
|
// System.out.println("Current Plan: " + seq.get(lastState).toString());
|
||||||
System.out.println("Current State: " + lastState.toString());
|
// System.out.println("Current State: " + lastState.toString());
|
||||||
System.out.println("--------------------");
|
// System.out.println("--------------------");
|
||||||
|
|
||||||
// Exit loop if we've passed the depth limit
|
// Exit loop if we've passed the depth limit
|
||||||
int currentDepth = previous_actions.size();
|
int currentDepth = previous_actions.size();
|
||||||
|
@ -116,8 +116,7 @@ public class AStarPlanner {
|
||||||
for (Action action : nonTrivialActions) {
|
for (Action action : nonTrivialActions) {
|
||||||
// System.out.println("Considering action: " + action.getName());
|
// System.out.println("Considering action: " + action.getName());
|
||||||
|
|
||||||
Value currentTime = Operations.getTime(previous_actions.size());
|
Optional<Set<Pair<State, Action>>> optNextStateActionPairs = Operations.apply(background, action, lastState);
|
||||||
Optional<Set<Pair<State, Action>>> optNextStateActionPairs = Operations.apply(background, action, lastState, currentTime);
|
|
||||||
|
|
||||||
// Ignore actions that aren't applicable
|
// Ignore actions that aren't applicable
|
||||||
if (optNextStateActionPairs.isEmpty()) {
|
if (optNextStateActionPairs.isEmpty()) {
|
||||||
|
|
Loading…
Reference in a new issue