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.

diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index 40de74d0a74eb31af5022511ffa6ef57ea583694..fe7b673a666ca0ea977b4b10209ace4150078f38 100644 (file)
--- 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<Node>{
@@ -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 53a8dbb39309571441bdd6d278bb10fd938f5ae9..67deaccaf1379ee08dc267e71ed0cb6f5b13c8f9 100644 (file)
--- 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 (file)
index 0000000..043f408
--- /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)