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.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.IndexType
- class vehicle_lang.ast.Indices
- 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.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.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.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)
- 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
- ConsList(item: _T, iterable: SupportsList[_T]) SupportsList[_T]
- abstract ConsVector(item: _T, vector: SupportsVector[_T]) SupportsVector[_T]
- DivRat(x: _SupportsRat, y: _SupportsRat) _SupportsRat
- Index(value: SupportsInt) int
- abstract Int(value: SupportsInt) _SupportsInt
- 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
- NegInt(x: _SupportsInt) _SupportsInt
- NegRat(x: _SupportsRat) _SupportsRat
- NilList() SupportsList[_T]
- Optimise(name: str, minimise: bool, context: Dict[str, Any], joiner: Callable[[Any, Any], Any], predicate: Callable[[Any], Any]) Any
- PowRat(x: _SupportsRat, y: _SupportsInt) _SupportsRat
- abstract Rat(value: SupportsFloat) _SupportsRat
- SubInt(x: _SupportsInt, y: _SupportsInt) _SupportsInt
- SubRat(x: _SupportsRat, y: _SupportsRat) _SupportsRat
- abstract Vector(*values: _T) SupportsVector[_T]
- class vehicle_lang.compile.abc.ABCTranslation
-
- abstract translate_DefFunction(declaration: DefFunction) _Declaration
- abstract translate_DefPostulate(declaration: DefPostulate) _Declaration
- abstract translate_PartialApp(expression: PartialApp) _Expression
- translate_declaration(declaration: Declaration) _Declaration
- translate_expression(expression: Expression) _Expression
- class vehicle_lang.compile.abc.Translation
- abstract translate_declaration(declaration: Declaration) _Declaration
- abstract translate_expression(expression: Expression) _Expression
vehicle_lang.compile.abcboolasbool
vehicle_lang.compile.abcnumeric
vehicle_lang.compile.python
- class vehicle_lang.compile.python.AST
- class vehicle_lang.compile.python.Binder(provenance: vehicle_lang.ast.Provenance, name: str | None, type: vehicle_lang.ast.Expression)
- provenance: Provenance
- type: Expression
- class vehicle_lang.compile.python.BuiltinFunction
- 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)
- class vehicle_lang.compile.python.PythonBuiltins(optimisers: Dict[str, Callable[[bool, Dict[str, Any], Callable[[~_SupportsRat, ~_SupportsRat], ~_SupportsRat], Callable[[Any], ~_SupportsRat]], ~_SupportsRat]] = <factory>)
- ConsVector(item: _T, vector: SupportsVector[_T]) SupportsVector[_T]
- Int(value: SupportsInt) int
- Nat(value: SupportsInt) int
- Rat(value: SupportsFloat) float
- 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
- translate_DefFunction(declaration: DefFunction) stmt
- translate_DefPostulate(declaration: DefPostulate) stmt
- translate_PartialApp(expression: PartialApp) expr
- 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:
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.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.