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.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)
- 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>)
- compile(program: Program, path: str | Path, declaration_context: Dict[str, Any] = {}) Dict[str, Any]
- 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.py_app(function: expr, *arguments: expr, provenance: Provenance) expr
Make a function call.
- 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. 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.