Preserve model values for exact sine points (#8188)

Fixes #8182.

diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index 245665d68dbd8c1a2a991869de9f44891266ed24..8ab36368798ebfbef906bddc13c73f0bf9b9c5fe 100644 (file)
--- 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 88ca1b71e1f9a16738baa03f4074ddc90cd01b38..a0589d10898316e4ddc030546c0f413b1a8c9c3b 100644 (file)
--- 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 ac94be864af1d6df426b96ad05a54813342bd707..262298772cf617836679ef99e4d85a2407a657b5 100644 (file)
--- 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 393e191dab80f1e8de2f5eaf0e064452e07a55f4..0d646392fbda78b2378b70ac8d8216c76e817839 100644 (file)
--- 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 (file)
index 0000000..13088e5
--- /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 (file)
index 0000000..0d71007
--- /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)