planner.encoder.Encoder Class Reference

Inheritance diagram for planner.encoder.Encoder:

Public Member Functions
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
	task
	modifier
	mutexes
	boolean_variables
	numeric_variables
	action_variables

Private Member Functions
def	_ground (self)
def	_sort_axioms (self)
	Stores numeric axioms sorted according to different criteria. More...
def	_computeSerialMutexes (self)
	Computes mutually exclusive actions for serial encodings, i.e., all actions are mutually exclusive. More...
def	_computeParallelMutexes (self)
	Computes mutually exclusive actions: Two actions (a1, a2) are mutex if: More...

Detailed Description

Base encoder class. Defines methods to build standard
state-based encodings -- i.e., Rintanen 09

Member Function Documentation

def planner.encoder.Encoder._computeParallelMutexes (   self )

private

Computes mutually exclusive actions: Two actions (a1, a2) are mutex if:

• intersection pre_a1 and eff_a2 (or viceversa) is non-empty
• intersection between eff_a1+ and eff_a2- (or viceversa) is non-empty
• intersection between numeric effects is non-empty

See, e.g., 'A Compilation of the Full PDDL+ Language into SMT'', Cashmore et al.

Returns

mutex: list of tuples defining action mutexes

def planner.encoder.Encoder._computeSerialMutexes (   self )

private

Computes mutually exclusive actions for serial encodings, i.e., all actions are mutually exclusive.

Returns

mutex: list of tuples defining action mutexes

def planner.encoder.Encoder._ground (   self )

private

Grounds action schemas as per TFD parser)

def planner.encoder.Encoder._sort_axioms (   self )

private

Stores numeric axioms sorted according to different criteria.

Returns 3 dictionaries:

Returns

axioms_by_name: numeric axioms sorted by name

depends_on: dependencies between axioms

axioms_by_layer: axioms sorted by layer (see "Using the Context-enhanced Additive Heuristic for Temporal and Numeric Planning.", Eyerich et al.)

def planner.encoder.Encoder.createVariables

(

self

)

Creates state and action variables needed in the encoding.

Variables are stored in dictionaries as follows:

dict[step][variable_name] = Z3 variable instance

def planner.encoder.Encoder.encode	(		self,
			horizon
	)

Basic method to build bounded encoding.

def planner.encoder.Encoder.encodeActions

(

self

)

Encodes universal axioms: each action variable implies its preconditions and effects.

Returns

actions: z3 formulas encoding actions.

def planner.encoder.Encoder.encodeExecutionSemantics

(

self

)

Encodes execution semantics as specified by modifier class.

Returns

axioms that specify execution semantics.

def planner.encoder.Encoder.encodeFrame

(

self

)

Encode explanatory frame axioms: a predicate retains its value unless it is modified by the effects of an action.

Returns

frame: list of frame axioms

def planner.encoder.Encoder.encodeGoalState

(

self

)

Encodes formula defining goal state.

Returns

goal: Z3 formula asserting propositional and numeric subgoals

def planner.encoder.Encoder.encodeInitialState

(

self

)

Encodes formula defining initial state.

Returns

initial: Z3 formula asserting initial state

---

The documentation for this class was generated from the following file:

• planner/encoder.py