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

18 commits

Author SHA1 Message Date
Simon Cruanes
3c41ab2484
refactor: new term representation for LIA/LRA 2022-01-31 15:13:25 -05:00
Simon Cruanes
4b2afd7a05
wip: LIA theory 2022-01-13 12:55:36 -05:00
Simon Cruanes
8410a57f1a
wip: feat(LIA): LIA solver, will rely on LRA solver 
we want to reuse the simplex, but do branch and bound + cutting planes
 2022-01-11 14:00:04 -05:00
Simon Cruanes
849d4319f2
fix theory combination for LRA 2022-01-11 14:00:04 -05:00
Simon Cruanes
2378fc37ac
fix LIA->LRA cast operation 2022-01-11 14:00:04 -05:00
Simon Cruanes
671fa6515a
fix missing conversions 2022-01-11 14:00:04 -05:00
Simon Cruanes
691ff12a01
wip: support LIA in input AST and base terms 2022-01-11 14:00:03 -05:00
Simon Cruanes
63f50d03fa
feat: proper proof production for theory merges in CC 
this involves resolution steps between the lemma (typically a kind of
horn clause with the merge as conclusion) and a bunch of literals
responsible for some equational hypotheses of this horn clause, being true
 2021-12-29 15:56:54 -05:00
Simon Cruanes
63eeb81290
refactor: modify interface of Th_data 2021-12-17 11:39:22 -05:00
Simon Cruanes
3589592296
wip: use real proofs 2021-10-16 22:00:29 -04:00
Simon Cruanes
597a6c378e
wip: split VecI32 and VecSmallInt 
- use VecSmallInt for small integers of type `int`
- use VecI32 to store actual int32 (in particular for proof steps)
 2021-10-16 20:31:56 -04:00
Simon Cruanes
fd1d068997
proof stubs and sat proof 2021-10-12 22:13:28 -04:00
Simon Cruanes
4308eba04d
fix 2021-10-11 23:19:40 -04:00
Simon Cruanes
e7e8873295
fix more warnings 2021-08-27 09:28:59 -04:00
Simon Cruanes
9f01b98cde wip: imperative proofs 
- getting closer to having the SMT solver compile again
- dummy proof implementation
- DRUP proof implementation for pure SAT solver
 2021-08-18 23:59:39 -04:00
Simon Cruanes
458f5fa9b6 finish renaming 2021-08-18 00:03:16 -04:00
Simon Cruanes
6578ea9136 move form to sidekick_base; rename {Term,Ty}.state into store 2021-07-03 22:48:44 -04:00
Simon Cruanes
80b50e8744 refactor: add solver instance in sidekick base 
move some functor instantiations from `sidekick-bin.smtlib` to
`sidekick-base.solver` so they're usable from a library.
 2021-07-03 22:28:57 -04:00