idp_solver.Parse

Classes to parse and annotate an IDP-Z3 theory.

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

Bases: idp_solver.Expression.ASTNode

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

execute()

Execute the IDP program

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

Bases: idp_solver.Expression.ASTNode

The class of AST nodes representing a vocabulary block.

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

Bases: idp_solver.Expression.ASTNode

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

Bases: idp_solver.Expression.ASTNode

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

Bases: idp_solver.Expression.ASTNode

AST node to represent type <symbol> := <enumeration>

Parameters
  • name (string) – name of the type

  • constructors ([Constructor]) – list of constructors in the enumeration

  • interpretation (SymbolInterpretation) – the symbol interpretation

  • translated (Z3) – the translation of the type in Z3

  • map (Dict[string, Constructor]) – a mapping from code to Expression

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

Bases: idp_solver.Expression.ASTNode

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

Bases: idp_solver.Expression.ASTNode

The class of AST nodes representing an entry in the vocabulary, declaring one or more symbols. Multi-symbols declaration are replaced by single-symbol declarations before the annotate() stage.

annotations

the annotations given by the expert.

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

symbols

the symbols beind defined, before expansion

Type

[Symbol]

name

the identifier of the symbol, after expansion of the node

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

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]

unit

the unit of the symbol, such as m (meters)

Type

str

category

the category that the symbol should belong to

Type

str

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

Bases: idp_solver.Expression.ASTNode

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

Bases: idp_solver.Expression.ASTNode

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

Bases: idp_solver.Expression.ASTNode

The class of AST nodes representing a theory block.

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

Bases: idp_solver.Expression.ASTNode

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

Bases: idp_solver.Expression.ASTNode

rename_args(new_vars)[source]

for Clark’s completion input : ‘!v: f(args) <- body(args)’ output: ‘!nv: f(nv) <- ?v: nv=args & body(args)’

compute(theory)[source]

expand quantifiers and interpret

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

Bases: idp_solver.Expression.ASTNode

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.

Returns None

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

Bases: idp_solver.Expression.ASTNode

contains(args, function, arity=None, rank=0, tuples=None)[source]

returns an Expression that says whether Tuple args is in the enumeration

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

Bases: idp_solver.Expression.ASTNode

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

Bases: idp_solver.Expression.ASTNode

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

Bases: idp_solver.Expression.ASTNode

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

Bases: idp_solver.Expression.ASTNode

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

Bases: idp_solver.Expression.ASTNode