diff --git a/scripts/update_api.py b/scripts/update_api.py index 6b953eefe3b..e9f01ebe6a6 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -54,6 +54,7 @@ ERROR_CODE = 11 DOUBLE = 12 FLOAT = 13 +CHAR = 14 FIRST_OBJ_ID = 100 @@ -62,33 +63,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' + PRINT_MODE : 'Z3_ast_print_mode', ERROR_CODE : 'Z3_error_code', CHAR: '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' + PRINT_MODE : 'ctypes.c_uint', ERROR_CODE : 'ctypes.c_uint', CHAR : 'ctypes.c_char' } # 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' } + PRINT_MODE : 'uint', ERROR_CODE : 'uint', CHAR : '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'} + BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char' } 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'} + BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint', CHAR : 'jchar'} # 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' } + BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char' } next_type_id = FIRST_OBJ_ID @@ -751,7 +752,7 @@ def mk_java(java_dir, package_name): Type2Napi = { VOID : '', VOID_PTR : '', INT : 'number', UINT : 'number', INT64 : 'number', UINT64 : 'number', DOUBLE : 'number', FLOAT : 'number', STRING : 'string', STRING_PTR : 'array', - BOOL : 'number', SYMBOL : 'external', PRINT_MODE : 'number', ERROR_CODE : 'number' } + BOOL : 'number', SYMBOL : 'external', PRINT_MODE : 'number', ERROR_CODE : 'number', CHAR : 'number' } def type2napi(t): try: @@ -761,7 +762,7 @@ def type2napi(t): Type2NapiBuilder = { VOID : '', VOID_PTR : '', INT : 'int32', UINT : 'uint32', INT64 : 'int64', UINT64 : 'uint64', DOUBLE : 'double', FLOAT : 'float', STRING : 'string', STRING_PTR : 'array', - BOOL : 'bool', SYMBOL : 'external', PRINT_MODE : 'int32', ERROR_CODE : 'int32' } + BOOL : 'bool', SYMBOL : 'external', PRINT_MODE : 'int32', ERROR_CODE : 'int32', CHAR : 'char' } def type2napibuilder(t): try: diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index d1816d807b3..33085c811cd 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -1278,6 +1278,7 @@ namespace qe { in->reset(); in->inc_depth(); result.push_back(in.get()); + std::cout << in->models_enabled() << " " << m_model_save.get() << "\n"; if (in->models_enabled()) { model_converter_ref mc; mc = model2model_converter(m_model_save.get()); diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 77d9a30f47e..a34dc787ab3 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -522,7 +522,7 @@ namespace smt { } instantiation_set const * get_uvar_inst_set(quantifier * q, unsigned i) const { - SASSERT(!has_quantifiers(q->get_expr())); + //SASSERT(!has_quantifiers(q->get_expr())); ast_idx_pair k(q, i); node * r = nullptr; if (m_uvars.find(k, r)) @@ -1735,12 +1735,6 @@ namespace smt { m_the_one(nullptr), m_uvar_inst_sets(nullptr) { if (has_quantifiers(q->get_expr()) && !m.is_lambda_def(q)) { - static bool displayed_flat_msg = false; - if (!displayed_flat_msg) { - // [Leo]: This warning message is not useful. - // warning_msg("For problems containing quantifiers, the model finding capabilities of Z3 work better when the formula does not contain nested quantifiers. You can use PULL_NESTED_QUANTIFIERS=true to eliminate nested quantifiers."); - displayed_flat_msg = true; - } proof_ref pr(m); expr_ref new_q(m); pull_quant pull(m); @@ -1753,7 +1747,7 @@ namespace smt { } CTRACE("model_finder_bug", has_quantifiers(m_flat_q->get_expr()), tout << mk_pp(q, m) << "\n" << mk_pp(m_flat_q, m) << "\n";); - SASSERT(m.is_lambda_def(q) || !has_quantifiers(m_flat_q->get_expr())); + // SASSERT(m.is_lambda_def(q) || !has_quantifiers(m_flat_q->get_expr())); } ~quantifier_info() { @@ -2200,7 +2194,7 @@ namespace smt { } else { SASSERT(is_quantifier(curr)); // no nested quantifiers - UNREACHABLE(); + //UNREACHABLE(); } } } @@ -2332,7 +2326,8 @@ namespace smt { } else { SASSERT(is_quantifier(curr)); - UNREACHABLE(); // can't happen, the quantifier is supposed to be flat. + SASSERT(is_lambda(curr)); + //UNREACHABLE(); // can't happen, the quantifier is supposed to be flat. } } } @@ -2385,7 +2380,7 @@ namespace smt { quantifier * q = d->get_flat_q(); if (m.is_lambda_def(q)) return; expr * e = q->get_expr(); - SASSERT(!has_quantifiers(e)); + //SASSERT(!has_quantifiers(e)); reset_cache(); SASSERT(m_ttodo.empty()); SASSERT(m_ftodo.empty());