// get the presubstitution
Trace("nl-ext-cm-debug") << " apply pre-substitution..." << std::endl;
std::vector<Node> passertions = assertions;
-
- // preprocess the assertions with the trancendental solver
- if (!d_trSlv.preprocessAssertionsCheckModel(passertions))
+ if (options::nlExt())
{
- return false;
+ // preprocess the assertions with the trancendental solver
+ if (!d_trSlv.preprocessAssertionsCheckModel(passertions))
+ {
+ return false;
+ }
}
Trace("nl-ext-cm") << "-----" << std::endl;
unsigned tdegree = d_trSlv.getTaylorDegree();
- bool ret =
- d_model.checkModel(passertions, false_asserts, tdegree, lemmas, gs);
+ bool ret = d_model.checkModel(passertions, tdegree, lemmas, gs);
return ret;
}
std::vector<NlLemma>& lems,
std::vector<NlLemma>& wlems)
{
- // initialize the non-linear solver
- d_nlSlv.initLastCall(assertions, false_asserts, xts);
- // initialize the trancendental function solver
std::vector<NlLemma> lemmas;
- d_trSlv.initLastCall(assertions, false_asserts, xts, lemmas);
-
- // process lemmas that may have been generated by the transcendental solver
- filterLemmas(lemmas, lems);
+ if (options::nlExt())
+ {
+ // initialize the non-linear solver
+ d_nlSlv.initLastCall(assertions, false_asserts, xts);
+ // initialize the trancendental function solver
+ d_trSlv.initLastCall(assertions, false_asserts, xts, lemmas);
+ // process lemmas that may have been generated by the transcendental solver
+ filterLemmas(lemmas, lems);
+ }
if (!lems.empty())
{
Trace("nl-ext") << " ...finished with " << lems.size()
}
//----------------------------------- possibly split on zero
- if (options::nlExtSplitZero())
+ if (options::nlExt() && options::nlExtSplitZero())
{
Trace("nl-ext") << "Get zero split lemmas..." << std::endl;
lemmas = d_nlSlv.checkSplitZero();
}
//-----------------------------------initial lemmas for transcendental
- //functions
- lemmas = d_trSlv.checkTranscendentalInitialRefine();
- filterLemmas(lemmas, lems);
- if (!lems.empty())
- {
- Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas."
- << std::endl;
- return lems.size();
- }
-
- //-----------------------------------lemmas based on sign (comparison to zero)
- lemmas = d_nlSlv.checkMonomialSign();
- filterLemmas(lemmas, lems);
- if (!lems.empty())
- {
- Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas."
- << std::endl;
- return lems.size();
- }
-
- //-----------------------------------monotonicity of transdental functions
- lemmas = d_trSlv.checkTranscendentalMonotonic();
- filterLemmas(lemmas, lems);
- if (!lems.empty())
- {
- Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas."
- << std::endl;
- return lems.size();
- }
-
- //-----------------------------------lemmas based on magnitude of non-zero
- //monomials
- for (unsigned c = 0; c < 3; c++)
+ if (options::nlExt())
{
- // c is effort level
- lemmas = d_nlSlv.checkMonomialMagnitude(c);
- unsigned nlem = lemmas.size();
+ // functions
+ lemmas = d_trSlv.checkTranscendentalInitialRefine();
filterLemmas(lemmas, lems);
if (!lems.empty())
{
- Trace("nl-ext") << " ...finished with " << lems.size()
- << " new lemmas (out of possible " << nlem << ")."
+ Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas."
<< std::endl;
return lems.size();
}
}
- //-----------------------------------inferred bounds lemmas
- // e.g. x >= t => y*x >= y*t
- std::vector<NlLemma> nt_lemmas;
- lemmas =
- d_nlSlv.checkMonomialInferBounds(nt_lemmas, assertions, false_asserts);
- // Trace("nl-ext") << "Bound lemmas : " << lemmas.size() << ", " <<
- // nt_lemmas.size() << std::endl; prioritize lemmas that do not
- // introduce new monomials
- filterLemmas(lemmas, lems);
-
- if (options::nlExtTangentPlanes() && options::nlExtTangentPlanesInterleave())
+ // main calls to nlExt
+ if (options::nlExt())
{
- lemmas = d_nlSlv.checkTangentPlanes();
+ //---------------------------------lemmas based on sign (comparison to zero)
+ lemmas = d_nlSlv.checkMonomialSign();
filterLemmas(lemmas, lems);
- }
-
- if (!lems.empty())
- {
- Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas."
- << std::endl;
- return lems.size();
- }
-
- // 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();
- }
+ if (!lems.empty())
+ {
+ Trace("nl-ext") << " ...finished with " << lems.size() << " new 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);
+ //-----------------------------------monotonicity of transdental functions
+ lemmas = d_trSlv.checkTranscendentalMonotonic();
filterLemmas(lemmas, lems);
if (!lems.empty())
{
<< 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();
+ //------------------------lemmas based on magnitude of non-zero monomials
+ for (unsigned c = 0; c < 3; c++)
+ {
+ // c is effort level
+ lemmas = d_nlSlv.checkMonomialMagnitude(c);
+ unsigned nlem = lemmas.size();
+ filterLemmas(lemmas, lems);
+ if (!lems.empty())
+ {
+ Trace("nl-ext") << " ...finished with " << lems.size()
+ << " new lemmas (out of possible " << nlem << ")."
+ << std::endl;
+ return lems.size();
+ }
+ }
+
+ //-----------------------------------inferred bounds lemmas
+ // e.g. x >= t => y*x >= y*t
+ std::vector<NlLemma> nt_lemmas;
+ lemmas =
+ d_nlSlv.checkMonomialInferBounds(nt_lemmas, assertions, false_asserts);
+ // Trace("nl-ext") << "Bound lemmas : " << lemmas.size() << ", " <<
+ // nt_lemmas.size() << std::endl; prioritize lemmas that do not
+ // introduce new monomials
filterLemmas(lemmas, lems);
+
+ if (options::nlExtTangentPlanes()
+ && options::nlExtTangentPlanesInterleave())
+ {
+ lemmas = d_nlSlv.checkTangentPlanes();
+ 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);
+ // 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);
+ }
}
+
Trace("nl-ext") << " ...finished with " << wlems.size() << " waiting lemmas."
<< std::endl;
}
// we are incomplete
- if (options::nlExtIncPrecision() && d_model.usedApproximate())
+ if (options::nlExt() && options::nlExtIncPrecision()
+ && d_model.usedApproximate())
{
d_trSlv.incrementTaylorDegree();
needsRecheck = true;
projects / cvc5.git / blobdiff