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.BuiltinFunction)

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.AddInt

class vehicle_lang.ast.AddNat

class vehicle_lang.ast.AddRat

class vehicle_lang.ast.And

class vehicle_lang.ast.AtVector

class vehicle_lang.ast.Bool(value: bool)

class vehicle_lang.ast.BoolType

class vehicle_lang.ast.ConsList

class vehicle_lang.ast.DivRat

class vehicle_lang.ast.EqIndex

class vehicle_lang.ast.EqInt

class vehicle_lang.ast.EqNat

class vehicle_lang.ast.EqRat

class vehicle_lang.ast.Exists

class vehicle_lang.ast.FoldList

class vehicle_lang.ast.FoldVector

class vehicle_lang.ast.Forall

class vehicle_lang.ast.GeIndex

class vehicle_lang.ast.GeInt

class vehicle_lang.ast.GeNat

class vehicle_lang.ast.GeRat

class vehicle_lang.ast.GtIndex

class vehicle_lang.ast.GtInt

class vehicle_lang.ast.GtNat

class vehicle_lang.ast.GtRat

class vehicle_lang.ast.If

class vehicle_lang.ast.Implies

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

class vehicle_lang.ast.IndexType

class vehicle_lang.ast.Indices

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

class vehicle_lang.ast.IntType

class vehicle_lang.ast.LeIndex

class vehicle_lang.ast.LeInt

class vehicle_lang.ast.LeNat

class vehicle_lang.ast.LeRat

class vehicle_lang.ast.ListType

class vehicle_lang.ast.LtIndex

class vehicle_lang.ast.LtInt

class vehicle_lang.ast.LtNat

class vehicle_lang.ast.LtRat

class vehicle_lang.ast.MapList

class vehicle_lang.ast.MapVector

class vehicle_lang.ast.MaxRat

class vehicle_lang.ast.MinRat

class vehicle_lang.ast.MulInt

class vehicle_lang.ast.MulNat

class vehicle_lang.ast.MulRat

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

class vehicle_lang.ast.NatType

class vehicle_lang.ast.NeIndex

class vehicle_lang.ast.NeInt

class vehicle_lang.ast.NeNat

class vehicle_lang.ast.NeRat

class vehicle_lang.ast.NegInt

class vehicle_lang.ast.NegRat

class vehicle_lang.ast.NilList

class vehicle_lang.ast.Not

class vehicle_lang.ast.Or

class vehicle_lang.ast.PowRat

class vehicle_lang.ast.Rat(numerator: int, denominator: int)

class vehicle_lang.ast.RatType

class vehicle_lang.ast.SubInt

class vehicle_lang.ast.SubRat

class vehicle_lang.ast.Unit

class vehicle_lang.ast.UnitType

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

class vehicle_lang.ast.VectorType

