diff options
Diffstat (limited to 'contrib/alttheoryskel/theory_DIR.cpp')
-rw-r--r-- | contrib/alttheoryskel/theory_DIR.cpp | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/contrib/alttheoryskel/theory_DIR.cpp b/contrib/alttheoryskel/theory_DIR.cpp new file mode 100644 index 000000000..eca07e909 --- /dev/null +++ b/contrib/alttheoryskel/theory_DIR.cpp @@ -0,0 +1,42 @@ +#include "theory/$dir/theory_$dir.h" + +using namespace std; + +namespace CVC4 { +namespace theory { +namespace $dir { + +/** Constructs a new instance of Theory$camel w.r.t. the provided contexts. */ +Theory$camel::Theory$camel(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + QuantifiersEngine* qe) : + Theory(THEORY_$alt_id, c, u, out, valuation, logicInfo, qe) { +}/* Theory$camel::Theory$camel() */ + +void Theory$camel::check(Effort level) { + + while(!done()) { + // Get all the assertions + Assertion assertion = get(); + TNode fact = assertion.assertion; + + Debug("$dir") << "Theory$camel::check(): processing " << fact << std::endl; + + // Do the work + switch(fact.getKind()) { + + /* cases for all the theory's kinds go here... */ + + default: + Unhandled(fact.getKind()); + } + } + +}/* Theory$camel::check() */ + +}/* CVC4::theory::$dir namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ |