Unstable Python API

`vehicle_lang.ast`

vehicle_lang.ast.load(path: str | Path, *, declarations: Iterable[str] = (), target: Target = Explicit.Explicit) → Program

Programs

class vehicle_lang.ast.Program

class vehicle_lang.ast.Main(declarations: Sequence[vehicle_lang.ast.Declaration])

Declarations

class vehicle_lang.ast.Declaration

class vehicle_lang.ast.DefFunction(provenance: vehicle_lang.ast.Provenance, name: str, type: vehicle_lang.ast.Expression, body: vehicle_lang.ast.Expression)

class vehicle_lang.ast.DefPostulate(provenance: vehicle_lang.ast.Provenance, name: str, body: vehicle_lang.ast.Expression)

Expressions

class vehicle_lang.ast.Expression

class vehicle_lang.ast.App(provenance: vehicle_lang.ast.Provenance, function: vehicle_lang.ast.Expression, arguments: Sequence[vehicle_lang.ast.Expression])

class vehicle_lang.ast.PartialApp(provenance: vehicle_lang.ast.Provenance, arity: int, function: vehicle_lang.ast.Expression, arguments: Sequence[vehicle_lang.ast.Expression])

class vehicle_lang.ast.Binder(provenance: vehicle_lang.ast.Provenance, name: str | None, type: vehicle_lang.ast.Expression)

class vehicle_lang.ast.BoundVar(provenance: vehicle_lang.ast.Provenance, name: str)

class vehicle_lang.ast.Builtin(provenance: vehicle_lang.ast.Provenance, builtin: vehicle_lang.ast.BuiltinConstant | vehicle_lang.ast.BuiltinFunction | vehicle_lang.ast.BuiltinLiteral | vehicle_lang.ast.BuiltinType)

class vehicle_lang.ast.FreeVar(provenance: vehicle_lang.ast.Provenance, name: str)

class vehicle_lang.ast.Lam(provenance: vehicle_lang.ast.Provenance, binders: Sequence[vehicle_lang.ast.Binder], body: vehicle_lang.ast.Expression)

class vehicle_lang.ast.Let(provenance: vehicle_lang.ast.Provenance, bound: vehicle_lang.ast.Expression, binder: vehicle_lang.ast.Binder, body: vehicle_lang.ast.Expression)

class vehicle_lang.ast.Pi(provenance: vehicle_lang.ast.Provenance, binder: vehicle_lang.ast.Binder, body: vehicle_lang.ast.Expression)

class vehicle_lang.ast.Universe(provenance: vehicle_lang.ast.Provenance, level: int)

Builtins

class vehicle_lang.ast.BuiltinFunction

class vehicle_lang.ast.ConsList

class vehicle_lang.ast.EqIndex

class vehicle_lang.ast.FoldList

class vehicle_lang.ast.GeIndex

class vehicle_lang.ast.GtIndex

class vehicle_lang.ast.If

class vehicle_lang.ast.Index(value: int)

class vehicle_lang.ast.IndexType

class vehicle_lang.ast.LeIndex

class vehicle_lang.ast.ListType

class vehicle_lang.ast.LtIndex

class vehicle_lang.ast.MapList

class vehicle_lang.ast.NeIndex

class vehicle_lang.ast.NilList

class vehicle_lang.ast.Unit

class vehicle_lang.ast.UnitType

Abstract Base Class

class vehicle_lang.ast.AST

Provenance

class vehicle_lang.ast.Provenance(lineno: int, col_offset: int, end_lineno: int | None = None, end_col_offset: int | None = None)

col_offset: int

end_col_offset: int | None = None

end_lineno: int | None = None

lineno: int

vehicle_lang.ast.MISSING: Provenance = Provenance(lineno=0, col_offset=0, end_lineno=None, end_col_offset=None): Provenance(lineno: int, col_offset: int, end_lineno: Optional[int] = None, end_col_offset: Optional[int] = None)

`vehicle_lang.compile`

`vehicle_lang.compile.abc`

`vehicle_lang.compile.abcboolasbool`

`vehicle_lang.compile.abcnumeric`

`vehicle_lang.compile.python`

exception vehicle_lang.compile.python.EraseType

class vehicle_lang.compile.python.PythonTranslation(builtins: vehicle_lang.compile.abc.builtins.ABCBuiltins[typing.Any, typing.Any, typing.Any, typing.Any, typing.Any, typing.Any, typing.Any, typing.Any, typing.Any, typing.Any], module_header: Sequence[ast.stmt] = <factory>, module_footer: Sequence[ast.stmt] = <factory>)

