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
1917 commits 53 branches 1 tag 17 MiB
Commit graph

1917 commits

This branch
This branch
All branches
Author SHA1 Message Date
Simon Cruanes
469b97934a
fix: more type checks in preprocess 2022-09-11 14:26:34 -04:00
Simon Cruanes
3d0461936f
fix: remove spurious check? 2022-09-11 14:10:01 -04:00
Simon Cruanes
abff92d972
fix warning 2022-09-11 14:09:56 -04:00
Simon Cruanes
67c9ffa2ac
fix(lit): add type checking assertion 2022-09-11 14:09:03 -04:00
Simon Cruanes
fad651a4cb
fix(find_foreign): memoization needs to account for is_sub 2022-09-11 13:55:25 -04:00
Simon Cruanes
337a0696f1
update guide 2022-09-10 22:22:30 -04:00
Simon Cruanes
f024fe821e
add regression test 2022-09-10 21:55:49 -04:00
Simon Cruanes
c9127c6cd7
fix(base/form): fix CNF for equiv 2022-09-10 21:48:51 -04:00
Simon Cruanes
fd39a414c3
fix(smt): sign error in literal 2022-09-10 21:48:08 -04:00
Simon Cruanes
7876820d4d
remove dead code 2022-09-10 15:02:44 -04:00
Simon Cruanes
87e91660ad
doc: update guide for now 2022-09-10 15:02:17 -04:00
Simon Cruanes
b8ee815d9d
update tools 2022-09-10 14:59:52 -04:00
Simon Cruanes
721ed2eac0
refactor(preprocess): introduce Find_foreign, runs after preprocess 2022-09-10 14:10:36 -04:00
Simon Cruanes
3d95fc16c4
feat(cc): use Term.pp. not Term.pp_debug 2022-09-10 14:10:13 -04:00
Simon Cruanes
8811699410
feat(term): add open_eq 2022-09-10 14:09:55 -04:00
Simon Cruanes
659fa7ba5b
wip: feat(lra): update to newer preprocessing 2022-09-09 22:16:59 -04:00
Simon Cruanes
e9c2491380
feat(th-bool): properly preprocess in equiv 2022-09-09 22:16:48 -04:00
Simon Cruanes
e94a7bd31c
refactor(preprocess): directly forward preprocess actions to solver 2022-09-08 22:05:40 -04:00
Simon Cruanes
c9138144f3
refactor(preprocess): break infinite recursion 2022-09-08 21:55:09 -04:00
Simon Cruanes
317f406620
wip: refactor(preprocess): recursive preprocess guided by theories 2022-09-07 19:35:09 -04:00
Simon Cruanes
6101e029b3
feat(core): add box, with a box constant 
this is a good alternative to gensym for preprocessing, as it is
idempotent and functional.
 2022-09-07 19:34:31 -04:00
Simon Cruanes
f7daf7e45e
wip: add theory combination to Preprocess, based on claim hooks 
theories must register hooks that specify what terms they claim for
their own, so that preprocess (which look at all terms and has the
global picture) can find where foreign terms are and give these to th
combination.
 2022-09-03 14:45:09 -04:00
Simon Cruanes
16eb12fac2
wip: preprocess in its own file 2022-09-03 14:09:13 -04:00
Simon Cruanes
e74439cf2a
wip: new attempt at theory combination 2022-09-01 22:34:27 -04:00
Simon Cruanes
47a0b075f0
fix(model builder): allow multiple add 2022-09-01 22:33:59 -04:00
Simon Cruanes
d741b4160d
remove is_valid_literal concept 2022-09-01 22:33:40 -04:00
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