| .. |
|
.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
|
Better color scheme for dot output
|
2014-11-20 14:38:44 +01:00 |
|
res.mli
|
Added theory lemma as possible premise for clauses
|
2014-11-12 17:29:11 +01:00 |
|
res_intf.ml
|
Removed solver_types module in solver.Make functor
|
2014-11-12 16:48:44 +01:00 |
|
sat.ml
|
Changed theory interface to allow pushing of clauses
|
2014-11-19 21:56:24 +01:00 |
|
sat.mli
|
Added Smt module
|
2014-11-14 17:40:29 +01:00 |
|
solver.ml
|
Fix for theory propagated clauses
|
2014-11-20 00:24:39 +01:00 |
|
solver.mli
|
Fixed indentation
|
2014-11-12 16:51:41 +01:00 |
|
solver_types.ml
|
Fix for theory propagated clauses
|
2014-11-20 00:24:39 +01:00 |
|
solver_types.mli
|
Added theory lemma as possible premise for clauses
|
2014-11-12 17:29:11 +01:00 |
|
solver_types_intf.ml
|
Fix for iteration on variables
|
2014-11-16 21:23:54 +01:00 |
|
theory_intf.ml
|
Changed theory interface to allow pushing of clauses
|
2014-11-19 21:56:24 +01:00 |
|
tseitin.ml
|
Replaced True and false as pure formulas in tseitin
|
2014-11-12 23:38:05 +01:00 |
|
tseitin.mli
|
Added tseitin cnf conversion
|
2014-11-08 16:18:20 +01:00 |
|
tseitin_intf.ml
|
Replaced True and false as pure formulas in tseitin
|
2014-11-12 23:38:05 +01:00 |
