Commit graph

  • 227df58afd
    merge Simon Cruanes 2021-12-07 10:17:46 -05:00
  • a614fdb2e1
    update benchpress file Simon Cruanes 2021-12-07 10:16:09 -05:00
  • 0b1acbb02b
    fix typo Adnan Ahmed 2021-12-06 23:25:31 +05:00
  • 2abccce985
    build flags Simon Cruanes 2021-11-29 10:33:56 -05:00
  • 7eff8fe2cb deploy: bf1f9e7ce1 c-cube 2021-11-29 00:14:38 +00:00
  • bf1f9e7ce1
    try to fix CI Simon Cruanes 2021-11-28 18:33:56 -05:00
  • b27fdc5507
    Merge pull request #16 from c-cube/wip-proof-smt Simon Cruanes 2021-11-28 18:21:48 -05:00
  • 2caafdb530
    fix test Simon Cruanes 2021-11-28 18:12:25 -05:00
  • f909e6bc9e
    fix proof production wrt conflict minimization Simon Cruanes 2021-11-28 18:10:15 -05:00
  • 1bf05d51ce
    fix(proof): emit proper result for RUP steps Simon Cruanes 2021-11-28 16:35:04 -05:00
  • 15e16a515d
    refactor(sat): improve code Simon Cruanes 2021-11-28 16:34:43 -05:00
  • e9b395b643
    feat(proof): do not emit trivial clause_rw steps Simon Cruanes 2021-11-28 16:33:57 -05:00
  • aad1daa4e4
    feat(quip): remove lit and not-normalization from quip Simon Cruanes 2021-11-28 13:36:19 -05:00
  • 0233801b95
    more debug messages Simon Cruanes 2021-11-28 11:28:55 -05:00
  • 2e4fd5e1c1
    update conflict resolution for better proofs, improve code Simon Cruanes 2021-11-27 15:30:45 -05:00
  • c5c5426ead
    quip: include all term definitions in proof Simon Cruanes 2021-11-19 23:25:21 -05:00
  • 38d90b250a
    refactor sat solver Simon Cruanes 2021-11-19 23:25:09 -05:00
  • 41fe798b23
    fix test Simon Cruanes 2021-11-19 22:50:22 -05:00
  • 7b15ea7280
    refactor(sat): fix proof construction at level 0; improve preprocessing Simon Cruanes 2021-11-19 22:35:48 -05:00
  • 4d3b278754
    feat(vec): add append, fix prepend Simon Cruanes 2021-11-19 22:35:40 -05:00
  • 1f9c43afa8
    fix(sat): generate proof in partition for eliminated level-0 lits Simon Cruanes 2021-11-14 23:08:02 -05:00
  • 69ee322c45
    remove dead code Simon Cruanes 2021-11-14 22:53:34 -05:00
  • 5d18086e53
    fix(sat): resolution at level 0 is not recursive Simon Cruanes 2021-11-14 22:50:12 -05:00
  • 7d70994758
    fix(proof): add neg-normalization Simon Cruanes 2021-11-14 22:50:05 -05:00
  • faf2af1bac
    update Simon Cruanes 2021-11-14 22:37:35 -05:00
  • ffa450ba08
    proof: normalize clauses in rw Simon Cruanes 2021-11-10 18:30:12 -05:00
  • a8a851a7de
    feat: ability to produce .gz proof files Simon Cruanes 2021-11-10 18:23:26 -05:00
  • 8c780e3ed5
    quip: add clause in expr_def Simon Cruanes 2021-11-10 18:04:52 -05:00
  • 0d00629923
    more compressed output of equations Simon Cruanes 2021-11-10 13:23:29 -05:00
  • f500704905
    fix(sat): level-0 resolution needs to be recursive Simon Cruanes 2021-11-10 13:20:00 -05:00
  • 72d79d7c0a
    fix emission of reference terms Simon Cruanes 2021-10-29 22:35:19 -04:00
  • 6b1b1eb587
    feat(proof): process more steps in proof reconstruction Simon Cruanes 2021-10-28 20:48:39 -04:00
  • 7d5b76a87a
    fix tests and warning Simon Cruanes 2021-10-27 21:54:30 -04:00
  • 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