From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 11 Mar 2022 17:40:16 +0000 (-0600)
Subject: Fix reduction for arc trig functions (#8289)
X-Git-Tag: cvc5-1.0.0~281
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3f09cf86d8a0129c12afc6ee63445c2a714ce5f6;p=cvc5.git

Fix reduction for arc trig functions (#8289)

We were not guarding the case where the argument was out of the bounds, e.g. arccos(x) requires -1 <= x <= 1.

Fixes cvc5/cvc5-projects#485.
---

diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
index 4b49c756e..18f30344a 100644
--- a/src/theory/arith/operator_elim.cpp
+++ b/src/theory/arith/operator_elim.cpp
@@ -356,6 +356,20 @@ Node OperatorElim::eliminateOperators(Node node,
                             nm->mkNode(LEQ, nm->mkConstReal(Rational(0)), var),
                             nm->mkNode(LT, var, pi));
         }
+        Node cond;
+        if (k == ARCSINE || k == ARCCOSINE || k == ARCSECANT
+            || k == ARCCOSECANT)
+        {
+          // -1 <= x <= 1
+          cond = nm->mkNode(
+              AND,
+              nm->mkNode(GEQ, node[0], nm->mkConstReal(Rational(-1))),
+              nm->mkNode(LEQ, node[0], nm->mkConstReal(Rational(1))));
+          if (k == ARCSECANT || k == ARCCOSECANT)
+          {
+            cond = cond.notNode();
+          }
+        }
 
         Kind rk =
             k == ARCSINE
@@ -369,6 +383,10 @@ Node OperatorElim::eliminateOperators(Node node,
                                      : (k == ARCSECANT ? SECANT : COTANGENT))));
         Node invTerm = nm->mkNode(rk, var);
         lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0]));
+        if (!cond.isNull())
+        {
+          lem = nm->mkNode(IMPLIES, cond, lem);
+        }
       }
       Assert(!lem.isNull());
       lems.push_back(mkSkolemLemma(lem, var));
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 48c602a62..d5cfc935e 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -810,6 +810,7 @@ set(regress_0_tests
   regress0/nl/nta/proj-issue376.smt2
   regress0/nl/nta/proj-issue403.smt2
   regress0/nl/nta/proj-issue460-pi-value.smt2
+  regress0/nl/nta/proj-issue483-arccos-oob.smt2
   regress0/nl/nta/real-pi.smt2
   regress0/nl/nta/sin-sym.smt2
   regress0/nl/nta/sin-sym-schema.smt2
diff --git a/test/regress/regress0/nl/nta/proj-issue483-arccos-oob.smt2 b/test/regress/regress0/nl/nta/proj-issue483-arccos-oob.smt2
new file mode 100644
index 000000000..aaaeaeff1
--- /dev/null
+++ b/test/regress/regress0/nl/nta/proj-issue483-arccos-oob.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(assert (>= real.pi (arccos real.pi)))
+(check-sat)
diff --git a/test/regress/regress1/nl/sugar-ident.smt2 b/test/regress/regress1/nl/sugar-ident.smt2
index 5d242cee6..7dd576ef9 100644
--- a/test/regress/regress1/nl/sugar-ident.smt2
+++ b/test/regress/regress1/nl/sugar-ident.smt2
@@ -14,8 +14,8 @@
 (declare-fun a5 () Bool)
 (declare-fun a6 () Bool)
 
-(assert (= a1 (not (= (sin (arcsin x1)) x1))))
-(assert (= a3 (< (arccos x3) 0)))
+(assert (= a1 (and (<= (- 1) x1 1) (not (= (sin (arcsin x1)) x1)))))
+(assert (= a3 (and (<= (- 1) x3 1) (< (arccos x3) 0))))
 (assert (= a4 (> (arctan x4) 1.8)))
 
 (assert (or a1 a3 a4))