diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-01 13:09:49 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-01 13:11:13 +0200 |
| commit | 3ac872f4a3f65bd1b38c1362b8ca9d351ed89333 (patch) | |
| tree | c62a424af1b419155af0f59612d376fc10e7a6b6 /src/theory/quantifiers/fun_def_process.h | |
| parent | 9350915de95c1b569eea8262c4602708dfa6c3fa (diff) | |
Improvements and bug fixes related to cbqi/cegqi. Minor fix for fmf with fun-def. Add skolemization options.
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 40364eeb7..63aa1bf94 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, bool is_fun_def = false ); + Node simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, int is_fun_def = 0 ); //simplify term void simplifyTerm( Node n, std::vector< Node >& constraints ); public: |