C3

The C3, SMT solver written in C. Currently WIP project...

Usage(SAT solver)

C3 has support for DIMACS file format as input for SAT solver.

$ ./c3 -D <DIMACS format file>

You can also solve Sudoku by following command.

$ ./test/sudoku/gen_cnf.sh

Usage(SMT solver)

C3 has also support SMT-LIB2 file format as input for SMT solver.

$ ./c3 -S <SMT-LIB2 format file>

Test

You can try random test. All expression are generated by random.

$ make test