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

Commit graph

  • 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
  • 50bfe79b6a
         test: use dune options, so, release mode Simon Cruanes 2022-02-02 16:12:29 -05:00
  • dbb9dabd1d
         simpler printing of models Simon Cruanes 2022-02-02 16:12:11 -05:00
  • a0a67549de
         feat(lra): proper model production from the simplex Simon Cruanes 2022-02-02 16:02:23 -05:00
  • 3fdb07b533
         feat: handle get-model/get-value from smtlib inputs Simon Cruanes 2022-02-02 15:51:44 -05:00
  • 3b1535e70a deploy: 4cdbaf17bf c-cube 2022-02-02 03:26:50 +00:00
  • 4cdbaf17bf
         fix opam file Simon Cruanes 2022-02-01 22:21:03 -05:00
  • 70206101f0
         feat: update bare Simon Cruanes 2022-02-01 22:10:31 -05:00
  • c99e02b38a
         try to fix tests for now Simon Cruanes 2022-01-31 15:45:15 -05:00
  • 44ad0935fe
         chore: add QF_UFLIA to makefile Simon Cruanes 2022-01-31 15:45:02 -05:00
  • cb369ec68d
         easier list of known logic Simon Cruanes 2022-01-31 15:28:02 -05:00
  • 3c41ab2484
         refactor: new term representation for LIA/LRA Simon Cruanes 2022-01-31 15:13:25 -05:00
  • d4cf722d32
         wip: LIA: just relax to LRA for now Simon Cruanes 2022-01-31 15:12:55 -05:00
  • 8b78057058
         test: detail Simon Cruanes 2022-01-31 11:08:46 -05:00
  • 10c8006597
         intsolver: partial implementation Simon Cruanes 2022-01-31 11:08:20 -05:00
  • be7451b070
         add ediv to arith Simon Cruanes 2022-01-31 11:08:01 -05:00
  • e77d2b81ca
         wip: feat(intsolver): classify constraints into sets E,L,G,M Simon Cruanes 2022-01-19 11:43:35 -05:00
  • 04e9d5b93c
         test: limit size of linexps in simplex tests Simon Cruanes 2022-01-19 11:43:22 -05:00
  • a6c056969c
         test: limit size of linexps in intsolver tests Simon Cruanes 2022-01-19 11:42:42 -05:00
  • 7ea4c4fb4a
         arith: more functions in Int Simon Cruanes 2022-01-19 11:42:31 -05:00
  • 417f4cf8ec
         wip: intsolver Simon Cruanes 2022-01-14 13:50:07 -05:00
  • f713106514
         lia: use branch and bound a bit Simon Cruanes 2022-01-14 13:34:23 -05:00
  • eaf56a941f
         test: hook intsolver tests Simon Cruanes 2022-01-14 13:34:15 -05:00
  • af1a1478f2
         wip: feat(intsolver): new integer solver based on FM extension (Williams '75) Simon Cruanes 2022-01-14 13:31:17 -05:00
  • 6e0358f5e1
         refactor(simplex): small changes, mostly debug Simon Cruanes 2022-01-14 13:30:50 -05:00
  • 4a9a128ab0
         test: rename test simplex Simon Cruanes 2022-01-14 11:35:25 -05:00
  • 38a6727f44
         udpate test Simon Cruanes 2022-01-14 11:35:04 -05:00
  • 5989d686da
         chore: add target to makefile Simon Cruanes 2022-01-13 12:55:15 -05:00
  • 4b2afd7a05
         wip: LIA theory Simon Cruanes 2022-01-13 12:54:35 -05:00
  • 7f2e92fe88
         feat(arith): more functions in Q Simon Cruanes 2022-01-13 12:54:09 -05:00
  • f1f1967059
         refactor: move simplex to its own library sidekick.simplex Simon Cruanes 2022-01-13 12:50:22 -05:00
  • 803b40bccf
         refactor(sat): cleaner store for delayed actions Simon Cruanes 2022-01-11 16:50:59 -05:00
  • 999e83f91c
         fix(lra): remove bound propagation, it is sometimes late to the party Simon Cruanes 2022-01-11 12:22:46 -05:00
  • 44af0afd59
         fix(lia): problems with only integer constants are not incomplete Simon Cruanes 2022-01-11 13:17:01 -05:00