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

533 commits

This branch
This branch
All branches
Author SHA1 Message Date
Guillaume Bury
5d4b87673d reverse arrow direction in DOT backend 2017-07-20 13:55:44 +02:00
Guillaume Bury
fa9b35f646 Merge branch 'master' of github.com:Gbury/mSAT 2017-07-19 00:18:10 +02:00
Guillaume Bury
02aa16870c Give all label a html context in dot backend 
Before, atoms printed in the dot backend could either be in a html
label, or in a simple label, which caused some problems for escaping
special characters such as newlines. This commit fixes that problem by
having all labels be html labels in the dot output.
 2017-07-19 00:16:37 +02:00
Guillaume Bury
dedfcf1784 Typo in README (again...) 2017-07-03 15:32:27 +02:00
Guillaume Bury
36381335f2 Typo in README 2017-07-03 15:31:42 +02:00
Simon Cruanes
b405634b1d fix typos 2017-06-20 17:37:03 +02:00
Guillaume Bury
e9b6772e75 Added equality explanation for mcsat 2017-06-20 17:16:12 +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
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