DESIGN_QUESTIONS

   1 vc.h
   2
   3 /* TODO provide way of querying whether you fall into a fragment /
   4  * returning what fragment you're in */
   5
   6 decision_engine.h
   7
   8   // TODO: design decision: decision engine should be notified of
   9   // propagated lits, and also why(?) (so that it can make decisions
  10   // based on the utility of various theories and various theory
  11   // literals).  How?  Maybe TheoryEngine has a backdoor into
  12   // DecisionEngine "behind the back" of the PropEngine?
  13
  14 result.h
  15
  16 // TODO: perhaps best to templatize Result on its Kind (SAT/Validity),
  17 // but this requires doing the same for Prover and needs discussion.
  18
  19 // TODO: subclass to provide models, etc.  This is really just
  20 // intended as a three-valued response code.
  21
  22 expr_builder.h
  23
  24   // TODO: store some flags here and install into attribute map when
  25   // the expr is created?  (we'd have to do that since we don't know
  26   // it's hash code yet)
  27
  28 prover.h
  29
  30 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
  31 // hood): use a type parameter and have check() delegate, or subclass
  32 // Prover and override check()?
  33 //
  34 // Probably better than that is to have a configuration object that
  35 // indicates which passes are desired.  The configuration occurs
  36 // elsewhere (and can even occur at runtime).  A simple "pass manager"
  37 // of sorts determines check()'s behavior.
  38 //
  39 // The CNF conversion can go on in PropEngine.
  40
  41 prover.h
  42
  43   /** (preprocessing)
  44    * Pre-process an Expr.  This is expected to be highly-variable,
  45    * with a lot of "source-level configurability" to add multiple
  46    * passes over the Expr.  TODO: may need to specify a LEVEL of
  47    * preprocessing (certain contexts need more/less ?).
  48    */
  49