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

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.Sample(name: str, locals: Sequence[str])

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

class vehicle_lang.compile.AST

classmethod from_json(value: str) → Self

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

class vehicle_lang.compile.Declaration

abstract get_name() → str

class vehicle_lang.compile.Expression

class vehicle_lang.compile.Program

class vehicle_lang.compile.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.PythonBuiltins(samplers: Dict[str, Callable[[Dict[str, Any]], Iterator[Any]]] = <factory>)

Int(value: SupportsInt) → int

Nat(value: SupportsInt) → int

Rat(value: SupportsFloat) → float

samplers: Dict[str, Callable[[Dict[str, Any]], Iterator[Any]]]

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

builtins: Builtins[Any, Any, Any, Any]

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

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

classmethod from_samplers(samplers: Dict[str, Callable[[Dict[str, Any]], Iterator[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.compile(path: str | Path, *, declarations: Iterable[str] = (), target: Target = Explicit.Explicit, translation: PythonTranslation | None = None) → Dict[str, Any]

vehicle_lang.compile.load_loss_function(path: str | Path, property_name: str, *, target: DifferentiableLogic = DifferentiableLogic.Vehicle, samplers: Dict[str, Callable[[Dict[str, Any]], Iterator[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 (Dict[str, Callable[[Dict[str, Any]], Iterator[Any]]]) – 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.compile.abc`

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

abstract AddInt(x: _Int, y: _Int) → _Int

abstract AddNat(x: _Nat, y: _Nat) → _Nat

abstract AddRat(x: _Rat, y: _Rat) → _Rat

abstract And(x: _Bool, y: _Bool) → _Bool

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

abstract Bool(value: bool) → _Bool

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

ConsVector(item: _T, vector: SupportsVector[_T]) → SupportsVector[_T]

abstract DivRat(x: _Rat, y: _Rat) → _Rat

abstract EqIndex(x: int, y: int) → _Bool

abstract EqInt(x: _Int, y: _Int) → _Bool

abstract EqNat(x: _Nat, y: _Nat) → _Bool

abstract EqRat(x: _Rat, y: _Rat) → _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

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: _Int, y: _Int) → _Bool

GeNat(x: _Nat, y: _Nat) → _Bool

GeRat(x: _Rat, y: _Rat) → _Bool

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

GtInt(x: _Int, y: _Int) → _Bool

GtNat(x: _Nat, y: _Nat) → _Bool

GtRat(x: _Rat, y: _Rat) → _Bool

abstract 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) → _Int

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

LeInt(x: _Int, y: _Int) → _Bool

LeNat(x: _Nat, y: _Nat) → _Bool

LeRat(x: _Rat, y: _Rat) → _Bool

abstract LtIndex(x: int, y: int) → _Bool

abstract LtInt(x: _Int, y: _Int) → _Bool

abstract LtNat(x: _Nat, y: _Nat) → _Bool

abstract LtRat(x: _Rat, y: _Rat) → _Bool

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

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

abstract MaxRat(x: _Rat, y: _Rat) → _Rat

abstract MinRat(x: _Rat, y: _Rat) → _Rat

abstract MulInt(x: _Int, y: _Int) → _Int

abstract MulNat(x: _Nat, y: _Nat) → _Nat

abstract MulRat(x: _Rat, y: _Rat) → _Rat

abstract Nat(value: SupportsInt) → _Nat

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

NeInt(x: _Int, y: _Int) → _Bool

NeNat(x: _Nat, y: _Nat) → _Bool

NeRat(x: _Rat, y: _Rat) → _Bool

abstract NegInt(x: _Int) → _Int

abstract NegRat(x: _Rat) → _Rat

NilList() → SupportsVector[_T]

abstract Not(x: _Bool) → _Bool

abstract Or(x: _Bool, y: _Bool) → _Bool

abstract PowRat(x: _Rat, y: _Int) → _Rat

abstract Rat(value: SupportsFloat) → _Rat

Sample(name: str, context: Dict[str, Any]) → SupportsList[_T]

abstract SubInt(x: _Int, y: _Int) → _Int

abstract SubRat(x: _Rat, y: _Rat) → _Rat

Unit() → Tuple[()]

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

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

samplers: Dict[str, Callable[[Dict[str, Any]], Iterator[Any]]]

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

class vehicle_lang.compile.abcboolasbool.ABCBoolAsBoolBuiltins(samplers: Dict[str, Callable[[Dict[str, Any]], Iterator[Any]]] = <factory>)

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

Bool(value: bool) → bool

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

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

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

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

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

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

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

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

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

Not(x: bool) → bool

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

samplers: Dict[str, Callable[[Dict[str, Any]], Iterator[Any]]]

`vehicle_lang.compile.abcnumeric`

class vehicle_lang.compile.abcnumeric.ABCNumericBuiltins(samplers: Dict[str, Callable[[Dict[str, Any]], Iterator[Any]]] = <factory>)

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

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

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

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

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

NegInt(x: _SupportsInt) → _SupportsInt

NegRat(x: _SupportsRat) → _SupportsRat

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

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

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

samplers: Dict[str, Callable[[Dict[str, Any]], Iterator[Any]]]

`vehicle_lang.compile.python`

exception vehicle_lang.compile.python.EraseType

class vehicle_lang.compile.python.PythonBuiltins(samplers: Dict[str, Callable[[Dict[str, Any]], Iterator[Any]]] = <factory>)

Int(value: SupportsInt) → int

Nat(value: SupportsInt) → int

Rat(value: SupportsFloat) → float

samplers: Dict[str, Callable[[Dict[str, Any]], Iterator[Any]]]

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

builtins: Builtins[Any, Any, Any, Any]

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

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

classmethod from_samplers(samplers: Dict[str, Callable[[Dict[str, Any]], Iterator[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.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_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.pygments`

`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.VehicleBuiltinUnsupported(builtin_name: str)

builtin_name: str

exception vehicle_lang.error.VehicleError

exception vehicle_lang.error.VehicleInternalError

exception vehicle_lang.error.VehiclePropertyNotFound(property_name: str)

property_name: str

exception vehicle_lang.error.VehicleSessionClosed

exception vehicle_lang.error.VehicleSessionUsed

`vehicle_lang.typing`

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