diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 707d067e2..3405d8751 100644 --- a/scripts/mk_project.py +++ b/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', diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp new file mode 100644 index 000000000..5511332b1 --- /dev/null +++ b/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 +#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); + } + +}; diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 69b7ea999..1d2b22059 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -143,6 +143,7 @@ namespace api { { if (m_interruptable) (*m_interruptable)(); + m_manager.set_cancel(true); } } diff --git a/src/api/z3.h b/src/api/z3.h index 8df894f40..15f0a5985 100644 --- a/src/api/z3.h +++ b/src/api/z3.h @@ -24,6 +24,7 @@ Notes: #include #include"z3_macros.h" #include"z3_api.h" +#include"z3_algebraic.h" #undef __in #undef __out diff --git a/src/api/z3_algebraic.h b/src/api/z3_algebraic.h new file mode 100644 index 000000000..eef791170 --- /dev/null +++ b/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 diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index b8ad11506..c39768d4c 100644 --- a/src/ast/arith_decl_plugin.h +++ b/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 { diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index bd5ffaf35..3fb422a2e 100644 --- a/src/ast/ast.cpp +++ b/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(); diff --git a/src/ast/ast.h b/src/ast/ast.h index 0ca47ccec..e9da41377 100644 --- a/src/ast/ast.h +++ b/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; }