Extending public API with internal objects

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

Makefile.in

@@ -338,6 +338,9 @@ install: $(BIN_DIR)/$(Z3) $(BIN_DIR)/lib$(Z3).@SO_EXT@  $(BIN_DIR)/lib$(Z3).a
 	@cp lib/z3.h        $(PREFIX)/include
 	@cp lib/z3_v1.h     $(PREFIX)/include
 	@cp lib/z3_macros.h $(PREFIX)/include
+	@cp lib/z3_internal.h $(PREFIX)/include
+	@cp lib/z3_internal_types.h $(PREFIX)/include
+	@cp lib/z3_poly.h   $(PREFIX)/include
 	@cp c++/z3++.h      $(PREFIX)/include
 
 uninstall:
@@ -349,6 +352,9 @@ uninstall:
 	@rm -f $(PREFIX)/include/z3_v1.h
 	@rm -f $(PREFIX)/include/z3_macros.h
 	@rm -f $(PREFIX)/include/z3++.h
+	@rm -f $(PREFIX)/include/z3_internal.h
+	@rm -f $(PREFIX)/include/z3_internal_types.h
+	@rm -f $(PREFIX)/include/z3_poly.h
 
 install-z3py: $(BIN_DIR)/lib$(Z3).@SO_EXT@
 	@if test $(HAS_PYTHON) -eq 0; then echo "Python is not available in your system."; exit 1; fi
@@ -360,6 +366,7 @@ install-z3py: $(BIN_DIR)/lib$(Z3).@SO_EXT@
 	@cp python/z3consts.pyc $(PYTHON_PACKAGE_DIR)
 	@cp python/z3tactics.pyc $(PYTHON_PACKAGE_DIR)
 	@cp python/z3printer.pyc $(PYTHON_PACKAGE_DIR)
+	@cp python/z3poly.pyc $(PYTHON_PACKAGE_DIR)
 	@cp $(BIN_DIR)/lib$(Z3).@SO_EXT@ $(PYTHON_PACKAGE_DIR)
 	@if python python/z3test.py; then echo "Z3Py was successfully installed."; else echo "Failed to execute Z3Py regressions..."; exit 1; fi
 
@@ -372,4 +379,5 @@ uninstall-z3py:
 	@rm -f $(PYTHON_PACKAGE_DIR)/z3consts.pyc
 	@rm -f $(PYTHON_PACKAGE_DIR)/z3tactics.pyc
 	@rm -f $(PYTHON_PACKAGE_DIR)/z3printer.pyc
+	@rm -f $(PYTHON_PACKAGE_DIR)/z3poly.pyc
 	@rm -f $(PYTHON_PACKAGE_DIR)/$(BIN_DIR)/lib$(Z3).@SO_EXT@

Microsoft.Z3/Native.cs

