simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-10 05:03:59 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions
1009 commits 53 branches 1 tag 17 MiB
Commit graph

80 commits

Author SHA1 Message Date
Simon Cruanes
0aa13ca808 refactor: provide a state for Ty.bool in core signature 2021-02-24 15:52:54 -05:00
Simon Cruanes
2810312e2f add simplify to LRA 2021-02-22 21:10:18 -05:00
Simon Cruanes
04615e4e3d Merge branch 'wip-lra-simplex' 2021-02-22 17:13:39 -05:00
Simon Cruanes
cfbd352ca0 feat(lra): restore theory combination; improve preprocessing 2021-02-16 14:01:21 -05:00
Simon Cruanes
a908f2b3f2 feat(arith): integrate simplex2 into sidekick; remove old simplex 2021-02-15 16:19:39 -05:00
Simon Cruanes
fafb001934 feat: add profiling system based on TEF 
- a `Sidekick_util.Profile` module, deps-free
- an optional sidekick.tef library that needs unix+mtime
 2020-12-22 16:27:45 -05:00
Simon Cruanes
35e5e30e93 fix(smtlib): handle "xor" 2020-12-22 14:59:21 -05:00
Simon Cruanes
14bb5898f0 Merge branch 'wip-fix-lra' into wip-lra-simplex-unsat-core 2020-12-22 11:46:09 -05:00
Simon Cruanes
db1c50f7ed feat(LRA): expose model after fourier-motzkin returns "SAT" 2020-11-17 16:52:49 -05:00
Simon Cruanes
77b33346f5 fix(tycheck): handle proper unary minus 2020-11-14 13:17:23 -05:00
Simon Cruanes
5ff0fff85b wip: refactor(lra): import Simplex from funarith, replace FM with it 2020-11-13 22:35:59 -05:00
Simon Cruanes
9a3e387405 refactor: explicit recursion in preprocessing 
if a preprocessor fires, it's up to it to preprocess subterms. rewriting
is now from the root, not the leaves on.

Use that in LRA to rewrite under linear expressions.
 2020-11-12 18:21:37 -05:00
Simon Cruanes
534fc45783 wip: better progress bar 2020-10-11 23:30:22 -04:00
Simon Cruanes
3449404964 refactor: move base-term to sidekick-arith 2020-10-10 17:43:42 -04:00
Simon Cruanes
349d884664 chore: add sidekick-arith library, depends on zarith 2020-10-10 17:18:20 -04:00
Simon Cruanes
e9931b377c remove bloody warn-error 2020-10-10 16:00:21 -04:00
Simon Cruanes
dc320bf0c9 fix(tycheck): handle n-ary +/- 2020-10-10 14:34:05 -04:00
Simon Cruanes
fabdb27dfe wip: feat(lra): preprocess by renaming lits/terms and storing defs 2020-10-04 21:37:03 -04:00
Simon Cruanes
ac6ca7d584 wip: properly typecheck and build LRA terms 2020-10-04 00:32:52 -04:00
Simon Cruanes
943efad206 feat: add AST for LRA 2020-10-03 23:46:45 -04:00
Simon Cruanes
216cbe762f missing lra file 2020-09-23 21:59:33 -04:00
Simon Cruanes
f59a5d9fce wip 2020-09-23 21:59:33 -04:00
Simon Cruanes
aff2e29a6b wip: representing real types and values 2020-09-23 21:59:29 -04:00
Simon Cruanes
4f12bfdb93 wip: LRA 2020-09-23 21:58:54 -04:00
Simon Cruanes
40d47a8d6c wip: lra 2020-09-23 21:58:54 -04:00
Simon Cruanes
95edfd9aa9 wip: LRA theory 2020-09-23 21:58:54 -04:00
Simon Cruanes
7d399ba201 handle :named attribute in smtlib 2020-08-18 10:01:36 -04:00
Simon Cruanes
e21dea4780 feat(cc): flag some explanations as being theory-induced 2020-01-17 18:49:14 -06:00
Simon Cruanes
a31b2b36ef fixes: add missing expl in monoids; handle is-c t 2020-01-14 22:41:33 -06:00
Simon Cruanes
b332e8ceb0 fix: preprocess away "ite" 2020-01-14 20:23:23 -06:00
Simon Cruanes
e58b29da02 fix(term): hashconsing error leading to non termination 2019-12-28 08:49:14 -06:00
Simon Cruanes
7c951c08ff wip: use t=c instead of (is _ c) t for nullary constructors 2019-12-28 05:17:47 -06:00
Simon Cruanes
444a0b9f85 wip: theory of datatypes 2019-12-28 05:17:47 -06:00
Simon Cruanes
8c5e28da28 wip: theory of datatypes 2019-12-28 05:17:47 -06:00
Simon Cruanes
949e079867 wip: add datatypes 2019-12-28 05:17:47 -06:00
Simon Cruanes
10cfa137b6 feat: handle parsing of .cnf files 2019-11-23 13:41:03 -06:00
Simon Cruanes
9b99560130 feat: handle typechecking and term building for datatypes 2019-11-23 13:23:30 -06:00
Simon Cruanes
3327c86841 refactor(smtlib): remove intermediate typed AST, type directly into terms 2019-11-23 13:23:30 -06:00
Simon Cruanes
409fe49ff0 feat(bin): use stmlib-utils 0.1, with versionned API and new statements 2019-11-07 10:35:59 -06:00
Simon Cruanes
8162a841fe refactor: depend on smtlib-utils instead of having custom parser 2019-11-05 17:11:32 -06:00
Simon Cruanes
9ddce6a186 feat(check-cc): add statistics 2019-10-30 13:31:04 -05:00
Simon Cruanes
7d8589accd refactor: change the functor stack 2019-10-29 15:06:19 -05:00
Simon Cruanes
0031c64ea9 feat(th-bool-static): check for new terms in the CC in final check 2019-10-08 09:08:05 -05:00
Simon Cruanes
49a7446631 feat(th-bool-static): add non-traversable opaque boolean term 2019-10-05 18:37:49 -05:00
Simon Cruanes
238226500a feat: add is_valid_literal filter to add_term_rec 2019-10-02 18:15:06 -05:00
Simon Cruanes
769b80030a feat: progress bar in solver 2019-07-31 04:36:32 -05:00
Simon Cruanes
d527b2b945 fix: remove some module aliases for 4.08 2019-07-31 03:25:04 -05:00
Simon Cruanes
70e4c655a2 refactor: split smtlib+bin into their own opam package 2019-06-07 17:59:07 -05:00
Simon Cruanes
38f001b0e7 refactor: move Lit inside the solver, as output, not input 2019-06-07 17:31:11 -05:00
Simon Cruanes
12ea0c3be4 feat: check propagations if --check is passed 2019-06-07 14:58:46 -05:00