From: yoni206 <yoni206@users.noreply.github.com>
Date: Fri, 25 Jun 2021 03:09:06 +0000 (-0700)
Subject: pow2: Adding monotonicity lemma  (#6793)
X-Git-Tag: cvc5-1.0.0~1555
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=abd18eeb854047e13e38518c536afd16a1be448d;p=cvc5.git

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.
---

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
diff --git a/src/theory/arith/nl/pow2_solver.h b/src/theory/arith/nl/pow2_solver.h
index 4796b2147..4c6fb8014 100644
--- a/src/theory/arith/nl/pow2_solver.h
+++ b/src/theory/arith/nl/pow2_solver.h
@@ -74,6 +74,9 @@ class Pow2Solver
    */
   void checkFullRefine();
 
+  /** sort d_pow2 according to their values in the current model */
+  void sortPow2sBasedOnModel();
+
   //-------------------------------------------- end lemma schemas
  private:
   // The inference manager that we push conflicts and lemmas to.
@@ -88,8 +91,8 @@ class Pow2Solver
   Node d_two;
 
   NodeSet d_initRefine;
-  /** all pow2 terms 
-   * Cleared at each last call effort check. 
+  /** all pow2 terms
+   * Cleared at each last call effort check.
    * */
   std::vector<Node> d_pow2s;
 
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 6a87776d6..2216d8fed 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -131,6 +131,8 @@ enum class InferenceId
   ARITH_NL_POW2_INIT_REFINE,
   // value refinements (Pow2Solver::checkFullRefine)
   ARITH_NL_POW2_VALUE_REFINE,
+  // monotonicity refinements (Pow2Solver::checkFullRefine)
+  ARITH_NL_POW2_MONOTONE_REFINE,
   //-------------------- nonlinear cad solver
   // conflict / infeasible subset obtained from cad
   ARITH_NL_CAD_CONFLICT,