| .. |
|
abstract-solver
|
feat(asolver): add pp_stats
|
2023-05-07 21:03:32 -04:00 |
|
algos/simplex
|
wip: feat(lra): update to newer preprocessing
|
2022-09-09 22:16:59 -04:00 |
|
arith
|
feat(tracing): introduce term/const serialization
|
2022-09-23 22:13:21 -04:00 |
|
base
|
detail in sidekick_base
|
2023-05-07 21:03:33 -04:00 |
|
bencode
|
improve tracing, add show_trace
|
2022-09-30 22:11:41 -04:00 |
|
bin-lib
|
use ocamlformat
|
2022-07-14 22:09:13 -04:00 |
|
cc
|
fix(CC): give proper explanations to on-merge hook conflicts
|
2023-05-07 21:03:31 -04:00 |
|
cdsat
|
cdsat
|
2023-05-09 20:42:24 -04:00 |
|
checker
|
remove veci32
|
2022-07-15 20:32:06 -04:00 |
|
core
|
feat(gensym): nicer names for gensym symbols
|
2022-10-19 22:25:29 -04:00 |
|
core-logic
|
feat(cdsat): use Vars_to_decide to decide in main outer loop
|
2023-05-07 21:03:34 -04:00 |
|
drup
|
remove veci32
|
2022-07-15 20:32:06 -04:00 |
|
main
|
feat(cdsat): embryo of plugins for bool and UF
|
2023-05-07 21:03:33 -04:00 |
|
memtrace
|
details: synopsis in dune files
|
2022-07-28 23:30:42 -04:00 |
|
mini-cc
|
sidekick-mini-cc: remove functor
|
2022-08-08 21:52:20 -04:00 |
|
proof
|
depth-restricted printing for terms and pterms
|
2022-10-13 21:43:16 -04:00 |
|
quip
|
use ocamlformat
|
2022-07-14 22:09:13 -04:00 |
|
sat
|
refactor: model building in smtlib, for smtlib
|
2022-10-15 22:42:10 -04:00 |
|
sigs
|
small change in sigs
|
2023-05-07 21:03:31 -04:00 |
|
simplify
|
refactor(simplify): use new proof trace from sidekick.proof
|
2022-10-12 12:20:50 -04:00 |
|
smt
|
feat(asolver): add pp_stats
|
2023-05-07 21:03:32 -04:00 |
|
smtlib
|
add todo
|
2022-10-23 20:58:25 -04:00 |
|
tef
|
update to handle mtime 2.0
|
2023-02-23 21:02:21 -05:00 |
|
th-bool-dyn
|
refactor: update remaining theories for new proof style
|
2022-10-12 22:19:00 -04:00 |
|
th-bool-static
|
refactor(th-bool): no need for gensym
|
2022-10-19 22:26:37 -04:00 |
|
th-cstor
|
fix(CC): give proper explanations to on-merge hook conflicts
|
2023-05-07 21:03:31 -04:00 |
|
th-data
|
fix(CC): give proper explanations to on-merge hook conflicts
|
2023-05-07 21:03:31 -04:00 |
|
th-lra
|
fix(CC): give proper explanations to on-merge hook conflicts
|
2023-05-07 21:03:31 -04:00 |
|
th-unin-ty
|
theory for uninterpreted types
|
2022-09-01 22:31:37 -04:00 |
|
tools
|
update tools
|
2022-09-10 14:59:52 -04:00 |
|
trace
|
improve Int_id for tracing
|
2022-10-12 12:20:20 -04:00 |
|
util
|
feat(util): improve debug printer wrt newlines
|
2023-05-07 21:03:33 -04:00 |
|
zarith
|
feat(tracing): introduce term/const serialization
|
2022-09-23 22:13:21 -04:00 |
