Vehicle
v0.9.0
Installation
The Vehicle specification language
Type checking a specification
Training with a specification
Verifying a specification
Exporting a specification to an ITP
Python API
Developer documentation
Vehicle
Index
Edit on GitHub
Index
Symbols
|
A
|
B
|
C
|
D
|
E
|
F
|
G
|
I
|
L
|
M
|
N
|
O
|
P
|
Q
|
R
|
S
|
T
|
U
|
V
|
Y
|
Z
Symbols
--cache
command line option
,
[1]
--dataset
command line option
--modulePrefix
command line option
--network
command line option
--output
command line option
--outputFile
command line option
--parameter
command line option
--property
command line option
--specification
command line option
,
[1]
,
[2]
--target
command line option
,
[1]
--typeSystem
command line option
--verifier
command line option
,
[1]
--verifierLocation
command line option
,
[1]
-c
command line option
,
[1]
-d
command line option
-l
command line option
,
[1]
-m
command line option
-n
command line option
-o
command line option
,
[1]
-p
command line option
,
[1]
-s
command line option
,
[1]
-t
command line option
,
[1]
,
[2]
-v
command line option
,
[1]
-y
command line option
A
ABCBoolAsBoolBuiltins (class in vehicle_lang.compile.abcboolasbool)
ABCNumericBuiltins (class in vehicle_lang.compile.abcnumeric)
ABCTranslation (class in vehicle_lang.compile.abc)
AddInt (class in vehicle_lang.ast)
AddInt() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcnumeric.ABCNumericBuiltins method)
AddNat (class in vehicle_lang.ast)
AddNat() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcnumeric.ABCNumericBuiltins method)
AddRat (class in vehicle_lang.ast)
AddRat() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcnumeric.ABCNumericBuiltins method)
And (class in vehicle_lang.ast)
And() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcboolasbool.ABCBoolAsBoolBuiltins method)
App (class in vehicle_lang.ast)
AST (class in vehicle_lang.ast)
(class in vehicle_lang.compile)
AtVector (class in vehicle_lang.ast)
AtVector() (vehicle_lang.compile.abc.Builtins method)
B
Binder (class in vehicle_lang.ast)
(class in vehicle_lang.compile)
Bool (class in vehicle_lang.ast)
Bool() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcboolasbool.ABCBoolAsBoolBuiltins method)
BoolType (class in vehicle_lang.ast)
BoundVar (class in vehicle_lang.ast)
Builtin (class in vehicle_lang.ast)
BuiltinFunction (class in vehicle_lang.ast)
(class in vehicle_lang.compile)
Builtins (class in vehicle_lang.compile.abc)
builtins (vehicle_lang.compile.python.PythonTranslation attribute)
(vehicle_lang.compile.PythonTranslation attribute)
C
col_offset (vehicle_lang.ast.Provenance attribute)
(vehicle_lang.compile.Provenance attribute)
command line option
--cache
,
[1]
--dataset
--modulePrefix
--network
--output
--outputFile
--parameter
--property
--specification
,
[1]
,
[2]
--target
,
[1]
--typeSystem
--verifier
,
[1]
--verifierLocation
,
[1]
-c
,
[1]
-d
-l
,
[1]
-m
-n
-o
,
[1]
-p
,
[1]
-s
,
[1]
-t
,
[1]
,
[2]
-v
,
[1]
-y
compile() (in module vehicle_lang.compile)
(vehicle_lang.compile.python.PythonTranslation method)
(vehicle_lang.compile.PythonTranslation method)
ConsList (class in vehicle_lang.ast)
ConsList() (vehicle_lang.compile.abc.Builtins method)
ConsVector (class in vehicle_lang.ast)
ConsVector() (vehicle_lang.compile.abc.Builtins method)
D
Declaration (class in vehicle_lang.ast)
(class in vehicle_lang.compile)
DeclarationName (in module vehicle_lang.typing)
DefFunction (class in vehicle_lang.ast)
DefPostulate (class in vehicle_lang.ast)
DifferentiableLogic (class in vehicle_lang)
(class in vehicle_lang.typing)
DivRat (class in vehicle_lang.ast)
DivRat() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcnumeric.ABCNumericBuiltins method)
DL2 (vehicle_lang.typing.DifferentiableLogic attribute)
E
end_col_offset (vehicle_lang.ast.Provenance attribute)
(vehicle_lang.compile.Provenance attribute)
end_lineno (vehicle_lang.ast.Provenance attribute)
(vehicle_lang.compile.Provenance attribute)
EqIndex (class in vehicle_lang.ast)
EqIndex() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcboolasbool.ABCBoolAsBoolBuiltins method)
EqInt (class in vehicle_lang.ast)
EqInt() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcboolasbool.ABCBoolAsBoolBuiltins method)
EqNat (class in vehicle_lang.ast)
EqNat() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcboolasbool.ABCBoolAsBoolBuiltins method)
EqRat (class in vehicle_lang.ast)
EqRat() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcboolasbool.ABCBoolAsBoolBuiltins method)
EraseType
Exists (class in vehicle_lang.ast)
Exists() (vehicle_lang.compile.abc.Builtins method)
Explicit (class in vehicle_lang.typing)
(vehicle_lang.typing.Explicit attribute)
Expression (class in vehicle_lang.ast)
(class in vehicle_lang.compile)
F
FoldList (class in vehicle_lang.ast)
FoldList() (vehicle_lang.compile.abc.Builtins method)
FoldVector (class in vehicle_lang.ast)
FoldVector() (vehicle_lang.compile.abc.Builtins method)
Forall (class in vehicle_lang.ast)
Forall() (vehicle_lang.compile.abc.Builtins method)
FreeVar (class in vehicle_lang.ast)
from_builtins() (vehicle_lang.compile.python.PythonTranslation class method)
(vehicle_lang.compile.PythonTranslation class method)
from_dict() (vehicle_lang.compile.AST class method)
(vehicle_lang.compile.Program class method)
from_json() (vehicle_lang.compile.AST class method)
from_samplers() (vehicle_lang.compile.python.PythonTranslation class method)
(vehicle_lang.compile.PythonTranslation class method)
G
GeIndex (class in vehicle_lang.ast)
GeIndex() (vehicle_lang.compile.abc.Builtins method)
GeInt (class in vehicle_lang.ast)
GeInt() (vehicle_lang.compile.abc.Builtins method)
GeNat (class in vehicle_lang.ast)
GeNat() (vehicle_lang.compile.abc.Builtins method)
GeRat (class in vehicle_lang.ast)
GeRat() (vehicle_lang.compile.abc.Builtins method)
get_name() (vehicle_lang.compile.Declaration method)
Godel (vehicle_lang.typing.DifferentiableLogic attribute)
GtIndex (class in vehicle_lang.ast)
GtIndex() (vehicle_lang.compile.abc.Builtins method)
GtInt (class in vehicle_lang.ast)
GtInt() (vehicle_lang.compile.abc.Builtins method)
GtNat (class in vehicle_lang.ast)
GtNat() (vehicle_lang.compile.abc.Builtins method)
GtRat (class in vehicle_lang.ast)
GtRat() (vehicle_lang.compile.abc.Builtins method)
I
If (class in vehicle_lang.ast)
If() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcboolasbool.ABCBoolAsBoolBuiltins method)
ignored_types (vehicle_lang.compile.python.PythonTranslation attribute)
(vehicle_lang.compile.PythonTranslation attribute)
Implies (class in vehicle_lang.ast)
Implies() (vehicle_lang.compile.abc.Builtins method)
Index (class in vehicle_lang.ast)
Index() (vehicle_lang.compile.abc.Builtins method)
IndexType (class in vehicle_lang.ast)
Indices (class in vehicle_lang.ast)
Indices() (vehicle_lang.compile.abc.Builtins method)
Int (class in vehicle_lang.ast)
Int() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.python.PythonBuiltins method)
(vehicle_lang.compile.PythonBuiltins method)
IntType (class in vehicle_lang.ast)
L
Lam (class in vehicle_lang.ast)
LeIndex (class in vehicle_lang.ast)
LeIndex() (vehicle_lang.compile.abc.Builtins method)
LeInt (class in vehicle_lang.ast)
LeInt() (vehicle_lang.compile.abc.Builtins method)
LeNat (class in vehicle_lang.ast)
LeNat() (vehicle_lang.compile.abc.Builtins method)
LeRat (class in vehicle_lang.ast)
LeRat() (vehicle_lang.compile.abc.Builtins method)
Let (class in vehicle_lang.ast)
lineno (vehicle_lang.ast.Provenance attribute)
(vehicle_lang.compile.Provenance attribute)
ListType (class in vehicle_lang.ast)
load() (in module vehicle_lang.ast)
load_loss_function() (in module vehicle_lang)
(in module vehicle_lang.compile)
LtIndex (class in vehicle_lang.ast)
LtIndex() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcboolasbool.ABCBoolAsBoolBuiltins method)
LtInt (class in vehicle_lang.ast)
LtInt() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcboolasbool.ABCBoolAsBoolBuiltins method)
LtNat (class in vehicle_lang.ast)
LtNat() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcboolasbool.ABCBoolAsBoolBuiltins method)
LtRat (class in vehicle_lang.ast)
LtRat() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcboolasbool.ABCBoolAsBoolBuiltins method)
Lukasiewicz (vehicle_lang.typing.DifferentiableLogic attribute)
M
Main (class in vehicle_lang.ast)
MapList (class in vehicle_lang.ast)
MapList() (vehicle_lang.compile.abc.Builtins method)
MapVector (class in vehicle_lang.ast)
MapVector() (vehicle_lang.compile.abc.Builtins method)
Marabou (vehicle_lang.typing.Verifier attribute)
(vehicle_lang.Verifier attribute)
MaxRat (class in vehicle_lang.ast)
MaxRat() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcnumeric.ABCNumericBuiltins method)
MinRat (class in vehicle_lang.ast)
MinRat() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcnumeric.ABCNumericBuiltins method)
MISSING (in module vehicle_lang.ast)
module
vehicle_lang.ast
vehicle_lang.compile
vehicle_lang.compile.abc
vehicle_lang.compile.abcboolasbool
vehicle_lang.compile.abcnumeric
vehicle_lang.compile.python
vehicle_lang.error
vehicle_lang.typing
module_footer (vehicle_lang.compile.python.PythonTranslation attribute)
(vehicle_lang.compile.PythonTranslation attribute)
module_header (vehicle_lang.compile.python.PythonTranslation attribute)
(vehicle_lang.compile.PythonTranslation attribute)
MulInt (class in vehicle_lang.ast)
MulInt() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcnumeric.ABCNumericBuiltins method)
MulNat (class in vehicle_lang.ast)
MulNat() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcnumeric.ABCNumericBuiltins method)
MulRat (class in vehicle_lang.ast)
MulRat() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcnumeric.ABCNumericBuiltins method)
N
name (vehicle_lang.compile.Binder attribute)
Nat (class in vehicle_lang.ast)
Nat() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.python.PythonBuiltins method)
(vehicle_lang.compile.PythonBuiltins method)
NatType (class in vehicle_lang.ast)
NegInt (class in vehicle_lang.ast)
NegInt() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcnumeric.ABCNumericBuiltins method)
NegRat (class in vehicle_lang.ast)
NegRat() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcnumeric.ABCNumericBuiltins method)
NeIndex (class in vehicle_lang.ast)
NeIndex() (vehicle_lang.compile.abc.Builtins method)
NeInt (class in vehicle_lang.ast)
NeInt() (vehicle_lang.compile.abc.Builtins method)
NeNat (class in vehicle_lang.ast)
NeNat() (vehicle_lang.compile.abc.Builtins method)
NeRat (class in vehicle_lang.ast)
NeRat() (vehicle_lang.compile.abc.Builtins method)
NilList (class in vehicle_lang.ast)
NilList() (vehicle_lang.compile.abc.Builtins method)
Not (class in vehicle_lang.ast)
Not() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcboolasbool.ABCBoolAsBoolBuiltins method)
O
Or (class in vehicle_lang.ast)
Or() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcboolasbool.ABCBoolAsBoolBuiltins method)
P
PartialApp (class in vehicle_lang.ast)
Pi (class in vehicle_lang.ast)
PowRat (class in vehicle_lang.ast)
PowRat() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcnumeric.ABCNumericBuiltins method)
Product (vehicle_lang.typing.DifferentiableLogic attribute)
Program (class in vehicle_lang.ast)
(class in vehicle_lang.compile)
Provenance (class in vehicle_lang.ast)
(class in vehicle_lang.compile)
provenance (vehicle_lang.compile.Binder attribute)
py_app() (in module vehicle_lang.compile.python)
py_binder() (in module vehicle_lang.compile.python)
py_builtin() (in module vehicle_lang.compile.python)
py_name() (in module vehicle_lang.compile.python)
py_partial_app() (in module vehicle_lang.compile.python)
py_qualified_name() (in module vehicle_lang.compile.python)
PythonBuiltins (class in vehicle_lang.compile)
(class in vehicle_lang.compile.python)
PythonTranslation (class in vehicle_lang.compile)
(class in vehicle_lang.compile.python)
Q
QuantifiedVariableName (in module vehicle_lang.typing)
R
Rat (class in vehicle_lang.ast)
Rat() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.python.PythonBuiltins method)
(vehicle_lang.compile.PythonBuiltins method)
RatType (class in vehicle_lang.ast)
S
Sample (class in vehicle_lang.ast)
Sample() (vehicle_lang.compile.abc.Builtins method)
samplers (vehicle_lang.compile.abc.Builtins attribute)
(vehicle_lang.compile.abcboolasbool.ABCBoolAsBoolBuiltins attribute)
(vehicle_lang.compile.abcnumeric.ABCNumericBuiltins attribute)
(vehicle_lang.compile.python.PythonBuiltins attribute)
(vehicle_lang.compile.PythonBuiltins attribute)
SubInt (class in vehicle_lang.ast)
SubInt() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcnumeric.ABCNumericBuiltins method)
SubRat (class in vehicle_lang.ast)
SubRat() (vehicle_lang.compile.abc.Builtins method)
(vehicle_lang.compile.abcnumeric.ABCNumericBuiltins method)
T
Target (class in vehicle_lang.typing)
translate_App() (vehicle_lang.compile.abc.ABCTranslation method)
(vehicle_lang.compile.python.PythonTranslation method)
(vehicle_lang.compile.PythonTranslation method)
translate_binder() (vehicle_lang.compile.python.PythonTranslation method)
(vehicle_lang.compile.PythonTranslation method)
translate_BoundVar() (vehicle_lang.compile.abc.ABCTranslation method)
(vehicle_lang.compile.python.PythonTranslation method)
(vehicle_lang.compile.PythonTranslation method)
translate_Builtin() (vehicle_lang.compile.abc.ABCTranslation method)
(vehicle_lang.compile.python.PythonTranslation method)
(vehicle_lang.compile.PythonTranslation method)
translate_declaration() (vehicle_lang.compile.abc.ABCTranslation method)
(vehicle_lang.compile.abc.Translation method)
translate_declarations() (vehicle_lang.compile.python.PythonTranslation method)
(vehicle_lang.compile.PythonTranslation method)
translate_DefFunction() (vehicle_lang.compile.abc.ABCTranslation method)
(vehicle_lang.compile.python.PythonTranslation method)
(vehicle_lang.compile.PythonTranslation method)
translate_DefPostulate() (vehicle_lang.compile.abc.ABCTranslation method)
(vehicle_lang.compile.python.PythonTranslation method)
(vehicle_lang.compile.PythonTranslation method)
translate_expression() (vehicle_lang.compile.abc.ABCTranslation method)
(vehicle_lang.compile.abc.Translation method)
translate_FreeVar() (vehicle_lang.compile.abc.ABCTranslation method)
(vehicle_lang.compile.python.PythonTranslation method)
(vehicle_lang.compile.PythonTranslation method)
translate_Lam() (vehicle_lang.compile.abc.ABCTranslation method)
(vehicle_lang.compile.python.PythonTranslation method)
(vehicle_lang.compile.PythonTranslation method)
translate_Let() (vehicle_lang.compile.abc.ABCTranslation method)
translate_Main() (vehicle_lang.compile.abc.ABCTranslation method)
(vehicle_lang.compile.python.PythonTranslation method)
(vehicle_lang.compile.PythonTranslation method)
translate_PartialApp() (vehicle_lang.compile.abc.ABCTranslation method)
(vehicle_lang.compile.python.PythonTranslation method)
(vehicle_lang.compile.PythonTranslation method)
translate_Pi() (vehicle_lang.compile.abc.ABCTranslation method)
(vehicle_lang.compile.python.PythonTranslation method)
(vehicle_lang.compile.PythonTranslation method)
translate_program() (vehicle_lang.compile.abc.ABCTranslation method)
(vehicle_lang.compile.abc.Translation method)
translate_Universe() (vehicle_lang.compile.abc.ABCTranslation method)
(vehicle_lang.compile.python.PythonTranslation method)
(vehicle_lang.compile.PythonTranslation method)
Translation (class in vehicle_lang.compile.abc)
type (vehicle_lang.compile.Binder attribute)
U
Unit (class in vehicle_lang.ast)
Unit() (vehicle_lang.compile.abc.Builtins method)
UnitType (class in vehicle_lang.ast)
Universe (class in vehicle_lang.ast)
V
Vector (class in vehicle_lang.ast)
Vector() (vehicle_lang.compile.abc.Builtins method)
VectorType (class in vehicle_lang.ast)
Vehicle (vehicle_lang.typing.DifferentiableLogic attribute)
vehicle_lang.ast
module
vehicle_lang.compile
module
vehicle_lang.compile.abc
module
vehicle_lang.compile.abcboolasbool
module
vehicle_lang.compile.abcnumeric
module
vehicle_lang.compile.python
module
vehicle_lang.error
module
vehicle_lang.typing
module
VehicleBuiltinUnsupported
VehicleError
VehicleInternalError
VehiclePropertyNotFound
VehicleSessionClosed
VehicleSessionUsed
Verifier (class in vehicle_lang)
(class in vehicle_lang.typing)
verify() (in module vehicle_lang)
Y
Yager (vehicle_lang.typing.DifferentiableLogic attribute)
Z
ZipWithVector (class in vehicle_lang.ast)
ZipWithVector() (vehicle_lang.compile.abc.Builtins method)
Read the Docs
v: v0.9.0
Versions
latest
stable
v0.9.0
v0.8.0
v0.7.0
v0.6.0
v0.5.1
v0.5.0
v0.4.1
v0.4.0
v0.3.3
v0.3.2
0.3.1
v0.3.0
v0.2.0
v0.1.0
Downloads
On Read the Docs
Project Home
Builds