Inheritance diagram for planner.encoder.EncoderSMT:

Collaboration diagram for planner.encoder.EncoderSMT:

Public Member Functions
def	encode (self, horizon)
	Builds SMT 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
	horizon

Public Attributes inherited from planner.encoder.Encoder
	task

	modifier

	mutexes

	boolean_variables

	numeric_variables

	action_variables

Detailed Description

Class that defines method to build SMT encoding.

Member Function Documentation

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

Builds SMT encoding.

Parameters

horizon horizon for bounded planning formula.

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