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

1392 commits

This branch
This branch
All branches
Author SHA1 Message Date
Simon Cruanes
8eb50afecb
feat(smt): provide SAT solver to theories upon initialization 2021-09-02 22:24:59 -04:00
Simon Cruanes
387ab518c4
feat: clause pools in SMT 2021-09-02 09:32:01 -04:00
Simon Cruanes
85c00ecfa2
cleanup 2021-09-01 09:00:39 -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
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
5017d9f8bf
Merge branch 'wip-drup-check' 2021-08-24 18:09:31 -04:00
Simon Cruanes
5505ece5fb
chore: fix warning 2021-08-23 10:49:12 -04:00
Simon Cruanes
07d512badc
fix: remove dep on mtime in checker 2021-08-23 10:17:51 -04:00
Simon Cruanes
28fad1e408
chore: ci on all branches 2021-08-23 10:03:16 -04:00
Simon Cruanes
d841090e1c
feat(checker): ability to read .drup.gz files 2021-08-23 00:10:37 -04:00
Simon Cruanes
2f41a54719
feat(main): for pure SAT, emit proofs into file or locally 2021-08-23 00:10:34 -04:00
Simon Cruanes
bb682b8080
fix(sat): emit proofs where needed 2021-08-23 00:08:09 -04:00
Simon Cruanes
fa04cb7997
refactor(th-bool): remove cache and most recursion 
the preprocessing framework already takes care of both.
 2021-08-22 15:50:42 -04:00
Simon Cruanes
baecce0946
feat: use Stat in SAT solver 2021-08-22 01:56:54 -04:00
Simon Cruanes
672f828c82
perf: return to default-pol=true 
previous commit fixed sign error (move from `negated` to `same_sign`
so restore good behavior
 2021-08-22 01:44:37 -04:00
Simon Cruanes
9aee35c6ce
fix other issue in th-bool preprocessing 2021-08-22 01:31:59 -04:00
Simon Cruanes
27796da5a8
fix preprocessing in th-bool 2021-08-22 01:29:01 -04:00
Simon Cruanes
e93e084eac
refactor: eager proofs; stronger preprocessing 
proofs are now directly emitted (almost) everywhere, which simplifies
a lot of things. preprocessing is more recursive (a bit too much
really).
 2021-08-22 01:13:41 -04:00
Simon Cruanes
0668f28ac7
try to fix boolean terms not decided by SAT solver 2021-08-21 14:00:31 -04:00
Simon Cruanes
075e251aed
fix: bad sign in SAT solver 2021-08-21 13:41:30 -04:00
Simon Cruanes
0e77c9ef33
perf(solver): default-pol=false 2021-08-20 18:49:15 -04:00
Simon Cruanes
22638a0c0b
tmp: use dummy proof in pure sat solver 2021-08-20 18:49:15 -04:00
Simon Cruanes
4cada7e7b6
perf 2021-08-20 18:18:30 -04:00
Simon Cruanes
1ab7d34a7d
refactor: make it compile again 2021-08-20 18:18:30 -04:00
Simon Cruanes
1d3867acb5
perf: use VecI32 for clause vector 2021-08-20 18:18:26 -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
8bc1f1c864 feat: inner DRUP proof checking for pure-sat-solver 2021-08-19 00:15:00 -04:00
Simon Cruanes
9f01b98cde wip: imperative proofs 
- getting closer to having the SMT solver compile again
- dummy proof implementation
- DRUP proof implementation for pure SAT solver
 2021-08-18 23:59:39 -04:00
Simon Cruanes
458f5fa9b6 finish renaming 2021-08-18 00:03:16 -04:00
Simon Cruanes
2bb6c94925 remove dead code 2021-08-18 00:01:54 -04:00
Simon Cruanes
10a4cf4c29 refactor: rename sidekick-msat-solver into sidekick-smt-solver 2021-08-18 00:01:25 -04:00
Simon Cruanes
6800b44b1c refactor: in msat-solver, adapt to new proofs 2021-08-17 23:59:43 -04:00
Simon Cruanes
7bead748a6 refactor: move SAT_PROOF into sidekick.core 
SAT proofs are part of bigger proofs, now. And we expect them to work on
the literals of CDCL(T) directly, bypassing the low level boolean atoms
 2021-08-17 23:59:02 -04:00
Simon Cruanes
cc1a93fa74 feat: add sidekick.lit small library for literals 2021-08-17 23:58:49 -04:00
Simon Cruanes
d40ce304ae wip: refactor proofs into traces 2021-08-17 09:29:46 -04:00
Simon Cruanes
27e775ee04 wip: refactor proofs for SMT 2021-08-12 22:05:49 -04:00
Simon Cruanes
9975a471f7 perf(drup): restore Atoms as integers 2021-08-11 09:30:53 -04:00
Simon Cruanes
51293bc66a feat(drup-check): functorize over atoms 2021-08-10 00:13:37 -04:00