diff options
Diffstat (limited to 'src/theory/quantifiers/quant_util.h')
| -rw-r--r-- | src/theory/quantifiers/quant_util.h | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 6a5726cc7..86c7bc3a0 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -28,6 +28,18 @@ namespace CVC4 { namespace theory { +class QuantArith +{ +public: + static bool getMonomial( Node n, std::map< Node, Node >& msum ); + static bool getMonomialSum( Node n, std::map< Node, Node >& msum ); + static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum ); + static bool isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k ); + static Node negate( Node t ); + static Node offset( Node t, int i ); +}; + + class QuantRelevance { private: |