FCSimplex branch merge

1 files changed, 92 insertions, 0 deletions

diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
new file mode 100644
index 000000000..0d754d159
--- /dev/null
+++ b/src/theory/arith/callbacks.h
@@ -0,0 +1,92 @@
+
+#pragma once
+
+#include "expr/node.h"
+#include "util/rational.h"
+#include "context/cdlist.h"
+
+#include "theory/arith/theory_arith_private_forward.h"
+#include "theory/arith/arithvar.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+/**
+ * ArithVarCallBack provides a mechanism for agreeing on callbacks while
+ * breaking mutual recursion inclusion order problems.
+ */
+class ArithVarCallBack {
+public:
+  virtual void operator()(ArithVar x) = 0;
+};
+
+/**
+ * Requests arithmetic variables for internal use,
+ * and releases arithmetic variables that are no longer being used.
+ */
+class ArithVarMalloc {
+public:
+  virtual ArithVar request() = 0;
+  virtual void release(ArithVar v) = 0;
+};
+
+class TNodeCallBack {
+public:
+  virtual void operator()(TNode n) = 0;
+};
+
+class NodeCallBack {
+public:
+  virtual void operator()(Node n) = 0;
+};
+
+class RationalCallBack {
+public:
+  virtual Rational operator()() const = 0;
+};
+
+class SetupLiteralCallBack : public TNodeCallBack {
+private:
+  TheoryArithPrivate& d_arith;
+public:
+  SetupLiteralCallBack(TheoryArithPrivate& ta) : d_arith(ta){}
+  void operator()(TNode lit);
+};
+
+class DeltaComputeCallback : public RationalCallBack {
+private:
+  const TheoryArithPrivate& d_ta;
+public:
+  DeltaComputeCallback(const TheoryArithPrivate& ta) : d_ta(ta){}
+  Rational operator()() const;
+};
+
+class BasicVarModelUpdateCallBack : public ArithVarCallBack{
+private:
+  TheoryArithPrivate& d_ta;
+public:
+  BasicVarModelUpdateCallBack(TheoryArithPrivate& ta) : d_ta(ta) {}
+  void operator()(ArithVar x);
+};
+
+class TempVarMalloc : public ArithVarMalloc {
+private:
+  TheoryArithPrivate& d_ta;
+public:
+  TempVarMalloc(TheoryArithPrivate& ta) : d_ta(ta) {}
+  ArithVar request();
+  void release(ArithVar v);
+};
+
+class RaiseConflict : public NodeCallBack {
+private:
+  TheoryArithPrivate& d_ta;
+public:
+  RaiseConflict(TheoryArithPrivate& ta) : d_ta(ta) {}
+  void operator()(Node n);
+};
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */