diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-05 09:56:00 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-05 09:56:00 -0500 |
| commit | abb71e0d55b23fcd28872866b64ffe64f76d1ee6 (patch) | |
| tree | 5a4da709b0dadc931ff73bdf6bb389f6c01967ee /src/theory/quantifiers/fun_def_process.h | |
| parent | c77213eaf165746a3704204ce56915b86c5f2a7a (diff) | |
Caching for fun def process, add regression.
Diffstat (limited to 'src/theory/quantifiers/fun_def_process.h')
| -rw-r--r-- | src/theory/quantifiers/fun_def_process.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h index 1f6ee6562..28a1f3cfa 100644 --- a/src/theory/quantifiers/fun_def_process.h +++ b/src/theory/quantifiers/fun_def_process.h @@ -32,9 +32,11 @@ namespace quantifiers { class FunDefFmf { private: //simplify - Node simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, int is_fun_def = 0 ); + Node simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, int is_fun_def, + std::map< int, std::map< Node, Node > >& visited, + std::map< int, std::map< Node, Node > >& visited_cons ); //simplify term - void simplifyTerm( Node n, std::vector< Node >& constraints ); + void simplifyTerm( Node n, std::vector< Node >& constraints, std::map< Node, bool >& visited ); public: FunDefFmf(){} ~FunDefFmf(){} |