diff --git a/examples/interp/iz3.cpp b/examples/interp/iz3.cpp deleted file mode 100755 index 915d3ba54..000000000 --- a/examples/interp/iz3.cpp +++ /dev/null @@ -1,449 +0,0 @@ - -/*++ -Copyright (c) 2015 Microsoft Corporation - ---*/ - -#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; - bool write = false; - - z3::config cfg; - // 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 == "-w" || flag == "--write") - write = 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(cfg, z3::context::interpolation()); - - if(write || anonymize) - Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB2_COMPLIANT); - else if(!flat_mode) - Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB_COMPLIANT); - - /* Read an interpolation problem */ - - unsigned num; - Z3_ast *constraints; - unsigned *parents = 0; - const char *error; - bool ok; - unsigned num_theory; - Z3_ast *theory; - - ok = Z3_read_interpolation_problem(ctx, &num, &constraints, tree_mode ? &parents : 0, filename, &error, &num_theory, &theory) != 0; - - /* 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(unsigned k = 0; k < num; k++) - constraints[k] = Z3_get_app_arg(ctx,app,k); - } - } - } - - /* Write out anonymized version. */ - - if(write || anonymize){ -#if 0 - Z3_anonymize_ast_vector(ctx,num,constraints); -#endif - std::string ofn = output_file.empty() ? "iz3out.smt2" : output_file; - Z3_write_interpolation_problem(ctx, num, constraints, parents, ofn.c_str(), num_theory, theory); - std::cout << "anonymized problem written to " << ofn << "\n"; - exit(0); - } - - /* Compute an interpolant, or get a model. */ - - Z3_ast *interpolants = (Z3_ast *)malloc((num-1) * sizeof(Z3_ast)); - Z3_model z3model = 0; - Z3_lbool result; - - if(!incremental_mode){ - /* In non-incremental mode, we just pass the constraints. */ - result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, constraints, parents, options, interpolants, &z3model, 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::solver s(ctx); - z3::expr_vector asserted(ctx), saved_interpolants(ctx); - - /* We start with nothing asserted. */ - for(unsigned i = 0; i < num; i++) asserted.push_back(ctx.bool_val(true)); - - /* Now we assert the constrints one at a time until UNSAT. */ - - for(unsigned i = 0; i < num; i++){ - asserted[i] = z3::expr(ctx, constraints[i]); - s.add(asserted[i]); - result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, &asserted[0], parents, options, interpolants, &z3model, 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. */ - saved_interpolants.push_back(z3::expr(ctx, interpolants[j])); - break; - } - } - } - - switch (result) { - - /* If UNSAT, print the interpolants */ - case Z3_L_FALSE: - printf("unsat\n"); - if(output_file.empty()){ - printf("interpolant:\n"); - for(unsigned 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 1 - if(check_mode){ - std::cout << "Checking interpolant...\n"; - bool chk; - chk = Z3_check_interpolant(ctx,num,constraints,parents,interpolants,&error,num_theory,theory) != 0; - 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, z3model)); - break; - } - - if(profile_mode) - std::cout << Z3_interpolation_profile(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 2863de628..dfe801bdd 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -94,7 +94,6 @@ def init_project_def(): set_z3py_dir('api/python') # Examples add_cpp_example('cpp_example', 'c++') - add_cpp_example('iz3', 'interp') add_cpp_example('z3_tptp', 'tptp') add_c_example('c_example', 'c') add_c_example('maxsat') diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 0b924c21f..67b60cbaf 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2592,7 +2592,7 @@ def mk_z3consts_py(api_files): if Z3PY_SRC_DIR is None: raise MKException("You must invoke set_z3py_dir(path):") - blank_pat = re.compile("^ *$") + blank_pat = re.compile("^ *\r?$") comment_pat = re.compile("^ *//.*$") typedef_pat = re.compile("typedef enum *") typedef2_pat = re.compile("typedef enum { *") @@ -2653,6 +2653,8 @@ def mk_z3consts_py(api_files): z3consts.write('%s = %s\n' % (k, i)) z3consts.write('\n') mode = SEARCHING + elif len(words) <= 2: + assert False, "Invalid %s, line: %s" % (api_file, linenum) else: if words[2] != '': if len(words[2]) > 1 and words[2][1] == 'x': @@ -2670,7 +2672,7 @@ def mk_z3consts_py(api_files): # Extract enumeration types from z3_api.h, and add .Net definitions def mk_z3consts_dotnet(api_files): - blank_pat = re.compile("^ *$") + blank_pat = re.compile("^ *\r?$") comment_pat = re.compile("^ *//.*$") typedef_pat = re.compile("typedef enum *") typedef2_pat = re.compile("typedef enum { *") @@ -2740,6 +2742,8 @@ def mk_z3consts_dotnet(api_files): z3consts.write(' %s = %s,\n' % (k, i)) z3consts.write(' }\n\n') mode = SEARCHING + elif len(words) <= 2: + assert False, "Invalid %s, line: %s" % (api_file, linenum) else: if words[2] != '': if len(words[2]) > 1 and words[2][1] == 'x': diff --git a/scripts/update_api.py b/scripts/update_api.py index 86f6ceee8..a4a8faab2 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -99,7 +99,7 @@ else: if s != None: enc = sys.stdout.encoding if enc != None: return s.decode(enc) - else: return s + else: return s.decode('ascii') else: return "" diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 8451c00c5..79a2fd965 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -103,9 +103,7 @@ namespace api { m_smtlib_parser = 0; m_smtlib_parser_has_decls = false; - - z3_bound_num_procs(); - + m_error_handler = &default_error_handler; m_basic_fid = m().get_basic_family_id(); diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 25c399d68..d56ba4af1 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2613,8 +2613,13 @@ namespace Microsoft.Z3 /// is an array of patterns, is an array /// with the sorts of the bound variables, is an array with the /// 'names' of the bound variables, and is the body of the - /// quantifier. Quantifiers are associated with weights indicating - /// the importance of using the quantifier during instantiation. + /// quantifier. Quantifiers are associated with weights indicating the importance of + /// using the quantifier during instantiation. + /// Note that the bound variables are de-Bruijn indices created using . + /// Z3 applies the convention that the last element in and + /// refers to the variable with index 0, the second to last element + /// of and refers to the variable + /// with index 1, etc. /// /// the sorts of the bound variables. /// names of the bound variables @@ -2644,6 +2649,11 @@ namespace Microsoft.Z3 /// /// Create a universal Quantifier. /// + /// + /// Creates a universal quantifier using a list of constants that will + /// form the set of bound variables. + /// + /// public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) { Contract.Requires(body != null); @@ -2659,7 +2669,10 @@ namespace Microsoft.Z3 /// /// Create an existential Quantifier. /// - /// + /// + /// Creates an existential quantifier using de-Brujin indexed variables. + /// (). + /// public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) { Contract.Requires(sorts != null); @@ -2678,6 +2691,11 @@ namespace Microsoft.Z3 /// /// Create an existential Quantifier. /// + /// + /// Creates an existential quantifier using a list of constants that will + /// form the set of bound variables. + /// + /// public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) { Contract.Requires(body != null); @@ -2693,6 +2711,7 @@ namespace Microsoft.Z3 /// /// Create a Quantifier. /// + /// public Quantifier MkQuantifier(bool universal, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) { Contract.Requires(body != null); @@ -2716,6 +2735,7 @@ namespace Microsoft.Z3 /// /// Create a Quantifier. /// + /// public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) { Contract.Requires(body != null); diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 0f9a85799..4d8484ced 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -433,8 +433,8 @@ public class Context extends IDisposable /** * Creates a fresh function declaration with a name prefixed with * {@code prefix}. - * @see mkFuncDecl(String,Sort,Sort) - * @see mkFuncDecl(String,Sort[],Sort) + * @see #mkFuncDecl(String,Sort,Sort) + * @see #mkFuncDecl(String,Sort[],Sort) **/ public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range) @@ -1722,9 +1722,9 @@ public class Context extends IDisposable **/ public Expr mkArrayExt(ArrayExpr arg1, ArrayExpr arg2) { - checkContextMatch(arg1); - checkContextMatch(arg2); - return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject())); + checkContextMatch(arg1); + checkContextMatch(arg2); + return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject())); } @@ -2025,6 +2025,7 @@ public class Context extends IDisposable /** * Create a universal Quantifier. + * * @param sorts the sorts of the bound variables. * @param names names of the bound variables * @param body the body of the quantifier. @@ -2034,17 +2035,22 @@ public class Context extends IDisposable * @param quantifierID optional symbol to track quantifier. * @param skolemID optional symbol to track skolem constants. * - * Remarks: Creates a forall formula, where - * {@code weight"/> is the weight, (m_rule); } @@ -830,7 +848,7 @@ namespace pdr { } r0 = get_rule(); app_ref_vector& inst = pt().get_inst(r0); - TRACE("pdr", tout << mk_pp(state(), m) << " instance: " << inst.size() << "\n";); + TRACE("pdr", tout << state() << " instance: " << inst.size() << "\n";); for (unsigned i = 0; i < inst.size(); ++i) { expr* v; if (model.find(inst[i].get(), v)) { @@ -852,7 +870,7 @@ namespace pdr { for (unsigned i = 0; i < indent; ++i) out << " "; out << m_level << " " << m_pt.head()->get_name() << " " << (m_closed?"closed":"open") << "\n"; for (unsigned i = 0; i < indent; ++i) out << " "; - out << " " << mk_pp(m_state, m_state.get_manager(), indent) << "\n"; + out << " " << mk_pp(m_state, m_state.get_manager(), indent) << " " << m_state->get_id() << "\n"; for (unsigned i = 0; i < children().size(); ++i) { children()[i]->display(out, indent + 1); } @@ -925,17 +943,6 @@ namespace pdr { } } - bool model_search::is_repeated(model_node& n) const { - model_node* p = n.parent(); - while (p) { - if (p->state() == n.state()) { - TRACE("pdr", tout << n.state() << "repeated\n";); - return true; - } - p = p->parent(); - } - return false; - } void model_search::add_leaf(model_node& n) { SASSERT(n.children().empty()); @@ -1012,11 +1019,11 @@ namespace pdr { nodes.erase(&n); bool is_goal = n.is_goal(); remove_goal(n); - if (!nodes.empty() && is_goal && backtrack) { + // TBD: siblings would also fail if n is not a goal. + if (!nodes.empty() && backtrack && nodes[0]->children().empty() && nodes[0]->is_closed()) { TRACE("pdr_verbose", for (unsigned i = 0; i < nodes.size(); ++i) n.display(tout << &n << "\n", 2);); model_node* n1 = nodes[0]; - n1->set_open(); - SASSERT(n1->children().empty()); + n1->set_open(); enqueue_leaf(n1); } @@ -1702,7 +1709,15 @@ namespace pdr { void context::validate_search() { expr_ref tr = m_search.get_trace(*this); - // TBD: tr << "\n"; + smt::kernel solver(m, get_fparams()); + solver.assert_expr(tr); + lbool res = solver.check(); + if (res != l_true) { + std::stringstream msg; + msg << "rule validation failed when checking: " << tr; + IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";); + throw default_exception(msg.str()); + } } void context::validate_model() { @@ -1938,11 +1953,11 @@ namespace pdr { proof_ref proof(m); SASSERT(m_last_result == l_true); proof = m_search.get_proof_trace(*this); - TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";); + TRACE("pdr", tout << "PDR trace: " << proof << "\n";); apply(m, m_pc.get(), proof); - TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";); + TRACE("pdr", tout << "PDR trace: " << proof << "\n";); // proof_utils::push_instantiations_up(proof); - // TRACE("pdr", tout << "PDR up: " << mk_pp(proof, m) << "\n";); + // TRACE("pdr", tout << "PDR up: " << proof << "\n";); return proof; } diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h index 35b9067b2..ad4b44d90 100644 --- a/src/muz/pdr/pdr_context.h +++ b/src/muz/pdr/pdr_context.h @@ -268,7 +268,6 @@ namespace pdr { void enqueue_leaf(model_node* n); // add leaf to priority queue. void update_models(); void set_leaf(model_node& n); // Set node as leaf, remove children. - bool is_repeated(model_node& n) const; unsigned num_goals() const; public: diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 1bb521923..cb598617c 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -191,7 +191,7 @@ namespace opt { m_msolver->set_adjust_value(m_adjust_value); is_sat = (*m_msolver)(); if (is_sat != l_false) { - m_msolver->get_model(m_model); + m_msolver->get_model(m_model, m_labels); } } @@ -247,8 +247,9 @@ namespace opt { m_upper = r; } - void maxsmt::get_model(model_ref& mdl) { + void maxsmt::get_model(model_ref& mdl, svector& labels) { mdl = m_model.get(); + labels = m_labels; } void maxsmt::commit_assignment() { diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 8d290a640..7dbf763e2 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -46,7 +46,7 @@ namespace opt { virtual bool get_assignment(unsigned index) const = 0; virtual void set_cancel(bool f) = 0; virtual void collect_statistics(statistics& st) const = 0; - virtual void get_model(model_ref& mdl) = 0; + virtual void get_model(model_ref& mdl, svector& labels) = 0; virtual void updt_params(params_ref& p) = 0; void set_adjust_value(adjust_value& adj) { m_adjust_value = adj; } @@ -67,6 +67,7 @@ namespace opt { rational m_lower; rational m_upper; model_ref m_model; + svector m_labels; svector m_assignment; // truth assignment to soft constraints params_ref m_params; // config @@ -79,9 +80,9 @@ namespace opt { virtual bool get_assignment(unsigned index) const { return m_assignment[index]; } virtual void set_cancel(bool f) { m_cancel = f; if (f) s().cancel(); else s().reset_cancel(); } virtual void collect_statistics(statistics& st) const { } - virtual void get_model(model_ref& mdl) { mdl = m_model.get(); } + virtual void get_model(model_ref& mdl, svector& labels) { mdl = m_model.get(); labels = m_labels;} virtual void commit_assignment(); - void set_model() { s().get_model(m_model); } + void set_model() { s().get_model(m_model); s().get_labels(m_labels); } virtual void updt_params(params_ref& p); solver& s(); void init(); @@ -122,6 +123,7 @@ namespace opt { rational m_upper; adjust_value m_adjust_value; model_ref m_model; + svector m_labels; params_ref m_params; public: maxsmt(maxsat_context& c); @@ -139,7 +141,7 @@ namespace opt { rational get_upper() const; void update_lower(rational const& r); void update_upper(rational const& r); - void get_model(model_ref& mdl); + void get_model(model_ref& mdl, svector& labels); bool get_assignment(unsigned index) const; void display_answer(std::ostream& out) const; void collect_statistics(statistics& st) const; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 1b4b1e7bc..1b33c2cf1 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -167,6 +167,10 @@ namespace opt { m_hard_constraints.reset(); } + void context::get_labels(svector & r) { + r.append(m_labels); + } + void context::set_hard_constraints(ptr_vector& fmls) { if (m_scoped_state.set(fmls)) { clear_state(); @@ -228,6 +232,7 @@ namespace opt { TRACE("opt", tout << "initial search result: " << is_sat << "\n";); if (is_sat != l_false) { s.get_model(m_model); + s.get_labels(m_labels); } if (is_sat != l_true) { return is_sat; @@ -276,11 +281,6 @@ namespace opt { } } - void context::set_model(model_ref& mdl) { - m_model = mdl; - fix_model(mdl); - } - void context::get_model(model_ref& mdl) { mdl = m_model; fix_model(mdl); @@ -289,7 +289,7 @@ namespace opt { lbool context::execute_min_max(unsigned index, bool committed, bool scoped, bool is_max) { if (scoped) get_solver().push(); lbool result = m_optsmt.lex(index, is_max); - if (result == l_true) m_optsmt.get_model(m_model); + if (result == l_true) m_optsmt.get_model(m_model, m_labels); if (scoped) get_solver().pop(1); if (result == l_true && committed) m_optsmt.commit_assignment(index); return result; @@ -300,7 +300,7 @@ namespace opt { maxsmt& ms = *m_maxsmts.find(id); if (scoped) get_solver().push(); lbool result = ms(); - if (result != l_false && (ms.get_model(tmp), tmp.get())) ms.get_model(m_model); + if (result != l_false && (ms.get_model(tmp, m_labels), tmp.get())) ms.get_model(m_model, m_labels); if (scoped) get_solver().pop(1); if (result == l_true && committed) ms.commit_assignment(); return result; @@ -453,7 +453,7 @@ namespace opt { } void context::yield() { - m_pareto->get_model(m_model); + m_pareto->get_model(m_model, m_labels); update_bound(true); update_bound(false); } @@ -1121,16 +1121,20 @@ namespace opt { } void context::display_assignment(std::ostream& out) { + out << "(objectives\n"; for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) { objective const& obj = m_scoped_state.m_objectives[i]; + out << " ("; display_objective(out, obj); if (get_lower_as_num(i) != get_upper_as_num(i)) { - out << " |-> [" << get_lower(i) << ":" << get_upper(i) << "]\n"; + out << " (" << get_lower(i) << " " << get_upper(i) << ")"; } else { - out << " |-> " << get_lower(i) << "\n"; + out << " " << get_lower(i); } + out << ")\n"; } + out << ")\n"; } void context::display_objective(std::ostream& out, objective const& obj) const { diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 735dc6905..dc180e8e6 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -162,6 +162,7 @@ namespace opt { bool m_pp_neat; symbol m_maxsat_engine; symbol m_logic; + svector m_labels; public: context(ast_manager& m); virtual ~context(); @@ -180,11 +181,10 @@ namespace opt { virtual lbool optimize(); virtual bool print_model() const; virtual void get_model(model_ref& _m); - virtual void set_model(model_ref& _m); virtual void fix_model(model_ref& _m); virtual void collect_statistics(statistics& stats) const; virtual proof* get_proof() { return 0; } - virtual void get_labels(svector & r) {} + virtual void get_labels(svector & r); virtual void get_unsat_core(ptr_vector & r) {} virtual std::string reason_unknown() const; diff --git a/src/opt/opt_pareto.cpp b/src/opt/opt_pareto.cpp index 5e1d4b269..dea744a72 100644 --- a/src/opt/opt_pareto.cpp +++ b/src/opt/opt_pareto.cpp @@ -38,6 +38,7 @@ namespace opt { return l_undef; } m_solver->get_model(m_model); + m_solver->get_labels(m_labels); IF_VERBOSE(1, model_ref mdl(m_model); cb.fix_model(mdl); @@ -96,6 +97,7 @@ namespace opt { } if (is_sat == l_true) { m_solver->get_model(m_model); + m_solver->get_labels(m_labels); mk_not_dominated_by(); } return is_sat; diff --git a/src/opt/opt_pareto.h b/src/opt/opt_pareto.h index 88a3ce9c1..122f29c55 100644 --- a/src/opt/opt_pareto.h +++ b/src/opt/opt_pareto.h @@ -31,7 +31,6 @@ namespace opt { virtual expr_ref mk_gt(unsigned i, model_ref& model) = 0; virtual expr_ref mk_ge(unsigned i, model_ref& model) = 0; virtual expr_ref mk_le(unsigned i, model_ref& model) = 0; - virtual void set_model(model_ref& m) = 0; virtual void fix_model(model_ref& m) = 0; }; class pareto_base { @@ -42,6 +41,7 @@ namespace opt { ref m_solver; params_ref m_params; model_ref m_model; + svector m_labels; public: pareto_base( ast_manager & m, @@ -77,8 +77,9 @@ namespace opt { } virtual lbool operator()() = 0; - virtual void get_model(model_ref& mdl) { + virtual void get_model(model_ref& mdl, svector& labels) { mdl = m_model; + labels = m_labels; } protected: diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 02effa337..c9ee61ebc 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -51,6 +51,7 @@ namespace opt { if (src[i] >= dst[i]) { dst[i] = src[i]; m_models.set(i, m_s->get_model(i)); + m_s->get_labels(m_labels); m_lower_fmls[i] = fmls[i].get(); if (dst[i].is_pos() && !dst[i].is_finite()) { // review: likely done already. m_lower_fmls[i] = m.mk_false(); @@ -156,7 +157,8 @@ namespace opt { if (is_sat == l_true) { disj.reset(); m_s->maximize_objectives(disj); - m_s->get_model(m_model); + m_s->get_model(m_model); + m_s->get_labels(m_labels); for (unsigned i = 0; i < ors.size(); ++i) { expr_ref tmp(m); m_model->eval(ors[i].get(), tmp); @@ -203,6 +205,7 @@ namespace opt { expr_ref optsmt::update_lower() { expr_ref_vector disj(m); m_s->get_model(m_model); + m_s->get_labels(m_labels); m_s->maximize_objectives(disj); set_max(m_lower, m_s->get_objective_values(), disj); TRACE("opt", @@ -331,6 +334,7 @@ namespace opt { m_s->maximize_objective(obj_index, block); m_s->get_model(m_model); + m_s->get_labels(m_labels); inf_eps obj = m_s->saved_objective_value(obj_index); if (obj > m_lower[obj_index]) { m_lower[obj_index] = obj; @@ -405,8 +409,9 @@ namespace opt { return m_upper[i]; } - void optsmt::get_model(model_ref& mdl) { + void optsmt::get_model(model_ref& mdl, svector & labels) { mdl = m_model.get(); + labels = m_labels; } // force lower_bound(i) <= objective_value(i) diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h index 10ea9f11c..f4efa25f9 100644 --- a/src/opt/optsmt.h +++ b/src/opt/optsmt.h @@ -38,6 +38,7 @@ namespace opt { svector m_vars; symbol m_optsmt_engine; model_ref m_model; + svector m_labels; sref_vector m_models; public: optsmt(ast_manager& m): @@ -60,7 +61,7 @@ namespace opt { inf_eps get_lower(unsigned index) const; inf_eps get_upper(unsigned index) const; bool objective_is_model_valid(unsigned index) const; - void get_model(model_ref& mdl); + void get_model(model_ref& mdl, svector& labels); model* get_model(unsigned index) const { return m_models[index]; } void update_lower(unsigned idx, inf_eps const& r); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index b0d771ba8..43b2c2e3f 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -250,7 +250,6 @@ public: return "no reason given"; } virtual void get_labels(svector & r) { - UNREACHABLE(); } virtual unsigned get_num_assertions() const { return m_fmls.size(); diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index d92eef5b8..d22ca88db 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -3646,6 +3646,9 @@ namespace smt { approx_set::iterator it1 = plbls1.begin(); approx_set::iterator end1 = plbls1.end(); for (; it1 != end1; ++it1) { + if (m_context.get_cancel_flag()) { + break; + } unsigned plbl1 = *it1; SASSERT(plbls1.may_contain(plbl1)); approx_set::iterator it2 = plbls2.begin(); @@ -3687,6 +3690,9 @@ namespace smt { approx_set::iterator it1 = plbls.begin(); approx_set::iterator end1 = plbls.end(); for (; it1 != end1; ++it1) { + if (m_context.get_cancel_flag()) { + break; + } unsigned plbl1 = *it1; SASSERT(plbls.may_contain(plbl1)); approx_set::iterator it2 = clbls.begin(); @@ -3706,6 +3712,9 @@ namespace smt { svector::iterator it1 = m_new_patterns.begin(); svector::iterator end1 = m_new_patterns.end(); for (; it1 != end1; ++it1) { + if (m_context.get_cancel_flag()) { + break; + } quantifier * qa = it1->first; app * mp = it1->second; SASSERT(m_ast_manager.is_pattern(mp)); diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 524dbeab6..edb4f1e55 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -721,8 +721,8 @@ namespace smt { IF_VERBOSE(100, verbose_stream() << "(smt.collecting-features)\n";); st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas()); IF_VERBOSE(1000, st.display_primitive(verbose_stream());); - bool fixnum = st.arith_k_sum_is_small(); - bool int_only = !st.m_has_rational && !st.m_has_real; + bool fixnum = st.arith_k_sum_is_small() && m_params.m_arith_fixnum; + bool int_only = !st.m_has_rational && !st.m_has_real && m_params.m_arith_int_only; switch(m_params.m_arith_mode) { case AS_NO_ARITH: m_context.register_plugin(alloc(smt::theory_dummy, m_manager.mk_family_id("arith"), "no arithmetic")); diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp index b84d5567c..7cba66a5a 100644 --- a/src/tactic/arith/eq2bv_tactic.cpp +++ b/src/tactic/arith/eq2bv_tactic.cpp @@ -305,14 +305,16 @@ public: m_nonfd.mark(f, true); expr* e1, *e2; if (m.is_eq(f, e1, e2)) { - if (is_fd(e1, e2)) { + if (is_fd(e1, e2) || is_fd(e2, e1)) { continue; - } - if (is_fd(e2, e1)) { - continue; - } + } } - m_todo.append(to_app(f)->get_num_args(), to_app(f)->get_args()); + if (is_app(f)) { + m_todo.append(to_app(f)->get_num_args(), to_app(f)->get_args()); + } + else if (is_quantifier(f)) { + m_todo.push_back(to_quantifier(f)->get_expr()); + } } } diff --git a/src/util/util.cpp b/src/util/util.cpp index c4b729adb..bfd4923a8 100644 --- a/src/util/util.cpp +++ b/src/util/util.cpp @@ -151,24 +151,3 @@ void escaped::display(std::ostream & out) const { } } -#ifdef _WINDOWS -#ifdef ARRAYSIZE -#undef ARRAYSIZE -#endif -#include -#endif - -void z3_bound_num_procs() { - -#ifdef _Z3_COMMERCIAL -#define Z3_COMMERCIAL_MAX_CORES 4 -#ifdef _WINDOWS - DWORD_PTR numProcs = (1 << Z3_COMMERCIAL_MAX_CORES) - 1; - SetProcessAffinityMask(GetCurrentProcess(), numProcs); -#endif -#else - // Not bounded: Research evaluations are - // not reasonable if run with artificial - // or hidden throttles. -#endif -} diff --git a/src/util/util.h b/src/util/util.h index f97f5c1f9..1e15b526c 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -400,7 +400,6 @@ inline size_t megabytes_to_bytes(unsigned mb) { return r; } -void z3_bound_num_procs(); #endif /* UTIL_H_ */