From 96d0781c9d0790a3d54ba8a4a339bc89c32f030c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 17 Aug 2017 11:39:06 +0100 Subject: [PATCH 1/8] Whitespace --- src/smt/mam.cpp | 492 ++++++++++++++++++++++++------------------------ 1 file changed, 246 insertions(+), 246 deletions(-) diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index f59a57bf3..1fc5ed220 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -34,7 +34,7 @@ Revision History: // send profiling information to stdout #define _PROFILE_MAM_TO_STDOUT // threshold in secs for being considered expensive -#define _PROFILE_MAM_THRESHOLD 30.0 +#define _PROFILE_MAM_THRESHOLD 30.0 // dump expensive (> _PROFILE_MAM_THRESHOLD) code trees whenever execute_core is executed. #define _PROFILE_MAM_EXPENSIVE // @@ -60,7 +60,7 @@ namespace smt { // ------------------------------------ class mam_impl; - + typedef trail_stack mam_trail_stack; typedef trail mam_trail; @@ -70,8 +70,8 @@ namespace smt { public: mam_value_trail(T & value):value_trail(value) {} }; - - + + // ------------------------------------ // // Auxiliary @@ -79,7 +79,7 @@ namespace smt { // ------------------------------------ class label_hasher { svector m_lbl2hash; // cache: lbl_id -> hash - + void mk_lbl_hash(unsigned lbl_id) { unsigned a = 17; unsigned b = 3; @@ -124,19 +124,19 @@ namespace smt { typedef enum { INIT1=0, INIT2, INIT3, INIT4, INIT5, INIT6, INITN, BIND1, BIND2, BIND3, BIND4, BIND5, BIND6, BINDN, - YIELD1, YIELD2, YIELD3, YIELD4, YIELD5, YIELD6, YIELDN, + YIELD1, YIELD2, YIELD3, YIELD4, YIELD5, YIELD6, YIELDN, COMPARE, CHECK, FILTER, CFILTER, PFILTER, CHOOSE, NOOP, CONTINUE, - GET_ENODE, + GET_ENODE, GET_CGR1, GET_CGR2, GET_CGR3, GET_CGR4, GET_CGR5, GET_CGR6, GET_CGRN, IS_CGR } opcode; - + struct instruction { opcode m_opcode; instruction * m_next; #ifdef _PROFILE_MAM unsigned m_counter; // how often it was executed -#endif +#endif bool is_init() const { return m_opcode >= INIT1 && m_opcode <= INITN; } @@ -147,7 +147,7 @@ namespace smt { // operators (e.g., + and *) are represented using n-ary // applications. // We do not need the extra field for INIT1, ..., INIT6. - unsigned m_num_args; + unsigned m_num_args; }; struct compare : public instruction { @@ -162,7 +162,7 @@ namespace smt { struct filter : public instruction { unsigned m_reg; - approx_set m_lbl_set; + approx_set m_lbl_set; }; struct pcheck : public instruction { @@ -211,15 +211,15 @@ namespace smt { approx_set m_lbl_set; // singleton set containing m_label /* The following field is an array of tagged pointers. - Each positon contains: + Each positon contains: 1- null (no joint), NULL_TAG 2- a boxed integer (i.e., register that contains the variable bind) VAR_TAG 3- an enode pointer (ground term) GROUND_TERM_TAG 4- or, a joint2 pointer. NESTED_VAR_TAG - + The size of the array is m_num_args. */ - enode * m_joints[0]; + enode * m_joints[0]; }; struct bind : public instruction { @@ -294,7 +294,7 @@ namespace smt { void display_joints(std::ostream & out, unsigned num_joints, enode * const * joints) { for (unsigned i = 0; i < num_joints; i++) { - if (i > 0) + if (i > 0) out << " "; enode * bare = joints[i]; switch (GET_TAG(bare)) { @@ -307,7 +307,7 @@ namespace smt { } void display_continue(std::ostream & out, const cont & c) { - out << "(CONTINUE " << c.m_label->get_name() << " " << c.m_num_args << " " << c.m_oreg << " " + out << "(CONTINUE " << c.m_label->get_name() << " " << c.m_num_args << " " << c.m_oreg << " " << c.m_lbl_set << " ("; display_joints(out, c.m_num_args, c.m_joints); out << "))"; @@ -317,38 +317,38 @@ namespace smt { out << "(" << op << " " << instr.m_reg << " " << instr.m_lbl_set << ")"; } - + std::ostream & operator<<(std::ostream & out, const instruction & instr) { switch (instr.m_opcode) { - case INIT1: case INIT2: case INIT3: case INIT4: case INIT5: case INIT6: case INITN: + case INIT1: case INIT2: case INIT3: case INIT4: case INIT5: case INIT6: case INITN: out << "(INIT"; - if (instr.m_opcode <= INIT6) + if (instr.m_opcode <= INIT6) out << (instr.m_opcode - INIT1 + 1); else out << "N"; out << ")"; break; - case BIND1: case BIND2: case BIND3: case BIND4: case BIND5: case BIND6: case BINDN: - display_bind(out, static_cast(instr)); + case BIND1: case BIND2: case BIND3: case BIND4: case BIND5: case BIND6: case BINDN: + display_bind(out, static_cast(instr)); break; case GET_CGR1: case GET_CGR2: case GET_CGR3: case GET_CGR4: case GET_CGR5: case GET_CGR6: case GET_CGRN: - display_get_cgr(out, static_cast(instr)); + display_get_cgr(out, static_cast(instr)); break; case IS_CGR: display_is_cgr(out, static_cast(instr)); break; - case YIELD1: case YIELD2: case YIELD3: case YIELD4: case YIELD5: case YIELD6: case YIELDN: - display_yield(out, static_cast(instr)); + case YIELD1: case YIELD2: case YIELD3: case YIELD4: case YIELD5: case YIELD6: case YIELDN: + display_yield(out, static_cast(instr)); break; case CONTINUE: display_continue(out, static_cast(instr)); break; - case COMPARE: - out << "(COMPARE " << static_cast(instr).m_reg1 << " " + case COMPARE: + out << "(COMPARE " << static_cast(instr).m_reg1 << " " << static_cast(instr).m_reg2 << ")"; break; case CHECK: - out << "(CHECK " << static_cast(instr).m_reg + out << "(CHECK " << static_cast(instr).m_reg << " #" << static_cast(instr).m_enode->get_owner_id() << ")"; break; case FILTER: @@ -361,14 +361,14 @@ namespace smt { display_filter(out, "PFILTER", static_cast(instr)); break; case GET_ENODE: - out << "(GET_ENODE " << static_cast(instr).m_oreg << " #" << + out << "(GET_ENODE " << static_cast(instr).m_oreg << " #" << static_cast(instr).m_enode->get_owner_id() << ")"; break; - case CHOOSE: + case CHOOSE: out << "(CHOOSE)"; break; - case NOOP: - out << "(NOOP)"; + case NOOP: + out << "(NOOP)"; break; } #ifdef _PROFILE_MAM @@ -379,7 +379,7 @@ namespace smt { // ------------------------------------ // - // Code Tree + // Code Tree // // ------------------------------------ @@ -404,11 +404,11 @@ namespace smt { unsigned m_num_regs; unsigned m_num_choices; instruction * m_root; - enode_vector m_candidates; + enode_vector m_candidates; #ifdef Z3DEBUG context * m_context; ptr_vector m_patterns; -#endif +#endif #ifdef _PROFILE_MAM stopwatch m_watch; unsigned m_counter; @@ -476,7 +476,7 @@ namespace smt { } } #endif - + public: code_tree(label_hasher & h, func_decl * lbl, unsigned short num_args, bool filter_candidates): m_lbl_hasher(h), @@ -500,8 +500,8 @@ namespace smt { #endif } - stopwatch & get_watch() { - return m_watch; + stopwatch & get_watch() { + return m_watch; } void inc_counter() { @@ -512,7 +512,7 @@ namespace smt { return m_counter; } #endif - + unsigned expected_num_args() const { return m_num_args; } @@ -532,7 +532,7 @@ namespace smt { bool filter_candidates() const { return m_filter_candidates != 0; } - + const instruction * get_root() const { return m_root; } @@ -558,7 +558,7 @@ namespace smt { SASSERT(m_context == 0); m_context = ctx; } - + ptr_vector & get_patterns() { return m_patterns; } @@ -614,7 +614,7 @@ namespace smt { return r; } - instruction * mk_init(unsigned n) { + instruction * mk_init(unsigned n) { SASSERT(n >= 1); opcode op = n <= 6 ? static_cast(INIT1 + n - 1) : INITN; if (op == INITN) { @@ -637,7 +637,7 @@ namespace smt { m_trail_stack(s), m_region(s.get_region()) { } - + code_tree * mk_code_tree(func_decl * lbl, unsigned short num_args, bool filter_candidates) { code_tree * r = alloc(code_tree,m_lbl_hasher, lbl, num_args, filter_candidates); r->m_root = mk_init(num_args); @@ -648,22 +648,22 @@ namespace smt { return new (m_region) joint2(f, pos, reg); } - compare * mk_compare(unsigned reg1, unsigned reg2) { - compare * r = mk_instr(COMPARE, sizeof(compare)); + compare * mk_compare(unsigned reg1, unsigned reg2) { + compare * r = mk_instr(COMPARE, sizeof(compare)); r->m_reg1 = reg1; r->m_reg2 = reg2; return r; } - - check * mk_check(unsigned reg, enode * n) { - check * r = mk_instr(CHECK, sizeof(check)); + + check * mk_check(unsigned reg, enode * n) { + check * r = mk_instr(CHECK, sizeof(check)); r->m_reg = reg; r->m_enode = n; return r; } filter * mk_filter_core(opcode op, unsigned reg, approx_set s) { - filter * r = mk_instr(op, sizeof(filter)); + filter * r = mk_instr(op, sizeof(filter)); r->m_reg = reg; r->m_lbl_set = s; return r; @@ -744,7 +744,7 @@ namespace smt { return y; } - cont * mk_cont(func_decl * lbl, unsigned short num_args, unsigned oreg, + cont * mk_cont(func_decl * lbl, unsigned short num_args, unsigned oreg, approx_set const & s, enode * const * joints) { SASSERT(num_args >= 1); cont * r = mk_instr(CONTINUE, sizeof(cont) + num_args * sizeof(enode*)); @@ -764,11 +764,11 @@ namespace smt { void save_num_regs(code_tree * tree) { m_trail_stack.push(mam_value_trail(tree->m_num_regs)); } - + void save_num_choices(code_tree * tree) { m_trail_stack.push(mam_value_trail(tree->m_num_choices)); } - + void insert_new_lbl_hash(filter * instr, unsigned h) { m_trail_stack.push(mam_value_trail(instr->m_lbl_set)); instr->m_lbl_set.insert(h); @@ -795,18 +795,18 @@ namespace smt { app * m_mp; code_tree * m_tree; unsigned m_num_choices; - bool m_is_tmp_tree; + bool m_is_tmp_tree; svector m_mp_already_processed; obj_map m_matched_exprs; - + struct pcheck_checked { func_decl * m_label; enode * m_enode; }; - - typedef enum { NOT_CHECKED, - CHECK_SET, + + typedef enum { NOT_CHECKED, + CHECK_SET, CHECK_SINGLETON } check_mark; svector m_mark; @@ -827,7 +827,7 @@ namespace smt { void set_check_mark(unsigned reg, check_mark m) { m_mark.setx(reg, m, NOT_CHECKED); } - + void init(code_tree * t, quantifier * qa, app * mp, unsigned first_idx) { SASSERT(m_ast_manager.is_pattern(mp)); #ifdef Z3DEBUG @@ -843,7 +843,7 @@ namespace smt { m_num_choices = 0; m_todo.reset(); m_registers.fill(0); - + app * p = to_app(mp->get_arg(first_idx)); SASSERT(t->get_root_lbl() == p->get_decl()); unsigned num_args = p->get_num_args(); @@ -861,7 +861,7 @@ namespace smt { } /** - \brief Return true if all arguments of n are bound variables. + \brief Return true if all arguments of n are bound variables. That is, during execution time, the variables will be already bound */ bool all_args_are_bound_vars(app * n) { @@ -877,7 +877,7 @@ namespace smt { } /** - \see get_stats + \see get_stats */ void get_stats_core(app * n, unsigned & sz, unsigned & num_unbound_vars) { sz++; @@ -912,7 +912,7 @@ namespace smt { /** \brief Process registers in m_todo. The registers in m_todo that produce non-BIND operations are processed first. Then, - a single BIND operation b is produced. + a single BIND operation b is produced. After executing this method m_todo will contain the registers in m_todo that produce BIND operations and were @@ -942,7 +942,7 @@ namespace smt { m_vars[var_id] = reg; continue; } - + SASSERT(is_app(p)); if (to_app(p)->is_ground()) { @@ -988,7 +988,7 @@ namespace smt { // change the first_app m_aux.push_back(first_app_reg); first_app = to_app(p); - first_app_reg = reg; + first_app_reg = reg; first_app_sz = sz; first_app_num_unbound_vars = num_unbound_vars; } @@ -1000,7 +1000,7 @@ namespace smt { } else { first_app = to_app(p); - first_app_reg = reg; + first_app_reg = reg; get_stats(first_app, first_app_sz, first_app_num_unbound_vars); } } @@ -1069,7 +1069,7 @@ namespace smt { has_unbound_vars = false; return get_num_bound_vars_core(n, has_unbound_vars); } - + /** \brief Compile a pattern where all free variables are already bound. Return the register where the enode congruent to f will be stored. @@ -1141,7 +1141,7 @@ namespace smt { approx_set s; if (m_use_filters) s.insert(m_lbl_hasher(lbl)); - + if (found_bounded_mp) { gen_mp_filter(p); } @@ -1156,17 +1156,17 @@ namespace smt { SASSERT(!is_quantifier(curr)); set_register(oreg + j, curr); m_todo.push_back(oreg + j); - + if ((is_var(curr) && m_vars[to_var(curr)->get_idx()] >= 0) || (is_app(curr) && (to_app(curr)->is_ground()))) has_depth1_joint = true; } - + if (has_depth1_joint) { for (unsigned j = 0; j < num_args; j++) { expr * curr = p->get_arg(j); - + if (is_var(curr)) { unsigned var_id = to_var(curr)->get_idx(); if (m_vars[var_id] >= 0) @@ -1175,15 +1175,15 @@ namespace smt { joints.push_back(NULL_TAG); continue; } - + SASSERT(is_app(curr)); - + if (to_app(curr)->is_ground()) { enode * e = mk_enode(m_context, m_qa, to_app(curr)); joints.push_back(TAG(enode *, e, GROUND_TERM_TAG)); continue; } - + joints.push_back(0); } } @@ -1236,7 +1236,7 @@ namespace smt { m_mp_already_processed[first_idx] = true; linearise_multi_pattern(first_idx); } - + #ifdef Z3DEBUG for (unsigned i = 0; i < m_qa->get_num_decls(); i++) { CTRACE("mam_new_bug", m_vars[i] < 0, tout << mk_ismt2_pp(m_qa, m_ast_manager) << "\ni: " << i << " m_vars[i]: " << m_vars[i] << "\n"; @@ -1248,7 +1248,7 @@ namespace smt { #endif SASSERT(head->m_next == 0); m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, m_qa->get_num_decls(), reinterpret_cast(m_vars.begin()))); - + ptr_vector::iterator it = m_seq.begin(); ptr_vector::iterator end = m_seq.end(); for (; it != end; ++it) { @@ -1268,7 +1268,7 @@ namespace smt { /* The nodes in the bottom of the code-tree can have a lot of children in big examples. Example: - parent-node: + parent-node: (CHOOSE) (CHECK #1 10) (YIELD ...) (CHOOSE) (CHECK #2 10) (YIELD ...) (CHOOSE) (CHECK #3 10) (YIELD ...) @@ -1277,9 +1277,9 @@ namespace smt { (CHOOSE) (CHECK #6 10) (YIELD ...) (CHOOSE) (CHECK #7 10) (YIELD ...) (CHOOSE) (CHECK #8 10) (YIELD ...) - ... + ... The method find_best_child will traverse this big list, and usually will not find - a compatible child. So, I limit the number of simple code sequences that can be + a compatible child. So, I limit the number of simple code sequences that can be traversed. */ #define FIND_BEST_CHILD_THRESHOLD 64 @@ -1305,11 +1305,11 @@ namespace smt { } return best_child; } - + bool is_compatible(bind * instr) const { unsigned ireg = instr->m_ireg; expr * n = m_registers[ireg]; - return + return n != 0 && is_app(n) && // It is wasteful to use a bind of a ground term. @@ -1318,15 +1318,15 @@ namespace smt { to_app(n)->get_decl() == instr->m_label && to_app(n)->get_num_args() == instr->m_num_args; } - + bool is_compatible(compare * instr) const { unsigned reg1 = instr->m_reg1; unsigned reg2 = instr->m_reg2; - return + return m_registers[reg1] != 0 && m_registers[reg1] == m_registers[reg2]; } - + bool is_compatible(check * instr) const { unsigned reg = instr->m_reg; enode * n = instr->m_enode; @@ -1366,25 +1366,25 @@ namespace smt { } /** - \brief We say a check operation is semi compatible if + \brief We say a check operation is semi compatible if it access a register that was not yet processed, and given reg = instr->m_reg 1- is_ground(m_registers[reg]) 2- get_pat_lbl_hash(reg) == m_enode->get_lbl_hash() - + If that is the case, then a CFILTER is created */ bool is_semi_compatible(check * instr) const { unsigned reg = instr->m_reg; - return + return m_registers[reg] != 0 && // if the register was already checked by another filter, then it doesn't make sense // to check it again. - get_check_mark(reg) == NOT_CHECKED && - is_ground(m_registers[reg]) && + get_check_mark(reg) == NOT_CHECKED && + is_ground(m_registers[reg]) && get_pat_lbl_hash(reg) == instr->m_enode->get_lbl_hash(); } - + /** \brief FILTER is not compatible with ground terms anymore. See CFILTER is the filter used for ground terms. @@ -1411,20 +1411,20 @@ namespace smt { } return false; } - + /** \brief See comments at is_semi_compatible(check * instr) and is_compatible(filter * instr). Remark: FILTER is not compatible with ground terms anymore */ bool is_semi_compatible(filter * instr) const { unsigned reg = instr->m_reg; - return + return m_registers[reg] != 0 && get_check_mark(reg) == NOT_CHECKED && is_app(m_registers[reg]) && !is_ground(m_registers[reg]); } - + bool is_compatible(cont * instr) const { unsigned oreg = instr->m_oreg; for (unsigned i = 0; i < instr->m_num_args; i++) @@ -1441,7 +1441,7 @@ namespace smt { many operations in the branch starting at child are compatible with the patterns in the registers stored in m_todo. - Set simple to true, if the tree starting at child is too simple + Set simple to true, if the tree starting at child is too simple (no branching and less than SIMPLE_SEQ_THRESHOLD instructions) */ unsigned get_compatibility_measure(choose * child, bool & simple) { @@ -1453,7 +1453,7 @@ namespace smt { while (curr != 0 && curr->m_opcode != CHOOSE && curr->m_opcode != NOOP) { num_instr++; switch (curr->m_opcode) { - case BIND1: case BIND2: case BIND3: case BIND4: case BIND5: case BIND6: case BINDN: + case BIND1: case BIND2: case BIND3: case BIND4: case BIND5: case BIND6: case BINDN: if (is_compatible(static_cast(curr))) { weight += 4; // the weight of BIND is bigger than COMPARE and CHECK unsigned ireg = static_cast(curr)->m_ireg; @@ -1512,7 +1512,7 @@ namespace smt { while (curr != 0 && curr->m_opcode != CHOOSE && curr->m_opcode != NOOP) { TRACE("mam_compiler_detail", tout << "processing instr: " << *curr << "\n";); switch (curr->m_opcode) { - case BIND1: case BIND2: case BIND3: case BIND4: case BIND5: case BIND6: case BINDN: + case BIND1: case BIND2: case BIND3: case BIND4: case BIND5: case BIND6: case BINDN: if (is_compatible(static_cast(curr))) { TRACE("mam_compiler_detail", tout << "compatible\n";); unsigned ireg = static_cast(curr)->m_ireg; @@ -1613,7 +1613,7 @@ namespace smt { TRACE("mam_compiler_detail", tout << "compatible\n";); unsigned reg = static_cast(curr)->m_reg; CTRACE("mam_compiler_bug", !m_todo.contains(reg), { - for (unsigned i = 0; i < m_todo.size(); i++) { tout << m_todo[i] << " "; } + for (unsigned i = 0; i < m_todo.size(); i++) { tout << m_todo[i] << " "; } tout << "\nregisters:\n"; for (unsigned i = 0; i < m_registers.size(); i++) { if (m_registers[i]) { tout << i << ":\n" << mk_pp(m_registers[i], m_ast_manager) << "\n"; } } tout << "quantifier:\n" << mk_pp(m_qa, m_ast_manager) << "\n"; @@ -1630,7 +1630,7 @@ namespace smt { TRACE("mam_compiler_detail", tout << "semi compatible\n";); unsigned reg = static_cast(curr)->m_reg; CTRACE("mam_compiler_bug", !m_todo.contains(reg), { - for (unsigned i = 0; i < m_todo.size(); i++) { tout << m_todo[i] << " "; } + for (unsigned i = 0; i < m_todo.size(); i++) { tout << m_todo[i] << " "; } tout << "\nregisters:\n"; for (unsigned i = 0; i < m_registers.size(); i++) { if (m_registers[i]) { tout << i << ":\n" << mk_pp(m_registers[i], m_ast_manager) << "\n"; } } tout << "quantifier:\n" << mk_pp(m_qa, m_ast_manager) << "\n"; @@ -1638,7 +1638,7 @@ namespace smt { }); SASSERT(m_todo.contains(reg)); unsigned h = get_pat_lbl_hash(reg); - TRACE("mam_lbl_bug", + TRACE("mam_lbl_bug", tout << "curr_set: " << static_cast(curr)->m_lbl_set << "\n"; tout << "new hash: " << h << "\n";); set_check_mark(reg, CHECK_SET); @@ -1650,7 +1650,7 @@ namespace smt { else { SASSERT(s.size() == 1); approx_set new_s(s); - new_s.insert(h); + new_s.insert(h); filter * new_instr = m_ct_manager.mk_filter(reg, new_s); m_compatible.push_back(new_instr); m_incompatible.push_back(curr); @@ -1669,11 +1669,11 @@ namespace smt { last = curr; curr = curr->m_next; } - + TRACE("mam_compiler", tout << *head << " " << head << "\n"; tout << "m_compatible.size(): " << m_compatible.size() << "\n"; tout << "m_incompatible.size(): " << m_incompatible.size() << "\n";); - + if (m_incompatible.empty()) { // sequence starting at head is fully compatible SASSERT(curr != 0); @@ -1756,19 +1756,19 @@ namespace smt { context & get_context() { return m_context; } - + /** \brief Create a new code tree for the given quantifier. - mp: is a pattern of qa that will be used to create the code tree - + - first_idx: index of mp that will be the "head" (first to be processed) of the multi-pattern. */ code_tree * mk_tree(quantifier * qa, app * mp, unsigned first_idx, bool filter_candidates) { SASSERT(m_ast_manager.is_pattern(mp)); app * p = to_app(mp->get_arg(first_idx)); unsigned num_args = p->get_num_args(); - code_tree * r = m_ct_manager.mk_code_tree(p->get_decl(), num_args, filter_candidates); + code_tree * r = m_ct_manager.mk_code_tree(p->get_decl(), num_args, filter_candidates); init(r, qa, mp, first_idx); linearise(r->m_root, first_idx); r->m_num_choices = m_num_choices; @@ -1795,12 +1795,12 @@ namespace smt { if (!is_tmp_tree) m_ct_manager.save_num_regs(tree); init(tree, qa, mp, first_idx); - m_num_choices = tree->m_num_choices; + m_num_choices = tree->m_num_choices; insert(tree->m_root, first_idx); TRACE("mam_bug", tout << "m_num_choices: " << m_num_choices << "\n";); if (m_num_choices > tree->m_num_choices) { - if (!is_tmp_tree) + if (!is_tmp_tree) m_ct_manager.save_num_choices(tree); tree->m_num_choices = m_num_choices; } @@ -1848,7 +1848,7 @@ namespace smt { }; typedef svector backtrack_stack; - + class interpreter { context & m_context; ast_manager & m_ast_manager; @@ -1893,7 +1893,7 @@ namespace smt { if (m_ast_manager.has_trace_stream()) m_used_enodes.push_back(n); } - + // We have to provide the number of expected arguments because we have flat-assoc applications such as +. // Flat-assoc applications may have arbitrary number of arguments. enode * get_first_f_app(func_decl * lbl, unsigned num_expected_args, enode * curr) { @@ -1950,7 +1950,7 @@ namespace smt { SASSERT(n != 0); do { if (n->get_decl() == f && - n->get_arg(0)->get_root() == m_args[0] && + n->get_arg(0)->get_root() == m_args[0] && n->get_arg(1)->get_root() == m_args[1]) { update_max_generation(n); return true; @@ -2001,7 +2001,7 @@ namespace smt { interpreter(context & ctx, mam & m, bool use_filters): m_context(ctx), m_ast_manager(ctx.get_manager()), - m_mam(m), + m_mam(m), m_use_filters(use_filters) { m_args.resize(INIT_ARGS_SIZE, 0); } @@ -2016,7 +2016,7 @@ namespace smt { if (m_backtrack_stack.size() < t->get_num_choices()) m_backtrack_stack.resize(t->get_num_choices()); } - + void execute(code_tree * t) { TRACE("trigger_bug", tout << "execute for code tree:\n"; t->display(tout);); init(t); @@ -2048,7 +2048,7 @@ namespace smt { } } } - + // init(t) must be invoked before execute_core void execute_core(code_tree * t, enode * n); @@ -2085,9 +2085,9 @@ namespace smt { enode_vector::const_iterator end = n->end_parents(); for (; it != end; ++it) { enode * p = *it; - if (p->get_decl() == f && + if (p->get_decl() == f && m_context.is_relevant(p) && - p->is_cgr() && + p->is_cgr() && p->get_arg(i)->get_root() == n) { v->push_back(p); } @@ -2111,7 +2111,7 @@ namespace smt { enode * p = *it1; if (p->get_decl() == j2->m_decl && m_context.is_relevant(p) && - p->is_cgr() && + p->is_cgr() && p->get_arg(j2->m_arg_pos)->get_root() == n) { // p is in joint2 p = p->get_root(); @@ -2121,7 +2121,7 @@ namespace smt { enode * p2 = *it2; if (p2->get_decl() == f && m_context.is_relevant(p2) && - p2->is_cgr() && + p2->is_cgr() && p2->get_arg(i)->get_root() == p) { v->push_back(p2); } @@ -2153,14 +2153,14 @@ namespace smt { goto non_depth1; } r = n->get_root(); - if (m_use_filters && r->get_plbls().empty_intersection(c->m_lbl_set)) + if (m_use_filters && r->get_plbls().empty_intersection(c->m_lbl_set)) return 0; if (r->get_num_parents() == 0) return 0; non_depth1: ; } - // traverse each joint and select the best one. + // traverse each joint and select the best one. enode_vector * best_v = 0; for (unsigned i = 0; i < num_args; i++) { enode * bare = c->m_joints[i]; @@ -2238,16 +2238,16 @@ namespace smt { out << mk_pp(n->get_owner(), m_ast_manager) << "\n"; } } - + void interpreter::display_instr_input_reg(std::ostream & out, const instruction * instr) { switch (instr->m_opcode) { - case INIT1: case INIT2: case INIT3: case INIT4: case INIT5: case INIT6: case INITN: - display_reg(out, 0); + case INIT1: case INIT2: case INIT3: case INIT4: case INIT5: case INIT6: case INITN: + display_reg(out, 0); break; - case BIND1: case BIND2: case BIND3: case BIND4: case BIND5: case BIND6: case BINDN: + case BIND1: case BIND2: case BIND3: case BIND4: case BIND5: case BIND6: case BINDN: display_reg(out, static_cast(instr)->m_ireg); break; - case COMPARE: + case COMPARE: display_reg(out, static_cast(instr)->m_reg1); display_reg(out, static_cast(instr)->m_reg2); break; @@ -2257,7 +2257,7 @@ namespace smt { case FILTER: display_reg(out, static_cast(instr)->m_reg); break; - case YIELD1: case YIELD2: case YIELD3: case YIELD4: case YIELD5: case YIELD6: case YIELDN: + case YIELD1: case YIELD2: case YIELD3: case YIELD4: case YIELD5: case YIELD6: case YIELDN: for (unsigned i = 0; i < static_cast(instr)->m_num_bindings; i++) { display_reg(out, static_cast(instr)->m_bindings[i]); } @@ -2308,7 +2308,7 @@ namespace smt { m_registers[0] = n; m_top = 0; - + main_loop: TRACE("mam_int", display_pc_info(tout);); @@ -2323,7 +2323,7 @@ namespace smt { m_registers[1] = m_app->get_arg(0); m_pc = m_pc->m_next; goto main_loop; - + case INIT2: m_app = m_registers[0]; if (m_app->get_num_args() != 2) @@ -2332,7 +2332,7 @@ namespace smt { m_registers[2] = m_app->get_arg(1); m_pc = m_pc->m_next; goto main_loop; - + case INIT3: m_app = m_registers[0]; if (m_app->get_num_args() != 3) @@ -2342,7 +2342,7 @@ namespace smt { m_registers[3] = m_app->get_arg(2); m_pc = m_pc->m_next; goto main_loop; - + case INIT4: m_app = m_registers[0]; if (m_app->get_num_args() != 4) @@ -2353,9 +2353,9 @@ namespace smt { m_registers[4] = m_app->get_arg(3); m_pc = m_pc->m_next; goto main_loop; - + case INIT5: - m_app = m_registers[0]; + m_app = m_registers[0]; if (m_app->get_num_args() != 5) goto backtrack; m_registers[1] = m_app->get_arg(0); @@ -2365,8 +2365,8 @@ namespace smt { m_registers[5] = m_app->get_arg(4); m_pc = m_pc->m_next; goto main_loop; - - case INIT6: + + case INIT6: m_app = m_registers[0]; if (m_app->get_num_args() != 6) goto backtrack; @@ -2378,7 +2378,7 @@ namespace smt { m_registers[6] = m_app->get_arg(5); m_pc = m_pc->m_next; goto main_loop; - + case INITN: m_app = m_registers[0]; m_num_args = m_app->get_num_args(); @@ -2388,7 +2388,7 @@ namespace smt { m_registers[i+1] = m_app->get_arg(i); m_pc = m_pc->m_next; goto main_loop; - + case COMPARE: m_n1 = m_registers[static_cast(m_pc)->m_reg1]; m_n2 = m_registers[static_cast(m_pc)->m_reg2]; @@ -2398,7 +2398,7 @@ namespace smt { goto backtrack; m_pc = m_pc->m_next; goto main_loop; - + case CHECK: m_n1 = m_registers[static_cast(m_pc)->m_reg]; m_n2 = static_cast(m_pc)->m_enode; @@ -2413,21 +2413,21 @@ namespace smt { The compiler will never merge two CFILTERs with different m_lbl_set fields. Essentially, CFILTER is used to combine CHECK statements, and FILTER for BIND */ - case CFILTER: + case CFILTER: case FILTER: m_n1 = m_registers[static_cast(m_pc)->m_reg]->get_root(); - if (static_cast(m_pc)->m_lbl_set.empty_intersection(m_n1->get_lbls())) + if (static_cast(m_pc)->m_lbl_set.empty_intersection(m_n1->get_lbls())) goto backtrack; m_pc = m_pc->m_next; goto main_loop; case PFILTER: m_n1 = m_registers[static_cast(m_pc)->m_reg]->get_root(); - if (static_cast(m_pc)->m_lbl_set.empty_intersection(m_n1->get_plbls())) + if (static_cast(m_pc)->m_lbl_set.empty_intersection(m_n1->get_plbls())) goto backtrack; m_pc = m_pc->m_next; goto main_loop; - + case CHOOSE: m_backtrack_stack[m_top].m_instr = m_pc; m_backtrack_stack[m_top].m_old_max_generation = m_max_generation; @@ -2439,7 +2439,7 @@ namespace smt { SASSERT(static_cast(m_pc)->m_alt == 0); m_pc = m_pc->m_next; goto main_loop; - + case BIND1: #define BIND_COMMON() \ m_n1 = m_registers[static_cast(m_pc)->m_ireg]; \ @@ -2456,19 +2456,19 @@ namespace smt { m_backtrack_stack[m_top].m_old_used_enodes_size = m_curr_used_enodes_size; \ m_backtrack_stack[m_top].m_curr = m_app; \ m_top++; - + BIND_COMMON(); m_registers[m_oreg] = m_app->get_arg(0); m_pc = m_pc->m_next; goto main_loop; - + case BIND2: BIND_COMMON(); m_registers[m_oreg] = m_app->get_arg(0); m_registers[m_oreg+1] = m_app->get_arg(1); m_pc = m_pc->m_next; goto main_loop; - + case BIND3: BIND_COMMON(); m_registers[m_oreg] = m_app->get_arg(0); @@ -2476,7 +2476,7 @@ namespace smt { m_registers[m_oreg+2] = m_app->get_arg(2); m_pc = m_pc->m_next; goto main_loop; - + case BIND4: BIND_COMMON(); m_registers[m_oreg] = m_app->get_arg(0); @@ -2485,7 +2485,7 @@ namespace smt { m_registers[m_oreg+3] = m_app->get_arg(3); m_pc = m_pc->m_next; goto main_loop; - + case BIND5: BIND_COMMON(); m_registers[m_oreg] = m_app->get_arg(0); @@ -2495,7 +2495,7 @@ namespace smt { m_registers[m_oreg+4] = m_app->get_arg(4); m_pc = m_pc->m_next; goto main_loop; - + case BIND6: BIND_COMMON(); m_registers[m_oreg] = m_app->get_arg(0); @@ -2506,7 +2506,7 @@ namespace smt { m_registers[m_oreg+5] = m_app->get_arg(5); m_pc = m_pc->m_next; goto main_loop; - + case BINDN: BIND_COMMON(); m_num_args = static_cast(m_pc)->m_num_args; @@ -2529,20 +2529,20 @@ namespace smt { m_max_generation, m_used_enodes) ON_MATCH(1); goto backtrack; - + case YIELD2: m_bindings[0] = m_registers[static_cast(m_pc)->m_bindings[1]]; m_bindings[1] = m_registers[static_cast(m_pc)->m_bindings[0]]; ON_MATCH(2); goto backtrack; - + case YIELD3: m_bindings[0] = m_registers[static_cast(m_pc)->m_bindings[2]]; m_bindings[1] = m_registers[static_cast(m_pc)->m_bindings[1]]; m_bindings[2] = m_registers[static_cast(m_pc)->m_bindings[0]]; ON_MATCH(3); goto backtrack; - + case YIELD4: m_bindings[0] = m_registers[static_cast(m_pc)->m_bindings[3]]; m_bindings[1] = m_registers[static_cast(m_pc)->m_bindings[2]]; @@ -2550,7 +2550,7 @@ namespace smt { m_bindings[3] = m_registers[static_cast(m_pc)->m_bindings[0]]; ON_MATCH(4); goto backtrack; - + case YIELD5: m_bindings[0] = m_registers[static_cast(m_pc)->m_bindings[4]]; m_bindings[1] = m_registers[static_cast(m_pc)->m_bindings[3]]; @@ -2559,7 +2559,7 @@ namespace smt { m_bindings[4] = m_registers[static_cast(m_pc)->m_bindings[0]]; ON_MATCH(5); goto backtrack; - + case YIELD6: m_bindings[0] = m_registers[static_cast(m_pc)->m_bindings[5]]; m_bindings[1] = m_registers[static_cast(m_pc)->m_bindings[4]]; @@ -2569,10 +2569,10 @@ namespace smt { m_bindings[5] = m_registers[static_cast(m_pc)->m_bindings[0]]; ON_MATCH(6); goto backtrack; - + case YIELDN: m_num_args = static_cast(m_pc)->m_num_bindings; - for (unsigned i = 0; i < m_num_args; i++) + for (unsigned i = 0; i < m_num_args; i++) m_bindings[i] = m_registers[static_cast(m_pc)->m_bindings[m_num_args - i - 1]]; ON_MATCH(m_num_args); goto backtrack; @@ -2590,7 +2590,7 @@ namespace smt { m_registers[static_cast(m_pc)->m_oreg] = m_n1; \ m_pc = m_pc->m_next; \ goto main_loop; - + #define SET_VAR(IDX) \ m_args[IDX] = m_registers[static_cast(m_pc)->m_iregs[IDX]]; \ if (m_use_filters && static_cast(m_pc)->m_lbl_set.empty_intersection(m_args[IDX]->get_root()->get_plbls())) { \ @@ -2599,7 +2599,7 @@ namespace smt { tout << "node set: "; m_args[IDX]->get_root()->get_plbls().display(tout); tout << "\n";); \ goto backtrack; \ } - + SET_VAR(0); GET_CGR_COMMON(); @@ -2644,11 +2644,11 @@ namespace smt { for (unsigned i = 0; i < m_num_args; i++) m_args[i] = m_registers[static_cast(m_pc)->m_iregs[i]]; GET_CGR_COMMON(); - + case IS_CGR: - if (!exec_is_cgr(static_cast(m_pc))) - goto backtrack; - m_pc = m_pc->m_next; + if (!exec_is_cgr(static_cast(m_pc))) + goto backtrack; + m_pc = m_pc->m_next; goto main_loop; case CONTINUE: @@ -2659,13 +2659,13 @@ namespace smt { goto backtrack; m_pattern_instances.push_back(m_app); TRACE("mam_int", tout << "continue candidate:\n" << mk_ll_pp(m_app->get_owner(), m_ast_manager);); - for (unsigned i = 0; i < m_num_args; i++) + for (unsigned i = 0; i < m_num_args; i++) m_registers[m_oreg+i] = m_app->get_arg(i); m_pc = m_pc->m_next; goto main_loop; } - + backtrack: TRACE("mam_int", tout << "backtracking.\n";); if (m_top == 0) { @@ -2723,19 +2723,19 @@ namespace smt { bp.m_curr = m_app; \ TRACE("mam_int", tout << "bind next candidate:\n" << mk_ll_pp(m_app->get_owner(), m_ast_manager);); \ m_oreg = m_b->m_oreg - + BBIND_COMMON(); m_registers[m_oreg] = m_app->get_arg(0); m_pc = m_b->m_next; goto main_loop; - + case BIND2: BBIND_COMMON(); m_registers[m_oreg] = m_app->get_arg(0); m_registers[m_oreg+1] = m_app->get_arg(1); m_pc = m_b->m_next; goto main_loop; - + case BIND3: BBIND_COMMON(); m_registers[m_oreg] = m_app->get_arg(0); @@ -2743,7 +2743,7 @@ namespace smt { m_registers[m_oreg+2] = m_app->get_arg(2); m_pc = m_b->m_next; goto main_loop; - + case BIND4: BBIND_COMMON(); m_registers[m_oreg] = m_app->get_arg(0); @@ -2752,7 +2752,7 @@ namespace smt { m_registers[m_oreg+3] = m_app->get_arg(3); m_pc = m_b->m_next; goto main_loop; - + case BIND5: BBIND_COMMON(); m_registers[m_oreg] = m_app->get_arg(0); @@ -2762,7 +2762,7 @@ namespace smt { m_registers[m_oreg+4] = m_app->get_arg(4); m_pc = m_b->m_next; goto main_loop; - + case BIND6: BBIND_COMMON(); m_registers[m_oreg] = m_app->get_arg(0); @@ -2773,7 +2773,7 @@ namespace smt { m_registers[m_oreg+5] = m_app->get_arg(5); m_pc = m_b->m_next; goto main_loop; - + case BINDN: BBIND_COMMON(); m_num_args = m_b->m_num_args; @@ -2781,7 +2781,7 @@ namespace smt { m_registers[m_oreg+i] = m_app->get_arg(i); m_pc = m_b->m_next; goto main_loop; - + case CONTINUE: ++bp.m_it; for (; bp.m_it != bp.m_end; ++bp.m_it) { @@ -2815,7 +2815,7 @@ namespace smt { recycle_enode_vector(bp.m_to_recycle); m_top--; goto backtrack; - + default: UNREACHABLE(); } @@ -2835,8 +2835,8 @@ namespace smt { } // ------------------------------------ - // - // A mapping from func_label -> code tree. + // + // A mapping from func_label -> code tree. // // ------------------------------------ class code_tree_map { @@ -2858,7 +2858,7 @@ namespace smt { m_trees[m_lbl_id] = 0; } }; - + public: code_tree_map(ast_manager & m, compiler & c, mam_trail_stack & s): m_ast_manager(m), @@ -2876,9 +2876,9 @@ namespace smt { /** \brief Add a pattern to the code tree map. - + - mp: is used a pattern for qa. - + - first_idx: index to be used as head of the multi-pattern mp */ void add_pattern(quantifier * qa, app * mp, unsigned first_idx) { @@ -2933,11 +2933,11 @@ namespace smt { }; // ------------------------------------ - // + // // Path trees AKA inverted path index // // ------------------------------------ - + /** \brief Temporary object used to encode a path of the form: @@ -2948,7 +2948,7 @@ namespace smt { parents p_0 of n that are f-applications, and n is the second argument, then for each such p_0, I want to follow the parents p_1 of p_0 that are g-applications, and p_0 is the third argument. Finally, I want to - follow the p_2 parents of p_1 that are h-applications and p_1 is the + follow the p_2 parents of p_1 that are h-applications and p_1 is the first argument of p_2. To improve the filtering power of the inverse path index, I'm also @@ -2961,11 +2961,11 @@ namespace smt { The idea is that I want only the f-parents s.t. the third argument is equal to t. */ struct path { - func_decl * m_label; + func_decl * m_label; unsigned short m_arg_idx; unsigned short m_ground_arg_idx; enode * m_ground_arg; - unsigned m_pattern_idx; + unsigned m_pattern_idx; path * m_child; path (func_decl * lbl, unsigned short arg_idx, unsigned short ground_arg_idx, enode * ground_arg, unsigned pat_idx, path * child): m_label(lbl), @@ -2977,7 +2977,7 @@ namespace smt { SASSERT(ground_arg != 0 || ground_arg_idx == 0); } }; - + bool is_equal(path const * p1, path const * p2) { for (;;) { if (p1->m_label != p2->m_label || @@ -2986,15 +2986,15 @@ namespace smt { (p1->m_child == 0) != (p2->m_child == 0)) { return false; } - + if (p1->m_child == 0 && p2->m_child == 0) return true; - + p1 = p1->m_child; p2 = p2->m_child; } } - + typedef ptr_vector paths; /** @@ -3009,7 +3009,7 @@ namespace smt { approx_set m_filter; path_tree * m_sibling; path_tree * m_first_child; - enode_vector * m_todo; // temporary field used to collect candidates + enode_vector * m_todo; // temporary field used to collect candidates #ifdef _PROFILE_PATH_TREE stopwatch m_watch; unsigned m_counter; @@ -3017,7 +3017,7 @@ namespace smt { unsigned m_num_neq_visited; bool m_already_displayed; //!< true if the path_tree was already displayed after reaching _PROFILE_PATH_TREE_THRESHOLD #endif - + path_tree(path * p, label_hasher & h): m_label(p->m_label), m_arg_idx(p->m_arg_idx), @@ -3047,7 +3047,7 @@ namespace smt { #ifdef _PROFILE_PATH_TREE out << ", counter: " << m_counter << ", num_eq_visited: " << m_num_eq_visited << ", num_neq_visited: " << m_num_neq_visited << ", avg. : " << static_cast(m_num_neq_visited)/static_cast(m_num_neq_visited+m_num_eq_visited); -#endif +#endif out << "\n"; curr->m_first_child->display(out, indent+1); curr = curr->m_sibling; @@ -3058,7 +3058,7 @@ namespace smt { typedef std::pair path_tree_pair; // ------------------------------------ - // + // // Matching Abstract Machine Implementation // // ------------------------------------ @@ -3071,8 +3071,8 @@ namespace smt { code_tree_manager m_ct_manager; compiler m_compiler; interpreter m_interpreter; - code_tree_map m_trees; - + code_tree_map m_trees; + ptr_vector m_tmp_trees; ptr_vector m_tmp_trees_to_delete; ptr_vector m_to_match; @@ -3088,11 +3088,11 @@ namespace smt { // auxiliary field used to update data-structures... typedef ptr_vector func_decls; - vector m_var_parent_labels; + vector m_var_parent_labels; region & m_region; region m_tmp_region; - path_tree_pair m_pp[APPROX_SET_CAPACITY][APPROX_SET_CAPACITY]; + path_tree_pair m_pp[APPROX_SET_CAPACITY][APPROX_SET_CAPACITY]; path_tree * m_pc[APPROX_SET_CAPACITY][APPROX_SET_CAPACITY]; pool m_pool; @@ -3105,7 +3105,7 @@ namespace smt { enode * m_r1; // temp field enode * m_r2; // temp field - + class add_shared_enode_trail; friend class add_shared_enode_trail; @@ -3125,7 +3125,7 @@ namespace smt { r->reset(); return r; } - + void recycle(enode_vector * v) { m_pool.recycle(v); } @@ -3133,12 +3133,12 @@ namespace smt { void add_candidate(code_tree * t, enode * app) { if (t != 0) { TRACE("mam_candidate", tout << "adding candidate:\n" << mk_ll_pp(app->get_owner(), m_ast_manager);); - if (!t->has_candidates()) + if (!t->has_candidates()) m_to_match.push_back(t); t->add_candidate(app); } } - + void add_candidate(enode * app) { func_decl * lbl = app->get_decl(); add_candidate(m_trees.get_code_tree_for(lbl), app); @@ -3152,7 +3152,7 @@ namespace smt { unsigned lbl_id = lbl->get_decl_id(); return lbl_id < m_is_clbl.size() && m_is_clbl[lbl_id]; } - + void update_lbls(enode * n, unsigned elem) { approx_set & r_lbls = n->get_root()->get_lbls(); if (!r_lbls.may_contain(elem)) { @@ -3203,14 +3203,14 @@ namespace smt { } } } - + void update_plbls(func_decl * lbl) { unsigned lbl_id = lbl->get_decl_id(); m_is_plbl.reserve(lbl_id+1, false); TRACE("trigger_bug", tout << "update_plbls: " << lbl->get_name() << " is already plbl: " << m_is_plbl[lbl_id] << ", lbl_id: " << lbl_id << "\n"; tout << "mam: " << this << "\n";); TRACE("mam_bug", tout << "update_plbls: " << lbl->get_name() << " is already plbl: " << m_is_plbl[lbl_id] << "\n";); - if (m_is_plbl[lbl_id]) + if (m_is_plbl[lbl_id]) return; m_trail_stack.push(set_bitvector_trail(m_is_plbl, lbl_id)); SASSERT(m_is_plbl[lbl_id]); @@ -3220,7 +3220,7 @@ namespace smt { enode_vector::const_iterator end = m_context.end_enodes_of(lbl); for (; it != end; ++it) { enode * app = *it; - if (m_context.is_relevant(app)) + if (m_context.is_relevant(app)) update_children_plbls(app, h); } } @@ -3234,12 +3234,12 @@ namespace smt { } } } - + code_tree * mk_code(quantifier * qa, app * mp, unsigned pat_idx) { SASSERT(m_ast_manager.is_pattern(mp)); - return m_compiler.mk_tree(qa, mp, pat_idx, true); + return m_compiler.mk_tree(qa, mp, pat_idx, true); } - + void insert_code(path_tree * t, quantifier * qa, app * mp, unsigned pat_idx) { SASSERT(m_ast_manager.is_pattern(mp)); m_compiler.insert(t->m_code, qa, mp, pat_idx, false); @@ -3254,7 +3254,7 @@ namespace smt { path_tree * prev = 0; while (p != 0) { curr = new (m_region) path_tree(p, m_lbl_hasher); - if (prev) + if (prev) prev->m_first_child = curr; if (!head) head = curr; @@ -3274,7 +3274,7 @@ namespace smt { while (t != 0) { if (t->m_label == p->m_label) { found_label = true; - if (t->m_arg_idx == p->m_arg_idx && + if (t->m_arg_idx == p->m_arg_idx && t->m_ground_arg == p->m_ground_arg && t->m_ground_arg_idx == p->m_ground_arg_idx ) { @@ -3326,7 +3326,7 @@ namespace smt { m_trail_stack.push(set_ptr_trail(m_pc[h1][h2])); m_pc[h1][h2] = mk_path_tree(p, qa, mp); } - TRACE("mam_path_tree_updt", + TRACE("mam_path_tree_updt", tout << "updated path tree:\n"; m_pc[h1][h2]->display(tout, 2);); } @@ -3343,7 +3343,7 @@ namespace smt { m_trail_stack.push(set_ptr_trail(m_pp[h1][h2].first)); m_pp[h1][h2].first = mk_path_tree(p1, qa, mp); insert(m_pp[h1][h2].first, p2, qa, mp); - } + } } else { if (h1 > h2) { @@ -3364,7 +3364,7 @@ namespace smt { m_pp[h1][h2].second = mk_path_tree(p2, qa, mp); } } - TRACE("mam_path_tree_updt", + TRACE("mam_path_tree_updt", tout << "updated path tree:\n"; SASSERT(h1 <= h2); m_pp[h1][h2].first->display(tout, 2); @@ -3418,28 +3418,28 @@ namespace smt { for (unsigned short i = 0; i < num_args; i++) { expr * child = pat->get_arg(i); path * new_path = new (m_tmp_region) path(plbl, i, ground_arg_pos, ground_arg, pat_idx, p); - + if (is_var(child)) { update_vars(to_var(child)->get_idx(), new_path, qa, mp); continue; } SASSERT(is_app(child)); - + if (to_app(child)->is_ground()) { enode * n = mk_enode(m_context, qa, to_app(child)); update_plbls(plbl); if (!n->has_lbl_hash()) n->set_lbl_hash(m_context); - TRACE("mam_bug", - tout << "updating pc labels " << plbl->get_name() << " " << + TRACE("mam_bug", + tout << "updating pc labels " << plbl->get_name() << " " << static_cast(n->get_lbl_hash()) << "\n"; tout << "#" << n->get_owner_id() << " " << n->get_root()->get_lbls() << "\n"; tout << "relevant: " << m_context.is_relevant(n) << "\n";); update_pc(m_lbl_hasher(plbl), n->get_lbl_hash(), new_path, qa, mp); continue; } - + func_decl * clbl = to_app(child)->get_decl(); TRACE("mam_bug", tout << "updating pc labels " << plbl->get_name() << " " << clbl->get_name() << "\n";); update_plbls(plbl); @@ -3468,7 +3468,7 @@ namespace smt { // (p_n, p_2, ..., p_1) unsigned num_patterns = mp->get_num_args(); for (unsigned i = 0; i < num_patterns; i++) { - app * pat = to_app(mp->get_arg(i)); + app * pat = to_app(mp->get_arg(i)); update_filters(pat, 0, qa, mp, i); } } @@ -3495,7 +3495,7 @@ namespace smt { \brief Check equality modulo the equality m_r1 = m_r2 */ bool is_eq(enode * n1, enode * n2) { - return + return n1->get_root() == n2->get_root() || (n1->get_root() == m_r1 && n2->get_root() == m_r2) || (n2->get_root() == m_r1 && n1->get_root() == m_r2); @@ -3524,7 +3524,7 @@ namespace smt { #ifdef _PROFILE_PATH_TREE t->m_counter++; #endif - TRACE("mam_path_tree", + TRACE("mam_path_tree", tout << "processing:\n"; t->display(tout, 2);); enode_vector * v = t->m_todo; @@ -3552,13 +3552,13 @@ namespace smt { // // In a previous version of Z3, the "enode mark field" was used to mark both cases. This is incorrect, // and Z3 may fail to find potential new matches. - // + // // The file regression\acu.sx exposed this problem. enode * curr_child = (*it1)->get_root(); - + if (m_use_filters && curr_child->get_plbls().empty_intersection(filter)) continue; - + #ifdef _PROFILE_PATH_TREE static unsigned counter2 = 0; static unsigned total_sz2 = 0; @@ -3571,7 +3571,7 @@ namespace smt { std::cout << "Avg2. " << static_cast(total_sz2)/static_cast(counter2) << ", Max2. " << max_sz2 << "\n"; #endif - TRACE("mam_path_tree", tout << "processing: #" << curr_child->get_owner_id() << "\n";); + TRACE("mam_path_tree", tout << "processing: #" << curr_child->get_owner_id() << "\n";); enode_vector::const_iterator it2 = curr_child->begin_parents(); enode_vector::const_iterator end2 = curr_child->end_parents(); for (; it2 != end2; ++it2) { @@ -3594,7 +3594,7 @@ namespace smt { if (filter.may_contain(m_lbl_hasher(lbl)) && !curr_parent->is_marked() && (curr_parent_cg == curr_parent || !is_eq(curr_parent_cg, curr_parent_root)) && - m_context.is_relevant(curr_parent) + m_context.is_relevant(curr_parent) ) { path_tree * curr_tree = t; while (curr_tree) { @@ -3693,14 +3693,14 @@ namespace smt { } if (n_plbl1 == n_plbl2) { SASSERT(m_pp[n_plbl1][n_plbl2].second == 0); - if (n_r1->get_num_parents() <= n_r2->get_num_parents()) + if (n_r1->get_num_parents() <= n_r2->get_num_parents()) collect_parents(n_r1, m_pp[n_plbl1][n_plbl2].first); else collect_parents(n_r2, m_pp[n_plbl1][n_plbl2].first); } else { SASSERT(n_plbl1 < n_plbl2); - if (n_r1->get_num_parents() <= n_r2->get_num_parents()) + if (n_r1->get_num_parents() <= n_r2->get_num_parents()) collect_parents(n_r1, m_pp[n_plbl1][n_plbl2].first); else collect_parents(n_r2, m_pp[n_plbl1][n_plbl2].second); @@ -3773,7 +3773,7 @@ namespace smt { enode_vector::const_iterator end3 = m_context.end_enodes_of(lbl); for (; it3 != end3; ++it3) { enode * app = *it3; - if (m_context.is_relevant(app)) + if (m_context.is_relevant(app)) m_interpreter.execute_core(tmp_tree, app); } m_tmp_trees[lbl_id] = 0; @@ -3786,7 +3786,7 @@ namespace smt { ptr_buffer todo; unsigned num_patterns = mp->get_num_args(); for (unsigned i = 0; i < num_patterns; i++) { - app * pat = to_app(mp->get_arg(i)); + app * pat = to_app(mp->get_arg(i)); TRACE("mam_pat", tout << mk_ismt2_pp(qa, m_ast_manager) << "\npat:\n" << mk_ismt2_pp(pat, m_ast_manager) << "\n";); SASSERT(!pat->is_ground()); todo.push_back(pat); @@ -3812,7 +3812,7 @@ namespace smt { public: mam_impl(context & ctx, bool use_filters): - mam(ctx), + mam(ctx), m_ast_manager(ctx.get_manager()), m_use_filters(use_filters), m_trail_stack(*this), @@ -3827,7 +3827,7 @@ namespace smt { DEBUG_CODE(m_check_missing_instances = false;); reset_pp_pc(); } - + virtual ~mam_impl() { m_trail_stack.reset(); } @@ -3854,11 +3854,11 @@ namespace smt { for (unsigned i = 0; i < num_patterns; i++) m_trees.add_pattern(qa, mp, i); } - + virtual void push_scope() { m_trail_stack.push_scope(); } - + virtual void pop_scope(unsigned num_scopes) { if (!m_to_match.empty()) { ptr_vector::iterator it = m_to_match.begin(); @@ -3894,8 +3894,8 @@ namespace smt { (*it)->display(out); } } - - virtual void match() { + + virtual void match() { TRACE("trigger_bug", tout << "match\n"; display(tout);); ptr_vector::iterator it = m_to_match.begin(); ptr_vector::iterator end = m_to_match.end(); @@ -3925,7 +3925,7 @@ namespace smt { enode_vector::const_iterator end2 = m_context.end_enodes_of(lbl); for (; it2 != end2; ++it2) { enode * curr = *it2; - if (use_irrelevant || m_context.is_relevant(curr)) + if (use_irrelevant || m_context.is_relevant(curr)) m_interpreter.execute_core(t, curr); } } @@ -3940,13 +3940,13 @@ namespace smt { return true; } #endif - + virtual void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, ptr_vector & used_enodes) { TRACE("trigger_bug", tout << "found match " << mk_pp(qa, m_ast_manager) << "\n";); #ifdef Z3DEBUG if (m_check_missing_instances) { if (!m_context.slow_contains_instance(qa, num_bindings, bindings)) { - TRACE("missing_instance", + TRACE("missing_instance", tout << "qa:\n" << mk_ll_pp(qa, m_ast_manager) << "\npat:\n" << mk_ll_pp(pat, m_ast_manager); for (unsigned i = 0; i < num_bindings; i++) tout << "#" << bindings[i]->get_owner_id() << "\n" << mk_ll_pp(bindings[i]->get_owner(), m_ast_manager) << "\n"; @@ -3967,23 +3967,23 @@ namespace smt { virtual bool is_shared(enode * n) const { return !m_shared_enodes.empty() && m_shared_enodes.contains(n); } - + // This method is invoked when n becomes relevant. // If lazy == true, then n is not added to the list of candidate enodes for matching. That is, the method just updates the lbls. virtual void relevant_eh(enode * n, bool lazy) { TRACE("trigger_bug", tout << "relevant_eh:\n" << mk_ismt2_pp(n->get_owner(), m_ast_manager) << "\n"; tout << "mam: " << this << "\n";); TRACE("mam", tout << "relevant_eh: #" << n->get_owner_id() << "\n";); - if (n->has_lbl_hash()) + if (n->has_lbl_hash()) update_lbls(n, n->get_lbl_hash()); - + if (n->get_num_args() > 0) { func_decl * lbl = n->get_decl(); unsigned h = m_lbl_hasher(lbl); - TRACE("trigger_bug", tout << "lbl: " << lbl->get_name() << " is_clbl(lbl): " << is_clbl(lbl) + TRACE("trigger_bug", tout << "lbl: " << lbl->get_name() << " is_clbl(lbl): " << is_clbl(lbl) << ", is_plbl(lbl): " << is_plbl(lbl) << ", h: " << h << "\n"; tout << "lbl_id: " << lbl->get_decl_id() << "\n";); - if (is_clbl(lbl)) + if (is_clbl(lbl)) update_lbls(n, h); if (is_plbl(lbl)) update_children_plbls(n, h); @@ -4002,28 +4002,28 @@ namespace smt { flet l2(m_r2, r2); TRACE("mam", tout << "add_eq_eh: #" << r1->get_owner_id() << " #" << r2->get_owner_id() << "\n";); - TRACE("mam_inc_bug_detail", m_context.display(tout);); - TRACE("mam_inc_bug", + TRACE("mam_inc_bug_detail", m_context.display(tout);); + TRACE("mam_inc_bug", tout << "before:\n#" << r1->get_owner_id() << " #" << r2->get_owner_id() << "\n"; tout << "r1.lbls: " << r1->get_lbls() << "\n"; tout << "r2.lbls: " << r2->get_lbls() << "\n"; tout << "r1.plbls: " << r1->get_plbls() << "\n"; tout << "r2.plbls: " << r2->get_plbls() << "\n";); - + process_pc(r1, r2); process_pc(r2, r1); process_pp(r1, r2); - + approx_set r1_plbls = r1->get_plbls(); approx_set & r2_plbls = r2->get_plbls(); approx_set r1_lbls = r1->get_lbls(); approx_set & r2_lbls = r2->get_lbls(); - + m_trail_stack.push(mam_value_trail(r2_lbls)); m_trail_stack.push(mam_value_trail(r2_plbls)); r2_lbls |= r1_lbls; - r2_plbls |= r1_plbls; - TRACE("mam_inc_bug", + r2_plbls |= r1_plbls; + TRACE("mam_inc_bug", tout << "after:\n"; tout << "r1.lbls: " << r1->get_lbls() << "\n"; tout << "r2.lbls: " << r2->get_lbls() << "\n"; From b2d590e0c9a5a11b955a7faea461bc45b688ce58 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 17 Aug 2017 16:00:59 +0100 Subject: [PATCH 2/8] Bugfix for MAM. Fixes #1213. Partially addresses #1212. --- src/smt/mam.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 1fc5ed220..19ccfbe98 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -2088,6 +2088,7 @@ namespace smt { if (p->get_decl() == f && m_context.is_relevant(p) && p->is_cgr() && + i < p->get_num_args() && p->get_arg(i)->get_root() == n) { v->push_back(p); } From 1620796bd1dfc6876c5f096593cda32fb4400baa Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 17 Aug 2017 17:25:04 +0100 Subject: [PATCH 3/8] 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 4/8] 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 5/8] 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 6/8] [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 7/8] 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 8/8] 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();