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

142 commits

Author SHA1 Message Date
Guillaume Bury
daa30a2b4f Correctly print edges in dot backend 
The bug was introduced when reversing the direction of edge arrow,
unfortunatley the "node <- node" syntax overlaps with the html label
syntax.
 2017-07-24 17:04:12 +02:00
Guillaume Bury
0c99e6b2e7 [breaking] Better interface for the DOT backend 2017-07-20 13:55:55 +02:00
Guillaume Bury
5d4b87673d reverse arrow direction in DOT backend 2017-07-20 13:55:44 +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
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
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
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
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
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
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
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
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
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
Guillaume Bury
61eb921f05 Added iCNF export to external 2016-11-25 10:34:31 +01:00
Simon Cruanes
15efe4aceb Revert "change strategy for vec reallocation" 
This reverts commit 7407669834.
 2016-11-24 17:38:09 +01:00
Simon Cruanes
20b4692e18 more accurate assertion 2016-11-24 14:21:51 +01:00