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.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]
- 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>)
- 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
- 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. Ifnew_state
is a string, it is pushed on the stack. This ensure the new current state isnew_state
. Ifnew_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 becombined('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.