@@ -8,6 +8,7 @@ using System.Runtime.InteropServices;
 
 namespace Microsoft.Z3
 {
+    using Z3_monomial = System.IntPtr;
     using Z3_config = System.IntPtr;
     using Z3_context = System.IntPtr;
     using Z3_ast = System.IntPtr;
@@ -34,6 +35,8 @@ namespace Microsoft.Z3
     using Z3_func_entry = System.IntPtr;
     using Z3_fixedpoint = System.IntPtr;
     using Z3_param_descrs = System.IntPtr;
+    using Z3_polynomial_manager = System.IntPtr;
+    using Z3_polynomial = System.IntPtr;
 
     public class Native
     {
@@ -1492,6 +1495,24 @@ namespace Microsoft.Z3
             [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
             public extern static Z3_ast Z3_get_context_assignment(Z3_context a0);
 
+            [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
+            public extern static Z3_polynomial_manager Z3_mk_polynomial_manager(Z3_context a0);
+
+            [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
+            public extern static void Z3_del_polynomial_manager(Z3_context a0, Z3_polynomial_manager a1);
+
+            [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
+            public extern static Z3_polynomial Z3_mk_zero_polynomial(Z3_context a0, Z3_polynomial_manager a1);
+
+            [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
+            public extern static void Z3_polynomial_inc_ref(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2);
+
+            [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
+            public extern static void Z3_polynomial_dec_ref(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2);
+
+            [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
+            public extern static IntPtr Z3_polynomial_to_string(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2);
+
         }
 
         public static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1) {
@@ -5215,6 +5236,51 @@ namespace Microsoft.Z3
             return r;
         }
 
+        public static Z3_polynomial_manager Z3_mk_polynomial_manager(Z3_context a0) {
+            Z3_polynomial_manager r = LIB.Z3_mk_polynomial_manager(a0);
+            Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
+            if (err != Z3_error_code.Z3_OK)
+                throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
+            return r;
+        }
+
+        public static void Z3_del_polynomial_manager(Z3_context a0, Z3_polynomial_manager a1) {
+            LIB.Z3_del_polynomial_manager(a0, a1);
+            Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
+            if (err != Z3_error_code.Z3_OK)
+                throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
+        }
+
+        public static Z3_polynomial Z3_mk_zero_polynomial(Z3_context a0, Z3_polynomial_manager a1) {
+            Z3_polynomial r = LIB.Z3_mk_zero_polynomial(a0, a1);
+            Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
+            if (err != Z3_error_code.Z3_OK)
+                throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
+            return r;
+        }
+
+        public static void Z3_polynomial_inc_ref(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2) {
+            LIB.Z3_polynomial_inc_ref(a0, a1, a2);
+            Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
+            if (err != Z3_error_code.Z3_OK)
+                throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
+        }
+
+        public static void Z3_polynomial_dec_ref(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2) {
+            LIB.Z3_polynomial_dec_ref(a0, a1, a2);
+            Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
+            if (err != Z3_error_code.Z3_OK)
+                throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
+        }
+
+        public static string Z3_polynomial_to_string(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2) {
+            IntPtr r = LIB.Z3_polynomial_to_string(a0, a1, a2);
+            Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
+            if (err != Z3_error_code.Z3_OK)
+                throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
+            return Marshal.PtrToStringAnsi(r);
+        }
+
     }
 
 }

lib/api_ast.cpp

@@ -16,7 +16,7 @@ Revision History:
 
 --*/
 #include<iostream>
-#include"z3.h"
+#include"z3_internal.h"
 #include"api_log_macros.h"
 #include"api_context.h"
 #include"api_util.h"

lib/api_commands.cpp

@@ -1,5 +1,6 @@
 // Automatically generated file, generator: update_api.py
 #include"z3.h"
+#include"z3_internal.h"
 #include"z3_replayer.h"
 void Z3_replacer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\n", Z3_get_error_msg_ex(ctx, c)); }
 void exec_Z3_mk_config(z3_replayer & in) {
@@ -3003,6 +3004,40 @@ void exec_Z3_get_context_assignment(z3_replayer & in) {
     reinterpret_cast<Z3_context>(in.get_obj(0)));
   in.store_result(result);
 }
+void exec_Z3_mk_polynomial_manager(z3_replayer & in) {
+  Z3_polynomial_manager result = Z3_mk_polynomial_manager(
+    reinterpret_cast<Z3_context>(in.get_obj(0)));
+  in.store_result(result);
+}
+void exec_Z3_del_polynomial_manager(z3_replayer & in) {
+  Z3_del_polynomial_manager(
+    reinterpret_cast<Z3_context>(in.get_obj(0)),
+    reinterpret_cast<Z3_polynomial_manager>(in.get_obj(1)));
+}
+void exec_Z3_mk_zero_polynomial(z3_replayer & in) {
+  Z3_polynomial result = Z3_mk_zero_polynomial(
+    reinterpret_cast<Z3_context>(in.get_obj(0)),
+    reinterpret_cast<Z3_polynomial_manager>(in.get_obj(1)));
+  in.store_result(result);
+}
+void exec_Z3_polynomial_inc_ref(z3_replayer & in) {
+  Z3_polynomial_inc_ref(
+    reinterpret_cast<Z3_context>(in.get_obj(0)),
+    reinterpret_cast<Z3_polynomial_manager>(in.get_obj(1)),
+    reinterpret_cast<Z3_polynomial>(in.get_obj(2)));
+}
+void exec_Z3_polynomial_dec_ref(z3_replayer & in) {
+  Z3_polynomial_dec_ref(
+    reinterpret_cast<Z3_context>(in.get_obj(0)),
+    reinterpret_cast<Z3_polynomial_manager>(in.get_obj(1)),
+    reinterpret_cast<Z3_polynomial>(in.get_obj(2)));
+}
+void exec_Z3_polynomial_to_string(z3_replayer & in) {
+  Z3_polynomial_to_string(
+    reinterpret_cast<Z3_context>(in.get_obj(0)),
+    reinterpret_cast<Z3_polynomial_manager>(in.get_obj(1)),
+    reinterpret_cast<Z3_polynomial>(in.get_obj(2)));
+}
 void register_z3_replayer_cmds(z3_replayer & in) {
   in.register_cmd(0, exec_Z3_mk_config);
   in.register_cmd(1, exec_Z3_del_config);
@@ -3481,4 +3516,10 @@ void register_z3_replayer_cmds(z3_replayer & in) {
   in.register_cmd(474, exec_Z3_context_to_string);
   in.register_cmd(475, exec_Z3_statistics_to_string);
   in.register_cmd(476, exec_Z3_get_context_assignment);
+  in.register_cmd(477, exec_Z3_mk_polynomial_manager);
+  in.register_cmd(478, exec_Z3_del_polynomial_manager);
+  in.register_cmd(479, exec_Z3_mk_zero_polynomial);
+  in.register_cmd(480, exec_Z3_polynomial_inc_ref);
+  in.register_cmd(481, exec_Z3_polynomial_dec_ref);
+  in.register_cmd(482, exec_Z3_polynomial_to_string);
 }

lib/api_log_macros.cpp

@@ -3315,3 +3315,41 @@ void log_Z3_get_context_assignment(Z3_context a0) {
   P(a0);
   C(476);
 }
+void log_Z3_mk_polynomial_manager(Z3_context a0) {
+  R();
+  P(a0);
+  C(477);
+}
+void log_Z3_del_polynomial_manager(Z3_context a0, Z3_polynomial_manager a1) {
+  R();
+  P(a0);
+  P(a1);
+  C(478);
+}
+void log_Z3_mk_zero_polynomial(Z3_context a0, Z3_polynomial_manager a1) {
+  R();
+  P(a0);
+  P(a1);
+  C(479);
+}
+void log_Z3_polynomial_inc_ref(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2) {
+  R();
+  P(a0);
+  P(a1);
+  P(a2);
+  C(480);
+}
+void log_Z3_polynomial_dec_ref(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2) {
+  R();
+  P(a0);
+  P(a1);
+  P(a2);
+  C(481);
+}
+void log_Z3_polynomial_to_string(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2) {
+  R();
+  P(a0);
+  P(a1);
+  P(a2);
+  C(482);
+}

lib/api_log_macros.h

@@ -975,3 +975,15 @@ void log_Z3_statistics_to_string(Z3_context a0);
 #define LOG_Z3_statistics_to_string(_ARG0) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_statistics_to_string(_ARG0); }
 void log_Z3_get_context_assignment(Z3_context a0);
 #define LOG_Z3_get_context_assignment(_ARG0) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_get_context_assignment(_ARG0); }
+void log_Z3_mk_polynomial_manager(Z3_context a0);
+#define LOG_Z3_mk_polynomial_manager(_ARG0) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_mk_polynomial_manager(_ARG0); }
+void log_Z3_del_polynomial_manager(Z3_context a0, Z3_polynomial_manager a1);
+#define LOG_Z3_del_polynomial_manager(_ARG0, _ARG1) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_del_polynomial_manager(_ARG0, _ARG1); }
+void log_Z3_mk_zero_polynomial(Z3_context a0, Z3_polynomial_manager a1);
+#define LOG_Z3_mk_zero_polynomial(_ARG0, _ARG1) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_mk_zero_polynomial(_ARG0, _ARG1); }
+void log_Z3_polynomial_inc_ref(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2);
+#define LOG_Z3_polynomial_inc_ref(_ARG0, _ARG1, _ARG2) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_polynomial_inc_ref(_ARG0, _ARG1, _ARG2); }
+void log_Z3_polynomial_dec_ref(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2);
+#define LOG_Z3_polynomial_dec_ref(_ARG0, _ARG1, _ARG2) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_polynomial_dec_ref(_ARG0, _ARG1, _ARG2); }
+void log_Z3_polynomial_to_string(Z3_context a0, Z3_polynomial_manager a1, Z3_polynomial a2);
+#define LOG_Z3_polynomial_to_string(_ARG0, _ARG1, _ARG2) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_polynomial_to_string(_ARG0, _ARG1, _ARG2); }

lib/api_poly.cpp

@@ -0,0 +1,78 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    api_poly.cpp
+
+Abstract:
+
+    External API for polynomial package
+    
+Author:
+
+    Leonardo de Moura (leonardo) 2012-10-18.
+
+Revision History:
+
+--*/
+#include"z3.h"
+#include"z3_internal.h"
+#include"api_context.h"
+#include"api_poly.h"
+#include"api_util.h"
+#include"api_log_macros.h"
+
+Z3_polynomial_manager Z3_mk_polynomial_manager(Z3_context c) {
+    Z3_TRY;
+    LOG_Z3_mk_polynomial_manager(c);
+    RESET_ERROR_CODE();
+    _Z3_polynomial_manager * m = alloc(_Z3_polynomial_manager);
+    RETURN_Z3(of_poly_manager(m));
+    Z3_CATCH_RETURN(0);
+}
+
+void Z3_del_polynomial_manager(Z3_context c, Z3_polynomial_manager m) {
+    Z3_TRY;
+    LOG_Z3_del_polynomial_manager(c, m);
+    RESET_ERROR_CODE();
+    dealloc(to_poly_manager(m));
+    Z3_CATCH;
+}
+
+Z3_polynomial Z3_mk_zero_polynomial(Z3_context c, Z3_polynomial_manager m) {
+    Z3_TRY;
+    LOG_Z3_mk_zero_polynomial(c, m);
+    RESET_ERROR_CODE();
+    polynomial::polynomial * r = to_poly_manager(m)->m_manager.mk_zero();
+    to_poly_manager(m)->m_result = r;
+    RETURN_Z3(of_poly(r));
+    Z3_CATCH_RETURN(0);
+}
+
+void Z3_polynomial_inc_ref(Z3_context c, Z3_polynomial_manager m, Z3_polynomial p) {
+    Z3_TRY;
+    LOG_Z3_polynomial_inc_ref(c, m, p);
+    RESET_ERROR_CODE();
+    to_poly_manager(m)->m_manager.inc_ref(to_poly(p));
+    Z3_CATCH;
+}
+
+void Z3_polynomial_dec_ref(Z3_context c, Z3_polynomial_manager m, Z3_polynomial p) {
+    Z3_TRY;
+    LOG_Z3_polynomial_inc_ref(c, m, p);
+    RESET_ERROR_CODE();
+    to_poly_manager(m)->m_manager.dec_ref(to_poly(p));
+    Z3_CATCH;
+}
+
+Z3_string Z3_polynomial_to_string(Z3_context c, Z3_polynomial_manager m, Z3_polynomial p) {
+    Z3_TRY;
+    LOG_Z3_polynomial_to_string(c, m, p);
+    RESET_ERROR_CODE();
+    std::ostringstream buffer;
+    to_poly_manager(m)->m_manager.display(buffer, to_poly(p));
+    return mk_c(c)->mk_external_string(buffer.str());
+    Z3_CATCH_RETURN("");
+}
+

lib/api_poly.h

@@ -0,0 +1,40 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    api_poly.h
+
+Abstract:
+    External API for polynomial package
+    
+Author:
+
+    Leonardo de Moura (leonardo) 2012-10-18.
+
+Revision History:
+
+--*/
+#ifndef _API_POLY_H_
+#define _API_POLY_H_
+
+#include"polynomial.h"
+
+struct _Z3_polynomial_manager {
+    unsynch_mpz_manager m_num_manager;
+    polynomial::manager m_manager;
+    polynomial_ref      m_result;
+
+    _Z3_polynomial_manager():
+        m_manager(m_num_manager),
+        m_result(m_manager) {
+    }
+};
+
+inline _Z3_polynomial_manager * to_poly_manager(Z3_polynomial_manager m) { return reinterpret_cast<_Z3_polynomial_manager*>(m); }
+inline Z3_polynomial_manager of_poly_manager(_Z3_polynomial_manager * m) { return reinterpret_cast<Z3_polynomial_manager>(m); }
+
+inline polynomial::polynomial * to_poly(Z3_polynomial p) { return reinterpret_cast<polynomial::polynomial*>(p); }
+inline Z3_polynomial of_poly(polynomial::polynomial * p) { return reinterpret_cast<Z3_polynomial>(p); }
+
+#endif

lib/api_util.h

@@ -20,6 +20,7 @@ Revision History:
 
 #include"params.h"
 #include"lbool.h"
+#include"ast.h"
 
 #define Z3_TRY try {
 #define Z3_CATCH_CORE(CODE) } catch (z3_exception & ex) { mk_c(c)->handle_exception(ex); CODE }

lib/lib.vcxproj

@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
 <Project DefaultTargets="Build" ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
   <ItemGroup Label="ProjectConfigurations">
     <ProjectConfiguration Include="commercial|Win32">
@@ -443,6 +443,7 @@
     <ClCompile Include="api_numeral.cpp" />
     <ClCompile Include="api_params.cpp" />
     <ClCompile Include="api_parsers.cpp" />
+    <ClCompile Include="api_poly.cpp" />
     <ClCompile Include="api_quant.cpp" />
     <ClCompile Include="api_solver_old.cpp" />
     <ClCompile Include="api_solver.cpp" />

lib/z3.h

@@ -24,6 +24,7 @@ Notes:
 #include<stdio.h>
 #include"z3_macros.h"
 #include"z3_api.h"
+#include"z3_internal_types.h"
 
 #undef __in
 #undef __out

lib/z3_api.h

@@ -1,3 +1,6 @@
+#ifndef _Z3_API_H_
+#define _Z3_API_H_
+
 #ifdef CAMLIDL
   #ifdef MLAPIV3
     #define ML3only
@@ -7556,3 +7559,5 @@ END_MLAPI_EXCLUDE
 #endif // CAMLIDL
 
 /*@}*/
+
+#endif

lib/z3_internal.h

@@ -0,0 +1,40 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    z3_internal.h
+
+Abstract:
+
+    Z3 internal API for C and Python.
+    It provides access to internal Z3 components.
+    It should only be used by advanced users.
+    We used it to build regression tests in Python.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-10-18
+
+Notes:
+    
+--*/
+#ifndef _Z3_INTERNAL_H_
+#define _Z3_INTERNAL_H_
+
+#include"z3_macros.h"
+#include"z3_api.h"
+#include"z3_internal_types.h"
+#include"z3_poly.h"
+
+#undef __in
+#undef __out
+#undef __inout
+#undef __in_z
+#undef __out_z
+#undef __ecount
+#undef __in_ecount
+#undef __out_ecount
+#undef __inout_ecount
+
+#endif

lib/z3_internal_types.h

@@ -0,0 +1,34 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    z3_internal_types.h
+
+Abstract:
+
+    Z3 internal API type declarations.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-10-18
+
+Notes:
+    
+--*/
+#ifndef _Z3_INTERNAL_TYPES_H_
+#define _Z3_INTERNAL_TYPES_H_
+
+DEFINE_TYPE(Z3_polynomial_manager);
+DEFINE_TYPE(Z3_polynomial);
+DEFINE_TYPE(Z3_monomial);
+
+/*
+  Definitions for update_api.py
+  
+  def_Type('POLYNOMIAL_MANAGER',           'Z3_polynomial_manager',           'PolynomialManagerObj')
+  def_Type('POLYNOMIAL',                   'Z3_polynomial',                   'PolynomialObj')
+  def_Type('MONOMIAL',                     'Z3_monomial',                     'MonomialObj')
+*/
+
+#endif

lib/z3_poly.h

@@ -0,0 +1,72 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    z3_poly.h
+
+Abstract:
+
+    Z3 multivariate polynomial API.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-10-18
+
+Notes:
+    
+--*/
+#ifndef _Z3_POLY_H_
+#define _Z3_POLY_H_
+
+#ifdef __cplusplus
+extern "C" {
+#endif // __cplusplus
+
+    /**
+       \brief Create a new polynomial manager.
+
+       def_API('Z3_mk_polynomial_manager', POLYNOMIAL_MANAGER, (_in(CONTEXT),))
+    */
+    Z3_polynomial_manager Z3_API Z3_mk_polynomial_manager(__in Z3_context c);
+    
+    /**
+       \brief Delete the given polynomial manager.
+       
+       def_API('Z3_del_polynomial_manager', VOID, (_in(CONTEXT), _in(POLYNOMIAL_MANAGER)))
+    */
+    void Z3_API Z3_del_polynomial_manager(__in Z3_context c, __in Z3_polynomial_manager m);
+
+    /**
+       \brief Return the zero polynomial.
+
+       def_API('Z3_mk_zero_polynomial', POLYNOMIAL, (_in(CONTEXT), _in(POLYNOMIAL_MANAGER)))
+    */
+    Z3_polynomial Z3_API Z3_mk_zero_polynomial(__in Z3_context c, __in Z3_polynomial_manager m);
+
+    /**
+       \brief Increment p's reference counter
+
+       def_API('Z3_polynomial_inc_ref', VOID, (_in(CONTEXT), _in(POLYNOMIAL_MANAGER), _in(POLYNOMIAL)))
+    */
+    void Z3_API Z3_polynomial_inc_ref(__in Z3_context c, __in Z3_polynomial_manager m, __in Z3_polynomial p);
+
+    /**
+       \brief Decrement p's reference counter.
+
+       def_API('Z3_polynomial_dec_ref', VOID, (_in(CONTEXT), _in(POLYNOMIAL_MANAGER), _in(POLYNOMIAL)))
+    */
+    void Z3_API Z3_polynomial_dec_ref(__in Z3_context c, __in Z3_polynomial_manager m, __in Z3_polynomial p);
+    
+    /**
+       \brief Convert the given polynomial into a string.
+
+       def_API('Z3_polynomial_to_string', STRING, (_in(CONTEXT), _in(POLYNOMIAL_MANAGER), _in(POLYNOMIAL)))
+    */
+    Z3_string Z3_API Z3_polynomial_to_string(__in Z3_context c, __in Z3_polynomial_manager m, __in Z3_polynomial p);
+
+#ifdef __cplusplus
+};
+#endif // __cplusplus
+
+#endif

python/z3core.py

@@ -904,6 +904,15 @@ def init(PATH):
   _lib.Z3_statistics_to_string.argtypes = [ContextObj]
   _lib.Z3_get_context_assignment.restype = Ast
   _lib.Z3_get_context_assignment.argtypes = [ContextObj]
+  _lib.Z3_mk_polynomial_manager.restype = PolynomialManagerObj
+  _lib.Z3_mk_polynomial_manager.argtypes = [ContextObj]
+  _lib.Z3_del_polynomial_manager.argtypes = [ContextObj, PolynomialManagerObj]
+  _lib.Z3_mk_zero_polynomial.restype = PolynomialObj
+  _lib.Z3_mk_zero_polynomial.argtypes = [ContextObj, PolynomialManagerObj]
+  _lib.Z3_polynomial_inc_ref.argtypes = [ContextObj, PolynomialManagerObj, PolynomialObj]
+  _lib.Z3_polynomial_dec_ref.argtypes = [ContextObj, PolynomialManagerObj, PolynomialObj]
+  _lib.Z3_polynomial_to_string.restype = ctypes.c_char_p
+  _lib.Z3_polynomial_to_string.argtypes = [ContextObj, PolynomialManagerObj, PolynomialObj]
 
 def Z3_mk_config():
   r = lib().Z3_mk_config()
@@ -4142,3 +4151,42 @@ def Z3_get_context_assignment(a0):
     raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))
   return r
 
+def Z3_mk_polynomial_manager(a0):
+  r = lib().Z3_mk_polynomial_manager(a0)
+  err = lib().Z3_get_error_code(a0)
+  if err != Z3_OK:
+    raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))
+  return r
+
+def Z3_del_polynomial_manager(a0, a1):
+  lib().Z3_del_polynomial_manager(a0, a1)
+  err = lib().Z3_get_error_code(a0)
+  if err != Z3_OK:
+    raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))
+
+def Z3_mk_zero_polynomial(a0, a1):
+  r = lib().Z3_mk_zero_polynomial(a0, a1)
+  err = lib().Z3_get_error_code(a0)
+  if err != Z3_OK:
+    raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))
+  return r
+
+def Z3_polynomial_inc_ref(a0, a1, a2):
+  lib().Z3_polynomial_inc_ref(a0, a1, a2)
+  err = lib().Z3_get_error_code(a0)
+  if err != Z3_OK:
+    raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))
+
+def Z3_polynomial_dec_ref(a0, a1, a2):
+  lib().Z3_polynomial_dec_ref(a0, a1, a2)
+  err = lib().Z3_get_error_code(a0)
+  if err != Z3_OK:
+    raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))
+
+def Z3_polynomial_to_string(a0, a1, a2):
+  r = lib().Z3_polynomial_to_string(a0, a1, a2)
+  err = lib().Z3_get_error_code(a0)
+  if err != Z3_OK:
+    raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))
+  return r
+

