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

1579 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
3589592296
wip: use real proofs 2021-10-16 22:00:29 -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
beda972def
wip: feat(base): proof chunk storage 2021-10-14 21:41:47 -04:00
Simon Cruanes
feb7a354e9
fix test 2021-10-13 00:30:43 -04:00
Simon Cruanes
12037c6ba2
test only >= 4.08 on CI 2021-10-12 23:05:47 -04:00
Simon Cruanes
b22e4b96ce
bump min requirement to 4.08 2021-10-12 23:05:25 -04:00
Simon Cruanes
a6b303bb90
remove dep on bare-encoding 2021-10-12 22:52:52 -04:00
Simon Cruanes
e90df644c4
chore: make CI ignore promotion rules 2021-10-12 22:46:41 -04:00
Simon Cruanes
3d17feab12
use standalone mode and promote for the BARE encoding of proofs 2021-10-12 22:45:45 -04:00
Simon Cruanes
fd1d068997
proof stubs and sat proof 2021-10-12 22:13:28 -04:00
Simon Cruanes
6fae75f94d
add Vec_unit to util 2021-10-12 22:13:05 -04:00
Simon Cruanes
4308eba04d
fix 2021-10-11 23:19:40 -04:00
Simon Cruanes
af901f54b1
proof production for th-data 2021-10-11 19:57:25 -04:00
Simon Cruanes
1779b7115a
wip: proof production (incl. better tracking of proofs in CC) 2021-10-11 14:27:14 -04:00
Simon Cruanes
0550f6fcfa
wip: proof production 2021-10-09 00:51:15 -04:00
Simon Cruanes
d3537f2c3f
wip: refactor proof 2021-10-07 20:49:39 -04:00
Simon Cruanes
bbb995b0d5
refactor some names related to proofs; wip add unit paramod 2021-10-03 20:32:37 -04:00
Simon Cruanes
04f1ba063d
wip: adapt CC to new proofs 2021-09-29 22:19:16 -04:00
Simon Cruanes
df40b5a5c1
wip: refactor(sat): generate detailed proofs again 
because proofs now require hypotheses but not in a resolution order, we
can still do conflict minimization.
 2021-09-29 22:18:36 -04:00
Simon Cruanes
4621cc948f
feat(core): change the way proofs work 
Now a proof returns a `step_id` which identifies its resulting clause.
This might be a dummy value when proofs are disabled.

We attach a step_id to each new clause to make sure it's properly
tracked, but step_ids might outlive their clause (and the actual proof
data might be on disk, only keeping in ram a small unique identifier).
 2021-09-29 22:16:22 -04:00
Simon Cruanes
313e9db026
feat(vec): add copy 2021-09-29 22:16:10 -04:00
Simon Cruanes
5e0652687a
wip: proof production using BARE for storage 2021-09-28 21:06:01 -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
acc682c5af
refactor(cc): simple renaming 2021-09-27 19:26:04 -04:00
Simon Cruanes
86512dbed0
utils 2021-09-27 19:22:48 -04:00
Simon Cruanes
c9e257d40b
cleanup 2021-09-27 12:14:04 -04:00
Simon Cruanes
5bed2d1c5f
detail 2021-09-26 23:56:40 -04:00
Simon Cruanes
a22bfe06c1
remove debug msgs 2021-08-31 23:19:06 -04:00
Simon Cruanes
debd8bcaf8
fix warning 2021-08-31 23:06:48 -04:00
Simon Cruanes
350a23d99e
feat: minimize conflicts 
similar to minisat's level 2 of minimization.
 2021-08-31 23:04:32 -04:00
Simon Cruanes
5080195c5b
feat: conflict minimization à la minisat 2021-08-31 22:59:38 -04:00
Simon Cruanes
521340a23f
feat: first full implem of clause pools 2021-08-31 22:56:42 -04:00
Simon Cruanes
10dca21f59
refactor: remove history in conflict resolution; remove simpls 
no need to simplify reasons anymore, we rely on DRUP for that.
 2021-08-31 22:56:11 -04:00
Simon Cruanes
f86498b386
feat: make it compile 2021-08-31 18:59:44 -04:00
Simon Cruanes
16bb65ebfa
wip: clause pools 2021-08-31 09:30:28 -04:00
Simon Cruanes
4a2367b1bd
refactor: use Atom.Vec (a VecI32) for atom vectors 2021-08-31 09:30:05 -04:00
Simon Cruanes
1877c00c02
wip: clauses pools 2021-08-30 09:32:32 -04:00
Simon Cruanes
81caf4824e
wip: feat: additional clause allocators in SAT 2021-08-30 09:03:37 -04:00
Simon Cruanes
73b39fe075
fix more warnings 2021-08-27 21:34:26 -04:00
Simon Cruanes
e7e8873295
fix more warnings 2021-08-27 09:28:59 -04:00
Simon Cruanes
b33f5fa5b1
fix tests 2021-08-26 09:19:21 -04:00