mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-10 05:03:59 -05:00
46 lines
1.3 KiB
Markdown
46 lines
1.3 KiB
Markdown
# Goals
|
||
|
||
## TODO
|
||
|
||
- typing and translation Ast -> Term (from mc2?)
|
||
- main executable for SMT solver
|
||
- theory of boolean constructs (on the fly Tseitin using local clauses)
|
||
- make CC work on QF_UF
|
||
* internalize terms on the fly (backtrackable)
|
||
* basic notion of activity for `ite`?
|
||
- have `CDCL.push_local` work properly
|
||
|
||
- remove tseitin lib
|
||
|
||
- write Shostak theory of datatypes (without acyclicity) with local case splits
|
||
- design evaluation system (guards + `eval_bool:(term -> bool) option` in custom TC)
|
||
- compilation of rec functions to defined constants
|
||
|
||
- Shostak theory of eq-ℚ
|
||
- datatype acyclicity check
|
||
|
||
- abstract domain propagation in CC
|
||
- domain propagation (intervals) for ℚ arith
|
||
- full ℚ theory: shostak + domains + if-sat simplex
|
||
|
||
## Main goals
|
||
|
||
- Add a backend to send proofs to dedukti
|
||
* First, pure resolution proofs
|
||
* Then, require theories to output lemma proofs for dedukti (in some format yet to be decided)
|
||
- Allow to plug one's code into boolean propagation
|
||
* react upon propagation (possibly by propagating more, or side-effect)
|
||
* more advanced/specific propagation (2-clauses)?
|
||
* implement 'constraints' (see https://www.lri.fr/~conchon/TER/2013/3/minisat.pdf )
|
||
|
||
## Long term goals
|
||
|
||
- max-sat/max-smt
|
||
- coq proofs ?
|
||
|
||
|
||
## Done
|
||
|
||
- base types (Term, Lit, …)
|
||
- theory combination
|
||
- basic design of theories
|