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.h | |
parent | a9174ce4dc3939bbe14c9aa1fd11c79c7877eb16 (diff) |
FCSimplex branch merge
Diffstat (limited to 'src/theory/arith/callbacks.h')
-rw-r--r-- | src/theory/arith/callbacks.h | 92 |
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 */ |