From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Mar 2022 23:09:24 +0000 (-0600)
Subject: Fix issue with dropping non-reduced sine terms (#8211)
X-Git-Tag: cvc5-1.0.0~338
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a30458a2a3e21f40e893fe545c6e9c2c73e32707;p=cvc5.git

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 e765a1599..6645589e2 100644
--- 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 9704957ac..5af290229 100644
--- 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 9ebff31ce..67be26f52 100644
--- 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
index 000000000..9eb8faf29
--- /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)