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