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

1891 commits

This branch
This branch
All branches
Author SHA1 Message Date
Simon Cruanes
efc01f507b
feat(term): add is_pi and weak containers 2022-09-01 22:33:15 -04:00
Simon Cruanes
2092bbef3f
feat(gensym): add reset 2022-09-01 22:32:52 -04:00
Simon Cruanes
0797ff0409
tiny helper 2022-09-01 22:32:24 -04:00
Simon Cruanes
8db63dbdc4
th-comb: remove claim-term, add claim-type 2022-09-01 22:31:50 -04:00
Simon Cruanes
1ce1bd31b9
theory for uninterpreted types 2022-09-01 22:31:37 -04:00
Simon Cruanes
52b60c4114
fix(main): method for measuring memory overhead was wrong 2022-08-31 00:47:11 -04:00
Simon Cruanes
34ad038d9a
temp: disable partial checks in LRA 2022-08-31 00:42:17 -04:00
Simon Cruanes
80b08e03cb
feat(const): add opaque_to_cc property, to control CC 2022-08-31 00:41:42 -04:00
Simon Cruanes
4dca7df629
actions: run tests on 4.14 only 2022-08-29 21:05:48 -04:00
Simon Cruanes
0f21cf069e
test: update expected results 2022-08-29 20:28:42 -04:00
Simon Cruanes
737a11504d
Merge branch 'wip-defunctorize-terms' 2022-08-29 20:27:27 -04:00
Simon Cruanes
83a4ae46c1
fix: use standard = even for LRA terms 
the LRA_view is only useful for views, but we build =/neq using builtin
=
 2022-08-28 00:22:51 -04:00
Simon Cruanes
28ad97d2b7
fix: typecheck issue 2022-08-27 23:42:19 -04:00
Simon Cruanes
4c90405391
refactor a bit 2022-08-27 23:09:29 -04:00
Simon Cruanes
01d0668fc6
fix(sat): check for new atoms in termination check in final_check 2022-08-27 23:08:58 -04:00
Simon Cruanes
5feb5d8e73
refactor: new API for combination, with theories claiming terms 
interface variables are terms claimed by >= 2 theories. Theories now
have a unique ID attributed at their creation.
 2022-08-27 22:51:16 -04:00
Simon Cruanes
ccb3753668
wip(smt): theory combination 2022-08-27 21:38:20 -04:00
Simon Cruanes
2a0feed32c
format 2022-08-27 20:48:32 -04:00
Simon Cruanes
df287e4ef7
update doc/guide 2022-08-27 20:44:30 -04:00
Simon Cruanes
137183f2fe
small fixes, warnings 2022-08-27 20:44:13 -04:00
Simon Cruanes
e3aa43f817
cleanup 2022-08-27 20:39:06 -04:00
Simon Cruanes
40734d5074
doc: update guide (temporarily) 
models still need to be updated.
 2022-08-27 20:24:28 -04:00
Simon Cruanes
90f100d9b1
helpers to build terms and solvers 2022-08-27 20:24:28 -04:00
Simon Cruanes
5f91d0bd76
fix spurious \r 2022-08-27 12:36:45 -04:00
Simon Cruanes
f0041f9dae
feat: reinstate LRA theory and terms 2022-08-26 22:17:02 -04:00
Simon Cruanes
e66a27229b
detail in printing 2022-08-26 22:16:45 -04:00
Simon Cruanes
e03e5e77a9
add LRA_term to base 2022-08-25 23:03:12 -04:00
Simon Cruanes
28173c1852
feat(term): replace E_app_uncurried with E_app_fold 2022-08-25 20:50:56 -04:00
Simon Cruanes
f6efc8f575
more unsat tests 2022-08-25 20:50:50 -04:00
Simon Cruanes
4d78be0c52
wip: model builder 2022-08-25 20:13:49 -04:00
Simon Cruanes
6ad07921c4
details 2022-08-22 22:12:27 -04:00
Simon Cruanes
dde63a9ef2
refactor: stats, small changes 2022-08-22 22:12:27 -04:00
Simon Cruanes
279ceade78
feat(base): in Form, use uncurried forms for and/or 2022-08-22 22:12:27 -04:00
Simon Cruanes
9762968373
feat(bool): use lists for B_and/B_or, along with App_uncurried 2022-08-22 22:12:27 -04:00
Simon Cruanes
dd66efb772
feat(term): add App_uncurried constructor 
sometimes currying is really costly. For example, in boolean formulas,
the formula `/\_i=1^100 a_i` has 100 atoms as subterms, but if
represented curried with binary `/\` it also has 98 intermediate
conjunctions as subterms. With how the rest of sidekick works, this
means each of these gets its own atom and CNF; instead we're going to
use App_uncurried.
 2022-08-22 22:12:27 -04:00
Simon Cruanes
dff65c5d26
refactor: Term.abs takes store again, so abs false can be false,true 2022-08-22 22:12:26 -04:00
Simon Cruanes
0ff197d56c
perf(core): have eq and not_ be simplying 
- `a=b` and `b=a` are now the same
- `not (not u)` and `u` are now the same
 2022-08-22 22:01:02 -04:00
Simon Cruanes
9c57dad3f1
perf: small changes in Event 2022-08-21 22:56:38 -04:00
Simon Cruanes
1eb26e5091
refactor(cc): cleanup a bit, smaller closures for backtracking 2022-08-21 22:34:15 -04:00
Simon Cruanes
30cf71522c
small refactor of CC 2022-08-21 22:01:07 -04:00
Simon Cruanes
e34f5a5c3c
cleanup 2022-08-21 13:53:48 -04:00
Simon Cruanes
007fbad243
fix some stats 2022-08-21 13:53:36 -04:00
Simon Cruanes
7dac9781bf
feat(sat): phase saving. remember polarity of decisions 2022-08-21 13:52:52 -04:00
Simon Cruanes
65f8a61913
feat(pure-sat): correct timing printing 2022-08-21 13:52:33 -04:00
Simon Cruanes
08606f4be0
refactor: use proper type in sat.store 2022-08-21 13:40:53 -04:00
Simon Cruanes
ca1abd8134
fix(smt): perform CC check after theory actions 2022-08-20 22:07:21 -04:00
Simon Cruanes
e0faf6ba72
feat: some spans in main/process 2022-08-20 00:21:45 -04:00
Simon Cruanes
28ce38002f
feat(profile): add ?args to spans 2022-08-20 00:21:28 -04:00
Simon Cruanes
3e39232696
fix build temporarily 2022-08-19 21:34:21 -04:00
Simon Cruanes
4d97f1a525
fix build 2022-08-19 21:32:55 -04:00