| Name | imandra JSON |
| Version |
2.0.0
JSON |
| download |
| home_page | None |
| Summary | A CLI and API client library for interfacing with Imandra's web APIs |
| upload_time | 2025-02-06 13:31:14 |
| maintainer | None |
| docs_url | None |
| author | None |
| requires_python | None |
| license | None |
| keywords |
imandra
|
| VCS |
|
| bugtrack_url |
|
| requirements |
No requirements were recorded.
|
| Travis-CI |
No Travis.
|
| coveralls test coverage |
No coveralls.
|
# Imandra CLI and API client library
[Imandra](https://www.imandra.ai) is a cloud-native automated reasoning engine for analysis of algorithms and data.
This package contains the `imandra` Python library for interacting with Imandra's web APIs. It includes:
- `imandra.core`, which provides programmatic access to Imandra X, Imandra's core reasoning engine.
- `imandra.u.agents.*` and `imandra.u.reasoners.*`, bindings to Imandra Universe Agents and Reasoners.
- `imandra.ipl`, tools for analysing Imandra Protocol Language (IPL) files.
If you're interested in developing Imandra X or IPL models, you may also want to see the [Imandra documentation](https://docs.imandra.ai/).
The `imandra` python API reference documentation is available [here](https://docs.imandra.ai/imandra-docs/python/imandra/).
## Authentication
First obtain an API key from https://universe.imandra.ai.
The Python library will read the API key from the first of:
1. The `api_key` parameter passed when instantiating a `Client`.
2. The `IMANDRA_API_KEY` environment variable.
3. The file `$HOME/.config/imandra/api_key` (MacOS and Linux) or `%USERPROFILE%\AppData\Local\imandra\api_key` (Windows)
## Example: Imandra Core
First, ensure dependencies for the `core` module are installed. Note that `imandra.core` requires Python >= 3.12.
```
$ pip install 'imandra[core]'
```
```
$ ipython
...
In [1]: from imandra.core import Client
In [2]: client = Client()
In [3]: client.eval_src('let f x = if x > 0 then if x * x < 0 then x else x + 1 else x')
Out[3]: success: true
In [4]: result = client.verify_src('fun x -> x > 0 ==> f x > 0')
In [5]: result
Out[5]:
proved {
proof_pp: "..."
}
In [6]: print(result.proved.proof_pp)
{ id = 1; concl = `|- x > 0 ==> f x > 0`;
view =
T_deduction {
premises =
[("p",
[{ id = 0; concl = `|- x > 0 ==> f x > 0`;
view = T_deduction {premises = []} }
])
]}
}
In [7]: result = client.instance_src('fun x -> f x = 43')
In [8]: result
Out[8]:
sat {
model {
m_type: Instance
src: "module M = struct\n\n let x = 42\n\n end\n"
artifact {
kind: "cir.model"
data: "..."
api_version: "v8"
}
}
}
In [9]: print(result.sat.model.src)
module M = struct
let x = 42
end
In [10]: result = client.decompose('f')
In [11]: result
Out[11]:
artifact {
kind: "cir.fun_decomp"
data: "..."
api_version: "v8"
}
regions_str {
constraints_str: "not (x > 0)"
invariant_str: "x"
model_str {
k: "x"
v: "0"
}
}
regions_str {
constraints_str: "not (x * x < 0)"
constraints_str: "x > 0"
invariant_str: "x + 1"
model_str {
k: "x"
v: "1"
}
}
task {
id {
id: "task:decomp:rE3VSX-t5kbrrAksQ4saBrMUs2uHTXfu-CqeZunV9aE="
}
kind: TASK_DECOMP
}
```
## Example: Imandra Universe reasoners
```
$ pip install imandra
```
```
$ ipython
In [1]: from imandra.u.reasoners.prover9 import Client
In [2]: client = Client()
In [3]: input = "formulas(sos).\n\n e * x = x.\n x'\'' * x = e.\n (x * y) * z = x * (y * z).\n\n x * x = e.\n\nend_of_list.\n\nformulas(goals).\n\n x * y = y * x.\n\nend_of_list ...: ."
In [4]: result = client.eval(input)
In [5]: print(result['results'][0])
============================== Prover9 ===============================
Prover9 (64) version 2009-11A, November 2009.
Process 18 was started by universe on localhost,
Mon Jan 6 14:52:26 2025
The command was "/imandra-universe/prover9/bin/prover9 -t 45".
============================== end of head ===========================
============================== INPUT =================================
formulas(sos).
e * x = x.
x''' * x = e.
(x * y) * z = x * (y * z).
x * x = e.
end_of_list.
formulas(goals).
x * y = y * x.
end_of_list.
============================== end of input ==========================
...
============================== PROOF =================================
% Proof 1 at 0.01 (+ 0.00) seconds.
% Length of proof is 16.
% Level of proof is 7.
% Maximum clause weight is 11.000.
% Given clauses 12.
1 x * y = y * x # label(non_clause) # label(goal). [goal].
2 e * x = x. [assumption].
3 x''' * x = e. [assumption].
4 (x * y) * z = x * (y * z). [assumption].
5 x * x = e. [assumption].
6 c2 * c1 != c1 * c2. [deny(1)].
7 x''' * (x * y) = y. [para(3(a,1),4(a,1,1)),rewrite([2(2)]),flip(a)].
8 x * (x * y) = y. [para(5(a,1),4(a,1,1)),rewrite([2(2)]),flip(a)].
9 x * (y * (x * y)) = e. [para(5(a,1),4(a,1)),flip(a)].
11 x'''''' * e = x. [para(3(a,1),7(a,1,2))].
13 x''' * e = x. [para(5(a,1),7(a,1,2))].
15 x''' = x. [back_rewrite(11),rewrite([13(8)])].
16 x * e = x. [back_rewrite(13),rewrite([15(3)])].
19 x * (y * x) = y. [para(9(a,1),8(a,1,2)),rewrite([16(2)]),flip(a)].
24 x * y = y * x. [para(19(a,1),8(a,1,2))].
25 $F. [resolve(24,a,6,a)].
============================== end of proof ==========================
============================== STATISTICS ============================
Given=12. Generated=122. Kept=23. proofs=1.
Usable=8. Sos=3. Demods=12. Limbo=2, Disabled=14. Hints=0.
Kept_by_rule=0, Deleted_by_rule=0.
Forward_subsumed=99. Back_subsumed=0.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=21 (0 lex), Back_demodulated=9. Back_unit_deleted=0.
Demod_attempts=770. Demod_rewrites=156.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
Megabytes=0.06.
User_CPU=0.01, System_CPU=0.00, Wall_clock=0.
============================== end of statistics =====================
============================== end of search =========================
THEOREM PROVED
```
## Example: Imandra Universe agents
```
$ pip install imandra[universe]
```
```
$ ipython
In [1]: from imandra.u.agents import cogito
In [2]: from langchain_core.messages import HumanMessage
In [3]: g = cogito.get_remote_graph()
In [4]: cogito.create_thread_sync(g)
In [5]: g.invoke({'messages': [HumanMessage(content='hello')], 'tasks': []})
Out[5]:
{'messages': [{'content': "You are Cogito, agent within Imandra Universe - a cloud platform for accessing automated logical reasoners, tools and agents connected to them.",
'additional_kwargs': {},
'response_metadata': {},
'type': 'system',
'name': None,
'id': 'ae883182-17df-4ced-87e2-4b79b7777e93'},
{'content': 'hello',
'additional_kwargs': {'example': False,
'additional_kwargs': {},
'response_metadata': {}},
'response_metadata': {},
'type': 'human',
'name': None,
'id': 'c5491021-fec5-4e4a-8651-eda927d8e473',
'example': False},
{'content': 'Hello! How can I assist you today?',
'additional_kwargs': {},
'response_metadata': {},
'type': 'ai',
'name': 'supervisor',
'id': '52e4fd16-235a-4ac2-bdba-3a20d19870a3',
'example': False,
'tool_calls': [],
'invalid_tool_calls': [],
'usage_metadata': None}],
'tasks': []}
```
## Example: IPL
```
$ pip install imandra
```
```
$ ipython
In [1]: from imandra.ipl import Client
In [2]: client = Client()
In [3]: job_id = client.unsat_analysis('/path/to/model.ipl', None, None)
In [4]: client.status(job_id)
Out[4]: 'processing'
In [5]: client.wait(job_id)
Out[5]: 'done'
In [6]: data = client.data(job_id)
In [7]: print(data['content'].decode('ascii'))
For message flow `simple_orders_one`, unsat cores: []
```
## CLI
The `imandra` package also adds an entry point called `imandra-cli` which exposes the `imandra` library functionality in a more discoverable way:
```sh
$ python3 -m venv ./my/venv
...
$ ./my/venv/pip install imandra
...
$ ./my/venv/bin/imandra-cli --help
usage: imandra [-h] auth,ipl,core,rule-synth,cfb ...
Imandra CLI
positional arguments:
{auth,ipl,core,rule-synth,cfb}
optional arguments:
-h, --help show this help message and exit
```
On Windows, the entry point can be found as `.\my\venv\Scripts\imandra-cli.exe`.
### CLI Authentication
This is the first step to start using the Imandra CLI. Our cloud environment requires a user account, which you can setup like this:
```sh
$ ./my/venv/bin/imandra-cli auth login
```
and follow the prompts to authenticate. This will create the relevant credentials in `~/.imandra` (or `%APPDATA%\imandra` on Windows).
You should now be able to invoke CLI commands that require authentication.
Raw data
{
"_id": null,
"home_page": null,
"name": "imandra",
"maintainer": null,
"docs_url": null,
"requires_python": null,
"maintainer_email": null,
"keywords": "imandra",
"author": null,
"author_email": null,
"download_url": "https://files.pythonhosted.org/packages/4e/af/8a479f70c50356b3ead6f7edebab2e23f7a720f6aff22bcfe575393c223c/imandra-2.0.0.tar.gz",
"platform": null,
"description": "# Imandra CLI and API client library\n\n[Imandra](https://www.imandra.ai) is a cloud-native automated reasoning engine for analysis of algorithms and data.\n\nThis package contains the `imandra` Python library for interacting with Imandra's web APIs. It includes:\n\n- `imandra.core`, which provides programmatic access to Imandra X, Imandra's core reasoning engine.\n- `imandra.u.agents.*` and `imandra.u.reasoners.*`, bindings to Imandra Universe Agents and Reasoners.\n- `imandra.ipl`, tools for analysing Imandra Protocol Language (IPL) files.\n\nIf you're interested in developing Imandra X or IPL models, you may also want to see the [Imandra documentation](https://docs.imandra.ai/).\n\nThe `imandra` python API reference documentation is available [here](https://docs.imandra.ai/imandra-docs/python/imandra/).\n\n## Authentication\n\nFirst obtain an API key from https://universe.imandra.ai.\n\nThe Python library will read the API key from the first of:\n\n1. The `api_key` parameter passed when instantiating a `Client`.\n2. The `IMANDRA_API_KEY` environment variable.\n3. The file `$HOME/.config/imandra/api_key` (MacOS and Linux) or `%USERPROFILE%\\AppData\\Local\\imandra\\api_key` (Windows)\n\n\n## Example: Imandra Core\n\nFirst, ensure dependencies for the `core` module are installed. Note that `imandra.core` requires Python >= 3.12.\n\n```\n$ pip install 'imandra[core]'\n```\n\n```\n$ ipython\n...\nIn [1]: from imandra.core import Client\n\nIn [2]: client = Client()\n\nIn [3]: client.eval_src('let f x = if x > 0 then if x * x < 0 then x else x + 1 else x')\nOut[3]: success: true\n\nIn [4]: result = client.verify_src('fun x -> x > 0 ==> f x > 0')\n\nIn [5]: result\nOut[5]:\nproved {\n proof_pp: \"...\"\n}\n\nIn [6]: print(result.proved.proof_pp)\n{ id = 1; concl = `|- x > 0 ==> f x > 0`;\n view =\n T_deduction {\n premises =\n [(\"p\",\n [{ id = 0; concl = `|- x > 0 ==> f x > 0`;\n view = T_deduction {premises = []} }\n ])\n ]}\n }\n\nIn [7]: result = client.instance_src('fun x -> f x = 43')\n\nIn [8]: result\nOut[8]:\nsat {\n model {\n m_type: Instance\n src: \"module M = struct\\n\\n let x = 42\\n\\n end\\n\"\n artifact {\n kind: \"cir.model\"\n data: \"...\"\n api_version: \"v8\"\n }\n }\n}\n\nIn [9]: print(result.sat.model.src)\nmodule M = struct\n\n let x = 42\n\n end\n\nIn [10]: result = client.decompose('f')\n\nIn [11]: result\nOut[11]:\nartifact {\n kind: \"cir.fun_decomp\"\n data: \"...\"\n api_version: \"v8\"\n}\nregions_str {\n constraints_str: \"not (x > 0)\"\n invariant_str: \"x\"\n model_str {\n k: \"x\"\n v: \"0\"\n }\n}\nregions_str {\n constraints_str: \"not (x * x < 0)\"\n constraints_str: \"x > 0\"\n invariant_str: \"x + 1\"\n model_str {\n k: \"x\"\n v: \"1\"\n }\n}\ntask {\n id {\n id: \"task:decomp:rE3VSX-t5kbrrAksQ4saBrMUs2uHTXfu-CqeZunV9aE=\"\n }\n kind: TASK_DECOMP\n}\n```\n\n## Example: Imandra Universe reasoners\n\n```\n$ pip install imandra\n```\n\n```\n$ ipython\n\nIn [1]: from imandra.u.reasoners.prover9 import Client\n\nIn [2]: client = Client()\n\nIn [3]: input = \"formulas(sos).\\n\\n e * x = x.\\n x'\\'' * x = e.\\n (x * y) * z = x * (y * z).\\n\\n x * x = e.\\n\\nend_of_list.\\n\\nformulas(goals).\\n\\n x * y = y * x.\\n\\nend_of_list ...: .\"\n\nIn [4]: result = client.eval(input)\n\nIn [5]: print(result['results'][0])\n============================== Prover9 ===============================\nProver9 (64) version 2009-11A, November 2009.\nProcess 18 was started by universe on localhost,\nMon Jan 6 14:52:26 2025\nThe command was \"/imandra-universe/prover9/bin/prover9 -t 45\".\n============================== end of head ===========================\n\n============================== INPUT =================================\n\nformulas(sos).\ne * x = x.\nx''' * x = e.\n(x * y) * z = x * (y * z).\nx * x = e.\nend_of_list.\n\nformulas(goals).\nx * y = y * x.\nend_of_list.\n\n============================== end of input ==========================\n\n...\n\n============================== PROOF =================================\n\n% Proof 1 at 0.01 (+ 0.00) seconds.\n% Length of proof is 16.\n% Level of proof is 7.\n% Maximum clause weight is 11.000.\n% Given clauses 12.\n\n1 x * y = y * x # label(non_clause) # label(goal). [goal].\n2 e * x = x. [assumption].\n3 x''' * x = e. [assumption].\n4 (x * y) * z = x * (y * z). [assumption].\n5 x * x = e. [assumption].\n6 c2 * c1 != c1 * c2. [deny(1)].\n7 x''' * (x * y) = y. [para(3(a,1),4(a,1,1)),rewrite([2(2)]),flip(a)].\n8 x * (x * y) = y. [para(5(a,1),4(a,1,1)),rewrite([2(2)]),flip(a)].\n9 x * (y * (x * y)) = e. [para(5(a,1),4(a,1)),flip(a)].\n11 x'''''' * e = x. [para(3(a,1),7(a,1,2))].\n13 x''' * e = x. [para(5(a,1),7(a,1,2))].\n15 x''' = x. [back_rewrite(11),rewrite([13(8)])].\n16 x * e = x. [back_rewrite(13),rewrite([15(3)])].\n19 x * (y * x) = y. [para(9(a,1),8(a,1,2)),rewrite([16(2)]),flip(a)].\n24 x * y = y * x. [para(19(a,1),8(a,1,2))].\n25 $F. [resolve(24,a,6,a)].\n\n============================== end of proof ==========================\n\n============================== STATISTICS ============================\n\nGiven=12. Generated=122. Kept=23. proofs=1.\nUsable=8. Sos=3. Demods=12. Limbo=2, Disabled=14. Hints=0.\nKept_by_rule=0, Deleted_by_rule=0.\nForward_subsumed=99. Back_subsumed=0.\nSos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.\nNew_demodulators=21 (0 lex), Back_demodulated=9. Back_unit_deleted=0.\nDemod_attempts=770. Demod_rewrites=156.\nRes_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.\nNonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.\nMegabytes=0.06.\nUser_CPU=0.01, System_CPU=0.00, Wall_clock=0.\n\n============================== end of statistics =====================\n\n============================== end of search =========================\n\nTHEOREM PROVED\n```\n\n## Example: Imandra Universe agents\n\n```\n$ pip install imandra[universe]\n```\n\n```\n$ ipython\n\nIn [1]: from imandra.u.agents import cogito\n\nIn [2]: from langchain_core.messages import HumanMessage\n\nIn [3]: g = cogito.get_remote_graph()\n\nIn [4]: cogito.create_thread_sync(g)\n\nIn [5]: g.invoke({'messages': [HumanMessage(content='hello')], 'tasks': []})\nOut[5]:\n{'messages': [{'content': \"You are Cogito, agent within Imandra Universe - a cloud platform for accessing automated logical reasoners, tools and agents connected to them.\",\n 'additional_kwargs': {},\n 'response_metadata': {},\n 'type': 'system',\n 'name': None,\n 'id': 'ae883182-17df-4ced-87e2-4b79b7777e93'},\n {'content': 'hello',\n 'additional_kwargs': {'example': False,\n 'additional_kwargs': {},\n 'response_metadata': {}},\n 'response_metadata': {},\n 'type': 'human',\n 'name': None,\n 'id': 'c5491021-fec5-4e4a-8651-eda927d8e473',\n 'example': False},\n {'content': 'Hello! How can I assist you today?',\n 'additional_kwargs': {},\n 'response_metadata': {},\n 'type': 'ai',\n 'name': 'supervisor',\n 'id': '52e4fd16-235a-4ac2-bdba-3a20d19870a3',\n 'example': False,\n 'tool_calls': [],\n 'invalid_tool_calls': [],\n 'usage_metadata': None}],\n 'tasks': []}\n```\n\n## Example: IPL\n\n```\n$ pip install imandra\n```\n\n```\n$ ipython\n\nIn [1]: from imandra.ipl import Client\n\nIn [2]: client = Client()\n\nIn [3]: job_id = client.unsat_analysis('/path/to/model.ipl', None, None)\n\nIn [4]: client.status(job_id)\nOut[4]: 'processing'\n\nIn [5]: client.wait(job_id)\nOut[5]: 'done'\n\nIn [6]: data = client.data(job_id)\n\nIn [7]: print(data['content'].decode('ascii'))\nFor message flow `simple_orders_one`, unsat cores: []\n```\n\n## CLI\n\nThe `imandra` package also adds an entry point called `imandra-cli` which exposes the `imandra` library functionality in a more discoverable way:\n\n```sh\n$ python3 -m venv ./my/venv\n...\n$ ./my/venv/pip install imandra\n...\n$ ./my/venv/bin/imandra-cli --help\nusage: imandra [-h] auth,ipl,core,rule-synth,cfb ...\n\nImandra CLI\n\npositional arguments:\n {auth,ipl,core,rule-synth,cfb}\n\noptional arguments:\n -h, --help show this help message and exit\n```\n\nOn Windows, the entry point can be found as `.\\my\\venv\\Scripts\\imandra-cli.exe`.\n\n### CLI Authentication\n\nThis is the first step to start using the Imandra CLI. Our cloud environment requires a user account, which you can setup like this:\n\n```sh\n$ ./my/venv/bin/imandra-cli auth login\n```\n\nand follow the prompts to authenticate. This will create the relevant credentials in `~/.imandra` (or `%APPDATA%\\imandra` on Windows).\n\nYou should now be able to invoke CLI commands that require authentication.\n",
"bugtrack_url": null,
"license": null,
"summary": "A CLI and API client library for interfacing with Imandra's web APIs",
"version": "2.0.0",
"project_urls": null,
"split_keywords": [
"imandra"
],
"urls": [
{
"comment_text": null,
"digests": {
"blake2b_256": "54114ce28624e784079e1604f1ab6d63f7e1f690889e231587b77fc5ab648aea",
"md5": "cf5f4bd555030685566e3f2ecad8ac36",
"sha256": "b5b0432a0db797cbad14cdf45a21ca8946309ecff87c4fa4edd49bd9cec3e009"
},
"downloads": -1,
"filename": "imandra-2.0.0-py3-none-any.whl",
"has_sig": false,
"md5_digest": "cf5f4bd555030685566e3f2ecad8ac36",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": null,
"size": 119312,
"upload_time": "2025-02-06T13:31:12",
"upload_time_iso_8601": "2025-02-06T13:31:12.824839Z",
"url": "https://files.pythonhosted.org/packages/54/11/4ce28624e784079e1604f1ab6d63f7e1f690889e231587b77fc5ab648aea/imandra-2.0.0-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "4eaf8a479f70c50356b3ead6f7edebab2e23f7a720f6aff22bcfe575393c223c",
"md5": "30972cd1af48c949bf35ee093f982765",
"sha256": "ff07553a510ea0dc46cb614b775ab9eece65a49b3bc0778a80289a5212977963"
},
"downloads": -1,
"filename": "imandra-2.0.0.tar.gz",
"has_sig": false,
"md5_digest": "30972cd1af48c949bf35ee093f982765",
"packagetype": "sdist",
"python_version": "source",
"requires_python": null,
"size": 57549,
"upload_time": "2025-02-06T13:31:14",
"upload_time_iso_8601": "2025-02-06T13:31:14.917891Z",
"url": "https://files.pythonhosted.org/packages/4e/af/8a479f70c50356b3ead6f7edebab2e23f7a720f6aff22bcfe575393c223c/imandra-2.0.0.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2025-02-06 13:31:14",
"github": false,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"lcname": "imandra"
}
