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

1333 commits

This branch
This branch
All branches
Author SHA1 Message Date
Simon Cruanes
ec6fb0d5e1 wip: checker binary 2021-08-07 17:20:52 -04:00
Simon Cruanes
971ae74ecc perf: compile only in native 2021-08-05 10:53:46 -04:00
Simon Cruanes
d117d656c5 test: add basic test for DRUP proof production 2021-08-02 23:48:52 -04:00
Simon Cruanes
e6fc7e7357 feat(sat): produce DRUP proofs if asked to 2021-08-02 23:48:52 -04:00
Simon Cruanes
b9800023ec feat(sat): missing call to on_learnt; better API 2021-08-02 23:48:52 -04:00
Simon Cruanes
a205c429e7 feat(sat): check proofs if asked to 2021-08-02 23:14:52 -04:00
Simon Cruanes
2d081c554b chore: fix makefile 2021-08-02 21:34:37 -04:00
Simon Cruanes
2a2b03ffc8 remove symlinks 2021-08-02 16:05:35 -04:00
Simon Cruanes
74f2844652 wip: DRUP checker 2021-08-02 16:05:35 -04:00
Simon Cruanes
a08cda8c5b test: add a lot more tests (for SAT) 2021-08-02 16:05:35 -04:00
Simon Cruanes
c14070b622 perf: compile in release by default 😡 2021-08-02 16:04:59 -04:00
Simon Cruanes
515a720d00 detail 2021-07-22 09:57:53 -04:00
Simon Cruanes
233df98229 perf(sat): proper GC for clauses 
GC is now eager in the cleanup of watchlists and more elaborate.

It starts by marking all clauses justifying literals on the trail,
because we cannot remove them yet (they might be used in resolution
steps during clause analysis).

Then, we sort set of learnt clauses by decreasing activity, and pop them
one by one until the target size is reached.  Clauses that are marked,
because they are on the trail, are kept on the side so we can push them
back at the end.

For each clause we want to remove, we start by marking it "dead".
Then we mark its two watch literals are "dirty", which means we will
need to purge their watchlists from dead clauses.

Then we purge watchlists (remove deadclauses entirely). At this point
the dead clauses are unreachable from both trail and watchlists.
We can remove all data for each such clause, and put their index for
recycling so another new clause can reuse their slot.

Finally we unmark dirty literals and saved-by-trail-explanation
explanation clauses.
 2021-07-21 20:29:27 -04:00
Simon Cruanes
a174e5958a more stats for main 2021-07-21 20:24:27 -04:00
Simon Cruanes
77c61b536e refactor(sat): rename some bitfields, leaner clause creation 2021-07-21 20:24:03 -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
97d87cc58f perf: tiny detail in int indices in solver 2021-07-20 23:34:38 -04:00
Simon Cruanes
29892d07de feat(util): Vec_float based on bigarrays 2021-07-20 23:33:57 -04:00
Simon Cruanes
a03d7f6bef fix 2021-07-20 23:31:21 -04:00
Simon Cruanes
11b1ea4eda feat(vec): more 2021-07-20 23:28:54 -04:00
Simon Cruanes
d53b3c291e feat: add "drup" case to proofs 2021-07-20 23:27:11 -04:00
Simon Cruanes
89051fd3ad perf(solver): use VecI32 in the heap 
this reduces the size of the heap (4 bits per element, not 8), and
reduces GC work by not scanning the bigarray
 2021-07-20 10:07:43 -04:00
Simon Cruanes
d08d5fe9c4 feat(util): add VecI32 based on bigarray 2021-07-20 10:07:29 -04:00
Simon Cruanes
347e098fc2 misc 2021-07-20 09:20:14 -04:00
Simon Cruanes
f2b2bbb973 some stats for the SAT solver 2021-07-19 21:44:58 -04:00
Simon Cruanes
b624a1ca5d cleanup: remove commented code 2021-07-19 21:15:16 -04:00
Simon Cruanes
e30cf9fdbf perf: allocate less in conflict analysis 
use preallocated vectors
 2021-07-19 21:13:00 -04:00
Simon Cruanes
7463bd66aa fix(sat): sign error 2021-07-19 09:57:02 -04:00
Simon Cruanes
227662f789 detail 2021-07-19 09:57:02 -04:00
Simon Cruanes
7f18e5f29a fix 2021-07-19 09:57:02 -04:00
Simon Cruanes
47bb521158 wip: refactor SAT solver 2021-07-19 09:57:02 -04:00
Simon Cruanes
b85c47ece1 wip: refactor(sat): use struct-of-array for atom/var 2021-07-19 09:57:02 -04:00
Simon Cruanes
162fd37d9d wip: refactor 2021-07-19 09:57:02 -04:00
Simon Cruanes
2107b3de7e feat(util): a Bitvec module, refactor testing 2021-07-19 09:57:02 -04:00
Simon Cruanes
97aab34e46 statistics for pure sat solver 2021-07-19 09:57:02 -04:00
Simon Cruanes
923033f9bf feat: mli for the SAT solver 2021-07-19 09:17:20 -04:00
Simon Cruanes
cab541e712 Merge branch 'wip-vendored-msat' 2021-07-18 20:50:18 -04:00
Simon Cruanes
15d86d7c62 refactor(sat): use first-class modules instead of records 2021-07-18 19:18:42 -04:00
Simon Cruanes
041e83139d feat: make mtime optional with dummy "tef" backend 2021-07-18 10:31:03 -04:00
Simon Cruanes
c7bf4b01e7 feat: optional memtrace support 2021-07-18 10:29:14 -04:00
Simon Cruanes
ff5cf1239c chore: CI on PRs 2021-07-18 09:29:55 -04:00
Simon Cruanes
5faa1d6ef7 chore: try to build again 2021-07-18 08:04:56 -04:00
Simon Cruanes
1aa160fe56 use a pure sat solver for cnf files 2021-07-18 02:46:04 -04:00
Simon Cruanes
4cb8887639 wip: remove all traces of mcsat from src/sat 2021-07-18 02:14:56 -04:00
Simon Cruanes
564dcec252 cleanup msat, rename it sidekick.sat 2021-07-18 01:40:55 -04:00
Simon Cruanes
4a337a85d3 cleanup msat 2021-07-18 01:29:28 -04:00
Simon Cruanes
1a58ab0bfc vendor current msat in src/sat for further modifications 2021-07-18 01:26:11 -04:00
Simon Cruanes
d024a6a3f0 prepare for vendoring 2021-07-18 01:24:04 -04:00
Simon Cruanes
1c2b37eb72 details 2021-07-04 22:48:55 -04:00