AlexanderKnueppel / AlexanderKnueppel/Skeditor
Rework of the ContractPropagator
未關閉
- 主要語言
- Java
- 星號
- 1
- 分支
- 5
- PR 合併指標
- 30 天內沒有已合併 PR
描述
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.
貢獻指南
這個儲存庫沒有索引到貢獻指南
評估
這個 Issue 還沒有評估資料。