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

124 commits

Author SHA1 Message Date
Simon Cruanes
2bd555d11b
feat(profile): proper string handling 2022-08-18 22:02:36 -04:00
Simon Cruanes
1b0d47a01d
feat(profile): add basic counters 2022-08-18 20:56:17 -04:00
Simon Cruanes
08a4ed892d
feat(stat): improve printing 2022-08-14 23:21:22 -04:00
Simon Cruanes
6f42c060f4
perf(util): more inlining 2022-08-14 22:33:33 -04:00
Simon Cruanes
63802fe3d6
feat(stat): improve printing api 2022-08-13 13:45:31 -04:00
Simon Cruanes
1edf054104
refactor(proof): use a suspension but keep uniform Proof_term.data type 
this makes proof terms uniformly printable or (de)serializable.
 2022-07-31 15:01:11 -04:00
Simon Cruanes
ee2ea784ad
remove Vec_unit 2022-07-30 23:22:25 -04:00
Simon Cruanes
851dda696a
feat(cc): have 2 phases of pre-merge events 
the first phase observes plugin data unchanged; the second one
is used to update plugin data themselves. This fix a bug that manifests
itself depending on implementation details of Event, where some theory's
event handler fires too late and observes a state that has already
changed.
 2022-07-22 21:31:42 -04:00
Simon Cruanes
6da6284711
refactor(cc): use explicit actions in CC, not effectful functions 2022-07-22 21:26:21 -04:00
Simon Cruanes
7a6d94e622
event: add a return type 2022-07-21 23:20:44 -04:00
Simon Cruanes
b10aaf05f2
wip: expose bug caused by order of event handlers 
if plugin data is updated before `Th_data.on_pre_merge` is called, it
never has a chance to observe the un-merged data and react accordingly.
we need to ensure that all handlers see the same data before any change
is made.
 2022-07-20 21:40:04 -04:00
Simon Cruanes
f3f0628261
large refactor with signature splitting, events, etc. 2022-07-18 23:20:07 -04:00
Simon Cruanes
ea752b5cf5
feat: add some BACKTRACKABLE sigs 2022-07-17 20:21:22 -04:00
Simon Cruanes
833fa8e038
add Event abstraction in Util 2022-07-17 20:20:46 -04:00
Simon Cruanes
00dec7ced8
remove iarray 2022-07-15 21:06:46 -04:00
Simon Cruanes
801d0b3e45
warnings 2022-07-15 20:32:58 -04:00
Simon Cruanes
5a559bec92
remove veci32 2022-07-15 20:32:06 -04:00
Simon Cruanes
a1bc186d2e
use ocamlformat 2022-07-14 22:09:13 -04:00
Simon Cruanes
82acf271d3
improve zarith and backtrackable table 2022-02-08 13:12:07 -05:00
Simon Cruanes
9517e88467
feat(util): add backtrackable ref 2021-12-07 14:08:06 -05:00
Simon Cruanes
4d3b278754
feat(vec): add append, fix prepend 2021-11-19 22:35:40 -05:00
Simon Cruanes
7d5b76a87a
fix tests and warning 2021-10-27 21:54:30 -04:00
Simon Cruanes
0abe4b7020
wip: decode more proof steps to quip 2021-10-27 21:50:28 -04:00
Simon Cruanes
4a30a06f87
wip: reconstruct quip proof from binary proof-trace 2021-10-26 21:57:17 -04:00
Simon Cruanes
63e7d6659e
wip: dump more steps to the trace file 2021-10-20 20:41:51 -04:00
Simon Cruanes
f5172a7927
wip: emit proof steps 2021-10-19 22:52:34 -04:00
Simon Cruanes
29d1fd5cf3
fix bug in veci32 2021-10-16 21:41:10 -04:00
Simon Cruanes
597a6c378e
wip: split VecI32 and VecSmallInt 
- use VecSmallInt for small integers of type `int`
- use VecI32 to store actual int32 (in particular for proof steps)
 2021-10-16 20:31:56 -04:00
Simon Cruanes
af1ef089af
wip: proper proof production using Proof_ser-based traces 2021-10-15 23:00:09 -04:00
Simon Cruanes
ca4a42f28a
improve API of chunk_stack 2021-10-14 23:40:58 -04:00
Simon Cruanes
7df124f94c
test: add a test using a file backend 2021-10-14 23:40:51 -04:00
Simon Cruanes
73cca4ca18
move chunk_stack to util, fix some bugs 2021-10-14 23:18:21 -04:00
Simon Cruanes
3a56fb0763
test file for chunk stack 2021-10-14 23:18:08 -04:00
Simon Cruanes
6fae75f94d
add Vec_unit to util 2021-10-12 22:13:05 -04:00
Simon Cruanes
d3537f2c3f
wip: refactor proof 2021-10-07 20:49:39 -04:00
Simon Cruanes
313e9db026
feat(vec): add copy 2021-09-29 22:16:10 -04:00
Simon Cruanes
bbe366989c
perf(sat): use Atom.Vec for temporary atom array 2021-09-27 19:28:45 -04:00
Simon Cruanes
74326b39c0
feat(vec): factor a bit of code for auxiliary functions in vectors 2021-09-27 19:26:04 -04:00
Simon Cruanes
86512dbed0
utils 2021-09-27 19:22:48 -04:00
Simon Cruanes
4a2367b1bd
refactor: use Atom.Vec (a VecI32) for atom vectors 2021-08-31 09:30:05 -04:00
Simon Cruanes
782afa4415
feat: move Int_id into its own module 2021-08-25 23:52:08 -04:00
Simon Cruanes
68250603c4
fix compat 2021-08-24 19:41:36 -04:00
Simon Cruanes
4cada7e7b6
perf 2021-08-20 18:18:30 -04:00
Simon Cruanes
5372170733
fix: make it compile again 2021-08-20 18:18:14 -04:00
Simon Cruanes
c8eb1ec29e
feat(util): add Vec_sig to express common vector interface 2021-08-20 18:04:54 -04:00
Simon Cruanes
3fbb9af664 refactor(sat): hide atoms, API now talks only about literals 2021-08-19 09:35:54 -04:00
Simon Cruanes
b4231d23c1 perf(checker): optimize watch literals 2021-08-08 02:36:30 -04:00
Simon Cruanes
3aa25cb2a2 sat: use an atom array for clauses again 
allocator is not worth the complexity, and has a lot of double
indirections anyway.
 2021-07-21 10:02:56 -04:00
Simon Cruanes
8b94e8404f wip: data-oriented clauses 2021-07-20 23:34:58 -04:00
Simon Cruanes
29892d07de feat(util): Vec_float based on bigarrays 2021-07-20 23:33:57 -04:00