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