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
519 commits 53 branches 1 tag 17 MiB
Commit graph

519 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Guillaume Bury
ea2c905644 Add forgetful propagation 2017-01-17 13:16:00 +01:00
Guillaume Bury
e8e619f3c7 Do not decide on unused variables 2017-01-17 12:29:39 +01:00
Guillaume Bury
c77c997ab8 Add used field to variables 2017-01-17 12:26:18 +01:00
Guillaume Bury
b5d816fbac Typo in doc 2017-01-17 12:26:12 +01:00
Guillaume Bury
a5733c818d Merge branch 'master' of github.com:Gbury/mSAT 2017-01-12 13:41:26 +01:00
Guillaume Bury
aeb52b69dd Fixed title in doc page 2017-01-12 13:41:05 +01:00
Guillaume Bury
109ddd7a73 Readme update 2016-12-26 12:24:07 +01:00
Guillaume Bury
35c99df753 Added some missing headers 2016-12-25 20:52:18 +01:00
Guillaume Bury
b391a98aa0 Typo in doc 2016-12-19 16:04:16 +01:00
Guillaume Bury
f80c3b3df7 [bugfix] Allow semantic propagation of already true lits 2016-12-19 15:58:48 +01:00
Guillaume Bury
58e6b924a8 Added full_slice function in Internal 2016-12-07 13:21:12 +01:00
Guillaume Bury
32128749b2 Some mli doc updates 2016-12-02 15:57:56 +01:00
Guillaume Bury
4159a34c20 Removed module alias for SAT expressions 2016-12-02 15:49:49 +01:00
Guillaume Bury
1d8fa08f92 Added Sat module to the lib. Updated README 2016-12-01 18:55:58 +01:00
Guillaume Bury
c53a81e54b Forgot to update .ml when adding Arg to .mli 2016-12-01 18:27:50 +01:00
Guillaume Bury
cd632ad345 Added link to 0.5.1 doc 2016-12-01 18:11:46 +01:00
Guillaume Bury
fe2f92ca3c Some more doc in mlis 2016-12-01 18:05:34 +01:00
Guillaume Bury
f0056c7b79 Massive doc upgrade for .mli 2016-12-01 17:49:21 +01:00
Guillaume Bury
3cefd85b21 Fixed some typos in doc 2016-12-01 15:50:57 +01:00
Guillaume Bury
8896ce2b79 Documentation update 2016-12-01 15:35:15 +01:00
Simon Cruanes
30832099b3 avoid allocating at every call to grow_to_at_least 2016-11-30 16:12:42 +01:00
Guillaume Bury
2e7e947b62 Allow level 0 semantic propagations 2016-11-25 15:16:10 +01:00
Guillaume Bury
64694b524d [breaking] Ceaner interface for mcsat propagations 2016-11-25 12:07:23 +01:00