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

Commit graph

  • 8410a57f1a
         wip: feat(LIA): LIA solver, will rely on LRA solver Simon Cruanes 2022-01-10 16:51:45 -05:00
  • fb0668e7ba
         wip: feat(lra): expose state via a registry key Simon Cruanes 2022-01-10 16:51:30 -05:00
  • f7195bf980
         feat(smt): ability for a theory to declare we're in incomplete fragment Simon Cruanes 2022-01-10 16:50:55 -05:00
  • af8ab338e6
         feat(smt): add a registry to share values between theories Simon Cruanes 2022-01-10 16:50:38 -05:00
  • 849d4319f2
         fix theory combination for LRA Simon Cruanes 2022-01-05 11:59:50 -05:00
  • eb97161992
         better debug Simon Cruanes 2022-01-05 11:21:58 -05:00
  • 2378fc37ac
         fix LIA->LRA cast operation Simon Cruanes 2022-01-04 18:36:00 -05:00
  • 671fa6515a
         fix missing conversions Simon Cruanes 2022-01-04 18:25:28 -05:00
  • 3477f39b73
         fix handling of numeral constants Simon Cruanes 2022-01-04 18:18:33 -05:00
  • 691ff12a01
         wip: support LIA in input AST and base terms Simon Cruanes 2022-01-04 18:16:16 -05:00
  • 02a9abde3e
         feat: add Q.is_int Simon Cruanes 2022-01-04 11:11:30 -05:00
  • 2bce3e6dd9
         refactor(LRA): custom iterators in simplex, makes code more readable Simon Cruanes 2022-01-04 11:09:25 -05:00
  • 2d9f17b5b1
         fix(sat): use a set of delayed actions Simon Cruanes 2022-01-11 13:17:18 -05:00
  • 8b263d4d46
         fix(sat): when theory-propagating a literal below current level, backtrack Simon Cruanes 2022-01-11 12:35:03 -05:00
  • 1ffe778951
         feat(solver): eager checking of proofs for theory propagation Simon Cruanes 2022-01-11 12:21:17 -05:00
  • a33029129e
         fix(CC): bug introduced by sharing mutable lazy state Simon Cruanes 2022-01-10 12:11:32 -05:00
  • 78df8252dc
         bugfix in CC explanations Simon Cruanes 2022-01-05 10:31:33 -05:00
  • df033eaa7e deploy: 0afdb06f6c c-cube 2022-01-04 14:50:36 +00:00
  • 0afdb06f6c
         Merge branch 'wip-datatype-proofs' Simon Cruanes 2022-01-04 09:46:10 -05:00
  • b6df2cd974
         clause-less steps in proofs wip-datatype-proofs Simon Cruanes 2022-01-03 22:59:31 -05:00
  • 2e26fc79df deploy: 88f57d213a c-cube 2022-01-03 22:15:13 +00:00
  • 88f57d213a
         rename stat Simon Cruanes 2021-12-20 16:40:22 -05:00
  • dbba6719bc
         fix compilation after rebase Simon Cruanes 2021-12-20 13:57:41 -05:00
  • 9d3da47f3b
         fix: missing implied bound update Simon Cruanes 2021-03-21 18:51:44 -04:00
  • 73c9878554
         wip: feat(lra): clarify construction of bounds; fix sign error Simon Cruanes 2021-03-21 01:22:51 -04:00
  • 721c01d12c
         feat(lra): make Erat.{plus,minus}_inf saturating Simon Cruanes 2021-03-21 01:22:30 -04:00
  • 34b1aa1799
         wip: feat(lra): propagate literals based on implied bounds for basic vars Simon Cruanes 2021-03-21 01:14:33 -04:00
  • ab4e115b32
         tmp: restore some preprocessing wip-lra-simplex-propagations-implied-tmp-2022-01-03 Simon Cruanes 2022-01-03 16:15:42 -05:00
  • 63f50d03fa
         feat: proper proof production for theory merges in CC Simon Cruanes 2021-12-29 15:56:54 -05:00
  • 80cb096e8a
         feat: change signature of explanations for CC theory merges Simon Cruanes 2021-12-28 23:07:10 -05:00
  • 45845072af deploy: be1c1573b1 c-cube 2021-12-28 21:48:24 +00:00
  • be1c1573b1
         feat(proof): emit is-a terms properly Simon Cruanes 2021-12-28 16:46:59 -05:00
  • 8958301a8e
         fix: update quip CLI arguments Simon Cruanes 2021-12-28 10:57:30 -05:00
  • b2e8f8b29d
         chore: disable CI on windows temporarily Simon Cruanes 2021-12-21 11:31:53 -05:00
  • 6970c83ff1
         rename stat Simon Cruanes 2021-12-20 16:40:22 -05:00
  • 6d46d2225b deploy: 584b56075f c-cube 2021-12-20 20:47:54 +00:00
  • 584b56075f
         feat: add push/pop for assumptions; add check_sat_propagation_only Simon Cruanes 2021-12-20 15:34:34 -05:00
  • 1e48bd54c6
         fix compilation after rebase Simon Cruanes 2021-12-20 13:57:41 -05:00
  • 6900fb2f72
         fix: missing implied bound update Simon Cruanes 2021-03-21 18:51:44 -04:00
  • 135ca2319a
         wip: feat(lra): clarify construction of bounds; fix sign error Simon Cruanes 2021-03-21 01:22:51 -04:00
  • fc46cb53e0
         feat(lra): make Erat.{plus,minus}_inf saturating Simon Cruanes 2021-03-21 01:22:30 -04:00
  • 4a26e3cd3e
         wip: feat(lra): propagate literals based on implied bounds for basic vars Simon Cruanes 2021-03-21 01:14:33 -04:00
  • 054fd84a0c deploy: 5d2f8a1d3d c-cube 2021-12-20 18:53:21 +00:00
  • 5d2f8a1d3d
         feat(api): add callbacks to measure progress or ask solver to stop Simon Cruanes 2021-12-20 13:51:59 -05:00
  • c03fc97f00
         better debug in CC Simon Cruanes 2021-12-17 16:40:03 -05:00
  • be2d57a717
         feat(cc): add an invariant check before returning a model Simon Cruanes 2021-12-17 15:29:28 -05:00
  • b19d80e443
         debug Simon Cruanes 2021-12-17 15:13:48 -05:00
  • 44c63d4c13
         debug Simon Cruanes 2021-12-17 16:40:52 -05:00
  • f9f471ce12
         details Simon Cruanes 2021-12-17 13:46:48 -05:00
  • 46b13d08d0
         add regression test Simon Cruanes 2021-12-17 13:21:30 -05:00
  • 2d24a21908
         fix: do not preprocess but add equations eagerly for single-cstor terms Simon Cruanes 2021-12-17 11:58:39 -05:00
  • 6d72203437
         fix: avoid preprocessing loops Simon Cruanes 2021-12-17 11:48:41 -05:00
  • eca5139a03 deploy: 0841bddbaf c-cube 2021-12-17 16:41:10 +00:00
  • 0841bddbaf
         feat(data): preprocessing step for single-cstor types Simon Cruanes 2021-12-17 11:39:25 -05:00
  • 63eeb81290
         refactor: modify interface of Th_data Simon Cruanes 2021-12-17 11:38:52 -05:00
  • 3b409c8944
         feat(proof): add proof_r1 as a pendant to proof_p1 for non-equations Simon Cruanes 2021-12-17 11:38:07 -05:00
  • 3ab1ddfea8
         fix: ensure all functions in SMT solver preprocess their literals Simon Cruanes 2021-12-16 13:49:43 -05:00
  • 2b48901535 deploy: 4ac2eb25a6 c-cube 2021-12-08 02:30:55 +00:00
  • 4ac2eb25a6
         use TEF in sudoku; improve a bit its ergonomics Simon Cruanes 2021-12-07 21:29:51 -05:00
  • e64013c660
         chore: upgrade bare autogen-code Simon Cruanes 2021-12-07 21:16:25 -05:00
  • 110f3f8527
         update benchpress file to actually run proofs Simon Cruanes 2021-12-07 21:16:12 -05:00
  • 2d8fc78bc4
         add expect test for the sudoku solver Simon Cruanes 2021-12-07 14:19:25 -05:00
  • 49009aa346 deploy: 72d121fa64 c-cube 2021-12-07 19:11:45 +00:00
  • 72d121fa64
         add example: the suduko solver, adapted from msat Simon Cruanes 2021-12-07 14:10:36 -05:00
  • cfede762c9
         feat(sat): provide a proof_dumm module Simon Cruanes 2021-12-07 14:08:16 -05:00
  • 9517e88467
         feat(util): add backtrackable ref Simon Cruanes 2021-12-07 14:07:41 -05:00
  • 8030393136 deploy: a614fdb2e1 c-cube 2021-12-07 15:22:59 +00:00
  • 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