Query Imandra via HTTP. See also https://github.com/aestheticIntegration/bs-imandra-client for a sample client implementation and OCaml API types.
The imandra_http_api_client
package is automatically generated by the OpenAPI Generator project:
- API version: 0.0.1
- Package version: 1.0.0
- Build package: org.openapitools.codegen.languages.PythonClientCodegen
Python 3.7+
This python library package is generated without supporting files like setup.py or requirements files
To be able to use it, you will need these dependencies in your own package that uses this library:
- urllib3 >= 1.25.3
- python-dateutil
- pydantic
- aenum
In your own code, to use this library to connect and interact with imandra-http-api-client, you can run the following:
import time
import imandra_http_api_client
from imandra_http_api_client.rest import ApiException
from pprint import pprint
# Defining the host is optional and defaults to http://localhost:3000
# See configuration.py for a list of all supported configuration parameters.
configuration = imandra_http_api_client.Configuration(
host = "http://localhost:3000"
)
# The client must configure the authentication and authorization parameters
# in accordance with the API server security policy.
# Examples for each auth method are provided below, use the example that
# satisfies your auth use case.
# Configure Bearer authorization: bearerAuth
configuration = imandra_http_api_client.Configuration(
access_token = os.environ["BEARER_TOKEN"]
)
# Enter a context with an instance of the API client
with imandra_http_api_client.ApiClient(configuration) as api_client:
# Create an instance of the API class
api_instance = imandra_http_api_client.DefaultApi(api_client)
eval_request_src = imandra_http_api_client.EvalRequestSrc(src="let f x = x + 1")
try:
# Evaluate a string of source code
api_response = api_instance.eval(eval_request_src)
print("The response of DefaultApi->eval:\n")
pprint(api_response)
except ApiException as e:
print("Exception when calling DefaultApi->eval: %s\n" % e)
All URIs are relative to http://localhost:3000
Class | Method | HTTP request | Description |
---|---|---|---|
DefaultApi | eval | POST /eval/by-src | Evaluate a string of source code |
DefaultApi | decompose | POST /decompose | Region decomposition of a function |
DefaultApi | get_history | GET /history | Get a text version of the Logic History |
DefaultApi | get_status | GET /status | Get server status |
DefaultApi | instance_by_name | POST /instance/by-name | Search for an instance from a property (boolean function) by name. (The name should exist from a previous call to `/eval`). This is the more 'primitive' call - calls to //by-src are for convenience and use Imandra_util.gensym to assign a name to your `src` block first, and then act by_name, so give this endpoint a try if you're having issues with //by-src. |
DefaultApi | instance_by_src | POST /instance/by-src | Obtain an instance from a property (boolean function) from lambda expression source |
DefaultApi | reset | POST /reset | Reset Imandra internal state |
DefaultApi | shutdown | POST /shutdown | Shutdown the server |
DefaultApi | verify_by_name | POST /verify/by-name | Verify a property (boolean function) by name. (The name should exist from a previous call to `/eval`). This is the more 'primitive' call - calls to //by-src are for convenience and use Imandra_util.gensym to assign a name to your `src` block first, and then act by_name, so give this endpoint a try if you're having issues with //by-src. |
DefaultApi | verify_by_src | POST /verify/by-src | Verify a property (boolean function) from lambda expression source |
- EvalRequestSrc
- EvalResponse
- DecomposeRegion
- DecomposeRequestSrc
- DecomposeResult
- Hints
- InductFunctionalBody
- InductStructuralBody
- InductStructuralStyle
- InductType
- InstanceRequestName
- InstanceRequestSrc
- InstanceResponse
- InstanceResult
- InstanceType
- Method
- MethodBody
- MethodExtSolverBody
- MethodInductBody
- MethodInductBodyBody
- MethodType
- MethodUnrollBody
- PrinterDetails
- ResponseError
- ResponseInstance
- ResponseModel
- Syntax
- UpToBody
- VerifyRequestName
- VerifyRequestSrc
- VerifyResponse
- VerifyResponseBody
- VerifyResult
- WithInstanceBody
- WithUnknownReasonBody
Authentication schemes defined for the API:
- Type: Bearer authentication