- //------------------------------------tangent planes
- if (options::nlExtTangentPlanes() && !options::nlExtTangentPlanesInterleave())
- {
- lemmas = d_nlSlv.checkTangentPlanes();
- filterLemmas(lemmas, wlems);
- }
- if (options::nlExtTfTangentPlanes())
- {
- lemmas = d_trSlv.checkTranscendentalTangentPlanes();
- filterLemmas(lemmas, wlems);
+ // from inferred bound inferences : now do ones that introduce new terms
+ filterLemmas(nt_lemmas, lems);
+ if (!lems.empty())
+ {
+ Trace("nl-ext") << " ...finished with " << lems.size()
+ << " new (monomial-introducing) lemmas." << std::endl;
+ return lems.size();
+ }
+
+ //------------------------------------factoring lemmas
+ // x*y + x*z >= t => exists k. k = y + z ^ x*k >= t
+ if (options::nlExtFactor())
+ {
+ lemmas = d_nlSlv.checkFactoring(assertions, false_asserts);
+ filterLemmas(lemmas, lems);
+ if (!lems.empty())
+ {
+ Trace("nl-ext") << " ...finished with " << lems.size()
+ << " new lemmas." << std::endl;
+ return lems.size();
+ }
+ }
+
+ //------------------------------------resolution bound inferences
+ // e.g. ( y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t
+ if (options::nlExtResBound())
+ {
+ lemmas = d_nlSlv.checkMonomialInferResBounds();
+ filterLemmas(lemmas, lems);
+ if (!lems.empty())
+ {
+ Trace("nl-ext") << " ...finished with " << lems.size()
+ << " new lemmas." << std::endl;
+ return lems.size();
+ }
+ }
+
+ //------------------------------------tangent planes
+ if (options::nlExtTangentPlanes()
+ && !options::nlExtTangentPlanesInterleave())
+ {
+ lemmas = d_nlSlv.checkTangentPlanes();
+ filterLemmas(lemmas, wlems);
+ }
+ if (options::nlExtTfTangentPlanes())
+ {
+ lemmas = d_trSlv.checkTranscendentalTangentPlanes();
+ filterLemmas(lemmas, wlems);
+ }