diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-26 15:16:15 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-26 15:16:23 +0100 |
| commit | 4f5c9dbbd0125294500cf5788cb131b355979fb6 (patch) | |
| tree | fd07a862b4ad35111d56bdfa84f17f8c44d45e6c /src/theory/quantifiers/quant_util.h | |
| parent | 92e4099d9d2b313a521d2a015e604645e24617f4 (diff) | |
Robust strategy for single invocation LIA synthesis conjectures. Add regressions.
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 f0dfb1ed6..eebf87dc0 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -37,6 +37,7 @@ public: 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 bool isolateEqCoeff( Node v, std::map< Node, Node >& msum, Node & veq ); static Node negate( Node t ); static Node offset( Node t, int i ); static void debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c ); |