Merging the unate-propagator branch into the trunk. This is a big update so expect a little turbulence. This commit will not compile. There will be a second commit that fixes this in a moment. I am delaying a change to avoid svn whining about a conflict.

1 files changed, 81 insertions, 0 deletions

diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
new file mode 100644
index 000000000..dc08788f3
--- /dev/null
+++ b/src/theory/theory_test_utils.h
@@ -0,0 +1,81 @@
+
+
+#include "cvc4_public.h"
+
+
+#ifndef __CVC4__THEORY__THEORY_TEST_UTILS_H
+#define __CVC4__THEORY__ITHEORY_TEST_UTILS_H
+
+#include "util/Assert.h"
+#include "expr/node.h"
+#include "theory/output_channel.h"
+#include "theory/interrupted.h"
+
+#include <vector>
+
+namespace CVC4{
+
+namespace theory {
+
+/**
+ * Very basic OutputChannel for testing simple Theory Behaviour.
+ * Stores a call sequence for the output channel
+ */
+enum OutputChannelCallType { CONFLICT, PROPOGATE, AUG_LEMMA, LEMMA, EXPLANATION };
+
+
+class TestOutputChannel : public theory::OutputChannel {
+public:
+  std::vector< pair<enum OutputChannelCallType, Node> > d_callHistory;
+
+  TestOutputChannel() {}
+
+  ~TestOutputChannel() {}
+
+  void safePoint()  throw(Interrupted, AssertionException) {}
+
+  void conflict(TNode n, bool safe = false)  throw(Interrupted, AssertionException) {
+    push(CONFLICT, n);
+  }
+
+  void propagate(TNode n, bool safe = false)  throw(Interrupted, AssertionException) {
+    push(PROPOGATE, n);
+  }
+
+  void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) {
+    push(LEMMA, n);
+  }
+  void augmentingLemma(TNode n, bool safe = false) throw(Interrupted, AssertionException){
+    push(AUG_LEMMA, n);
+  }
+  void explanation(TNode n, bool safe = false)  throw(Interrupted, AssertionException) {
+    push(EXPLANATION, n);
+  }
+
+  void clear() {
+    d_callHistory.clear();
+  }
+
+  Node getIthNode(int i) {
+    Node tmp = (d_callHistory[i]).second;
+    return tmp;
+  }
+
+  OutputChannelCallType getIthCallType(int i) {
+    return (d_callHistory[i]).first;
+  }
+
+  unsigned getNumCalls() {
+    return d_callHistory.size();
+  }
+
+private:
+  void push(OutputChannelCallType call, TNode n) {
+    d_callHistory.push_back(make_pair(call,n));
+  }
+};/* class TestOutputChannel */
+
+}/* namespace theory */
+}/* namespace CVC4 */
+
+#endif /* __CVC4__THEORY__THEORY_TEST_UTILS_H */