diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-01 23:20:09 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-01 23:20:09 -0500 |
| commit | 3f2c2c745ae2f13441c1cabd363e6539c9bdaeb9 (patch) | |
| tree | b5c785e9a5e16d430f45b2a40f78e40247111233 /src/theory/quantifiers/term_database_sygus.h | |
| parent | 4b580ea3876055f701b13e67e0e4e78abbe47674 (diff) | |
(Move-only) Split quant util (#1306)
* Initial draft of splitting quant util.
* Minor
* Document recursive term builder.
* Rename file, minor.
* Clang format
Diffstat (limited to 'src/theory/quantifiers/term_database_sygus.h')
| -rw-r--r-- | src/theory/quantifiers/term_database_sygus.h | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h index 030963b58..c819bc781 100644 --- a/src/theory/quantifiers/term_database_sygus.h +++ b/src/theory/quantifiers/term_database_sygus.h @@ -17,6 +17,7 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H #define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H +#include "theory/quantifiers/sygus_explain.h" #include "theory/quantifiers/term_database.h" namespace CVC4 { @@ -25,6 +26,7 @@ namespace quantifiers { class CegConjecture; +// TODO (as part of #1235) move to sygus_invariance.h class SygusInvarianceTest { protected: // check whether nvn[ x ] should be excluded @@ -239,7 +241,8 @@ public: // for symmetry breaking int solveForArgument( TypeNode tnp, unsigned cindex, unsigned arg ); //for eager instantiation -private: + // TODO (as part of #1235) move some of these functions to sygus_explain.h + private: std::map< Node, std::map< Node, bool > > d_subterms; std::map< Node, std::vector< Node > > d_evals; std::map< Node, std::vector< std::vector< Node > > > d_eval_args; |