builtins: ABCBuiltins[Any, Any, Any, Any, Any, Any, Any, Any, Any, Any]

compile(program: Program, path: str | Path, declaration_context: Dict[str, Any] = {}) → Dict[str, Any]

ignored_types: List[str]

module_footer: Sequence[stmt]

module_header: Sequence[stmt]

translate_App(expression: App) → expr

translate_BoundVar(expression: BoundVar) → expr

translate_Builtin(expression: Builtin) → expr

translate_DefFunction(declaration: DefFunction) → stmt

translate_DefPostulate(declaration: DefPostulate) → stmt

translate_FreeVar(expression: FreeVar) → expr

translate_Lam(expression: Lam) → expr

translate_Main(program: Main) → Module

translate_PartialApp(expression: PartialApp) → expr

translate_Pi(_expression: Pi) → expr

translate_Universe(_expression: Universe) → expr

translate_binder(binder: Binder) → arg

translate_declarations(declarations: Iterator[Declaration]) → Iterator[stmt]

vehicle_lang.compile.python.py_app(function: expr, *arguments: expr, provenance: Provenance) → expr

Make a function call.

vehicle_lang.compile.python.py_binder(*args: arg) → arguments

Make a binder which only uses args.

vehicle_lang.compile.python.py_builtin(builtin: str, *, provenance: Provenance) → expr

Make a builtin function call.

vehicle_lang.compile.python.py_fraction(value: Fraction, provenance: Provenance) → expr

vehicle_lang.compile.python.py_name(name: str, *, provenance: Provenance) → Name

Make a name.

vehicle_lang.compile.python.py_partial_app(function: expr, *arguments: expr, provenance: Provenance) → expr

Make a partial function call.

vehicle_lang.compile.python.py_qualified_name(*parts: str, provenance: Provenance) → expr

Make a qualified name.

vehicle_lang.compile.python.py_scalar(value: DType, provenance: Provenance) → expr

Make a scalar.

vehicle_lang.compile.python.py_tensor(tensor: Tensor[DType], provenance: Provenance) → expr

Make a tensor.

vehicle_lang.compile.python.py_tuple(elements: List[expr], provenance: Provenance) → expr

Make a tuple.

`vehicle_lang.pygments`

class vehicle_lang.pygments.VehicleLexer(*args, **kwds)

aliases = ['vehicle']: A list of short, unique identifiers that can be used to look up the lexer from a list, e.g., using get_lexer_by_name().

filenames = ['*.vcl']: A list of fnmatch patterns that match filenames which contain content for this lexer. The patterns in this list should be unique among all lexers.

name = 'Vehicle': Full name of the lexer, in human-readable form

