From 2a7e0f4c8fe3d30da9be170a946f89f92606d5c1 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 28 Feb 2022 16:04:16 -0600
Subject: [PATCH] Preserve model values for exact sine points (#8188)

Fixes #8182.
---
 src/theory/arith/nl/transcendental/sine_solver.cpp  |  7 +++++++
 src/theory/arith/nl/transcendental/sine_solver.h    |  6 ++++++
 .../nl/transcendental/transcendental_solver.cpp     | 13 ++++++++++---
 test/regress/CMakeLists.txt                         |  2 ++
 .../regress0/nl/nta/issue8182-2-exact-mv-keep.smt2  |  8 ++++++++
 .../regress0/nl/nta/issue8182-exact-mv-keep.smt2    |  7 +++++++
 6 files changed, 40 insertions(+), 3 deletions(-)
 create mode 100644 test/regress/regress0/nl/nta/issue8182-2-exact-mv-keep.smt2
 create mode 100644 test/regress/regress0/nl/nta/issue8182-exact-mv-keep.smt2

diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index 245665d68..8ab363687 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -595,6 +595,13 @@ std::pair<Node, Node> SineSolver::getSecantBounds(TNode e,
   return bounds;
 }
 
+bool SineSolver::hasExactModelValue(TNode n) const
+{
+  Assert(n.getKind() == SINE);
+  Node mv = d_data->d_model.computeAbstractModelValue(n[0]);
+  return d_mpointsSine.find(mv) != d_mpointsSine.end();
+}
+
 }  // namespace transcendental
 }  // namespace nl
 }  // namespace arith
diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h
index 88ca1b71e..a0589d108 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.h
+++ b/src/theory/arith/nl/transcendental/sine_solver.h
@@ -108,6 +108,12 @@ class SineSolver : protected EnvObj
                       unsigned actual_d,
                       int region);
 
+  /**
+   * Does n of the form sin(x) have an exact model value? This is true if
+   * the model value of x is in the domain of d_mpointsSine.
+   */
+  bool hasExactModelValue(TNode n) const;
+
  private:
   std::pair<Node, Node> getSecantBounds(TNode e,
                                         TNode c,
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index ac94be864..262298772 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -457,11 +457,18 @@ void TranscendentalSolver::postProcessModel(std::map<Node, Node>& arithModel,
   std::unordered_map<Node, Node> trReps;
   for (const Node& n : termSet)
   {
-    if (isTranscendentalKind(n.getKind()))
+    Kind k = n.getKind();
+    if (!isTranscendentalKind(n.getKind()))
     {
-      Node r = d_astate.getRepresentative(n);
-      trReps[r] = n;
+      continue;
+    }
+    // it might have an exact value, in which case there is nothing to do
+    if (k == SINE && d_sineSlv.hasExactModelValue(n))
+    {
+      continue;
     }
+    Node r = d_astate.getRepresentative(n);
+    trReps[r] = n;
   }
   if (trReps.empty())
   {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 393e191da..0d646392f 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -792,6 +792,8 @@ set(regress_0_tests
   regress0/nl/nta/issue7938-tf-model.smt2
   regress0/nl/nta/issue8147-unc-model.smt2
   regress0/nl/nta/issue8160-model-purify.smt2
+  regress0/nl/nta/issue8182-exact-mv-keep.smt2
+  regress0/nl/nta/issue8182-2-exact-mv-keep.smt2
   regress0/nl/nta/proj-issue460-pi-value.smt2
   regress0/nl/nta/real-pi.smt2
   regress0/nl/nta/sin-sym.smt2
diff --git a/test/regress/regress0/nl/nta/issue8182-2-exact-mv-keep.smt2 b/test/regress/regress0/nl/nta/issue8182-2-exact-mv-keep.smt2
new file mode 100644
index 000000000..13088e551
--- /dev/null
+++ b/test/regress/regress0/nl/nta/issue8182-2-exact-mv-keep.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(assert (= a (* b (+ (sin a) (/ 1 a)))))
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/issue8182-exact-mv-keep.smt2 b/test/regress/regress0/nl/nta/issue8182-exact-mv-keep.smt2
new file mode 100644
index 000000000..0d71007ac
--- /dev/null
+++ b/test/regress/regress0/nl/nta/issue8182-exact-mv-keep.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun v () Real)
+(assert (forall ((V Real)) (> 0 (/ 0.0 v))))
+(assert (= 0.0 (* (sin v) (sin 1.0))))
+(check-sat)
-- 
2.30.2