From 1620796bd1dfc6876c5f096593cda32fb4400baa Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 17 Aug 2017 17:25:04 +0100 Subject: [PATCH 1/6] Whitespace --- src/ast/pattern/pattern_inference.cpp | 71 +++++++++++++-------------- 1 file changed, 35 insertions(+), 36 deletions(-) diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp index c8247e409..11268b2f3 100644 --- a/src/ast/pattern/pattern_inference.cpp +++ b/src/ast/pattern/pattern_inference.cpp @@ -54,7 +54,7 @@ bool smaller_pattern::process(expr * p1, expr * p2) { unsigned num1 = app1->get_num_args(); if (num1 != app2->get_num_args() || app1->get_decl() != app2->get_decl()) return false; - for (unsigned i = 0; i < num1; i++) + for (unsigned i = 0; i < num1; i++) save(app1->get_arg(i), app2->get_arg(i)); break; } @@ -67,7 +67,7 @@ bool smaller_pattern::process(expr * p1, expr * p2) { return false; } // it is a variable bound by an external quantifier - else if (p1 != p2) + else if (p1 != p2) return false; break; } @@ -137,7 +137,7 @@ bool pattern_inference::collect::visit_children(expr * n, unsigned delta) { bool visited = true; unsigned i; switch (n->get_kind()) { - case AST_APP: + case AST_APP: i = to_app(n)->get_num_args(); while (i > 0) { --i; @@ -187,14 +187,14 @@ void pattern_inference::collect::save_candidate(expr * n, unsigned delta) { save(n, delta, 0); return; } - + if (c->get_num_args() == 0) { save(n, delta, alloc(info, m, n, uint_set(), 1)); return; } ptr_buffer buffer; - bool changed = false; // false if none of the children is mapped to a node different from itself. + bool changed = false; // false if none of the children is mapped to a node different from itself. uint_set free_vars; unsigned size = 1; unsigned num = c->get_num_args(); @@ -216,7 +216,7 @@ void pattern_inference::collect::save_candidate(expr * n, unsigned delta) { if (child != child_info->m_node.get()) changed = true; } - + app * new_node = 0; if (changed) new_node = m.mk_app(decl, buffer.size(), buffer.c_ptr()); @@ -229,11 +229,11 @@ void pattern_inference::collect::save_candidate(expr * n, unsigned delta) { // // Remark: The rule above has an exception. The operators (div, idiv, mod) are allowed to be // used as patterns even when they are not nested in other terms. The motivation is that - // Z3 currently doesn't implement them (i.e., they are uninterpreted). So, some users add axioms + // Z3 currently doesn't implement them (i.e., they are uninterpreted). So, some users add axioms // stating properties about these operators. family_id fid = c->get_family_id(); decl_kind k = c->get_decl_kind(); - if (!free_vars.empty() && + if (!free_vars.empty() && (fid != m_afid || (fid == m_afid && !m_owner.m_nested_arith_only && (k == OP_DIV || k == OP_IDIV || k == OP_MOD || k == OP_REM || k == OP_MUL)))) { TRACE("pattern_inference", tout << "potential candidate: \n" << mk_pp(new_node, m) << "\n";); m_owner.add_candidate(new_node, free_vars, size); @@ -288,7 +288,7 @@ void pattern_inference::filter_looping_patterns(ptr_vector & result) { uint_set const & s2 = e2->get_data().m_value.m_free_vars; // Remark: the comparison operator only makes sense if both AST nodes // contain the same number of variables. - // Example: + // Example: // (f X Y) <: (f (g X Z W) Y) if (s1 == s2 && m_le(m_num_bindings, n1, n2) && !m_le(m_num_bindings, n2, n1)) { smaller = true; @@ -421,12 +421,12 @@ void pattern_inference::candidates2unary_patterns(ptr_vector const & candid } // TODO: this code is too inefficient when the number of candidate -// patterns is too big. +// patterns is too big. // HACK: limit the number of case-splits: #define MAX_SPLITS 32 -void pattern_inference::candidates2multi_patterns(unsigned max_num_patterns, - ptr_vector const & candidate_patterns, +void pattern_inference::candidates2multi_patterns(unsigned max_num_patterns, + ptr_vector const & candidate_patterns, app_ref_buffer & result) { SASSERT(!candidate_patterns.empty()); m_pre_patterns.push_back(alloc(pre_pattern)); @@ -464,7 +464,7 @@ void pattern_inference::candidates2multi_patterns(unsigned max_num_patterns, m_pre_patterns.push_back(curr); } } - TRACE("pattern_inference", tout << "m_pre_patterns.size(): " << m_pre_patterns.size() << + TRACE("pattern_inference", tout << "m_pre_patterns.size(): " << m_pre_patterns.size() << "\nnum_splits: " << num_splits << "\n";); } } @@ -478,7 +478,7 @@ void pattern_inference::reset_pre_patterns() { static void dump_app_vector(std::ostream & out, ptr_vector const & v, ast_manager & m) { ptr_vector::const_iterator it = v.begin(); ptr_vector::const_iterator end = v.end(); - for (; it != end; ++it) + for (; it != end; ++it) out << mk_pp(*it, m) << "\n"; } #endif @@ -487,8 +487,8 @@ bool pattern_inference::is_forbidden(app * n) const { func_decl const * decl = n->get_decl(); if (is_ground(n)) return false; - // Remark: skolem constants should not be used in patterns, since they do not - // occur outside of the quantifier. That is, Z3 will never match this kind of + // Remark: skolem constants should not be used in patterns, since they do not + // occur outside of the quantifier. That is, Z3 will never match this kind of // pattern. if (m_params.m_pi_avoid_skolems && decl->is_skolem()) { CTRACE("pattern_inference_skolem", decl->is_skolem(), tout << "ignoring: " << mk_pp(n, m) << "\n";); @@ -521,9 +521,9 @@ bool pattern_inference::has_preferred_patterns(ptr_vector & candidate_patte return found; } -void pattern_inference::mk_patterns(unsigned num_bindings, - expr * n, - unsigned num_no_patterns, +void pattern_inference::mk_patterns(unsigned num_bindings, + expr * n, + unsigned num_no_patterns, expr * const * no_patterns, app_ref_buffer & result) { m_num_bindings = num_bindings; @@ -532,7 +532,7 @@ void pattern_inference::mk_patterns(unsigned num_bindings, m_collect(n, num_bindings); - TRACE("pattern_inference", + TRACE("pattern_inference", tout << mk_pp(n, m); tout << "\ncandidates:\n"; unsigned num = m_candidates.size(); @@ -558,7 +558,7 @@ void pattern_inference::mk_patterns(unsigned num_bindings, m_tmp1.reset(); candidates2unary_patterns(m_tmp2, m_tmp1, result); unsigned num_extra_multi_patterns = m_params.m_pi_max_multi_patterns; - if (result.empty()) + if (result.empty()) num_extra_multi_patterns++; if (num_extra_multi_patterns > 0 && !m_tmp1.empty()) { // m_pattern_weight_lt is not a total order @@ -604,7 +604,7 @@ void pattern_inference::reduce1_quantifier(quantifier * q) { else { quantifier_ref tmp(m); tmp = m.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), q->get_expr()); - new_q = m.update_quantifier_weight(tmp, new_weight); + new_q = m.update_quantifier_weight(tmp, new_weight); TRACE("pattern_inference", tout << "found patterns in database, weight: " << new_weight << "\n" << mk_pp(new_q, m) << "\n";); } proof * pr = 0; @@ -635,15 +635,15 @@ void pattern_inference::reduce1_quantifier(quantifier * q) { proof * new_pattern_pr; get_cached(q->get_no_pattern(i), new_pattern, new_pattern_pr); new_no_patterns.push_back(new_pattern); - } - + } + app_ref_buffer new_patterns(m); - + if (m_params.m_pi_arith == AP_CONSERVATIVE) m_forbidden.push_back(m_afid); mk_patterns(q->get_num_decls(), new_body, new_no_patterns.size(), new_no_patterns.c_ptr(), new_patterns); - + if (new_patterns.empty() && !new_no_patterns.empty()) { if (new_patterns.empty()) { mk_patterns(q->get_num_decls(), new_body, 0, 0, new_patterns); @@ -652,7 +652,7 @@ void pattern_inference::reduce1_quantifier(quantifier * q) { } } } - + if (m_params.m_pi_arith == AP_CONSERVATIVE) { m_forbidden.pop_back(); if (new_patterns.empty()) { @@ -661,13 +661,13 @@ void pattern_inference::reduce1_quantifier(quantifier * q) { if (!new_patterns.empty()) { weight = std::max(weight, static_cast(m_params.m_pi_arith_weight)); if (m_params.m_pi_warnings) { - warning_msg("using arith. in pattern (quantifier id: %s), the weight was increased to %d (this value can be modified using PI_ARITH_WEIGHT=).", + warning_msg("using arith. in pattern (quantifier id: %s), the weight was increased to %d (this value can be modified using PI_ARITH_WEIGHT=).", q->get_qid().str().c_str(), weight); } } } } - + if (m_params.m_pi_arith != AP_NO && new_patterns.empty()) { if (new_patterns.empty()) { flet l1(m_nested_arith_only, false); // try to find a non-nested arith pattern @@ -676,8 +676,8 @@ void pattern_inference::reduce1_quantifier(quantifier * q) { if (!new_patterns.empty()) { weight = std::max(weight, static_cast(m_params.m_pi_non_nested_arith_weight)); if (m_params.m_pi_warnings) { - warning_msg("using non nested arith. pattern (quantifier id: %s), the weight was increased to %d (this value can be modified using PI_NON_NESTED_ARITH_WEIGHT=).", - q->get_qid().str().c_str(), weight); + warning_msg("using non nested arith. pattern (quantifier id: %s), the weight was increased to %d (this value can be modified using PI_NON_NESTED_ARITH_WEIGHT=).", + q->get_qid().str().c_str(), weight); } // verbose_stream() << mk_pp(q, m) << "\n"; } @@ -689,12 +689,12 @@ void pattern_inference::reduce1_quantifier(quantifier * q) { if (weight != q->get_weight()) new_q = m.update_quantifier_weight(new_q, weight); proof_ref pr(m); - if (m.fine_grain_proofs()) { + if (m.fine_grain_proofs()) { if (new_body_pr == 0) new_body_pr = m.mk_reflexivity(new_body); pr = m.mk_quant_intro(q, new_q, new_body_pr); } - + if (new_patterns.empty() && m_params.m_pi_pull_quantifiers) { pull_quant pull(m); expr_ref new_expr(m); @@ -728,9 +728,8 @@ void pattern_inference::reduce1_quantifier(quantifier * q) { cache_result(q, q, 0); return; } - - cache_result(q, new_q, pr); + cache_result(q, new_q, pr); } @@ -739,7 +738,7 @@ void pattern_inference::reduce1_quantifier(quantifier * q) { static void dump_expr_vector(std::ostream & out, ptr_vector const & v, ast_manager & m) { ptr_vector::const_iterator it = v.begin(); ptr_vector::const_iterator end = v.end(); - for (; it != end; ++it) + for (; it != end; ++it) out << mk_pp(*it, m) << "\n"; } #endif From 3487b368d1413cdff2de9f269a76f7ab92148ec9 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 17 Aug 2017 17:27:06 +0100 Subject: [PATCH 2/6] Added diagnostic output for pattern inference. --- src/ast/pattern/pattern_inference.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp index 11268b2f3..d97c2f094 100644 --- a/src/ast/pattern/pattern_inference.cpp +++ b/src/ast/pattern/pattern_inference.cpp @@ -729,6 +729,12 @@ void pattern_inference::reduce1_quantifier(quantifier * q) { return; } + IF_IVERBOSE(10, + verbose_stream() << "(smt.inferred-patterns :qid " << q->get_qid() << "\n"; + for (unsigned i = 0; i < new_patterns.size(); i++) + verbose_stream() << " " << mk_ismt2_pp(new_patterns[i], m, 2) << "\n"; + verbose_stream() << ")\n"; ); + cache_result(q, new_q, pr); } From a2d7b43554adff1e480cf0c6a8e341d562928aa9 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 17 Aug 2017 17:47:40 +0100 Subject: [PATCH 3/6] Update header includes to be relative to `src/` directory. --- scripts/update_api.py | 12 ++++++------ src/api/api_algebraic.cpp | 2 +- src/api/api_arith.cpp | 2 +- src/api/api_array.cpp | 2 +- src/api/api_ast.cpp | 2 +- src/api/api_ast_map.cpp | 2 +- src/api/api_ast_vector.cpp | 2 +- src/api/api_bv.cpp | 2 +- src/api/api_config_params.cpp | 2 +- src/api/api_context.cpp | 4 ++-- src/api/api_datalog.cpp | 2 +- src/api/api_datatype.cpp | 2 +- src/api/api_fpa.cpp | 2 +- src/api/api_goal.cpp | 2 +- src/api/api_interp.cpp | 2 +- src/api/api_log.cpp | 4 ++-- src/api/api_model.cpp | 2 +- src/api/api_numeral.cpp | 2 +- src/api/api_opt.cpp | 2 +- src/api/api_params.cpp | 2 +- src/api/api_parsers.cpp | 2 +- src/api/api_pb.cpp | 2 +- src/api/api_polynomial.cpp | 2 +- src/api/api_qe.cpp | 2 +- src/api/api_quant.cpp | 2 +- src/api/api_rcf.cpp | 2 +- src/api/api_seq.cpp | 2 +- src/api/api_solver.cpp | 2 +- src/api/api_stats.cpp | 2 +- src/api/api_tactic.cpp | 2 +- src/cmd_context/basic_cmds.cpp | 2 +- src/duality/duality_wrapper.h | 2 +- src/shell/main.cpp | 2 +- 33 files changed, 40 insertions(+), 40 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 4000b3da2..67a1b8a33 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1573,7 +1573,7 @@ def def_APIs(api_files): def write_log_h_preamble(log_h): log_h.write('// Automatically generated file\n') - log_h.write('#include\"z3.h\"\n') + log_h.write('#include\"api/z3.h\"\n') log_h.write('#ifdef __GNUC__\n') log_h.write('#define _Z3_UNUSED __attribute__((unused))\n') log_h.write('#else\n') @@ -1592,14 +1592,14 @@ def write_log_h_preamble(log_h): def write_log_c_preamble(log_c): log_c.write('// Automatically generated file\n') log_c.write('#include\n') - log_c.write('#include\"z3.h\"\n') - log_c.write('#include\"api_log_macros.h\"\n') - log_c.write('#include\"z3_logger.h\"\n') + log_c.write('#include\"api/z3.h\"\n') + log_c.write('#include\"api/api_log_macros.h\"\n') + log_c.write('#include\"api/z3_logger.h\"\n') def write_exe_c_preamble(exe_c): exe_c.write('// Automatically generated file\n') - exe_c.write('#include\"z3.h\"\n') - exe_c.write('#include\"z3_replayer.h\"\n') + exe_c.write('#include\"api/z3.h\"\n') + exe_c.write('#include\"api/z3_replayer.h\"\n') # exe_c.write('void Z3_replayer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg(ctx, c)); }\n') diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp index 40e8c846b..96d8392ba 100644 --- a/src/api/api_algebraic.cpp +++ b/src/api/api_algebraic.cpp @@ -18,7 +18,7 @@ Notes: --*/ #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_ast_vector.h" #include "math/polynomial/algebraic_numbers.h" diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp index 80eb261ad..8fbed6f46 100644 --- a/src/api/api_arith.cpp +++ b/src/api/api_arith.cpp @@ -16,7 +16,7 @@ Revision History: --*/ #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_util.h" #include "ast/arith_decl_plugin.h" diff --git a/src/api/api_array.cpp b/src/api/api_array.cpp index f4682ea8f..a5916e987 100644 --- a/src/api/api_array.cpp +++ b/src/api/api_array.cpp @@ -16,7 +16,7 @@ Revision History: --*/ #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_util.h" #include "ast/array_decl_plugin.h" diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index c14a24df1..ab93c3cbd 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -16,7 +16,7 @@ Revision History: --*/ #include -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_util.h" #include "ast/well_sorted.h" diff --git a/src/api/api_ast_map.cpp b/src/api/api_ast_map.cpp index fc593c1f5..d0388b97a 100644 --- a/src/api/api_ast_map.cpp +++ b/src/api/api_ast_map.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_ast_map.h" #include "api/api_ast_vector.h" diff --git a/src/api/api_ast_vector.cpp b/src/api/api_ast_vector.cpp index 04802cba5..471a308b6 100644 --- a/src/api/api_ast_vector.cpp +++ b/src/api/api_ast_vector.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_ast_vector.h" #include "ast/ast_translation.h" diff --git a/src/api/api_bv.cpp b/src/api/api_bv.cpp index 52fcb867c..3b5d60be3 100644 --- a/src/api/api_bv.cpp +++ b/src/api/api_bv.cpp @@ -16,7 +16,7 @@ Revision History: --*/ #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_util.h" #include "ast/bv_decl_plugin.h" diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp index d35297f59..460101d34 100644 --- a/src/api/api_config_params.cpp +++ b/src/api/api_config_params.cpp @@ -18,7 +18,7 @@ Revision History: #include "api/z3.h" #include "api/api_context.h" #include "ast/pp.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_util.h" #include "cmd_context/cmd_context.h" #include "util/symbol.h" diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 2c93ee85d..210e0a1d4 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -20,10 +20,10 @@ Revision History: #include #include "api/api_context.h" #include "parsers/smt/smtparser.h" -#include"version.h" +#include "util/version.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_util.h" #include "ast/reg_decl_plugins.h" #include "math/realclosure/realclosure.h" diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 8f863ed42..397e2a8af 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -20,7 +20,7 @@ Revision History: #include "api/api_util.h" #include "ast/ast_pp.h" #include "api/api_ast_vector.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_stats.h" #include "muz/fp/datalog_parser.h" #include "util/cancel_eh.h" diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index 7e9758a04..851d96a4e 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -16,7 +16,7 @@ Revision History: --*/ #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_util.h" #include "ast/datatype_decl_plugin.h" diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 8e4d13af4..484cb3d76 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -18,7 +18,7 @@ Notes: --*/ #include #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "ast/fpa_decl_plugin.h" diff --git a/src/api/api_goal.cpp b/src/api/api_goal.cpp index 3fe23828d..0f1b9056b 100644 --- a/src/api/api_goal.cpp +++ b/src/api/api_goal.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_goal.h" #include "ast/ast_translation.h" diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 276e56989..fb2699e0a 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -18,7 +18,7 @@ #include #include #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_tactic.h" #include "api/api_solver.h" diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp index aa00de424..410110d9a 100644 --- a/src/api/api_log.cpp +++ b/src/api/api_log.cpp @@ -17,9 +17,9 @@ Revision History: --*/ #include #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "util/util.h" -#include"version.h" +#include "util/version.h" std::ostream * g_z3_log = 0; bool g_z3_log_enabled = false; diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index 73428a3d7..de917650d 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_model.h" #include "api/api_ast_vector.h" diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index c3717b5d2..95bc0bef9 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_util.h" #include "ast/arith_decl_plugin.h" diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 8c49b526e..a967dfb2b 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_stats.h" #include "api/api_context.h" #include "api/api_util.h" diff --git a/src/api/api_params.cpp b/src/api/api_params.cpp index 86dfe9a93..3f3cbed1d 100644 --- a/src/api/api_params.cpp +++ b/src/api/api_params.cpp @@ -19,7 +19,7 @@ Revision History: --*/ #include #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_util.h" #include "util/params.h" diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index 8c2723e9a..bef31e9f1 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_util.h" #include "cmd_context/cmd_context.h" diff --git a/src/api/api_pb.cpp b/src/api/api_pb.cpp index 97e627ec0..e6f8f77b4 100644 --- a/src/api/api_pb.cpp +++ b/src/api/api_pb.cpp @@ -16,7 +16,7 @@ Revision History: --*/ #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_util.h" #include "ast/pb_decl_plugin.h" diff --git a/src/api/api_polynomial.cpp b/src/api/api_polynomial.cpp index 398fdeb3a..9be73289f 100644 --- a/src/api/api_polynomial.cpp +++ b/src/api/api_polynomial.cpp @@ -17,7 +17,7 @@ Notes: --*/ #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_polynomial.h" #include "api/api_ast_vector.h" diff --git a/src/api/api_qe.cpp b/src/api/api_qe.cpp index 0c2948ce5..34f21d64b 100644 --- a/src/api/api_qe.cpp +++ b/src/api/api_qe.cpp @@ -19,7 +19,7 @@ Notes: #include #include "api/z3.h" -#include "api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_util.h" #include "api/api_model.h" diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp index f7d5bf13a..d64768b3b 100644 --- a/src/api/api_quant.cpp +++ b/src/api/api_quant.cpp @@ -16,7 +16,7 @@ Revision History: --*/ #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_util.h" #include "parsers/util/pattern_validation.h" diff --git a/src/api/api_rcf.cpp b/src/api/api_rcf.cpp index 377e83a44..84c250114 100644 --- a/src/api/api_rcf.cpp +++ b/src/api/api_rcf.cpp @@ -21,7 +21,7 @@ Notes: --*/ #include #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "math/realclosure/realclosure.h" diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index a652fd912..44003a5fb 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_util.h" #include "ast/ast_pp.h" diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 6435b8288..7fd6d08fe 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -18,7 +18,7 @@ Revision History: --*/ #include #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_tactic.h" #include "api/api_solver.h" diff --git a/src/api/api_stats.cpp b/src/api/api_stats.cpp index 440aec22d..a92b908dc 100644 --- a/src/api/api_stats.cpp +++ b/src/api/api_stats.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_stats.h" diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index 661660a63..ccb1ce597 100644 --- a/src/api/api_tactic.cpp +++ b/src/api/api_tactic.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include #include "api/z3.h" -#include"api_log_macros.h" +#include "api/api_log_macros.h" #include "api/api_context.h" #include "api/api_tactic.h" #include "api/api_model.h" diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index db522b82b..c81170ba4 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -16,7 +16,7 @@ Notes: --*/ #include "cmd_context/cmd_context.h" -#include"version.h" +#include "util/version.h" #include "ast/ast_smt_pp.h" #include "ast/ast_smt2_pp.h" #include "ast/ast_pp.h" diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index 8e2d70ea6..8ea8017a2 100644 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -27,7 +27,7 @@ #include #include #include -#include"version.h" +#include "util/version.h" #include #include "interp/iz3hash.h" diff --git a/src/shell/main.cpp b/src/shell/main.cpp index 3f3ba5182..3d2609c4f 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -26,7 +26,7 @@ Revision History: #include "shell/smtlib_frontend.h" #include "shell/z3_log_frontend.h" #include "util/warning.h" -#include"version.h" +#include "util/version.h" #include "shell/dimacs_frontend.h" #include "shell/datalog_frontend.h" #include "shell/opt_frontend.h" From 920c596c23528da5daaee7c2fdc04e78077c46dd Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 17 Aug 2017 18:14:49 +0100 Subject: [PATCH 4/6] [CMake] Clean up setting include paths. Now that all include paths are relative to the `src/` trees ( one in source tree and one in the build tree) we can simplify what the CMake build does significantly. While I'm here I also removed some dead code that wasn't doing anything useful. --- cmake/z3_add_component.cmake | 29 ++--------------------------- 1 file changed, 2 insertions(+), 27 deletions(-) diff --git a/cmake/z3_add_component.cmake b/cmake/z3_add_component.cmake index b70838750..d87ffbe61 100644 --- a/cmake/z3_add_component.cmake +++ b/cmake/z3_add_component.cmake @@ -36,15 +36,8 @@ function(z3_add_component_dependencies_to_target target_name) # Remaing args should be component names set(_expanded_deps ${ARGN}) foreach (dependency ${_expanded_deps}) - # FIXME: Adding these include paths wouldn't be necessary if the sources - # used include paths rooted in the ``src`` directory. - get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES) - foreach (inc_dir ${_dep_include_dirs}) - target_include_directories(${target_name} PRIVATE "${inc_dir}") - endforeach() - unset(_dep_include_dirs) # Ensure this component's dependencies are built before this component. - # This important because we might need the generated header files in + # This is important because we might need the generated header files in # other components. add_dependencies(${target_name} ${dependency}) endforeach() @@ -214,18 +207,14 @@ macro(z3_add_component component_name) target_compile_options(${component_name} PRIVATE ${flag}) endforeach() - # It's unfortunate that we have to manage the include directories and dependencies ourselves. + # It's unfortunate that we have to manage dependencies ourselves. # # If we weren't building "object" libraries we could use # ``` - # target_include_directories(${component_name} INTERFACE "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}") # target_link_libraries(${component_name} INTERFACE ${Z3_MOD_COMPONENT_DEPENDENCIES}) # ``` # but we can't do that with "object" libraries. - # Record this component's include directories - set_property(GLOBAL PROPERTY Z3_${component_name}_INCLUDES "${CMAKE_CURRENT_SOURCE_DIR}") - set_property(GLOBAL APPEND PROPERTY Z3_${component_name}_INCLUDES "${CMAKE_CURRENT_BINARY_DIR}") set_property(GLOBAL PROPERTY Z3_${component_name}_DEPS "") # Record this component's dependencies foreach (dependency ${Z3_MOD_COMPONENT_DEPENDENCIES}) @@ -243,12 +232,6 @@ macro(z3_add_component component_name) endif() #message(STATUS "Component \"${component_name}\" has the following dependencies ${_expanded_deps}") - # For any generated header files for this component - target_include_directories(${component_name} PRIVATE "${CMAKE_CURRENT_BINARY_DIR}") - # So that any generated header files can refer to source files in the component's - # source tree - target_include_directories(${component_name} PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}") - # Add any extra include directories foreach (extra_include ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}) target_include_directories(${component_name} PRIVATE "${extra_include}") @@ -283,7 +266,6 @@ macro(z3_add_install_tactic_rule) endforeach() unset(_component_tactic_header_files) - list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}") add_custom_command(OUTPUT "install_tactic.cpp" COMMAND "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py" @@ -311,13 +293,6 @@ macro(z3_add_memory_initializer_rule) ) endif() z3_expand_dependencies(_expanded_components ${ARGN}) - # Get paths to search - set(_search_paths "") - foreach (dependency ${_expanded_components}) - get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES) - list(APPEND _search_paths ${_dep_include_dirs}) - endforeach() - list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}") # Get header files that declare initializers and finalizers set(_mem_init_finalize_headers "") From 320c81e497f3d1d1810fecda840a91265ba68b77 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 17 Aug 2017 19:18:14 +0100 Subject: [PATCH 5/6] Whitespace --- src/smt/smt_model_checker.cpp | 46 +++++++++++++++++------------------ src/smt/smt_model_checker.h | 6 ++--- 2 files changed, 26 insertions(+), 26 deletions(-) diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index d5b8415c3..23e2589f9 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -53,8 +53,8 @@ namespace smt { } void model_checker::set_qm(quantifier_manager & qm) { - SASSERT(m_qm == 0); - SASSERT(m_context == 0); + SASSERT(m_qm == 0); + SASSERT(m_context == 0); m_qm = &qm; m_context = &(m_qm->get_context()); } @@ -112,7 +112,7 @@ namespace smt { if (!m_curr_model->eval(q->get_expr(), tmp, true)) { return; } - TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";); + TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";); ptr_buffer subst_args; unsigned num_decls = q->get_num_decls(); subst_args.resize(num_decls, 0); @@ -139,7 +139,7 @@ namespace smt { bool model_checker::add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv) { if (cex == 0) { TRACE("model_checker", tout << "no model is available\n";); - return false; + return false; } unsigned num_decls = q->get_num_decls(); // Remark: sks were created for the flat version of q. @@ -187,20 +187,20 @@ namespace smt { } bindings.set(num_decls - i - 1, sk_value); } - + TRACE("model_checker", tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: "; for (unsigned i = 0; i < num_decls; i++) { tout << mk_ismt2_pp(bindings[i].get(), m) << " "; } tout << "\n";); - + max_generation = std::max(m_qm->get_generation(q), max_generation); add_instance(q, bindings, max_generation); return true; } void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation) { - for (unsigned i = 0; i < bindings.size(); i++) + for (unsigned i = 0; i < bindings.size(); i++) m_new_instances_bindings.push_back(bindings[i]); void * mem = m_new_instances_region.allocate(instance::get_obj_size(q->get_num_decls())); instance * new_inst = new (mem) instance(q, bindings.c_ptr(), max_generation); @@ -260,39 +260,39 @@ namespace smt { bool model_checker::check(quantifier * q) { SASSERT(!m_aux_context->relevancy()); m_aux_context->push(); - + quantifier * flat_q = get_flat_quantifier(q); - TRACE("model_checker", tout << "model checking:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" << + TRACE("model_checker", tout << "model checking:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" << mk_ismt2_pp(flat_q->get_expr(), m) << "\n";); expr_ref_vector sks(m); assert_neg_q_m(flat_q, sks); - TRACE("model_checker", tout << "skolems:\n"; + TRACE("model_checker", tout << "skolems:\n"; for (unsigned i = 0; i < sks.size(); i++) { expr * sk = sks.get(i); tout << mk_ismt2_pp(sk, m) << " " << mk_pp(m.get_sort(sk), m) << "\n"; }); - + lbool r = m_aux_context->check(); TRACE("model_checker", tout << "[complete] model-checker result: " << to_sat_str(r) << "\n";); if (r != l_true) { m_aux_context->pop(1); return r == l_false; // quantifier is satisfied by m_curr_model } - + model_ref complete_cex; - m_aux_context->get_model(complete_cex); - + m_aux_context->get_model(complete_cex); + // try to find new instances using instantiation sets. m_model_finder.restrict_sks_to_inst_set(m_aux_context.get(), q, sks); - + unsigned num_new_instances = 0; while (true) { lbool r = m_aux_context->check(); - TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";); + TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";); if (r != l_true) - break; + break; model_ref cex; m_aux_context->get_model(cex); if (!add_instance(q, cex.get(), sks, true)) { @@ -302,7 +302,7 @@ namespace smt { if (num_new_instances >= m_max_cexs || !add_blocking_clause(cex.get(), sks)) { TRACE("model_checker", tout << "Add blocking clause failed new-instances: " << num_new_instances << " max-cex: " << m_max_cexs << "\n";); // add_blocking_clause failed... stop the search for new counter-examples... - break; + break; } } @@ -395,17 +395,17 @@ namespace smt { check_quantifiers(false, found_relevant, num_failures); - + if (found_relevant) m_iteration_idx++; TRACE("model_checker", tout << "model after check:\n"; model_pp(tout, *md);); - TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";); + TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";); m_max_cexs += m_params.m_mbqi_max_cexs; if (num_failures == 0 && !m_context->validate_model()) { num_failures = 1; - // this time force expanding recursive function definitions + // this time force expanding recursive function definitions // that are not forced true in the current model. check_quantifiers(true, found_relevant, num_failures); } @@ -426,7 +426,7 @@ namespace smt { for (; it != end; ++it) { quantifier * q = *it; if(!m_qm->mbqi_enabled(q)) continue; - TRACE("model_checker", + TRACE("model_checker", tout << "Check: " << mk_pp(q, m) << "\n"; tout << m_context->get_assignment(q) << "\n";); @@ -505,7 +505,7 @@ namespace smt { expr * b = inst->m_bindings[i]; tout << mk_pp(b, m) << "\n"; }); - TRACE("model_checker_instance", + TRACE("model_checker_instance", expr_ref inst_expr(m); instantiate(m, q, inst->m_bindings, inst_expr); tout << "(assert " << mk_ismt2_pp(inst_expr, m) << ")\n";); diff --git a/src/smt/smt_model_checker.h b/src/smt/smt_model_checker.h index 7f2ed8ca7..4a9c28aba 100644 --- a/src/smt/smt_model_checker.h +++ b/src/smt/smt_model_checker.h @@ -39,7 +39,7 @@ namespace smt { class model_checker { ast_manager & m; // _manager; qi_params const & m_params; - // copy of smt_params for auxiliary context. + // copy of smt_params for auxiliary context. // the idea is to use a different configuration for the aux context (e.g., disable relevancy) scoped_ptr m_fparams; quantifier_manager * m_qm; @@ -83,8 +83,8 @@ namespace smt { struct is_model_value {}; expr_mark m_visited; - bool contains_model_value(expr* e); - void add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation); + bool contains_model_value(expr * e); + void add_instance(quantifier * q, expr_ref_vector const & bindings, unsigned max_generation); public: model_checker(ast_manager & m, qi_params const & p, model_finder & mf); From abd599f48ef74f2acd4324abbc2610eac9338ebc Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 17 Aug 2017 19:29:37 +0100 Subject: [PATCH 6/6] Fixed ref-counting bug in smt_model_checker. Fixes #1212. --- src/smt/smt_model_checker.cpp | 11 ++++++++--- src/smt/smt_model_checker.h | 2 +- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 23e2589f9..875e7adf2 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -40,7 +40,7 @@ namespace smt { m_max_cexs(1), m_iteration_idx(0), m_curr_model(0), - m_new_instances_bindings(m) { + m_pinned_exprs(m) { } model_checker::~model_checker() { @@ -200,8 +200,12 @@ namespace smt { } void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation) { + SASSERT(q->get_num_decls() == bindings.size()); + for (unsigned i = 0; i < bindings.size(); i++) - m_new_instances_bindings.push_back(bindings[i]); + m_pinned_exprs.push_back(bindings[i]); + m_pinned_exprs.push_back(q); + void * mem = m_new_instances_region.allocate(instance::get_obj_size(q->get_num_decls())); instance * new_inst = new (mem) instance(q, bindings.c_ptr(), max_generation); m_new_instances.push_back(new_inst); @@ -469,8 +473,9 @@ namespace smt { } void model_checker::reset_new_instances() { - m_new_instances_region.reset(); + m_pinned_exprs.reset(); m_new_instances.reset(); + m_new_instances_region.reset(); } void model_checker::reset() { diff --git a/src/smt/smt_model_checker.h b/src/smt/smt_model_checker.h index 4a9c28aba..778f913c3 100644 --- a/src/smt/smt_model_checker.h +++ b/src/smt/smt_model_checker.h @@ -73,8 +73,8 @@ namespace smt { }; region m_new_instances_region; - expr_ref_vector m_new_instances_bindings; ptr_vector m_new_instances; + expr_ref_vector m_pinned_exprs; bool add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv); void reset_new_instances(); void assert_new_instances();