arbrad/ic3ref

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

ic3ref's Issues

False bug report?

Hi Aaron,
IC3 reports 'buggy' for the aag file below. The file contains a single output (which raises to 1 if bug found) and a single input.

aag 4 1 1 1 2
2
6 2
8
8 6 5
4 1 1
i0 i_r
l0 r-latch
o0 err
c
example1: r -> Xg

And here the dot for the file:

Current issues

1. The comparator for stable_sort is passed by value, not by reference, which is a performance issue as a HeuristicLitOrder object holds substantial data. [31 May 2015: Fixed by mgudemann.]
2. micAttempts is currently set to 3. It should be set to something much higher to allow more aggressive (but more expensive) inductive generalization.
3. One-SAT-context-per-frame is inefficient, as it turns out. There should be one context for all frames.
4. The logic cone should be loaded on-demand, not all at once.

Issues (1) and (2) are quick to fix, although I'm not currently maintaining the code.

Issues (3) and (4) are somewhat fundamental to the implementation.

Segmentation Fault

Hi, again:) The following `corner-case' file causes IC3 to crash with segfault:

aag 5 2 0 1 3
2
4
7
6 9 11
8 2 4
10 3 5
i0 i
i1 controllable
c
G(i <-> c)
special case -- no latches
realizable

gdb ./IC3
run < eq.aag
Program received signal SIGSEGV, Segmentation fault.
value (p=..., this=) at ./minisat/core/Solver.h:351
351 inline lbool Solver::value (Lit p) const { return assigns[var(p)] ^ sign(p); }

Reading Aiger files causes IC3 binary to not function properly (Mac OS X)

Despite the compilation process succeeding without any issues, running the command ./IC3 with the specified parameters produces nothing. The process must be killed in order to exit. I traced down the bug to this line in aiger.c: aiger_read_header

aiger_next_ch (reader);
if (reader->ch != 'a')
return aiger_error_u (private,
"line %u: expected 'a' as first character",
reader->lineno);

The aiger files being run were the benchmarks that were run in the original IC3 paper. It seems that the aiger files are not being read/parsed properly, despite providing proper ones.