diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 77f7702f2..b348e7d36 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -1,5 +1,7 @@ #include #include"z3++.h" + + using namespace z3; /** diff --git a/examples/interp/iz3.cpp b/examples/interp/iz3.cpp index fa7d8b896..6d631ebc9 100755 --- a/examples/interp/iz3.cpp +++ b/examples/interp/iz3.cpp @@ -90,12 +90,12 @@ int main(int argc, const char **argv) { /* Read an interpolation problem */ - int num; + unsigned num; Z3_ast *constraints; - int *parents = 0; + unsigned *parents = 0; const char *error; bool ok; - int num_theory; + unsigned num_theory; Z3_ast *theory; ok = Z3_read_interpolation_problem(ctx, &num, &constraints, tree_mode ? &parents : 0, filename, &error, &num_theory, &theory); @@ -144,7 +144,7 @@ int main(int argc, const char **argv) { if(!incremental_mode){ /* In non-incremental mode, we just pass the constraints. */ - result = Z3_interpolate(ctx, num, constraints, (unsigned int *)parents, options, interpolants, &model, 0, false, num_theory, theory); + result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, constraints, parents, options, interpolants, &model, 0, false, num_theory, theory); } else { @@ -165,7 +165,7 @@ int main(int argc, const char **argv) { for(int i = 0; i < num; i++){ asserted[i] = constraints[i]; Z3_assert_cnstr(ctx,constraints[i]); // assert one constraint - result = Z3_interpolate(ctx, num, &asserted[0], (unsigned int *)parents, options, interpolants, &model, 0, true, 0, 0); + result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, &asserted[0], parents, options, interpolants, &model, 0, true, 0, 0); if(result == Z3_L_FALSE){ for(unsigned j = 0; j < num-1; j++) /* Since we want the interpolant formulas to survive a "pop", we diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 6f8fe1f7f..170124bd8 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -75,7 +75,7 @@ def init_project_def(): # dll_name='foci2', # export_files=['foci2stub.cpp']) # add_lib('interp', ['solver','foci2']) - API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h'] + API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_interp.h'] add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure', 'interp'], includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files) add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3') diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 035cdd3c4..4641a7b1b 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -455,7 +455,7 @@ def display_help(exit_code): print(" -v, --vsproj generate Visual Studio Project Files.") if IS_WINDOWS: print(" -n, --nodotnet do not generate Microsoft.Z3.dll make rules.") - print(" -j, --java generate Java bindinds.") + print(" -j, --java generate Java bindings.") print(" --staticlib build Z3 static library.") if not IS_WINDOWS: print(" -g, --gmp use GMP.") @@ -587,7 +587,7 @@ def set_z3py_dir(p): raise MKException("Python bindings directory '%s' does not exist" % full) Z3PY_SRC_DIR = full if VERBOSE: - print("Python bindinds directory was detected.") + print("Python bindings directory was detected.") _UNIQ_ID = 0 @@ -1801,7 +1801,7 @@ def def_module_params(module_name, export, params, class_name=None, description= out.write(' {}\n') out.write(' static void collect_param_descrs(param_descrs & d) {\n') for param in params: - out.write(' d.insert("%s", %s, "%s", "%s");\n' % (param[0], TYPE2CPK[param[1]], param[3], pyg_default(param))) + out.write(' d.insert("%s", %s, "%s", "%s","%s");\n' % (param[0], TYPE2CPK[param[1]], param[3], pyg_default(param), module_name)) out.write(' }\n') if export: out.write(' /*\n') @@ -2522,7 +2522,11 @@ def mk_vs_proj(name, components): f.write(' \n') f.write(' Disabled\n') f.write(' WIN32;_DEBUG;Z3DEBUG;_TRACE;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)\n') - f.write(' true\n') + if VS_PAR: + f.write(' false\n') + f.write(' true\n') + else: + f.write(' true\n') f.write(' EnableFastChecks\n') f.write(' Level3\n') f.write(' MultiThreadedDebugDLL\n') @@ -2556,7 +2560,11 @@ def mk_vs_proj(name, components): f.write(' \n') f.write(' Disabled\n') f.write(' WIN32;_NDEBUG;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)\n') - f.write(' true\n') + if VS_PAR: + f.write(' false\n') + f.write(' true\n') + else: + f.write(' true\n') f.write(' EnableFastChecks\n') f.write(' Level3\n') f.write(' MultiThreadedDLL\n') diff --git a/scripts/update_api.py b/scripts/update_api.py index 97dacb44b..e08adf111 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -108,6 +108,7 @@ INOUT = 2 IN_ARRAY = 3 OUT_ARRAY = 4 INOUT_ARRAY = 5 +OUT_MANAGED_ARRAY = 6 # Primitive Types VOID = 0 @@ -131,13 +132,13 @@ def is_obj(ty): Type2Str = { VOID : 'void', VOID_PTR : 'void*', INT : 'int', UINT : 'unsigned', INT64 : '__int64', UINT64 : '__uint64', DOUBLE : 'double', STRING : 'Z3_string', STRING_PTR : 'Z3_string_ptr', BOOL : 'Z3_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' } 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', 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' } # Mapping to .NET types @@ -148,11 +149,11 @@ Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', # Mapping to Java types Type2Java = { VOID : 'void', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double', 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'} Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', INT64 : 'jlong', UINT64 : 'jlong', DOUBLE : 'jdouble', 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'} next_type_id = FIRST_OBJ_ID @@ -224,6 +225,10 @@ def _out_array2(cap, sz, ty): def _inout_array(sz, ty): return (INOUT_ARRAY, ty, sz, sz); +def _out_managed_array(sz,ty): + return (OUT_MANAGED_ARRAY, ty, 0, sz) + + def param_kind(p): return p[0] @@ -254,12 +259,14 @@ def param2dotnet(p): return "out IntPtr" else: return "[In, Out] ref %s" % type2dotnet(param_type(p)) - if k == IN_ARRAY: + elif k == IN_ARRAY: return "[In] %s[]" % type2dotnet(param_type(p)) - if k == INOUT_ARRAY: + elif k == INOUT_ARRAY: return "[In, Out] %s[]" % type2dotnet(param_type(p)) - if k == OUT_ARRAY: + elif k == OUT_ARRAY: return "[Out] %s[]" % type2dotnet(param_type(p)) + elif k == OUT_MANAGED_ARRAY: + return "[Out] out %s[]" % type2dotnet(param_type(p)) else: return type2dotnet(param_type(p)) @@ -268,7 +275,7 @@ def param2java(p): if k == OUT: if param_type(p) == INT or param_type(p) == UINT: return "IntPtr" - elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) >= FIRST_OBJ_ID: + elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) == VOID_PTR or param_type(p) >= FIRST_OBJ_ID: return "LongPtr" elif param_type(p) == STRING: return "StringPtr" @@ -276,8 +283,13 @@ def param2java(p): print("ERROR: unreachable code") assert(False) exit(1) - if k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: + elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: return "%s[]" % type2java(param_type(p)) + elif k == OUT_MANAGED_ARRAY: + if param_type(p) == UINT: + return "UIntArrayPtr" + else: + return "ObjArrayPtr" else: return type2java(param_type(p)) @@ -466,6 +478,8 @@ def mk_dotnet_wrappers(): dotnet.write('out '); else: dotnet.write('ref ') + elif param_kind(param) == OUT_MANAGED_ARRAY: + dotnet.write('out '); dotnet.write('a%d' % i) i = i + 1 dotnet.write(');\n'); @@ -522,6 +536,8 @@ def mk_java(): java_native.write(' public static class IntPtr { public int value; }\n') java_native.write(' public static class LongPtr { public long value; }\n') java_native.write(' public static class StringPtr { public String value; }\n') + java_native.write(' public static class ObjArrayPtr { public long[] value; }\n') + java_native.write(' public static class UIntArrayPtr { public int[] value; }\n') java_native.write(' public static native void setInternalErrorHandler(long ctx);\n\n') if IS_WINDOWS or os.uname()[0]=="CYGWIN": java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name) @@ -676,9 +692,11 @@ def mk_java(): if param_type(param) == INT or param_type(param) == UINT: java_wrapper.write(' jenv->GetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i)) else: - java_wrapper.write(' GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i)) + java_wrapper.write(' GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i)) elif k == IN and param_type(param) == STRING: java_wrapper.write(' Z3_string _a%s = (Z3_string) jenv->GetStringUTFChars(a%s, NULL);\n' % (i, i)) + elif k == OUT_MANAGED_ARRAY: + java_wrapper.write(' %s * _a%s = 0;\n' % (type2str(param_type(param)), i)) i = i + 1 # invoke procedure java_wrapper.write(' ') @@ -697,6 +715,8 @@ def mk_java(): java_wrapper.write('&_a%s' % i) elif k == OUT_ARRAY or k == IN_ARRAY or k == INOUT_ARRAY: java_wrapper.write('_a%s' % i) + elif k == OUT_MANAGED_ARRAY: + java_wrapper.write('&_a%s' % i) elif k == IN and param_type(param) == STRING: java_wrapper.write('_a%s' % i) else: @@ -732,6 +752,8 @@ def mk_java(): java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "J");\n') java_wrapper.write(' jenv->SetLongField(a%s, fid, (jlong) _a%s);\n' % (i, i)) java_wrapper.write(' }\n') + elif k == OUT_MANAGED_ARRAY: + java_wrapper.write(' *(jlong**)a%s = (jlong*)_a%s;\n' % (i, i)) i = i + 1 # return if result == STRING: @@ -932,6 +954,9 @@ def def_API(name, result, params): elif ty == INT64: log_c.write(" I(0);\n") exe_c.write("in.get_int64_addr(%s)" % i) + elif ty == VOID_PTR: + log_c.write(" P(0);\n") + exe_c.write("in.get_obj_addr(%s)" % i) else: error("unsupported parameter for %s, %s" % (name, p)) elif kind == IN_ARRAY or kind == INOUT_ARRAY: @@ -953,22 +978,43 @@ def def_API(name, result, params): log_c.write(" Au(a%s);\n" % sz) exe_c.write("in.get_uint_array(%s)" % i) else: - error ("unsupported parameter for %s, %s" % (name, p)) + error ("unsupported parameter for %s, %s" % (ty, name, p)) elif kind == OUT_ARRAY: sz = param_array_capacity_pos(p) - log_c.write(" for (unsigned i = 0; i < a%s; i++) { " % sz) + sz_p = params[sz] + sz_p_k = param_kind(sz_p) + tstr = type2str(ty) + if sz_p_k == OUT or sz_p_k == INOUT: + sz_e = ("(*a%s)" % sz) + else: + sz_e = ("a%s" % sz) + log_c.write(" for (unsigned i = 0; i < %s; i++) { " % sz_e) if is_obj(ty): log_c.write("P(0);") log_c.write(" }\n") - log_c.write(" Ap(a%s);\n" % sz) - exe_c.write("reinterpret_cast<%s*>(in.get_obj_array(%s))" % (type2str(ty), i)) + log_c.write(" Ap(%s);\n" % sz_e) + exe_c.write("reinterpret_cast<%s*>(in.get_obj_array(%s))" % (tstr, i)) elif ty == UINT: log_c.write("U(0);") log_c.write(" }\n") - log_c.write(" Au(a%s);\n" % sz) + log_c.write(" Au(%s);\n" % sz_e) exe_c.write("in.get_uint_array(%s)" % i) else: error ("unsupported parameter for %s, %s" % (name, p)) + elif kind == OUT_MANAGED_ARRAY: + sz = param_array_size_pos(p) + sz_p = params[sz] + sz_p_k = param_kind(sz_p) + tstr = type2str(ty) + if sz_p_k == OUT or sz_p_k == INOUT: + sz_e = ("(*a%s)" % sz) + else: + sz_e = ("a%s" % sz) + log_c.write(" for (unsigned i = 0; i < %s; i++) { " % sz_e) + log_c.write("P(0);") + log_c.write(" }\n") + log_c.write(" Ap(%s);\n" % sz_e) + exe_c.write("reinterpret_cast<%s**>(in.get_obj_array(%s))" % (tstr, i)) else: error ("unsupported parameter for %s, %s" % (name, p)) i = i + 1 diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 715732be6..c2864ca2d 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -208,7 +208,7 @@ extern "C" { MK_BINARY(Z3_mk_xor, mk_c(c)->get_basic_fid(), OP_XOR, SKIP); MK_NARY(Z3_mk_and, mk_c(c)->get_basic_fid(), OP_AND, SKIP); MK_NARY(Z3_mk_or, mk_c(c)->get_basic_fid(), OP_OR, SKIP); - MK_UNARY(Z3_mk_interp, mk_c(c)->get_basic_fid(), OP_INTERP, SKIP); + MK_UNARY(Z3_mk_interpolant, mk_c(c)->get_basic_fid(), OP_INTERP, SKIP); Z3_ast mk_ite_core(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3) { expr * result = mk_c(c)->m().mk_ite(to_expr(t1), to_expr(t2), to_expr(t3)); diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp index 48c2df4a9..c46e7363d 100644 --- a/src/api/api_config_params.cpp +++ b/src/api/api_config_params.cpp @@ -106,10 +106,4 @@ extern "C" { Z3_CATCH; } - Z3_bool Z3_API Z3_get_param_value(Z3_context c, Z3_string param_id, Z3_string* param_value) { - LOG_Z3_get_param_value(c, param_id, param_value); - // TODO - return Z3_FALSE; - } - }; diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 05e1ca675..b10621d43 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -128,6 +128,7 @@ namespace api { for (unsigned i = 0; i < m_replay_stack.size(); ++i) { dealloc(m_replay_stack[i]); } + m_ast_trail.reset(); } reset_parser(); dealloc(m_solver); @@ -342,24 +343,21 @@ namespace api { void context::push() { get_smt_kernel().push(); - if (!m_user_ref_count) { - m_ast_lim.push_back(m_ast_trail.size()); - m_replay_stack.push_back(0); - } + m_ast_lim.push_back(m_ast_trail.size()); + m_replay_stack.push_back(0); } void context::pop(unsigned num_scopes) { for (unsigned i = 0; i < num_scopes; ++i) { - if (!m_user_ref_count) { - unsigned sz = m_ast_lim.back(); - m_ast_lim.pop_back(); - dealloc(m_replay_stack.back()); - m_replay_stack.pop_back(); - while (m_ast_trail.size() > sz) { - m_ast_trail.pop_back(); - } + unsigned sz = m_ast_lim.back(); + m_ast_lim.pop_back(); + dealloc(m_replay_stack.back()); + m_replay_stack.pop_back(); + while (m_ast_trail.size() > sz) { + m_ast_trail.pop_back(); } } + SASSERT(num_scopes <= get_smt_kernel().get_scope_level()); get_smt_kernel().pop(num_scopes); } diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 03d5ff843..dbf68da38 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -3,14 +3,14 @@ Copyright (c) 2011 Microsoft Corporation Module Name: - api_interp.cpp +api_interp.cpp Abstract: - API for interpolation +API for interpolation Author: - Ken McMillan +Ken McMillan Revision History: @@ -45,669 +45,676 @@ using namespace stl_ext; // WARNING: don't make a hash_map with this if the range type // has a destructor: you'll get an address dependency!!! namespace stl_ext { - template <> - class hash { - public: - size_t operator()(const Z3_ast p) const { - return (size_t) p; - } - }; + template <> + class hash < Z3_ast > { + public: + size_t operator()(const Z3_ast p) const { + return (size_t)p; + } + }; } typedef interpolation_options_struct *Z3_interpolation_options; extern "C" { - Z3_context Z3_mk_interpolation_context(Z3_config cfg){ - if(!cfg) cfg = Z3_mk_config(); - Z3_set_param_value(cfg, "PROOF", "true"); - Z3_set_param_value(cfg, "MODEL", "true"); - // Z3_set_param_value(cfg, "PRE_SIMPLIFIER","false"); - // Z3_set_param_value(cfg, "SIMPLIFY_CLAUSES","false"); - - Z3_context ctx = Z3_mk_context(cfg); - Z3_del_config(cfg); - return ctx; - } - - void Z3_interpolate_proof(Z3_context ctx, - Z3_ast proof, - int num, - Z3_ast *cnsts, - unsigned *parents, - Z3_params options, - Z3_ast *interps, - int num_theory, - Z3_ast *theory - ){ + Z3_context Z3_mk_interpolation_context(Z3_config cfg){ + if (!cfg) cfg = Z3_mk_config(); + Z3_set_param_value(cfg, "PROOF", "true"); + Z3_set_param_value(cfg, "MODEL", "true"); + // Z3_set_param_value(cfg, "PRE_SIMPLIFIER","false"); + // Z3_set_param_value(cfg, "SIMPLIFY_CLAUSES","false"); - if(num > 1){ // if we have interpolants to compute - - ptr_vector pre_cnsts_vec(num); // get constraints in a vector - for(int i = 0; i < num; i++){ - ast *a = to_ast(cnsts[i]); - pre_cnsts_vec[i] = a; - } - - ::vector pre_parents_vec; // get parents in a vector - if(parents){ - pre_parents_vec.resize(num); - for(int i = 0; i < num; i++) - pre_parents_vec[i] = parents[i]; + Z3_context ctx = Z3_mk_context(cfg); + Z3_del_config(cfg); + return ctx; + } + + void Z3_interpolate_proof(Z3_context ctx, + Z3_ast proof, + int num, + Z3_ast *cnsts, + unsigned *parents, + Z3_params options, + Z3_ast *interps, + int num_theory, + Z3_ast *theory) + { + + if (num > 1){ // if we have interpolants to compute + + ptr_vector pre_cnsts_vec(num); // get constraints in a vector + for (int i = 0; i < num; i++){ + ast *a = to_ast(cnsts[i]); + pre_cnsts_vec[i] = a; + } + + ::vector pre_parents_vec; // get parents in a vector + if (parents){ + pre_parents_vec.resize(num); + for (int i = 0; i < num; i++) + pre_parents_vec[i] = parents[i]; + } + + ptr_vector theory_vec; // get background theory in a vector + if (theory){ + theory_vec.resize(num_theory); + for (int i = 0; i < num_theory; i++) + theory_vec[i] = to_ast(theory[i]); + } + + ptr_vector interpolants(num - 1); // make space for result + + ast_manager &_m = mk_c(ctx)->m(); + iz3interpolate(_m, + to_ast(proof), + pre_cnsts_vec, + pre_parents_vec, + interpolants, + theory_vec, + 0); // ignore params for now FIXME + + // copy result back + for (unsigned i = 0; i < interpolants.size(); i++){ + mk_c(ctx)->save_ast_trail(interpolants[i]); + interps[i] = of_ast(interpolants[i]); + _m.dec_ref(interpolants[i]); + } } - - ptr_vector theory_vec; // get background theory in a vector - if(theory){ - theory_vec.resize(num_theory); - for(int i = 0; i < num_theory; i++) - theory_vec[i] = to_ast(theory[i]); - } - - ptr_vector interpolants(num-1); // make space for result - - ast_manager &_m = mk_c(ctx)->m(); - iz3interpolate(_m, - to_ast(proof), - pre_cnsts_vec, - pre_parents_vec, - interpolants, - theory_vec, - 0); // ignore params for now FIXME + } - // copy result back - for(unsigned i = 0; i < interpolants.size(); i++){ - mk_c(ctx)->save_ast_trail(interpolants[i]); - interps[i] = of_ast(interpolants[i]); - _m.dec_ref(interpolants[i]); - } - } - } + static std::ostringstream itp_err; - Z3_lbool Z3_interpolate(Z3_context ctx, - int num, - Z3_ast *cnsts, - unsigned *parents, - Z3_params options, - Z3_ast *interps, - Z3_model *model, - Z3_literals *labels, - int incremental, - int num_theory, - Z3_ast *theory - ){ + int Z3_check_interpolant(Z3_context ctx, + unsigned num, + Z3_ast *cnsts, + unsigned *parents, + Z3_ast *itp, + Z3_string *error, + unsigned num_theory, + Z3_ast *theory){ - - profiling::timer_start("Solve"); + ast_manager &_m = mk_c(ctx)->m(); + itp_err.clear(); - if(!incremental){ + // need a solver -- make one here, but how? + params_ref p = params_ref::get_empty(); //FIXME + scoped_ptr sf(mk_smt_solver_factory()); + scoped_ptr sp((*(sf))(_m, p, false, true, false, symbol("AUFLIA"))); - profiling::timer_start("Z3 assert"); + ptr_vector cnsts_vec(num); // get constraints in a vector + for (unsigned i = 0; i < num; i++){ + ast *a = to_ast(cnsts[i]); + cnsts_vec[i] = a; + } - Z3_push(ctx); // so we can rewind later - - for(int i = 0; i < num; i++) - Z3_assert_cnstr(ctx,cnsts[i]); // assert all the constraints + ptr_vector itp_vec(num); // get interpolants in a vector + for (unsigned i = 0; i < num - 1; i++){ + ast *a = to_ast(itp[i]); + itp_vec[i] = a; + } - if(theory){ - for(int i = 0; i < num_theory; i++) - Z3_assert_cnstr(ctx,theory[i]); - } + ::vector parents_vec; // get parents in a vector + if (parents){ + parents_vec.resize(num); + for (unsigned i = 0; i < num; i++) + parents_vec[i] = parents[i]; + } - profiling::timer_stop("Z3 assert"); + ptr_vector theory_vec; // get background theory in a vector + if (theory){ + theory_vec.resize(num_theory); + for (unsigned i = 0; i < num_theory; i++) + theory_vec[i] = to_ast(theory[i]); + } + + bool res = iz3check(_m, + sp.get(), + itp_err, + cnsts_vec, + parents_vec, + itp_vec, + theory_vec); + + *error = res ? 0 : itp_err.str().c_str(); + return res; } - // Get a proof of unsat - - Z3_ast proof; - Z3_lbool result; - - profiling::timer_start("Z3 solving"); - result = Z3_check_assumptions(ctx, 0, 0, model, &proof, 0, 0); - profiling::timer_stop("Z3 solving"); - - switch (result) { - case Z3_L_FALSE: - - Z3_interpolate_proof(ctx, - proof, - num, - cnsts, - parents, - options, - interps, - num_theory, - theory); + static std::string Z3_profile_string; - if(!incremental) - for(int i = 0; i < num-1; i++) - Z3_persist_ast(ctx,interps[i],1); - break; - - case Z3_L_UNDEF: - if(labels) - *labels = Z3_get_relevant_labels(ctx); - break; - - case Z3_L_TRUE: - if(labels) - *labels = Z3_get_relevant_labels(ctx); - break; + Z3_string Z3_interpolation_profile(Z3_context ctx){ + std::ostringstream f; + profiling::print(f); + Z3_profile_string = f.str(); + return Z3_profile_string.c_str(); } - profiling::timer_start("Z3 pop"); - if(!incremental) - Z3_pop(ctx,1); - profiling::timer_stop("Z3 pop"); - profiling::timer_stop("Solve"); - - return result; - - } - - static std::ostringstream itp_err; - - int Z3_check_interpolant(Z3_context ctx, - int num, - Z3_ast *cnsts, - int *parents, - Z3_ast *itp, - const char **error, - int num_theory, - Z3_ast *theory){ - - ast_manager &_m = mk_c(ctx)->m(); - itp_err.clear(); - - // need a solver -- make one here, but how? - params_ref p = params_ref::get_empty(); //FIXME - scoped_ptr sf(mk_smt_solver_factory()); - scoped_ptr sp((*(sf))(_m, p, false, true, false, symbol("AUFLIA"))); - - ptr_vector cnsts_vec(num); // get constraints in a vector - for(int i = 0; i < num; i++){ - ast *a = to_ast(cnsts[i]); - cnsts_vec[i] = a; - } - - ptr_vector itp_vec(num); // get interpolants in a vector - for(int i = 0; i < num-1; i++){ - ast *a = to_ast(itp[i]); - itp_vec[i] = a; + Z3_interpolation_options + Z3_mk_interpolation_options(){ + return (Z3_interpolation_options) new interpolation_options_struct; } - ::vector parents_vec; // get parents in a vector - if(parents){ - parents_vec.resize(num); - for(int i = 0; i < num; i++) - parents_vec[i] = parents[i]; - } - - ptr_vector theory_vec; // get background theory in a vector - if(theory){ - theory_vec.resize(num_theory); - for(int i = 0; i < num_theory; i++) - theory_vec[i] = to_ast(theory[i]); - } - - bool res = iz3check(_m, - sp.get(), - itp_err, - cnsts_vec, - parents_vec, - itp_vec, - theory_vec); - - *error = res ? 0 : itp_err.str().c_str(); - return res; - } - - - static std::string Z3_profile_string; - - Z3_string Z3_interpolation_profile(Z3_context ctx){ - std::ostringstream f; - profiling::print(f); - Z3_profile_string = f.str(); - return Z3_profile_string.c_str(); - } - - - Z3_interpolation_options - Z3_mk_interpolation_options(){ - return (Z3_interpolation_options) new interpolation_options_struct; - } - - void - Z3_del_interpolation_options(Z3_interpolation_options opts){ - delete opts; - } - - void - Z3_set_interpolation_option(Z3_interpolation_options opts, - Z3_string name, - Z3_string value){ - opts->map[name] = value; - } - - Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p){ - Z3_TRY; - LOG_Z3_get_interpolant(c, pf, pat, p); - RESET_ERROR_CODE(); - - Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m()); - mk_c(c)->save_object(v); - - ast *_pf = to_ast(pf); - ast *_pat = to_ast(pat); - - ptr_vector interp; - ptr_vector cnsts; // to throw away - - ast_manager &_m = mk_c(c)->m(); - - iz3interpolate(_m, - _pf, - cnsts, - _pat, - interp, - (interpolation_options_struct *) 0 // ignore params for now - ); - - // copy result back - for(unsigned i = 0; i < interp.size(); i++){ - v->m_ast_vector.push_back(interp[i]); - _m.dec_ref(interp[i]); - } - RETURN_Z3(of_ast_vector(v)); - Z3_CATCH_RETURN(0); - } - - Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *out_interp, __out Z3_model *model){ - Z3_TRY; - LOG_Z3_compute_interpolant(c, pat, p, out_interp, model); - RESET_ERROR_CODE(); - - - // params_ref &_p = to_params(p)->m_params; - params_ref _p; - _p.set_bool("proof", true); // this is currently useless - - scoped_proof_mode spm(mk_c(c)->m(),PGM_FINE); - scoped_ptr sf = mk_smt_solver_factory(); - scoped_ptr m_solver((*sf)(mk_c(c)->m(), _p, true, true, true, ::symbol::null)); - m_solver.get()->updt_params(_p); // why do we have to do this? - - ast *_pat = to_ast(pat); - - ptr_vector interp; - ptr_vector cnsts; // to throw away - - ast_manager &_m = mk_c(c)->m(); - - model_ref m; - lbool _status = iz3interpolate(_m, - *(m_solver.get()), - _pat, - cnsts, - interp, - m, - 0 // ignore params for now - ); - - Z3_lbool status = of_lbool(_status); - - Z3_ast_vector_ref *v = 0; - *model = 0; - - if(_status == l_false){ - // copy result back - v = alloc(Z3_ast_vector_ref, mk_c(c)->m()); - mk_c(c)->save_object(v); - for(unsigned i = 0; i < interp.size(); i++){ - v->m_ast_vector.push_back(interp[i]); - _m.dec_ref(interp[i]); - } - } - else { - model_ref _m; - m_solver.get()->get_model(_m); - Z3_model_ref *crap = alloc(Z3_model_ref); - crap->m_model = _m.get(); - mk_c(c)->save_object(crap); - *model = of_model(crap); + void + Z3_del_interpolation_options(Z3_interpolation_options opts){ + delete opts; } - *out_interp = of_ast_vector(v); - - return status; - Z3_CATCH_RETURN(Z3_L_UNDEF); - } + void + Z3_set_interpolation_option(Z3_interpolation_options opts, + Z3_string name, + Z3_string value){ + opts->map[name] = value; + } + + Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p){ + Z3_TRY; + LOG_Z3_get_interpolant(c, pf, pat, p); + RESET_ERROR_CODE(); + + Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m()); + mk_c(c)->save_object(v); + + ast *_pf = to_ast(pf); + ast *_pat = to_ast(pat); + + ptr_vector interp; + ptr_vector cnsts; // to throw away + + ast_manager &_m = mk_c(c)->m(); + + iz3interpolate(_m, + _pf, + cnsts, + _pat, + interp, + (interpolation_options_struct *)0 // ignore params for now + ); + + // copy result back + for (unsigned i = 0; i < interp.size(); i++){ + v->m_ast_vector.push_back(interp[i]); + _m.dec_ref(interp[i]); + } + RETURN_Z3(of_ast_vector(v)); + Z3_CATCH_RETURN(0); + } + + Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *out_interp, __out Z3_model *model){ + Z3_TRY; + LOG_Z3_compute_interpolant(c, pat, p, out_interp, model); + RESET_ERROR_CODE(); + + + // params_ref &_p = to_params(p)->m_params; + params_ref _p; + _p.set_bool("proof", true); // this is currently useless + + scoped_proof_mode spm(mk_c(c)->m(), PGM_FINE); + scoped_ptr sf = mk_smt_solver_factory(); + scoped_ptr m_solver((*sf)(mk_c(c)->m(), _p, true, true, true, ::symbol::null)); + m_solver.get()->updt_params(_p); // why do we have to do this? + + ast *_pat = to_ast(pat); + + ptr_vector interp; + ptr_vector cnsts; // to throw away + + ast_manager &_m = mk_c(c)->m(); + + model_ref m; + lbool _status = iz3interpolate(_m, + *(m_solver.get()), + _pat, + cnsts, + interp, + m, + 0 // ignore params for now + ); + + Z3_lbool status = of_lbool(_status); + + Z3_ast_vector_ref *v = 0; + *model = 0; + + if (_status == l_false){ + // copy result back + v = alloc(Z3_ast_vector_ref, mk_c(c)->m()); + mk_c(c)->save_object(v); + for (unsigned i = 0; i < interp.size(); i++){ + v->m_ast_vector.push_back(interp[i]); + _m.dec_ref(interp[i]); + } + } + else { + model_ref _m; + m_solver.get()->get_model(_m); + Z3_model_ref *crap = alloc(Z3_model_ref); + crap->m_model = _m.get(); + mk_c(c)->save_object(crap); + *model = of_model(crap); + } + + *out_interp = of_ast_vector(v); + + return status; + Z3_CATCH_RETURN(Z3_L_UNDEF); + } }; static void tokenize(const std::string &str, std::vector &tokens){ - for(unsigned i = 0; i < str.size();){ - if(str[i] == ' '){i++; continue;} - unsigned beg = i; - while(i < str.size() && str[i] != ' ')i++; - if(i > beg) - tokens.push_back(str.substr(beg,i-beg)); - } + for (unsigned i = 0; i < str.size();){ + if (str[i] == ' '){ i++; continue; } + unsigned beg = i; + while (i < str.size() && str[i] != ' ')i++; + if (i > beg) + tokens.push_back(str.substr(beg, i - beg)); + } } -static void get_file_params(const char *filename, hash_map ¶ms){ - std::ifstream f(filename); - if(f){ - std::string first_line; - std::getline(f,first_line); - // std::cout << "first line: '" << first_line << "'" << std::endl; - if(first_line.size() >= 2 && first_line[0] == ';' && first_line[1] == '!'){ - std::vector tokens; - tokenize(first_line.substr(2,first_line.size()-2),tokens); - for(unsigned i = 0; i < tokens.size(); i++){ - std::string &tok = tokens[i]; - size_t eqpos = tok.find('='); - if(eqpos >= 0 && eqpos < tok.size()){ - std::string left = tok.substr(0,eqpos); - std::string right = tok.substr(eqpos+1,tok.size()-eqpos-1); - params[left] = right; +static void get_file_params(const char *filename, hash_map ¶ms){ + std::ifstream f(filename); + if (f){ + std::string first_line; + std::getline(f, first_line); + // std::cout << "first line: '" << first_line << "'" << std::endl; + if (first_line.size() >= 2 && first_line[0] == ';' && first_line[1] == '!'){ + std::vector tokens; + tokenize(first_line.substr(2, first_line.size() - 2), tokens); + for (unsigned i = 0; i < tokens.size(); i++){ + std::string &tok = tokens[i]; + size_t eqpos = tok.find('='); + if (eqpos != std::string::npos){ + std::string left = tok.substr(0, eqpos); + std::string right = tok.substr(eqpos + 1, tok.size() - eqpos - 1); + params[left] = right; + } + } } - } + f.close(); } - f.close(); - } } extern "C" { #if 0 - static void iZ3_write_seq(Z3_context ctx, int num, Z3_ast *cnsts, const char *filename, int num_theory, Z3_ast *theory){ - int num_fmlas = num+num_theory; - std::vector fmlas(num_fmlas); - if(num_theory) - std::copy(theory,theory+num_theory,fmlas.begin()); - for(int i = 0; i < num_theory; i++) - fmlas[i] = Z3_mk_implies(ctx,Z3_mk_true(ctx),fmlas[i]); - std::copy(cnsts,cnsts+num,fmlas.begin()+num_theory); - Z3_string smt = Z3_benchmark_to_smtlib_string(ctx,"none","AUFLIA","unknown","",num_fmlas-1,&fmlas[0],fmlas[num_fmlas-1]); - std::ofstream f(filename); - if(num_theory) - f << ";! THEORY=" << num_theory << "\n"; - f << smt; - f.close(); - } + static void iZ3_write_seq(Z3_context ctx, int num, Z3_ast *cnsts, const char *filename, int num_theory, Z3_ast *theory){ + int num_fmlas = num+num_theory; + std::vector fmlas(num_fmlas); + if(num_theory) + std::copy(theory,theory+num_theory,fmlas.begin()); + for(int i = 0; i < num_theory; i++) + fmlas[i] = Z3_mk_implies(ctx,Z3_mk_true(ctx),fmlas[i]); + std::copy(cnsts,cnsts+num,fmlas.begin()+num_theory); + Z3_string smt = Z3_benchmark_to_smtlib_string(ctx,"none","AUFLIA","unknown","",num_fmlas-1,&fmlas[0],fmlas[num_fmlas-1]); + std::ofstream f(filename); + if(num_theory) + f << ";! THEORY=" << num_theory << "\n"; + f << smt; + f.close(); + } - void Z3_write_interpolation_problem(Z3_context ctx, int num, Z3_ast *cnsts, int *parents, const char *filename, int num_theory, Z3_ast *theory){ - if(!parents){ - iZ3_write_seq(ctx,num,cnsts,filename,num_theory,theory); - return; + void Z3_write_interpolation_problem(Z3_context ctx, int num, Z3_ast *cnsts, unsigned *parents, const char *filename, int num_theory, Z3_ast *theory){ + if(!parents){ + iZ3_write_seq(ctx,num,cnsts,filename,num_theory,theory); + return; + } + std::vector tcnsts(num); + hash_map syms; + for(int j = 0; j < num - 1; j++){ + std::ostringstream oss; + oss << "$P" << j; + std::string name = oss.str(); + Z3_symbol s = Z3_mk_string_symbol(ctx, name.c_str()); + Z3_ast symbol = Z3_mk_const(ctx, s, Z3_mk_bool_sort(ctx)); + syms[j] = symbol; + tcnsts[j] = Z3_mk_implies(ctx,cnsts[j],symbol); + } + tcnsts[num-1] = Z3_mk_implies(ctx,cnsts[num-1],Z3_mk_false(ctx)); + for(int j = num-2; j >= 0; j--){ + int parent = parents[j]; + // assert(parent >= 0 && parent < num); + tcnsts[parent] = Z3_mk_implies(ctx,syms[j],tcnsts[parent]); + } + iZ3_write_seq(ctx,num,&tcnsts[0],filename,num_theory,theory); } - std::vector tcnsts(num); - hash_map syms; - for(int j = 0; j < num - 1; j++){ - std::ostringstream oss; - oss << "$P" << j; - std::string name = oss.str(); - Z3_symbol s = Z3_mk_string_symbol(ctx, name.c_str()); - Z3_ast symbol = Z3_mk_const(ctx, s, Z3_mk_bool_sort(ctx)); - syms[j] = symbol; - tcnsts[j] = Z3_mk_implies(ctx,cnsts[j],symbol); - } - tcnsts[num-1] = Z3_mk_implies(ctx,cnsts[num-1],Z3_mk_false(ctx)); - for(int j = num-2; j >= 0; j--){ - int parent = parents[j]; - // assert(parent >= 0 && parent < num); - tcnsts[parent] = Z3_mk_implies(ctx,syms[j],tcnsts[parent]); - } - iZ3_write_seq(ctx,num,&tcnsts[0],filename,num_theory,theory); - } #else - static Z3_ast and_vec(Z3_context ctx,svector &c){ - return (c.size() > 1) ? Z3_mk_and(ctx,c.size(),&c[0]) : c[0]; - } - - static Z3_ast parents_vector_to_tree(Z3_context ctx, int num, Z3_ast *cnsts, int *parents){ - Z3_ast res; - if(!parents){ - res = Z3_mk_interp(ctx,cnsts[0]); - for(int i = 1; i < num-1; i++){ - Z3_ast bar[2] = {res,cnsts[i]}; - res = Z3_mk_interp(ctx,Z3_mk_and(ctx,2,bar)); - } - if(num > 1){ - Z3_ast bar[2] = {res,cnsts[num-1]}; - res = Z3_mk_and(ctx,2,bar); - } + static Z3_ast and_vec(Z3_context ctx, svector &c){ + return (c.size() > 1) ? Z3_mk_and(ctx, c.size(), &c[0]) : c[0]; } - else { - std::vector > chs(num); - for(int i = 0; i < num-1; i++){ - svector &c = chs[i]; - c.push_back(cnsts[i]); - Z3_ast foo = Z3_mk_interp(ctx,and_vec(ctx,c)); - chs[parents[i]].push_back(foo); - } - { - svector &c = chs[num-1]; - c.push_back(cnsts[num-1]); - res = and_vec(ctx,c); - } - } - Z3_inc_ref(ctx,res); - return res; - } - void Z3_write_interpolation_problem(Z3_context ctx, int num, Z3_ast *cnsts, int *parents, const char *filename, int num_theory, Z3_ast *theory){ - std::ofstream f(filename); - if(num > 0){ - ptr_vector cnsts_vec(num); // get constraints in a vector - for(int i = 0; i < num; i++){ - expr *a = to_expr(cnsts[i]); - cnsts_vec[i] = a; + static Z3_ast parents_vector_to_tree(Z3_context ctx, int num, Z3_ast *cnsts, unsigned *parents){ + Z3_ast res; + if (!parents){ + res = Z3_mk_interpolant(ctx, cnsts[0]); + for (int i = 1; i < num - 1; i++){ + Z3_ast bar[2] = { res, cnsts[i] }; + res = Z3_mk_interpolant(ctx, Z3_mk_and(ctx, 2, bar)); + } + if (num > 1){ + Z3_ast bar[2] = { res, cnsts[num - 1] }; + res = Z3_mk_and(ctx, 2, bar); + } + } + else { + std::vector > chs(num); + for (int i = 0; i < num - 1; i++){ + svector &c = chs[i]; + c.push_back(cnsts[i]); + Z3_ast foo = Z3_mk_interpolant(ctx, and_vec(ctx, c)); + chs[parents[i]].push_back(foo); + } + { + svector &c = chs[num - 1]; + c.push_back(cnsts[num - 1]); + res = and_vec(ctx, c); } - Z3_ast tree = parents_vector_to_tree(ctx,num,cnsts,parents); - for(int i = 0; i < num_theory; i++){ - expr *a = to_expr(theory[i]); - cnsts_vec.push_back(a); - } - iz3pp(mk_c(ctx)->m(),cnsts_vec,to_expr(tree),f); - Z3_dec_ref(ctx,tree); + } + Z3_inc_ref(ctx, res); + return res; } - f.close(); + + void Z3_write_interpolation_problem(Z3_context ctx, unsigned num, Z3_ast *cnsts, unsigned *parents, const char *filename, unsigned num_theory, Z3_ast *theory){ + std::ofstream f(filename); + if (num > 0){ +#if 0 + // Suggested shorthand: + ptr_vector cnsts_vec; + cnsts_vec.append(num, to_exprs(cnsts)); + cnsts_vec.append(num_theory, to_exprs(theory)); +#endif + ptr_vector cnsts_vec(num); // get constraints in a vector + for (unsigned i = 0; i < num; i++){ + expr *a = to_expr(cnsts[i]); + cnsts_vec[i] = a; + } + for (unsigned i = 0; i < num_theory; i++){ + expr *a = to_expr(theory[i]); + cnsts_vec.push_back(a); + } + Z3_ast tree = parents_vector_to_tree(ctx, num, cnsts, parents); + iz3pp(mk_c(ctx)->m(), cnsts_vec, to_expr(tree), f); + Z3_dec_ref(ctx, tree); + } + f.close(); #if 0 - - if(!parents){ - iZ3_write_seq(ctx,num,cnsts,filename,num_theory,theory); - return; - } - std::vector tcnsts(num); - hash_map syms; - for(int j = 0; j < num - 1; j++){ - std::ostringstream oss; - oss << "$P" << j; - std::string name = oss.str(); - Z3_symbol s = Z3_mk_string_symbol(ctx, name.c_str()); - Z3_ast symbol = Z3_mk_const(ctx, s, Z3_mk_bool_sort(ctx)); - syms[j] = symbol; - tcnsts[j] = Z3_mk_implies(ctx,cnsts[j],symbol); - } - tcnsts[num-1] = Z3_mk_implies(ctx,cnsts[num-1],Z3_mk_false(ctx)); - for(int j = num-2; j >= 0; j--){ - int parent = parents[j]; - // assert(parent >= 0 && parent < num); - tcnsts[parent] = Z3_mk_implies(ctx,syms[j],tcnsts[parent]); - } - iZ3_write_seq(ctx,num,&tcnsts[0],filename,num_theory,theory); + + if(!parents){ + iZ3_write_seq(ctx,num,cnsts,filename,num_theory,theory); + return; + } + std::vector tcnsts(num); + hash_map syms; + for(int j = 0; j < num - 1; j++){ + std::ostringstream oss; + oss << "$P" << j; + std::string name = oss.str(); + Z3_symbol s = Z3_mk_string_symbol(ctx, name.c_str()); + Z3_ast symbol = Z3_mk_const(ctx, s, Z3_mk_bool_sort(ctx)); + syms[j] = symbol; + tcnsts[j] = Z3_mk_implies(ctx,cnsts[j],symbol); + } + tcnsts[num-1] = Z3_mk_implies(ctx,cnsts[num-1],Z3_mk_false(ctx)); + for(int j = num-2; j >= 0; j--){ + int parent = parents[j]; + // assert(parent >= 0 && parent < num); + tcnsts[parent] = Z3_mk_implies(ctx,syms[j],tcnsts[parent]); + } + iZ3_write_seq(ctx,num,&tcnsts[0],filename,num_theory,theory); #endif - } + } #endif - static std::vector read_cnsts; - static std::vector read_parents; - static std::ostringstream read_error; - static std::string read_msg; - static std::vector read_theory; + static std::vector read_cnsts; + static std::vector read_parents; + static std::ostringstream read_error; + static std::string read_msg; + static std::vector read_theory; - static bool iZ3_parse(Z3_context ctx, const char *filename, const char **error, svector &assertions){ - read_error.clear(); - try { - std::string foo(filename); - if(foo.size() >= 5 && foo.substr(foo.size()-5) == ".smt2"){ - Z3_ast ass = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0); - Z3_app app = Z3_to_app(ctx,ass); - int nconjs = Z3_get_app_num_args(ctx,app); - assertions.resize(nconjs); - for(int k = 0; k < nconjs; k++) - assertions[k] = Z3_get_app_arg(ctx,app,k); - } - else { - Z3_parse_smtlib_file(ctx, filename, 0, 0, 0, 0, 0, 0); - int numa = Z3_get_smtlib_num_assumptions(ctx); - int numf = Z3_get_smtlib_num_formulas(ctx); - int num = numa + numf; - - assertions.resize(num); - for(int j = 0; j < num; j++){ - if(j < numa) - assertions[j] = Z3_get_smtlib_assumption(ctx,j); - else - assertions[j] = Z3_get_smtlib_formula(ctx,j-numa); - } - } - } - catch(...) { - read_error << "SMTLIB parse error: " << Z3_get_smtlib_error(ctx); - read_msg = read_error.str(); - *error = read_msg.c_str(); - return false; - } - Z3_set_error_handler(ctx, 0); - return true; - } - + static bool iZ3_parse(Z3_context ctx, const char *filename, const char **error, svector &assertions){ + read_error.clear(); + try { + std::string foo(filename); + if (foo.size() >= 5 && foo.substr(foo.size() - 5) == ".smt2"){ + Z3_ast ass = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0); + Z3_app app = Z3_to_app(ctx, ass); + int nconjs = Z3_get_app_num_args(ctx, app); + assertions.resize(nconjs); + for (int k = 0; k < nconjs; k++) + assertions[k] = Z3_get_app_arg(ctx, app, k); + } + else { + Z3_parse_smtlib_file(ctx, filename, 0, 0, 0, 0, 0, 0); + int numa = Z3_get_smtlib_num_assumptions(ctx); + int numf = Z3_get_smtlib_num_formulas(ctx); + int num = numa + numf; - int Z3_read_interpolation_problem(Z3_context ctx, int *_num, Z3_ast **cnsts, int **parents, const char *filename, const char **error, int *ret_num_theory, Z3_ast **theory ){ - - hash_map file_params; - get_file_params(filename,file_params); - - unsigned num_theory = 0; - if(file_params.find("THEORY") != file_params.end()) - num_theory = atoi(file_params["THEORY"].c_str()); - - svector assertions; - if(!iZ3_parse(ctx,filename,error,assertions)) - return false; - - if(num_theory > assertions.size()) - num_theory = assertions.size(); - unsigned num = assertions.size() - num_theory; - - read_cnsts.resize(num); - read_parents.resize(num); - read_theory.resize(num_theory); - - for(unsigned j = 0; j < num_theory; j++) - read_theory[j] = assertions[j]; - for(unsigned j = 0; j < num; j++) - read_cnsts[j] = assertions[j+num_theory]; - - if(ret_num_theory) - *ret_num_theory = num_theory; - if(theory) - *theory = &read_theory[0]; - - if(!parents){ - *_num = num; - *cnsts = &read_cnsts[0]; - return true; + assertions.resize(num); + for (int j = 0; j < num; j++){ + if (j < numa) + assertions[j] = Z3_get_smtlib_assumption(ctx, j); + else + assertions[j] = Z3_get_smtlib_formula(ctx, j - numa); + } + } + } + catch (...) { + read_error << "SMTLIB parse error: " << Z3_get_smtlib_error(ctx); + read_msg = read_error.str(); + *error = read_msg.c_str(); + return false; + } + Z3_set_error_handler(ctx, 0); + return true; } - for(unsigned j = 0; j < num; j++) - read_parents[j] = SHRT_MAX; - - hash_map pred_map; - for(unsigned j = 0; j < num; j++){ - Z3_ast lhs = 0, rhs = read_cnsts[j]; + int Z3_read_interpolation_problem(Z3_context ctx, unsigned *_num, Z3_ast *cnsts[], unsigned *parents[], const char *filename, Z3_string_ptr error, unsigned *ret_num_theory, Z3_ast *theory[]){ - if(Z3_get_decl_kind(ctx,Z3_get_app_decl(ctx,Z3_to_app(ctx,rhs))) == Z3_OP_IMPLIES){ - Z3_app app1 = Z3_to_app(ctx,rhs); - Z3_ast lhs1 = Z3_get_app_arg(ctx,app1,0); - Z3_ast rhs1 = Z3_get_app_arg(ctx,app1,1); - if(Z3_get_decl_kind(ctx,Z3_get_app_decl(ctx,Z3_to_app(ctx,lhs1))) == Z3_OP_AND){ - Z3_app app2 = Z3_to_app(ctx,lhs1); - int nconjs = Z3_get_app_num_args(ctx,app2); - for(int k = nconjs - 1; k >= 0; --k) - rhs1 = Z3_mk_implies(ctx,Z3_get_app_arg(ctx,app2,k),rhs1); - rhs = rhs1; - } - } + hash_map file_params; + get_file_params(filename, file_params); + + unsigned num_theory = 0; + if (file_params.find("THEORY") != file_params.end()) + num_theory = atoi(file_params["THEORY"].c_str()); + + svector assertions; + if (!iZ3_parse(ctx, filename, error, assertions)) + return false; + + if (num_theory > assertions.size()) + num_theory = assertions.size(); + unsigned num = assertions.size() - num_theory; + + read_cnsts.resize(num); + read_parents.resize(num); + read_theory.resize(num_theory); + + for (unsigned j = 0; j < num_theory; j++) + read_theory[j] = assertions[j]; + for (unsigned j = 0; j < num; j++) + read_cnsts[j] = assertions[j + num_theory]; + + if (ret_num_theory) + *ret_num_theory = num_theory; + if (theory) + *theory = &read_theory[0]; + + if (!parents){ + *_num = num; + *cnsts = &read_cnsts[0]; + return true; + } + + for (unsigned j = 0; j < num; j++) + read_parents[j] = SHRT_MAX; + + hash_map pred_map; + + for (unsigned j = 0; j < num; j++){ + Z3_ast lhs = 0, rhs = read_cnsts[j]; + + if (Z3_get_decl_kind(ctx, Z3_get_app_decl(ctx, Z3_to_app(ctx, rhs))) == Z3_OP_IMPLIES){ + Z3_app app1 = Z3_to_app(ctx, rhs); + Z3_ast lhs1 = Z3_get_app_arg(ctx, app1, 0); + Z3_ast rhs1 = Z3_get_app_arg(ctx, app1, 1); + if (Z3_get_decl_kind(ctx, Z3_get_app_decl(ctx, Z3_to_app(ctx, lhs1))) == Z3_OP_AND){ + Z3_app app2 = Z3_to_app(ctx, lhs1); + int nconjs = Z3_get_app_num_args(ctx, app2); + for (int k = nconjs - 1; k >= 0; --k) + rhs1 = Z3_mk_implies(ctx, Z3_get_app_arg(ctx, app2, k), rhs1); + rhs = rhs1; + } + } + + while (1){ + Z3_app app = Z3_to_app(ctx, rhs); + Z3_func_decl func = Z3_get_app_decl(ctx, app); + Z3_decl_kind dk = Z3_get_decl_kind(ctx, func); + if (dk == Z3_OP_IMPLIES){ + if (lhs){ + Z3_ast child = lhs; + if (pred_map.find(child) == pred_map.end()){ + read_error << "formula " << j + 1 << ": unknown: " << Z3_ast_to_string(ctx, child); + goto fail; + } + int child_num = pred_map[child]; + if (read_parents[child_num] != SHRT_MAX){ + read_error << "formula " << j + 1 << ": multiple reference: " << Z3_ast_to_string(ctx, child); + goto fail; + } + read_parents[child_num] = j; + } + lhs = Z3_get_app_arg(ctx, app, 0); + rhs = Z3_get_app_arg(ctx, app, 1); + } + else { + if (!lhs){ + read_error << "formula " << j + 1 << ": should be (implies {children} fmla parent)"; + goto fail; + } + read_cnsts[j] = lhs; + Z3_ast name = rhs; + if (pred_map.find(name) != pred_map.end()){ + read_error << "formula " << j + 1 << ": duplicate symbol"; + goto fail; + } + pred_map[name] = j; + break; + } + } + } + + for (unsigned j = 0; j < num - 1; j++) + if (read_parents[j] == SHRT_MIN){ + read_error << "formula " << j + 1 << ": unreferenced"; + goto fail; + } + + *_num = num; + *cnsts = &read_cnsts[0]; + *parents = &read_parents[0]; + return true; + + fail: + read_msg = read_error.str(); + *error = read_msg.c_str(); + return false; - while(1){ - Z3_app app = Z3_to_app(ctx,rhs); - Z3_func_decl func = Z3_get_app_decl(ctx,app); - Z3_decl_kind dk = Z3_get_decl_kind(ctx,func); - if(dk == Z3_OP_IMPLIES){ - if(lhs){ - Z3_ast child = lhs; - if(pred_map.find(child) == pred_map.end()){ - read_error << "formula " << j+1 << ": unknown: " << Z3_ast_to_string(ctx,child); - goto fail; - } - int child_num = pred_map[child]; - if(read_parents[child_num] != SHRT_MAX){ - read_error << "formula " << j+1 << ": multiple reference: " << Z3_ast_to_string(ctx,child); - goto fail; - } - read_parents[child_num] = j; - } - lhs = Z3_get_app_arg(ctx,app,0); - rhs = Z3_get_app_arg(ctx,app,1); - } - else { - if(!lhs){ - read_error << "formula " << j+1 << ": should be (implies {children} fmla parent)"; - goto fail; - } - read_cnsts[j] = lhs; - Z3_ast name = rhs; - if(pred_map.find(name) != pred_map.end()){ - read_error << "formula " << j+1 << ": duplicate symbol"; - goto fail; - } - pred_map[name] = j; - break; - } - } } - - for(unsigned j = 0; j < num-1; j++) - if(read_parents[j] == SHRT_MIN){ - read_error << "formula " << j+1 << ": unreferenced"; - goto fail; - } - - *_num = num; - *cnsts = &read_cnsts[0]; - *parents = &read_parents[0]; - return true; - - fail: - read_msg = read_error.str(); - *error = read_msg.c_str(); - return false; - - } } + + +#if 0 +/** Constant reprepresenting a root of a formula tree for tree interpolation */ +#define IZ3_ROOT SHRT_MAX + +/** This function uses Z3 to determine satisfiability of a set of +constraints. If UNSAT, an interpolant is returned, based on the +refutation generated by Z3. If SAT, a model is returned. + +If "parents" is non-null, computes a tree interpolant. The tree is +defined by the array "parents". This array maps each formula in +the tree to its parent, where formulas are indicated by their +integer index in "cnsts". The parent of formula n must have index +greater than n. The last formula is the root of the tree. Its +parent entry should be the constant IZ3_ROOT. + +If "parents" is null, computes a sequence interpolant. + +\param ctx The Z3 context. Must be generated by iz3_mk_context +\param num The number of constraints in the sequence +\param cnsts Array of constraints (AST's in context ctx) +\param parents The parents vector defining the tree structure +\param options Interpolation options (may be NULL) +\param interps Array to return interpolants (size at least num-1, may be NULL) +\param model Returns a Z3 model if constraints SAT (may be NULL) +\param labels Returns relevant labels if SAT (may be NULL) +\param incremental + +VERY IMPORTANT: All the Z3 formulas in cnsts must be in Z3 +context ctx. The model and interpolants returned are also +in this context. + +The return code is as in Z3_check_assumptions, that is, + +Z3_L_FALSE = constraints UNSAT (interpolants returned) +Z3_L_TRUE = constraints SAT (model returned) +Z3_L_UNDEF = Z3 produced no result, or interpolation not possible + +Currently, this function supports integer and boolean variables, +as well as arrays over these types, with linear arithmetic, +uninterpreted functions and quantifiers over integers (that is +AUFLIA). Interpolants are produced in AULIA. However, some +uses of array operations may cause quantifiers to appear in the +interpolants even when there are no quantifiers in the input formulas. +Although quantifiers may appear in the input formulas, Z3 may give up in +this case, returning Z3_L_UNDEF. + +If "incremental" is true, cnsts must contain exactly the set of +formulas that are currently asserted in the context. If false, +there must be no formulas currently asserted in the context. +Setting "incremental" to true makes it posisble to incrementally +add and remove constraints from the context until the context +becomes UNSAT, at which point an interpolant is computed. Caution +must be used, however. Before popping the context, if you wish to +keep the interolant formulas, you *must* preserve them by using +Z3_persist_ast. Also, if you want to simplify the interpolant +formulas using Z3_simplify, you must first pop all of the +assertions in the context (or use a different context). Otherwise, +the formulas will be simplified *relative* to these constraints, +which is almost certainly not what you want. + + +Current limitations on tree interpolants. In a tree interpolation +problem, each constant (0-ary function symbol) must occur only +along one path from root to leaf. Function symbols (of arity > 0) +are considered to have global scope (i.e., may appear in any +interpolant formula). + +def_API('Z3_interpolate', BOOL, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in(PARAMS), _out_array(1, AST), _out(MODEL), _out(LITERALS), _in(UINT), _in(UINT), _in_array(9, AST))) +*/ + +Z3_lbool Z3_API Z3_interpolate(__in Z3_context ctx, + __in unsigned num, + __in_ecount(num) Z3_ast *cnsts, + __in_ecount(num) unsigned *parents, + __in Z3_params options, + __out_ecount(num - 1) Z3_ast *interps, + __out Z3_model *model, + __out Z3_literals *labels, + __in unsigned incremental, + __in unsigned num_theory, + __in_ecount(num_theory) Z3_ast *theory); +#endif \ No newline at end of file diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index f17f7a586..f0c31d800 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -60,6 +60,7 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } + mk_c(c)->save_ast_trail(r); RETURN_Z3(of_expr(r)); Z3_CATCH_RETURN(0); } @@ -263,6 +264,7 @@ extern "C" { RESET_ERROR_CODE(); CHECK_NON_NULL(f, 0); expr * e = to_func_interp_ref(f)->get_else(); + mk_c(c)->save_ast_trail(e); RETURN_Z3(of_expr(e)); Z3_CATCH_RETURN(0); } @@ -301,6 +303,7 @@ extern "C" { LOG_Z3_func_entry_get_value(c, e); RESET_ERROR_CODE(); expr * v = to_func_entry_ref(e)->get_result(); + mk_c(c)->save_ast_trail(v); RETURN_Z3(of_expr(v)); Z3_CATCH_RETURN(0); } diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index c8b1723f1..e57050e82 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -40,6 +40,11 @@ extern "C" { params_ref p = s->m_params; mk_c(c)->params().get_solver_params(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled); s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic); + + param_descrs r; + s->m_solver->collect_param_descrs(r); + context_params::collect_solver_param_descrs(r); + p.validate(r); s->m_solver->updt_params(p); } @@ -102,6 +107,7 @@ extern "C" { if (!initialized) init_solver(c, s); to_solver_ref(s)->collect_param_descrs(descrs); + context_params::collect_solver_param_descrs(descrs); if (!initialized) to_solver(s)->m_solver = 0; descrs.display(buffer); @@ -119,6 +125,7 @@ extern "C" { if (!initialized) init_solver(c, s); to_solver_ref(s)->collect_param_descrs(d->m_descrs); + context_params::collect_solver_param_descrs(d->m_descrs); if (!initialized) to_solver(s)->m_solver = 0; Z3_param_descrs r = of_param_descrs(d); @@ -130,14 +137,19 @@ extern "C" { Z3_TRY; LOG_Z3_solver_set_params(c, s, p); RESET_ERROR_CODE(); + if (to_solver(s)->m_solver) { bool old_model = to_solver(s)->m_params.get_bool("model", true); bool new_model = to_param_ref(p).get_bool("model", true); if (old_model != new_model) to_solver_ref(s)->set_produce_models(new_model); + param_descrs r; + to_solver_ref(s)->collect_param_descrs(r); + context_params::collect_solver_param_descrs(r); + to_param_ref(p).validate(r); to_solver_ref(s)->updt_params(to_param_ref(p)); } - to_solver(s)->m_params = to_param_ref(p); + to_solver(s)->m_params.append(to_param_ref(p)); Z3_CATCH; } diff --git a/src/api/api_solver_old.cpp b/src/api/api_solver_old.cpp index e0533fbd9..b81fb2f2c 100644 --- a/src/api/api_solver_old.cpp +++ b/src/api/api_solver_old.cpp @@ -40,7 +40,7 @@ extern "C" { LOG_Z3_pop(c, num_scopes); RESET_ERROR_CODE(); CHECK_SEARCHING(c); - if (num_scopes > mk_c(c)->get_smt_kernel().get_scope_level()) { + if (num_scopes > mk_c(c)->get_num_scopes()) { SET_ERROR_CODE(Z3_IOB); return; } diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index 911360047..adfd0fb71 100644 --- a/src/api/api_tactic.cpp +++ b/src/api/api_tactic.cpp @@ -222,6 +222,9 @@ extern "C" { Z3_TRY; LOG_Z3_tactic_using_params(c, t, p); RESET_ERROR_CODE(); + param_descrs r; + to_tactic_ref(t)->collect_param_descrs(r); + to_param_ref(p).validate(r); tactic * new_t = using_params(to_tactic_ref(t), to_param_ref(p)); RETURN_TACTIC(new_t); Z3_CATCH_RETURN(0); @@ -447,6 +450,9 @@ extern "C" { Z3_TRY; LOG_Z3_tactic_apply_ex(c, t, g, p); RESET_ERROR_CODE(); + param_descrs pd; + to_tactic_ref(t)->collect_param_descrs(pd); + to_param_ref(p).validate(pd); Z3_apply_result r = _tactic_apply(c, t, g, to_param_ref(p)); RETURN_Z3(r); Z3_CATCH_RETURN(0); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 8f228cdba..c35208d86 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -85,6 +85,8 @@ namespace z3 { friend std::ostream & operator<<(std::ostream & out, exception const & e) { out << e.msg(); return out; } }; + + /** \brief Z3 global configuration object. */ @@ -269,8 +271,9 @@ namespace z3 { object(object const & s):m_ctx(s.m_ctx) {} context & ctx() const { return *m_ctx; } void check_error() const { m_ctx->check_error(); } - friend void check_context(object const & a, object const & b) { assert(a.m_ctx == b.m_ctx); } + friend void check_context(object const & a, object const & b); }; + inline void check_context(object const & a, object const & b) { assert(a.m_ctx == b.m_ctx); } class symbol : public object { Z3_symbol m_sym; @@ -282,7 +285,7 @@ namespace z3 { Z3_symbol_kind kind() const { return Z3_get_symbol_kind(ctx(), m_sym); } std::string str() const { assert(kind() == Z3_STRING_SYMBOL); return Z3_get_symbol_string(ctx(), m_sym); } int to_int() const { assert(kind() == Z3_INT_SYMBOL); return Z3_get_symbol_int(ctx(), m_sym); } - friend std::ostream & operator<<(std::ostream & out, symbol const & s) { + friend std::ostream & operator<<(std::ostream & out, symbol const & s) { if (s.kind() == Z3_INT_SYMBOL) out << "k!" << s.to_int(); else @@ -291,6 +294,7 @@ namespace z3 { } }; + class params : public object { Z3_params m_params; public: @@ -309,7 +313,9 @@ namespace z3 { void set(char const * k, unsigned n) { Z3_params_set_uint(ctx(), m_params, ctx().str_symbol(k), n); } void set(char const * k, double n) { Z3_params_set_double(ctx(), m_params, ctx().str_symbol(k), n); } void set(char const * k, symbol const & s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), s); } - friend std::ostream & operator<<(std::ostream & out, params const & p) { out << Z3_params_to_string(p.ctx(), p); return out; } + friend std::ostream & operator<<(std::ostream & out, params const & p) { + out << Z3_params_to_string(p.ctx(), p); return out; + } }; class ast : public object { @@ -325,14 +331,19 @@ namespace z3 { ast & operator=(ast const & s) { Z3_inc_ref(s.ctx(), s.m_ast); if (m_ast) Z3_dec_ref(ctx(), m_ast); m_ctx = s.m_ctx; m_ast = s.m_ast; return *this; } Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; } unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; } - friend std::ostream & operator<<(std::ostream & out, ast const & n) { out << Z3_ast_to_string(n.ctx(), n.m_ast); return out; } + friend std::ostream & operator<<(std::ostream & out, ast const & n) { + out << Z3_ast_to_string(n.ctx(), n.m_ast); return out; + } /** \brief Return true if the ASTs are structurally identical. */ - friend bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b) != 0; } + friend bool eq(ast const & a, ast const & b); }; + inline bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b) != 0; } + + /** \brief A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort. */ @@ -570,6 +581,7 @@ namespace z3 { return expr(a.ctx(), r); } + /** \brief Return an expression representing a and b. @@ -585,6 +597,7 @@ namespace z3 { return expr(a.ctx(), r); } + /** \brief Return an expression representing a and b. The C++ Boolean value \c b is automatically converted into a Z3 Boolean constant. @@ -636,21 +649,10 @@ namespace z3 { a.check_error(); return expr(a.ctx(), r); } - friend expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); } - friend expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); } + friend expr implies(expr const & a, bool b); + friend expr implies(bool a, expr const & b); - /** - \brief Create the if-then-else expression ite(c, t, e) - - \pre c.is_bool() - */ - friend expr ite(expr const & c, expr const & t, expr const & e) { - check_context(c, t); check_context(c, e); - assert(c.is_bool()); - Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e); - c.check_error(); - return expr(c.ctx(), r); - } + friend expr ite(expr const & c, expr const & t, expr const & e); friend expr distinct(expr_vector const& args); @@ -716,15 +718,9 @@ namespace z3 { /** \brief Power operator */ - friend expr pw(expr const & a, expr const & b) { - assert(a.is_arith() && b.is_arith()); - check_context(a, b); - Z3_ast r = Z3_mk_power(a.ctx(), a, b); - a.check_error(); - return expr(a.ctx(), r); - } - friend expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); } - friend expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); } + friend expr pw(expr const & a, expr const & b); + friend expr pw(expr const & a, int b); + friend expr pw(int a, expr const & b); friend expr operator/(expr const & a, expr const & b) { check_context(a, b); @@ -891,6 +887,38 @@ namespace z3 { expr substitute(expr_vector const& dst); }; + + inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); } + inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); } + + inline expr pw(expr const & a, expr const & b) { + assert(a.is_arith() && b.is_arith()); + check_context(a, b); + Z3_ast r = Z3_mk_power(a.ctx(), a, b); + a.check_error(); + return expr(a.ctx(), r); + } + inline expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); } + inline expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); } + + + + + + /** + \brief Create the if-then-else expression ite(c, t, e) + + \pre c.is_bool() + */ + + inline expr ite(expr const & c, expr const & t, expr const & e) { + check_context(c, t); check_context(c, e); + assert(c.is_bool()); + Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e); + c.check_error(); + return expr(c.ctx(), r); + } + /** \brief Wraps a Z3_ast as an expr object. It also checks for errors. @@ -1404,22 +1432,28 @@ namespace z3 { t1.check_error(); return tactic(t1.ctx(), r); } - friend tactic repeat(tactic const & t, unsigned max=UINT_MAX) { - Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max); - t.check_error(); - return tactic(t.ctx(), r); - } - friend tactic with(tactic const & t, params const & p) { - Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p); - t.check_error(); - return tactic(t.ctx(), r); - } - friend tactic try_for(tactic const & t, unsigned ms) { - Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms); - t.check_error(); - return tactic(t.ctx(), r); - } + friend tactic repeat(tactic const & t, unsigned max); + friend tactic with(tactic const & t, params const & p); + friend tactic try_for(tactic const & t, unsigned ms); }; + + inline tactic repeat(tactic const & t, unsigned max=UINT_MAX) { + Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max); + t.check_error(); + return tactic(t.ctx(), r); + } + + inline tactic with(tactic const & t, params const & p) { + Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p); + t.check_error(); + return tactic(t.ctx(), r); + } + inline tactic try_for(tactic const & t, unsigned ms) { + Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms); + t.check_error(); + return tactic(t.ctx(), r); + } + class probe : public object { Z3_probe m_probe; diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 2b88cbab7..1c03d76b6 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -3527,28 +3527,11 @@ namespace Microsoft.Z3 /// Only a few configuration parameters are mutable once the context is created. /// An exception is thrown when trying to modify an immutable parameter. /// - /// public void UpdateParamValue(string id, string value) { Native.Z3_update_param_value(nCtx, id, value); } - /// - /// Get a configuration parameter. - /// - /// - /// Returns null if the parameter value does not exist. - /// - /// - public string GetParamValue(string id) - { - IntPtr res = IntPtr.Zero; - if (Native.Z3_get_param_value(nCtx, id, out res) == 0) - return null; - else - return Marshal.PtrToStringAnsi(res); - } - #endregion #region Internal diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index c8fdfb51f..f4a63a61b 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -323,6 +323,14 @@ namespace Microsoft.Z3 #endregion + #region Interpolation + /// + /// Indicates whether the term is marked for interpolation. + /// + /// + public bool IsInterpolant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INTERP; } } + #endregion + #region Arithmetic Terms /// /// Indicates whether the term is of integer sort. @@ -791,7 +799,7 @@ namespace Microsoft.Z3 /// /// A label literal has a set of string parameters. It takes no arguments. public bool IsLabelLit { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } } - #endregion + #endregion #region Proof Terms /// diff --git a/src/api/dotnet/InterpolationContext.cs b/src/api/dotnet/InterpolationContext.cs new file mode 100644 index 000000000..b5ada1bbd --- /dev/null +++ b/src/api/dotnet/InterpolationContext.cs @@ -0,0 +1,162 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Diagnostics.Contracts; +using System.Runtime.InteropServices; + +namespace Microsoft.Z3 +{ + /// + /// The InterpolationContext is suitable for generation of interpolants. + /// + /// For more information on interpolation please refer + /// too the C/C++ API, which is well documented. + [ContractVerification(true)] + class InterpolationContext : Context + { + + /// + /// Constructor. + /// + public InterpolationContext() : base() { } + + /// + /// Constructor. + /// + /// + public InterpolationContext(Dictionary settings) : base(settings) { } + + #region Terms + /// + /// Create an expression that marks a formula position for interpolation. + /// + public BoolExpr MkInterpolant(BoolExpr a) + { + Contract.Requires(a != null); + Contract.Ensures(Contract.Result() != null); + + CheckContextMatch(a); + return new BoolExpr(this, Native.Z3_mk_interpolant(nCtx, a.NativeObject)); + } + #endregion + + /// + /// Computes an interpolant. + /// + /// For more information on interpolation please refer + /// too the function Z3_get_interpolant in the C/C++ API, which is + /// well documented. + Expr[] GetInterpolant(Expr pf, Expr pat, Params p) + { + Contract.Requires(pf != null); + Contract.Requires(pat != null); + Contract.Requires(p != null); + Contract.Ensures(Contract.Result() != null); + + CheckContextMatch(pf); + CheckContextMatch(pat); + CheckContextMatch(p); + + ASTVector seq = new ASTVector(this, Native.Z3_get_interpolant(nCtx, pf.NativeObject, pat.NativeObject, p.NativeObject)); + uint n = seq.Size; + Expr[] res = new Expr[n]; + for (uint i = 0; i < n; i++) + res[i] = Expr.Create(this, seq[i].NativeObject); + return res; + } + + /// + /// Computes an interpolant. + /// + /// For more information on interpolation please refer + /// too the function Z3_compute_interpolant in the C/C++ API, which is + /// well documented. + Z3_lbool ComputeInterpolant(Expr pat, Params p, out ASTVector interp, out Model model) + { + Contract.Requires(pat != null); + Contract.Requires(p != null); + Contract.Ensures(Contract.ValueAtReturn(out interp) != null); + Contract.Ensures(Contract.ValueAtReturn(out model) != null); + + CheckContextMatch(pat); + CheckContextMatch(p); + + IntPtr i = IntPtr.Zero, m = IntPtr.Zero; + int r = Native.Z3_compute_interpolant(nCtx, pat.NativeObject, p.NativeObject, ref i, ref m); + interp = new ASTVector(this, i); + model = new Model(this, m); + return (Z3_lbool)r; + } + + /// + /// Return a string summarizing cumulative time used for interpolation. + /// + /// For more information on interpolation please refer + /// too the function Z3_interpolation_profile in the C/C++ API, which is + /// well documented. + public string InterpolationProfile() + { + return Native.Z3_interpolation_profile(nCtx); + } + + /// + /// Checks the correctness of an interpolant. + /// + /// For more information on interpolation please refer + /// too the function Z3_check_interpolant in the C/C++ API, which is + /// well documented. + public int CheckInterpolant(Expr[] cnsts, uint[] parents, Expr[] interps, out string error, Expr[] theory) + { + Contract.Requires(cnsts.Length == parents.Length); + Contract.Requires(cnsts.Length == interps.Length + 1); + IntPtr n_err_str; + int r = Native.Z3_check_interpolant(nCtx, + (uint)cnsts.Length, + Expr.ArrayToNative(cnsts), + parents, + Expr.ArrayToNative(interps), + out n_err_str, + (uint)theory.Length, + Expr.ArrayToNative(theory)); + error = Marshal.PtrToStringAnsi(n_err_str); + return r; + } + + /// + /// Reads an interpolation problem from a file. + /// + /// For more information on interpolation please refer + /// too the function Z3_read_interpolation_problem in the C/C++ API, which is + /// well documented. + public int ReadInterpolationProblem(string filename, out Expr[] cnsts, out uint[] parents, out string error, out Expr[] theory) + { + uint num = 0, num_theory = 0; + IntPtr[] n_cnsts; + IntPtr[] n_theory; + IntPtr n_err_str; + int r = Native.Z3_read_interpolation_problem(nCtx, ref num, out n_cnsts, out parents, filename, out n_err_str, ref num_theory, out n_theory); + error = Marshal.PtrToStringAnsi(n_err_str); + cnsts = new Expr[num]; + parents = new uint[num]; + theory = new Expr[num_theory]; + for (int i = 0; i < num; i++) + cnsts[i] = Expr.Create(this, n_cnsts[i]); + for (int i = 0; i < num_theory; i++) + theory[i] = Expr.Create(this, n_theory[i]); + return r; + } + + /// + /// Writes an interpolation problem to a file. + /// + /// For more information on interpolation please refer + /// too the function Z3_write_interpolation_problem in the C/C++ API, which is + /// well documented. + public void WriteInterpolationProblem(string filename, Expr[] cnsts, uint[] parents, Expr[] theory) + { + Contract.Requires(cnsts.Length == parents.Length); + Native.Z3_write_interpolation_problem(nCtx, (uint)cnsts.Length, Expr.ArrayToNative(cnsts), parents, filename, (uint)theory.Length, Expr.ArrayToNative(theory)); + } + } +} diff --git a/src/api/dotnet/Microsoft.Z3.csproj b/src/api/dotnet/Microsoft.Z3.csproj index 0a062054d..cc7d3c0c5 100644 --- a/src/api/dotnet/Microsoft.Z3.csproj +++ b/src/api/dotnet/Microsoft.Z3.csproj @@ -19,12 +19,12 @@ true full false - ..\Debug\ + ..\..\..\..\..\cwinter\bugs\z3bugs\Debug\ DEBUG;TRACE prompt 4 true - ..\Debug\Microsoft.Z3.XML + C:\cwinter\bugs\z3bugs\Debug\Microsoft.Z3.XML False False True @@ -254,7 +254,7 @@ true - bin\x86\Debug\ + ..\..\..\..\..\cwinter\bugs\z3bugs\Debug\ DEBUG;TRACE true full @@ -266,7 +266,7 @@ MinimumRecommendedRules.ruleset ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - bin\x86\Debug\Microsoft.Z3.XML + C:\cwinter\bugs\z3bugs\Debug\Microsoft.Z3.XML bin\x86\Release\ @@ -352,6 +352,7 @@ + diff --git a/src/api/dotnet/Params.cs b/src/api/dotnet/Params.cs index 56a7a891f..c33728491 100644 --- a/src/api/dotnet/Params.cs +++ b/src/api/dotnet/Params.cs @@ -58,6 +58,16 @@ namespace Microsoft.Z3 Native.Z3_params_set_double(Context.nCtx, NativeObject, name.NativeObject, value); } + /// + /// Adds a parameter setting. + /// + public void Add(Symbol name, string value) + { + Contract.Requires(value != null); + + Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, Context.MkSymbol(value).NativeObject); + } + /// /// Adds a parameter setting. /// @@ -103,6 +113,16 @@ namespace Microsoft.Z3 Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value.NativeObject); } + /// + /// Adds a parameter setting. + /// + public void Add(string name, string value) + { + Contract.Requires(value != null); + + Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, Context.MkSymbol(value).NativeObject); + } + /// /// A string representation of the parameter set. /// diff --git a/src/api/dotnet/TupleSort.cs b/src/api/dotnet/TupleSort.cs index 1e4af5cd7..81a0eaf60 100644 --- a/src/api/dotnet/TupleSort.cs +++ b/src/api/dotnet/TupleSort.cs @@ -74,9 +74,10 @@ namespace Microsoft.Z3 Contract.Requires(name != null); IntPtr t = IntPtr.Zero; + IntPtr[] f = new IntPtr[numFields]; NativeObject = Native.Z3_mk_tuple_sort(ctx.nCtx, name.NativeObject, numFields, Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts), - ref t, new IntPtr[numFields]); + ref t, f); } #endregion }; diff --git a/src/api/java/AST.java b/src/api/java/AST.java index fa5cd8284..1f5463ec7 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from AST.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + AST.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ASTDecRefQueue.java b/src/api/java/ASTDecRefQueue.java index e0711363d..6ae84eb41 100644 --- a/src/api/java/ASTDecRefQueue.java +++ b/src/api/java/ASTDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ASTDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java index dbe7fbd02..6a4e6d56f 100644 --- a/src/api/java/ASTMap.java +++ b/src/api/java/ASTMap.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from ASTMap.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ASTMap.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java index 39e32f5d5..07b7dbf56 100644 --- a/src/api/java/ASTVector.java +++ b/src/api/java/ASTVector.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from ASTVector.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ASTVector.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/AlgebraicNum.java b/src/api/java/AlgebraicNum.java index eaeae933d..340f37f80 100644 --- a/src/api/java/AlgebraicNum.java +++ b/src/api/java/AlgebraicNum.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from AlgebraicNum.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + AlgebraicNum.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java index e6c6b89fd..c550c05ae 100644 --- a/src/api/java/ApplyResult.java +++ b/src/api/java/ApplyResult.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from ApplyResult.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ApplyResult.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ApplyResultDecRefQueue.java b/src/api/java/ApplyResultDecRefQueue.java index 275f4b8f0..78f74d6cc 100644 --- a/src/api/java/ApplyResultDecRefQueue.java +++ b/src/api/java/ApplyResultDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ApplyResultDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ArithExpr.java b/src/api/java/ArithExpr.java index c429f2322..83ec35d01 100644 --- a/src/api/java/ArithExpr.java +++ b/src/api/java/ArithExpr.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from ArithExpr.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - * **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ArithExpr.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ArithSort.java b/src/api/java/ArithSort.java index 5e1780539..2346d9b74 100644 --- a/src/api/java/ArithSort.java +++ b/src/api/java/ArithSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from ArithSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ArithSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ArrayExpr.java b/src/api/java/ArrayExpr.java index b3bbb8d75..2d5a5a273 100644 --- a/src/api/java/ArrayExpr.java +++ b/src/api/java/ArrayExpr.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from ArrayExpr.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ArrayExpr.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ArraySort.java b/src/api/java/ArraySort.java index 2ab8a9750..a371fa3cb 100644 --- a/src/api/java/ArraySort.java +++ b/src/api/java/ArraySort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from ArraySort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ArraySort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/AstMapDecRefQueue.java b/src/api/java/AstMapDecRefQueue.java index f4c6b2ab5..a4e02d29f 100644 --- a/src/api/java/AstMapDecRefQueue.java +++ b/src/api/java/AstMapDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + AstMapDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/AstVectorDecRefQueue.java b/src/api/java/AstVectorDecRefQueue.java index bdabcdcb1..e0c7988a9 100644 --- a/src/api/java/AstVectorDecRefQueue.java +++ b/src/api/java/AstVectorDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + AstVectorDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/BitVecExpr.java b/src/api/java/BitVecExpr.java index 9602ea3a0..24b1cfdf3 100644 --- a/src/api/java/BitVecExpr.java +++ b/src/api/java/BitVecExpr.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from BitVecExpr.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + BitVecExpr.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/BitVecNum.java b/src/api/java/BitVecNum.java index 2dd0dd75a..69ac5dadc 100644 --- a/src/api/java/BitVecNum.java +++ b/src/api/java/BitVecNum.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from BitVecNum.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + BitVecNum.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/BitVecSort.java b/src/api/java/BitVecSort.java index c2ec4c26e..be406c806 100644 --- a/src/api/java/BitVecSort.java +++ b/src/api/java/BitVecSort.java @@ -1,8 +1,20 @@ /** - * This file was automatically generated from BitVecSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + BitVecSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ + package com.microsoft.z3; /** diff --git a/src/api/java/BoolExpr.java b/src/api/java/BoolExpr.java index 40786f76d..99453496a 100644 --- a/src/api/java/BoolExpr.java +++ b/src/api/java/BoolExpr.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from BoolExpr.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + BoolExpr.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/BoolSort.java b/src/api/java/BoolSort.java index 03711289a..85ca0a7f7 100644 --- a/src/api/java/BoolSort.java +++ b/src/api/java/BoolSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from BoolSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + BoolSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Constructor.java b/src/api/java/Constructor.java index 0c53da73c..4813c2b0a 100644 --- a/src/api/java/Constructor.java +++ b/src/api/java/Constructor.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Constructor.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Constructor.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java index a33276ebb..315a2e535 100644 --- a/src/api/java/ConstructorList.java +++ b/src/api/java/ConstructorList.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from ConstructorList.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ConstructorList.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 6b6c63ac3..4fbd79be2 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Context.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Context.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; @@ -2904,27 +2915,13 @@ public class Context extends IDisposable * configuration parameters can be obtained using the Z3 executable: * z3.exe -ini? Only a few configuration parameters are mutable * once the context is created. An exception is thrown when trying to modify - * an immutable parameter. + * an immutable parameter. **/ public void updateParamValue(String id, String value) throws Z3Exception { Native.updateParamValue(nCtx(), id, value); } - /** - * Get a configuration parameter. Returns null if the parameter - * value does not exist. - **/ - public String getParamValue(String id) throws Z3Exception - { - Native.StringPtr res = new Native.StringPtr(); - boolean r = Native.getParamValue(nCtx(), id, res); - if (!r) - return null; - else - return res.value; - } - long m_ctx = 0; long nCtx() diff --git a/src/api/java/DatatypeExpr.java b/src/api/java/DatatypeExpr.java index 63cb02f80..806ceacab 100644 --- a/src/api/java/DatatypeExpr.java +++ b/src/api/java/DatatypeExpr.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from DatatypeExpr.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + DatatypeExpr.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/DatatypeSort.java b/src/api/java/DatatypeSort.java index f7b2f7d32..9c339d932 100644 --- a/src/api/java/DatatypeSort.java +++ b/src/api/java/DatatypeSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from DatatypeSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + DatatypeSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java index c0fb6d1d6..9715b9a97 100644 --- a/src/api/java/EnumSort.java +++ b/src/api/java/EnumSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from EnumSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + EnumSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index f7edc6a2b..3773e749d 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Expr.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Expr.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/FiniteDomainSort.java b/src/api/java/FiniteDomainSort.java index a8ba0d8c3..4cb2ab917 100644 --- a/src/api/java/FiniteDomainSort.java +++ b/src/api/java/FiniteDomainSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from FiniteDomainSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + FiniteDomainSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index 4710368aa..57e1e105a 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Fixedpoint.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Fixedpoint.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/FixedpointDecRefQueue.java b/src/api/java/FixedpointDecRefQueue.java index e52389b85..2ea40dd2c 100644 --- a/src/api/java/FixedpointDecRefQueue.java +++ b/src/api/java/FixedpointDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + FixedpointDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java index ada44bbd7..573ebd102 100644 --- a/src/api/java/FuncDecl.java +++ b/src/api/java/FuncDecl.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from FuncDecl.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + FuncDecl.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java index b7fa118e9..243ade71f 100644 --- a/src/api/java/FuncInterp.java +++ b/src/api/java/FuncInterp.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from FuncInterp.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + FuncInterp.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/FuncInterpDecRefQueue.java b/src/api/java/FuncInterpDecRefQueue.java index e2814a9b8..8bdad4ad5 100644 --- a/src/api/java/FuncInterpDecRefQueue.java +++ b/src/api/java/FuncInterpDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + FuncInterpDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/FuncInterpEntryDecRefQueue.java b/src/api/java/FuncInterpEntryDecRefQueue.java index 61488ec74..494c2695c 100644 --- a/src/api/java/FuncInterpEntryDecRefQueue.java +++ b/src/api/java/FuncInterpEntryDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + FuncInterpEntryDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Global.java b/src/api/java/Global.java index 33a828fb8..b97e48721 100644 --- a/src/api/java/Global.java +++ b/src/api/java/Global.java @@ -1,7 +1,19 @@ /** - * Global.java - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Global.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java index c486a57b3..aba8b0149 100644 --- a/src/api/java/Goal.java +++ b/src/api/java/Goal.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Goal.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Goal.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/GoalDecRefQueue.java b/src/api/java/GoalDecRefQueue.java index 0c7b8f5d9..45992170f 100644 --- a/src/api/java/GoalDecRefQueue.java +++ b/src/api/java/GoalDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + GoalDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/IDecRefQueue.java b/src/api/java/IDecRefQueue.java index ddb679910..2190f8e4d 100644 --- a/src/api/java/IDecRefQueue.java +++ b/src/api/java/IDecRefQueue.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from IDecRefQueue.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + IDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/IntExpr.java b/src/api/java/IntExpr.java index 78cc15f90..2e90c3cbf 100644 --- a/src/api/java/IntExpr.java +++ b/src/api/java/IntExpr.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from IntExpr.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + IntExpr.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/IntNum.java b/src/api/java/IntNum.java index ebf237a2e..0fdcf1aa6 100644 --- a/src/api/java/IntNum.java +++ b/src/api/java/IntNum.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from IntNum.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + IntNum.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/IntSort.java b/src/api/java/IntSort.java index 44e48ccd1..bcfc730c4 100644 --- a/src/api/java/IntSort.java +++ b/src/api/java/IntSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from IntSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + IntSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/IntSymbol.java b/src/api/java/IntSymbol.java index 113b507c3..b0f1af685 100644 --- a/src/api/java/IntSymbol.java +++ b/src/api/java/IntSymbol.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from IntSymbol.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + IntSymbol.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java new file mode 100644 index 000000000..3e9996b3e --- /dev/null +++ b/src/api/java/InterpolationContext.java @@ -0,0 +1,183 @@ +/** +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + InterpolationContext.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ + +package com.microsoft.z3; + +import java.util.Map; +import java.lang.String; + +import com.microsoft.z3.Native.IntPtr; +import com.microsoft.z3.Native.UIntArrayPtr; +import com.microsoft.z3.enumerations.Z3_lbool; + +/** + * The InterpolationContext is suitable for generation of interpolants. + * + * For more information on interpolation please refer + * too the C/C++ API, which is well documented. + **/ +public class InterpolationContext extends Context +{ + /** + * Constructor. + **/ + public InterpolationContext() throws Z3Exception + { + m_ctx = Native.mkInterpolationContext(0); + initContext(); + } + + /** + * Constructor. + * + * + **/ + public InterpolationContext(Map settings) throws Z3Exception + { + long cfg = Native.mkConfig(); + for (Map.Entry kv : settings.entrySet()) + Native.setParamValue(cfg, kv.getKey(), kv.getValue()); + m_ctx = Native.mkInterpolationContext(cfg); + Native.delConfig(cfg); + initContext(); + } + + /** + * Create an expression that marks a formula position for interpolation. + * @throws Z3Exception + **/ + public BoolExpr MkInterpolant(BoolExpr a) throws Z3Exception + { + checkContextMatch(a); + return new BoolExpr(this, Native.mkInterpolant(nCtx(), a.getNativeObject())); + } + + /** + * Computes an interpolant. + * For more information on interpolation please refer + * too the function Z3_get_interpolant in the C/C++ API, which is + * well documented. + * @throws Z3Exception + **/ + Expr[] GetInterpolant(Expr pf, Expr pat, Params p) throws Z3Exception + { + checkContextMatch(pf); + checkContextMatch(pat); + checkContextMatch(p); + + ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject())); + int n = seq.size(); + Expr[] res = new Expr[n]; + for (int i = 0; i < n; i++) + res[i] = Expr.create(this, seq.get(i).getNativeObject()); + return res; + } + + /** + * Computes an interpolant. + * For more information on interpolation please refer + * too the function Z3_compute_interpolant in the C/C++ API, which is + * well documented. + * @throws Z3Exception + **/ + Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model) throws Z3Exception + { + checkContextMatch(pat); + checkContextMatch(p); + + Native.LongPtr n_i = new Native.LongPtr(); + Native.LongPtr n_m = new Native.LongPtr(); + int r = Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m); + interp = new ASTVector(this, n_i.value); + model = new Model(this, n_m.value); + return Z3_lbool.fromInt(r); + } + + /// + /// Return a string summarizing cumulative time used for interpolation. + /// + /// For more information on interpolation please refer + /// too the function Z3_interpolation_profile in the C/C++ API, which is + /// well documented. + public String InterpolationProfile() throws Z3Exception + { + return Native.interpolationProfile(nCtx()); + } + + /// + /// Checks the correctness of an interpolant. + /// + /// For more information on interpolation please refer + /// too the function Z3_check_interpolant in the C/C++ API, which is + /// well documented. + public int CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory) throws Z3Exception + { + Native.StringPtr n_err_str = new Native.StringPtr(); + int r = Native.checkInterpolant(nCtx(), + cnsts.length, + Expr.arrayToNative(cnsts), + parents, + Expr.arrayToNative(interps), + n_err_str, + theory.length, + Expr.arrayToNative(theory)); + error = n_err_str.value; + return r; + } + + /// + /// Reads an interpolation problem from a file. + /// + /// For more information on interpolation please refer + /// too the function Z3_read_interpolation_problem in the C/C++ API, which is + /// well documented. + public int ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception + { + Native.IntPtr n_num = new Native.IntPtr(); + Native.IntPtr n_num_theory = new Native.IntPtr(); + Native.ObjArrayPtr n_cnsts = new Native.ObjArrayPtr(); + Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr(); + Native.ObjArrayPtr n_theory = new Native.ObjArrayPtr(); + Native.StringPtr n_err_str = new Native.StringPtr(); + int r = Native.readInterpolationProblem(nCtx(), n_num, n_cnsts, n_parents, filename, n_err_str, n_num_theory, n_theory); + int num = n_num.value; + int num_theory = n_num_theory.value; + error = n_err_str.value; + cnsts = new Expr[num]; + parents = new int[num]; + theory = new Expr[num_theory]; + for (int i = 0; i < num; i++) + { + cnsts[i] = Expr.create(this, n_cnsts.value[i]); + parents[i] = n_parents.value[i]; + } + for (int i = 0; i < num_theory; i++) + theory[i] = Expr.create(this, n_theory.value[i]); + return r; + } + + /// + /// Writes an interpolation problem to a file. + /// + /// For more information on interpolation please refer + /// too the function Z3_write_interpolation_problem in the C/C++ API, which is + /// well documented. + public void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception + { + Native.writeInterpolationProblem(nCtx(), cnsts.length, Expr.arrayToNative(cnsts), parents, filename, theory.length, Expr.arrayToNative(theory)); + } +} diff --git a/src/api/java/ListSort.java b/src/api/java/ListSort.java index af1645187..52cb1a179 100644 --- a/src/api/java/ListSort.java +++ b/src/api/java/ListSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from ListSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ListSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Log.java b/src/api/java/Log.java index 99581cedb..254da1bc6 100644 --- a/src/api/java/Log.java +++ b/src/api/java/Log.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Log.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Log.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Model.java b/src/api/java/Model.java index 32247eb4a..11eed201e 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Model.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Model.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ModelDecRefQueue.java b/src/api/java/ModelDecRefQueue.java index a0542714e..1200b29be 100644 --- a/src/api/java/ModelDecRefQueue.java +++ b/src/api/java/ModelDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ModelDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ParamDescrs.java b/src/api/java/ParamDescrs.java index 3b3e76e51..4afae9f76 100644 --- a/src/api/java/ParamDescrs.java +++ b/src/api/java/ParamDescrs.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from ParamDescrs.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ParamDescrs.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ParamDescrsDecRefQueue.java b/src/api/java/ParamDescrsDecRefQueue.java index 70806041d..a29565e8e 100644 --- a/src/api/java/ParamDescrsDecRefQueue.java +++ b/src/api/java/ParamDescrsDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ParamDescrsDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Params.java b/src/api/java/Params.java index 68af4386b..bbe6d66cf 100644 --- a/src/api/java/Params.java +++ b/src/api/java/Params.java @@ -1,8 +1,20 @@ /** - * This file was automatically generated from Params.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Params.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ + package com.microsoft.z3; @@ -28,6 +40,17 @@ public class Params extends Z3Object Native.paramsSetDouble(getContext().nCtx(), getNativeObject(), name.getNativeObject(), value); } + + /** + * Adds a parameter setting. + **/ + public void add(Symbol name, String value) throws Z3Exception + { + + Native.paramsSetSymbol(getContext().nCtx(), getNativeObject(), + name.getNativeObject(), + getContext().mkSymbol(value).getNativeObject()); + } /** * Adds a parameter setting. @@ -75,6 +98,17 @@ public class Params extends Z3Object .mkSymbol(name).getNativeObject(), value.getNativeObject()); } + /** + * Adds a parameter setting. + **/ + public void add(String name, String value) throws Z3Exception + { + + Native.paramsSetSymbol(getContext().nCtx(), getNativeObject(), + getContext().mkSymbol(name).getNativeObject(), + getContext().mkSymbol(value).getNativeObject()); + } + /** * A string representation of the parameter set. **/ diff --git a/src/api/java/ParamsDecRefQueue.java b/src/api/java/ParamsDecRefQueue.java index 361fdf133..7d71feb8f 100644 --- a/src/api/java/ParamsDecRefQueue.java +++ b/src/api/java/ParamsDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ParamDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Pattern.java b/src/api/java/Pattern.java index cd9340c9d..797b387d0 100644 --- a/src/api/java/Pattern.java +++ b/src/api/java/Pattern.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Pattern.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Pattern.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Probe.java b/src/api/java/Probe.java index b68b0266f..17ad81b5c 100644 --- a/src/api/java/Probe.java +++ b/src/api/java/Probe.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Probe.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Probe.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/ProbeDecRefQueue.java b/src/api/java/ProbeDecRefQueue.java index 0ae0b0e8e..fda5d37b4 100644 --- a/src/api/java/ProbeDecRefQueue.java +++ b/src/api/java/ProbeDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ProbeDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java index 78a0fc03f..e9aeefcca 100644 --- a/src/api/java/Quantifier.java +++ b/src/api/java/Quantifier.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Quantifier.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Quantifier.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/RatNum.java b/src/api/java/RatNum.java index e1cb5b346..f937ea593 100644 --- a/src/api/java/RatNum.java +++ b/src/api/java/RatNum.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from RatNum.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + RatNum.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/RealExpr.java b/src/api/java/RealExpr.java index 20d603d9a..6188e2999 100644 --- a/src/api/java/RealExpr.java +++ b/src/api/java/RealExpr.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from RealExpr.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + RealExpr.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/RealSort.java b/src/api/java/RealSort.java index ce7295ead..d76823a0d 100644 --- a/src/api/java/RealSort.java +++ b/src/api/java/RealSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from RealSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + RealSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/RelationSort.java b/src/api/java/RelationSort.java index bdc4d7804..77f6c595b 100644 --- a/src/api/java/RelationSort.java +++ b/src/api/java/RelationSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from RelationSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + RelationSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/SetSort.java b/src/api/java/SetSort.java index a94a34b26..69126933a 100644 --- a/src/api/java/SetSort.java +++ b/src/api/java/SetSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from SetSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + SetSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index 3827de07a..e129189f9 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Solver.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Solver.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/SolverDecRefQueue.java b/src/api/java/SolverDecRefQueue.java index 1c715716a..993c99621 100644 --- a/src/api/java/SolverDecRefQueue.java +++ b/src/api/java/SolverDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + SolverDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index 381b9b0ae..7bcc7ce7e 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Sort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Sort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java index c36020bd6..315feeaa2 100644 --- a/src/api/java/Statistics.java +++ b/src/api/java/Statistics.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Statistics.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Statistics.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/StatisticsDecRefQueue.java b/src/api/java/StatisticsDecRefQueue.java index d16bf3710..db3e32c86 100644 --- a/src/api/java/StatisticsDecRefQueue.java +++ b/src/api/java/StatisticsDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + StatisticsDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Status.java b/src/api/java/Status.java index e37631070..a08f47909 100644 --- a/src/api/java/Status.java +++ b/src/api/java/Status.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Status.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Status.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/StringSymbol.java b/src/api/java/StringSymbol.java index 951051aa0..09273c946 100644 --- a/src/api/java/StringSymbol.java +++ b/src/api/java/StringSymbol.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from StringSymbol.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + StringSymbol.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Symbol.java b/src/api/java/Symbol.java index 177409ec8..856c9b57e 100644 --- a/src/api/java/Symbol.java +++ b/src/api/java/Symbol.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Symbol.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Symbol.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Tactic.java b/src/api/java/Tactic.java index e62096715..6573a1407 100644 --- a/src/api/java/Tactic.java +++ b/src/api/java/Tactic.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Tactic.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Tactic.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/TacticDecRefQueue.java b/src/api/java/TacticDecRefQueue.java index 50fba156e..5557d03b8 100644 --- a/src/api/java/TacticDecRefQueue.java +++ b/src/api/java/TacticDecRefQueue.java @@ -1,7 +1,19 @@ /** - * Copyright (c) 2012 Microsoft Corporation - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + TacticDecRefQueue.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/TupleSort.java b/src/api/java/TupleSort.java index 554581d0f..523f8d676 100644 --- a/src/api/java/TupleSort.java +++ b/src/api/java/TupleSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from TupleSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + TupleSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/UninterpretedSort.java b/src/api/java/UninterpretedSort.java index 51df17543..07e4707f5 100644 --- a/src/api/java/UninterpretedSort.java +++ b/src/api/java/UninterpretedSort.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from UninterpretedSort.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + UninterpretedSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Version.java b/src/api/java/Version.java index b96fb50f9..3f019390b 100644 --- a/src/api/java/Version.java +++ b/src/api/java/Version.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Version.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Version.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Z3Exception.java b/src/api/java/Z3Exception.java index 24dc586d4..2522db627 100644 --- a/src/api/java/Z3Exception.java +++ b/src/api/java/Z3Exception.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Z3Exception.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Z3Exception.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java index 6c2c11e25..03cfcd625 100644 --- a/src/api/java/Z3Object.java +++ b/src/api/java/Z3Object.java @@ -1,8 +1,19 @@ /** - * This file was automatically generated from Z3Object.cs - * w/ further modifications by: - * @author Christoph M. Wintersteiger (cwinter) - **/ +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + Z3Object.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ package com.microsoft.z3; diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 50d29a790..470280630 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -297,6 +297,11 @@ class AstRef(Z3PPObject): """Return a pointer to the corresponding C Z3_ast object.""" return self.ast + def get_id(self): + """Return unique identifier for object. It can be used for hash-tables and maps.""" + return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) + + def ctx_ref(self): """Return a reference to the C context where this AST node is stored.""" return self.ctx.ref() @@ -447,6 +452,10 @@ class SortRef(AstRef): def as_ast(self): return Z3_sort_to_ast(self.ctx_ref(), self.ast) + def get_id(self): + return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) + + def kind(self): """Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts. @@ -585,6 +594,9 @@ class FuncDeclRef(AstRef): def as_ast(self): return Z3_func_decl_to_ast(self.ctx_ref(), self.ast) + def get_id(self): + return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) + def as_func_decl(self): return self.ast @@ -730,6 +742,9 @@ class ExprRef(AstRef): def as_ast(self): return self.ast + def get_id(self): + return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) + def sort(self): """Return the sort of expression `self`. @@ -1524,6 +1539,9 @@ class PatternRef(ExprRef): def as_ast(self): return Z3_pattern_to_ast(self.ctx_ref(), self.ast) + def get_id(self): + return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) + def is_pattern(a): """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation. @@ -1586,6 +1604,9 @@ class QuantifierRef(BoolRef): def as_ast(self): return self.ast + def get_id(self): + return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) + def sort(self): """Return the Boolean sort.""" return BoolSort(self.ctx) @@ -4448,7 +4469,7 @@ def args2params(arguments, keywords, ctx=None): A ':' is added to the keywords, and '_' is replaced with '-' >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True}) - (params model 1 relevancy 2 elim_and 1) + (params model true relevancy 2 elim_and true) """ if __debug__: _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.") @@ -6011,6 +6032,24 @@ class Solver(Z3PPObject): """ return Z3_solver_to_string(self.ctx.ref(), self.solver) + def to_smt2(self): + """return SMTLIB2 formatted benchmark for solver's assertions""" + es = self.assertions() + sz = len(es) + sz1 = sz + if sz1 > 0: + sz1 -= 1 + v = (Ast * sz1)() + for i in range(sz1): + v[i] = es[i].as_ast() + if sz > 0: + e = es[sz1].as_ast() + else: + e = BoolVal(True, self.ctx).as_ast() + return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e) + + + def SolverFor(logic, ctx=None): """Create a solver customized for the given logic. @@ -6960,7 +6999,7 @@ def substitute(t, *m): if isinstance(m, tuple): m1 = _get_args(m) if isinstance(m1, list): - m = _get_args(m1) + m = m1 if __debug__: _z3_assert(is_expr(t), "Z3 expression expected") _z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.") @@ -7253,19 +7292,19 @@ def parse_smt2_file(f, sorts={}, decls={}, ctx=None): dsz, dnames, ddecls = _dict2darray(decls, ctx) return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) -def Interp(a,ctx=None): +def Interpolant(a,ctx=None): """Create an interpolation operator. The argument is an interpolation pattern (see tree_interpolant). >>> x = Int('x') - >>> print Interp(x>0) + >>> print Interpolant(x>0) interp(x > 0) """ ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx)) s = BoolSort(ctx) a = s.cast(a) - return BoolRef(Z3_mk_interp(ctx.ref(), a.as_ast()), ctx) + return BoolRef(Z3_mk_interpolant(ctx.ref(), a.as_ast()), ctx) def tree_interpolant(pat,p=None,ctx=None): """Compute interpolant for a tree of formulas. @@ -7304,10 +7343,10 @@ def tree_interpolant(pat,p=None,ctx=None): >>> x = Int('x') >>> y = Int('y') - >>> print tree_interpolant(And(Interp(x < 0), Interp(y > 2), x == y)) + >>> print tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y)) [Not(x >= 0), Not(y <= 2)] - >>> g = And(Interp(x<0),x<2) + >>> g = And(Interpolant(x<0),x<2) >>> try: ... print tree_interpolant(g).sexpr() ... except ModelRef as m: @@ -7342,11 +7381,11 @@ def binary_interpolant(a,b,p=None,ctx=None): If parameters p are supplied, these are used in creating the solver that determines satisfiability. - >>> x = Int('x') - >>> print binary_interpolant(x<0,x>2) - x <= 2 + x = Int('x') + print binary_interpolant(x<0,x>2) + Not(x >= 0) """ - f = And(Interp(a),b) + f = And(Interpolant(a),b) return tree_interpolant(f,p,ctx)[0] def sequence_interpolant(v,p=None,ctx=None): @@ -7375,6 +7414,6 @@ def sequence_interpolant(v,p=None,ctx=None): """ f = v[0] for i in range(1,len(v)): - f = And(Interp(f),v[i]) + f = And(Interpolant(f),v[i]) return tree_interpolant(f,p,ctx) diff --git a/src/api/python/z3types.py b/src/api/python/z3types.py index 593312d68..5d59368ff 100644 --- a/src/api/python/z3types.py +++ b/src/api/python/z3types.py @@ -4,7 +4,7 @@ class Z3Exception(Exception): def __init__(self, value): self.value = value def __str__(self): - return repr(self.value) + return str(self.value) class ContextObj(ctypes.c_void_p): def __init__(self, context): self._as_parameter_ = context diff --git a/src/api/z3.h b/src/api/z3.h index db8becafd..2ebc20977 100644 --- a/src/api/z3.h +++ b/src/api/z3.h @@ -27,6 +27,7 @@ Notes: #include"z3_algebraic.h" #include"z3_polynomial.h" #include"z3_rcf.h" +#include"z3_interp.h" #undef __in #undef __out diff --git a/src/api/z3_api.h b/src/api/z3_api.h index b9f4975e8..2e3ddf4b4 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1375,6 +1375,16 @@ extern "C" { although some parameters can be changed using #Z3_update_param_value. All main interaction with Z3 happens in the context of a \c Z3_context. + In contrast to #Z3_mk_context_rc, the life time of Z3_ast objects + are determined by the scope level of #Z3_push and #Z3_pop. + In other words, a Z3_ast object remains valid until there is a + call to Z3_pop that takes the current scope below the level where + the object was created. + + Note that all other reference counted objects, including Z3_model, + Z3_solver, Z3_func_interp have to be managed by the caller. + Their reference counts are not handled by the context. + \conly \sa Z3_del_context \conly \deprecated Use #Z3_mk_context_rc @@ -1452,15 +1462,6 @@ extern "C" { */ void Z3_API Z3_update_param_value(__in Z3_context c, __in Z3_string param_id, __in Z3_string param_value); - /** - \brief Return the value of a context parameter. - - \sa Z3_global_param_get - - def_API('Z3_get_param_value', BOOL, (_in(CONTEXT), _in(STRING), _out(STRING))) - */ - Z3_bool_opt Z3_API Z3_get_param_value(__in Z3_context c, __in Z3_string param_id, __out_opt Z3_string_ptr param_value); - #ifdef CorML4 /** \brief Interrupt the execution of a Z3 procedure. @@ -1769,7 +1770,7 @@ extern "C" { Z3_sort Z3_API Z3_mk_tuple_sort(__in Z3_context c, __in Z3_symbol mk_tuple_name, __in unsigned num_fields, - __in_ecount(num_fields) Z3_symbol const field_names[], + __in_ecount(num_fields) Z3_symbol const field_names[], __in_ecount(num_fields) Z3_sort const field_sorts[], __out Z3_func_decl * mk_tuple_decl, __out_ecount(num_fields) Z3_func_decl proj_decl[]); @@ -2106,17 +2107,7 @@ END_MLAPI_EXCLUDE def_API('Z3_mk_not', AST, (_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_not(__in Z3_context c, __in Z3_ast a); - - /** - \brief \mlh mk_interp c a \endmlh - Create an AST node marking a formula position for interpolation. - The node \c a must have Boolean sort. - - def_API('Z3_mk_interp', AST, (_in(CONTEXT), _in(AST))) - */ - Z3_ast Z3_API Z3_mk_interp(__in Z3_context c, __in Z3_ast a); - /** \brief \mlh mk_ite c t1 t2 t2 \endmlh Create an AST node representing an if-then-else: ite(t1, t2, @@ -4907,8 +4898,7 @@ END_MLAPI_EXCLUDE __in_ecount(num_sorts) Z3_sort const sorts[], __in unsigned num_decls, __in_ecount(num_decls) Z3_symbol const decl_names[], - __in_ecount(num_decls) Z3_func_decl const decls[] - ); + __in_ecount(num_decls) Z3_func_decl const decls[]); /** \brief Similar to #Z3_parse_smtlib2_string, but reads the benchmark from a file. @@ -4917,13 +4907,12 @@ END_MLAPI_EXCLUDE */ Z3_ast Z3_API Z3_parse_smtlib2_file(__in Z3_context c, __in Z3_string file_name, - __in unsigned num_sorts, - __in_ecount(num_sorts) Z3_symbol const sort_names[], - __in_ecount(num_sorts) Z3_sort const sorts[], - __in unsigned num_decls, - __in_ecount(num_decls) Z3_symbol const decl_names[], - __in_ecount(num_decls) Z3_func_decl const decls[] - ); + __in unsigned num_sorts, + __in_ecount(num_sorts) Z3_symbol const sort_names[], + __in_ecount(num_sorts) Z3_sort const sorts[], + __in unsigned num_decls, + __in_ecount(num_decls) Z3_symbol const decl_names[], + __in_ecount(num_decls) Z3_func_decl const decls[]); #ifdef ML4only #include @@ -6610,6 +6599,13 @@ END_MLAPI_EXCLUDE /** \brief Create a new (incremental) solver. + The function #Z3_solver_get_model retrieves a model if the + assertions is satisfiable (i.e., the result is \c + Z3_L_TRUE) and model construction is enabled. + The function #Z3_solver_get_model can also be used even + if the result is \c Z3_L_UNDEF, but the returned model + is not guaranteed to satisfy quantified assertions. + def_API('Z3_mk_simple_solver', SOLVER, (_in(CONTEXT),)) */ Z3_solver Z3_API Z3_mk_simple_solver(__in Z3_context c); @@ -6747,8 +6743,11 @@ END_MLAPI_EXCLUDE \brief Check whether the assertions in a given solver are consistent or not. The function #Z3_solver_get_model retrieves a model if the - assertions are not unsatisfiable (i.e., the result is not \c - Z3_L_FALSE) and model construction is enabled. + assertions is satisfiable (i.e., the result is \c + Z3_L_TRUE) and model construction is enabled. + Note that if the call returns Z3_L_UNDEF, Z3 does not + ensure that calls to #Z3_solver_get_model succeed and any models + produced in this case are not guaranteed to satisfy the assertions. The function #Z3_solver_get_proof retrieves a proof if proof generation was enabled when the context was created, and the @@ -7059,7 +7058,7 @@ END_MLAPI_EXCLUDE \mlonly then a valid model is returned. Otherwise, it is unsafe to use the returned model.\endmlonly \conly The caller is responsible for deleting the model using the function #Z3_del_model. - \conly \remark In constrast with the rest of the Z3 API, the reference counter of the + \conly \remark In contrast with the rest of the Z3 API, the reference counter of the \conly model is incremented. This is to guarantee backward compatibility. In previous \conly versions, models did not support reference counting. @@ -7172,6 +7171,11 @@ END_MLAPI_EXCLUDE \brief Delete a model object. \sa Z3_check_and_get_model + + \conly \remark The Z3_check_and_get_model automatically increments a reference count on the model. + \conly The expected usage is that models created by that method are deleted using Z3_del_model. + \conly This is for backwards compatibility and in contrast to the rest of the API where + \conly callers are responsible for managing reference counts. \deprecated Subsumed by Z3_solver API @@ -7675,314 +7679,6 @@ END_MLAPI_EXCLUDE Z3_ast Z3_API Z3_get_context_assignment(__in Z3_context c); /*@}*/ - - /** - @name Interpolation - */ - /*@{*/ - - /** \brief This function generates a Z3 context suitable for generation of - interpolants. Formulas can be generated as abstract syntx trees in - this context using the Z3 C API. - - Interpolants are also generated as AST's in this context. - - If cfg is non-null, it will be used as the base configuration - for the Z3 context. This makes it possible to set Z3 options - to be used during interpolation. This feature should be used - with some caution however, as it may be that certain Z3 options - are incompatible with interpolation. - - def_API('Z3_mk_interpolation_context', CONTEXT, (_in(CONFIG),)) - - */ - - Z3_context Z3_API Z3_mk_interpolation_context(__in Z3_config cfg); - - /** Compute an interpolant from a refutation. This takes a proof of - "false" from a set of formulas C, and an interpolation - pattern. The pattern pat is a formula combining the formulas in C - using logical conjunction and the "interp" operator (see - #Z3_mk_interp). This interp operator is logically the identity - operator. It marks the sub-formulas of the pattern for which interpolants should - be computed. The interpolant is a map sigma from marked subformulas to - formulas, such that, for each marked subformula phi of pat (where phi sigma - is phi with sigma(psi) substituted for each subformula psi of phi such that - psi in dom(sigma)): - - 1) phi sigma implies sigma(phi), and - - 2) sigma(phi) is in the common uninterpreted vocabulary between - the formulas of C occurring in phi and those not occurring in - phi - - and moreover pat sigma implies false. In the simplest case - an interpolant for the pattern "(and (interp A) B)" maps A - to an interpolant for A /\ B. - - The return value is a vector of formulas representing sigma. The - vector contains sigma(phi) for each marked subformula of pat, in - pre-order traversal. This means that subformulas of phi occur before phi - in the vector. Also, subformulas that occur multiply in pat will - occur multiply in the result vector. - - In particular, calling Z3_get_interpolant on a pattern of the - form (interp ... (interp (and (interp A_1) A_2)) ... A_N) will - result in a sequence interpolant for A_1, A_2,... A_N. - - Neglecting interp markers, the pattern must be a conjunction of - formulas in C, the set of premises of the proof. Otherwise an - error is flagged. - - Any premises of the proof not present in the pattern are - treated as "background theory". Predicate and function symbols - occurring in the background theory are treated as interpreted and - thus always allowed in the interpolant. - - Interpolant may not necessarily be computable from all - proofs. To be sure an interpolant can be computed, the proof - must be generated by an SMT solver for which interpoaltion is - supported, and the premises must be expressed using only - theories and operators for which interpolation is supported. - - Currently, the only SMT solver that is supported is the legacy - SMT solver. Such a solver is available as the default solver in - #Z3_context objects produced by #Z3_mk_interpolation_context. - Currently, the theories supported are equality with - uninterpreted functions, linear integer arithmetic, and the - theory of arrays (in SMT-LIB terms, this is AUFLIA). - Quantifiers are allowed. Use of any other operators (including - "labels") may result in failure to compute an interpolant from a - proof. - - Parameters: - - \param c logical context. - \param pf a refutation from premises (assertions) C - \param pat an interpolation pattern over C - \param p parameters - - def_API('Z3_get_interpolant', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(PARAMS))) - */ - - Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p); - - /* Compute an interpolant for an unsatisfiable conjunction of formulas. - - This takes as an argument an interpolation pattern as in - #Z3_get_interpolant. This is a conjunction, some subformulas of - which are marked with the "interp" operator (see #Z3_mk_interp). - - The conjunction is first checked for unsatisfiability. The result - of this check is returned in the out parameter "status". If the result - is unsat, an interpolant is computed from the refutation as in #Z3_get_interpolant - and returned as a vector of formulas. Otherwise the return value is - an empty formula. - - See #Z3_get_interpolant for a discussion of supported theories. - - The advantage of this function over #Z3_get_interpolant is that - it is not necessary to create a suitable SMT solver and generate - a proof. The disadvantage is that it is not possible to use the - solver incrementally. - - Parameters: - - \param c logical context. - \param pat an interpolation pattern - \param p parameters for solver creation - \param status returns the status of the sat check - \param model returns model if satisfiable - - Return value: status of SAT check - - def_API('Z3_compute_interpolant', INT, (_in(CONTEXT), _in(AST), _in(PARAMS), _out(AST_VECTOR), _out(MODEL))) - */ - - Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *interp, __out Z3_model *model); - - -/** Constant reprepresenting a root of a formula tree for tree interpolation */ -#define IZ3_ROOT SHRT_MAX - -/** This function uses Z3 to determine satisfiability of a set of - constraints. If UNSAT, an interpolant is returned, based on the - refutation generated by Z3. If SAT, a model is returned. - - If "parents" is non-null, computes a tree interpolant. The tree is - defined by the array "parents". This array maps each formula in - the tree to its parent, where formulas are indicated by their - integer index in "cnsts". The parent of formula n must have index - greater than n. The last formula is the root of the tree. Its - parent entry should be the constant IZ3_ROOT. - - If "parents" is null, computes a sequence interpolant. - - \param ctx The Z3 context. Must be generated by iz3_mk_context - \param num The number of constraints in the sequence - \param cnsts Array of constraints (AST's in context ctx) - \param parents The parents vector defining the tree structure - \param options Interpolation options (may be NULL) - \param interps Array to return interpolants (size at least num-1, may be NULL) - \param model Returns a Z3 model if constraints SAT (may be NULL) - \param labels Returns relevant labels if SAT (may be NULL) - \param incremental - - VERY IMPORTANT: All the Z3 formulas in cnsts must be in Z3 - context ctx. The model and interpolants returned are also - in this context. - - The return code is as in Z3_check_assumptions, that is, - - Z3_L_FALSE = constraints UNSAT (interpolants returned) - Z3_L_TRUE = constraints SAT (model returned) - Z3_L_UNDEF = Z3 produced no result, or interpolation not possible - - Currently, this function supports integer and boolean variables, - as well as arrays over these types, with linear arithmetic, - uninterpreted functions and quantifiers over integers (that is - AUFLIA). Interpolants are produced in AUFLIA. However, some - uses of array operations may cause quantifiers to appear in the - interpolants even when there are no quantifiers in the input formulas. - Although quantifiers may appear in the input formulas, Z3 may give up in - this case, returning Z3_L_UNDEF. - - If "incremental" is true, cnsts must contain exactly the set of - formulas that are currently asserted in the context. If false, - there must be no formulas currently asserted in the context. - Setting "incremental" to true makes it posisble to incrementally - add and remove constraints from the context until the context - becomes UNSAT, at which point an interpolant is computed. Caution - must be used, however. Before popping the context, if you wish to - keep the interolant formulas, you *must* preserve them by using - Z3_persist_ast. Also, if you want to simplify the interpolant - formulas using Z3_simplify, you must first pop all of the - assertions in the context (or use a different context). Otherwise, - the formulas will be simplified *relative* to these constraints, - which is almost certainly not what you want. - - - Current limitations on tree interpolants. In a tree interpolation - problem, each constant (0-ary function symbol) must occur only - along one path from root to leaf. Function symbols (of arity > 0) - are considered to have global scope (i.e., may appear in any - interpolant formula). - - - */ - - - Z3_lbool Z3_API Z3_interpolate(__in Z3_context ctx, - __in int num, - __in_ecount(num) Z3_ast *cnsts, - __in_ecount(num) unsigned *parents, - __in Z3_params options, - __out_ecount(num-1) Z3_ast *interps, - __out Z3_model *model, - __out Z3_literals *labels, - __in int incremental, - __in int num_theory, - __in_ecount(num_theory) Z3_ast *theory); - - /** Return a string summarizing cumulative time used for - interpolation. This string is purely for entertainment purposes - and has no semantics. - - \param ctx The context (currently ignored) - - def_API('Z3_interpolation_profile', STRING, (_in(CONTEXT),)) - */ - - Z3_string Z3_API Z3_interpolation_profile(__in Z3_context ctx); - - /** - \brief Read an interpolation problem from file. - - \param ctx The Z3 context. This resets the error handler of ctx. - \param filename The file name to read. - \param num Returns length of sequence. - \param cnsts Returns sequence of formulas (do not free) - \param parents Returns the parents vector (or NULL for sequence) - \param error Returns an error message in case of failure (do not free the string) - - Returns true on success. - - File formats: Currently two formats are supported, based on - SMT-LIB2. For sequence interpolants, the sequence of constraints is - represented by the sequence of "assert" commands in the file. - - For tree interpolants, one symbol of type bool is associated to - each vertex of the tree. For each vertex v there is an "assert" - of the form: - - (implies (and c1 ... cn f) v) - - where c1 .. cn are the children of v (which must precede v in the file) - and f is the formula assiciated to node v. The last formula in the - file is the root vertex, and is represented by the predicate "false". - - A solution to a tree interpolation problem can be thought of as a - valuation of the vertices that makes all the implications true - where each value is represented using the common symbols between - the formulas in the subtree and the remainder of the formulas. - - */ - - - int Z3_API Z3_read_interpolation_problem(__in Z3_context ctx, - __out int *num, - __out_ecount(*num) Z3_ast **cnsts, - __out_ecount(*num) int **parents, - __in const char *filename, - __out const char **error, - __out int *num_theory, - __out_ecount(*num_theory) Z3_ast **theory); - - - - /** Check the correctness of an interpolant. The Z3 context must - have no constraints asserted when this call is made. That means - that after interpolating, you must first fully pop the Z3 - context before calling this. See Z3_interpolate for meaning of parameters. - - \param ctx The Z3 context. Must be generated by Z3_mk_interpolation_context - \param num The number of constraints in the sequence - \param cnsts Array of constraints (AST's in context ctx) - \param parents The parents vector (or NULL for sequence) - \param interps The interpolant to check - \param error Returns an error message if interpolant incorrect (do not free the string) - - Return value is Z3_L_TRUE if interpolant is verified, Z3_L_FALSE if - incorrect, and Z3_L_UNDEF if unknown. - - */ - - int Z3_API Z3_check_interpolant(Z3_context ctx, int num, Z3_ast *cnsts, int *parents, Z3_ast *interps, const char **error, - int num_theory, Z3_ast *theory); - - /** Write an interpolation problem to file suitable for reading with - Z3_read_interpolation_problem. The output file is a sequence - of SMT-LIB2 format commands, suitable for reading with command-line Z3 - or other interpolating solvers. - - \param ctx The Z3 context. Must be generated by z3_mk_interpolation_context - \param num The number of constraints in the sequence - \param cnsts Array of constraints - \param parents The parents vector (or NULL for sequence) - \param filename The file name to write - - */ - - void Z3_API Z3_write_interpolation_problem(Z3_context ctx, - int num, - Z3_ast *cnsts, - int *parents, - const char *filename, - int num_theory, - Z3_ast *theory); - - - #endif diff --git a/src/api/z3_interp.h b/src/api/z3_interp.h new file mode 100644 index 000000000..729851988 --- /dev/null +++ b/src/api/z3_interp.h @@ -0,0 +1,277 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + z3_interp.h + +Abstract: + + API for interpolation + +Author: + + Kenneth McMillan (kenmcmil) + +Notes: + +--*/ +#ifndef _Z3_INTERPOLATION_H_ +#define _Z3_INTERPOLATION_H_ + +#ifdef __cplusplus +extern "C" { +#endif // __cplusplus + + /** + @name Interpolation + */ + /*@{*/ + + /** + \brief \mlh mk_interp c a \endmlh + Create an AST node marking a formula position for interpolation. + + The node \c a must have Boolean sort. + + def_API('Z3_mk_interpolant', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_interpolant(__in Z3_context c, __in Z3_ast a); + + + /** \brief This function generates a Z3 context suitable for generation of + interpolants. Formulas can be generated as abstract syntax trees in + this context using the Z3 C API. + + Interpolants are also generated as AST's in this context. + + If cfg is non-null, it will be used as the base configuration + for the Z3 context. This makes it possible to set Z3 options + to be used during interpolation. This feature should be used + with some caution however, as it may be that certain Z3 options + are incompatible with interpolation. + + def_API('Z3_mk_interpolation_context', CONTEXT, (_in(CONFIG),)) + + */ + + Z3_context Z3_API Z3_mk_interpolation_context(__in Z3_config cfg); + + /** Compute an interpolant from a refutation. This takes a proof of + "false" from a set of formulas C, and an interpolation + pattern. The pattern pat is a formula combining the formulas in C + using logical conjunction and the "interp" operator (see + #Z3_mk_interpolant). This interp operator is logically the identity + operator. It marks the sub-formulas of the pattern for which interpolants should + be computed. The interpolant is a map sigma from marked subformulas to + formulas, such that, for each marked subformula phi of pat (where phi sigma + is phi with sigma(psi) substituted for each subformula psi of phi such that + psi in dom(sigma)): + + 1) phi sigma implies sigma(phi), and + + 2) sigma(phi) is in the common uninterpreted vocabulary between + the formulas of C occurring in phi and those not occurring in + phi + + and moreover pat sigma implies false. In the simplest case + an interpolant for the pattern "(and (interp A) B)" maps A + to an interpolant for A /\ B. + + The return value is a vector of formulas representing sigma. The + vector contains sigma(phi) for each marked subformula of pat, in + pre-order traversal. This means that subformulas of phi occur before phi + in the vector. Also, subformulas that occur multiply in pat will + occur multiply in the result vector. + + In particular, calling Z3_get_interpolant on a pattern of the + form (interp ... (interp (and (interp A_1) A_2)) ... A_N) will + result in a sequence interpolant for A_1, A_2,... A_N. + + Neglecting interp markers, the pattern must be a conjunction of + formulas in C, the set of premises of the proof. Otherwise an + error is flagged. + + Any premises of the proof not present in the pattern are + treated as "background theory". Predicate and function symbols + occurring in the background theory are treated as interpreted and + thus always allowed in the interpolant. + + Interpolant may not necessarily be computable from all + proofs. To be sure an interpolant can be computed, the proof + must be generated by an SMT solver for which interpoaltion is + supported, and the premises must be expressed using only + theories and operators for which interpolation is supported. + + Currently, the only SMT solver that is supported is the legacy + SMT solver. Such a solver is available as the default solver in + #Z3_context objects produced by #Z3_mk_interpolation_context. + Currently, the theories supported are equality with + uninterpreted functions, linear integer arithmetic, and the + theory of arrays (in SMT-LIB terms, this is AUFLIA). + Quantifiers are allowed. Use of any other operators (including + "labels") may result in failure to compute an interpolant from a + proof. + + Parameters: + + \param c logical context. + \param pf a refutation from premises (assertions) C + \param pat an interpolation pattern over C + \param p parameters + + def_API('Z3_get_interpolant', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(PARAMS))) + */ + + Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p); + + /* Compute an interpolant for an unsatisfiable conjunction of formulas. + + This takes as an argument an interpolation pattern as in + #Z3_get_interpolant. This is a conjunction, some subformulas of + which are marked with the "interp" operator (see #Z3_mk_interpolant). + + The conjunction is first checked for unsatisfiability. The result + of this check is returned in the out parameter "status". If the result + is unsat, an interpolant is computed from the refutation as in #Z3_get_interpolant + and returned as a vector of formulas. Otherwise the return value is + an empty formula. + + See #Z3_get_interpolant for a discussion of supported theories. + + The advantage of this function over #Z3_get_interpolant is that + it is not necessary to create a suitable SMT solver and generate + a proof. The disadvantage is that it is not possible to use the + solver incrementally. + + Parameters: + + \param c logical context. + \param pat an interpolation pattern + \param p parameters for solver creation + \param status returns the status of the sat check + \param model returns model if satisfiable + + Return value: status of SAT check + + def_API('Z3_compute_interpolant', INT, (_in(CONTEXT), _in(AST), _in(PARAMS), _out(AST_VECTOR), _out(MODEL))) + */ + + Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, + __in Z3_ast pat, + __in Z3_params p, + __out Z3_ast_vector *interp, + __out Z3_model *model); + + /** Return a string summarizing cumulative time used for + interpolation. This string is purely for entertainment purposes + and has no semantics. + + \param ctx The context (currently ignored) + + + def_API('Z3_interpolation_profile', STRING, (_in(CONTEXT),)) + */ + + Z3_string Z3_API Z3_interpolation_profile(__in Z3_context ctx); + + /** + \brief Read an interpolation problem from file. + + \param ctx The Z3 context. This resets the error handler of ctx. + \param filename The file name to read. + \param num Returns length of sequence. + \param cnsts Returns sequence of formulas (do not free) + \param parents Returns the parents vector (or NULL for sequence) + \param error Returns an error message in case of failure (do not free the string) + + Returns true on success. + + File formats: Currently two formats are supported, based on + SMT-LIB2. For sequence interpolants, the sequence of constraints is + represented by the sequence of "assert" commands in the file. + + For tree interpolants, one symbol of type bool is associated to + each vertex of the tree. For each vertex v there is an "assert" + of the form: + + (implies (and c1 ... cn f) v) + + where c1 .. cn are the children of v (which must precede v in the file) + and f is the formula assiciated to node v. The last formula in the + file is the root vertex, and is represented by the predicate "false". + + A solution to a tree interpolation problem can be thought of as a + valuation of the vertices that makes all the implications true + where each value is represented using the common symbols between + the formulas in the subtree and the remainder of the formulas. + + def_API('Z3_read_interpolation_problem', INT, (_in(CONTEXT), _out(UINT), _out_managed_array(1, AST), _out_managed_array(1, UINT), _in(STRING), _out(STRING), _out(UINT), _out_managed_array(6, AST))) + + */ + + int Z3_API Z3_read_interpolation_problem(__in Z3_context ctx, + __out unsigned *num, + __out Z3_ast *cnsts[], + __out unsigned *parents[], + __in Z3_string filename, + __out_opt Z3_string_ptr error, + __out unsigned *num_theory, + __out Z3_ast *theory[]); + + + + /** Check the correctness of an interpolant. The Z3 context must + have no constraints asserted when this call is made. That means + that after interpolating, you must first fully pop the Z3 + context before calling this. See Z3_interpolate for meaning of parameters. + + \param ctx The Z3 context. Must be generated by Z3_mk_interpolation_context + \param num The number of constraints in the sequence + \param cnsts Array of constraints (AST's in context ctx) + \param parents The parents vector (or NULL for sequence) + \param interps The interpolant to check + \param error Returns an error message if interpolant incorrect (do not free the string) + + Return value is Z3_L_TRUE if interpolant is verified, Z3_L_FALSE if + incorrect, and Z3_L_UNDEF if unknown. + + def_API('Z3_check_interpolant', INT, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in_array(1, AST), _out(STRING), _in(UINT), _in_array(6, AST))) + */ + + int Z3_API Z3_check_interpolant(__in Z3_context ctx, + __in unsigned num, + __in_ecount(num) Z3_ast cnsts[], + __in_ecount(num) unsigned parents[], + __in_ecount(num - 1) Z3_ast *interps, + __out_opt Z3_string_ptr error, + __in unsigned num_theory, + __in_ecount(num_theory) Z3_ast theory[]); + + /** Write an interpolation problem to file suitable for reading with + Z3_read_interpolation_problem. The output file is a sequence + of SMT-LIB2 format commands, suitable for reading with command-line Z3 + or other interpolating solvers. + + \param ctx The Z3 context. Must be generated by z3_mk_interpolation_context + \param num The number of constraints in the sequence + \param cnsts Array of constraints + \param parents The parents vector (or NULL for sequence) + \param filename The file name to write + + def_API('Z3_write_interpolation_problem', VOID, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in(STRING), _in(UINT), _in_array(5, AST))) + */ + + void Z3_API Z3_write_interpolation_problem(__in Z3_context ctx, + __in unsigned num, + __in_ecount(num) Z3_ast cnsts[], + __in_ecount(num) unsigned parents[], + __in Z3_string filename, + __in unsigned num_theory, + __in_ecount(num_theory) Z3_ast theory[]); + +#ifdef __cplusplus +}; +#endif // __cplusplus + +#endif diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index df26422c8..5466df069 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -314,8 +314,8 @@ func_decl * float_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_paramete symbol name; switch (k) { case OP_FLOAT_REM: name = "remainder"; break; - case OP_FLOAT_MIN: name = "min"; break; - case OP_FLOAT_MAX: name = "max"; break; + case OP_FLOAT_MIN: name = "fp.min"; break; + case OP_FLOAT_MAX: name = "fp.max"; break; default: UNREACHABLE(); break; @@ -581,8 +581,9 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co op_names.push_back(builtin_name("isSubnormal", OP_FLOAT_IS_SUBNORMAL)); op_names.push_back(builtin_name("isSignMinus", OP_FLOAT_IS_SIGN_MINUS)); - op_names.push_back(builtin_name("min", OP_FLOAT_MIN)); - op_names.push_back(builtin_name("max", OP_FLOAT_MAX)); + // Disabled min/max, clashes with user-defined min/max functions + // op_names.push_back(builtin_name("min", OP_FLOAT_MIN)); + // op_names.push_back(builtin_name("max", OP_FLOAT_MAX)); op_names.push_back(builtin_name("asFloat", OP_TO_FLOAT)); diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index b41aa2238..b579d698e 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -911,18 +911,34 @@ void bit_blaster_tpl::mk_shl(unsigned sz, expr * const * a_bits, expr * con out_bits.push_back(a_bits[i]); } else { - expr_ref_vector eqs(m()); - mk_eqs(sz, b_bits, eqs); - for (unsigned i = 0; i < sz; i++) { + out_bits.append(sz, a_bits); + + unsigned i = 0; + expr_ref_vector new_out_bits(m()); + for (; i < sz; ++i) { checkpoint(); - expr_ref out(m()); - mk_ite(eqs.get(i), a_bits[0], m().mk_false(), out); - for (unsigned j = 1; j <= i; j++) { + unsigned shift_i = 1 << i; + if (shift_i >= sz) break; + for (unsigned j = 0; j < sz; ++j) { expr_ref new_out(m()); - mk_ite(eqs.get(i - j), a_bits[j], out, new_out); - out = new_out; + expr* a_j = m().mk_false(); + if (shift_i <= j) a_j = out_bits[j-shift_i].get(); + mk_ite(b_bits[i], a_j, out_bits[j].get(), new_out); + new_out_bits.push_back(new_out); } - out_bits.push_back(out); + out_bits.reset(); + out_bits.append(new_out_bits); + new_out_bits.reset(); + } + expr_ref is_large(m()); + is_large = m().mk_false(); + for (; i < sz; ++i) { + mk_or(is_large, b_bits[i], is_large); + } + for (unsigned j = 0; j < sz; ++j) { + expr_ref new_out(m()); + mk_ite(is_large, m().mk_false(), out_bits[j].get(), new_out); + out_bits[j] = new_out; } } } @@ -939,19 +955,32 @@ void bit_blaster_tpl::mk_lshr(unsigned sz, expr * const * a_bits, expr * co out_bits.push_back(m().mk_false()); } else { - expr_ref_vector eqs(m()); - mk_eqs(sz, b_bits, eqs); - out_bits.resize(sz); - for (unsigned i = 0; i < sz; i++) { + out_bits.append(sz, a_bits); + unsigned i = 0; + for (; i < sz; ++i) { checkpoint(); - expr_ref out(m()); - mk_ite(eqs.get(i), a_bits[sz-1], m().mk_false(), out); - for (unsigned j = 1; j <= i; j++) { + expr_ref_vector new_out_bits(m()); + unsigned shift_i = 1 << i; + if (shift_i >= sz) break; + for (unsigned j = 0; j < sz; ++j) { expr_ref new_out(m()); - mk_ite(eqs.get(i - j), a_bits[sz - j - 1], out, new_out); - out = new_out; + expr* a_j = m().mk_false(); + if (shift_i + j < sz) a_j = out_bits[j+shift_i].get(); + mk_ite(b_bits[i], a_j, out_bits[j].get(), new_out); + new_out_bits.push_back(new_out); } - out_bits.set(sz - i - 1, out); + out_bits.reset(); + out_bits.append(new_out_bits); + } + expr_ref is_large(m()); + is_large = m().mk_false(); + for (; i < sz; ++i) { + mk_or(is_large, b_bits[i], is_large); + } + for (unsigned j = 0; j < sz; ++j) { + expr_ref new_out(m()); + mk_ite(is_large, m().mk_false(), out_bits[j].get(), new_out); + out_bits[j] = new_out; } } } @@ -968,20 +997,32 @@ void bit_blaster_tpl::mk_ashr(unsigned sz, expr * const * a_bits, expr * co out_bits.push_back(a_bits[sz-1]); } else { - expr_ref_vector eqs(m()); - mk_eqs(sz, b_bits, eqs); - out_bits.resize(sz); - for (unsigned i = 0; i < sz; i++) { + out_bits.append(sz, a_bits); + unsigned i = 0; + for (; i < sz; ++i) { checkpoint(); - expr_ref out(m()); - out = a_bits[sz-1]; - for (unsigned j = 1; j <= i; j++) { + expr_ref_vector new_out_bits(m()); + unsigned shift_i = 1 << i; + if (shift_i >= sz) break; + for (unsigned j = 0; j < sz; ++j) { expr_ref new_out(m()); - mk_ite(eqs.get(i - j), a_bits[sz - j - 1], out, new_out); - out = new_out; + expr* a_j = a_bits[sz-1]; + if (shift_i + j < sz) a_j = out_bits[j+shift_i].get(); + mk_ite(b_bits[i], a_j, out_bits[j].get(), new_out); + new_out_bits.push_back(new_out); } - TRACE("bit_blaster", tout << (sz - i - 1) << " :\n" << mk_pp(out, m()) << "\n";); - out_bits.set(sz - i - 1, out); + out_bits.reset(); + out_bits.append(new_out_bits); + } + expr_ref is_large(m()); + is_large = m().mk_false(); + for (; i < sz; ++i) { + mk_or(is_large, b_bits[i], is_large); + } + for (unsigned j = 0; j < sz; ++j) { + expr_ref new_out(m()); + mk_ite(is_large, a_bits[sz-1], out_bits[j].get(), new_out); + out_bits[j] = new_out; } } } diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 5d19c53e3..0e2c8e781 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -73,6 +73,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { m_a_rw.updt_params(p); m_bv_rw.updt_params(p); m_ar_rw.updt_params(p); + m_f_rw.updt_params(p); updt_local_params(p); } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 20539266b..ce2838aba 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -346,8 +346,14 @@ cmd_context::~cmd_context() { } void cmd_context::set_cancel(bool f) { - if (m_solver) - m_solver->set_cancel(f); + if (m_solver) { + if (f) { + m_solver->cancel(); + } + else { + m_solver->reset_cancel(); + } + } if (has_manager()) m().set_cancel(f); } diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp index 0ec44e0cf..254a1d931 100644 --- a/src/cmd_context/context_params.cpp +++ b/src/cmd_context/context_params.cpp @@ -86,7 +86,13 @@ void context_params::set(char const * param, char const * value) { set_bool(m_smtlib2_compliant, param, value); } else { - throw default_exception("unknown parameter '%s'", p.c_str()); + param_descrs d; + collect_param_descrs(d); + std::stringstream strm; + strm << "unknown parameter '" << p << "'\n"; + strm << "Legal parameters are:\n"; + d.display(strm, 2, false, false); + throw default_exception(strm.str()); } } @@ -114,15 +120,19 @@ void context_params::collect_param_descrs(param_descrs & d) { d.insert("well_sorted_check", CPK_BOOL, "type checker", "true"); d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true"); d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true"); - d.insert("proof", CPK_BOOL, "proof generation, it must be enabled when the Z3 context is created", "false"); d.insert("check_interpolants", CPK_BOOL, "check correctness of interpolants", "false"); - d.insert("model", CPK_BOOL, "model generation for solvers, this parameter can be overwritten when creating a solver", "true"); d.insert("model_validate", CPK_BOOL, "validate models produced by solvers", "false"); d.insert("trace", CPK_BOOL, "trace generation for VCC", "false"); d.insert("trace_file_name", CPK_STRING, "trace out file name (see option 'trace')", "z3.log"); - d.insert("unsat_core", CPK_BOOL, "unsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generation", "false"); d.insert("debug_ref_count", CPK_BOOL, "debug support for AST reference counting", "false"); d.insert("smtlib2_compliant", CPK_BOOL, "enable/disable SMT-LIB 2.0 compliance", "false"); + collect_solver_param_descrs(d); +} + +void context_params::collect_solver_param_descrs(param_descrs & d) { + d.insert("proof", CPK_BOOL, "proof generation, it must be enabled when the Z3 context is created", "false"); + d.insert("model", CPK_BOOL, "model generation for solvers, this parameter can be overwritten when creating a solver", "true"); + d.insert("unsat_core", CPK_BOOL, "unsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generation", "false"); } params_ref context_params::merge_default_params(params_ref const & p) { diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h index 7271bb84f..e26fd3fe5 100644 --- a/src/cmd_context/context_params.h +++ b/src/cmd_context/context_params.h @@ -55,6 +55,8 @@ public: */ void get_solver_params(ast_manager const & m, params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled); + static void collect_solver_param_descrs(param_descrs & d); + /** \brief Include in p parameters derived from this context_params. These are parameters that are meaningful for tactics and solvers. diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 27014bca9..75d56928e 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -500,7 +500,7 @@ static tactic * mk_using_params(cmd_context & ctx, sexpr * n) { symbol param_name = symbol(norm_param_name(c->get_symbol()).c_str()); c = n->get_child(i); i++; - switch (descrs.get_kind(param_name)) { + switch (descrs.get_kind_in_module(param_name)) { case CPK_INVALID: throw cmd_exception("invalid using-params combinator, unknown parameter ", param_name, c->get_line(), c->get_pos()); case CPK_BOOL: diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index f5d96e740..3f1883749 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -4117,7 +4117,6 @@ namespace polynomial { polynomial_ref H(m_wrapper), C(m_wrapper); polynomial_ref lc_H(m_wrapper); unsigned min_deg_q = UINT_MAX; - var next_x = vars[idx+1]; unsigned counter = 0; for (;; counter++) { @@ -4137,7 +4136,7 @@ namespace polynomial { var q_var = max_var(q); unsigned deg_q = q_var == null_var ? 0 : degree(q, q_var); TRACE("mgcd_detail", tout << "counter: " << counter << "\nidx: " << idx << "\nq: " << q << "\ndeg_q: " << deg_q << "\nmin_deg_q: " << - min_deg_q << "\nnext_x: x" << next_x << "\nmax_var(q): " << q_var << "\n";); + min_deg_q << "\nnext_x: x" << vars[idx+1] << "\nmax_var(q): " << q_var << "\n";); if (deg_q < min_deg_q) { TRACE("mgcd_detail", tout << "reseting...\n";); counter = 0; @@ -5113,10 +5112,9 @@ namespace polynomial { monomial const * m_r = R.m(max_R); numeral const & a_r = R.a(max_R); monomial * m_r_q = 0; - bool q_div_r = div(m_r, m_q, m_r_q); + VERIFY(div(m_r, m_q, m_r_q)); TRACE("polynomial", tout << "m_r: "; m_r->display(tout); tout << "\nm_q: "; m_q->display(tout); tout << "\n"; if (m_r_q) { tout << "m_r_q: "; m_r_q->display(tout); tout << "\n"; }); - SASSERT(q_div_r); m_r_q_ref = m_r_q; m_manager.div(a_r, a_q, a_r_q); C.add(a_r_q, m_r_q); // C <- C + (a_r/a_q)*(m_r/m_q) diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index ca7277d07..2548d1180 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -1109,11 +1109,11 @@ namespace datalog { void context::get_raw_rule_formulas(expr_ref_vector& rules, svector& names, vector &bounds){ for (unsigned i = 0; i < m_rule_fmls.size(); ++i) { - expr_ref r = bind_variables(m_rule_fmls[i].get(), true); - rules.push_back(r.get()); - // rules.push_back(m_rule_fmls[i].get()); - names.push_back(m_rule_names[i]); - bounds.push_back(m_rule_bounds[i]); + expr_ref r = bind_variables(m_rule_fmls[i].get(), true); + rules.push_back(r.get()); + // rules.push_back(m_rule_fmls[i].get()); + names.push_back(m_rule_names[i]); + bounds.push_back(m_rule_bounds[i]); } } diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index 94dd5d0a0..a1f3af401 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -47,6 +47,7 @@ Notes: #include "dl_boogie_proof.h" #include "qe_util.h" #include "scoped_proof.h" +#include "expr_safe_replace.h" namespace pdr { @@ -1062,10 +1063,7 @@ namespace pdr { predicates.pop_back(); for (unsigned i = rule->get_uninterpreted_tail_size(); i < rule->get_tail_size(); ++i) { subst.apply(2, deltas, expr_offset(rule->get_tail(i), 1), tmp); - dctx.get_rewriter()(tmp); - if (!m.is_true(tmp)) { - constraints.push_back(tmp); - } + constraints.push_back(tmp); } for (unsigned i = 0; i < constraints.size(); ++i) { max_var = std::max(vc.get_max_var(constraints[i].get()), max_var); @@ -1088,7 +1086,28 @@ namespace pdr { children.append(n->children()); } - return pm.mk_and(constraints); + + expr_safe_replace repl(m); + for (unsigned i = 0; i < constraints.size(); ++i) { + expr* e = constraints[i].get(), *e1, *e2; + if (m.is_eq(e, e1, e2) && is_var(e1) && is_ground(e2)) { + repl.insert(e1, e2); + } + else if (m.is_eq(e, e1, e2) && is_var(e2) && is_ground(e1)) { + repl.insert(e2, e1); + } + } + expr_ref_vector result(m); + for (unsigned i = 0; i < constraints.size(); ++i) { + expr_ref tmp(m); + tmp = constraints[i].get(); + repl(tmp); + dctx.get_rewriter()(tmp); + if (!m.is_true(tmp)) { + result.push_back(tmp); + } + } + return pm.mk_and(result); } proof_ref model_search::get_proof_trace(context const& ctx) { @@ -1221,6 +1240,7 @@ namespace pdr { remove_node(*m_root, false); dealloc(m_root); m_root = 0; + m_cache.reset(); } } @@ -1254,7 +1274,7 @@ namespace pdr { m_pm(m_fparams, params.max_num_contexts(), m), m_query_pred(m), m_query(0), - m_search(m_params.bfs_model_search(), m), + m_search(m_params.bfs_model_search()), m_last_result(l_undef), m_inductive_lvl(0), m_expanded_lvl(0), diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h index a85011600..e21f46412 100644 --- a/src/muz/pdr/pdr_context.h +++ b/src/muz/pdr/pdr_context.h @@ -245,7 +245,6 @@ namespace pdr { class model_search { typedef ptr_vector model_nodes; - ast_manager& m; bool m_bfs; model_node* m_root; std::deque m_leaves; @@ -258,7 +257,7 @@ namespace pdr { void enqueue_leaf(model_node& n); // add leaf to priority queue. void update_models(); public: - model_search(bool bfs, ast_manager& m): m(m), m_bfs(bfs), m_root(0) {} + model_search(bool bfs): m_bfs(bfs), m_root(0) {} ~model_search(); void reset(); diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp index 276e7b836..2a2507d7f 100644 --- a/src/muz/rel/dl_compiler.cpp +++ b/src/muz/rel/dl_compiler.cpp @@ -589,49 +589,8 @@ namespace datalog { dealloc = true; } - //enforce negative predicates - unsigned ut_len=r->get_uninterpreted_tail_size(); - for(unsigned i=pt_len; iget_tail(i); - func_decl * neg_pred = neg_tail->get_decl(); - variable_intersection neg_intersection(m_context.get_manager()); - neg_intersection.populate(single_res_expr, neg_tail); - unsigned_vector t_cols(neg_intersection.size(), neg_intersection.get_cols1()); - unsigned_vector neg_cols(neg_intersection.size(), neg_intersection.get_cols2()); - - unsigned neg_len = neg_tail->get_num_args(); - for(unsigned i=0; iget_arg(i); - if(is_var(e)) { - continue; - } - SASSERT(is_app(e)); - relation_sort arg_sort; - m_context.get_rel_context()->get_rmanager().from_predicate(neg_pred, i, arg_sort); - reg_idx new_reg; - bool new_dealloc; - make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, new_dealloc, acc); - - if (dealloc) - make_dealloc_non_void(filtered_res, acc); - dealloc = new_dealloc; - filtered_res = new_reg; // here filtered_res value gets changed !! - - t_cols.push_back(single_res_expr.size()); - neg_cols.push_back(i); - single_res_expr.push_back(e); - } - SASSERT(t_cols.size()==neg_cols.size()); - - reg_idx neg_reg = m_pred_regs.find(neg_pred); - if (!dealloc) - make_clone(filtered_res, filtered_res, acc); - acc.push_back(instruction::mk_filter_by_negation(filtered_res, neg_reg, t_cols.size(), - t_cols.c_ptr(), neg_cols.c_ptr())); - dealloc = true; - } - // enforce interpreted tail predicates + unsigned ut_len = r->get_uninterpreted_tail_size(); unsigned ft_len = r->get_tail_size(); // full tail ptr_vector tail; for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) { @@ -738,6 +697,47 @@ namespace datalog { dealloc = true; } + //enforce negative predicates + for (unsigned i = pt_len; iget_tail(i); + func_decl * neg_pred = neg_tail->get_decl(); + variable_intersection neg_intersection(m_context.get_manager()); + neg_intersection.populate(single_res_expr, neg_tail); + unsigned_vector t_cols(neg_intersection.size(), neg_intersection.get_cols1()); + unsigned_vector neg_cols(neg_intersection.size(), neg_intersection.get_cols2()); + + unsigned neg_len = neg_tail->get_num_args(); + for (unsigned i = 0; iget_arg(i); + if (is_var(e)) { + continue; + } + SASSERT(is_app(e)); + relation_sort arg_sort; + m_context.get_rel_context()->get_rmanager().from_predicate(neg_pred, i, arg_sort); + reg_idx new_reg; + bool new_dealloc; + make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, new_dealloc, acc); + + if (dealloc) + make_dealloc_non_void(filtered_res, acc); + dealloc = new_dealloc; + filtered_res = new_reg; // here filtered_res value gets changed !! + + t_cols.push_back(single_res_expr.size()); + neg_cols.push_back(i); + single_res_expr.push_back(e); + } + SASSERT(t_cols.size() == neg_cols.size()); + + reg_idx neg_reg = m_pred_regs.find(neg_pred); + if (!dealloc) + make_clone(filtered_res, filtered_res, acc); + acc.push_back(instruction::mk_filter_by_negation(filtered_res, neg_reg, t_cols.size(), + t_cols.c_ptr(), neg_cols.c_ptr())); + dealloc = true; + } + #if 0 // this version is potentially better for non-symbolic tables, // since it constraints each unbound column at a time (reducing the diff --git a/src/muz/rel/dl_vector_relation.h b/src/muz/rel/dl_vector_relation.h index 114f4ca43..4d0917359 100644 --- a/src/muz/rel/dl_vector_relation.h +++ b/src/muz/rel/dl_vector_relation.h @@ -62,8 +62,6 @@ namespace datalog { dealloc(m_elems); } - virtual bool can_swap() const { return true; } - virtual void swap(relation_base& other) { vector_relation& o = dynamic_cast(other); if (&o == this) return; diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index 770a49c07..d229d8735 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -1449,10 +1449,23 @@ namespace qe { m_solver.assert_expr(m_fml); if (assumption) m_solver.assert_expr(assumption); - bool is_sat = false; - while (l_true == m_solver.check()) { - is_sat = true; - final_check(); + bool is_sat = false; + lbool res = l_true; + while (true) { + res = m_solver.check(); + if (res == l_true) { + is_sat = true; + final_check(); + } + else { + break; + } + } + if (res == l_undef) { + free_vars.append(num_vars, vars); + reset(); + m_solver.pop(1); + return; } if (!is_sat) { @@ -1484,12 +1497,13 @@ namespace qe { ); free_vars.append(m_free_vars); - SASSERT(!m_free_vars.empty() || m_solver.inconsistent()); + if (!m_free_vars.empty() || m_solver.inconsistent()) { - if (m_fml.get() != m_subfml.get()) { - scoped_ptr rp = mk_default_expr_replacer(m); - rp->apply_substitution(to_app(m_subfml.get()), fml, m_fml); - fml = m_fml; + if (m_fml.get() != m_subfml.get()) { + scoped_ptr rp = mk_default_expr_replacer(m); + rp->apply_substitution(to_app(m_subfml.get()), fml, m_fml); + fml = m_fml; + } } reset(); m_solver.pop(1); @@ -2224,8 +2238,7 @@ namespace qe { m_params(p), m_trail(m), m_qe(0), - m_assumption(m.mk_true()), - m_use_new_qe(true) + m_assumption(m.mk_true()) { } @@ -2247,12 +2260,6 @@ namespace qe { } void expr_quant_elim::updt_params(params_ref const& p) { - bool r = p.get_bool("use_neq_qe", m_use_new_qe); - if (r != m_use_new_qe) { - dealloc(m_qe); - m_qe = 0; - m_use_new_qe = r; - } init_qe(); m_qe->updt_params(p); } @@ -2260,7 +2267,6 @@ namespace qe { void expr_quant_elim::collect_param_descrs(param_descrs& r) { r.insert("eliminate_variables_as_block", CPK_BOOL, "(default: true) eliminate variables as a block (true) or one at a time (false)"); - // r.insert("use_new_qe", CPK_BOOL, "(default: true) invoke quantifier engine based on abstracted solver"); } void expr_quant_elim::init_qe() { @@ -2490,7 +2496,7 @@ namespace qe { class simplify_solver_context : public i_solver_context { ast_manager& m; - smt_params m_fparams; + smt_params m_fparams; app_ref_vector* m_vars; expr_ref* m_fml; ptr_vector m_contains; @@ -2506,6 +2512,10 @@ namespace qe { add_plugin(mk_arith_plugin(*this, false, m_fparams)); } + void updt_params(params_ref const& p) { + m_fparams.updt_params(p); + } + virtual ~simplify_solver_context() { reset(); } void solve(expr_ref& fml, app_ref_vector& vars) { @@ -2596,6 +2606,10 @@ namespace qe { public: impl(ast_manager& m) : m(m), m_ctx(m) {} + void updt_params(params_ref const& p) { + m_ctx.updt_params(p); + } + bool reduce_quantifier( quantifier * old_q, expr * new_body, @@ -2659,6 +2673,10 @@ namespace qe { return imp->reduce_quantifier(old_q, new_body, new_patterns, new_no_patterns, result, result_pr); } + void simplify_rewriter_cfg::updt_params(params_ref const& p) { + imp->updt_params(p); + } + bool simplify_rewriter_cfg::pre_visit(expr* e) { if (!is_quantifier(e)) return true; quantifier * q = to_quantifier(e); @@ -2666,7 +2684,6 @@ namespace qe { } void simplify_exists(app_ref_vector& vars, expr_ref& fml) { - smt_params params; ast_manager& m = fml.get_manager(); simplify_solver_context ctx(m); ctx.solve(fml, vars); diff --git a/src/qe/qe.h b/src/qe/qe.h index 1697a5cbd..0fd2ff60c 100644 --- a/src/qe/qe.h +++ b/src/qe/qe.h @@ -275,13 +275,12 @@ namespace qe { class expr_quant_elim { ast_manager& m; - smt_params const& m_fparams; + smt_params const& m_fparams; params_ref m_params; expr_ref_vector m_trail; obj_map m_visited; quant_elim* m_qe; expr* m_assumption; - bool m_use_new_qe; public: expr_quant_elim(ast_manager& m, smt_params const& fp, params_ref const& p = params_ref()); ~expr_quant_elim(); @@ -372,6 +371,8 @@ namespace qe { bool pre_visit(expr* e); + void updt_params(params_ref const& p); + }; class simplify_rewriter_star : public rewriter_tpl { @@ -380,6 +381,8 @@ namespace qe { simplify_rewriter_star(ast_manager& m): rewriter_tpl(m, false, m_cfg), m_cfg(m) {} + + void updt_params(params_ref const& p) { m_cfg.updt_params(p); } }; }; diff --git a/src/qe/qe_sat_tactic.cpp b/src/qe/qe_sat_tactic.cpp index b4a1a6a8b..2be32c02d 100644 --- a/src/qe/qe_sat_tactic.cpp +++ b/src/qe/qe_sat_tactic.cpp @@ -74,6 +74,7 @@ namespace qe { is_relevant_default m_is_relevant; mk_atom_default m_mk_atom; th_rewriter m_rewriter; + simplify_rewriter_star m_qe_rw; expr_strong_context_simplifier m_ctx_rewriter; class solver_context : public i_solver_context { @@ -218,6 +219,7 @@ namespace qe { m_Ms(m), m_assignments(m), m_rewriter(m), + m_qe_rw(m), m_ctx_rewriter(m_fparams, m) { m_fparams.m_model = true; } @@ -256,10 +258,9 @@ namespace qe { ptr_vector fmls; goal->get_formulas(fmls); m_fml = m.mk_and(fmls.size(), fmls.c_ptr()); - TRACE("qe", tout << "input: " << mk_pp(m_fml,m) << "\n";); - simplify_rewriter_star rw(m); + TRACE("qe", tout << "input: " << mk_pp(m_fml,m) << "\n";); expr_ref tmp(m); - rw(m_fml, tmp); + m_qe_rw(m_fml, tmp); m_fml = tmp; TRACE("qe", tout << "reduced: " << mk_pp(m_fml,m) << "\n";); skolemize_existential_prefix(); @@ -305,6 +306,8 @@ namespace qe { m_projection_mode_param = p.get_bool("projection_mode", m_projection_mode_param); m_strong_context_simplify_param = p.get_bool("strong_context_simplify", m_strong_context_simplify_param); m_ctx_simplify_local_param = p.get_bool("strong_context_simplify_local", m_ctx_simplify_local_param); + m_fparams.updt_params(p); + m_qe_rw.updt_params(p); } virtual void collect_param_descrs(param_descrs & r) { diff --git a/src/qe/qe_tactic.cpp b/src/qe/qe_tactic.cpp index 5b522e041..8819d704b 100644 --- a/src/qe/qe_tactic.cpp +++ b/src/qe/qe_tactic.cpp @@ -36,6 +36,7 @@ class qe_tactic : public tactic { } void updt_params(params_ref const & p) { + m_fparams.updt_params(p); m_fparams.m_nlquant_elim = p.get_bool("qe_nonlinear", false); m_qe.updt_params(p); } diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index b8ac520b2..193bf59f2 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -215,7 +215,7 @@ namespace sat { sat_asymm_branch_params::collect_param_descrs(d); } - void asymm_branch::collect_statistics(statistics & st) { + void asymm_branch::collect_statistics(statistics & st) const { st.update("elim literals", m_elim_literals); } diff --git a/src/sat/sat_asymm_branch.h b/src/sat/sat_asymm_branch.h index 6ffd239eb..f10522fab 100644 --- a/src/sat/sat_asymm_branch.h +++ b/src/sat/sat_asymm_branch.h @@ -49,7 +49,7 @@ namespace sat { void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); - void collect_statistics(statistics & st); + void collect_statistics(statistics & st) const; void reset_statistics(); void dec(unsigned c) { m_counter -= c; } diff --git a/src/sat/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp index 4b1ac2c92..959f5e94f 100644 --- a/src/sat/sat_cleaner.cpp +++ b/src/sat/sat_cleaner.cpp @@ -206,7 +206,7 @@ namespace sat { m_elim_literals = 0; } - void cleaner::collect_statistics(statistics & st) { + void cleaner::collect_statistics(statistics & st) const { st.update("elim clauses", m_elim_clauses); st.update("elim literals", m_elim_literals); } diff --git a/src/sat/sat_cleaner.h b/src/sat/sat_cleaner.h index d4306afcd..d22408926 100644 --- a/src/sat/sat_cleaner.h +++ b/src/sat/sat_cleaner.h @@ -42,7 +42,7 @@ namespace sat { bool operator()(bool force = false); - void collect_statistics(statistics & st); + void collect_statistics(statistics & st) const; void reset_statistics(); void dec() { m_cleanup_counter--; } diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index cc0f97ff0..fb81809b1 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -68,7 +68,10 @@ namespace sat { m_restart_factor = p.restart_factor(); m_random_freq = p.random_freq(); - + m_random_seed = p.random_seed(); + if (m_random_seed == 0) + m_random_seed = _p.get_uint("random_seed", 0); + m_burst_search = p.burst_search(); m_max_conflicts = p.max_conflicts(); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 90ebe968b..253786e11 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -53,6 +53,7 @@ namespace sat { unsigned m_restart_initial; double m_restart_factor; // for geometric case double m_random_freq; + unsigned m_random_seed; unsigned m_burst_search; unsigned m_max_conflicts; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 71579b86a..de0283897 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -9,6 +9,7 @@ def_module_params('sat', ('restart.initial', UINT, 100, 'initial restart (number of conflicts)'), ('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'), ('random_freq', DOUBLE, 0.01, 'frequency of random case splits'), + ('random_seed', UINT, 0, 'random seed'), ('burst_search', UINT, 100, 'number of conflicts before first global simplification'), ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts'), ('gc', SYMBOL, 'glue_psm', 'garbage collection strategy: psm, glue, glue_psm, dyn_psm'), diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp index f9741cd7b..165d39ad8 100644 --- a/src/sat/sat_probing.cpp +++ b/src/sat/sat_probing.cpp @@ -196,6 +196,7 @@ namespace sat { s.propagate(false); // make sure propagation queue is empty if (s.inconsistent()) return true; + SASSERT(s.m_qhead == s.m_trail.size()); CASSERT("probing", s.check_invariant()); if (!force && m_counter > 0) return true; @@ -259,7 +260,7 @@ namespace sat { m_to_assert.finalize(); } - void probing::collect_statistics(statistics & st) { + void probing::collect_statistics(statistics & st) const { st.update("probing assigned", m_num_assigned); } diff --git a/src/sat/sat_probing.h b/src/sat/sat_probing.h index 9f3c1ae87..2061b74bd 100644 --- a/src/sat/sat_probing.h +++ b/src/sat/sat_probing.h @@ -71,7 +71,7 @@ namespace sat { void free_memory(); - void collect_statistics(statistics & st); + void collect_statistics(statistics & st) const; void reset_statistics(); // return the literals implied by l. diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp index 29f3f006f..ffbdb31c6 100644 --- a/src/sat/sat_scc.cpp +++ b/src/sat/sat_scc.cpp @@ -223,7 +223,7 @@ namespace sat { return to_elim.size(); } - void scc::collect_statistics(statistics & st) { + void scc::collect_statistics(statistics & st) const { st.update("elim bool vars", m_num_elim); } diff --git a/src/sat/sat_scc.h b/src/sat/sat_scc.h index c85cc7d42..5f69e11c6 100644 --- a/src/sat/sat_scc.h +++ b/src/sat/sat_scc.h @@ -40,7 +40,7 @@ namespace sat { void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); - void collect_statistics(statistics & st); + void collect_statistics(statistics & st) const; void reset_statistics(); }; }; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index f20ffa7c7..219b9f278 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -918,7 +918,11 @@ namespace sat { void process(literal l) { TRACE("blocked_clause", tout << "processing: " << l << "\n";); model_converter::entry * new_entry = 0; + if (s.is_external(l.var()) || s.was_eliminated(l.var())) + return; + { + m_to_remove.reset(); { clause_use_list & occs = s.m_use_list.get(l); @@ -1339,6 +1343,7 @@ namespace sat { } TRACE("resolution", tout << "found var to eliminate, before: " << before_clauses << " after: " << after_clauses << "\n";); + // eliminate variable model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v); save_clauses(mc_entry, m_pos_cls); @@ -1466,7 +1471,7 @@ namespace sat { sat_simplifier_params::collect_param_descrs(r); } - void simplifier::collect_statistics(statistics & st) { + void simplifier::collect_statistics(statistics & st) const { st.update("subsumed", m_num_subsumed); st.update("subsumption resolution", m_num_sub_res); st.update("elim literals", m_num_elim_lits); diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index 96d346598..cb6fa9557 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -180,7 +180,7 @@ namespace sat { void free_memory(); - void collect_statistics(statistics & st); + void collect_statistics(statistics & st) const; void reset_statistics(); }; }; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index f4bf5393c..f898130af 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -46,7 +46,7 @@ namespace sat { m_qhead(0), m_scope_lvl(0), m_params(p) { - m_config.updt_params(p); + updt_params(p); } solver::~solver() { @@ -459,9 +459,6 @@ namespace sat { void solver::set_conflict(justification c, literal not_l) { if (m_inconsistent) return; - TRACE("sat_conflict", tout << "conflict\n";); - // int * p = 0; - // *p = 0; m_inconsistent = true; m_conflict = c; m_not_l = not_l; @@ -863,6 +860,7 @@ namespace sat { m_next_simplify = 0; m_stopwatch.reset(); m_stopwatch.start(); + TRACE("sat", display(tout);); } /** @@ -1972,7 +1970,7 @@ namespace sat { m_asymm_branch.updt_params(p); m_probing.updt_params(p); m_scc.updt_params(p); - m_rand.set_seed(p.get_uint("random_seed", 0)); + m_rand.set_seed(m_config.m_random_seed); } void solver::collect_param_descrs(param_descrs & d) { diff --git a/src/smt/arith_eq_solver.cpp b/src/smt/arith_eq_solver.cpp index 41a61bf73..9a6868ff1 100644 --- a/src/smt/arith_eq_solver.cpp +++ b/src/smt/arith_eq_solver.cpp @@ -604,7 +604,9 @@ bool arith_eq_solver::solve_integer_equations_gcd( } SASSERT(g == r0[i]); } - SASSERT(abs(r0[i]).is_one()); + if (!abs(r0[i]).is_one()) { + return false; + } live.erase(live.begin()+live_pos); for (j = 0; j < live.size(); ++j) { row& r = rows[live[j]]; diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index f1c407dc7..18619c8ec 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -19,10 +19,11 @@ Revision History: #include"smt_params.h" #include"smt_params_helper.hpp" #include"model_params.hpp" +#include"gparams.h" void smt_params::updt_local_params(params_ref const & _p) { smt_params_helper p(_p); - m_auto_config = p.auto_config(); + m_auto_config = p.auto_config() && gparams::get_value("auto_config") == "true"; // auto-config is not scoped by smt in gparams. m_random_seed = p.random_seed(); m_relevancy_lvl = p.relevancy(); m_ematching = p.ematching(); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 4f3c73ce6..f3f2d4948 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1615,6 +1615,8 @@ namespace smt { unsigned qhead = m_qhead; if (!bcp()) return false; + if (m_cancel_flag) + return true; SASSERT(!inconsistent()); propagate_relevancy(qhead); if (inconsistent()) @@ -3945,7 +3947,7 @@ namespace smt { m_fingerprints.display(tout); ); failure fl = get_last_search_failure(); - if (fl == TIMEOUT || fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS || fl == THEORY) { + if (fl == TIMEOUT || fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS) { // don't generate model. return; } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 5abdfa5f9..24a4c0f45 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -76,7 +76,7 @@ namespace smt { protected: ast_manager & m_manager; - smt_params & m_fparams; + smt_params & m_fparams; params_ref m_params; setup m_setup; volatile bool m_cancel_flag; diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 526447f9f..7053d63ec 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -136,9 +136,8 @@ namespace smt { if (cex == 0) return false; // no model available. unsigned num_decls = q->get_num_decls(); - unsigned num_sks = sks.size(); // Remark: sks were created for the flat version of q. - SASSERT(num_sks >= num_decls); + SASSERT(sks.size() >= num_decls); expr_ref_buffer bindings(m_manager); bindings.resize(num_decls); unsigned max_generation = 0; diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index e9b0e069a..b76fb6c74 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -453,9 +453,9 @@ namespace smt { instantiated. */ virtual void add(quantifier * q) { - if (m_fparams->m_mbqi && mbqi_enabled(q)) { - m_model_finder->register_quantifier(q); - } + if (m_fparams->m_mbqi && mbqi_enabled(q)) { + m_model_finder->register_quantifier(q); + } } virtual void del(quantifier * q) { diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 998dd72e6..d1af762bb 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -410,6 +410,7 @@ namespace smt { atoms m_atoms; // set of theory atoms ptr_vector m_asserted_bounds; // set of asserted bounds unsigned m_asserted_qhead; + ptr_vector m_new_atoms; // new bound atoms that have yet to be internalized. svector m_nl_monomials; // non linear monomials svector m_nl_propagated; // non linear monomials that became linear v_dependency_manager m_dep_manager; // for tracking bounds during non-linear reasoning @@ -570,6 +571,22 @@ namespace smt { void mk_clause(literal l1, literal l2, unsigned num_params, parameter * params); void mk_clause(literal l1, literal l2, literal l3, unsigned num_params, parameter * params); void mk_bound_axioms(atom * a); + void mk_bound_axiom(atom* a1, atom* a2); + void flush_bound_axioms(); + typename atoms::iterator next_sup(atom* a1, atom_kind kind, + typename atoms::iterator it, + typename atoms::iterator end, + bool& found_compatible); + typename atoms::iterator next_inf(atom* a1, atom_kind kind, + typename atoms::iterator it, + typename atoms::iterator end, + bool& found_compatible); + typename atoms::iterator first(atom_kind kind, + typename atoms::iterator it, + typename atoms::iterator end); + struct compare_atoms { + bool operator()(atom* a1, atom* a2) const { return a1->get_k() < a2->get_k(); } + }; virtual bool default_internalizer() const { return false; } virtual bool internalize_atom(app * n, bool gate_ctx); virtual bool internalize_term(app * term); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index fbc043048..66d232227 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -348,13 +348,24 @@ namespace smt { context & ctx = get_context(); simplifier & s = ctx.get_simplifier(); expr_ref s_ante(m), s_conseq(m); + expr* s_conseq_n, * s_ante_n; + bool negated; proof_ref pr(m); + s(ante, s_ante, pr); + negated = m.is_not(s_ante, s_ante_n); + if (negated) s_ante = s_ante_n; ctx.internalize(s_ante, false); literal l_ante = ctx.get_literal(s_ante); + if (negated) l_ante.neg(); + s(conseq, s_conseq, pr); + negated = m.is_not(s_conseq, s_conseq_n); + if (negated) s_conseq = s_conseq_n; ctx.internalize(s_conseq, false); literal l_conseq = ctx.get_literal(s_conseq); + if (negated) l_conseq.neg(); + literal lits[2] = {l_ante, l_conseq}; ctx.mk_th_axiom(get_id(), 2, lits); if (ctx.relevancy()) { @@ -800,48 +811,238 @@ namespace smt { template void theory_arith::mk_bound_axioms(atom * a1) { theory_var v = a1->get_var(); - literal l1(a1->get_bool_var()); + atoms & occs = m_var_occs[v]; + if (!get_context().is_searching()) { + // + // NB. We make an assumption that user push calls propagation + // before internal scopes are pushed. This flushes all newly + // asserted atoms into the right context. + // + m_new_atoms.push_back(a1); + return; + } numeral const & k1(a1->get_k()); atom_kind kind1 = a1->get_atom_kind(); TRACE("mk_bound_axioms", tout << "making bound axioms for v" << v << " " << kind1 << " " << k1 << "\n";); - atoms & occs = m_var_occs[v]; typename atoms::iterator it = occs.begin(); typename atoms::iterator end = occs.end(); + + typename atoms::iterator lo_inf = end, lo_sup = end; + typename atoms::iterator hi_inf = end, hi_sup = end; for (; it != end; ++it) { - atom * a2 = *it; - literal l2(a2->get_bool_var()); - numeral const & k2 = a2->get_k(); - atom_kind kind2 = a2->get_atom_kind(); + atom * a2 = *it; + numeral const & k2(a2->get_k()); + atom_kind kind2 = a2->get_atom_kind(); SASSERT(k1 != k2 || kind1 != kind2); - SASSERT(a2->get_var() == v); - parameter coeffs[3] = { parameter(symbol("farkas")), parameter(rational(1)), parameter(rational(1)) }; - if (kind1 == A_LOWER) { - if (kind2 == A_LOWER) { - // x >= k1, x >= k2 - if (k1 >= k2) mk_clause(~l1, l2, 3, coeffs); - else mk_clause(~l2, l1, 3, coeffs); + if (kind2 == A_LOWER) { + if (k2 < k1) { + if (lo_inf == end || k2 > (*lo_inf)->get_k()) { + lo_inf = it; + } } - else { - // x >= k1, x <= k2 - if (k1 > k2) mk_clause(~l1, ~l2, 3, coeffs); - else mk_clause(l1, l2, 3, coeffs); + else if (lo_sup == end || k2 < (*lo_sup)->get_k()) { + lo_sup = it; } } - else { - if (kind2 == A_LOWER) { - // x <= k1, x >= k2 - if (k1 < k2) mk_clause(~l1, ~l2, 3, coeffs); - else mk_clause(l1, l2, 3, coeffs); + else if (k2 < k1) { + if (hi_inf == end || k2 > (*hi_inf)->get_k()) { + hi_inf = it; + } + } + else if (hi_sup == end || k2 < (*hi_sup)->get_k()) { + hi_sup = it; + } + } + if (lo_inf != end) mk_bound_axiom(a1, *lo_inf); + if (lo_sup != end) mk_bound_axiom(a1, *lo_sup); + if (hi_inf != end) mk_bound_axiom(a1, *hi_inf); + if (hi_sup != end) mk_bound_axiom(a1, *hi_sup); + } + + template + void theory_arith::mk_bound_axiom(atom* a1, atom* a2) { + theory_var v = a1->get_var(); + literal l1(a1->get_bool_var()); + literal l2(a2->get_bool_var()); + numeral const & k1(a1->get_k()); + numeral const & k2(a2->get_k()); + atom_kind kind1 = a1->get_atom_kind(); + atom_kind kind2 = a2->get_atom_kind(); + bool v_is_int = is_int(v); + SASSERT(v == a2->get_var()); + SASSERT(k1 != k2 || kind1 != kind2); + parameter coeffs[3] = { parameter(symbol("farkas")), + parameter(rational(1)), parameter(rational(1)) }; + + if (kind1 == A_LOWER) { + if (kind2 == A_LOWER) { + if (k2 <= k1) { + mk_clause(~l1, l2, 3, coeffs); } else { - // x <= k1, x <= k2 - if (k1 < k2) mk_clause(~l1, l2, 3, coeffs); - else mk_clause(~l2, l1, 3, coeffs); + mk_clause(l1, ~l2, 3, coeffs); + } + } + else if (k1 <= k2) { + // k1 <= k2, k1 <= x or x <= k2 + mk_clause(l1, l2, 3, coeffs); + } + else { + // k1 > hi_inf, k1 <= x => ~(x <= hi_inf) + mk_clause(~l1, ~l2, 3, coeffs); + if (v_is_int && k1 == k2 + numeral(1)) { + // k1 <= x or x <= k1-1 + mk_clause(l1, l2, 3, coeffs); } } } + else if (kind2 == A_LOWER) { + if (k1 >= k2) { + // k1 >= lo_inf, k1 >= x or lo_inf <= x + mk_clause(l1, l2, 3, coeffs); + } + else { + // k1 < k2, k2 <= x => ~(x <= k1) + mk_clause(~l1, ~l2, 3, coeffs); + if (v_is_int && k1 == k2 - numeral(1)) { + // x <= k1 or k1+l <= x + mk_clause(l1, l2, 3, coeffs); + } + + } + } + else { + // kind1 == A_UPPER, kind2 == A_UPPER + if (k1 >= k2) { + // k1 >= k2, x <= k2 => x <= k1 + mk_clause(l1, ~l2, 3, coeffs); + } + else { + // k1 <= hi_sup , x <= k1 => x <= hi_sup + mk_clause(~l1, l2, 3, coeffs); + } + } } + template + void theory_arith::flush_bound_axioms() { + while (!m_new_atoms.empty()) { + ptr_vector atoms; + atoms.push_back(m_new_atoms.back()); + m_new_atoms.pop_back(); + theory_var v = atoms.back()->get_var(); + for (unsigned i = 0; i < m_new_atoms.size(); ++i) { + if (m_new_atoms[i]->get_var() == v) { + atoms.push_back(m_new_atoms[i]); + m_new_atoms[i] = m_new_atoms.back(); + m_new_atoms.pop_back(); + --i; + } + } + ptr_vector occs(m_var_occs[v]); + + std::sort(atoms.begin(), atoms.end(), compare_atoms()); + std::sort(occs.begin(), occs.end(), compare_atoms()); + + typename atoms::iterator begin1 = occs.begin(); + typename atoms::iterator begin2 = occs.begin(); + typename atoms::iterator end = occs.end(); + begin1 = first(A_LOWER, begin1, end); + begin2 = first(A_UPPER, begin2, end); + + typename atoms::iterator lo_inf = begin1, lo_sup = begin1; + typename atoms::iterator hi_inf = begin2, hi_sup = begin2; + typename atoms::iterator lo_inf1 = begin1, lo_sup1 = begin1; + typename atoms::iterator hi_inf1 = begin2, hi_sup1 = begin2; + bool flo_inf, fhi_inf, flo_sup, fhi_sup; + ptr_addr_hashtable visited; + for (unsigned i = 0; i < atoms.size(); ++i) { + atom* a1 = atoms[i]; + lo_inf1 = next_inf(a1, A_LOWER, lo_inf, end, flo_inf); + hi_inf1 = next_inf(a1, A_UPPER, hi_inf, end, fhi_inf); + lo_sup1 = next_sup(a1, A_LOWER, lo_sup, end, flo_sup); + hi_sup1 = next_sup(a1, A_UPPER, hi_sup, end, fhi_sup); + if (lo_inf1 != end) lo_inf = lo_inf1; + if (lo_sup1 != end) lo_sup = lo_sup1; + if (hi_inf1 != end) hi_inf = hi_inf1; + if (hi_sup1 != end) hi_sup = hi_sup1; + if (!flo_inf) lo_inf = end; + if (!fhi_inf) hi_inf = end; + if (!flo_sup) lo_sup = end; + if (!fhi_sup) hi_sup = end; + visited.insert(a1); + if (lo_inf1 != end && lo_inf != end && !visited.contains(*lo_inf)) mk_bound_axiom(a1, *lo_inf); + if (lo_sup1 != end && lo_sup != end && !visited.contains(*lo_sup)) mk_bound_axiom(a1, *lo_sup); + if (hi_inf1 != end && hi_inf != end && !visited.contains(*hi_inf)) mk_bound_axiom(a1, *hi_inf); + if (hi_sup1 != end && hi_sup != end && !visited.contains(*hi_sup)) mk_bound_axiom(a1, *hi_sup); + } + } + } + + template + typename theory_arith::atoms::iterator + theory_arith::first( + atom_kind kind, + typename atoms::iterator it, + typename atoms::iterator end) { + for (; it != end; ++it) { + atom* a = *it; + if (a->get_atom_kind() == kind) return it; + } + return end; + } + + template + typename theory_arith::atoms::iterator + theory_arith::next_inf( + atom* a1, + atom_kind kind, + typename atoms::iterator it, + typename atoms::iterator end, + bool& found_compatible) { + numeral const & k1(a1->get_k()); + typename atoms::iterator result = end; + found_compatible = false; + for (; it != end; ++it) { + atom * a2 = *it; + if (a1 == a2) continue; + if (a2->get_atom_kind() != kind) continue; + numeral const & k2(a2->get_k()); + found_compatible = true; + if (k2 <= k1) { + result = it; + } + else { + break; + } + } + return result; + } + + template + typename theory_arith::atoms::iterator + theory_arith::next_sup( + atom* a1, + atom_kind kind, + typename atoms::iterator it, + typename atoms::iterator end, + bool& found_compatible) { + numeral const & k1(a1->get_k()); + found_compatible = false; + for (; it != end; ++it) { + atom * a2 = *it; + if (a1 == a2) continue; + if (a2->get_atom_kind() != kind) continue; + numeral const & k2(a2->get_k()); + found_compatible = true; + if (k1 < k2) { + return it; + } + } + return end; + } + + template bool theory_arith::internalize_atom(app * n, bool gate_ctx) { TRACE("arith_internalize", tout << "internalising atom:\n" << mk_pp(n, this->get_manager()) << "\n";); @@ -879,7 +1080,7 @@ namespace smt { bool_var bv = ctx.mk_bool_var(n); ctx.set_var_theory(bv, get_id()); rational _k; - m_util.is_numeral(rhs, _k); + VERIFY(m_util.is_numeral(rhs, _k)); numeral k(_k); atom * a = alloc(atom, bv, v, k, kind); mk_bound_axioms(a); @@ -927,6 +1128,7 @@ namespace smt { template void theory_arith::assign_eh(bool_var v, bool is_true) { + TRACE("arith", tout << "v" << v << " " << is_true << "\n";); atom * a = get_bv2a(v); if (!a) return; SASSERT(get_context().get_assignment(a->get_bool_var()) != l_undef); @@ -1072,8 +1274,10 @@ namespace smt { } } while (m_final_check_idx != old_idx); - if (result == FC_DONE && m_found_unsupported_op) + if (result == FC_DONE && m_found_unsupported_op) { + TRACE("arith", tout << "Found unsupported operation\n";); result = FC_GIVEUP; + } return result; } @@ -1142,6 +1346,7 @@ namespace smt { CASSERT("arith", wf_columns()); CASSERT("arith", valid_row_assignment()); + flush_bound_axioms(); propagate_linear_monomials(); while (m_asserted_qhead < m_asserted_bounds.size()) { bound * b = m_asserted_bounds[m_asserted_qhead]; @@ -2421,6 +2626,8 @@ namespace smt { if (val == l_undef) continue; // TODO: check if the following line is a bottleneck + TRACE("arith", tout << "v" << a->get_bool_var() << " " << (val == l_true) << "\n";); + a->assign_eh(val == l_true, get_epsilon(a->get_var())); if (val != l_undef && a->get_bound_kind() == b->get_bound_kind()) { SASSERT((ctx.get_assignment(bv) == l_true) == a->is_true()); @@ -2916,6 +3123,7 @@ namespace smt { SASSERT(m_to_patch.empty()); m_to_check.reset(); m_in_to_check.reset(); + m_new_atoms.reset(); CASSERT("arith", wf_rows()); CASSERT("arith", wf_columns()); CASSERT("arith", valid_row_assignment()); diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index e0ecc087a..0a70e2645 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -1294,8 +1294,10 @@ namespace smt { } tout << "max: " << max << ", min: " << min << "\n";); - if (m_params.m_arith_ignore_int) + if (m_params.m_arith_ignore_int) { + TRACE("arith", tout << "Ignore int: give up\n";); return FC_GIVEUP; + } if (!gcd_test()) return FC_CONTINUE; diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index d02c9e540..6a7017a29 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -2314,13 +2314,15 @@ namespace smt { return FC_DONE; } - if (!m_params.m_nl_arith) + if (!m_params.m_nl_arith) { + TRACE("non_linear", tout << "Non-linear is not enabled\n";); return FC_GIVEUP; + } TRACE("process_non_linear", display(tout);); if (m_nl_rounds > m_params.m_nl_arith_rounds) { - TRACE("non_linear", tout << "GIVE UP non linear problem...\n";); + TRACE("non_linear", tout << "GIVEUP non linear problem...\n";); IF_VERBOSE(3, verbose_stream() << "Max. non linear arithmetic rounds. Increase threshold using NL_ARITH_ROUNDS=\n";); return FC_GIVEUP; } diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 8b3021573..6bcae6f60 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -53,6 +53,7 @@ namespace smt { unsigned bv_size = get_bv_size(n); context & ctx = get_context(); literal_vector & bits = m_bits[v]; + bits.reset(); for (unsigned i = 0; i < bv_size; i++) { app * bit = mk_bit2bool(owner, i); ctx.internalize(bit, true); @@ -75,12 +76,14 @@ namespace smt { void theory_bv::mk_bit2bool(app * n) { context & ctx = get_context(); SASSERT(!ctx.b_internalized(n)); - if (!ctx.e_internalized(n->get_arg(0))) { + + expr* first_arg = n->get_arg(0); + + if (!ctx.e_internalized(first_arg)) { // This may happen if bit2bool(x) is in a conflict // clause that is being reinitialized, and x was not reinitialized // yet. - // So, we internalize x (i.e., n->get_arg(0)) - expr * first_arg = n->get_arg(0); + // So, we internalize x (i.e., arg) ctx.internalize(first_arg, false); SASSERT(ctx.e_internalized(first_arg)); // In most cases, when x is internalized, its bits are created. @@ -91,10 +94,27 @@ namespace smt { // This will also force the creation of all bits for x. enode * first_arg_enode = ctx.get_enode(first_arg); get_var(first_arg_enode); - SASSERT(ctx.b_internalized(n)); + // numerals are not blasted into bit2bool, so we do this directly. + if (!ctx.b_internalized(n)) { + rational val; + unsigned sz; + VERIFY(m_util.is_numeral(first_arg, val, sz)); + theory_var v = first_arg_enode->get_th_var(get_id()); + app* owner = first_arg_enode->get_owner(); + for (unsigned i = 0; i < sz; ++i) { + ctx.internalize(mk_bit2bool(owner, i), true); + } + m_bits[v].reset(); + rational bit; + for (unsigned i = 0; i < sz; ++i) { + div(val, rational::power_of_two(i), bit); + mod(bit, rational(2), bit); + m_bits[v].push_back(bit.is_zero()?false_literal:true_literal); + } + } } else { - enode * arg = ctx.get_enode(n->get_arg(0)); + enode * arg = ctx.get_enode(first_arg); // The argument was already internalized, but it may not have a theory variable associated with it. // For example, for ite-terms the method apply_sort_cnstr is not invoked. // See comment in the then-branch. @@ -1041,6 +1061,7 @@ namespace smt { void theory_bv::new_diseq_eh(theory_var v1, theory_var v2) { if (is_bv(v1)) { + SASSERT(m_bits[v1].size() == m_bits[v2].size()); expand_diseq(v1, v2); } } @@ -1381,6 +1402,7 @@ namespace smt { if (v1 != null_theory_var) { // conflict was detected ... v1 and v2 have complementary bits SASSERT(m_bits[v1][it->m_idx] == ~(m_bits[v2][it->m_idx])); + SASSERT(m_bits[v1].size() == m_bits[v2].size()); mk_new_diseq_axiom(v1, v2, it->m_idx); RESET_MERGET_AUX(); return false; diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 390803957..a2e1ece40 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -983,11 +983,8 @@ template void theory_diff_logic::get_eq_antecedents( theory_var v1, theory_var v2, unsigned timestamp, conflict_resolution & cr) { imp_functor functor(cr); - bool r; - r = m_graph.find_shortest_zero_edge_path(v1, v2, timestamp, functor); - SASSERT(r); - r = m_graph.find_shortest_zero_edge_path(v2, v1, timestamp, functor); - SASSERT(r); + VERIFY(m_graph.find_shortest_zero_edge_path(v1, v2, timestamp, functor)); + VERIFY(m_graph.find_shortest_zero_edge_path(v2, v1, timestamp, functor)); } template diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index a98e5be49..dfbb62f65 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -218,8 +218,14 @@ public: } virtual void set_cancel(bool f) { - m_solver1->set_cancel(f); - m_solver2->set_cancel(f); + if (f) { + m_solver1->cancel(); + m_solver2->cancel(); + } + else { + m_solver1->reset_cancel(); + m_solver2->reset_cancel(); + } } virtual void set_progress_callback(progress_callback * callback) { diff --git a/src/solver/solver.h b/src/solver/solver.h index e047bace1..a95c649c0 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -99,7 +99,6 @@ public: */ virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) = 0; - virtual void set_cancel(bool f) {} /** \brief Interrupt this solver. */ @@ -130,6 +129,9 @@ public: \brief Display the content of this solver. */ virtual void display(std::ostream & out) const; +protected: + virtual void set_cancel(bool f) = 0; + }; #endif diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 1268fbcea..fb4898ecd 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -173,8 +173,12 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass } void tactic2solver::set_cancel(bool f) { - if (m_tactic.get()) - m_tactic->set_cancel(f); + if (m_tactic.get()) { + if (f) + m_tactic->cancel(); + else + m_tactic->reset_cancel(); + } } void tactic2solver::collect_statistics(statistics & st) const { diff --git a/src/tactic/aig/aig.h b/src/tactic/aig/aig.h index c8befd9b2..291bfbcf3 100644 --- a/src/tactic/aig/aig.h +++ b/src/tactic/aig/aig.h @@ -73,8 +73,6 @@ public: void display(std::ostream & out, aig_ref const & r) const; void display_smt2(std::ostream & out, aig_ref const & r) const; unsigned get_num_aigs() const; - void cancel() { set_cancel(true); } - void reset_cancel() { set_cancel(false); } void set_cancel(bool f); }; diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp index d396359a3..9bf967be3 100644 --- a/src/tactic/arith/add_bounds_tactic.cpp +++ b/src/tactic/arith/add_bounds_tactic.cpp @@ -172,18 +172,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m, m_params); #pragma omp critical (tactic_cancel) { - d = m_imp; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } protected: diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp index a1aa0bdc8..e8fb72be4 100644 --- a/src/tactic/arith/degree_shift_tactic.cpp +++ b/src/tactic/arith/degree_shift_tactic.cpp @@ -319,18 +319,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } protected: diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp index b534c8295..1a33bf4f2 100644 --- a/src/tactic/arith/diff_neq_tactic.cpp +++ b/src/tactic/arith/diff_neq_tactic.cpp @@ -398,20 +398,13 @@ public: } virtual void cleanup() { - unsigned num_conflicts = m_imp->m_num_conflicts; - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m, m_params); + d->m_num_conflicts = m_imp->m_num_conflicts; #pragma omp critical (tactic_cancel) { - d = m_imp; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } - m_imp->m_num_conflicts = num_conflicts; } protected: diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp index 4eec83037..dc17a4f87 100644 --- a/src/tactic/arith/factor_tactic.cpp +++ b/src/tactic/arith/factor_tactic.cpp @@ -333,18 +333,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } virtual void set_cancel(bool f) { diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp index d2e3ebf1f..693066ee1 100644 --- a/src/tactic/arith/fix_dl_var_tactic.cpp +++ b/src/tactic/arith/fix_dl_var_tactic.cpp @@ -338,18 +338,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } virtual void set_cancel(bool f) { diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp index c4b7cbaf3..c180029ae 100644 --- a/src/tactic/arith/fm_tactic.cpp +++ b/src/tactic/arith/fm_tactic.cpp @@ -1682,18 +1682,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } virtual void operator()(goal_ref const & in, diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index 9ee8f6728..33d5f138e 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -345,18 +345,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m, m_params); #pragma omp critical (tactic_cancel) { - d = m_imp; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } protected: diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp index a62b311b5..323903f6c 100644 --- a/src/tactic/arith/normalize_bounds_tactic.cpp +++ b/src/tactic/arith/normalize_bounds_tactic.cpp @@ -191,17 +191,12 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m, m_params); #pragma omp critical (tactic_cancel) { - d = m_imp; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } protected: diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index 89195a9d5..643195b05 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -1002,17 +1002,12 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m, m_params); #pragma omp critical (tactic_cancel) { - d = m_imp; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } protected: diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp index 12954005f..d7e4f30d2 100644 --- a/src/tactic/arith/propagate_ineqs_tactic.cpp +++ b/src/tactic/arith/propagate_ineqs_tactic.cpp @@ -548,16 +548,10 @@ void propagate_ineqs_tactic::set_cancel(bool f) { } void propagate_ineqs_tactic::cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m, m_params); #pragma omp critical (tactic_cancel) { - d = m_imp; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp index 3b1a86345..3d222cf56 100644 --- a/src/tactic/arith/recover_01_tactic.cpp +++ b/src/tactic/arith/recover_01_tactic.cpp @@ -425,18 +425,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m, m_params); #pragma omp critical (tactic_cancel) { - d = m_imp; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } protected: diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp index 0330141cb..33423c8b1 100644 --- a/src/tactic/bv/bit_blaster_tactic.cpp +++ b/src/tactic/bv/bit_blaster_tactic.cpp @@ -140,18 +140,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m(); - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m(), m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } unsigned get_num_steps() const { diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp index 8dcaf2112..5f20015ca 100644 --- a/src/tactic/bv/bv1_blaster_tactic.cpp +++ b/src/tactic/bv/bv1_blaster_tactic.cpp @@ -465,18 +465,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m(); - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m(), m_params); #pragma omp critical (tactic_cancel) { - d = m_imp; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } unsigned get_num_steps() const { diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index d3fdb6e56..e149afc75 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -392,17 +392,11 @@ void bv_size_reduction_tactic::set_cancel(bool f) { } void bv_size_reduction_tactic::cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp index f60487d60..56b18dd8d 100644 --- a/src/tactic/bv/max_bv_sharing_tactic.cpp +++ b/src/tactic/bv/max_bv_sharing_tactic.cpp @@ -311,18 +311,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m(); - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m(), m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } virtual void set_cancel(bool f) { diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp index 1f560ef62..aca6d9084 100644 --- a/src/tactic/core/cofactor_elim_term_ite.cpp +++ b/src/tactic/core/cofactor_elim_term_ite.cpp @@ -683,12 +683,7 @@ cofactor_elim_term_ite::cofactor_elim_term_ite(ast_manager & m, params_ref const } cofactor_elim_term_ite::~cofactor_elim_term_ite() { - imp * d = m_imp; - #pragma omp critical (cofactor_elim_term_ite) - { - m_imp = 0; - } - dealloc(d); + dealloc(m_imp); } void cofactor_elim_term_ite::updt_params(params_ref const & p) { @@ -704,19 +699,17 @@ void cofactor_elim_term_ite::operator()(expr * t, expr_ref & r) { } void cofactor_elim_term_ite::set_cancel(bool f) { - #pragma omp critical (cofactor_elim_term_ite) - { - if (m_imp) - m_imp->set_cancel(f); - } + if (m_imp) + m_imp->set_cancel(f); } void cofactor_elim_term_ite::cleanup() { - ast_manager & m = m_imp->m; - #pragma omp critical (cofactor_elim_term_ite) + ast_manager & m = m_imp->m; + imp * d = alloc(imp, m, m_params); + #pragma omp critical (tactic_cancel) { - dealloc(m_imp); - m_imp = alloc(imp, m, m_params); + std::swap(d, m_imp); } + dealloc(d); } diff --git a/src/tactic/core/cofactor_elim_term_ite.h b/src/tactic/core/cofactor_elim_term_ite.h index ce2f31ea0..e734fcad6 100644 --- a/src/tactic/core/cofactor_elim_term_ite.h +++ b/src/tactic/core/cofactor_elim_term_ite.h @@ -37,8 +37,9 @@ public: void cancel() { set_cancel(true); } void reset_cancel() { set_cancel(false); } - void set_cancel(bool f); void cleanup(); + void set_cancel(bool f); + }; #endif diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 71f4771a9..bb38d28ce 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -548,16 +548,11 @@ void ctx_simplify_tactic::set_cancel(bool f) { void ctx_simplify_tactic::cleanup() { ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } diff --git a/src/tactic/core/der_tactic.cpp b/src/tactic/core/der_tactic.cpp index c2245b409..2277c3fa8 100644 --- a/src/tactic/core/der_tactic.cpp +++ b/src/tactic/core/der_tactic.cpp @@ -90,17 +90,12 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m(); - imp * d = m_imp; + imp * d = alloc(imp, m); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } virtual void set_cancel(bool f) { diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp index 456bad5e0..e49884004 100644 --- a/src/tactic/core/elim_term_ite_tactic.cpp +++ b/src/tactic/core/elim_term_ite_tactic.cpp @@ -174,17 +174,12 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } virtual void set_cancel(bool f) { diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 4d64bf061..6d7bcb2f2 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -1036,18 +1036,13 @@ public: virtual void cleanup() { unsigned num_elim_apps = get_num_elim_apps(); - ast_manager & m = m_imp->m_manager; - imp * d = m_imp; + ast_manager & m = m_imp->m_manager; + imp * d = alloc(imp, m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } m_imp->m_num_elim_apps = num_elim_apps; } diff --git a/src/tactic/core/occf_tactic.cpp b/src/tactic/core/occf_tactic.cpp index f8f6174b9..9b974ae19 100644 --- a/src/tactic/core/occf_tactic.cpp +++ b/src/tactic/core/occf_tactic.cpp @@ -225,18 +225,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } protected: diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp index 1e358177f..5873efd61 100644 --- a/src/tactic/core/propagate_values_tactic.cpp +++ b/src/tactic/core/propagate_values_tactic.cpp @@ -255,17 +255,12 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m(); - imp * d = m_imp; + imp * d = alloc(imp, m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } protected: diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index 59ed2dcd3..99375e6e8 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -541,17 +541,12 @@ void reduce_args_tactic::set_cancel(bool f) { } void reduce_args_tactic::cleanup() { - ast_manager & m = m_imp->m(); - imp * d = m_imp; + ast_manager & m = m_imp->m(); + imp * d = alloc(imp, m); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp index 95db962a7..39f10e10c 100644 --- a/src/tactic/core/simplify_tactic.cpp +++ b/src/tactic/core/simplify_tactic.cpp @@ -115,17 +115,12 @@ void simplify_tactic::set_cancel(bool f) { void simplify_tactic::cleanup() { ast_manager & m = m_imp->m(); - imp * d = m_imp; + imp * d = alloc(imp, m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } unsigned simplify_tactic::get_num_steps() const { diff --git a/src/tactic/core/simplify_tactic.h b/src/tactic/core/simplify_tactic.h index fc9cb393c..1ba5a6da8 100644 --- a/src/tactic/core/simplify_tactic.h +++ b/src/tactic/core/simplify_tactic.h @@ -43,9 +43,11 @@ public: virtual void cleanup(); unsigned get_num_steps() const; - virtual void set_cancel(bool f); virtual tactic * translate(ast_manager & m) { return alloc(simplify_tactic, m, m_params); } +protected: + virtual void set_cancel(bool f); + }; tactic * mk_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()); diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index 995940406..3b0a57d20 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -749,23 +749,19 @@ public: virtual void cleanup() { unsigned num_elim_vars = m_imp->m_num_eliminated_vars; ast_manager & m = m_imp->m(); - imp * d = m_imp; expr_replacer * r = m_imp->m_r; if (r) r->set_substitution(0); bool owner = m_imp->m_r_owner; m_imp->m_r_owner = false; // stole replacer + + imp * d = alloc(imp, m, m_params, r, owner); + d->m_num_eliminated_vars = num_elim_vars; #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params, r, owner); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } - m_imp->m_num_eliminated_vars = num_elim_vars; } virtual void collect_statistics(statistics & st) const { diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp index b6c4b0655..c5be7ab1f 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/src/tactic/core/tseitin_cnf_tactic.cpp @@ -898,20 +898,14 @@ public: } virtual void cleanup() { - unsigned num_aux_vars = m_imp->m_num_aux_vars; ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m, m_params); + d->m_num_aux_vars = m_imp->m_num_aux_vars; #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } - m_imp->m_num_aux_vars = num_aux_vars; } virtual void set_cancel(bool f) { diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index 3a6b7ea45..4a3a01b6f 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -138,19 +138,13 @@ public: (*m_imp)(in, result, mc, pc, core); } - virtual void cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + virtual void cleanup() { + imp * d = alloc(imp, m_imp->m, m_params); #pragma omp critical (tactic_cancel) { - d = m_imp; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } protected: diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index ea5d60668..6783d9621 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -557,17 +557,12 @@ public: } virtual void cleanup() { - imp * d = m_imp; + imp * d = alloc(imp, m, m_params, m_stats); #pragma omp critical (tactic_cancel) { - d = m_imp; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params, m_stats); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } virtual void collect_statistics(statistics & st) const { diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index 80de1bcd0..8b4f9f576 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -47,7 +47,6 @@ public: void cancel(); void reset_cancel(); - virtual void set_cancel(bool f) {} /** \brief Apply tactic to goal \c in. @@ -96,6 +95,13 @@ public: // translate tactic to the given manager virtual tactic * translate(ast_manager & m) = 0; +private: + friend class nary_tactical; + friend class binary_tactical; + friend class unary_tactical; + + virtual void set_cancel(bool f) {} + }; typedef ref tactic_ref; diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index ca66b7a14..cfb4ec194 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -102,11 +102,8 @@ protected: \brief Reset cancel flag of t if this was not canceled. */ void parent_reset_cancel(tactic & t) { - #pragma omp critical (tactic_cancel) - { - if (!m_cancel) { - t.set_cancel(false); - } + if (!m_cancel) { + t.reset_cancel(); } } @@ -393,11 +390,8 @@ protected: \brief Reset cancel flag of st if this was not canceled. */ void parent_reset_cancel(tactic & t) { - #pragma omp critical (tactic_cancel) - { - if (!m_cancel) { - t.set_cancel(false); - } + if (!m_cancel) { + t.reset_cancel(); } } @@ -988,7 +982,7 @@ protected: virtual void set_cancel(bool f) { m_cancel = f; if (m_t) - m_t->set_cancel(f); + m_t->set_cancel(f); } template @@ -1282,7 +1276,7 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - if (m_p->operator()(*(in.get())).is_true()) + if (m_p->operator()(*(in.get())).is_true()) m_t1->operator()(in, result, mc, pc, core); else m_t2->operator()(in, result, mc, pc, core); diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp index 14a42ec51..2f0262fc8 100644 --- a/src/tactic/ufbv/macro_finder_tactic.cpp +++ b/src/tactic/ufbv/macro_finder_tactic.cpp @@ -144,17 +144,12 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m(); - imp * d = m_imp; + imp * d = alloc(imp, m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } virtual void set_cancel(bool f) { diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp index 393a40603..cea8f2cfc 100644 --- a/src/tactic/ufbv/quasi_macros_tactic.cpp +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -151,17 +151,12 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m(); - imp * d = m_imp; + imp * d = alloc(imp, m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } virtual void set_cancel(bool f) { diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp index 0705c627c..efecb38ba 100644 --- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp +++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp @@ -119,17 +119,12 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m(); - imp * d = m_imp; + imp * d = alloc(imp, m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } virtual void set_cancel(bool f) { diff --git a/src/util/bit_vector.cpp b/src/util/bit_vector.cpp index 6885b93e8..1490b9628 100644 --- a/src/util/bit_vector.cpp +++ b/src/util/bit_vector.cpp @@ -138,9 +138,8 @@ bool bit_vector::operator==(bit_vector const & source) const { bit_vector & bit_vector::operator|=(bit_vector const & source) { if (size() < source.size()) resize(source.size(), false); - unsigned n1 = num_words(); unsigned n2 = source.num_words(); - SASSERT(n2 <= n1); + SASSERT(n2 <= num_words()); unsigned bit_rest = source.m_num_bits % 32; if (bit_rest == 0) { unsigned i = 0; diff --git a/src/util/cmd_context_types.h b/src/util/cmd_context_types.h index b0a0226e8..e334dc0d2 100644 --- a/src/util/cmd_context_types.h +++ b/src/util/cmd_context_types.h @@ -55,12 +55,12 @@ class cmd_exception : public default_exception { } public: cmd_exception(char const * msg):default_exception(msg), m_line(-1), m_pos(-1) {} - cmd_exception(std::string const & msg):default_exception(msg.c_str()), m_line(-1), m_pos(-1) {} - cmd_exception(std::string const & msg, int line, int pos):default_exception(msg.c_str()), m_line(line), m_pos(pos) {} + cmd_exception(std::string const & msg):default_exception(msg), m_line(-1), m_pos(-1) {} + cmd_exception(std::string const & msg, int line, int pos):default_exception(msg), m_line(line), m_pos(pos) {} cmd_exception(char const * msg, symbol const & s): - default_exception(compose(msg,s).c_str()),m_line(-1),m_pos(-1) {} + default_exception(compose(msg,s)),m_line(-1),m_pos(-1) {} cmd_exception(char const * msg, symbol const & s, int line, int pos): - default_exception(compose(msg,s).c_str()),m_line(line),m_pos(pos) {} + default_exception(compose(msg,s)),m_line(line),m_pos(pos) {} bool has_pos() const { return m_line >= 0; } int line() const { SASSERT(has_pos()); return m_line; } diff --git a/src/util/debug.h b/src/util/debug.h index 9e519982f..a36743f73 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -73,7 +73,7 @@ bool is_debug_enabled(const char * tag); UNREACHABLE(); \ } #else -#define VERIFY(_x_) (_x_) +#define VERIFY(_x_) (void)(_x_) #endif #define MAKE_NAME2(LINE) zofty_ ## LINE diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 1d9426390..adffe6bde 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -201,7 +201,7 @@ public: } } - void throw_unknown_parameter(symbol const & param_name, symbol const & mod_name) { + void throw_unknown_parameter(symbol const & param_name, param_descrs const& d, symbol const & mod_name) { if (mod_name == symbol::null) { char const * new_name = get_new_param_name(param_name); if (new_name) { @@ -213,11 +213,56 @@ public: param_name.bare_str()); } else { - throw exception("unknown parameter '%s'", param_name.bare_str()); + std::stringstream strm; + strm << "unknown parameter '" << param_name << "'\n"; + strm << "Legal parameters are:\n"; + d.display(strm, 2, false, false); + throw default_exception(strm.str()); } } else { - throw exception("unknown parameter '%s' at module '%s'", param_name.bare_str(), mod_name.bare_str()); + std::stringstream strm; + strm << "unknown parameter '" << param_name << "' "; + strm << "at module '" << mod_name << "'\n"; + strm << "Legal parameters are:\n"; + d.display(strm, 2, false, false); + throw default_exception(strm.str()); + } + } + + void validate_type(symbol const& name, char const* value, param_descrs const& d) { + param_kind k = d.get_kind(name); + std::stringstream strm; + char const* _value = value; + switch (k) { + case CPK_UINT: + for (; *value; ++value) { + if (!('0' <= *value && *value <= '9')) { + strm << "Expected values for parameter " << name + << " is an unsigned integer. It was given argument '" << _value << "'"; + throw default_exception(strm.str()); + } + } + break; + case CPK_DOUBLE: + for (; *value; ++value) { + if (!('0' <= *value && *value <= '9') && *value != '.' && *value != '-' && *value != '/') { + strm << "Expected values for parameter " << name + << " is a double. It was given argument '" << _value << "'"; + throw default_exception(strm.str()); + } + } + break; + + case CPK_BOOL: + if (strcmp(value, "true") != 0 && strcmp(value, "false") != 0) { + strm << "Expected values for parameter " << name + << " are 'true' or 'false'. It was given argument '" << value << "'"; + throw default_exception(strm.str()); + } + break; + default: + break; } } @@ -225,7 +270,7 @@ public: param_kind k = d.get_kind(param_name); params_ref & ps = get_params(mod_name); if (k == CPK_INVALID) { - throw_unknown_parameter(param_name, mod_name); + throw_unknown_parameter(param_name, d, mod_name); } else if (k == CPK_UINT) { long val = strtol(value, 0, 10); @@ -282,11 +327,13 @@ public: symbol m, p; normalize(name, m, p); if (m == symbol::null) { + validate_type(p, value, get_param_descrs()); set(get_param_descrs(), p, value, m); } else { param_descrs * d; if (get_module_param_descrs().find(m, d)) { + validate_type(p, value, *d); set(*d, p, value, m); } else { @@ -312,7 +359,7 @@ public: std::string get_default(param_descrs const & d, symbol const & p, symbol const & m) { if (!d.contains(p)) { - throw_unknown_parameter(p, m); + throw_unknown_parameter(p, d, m); } char const * r = d.get_default(p); if (r == 0) @@ -478,7 +525,7 @@ public: throw exception("unknown module '%s'", m.bare_str()); } if (!d->contains(p)) - throw_unknown_parameter(p, m); + throw_unknown_parameter(p, *d, m); out << " name: " << p << "\n"; if (m != symbol::null) { out << " module: " << m << "\n"; diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 3f2e224d9..45088d5d4 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -35,6 +35,7 @@ static long long g_memory_max_used_size = 0; static long long g_memory_watermark = 0; static bool g_exit_when_out_of_memory = false; static char const * g_out_of_memory_msg = "ERROR: out of memory"; +static volatile bool g_memory_fully_initialized = false; void memory::exit_when_out_of_memory(bool flag, char const * msg) { g_exit_when_out_of_memory = flag; @@ -83,10 +84,18 @@ void memory::initialize(size_t max_size) { initialize = true; } } - if (!initialize) - return; - g_memory_out_of_memory = false; - mem_initialize(); + if (initialize) { + g_memory_out_of_memory = false; + mem_initialize(); + g_memory_fully_initialized = true; + } + else { + // Delay the current thread until the DLL is fully initialized + // Without this, multiple threads can start to call API functions + // before memory::initialize(...) finishes. + while (!g_memory_fully_initialized) + /* wait */ ; + } } bool memory::is_out_of_memory() { @@ -98,9 +107,9 @@ bool memory::is_out_of_memory() { return r; } -void memory::set_high_watermark(size_t watermak) { +void memory::set_high_watermark(size_t watermark) { // This method is only safe to invoke at initialization time, that is, before the threads are created. - g_memory_watermark = watermak; + g_memory_watermark = watermark; } bool memory::above_high_watermark() { diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 8cb6ed4fc..f5785c072 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -120,7 +120,8 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, double value) { // double === mpf(11, 53) COMPILE_TIME_ASSERT(sizeof(double) == 8); - uint64 raw = *reinterpret_cast(&value); + uint64 raw; + memcpy(&raw, &value, sizeof(double)); bool sign = (raw >> 63) != 0; int64 e = ((raw & 0x7FF0000000000000ull) >> 52) - 1023; uint64 s = raw & 0x000FFFFFFFFFFFFFull; @@ -155,7 +156,8 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, float value) { // single === mpf(8, 24) COMPILE_TIME_ASSERT(sizeof(float) == 4); - unsigned int raw = *reinterpret_cast(&value); + unsigned int raw; + memcpy(&raw, &value, sizeof(float)); bool sign = (raw >> 31) != 0; signed int e = ((raw & 0x7F800000) >> 23) - 127; unsigned int s = raw & 0x007FFFFF; @@ -1288,7 +1290,9 @@ double mpf_manager::to_double(mpf const & x) { if (x.sign) raw = raw | 0x8000000000000000ull; - return *reinterpret_cast(&raw); + double ret; + memcpy(&ret, &raw, sizeof(double)); + return ret; } float mpf_manager::to_float(mpf const & x) { @@ -1318,7 +1322,9 @@ float mpf_manager::to_float(mpf const & x) { if (x.sign) raw = raw | 0x80000000; - return *reinterpret_cast(&raw); + float ret; + memcpy(&ret, &raw, sizeof(float)); + return ret; } bool mpf_manager::is_nan(mpf const & x) { @@ -1679,7 +1685,7 @@ void mpf_manager::round(mpf_rounding_mode rm, mpf & o) { TRACE("mpf_dbg", tout << "OVF2 = " << OVF2 << std::endl;); TRACE("mpf_dbg", tout << "o_has_max_exp = " << o_has_max_exp << std::endl;); - if (!OVFen && SIGovf && o_has_max_exp) + if (!OVFen && OVF2) mk_round_inf(rm, o); else { const mpz & p = m_powers2(o.sbits-1); diff --git a/src/util/mpff.cpp b/src/util/mpff.cpp index 892a7fe24..7678a051e 100644 --- a/src/util/mpff.cpp +++ b/src/util/mpff.cpp @@ -43,8 +43,7 @@ mpff_manager::mpff_manager(unsigned prec, unsigned initial_capacity) { for (unsigned i = 0; i < MPFF_NUM_BUFFERS; i++) m_buffers[i].resize(2 * prec, 0); // Reserve space for zero - unsigned zero_sig_idx = m_id_gen.mk(); - SASSERT(zero_sig_idx == 0); + VERIFY(m_id_gen.mk() == 0); set(m_one, 1); } diff --git a/src/util/mpfx.cpp b/src/util/mpfx.cpp index cf6f8338f..c0b3a1936 100644 --- a/src/util/mpfx.cpp +++ b/src/util/mpfx.cpp @@ -38,8 +38,7 @@ mpfx_manager::mpfx_manager(unsigned int_sz, unsigned frac_sz, unsigned initial_c m_buffer0.resize(2*m_total_sz, 0); m_buffer1.resize(2*m_total_sz, 0); m_buffer2.resize(2*m_total_sz, 0); - unsigned zero_sig_idx = m_id_gen.mk(); - SASSERT(zero_sig_idx == 0); + VERIFY(m_id_gen.mk() == 0); set(m_one, 1); } diff --git a/src/util/mpq.cpp b/src/util/mpq.cpp index eda937029..df4d207a6 100644 --- a/src/util/mpq.cpp +++ b/src/util/mpq.cpp @@ -235,6 +235,9 @@ void mpq_manager::set(mpq & a, char const * val) { SASSERT(str[0] - '0' <= 9); exp = (10*exp) + (str[0] - '0'); } + else if ('/' == str[0]) { + throw default_exception("mixing rational/scientific notation"); + } TRACE("mpq_set", tout << "[exp]: " << exp << ", str[0]: " << (str[0] - '0') << std::endl;); ++str; } diff --git a/src/util/params.cpp b/src/util/params.cpp index 4aff0de92..b869f8e3d 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -51,31 +51,34 @@ struct param_descrs::imp { param_kind m_kind; char const * m_descr; char const * m_default; + char const * m_module; - info(param_kind k, char const * descr, char const * def): + info(param_kind k, char const * descr, char const * def, char const* module): m_kind(k), m_descr(descr), - m_default(def) { + m_default(def), + m_module(module) { } info(): m_kind(CPK_INVALID), m_descr(0), - m_default(0) { + m_default(0), + m_module(0) { } }; dictionary m_info; svector m_names; - void insert(symbol const & name, param_kind k, char const * descr, char const * def) { + void insert(symbol const & name, param_kind k, char const * descr, char const * def, char const* module) { SASSERT(!name.is_numerical()); info i; if (m_info.find(name, i)) { SASSERT(i.m_kind == k); return; } - m_info.insert(name, info(k, descr, def)); + m_info.insert(name, info(k, descr, def, module)); m_names.push_back(name); } @@ -94,6 +97,42 @@ struct param_descrs::imp { return CPK_INVALID; } + bool split_name(symbol const& name, symbol & prefix, symbol & suffix) const { + if (name.is_numerical()) return false; + char const* str = name.bare_str(); + char const* period = strchr(str,'.'); + if (!period) return false; + svector prefix_((unsigned)(period-str), str); + prefix_.push_back(0); + prefix = symbol(prefix_.c_ptr()); + suffix = symbol(period + 1); + return true; + } + + param_kind get_kind_in_module(symbol & name) const { + param_kind k = get_kind(name); + symbol prefix, suffix; + if (k == CPK_INVALID && split_name(name, prefix, suffix)) { + k = get_kind(suffix); + if (k != CPK_INVALID) { + if (symbol(get_module(suffix)) == prefix) { + name = suffix; + } + else { + k = CPK_INVALID; + } + } + } + return k; + } + + char const* get_module(symbol const& name) const { + info i; + if (m_info.find(name, i)) + return i.m_module; + return 0; + } + char const * get_descr(symbol const & name) const { info i; if (m_info.find(name, i)) @@ -162,7 +201,7 @@ struct param_descrs::imp { dictionary::iterator it = other.m_imp->m_info.begin(); dictionary::iterator end = other.m_imp->m_info.end(); for (; it != end; ++it) { - insert(it->m_key, it->m_value.m_kind, it->m_value.m_descr, it->m_value.m_default); + insert(it->m_key, it->m_value.m_kind, it->m_value.m_descr, it->m_value.m_default, it->m_value.m_module); } } @@ -180,12 +219,12 @@ void param_descrs::copy(param_descrs & other) { m_imp->copy(other); } -void param_descrs::insert(symbol const & name, param_kind k, char const * descr, char const * def) { - m_imp->insert(name, k, descr, def); +void param_descrs::insert(symbol const & name, param_kind k, char const * descr, char const * def, char const* module) { + m_imp->insert(name, k, descr, def, module); } -void param_descrs::insert(char const * name, param_kind k, char const * descr, char const * def) { - insert(symbol(name), k, descr, def); +void param_descrs::insert(char const * name, param_kind k, char const * descr, char const * def, char const* module) { + insert(symbol(name), k, descr, def, module); } bool param_descrs::contains(char const * name) const { @@ -220,6 +259,10 @@ void param_descrs::erase(char const * name) { erase(symbol(name)); } +param_kind param_descrs::get_kind_in_module(symbol & name) const { + return m_imp->get_kind_in_module(name); +} + param_kind param_descrs::get_kind(symbol const & name) const { return m_imp->get_kind(name); } @@ -236,6 +279,10 @@ symbol param_descrs::get_param_name(unsigned i) const { return m_imp->get_param_name(i); } +char const* param_descrs::get_module(symbol const& name) const { + return m_imp->get_module(name); +} + void param_descrs::display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const { return m_imp->display(out, indent, smt2_style, include_descr); } @@ -297,15 +344,27 @@ public: void reset(symbol const & k); void reset(char const * k); - void validate(param_descrs const & p) const { - svector::const_iterator it = m_entries.begin(); - svector::const_iterator end = m_entries.end(); + + void validate(param_descrs const & p) { + svector::iterator it = m_entries.begin(); + svector::iterator end = m_entries.end(); + symbol suffix, prefix; for (; it != end; ++it) { - param_kind expected = p.get_kind(it->first); - if (expected == CPK_INVALID) - throw default_exception("unknown parameter '%s'", it->first.str().c_str()); - if (it->second.m_kind != expected) - throw default_exception("parameter kind mismatch '%s'", it->first.str().c_str()); + param_kind expected = p.get_kind_in_module(it->first); + if (expected == CPK_INVALID) { + std::stringstream strm; + strm << "unknown parameter '" << it->first.str() << "'\n"; + strm << "Legal parameters are:\n"; + p.display(strm, 2, false, false); + throw default_exception(strm.str()); + } + if (it->second.m_kind != expected && + !(it->second.m_kind == CPK_UINT && expected == CPK_NUMERAL)) { + std::stringstream strm; + strm << "Parameter " << it->first.str() << " was given argument of type "; + strm << it->second.m_kind << ", expected " << expected; + throw default_exception(strm.str()); + } } } @@ -347,11 +406,11 @@ public: out << "(params"; svector::const_iterator it = m_entries.begin(); svector::const_iterator end = m_entries.end(); - for (; it != end; ++it) { - out << " " << it->first; + for (; it != end; ++it) { + out << " " << it->first; switch (it->second.m_kind) { case CPK_BOOL: - out << " " << it->second.m_bool_value; + out << " " << (it->second.m_bool_value?"true":"false"); break; case CPK_UINT: out << " " <second.m_uint_value; @@ -376,6 +435,41 @@ public: out << ")"; } + void display_smt2(std::ostream & out, char const* module, param_descrs& descrs) const { + svector::const_iterator it = m_entries.begin(); + svector::const_iterator end = m_entries.end(); + for (; it != end; ++it) { + if (!descrs.contains(it->first)) continue; + out << "(set-option :"; + out << module << "."; + out << it->first; + switch (it->second.m_kind) { + case CPK_BOOL: + out << " " << (it->second.m_bool_value?"true":"false"); + break; + case CPK_UINT: + out << " " <second.m_uint_value; + break; + case CPK_DOUBLE: + out << " " << it->second.m_double_value; + break; + case CPK_NUMERAL: + out << " " << *(it->second.m_rat_value); + break; + case CPK_SYMBOL: + out << " " << symbol::mk_symbol_from_c_ptr(it->second.m_sym_value); + break; + case CPK_STRING: + out << " " << it->second.m_str_value; + break; + default: + UNREACHABLE(); + break; + } + out << ")\n"; + } + } + void display(std::ostream & out, symbol const & k) const { svector::const_iterator it = m_entries.begin(); svector::const_iterator end = m_entries.end(); @@ -423,10 +517,17 @@ params_ref::params_ref(params_ref const & p): void params_ref::display(std::ostream & out) const { if (m_params) m_params->display(out); - else + else out << "(params)"; } +void params_ref::display_smt2(std::ostream& out, char const* module, param_descrs& descrs) const { + if (m_params) + m_params->display_smt2(out, module, descrs); + +} + + void params_ref::display(std::ostream & out, char const * k) const { display(out, symbol(k)); } @@ -438,7 +539,7 @@ void params_ref::display(std::ostream & out, symbol const & k) const { out << "default"; } -void params_ref::validate(param_descrs const & p) const { +void params_ref::validate(param_descrs const & p) { if (m_params) m_params->validate(p); } diff --git a/src/util/params.h b/src/util/params.h index 15be825b0..e4a2b3693 100644 --- a/src/util/params.h +++ b/src/util/params.h @@ -90,8 +90,9 @@ public: void set_sym(char const * k, symbol const & v); void display(std::ostream & out) const; + void display_smt2(std::ostream& out, char const* module, param_descrs& module_desc) const; - void validate(param_descrs const & p) const; + void validate(param_descrs const & p); /* \brief Display the value of the given parameter. @@ -114,14 +115,15 @@ public: param_descrs(); ~param_descrs(); void copy(param_descrs & other); - void insert(char const * name, param_kind k, char const * descr, char const * def = 0); - void insert(symbol const & name, param_kind k, char const * descr, char const * def = 0); + void insert(char const * name, param_kind k, char const * descr, char const * def = 0, char const* module = 0); + void insert(symbol const & name, param_kind k, char const * descr, char const * def = 0, char const* module = 0); bool contains(char const * name) const; bool contains(symbol const & name) const; void erase(char const * name); void erase(symbol const & name); param_kind get_kind(char const * name) const; param_kind get_kind(symbol const & name) const; + param_kind get_kind_in_module(symbol & name) const; char const * get_descr(char const * name) const; char const * get_descr(symbol const & name) const; char const * get_default(char const * name) const; @@ -129,6 +131,7 @@ public: void display(std::ostream & out, unsigned indent = 0, bool smt2_style=false, bool include_descr=true) const; unsigned size() const; symbol get_param_name(unsigned idx) const; + char const * get_module(symbol const& name) const; }; void insert_max_memory(param_descrs & r); diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index c4a640009..15891168c 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -129,7 +129,7 @@ struct scoped_timer::imp { WT_EXECUTEINTIMERTHREAD); #elif defined(__APPLE__) && defined(__MACH__) // Mac OS X - m_interval = ms; + m_interval = ms?ms:0xFFFFFFFF; if (pthread_attr_init(&m_attributes) != 0) throw default_exception("failed to initialize timer thread attributes"); if (pthread_cond_init(&m_condition_var, NULL) != 0) diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index 661d3762b..425a13567 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -90,7 +90,7 @@ public: ~stopwatch() {} void reset() { - m_time = 0ull; + m_time = 0ull; } void start() { @@ -101,11 +101,11 @@ public: } void stop() { - if (m_running) { + if (m_running) { mach_timespec_t _stop; clock_get_time(m_host_clock, &_stop); m_time += (_stop.tv_sec - m_start.tv_sec) * 1000000000ull; - m_time += (_stop.tv_nsec - m_start.tv_nsec); + m_time += (_stop.tv_nsec - m_start.tv_nsec); m_running = false; } } @@ -120,7 +120,7 @@ public: } double get_current_seconds() const { - return get_seconds(); + return get_seconds(); } }; @@ -141,22 +141,23 @@ public: ~stopwatch() {} void reset() { - m_time = 0ull; + m_time = 0ull; } void start() { if (!m_running) { - clock_gettime(CLOCK_THREAD_CPUTIME_ID, &m_start); + clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &m_start); m_running = true; } } void stop() { - if (m_running) { + if (m_running) { struct timespec _stop; - clock_gettime(CLOCK_THREAD_CPUTIME_ID, &_stop); + clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &_stop); m_time += (_stop.tv_sec - m_start.tv_sec) * 1000000000ull; - m_time += (_stop.tv_nsec - m_start.tv_nsec); + if (m_time != 0 || _stop.tv_nsec >= m_start.tv_nsec) + m_time += (_stop.tv_nsec - m_start.tv_nsec); m_running = false; } } @@ -171,7 +172,7 @@ public: } double get_current_seconds() const { - return get_seconds(); + return get_seconds(); } }; diff --git a/src/util/util.h b/src/util/util.h index 0aa8f881d..cbc19b759 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -95,7 +95,10 @@ unsigned uint64_log2(uint64 v); COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); // Return the number of 1 bits in v. -inline unsigned get_num_1bits(unsigned v) { +static inline unsigned get_num_1bits(unsigned v) { +#ifdef __GNUC__ + return __builtin_popcount(v); +#else #ifdef Z3DEBUG unsigned c; unsigned v1 = v; @@ -108,15 +111,16 @@ inline unsigned get_num_1bits(unsigned v) { unsigned r = (((v + (v >> 4)) & 0xF0F0F0F) * 0x1010101) >> 24; SASSERT(c == r); return r; +#endif } // Remark: on gcc, the operators << and >> do not produce zero when the second argument >= 64. // So, I'm using the following two definitions to fix the problem -inline uint64 shift_right(uint64 x, uint64 y) { +static inline uint64 shift_right(uint64 x, uint64 y) { return y < 64ull ? (x >> y) : 0ull; } -inline uint64 shift_left(uint64 x, uint64 y) { +static inline uint64 shift_left(uint64 x, uint64 y) { return y < 64ull ? (x << y) : 0ull; } @@ -255,10 +259,6 @@ inline std::ostream & operator<<(std::ostream & out, std::pair const & p return out; } -#ifndef _WINDOWS -#define __forceinline inline -#endif - template bool has_duplicates(const IT & begin, const IT & end) { for (IT it1 = begin; it1 != end; ++it1) {