From 3f09cf86d8a0129c12afc6ee63445c2a714ce5f6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 11 Mar 2022 11:40:16 -0600 Subject: [PATCH] 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. --- src/theory/arith/operator_elim.cpp | 18 ++++++++++++++++++ test/regress/CMakeLists.txt | 1 + .../nl/nta/proj-issue483-arccos-oob.smt2 | 6 ++++++ test/regress/regress1/nl/sugar-ident.smt2 | 4 ++-- 4 files changed, 27 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/nl/nta/proj-issue483-arccos-oob.smt2 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)) -- 2.30.2