diff options
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; |