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

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