exposing algebraic numbers in the API (working in progress)

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

scripts/mk_project.py

@@ -59,10 +59,10 @@ def init_project_def():
     add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'muz_qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
     add_lib('smtparser', ['portfolio'], 'parsers/smt')
     add_lib('api', ['portfolio', 'user_plugin', 'smtparser'],
-            includes2install=['z3.h', 'z3_api.h', 'z3_v1.h', 'z3_macros.h'])
+            includes2install=['z3.h', 'z3_api.h', 'z3_v1.h', 'z3_macros.h', 'z3_algebraic.h'])
     add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3')
     add_exe('test', ['api', 'fuzzing'], exe_name='test-z3', install=False)
-    API_files = ['z3_api.h']
+    API_files = ['z3_api.h', 'z3_algebraic.h']
     add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', 
             reexports=['api'], 
             dll_name='libz3', 

src/api/api_algebraic.cpp

@@ -0,0 +1,198 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    api_algebraic.cpp
+
+Abstract:
+
+    Additional APIs for handling Z3 algebraic numbers encoded as 
+    Z3_ASTs
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-12-07
+
+Notes:
+    
+--*/
+#include<iostream>
+#include"z3.h"
+#include"api_log_macros.h"
+#include"api_context.h"
+
+extern "C" {
+
+    Z3_bool Z3_API Z3_algebraic_is_value(Z3_context c, Z3_ast a) {
+        Z3_TRY;
+        LOG_Z3_algebraic_is_value(c, a);
+        RESET_ERROR_CODE();
+        // TODO
+        return Z3_FALSE;
+        Z3_CATCH_RETURN(Z3_FALSE);
+    }
+
+    Z3_bool Z3_API Z3_algebraic_is_pos(Z3_context c, Z3_ast a) {
+        Z3_TRY;
+        LOG_Z3_algebraic_is_pos(c, a);
+        RESET_ERROR_CODE();
+        // TODO
+        return Z3_FALSE;
+        Z3_CATCH_RETURN(Z3_FALSE);
+    }
+
+    Z3_bool Z3_API Z3_algebraic_is_neg(Z3_context c, Z3_ast a) {
+        Z3_TRY;
+        LOG_Z3_algebraic_is_neg(c, a);
+        RESET_ERROR_CODE();
+        // TODO
+        return Z3_FALSE;
+        Z3_CATCH_RETURN(Z3_FALSE);
+    }
+
+    Z3_bool Z3_API Z3_algebraic_is_zero(Z3_context c, Z3_ast a) {
+        Z3_TRY;
+        LOG_Z3_algebraic_is_zero(c, a);
+        RESET_ERROR_CODE();
+        // TODO
+        return Z3_FALSE;
+        Z3_CATCH_RETURN(Z3_FALSE);
+    }
+
+    int Z3_API Z3_algebraic_sign(Z3_context c, Z3_ast a) {
+        Z3_TRY;
+        LOG_Z3_algebraic_sign(c, a);
+        RESET_ERROR_CODE();
+        // TODO
+        return 0;
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_algebraic_add(Z3_context c, Z3_ast a, Z3_ast b) {
+        Z3_TRY;
+        LOG_Z3_algebraic_add(c, a, b);
+        RESET_ERROR_CODE();
+        // TODO
+        return 0;
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_algebraic_sub(Z3_context c, Z3_ast a, Z3_ast b) {
+        Z3_TRY;
+        LOG_Z3_algebraic_sub(c, a, b);
+        RESET_ERROR_CODE();
+        // TODO
+        return 0;
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_algebraic_mul(Z3_context c, Z3_ast a, Z3_ast b) {
+        Z3_TRY;
+        LOG_Z3_algebraic_mul(c, a, b);
+        RESET_ERROR_CODE();
+        // TODO
+        return 0;
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_algebraic_div(Z3_context c, Z3_ast a, Z3_ast b) {
+        Z3_TRY;
+        LOG_Z3_algebraic_div(c, a, b);
+        RESET_ERROR_CODE();
+        // TODO
+        return 0;
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_algebraic_root(Z3_context c, Z3_ast a, unsigned k) {
+        Z3_TRY;
+        LOG_Z3_algebraic_root(c, a, k);
+        RESET_ERROR_CODE();
+        // TODO
+        return 0;
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_algebraic_power(Z3_context c, Z3_ast a, unsigned k) {
+        Z3_TRY;
+        LOG_Z3_algebraic_power(c, a, k);
+        RESET_ERROR_CODE();
+        // TODO
+        return 0;
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_bool Z3_API Z3_algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b) {
+        Z3_TRY;
+        LOG_Z3_algebraic_lt(c, a, b);
+        RESET_ERROR_CODE();
+        // TODO
+        return Z3_FALSE;
+        Z3_CATCH_RETURN(Z3_FALSE);
+    }
+
+    Z3_bool Z3_API Z3_algebraic_gt(Z3_context c, Z3_ast a, Z3_ast b) {
+        Z3_TRY;
+        LOG_Z3_algebraic_gt(c, a, b);
+        RESET_ERROR_CODE();
+        // TODO
+        return Z3_FALSE;
+        Z3_CATCH_RETURN(Z3_FALSE);
+    }
+
+    Z3_bool Z3_API Z3_algebraic_le(Z3_context c, Z3_ast a, Z3_ast b) {
+        Z3_TRY;
+        LOG_Z3_algebraic_le(c, a, b);
+        RESET_ERROR_CODE();
+        // TODO
+        return Z3_FALSE;
+        Z3_CATCH_RETURN(Z3_FALSE);
+    }
+
+    Z3_bool Z3_API Z3_algebraic_ge(Z3_context c, Z3_ast a, Z3_ast b) {
+        Z3_TRY;
+        LOG_Z3_algebraic_ge(c, a, b);
+        RESET_ERROR_CODE();
+        // TODO
+        return Z3_FALSE;
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_bool Z3_API Z3_algebraic_eq(Z3_context c, Z3_ast a, Z3_ast b) {
+        Z3_TRY;
+        LOG_Z3_algebraic_eq(c, a, b);
+        RESET_ERROR_CODE();
+        // TODO
+        return Z3_FALSE;
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_bool Z3_API Z3_algebraic_neq(Z3_context c, Z3_ast a, Z3_ast b) {
+        Z3_TRY;
+        LOG_Z3_algebraic_neq(c, a, b);
+        RESET_ERROR_CODE();
+        // TODO
+        return Z3_FALSE;
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast_vector Z3_API Z3_algebraic_roots(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]) {
+        Z3_TRY;
+        LOG_Z3_algebraic_roots(c, p, n, a);
+        RESET_ERROR_CODE();
+        // TODO
+        return 0;
+        Z3_CATCH_RETURN(0);
+    }
+
+    int Z3_API Z3_algebraic_eval(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]) {
+        Z3_TRY;
+        LOG_Z3_algebraic_eval(c, p, n, a);
+        RESET_ERROR_CODE();
+        // TODO
+        return 0;
+        Z3_CATCH_RETURN(0);
+    }
+
+};

src/api/api_context.cpp

@@ -143,6 +143,7 @@ namespace api {
         {
             if (m_interruptable)
                 (*m_interruptable)();
+            m_manager.set_cancel(true);
         }
     }
     

src/api/z3.h

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

src/api/z3_algebraic.h

@@ -0,0 +1,226 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    z3_algebraic.h
+
+Abstract:
+
+    Additional APIs for handling Z3 algebraic numbers encoded as 
+    Z3_ASTs
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-12-07
+
+Notes:
+    
+--*/
+
+#ifndef _Z3_ALGEBRAIC_H_
+#define _Z3_ALGEBRAIC_H_
+
+#ifdef __cplusplus
+extern "C" {
+#endif // __cplusplus
+
+    /**
+       \brief Return Z3_TRUE if \c can be used as value in the Z3 real algebraic
+       number package.
+
+       def_API('Z3_algebraic_is_value', BOOL, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_bool Z3_API Z3_algebraic_is_value(__in Z3_context c, __in Z3_ast a);
+
+    /**
+       \brief Return the Z3_TRUE if \c a is positive, and Z3_FALSE otherwise.
+
+       \pre Z3_algebraic_is_value(c, a)
+
+       def_API('Z3_algebraic_is_pos', BOOL, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_bool Z3_API Z3_algebraic_is_pos(__in Z3_context c, __in Z3_ast a);
+
+    /**
+       \brief Return the Z3_TRUE if \c a is negative, and Z3_FALSE otherwise.
+
+       \pre Z3_algebraic_is_value(c, a)
+
+       def_API('Z3_algebraic_is_neg', BOOL, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_bool Z3_API Z3_algebraic_is_neg(__in Z3_context c, __in Z3_ast a);
+
+    /**
+       \brief Return the Z3_TRUE if \c a is zero, and Z3_FALSE otherwise.
+
+       \pre Z3_algebraic_is_value(c, a)
+
+       def_API('Z3_algebraic_is_zero', BOOL, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_bool Z3_API Z3_algebraic_is_zero(__in Z3_context c, __in Z3_ast a);
+
+    /**
+       \brief Return 1 if \c a is positive, 0 if \c a is zero, and -1 if \c a is negative.
+
+       \pre Z3_algebraic_is_value(c, a)
+
+       def_API('Z3_algebraic_sign', INT, (_in(CONTEXT), _in(AST)))
+    */
+    int Z3_API Z3_algebraic_sign(__in Z3_context c, __in Z3_ast a);
+
+    /**
+       \brief Return the value a + b. 
+
+       \pre Z3_algebraic_is_value(c, a)
+       \pre Z3_algebraic_is_value(c, b)
+       \post Z3_algebraic_is_value(c, result)
+
+       def_API('Z3_algebraic_add', AST, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_algebraic_add(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);    
+
+    /**
+       \brief Return the value a - b. 
+
+       \pre Z3_algebraic_is_value(c, a)
+       \pre Z3_algebraic_is_value(c, b)
+       \post Z3_algebraic_is_value(c, result)
+
+       def_API('Z3_algebraic_sub', AST, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_algebraic_sub(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);    
+
+    /**
+       \brief Return the value a * b. 
+
+       \pre Z3_algebraic_is_value(c, a)
+       \pre Z3_algebraic_is_value(c, b)
+       \post Z3_algebraic_is_value(c, result)
+
+       def_API('Z3_algebraic_mul', AST, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_algebraic_mul(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);    
+    
+    /**
+       \brief Return the value a / b. 
+
+       \pre Z3_algebraic_is_value(c, a)
+       \pre Z3_algebraic_is_value(c, b)
+       \pre !Z3_algebraic_is_zero(c, b)
+       \post Z3_algebraic_is_value(c, result)
+
+       def_API('Z3_algebraic_div', AST, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_algebraic_div(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);    
+    
+    /**
+       \brief Return the a^(1/k)
+
+       \pre Z3_algebraic_is_value(c, a)
+       \pre k is even => !Z3_algebraic_is_neg(c, a)
+       \post Z3_algebraic_is_value(c, result)
+
+       def_API('Z3_algebraic_root', AST, (_in(CONTEXT), _in(AST), _in(UINT)))
+    */
+    Z3_ast Z3_API Z3_algebraic_root(__in Z3_context c, __in Z3_ast a, __in unsigned k);
+
+    /**
+       \brief Return the a^k
+
+       \pre Z3_algebraic_is_value(c, a)
+       \post Z3_algebraic_is_value(c, result)
+
+       def_API('Z3_algebraic_power', AST, (_in(CONTEXT), _in(AST), _in(UINT)))
+    */
+    Z3_ast Z3_API Z3_algebraic_power(__in Z3_context c, __in Z3_ast a, __in unsigned k);
+    
+    /**
+       \brief Return Z3_TRUE if a < b, and Z3_FALSE otherwise.
+
+       \pre Z3_algebraic_is_value(c, a)
+       \pre Z3_algebraic_is_value(c, b)
+
+       def_API('Z3_algebraic_lt', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_bool Z3_API Z3_algebraic_lt(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);    
+    
+    /**
+       \brief Return Z3_TRUE if a > b, and Z3_FALSE otherwise.
+
+       \pre Z3_algebraic_is_value(c, a)
+       \pre Z3_algebraic_is_value(c, b)
+
+       def_API('Z3_algebraic_gt', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_bool Z3_API Z3_algebraic_gt(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);    
+
+    /**
+       \brief Return Z3_TRUE if a <= b, and Z3_FALSE otherwise.
+
+       \pre Z3_algebraic_is_value(c, a)
+       \pre Z3_algebraic_is_value(c, b)
+
+       def_API('Z3_algebraic_le', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_bool Z3_API Z3_algebraic_le(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);    
+
+    /**
+       \brief Return Z3_TRUE if a >= b, and Z3_FALSE otherwise.
+
+       \pre Z3_algebraic_is_value(c, a)
+       \pre Z3_algebraic_is_value(c, b)
+
+       def_API('Z3_algebraic_ge', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_bool Z3_API Z3_algebraic_ge(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);    
+
+    /**
+       \brief Return Z3_TRUE if a == b, and Z3_FALSE otherwise.
+
+       \pre Z3_algebraic_is_value(c, a)
+       \pre Z3_algebraic_is_value(c, b)
+
+       def_API('Z3_algebraic_eq', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_bool Z3_API Z3_algebraic_eq(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);    
+
+    /**
+       \brief Return Z3_TRUE if a != b, and Z3_FALSE otherwise.
+
+       \pre Z3_algebraic_is_value(c, a)
+       \pre Z3_algebraic_is_value(c, b)
+
+       def_API('Z3_algebraic_neq', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_bool Z3_API Z3_algebraic_neq(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);    
+
+    /**
+       \brief Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the 
+       roots of the univariate polynomial p(a[0], ..., a[n-1], x_n).
+       
+       \pre p is a Z3 expression that contains only arithmetic terms and free variables.
+       \pre forall i in [0, n) Z3_algebraic_is_value(c, a[i])
+       \post forall r in result Z3_algebraic_is_value(c, result)
+
+       def_API('Z3_algebraic_roots', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST)))
+    */
+    Z3_ast_vector Z3_API Z3_algebraic_roots(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[]);    
+
+    /**
+       \brief Given a multivariate polynomial p(x_0, ..., x_{n-1}), return the 
+       sign of p(a[0], ..., a[n-1]).
+       
+       \pre p is a Z3 expression that contains only arithmetic terms and free variables.
+       \pre forall i in [0, n) Z3_algebraic_is_value(c, a[i])
+
+       def_API('Z3_algebraic_eval', INT, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST)))
+    */
+    int Z3_API Z3_algebraic_eval(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[]);    
+
+
+#ifdef __cplusplus
+};
+#endif // __cplusplus
+
+#endif

src/ast/arith_decl_plugin.h

@@ -184,7 +184,7 @@ public:
 
     virtual expr * get_some_value(sort * s);
 
-    void set_cancel(bool f);
+    virtual void set_cancel(bool f);
 };
 
 class arith_util {

src/ast/ast.cpp

@@ -1336,6 +1336,12 @@ ast_manager::~ast_manager() {
     }
 }
 
+void ast_manager::set_cancel(bool f) {
+    for (unsigned i = 0; i < m_plugins.size(); i++) {
+        m_plugins[i]->set_cancel(f);
+    }
+}
+
 void ast_manager::compact_memory() {
     m_alloc.consolidate();
     unsigned capacity = m_ast_table.capacity();

src/ast/ast.h

@@ -921,6 +921,8 @@ public:
     virtual ~decl_plugin() {}
     virtual void finalize() {}
 
+    virtual void set_cancel(bool f) {}
+
     virtual decl_plugin * mk_fresh() = 0;
 
     family_id get_family_id() const { return m_family_id; }
@@ -1400,6 +1402,9 @@ public:
     ast_manager(ast_manager const & src, bool disable_proofs = false);
     ~ast_manager();
 
+    // propagate cancellation signal to decl_plugins
+    void set_cancel(bool f);
+
     bool has_trace_stream() const { return m_trace_stream != 0; }
     std::ostream & trace_stream() { SASSERT(has_trace_stream()); return *m_trace_stream; }