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

Commit graph

  • 0abe4b7020
         wip: decode more proof steps to quip Simon Cruanes 2021-10-27 21:50:28 -04:00
  • 992b93abcf
         fix(sat): clause in a unsat result must not contain 0-level literals Simon Cruanes 2021-10-27 20:19:01 -04:00
  • 5a6019f834
         missing module Simon Cruanes 2021-10-26 22:04:33 -04:00
  • 4a30a06f87
         wip: reconstruct quip proof from binary proof-trace Simon Cruanes 2021-10-26 21:57:17 -04:00
  • d8518ae942
         wip: standalone module for Quip proofs Simon Cruanes 2021-10-25 19:52:00 -04:00
  • b5749a1b72
         emit many more proof steps Simon Cruanes 2021-10-22 21:31:44 -04:00
  • c2b8d93cf4
         refactor proof storage Simon Cruanes 2021-10-21 23:28:53 -04:00
  • a871192c5e
         fix bug in proof emission Simon Cruanes 2021-10-21 20:53:06 -04:00
  • 84f7a39423
         fix doc test Simon Cruanes 2021-10-21 20:42:12 -04:00
  • 8ac2267595
         add a simple binary to dump proof traces Simon Cruanes 2021-10-21 20:33:10 -04:00
  • 7e40851e1b
         use sidekick-base.proof-trace in base Simon Cruanes 2021-10-21 20:32:47 -04:00
  • 254d6a1906
         feat: library for the proof step serialization Simon Cruanes 2021-10-21 20:32:34 -04:00
  • 63e7d6659e
         wip: dump more steps to the trace file Simon Cruanes 2021-10-20 20:41:51 -04:00
  • f5172a7927
         wip: emit proof steps Simon Cruanes 2021-10-19 22:52:34 -04:00
  • 3589592296
         wip: use real proofs Simon Cruanes 2021-10-16 22:00:29 -04:00
  • 29d1fd5cf3
         fix bug in veci32 Simon Cruanes 2021-10-16 21:40:45 -04:00
  • 597a6c378e
         wip: split VecI32 and VecSmallInt Simon Cruanes 2021-10-16 20:31:56 -04:00
  • af1ef089af
         wip: proper proof production using Proof_ser-based traces Simon Cruanes 2021-10-15 23:00:09 -04:00
  • ca4a42f28a
         improve API of chunk_stack Simon Cruanes 2021-10-14 23:40:58 -04:00
  • 7df124f94c
         test: add a test using a file backend Simon Cruanes 2021-10-14 23:40:51 -04:00
  • 73cca4ca18
         move chunk_stack to util, fix some bugs Simon Cruanes 2021-10-14 23:18:21 -04:00
  • 3a56fb0763
         test file for chunk stack Simon Cruanes 2021-10-14 23:17:55 -04:00
  • beda972def
         wip: feat(base): proof chunk storage Simon Cruanes 2021-10-14 21:41:47 -04:00
  • feb7a354e9
         fix test Simon Cruanes 2021-10-13 00:30:43 -04:00
  • 12037c6ba2
         test only >= 4.08 on CI Simon Cruanes 2021-10-12 23:05:47 -04:00
  • b22e4b96ce
         bump min requirement to 4.08 Simon Cruanes 2021-10-12 23:05:06 -04:00
  • a6b303bb90
         remove dep on bare-encoding Simon Cruanes 2021-10-12 22:52:52 -04:00
  • e90df644c4
         chore: make CI ignore promotion rules Simon Cruanes 2021-10-12 22:46:41 -04:00
  • 3d17feab12
         use standalone mode and promote for the BARE encoding of proofs Simon Cruanes 2021-10-12 22:45:04 -04:00
  • fd1d068997
         proof stubs and sat proof Simon Cruanes 2021-10-12 22:13:28 -04:00
  • 6fae75f94d
         add Vec_unit to util Simon Cruanes 2021-10-12 22:13:05 -04:00
  • 4308eba04d
         fix Simon Cruanes 2021-10-11 23:19:24 -04:00
  • af901f54b1
         proof production for th-data Simon Cruanes 2021-10-11 19:57:25 -04:00
  • 1779b7115a
         wip: proof production (incl. better tracking of proofs in CC) Simon Cruanes 2021-10-11 14:27:14 -04:00
  • 0550f6fcfa
         wip: proof production Simon Cruanes 2021-10-09 00:51:15 -04:00
  • d3537f2c3f
         wip: refactor proof Simon Cruanes 2021-10-07 20:49:39 -04:00
  • bbb995b0d5
         refactor some names related to proofs; wip add unit paramod Simon Cruanes 2021-10-03 20:32:37 -04:00
  • 04f1ba063d
         wip: adapt CC to new proofs Simon Cruanes 2021-09-29 22:19:16 -04:00
  • df40b5a5c1
         wip: refactor(sat): generate detailed proofs again Simon Cruanes 2021-09-29 22:18:36 -04:00
  • 4621cc948f
         feat(core): change the way proofs work Simon Cruanes 2021-09-29 22:16:22 -04:00
  • 313e9db026
         feat(vec): add copy Simon Cruanes 2021-09-29 22:16:10 -04:00
  • 5e0652687a
         wip: proof production using BARE for storage Simon Cruanes 2021-09-28 21:06:01 -04:00
  • 4302c028d6 deploy: bbe366989c c-cube 2021-09-27 23:32:36 +00:00
  • bbe366989c
         perf(sat): use Atom.Vec for temporary atom array Simon Cruanes 2021-09-26 21:35:14 -04:00
  • a1381533d9 deploy: 74326b39c0 c-cube 2021-09-27 23:28:29 +00:00
  • c7511b2934
         fix compilation error wip-dyn-trans Simon Cruanes 2021-09-27 12:18:37 -04:00
  • c2b1bd038d
         perf(sat): use Atom.Vec for temporary atom array Simon Cruanes 2021-09-26 21:35:14 -04:00
  • 1f5806244e
         fix docstrings Simon Cruanes 2021-09-26 21:00:51 -04:00
  • 697678d6d2
         feat(dyn-trans): provide config record when instantiating theory Simon Cruanes 2021-09-24 22:44:52 -04:00
  • 5f51863cd3
         feat(dyn-trans): track activity of terms to guide instantiation Simon Cruanes 2021-09-20 06:30:39 -04:00
  • 3840fefb0e
         wip: feat(dyn-trans): provide config via env vars Simon Cruanes 2021-09-19 13:07:06 -04:00
  • 156eadd9df
         feat(sat): refactor a bit clause pools; add stats Simon Cruanes 2021-09-19 13:06:53 -04:00
  • 14d2a89196
         feat(cc): expose more functions for N.t->literals Simon Cruanes 2021-09-19 13:05:43 -04:00
  • 265442116f
         feat(core): provide mk_eqn in CC Simon Cruanes 2021-09-19 13:03:44 -04:00
  • 156af6e803
         update doc Simon Cruanes 2021-09-19 12:55:00 -04:00
  • 91a307d6fa
         detail Simon Cruanes 2021-09-13 06:46:54 -04:00
  • d7f09d5b09
         basic proof emission for dyn-trans Simon Cruanes 2021-09-13 06:44:59 -04:00
  • 405d48ac2d
         feat(dyn-trans): first implementation, quite aggressive Simon Cruanes 2021-09-13 06:35:03 -04:00
  • a12e17ffda
         more hooks in CC (to add clauses) Simon Cruanes 2021-09-13 06:34:45 -04:00
  • 18f86e8eb7
         setup dyn-trans in main solver Simon Cruanes 2021-09-09 08:57:14 -04:00
  • 729f171985
         wip: theory for dyn-trans axioms Simon Cruanes 2021-09-09 08:56:47 -04:00
  • 79386c2cbd
         feat(smt): provide SAT solver to theories upon initialization Simon Cruanes 2021-09-02 22:24:59 -04:00
  • c151f2981f
         feat: clause pools in SMT Simon Cruanes 2021-09-02 09:32:01 -04:00
  • 74326b39c0
         feat(vec): factor a bit of code for auxiliary functions in vectors Simon Cruanes 2021-09-26 21:01:04 -04:00
  • acc682c5af
         refactor(cc): simple renaming Simon Cruanes 2021-09-09 08:57:03 -04:00
  • 86512dbed0
         utils Simon Cruanes 2021-09-13 06:34:21 -04:00
  • c9e257d40b
         cleanup Simon Cruanes 2021-09-01 09:00:39 -04:00
  • 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