diff options
Diffstat (limited to 'src/theory/quantifiers/quant_util.h')
-rw-r--r-- | src/theory/quantifiers/quant_util.h | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 6a5726cc7..d248a8999 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -28,6 +28,17 @@ 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 ); +}; + + class QuantRelevance { private: |