tokens = {'root': [('--.*\\n', ('Comment',)), ('\\{-((.)(?<!-))*-((.)(?<![-\\}])((.)(?<!-))*-|-)*\\}', ('Comment',)), ('True|False', ('Name', 'Builtin')), ('(\\d)+', ('Literal', 'Number', 'Integer')), ('(\\d)+\\.(\\d)+', ('Literal', 'Number', 'Float')), ('@network', ('Keyword', 'Declaration')), ('@dataset', ('Keyword', 'Declaration')), ('@parameter', ('Keyword', 'Declaration')), ('@property', ('Keyword', 'Declaration')), ('@postulate', ('Keyword', 'Declaration')), ('->', ('Operator',)), ('forallT', ('Keyword',)), ('if', ('Keyword',)), ('then', ('Keyword',)), ('else', ('Keyword',)), ('\\.', ('Punctuation',)), (':', ('Punctuation',)), ('\\\\', ('Punctuation',)), ('let', ('Keyword',)), ('Type', ('Keyword', 'Type')), ('Unit', ('Keyword', 'Type')), ('Bool', ('Keyword', 'Type')), ('Nat', ('Keyword', 'Type')), ('Int', ('Keyword', 'Type')), ('Rat', ('Keyword', 'Type')), ('Vector', ('Keyword', 'Type')), ('List', ('Keyword', 'Type')), ('Index', ('Keyword', 'Type')), ('forall', ('Keyword',)), ('exists', ('Keyword',)), ('foreach', ('Keyword',)), ('=>', ('Operator',)), ('and', ('Operator', 'Word')), ('or', ('Operator', 'Word')), ('not', ('Operator', 'Word')), ('==', ('Operator',)), ('!=', ('Operator',)), ('<=', ('Operator',)), ('<', ('Operator',)), ('>=', ('Operator',)), ('>', ('Operator',)), ('\\*', ('Operator',)), ('/', ('Operator',)), ('\\+', ('Operator',)), ('-', ('Operator',)), ('nil', ('Operator',)), ('::', ('Operator',)), ('\\[', ('Operator',)), ('\\]', ('Operator',)), ('::v', ('Operator',)), ('!', ('Operator',)), ('map', ('Name', 'Builtin')), ('fold', ('Name', 'Builtin')), ('dfold', ('Name', 'Builtin')), ('indices', ('Name', 'Builtin')), ('HasEq', ('Keyword', 'Type')), ('HasNotEq', ('Keyword', 'Type')), ('HasAdd', ('Keyword', 'Type')), ('HasSub', ('Keyword', 'Type')), ('HasMul', ('Keyword', 'Type')), ('HasFold', ('Keyword', 'Type')), ('HasMap', ('Keyword', 'Type')), ('[a-zA-Z](_|\\d|[a-zA-Z])*', ('Name',)), ('\\?(_|\\d|[a-zA-Z])*', ('Name',)), ('(\\d|[a-zA-Z])+', ('Name',)), ("[a-zA-Z]([a-zA-Z]|\\d|_|\\')*", ('Name',)), ('\\(|\\)|\\{|\\}|\\{\\{|\\}\\}|=|,|\\(\\)|;', ('Punctuation',)), ('(\\d)+', ('Literal', 'Number', 'Integer')), ('(\\d)+\\.(\\d)+(e(-)?(\\d)+)?', ('Literal', 'Number', 'Float')), ('"((.)(?<!["\\\\])|\\\\["\\\\nt])*"', ('Literal', 'String', 'Double')), ("\\'((.)(?<![\\'\\\\])|\\\\[\\'\\\\nt])\\'", ('Literal', 'String', 'Char')), ('\\s+', ('Space',)), ('--.*\\n', ('Comment',)), ('\\{-((.)(?<!-))*-((.)(?<![-\\}])((.)(?<!-))*-|-)*\\}', ('Comment',)), ('True|False', ('Name',)), ('(\\d)+', ('Name',)), ('(\\d)+\\.(\\d)+', ('Name',)), ('@network', ('Name',)), ('@dataset', ('Name',)), ('@parameter', ('Name',)), ('@property', ('Name',)), ('@postulate', ('Name',)), ('@noinline', ('Name',)), ('->', ('Name',)), ('forallT', ('Name',)), ('if', ('Name',)), ('then', ('Name',)), ('else', ('Name',)), ('\\.', ('Name',)), (':', ('Name',)), ('\\\\', ('Name',)), ('let', ('Name',)), ('Type', ('Name',)), ('Unit', ('Name',)), ('Bool', ('Name',)), ('Nat', ('Name',)), ('Int', ('Name',)), ('Rat', ('Name',)), ('Vector', ('Name',)), ('List', ('Name',)), ('Index', ('Name',)), ('forall', ('Name',)), ('exists', ('Name',)), ('foreach', ('Name',)), ('=>', ('Name',)), ('and', ('Name',)), ('or', ('Name',)), ('not', ('Name',)), ('==', ('Name',)), ('!=', ('Name',)), ('<=', ('Name',)), ('<', ('Name',)), ('>=', ('Name',)), ('>', ('Name',)), ('\\*', ('Name',)), ('/', ('Name',)), ('\\+', ('Name',)), ('-', ('Name',)), ('nil', ('Name',)), ('::', ('Name',)), ('\\[', ('Name',)), ('\\]', ('Name',)), ('::v', ('Name',)), ('!', ('Name',)), ('map', ('Name',)), ('fold', ('Name',)), ('dfold', ('Name',)), ('indices', ('Name',)), ('fromNat', ('Name',)), ('fromInt', ('Name',)), ('HasEq', ('Name',)), ('HasNotEq', ('Name',)), ('HasAdd', ('Name',)), ('HasSub', ('Name',)), ('HasMul', ('Name',)), ('HasFold', ('Name',)), ('HasMap', ('Name',)), ('[a-zA-Z](_|\\d|[a-zA-Z])*', ('Name',)), ('\\?(_|\\d|[a-zA-Z])*', ('Name',)), ('(\\d|[a-zA-Z])+', ('Name',)), ("[a-zA-Z]([a-zA-Z]|\\d|_|\\')*", ('Name',)), ('\\(|\\)|\\{|\\}|\\{\\{|\\}\\}|=|,|\\(\\)|;', ('Operator',)), ('(\\d)+', ('Literal', 'Number', 'Integer')), ('(\\d)+\\.(\\d)+(e(-)?(\\d)+)?', ('Literal', 'Number', 'Float')), ('"((.)(?<!["\\\\])|\\\\["\\\\nt])*"', ('Literal', 'String', 'Double')), ("\\'((.)(?<![\\'\\\\])|\\\\[\\'\\\\nt])\\'", ('Literal', 'String', 'Char')), ('\\s+', ('Space',))]}

