diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-28 09:35:43 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-28 09:36:00 -0500 |
| commit | e796efe0adb98dc2572ab57d5dc62b8eb11478c0 (patch) | |
| tree | abc704b16240d785435aa63245705bbe036f8411 /src/theory/quantifiers/term_database.h | |
| parent | f0a621b5cd4478ea9b7263ebe1d162495553e1a9 (diff) | |
More work on sygus. Add regress4 to Makefile.
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index fa27f0160..5b29a72ce 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -673,7 +673,12 @@ private: public: void registerEvalTerm( Node n ); void registerModelValue( Node n, Node v, std::vector< Node >& exps, std::vector< Node >& terms, std::vector< Node >& vals ); - Node unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp ); + Node unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp, bool track_exp = true ); + Node unfold( Node en ){ + std::map< Node, Node > vtm; + std::vector< Node > exp; + return unfold( en, vtm, exp, false ); + } }; }/* CVC4::theory::quantifiers namespace */ |