IC3 reference implementation: a short, simple, fairly competitive implementation of IC3. Read it, tune it, extend it, play with it.
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
IC3.cpp
IC3.h
LICENSE
Makefile
Model.cpp
Model.h
README
main.cpp

README

IC3 reference implementation: a short, simple, fairly competitive
implementation of IC3.  Read it, tune it, extend it, play with it.

Copyright 2013, Aaron R. Bradley

1. Obtain the latest version of Minisat at

    https://github.com/niklasso/minisat

  Unpack it into ic3ref/minisat (so that Solver.h is at
  ic3ref/minisat/minisat/core/Solver.h).  Make.

2. Obtain the AIGER utilities (aiger-1.9.4.tar.gz) at 

    http://fmv.jku.at/aiger/

  Unpack it into ic3/aiger (so that aiger.c is at
  ic3ref/aiger/aiger.c).  DO NOT MAKE.

3. At ic3ref, make.

4. Run

    ./IC3 [<option>|<property ID>]* < <AIGER file>

  where

    -v: enables verbose output

    -s: enables output of runtime statistics

    -r: randomizes execution to better indicate performance

    -b: uses basic generalization

    <property ID>: an integer specifying a property index in the AIGER
        file, which defaults to 0.  If 'B' is non-0, prefers 'B' to
        'O' (see AIGER 1.9 format).

    <AIGER file>: AIGER formatted file with .aig or .aag extension