simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-05-05 17:04:39 -04:00
Code Issues Projects Releases Packages Wiki Activity Actions

Commit graph

  • 51a784d487 deploy: 5bed2d1c5f c-cube 2021-09-27 04:02:21 +00:00
  • 5bed2d1c5f
         detail Simon Cruanes 2021-09-26 23:56:40 -04:00
  • aaec84dfb6
         wip: gc atoms and reuse them wip-dyn-trans-gc-atoms Simon Cruanes 2021-09-26 21:35:34 -04:00
  • f640bd23a5
         perf(sat): use Atom.Vec for temporary atom array Simon Cruanes 2021-09-26 21:35:14 -04:00
  • aacf74f4cf
         feat(vec): factor a bit of code for auxiliary functions in vectors Simon Cruanes 2021-09-26 21:01:04 -04:00
  • bbe2c6c5bb
         fix docstrings Simon Cruanes 2021-09-26 21:00:51 -04:00
  • c6adc9b25f
         feat(dyn-trans): provide config record when instantiating theory Simon Cruanes 2021-09-24 22:44:52 -04:00
  • e442c440ab
         feat(dyn-trans): track activity of terms to guide instantiation Simon Cruanes 2021-09-20 06:30:39 -04:00
  • bdb45bfb76
         wip: feat(dyn-trans): provide config via env vars Simon Cruanes 2021-09-19 13:07:06 -04:00
  • 3ff64a3817
         feat(sat): refactor a bit clause pools; add stats Simon Cruanes 2021-09-19 13:06:53 -04:00
  • 21e8d6c803
         feat(cc): expose more functions for N.t->literals Simon Cruanes 2021-09-19 13:05:43 -04:00
  • 0902777527
         feat(core): provide mk_eqn in CC Simon Cruanes 2021-09-19 13:03:44 -04:00
  • 1188c54d3c
         update doc Simon Cruanes 2021-09-19 12:55:00 -04:00
  • 45de142b22
         detail Simon Cruanes 2021-09-13 06:46:54 -04:00
  • b108d9f3df
         basic proof emission for dyn-trans Simon Cruanes 2021-09-13 06:44:59 -04:00
  • 3284cfffd4
         feat(dyn-trans): first implementation, quite aggressive Simon Cruanes 2021-09-13 06:35:03 -04:00
  • 677cc0c116
         more hooks in CC (to add clauses) Simon Cruanes 2021-09-13 06:34:45 -04:00
  • 3ea7064de4
         utils Simon Cruanes 2021-09-13 06:34:21 -04:00
  • d1db53f002
         setup dyn-trans in main solver Simon Cruanes 2021-09-09 08:57:14 -04:00
  • 804759f873
         refactor(cc): simple renaming Simon Cruanes 2021-09-09 08:57:03 -04:00
  • 7348a0a481
         wip: theory for dyn-trans axioms Simon Cruanes 2021-09-09 08:56:47 -04:00
  • 01a4bfc50c
         todo Simon Cruanes 2021-09-05 10:56:06 -04:00
  • 8eb50afecb
         feat(smt): provide SAT solver to theories upon initialization wip-custom-clause-allocators Simon Cruanes 2021-09-02 22:24:59 -04:00
  • 387ab518c4
         feat: clause pools in SMT Simon Cruanes 2021-09-02 09:32:01 -04:00
  • 85c00ecfa2
         cleanup Simon Cruanes 2021-09-01 09:00:39 -04:00
  • a22bfe06c1
         remove debug msgs Simon Cruanes 2021-08-31 23:19:06 -04:00
  • debd8bcaf8
         fix warning Simon Cruanes 2021-07-19 23:05:03 -04:00
  • 350a23d99e
         feat: minimize conflicts Simon Cruanes 2021-07-19 22:35:23 -04:00
  • 5080195c5b
         feat: conflict minimization à la minisat Simon Cruanes 2019-01-25 20:06:52 -06:00
  • 521340a23f
         feat: first full implem of clause pools Simon Cruanes 2021-08-31 22:56:42 -04:00
  • 10dca21f59
         refactor: remove history in conflict resolution; remove simpls Simon Cruanes 2021-08-31 22:56:11 -04:00
  • f86498b386
         feat: make it compile Simon Cruanes 2021-08-31 18:59:44 -04:00
  • 16bb65ebfa
         wip: clause pools Simon Cruanes 2021-08-31 09:30:28 -04:00
  • 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