diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-06 09:35:49 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-06 09:35:59 +0100 |
| commit | 363e4c378f0bc9598a93c80bce9ecaebca2efdd1 (patch) | |
| tree | e40a637326719738866bfbb790aa704a3522a2c1 /src/theory/quantifiers/quant_util.h | |
| parent | fca6fd532abda44c4da48d5c167b77600690e221 (diff) | |
Handle missing cases for single inv solution reconstruction. Minor fixes. Refactor.
Diffstat (limited to 'src/theory/quantifiers/quant_util.h')
| -rw-r--r-- | src/theory/quantifiers/quant_util.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 7c1ca2444..f0dfb1ed6 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -32,6 +32,7 @@ class QuantifiersEngine; class QuantArith { public: + static bool getMonomial( Node n, Node& c, Node& v ); 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 ); |