At all time there is a stack of states. Initially, the stack contains a single state ‘root’. The top of the stack is called “the current state”.

Dict of {'state': [(regex, tokentype, new_state), ...], ...}

new_state can be omitted to signify no state transition. If new_state is a string, it is pushed on the stack. This ensure the new current state is new_state. If new_state is a tuple of strings, all of those strings are pushed on the stack and the current state will be the last element of the list. new_state can also be combined('state1', 'state2', ...) to signify a new, anonymous state combined from the rules of two or more existing ones. Furthermore, it can be ‘#pop’ to signify going back one step in the state stack, or ‘#push’ to push the current state on the stack again. Note that if you push while in a combined state, the combined state itself is pushed, and not only the state in which the rule is defined.

The tuple can also be replaced with include('state'), in which case the rules from the state named by the string are included in the current one.

`vehicle_lang.verify`

vehicle_lang.verify.verify(specification: str | Path, properties: Iterable[str] | None = None, networks: Dict[str, str | Path] = {}, datasets: Dict[str, str | Path] = {}, parameters: Dict[str, Any] = {}, verifier: Verifier = Verifier.Marabou, verifier_location: str | Path | None = None, cache: str | Path | None = None) → None

Check whether properties in a Vehicle specification hold.

Parameters:

specification (str | Path) – The path to the Vehicle specification file to verify.
properties (Iterable[str] | None) – The names of the properties in the specification to verify, defaults to all declarations.
networks (Dict[str, str | Path]) – A map from the network names in the specification to files containing the networks.
datasets (Dict[str, str | Path]) – A map from the dataset names in the specification to files containing the datasets.
parameters (Dict[str, Any]) – A map from the parameter names in the specification to the values to be used in verification.
verifier (Verifier) – The verifier to be used, defaults to Marabou.
verifier_location (str | Path | None) – The path to the verifier executable, defaults to searching the system path.
cache (str | Path | None) – The path to the proof cache used by Vehicle, defaults to not writing a proof cache.

`vehicle_lang.error`

exception vehicle_lang.error.VehicleError

exception vehicle_lang.error.VehicleInternalError

`vehicle_lang.typing`

vehicle_lang.typing.AnyOptimiser

An optimiser that promises to work for any type.

alias of Callable[[bool, Dict[str, Any], Callable[[Any, Any], Any], Callable[[Any], Any]], Any]

vehicle_lang.typing.AnyOptimisers

A mapping from quantified variable names to optimisers.

alias of Dict[str, Callable[[bool, Dict[str, Any], Callable[[Any, Any], Any], Callable[[Any], Any]], Any]]

vehicle_lang.typing.DeclarationName: A name of a top-level declaration in a Vehicle specification file.

class vehicle_lang.typing.DifferentiableLogic(value)

The differentiable logics supported by Vehicle.

DL2 = 2

Godel = 3

Lukasiewicz = 4

Product = 5

Vehicle = 1

Yager = 6

class vehicle_lang.typing.Explicit(value)

The direct translation from Vehicle to Python.

Explicit = 1

vehicle_lang.typing.Optimiser

TODO: add description

alias of Callable[[bool, Dict[str, _T], Callable[[_R, _R], _R], Callable[[_T], _R]], _R]

vehicle_lang.typing.QuantifiedVariableName: A name of a quantified variable in a Vehicle specification file.

class vehicle_lang.typing.Target(*args, **kwargs)

Translation targets from Vehicle to Python.

Valid values are either Explicit or any member of DifferentiableLogic.

class vehicle_lang.typing.Verifier(value)

The neural network verifiers supported by Vehicle.

Marabou = 1: The Marabou verifier.

Unstable Python API

vehicle_lang.ast

Programs

Declarations

Expressions

Builtins

Abstract Base Class

Provenance

vehicle_lang.compile

vehicle_lang.compile.abc

vehicle_lang.compile.abcboolasbool

vehicle_lang.compile.abcnumeric

vehicle_lang.compile.python

vehicle_lang.pygments

vehicle_lang.verify

vehicle_lang.error

vehicle_lang.typing