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