diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2021-06-24 20:09:06 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-24 22:09:06 -0500 |
commit | abd18eeb854047e13e38518c536afd16a1be448d (patch) | |
tree | e12f69826feb922dc80f228ecbb78276ee3613a9 /src/theory/arith/nl/pow2_solver.cpp | |
parent | dd31ac04ed448358da613ab97a2a929df8cf8fd5 (diff) |
pow2: Adding monotonicity lemma (#6793)
We add the lemma x<=y --> pow2(x)<=pow2(y) to the pow2 solver.
Additionally, some renaming of variables is introduced for better clarity.
Diffstat (limited to 'src/theory/arith/nl/pow2_solver.cpp')
-rw-r--r-- | src/theory/arith/nl/pow2_solver.cpp | 67 |
1 files changed, 53 insertions, 14 deletions
diff --git a/src/theory/arith/nl/pow2_solver.cpp b/src/theory/arith/nl/pow2_solver.cpp index 9864fc709..41b9e6d72 100644 --- a/src/theory/arith/nl/pow2_solver.cpp +++ b/src/theory/arith/nl/pow2_solver.cpp @@ -86,35 +86,74 @@ void Pow2Solver::checkInitialRefine() } } +void Pow2Solver::sortPow2sBasedOnModel() +{ + struct + { + bool operator()(Node a, Node b, NlModel& model) const + { + return model.computeConcreteModelValue(a[0]) + < model.computeConcreteModelValue(b[0]); + } + } modelSort; + using namespace std::placeholders; + std::sort( + d_pow2s.begin(), d_pow2s.end(), std::bind(modelSort, _1, _2, d_model)); +} + void Pow2Solver::checkFullRefine() { - Trace("pow2-check") << "Pow2Solver::checkFullRefine"; - Trace("pow2-check") << "pow2 terms: " << std::endl; - for (const Node& i : d_pow2s) + Trace("pow2-check") << "Pow2Solver::checkFullRefine" << std::endl; + NodeManager* nm = NodeManager::currentNM(); + sortPow2sBasedOnModel(); + // add lemmas for each pow2 term + for (uint64_t i = 0, size = d_pow2s.size(); i < size; i++) { - Node valPow2x = d_model.computeAbstractModelValue(i); - Node valPow2xC = d_model.computeConcreteModelValue(i); + Node n = d_pow2s[i]; + Node valPow2xAbstract = d_model.computeAbstractModelValue(n); + Node valPow2xConcrete = d_model.computeConcreteModelValue(n); + Node valXConcrete = d_model.computeConcreteModelValue(n[0]); if (Trace.isOn("pow2-check")) { - Node x = i[0]; - Node valX = d_model.computeConcreteModelValue(x); - - Trace("pow2-check") << "* " << i << ", value = " << valPow2x << std::endl; - Trace("pow2-check") << " actual (" << valX << ", " - << ") = " << valPow2xC << std::endl; + Trace("pow2-check") << "* " << i << ", value = " << valPow2xAbstract + << std::endl; + Trace("pow2-check") << " actual (" << valXConcrete << ", " + << ") = " << valPow2xConcrete << std::endl; } - if (valPow2x == valPow2xC) + if (valPow2xAbstract == valPow2xConcrete) { Trace("pow2-check") << "...already correct" << std::endl; continue; } + // add monotinicity lemmas + for (uint64_t j = i + 1; j < size; j++) + { + Node m = d_pow2s[j]; + Node valPow2yConcrete = d_model.computeConcreteModelValue(m); + Node valYConcrete = d_model.computeConcreteModelValue(m[0]); + + Integer x = valXConcrete.getConst<Rational>().getNumerator(); + Integer y = valYConcrete.getConst<Rational>().getNumerator(); + Integer pow2x = valPow2xConcrete.getConst<Rational>().getNumerator(); + Integer pow2y = valPow2yConcrete.getConst<Rational>().getNumerator(); + + if (x <= y && pow2x > pow2y) + { + Node assumption = nm->mkNode(LEQ, n[0], m[0]); + Node conclusion = nm->mkNode(LEQ, n, m); + Node lem = nm->mkNode(IMPLIES, assumption, conclusion); + d_im.addPendingLemma( + lem, InferenceId::ARITH_NL_POW2_MONOTONE_REFINE, nullptr, true); + } + } + // Place holder for additional lemma schemas - // + // End of additional lemma schemas // this is the most naive model-based schema based on model values - Node lem = valueBasedLemma(i); + Node lem = valueBasedLemma(n); Trace("pow2-lemma") << "Pow2Solver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl; // send the value lemma |