diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-02 17:42:31 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-02 17:42:31 +0100 |
| commit | 8deb9d980d7b0e281a0190539b756896a487c451 (patch) | |
| tree | ce0bfe29b53cc16c8854fa6833f2dda3b9122c6f /src/theory/quantifiers/quant_util.h | |
| parent | 6d37c136a251b957197269aeb389a9f1ae07e620 (diff) | |
Single invocation module for counterexample guided quantifier instantiation --cegqi-si. Minor improvements to syntax-guided case, refactoring. Do not apply exhaustive tester inference for sygus datatypes.
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 d7e220b2e..1b053cf6a 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -38,6 +38,7 @@ public: 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 ); + static void debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c ); }; |