diff options
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 9f43c1d35..fa27f0160 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -672,7 +672,8 @@ private: std::map< Node, std::map< Node, unsigned > > d_node_mv_args_proc; public: void registerEvalTerm( Node n ); - void registerModelValue( Node n, Node v, std::vector< Node >& lems ); + 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 ); }; }/* CVC4::theory::quantifiers namespace */ |