diff --git a/scripts/update_api.py b/scripts/update_api.py index 64d6ea8c6a1..eeebfd0768c 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -55,6 +55,7 @@ DOUBLE = 12 FLOAT = 13 CHAR = 14 +CHAR_PTR = 15 FIRST_OBJ_ID = 100 @@ -63,33 +64,33 @@ def is_obj(ty): Type2Str = { VOID : 'void', VOID_PTR : 'void*', INT : 'int', UINT : 'unsigned', INT64 : 'int64_t', UINT64 : 'uint64_t', DOUBLE : 'double', FLOAT : 'float', STRING : 'Z3_string', STRING_PTR : 'Z3_string_ptr', BOOL : 'bool', SYMBOL : 'Z3_symbol', - PRINT_MODE : 'Z3_ast_print_mode', ERROR_CODE : 'Z3_error_code', CHAR: 'char' + PRINT_MODE : 'Z3_ast_print_mode', ERROR_CODE : 'Z3_error_code', CHAR: 'char', CHAR_PTR: 'char*' } Type2PyStr = { VOID_PTR : 'ctypes.c_void_p', INT : 'ctypes.c_int', UINT : 'ctypes.c_uint', INT64 : 'ctypes.c_longlong', UINT64 : 'ctypes.c_ulonglong', DOUBLE : 'ctypes.c_double', FLOAT : 'ctypes.c_float', STRING : 'ctypes.c_char_p', STRING_PTR : 'ctypes.POINTER(ctypes.c_char_p)', BOOL : 'ctypes.c_bool', SYMBOL : 'Symbol', - PRINT_MODE : 'ctypes.c_uint', ERROR_CODE : 'ctypes.c_uint', CHAR : 'ctypes.c_char' + PRINT_MODE : 'ctypes.c_uint', ERROR_CODE : 'ctypes.c_uint', CHAR : 'ctypes.c_char', CHAR_PTR: 'ctypes.c_char_p' } # Mapping to .NET types Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', INT64 : 'Int64', UINT64 : 'UInt64', DOUBLE : 'double', FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'byte', SYMBOL : 'IntPtr', - PRINT_MODE : 'uint', ERROR_CODE : 'uint', CHAR : 'char' } + PRINT_MODE : 'uint', ERROR_CODE : 'uint', CHAR : 'char', CHAR_PTR : 'char*' } # Mapping to Java types Type2Java = { VOID : 'void', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double', FLOAT : 'float', STRING : 'String', STRING_PTR : 'StringPtr', - BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char' } + BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'long' } Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', INT64 : 'jlong', UINT64 : 'jlong', DOUBLE : 'jdouble', FLOAT : 'jfloat', STRING : 'jstring', STRING_PTR : 'jobject', - BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint', CHAR : 'jchar'} + BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint', CHAR : 'jchar', CHAR_PTR : 'jlong'} # Mapping to ML types Type2ML = { VOID : 'unit', VOID_PTR : 'VOIDP', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float', FLOAT : 'float', STRING : 'string', STRING_PTR : 'char**', - BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char' } + BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'char*' } next_type_id = FIRST_OBJ_ID diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp index 69fde33a7f4..87f6efeb7af 100644 --- a/src/api/api_arith.cpp +++ b/src/api/api_arith.cpp @@ -88,6 +88,7 @@ extern "C" { MK_ARITH_PRED(Z3_mk_gt, OP_GT); MK_ARITH_PRED(Z3_mk_le, OP_LE); MK_ARITH_PRED(Z3_mk_ge, OP_GE); + MK_ARITH_PRED(Z3_mk_divides, OP_IDIVIDES); MK_UNARY(Z3_mk_int2real, mk_c(c)->get_arith_fid(), OP_TO_REAL, SKIP); MK_UNARY(Z3_mk_real2int, mk_c(c)->get_arith_fid(), OP_TO_INT, SKIP); MK_UNARY(Z3_mk_is_int, mk_c(c)->get_arith_fid(), OP_IS_INT, SKIP); diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index 00136c0215d..e8848b6600f 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -150,7 +150,7 @@ extern "C" { Z3_CATCH_RETURN(""); } - Z3_string Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned* length) { + Z3_char_ptr Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned* length) { Z3_TRY; LOG_Z3_get_lstring(c, s, length); RESET_ERROR_CODE(); diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 6909bb33d10..a575ec9a473 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -80,6 +80,7 @@ typedef bool Z3_bool; \brief Z3 string type. It is just an alias for \ccode{const char *}. */ typedef const char * Z3_string; +typedef char const* Z3_char_ptr; typedef Z3_string * Z3_string_ptr; /** @@ -2494,6 +2495,17 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2); + /** + \brief Create division predicate. + + The nodes \c t1 and \c t2 must be of integer sort. + The predicate is true when \c t1 divides \c t2. For the predicate to be part of + linear integer arithmetic, the first argument \c t1 must be a non-zero integer. + + def_API('Z3_mk_divides', AST, (_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_divides(Z3_context c, Z3_ast t1, Z3_ast t2); + /** \brief Coerce an integer to a real. @@ -3454,9 +3466,9 @@ extern "C" { \pre Z3_is_string(c, s) - def_API('Z3_get_lstring' ,STRING ,(_in(CONTEXT), _in(AST), _out(UINT))) + def_API('Z3_get_lstring' ,CHAR_PTR ,(_in(CONTEXT), _in(AST), _out(UINT))) */ - Z3_string Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned* length); + Z3_char_ptr Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned* length); /** \brief Create an empty sequence of the sequence sort \c seq. diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index aa650697d28..64973f7d13d 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -379,6 +379,7 @@ class arith_util : public arith_recognizers { app * mk_ge(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_GE, arg1, arg2); } app * mk_lt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LT, arg1, arg2); } app * mk_gt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_GT, arg1, arg2); } + app * mk_divides(expr* arg1, expr* arg2) { return m_manager.mk_app(m_afid, OP_IDIVIDES, arg1, arg2); } app * mk_add(unsigned num_args, expr * const * args) const { return num_args == 1 && is_app(args[0]) ? to_app(args[0]) : m_manager.mk_app(m_afid, OP_ADD, num_args, args); } app * mk_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2); }