python/z3poly.py

@@ -0,0 +1,67 @@
+############################################
+# Copyright (c) 2012 Microsoft Corporation
+# 
+# Z3 Polynomial interface
+#
+# Author: Leonardo de Moura (leonardo)
+############################################
+from z3 import *
+
+class PolynomialManager:
+    """Polynomial Manager.
+    """
+    def __init__(self, ctx=None):
+        self.ctx     = z3._get_ctx(ctx)
+        self.manager = Z3_mk_polynomial_manager(self.ctx_ref())
+        
+    def __del__(self):
+        Z3_del_polynomial_manager(self.ctx_ref(), self.manager)
+
+    def ctx_ref(self):
+        return self.ctx.ref()
+
+    def m(self):
+        return self.manager
+
+_main_pmanager = None
+def main_pmanager():
+    """Return a reference to the global Polynomial manager.
+    """
+    global _main_pmanager
+    if _main_pmanager == None:
+        _main_pmanager = PolynomialManager()
+    return _main_pmanager  
+
+def _get_pmanager(ctx):
+    if ctx == None:
+        return main_pmanager()
+    else:
+        return ctx
+
+class Polynomial:
+    """Multivariate polynomials.
+    """
+    def __init__(self, poly=None, m=None):
+        self.pmanager = _get_pmanager(m)
+        if poly == None:
+            self.poly = Z3_mk_zero_polynomial(self.ctx_ref(), self.m())
+        else:
+            self.poly = poly
+        Z3_polynomial_inc_ref(self.ctx_ref(), self.m(), self.poly)
+    
+    def __del__(self):
+        Z3_polynomial_dec_ref(self.ctx_ref(), self.m(), self.poly)
+
+    def m(self):
+        return self.pmanager.m()
+
+    def ctx_ref(self):
+        return self.pmanager.ctx_ref()
+    
+    def __repr__(self):
+        return Z3_polynomial_to_string(self.ctx_ref(), self.m(), self.poly)
+
+# test
+p = Polynomial()
+print p
+

