Skip to content
/ pybmc Public

Implementation of bounded model checking with Z3py. (AIGER1.0 support)

Notifications You must be signed in to change notification settings

Gy-Hu/pybmc

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

20 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

pybmc

Dependencies

  • aigertool: Used to convert aig format to aag format. Put it in the same directory as main.py by execute git clone https://github.com/arminbiere/aiger.git here, and build it with ./configure.sh && make. Without this tool will only support aag format.

USAGE

  • python main.py --aag <path to config file> --k <number of bound>: run the algorithm with the given aag format file and bound k

Note

  • git checkout k-induction to switch to the k-induction branch

About

Implementation of bounded model checking with Z3py. (AIGER1.0 support)

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages