Fix issue with dropping non-reduced sine terms (#8211)

Fixes #8208.

A spurious "break" was leftover from when this code was a loop, this meant when the first reduced term was encountered, it ignored the remainder.

diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index e765a1599102a5d4079781a6cd61cb5bc7afd7c8..6645589e2c288302d151378e265dbfc0b842f3c6 100644 (file)
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -144,7 +144,6 @@ void SineSolver::doReductions()
           d_data->addModelBoundForPurifyTerm(tf, mvs, mvs);
         }
         reduced = true;
-        break;
       }
     }
     if (!reduced)

diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index 9704957ac6ed406e9e76d621d8e3147e44ab7102..5af2902290f51224cf676d6e88c9a3af1a2ac06a 100644 (file)
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -73,6 +73,7 @@ void TranscendentalState::init(const std::vector<Node>& xts,
   d_funcMap.clear();
   d_tf_region.clear();
 
+  Trace("nl-ext-trans-init") << "TranscendentalState::init" << std::endl;
   bool needPi = false;
   // for computing congruence
   std::map<Kind, ArgTrie> argTrie;
@@ -118,6 +119,7 @@ void TranscendentalState::init(const std::vector<Node>& xts,
         d_trPurifies[a] = a;
       }
     }
+    Trace("nl-ext-trans-init") << "extf: " << a << ", consider=" << consider << std::endl;
     if (!consider)
     {
       // must assign a purified term
@@ -188,6 +190,7 @@ void TranscendentalState::ensureCongruence(TNode a,
     Assert(aa.getNumChildren() == a.getNumChildren());
     Node mvaa = d_model.computeAbstractModelValue(a);
     Node mvaaa = d_model.computeAbstractModelValue(aa);
+    Trace("nl-ext-trans-init") << "...congruent to " << aa << std::endl;
     if (mvaa != mvaaa)
     {
       std::vector<Node> exp;
@@ -198,12 +201,14 @@ void TranscendentalState::ensureCongruence(TNode a,
       Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(Kind::AND, exp);
       Node cong_lemma = expn.impNode(a.eqNode(aa));
       d_im.addPendingLemma(cong_lemma, InferenceId::ARITH_NL_CONGRUENCE);
+      Trace("nl-ext-trans-init") << "...needs lemma" << std::endl;
     }
   }
   else
   {
     // new representative of congruence class
     d_funcMap[a.getKind()].push_back(a);
+    Trace("nl-ext-trans-init") << "...new rep" << std::endl;
   }
   // add to congruence class
   d_funcCongClass[aa].push_back(a);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 9ebff31ceccffe16d6c72cf28f830435b93c41a1..67be26f52d936fe0555c4332f6ca4b98b0dc2ee6 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -799,6 +799,7 @@ set(regress_0_tests
   regress0/nl/nta/issue8182-exact-mv-keep.smt2
   regress0/nl/nta/issue8182-2-exact-mv-keep.smt2
   regress0/nl/nta/issue8183-tc-pi.smt2
+  regress0/nl/nta/issue8208-red-nred.smt2
   regress0/nl/nta/proj-issue403.smt2
   regress0/nl/nta/proj-issue460-pi-value.smt2
   regress0/nl/nta/real-pi.smt2

diff --git a/test/regress/regress0/nl/nta/issue8208-red-nred.smt2 b/test/regress/regress0/nl/nta/issue8208-red-nred.smt2
new file mode 100644 (file)
index 0000000..9eb8faf
--- /dev/null
+++ b/test/regress/regress0/nl/nta/issue8208-red-nred.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-const a Real)
+(declare-const b Real)
+(assert (< (sin a) (/ 0.0 (sin b))))
+(check-sat)