additional headers and modifications; now passes syntax check

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;