contrib/alttheoryskel/theory_DIR.cpp

   1 #include "theory/$dir/theory_$dir.h"
   2
   3 using namespace std;
   4
   5 namespace CVC4 {
   6 namespace theory {
   7 namespace $dir {
   8
   9 /** Constructs a new instance of Theory$camel w.r.t. the provided contexts. */
  10 Theory$camel::Theory$camel(context::Context* c,
  11                            context::UserContext* u,
  12                            OutputChannel& out,
  13                            Valuation valuation,
  14                            const LogicInfo& logicInfo) :
  15     Theory(THEORY_$alt_id, c, u, out, valuation, logicInfo) {
  16 }/* Theory$camel::Theory$camel() */
  17
  18 void Theory$camel::check(Effort level) {
  19   if (done() && !fullEffort(level)) {
  20     return;
  21   }
  22
  23   TimerStat::CodeTimer checkTimer(d_checkTime);
  24
  25   while(!done()) {
  26     // Get all the assertions
  27     Assertion assertion = get();
  28     TNode fact = assertion.assertion;
  29
  30     Debug("$dir") << "Theory$camel::check(): processing " << fact << std::endl;
  31
  32     // Do the work
  33     switch(fact.getKind()) {
  34
  35     /* cases for all the theory's kinds go here... */
  36
  37     default:
  38       Unhandled(fact.getKind());
  39     }
  40   }
  41
  42 }/* Theory$camel::check() */
  43
  44 }/* CVC4::theory::$dir namespace */
  45 }/* CVC4::theory namespace */
  46 }/* CVC4 namespace */