simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-18 00:26:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Commit graph

  • 4a2367b1bd
         refactor: use Atom.Vec (a VecI32) for atom vectors Simon Cruanes 2021-08-31 09:30:05 -04:00
  • 1877c00c02
         wip: clauses pools Simon Cruanes 2021-08-30 09:32:32 -04:00
  • 81caf4824e
         wip: feat: additional clause allocators in SAT Simon Cruanes 2021-08-24 18:55:31 -04:00
  • 73b39fe075
         fix more warnings Simon Cruanes 2021-08-27 21:33:12 -04:00
  • 744f8d60b8
         update index Simon Cruanes 2021-08-27 09:49:42 -04:00
  • e9675743b0 deploy: e7e8873295 c-cube 2021-08-27 13:29:59 +00:00
  • e7e8873295
         fix more warnings Simon Cruanes 2021-08-27 09:28:59 -04:00
  • b33f5fa5b1
         fix tests Simon Cruanes 2021-08-26 09:19:21 -04:00
  • 4e0eae6d9e
         perf: restore previous handling of bitfields wip-dod-cc Simon Cruanes 2021-08-26 00:10:43 -04:00
  • 1fad70d0ae deploy: 782afa4415 c-cube 2021-08-26 03:54:35 +00:00
  • 4fd291b117
         wip: continue refactor Simon Cruanes 2021-08-25 23:51:20 -04:00
  • 4d312ad1aa
         refactor(cc): move to struct-of-array Simon Cruanes 2021-08-25 22:24:29 -04:00
  • 0efef5b6ef
         wip: refactor(CC): use data oriented techniques (SoA) Simon Cruanes 2021-08-25 09:36:40 -04:00
  • 782afa4415
         feat: move Int_id into its own module Simon Cruanes 2021-08-25 09:36:24 -04:00
  • d0a9eb491d deploy: 7f42c0c00587a595c8c75b70ea2451f65cabe251 c-cube 2021-08-25 13:37:50 +00:00
  • 68250603c4
         fix compat Simon Cruanes 2021-08-24 19:41:36 -04:00
  • daed868aaa deploy: 5017d9f8bf c-cube 2021-08-24 22:15:31 +00:00
  • 5017d9f8bf
         Merge branch 'wip-drup-check' Simon Cruanes 2021-08-24 18:09:31 -04:00
  • 5505ece5fb
         chore: fix warning wip-drup-check Simon Cruanes 2021-08-23 10:49:12 -04:00
  • 07d512badc
         fix: remove dep on mtime in checker Simon Cruanes 2021-08-23 10:17:51 -04:00
  • 28fad1e408
         chore: ci on all branches Simon Cruanes 2021-08-23 10:03:16 -04:00
  • d841090e1c
         feat(checker): ability to read .drup.gz files Simon Cruanes 2021-08-23 00:10:37 -04:00
  • 2f41a54719
         feat(main): for pure SAT, emit proofs into file or locally Simon Cruanes 2021-08-23 00:08:20 -04:00
  • bb682b8080
         fix(sat): emit proofs where needed Simon Cruanes 2021-08-23 00:08:09 -04:00
  • fa04cb7997
         refactor(th-bool): remove cache and most recursion Simon Cruanes 2021-08-22 15:50:42 -04:00
  • baecce0946
         feat: use Stat in SAT solver Simon Cruanes 2021-08-22 01:56:54 -04:00
  • 672f828c82
         perf: return to default-pol=true Simon Cruanes 2021-08-22 01:44:37 -04:00
  • 9aee35c6ce
         fix other issue in th-bool preprocessing Simon Cruanes 2021-08-22 01:31:59 -04:00
  • 27796da5a8
         fix preprocessing in th-bool Simon Cruanes 2021-08-22 01:29:01 -04:00
  • e93e084eac
         refactor: eager proofs; stronger preprocessing Simon Cruanes 2021-08-22 01:13:41 -04:00
  • f5240a857b
         wip: refactor: replace literals by mere terms wip-no-lits Simon Cruanes 2021-08-21 14:39:37 -04:00
  • 0668f28ac7
         try to fix boolean terms not decided by SAT solver Simon Cruanes 2021-08-21 14:00:31 -04:00
  • 075e251aed
         fix: bad sign in SAT solver Simon Cruanes 2021-08-21 13:41:30 -04:00
  • 0e77c9ef33
         perf(solver): default-pol=false Simon Cruanes 2021-08-20 18:46:16 -04:00
  • 22638a0c0b
         tmp: use dummy proof in pure sat solver Simon Cruanes 2021-08-20 18:45:39 -04:00
  • 4cada7e7b6
         perf Simon Cruanes 2021-08-20 18:16:42 -04:00
  • 1ab7d34a7d
         refactor: make it compile again Simon Cruanes 2021-08-20 09:59:10 -04:00
  • 1d3867acb5
         perf: use VecI32 for clause vector Simon Cruanes 2021-08-20 18:18:26 -04:00
  • 5372170733
         fix: make it compile again Simon Cruanes 2021-08-20 18:18:14 -04:00
  • c8eb1ec29e
         feat(util): add Vec_sig to express common vector interface Simon Cruanes 2021-08-20 18:04:54 -04:00
  • 3fbb9af664 refactor(sat): hide atoms, API now talks only about literals Simon Cruanes 2021-08-19 09:35:54 -04:00
  • 8bc1f1c864 feat: inner DRUP proof checking for pure-sat-solver Simon Cruanes 2021-08-19 00:15:00 -04:00
  • 9f01b98cde wip: imperative proofs Simon Cruanes 2021-08-18 23:59:39 -04:00
  • 76df299a36 wip: perf(bitvec): use a VecI32.t underneath wip-dod-sat-bitvec-i32 Simon Cruanes 2021-08-18 12:43:56 -04:00
  • c81d10426f chore: makefile Simon Cruanes 2021-08-18 12:43:48 -04:00
  • 458f5fa9b6 finish renaming Simon Cruanes 2021-08-18 00:03:16 -04:00
  • 2bb6c94925 remove dead code Simon Cruanes 2021-08-18 00:01:54 -04:00
  • 10a4cf4c29 refactor: rename sidekick-msat-solver into sidekick-smt-solver Simon Cruanes 2021-08-18 00:01:25 -04:00
  • 6800b44b1c refactor: in msat-solver, adapt to new proofs Simon Cruanes 2021-08-17 23:59:43 -04:00
  • 7bead748a6 refactor: move SAT_PROOF into sidekick.core Simon Cruanes 2021-08-17 23:59:02 -04:00
  • cc1a93fa74 feat: add sidekick.lit small library for literals Simon Cruanes 2021-08-17 23:58:49 -04:00
  • d40ce304ae wip: refactor proofs into traces Simon Cruanes 2021-08-17 09:29:46 -04:00
  • 27e775ee04 wip: refactor proofs for SMT Simon Cruanes 2021-08-12 22:05:49 -04:00
  • 9975a471f7 perf(drup): restore Atoms as integers Simon Cruanes 2021-08-11 09:30:53 -04:00
  • 51293bc66a feat(drup-check): functorize over atoms Simon Cruanes 2021-08-10 00:13:37 -04:00
  • bdb41fcdc7 perf: more inlining for checker Simon Cruanes 2021-08-08 02:39:41 -04:00
  • b4231d23c1 perf(checker): optimize watch literals Simon Cruanes 2021-08-08 02:36:30 -04:00
  • ab6e574298 feat(drup): first version of checker Simon Cruanes 2021-08-08 02:18:58 -04:00
  • a8522e66f0 refactor: renaming in DRUP traces Simon Cruanes 2021-08-08 00:46:58 -04:00
  • feff94bdbb doc: update guide (models changed, more printers needed) Simon Cruanes 2021-08-07 21:09:20 -04:00
  • bef0c810d3 wip: trace checking Simon Cruanes 2021-08-07 18:10:42 -04:00
  • ec6fb0d5e1 wip: checker binary Simon Cruanes 2021-08-07 17:20:52 -04:00
  • 971ae74ecc perf: compile only in native Simon Cruanes 2021-08-05 10:53:46 -04:00
  • d117d656c5 test: add basic test for DRUP proof production Simon Cruanes 2021-08-02 23:47:45 -04:00
  • e6fc7e7357 feat(sat): produce DRUP proofs if asked to Simon Cruanes 2021-08-02 23:48:04 -04:00
  • b9800023ec feat(sat): missing call to on_learnt; better API Simon Cruanes 2021-08-02 23:48:27 -04:00
  • ed114f8abe feat(sat): check proofs if asked to Simon Cruanes 2021-08-02 23:13:18 -04:00
  • a205c429e7 feat(sat): check proofs if asked to Simon Cruanes 2021-08-02 23:13:18 -04:00
  • 2d081c554b chore: fix makefile Simon Cruanes 2021-08-02 21:34:37 -04:00
  • 2a2b03ffc8 remove symlinks Simon Cruanes 2021-07-30 11:34:58 -04:00
  • 74f2844652 wip: DRUP checker Simon Cruanes 2021-07-23 00:08:52 -04:00
  • a08cda8c5b test: add a lot more tests (for SAT) Simon Cruanes 2021-07-22 23:31:55 -04:00
  • c14070b622 perf: compile in release by default 😡 wip-dod-sat Simon Cruanes 2021-08-02 16:04:59 -04:00
  • 62f45777a1 feat(sat): implement phase saving in the SAT solver wip-sat-phase-saving-2021-07-22 Simon Cruanes 2021-07-22 09:58:04 -04:00
  • 515a720d00 detail Simon Cruanes 2021-07-22 09:57:53 -04:00
  • 233df98229 perf(sat): proper GC for clauses Simon Cruanes 2021-07-21 20:24:33 -04:00
  • a174e5958a more stats for main Simon Cruanes 2021-07-21 20:24:27 -04:00
  • 77c61b536e refactor(sat): rename some bitfields, leaner clause creation Simon Cruanes 2021-07-21 20:24:03 -04:00
  • 3aa25cb2a2 sat: use an atom array for clauses again Simon Cruanes 2021-07-21 10:02:56 -04:00
  • 8b94e8404f wip: data-oriented clauses Simon Cruanes 2021-07-20 23:34:58 -04:00
  • 97d87cc58f perf: tiny detail in int indices in solver Simon Cruanes 2021-07-20 23:34:38 -04:00
  • 29892d07de feat(util): Vec_float based on bigarrays Simon Cruanes 2021-07-20 23:33:37 -04:00
  • a03d7f6bef fix Simon Cruanes 2021-07-20 23:30:51 -04:00
  • 11b1ea4eda feat(vec): more Simon Cruanes 2021-07-20 23:28:18 -04:00
  • d53b3c291e feat: add "drup" case to proofs Simon Cruanes 2021-07-20 23:27:11 -04:00
  • 89051fd3ad perf(solver): use VecI32 in the heap Simon Cruanes 2021-07-20 10:07:43 -04:00
  • d08d5fe9c4 feat(util): add VecI32 based on bigarray Simon Cruanes 2021-07-20 10:07:29 -04:00
  • 347e098fc2 misc Simon Cruanes 2021-07-19 23:09:34 -04:00
  • 674a619ca7 deploy: eb23644195 c-cube 2021-07-20 04:52:29 +00:00
  • eb23644195 fix ci for gh-pages Simon Cruanes 2021-07-20 00:46:16 -04:00
  • 6f7f2b2823 fix doc Simon Cruanes 2021-07-20 00:35:49 -04:00
  • f2b2bbb973 some stats for the SAT solver Simon Cruanes 2021-07-19 21:44:58 -04:00
  • b624a1ca5d cleanup: remove commented code Simon Cruanes 2021-07-19 21:15:16 -04:00
  • e30cf9fdbf perf: allocate less in conflict analysis Simon Cruanes 2021-07-19 21:13:00 -04:00
  • 7463bd66aa fix(sat): sign error Simon Cruanes 2021-07-19 09:45:34 -04:00
  • 227662f789 detail Simon Cruanes 2021-07-19 09:23:32 -04:00
  • 7f18e5f29a fix Simon Cruanes 2021-07-19 00:27:20 -04:00
  • 47bb521158 wip: refactor SAT solver Simon Cruanes 2021-07-19 00:23:17 -04:00
  • b85c47ece1 wip: refactor(sat): use struct-of-array for atom/var Simon Cruanes 2021-07-18 22:28:02 -04:00
  • 162fd37d9d wip: refactor Simon Cruanes 2021-07-18 20:49:15 -04:00