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 4b49c756ed3245522a2f2ee50adc69922eab5a8d..18f30344a60189c449c09fc904692a18b9b0d7af 100644 (file)
--- 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 48c602a62068eab842686d2ab3b8e942ed7a6d49..d5cfc935e5435ae0e0687690d43c713310578c25 100644 (file)
--- 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 (file)
index 0000000..aaaeaef
--- /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 5d242cee6d3d34005b3b2f84f7d1caceff3ce2c5..7dd576ef909d9a9f9b9ad1fdc3996e82b589dc6e 100644 (file)
--- 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))