rairlab/Spectra
1
0
Fork 0
mirror of https://github.com/RAIRLab/Spectra.git synced 2024-11-23 09:26:30 -05:00
Code Issues Projects Releases Packages Wiki Activity

Cleaning up application of states

Browse source
This commit is contained in:
Brandon Rozek 2023-10-31 15:03:00 -04:00
parent c189cdb650
commit 2f08f98845
No known key found for this signature in database
GPG key ID: 26E457DA82C9F480
1 changed files with 18 additions and 64 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

80
src/main/java/org/rairlab/planner/Operations.java
View file

@ -163,9 +163,8 @@ public class Operations {
public static Optional<Set<Pair<State, Action>>> apply(Set<Formula> background, Action action, State state) {
// Get resulting states from cache if computed before
if(applyCache.containsKey(Triple.of(background, action, state))){
Optional<Set<Pair<State, Action>>> ans = applyCache.get(Triple.of(background, action, state));
if(ans.isPresent()){
return applyCache.get(Triple.of(background, action, state));
@ -173,87 +172,46 @@ public class Operations {
}
}
// Ask theorem prover for witnesses that satisfy the precondition
Set<Formula> givens = Sets.union(background, state.getFormulae());
Optional<Set<Map<Variable, Value>>> bindingsOpt = proveAndGetBindingsCached(givens, action.getPrecondition(), action.openVars());
State newState;
// If not witnesses found, return nothing
if (!bindingsOpt.isPresent()) {
applyCache.put(Triple.of(background, action, state), Optional.empty());
return Optional.empty();
}
Visualizer.nested(action.getName());
Set<Pair<State, Action>> nextStates = Sets.newSet();
Set<Pair<State, Action>> nexts = Sets.newSet();
for (Map<Variable, Value> binding : bindingsOpt.get()) {
if (THROW_AWAY_EMPTY_BINDINGS && binding.values().stream().anyMatch(x -> x instanceof Variable)) {
continue;
}
Set<Formula> instantiatedDeletions = action.instantiateDeletions(binding);
Set<Formula> formulaeToRemove = state.getFormulae().stream().
filter(f -> instantiatedDeletions.stream().anyMatch(d -> equivalent(Sets.union(background, state.getFormulae()), f, d))).collect(Collectors.toSet());
Set<Formula> newFormulae = Sets.union(background, state.getFormulae());
newFormulae = Sets.union(newFormulae, action.instantiateAdditions(binding).stream().map(Simplifier::simplify).collect(Collectors.toSet()));
newFormulae = Sets.difference(newFormulae, formulaeToRemove);
newState = State.initializeWith(newFormulae);
nexts.add(ImmutablePair.of(newState, action.instantiate(binding)));
// Apply binding to get grounded action and calculate the next state
// newState = (oldState - Deletions(a)) U Additions(a)
Action groundedAction = action.instantiate(binding);
State newState = State.initializeWith(Sets.union(
Sets.difference(state.getFormulae(), groundedAction.getDeletions()),
groundedAction.getAdditions()
));
// If the state progresses, record it as a possible next state
if (!newState.equals(state)) {
nextStates.add(ImmutablePair.of(newState, groundedAction));
}
}
if (nexts.isEmpty()) {
Map<Variable, Value> emptyBinding = CollectionUtils.newMap();
Set<Formula> instantiatedDeletions = action.instantiateDeletions(emptyBinding);
Set<Formula> formulaeToRemove = state.getFormulae().stream().
filter(f -> instantiatedDeletions.stream().anyMatch(d -> equivalent(background, f, d))).collect(Collectors.toSet());
Set<Formula> newFormulae = state.getFormulae();
newFormulae = Sets.union(newFormulae, action.instantiateAdditions(emptyBinding));
newFormulae = Sets.difference(newFormulae, formulaeToRemove);
newState = State.initializeWith(newFormulae);
nexts.add(ImmutablePair.of(newState, action.instantiate(emptyBinding)));
}
nexts = nexts.stream().filter(n-> !n.getLeft().getFormulae().equals(state.getFormulae())).collect(Collectors.toSet());;
applyCache.put(Triple.of(background, action ,state), Optional.of(nexts));
return Optional.of(nexts);
applyCache.put(Triple.of(background, action, state), Optional.of(nextStates));
return Optional.of(nextStates);
}
public static boolean equivalent(Set<Formula> background, Formula f1, Formula f2) {
if (!DEEP_EQUIVALENCE) {
return f1.equals(f2);
}
@ -263,7 +221,6 @@ public class Operations {
}
public static boolean satisfies(Set<Formula> background, State state, State goal) {
if ((Sets.union(background, state.getFormulae()).containsAll(goal.getFormulae()))) {
return true;
}
@ -272,16 +229,13 @@ public class Operations {
Sets.union(background, state.getFormulae()),
Commons.makeAnd(goal.getFormulae())
).isPresent();
}
public static boolean conflicts(Set<Formula> background, State state1, State state2) {
return proveCached(
Sets.union(background, Sets.union(state1.getFormulae(), state2.getFormulae())),
State.FALSE
).isPresent();
}
}