simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-16 15:56:24 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Commit graph

  • fc5a2d4e9d capitalization of files; add new Log Simon Cruanes 2017-12-28 14:03:23 +01:00
  • 144af560ab Presentation slide for the poster ocaml-workshop-2017 Guillaume Bury 2017-09-07 13:15:27 +02:00
  • 0bec9b7bec Typos fix Guillaume Bury 2017-09-04 16:08:51 +02:00
  • fb9c83aac9 Pdf update Guillaume Bury 2017-09-04 12:30:36 +02:00
  • fcb953d02c Small update to bench table Guillaume Bury 2017-09-04 12:27:59 +02:00
  • 52468260e4 Final update (hopefully) Guillaume Bury 2017-09-04 12:18:31 +02:00
  • 1a9f4a554c Some revisions Guillaume Bury 2017-08-31 16:40:14 +02:00
  • 64c170f3a1 Corrections Guillaume Bury 2017-08-31 16:27:51 +02:00
  • c1d00c21ca First final draft of poster Guillaume Bury 2017-08-31 15:07:20 +02:00
  • e847c73cf9 poste rupdate Guillaume Bury 2017-08-31 13:32:16 +02:00
  • a0d0125eed poster update Guillaume Bury 2017-08-31 12:07:11 +02:00
  • bed469c0cf Clear unused hyps in coq proofs Guillaume Bury 2017-08-29 15:18:10 +02:00
  • 7749f7aaac Manual re-indent Guillaume Bury 2017-08-25 19:15:12 +02:00
  • 679d928b88 Auto re-indent Guillaume Bury 2017-08-25 19:11:58 +02:00
  • 631280af9a Remove use of Array.memq (absent from ocaml <4.03) Guillaume Bury 2017-08-25 19:08:52 +02:00
  • 2db3a5a494 Ignore some smtlib statements in test executable Guillaume Bury 2017-08-25 18:36:42 +02:00
  • 4989026f06 Fix mcsat conflict analysis Guillaume Bury 2017-08-25 18:33:42 +02:00
  • 82375aa288 Poster update Guillaume Bury 2017-08-23 22:56:57 +02:00
  • 09bd730ff5 poster start Guillaume Bury 2017-08-23 13:47:57 +02:00
  • 8eee822ad6 Removed some unused code in coq backend Guillaume Bury 2017-08-22 14:55:21 +02:00
  • 887de5d0af Change coq backend requirements Guillaume Bury 2017-08-16 11:49:51 +02:00
  • bd5fa2426b Use pose proof instead of assert in coq backend Guillaume Bury 2017-08-12 09:58:13 +02:00
  • 685f804c09 Final proposition, including fixes to reviews Guillaume Bury 2017-08-12 01:12:27 +02:00
  • fa7da17cde Fix Coq backend Guillaume Bury 2017-08-09 21:53:06 +02:00
  • 87f080ea47 Fix Coq backend Guillaume Bury 2017-08-09 21:09:44 +02:00
  • 04eb1ec1c5 Fixes to the Coq backend Guillaume Bury 2017-08-09 20:55:27 +02:00
  • 0119d04899 Update after Dolmen change Guillaume Bury 2017-08-09 20:54:53 +02:00
  • 607ec3f043 Added Coq backend (not tested yet) Guillaume Bury 2017-08-07 18:09:25 +02:00
  • daa30a2b4f Correctly print edges in dot backend Guillaume Bury 2017-07-24 17:04:12 +02:00
  • 0c99e6b2e7 [breaking] Better interface for the DOT backend Guillaume Bury 2017-07-20 13:55:55 +02:00
  • 5d4b87673d reverse arrow direction in DOT backend Guillaume Bury 2017-07-20 13:55:44 +02:00
  • fa9b35f646 Merge branch 'master' of github.com:Gbury/mSAT Guillaume Bury 2017-07-19 00:18:10 +02:00
  • 02aa16870c Give all label a html context in dot backend Guillaume Bury 2017-07-19 00:16:37 +02:00
  • dedfcf1784 Typo in README (again...) Guillaume Bury 2017-07-03 15:32:27 +02:00
  • 36381335f2 Typo in README Guillaume Bury 2017-07-03 15:31:42 +02:00
  • b405634b1d fix typos Simon Cruanes 2017-06-20 17:37:03 +02:00
  • e9b6772e75 Added equality explanation for mcsat Guillaume Bury 2017-06-20 17:16:12 +02:00
  • 281a80b7ac Remove ocaml versions incompatible with landmarks profile Guillaume Bury 2017-06-07 14:14:33 +02:00
  • cdb5cc9040 Added landamrks dependency to travis file Guillaume Bury 2017-06-07 13:55:42 +02:00
  • 5a079069ea Use landmarks for profiling Guillaume Bury 2017-06-07 11:57:26 +02:00
  • a5449285ee Final propal Guillaume Bury 2017-06-07 10:53:30 +02:00
  • 19900bbba8 First draft Guillaume Bury 2017-05-30 19:31:13 +02:00
  • 42ce75120a cleanup Guillaume Bury 2017-05-30 16:54:53 +02:00
  • 92835bcdda Add useful function on proof steps Guillaume Bury 2017-04-12 20:48:08 +02:00
  • 88c122c4a4 Remove incorrect tag duplication Guillaume Bury 2017-04-12 19:40:21 +02:00
  • 0fe8ded071 [bugfix] Fix typo following doublon elimination Guillaume Bury 2017-04-12 19:23:46 +02:00
  • 7e95911dd8 [bugfix] Allow late mcsat conflicts (wrt assigns) Guillaume Bury 2017-04-07 15:13:27 +02:00
  • 5725cf5173 Move calls to eliminate_doublons in a single place Guillaume Bury 2017-03-31 15:35:53 +02:00
  • f5f9a4ab69 Extend the 'seen' field to store more information Guillaume Bury 2017-03-31 15:05:53 +02:00
  • 33cf73e304 [bug] Add test file Guillaume Bury 2017-03-31 15:17:31 +02:00
  • 4aa4cb063c Add original problem to bug testfile Guillaume Bury 2017-03-30 19:32:33 +02:00
  • 88eaa03968 Internal check also checks for undecided lits Guillaume Bury 2017-03-30 19:29:53 +02:00
  • 7f634da201 Rename a function to avoid (harmless) shadowing Guillaume Bury 2017-03-30 18:50:46 +02:00
  • 2874dd9cea [bugfix] Fix undecided lit bug Guillaume Bury 2017-03-30 18:47:54 +02:00
  • 7a7f224dd5 Add bug testfile Guillaume Bury 2017-03-30 18:47:10 +02:00
  • 2f3a044271 Add local assumptions support to msat binary Guillaume Bury 2017-03-30 18:41:35 +02:00
  • 154cb373fc Add generativity of Dimacs functor Guillaume Bury 2017-03-27 16:32:25 +02:00
  • d0d47fe73f Moved Dimacs problem export in its own module Guillaume Bury 2017-03-27 15:37:41 +02:00
  • b5a1ee8a5c prepare for 0.6.1 Simon Cruanes 2017-03-22 15:57:53 +01:00
  • 9019de5a95 Add simple fonctor for dot backend Guillaume Bury 2017-02-18 15:16:53 +01:00
  • 7776b6e2f0 Fix use of asprintf (missing in 4.00.1) Guillaume Bury 2017-02-15 14:03:10 +01:00
  • a13906184c Fix warnings Guillaume Bury 2017-02-15 13:34:21 +01:00
  • f20b212b72 Remove warn_error(+8) from _tags Guillaume Bury 2017-02-15 13:06:00 +01:00
  • 8076c06047 [bugfix] Eliminate duplicates in input clauses Guillaume Bury 2017-02-14 19:21:07 +01:00
  • 8acf02cb74 [bugfix] subterm insertion in forgetful propagation Guillaume Bury 2017-01-29 13:33:24 +01:00
  • 44509c6f8d [bugfix] conflict in forgetful propagation Guillaume Bury 2017-01-27 17:56:47 +01:00
  • f82e475a42 add tseitin-free example to the readme Simon Cruanes 2017-01-26 15:09:31 +01:00
  • 8e7efcfd3b ocamlinit file Simon Cruanes 2017-01-26 15:02:38 +01:00
  • 1cb5eb3fcb [opam] Install doc conditionally Guillaume Bury 2017-01-25 18:13:41 +01:00
  • 74a4677bb7 Updated version number Guillaume Bury 2017-01-25 17:50:04 +01:00
  • 733e71e332 [opam] Update opam file to add doc building Guillaume Bury 2017-01-25 17:09:41 +01:00
  • dde54d2ea9 [changes] Added changelog Guillaume Bury 2017-01-24 11:28:40 +01:00
  • 928622b511 [feature] New functions new_lit and new_atom Guillaume Bury 2017-01-24 10:55:52 +01:00
  • 204e184b86 [doc] Better description for Plugin_intf.reason Guillaume Bury 2017-01-24 10:54:01 +01:00
  • 1f5b5fc422 Renamed new_atom -> create_atom Guillaume Bury 2017-01-24 10:53:34 +01:00
  • ee6c61086a fix bad indentation Simon Cruanes 2017-01-24 10:14:46 +01:00
  • d538e19411 Fix typo of Plugin_intf.reason Guillaume Bury 2017-01-17 15:59:29 +01:00
  • ea2c905644 Add forgetful propagation Guillaume Bury 2016-08-04 22:18:39 +02:00
  • e8e619f3c7 Do not decide on unused variables Guillaume Bury 2017-01-17 12:29:39 +01:00
  • c77c997ab8 Add used field to variables Guillaume Bury 2017-01-17 12:26:18 +01:00
  • b5d816fbac Typo in doc Guillaume Bury 2017-01-17 12:26:12 +01:00
  • a5733c818d Merge branch 'master' of github.com:Gbury/mSAT Guillaume Bury 2017-01-12 13:41:26 +01:00
  • aeb52b69dd Fixed title in doc page Guillaume Bury 2017-01-12 13:41:05 +01:00
  • 109ddd7a73 Readme update Guillaume Bury 2016-12-26 12:24:07 +01:00
  • 35c99df753 Added some missing headers Guillaume Bury 2016-12-25 20:52:18 +01:00
  • b391a98aa0 Typo in doc Guillaume Bury 2016-12-19 16:04:16 +01:00
  • f80c3b3df7 [bugfix] Allow semantic propagation of already true lits Guillaume Bury 2016-12-19 15:58:48 +01:00
  • 58e6b924a8 Added full_slice function in Internal Guillaume Bury 2016-12-07 13:21:12 +01:00
  • 32128749b2 Some mli doc updates Guillaume Bury 2016-12-02 15:57:56 +01:00
  • 4159a34c20 Removed module alias for SAT expressions Guillaume Bury 2016-12-02 15:49:49 +01:00
  • 1d8fa08f92 Added Sat module to the lib. Updated README Guillaume Bury 2016-12-01 18:55:58 +01:00
  • c53a81e54b Forgot to update .ml when adding Arg to .mli Guillaume Bury 2016-12-01 18:27:50 +01:00
  • cd632ad345 Added link to 0.5.1 doc Guillaume Bury 2016-12-01 18:11:46 +01:00
  • fe2f92ca3c Some more doc in mlis Guillaume Bury 2016-12-01 18:05:34 +01:00
  • f0056c7b79 Massive doc upgrade for .mli Guillaume Bury 2016-12-01 17:49:21 +01:00
  • 3cefd85b21 Fixed some typos in doc Guillaume Bury 2016-12-01 15:50:57 +01:00
  • 8896ce2b79 Documentation update Guillaume Bury 2016-12-01 15:31:30 +01:00
  • 30832099b3 avoid allocating at every call to grow_to_at_least Simon Cruanes 2016-11-30 16:08:03 +01:00
  • 2e7e947b62 Allow level 0 semantic propagations Guillaume Bury 2016-11-25 15:16:10 +01:00
  • 64694b524d [breaking] Ceaner interface for mcsat propagations Guillaume Bury 2016-11-25 12:07:23 +01:00