Metadata-Version: 2.4
Name: intrepyd
Version: 0.14.0
Summary: Simulator and model checkers for circuits, as a python API
Author-email: Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
Maintainer-email: Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
License-Expression: BSD-3-Clause AND LicenseRef-Intrepid AND MIT
Project-URL: Homepage, https://github.com/formalmethods/intrepyd
Project-URL: Source, https://github.com/formalmethods/intrepyd
Project-URL: Issues, https://github.com/formalmethods/intrepyd/issues
Project-URL: Changelog, https://github.com/formalmethods/intrepyd/blob/main/CHANGELOG.md
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Science/Research
Classifier: Operating System :: Microsoft :: Windows
Classifier: Operating System :: POSIX :: Linux
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3 :: Only
Classifier: Topic :: Scientific/Engineering
Requires-Python: >=3.11
Description-Content-Type: text/markdown
License-File: LICENSE.md
License-File: CREDITS.md
License-File: intrepyd/LICENSE.intrepid
Requires-Dist: pandas
Requires-Dist: antlr4-python3-runtime==4.9.1
Provides-Extra: plots
Requires-Dist: matplotlib; extra == "plots"
Dynamic: license-file

# Intrepyd

Intrepyd is a python module that provides a simulator and model checkers in
form of a rich API, to allow the rapid prototyping of **formal methods**
algorithms for the rigorous analysis of circuits, specifications and models.

- Circuits of inputs, latches and combinational nets over booleans, bounded
  and unbounded integers, reals and floats.
- A simulator, and four engines: bounded model checking, k-induction,
  backward reachability and IC3/PDR, whose proofs are checked; a portfolio
  runs them all in parallel, and answers with the first of them.
- Front-ends for Lustre and IEC 61131-3 Structured Text (PLCopen XML).
- Traces as pandas data frames.

```
pip install intrepyd
```

Wheels are available for Linux (x86-64, glibc 2.28 or newer) and Windows
(x86-64), for python 3.11 or newer. Each one carries the intrepid model
checking library for its platform, so there is nothing else to install.

```python
import intrepyd as ip
from intrepyd.engine import EngineResult

ctx = ip.Context()
int8_t = ctx.mk_int8_type()
c = ctx.mk_latch('c', int8_t)
ctx.set_latch_init_next(c, ctx.mk_number('0', int8_t),
                        ctx.mk_add(c, ctx.mk_number('1', int8_t)))

bmc = ctx.mk_bmc()
bmc.add_target(ctx.mk_eq(c, ctx.mk_number('5', int8_t)))
bmc.set_current_depth(5)
assert bmc.reach_targets() == EngineResult.REACHABLE
```

The documentation, the source and the issue tracker are on
[GitHub](https://github.com/formalmethods/intrepyd); a collection of
experiences using Intrepyd is in the
[Formal Methods Little Corner](https://formalmethods.github.io).

Intrepyd is released under the BSD 3-Clause license. The intrepid library
bundled in the wheels is proprietary, and its license, installed as
`intrepyd/LICENSE.intrepid`, allows it to be used and redistributed freely,
unmodified, as part of intrepyd. It links the Z3 SMT solver, released under
the MIT license.
