FCSimplex branch merge

1 files changed, 37 insertions, 0 deletions

diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp
new file mode 100644
index 000000000..6b6170b20
--- /dev/null
+++ b/src/theory/arith/callbacks.cpp
@@ -0,0 +1,37 @@
+#include "theory/arith/callbacks.h"
+#include "theory/arith/theory_arith_private.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+void SetupLiteralCallBack::operator()(TNode lit){
+  TNode atom = (lit.getKind() == kind::NOT) ? lit[0] : lit;
+  if(!d_arith.isSetup(atom)){
+    d_arith.setupAtom(atom);
+  }
+}
+
+Rational DeltaComputeCallback::operator()() const{
+  return d_ta.deltaValueForTotalOrder();
+}
+
+ArithVar TempVarMalloc::request(){
+  Node skolem = mkRealSkolem("tmpVar");
+  return d_ta.requestArithVar(skolem, false);
+}
+void TempVarMalloc::release(ArithVar v){
+  d_ta.releaseArithVar(v);
+}
+
+void BasicVarModelUpdateCallBack::operator()(ArithVar x){
+  d_ta.signal(x);
+}
+
+void RaiseConflict::operator()(Node n){
+  d_ta.raiseConflict(n);
+}
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */