bump version, add double access

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

CMakeLists.txt

@@ -34,7 +34,7 @@ endif()
 ################################################################################
 set(Z3_VERSION_MAJOR 4)
 set(Z3_VERSION_MINOR 8)
-set(Z3_VERSION_PATCH 0)
+set(Z3_VERSION_PATCH 2)
 set(Z3_VERSION_TWEAK 0)
 set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}")
 set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified

examples/c++/example.cpp

@@ -835,6 +835,17 @@ void tst_visit() {
     visit(f);
 }
 
+void tst_numeral() {
+    context c;
+    expr x = c.real_val("1/3");
+    double d = 0;
+    if (!x.is_numeral(d)) {
+        std::cout << x << " is not recognized as a numeral\n";
+        return;
+    }
+    std::cout << x << " is " << d << "\n";
+}
+
 void incremental_example1() {
     std::cout << "incremental example1\n";
     context c;
@@ -1212,6 +1223,7 @@ int main() {
         tactic_example9(); std::cout << "\n";
         tactic_qe(); std::cout << "\n";
         tst_visit(); std::cout << "\n";
+        tst_numeral(); std::cout << "\n";
         incremental_example1(); std::cout << "\n";
         incremental_example2(); std::cout << "\n";
         incremental_example3(); std::cout << "\n";

scripts/mk_project.py

@@ -9,7 +9,7 @@ from mk_util import *
 
 # Z3 Project definition
 def init_project_def():
-    set_version(4, 8, 0, 0)
+    set_version(4, 8, 2, 0)
     add_lib('util', [], includes2install = ['z3_version.h'])
     add_lib('polynomial', ['util'], 'math/polynomial')
     add_lib('sat', ['util'])

src/api/api_numeral.cpp

@@ -227,6 +227,11 @@ extern "C" {
         Z3_CATCH_RETURN("");
     }
 
+    double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a) {
+        Z3_string s = Z3_get_numeral_decimal_string(c, a, 12);
+        return std::stod(std::string(s));
+    }
+
     Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision) {
         Z3_TRY;
         LOG_Z3_get_numeral_decimal_string(c, a, precision);

src/api/c++/z3++.h

@@ -709,6 +709,7 @@ namespace z3 {
         bool is_numeral_u(unsigned& i) const { bool r = 0 != Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
         bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
         bool is_numeral(std::string& s, unsigned precision) const { if (!is_numeral()) return false; s = Z3_get_numeral_decimal_string(ctx(), m_ast, precision); check_error(); return true; }
+        bool is_numeral(double& d) const { if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; }
         /**
            \brief Return true if this expression is an application.
         */

src/api/dotnet/RatNum.cs

@@ -92,6 +92,14 @@ namespace Microsoft.Z3
             return Native.Z3_get_numeral_decimal_string(Context.nCtx, NativeObject, precision);
         }
 
+        /// <summary>
+        /// Returns a double representing the value.
+        /// </summary>
+        public double Double
+        {
+            get { return Native.Z3_get_numeral_double(Context.nCtx, NativeObject); }
+        }
+
         /// <summary>
         /// Returns a string representation of the numeral.
         /// </summary>        

src/api/dotnet/core/project.json

@@ -1,22 +0,0 @@
-{
-    "version": "1.0.0-*",
-    "buildOptions": {
-        "debugType": "portable",
-        "emitEntryPoint": false,
-        "outputName": "Microsoft.Z3",
-        "compile": [ "../*.cs", "*.cs" ],
-        "define": ["DOTNET_CORE"]
-    },
-    "dependencies": { },
-    "frameworks": {
-        "netcoreapp1.0": {
-            "dependencies": {
-                "Microsoft.NETCore.App": {
-                    "type": "platform",
-                    "version": "1.0.1"
-                }
-            },
-            "imports": "dnxcore50"
-        }
-    }
-}

src/api/z3_api.h

@@ -4438,6 +4438,15 @@ extern "C" {
     */
     Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision);
 
+    /**
+       \brief Return numeral as a double.
+
+       \pre Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST || Z3_is_algebraic_number(c, a)
+
+       def_API('Z3_get_numeral_double', STRING, (_in(CONTEXT), _in(AST)))
+    */
+    double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a);
+
     /**
        \brief Return the numerator (as a numeral AST) of a numeral AST of sort Real.