Guard uses of printing approximations for constants (#5247)

Errors with these methods were encountered while working on new techniques for arithmetic preprocessing.

Also, there is obvious inefficiency since approximations for constants are being computed when certain traces are disabled.

diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp
index cbd976b032e5498d8c561e5570e65dca4cdfd6dd..1a5bc356f9e4807fe9bd1473c61399f337c42dcc 100644 (file)
--- a/src/theory/arith/arith_utilities.cpp
+++ b/src/theory/arith/arith_utilities.cpp
@@ -106,7 +106,11 @@ bool isTranscendentalKind(Kind k)
 
 Node getApproximateConstant(Node c, bool isLower, unsigned prec)
 {
-  Assert(c.isConst());
+  if (!c.isConst())
+  {
+    Assert(false) << "getApproximateConstant: non-constant input " << c;
+    return Node::null();
+  }
   Rational cr = c.getConst<Rational>();
 
   unsigned lower = 0;
@@ -178,7 +182,12 @@ Node getApproximateConstant(Node c, bool isLower, unsigned prec)
 
 void printRationalApprox(const char* c, Node cr, unsigned prec)
 {
-  Assert(cr.isConst());
+  if (!cr.isConst())
+  {
+    Assert(false) << "printRationalApprox: non-constant input " << cr;
+    Trace(c) << cr;
+    return;
+  }
   Node ca = getApproximateConstant(cr, true, prec);
   if (ca != cr)
   {

diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index 711173bc8cf7d39a23144dba74085e63309d752d..b27654b2cfe8dfb1eecc61678268af2f0f9818a8 100644 (file)
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -260,10 +260,13 @@ bool NlModel::checkModel(const std::vector<Node>& assertions,
             {
               // set its exact model value in the substitution
               Node curv = computeConcreteModelValue(cur);
-              Trace("nl-ext-cm")
-                  << "check-model-bound : exact : " << cur << " = ";
-              printRationalApprox("nl-ext-cm", curv);
-              Trace("nl-ext-cm") << std::endl;
+              if (Trace.isOn("nl-ext-cm"))
+              {
+                Trace("nl-ext-cm")
+                    << "check-model-bound : exact : " << cur << " = ";
+                printRationalApprox("nl-ext-cm", curv);
+                Trace("nl-ext-cm") << std::endl;
+              }
               bool ret = addCheckModelSubstitution(cur, curv);
               AlwaysAssert(ret);
             }
@@ -591,9 +594,12 @@ bool NlModel::solveEqualitySimple(Node eq,
       if (uvf.isVar() && !hasCheckModelAssignment(uvf))
       {
         Node uvfv = computeConcreteModelValue(uvf);
-        Trace("nl-ext-cm") << "check-model-bound : exact : " << uvf << " = ";
-        printRationalApprox("nl-ext-cm", uvfv);
-        Trace("nl-ext-cm") << std::endl;
+        if (Trace.isOn("nl-ext-cm"))
+        {
+          Trace("nl-ext-cm") << "check-model-bound : exact : " << uvf << " = ";
+          printRationalApprox("nl-ext-cm", uvfv);
+          Trace("nl-ext-cm") << std::endl;
+        }
         bool ret = addCheckModelSubstitution(uvf, uvfv);
         // recurse
         return ret ? solveEqualitySimple(eq, d, lemmas) : false;
@@ -620,9 +626,12 @@ bool NlModel::solveEqualitySimple(Node eq,
       return false;
     }
     Node val = nm->mkConst(-c.getConst<Rational>() / b.getConst<Rational>());
-    Trace("nl-ext-cm") << "check-model-bound : exact : " << var << " = ";
-    printRationalApprox("nl-ext-cm", val);
-    Trace("nl-ext-cm") << std::endl;
+    if (Trace.isOn("nl-ext-cm"))
+    {
+      Trace("nl-ext-cm") << "check-model-bound : exact : " << var << " = ";
+      printRationalApprox("nl-ext-cm", val);
+      Trace("nl-ext-cm") << std::endl;
+    }
     bool ret = addCheckModelSubstitution(var, val);
     if (ret)
     {
@@ -701,31 +710,40 @@ bool NlModel::solveEqualitySimple(Node eq,
                    nm->mkNode(MULT,
                               nm->mkConst(Rational(1) / Rational(2)),
                               nm->mkNode(PLUS, bounds[r][0], bounds[r][1])));
-    Trace("nl-ext-cm-debug") << "Bound option #" << r << " : ";
-    printRationalApprox("nl-ext-cm-debug", bounds[r][0]);
-    Trace("nl-ext-cm-debug") << "...";
-    printRationalApprox("nl-ext-cm-debug", bounds[r][1]);
-    Trace("nl-ext-cm-debug") << std::endl;
+    if (Trace.isOn("nl-ext-cm-debug"))
+    {
+      Trace("nl-ext-cm-debug") << "Bound option #" << r << " : ";
+      printRationalApprox("nl-ext-cm-debug", bounds[r][0]);
+      Trace("nl-ext-cm-debug") << "...";
+      printRationalApprox("nl-ext-cm-debug", bounds[r][1]);
+      Trace("nl-ext-cm-debug") << std::endl;
+    }
     diff = Rewriter::rewrite(diff);
     Assert(diff.isConst());
     diff = nm->mkConst(diff.getConst<Rational>().abs());
     diff_bound[r] = diff;
-    Trace("nl-ext-cm-debug") << "...diff from model value (";
-    printRationalApprox("nl-ext-cm-debug", m_var);
-    Trace("nl-ext-cm-debug") << ") is ";
-    printRationalApprox("nl-ext-cm-debug", diff_bound[r]);
-    Trace("nl-ext-cm-debug") << std::endl;
+    if (Trace.isOn("nl-ext-cm-debug"))
+    {
+      Trace("nl-ext-cm-debug") << "...diff from model value (";
+      printRationalApprox("nl-ext-cm-debug", m_var);
+      Trace("nl-ext-cm-debug") << ") is ";
+      printRationalApprox("nl-ext-cm-debug", diff_bound[r]);
+      Trace("nl-ext-cm-debug") << std::endl;
+    }
   }
   // take the one that var is closer to in the model
   Node cmp = nm->mkNode(GEQ, diff_bound[0], diff_bound[1]);
   cmp = Rewriter::rewrite(cmp);
   Assert(cmp.isConst());
   unsigned r_use_index = cmp == d_true ? 1 : 0;
-  Trace("nl-ext-cm") << "check-model-bound : approximate (sqrt) : ";
-  printRationalApprox("nl-ext-cm", bounds[r_use_index][0]);
-  Trace("nl-ext-cm") << " <= " << var << " <= ";
-  printRationalApprox("nl-ext-cm", bounds[r_use_index][1]);
-  Trace("nl-ext-cm") << std::endl;
+  if (Trace.isOn("nl-ext-cm"))
+  {
+    Trace("nl-ext-cm") << "check-model-bound : approximate (sqrt) : ";
+    printRationalApprox("nl-ext-cm", bounds[r_use_index][0]);
+    Trace("nl-ext-cm") << " <= " << var << " <= ";
+    printRationalApprox("nl-ext-cm", bounds[r_use_index][1]);
+    Trace("nl-ext-cm") << std::endl;
+  }
   bool ret =
       addCheckModelBound(var, bounds[r_use_index][0], bounds[r_use_index][1]);
   if (ret)