class vehicle_lang.ast.ZipWithVector

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`

class vehicle_lang.compile.abc.ABCBuiltins

AddInt(x: _SupportsInt, y: _SupportsInt) → _SupportsInt

AddNat(x: _SupportsNat, y: _SupportsNat) → _SupportsNat

AddRat(x: _SupportsRat, y: _SupportsRat) → _SupportsRat

And(x: bool, y: bool) → bool

abstract AtVector(vector: SupportsVector[_T], index: int) → _T

Bool(value: bool) → bool

ConsList(item: _T, iterable: SupportsList[_T]) → SupportsList[_T]

DivRat(x: _SupportsRat, y: _SupportsRat) → _SupportsRat

EqIndex(x: int, y: int) → bool

EqInt(x: _SupportsInt, y: _SupportsInt) → bool

EqNat(x: _SupportsNat, y: _SupportsNat) → bool

EqRat(x: _SupportsRat, y: _SupportsRat) → bool

Exists(name: str, context: Dict[str, Any], predicate: Callable[[_T], bool]) → bool

FoldList(function: Callable[[_S, _T], _T], initial: _T, iterable: SupportsList[_S]) → _T

abstract FoldVector(function: Callable[[_S, _T], _T], initial: _T, vector: SupportsVector[_S]) → _T

Forall(name: str, context: Dict[str, Any], predicate: Callable[[_T], bool]) → bool

GeIndex(x: int, y: int) → bool

GeInt(x: _SupportsInt, y: _SupportsInt) → bool

GeNat(x: _SupportsNat, y: _SupportsNat) → bool

GeRat(x: _SupportsRat, y: _SupportsRat) → bool

GtIndex(x: int, y: int) → bool

GtInt(x: _SupportsInt, y: _SupportsInt) → bool

GtNat(x: _SupportsNat, y: _SupportsNat) → bool

GtRat(x: _SupportsRat, y: _SupportsRat) → bool

If(cond: bool, if_true: _T, if_false: _T) → _T

Implies(x: bool, y: bool) → bool

Index(value: SupportsInt) → int

Indices(upto: int) → SupportsVector[int]

abstract Int(value: SupportsInt) → _SupportsInt

LeIndex(x: int, y: int) → bool

LeInt(x: _SupportsInt, y: _SupportsInt) → bool

LeNat(x: _SupportsNat, y: _SupportsNat) → bool

LeRat(x: _SupportsRat, y: _SupportsRat) → bool

LtIndex(x: int, y: int) → bool

LtInt(x: _SupportsInt, y: _SupportsInt) → bool

LtNat(x: _SupportsNat, y: _SupportsNat) → bool

LtRat(x: _SupportsRat, y: _SupportsRat) → bool

MapList(function: Callable[[_S], _T], iterable: SupportsList[_S]) → SupportsList[_T]

abstract MapVector(function: Callable[[_S], _T], vector: SupportsVector[_S]) → SupportsVector[_T]

MaxRat(x: _SupportsRat, y: _SupportsRat) → _SupportsRat

MinRat(x: _SupportsRat, y: _SupportsRat) → _SupportsRat

MulInt(x: _SupportsInt, y: _SupportsInt) → _SupportsInt

MulNat(x: _SupportsNat, y: _SupportsNat) → _SupportsNat

MulRat(x: _SupportsRat, y: _SupportsRat) → _SupportsRat

abstract Nat(value: SupportsInt) → _SupportsNat

NeIndex(x: int, y: int) → bool

NeInt(x: _SupportsInt, y: _SupportsInt) → bool

NeNat(x: _SupportsNat, y: _SupportsNat) → bool

NeRat(x: _SupportsRat, y: _SupportsRat) → bool

NegInt(x: _SupportsInt) → _SupportsInt

NegRat(x: _SupportsRat) → _SupportsRat

NilList() → SupportsList[_T]

Not(x: bool) → bool

Optimise(name: str, minimise: bool, context: Dict[str, Any], joiner: Callable[[Any, Any], Any], predicate: Callable[[Any], Any]) → Any

Or(x: bool, y: bool) → bool

PowRat(x: _SupportsRat, y: _SupportsInt) → _SupportsRat

abstract Rat(value: SupportsFloat) → _SupportsRat

SubInt(x: _SupportsInt, y: _SupportsInt) → _SupportsInt

SubRat(x: _SupportsRat, y: _SupportsRat) → _SupportsRat

Unit() → Tuple[()]

abstract Vector(*values: _T) → SupportsVector[_T]

abstract ZipWithVector(function: Callable[[_S, _T], _U], vector1: SupportsVector[_S], vector2: SupportsVector[_T]) → SupportsVector[_U]

optimisers: Dict[str, Callable[[bool, Dict[str, Any], Callable[[_SupportsRat, _SupportsRat], _SupportsRat], Callable[[Any], _SupportsRat]], _SupportsRat]]

class vehicle_lang.compile.abc.ABCTranslation

abstract translate_App(expression: App) → _Expression

abstract translate_BoundVar(expression: BoundVar) → _Expression

abstract translate_Builtin(expression: Builtin) → _Expression

abstract translate_DefFunction(declaration: DefFunction) → _Declaration

abstract translate_DefPostulate(declaration: DefPostulate) → _Declaration

abstract translate_FreeVar(expression: FreeVar) → _Expression

abstract translate_Lam(expression: Lam) → _Expression

translate_Let(expression: Let) → _Expression

abstract translate_Main(program: Main) → _Program

abstract translate_PartialApp(expression: PartialApp) → _Expression

abstract translate_Pi(expression: Pi) → _Expression

abstract translate_Universe(expression: Universe) → _Expression

translate_declaration(declaration: Declaration) → _Declaration

translate_expression(expression: Expression) → _Expression

translate_program(program: Program) → _Program

class vehicle_lang.compile.abc.Translation

abstract translate_declaration(declaration: Declaration) → _Declaration

abstract translate_expression(expression: Expression) → _Expression

abstract translate_program(program: Program) → _Program

`vehicle_lang.compile.abcboolasbool`

`vehicle_lang.compile.abcnumeric`

`vehicle_lang.compile.python`

class vehicle_lang.compile.python.AST

classmethod from_json(value: str) → Self

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

name: str | None

provenance: Provenance

type: Expression

class vehicle_lang.compile.python.BuiltinFunction

class vehicle_lang.compile.python.Declaration

abstract get_name() → str

class vehicle_lang.compile.python.Expression

class vehicle_lang.compile.python.Program

class vehicle_lang.compile.python.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

class vehicle_lang.compile.python.PythonBuiltins(optimisers: Dict[str, Callable[[bool, Dict[str, Any], Callable[[~_SupportsRat, ~_SupportsRat], ~_SupportsRat], Callable[[Any], ~_SupportsRat]], ~_SupportsRat]] = <factory>)

AtVector(vector: SupportsVector[_T], index: int) → _T

FoldVector(function: Callable[[_S, _T], _T], initial: _T, vector: SupportsVector[_S]) → _T

Int(value: SupportsInt) → int

MapVector(function: Callable[[_S], _T], vector: SupportsVector[_S]) → Tuple[_T, ...]

Nat(value: SupportsInt) → int

Rat(value: SupportsFloat) → float

Vector(*values: _T) → Tuple[_T, ...]

ZipWithVector(function: Callable[[_S, _T], _U], vector1: SupportsVector[_S], vector2: SupportsVector[_T]) → Tuple[_U, ...]

optimisers: Dict[str, Callable[[bool, Dict[str, Any], Callable[[_SupportsRat, _SupportsRat], _SupportsRat], Callable[[Any], _SupportsRat]], _SupportsRat]]

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

builtins: ABCBuiltins[Any, Any, Any]

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

classmethod from_builtins(builtins: ABCBuiltins[Any, Any, Any]) → Self

classmethod from_optimisers(optimisers: Dict[str, Callable[[bool, Dict[str, Any], Callable[[Any, Any], Any], Callable[[Any], Any]], Any]]) → Self

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.load_loss_function(path: str | Path, property_name: str, *, target: DifferentiableLogic = DifferentiableLogic.Vehicle, optimisers: Dict[str, Callable[[bool, Dict[str, Any], Callable[[Any, Any], Any], Callable[[Any], Any]], Any]] = {}) → Any

Load a loss function from a property in a Vehicle specification.

Parameters:

path (str | Path) – The path to the Vehicle specification file.
property_name (str) – The name of the Vehicle property to load.
target (DifferentiableLogic) – The differentiable logic to use for interpreting the Vehicle property as a loss function, defaults to the Vehicle logic.
samplers – A map from quantified variable names to samplers for their values. See Sampler for more details.

Returns:

A function that takes the required external resources in the specification as keyword arguments and returns the loss corresponding to the property.

Return type:

Any

`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