Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
190 changes: 60 additions & 130 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,156 +1,86 @@
# Cirbo: A New Tool for Boolean Circuit Analysis and Synthesis

## Environment setup
Cirbo is a Python library that provides methods for
Boolean circuit manipulation, analysis, and synthesis

Usage example
```py
from cirbo.core import Circuit, Gate, gate
from cirbo.synthesis.generation.arithmetics import add_sum_n_bits

# Create an empty circuit with 6 inputs.
ckt = Circuit.bare_circuit(input_size=6)
# Generate and connect a "gadget" subcircuit
# that computes the sum of the input bits.
b0, b1, b2 = add_sum_n_bits(ckt, ckt.inputs)
# Manually add output gate that yield True only
# if at least half of the inputs are True.
ckt.add_gate(Gate('a0', gate.AND, (b0, b1)))
ckt.add_gate(Gate('a1', gate.OR, ('a0', b2)))
ckt.mark_as_output('a1')

# Calculate general boolean function properties.
print(f"Is monotone: {ckt.is_monotone()}")
print(f"Is symmetric: {ckt.is_symmetric()}")
print(f"Is constant: {ckt.is_constant()}")

# Draw the graph and show the image in the default viewer.
ckt.view_graph()
```

More examples are available in the [tutorial](https://github.com/SPbSAT/cirbo/tree/main/tutorial).

`Python 3.9` is used to cover all currently [maintained Python versions](https://devguide.python.org/versions/).
## Installation

Package was tested on `Ubuntu` and `Mac OS Ventura 13` machines.
The package is currently available on Test PyPI and will be published on PyPI after testing.

1. Update submodules `git submodule update --init --recursive`
1. Install following packages using your package manager:
- dev version of `python3.9-dev` and `python3.9-distutils`
- `build-essential` package for Ubuntu.
- `cmake` and suitable C++ compiler, e.g. `gcc`
- `graphviz` library
To install the package from Test PyPI into your virtual environment, run:

Command for Ubuntu:
```shell
sudo apt install python3-dev python3.9-dev python3.9-distutils gcc cmake graphviz build-essential
```

> Note: python3.9 is unavailable in latest versions of Ubuntu, so `deadsnakes`
> ppa may be useful: https://launchpad.net/~deadsnakes/+archive/ubuntu/ppa
```sh
python -m pip install --index-url https://test.pypi.org/simple/ --extra-index-url https://pypi.org/simple/ cirbo
```

1. Install `poetry` ([official instruction](https://python-poetry.org/docs/)) (`cirbo` requires `poetry` version to be `>= 2.0.0`)
1. Build dist with extensions locally by running `poetry build`
Instructions on how to set up the development environment are provided in the separate [dev README](README_DEV.md).

> Note: building `ABC` extension may take long time, one can skip it
> using `(export DISABLE_ABC_CEXT=1 && poetry build && poetry install)`
> command.
## Documentation

1. Setup virtual environment by running `poetry install`
1. Execute `poetry env activate`
1. Enable virtual environment using command, which was printed by previous command.
The main library features are described in the paper "Cirbo: A New Tool for Boolean Circuit Analysis and Synthesis" ([arXiv](https://arxiv.org/abs/2412.14933), [AAAI-25](https://ojs.aaai.org/index.php/AAAI/article/view/33207)).

> Note: it may be necessary to restart an IDE after extensions
> are built and installed to refresh its index and stubs.
Currently, `cirbo` does not have web-hosted documentation, but it can be built locally using Sphinx (see the [dev README](README_DEV.md) for details).

## Package structure

Some features of a package are demonstrated in the special modules located in
the `tutorial/` directory. The same code snippets are used in the paper's listings.
This is probably a first place that should be explored after environment is set up.

Directory `docs/` contains pre-rendered auto-api documentation of package `cirbo`.
Main classes and methods of `cirbo` can be explored it that documentation. To begin
exploration open `docs/index.html` in a browser.
Some features of the package are demonstrated in the example modules located in
the `tutorial/` directory. Similar code snippets are used in the paper's listings.
This is probably the first place to explore after environment is set up.

Main `cirbo/` directory is a Python package root. It provides following subpackages:
The `cirbo/` directory is the root of the Python package and contains the following subpackages:

- `core` — provides core classes and structures:
- main boolean function abstractions: `Function` protocol to represent any
boolean function and `FunctionModel` protocol to represent any partially
defined boolean function
- structures to carry representations of a boolean function (`TruthTable`,
- core abstractions for Boolean functions: the `Function` protocol to represent any
Boolean function and the `FunctionModel` protocol to represent partially
defined Boolean functions.
- data structures for representing Boolean functions (`TruthTable`,
`PyFunction` and `Circuit`)
- a `Circuit` class alongside with circuit manipulation operations.
- the `Circuit` class along with circuit manipulation operations.
- `synthesis` — provides tools for circuit synthesis:
- methods to synthesize new circuit either by providing model of a function
(e.g. truth table with don't care values) and then formulating and solving
a SAT problem of finding feasible circuit.
- methods to generate circuits describing arithmetical and logical operations
(e.g. `generate_sum_n_bits` and `generate_if_then_else`) or add such gadget to
- methods to generate circuits describing arithmetic and logical operations
(e.g. `generate_sum_n_bits` and `generate_if_then_else`) or to add such gadgets to
an existing circuit.
- `minimization` — provides methods to minimize circuits:
- low-effort circuit minimization algorithms (e.g. cleaning redundant gates,
merging unary operators, merging duplicates, brute forcing equivalent gates).
- high-effort circuit minimization trying to simplify small subcircuits within
- lightweight circuit minimization algorithms (e.g. cleaning redundant gates,
merging unary operators, merging duplicates, brute-force search for equivalent gates).
- heavyweight circuit minimization that tries to simplify small subcircuits within
original circuit.
- `sat` — provides tools related to `SAT` solving:
- method to build a miter from two given circuits.
- method to reduce of `Circuit SAT` to `SAT` using Tseytin transformation.
- method to call `SAT` solvers using [pysat toolkit](https://github.com/pysathq/pysat).
- `sat` — provides tools related to SAT solving:
- a method to build a miter from two given circuits.
- a method to reduce of circuit satisfiability to SAT using Tseytin transformation.
- a method to call SAT solvers using [pysat toolkit](https://github.com/pysathq/pysat).
- `circuits_db` — provides methods to manage (read and write) database of
(nearly) optimal small circuits. Can be useful for either search for circuit with
given (partially defined) truth table or for an optimization of existing circuit.

> Note: most of a public methods provide docstrings, which can be useful when
> exploring `cirbo`.

Directory `data/` contains databases of small (nearly) optimal circuits, and
an exemplar of circuit encoded in BENCH format needed for `tutorial/`.

Directory `extensions/` contains C/C++ extensions written using `pybind11`.
Those extensions allow usage of `ABC` and `mockturtle` within python env.

Directory `third_party/` contains all third party libraries (excluding ones
installed form `pypi`) distributed alongside current zip archive (whilts
originally those dependencies are managed using `git submodule`). Those
include: `ABC`, `mockturtle` and `pybind11`.

Directory `tools/` contains utilities helpful for running linting checks or formatters.

Directory `tests/` contains all tests that cover both `cirbo/` and `extensions/`.

## Technical info

### C/C++ extensions

`cirbo` package provides integration with external `C/C++` libraries (`mockturtle`
and `ABC`). Such extensions are written using `pybind11` and should be built before
used locally. To build dependencies run `poetry build` and to install them use
`poetry install` after.

> Note: to build dependencies one should have all building tools available
> in the system. Currently, dependencies require `C++` compiler and `cmake`
> to be available.

> Warning: `ABC` extension takes quite a long time (>10 min) to build. There is
> an option to avoid its building: `(export DISABLE_ABC_CEXT=1 && poetry build)`
> (parenthesis should be included). It can be helpful for fast testing because,
> but yet it may cause some `cirbo` functionality to not work property.

### Code quality

Code quality is sustained through both test-driven development and mandatory
linter checks.

#### Tests

Tests are written and executed using `pytest`. To execute unit tests run
`poetry run pytest`. Some tests have markers that disable their execution
by default due to their long execution times or extra dependencies requirements.
To execute all tests run `poetry run pytest -m 'not manual'`.

#### Linters

`mypy` is used for static type checking and `flake8` is used for general linting.

`black`, `docformatter` and `usort` are used both to check if code is properly
formatted (e.g. in CI checks) and to format code locally.

#### Tools

All formatters can be run at once in poetry environment using following tool script:

`python ./tools/formatter.py`

All checks can be run at once in poetry environment using following tool script:

`python ./tools/check.py`

If everything is good, output is expected to be like the following:

```
(cirbo-py3.9) cirbo$ python ./tools/check.py
1. MYPY CHECK SUCCEED
2. FLAKE8 CHECK SUCCEED
3. PYTEST CHECK SUCCEED
4. USORT CHECK SUCCEED
5. DOCFORMATTER CHECK SUCCEED
6. BLACK CHECK SUCCEED
```

## Development and contribution
(nearly) optimal small circuits. It can be useful for searching for a circuit with
a given (partially defined) truth table or for optimizing an existing circuit.

More detailed developer's README can be found [nearby](README_DEV.md).
> Note: most public methods have docstrings, which are useful when exploring `cirbo`.
46 changes: 31 additions & 15 deletions README_DEV.md
Original file line number Diff line number Diff line change
Expand Up @@ -34,25 +34,23 @@ Package was tested on `Ubuntu` and `Mac OS Ventura 13` machines.

> Note: it may be necessary to restart an IDE after extensions
> are built and installed to refresh its index and stubs.
nstalled to refresh its index and stubs.

## Building extensions
## Building C/C++ extensions

This package provides bridges to some external `C/C++` libraries. Extensions
are written using `pybind11` and should be built before used locally. To build
dependencies run `poetry build` and to install them after use `poetry install`.
The `cirbo` package provides integration with external C/C++ libraries (`mockturtle` and `ABC`).
These extensions are written using `pybind11` and should be built before being used locally.
To build the dependencies, run `poetry build`, and then install the package with `poetry install`.

Note: to build dependencies one should have all building tools available
in the system. Currently, dependencies require `C++` compiler and `cmake`
to be available.
> Note: to build the dependencies, you need the required build tools installed
> on your system. Currently, the dependencies require a C++ compiler and CMake.

Some extensions can be disabled using environment variables if one doesn't
need them. For example `(export DISABLE_ABC_CEXT=1 && poetry build)` (parenthesis
should be included) will build wheels without `ABC` bridge module. It can be
helpful for CI or fast testing because `ABC` compilation times are heavy.

Tests that use `ABC` extension can be skipped by passing option `-m 'not ABC'`
to `pytest` run.
> Warning: the `ABC` extension takes quite a long time (>10 min) to build. You
> can skip building it with `(export DISABLE_ABC_CEXT=1 && poetry build)` (parentheses
> should be included). This can be helpful for faster testing, but it may cause
> some `cirbo` functionality to not work properly.
>
> Tests that use `ABC` extension can be skipped by passing option `-m 'not ABC'`
> to `pytest` run.

## Codestyle guidelines

Expand Down Expand Up @@ -159,6 +157,24 @@ Read more about submodules in
```
5. Add python tests to `tests/<extension name>` package.

## Building documentation

Currently, documentation can be generated using `Sphinx` in dev environment.
To do it simply navigate to `docs/` and execute `make html`.

## Dev Directories

Besides main source directory `cirbo/` this repo contains:
- Directory `tutorial/` with several library usage examples.
- Directory `extensions/` with C/C++ extensions written using `pybind11`.
Those extensions allow usage of `ABC` and `mockturtle` within python env.
- Directory `third_party/` with all third party libraries (excluding ones
installed form `pypi`) distributed alongside current zip archive (whilts
originally those dependencies are managed using `git submodule`). Those
include: `ABC`, `mockturtle` and `pybind11`.
- Directory `tools/` with utilities helpful for running linting checks or formatters.
- Directory `tests/` with all tests that cover both `cirbo/` and `extensions/`.

## CI flow

GitHub Actions are used for CI. Following checks are executed automatically for
Expand Down
41 changes: 0 additions & 41 deletions README_PYPI.md

This file was deleted.

2 changes: 1 addition & 1 deletion pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ authors = [
maintainers = [
{name = "Fedor Kurmazov", email = "f.kurmazov.b@gmail.com"}
]
readme = "README_PYPI.md"
readme = "README.md"
license = {file = "LICENCE"}
# Temporary guard against occasional publishing.
classifiers = [
Expand Down
25 changes: 25 additions & 0 deletions tutorial/01_intro.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
# Cirbo is a Python library that provides methods for
# Boolean circuit manipulations, analysis and synthesis.
# Code below demonstrates how simple Boolean circuit can
# be constructed, analyzed and drawn.
from cirbo.core import Circuit, Gate, gate
from cirbo.synthesis.generation.arithmetics import add_sum_n_bits

# Create an empty circuit with 6 inputs.
ckt = Circuit.bare_circuit(input_size=6)
# Generate and connect a "gadget" subcircuit
# that computes the sum of the input bits.
b0, b1, b2 = add_sum_n_bits(ckt, ckt.inputs)
# Manually add output gate that yield True only
# if at least half of the inputs are True.
ckt.add_gate(Gate('a0', gate.AND, (b0, b1)))
ckt.add_gate(Gate('a1', gate.OR, ('a0', b2)))
ckt.mark_as_output('a1')

# Calculate general boolean function properties.
print(f"Is monotone: {ckt.is_monotone()}")
print(f"Is symmetric: {ckt.is_symmetric()}")
print(f"Is constant: {ckt.is_constant()}")

# Draw graph and show image in the default viewer.
ckt.view_graph()