Guillaume Bury 3d951db181 Small update for clause info about proofs		2015-02-09 15:34:49 +01:00
..
.merlin
expr_intf.ml
formula_intf.ml
log_intf.ml	Solver modules are paramtrized by log module	2015-01-20 12:58:28 +01:00
mcproof.ml	Min/max typo	2015-02-06 14:36:09 +01:00
mcproof.mli
mcsolver.ml	[bugfix] semantic backtrack added decision with wrong level	2015-02-09 14:15:15 +01:00
mcsolver.mli	Solver modules are paramtrized by log module	2015-01-20 12:58:28 +01:00
mcsolver_types.ml	Replaced maps by hashtbl for mcsat	2015-02-06 09:56:41 +01:00
mcsolver_types.mli
mcsolver_types_intf.ml	Update for proof output in dot	2015-01-29 15:00:52 +01:00
plugin_intf.ml	Added 'if_sat' possibility for plugins	2015-02-03 17:37:36 +01:00
res.ml	small perf change	2015-02-06 17:47:29 +01:00
res.mli
res_intf.ml
solver.ml	Small update for clause info about proofs	2015-02-09 15:34:49 +01:00
solver.mli	Replaced clause number by tag in solver.assume	2015-02-06 15:46:56 +01:00
solver_types.ml	Replaced clause number by tag in solver.assume	2015-02-06 15:46:56 +01:00
solver_types.mli
solver_types_intf.ml	Replaced clause number by tag in solver.assume	2015-02-06 15:46:56 +01:00
theory_intf.ml
tseitin.ml
tseitin.mli
tseitin_intf.ml