diff options
Diffstat (limited to 'DESIGN_QUESTIONS')
-rw-r--r-- | DESIGN_QUESTIONS | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/DESIGN_QUESTIONS b/DESIGN_QUESTIONS index 12704c6bf..670089c34 100644 --- a/DESIGN_QUESTIONS +++ b/DESIGN_QUESTIONS @@ -25,6 +25,13 @@ expr_builder.h // the expr is created? (we'd have to do that since we don't know // it's hash code yet) +expr_builder.h + + /* TODO design: these modify ExprBuilder */ + ExprBuilder& operator!() { return notExpr(); } + ExprBuilder& operator&&(const Expr& right) { return andExpr(right); } + ExprBuilder& operator||(const Expr& right) { return orExpr(right); } + prover.h // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the @@ -47,3 +54,15 @@ prover.h * preprocessing (certain contexts need more/less ?). */ +theory.h + + // TODO: these use the current EM (but must be renamed) + + // TODO design decisoin: instead of returning a set of literals + // here, perhaps we have an interface back into the prop engine + // where we assert directly. we might sometimes unknowingly assert + // something clearly inconsistent (esp. in a parallel context). + // This would allow the PropEngine to cancel our further work since + // we're already inconsistent---also could strategize dynamically on + // whether enough theory prop work has occurred. + virtual void propagate(Effort level = FULL_EFFORT) = 0; |