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

  • 23dcf79560 more regression tests Simon Cruanes 2020-12-22 15:02:12 -05:00
  • 7ef673ca30 refactor mini-cc Simon Cruanes 2020-12-22 14:59:30 -05:00
  • 35e5e30e93 fix(smtlib): handle "xor" Simon Cruanes 2020-12-22 14:59:21 -05:00
  • 3d46986161 test: add regression test for xor Simon Cruanes 2020-12-22 14:59:06 -05:00
  • 7cb97a89c5 make type abstract Simon Cruanes 2020-12-22 12:36:02 -05:00
  • 1890f7af13 try to tighten type constraints Simon Cruanes 2020-12-22 12:30:01 -05:00
  • f05de5f741 fix warnings Simon Cruanes 2020-12-22 12:17:32 -05:00
  • 6c1b7df301 chore: try to fix build again Simon Cruanes 2020-12-22 11:53:12 -05:00
  • 14bb5898f0 Merge branch 'wip-fix-lra' into wip-lra-simplex-unsat-core Simon Cruanes 2020-12-22 11:46:09 -05:00
  • 354e432a40 chore: add cache to CI Simon Cruanes 2020-12-22 11:07:54 -05:00
  • 5ca4730968 try to fix build Simon Cruanes 2020-12-22 11:06:59 -05:00
  • 3b3a2e1caf use simplex conflicts in LRA Simon Cruanes 2020-12-22 10:55:55 -05:00
  • 4be726db43 Add unsat core explanations to the simplex Guillaume Bury 2020-12-22 14:16:23 +01:00
  • 9d579af235 wip: make lazyness of model explicit wip-fix-lra Simon Cruanes 2020-12-21 16:15:49 -05:00
  • b3a7acf95b feat(LRA): handle congruence closure and theory combination in LRA Simon Cruanes 2020-11-17 18:24:09 -05:00
  • 6417bbdd80 feat(util): add Backtrack_stack.iter Simon Cruanes 2020-11-17 18:23:58 -05:00
  • 9839e5a36b feat(core): add push_decision, for model-based th combination Simon Cruanes 2020-11-17 18:23:16 -05:00
  • 60fe3506d5 feat(core): add CC.explain_eq to explain why two nodes were merged Simon Cruanes 2020-11-17 18:22:51 -05:00
  • 6a0731eeb1 refactor: improve model production in FM Simon Cruanes 2020-11-17 17:03:12 -05:00
  • db1c50f7ed feat(LRA): expose model after fourier-motzkin returns "SAT" Simon Cruanes 2020-11-17 16:52:49 -05:00
  • 1b7d084a9c chore: allow smtlib-utils 0.2 Simon Cruanes 2020-11-17 14:39:39 -05:00
  • 764695bb65 feat: pass a sign along with the formula in acts_add_decision_lit Simon Cruanes 2020-11-14 18:58:40 -05:00
  • 883b27ccc9 add uflra to makefile targets Simon Cruanes 2020-11-14 16:59:19 -05:00
  • 77b33346f5 fix(tycheck): handle proper unary minus Simon Cruanes 2020-11-14 13:17:23 -05:00
  • 103c320577 fix(lra): fixed case splitting on a != b Simon Cruanes 2020-11-14 00:23:45 -05:00
  • 37089adb17 feat: add -t option to main Simon Cruanes 2020-11-14 00:23:35 -05:00
  • b2ab465cff fix(LRA): track explanations properly when rewriting with an equality Simon Cruanes 2020-11-13 23:58:14 -05:00
  • a6f6a99fb3 fix: small perf improvement Simon Cruanes 2020-11-13 23:28:39 -05:00
  • 39ed753b38 add tests for simplex Simon Cruanes 2020-11-13 23:28:32 -05:00
  • 5ff0fff85b wip: refactor(lra): import Simplex from funarith, replace FM with it Simon Cruanes 2020-11-13 22:35:59 -05:00
  • 4097ed9dc2 refactor: account for @gbury's review Simon Cruanes 2019-12-28 07:47:53 -06:00
  • 919c1e6011 fix: only push atoms that don't have a value into next_decisions Simon Cruanes 2019-10-29 14:35:26 -05:00
  • 2286a72437 fix: in final-check, resume if there are new decisions to do Simon Cruanes 2019-10-29 14:34:13 -05:00
  • 79b1585804 feat: allow the theory to ask for some literals to be decided on Simon Cruanes 2019-10-29 14:21:25 -05:00
  • d9bf16dfde feat: allow to set the default polarity of variables at creation time Simon Cruanes 2019-12-28 08:07:22 -06:00
  • df25e84a01 fix(LRA): fix bug in FM resolution; add more comments Simon Cruanes 2020-11-12 19:23:45 -05:00
  • 0fc5b279d1 fix(LRA): invalid normalization Simon Cruanes 2020-11-12 18:46:43 -05:00
  • 3e703cf89e refactor: better debug in LRA Simon Cruanes 2020-11-12 18:46:34 -05:00
  • 9a3e387405 refactor: explicit recursion in preprocessing Simon Cruanes 2020-11-12 18:21:37 -05:00
  • 410a4005c3 chore: avoid tests dir Simon Cruanes 2020-11-12 18:00:42 -05:00
  • f510bfaf25 add regression tests for LRA Simon Cruanes 2020-10-20 15:43:02 -04:00
  • 51be2f52e8 style Simon Cruanes 2020-10-12 02:06:16 -04:00
  • 534fc45783 wip: better progress bar Simon Cruanes 2020-10-11 23:30:22 -04:00
  • f556fe58ab test: clarify where tests belong Simon Cruanes 2020-10-10 18:54:57 -04:00
  • 3449404964 refactor: move base-term to sidekick-arith Simon Cruanes 2020-10-10 17:43:42 -04:00
  • 349d884664 chore: add sidekick-arith library, depends on zarith Simon Cruanes 2020-10-10 17:17:26 -04:00
  • 7a74ec45b7 fix Simon Cruanes 2020-10-10 16:39:25 -04:00
  • e9931b377c remove bloody warn-error Simon Cruanes 2020-10-10 16:00:21 -04:00
  • 242f554974 chore: remove deps on funarith wip-lra Simon Cruanes 2020-10-10 14:34:13 -04:00
  • dc320bf0c9 fix(tycheck): handle n-ary +/- Simon Cruanes 2020-10-10 14:34:05 -04:00
  • 7c3c88d6f6 feat(lra): bugfixes Simon Cruanes 2020-10-10 14:33:54 -04:00
  • 93b56618f1 wip: first implem of Fourier Motzkin Simon Cruanes 2020-10-10 01:22:22 -04:00
  • 9783c3ae1b wip: reimplement a fourier motzkin module, from scratch Simon Cruanes 2020-10-10 00:00:20 -04:00
  • c67e44e654 detail Simon Cruanes 2020-10-09 23:59:38 -04:00
  • 581c7eff0b wip Simon Cruanes 2020-10-09 22:09:15 -04:00
  • 7e6800811f wip: LRA: process all lits during final check Simon Cruanes 2020-10-04 22:28:09 -04:00
  • fabdb27dfe wip: feat(lra): preprocess by renaming lits/terms and storing defs Simon Cruanes 2020-10-04 21:37:03 -04:00
  • ac6ca7d584 wip: properly typecheck and build LRA terms Simon Cruanes 2020-10-04 00:32:52 -04:00
  • 943efad206 feat: add AST for LRA Simon Cruanes 2020-10-03 23:46:45 -04:00
  • 216cbe762f missing lra file Simon Cruanes 2020-09-08 22:29:36 -04:00
  • f59a5d9fce wip Simon Cruanes 2020-09-08 22:20:03 -04:00
  • aff2e29a6b wip: representing real types and values Simon Cruanes 2020-08-16 16:30:23 -04:00
  • 4f12bfdb93 wip: LRA Simon Cruanes 2020-08-16 11:53:02 -04:00
  • 40d47a8d6c wip: lra Simon Cruanes 2020-02-26 09:04:38 -06:00
  • 95edfd9aa9 wip: LRA theory Simon Cruanes 2020-02-22 14:02:31 -06:00
  • 5c1fb51277 chore: small opam changes Simon Cruanes 2020-02-22 14:02:12 -06:00
  • c5bce67fcf remove pin depends Simon Cruanes 2020-09-23 21:57:31 -04:00
  • 4bce0f32d4 prepare for 0.8.3 Simon Cruanes 2020-09-09 15:39:52 -04:00
  • 9ef84f1df3 fix test on 2.8.1 Simon Cruanes 2020-09-09 15:38:07 -04:00
  • 6df11c2962 fix compat bug Simon Cruanes 2020-09-08 23:40:47 -04:00
  • c7fae418ab chore: pin-depends for msat Simon Cruanes 2020-09-08 23:21:35 -04:00
  • 8eb32fa9ab fix: support containers 2.8.1 and above Simon Cruanes 2020-09-08 22:42:38 -04:00
  • cc18830eae chore: fix opam file Simon Cruanes 2020-09-08 22:34:02 -04:00
  • ae6d298790 move to containers 3.0 Simon Cruanes 2020-09-08 22:29:25 -04:00
  • 7d399ba201 handle :named attribute in smtlib Simon Cruanes 2020-08-18 10:01:36 -04:00
  • c5180f3f63 remove dead symlink Simon Cruanes 2020-08-18 10:01:15 -04:00
  • 6a04c7f4dd chore: travis versions Simon Cruanes 2020-08-04 11:15:04 -04:00
  • eb3685e48f update readme Simon Cruanes 2020-08-04 11:06:13 -04:00
  • 8a60f2d913 add opam bounds Simon Cruanes 2020-08-04 11:04:24 -04:00
  • 2431c4caa0 chore: tighten bound on msat Simon Cruanes 2020-07-28 16:01:22 -04:00
  • b724882516 test: detail in benchpress config Simon Cruanes 2020-07-28 15:55:54 -04:00
  • 527b5657b3
         chore: remove artifact from github action Simon Cruanes 2020-05-28 17:34:49 -04:00
  • 707085b2c1 add basic config for benchpress Simon Cruanes 2020-05-15 18:20:31 -04:00
  • 7032d5220a fix typo in a name Simon Cruanes 2020-04-27 12:47:11 -04:00
  • 8ef4913c92 chore: disable opam testing for msat-bin Simon Cruanes 2020-02-28 09:29:48 -06:00
  • b4ef8e4e67 chore: use a different travis script Simon Cruanes 2020-02-24 17:46:35 -06:00
  • 65bd7e7744 prepare for 0.8.2 Simon Cruanes 2020-02-24 17:38:56 -06:00
  • 0b283a384d test: add some regression tests Simon Cruanes 2020-02-21 16:46:57 -06:00
  • da3cb275be chore: version bump on containers Simon Cruanes 2020-02-21 13:53:41 -06:00
  • 7cfdb3507c fix(th-data): fix acyclicity Simon Cruanes 2020-02-20 19:32:33 -06:00
  • 4e1b35d2c3 test: add regression test Simon Cruanes 2020-02-17 12:30:58 -06:00
  • bb449257d8 fix(solver): in final-check, fixpoint until CC has no merges Simon Cruanes 2020-02-15 14:40:57 -06:00
  • 93b993825b chore(make): also remove trailing spaces in make reindent Simon Cruanes 2020-02-15 14:36:39 -06:00
  • 11d8f8e879 remove dead code, some printing info Simon Cruanes 2020-02-15 14:33:44 -06:00
  • 6aae70f15a test: add more regression tests for datatypes Simon Cruanes 2020-01-17 19:12:50 -06:00
  • b2c047190f fix(data): check is-a lits in final-check Simon Cruanes 2020-01-17 19:12:06 -06:00
  • eb64acb31f fix(data): reimplement acyclicity check Simon Cruanes 2020-01-17 19:10:46 -06:00
  • e21dea4780 feat(cc): flag some explanations as being theory-induced Simon Cruanes 2020-01-17 18:48:17 -06:00
  • 5bcecfd68c Merge branch 'wip-data' Simon Cruanes 2020-01-14 23:02:49 -06:00
  • c4a4edde3a chore: fix opam file Simon Cruanes 2020-01-14 23:00:07 -06:00