128 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Guillaume Bury	dbf0646171	Bugfix in proof generation	2014-11-15 18:38:24 +01:00
Guillaume Bury	6801acdafd	Normalisation is now done in constructors for smt	2014-11-15 12:20:34 +01:00
Guillaume Bury	e92740e75e	Better integration of smt into sat-solve (sic)	2014-11-15 00:59:09 +01:00
Guillaume Bury	37d8ddbd7b	Trivial tests for smt	2014-11-14 18:01:07 +01:00
Guillaume Bury	8ae3277cb3	Fixed a bug in documentaion placement in html	2014-11-14 17:59:50 +01:00
Guillaume Bury	fcbcf5a9d4	Small fix for tautologies in cc for smt	2014-11-14 17:53:16 +01:00
Guillaume Bury	566c30bdcc	Added Smt module	2014-11-14 17:40:29 +01:00
Guillaume Bury	b7c5b39e02	moved smt folder to old	2014-11-14 11:58:43 +01:00
Guillaume Bury	6dc90d5f3f	TODO Update	2014-11-13 00:13:12 +01:00
Guillaume Bury	55c5c3f0f0	Fix in doc	2014-11-12 23:39:04 +01:00
Guillaume Bury	c963145b8f	Replaced True and false as pure formulas in tseitin	2014-11-12 23:38:05 +01:00
Guillaume Bury	ec32a67e54	Better doc for theory interface	2014-11-12 21:29:15 +01:00
Guillaume Bury	752fcbe2ba	Tail-rec version of sform in tseitin.	2014-11-12 18:56:56 +01:00
Guillaume Bury	e2d4f4fdc5	Added theory lemma as possible premise for clauses	2014-11-12 17:29:11 +01:00
Guillaume Bury	aad20489cd	Fix in doc comment	2014-11-12 16:53:19 +01:00
Guillaume Bury	b44c3c3559	Fixed indentation	2014-11-12 16:51:41 +01:00
Guillaume Bury	73c9082b3a	Removed solver_types module in solver.Make functor	2014-11-12 16:48:44 +01:00
Guillaume Bury	2b2631b1c3	Removed a few warnings	2014-11-12 16:27:52 +01:00
Guillaume Bury	35ce540684	Progressing on new theory interface	2014-11-12 16:24:08 +01:00
Guillaume Bury	68a1249527	New interface for theories (still needs work in solver.ml)	2014-11-11 23:52:36 +01:00
Guillaume Bury	9b733851c6	Removed useless argument to Th.assume	2014-11-11 15:34:10 +01:00
Guillaume Bury	b50246d55d	Some more doc + indentation	2014-11-11 13:54:24 +01:00
Guillaume Bury	6338f682df	Added unsat-core option in sat_solve ... Cleaned up a bit soler_types and added some doc	2014-11-11 12:25:16 +01:00
Guillaume Bury	ccfbe72bdf	Safer code for input format auto-detection	2014-11-11 10:45:01 +01:00
Guillaume Bury	172ff8bca3	Added smtlib unsat tests to test script	2014-11-10 20:01:51 +01:00
Guillaume Bury	562fcc1930	Added auto-detection of input format	2014-11-10 19:59:40 +01:00
Guillaume Bury	625c0ad309	Fix for tseitin cnf conversion	2014-11-10 19:47:42 +01:00
Guillaume Bury	e74dddc4b0	Removed outdated .depend	2014-11-10 19:28:52 +01:00
Guillaume Bury	b109924bc1	New option to print cnf after conversion.	2014-11-10 00:24:41 +01:00
Guillaume Bury	4c040ccbde	Added smtlib input option	2014-11-09 23:39:54 +01:00
Guillaume Bury	a28cf4098c	Removed useless dir in Makefile	2014-11-09 18:43:33 +01:00
Guillaume Bury	ff34f5c6f0	Added tseitin cnf conversion	2014-11-08 16:18:20 +01:00
Guillaume Bury	d6cfd27f32	Fixed a bug in proof dot printer (+ indent)	2014-11-07 17:46:32 +01:00
Guillaume Bury	cac9df4510	Parametric input/output in sat_solve	2014-11-07 16:05:38 +01:00
Guillaume Bury	e1486b416d	Lots of fixes for proof generation.	2014-11-07 15:11:32 +01:00
Guillaume Bury	7d7859010e	Removed unsat_core from solver.ml	2014-11-07 13:48:12 +01:00
Guillaume Bury	6073622a8c	Unit hyp clauses are now added as assumptions in the proof	2014-11-07 09:37:36 +01:00
Guillaume Bury	19ebfeb866	Now using unicode characters	2014-11-06 21:24:11 +01:00
Guillaume Bury	fd4a618c2a	Better dot output for unsat proofs	2014-11-06 21:05:45 +01:00
Guillaume Bury	62835b35d0	Indentation + some debug output in res.ml	2014-11-06 18:56:39 +01:00
Guillaume Bury	a13029f96c	Added proof building and output for pure sat.	2014-11-06 18:25:55 +01:00
Guillaume Bury	f36aa78a35	In sat/sat, replaced theory state with type unit	2014-11-06 00:20:40 +01:00
Guillaume Bury	f9fde897e0	Better logging in index when benchmarking (again)	2014-11-05 23:50:29 +01:00
Guillaume Bury	7288f6ece2	Better logging in log/index when running benchs on same commit ... New sync target in bench/Makefile (untested though)	2014-11-05 23:38:50 +01:00
Guillaume Bury	a31285d3ad	New bench target in root Makefile ... bench/Makefile now builds the test utility if not already built	2014-11-05 23:00:58 +01:00
Guillaume Bury	51f5a00224	sat_solve is now build in 'all', test replacfes test-full in Makefile ... targets.	2014-11-05 21:19:28 +01:00
Simon Cruanes	b614e743e2	follow symlinks in bench/makefile	2014-11-05 20:02:38 +01:00
Simon Cruanes	f9d4b9a00e	new Sparse_vec structure, used for vectors with "holes"	2014-11-05 17:41:34 +01:00
Guillaume Bury	b6aa6ed2fc	Makefile for benchs.	2014-11-05 15:59:04 +01:00
Guillaume Bury	3422634923	Replaced List.map with List.rev_map ... Added Vec.set_unsafe and fixed a few bugs	2014-11-05 15:57:48 +01:00