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

1378 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Simon Cruanes
bdb41fcdc7 perf: more inlining for checker 2021-08-08 02:39:41 -04:00
Simon Cruanes
b4231d23c1 perf(checker): optimize watch literals 2021-08-08 02:36:30 -04:00
Simon Cruanes
ab6e574298 feat(drup): first version of checker 2021-08-08 02:18:58 -04:00
Simon Cruanes
a8522e66f0 refactor: renaming in DRUP traces 2021-08-08 00:46:58 -04:00
Simon Cruanes
feff94bdbb doc: update guide (models changed, more printers needed) 2021-08-07 21:09:20 -04:00
Simon Cruanes
bef0c810d3 wip: trace checking 
- continue Drup checker
- create sidekick-bin.lib to share parsers
- parse problem+proof for sidekick-check
 2021-08-07 18:10:42 -04:00
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
ed114f8abe feat(sat): check proofs if asked to 2021-08-02 23:17:29 -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