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

253 commits

Author SHA1 Message Date
Simon Cruanes
2430eb754d feat(cc): make bitfields non-global; remove dead code 2019-06-11 11:38:54 -05:00
Simon Cruanes
ed4ba4057f feat: solver actions are the same as CC actions 2019-06-11 10:28:00 -05:00
Simon Cruanes
3e7ef47fab feat: add CC.merge_t 2019-06-11 10:26:04 -05:00
Simon Cruanes
36449d1645 feat(cc): expose a way to access bitfields 2019-06-10 15:19:57 -05:00
Simon Cruanes
6c603d5589 refactor: remove code that checks invariants 2019-06-10 14:28:05 -05:00
Simon Cruanes
b2f6a30cc8 feat: function to add a theory and retain its state 2019-06-10 14:16:09 -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
ef1110925f feat(cc): callback on propagations 2019-06-07 14:58:41 -05:00
Simon Cruanes
357dc73426 feat(check): use mini-cc to check CC conflicts on the fly 2019-06-07 14:47:52 -05:00
Simon Cruanes
2efa811b3f fix: more precise signature 2019-06-07 11:34:06 -05:00
Simon Cruanes
e3e964a4c6 fix: first version that seems to work on QF_UF 2019-06-07 11:23:53 -05:00
Simon Cruanes
cad49b3747 wip: preprocess/simplify as part of theories 2019-06-06 17:13:21 -05:00
Simon Cruanes
2e7ab9ba9b wip: simplify a lot and only keep th-bool-static in the functor 2019-06-05 16:53:13 -05:00
Simon Cruanes
080a20480f refactor: continue functorization of sidekick 2019-05-27 19:55:21 -05:00
Simon Cruanes
c36092d217 refactor: updated interface for sidekick_core 2019-05-27 17:03:51 -05:00
Simon Cruanes
6e9e95c233 wip: functorize everything 2019-05-26 23:20:47 -05:00
Simon Cruanes
bb0c0d44b2 wip: add core library with signatures for the whole system 2019-05-18 18:27:39 -05:00
Simon Cruanes
d73684902f wip: have a proper smtlib parser 2018-02-05 23:09:29 -06:00
Simon Cruanes
221ed7dcdb continue large refactoring, progress in theory combination 
- first draft of theory combination
- theory interface
- have the project compile
 2018-02-01 22:53:06 -06:00
Simon Cruanes
50fe488dcb refactor types for terms and congruence closure 
- terms are extensible
- explanations have a custom case, shaped as a term
- remove distinction repr/node in Equiv_class, for simplicity
- make propositional connectives n-ary
 2018-01-30 21:55:37 -06:00
Simon Cruanes
3e50a3fc5d some updates to core lib 2018-01-26 21:32:21 -06:00
Simon Cruanes
ac396e8cf5 rename to cdcl 2018-01-22 22:09:47 -06:00
Simon Cruanes
8c8209c08c large refactoring to keep only a simpler, easier CDCL(T) interface 
- only one functor to instantiate
- explicit state that is carried around
- remove minismt stuff
 2018-01-22 21:52:06 -06:00
Simon Cruanes
7324647fb1 doc 2018-01-03 22:08:55 +01:00
Simon Cruanes
53cc8b35a0 more controled API for Res 2018-01-03 22:07:40 +01:00
Simon Cruanes
3f4f7ec7e4 a bit of doc 2018-01-03 22:01:12 +01:00
Simon Cruanes
c7015450a1 typo 2017-12-29 22:10:01 +01:00
Simon Cruanes
2caf53c24f expose {push,pop} in main solver 2017-12-29 21:29:43 +01:00
Simon Cruanes
be929d056a remove useless functions 2017-12-29 19:12:17 +01:00
Simon Cruanes
d47071c4f0 reinstate better way of picking watch literals 2017-12-29 19:00:54 +01:00
Simon Cruanes
70fcded713 reset some record accesses, for perf 2017-12-29 18:53:26 +01:00
Simon Cruanes
d415f8ed20 do not expose St in solver, but only expose a restricted API. 2017-12-29 18:29:56 +01:00
Simon Cruanes
c14f0ba020 make Solver.t more lightweight by removing some useless fields 2017-12-29 17:29:24 +01:00
Simon Cruanes
a65309d5e6 add optional size argument to create functions 2017-12-29 17:24:09 +01:00
Simon Cruanes
99078b2335 make state explicit and add type t state-wrapper in most modules 2017-12-29 16:48:26 +01:00
Simon Cruanes
148c1da3cc wip: use submodules of Solver_types to clean up code 2017-12-29 15:29:04 +01:00
Simon Cruanes
06af58e6f3 faster addition of clauses' watch literals 
instead of sorting the whole clause, just select two highest level lits
 2017-12-29 12:32:27 +01:00
Simon Cruanes
d6c84b93bf restrict what Msat core lib exposes, provide shortcuts 2017-12-28 19:31:55 +01:00
Simon Cruanes
1037c06636 use generative functors, remove a layer of nesting for SMT libs 2017-12-28 19:12:41 +01:00
Simon Cruanes
db54c8e9b2 cleanup in fields 2017-12-28 18:03:00 +01:00
Simon Cruanes
7722319b0a move tseitin transformation into its own lib 2017-12-28 16:01:36 +01:00
Simon Cruanes
ac50e10788 big refactoring 
- move to jbuilder
- use a functorial heap (with indices embedded in lit/var)
- update Vec with optims from mc2
- change semantics of Vec.shrink
- use new Log module
 2017-12-28 15:51:04 +01:00
Simon Cruanes
fc5a2d4e9d capitalization of files; add new Log 2017-12-28 14:13:10 +01:00
Guillaume Bury
bed469c0cf Clear unused hyps in coq proofs 2017-08-29 15:18:10 +02:00
Guillaume Bury
7749f7aaac Manual re-indent 2017-08-25 19:15:12 +02:00
Guillaume Bury
679d928b88 Auto re-indent 2017-08-25 19:11:58 +02:00
Guillaume Bury
4989026f06 Fix mcsat conflict analysis 
When analyzing an mcst conflict clause and looking at a semantic
propagation in the trail, the last resolved clause was looked at again,
which caused an invalid history to be generated (the computation of the
backtrack clause was not affected because the second resolution of the clause
was basically a no-op thanks to the 'seen' field), thus it did not
introduce any soundness bug, just a faulty clause history which was
caught during proof expansion.
 2017-08-25 18:33:42 +02:00
Guillaume Bury
607ec3f043 Added Coq backend (not tested yet) 2017-08-09 09:45:18 +02:00
Guillaume Bury
0c99e6b2e7 [breaking] Better interface for the DOT backend 2017-07-20 13:55:55 +02:00
Guillaume Bury
92835bcdda Add useful function on proof steps 
These new functions are designed to help people if (or when) the proof
API will break next time (i.e. adding a new variant case in step).
 2017-04-12 20:48:08 +02:00