simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-05-05 08:54:24 -04:00
Code Issues Projects Releases Packages Wiki Activity Actions
1950 commits 55 branches 1 tag 20 MiB
Commit graph

1950 commits

This branch
This branch
All branches
Author SHA1 Message Date
Simon Cruanes
62422169ea fix qcheck deprecation warnings 2026-05-03 23:03:27 -04:00
Simon Cruanes
4c4ff26d07 remove dead script 2026-05-03 22:45:51 -04:00
Simon Cruanes
969a04f630 make format + ignore generated .granite files 2026-05-04 02:42:00 +00:00
Simon Cruanes
3932c247d4 proof: eliminate P_let/P_local; emit subproofs eagerly via tracer 
CC.proof_of_th_lemmas now takes a Proof.Tracer.t and emits each
binding immediately (Tracer.add_step), receiving the byte offset as
a Step.id, and uses P_ref to reference it.  No more local_gen/P_let.

- Pterm: remove P_local, P_let, local_ref, let_, local_ref constructor
- CC/Expl_state: remove local_gen field and new_local_id; thread
  tracer through to_resolved_expl and lits_and_proof_of_expl
- proof_encoder: drop P_let/P_local match arms (now exhaustive)
- twp_pterm: drop P_local/P_let handling and emit_pterm_with_locals
 2026-05-04 02:41:11 +00:00
Simon Cruanes
62f88df1f4 add minidag proof emitter; wire as default tracer replacing bencode 2026-05-04 02:41:11 +00:00
Simon Cruanes
aa53ae601a port minidag encode/decode from granite (encoding part only) 2026-05-03 19:18:37 +00:00
Simon Cruanes
0c965aec23 proof export into talweg text format 2026-03-19 04:33:12 +00:00
Simon Cruanes
990a1e6f69 format 2026-03-19 04:33:12 +00:00
Simon Cruanes
d9a0b66973 fix warnings 2026-03-19 04:33:12 +00:00
Simon Cruanes
491f368142 gitignore 2026-03-19 04:33:12 +00:00
Simon Cruanes
26d58218d4 sample lia problems 2026-03-19 04:33:12 +00:00
Simon Cruanes
1daf8d6fed
delete plugin 2026-03-19 00:22:55 -04:00
Simon Cruanes
f7a04f1f93 fix compilation error 2026-03-19 03:35:26 +00:00
Simon Cruanes
5fcbaaacac ocamlformat 0.27 2026-03-19 03:27:48 +00:00
Simon Cruanes
fd50e0a34b remove specialized vectors, keep only Vec 2026-03-19 03:27:23 +00:00
Simon Cruanes
08b3da6931 reformat dune files 2026-03-19 03:26:39 +00:00
Simon Cruanes
98128717df refactor: Rrplace Veci and Vec_float with polymorphic Vec 2026-03-14 15:21:01 -04:00
Simon Cruanes
fcbaaae81d Vec: fix bound check error 2026-03-11 03:26:57 -04:00
Simon Cruanes
6c8d6840f8
chore: update workflows 2025-01-27 21:49:09 -05:00
Simon Cruanes
90a5c7bc06
ocamlforamt 2025-01-27 21:49:05 -05:00
Simon Cruanes
8e6036bf3f
chore: CI 2023-12-27 19:45:57 -05:00
Simon Cruanes
13440d60f6
chore: CI 2023-12-27 19:31:55 -05:00
Simon Cruanes
eff6016151
support trace-fuchsia if present 2023-12-27 17:24:35 -05:00
Simon Cruanes
54077446ca
require ocaml 4.08, compat with containers 3.13 2023-12-07 00:14:16 -05:00
Simon Cruanes
85c39d3642
faster CI 2023-12-07 00:03:36 -05:00
Simon Cruanes
43c8e60790
use trace instead of our own custom tracing setup 2023-10-06 22:04:15 -04:00
Simon Cruanes
4bb15f8b5e
comments 2023-10-06 21:35:23 -04:00
Simon Cruanes
c35d721c6d fix: compute model even if (potentially) new interface eqns are produced 
close #19
 2023-06-28 11:42:26 -04:00
Simon Cruanes
3ebc532486 more tests 2023-06-26 15:40:38 -04:00
Simon Cruanes
923cbec6e5 remove debug msg 2023-06-26 15:40:38 -04:00
Simon Cruanes
8d8ef4211b fix sign error 2023-06-26 15:40:38 -04:00
Simon Cruanes
67e9eabf43 add another bug repro 2023-06-26 15:40:38 -04:00
Simon Cruanes
477c780f18 CI 2023-06-26 15:40:38 -04:00
Simon Cruanes
d8612f84c9 doc 2023-06-26 15:40:38 -04:00
Simon Cruanes
2e29ab20dd fix benchpress config 2023-06-26 15:40:38 -04:00
Simon Cruanes
3ba2583966 fix lra: define expressions occurring in subterms properly 
these sub-expressions need to be registered in the Simplex, possibly
using an intermediate variable in case there's an offset.
 2023-06-26 15:40:38 -04:00
Simon Cruanes
c4d3c44c49 warnings and comments 2023-06-26 15:40:38 -04:00
Simon Cruanes
c64bebaf6f fix warning 2023-06-26 15:40:38 -04:00
Simon Cruanes
dcdc55ee1f add non reduced test too 2023-06-26 15:40:38 -04:00
Simon Cruanes
87f9be7fe0 test: add regression test for LRA bug 2023-06-26 15:40:38 -04:00
Simon Cruanes
619da6fbcb
fix warnings 2023-06-23 20:44:01 -04:00
Simon Cruanes
7fbfb8439b
Merge branch 'master' into wip-produce-smtlib-models 2023-04-20 22:10:03 -04:00
Simon Cruanes
659f69f989
opam 2023-04-20 10:40:44 -04:00
Simon Cruanes
40a743badb
update to handle mtime 2.0 2023-02-23 21:02:21 -05:00
Simon Cruanes
4c330e4ed6
ocamlformat 2023-02-23 21:01:34 -05:00
Simon Cruanes
f5ccbb476b
add todo 2022-10-23 20:58:25 -04:00
Simon Cruanes
651f2c1150
warnings 2022-10-23 20:56:10 -04:00
Simon Cruanes
7f5c6d4131
wip: check models 2022-10-23 20:56:05 -04:00
Simon Cruanes
f905b754aa
wip: check models 2022-10-23 20:55:25 -04:00
Simon Cruanes
173908cadc
warnings 2022-10-20 16:12:52 -04:00