diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-31 19:06:55 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-31 17:06:55 -0700 |
| commit | 4be329c881c510caab5995b5ecbe3ae9961b3eed (patch) | |
| tree | 861c99dcdabf8bd225e927ce68341d6cc440e5af /src/theory/quantifiers_engine.cpp | |
| parent | 0522ca5e33f1262c2659aa3afc646ccfae577ffe (diff) | |
Reduce before preregister. (#2025)
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 944010ab1..f8053f2b3 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -788,6 +788,12 @@ void QuantifiersEngine::preRegisterQuantifier(Node q) } Trace("quant-debug") << "QuantifiersEngine : Pre-register " << q << std::endl; d_quants_prereg.insert(q); + // try to reduce + if (reduceQuantifier(q)) + { + // if we can reduce it, nothing left to do + return; + } // ensure that it is registered registerQuantifierInternal(q); // register with each module |