diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-28 17:09:01 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-28 17:09:01 -0500 |
commit | 6a2148c3cfb20928b2e721726345ea96149154d9 (patch) | |
tree | 70ea52d5edbf00ae495738f853df459a5efe7303 /src/theory/quantifiers/fun_def_process.h | |
parent | 2978e5fa3434b80d3ca440ec482d5fe07bf5d368 (diff) |
Fix for get constraints method in fmf-fun (#2399)
Diffstat (limited to 'src/theory/quantifiers/fun_def_process.h')
-rw-r--r-- | src/theory/quantifiers/fun_def_process.h | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h index b59c6199a..78adc710c 100644 --- a/src/theory/quantifiers/fun_def_process.h +++ b/src/theory/quantifiers/fun_def_process.h @@ -49,11 +49,6 @@ private: Node simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, bool is_fun_def, std::map< int, std::map< Node, Node > >& visited, std::map< int, std::map< Node, Node > >& visited_cons ); - /** simplify term - * This computes constraints for the final else branch of A_0 in Figure 1 - * of Reynolds et al "Model Finding for Recursive Functions". - */ - void simplifyTerm( Node n, std::vector< Node >& constraints, std::map< Node, bool >& visited ); public: FunDefFmf(){} ~FunDefFmf(){} @@ -70,6 +65,15 @@ public: * which are Sigma^{dfn} in that paper. */ void simplify( std::vector< Node >& assertions ); + /** get constraints + * + * This computes constraints for the final else branch of A_0 in Figure 1 + * of Reynolds et al "Model Finding for Recursive Functions". The range of + * the cache visited stores the constraint (if any) for each node. + */ + void getConstraints(Node n, + std::vector<Node>& constraints, + std::map<Node, Node>& visited); }; |