sidekick

simon/sidekick

Fork 0

mirror of https://github.com/c-cube/sidekick.git synced 2026-05-05 17:04:39 -04:00

Commit graph

8c8209c08c large refactoring to keep only a simpler, easier CDCL(T) interface Simon Cruanes 2018-01-21 18:46:28 -06:00
d723aee809 large refactoring to keep only a simpler, easier CDCL(T) interface cdclt Simon Cruanes 2018-01-21 18:46:28 -06:00
7324647fb1 doc msat-refactor Simon Cruanes 2018-01-03 22:08:55 +01:00
53cc8b35a0 more controled API for Res Simon Cruanes 2018-01-03 22:07:40 +01:00
3f4f7ec7e4 a bit of doc Simon Cruanes 2018-01-03 22:01:12 +01:00
a9d762673a fix small linter issue in opam Simon Cruanes 2017-12-30 21:10:25 +01:00
c7015450a1 typo Simon Cruanes 2017-12-29 22:10:01 +01:00
2caf53c24f expose {push,pop} in main solver Simon Cruanes 2017-12-29 21:29:43 +01:00
be929d056a remove useless functions Simon Cruanes 2017-12-29 19:12:17 +01:00
d47071c4f0 reinstate better way of picking watch literals Simon Cruanes 2017-12-29 19:00:32 +01:00
70fcded713 reset some record accesses, for perf Simon Cruanes 2017-12-29 18:53:26 +01:00
38b670ebc0 detail Simon Cruanes 2017-12-29 18:35:27 +01:00
d415f8ed20 do not expose St in solver, but only expose a restricted API. Simon Cruanes 2017-12-29 18:29:56 +01:00
c14f0ba020 make Solver.t more lightweight by removing some useless fields Simon Cruanes 2017-12-29 17:29:24 +01:00
a65309d5e6 add optional size argument to create functions Simon Cruanes 2017-12-29 17:24:09 +01:00
99078b2335 make state explicit and add type t state-wrapper in most modules Simon Cruanes 2017-12-29 16:48:26 +01:00
148c1da3cc wip: use submodules of Solver_types to clean up code Simon Cruanes 2017-12-29 15:29:04 +01:00
06af58e6f3 faster addition of clauses' watch literals Simon Cruanes 2017-12-29 12:32:27 +01:00
1592196c72 dependencies in opam files; put binary in minismt package Simon Cruanes 2017-12-28 19:47:05 +01:00
1cd70b048c split some features into minismt lib Simon Cruanes 2017-12-28 19:43:54 +01:00
d6c84b93bf restrict what Msat core lib exposes, provide shortcuts Simon Cruanes 2017-12-28 19:23:36 +01:00
1037c06636 use generative functors, remove a layer of nesting for SMT libs Simon Cruanes 2017-12-28 19:12:41 +01:00
d4646ffd63 makefile Simon Cruanes 2017-12-28 19:12:32 +01:00
b3e9b640f0 ocpindent config Simon Cruanes 2017-12-28 18:55:01 +01:00
4aed7762a7 remove useless dir Simon Cruanes 2017-12-28 18:48:21 +01:00
875efa33c6 update opam files Simon Cruanes 2017-12-28 18:14:32 +01:00
db54c8e9b2 cleanup in fields Simon Cruanes 2017-12-28 18:03:00 +01:00
d884c9fe41 travis Simon Cruanes 2017-12-28 17:33:03 +01:00
2a3afe7ec1 update travis Simon Cruanes 2017-12-28 16:08:49 +01:00
5e12b26fc0 fix warnings Simon Cruanes 2017-12-28 16:02:47 +01:00
7722319b0a move tseitin transformation into its own lib Simon Cruanes 2017-12-28 16:01:36 +01:00
64d7314aab details Simon Cruanes 2017-12-28 15:55:00 +01:00
ac50e10788 big refactoring Simon Cruanes 2017-12-28 15:51:04 +01:00
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