ic3-rel-ind-graphs

Early-stage research project to analyze the dependency structure of invariants generated by IC3/PDR.

Instructions

Setup

Make the following scripts executable:

• setup-IC3ref.sh
• get-hwmcc17.sh
• gen_graph.py
• test.sh

Then run the following:

./setup-IC3ref.sh
./get-hwmcc17.sh

Usage

To run on all hwmcc17 benchmarks with a timeout (set at top of script), run ./test.sh

To run individually, do the following:

./IC3 --dump=<base name with no extension> < <benchmark>.aig
./gen_graph.py -t <dumped filename>-trans.cnf -i <dumped filename>-inv.cnf -ip <dumped filename>-inv-primed.cnf -o <output_name>

This will generate a graph <output_name>.dot.

You can also check that the dumped invariant is an inductive invariant with the following command:

./check_inv.py --init ./<dumpname>-init.cnf --trans ./<dumpname>-trans.cnf --inv ./<dumpname>-inv.cnf --primes ./<dumpname>-mapping.txt