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