diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-31 11:35:11 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-31 11:35:19 +0100 |
| commit | 458b2b7eb5bdf09a1a886f4e2a165380d5fd918f (patch) | |
| tree | 342d05bab92d0aa349ab833e6a4b60e887670295 /src/theory/quantifiers/fun_def_process.h | |
| parent | 5a285d5247b56b00895774c909f09c8ad1e3889c (diff) | |
Do not allow duplication of function definitions. Set incomplete flag in model builder.
Diffstat (limited to 'src/theory/quantifiers/fun_def_process.h')
| -rw-r--r-- | src/theory/quantifiers/fun_def_process.h | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h index 22adf427d..40364eeb7 100644 --- a/src/theory/quantifiers/fun_def_process.h +++ b/src/theory/quantifiers/fun_def_process.h @@ -35,8 +35,6 @@ private: std::map< Node, TypeNode > d_sorts; //defined functions to injections input -> argument elements std::map< Node, std::vector< Node > > d_input_arg_inj; - //flatten ITE - void flattenITE( Node lhs, Node n, std::vector< std::vector< Node > >& conds, std::vector< Node >& terms ); //simplify Node simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, bool is_fun_def = false ); //simplify term |