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

  • b97582daa2
         wip: refactor(smt): remove layers of functors, split into modules Simon Cruanes 2022-07-30 00:19:29 -04:00
  • 7595f66e59
         refactor(core): add Proof_step Simon Cruanes 2022-07-29 23:27:04 -04:00
  • a9ae790d7f
         refactor(cc): split into modules, fully defunctorize Simon Cruanes 2022-07-29 23:25:48 -04:00
  • e30590955e
         refactor(sat): remove unused values, split code off main functor Simon Cruanes 2022-07-29 22:37:31 -04:00
  • d4ba4602a4
         refactor(sat): simplify interface a lot Simon Cruanes 2022-07-29 22:28:21 -04:00
  • c09650db51
         refactor(cc): continue de-functorizing Simon Cruanes 2022-07-29 00:15:05 -04:00
  • 464bc66474
         wip: refactor(cc): remove layers of functorization Simon Cruanes 2022-07-29 00:02:27 -04:00
  • 1905d2d628
         feat(core): improve Lit Simon Cruanes 2022-07-29 00:02:06 -04:00
  • 9df981d650
         feat(core): concrete lit, proof traces, proof terms Simon Cruanes 2022-07-28 23:30:56 -04:00
  • 65c6872853
         details: synopsis in dune files Simon Cruanes 2022-07-28 23:30:42 -04:00
  • c1af4374bd
         core-logic: make Types_ private Simon Cruanes 2022-07-28 23:12:18 -04:00
  • 68c03a39b3
         feat(core-logic): add a few builtins (=, bool, ite, not, true, false) Simon Cruanes 2022-07-28 20:25:17 -04:00
  • a4db8b6e94
         small improvement Simon Cruanes 2022-07-28 15:27:14 -04:00
  • c6407bfec1
         refactor a bit Simon Cruanes 2022-07-28 14:54:23 -04:00
  • e70daf4531
         remove dead code Simon Cruanes 2022-07-28 14:52:11 -04:00
  • e235a65567
         test: add more to unittest/core-logic Simon Cruanes 2022-07-28 14:51:43 -04:00
  • bfa434562e
         fix(core-logic/term): make ty unfailing; fix DB bugs Simon Cruanes 2022-07-28 14:51:24 -04:00
  • dbd20c999b
         refactor test Simon Cruanes 2022-07-28 13:55:09 -04:00
  • 6f376cfaf2
         refactor: rename core-ast to core-logic; split into modules Simon Cruanes 2022-07-28 13:54:38 -04:00
  • 435845d1d4
         update tests Simon Cruanes 2022-07-27 22:45:10 -04:00
  • 88eb2575c3
         feat(sigs): add some basic sigs Simon Cruanes 2022-07-27 22:40:46 -04:00
  • 2db3343bcd
         improve unittest for core-ast Simon Cruanes 2022-07-27 22:40:36 -04:00
  • 8950601fb2
         fix(core-ast): fix some issues in type computations; print arrows Simon Cruanes 2022-07-27 22:40:16 -04:00
  • e52a7ac0ea
         test: add basic unit-test for core-ast Simon Cruanes 2022-07-27 21:41:59 -04:00
  • 410c5b1ee2
         feat: start core-ast library Simon Cruanes 2022-07-27 21:41:00 -04:00
  • 0e5bde0f40
         detail Simon Cruanes 2022-07-23 00:24:56 -04:00
  • 4a6237191e
         wip: try to restore old model construction Simon Cruanes 2022-07-22 22:16:04 -04:00
  • 2922cca78f
         fix: proper negation when raising an acyclicity conflict Simon Cruanes 2022-07-22 21:54:22 -04:00
  • c8800fe3e2
         promote test results Simon Cruanes 2022-07-22 21:45:56 -04:00
  • 851dda696a
         feat(cc): have 2 phases of pre-merge events Simon Cruanes 2022-07-22 21:31:42 -04:00
  • 6da6284711
         refactor(cc): use explicit actions in CC, not effectful functions Simon Cruanes 2022-07-22 21:26:21 -04:00
  • e37f66c394
         feat(cc): remove same-val explanations and model mode Simon Cruanes 2022-07-21 23:29:07 -04:00
  • dc68a60151
         feat(cc): remove callbacks, return list of actions Simon Cruanes 2022-07-21 23:21:07 -04:00
  • 6694ce856b
         fix sat for new event Simon Cruanes 2022-07-21 23:21:01 -04:00
  • 7a6d94e622
         event: add a return type Simon Cruanes 2022-07-21 23:20:44 -04:00
  • b10aaf05f2
         wip: expose bug caused by order of event handlers wip-simplify-functors-2022-07-15 Simon Cruanes 2022-07-20 21:40:04 -04:00
  • e1a4ce587f
         fix sudoku solver Simon Cruanes 2022-07-20 20:13:16 -04:00
  • 729c72a27d
         sidekick.sh: make dune phase silent Simon Cruanes 2022-07-18 23:28:45 -04:00
  • 6dca63b0ea
         renamings Simon Cruanes 2022-07-18 23:27:12 -04:00
  • b0cb60ab67
         gitignore Simon Cruanes 2022-07-18 23:27:07 -04:00
  • f3f0628261
         large refactor with signature splitting, events, etc. Simon Cruanes 2022-07-18 23:20:07 -04:00
  • b2d0ea2d33
         add sidekick.sh launcher script Simon Cruanes 2022-07-18 23:17:29 -04:00
  • ea752b5cf5
         feat: add some BACKTRACKABLE sigs Simon Cruanes 2022-07-17 20:21:22 -04:00
  • 833fa8e038
         add Event abstraction in Util Simon Cruanes 2022-07-17 20:20:46 -04:00
  • 7d8b1f70bd deploy: 679b35012b c-cube 2022-07-16 03:53:41 +00:00
  • 633a658e0c
         wip: use new sigs Simon Cruanes 2022-07-15 23:51:53 -04:00
  • ab6bcf8cbe
         add many small sigs libraries Simon Cruanes 2022-07-15 23:51:41 -04:00
  • 679b35012b
         SAT: remove clause pools last-stable-with-functor Simon Cruanes 2022-07-15 21:12:04 -04:00
  • 00dec7ced8
         remove iarray Simon Cruanes 2022-07-15 21:06:46 -04:00
  • 801d0b3e45
         warnings Simon Cruanes 2022-07-15 20:32:58 -04:00
  • 5a559bec92
         remove veci32 Simon Cruanes 2022-07-15 20:32:06 -04:00
  • ba4b4c0302
         rename build Simon Cruanes 2022-07-14 22:29:48 -04:00
  • 44ca7daf75
         remove file Simon Cruanes 2022-07-14 22:29:12 -04:00
  • 325acc5724
         fix tests Simon Cruanes 2022-07-14 22:17:25 -04:00
  • 5f0ff14215 deploy: 85c850d464 c-cube 2022-07-15 02:12:10 +00:00
  • 85c850d464
         update tests after removal of lia Simon Cruanes 2022-07-14 22:10:14 -04:00
  • a1bc186d2e
         use ocamlformat Simon Cruanes 2022-07-14 22:07:29 -04:00
  • e2b9b2874c
         fix more warnings; remove never completed LIA stuff Simon Cruanes 2022-07-14 22:01:23 -04:00
  • fd500a3d7d
         fix some warnings Simon Cruanes 2022-07-14 21:56:37 -04:00
  • 116f19215a deploy: b16fce6f26 c-cube 2022-07-15 01:53:58 +00:00
  • 96bc3e2340
         update tests Simon Cruanes 2022-07-14 21:48:19 -04:00
  • b16fce6f26
         Merge branch 'master' into wip-model-th-comb wip-model-th-comb Simon Cruanes 2022-07-14 21:46:36 -04:00
  • 1946a5e7cf
         feat: construct model from congruence closure after th-combination Simon Cruanes 2022-02-17 22:05:31 -05:00
  • a388c96fe3
         cc: remove new_merges Simon Cruanes 2022-02-17 22:03:33 -05:00
  • cdc5d160a7
         cc: use backtrackable table Simon Cruanes 2022-02-17 22:03:18 -05:00
  • d153c80ca5
         details Simon Cruanes 2022-02-17 21:21:51 -05:00
  • 8530c07c59
         lra: better debug Simon Cruanes 2022-02-17 21:21:40 -05:00
  • 8fb0152754
         feat(smt): simplify the final check loop significantly Simon Cruanes 2022-02-17 21:20:43 -05:00
  • da18ba3620
         perf(cc): only assign model values to term present in CC Simon Cruanes 2022-02-17 21:20:17 -05:00
  • 6e941683a2
         add with_model_mode to congruence closure Simon Cruanes 2022-02-17 18:08:55 -05:00
  • 95f84b4854
         refactor(th-comb): provide full model to the CC Simon Cruanes 2022-02-17 16:36:07 -05:00
  • fd66039c8d
         wip: theory combination by exposing model (classes) directly to CC Simon Cruanes 2022-02-17 13:49:47 -05:00
  • 65d4a90df1
         tef: stop compression, too fragile. just emit a .json file wip-preprocess-2022-02-04 Simon Cruanes 2022-02-17 21:19:53 -05:00
  • f26d178380
         feat(main): catch ctrl-c to cleanup Simon Cruanes 2022-02-17 21:19:19 -05:00
  • 52cae96ee2
         improve progress bar and printingof stat after timeout Simon Cruanes 2022-02-17 18:27:20 -05:00
  • 20791a551f
         feat: enforce time/memory limits in main runner Simon Cruanes 2022-02-17 13:09:48 -05:00
  • e177534a46
         chore: ugprade bare encoding Simon Cruanes 2022-02-16 14:20:27 -05:00
  • c0288902c0
         feat: check on_progress in more places Simon Cruanes 2022-02-16 13:24:43 -05:00
  • 5b0a2ad4a4
         debug Simon Cruanes 2022-02-15 16:57:25 -05:00
  • f3947f2237
         update model construction function Simon Cruanes 2022-02-15 12:23:04 -05:00
  • 7f45cc6967
         fix test Simon Cruanes 2022-02-14 11:36:50 -05:00
  • fb552ba8b2
         update expected test Simon Cruanes 2022-02-14 11:20:59 -05:00
  • 98c30bf0cc
         updates and cleanup Simon Cruanes 2022-02-14 10:46:08 -05:00
  • 73289d1ded
         test: regressions test for LRA Simon Cruanes 2022-02-08 13:45:26 -05:00
  • e481c74398
         refactor(LRA): new preprocessing, new shape of terms Simon Cruanes 2022-02-08 13:14:24 -05:00
  • c22fc62f3e
         base: remove simplex cases in arith terms Simon Cruanes 2022-02-08 13:14:07 -05:00
  • f268e86100
         refactor(smt-solver): preprocess literals in push_decision Simon Cruanes 2022-02-08 13:13:23 -05:00
  • a81a21c341
         core: add n_levels to monoid Simon Cruanes 2022-02-08 13:13:00 -05:00
  • 1d702029ee
         fix(typecheck): use logic to decide default type of numerals Simon Cruanes 2022-02-08 13:12:29 -05:00
  • 82acf271d3
         improve zarith and backtrackable table Simon Cruanes 2022-02-08 13:12:07 -05:00
  • fbf7c5e090
         chore: makefile Simon Cruanes 2022-02-08 13:11:36 -05:00
  • d9a701140c
         debug Simon Cruanes 2022-02-07 10:57:39 -05:00
  • d11b9d585c
         fix(smt): improve theory combination a bit Simon Cruanes 2022-02-04 16:40:55 -05:00
  • ab74b1a792
         fix(lra): preprocessing of linexps with non-zero constants Simon Cruanes 2022-02-04 16:16:00 -05:00
  • cbc9c5ac6f
         refactor(smt): preprocessing is now using a queue of delayed actions Simon Cruanes 2022-02-04 16:08:01 -05:00
  • f9036fa33b
         feat(bool): do not eliminate ite terms. Simon Cruanes 2022-02-04 09:24:27 -05:00
  • 2885563929
         fix(lra): better handling of model production for preprocessed-away terms wip-lia Simon Cruanes 2022-02-03 14:24:07 -05:00
  • 9cf9b025ab
         debug Simon Cruanes 2022-02-03 14:09:56 -05:00
  • a98132ed0c
         feat(model): add theory hooks to "complete" models Simon Cruanes 2022-02-03 14:00:43 -05:00
  • c4bbaddc06
         new regression test for (get-model); fix mdx test Simon Cruanes 2022-02-02 16:12:55 -05:00