diff options
Diffstat (limited to 'src/theory/arith/callbacks.cpp')
-rw-r--r-- | src/theory/arith/callbacks.cpp | 37 |
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 */ |