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/update_api.py b/scripts/update_api.py index 97dacb44b..791c23ddd 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -123,6 +123,7 @@ SYMBOL = 9 PRINT_MODE = 10 ERROR_CODE = 11 DOUBLE = 12 +UINT_PTR = 13 FIRST_OBJ_ID = 100 @@ -131,28 +132,28 @@ 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', UINT_PTR : 'unsigned*' } 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', UINT_PTR : 'ctypes.POINTER(ctypes.c_uint)' } # Mapping to .NET types Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', INT64 : 'Int64', UINT64 : 'UInt64', DOUBLE : 'double', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'int', SYMBOL : 'IntPtr', - PRINT_MODE : 'uint', ERROR_CODE : 'uint' } + PRINT_MODE : 'uint', ERROR_CODE : 'uint', UINT_PTR : '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', UINT_PTR : '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', UINT_PTR : 'jlong'} next_type_id = FIRST_OBJ_ID @@ -259,7 +260,7 @@ def param2dotnet(p): if k == INOUT_ARRAY: return "[In, Out] %s[]" % type2dotnet(param_type(p)) if k == OUT_ARRAY: - return "[Out] %s[]" % type2dotnet(param_type(p)) + return "[Out] out %s[]" % type2dotnet(param_type(p)) else: return type2dotnet(param_type(p)) @@ -466,6 +467,8 @@ def mk_dotnet_wrappers(): dotnet.write('out '); else: dotnet.write('ref ') + elif param_kind(param) == OUT_ARRAY: + dotnet.write('out '); dotnet.write('a%d' % i) i = i + 1 dotnet.write(');\n'); @@ -953,20 +956,33 @@ 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) + tstr = tstr + '*' + 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) + elif ty == UINT_PTR: + 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)) else: 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_interp.cpp b/src/api/api_interp.cpp index e06ad5192..8740e99a5 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,669 @@ 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]); - } - } - } + Z3_lbool Z3_interpolate(Z3_context ctx, + unsigned num, + Z3_ast *cnsts, + unsigned *parents, + Z3_params options, + Z3_ast *interps, + Z3_model *model, + Z3_literals *labels, + unsigned incremental, + unsigned num_theory, + Z3_ast *theory + ){ - 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 - ){ - - profiling::timer_start("Solve"); + profiling::timer_start("Solve"); - if(!incremental){ + if (!incremental){ - profiling::timer_start("Z3 assert"); + profiling::timer_start("Z3 assert"); - 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 + Z3_push(ctx); // so we can rewind later - if(theory){ - for(int i = 0; i < num_theory; i++) - Z3_assert_cnstr(ctx,theory[i]); - } + for (int i = 0; i < num; i++) + Z3_assert_cnstr(ctx, cnsts[i]); // assert all the constraints - profiling::timer_stop("Z3 assert"); + if (theory){ + for (int i = 0; i < num_theory; i++) + Z3_assert_cnstr(ctx, theory[i]); + } + + profiling::timer_stop("Z3 assert"); + } + + + // 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); + + 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; + } + + 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, + unsigned num, + Z3_ast *cnsts, + unsigned *parents, + Z3_ast *itp, + Z3_string *error, + unsigned 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; + } + + ::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; } - // 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 != std::string::npos){ - 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){ + 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; + } + 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); + } + 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, const char **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; - - } } diff --git a/src/api/dotnet/Constructor.cs b/src/api/dotnet/Constructor.cs index 527b8bc13..8d478dd85 100644 --- a/src/api/dotnet/Constructor.cs +++ b/src/api/dotnet/Constructor.cs @@ -50,7 +50,7 @@ namespace Microsoft.Z3 IntPtr constructor = IntPtr.Zero; IntPtr tester = IntPtr.Zero; IntPtr[] accessors = new IntPtr[n]; - Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors); + Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, out accessors); return new FuncDecl(Context, constructor); } } @@ -66,7 +66,7 @@ namespace Microsoft.Z3 IntPtr constructor = IntPtr.Zero; IntPtr tester = IntPtr.Zero; IntPtr[] accessors = new IntPtr[n]; - Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors); + Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, out accessors); return new FuncDecl(Context, tester); } } @@ -82,7 +82,7 @@ namespace Microsoft.Z3 IntPtr constructor = IntPtr.Zero; IntPtr tester = IntPtr.Zero; IntPtr[] accessors = new IntPtr[n]; - Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors); + Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, out accessors); FuncDecl[] t = new FuncDecl[n]; for (uint i = 0; i < n; i++) t[i] = new FuncDecl(Context, accessors[i]); diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 2b88cbab7..a9e25de4f 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -424,7 +424,7 @@ namespace Microsoft.Z3 n_constr[i] = cla[i].NativeObject; } IntPtr[] n_res = new IntPtr[n]; - Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr); + Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), out n_res, n_constr); DatatypeSort[] res = new DatatypeSort[n]; for (uint i = 0; i < n; i++) res[i] = new DatatypeSort(this, n_res[i]); diff --git a/src/api/dotnet/EnumSort.cs b/src/api/dotnet/EnumSort.cs index e62043078..db3d5123f 100644 --- a/src/api/dotnet/EnumSort.cs +++ b/src/api/dotnet/EnumSort.cs @@ -88,7 +88,7 @@ namespace Microsoft.Z3 IntPtr[] n_constdecls = new IntPtr[n]; IntPtr[] n_testers = new IntPtr[n]; NativeObject = Native.Z3_mk_enumeration_sort(ctx.nCtx, name.NativeObject, (uint)n, - Symbol.ArrayToNative(enumNames), n_constdecls, n_testers); + Symbol.ArrayToNative(enumNames), out n_constdecls, out n_testers); } #endregion }; 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..559a1bfc7 --- /dev/null +++ b/src/api/dotnet/InterpolationContext.cs @@ -0,0 +1,206 @@ +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; + } + + /// + /// 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 Interpolate(Expr[] cnsts, uint[] parents, Params options, bool incremental, Expr[] theory, out Expr[] interps, out Model model) + { + Contract.Requires(cnsts != null); + Contract.Requires(parents != null); + Contract.Requires(cnsts.Length == parents.Length); + Contract.Ensures(Contract.ValueAtReturn(out interps) != null); + Contract.Ensures(Contract.ValueAtReturn(out model) != null); + + CheckContextMatch(cnsts); + CheckContextMatch(theory); + + uint sz = (uint)cnsts.Length; + + IntPtr[] ni = new IntPtr[sz - 1]; + IntPtr nm = IntPtr.Zero; + IntPtr z = IntPtr.Zero; + + int r = Native.Z3_interpolate(nCtx, + sz, Expr.ArrayToNative(cnsts), parents, + options.NativeObject, + out ni, + ref nm, + ref z, // Z3_lterals are deprecated. + (uint)(incremental ? 1 : 0), + (uint)theory.Length, Expr.ArrayToNative(theory)); + + interps = new Expr[sz - 1]; + for (uint i = 0; i < sz - 1; i++) + interps[i] = Expr.Create(this, ni[i]); + + model = new Model(this, nm); + + 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; + uint[][] n_parents; + int r = Native.Z3_read_interpolation_problem(nCtx, ref num, out n_cnsts, out n_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]); + parents[i] = n_parents[0][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, int[] parents, string error, Expr[] theory) + { + Contract.Requires(cnsts.Length == parents.Length); + } + } +} 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/TupleSort.cs b/src/api/dotnet/TupleSort.cs index 1e4af5cd7..7d0b6a853 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; NativeObject = Native.Z3_mk_tuple_sort(ctx.nCtx, name.NativeObject, numFields, Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts), - ref t, new IntPtr[numFields]); + ref t, out f); } #endregion }; diff --git a/src/api/python/z3.py b/src/api/python/z3.py index b6cceeb8e..1a5565ab5 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -7253,19 +7253,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 +7304,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: @@ -7346,7 +7346,7 @@ def binary_interpolant(a,b,p=None,ctx=None): 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 +7375,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/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 b561b6bf1..41ccf532e 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -2116,17 +2116,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, @@ -7700,314 +7690,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..1aac13b6e --- /dev/null +++ b/src/api/z3_interp.h @@ -0,0 +1,359 @@ +/*++ +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); + + + /** 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); + + /** 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_array(1, AST), _out_array(1, UINT_PTR), _in(STRING), _out(STRING), _out(UINT), _out_array(6, AST))) + + */ + + int Z3_API Z3_read_interpolation_problem(__in Z3_context ctx, + __out unsigned *num, + __out_ecount(*num) Z3_ast **cnsts, + __out_ecount(*num) unsigned **parents, + __in Z3_string filename, + __out Z3_string *error, + __out unsigned *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. + + 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 Z3_string *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