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