AlexanderKnueppel / AlexanderKnueppel/Skeditor
Rework of the ContractPropagator
Aperta
- Lingua principale
- Java
- Stelle
- 1
- Fork
- 5
- Metriche di merge delle PR
- Nessuna PR unita negli ultimi 30g
Descrizione
The current propagator is an ad-hoc solution that lacks a rigor foundation (cf. package ```de.tubs.skeditor.contracting```). That is, manipulating the formulas (e.g., updating, creating the cnf, or just minimizing) poses a real challenge at this stage.
# Envisioned solution
Treat conditions as SMT-formulas with arithmetic and add Z3 by Microsoft as the back-end solver. This would also enable checking formulas for contradictions etc.
Guida per i contributori
Nessuna guida per i contributori indicizzata per questo repository
Valutazione
Questa issue non è ancora stata valutata.