diff options
author | Tim King <taking@cs.nyu.edu> | 2013-04-26 17:10:21 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-26 17:10:21 -0400 |
commit | 9098391fe334d829ec4101f190b8f1fa21c30752 (patch) | |
tree | b134fc1fe1c767a50013e1449330ca6a7ee18a3d /src/theory/arith/callbacks.cpp | |
parent | a9174ce4dc3939bbe14c9aa1fd11c79c7877eb16 (diff) |
FCSimplex branch merge
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 */ |