Library for modeling functions over discrete sets using aiger circuits.
Project description
py-aiger-discrete
Library for modeling functions over discrete sets using aiger circuits.
Installation
If you just need to use py-aiger-discrete
, you can just run:
$ pip install py-aiger-discrete
For developers, note that this project uses the poetry python package/dependency management tool. Please familarize yourself with it and then run:
$ poetry install
About
This library helps with modeling functions over finite sets using circuits.
f : A → B₁ × B₂ × … × Bₘ
where A ⊆ A₁ × A₂ × … × Aₙ
.
This is done by providing:
- A encoder/decoder pair for each set to and from (unsigned) integers.
- A circuit that uses the bit-vector representation of these integers
to compute
f
. - A circuit that monitors if the input bit-vector sequence is
valid
, i.e., a member ofA
.
Functionally, the py-aiger-discrete
library centers around the
aiger_discrete.FiniteFunc
class which has 4 attributes an aiger_bv.AIGBV
object.
- A string
valid_id
indicating - A circuit,
circ
, over named bit-vectors in the form of anaiger_bv.AIGBV
object. One of the outputs must be namedvalid_id
. - A mapping from inputs to
aiger_discrete.Encoding
objects which encode/decode objects to integers. The standard bit-encoding of unsigned integers is feed intocirc
. - A mapping from outputs to
aiger_discrete.Encoding
objects which encode/decode objects to integers. These encodings are used to decode the resulting bit-vectors ofcirc
.
Usage
Below we provide a basic usage example. This example assumes basic
knowledge of the py-aiger
ecosystem and particularly py-aiger-bv
.
import aiger_bv as BV
from aiger_discrete import Encoding, from_aigbv
# Will assume inputs are in 'A', 'B', 'C', 'D', or 'E'.
ascii_encoder = Encoding(
decode=lambda x: chr(x + ord('A')), # Make 'A' map to 0.
encode=lambda x: ord(x) - ord('A'),
)
# Create function which maps: A -> B, B -> C, C -> D, D -> E.
x = BV.uatom(3, 'x') # need 3 bits to capture 5 input types.
update_expr = (x + 1) & 0b111
circ = update_expr.with_output('y').aigbv
# Need to assert that the inputs are less than 4.
circ |= (x <= 4).with_output('##valid').aigbv
func = from_aigbv(
circ,
input_encodings={'x': ascii_encoder},
output_encodings={'y': ascii_encoder},
valid_id='##valid',
)
assert func('A') == 'B'
assert func('B') == 'C'
assert func('C') == 'D'
assert func('D') == 'E'
assert func('E') == 'A'
Note that py-aiger-discrete
implements most of the circuit API as aiger_bv.AIGBV
.
For example, sequential composition:
func12 = func1 >> func2
or parallel composition:
func12 = func1 | func2
or unrolling:
func_unrolled = func1.unroll(5)
or feedback:
func_cycle = func1.loopback({
'input': 'x',
'output': 'y',
'keep_output': True,
})
or renaming:
func_renamed = func1['i', {'x': 'z'}]
assert func1.inputs == {'z'}
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Hashes for py_aiger_discrete-0.1.1-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 1dcf05d79c8c199b5d069071e17ec75f714ede1d0e674d7b3f61ea0f3ae45089 |
|
MD5 | fcabbdb9acb4c941905ac7813f4a3cbc |
|
BLAKE2b-256 | f9207220567604fd58c578429ab96c1bd54bda0b9001e39b5946b0f80850e053 |