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

1608 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
633a658e0c
wip: use new sigs 2022-07-15 23:51:53 -04:00
Simon Cruanes
ab6bcf8cbe
add many small sigs libraries 2022-07-15 23:51:41 -04:00
Simon Cruanes
679b35012b
SAT: remove clause pools 2022-07-15 21:12:04 -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
ba4b4c0302
rename build 2022-07-14 22:29:48 -04:00
Simon Cruanes
44ca7daf75
remove file 2022-07-14 22:29:12 -04:00
Simon Cruanes
325acc5724
fix tests 2022-07-14 22:17:25 -04:00
Simon Cruanes
85c850d464
update tests after removal of lia 2022-07-14 22:10:14 -04:00
Simon Cruanes
a1bc186d2e
use ocamlformat 2022-07-14 22:09:13 -04:00
Simon Cruanes
e2b9b2874c
fix more warnings; remove never completed LIA stuff 2022-07-14 22:01:23 -04:00
Simon Cruanes
fd500a3d7d
fix some warnings 2022-07-14 21:56:37 -04:00
Simon Cruanes
96bc3e2340
update tests 2022-07-14 21:48:19 -04:00
Simon Cruanes
b16fce6f26
Merge branch 'master' into wip-model-th-comb 2022-07-14 21:46:36 -04:00
Simon Cruanes
1946a5e7cf
feat: construct model from congruence closure after th-combination 
we already obtain a model from theories, and saturate the congruence
closure with it, it's a shame not to use it.
 2022-02-18 14:59:27 -05:00
Simon Cruanes
a388c96fe3
cc: remove new_merges 2022-02-18 14:59:27 -05:00
Simon Cruanes
cdc5d160a7
cc: use backtrackable table 2022-02-18 14:59:27 -05:00
Simon Cruanes
d153c80ca5
details 2022-02-18 14:59:27 -05:00
Simon Cruanes
8530c07c59
lra: better debug 2022-02-18 14:59:27 -05:00
Simon Cruanes
8fb0152754
feat(smt): simplify the final check loop significantly 2022-02-18 14:59:26 -05:00
Simon Cruanes
da18ba3620
perf(cc): only assign model values to term present in CC 2022-02-18 14:59:26 -05:00
Simon Cruanes
6e941683a2
add with_model_mode to congruence closure 
this mode:
- enables `set_mode_value`
- disables all callbacks
- can only be used locally with a push/pop wrapper
 2022-02-18 14:59:26 -05:00
Simon Cruanes
95f84b4854
refactor(th-comb): provide full model to the CC 
this way it can fail on merges of classes assigned conflicting value.
 2022-02-18 14:59:26 -05:00
Simon Cruanes
fd66039c8d
wip: theory combination by exposing model (classes) directly to CC 2022-02-18 14:59:26 -05:00
Simon Cruanes
65d4a90df1
tef: stop compression, too fragile. just emit a .json file 2022-02-18 14:59:26 -05:00
Simon Cruanes
f26d178380
feat(main): catch ctrl-c to cleanup 
this allows us to cleanup progress bar, print stats, finish tracing,
etc.
 2022-02-18 14:59:26 -05:00
Simon Cruanes
52cae96ee2
improve progress bar and printingof stat after timeout 2022-02-18 14:59:25 -05:00
Simon Cruanes
20791a551f
feat: enforce time/memory limits in main runner 2022-02-17 13:09:48 -05:00
Simon Cruanes
e177534a46
chore: ugprade bare encoding 2022-02-16 14:20:27 -05:00
Simon Cruanes
c0288902c0
feat: check on_progress in more places 2022-02-16 13:24:43 -05:00
Simon Cruanes
5b0a2ad4a4
debug 2022-02-15 16:57:25 -05:00
Simon Cruanes
f3947f2237
update model construction function 2022-02-15 12:23:04 -05:00
Simon Cruanes
7f45cc6967
fix test 2022-02-14 11:36:50 -05:00
Simon Cruanes
fb552ba8b2
update expected test 2022-02-14 11:20:59 -05:00
Simon Cruanes
98c30bf0cc
updates and cleanup 2022-02-14 10:46:08 -05:00
Simon Cruanes
73289d1ded
test: regressions test for LRA 2022-02-08 13:45:43 -05:00
Simon Cruanes
e481c74398
refactor(LRA): new preprocessing, new shape of terms 2022-02-08 13:14:24 -05:00
Simon Cruanes
c22fc62f3e
base: remove simplex cases in arith terms 2022-02-08 13:14:07 -05:00
Simon Cruanes
f268e86100
refactor(smt-solver): preprocess literals in push_decision 2022-02-08 13:13:23 -05:00
Simon Cruanes
a81a21c341
core: add n_levels to monoid 2022-02-08 13:13:00 -05:00
Simon Cruanes
1d702029ee
fix(typecheck): use logic to decide default type of numerals 2022-02-08 13:12:29 -05:00
Simon Cruanes
82acf271d3
improve zarith and backtrackable table 2022-02-08 13:12:07 -05:00
Simon Cruanes
fbf7c5e090
chore: makefile 2022-02-08 13:11:36 -05:00
Simon Cruanes
d9a701140c
debug 2022-02-07 10:57:39 -05:00
Simon Cruanes
d11b9d585c
fix(smt): improve theory combination a bit 2022-02-04 16:40:55 -05:00
Simon Cruanes
ab74b1a792
fix(lra): preprocessing of linexps with non-zero constants 2022-02-04 16:16:00 -05:00
Simon Cruanes
cbc9c5ac6f
refactor(smt): preprocessing is now using a queue of delayed actions 
- preprocessing doesn't simplify anymore, it assumes terms are already
  simplified. It only adds clauses/adds literals, it does not return
  new terms.
- adding clauses/literals to SAT is done as delayed actions, to avoid
  issues of reentrancy.
  These actions are performed after preprocessing, in a loop that has
  access to the SAT solver.
 2022-02-04 16:08:01 -05:00