From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 17 Feb 2022 21:40:22 +0000 (-0600)
Subject: Introduce skolem function to make transcendental function purification consistent... 
X-Git-Tag: cvc5-1.0.0~417
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cdef52f07aef156ad19dea89862a1b8d4373ea3a;p=cvc5.git

Introduce skolem function to make transcendental function purification consistent (#8116)

Previously, we could introduce multiple purifications for the same sin term.
---

diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index 11617e14f..4bda69bcb 100644
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -56,6 +56,8 @@ const char* toString(SkolemFunId id)
     case SkolemFunId::INT_DIV_BY_ZERO: return "INT_DIV_BY_ZERO";
     case SkolemFunId::MOD_BY_ZERO: return "MOD_BY_ZERO";
     case SkolemFunId::SQRT: return "SQRT";
+    case SkolemFunId::TRANSCENDENTAL_PURIFY_ARG:
+      return "TRANSCENDENTAL_PURIFY_ARG";
     case SkolemFunId::SELECTOR_WRONG: return "SELECTOR_WRONG";
     case SkolemFunId::SHARED_SELECTOR: return "SHARED_SELECTOR";
     case SkolemFunId::SEQ_NTH_OOB: return "SEQ_NTH_OOB";
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 97997cdc9..2c696d23f 100644
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -38,6 +38,12 @@ enum class SkolemFunId
   MOD_BY_ZERO,
   /** an uninterpreted function f s.t. f(x) = sqrt(x) */
   SQRT,
+  /**
+   * Argument used to purify trancendental function app f(x).
+   * For sin(x), this is a variable that is assumed to be in phase with x that
+   * is between -pi and pi
+   */
+  TRANSCENDENTAL_PURIFY_ARG,
   /** a wrongly applied selector */
   SELECTOR_WRONG,
   /** a shared selector */
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index 25a5a511f..9f7e474bb 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -67,8 +67,8 @@ void TranscendentalSolver::initLastCall(const std::vector<Node>& xts)
     Assert(d_tstate.d_trMaster.find(a) == d_tstate.d_trMaster.end());
     Kind k = a.getKind();
     Assert(k == Kind::SINE || k == Kind::EXPONENTIAL);
-    Node y = sm->mkDummySkolem(
-        "y", nm->realType(), "phase shifted trigonometric arg");
+    Node y = sm->mkSkolemFunction(
+        SkolemFunId::TRANSCENDENTAL_PURIFY_ARG, nm->realType(), a);
     Node new_a = nm->mkNode(k, y);
     d_tstate.d_trSlaves[new_a].insert(new_a);
     d_tstate.d_trSlaves[new_a].insert(a);