simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions
1778 commits 53 branches 1 tag 17 MiB
Commit graph

85 commits

Author SHA1 Message Date
Guillaume Bury
ccebc8c44a Fix for uip unit clause which conflicts with level0 2015-01-26 15:01:26 +01:00
Guillaume Bury
aacae0883b Bundled both smt and mcsat in sat_solve; updated the tests in Makefile 2014-12-16 21:32:18 +01:00
Guillaume Bury
ca70f87973 Mcsat now works 2014-12-16 17:30:14 +01:00
Guillaume Bury
aee73abd47 Progressing. Conflict clause computing is broken 2014-12-15 17:09:01 +01:00
Guillaume Bury
8e8a592475 Some reorganization of files/folders 2014-12-11 17:02:27 +01:00
Guillaume Bury
5654414bfa Small fixes 2014-11-18 18:41:32 +01:00
Simon Cruanes
460df56d4b fix makefile (bis) 2014-11-18 17:56:29 +01:00
Simon Cruanes
50b62b4802 fix redundancies in Makefile 2014-11-18 17:53:45 +01:00
Guillaume Bury
5bcb8ae99f Added a few features in bench_stats 2014-11-17 17:07:40 +01:00
Guillaume Bury
b992794a77 Added diff computing in bench_stats 2014-11-17 15:48:41 +01:00
Guillaume Bury
ee86da6329 Added minimal utility for getting bench stats 2014-11-17 13:55:32 +01:00
Guillaume Bury
384bcb7270 Better explanations in equivalence closure 2014-11-15 18:39:19 +01:00
Guillaume Bury
566c30bdcc Added Smt module 2014-11-14 17:40:29 +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
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
1a2d4ccb73 main test program: move test.ml to sat_solve.ml 2014-11-04 20:40:08 +01:00
Simon Cruanes
30e372d302 moved vec, iheap, etc. from common/ to util/; 
removed dependency of util/ on unix,str
 2014-11-04 20:25:26 +01:00
Simon Cruanes
e95dec0663 fix test; make test scripts PWD-independent 2014-11-04 17:48:22 +01:00
Guillaume Bury
f5563a554f Test utility now compiled to native code 
Added bench/run
 2014-11-04 17:42:15 +01:00
Guillaume Bury
4435821936 New lexer/parser for dimacs format. 2014-11-04 15:41:25 +01:00
Guillaume Bury
7cd1f38d49 New test script. 2014-11-01 23:42:57 +01:00
Guillaume Bury
df524375a7 Added small lexer/parser for dimacs (work in progress). 2014-11-01 21:43:58 +01:00
Guillaume Bury
3c235e259d Sat Solver is broken. 2014-11-01 02:12:17 +01:00
Guillaume Bury
a00506b95f Solver module is now functorised. 'make' now compiles. 2014-10-31 16:21:11 +01:00
Guillaume Bury
4acd669d6f Merge branch 'master' of github.com:Gbury/mSAT 2014-10-29 19:05:37 +01:00
Simon Cruanes
3b37848470 add reinstall target to makefile 2014-10-29 14:54:12 +01:00
Simon Cruanes
a1f46f4870 documentation 2014-10-29 14:25:29 +01:00
Guillaume Bury
cb988eadfa Merge branch 'master' of github.com:Gbury/mSAT 2014-10-29 14:22:27 +01:00
Guillaume Bury
3b06af2977 Removed unused variable in Makefile 2014-10-29 14:22:03 +01:00
Simon Cruanes
ed3d6be013 missing files now installed 2014-10-29 14:21:49 +01:00
Simon Cruanes
db71f48470 modify build system 2014-10-29 14:18:00 +01:00
Simon Cruanes
061369b392 update build system 2014-10-29 13:56:13 +01:00
Guillaume Bury
ed037a4aab Replaced old makefile (we use ocamlbuild now). 
Added .merlin (still may needs some work though).
Fixed some warning of deprecated use of 'Pervasives.or'
 2014-10-29 12:43:08 +01:00