diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-04 09:19:46 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-04 09:19:46 +0100 |
| commit | 03541f4faeb820539ac25f06f1e64adc7aedca6f (patch) | |
| tree | 19e09a23a205d1598b8cba8682aadac8a1b0edee /src/theory/quantifiers/quant_util.h | |
| parent | 3df24b6e0480799e8f400d15778ed5d3fb2ba7ae (diff) | |
Start work on simplifying single inv solutions. Minor.
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 1b053cf6a..7c1ca2444 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -39,6 +39,7 @@ public: static Node negate( Node t ); static Node offset( Node t, int i ); static void debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c ); + static bool solveEqualityFor( Node lit, Node v, Node & veq ); }; |