From a6fcdecfd7be610006bd39cfb38fb53bad5a94ed Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 12 Mar 2020 14:23:45 -0700
Subject: [PATCH] Add accessor for lower/upper bounds of algebraic numerals
 #3245

The pretty printer for algebraic numerals prints a polynomial root expression, however, polynomial root expressions are not exposed over the API. The C API contains methods for approximating root objects from above and below with arbitrary precision. These functions are now exposed over the C++ API.
Note that algebraic numbers are also disjoint from rcf (real closed field) objects.
Thus, z3 doesn't support adding "pi" as an extension field to algebraic numbers that are used by the nlsat solver. It operats on algebraic numbers formed by roots over polynomial with rational coefficients
---
 src/api/c++/z3++.h      | 17 +++++++++++++++++
 src/smt/smt_context.cpp | 11 +++++++----
 src/smt/theory_seq.cpp  |  1 +
 3 files changed, 25 insertions(+), 4 deletions(-)

diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index dde9ba86f..00a647474 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -797,6 +797,23 @@ namespace z3 {
             assert(is_numeral() || is_algebraic());
             return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
         }
+
+        /**
+         * Retrieve lower and upper bounds for algebraic numerals based on a decimal precision
+         */
+        expr algebraic_lower(unsigned precision) const { 
+            assert(is_algebraic());      
+            Z3_ast r = Z3_get_algebraic_number_lower(ctx(), m_ast, precision);
+            check_error();
+            return expr(ctx(), r);
+        }
+
+        expr algebraic_upper(unsigned precision) const { 
+            assert(is_algebraic());      
+            Z3_ast r = Z3_get_algebraic_number_upper(ctx(), m_ast, precision);
+            check_error();
+            return expr(ctx(), r);
+        }
         
 
         /**
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 8167d6b40..10fb7836e 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3364,10 +3364,13 @@ namespace smt {
             r = l_undef;
         }
         if (r == l_true && gparams::get_value("model_validate") == "true") {
-            model_ref mdl;
-            get_model(mdl);
-            for (theory* t : m_theory_set) {
-                t->validate_model(*mdl);
+            recfun::util u(m);
+            if (u.get_rec_funs().empty()) {
+                model_ref mdl;
+                get_model(mdl);
+                for (theory* t : m_theory_set) {
+                    t->validate_model(*mdl);
+                }
             }
 #if 0
             for (literal lit : m_assigned_literals) {
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 8fee8fe3c..6351b84de 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -4412,6 +4412,7 @@ app* theory_seq::mk_value(app* e) {
 
 
 void theory_seq::validate_model(model& mdl) {
+    return;
     for (auto const& eq : m_eqs) {
         expr_ref_vector ls = eq.ls();
         expr_ref_vector rs = eq.rs();