idp_solver.Parse

Classes to parse and annotate an IDP-Z3 theory.

class idp_solver.Parse.Idp(**kwargs)

Bases: object

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

execute()

Execute the IDP program

class idp_solver.Parse.Vocabulary(**kwargs)

Bases: object

The class of AST nodes representing a vocabulary block.

class idp_solver.Parse.SymbolDeclaration(**kwargs)

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)

Bases: object

The class of AST nodes representing a theory block.

class idp_solver.Parse.Structure(**kwargs)

Bases: object

The class of AST nodes representing an structure block.

annotate(idp)

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. Returns None: