diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-03 03:37:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-03 03:37:08 +0000 |
commit | 842e581321bcd9f30c60b9dacc671843ca776fed (patch) | |
tree | 202ddf8dae7e090e06d5aed869337ef9162309cd /DESIGN_QUESTIONS | |
parent | 541379b3d361e255cd664207f8b2e278a5b5e3eb (diff) |
additional headers and modifications; now passes syntax check
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; |