Verify various properties of boolean expressions using a concise DSL.
Project description
VeriBool
Verify properties of boolean expressions using a concise DSL.
I know you just want to press that button
Installation
python3 -m pip install veribool
Usage
# directly compile the expression to a python lambda expression
# add the -i/--interactive flag to drop into a python interpreter with
# fn = <the boolean expression as a lambda>
$: veribool compile "x'y' + x'z + xyz"
lambda x, y, z, **_kwargs: (((not x) and (not y)) or (((not x) and z) or (x and y and z)))
# find a diverging input for two boolean expressions
$: veribool diff "x xnor (yz)" "x'y' + x'z + xyz"
[0, 1, 0] - True vs False
# $? == 0 if expressions match
$: veribool diff "x xnor (yz)" "x'y' + x'z' + xyz" && echo equal
equal
# generate truth table
$: veribool truth "x xnor (yz)"
[0, 0, 0] - True
[0, 0, 1] - True
[0, 1, 0] - True
[0, 1, 1] - False
[1, 0, 0] - False
[1, 0, 1] - False
[1, 1, 0] - False
[1, 1, 1] - True
DSL
This project implements a compiler for a boolean expression DSL closely modeling mathematical boolean algebra notation.
Rules:
- each variable is 1 case-sensitive alphabetical character
- parenthesis exist
x'
is the complement ofx
xy
is theand
ofx
andy
x + y
is theor
ofx
andy
x ^ y
andx xor y
are thexor
ofx
andy
x xnor y
is thexnor
ofx
andy
- order of operations is:
parenthesis
,not
,and
followed by the rest of the operators
Roadmap
- use z3 as a backend
- add some basic simplifications
- output to verilog / other languages
Developers
Developed by Ronak Badhe
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
veribool-0.0.0.tar.gz
(6.9 kB
view hashes)