| .. |
|
.merlin
|
Few fixes. Sat Solver is working.
|
2014-11-01 16:31:19 +01:00 |
|
explanation.ml
|
Few fixes. Sat Solver is working.
|
2014-11-01 16:31:19 +01:00 |
|
explanation.mli
|
Added some documentation.
|
2014-11-01 17:12:56 +01:00 |
|
explanation_intf.ml
|
Added some documentation.
|
2014-11-01 17:12:56 +01:00 |
|
formula_intf.ml
|
Added tseitin cnf conversion
|
2014-11-08 16:18:20 +01:00 |
|
res.ml
|
Fixed a bug in proof dot printer (+ indent)
|
2014-11-07 17:46:32 +01:00 |
|
res.mli
|
Added proof building and output for pure sat.
|
2014-11-06 18:25:55 +01:00 |
|
res_intf.ml
|
Lots of fixes for proof generation.
|
2014-11-07 15:11:32 +01:00 |
|
sat.ml
|
Added tseitin cnf conversion
|
2014-11-08 16:18:20 +01:00 |
|
sat.mli
|
Added tseitin cnf conversion
|
2014-11-08 16:18:20 +01:00 |
|
solver.ml
|
Lots of fixes for proof generation.
|
2014-11-07 15:11:32 +01:00 |
|
solver.mli
|
Removed unsat_core from solver.ml
|
2014-11-07 13:48:12 +01:00 |
|
solver_types.ml
|
Indentation + some debug output in res.ml
|
2014-11-06 18:56:39 +01:00 |
|
solver_types.mli
|
Added some documentation.
|
2014-11-01 17:12:56 +01:00 |
|
solver_types_intf.ml
|
Added proof building and output for pure sat.
|
2014-11-06 18:25:55 +01:00 |
|
theory_intf.ml
|
comments and Vec.exists, used in Solver
|
2014-11-03 23:51:10 +01:00 |
|
tseitin.ml
|
Added tseitin cnf conversion
|
2014-11-08 16:18:20 +01:00 |
|
tseitin.mli
|
Added tseitin cnf conversion
|
2014-11-08 16:18:20 +01:00 |
|
tseitin_intf.ml
|
Added tseitin cnf conversion
|
2014-11-08 16:18:20 +01:00 |
