utils.py File Reference

Functions
def	utils.getDomainName (task_filename)
	Tries to find PDDL domain file when only problem file is supplied. More...
def	utils.getValFromModel (assignment)
	Extracts values from Z3 model making sure types are properly converted. More...
def	utils.varNameFromNFluent (fluent)
	Returns variable name used for encoding numeric fluents in SMT. More...
def	utils.varNameFromBFluent (fluent)
	Returns variable name used for encoding boolean fluents in SMT. More...
def	utils.isBoolFluent (fluent)
	Checks if fluent is propositional. More...
def	utils.isNumFluent (fluent)
	Checks if fluent is numeric. More...
def	utils.inorderTraversal (encoder, nax, numeric_variables)
	Traverses the parsed domain as returned by TFD parser: More...
def	utils.inorderTraversalFC (encoder, condition, numeric_variables)
	Inorder traversal for Comparison axioms – see "Using the Context-enhanced Additive Heuristic for Temporal and Numeric Planning", Eyerich et al. More...
def	utils.extractVariables (encoder, nax, variables)
	Extracts variables contained in PDDL numeric expressions. More...
def	utils.extractVariablesFC (encoder, condition)
	Extracts variables contained in PDDL comparison axioms. More...
def	utils.parseMetric (encoder)
	Extracts variables appearing in PDDL metric. More...
def	utils.buildMetricExpr (encoder)
	Builds Z3 expression of PDDL metric. More...
def	utils.printSMTFormula (formula, problem_name)
	Prints SMT planning formula in SMT-LIB syntax. More...
def	utils.printOMTFormula (formula, problem_name)
	Prints OMT planning formula in SMT-LIB syntax. More...

Function Documentation

def utils.buildMetricExpr

(

encoder

)

Builds Z3 expression of PDDL metric.

Parameters

encoder

encoder object.

Returns

metricExpr: Z3 expression encoding metric.

def utils.extractVariables	(		encoder,
			nax,
			variables
	)

Extracts variables contained in PDDL numeric expressions.

Parameters

encoder.
nax	numeric axioms returned by TFD.
variables	dictionary containing Z3 variables.

Returns

variables: list of Z3 variables.

def utils.extractVariablesFC	(		encoder,
			condition
	)

Extracts variables contained in PDDL comparison axioms.

Parameters

encoder.
condition	PDDL comparison axiom.

Returns

variables: list of Z3 variables.

def utils.getDomainName

(

task_filename

)

Tries to find PDDL domain file when only problem file is supplied.

Parameters

task_filename

path to PDDL problem file.

Returns

domain_filename: path to PDDL domain, if found.

def utils.getValFromModel

(

assignment

)

Extracts values from Z3 model making sure types are properly converted.

Parameters

assigment

variable assignment with Z3 type.

Returns

variable assignment with Python type.

def utils.inorderTraversal	(		encoder,
			nax,
			numeric_variables
	)

Traverses the parsed domain as returned by TFD parser:

See "Using the Context-enhanced Additive Heuristic for Temporal and Numeric Planning", Eyerich et al.

Parameters

encode	object.
nax	numeric axioms returned by parser.
numeric_variables	Z3 numeric variables.

Returns

Z3 arithmetic expression (simple expression).

def utils.inorderTraversalFC	(		encoder,
			condition,
			numeric_variables
	)

Inorder traversal for Comparison axioms – see "Using the Context-enhanced Additive Heuristic for Temporal and Numeric Planning", Eyerich et al.

Internally relies on inorderTraversal().

Parameters

encoder
codnition	numeric PDDL condition.
numeric_variables	dictionary with Z3 variables

Returns

Z3 arithmetic expression (comparison).

def utils.isBoolFluent

(

fluent

)

Checks if fluent is propositional.

Parameters

fluent

PDDL fluent.

Returns

Truth value.

def utils.isNumFluent

(

fluent

)

Checks if fluent is numeric.

Parameters

fluent

PDDL fluent.

Returns

Truth value.

def utils.parseMetric

(

encoder

)

Extracts variables appearing in PDDL metric.

Parameters

encoder.

Returns

var_names: list of Z3 variables.

def utils.printOMTFormula	(		formula,
			problem_name
	)

Prints OMT planning formula in SMT-LIB syntax.

Parameters

formula
problem_name

def utils.printSMTFormula	(		formula,
			problem_name
	)

Prints SMT planning formula in SMT-LIB syntax.

Parameters

formula
problem_name

def utils.varNameFromBFluent

(

fluent

)

Returns variable name used for encoding boolean fluents in SMT.

Parameters

fluent

Propositional PDDL fluent.

Returns

Z3 variable name.

def utils.varNameFromNFluent

(

fluent

)

Returns variable name used for encoding numeric fluents in SMT.

Parameters

fluent

Numeric PDDL fluent

Returns

Z3 variable name.