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

542 commits

This branch
This branch
All branches
Author SHA1 Message Date
Guillaume Bury
144af560ab Presentation slide for the poster 2017-09-07 13:15:27 +02:00
Guillaume Bury
0bec9b7bec Typos fix 2017-09-04 16:08:51 +02:00
Guillaume Bury
fb9c83aac9 Pdf update 2017-09-04 12:30:36 +02:00
Guillaume Bury
fcb953d02c Small update to bench table 2017-09-04 12:27:59 +02:00
Guillaume Bury
52468260e4 Final update (hopefully) 2017-09-04 12:18:31 +02:00
Guillaume Bury
1a9f4a554c Some revisions 2017-08-31 16:40:14 +02:00
Guillaume Bury
64c170f3a1 Corrections 2017-08-31 16:27:51 +02:00
Guillaume Bury
c1d00c21ca First final draft of poster 2017-08-31 15:07:20 +02:00
Guillaume Bury
e847c73cf9 poste rupdate 2017-08-31 13:32:16 +02:00
Guillaume Bury
a0d0125eed poster update 2017-08-31 12:07:11 +02:00
Guillaume Bury
82375aa288 Poster update 2017-08-23 22:56:57 +02:00
Guillaume Bury
09bd730ff5 poster start 2017-08-23 13:47:57 +02:00
Guillaume Bury
685f804c09 Final proposition, including fixes to reviews 2017-08-12 01:12:27 +02:00
Guillaume Bury
a5449285ee Final propal 2017-06-07 10:53:30 +02:00
Guillaume Bury
19900bbba8 First draft 2017-05-30 19:31:13 +02:00
Guillaume Bury
42ce75120a cleanup 2017-05-30 16:54:53 +02:00
Guillaume Bury
92835bcdda Add useful function on proof steps 
These new functions are designed to help people if (or when) the proof
API will break next time (i.e. adding a new variant case in step).
 2017-04-12 20:48:08 +02:00
Guillaume Bury
88c122c4a4 Remove incorrect tag duplication 2017-04-12 19:40:21 +02:00
Guillaume Bury
0fe8ded071 [bugfix] Fix typo following doublon elimination 
Following a bugfix for doublon elimination, doublons are now eliminated
in add_clause, and as such, in case no simplification is made, the
clause without doublons should be used (and not init). This was a typo
missed during the refactoring of doublon elimination.
 2017-04-12 19:23:46 +02:00
Guillaume Bury
7e95911dd8 [bugfix] Allow late mcsat conflicts (wrt assigns) 2017-04-07 15:13:27 +02:00
Guillaume Bury
5725cf5173 Move calls to eliminate_doublons in a single place 2017-03-31 15:39:43 +02:00
Guillaume Bury
f5f9a4ab69 Extend the 'seen' field to store more information 2017-03-31 15:17:51 +02:00
Guillaume Bury
33cf73e304 [bug] Add test file 2017-03-31 15:17:31 +02:00
Guillaume Bury
4aa4cb063c Add original problem to bug testfile 2017-03-30 19:32:33 +02:00
Guillaume Bury
88eaa03968 Internal check also checks for undecided lits 2017-03-30 19:29:53 +02:00
Guillaume Bury
7f634da201 Rename a function to avoid (harmless) shadowing 2017-03-30 18:50:46 +02:00
Guillaume Bury
2874dd9cea [bugfix] Fix undecided lit bug 2017-03-30 18:47:54 +02:00
Guillaume Bury
7a7f224dd5 Add bug testfile 2017-03-30 18:47:10 +02:00
Guillaume Bury
2f3a044271 Add local assumptions support to msat binary 2017-03-30 18:41:35 +02:00
Guillaume Bury
154cb373fc Add generativity of Dimacs functor 
Since the dimacs functor has an internal state (relating to the output
in iCNF format), it is desirable to have a generative functor, inc as
esomeone wants to output select parts of a problem to two distinct iCNF
files).
 2017-03-27 16:32:25 +02:00
Guillaume Bury
d0d47fe73f Moved Dimacs problem export in its own module 2017-03-27 15:37:41 +02:00
Simon Cruanes
b5a1ee8a5c prepare for 0.6.1 2017-03-22 15:57:53 +01:00
Guillaume Bury
9019de5a95 Add simple fonctor for dot backend 2017-02-18 15:16:53 +01:00
Guillaume Bury
7776b6e2f0 Fix use of asprintf (missing in 4.00.1) 2017-02-15 14:03:10 +01:00
Guillaume Bury
a13906184c Fix warnings 2017-02-15 13:34:21 +01:00
Guillaume Bury
f20b212b72 Remove warn_error(+8) from _tags 2017-02-15 13:06:00 +01:00
Guillaume Bury
8076c06047 [bugfix] Eliminate duplicates in input clauses 
When adding clauses that conatins duplicates, the checking
of some proof would fail because there would sometime be multiple
littrals to resolve over. This fixes that problem.
 2017-02-15 13:04:54 +01:00
Guillaume Bury
8acf02cb74 [bugfix] subterm insertion in forgetful propagation 2017-01-29 13:38:00 +01:00
Guillaume Bury
44509c6f8d [bugfix] conflict in forgetful propagation 2017-01-27 17:56:47 +01:00
Simon Cruanes
f82e475a42 add tseitin-free example to the readme 2017-01-26 15:09:31 +01:00
Simon Cruanes
8e7efcfd3b ocamlinit file 2017-01-26 15:02:38 +01:00
Guillaume Bury
1cb5eb3fcb [opam] Install doc conditionally 2017-01-25 18:21:32 +01:00
Guillaume Bury
74a4677bb7 Updated version number 2017-01-25 17:51:15 +01:00
Guillaume Bury
733e71e332 [opam] Update opam file to add doc building 2017-01-25 17:36:37 +01:00
Guillaume Bury
dde54d2ea9 [changes] Added changelog 2017-01-24 11:28:40 +01:00
Guillaume Bury
928622b511 [feature] New functions new_lit and new_atom 2017-01-24 11:12:17 +01:00
Guillaume Bury
204e184b86 [doc] Better description for Plugin_intf.reason 2017-01-24 11:12:17 +01:00
Guillaume Bury
1f5b5fc422 Renamed new_atom -> create_atom 2017-01-24 11:12:17 +01:00
Simon Cruanes
ee6c61086a fix bad indentation 2017-01-24 10:14:46 +01:00
Guillaume Bury
d538e19411 Fix typo of Plugin_intf.reason 2017-01-17 15:59:29 +01:00