idp_solver.Parse¶

Classes to parse and annotate an IDP-Z3 theory.

class idp_solver.Parse.Idp(**kwargs)[source]

Bases: object

The class of AST nodes representing an IDP-Z3 program.

execute()

Execute the IDP program

class idp_solver.Parse.Vocabulary(**kwargs)[source]

Bases: object

The class of AST nodes representing a vocabulary block.

class idp_solver.Parse.SymbolDeclaration(**kwargs)[source]

Bases: object

The class of AST nodes representing an entry in the vocabulary, declaring a symbol.

annotations

the annotations given by the expert.

annotations[‘reading’] is the annotation giving the intended meaning of the expression (in English).

name

the identifier of the symbol

Type: string
sorts

the types of the arguments

Type: List[Sort]
out

the type of the symbol

type

the name of the type of the symbol

Type: string
arity

the number of arguments

Type: int
function

True if the symbol is a function

Type: bool
domain

the list of possible tuples of arguments

Type: List
instances

a mapping from the code of a symbol applied to a tuple of arguments to its parsed AST

Type: Dict[string, Expression]
range

the list of possible values

Type: List[Expression]
typeConstraints

the type constraint on the ranges of the symbol applied to each possible tuple of arguments

Type: List[Expression]
class idp_solver.Parse.Theory(**kwargs)[source]

Bases: object

The class of AST nodes representing a theory block.

class idp_solver.Parse.Structure(**kwargs)[source]

Bases: object

The class of AST nodes representing an structure block.

annotate(idp)[source]

Annotates the structure with the enumerations found in it. Every enumeration is converted into an assignment, which is added to self.assignments.

Parameters: idp – a Parse.Idp object.