From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 19 Feb 2020 07:23:43 +0000 (-0600)
Subject: Fix approximate bounds for transcendental functions whose model values rewrite (... 
X-Git-Tag: cvc5-1.0.0~3635
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8fe04676488e7ff4fbe149f98b1ad62f2bdfee1d;p=cvc5.git

Fix approximate bounds for transcendental functions whose model values rewrite (#3747)

* Fix bounds for negative sine apps

* Format

* Comment

Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
---

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 1c8b9611f..6c04268db 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -793,15 +793,40 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
       bool success = true;
       // tf is Figure 3 : tf( x )
       Node atf = d_model.computeConcreteModelValue(tf);
+      Trace("nl-ext-cm-debug")
+          << "Value for is " << tf << " is " << atf << std::endl;
+      Node bl;
+      Node bu;
       if (k == PI)
       {
-        success = d_model.addCheckModelBound(atf, d_pi_bound[0], d_pi_bound[1]);
+        bl = d_pi_bound[0];
+        bu = d_pi_bound[1];
       }
       else if (d_model.isRefineableTfFun(tf))
       {
         d_model.setUsedApproximate();
         std::pair<Node, Node> bounds = getTfModelBounds(tf, d_taylor_degree);
-        success = d_model.addCheckModelBound(atf, bounds.first, bounds.second);
+        bl = bounds.first;
+        bu = bounds.second;
+      }
+      if (!bl.isNull() && !bu.isNull())
+      {
+        // We have rewritten an application of a transcendental function
+        // based on the current model values.It could be that the model value
+        // rewrites sin(x) ---> sin(-c) ---> -sin(c), thus we need
+        // to negate the bounds in this case.
+        if (atf.getKind() != tf.getKind())
+        {
+          if (atf.getKind() == MULT && atf.getNumChildren() == 2
+              && atf[0] == d_neg_one)
+          {
+            atf = atf[1];
+            Node btmp = bl;
+            bl = ArithMSum::negate(bu);
+            bu = ArithMSum::negate(btmp);
+          }
+        }
+        success = d_model.addCheckModelBound(atf, bl, bu);
       }
       if (!success)
       {