vc.h

/* TODO provide way of querying whether you fall into a fragment /
 * returning what fragment you're in */

decision_engine.h

  // TODO: design decision: decision engine should be notified of
  // propagated lits, and also why(?) (so that it can make decisions
  // based on the utility of various theories and various theory
  // literals).  How?  Maybe TheoryEngine has a backdoor into
  // DecisionEngine "behind the back" of the PropEngine?

result.h

// TODO: perhaps best to templatize Result on its Kind (SAT/Validity),
// but this requires doing the same for Prover and needs discussion.

// TODO: subclass to provide models, etc.  This is really just
// intended as a three-valued response code.

expr_builder.h

  // TODO: store some flags here and install into attribute map when
  // 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
// hood): use a type parameter and have check() delegate, or subclass
// Prover and override check()?
//
// Probably better than that is to have a configuration object that
// indicates which passes are desired.  The configuration occurs
// elsewhere (and can even occur at runtime).  A simple "pass manager"
// of sorts determines check()'s behavior.
//
// The CNF conversion can go on in PropEngine.

prover.h

  /** (preprocessing)
   * Pre-process an Expr.  This is expected to be highly-variable,
   * with a lot of "source-level configurability" to add multiple
   * passes over the Expr.  TODO: may need to specify a LEVEL of
   * preprocessing (certain contexts need more/less ?).
   */

theory.h

  // TODO: these use the current EM (but must be renamed)

  // TODO design decision: 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;

  could provide a continuation (essentially) to propagate literals.
  argument Propagator prop
  class Propagator {
    PropEngine d_pe;
  public:
    // may not return due to a longjmp (?) or perhaps an exception
    // returns next continuation
    Propagator operator()(Literal l);
  };


==========================
TODO:  add throw() specifications