simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

TODO Update

Browse source
This commit is contained in:
Guillaume Bury 2014-11-13 00:13:12 +01:00
parent 55c5c3f0f0
commit 6dc90d5f3f
1 changed files with 0 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
TODO.md
View file

@ -2,13 +2,6 @@
## Main goals ## Main goals
- Modify theories to allow passing bulk of assumed literals
* Create shared "vector" (formulas/atoms ?)
* Allow theory propagation
- Cleanup code
* Simplify Solver.Make functor
- Add proof output for smt/theories
* Each theory brings its own proof output (tautologies), somehow
- Allow to plug one's code into boolean propagation - Allow to plug one's code into boolean propagation
* react upon propagation (possibly by propagating more, or side-effect) * react upon propagation (possibly by propagating more, or side-effect)
* more advanced/specific propagation (2-clauses)? * more advanced/specific propagation (2-clauses)?