From a4b9a04373f463607a09c71c26f7dbcad37d219c Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 26 May 2022 09:45:13 -0700 Subject: [PATCH] Make sure phase-shift lemma is properly typed (#8824) This PR addresses #8773 by making sure that the phase shift lemmas generated by the sine solver are properly typed. --- src/theory/arith/nl/transcendental/sine_solver.cpp | 6 ++++-- test/regress/cli/CMakeLists.txt | 1 + test/regress/cli/regress0/nl/nta/issue8773-phase-shift.smt2 | 4 ++++ 3 files changed, 9 insertions(+), 2 deletions(-) create mode 100644 test/regress/cli/regress0/nl/nta/issue8773-phase-shift.smt2 diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 40de74d0a..fe7b673a6 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -149,6 +149,8 @@ void SineSolver::doReductions() Node SineSolver::getPhaseShiftLemma(const Node& x, const Node& y, const Node& s) { NodeManager* nm = NodeManager::currentNM(); + Node xr = (x.getType().isInteger() ? nm->mkNode(Kind::TO_REAL, x) : x); + Node yr = (y.getType().isInteger() ? nm->mkNode(Kind::TO_REAL, y) : y); Node mone = nm->mkConstReal(Rational(-1)); Node pi = nm->mkNullaryOperator(nm->realType(), PI); return nm->mkAnd(std::vector{ @@ -160,8 +162,8 @@ Node SineSolver::getPhaseShiftLemma(const Node& x, const Node& y, const Node& s) nm->mkNode(GEQ, x, nm->mkNode(MULT, mone, pi)), nm->mkNode(LEQ, x, pi), }), - x.eqNode(y), - x.eqNode(nm->mkNode( + xr.eqNode(yr), + xr.eqNode(nm->mkNode( ADD, y, nm->mkNode(MULT, nm->mkConstReal(2), s, pi)))), nm->mkNode(SINE, y).eqNode(nm->mkNode(SINE, x))}); } diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 53a8dbb39..67deaccaf 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -846,6 +846,7 @@ set(regress_0_tests regress0/nl/nta/issue8208-red-nred.smt2 regress0/nl/nta/issue8294-2-double-solve.smt2 regress0/nl/nta/issue8415-embed-arg.smt2 + regress0/nl/nta/issue8773-phase-shift.smt2 regress0/nl/nta/pi-simplest.smt2 regress0/nl/nta/proj-issue376.smt2 regress0/nl/nta/proj-issue403.smt2 diff --git a/test/regress/cli/regress0/nl/nta/issue8773-phase-shift.smt2 b/test/regress/cli/regress0/nl/nta/issue8773-phase-shift.smt2 new file mode 100644 index 000000000..043f4086f --- /dev/null +++ b/test/regress/cli/regress0/nl/nta/issue8773-phase-shift.smt2 @@ -0,0 +1,4 @@ +; EXPECT: unsat +(set-logic QF_NRAT) +(assert (= 0.0 (sin 7))) +(check-sat) -- 2.30.2