Fixes for bounds on transcendental functions (#3832)

This PR refactors and fixes how bounds are set for transcendental functions. The new code ensures that all transcendental function applications are given bounds. (Our previous failures to do so were hindering our ability to say "sat", due to NlModel::checkModel failures).

There were previously two issues on why transcendental function applications were not being assigned bounds:

"Slave" transcendental functions (e.g. those that we reduce via sin(t) = sin(y) ^ -pi <= y <= pi ^ y + 2*pi*N = t) were not being given bounds explicitly,
Transcendental functions that are congruent to others (e.g. f(x) where f(y) exists and x=y in the current context) were being ignored and hence not bound.
This PR clarifies the master/slave relationship that tracks which transcendental function applications have been purified, and furthermore tracks congruence classes.

The setting of bounds and the check-model is further simplified by setting bounds on the original terms, whereas the current code sets bounds on the model values of terms. In other words, previously if we had term sin(y) and y^M = c, then we'd set bounds for sin(c), whereas the new code sets the bound on sin(y) directly.

Fixes #3783. We answer unknown without an assertion failure on that benchmark now. Further work based on ignoring literals from internally generated lemmas is necessary for solving it sat.

1 files changed, 6 insertions, 3 deletions

diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp
index 65aaceb80..cbb27197f 100644
--- a/src/theory/arith/arith_utilities.cpp
+++ b/src/theory/arith/arith_utilities.cpp
@@ -224,10 +224,13 @@ Node arithSubstitute(Node n, std::vector<Node>& vars, std::vector<Node>& subs)
       else
       {
         TheoryId ctid = theory::kindToTheoryId(ck);
-        if (ctid != THEORY_ARITH && ctid != THEORY_BOOL
-            && ctid != THEORY_BUILTIN)
+        if ((ctid != THEORY_ARITH && ctid != THEORY_BOOL
+             && ctid != THEORY_BUILTIN)
+            || isTranscendentalKind(ck))
         {
-          // do not traverse beneath applications that belong to another theory
+          // Do not traverse beneath applications that belong to another theory
+          // besides (core) arithmetic. Notice that transcendental function
+          // applications are also not traversed here.
           visited[cur] = cur;
         }
         else