diff --git a/examples/interp/iz3.cpp b/examples/interp/iz3.cpp new file mode 100755 index 000000000..99a538549 --- /dev/null +++ b/examples/interp/iz3.cpp @@ -0,0 +1,446 @@ +#include +#include +#include +#include +#include +#include "z3.h" + + + +int usage(const char **argv){ + std::cerr << "usage: " << argv[0] << " [options] file.smt" << std::endl; + std::cerr << std::endl; + std::cerr << "options:" << std::endl; + std::cerr << " -t,--tree tree interpolation" << std::endl; + std::cerr << " -c,--check check result" << std::endl; + std::cerr << " -p,--profile profile execution" << std::endl; + std::cerr << " -w,--weak weak interpolants" << std::endl; + std::cerr << " -f,--flat ouput flat formulas" << std::endl; + std::cerr << " -o ouput to SMT-LIB file" << std::endl; + std::cerr << " -a,--anon anonymize" << std::endl; + std::cerr << " -s,--simple simple proof mode" << std::endl; + std::cerr << std::endl; + return 1; +} + +int main(int argc, const char **argv) { + + bool tree_mode = false; + bool check_mode = false; + bool profile_mode = false; + bool incremental_mode = false; + std::string output_file; + bool flat_mode = false; + bool anonymize = false; + + Z3_config cfg = Z3_mk_config(); + // Z3_interpolation_options options = Z3_mk_interpolation_options(); + Z3_params options = 0; + + /* Parse the command line */ + int argn = 1; + while(argn < argc-1){ + std::string flag = argv[argn]; + if(flag[0] == '-'){ + if(flag == "-t" || flag == "--tree") + tree_mode = true; + else if(flag == "-c" || flag == "--check") + check_mode = true; + else if(flag == "-p" || flag == "--profile") + profile_mode = true; +#if 0 + else if(flag == "-w" || flag == "--weak") + Z3_set_interpolation_option(options,"weak","1"); + else if(flag == "--secondary") + Z3_set_interpolation_option(options,"secondary","1"); +#endif + else if(flag == "-i" || flag == "--incremental") + incremental_mode = true; + else if(flag == "-o"){ + argn++; + if(argn >= argc) return usage(argv); + output_file = argv[argn]; + } + else if(flag == "-f" || flag == "--flat") + flat_mode = true; + else if(flag == "-a" || flag == "--anon") + anonymize = true; + else if(flag == "-s" || flag == "--simple") + Z3_set_param_value(cfg,"PREPROCESS","false"); + else + return usage(argv); + } + argn++; + } + if(argn != argc-1) + return usage(argv); + const char *filename = argv[argn]; + + + /* Create a Z3 context to contain formulas */ + Z3_context ctx = Z3_mk_interpolation_context(cfg); + + if(!flat_mode) + Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB_COMPLIANT); + + /* Read an interpolation problem */ + + int num; + Z3_ast *constraints; + int *parents = 0; + const char *error; + bool ok; + int num_theory; + Z3_ast *theory; + + ok = Z3_read_interpolation_problem(ctx, &num, &constraints, tree_mode ? &parents : 0, filename, &error, &num_theory, &theory); + + /* If parse failed, print the error message */ + + if(!ok){ + std::cerr << error << "\n"; + return 1; + } + + /* if we get only one formula, and it is a conjunction, split it into conjuncts. */ + if(!tree_mode && num == 1){ + Z3_app app = Z3_to_app(ctx,constraints[0]); + Z3_func_decl func = Z3_get_app_decl(ctx,app); + Z3_decl_kind dk = Z3_get_decl_kind(ctx,func); + if(dk == Z3_OP_AND){ + int nconjs = Z3_get_app_num_args(ctx,app); + if(nconjs > 1){ + std::cout << "Splitting formula into " << nconjs << " conjuncts...\n"; + num = nconjs; + constraints = new Z3_ast[num]; + for(int k = 0; k < num; k++) + constraints[k] = Z3_get_app_arg(ctx,app,k); + } + } + } + +#if 0 + /* Write out anonymized version. */ + + if(anonymize){ + Z3_anonymize_ast_vector(ctx,num,constraints); + std::string ofn = output_file.empty() ? "anon.smt" : output_file; + Z3_write_interpolation_problem(ctx, num, constraints, parents, ofn.c_str()); + std::cout << "anonymized problem written to " << ofn << "\n"; + exit(0); + } +#endif + + /* Compute an interpolant, or get a model. */ + + Z3_ast *interpolants = (Z3_ast *)malloc((num-1) * sizeof(Z3_ast)); + Z3_model model = 0; + Z3_lbool result; + + 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); + } + else { + + /* This is a somewhat useless demonstration of incremental mode. + Here, we assert the constraints in the context, then pass them to + iZ3 in an array, so iZ3 knows the sequence. Note it's safe to pass + "true", even though we haven't techically asserted if. */ + + Z3_push(ctx); + std::vector asserted(num); + + /* We start with nothing asserted. */ + for(int i = 0; i < num; i++) + asserted[i] = Z3_mk_true(ctx); + + /* Now we assert the constrints one at a time until UNSAT. */ + + 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); + if(result == Z3_L_FALSE){ + for(unsigned j = 0; j < num-1; j++) + /* Since we want the interpolant formulas to survive a "pop", we + "persist" them here. */ + Z3_persist_ast(ctx,interpolants[j],1); + break; + } + } + Z3_pop(ctx,1); + } + + switch (result) { + + /* If UNSAT, print the interpolants */ + case Z3_L_FALSE: + printf("unsat\n"); + if(output_file.empty()){ + printf("interpolant:\n"); + for(int i = 0; i < num-1; i++) + printf("%s\n", Z3_ast_to_string(ctx, interpolants[i])); + } + else { +#if 0 + Z3_write_interpolation_problem(ctx,num-1,interpolants,0,output_file.c_str()); + printf("interpolant written to %s\n",output_file.c_str()); +#endif + } +#if 0 + if(check_mode){ + std::cout << "Checking interpolant...\n"; + bool chk; + chk = Z3_check_interpolant(ctx,num,constraints,parents,interpolants,&error,num_theory,theory); + if(chk) + std::cout << "Interpolant is correct\n"; + else { + std::cout << "Interpolant is incorrect\n"; + std::cout << error; + return 1; + } + } +#endif + break; + case Z3_L_UNDEF: + printf("fail\n"); + break; + case Z3_L_TRUE: + printf("sat\n"); + printf("model:\n%s\n", Z3_model_to_string(ctx, model)); + break; + } + + std::cout << Z3_interpolation_profile(ctx); + + /* Delete the model if there is one */ + + if (model) + Z3_del_model(ctx, model); + + /* Delete logical context. */ + + Z3_del_context(ctx); + free(interpolants); + + return 0; +} + + +#if 0 + + + +int test(){ + int i; + + /* Create a Z3 context to contain formulas */ + + Z3_config cfg = Z3_mk_config(); + Z3_context ctx = iz3_mk_context(cfg); + + int num = 2; + + Z3_ast *constraints = (Z3_ast *)malloc(num * sizeof(Z3_ast)); + +#if 1 + Z3_sort arr = Z3_mk_array_sort(ctx,Z3_mk_int_sort(ctx),Z3_mk_bool_sort(ctx)); + Z3_symbol as = Z3_mk_string_symbol(ctx, "a"); + Z3_symbol bs = Z3_mk_string_symbol(ctx, "b"); + Z3_symbol xs = Z3_mk_string_symbol(ctx, "x"); + + Z3_ast a = Z3_mk_const(ctx,as,arr); + Z3_ast b = Z3_mk_const(ctx,bs,arr); + Z3_ast x = Z3_mk_const(ctx,xs,Z3_mk_int_sort(ctx)); + + Z3_ast c1 = Z3_mk_eq(ctx,a,Z3_mk_store(ctx,b,x,Z3_mk_true(ctx))); + Z3_ast c2 = Z3_mk_not(ctx,Z3_mk_select(ctx,a,x)); +#else + Z3_symbol xs = Z3_mk_string_symbol(ctx, "x"); + Z3_ast x = Z3_mk_const(ctx,xs,Z3_mk_bool_sort(ctx)); + Z3_ast c1 = Z3_mk_eq(ctx,x,Z3_mk_true(ctx)); + Z3_ast c2 = Z3_mk_eq(ctx,x,Z3_mk_false(ctx)); + +#endif + + constraints[0] = c1; + constraints[1] = c2; + + /* print out the result for grins. */ + + // Z3_string smtout = Z3_benchmark_to_smtlib_string (ctx, "foo", "QFLIA", "sat", "", num, constraints, Z3_mk_true(ctx)); + + // Z3_string smtout = Z3_ast_to_string(ctx,constraints[0]); + // Z3_string smtout = Z3_context_to_string(ctx); + // puts(smtout); + + iz3_print(ctx,num,constraints,"iZ3temp.smt"); + + /* Make room for interpolants. */ + + Z3_ast *interpolants = (Z3_ast *)malloc((num-1) * sizeof(Z3_ast)); + + /* Make room for the model. */ + + Z3_model model = 0; + + /* Call the prover */ + + Z3_lbool result = iz3_interpolate(ctx, num, constraints, interpolants, &model); + + switch (result) { + + /* If UNSAT, print the interpolants */ + case Z3_L_FALSE: + printf("unsat, interpolants:\n"); + for(i = 0; i < num-1; i++) + printf("%s\n", Z3_ast_to_string(ctx, interpolants[i])); + break; + case Z3_L_UNDEF: + printf("fail\n"); + break; + case Z3_L_TRUE: + printf("sat\n"); + printf("model:\n%s\n", Z3_model_to_string(ctx, model)); + break; + } + + /* Delete the model if there is one */ + + if (model) + Z3_del_model(ctx, model); + + /* Delete logical context (note, we call iz3_del_context, not + Z3_del_context */ + + iz3_del_context(ctx); + + return 1; +} + +struct z3_error { + Z3_error_code c; + z3_error(Z3_error_code _c) : c(_c) {} +}; + +extern "C" { + static void throw_z3_error(Z3_error_code c){ + throw z3_error(c); + } +} + +int main(int argc, const char **argv) { + + /* Create a Z3 context to contain formulas */ + + Z3_config cfg = Z3_mk_config(); + Z3_context ctx = iz3_mk_context(cfg); + Z3_set_error_handler(ctx, throw_z3_error); + + /* Make some constraints, by parsing an smtlib formatted file given as arg 1 */ + + try { + Z3_parse_smtlib_file(ctx, argv[1], 0, 0, 0, 0, 0, 0); + } + catch(const z3_error &err){ + std::cerr << "Z3 error: " << Z3_get_error_msg(err.c) << "\n"; + std::cerr << Z3_get_smtlib_error(ctx) << "\n"; + return(1); + } + + /* Get the constraints from the parser. */ + + int num = Z3_get_smtlib_num_formulas(ctx); + + if(num == 0){ + std::cerr << "iZ3 error: File contains no formulas.\n"; + return 1; + } + + + Z3_ast *constraints = (Z3_ast *)malloc(num * sizeof(Z3_ast)); + + int i; + for (i = 0; i < num; i++) + constraints[i] = Z3_get_smtlib_formula(ctx, i); + + /* if we get only one formula, and it is a conjunction, split it into conjuncts. */ + if(num == 1){ + Z3_app app = Z3_to_app(ctx,constraints[0]); + Z3_func_decl func = Z3_get_app_decl(ctx,app); + Z3_decl_kind dk = Z3_get_decl_kind(ctx,func); + if(dk == Z3_OP_AND){ + int nconjs = Z3_get_app_num_args(ctx,app); + if(nconjs > 1){ + std::cout << "Splitting formula into " << nconjs << " conjuncts...\n"; + num = nconjs; + constraints = new Z3_ast[num]; + for(int k = 0; k < num; k++) + constraints[k] = Z3_get_app_arg(ctx,app,k); + } + } + } + + + /* print out the result for grins. */ + + // Z3_string smtout = Z3_benchmark_to_smtlib_string (ctx, "foo", "QFLIA", "sat", "", num, constraints, Z3_mk_true(ctx)); + + // Z3_string smtout = Z3_ast_to_string(ctx,constraints[0]); + // Z3_string smtout = Z3_context_to_string(ctx); + // puts(smtout); + + // iz3_print(ctx,num,constraints,"iZ3temp.smt"); + + /* Make room for interpolants. */ + + Z3_ast *interpolants = (Z3_ast *)malloc((num-1) * sizeof(Z3_ast)); + + /* Make room for the model. */ + + Z3_model model = 0; + + /* Call the prover */ + + Z3_lbool result = iz3_interpolate(ctx, num, constraints, interpolants, &model); + + switch (result) { + + /* If UNSAT, print the interpolants */ + case Z3_L_FALSE: + printf("unsat, interpolants:\n"); + for(i = 0; i < num-1; i++) + printf("%s\n", Z3_ast_to_string(ctx, interpolants[i])); + std::cout << "Checking interpolants...\n"; + const char *error; + if(iZ3_check_interpolant(ctx, num, constraints, 0, interpolants, &error)) + std::cout << "Interpolant is correct\n"; + else { + std::cout << "Interpolant is incorrect\n"; + std::cout << error << "\n"; + } + break; + case Z3_L_UNDEF: + printf("fail\n"); + break; + case Z3_L_TRUE: + printf("sat\n"); + printf("model:\n%s\n", Z3_model_to_string(ctx, model)); + break; + } + + /* Delete the model if there is one */ + + if (model) + Z3_del_model(ctx, model); + + /* Delete logical context (note, we call iz3_del_context, not + Z3_del_context */ + + iz3_del_context(ctx); + + return 0; +} + +#endif diff --git a/scripts/mk_project.py b/scripts/mk_project.py index e4c788cea..f5156ede6 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -53,13 +53,16 @@ def init_project_def(): add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa') add_lib('smt_tactic', ['smt'], 'smt/tactic') add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls') - # TODO: split muz_qe into muz, qe. Perhaps, we should also consider breaking muz into muz and pdr. + # TODO: split muz_qe inbto muz, qe. Perhaps, we should also consider breaking muz into muz and pdr. add_lib('muz_qe', ['smt', 'sat', 'smt2parser']) add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'muz_qe'], 'tactic/smtlogics') add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'muz_qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') add_lib('smtparser', ['portfolio'], 'parsers/smt') - add_lib('interp', ['solver']) + add_dll('foci2', ['util'], 'interp/foci2stub', + 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'] add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure', 'interp'], includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files) @@ -76,6 +79,7 @@ def init_project_def(): set_z3py_dir('api/python') # Examples add_cpp_example('cpp_example', 'c++') + add_cpp_example('iz3', 'interp') add_c_example('c_example', 'c') add_c_example('maxsat') add_dotnet_example('dotnet_example', 'dotnet') diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 09aada950..b0c7f7f58 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -29,6 +29,7 @@ CXX=getenv("CXX", None) CC=getenv("CC", None) CPPFLAGS=getenv("CPPFLAGS", "") CXXFLAGS=getenv("CXXFLAGS", "") +EXAMP_DEBUG_FLAG='' LDFLAGS=getenv("LDFLAGS", "") JNI_HOME=getenv("JNI_HOME", None) @@ -665,6 +666,10 @@ class Component: self.src_dir = os.path.join(SRC_DIR, path) self.to_src_dir = os.path.join(REV_BUILD_DIR, self.src_dir) + def get_link_name(self): + return os.path.join(self.build_dir, self.name) + '$(LIB_EXT)' + + # Find fname in the include paths for the given component. # ownerfile is only used for creating error messages. # That is, we were looking for fname when processing ownerfile @@ -880,7 +885,7 @@ class ExeComponent(Component): out.write(obj) for dep in deps: c_dep = get_component(dep) - out.write(' %s$(LIB_EXT)' % os.path.join(c_dep.build_dir, c_dep.name)) + out.write(' ' + c_dep.get_link_name()) out.write('\n') out.write('\t$(LINK) $(LINK_OUT_FLAG)%s $(LINK_FLAGS)' % exefile) for obj in objs: @@ -888,7 +893,7 @@ class ExeComponent(Component): out.write(obj) for dep in deps: c_dep = get_component(dep) - out.write(' %s$(LIB_EXT)' % os.path.join(c_dep.build_dir, c_dep.name)) + out.write(' ' + c_dep.get_link_name()) out.write(' $(LINK_EXTRA_FLAGS)\n') out.write('%s: %s\n\n' % (self.name, exefile)) @@ -954,6 +959,12 @@ class DLLComponent(Component): self.install = install self.static = static + def get_link_name(self): + if self.static: + return os.path.join(self.build_dir, self.name) + '$(LIB_EXT)' + else: + return self.name + '$(SO_EXT)' + def mk_makefile(self, out): Component.mk_makefile(self, out) # generate rule for (SO_EXT) @@ -976,7 +987,7 @@ class DLLComponent(Component): for dep in deps: if not dep in self.reexports: c_dep = get_component(dep) - out.write(' %s$(LIB_EXT)' % os.path.join(c_dep.build_dir, c_dep.name)) + out.write(' ' + c_dep.get_link_name()) out.write('\n') out.write('\t$(LINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS)' % dllfile) for obj in objs: @@ -985,7 +996,7 @@ class DLLComponent(Component): for dep in deps: if not dep in self.reexports: c_dep = get_component(dep) - out.write(' %s$(LIB_EXT)' % os.path.join(c_dep.build_dir, c_dep.name)) + out.write(' ' + c_dep.get_link_name()) out.write(' $(SLINK_EXTRA_FLAGS)') if IS_WINDOWS: out.write(' /DEF:%s.def' % os.path.join(self.to_src_dir, self.name)) @@ -1228,7 +1239,7 @@ class CppExampleComponent(ExampleComponent): out.write(' ') out.write(os.path.join(self.to_ex_dir, cppfile)) out.write('\n') - out.write('\t%s $(LINK_OUT_FLAG)%s $(LINK_FLAGS)' % (self.compiler(), exefile)) + out.write('\t%s $(EXAMP_DEBUG_FLAG) $(LINK_OUT_FLAG)%s $(LINK_FLAGS)' % (self.compiler(), exefile)) # Add include dir components out.write(' -I%s' % get_component(API_COMPONENT).to_src_dir) out.write(' -I%s' % get_component(CPP_COMPONENT).to_src_dir) @@ -1476,6 +1487,7 @@ def mk_config(): CXXFLAGS = '%s -D_NO_OMP_' % CXXFLAGS if DEBUG_MODE: CXXFLAGS = '%s -g -Wall' % CXXFLAGS + EXAMP_DEBUG_FLAG = '-g' else: if GPROF: CXXFLAGS = '%s -O3 -D _EXTERNAL_RELEASE' % CXXFLAGS @@ -1519,6 +1531,7 @@ def mk_config(): config.write('CC=%s\n' % CC) config.write('CXX=%s\n' % CXX) config.write('CXXFLAGS=%s %s\n' % (CPPFLAGS, CXXFLAGS)) + config.write('EXAMP_DEBUG_FLAG=%s\n' % EXAMP_DEBUG_FLAG) config.write('CXX_OUT_FLAG=-o \n') config.write('OBJ_EXT=.o\n') config.write('LIB_EXT=.a\n') diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index d32bf8b4e..246d5cd8c 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -33,6 +33,11 @@ Revision History: #include"smt_implied_equalities.h" #include"iz3interp.h" #include"iz3profiling.h" +#include"iz3hash.h" + +#ifndef WIN32 +using namespace stl_ext; +#endif typedef interpolation_options_struct *Z3_interpolation_options; @@ -40,7 +45,7 @@ extern "C" { Z3_context Z3_mk_interpolation_context(Z3_config cfg){ if(!cfg) cfg = Z3_mk_config(); - Z3_set_param_value(cfg, "PROOF_MODE", "2"); + 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"); @@ -69,7 +74,7 @@ extern "C" { pre_cnsts_vec[i] = a; } - vector pre_parents_vec; // get parents in a vector + ::vector pre_parents_vec; // get parents in a vector if(parents){ pre_parents_vec.resize(num); for(int i = 0; i < num; i++) @@ -109,7 +114,7 @@ extern "C" { Z3_ast *interps, Z3_model *model, Z3_literals *labels, - bool incremental, + int incremental, int num_theory, Z3_ast *theory ){ @@ -198,4 +203,242 @@ extern "C" { opts->map[name] = value; } + + }; + + +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)); + } +} + +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]; + int eqpos = tok.find('='); + if(eqpos >= 0 && eqpos < (int)tok.size()){ + std::string left = tok.substr(0,eqpos); + std::string right = tok.substr(eqpos+1,tok.size()-eqpos-1); + params[left] = right; + } + } + } + f.close(); + } +} + +extern "C" { + + 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; + } + 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); + } + + 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, std::vector &assertions){ + read_error.clear(); + try { + std::string foo(filename); + if(!foo.empty() && foo[foo.size()-1] == '2'){ + 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; + } + + + 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); + + int num_theory = 0; + if(file_params.find("THEORY") != file_params.end()) + num_theory = atoi(file_params["THEORY"].c_str()); + + std::vector assertions; + if(!iZ3_parse(ctx,filename,error,assertions)) + return false; + + if(num_theory > (int)assertions.size()) + num_theory = assertions.size(); + int num = assertions.size() - num_theory; + + read_cnsts.resize(num); + read_parents.resize(num); + read_theory.resize(num_theory); + + for(int j = 0; j < num_theory; j++) + read_theory[j] = assertions[j]; + for(int 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(int j = 0; j < num; j++) + read_parents[j] = SHRT_MAX; + + hash_map pred_map; + + for(int 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(int 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/z3_api.h b/src/api/z3_api.h index 975b45940..76c34121f 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -7750,8 +7750,6 @@ END_MLAPI_EXCLUDE are considered to have global scope (i.e., may appear in any interpolant formula). - def_API('Z3_interpolate', INT, (_in(CONTEXT), _in(INT), _in_array(1,AST), _in_array(1,UINT), _in(PARAMS), _out_array(1,AST), _out(MODEL), _out(LITERALS), _in(BOOL), _in(INT), _in_array(9,AST),)) - */ @@ -7762,11 +7760,11 @@ END_MLAPI_EXCLUDE __in_ecount(num) unsigned *parents, __in Z3_params options, __out_ecount(num-1) Z3_ast *interps, - __out Z3_model *model = 0, - __out Z3_literals *labels = 0, - __in bool incremental = false, - __in int num_theory = 0, - __in_ecount(num_theory) Z3_ast *theory = 0); + __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 @@ -7779,6 +7777,49 @@ END_MLAPI_EXCLUDE Z3_string Z3_API Z3_interpolation_profile(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); + #endif diff --git a/src/interp/foci2stub/foci2.cpp b/src/interp/foci2stub/foci2.cpp new file mode 100644 index 000000000..31908855b --- /dev/null +++ b/src/interp/foci2stub/foci2.cpp @@ -0,0 +1,25 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + foci2.cpp + +Abstract: + + Fake foci2, to be replaced + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ + + +#include "foci2.h" + +FOCI2_EXPORT foci2 *foci2::create(const std::string &){ + return 0; +} diff --git a/src/interp/foci2.h b/src/interp/foci2stub/foci2.h similarity index 100% rename from src/interp/foci2.h rename to src/interp/foci2stub/foci2.h diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index 15bdf0c22..0289c90c7 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -233,7 +233,7 @@ void iz3interpolate(scoped_ptr &_m_manager, const ptr_vector &cnsts, const ::vector &parents, ptr_vector &interps, - const ptr_vector theory, + const ptr_vector &theory, interpolation_options_struct * options) { std::vector _cnsts(cnsts.size()); diff --git a/src/interp/iz3interp.h b/src/interp/iz3interp.h index 4e76b74fd..65ba1f15a 100644 --- a/src/interp/iz3interp.h +++ b/src/interp/iz3interp.h @@ -34,7 +34,7 @@ void iz3interpolate(scoped_ptr &_m_manager, const ptr_vector &cnsts, const ::vector &parents, ptr_vector &interps, - const ptr_vector theory, + const ptr_vector &theory, interpolation_options_struct * options = 0); #endif diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index f44c68dc2..93f541430 100644 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -44,7 +44,54 @@ iz3mgr::ast iz3mgr::make_var(const std::string &name, type ty){ } iz3mgr::ast iz3mgr::make(opr op, int n, raw_ast **args){ - return m().mk_app(m().get_basic_family_id(), op, 0, 0, n, (expr **)args); + switch(op) { + case True: return mki(m_basic_fid,OP_TRUE,n,args); + case False: return mki(m_basic_fid,OP_FALSE,n,args); + case Equal: return mki(m_basic_fid,OP_EQ,n,args); + case Distinct: return mki(m_basic_fid,OP_DISTINCT,n,args); + case Ite: return mki(m_basic_fid,OP_ITE,n,args); + case And: return mki(m_basic_fid,OP_AND,n,args); + case Or: return mki(m_basic_fid,OP_OR,n,args); + case Iff: return mki(m_basic_fid,OP_IFF,n,args); + case Xor: return mki(m_basic_fid,OP_XOR,n,args); + case Not: return mki(m_basic_fid,OP_NOT,n,args); + case Implies: return mki(m_basic_fid,OP_IMPLIES,n,args); + case Oeq: return mki(m_basic_fid,OP_OEQ,n,args); + case Leq: return mki(m_arith_fid,OP_LE,n,args); + case Geq: return mki(m_arith_fid,OP_GE,n,args); + case Lt: return mki(m_arith_fid,OP_LT,n,args); + case Gt: return mki(m_arith_fid,OP_GT,n,args); + case Plus: return mki(m_arith_fid,OP_ADD,n,args); + case Sub: return mki(m_arith_fid,OP_SUB,n,args); + case Uminus: return mki(m_arith_fid,OP_UMINUS,n,args); + case Times: return mki(m_arith_fid,OP_MUL,n,args); + case Div: return mki(m_arith_fid,OP_DIV,n,args); + case Idiv: return mki(m_arith_fid,OP_IDIV,n,args); + case Rem: return mki(m_arith_fid,OP_REM,n,args); + case Mod: return mki(m_arith_fid,OP_MOD,n,args); + case Power: return mki(m_arith_fid,OP_POWER,n,args); + case ToReal: return mki(m_arith_fid,OP_TO_REAL,n,args); + case ToInt: return mki(m_arith_fid,OP_TO_INT,n,args); + case IsInt: return mki(m_arith_fid,OP_IS_INT,n,args); + case Store: return mki(m_array_fid,OP_STORE,n,args); + case Select: return mki(m_array_fid,OP_SELECT,n,args); + case ConstArray: return mki(m_array_fid,OP_CONST_ARRAY,n,args); + case ArrayDefault: return mki(m_array_fid,OP_ARRAY_DEFAULT,n,args); + case ArrayMap: return mki(m_array_fid,OP_ARRAY_MAP,n,args); + case SetUnion: return mki(m_array_fid,OP_SET_UNION,n,args); + case SetIntersect: return mki(m_array_fid,OP_SET_INTERSECT,n,args); + case SetDifference: return mki(m_array_fid,OP_SET_DIFFERENCE,n,args); + case SetComplement: return mki(m_array_fid,OP_SET_COMPLEMENT,n,args); + case SetSubSet: return mki(m_array_fid,OP_SET_SUBSET,n,args); + case AsArray: return mki(m_array_fid,OP_AS_ARRAY,n,args); + default: + assert(0); + return ast(); + } +} + +iz3mgr::ast iz3mgr::mki(family_id fid, decl_kind dk, int n, raw_ast **args){ + return m().mk_app(fid, dk, 0, 0, n, (expr **)args); } iz3mgr::ast iz3mgr::make(opr op, const std::vector &args){ diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index efcbb0d6f..c96a20c7b 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -420,8 +420,8 @@ class iz3mgr { scoped_ptr m_manager; private: + ast mki(family_id fid, decl_kind sk, int n, raw_ast **args); ast make(opr op, int n, raw_ast **args); - ast make(symb sym, int n, raw_ast **args); family_id m_basic_fid; diff --git a/src/interp/iz3profiling.cpp b/src/interp/iz3profiling.cpp new file mode 100755 index 000000000..f18866f30 --- /dev/null +++ b/src/interp/iz3profiling.cpp @@ -0,0 +1,138 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3profiling.h + +Abstract: + + Some routines for measuring performance. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ + +#include "iz3profiling.h" + +#include +#include +#include +#include +#include + + +// FIXME fill in these stubs + +#define clock_t int + +static clock_t current_time(){ + return 0; +} + +static void output_time(std::ostream &os, clock_t time){ + os << ((double)time)/1000; +} + + +namespace profiling { + + void show_time(){ + output_time(std::cout,current_time()); + std::cout << "\n"; + } + + typedef std::map nmap; + + struct node { + std::string name; + clock_t time; + clock_t start_time; + nmap sub; + struct node *parent; + + node(); + } top; + + node::node(){ + time = 0; + parent = 0; + } + + struct node *current; + + struct init { + init(){ + top.name = "TOTAL"; + current = ⊤ + } + } initializer; + + struct time_entry { + clock_t t; + time_entry(){t = 0;}; + void add(clock_t incr){t += incr;} + }; + + struct ltstr + { + bool operator()(const char* s1, const char* s2) const + { + return strcmp(s1, s2) < 0; + } + }; + + typedef std::map tmap; + + static std::ostream *pfs; + + void print_node(node &top, int indent, tmap &totals){ + for(int i = 0; i < indent; i++) (*pfs) << " "; + (*pfs) << top.name; + int dots = 70 - 2 * indent - top.name.size(); + for(int i = 0; i second,indent+1,totals); + } + + void print(std::ostream &os) { + pfs = &os; + top.time = 0; + for(nmap::iterator it = top.sub.begin(); it != top.sub.end(); it++) + top.time += it->second.time; + tmap totals; + print_node(top,0,totals); + (*pfs) << "TOTALS:" << std::endl; + for(tmap::iterator it = totals.begin(); it != totals.end(); it++){ + (*pfs) << (it->first) << " "; + output_time(*pfs, it->second.t); + (*pfs) << std::endl; + } + } + + void timer_start(const char *name){ + node &child = current->sub[name]; + if(child.name.empty()){ // a new node + child.parent = current; + child.name = name; + } + child.start_time = current_time(); + current = &child; + } + + void timer_stop(const char *name){ + if(current->name != name || !current->parent){ + std::cerr << "imbalanced timer_start and timer_stop"; + exit(1); + } + current->time += (current_time() - current->start_time); + current = current->parent; + } +}