python/z3types.py

@@ -105,3 +105,15 @@ class FuncInterpObj(ctypes.c_void_p):
 class FuncEntryObj(ctypes.c_void_p):
   def __init__(self, e): self._as_parameter_ = e
   def from_param(obj): return obj
+
+class PolynomialManagerObj(ctypes.c_void_p):
+  def __init__(self, e): self._as_parameter_ = e
+  def from_param(obj): return obj
+
+class PolynomialObj(ctypes.c_void_p):
+  def __init__(self, e): self._as_parameter_ = e
+  def from_param(obj): return obj
+
+class MonomialObj(ctypes.c_void_p):
+  def __init__(self, e): self._as_parameter_ = e
+  def from_param(obj): return obj

update_api.py

@@ -16,6 +16,8 @@ def add_api_file(dir, file):
     API_FILES.append("%s%s%s" % (dir, os.sep, file))
 
 add_api_file('lib', 'z3_api.h')
+add_api_file('lib', 'z3_internal_types.h')
+add_api_file('lib', 'z3_poly.h')
 
 # Extract enumeration types from z3_api.h, and add .Net definitions
 def mk_z3consts_donet():
@@ -238,6 +240,7 @@ log_c.write('#include\"z3_logger.h\"\n')
 ##
 exe_c.write('// Automatically generated file, generator: update_api.py\n')
 exe_c.write('#include\"z3.h\"\n')
+exe_c.write('#include\"z3_internal.h\"\n')
 exe_c.write('#include\"z3_replayer.h\"\n')
 ##
 log_h.write('extern std::ostream * g_z3_log;\n')