|
OMTPlan: Optimal Planning Modulo Theories
|
Public Member Functions | |
| def | encodeObjective (self) |
| Encodes objective function. More... | |
| def | createAuxVariables (self) |
| def | encodeRelaxedActions (self) |
| Encodes relaxed universal axioms. More... | |
| def | encodeTransitiveClosure (self) |
| Encodes computation of transitive closure at step n+1 (see related paper). More... | |
| def | encodeRelaxedGoal (self) |
| Encodes relaxed goals. More... | |
| def | encodeAdditionalCosts (self) |
| Encodes costs for relaxed actions that may be executed in the suffix. More... | |
| def | encodeASAP (self) |
| Encodes constraints that push execution of actions as early as possible. More... | |
| def | encodeOnlyIfNeeded (self) |
| Enforces that auxiliary variables can be executed only ifall steps before the suffix are filled with at least one action. More... | |
| def | encode (self, horizon) |
| Builds OMT encoding. More... | |
 Public Member Functions inherited from planner.encoder.Encoder | |
| def | __init__ (self, task, modifier) |
| def | createVariables (self) |
| Creates state and action variables needed in the encoding. More... | |
| def | encodeInitialState (self) |
| Encodes formula defining initial state. More... | |
| def | encodeGoalState (self) |
| Encodes formula defining goal state. More... | |
| def | encodeActions (self) |
| Encodes universal axioms: each action variable implies its preconditions and effects. More... | |
| def | encodeFrame (self) |
| Encode explanatory frame axioms: a predicate retains its value unless it is modified by the effects of an action. More... | |
| def | encodeExecutionSemantics (self) |
| Encodes execution semantics as specified by modifier class. More... | |
| def | encode (self, horizon) |
Public Attributes | |
| touched_variables | |
| auxiliary_actions | |
| final_costs | |
| horizon | |
| var_objective | |
| Public Attributes inherited from planner.encoder.Encoder | |
| task | |
| modifier | |
| mutexes | |
| boolean_variables | |
| numeric_variables | |
| action_variables | |
Class that defines method to build SMT encoding.
| def planner.encoder.EncoderOMT.createAuxVariables | ( | self | ) |
Creates auxiliary variables used in relaxed suffix (see related paper).
| def planner.encoder.EncoderOMT.encode | ( | self, | |
| horizon | |||
| ) |
Builds OMT encoding.
| horizon | horizon for bounded planning formula. |
| def planner.encoder.EncoderOMT.encodeAdditionalCosts | ( | self | ) |
Encodes costs for relaxed actions that may be executed in the suffix.
At each step, we define a cost variables that is equal to the summation of pseudoboolean terms (if action is executed we pay a price – see paper)
| def planner.encoder.EncoderOMT.encodeASAP | ( | self | ) |
Encodes constraints that push execution of actions as early as possible.
| def planner.encoder.EncoderOMT.encodeObjective | ( | self | ) |
Encodes objective function.
If domain is metric it builds a Z3 formula encoding the metric, otherwise it builds a pseudoboolean objective (i.e., we pay one each time an action is executed).
| def planner.encoder.EncoderOMT.encodeOnlyIfNeeded | ( | self | ) |
Enforces that auxiliary variables can be executed only ifall steps before the suffix are filled with at least one action.
| def planner.encoder.EncoderOMT.encodeRelaxedActions | ( | self | ) |
Encodes relaxed universal axioms.
| def planner.encoder.EncoderOMT.encodeRelaxedGoal | ( | self | ) |
Encodes relaxed goals.
| def planner.encoder.EncoderOMT.encodeTransitiveClosure | ( | self | ) |
Encodes computation of transitive closure at step n+1 (see related paper).
1.8.11
