diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-26 19:26:21 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-26 19:26:21 +0200 |
commit | f07e8a3f06feb789692ede8ad9d25a2e049af769 (patch) | |
tree | bdeb79262056c70c6b5125ed11a392a4fa1864f7 /src/theory/quantifiers/fun_def_process.h | |
parent | 349deb0522c4602b740d96f6a688b644dd84c64f (diff) |
Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullModel=false assigns values to eqc. Bug fix for fmf-fun. Minor change to resource limiting for quantifiers. Add fmf regressions.
Diffstat (limited to 'src/theory/quantifiers/fun_def_process.h')
-rw-r--r-- | src/theory/quantifiers/fun_def_process.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h index 63aa1bf94..54735d4d6 100644 --- a/src/theory/quantifiers/fun_def_process.h +++ b/src/theory/quantifiers/fun_def_process.h @@ -36,7 +36,7 @@ private: //defined functions to injections input -> argument elements std::map< Node, std::vector< Node > > d_input_arg_inj; //simplify - Node simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, int is_fun_def = 0 ); + Node simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, int is_fun_def = 0 ); //simplify term void simplifyTerm( Node n, std::vector< Node >& constraints ); public: |