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

  • 7dac9781bf
         feat(sat): phase saving. remember polarity of decisions Simon Cruanes 2022-08-21 13:52:52 -04:00
  • 65f8a61913
         feat(pure-sat): correct timing printing Simon Cruanes 2022-08-21 13:52:33 -04:00
  • 08606f4be0
         refactor: use proper type in sat.store Simon Cruanes 2022-08-21 13:40:53 -04:00
  • ca1abd8134
         fix(smt): perform CC check after theory actions Simon Cruanes 2022-08-20 22:07:21 -04:00
  • e0faf6ba72
         feat: some spans in main/process Simon Cruanes 2022-08-20 00:21:45 -04:00
  • 28ce38002f
         feat(profile): add ?args to spans Simon Cruanes 2022-08-20 00:21:28 -04:00
  • 3e39232696
         fix build temporarily Simon Cruanes 2022-08-19 21:33:49 -04:00
  • 4d97f1a525
         fix build Simon Cruanes 2022-08-19 21:32:55 -04:00
  • 5fa5fb5bd7
         fix(th-data): need to propagate from is-a eagerly Simon Cruanes 2022-08-19 21:31:27 -04:00
  • 177cd70fac
         feat(e_node): remove useless assertion Simon Cruanes 2022-08-19 21:31:04 -04:00
  • c643e547f6
         wip: refactor(th-data): remove some model building, cleanup code Simon Cruanes 2022-08-19 00:08:57 -04:00
  • 1c30fb1f95
         feat(sat): add counters for decision level/trail depth Simon Cruanes 2022-08-18 22:03:15 -04:00
  • a21389063a
         feat(log): if Profile is enabled, forward messages to it Simon Cruanes 2022-08-18 22:02:52 -04:00
  • 2bd555d11b
         feat(profile): proper string handling Simon Cruanes 2022-08-18 22:02:36 -04:00
  • 0c658e3ee4
         feat(term): add replace Simon Cruanes 2022-08-18 22:01:41 -04:00
  • 1b0d47a01d
         feat(profile): add basic counters Simon Cruanes 2022-08-18 20:56:17 -04:00
  • 27ccd367b2
         fix output so benchpress can parse it Simon Cruanes 2022-08-16 23:34:08 -04:00
  • 663f291bd5
         port fix for bug introduced in 1946a5e7 Simon Cruanes 2022-08-16 23:25:44 -04:00
  • 7fb557ae8b
         fix bug introduced in 1946a5e7 Simon Cruanes 2022-08-16 23:23:21 -04:00
  • 6a4947a25c
         feat(term): printer Simon Cruanes 2022-08-16 23:21:07 -04:00
  • b7eb6749a1
         add missing files from th-bool-dyn Simon Cruanes 2022-08-16 21:58:38 -04:00
  • a446af49be
         doc Simon Cruanes 2022-08-16 21:58:00 -04:00
  • b23a031519
         fix: time measurements were wrong Simon Cruanes 2022-08-16 21:45:16 -04:00
  • b61ec35451
         fix(th-bool-dyn): do not propagate, just add clauses depending on polarity Simon Cruanes 2022-08-16 21:37:56 -04:00
  • e4acb2cfca
         fix(th-bool-dyn): add clauses in partial check; register simplifier Simon Cruanes 2022-08-16 21:35:13 -04:00
  • 57941a952a
         add th-bool-dyn for dynamic boolean clausification Simon Cruanes 2022-08-16 21:30:17 -04:00
  • 5b87ff3e46
         feat(theory): add name accessor Simon Cruanes 2022-08-16 21:29:58 -04:00
  • 310d2183c4
         add Lit.Tbl,Lit.Set,Lit.Map Simon Cruanes 2022-08-16 21:29:45 -04:00
  • 947f790f9f
         debug in sat Simon Cruanes 2022-08-16 21:29:29 -04:00
  • 99dc9743a3
         doc Simon Cruanes 2022-08-16 21:29:12 -04:00
  • 6c14690fba
         cleanup code Simon Cruanes 2022-08-16 21:27:46 -04:00
  • e233c846ec
         refactor: cleanup config a bit Simon Cruanes 2022-08-16 21:27:32 -04:00
  • d5b7c2b0ee
         feat(printer): always put (), do not box applications Simon Cruanes 2022-08-16 21:27:09 -04:00
  • 94ba945bf3
         feat(cc.plugin): plugins have state, passed at init Simon Cruanes 2022-08-14 23:21:49 -04:00
  • e9dae47d0b
         fixup: modify benchpress for new output Simon Cruanes 2022-08-14 23:21:40 -04:00
  • 08a4ed892d
         feat(stat): improve printing Simon Cruanes 2022-08-14 23:21:22 -04:00
  • 2ab93aee04
         feat(main): fix initial time; better display (smtlib-friendly) Simon Cruanes 2022-08-14 23:21:02 -04:00
  • 6fca21bd33
         symlink in makefile Simon Cruanes 2022-08-14 22:35:34 -04:00
  • 541d0c2545
         cleanup Simon Cruanes 2022-08-14 22:33:21 -04:00
  • 6f42c060f4
         perf(util): more inlining Simon Cruanes 2022-08-14 22:32:51 -04:00
  • 23e70a192a
         perf(cc): more inlining; remove dead code Simon Cruanes 2022-08-14 22:32:28 -04:00
  • 82691069f1
         perf: dune flags Simon Cruanes 2022-08-14 22:32:21 -04:00
  • 6b09a562c5
         comment out tests for now Simon Cruanes 2022-08-14 14:17:18 -04:00
  • ba2e191882
         detail Simon Cruanes 2022-08-14 14:15:45 -04:00
  • ff6dc527bd
         comment out some profiling Simon Cruanes 2022-08-14 14:14:50 -04:00
  • 517a5d2e5f
         better tracing Simon Cruanes 2022-08-13 13:55:01 -04:00
  • 6ccabc70aa
         feat(sudoku): add stats Simon Cruanes 2022-08-13 13:45:38 -04:00
  • 63802fe3d6
         feat(stat): improve printing api Simon Cruanes 2022-08-13 13:45:21 -04:00
  • eddbf139fc
         refactor sudoku solver; make it compile; use new term repr Simon Cruanes 2022-08-13 13:30:21 -04:00
  • 92edae353d
         feat(sat): add mk_plugin_cdcl_t Simon Cruanes 2022-08-13 13:30:08 -04:00
  • c2eac5e2c3
         update doc Simon Cruanes 2022-08-13 13:30:03 -04:00
  • 632d5e3f40
         fix(core-logic): ensure store IDs fit in 5 bits Simon Cruanes 2022-08-13 13:29:49 -04:00
  • 7d46a38e2c
         fix compilation in unittest Simon Cruanes 2022-08-13 13:29:35 -04:00
  • 85314379a5
         fix type of is_a Simon Cruanes 2022-08-12 23:21:56 -04:00
  • 85eef2d117
         feat(base/data): fix types for cstor/select term builders Simon Cruanes 2022-08-12 23:17:20 -04:00
  • e99192869d
         remove debug Simon Cruanes 2022-08-12 23:17:15 -04:00
  • 593b693caf
         refactor lit a bit Simon Cruanes 2022-08-12 23:09:56 -04:00
  • 4d02e2a1c7
         fix(cc): bug in backtracking Simon Cruanes 2022-08-12 23:09:48 -04:00
  • 7bbe70b060
         bugfix in CC wip-better-cc-2022-07-21 Simon Cruanes 2022-08-12 23:07:32 -04:00
  • b73c1bf464
         feat(bool): use binary symbols for boolean operators Simon Cruanes 2022-08-10 22:41:53 -04:00
  • 67d5f244c1
         feat(Term): offer is_type and is_a_type Simon Cruanes 2022-08-10 22:41:26 -04:00
  • d14617ca77
         refactor: rush to have sidekick compile again. th-lra is commented out Simon Cruanes 2022-08-10 22:08:57 -04:00
  • 1f79ee05f2
         wip: make Base really usable, add th-data/th-bool Simon Cruanes 2022-08-10 22:08:43 -04:00
  • 8777682e07
         detail in core_logic Simon Cruanes 2022-08-10 22:08:33 -04:00
  • 81f159d25d
         feat(th-bool): add proof_rules, use std gensym Simon Cruanes 2022-08-10 22:08:09 -04:00
  • 647d66a196
         feat(th-data): use lists, not iter/array; add Proof_rules Simon Cruanes 2022-08-10 22:07:54 -04:00
  • b9c0265cb9
         feat(core): add Gensym module, add Proof_trace.close Simon Cruanes 2022-08-10 22:07:30 -04:00
  • 95dcb0ae74
         wip: refactor further Simon Cruanes 2022-08-09 22:41:13 -04:00
  • fc5ce9bf87
         wip: make it compile Simon Cruanes 2022-08-08 21:52:47 -04:00
  • 7d59846d72
         wip: refactor base Simon Cruanes 2022-08-08 21:52:39 -04:00
  • 8003cdcebb
         sidekick-mini-cc: remove functor Simon Cruanes 2022-08-08 21:52:20 -04:00
  • 95beb2bf27
         core: add better printer Simon Cruanes 2022-08-08 21:49:47 -04:00
  • f17e689a3c
         feat(cc): adapt to the new CC_view Simon Cruanes 2022-08-08 21:22:48 -04:00
  • 2a8eb0c166
         refactor tests for mini-cc Simon Cruanes 2022-08-08 21:22:33 -04:00
  • 7aa113f379
         feat(core): make CC_view part of the core library; with default CC view Simon Cruanes 2022-08-08 21:17:37 -04:00
  • 010451145c
         fix(core-logic): bad constant for ite Simon Cruanes 2022-08-08 21:16:54 -04:00
  • 97a5c8efa3
         detail Simon Cruanes 2022-08-07 22:42:35 -04:00
  • 5b6fd14dcf
         wip: refactor(base): split into several views, all based on Const Simon Cruanes 2022-08-07 22:41:26 -04:00
  • 4dcc3ea4ad
         small changes in smt Simon Cruanes 2022-08-07 22:41:13 -04:00
  • 86bc9453d5
         rename dir Simon Cruanes 2022-08-07 22:41:05 -04:00
  • c2af589282
         add core.bool_view Simon Cruanes 2022-08-07 22:40:39 -04:00
  • c873346047
         detail in th-lra Simon Cruanes 2022-08-05 21:56:45 -04:00
  • a7e7b38d1b
         core: re-export Const.t properly Simon Cruanes 2022-08-05 21:56:23 -04:00
  • 24e79df776
         wip: refactor base Simon Cruanes 2022-08-05 21:55:53 -04:00
  • 4aec4fe491
         refactor(proofs): make proof terms a recursive term Simon Cruanes 2022-08-01 20:42:45 -04:00
  • 1edf054104
         refactor(proof): use a suspension but keep uniform Proof_term.data type Simon Cruanes 2022-07-31 15:00:27 -04:00
  • dd50ab079e
         remove most proof-trace code Simon Cruanes 2022-07-30 23:59:15 -04:00
  • 06107c212f
         remove most sigs Simon Cruanes 2022-07-30 23:58:34 -04:00
  • 65e876bebc
         chore: makefile Simon Cruanes 2022-07-30 23:58:18 -04:00
  • ee2ea784ad
         remove Vec_unit Simon Cruanes 2022-07-30 23:22:25 -04:00
  • 36204c5e5e
         refactor some more Simon Cruanes 2022-07-30 23:04:49 -04:00
  • 0ff5ac9a3f
         refactor(th-lra): rename to th-lra Simon Cruanes 2022-07-30 23:03:57 -04:00
  • 0d0751b7d2
         refactor(theories): remove functors Simon Cruanes 2022-07-30 23:01:29 -04:00
  • df9fa11507
         refactor(th-lra): adapt to new code Simon Cruanes 2022-07-30 21:51:46 -04:00
  • 05faac97e7
         refactor(smt): remove functor, split into modules Simon Cruanes 2022-07-30 21:18:30 -04:00
  • 6e1da96e7e
         include solver directly in Sidekick_sat Simon Cruanes 2022-07-30 21:18:18 -04:00
  • 1e1b0f352d
         feat(simplify): add sidekick_simplify library Simon Cruanes 2022-07-30 21:17:55 -04:00
  • 83e456ef8a
         remove sidekick_lit functor Simon Cruanes 2022-07-30 21:17:37 -04:00
  • 1ecb189fd5
         refactor: core and CC Simon Cruanes 2022-07-30 21:17:20 -04:00
  • 085e37e063
         refactor(sat): remove functor, split into modules Simon Cruanes 2022-07-30 20:27:47 -04:00