summaryrefslogtreecommitdiff
path: root/contrib/alttheoryskel/theory_DIR.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/alttheoryskel/theory_DIR.cpp')
-rw-r--r--contrib/alttheoryskel/theory_DIR.cpp42
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback