diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index c4a4da00c..46fe5bd6d 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1964,7 +1964,7 @@ struct let from_file (x:optimize) (s:string) = Z3native.optimize_from_file (gc x) x s let from_string (x:optimize) (s:string) = Z3native.optimize_from_string (gc x) x s let get_assertions (x:optimize) = AST.ASTVector.to_expr_list (Z3native.optimize_get_assertions (gc x) x) - let get_objectives (x:optimize) = AST.ASTVector.to_expr_list (Z3native.optimize_get_statistics (gc x) x) + let get_objectives (x:optimize) = AST.ASTVector.to_expr_list (Z3native.optimize_get_objectives (gc x) x) end diff --git a/src/ast/macros/macro_finder.cpp b/src/ast/macros/macro_finder.cpp index 9a8e552fc..ed067f331 100644 --- a/src/ast/macros/macro_finder.cpp +++ b/src/ast/macros/macro_finder.cpp @@ -25,89 +25,94 @@ Revision History: bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) { if (!is_quantifier(n) || !to_quantifier(n)->is_forall()) return false; - TRACE("macro_finder", tout << "processing: " << mk_pp(n, m_manager) << "\n";); + TRACE("macro_finder", tout << "processing: " << mk_pp(n, m) << "\n";); expr * body = to_quantifier(n)->get_expr(); unsigned num_decls = to_quantifier(n)->get_num_decls(); return m_util.is_simple_macro(body, num_decls, head, def); } /** - \brief Detect macros of the form + \brief Detect macros of the form 1- (forall (X) (= (+ (f X) (R X)) c)) 2- (forall (X) (<= (+ (f X) (R X)) c)) 3- (forall (X) (>= (+ (f X) (R X)) c)) The second and third cases are first converted into (forall (X) (= (f X) (+ c (* -1 (R x)) (k X)))) - and + and (forall (X) (<= (k X) 0)) when case 2 (forall (X) (>= (k X) 0)) when case 3 For case 2 & 3, the new quantifiers are stored in new_exprs and new_prs. */ -bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) { +bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_dependency * dep, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) { if (!is_quantifier(n) || !to_quantifier(n)->is_forall()) return false; expr * body = to_quantifier(n)->get_expr(); unsigned num_decls = to_quantifier(n)->get_num_decls(); - if (!m_autil.is_le(body) && !m_autil.is_ge(body) && !m_manager.is_eq(body)) + if (!m_autil.is_le(body) && !m_autil.is_ge(body) && !m.is_eq(body)) return false; if (!m_autil.is_add(to_app(body)->get_arg(0))) return false; - app_ref head(m_manager); - expr_ref def(m_manager); + app_ref head(m); + expr_ref def(m); bool inv = false; if (!m_util.is_arith_macro(body, num_decls, head, def, inv)) return false; - app_ref new_body(m_manager); - - if (!inv || m_manager.is_eq(body)) - new_body = m_manager.mk_app(to_app(body)->get_decl(), head, def); + app_ref new_body(m); + + if (!inv || m.is_eq(body)) + new_body = m.mk_app(to_app(body)->get_decl(), head, def); else if (m_autil.is_le(body)) new_body = m_autil.mk_ge(head, def); else new_body = m_autil.mk_le(head, def); - quantifier_ref new_q(m_manager); - new_q = m_manager.update_quantifier(to_quantifier(n), new_body); + quantifier_ref new_q(m); + new_q = m.update_quantifier(to_quantifier(n), new_body); proof * new_pr = 0; - if (m_manager.proofs_enabled()) { - proof * rw = m_manager.mk_rewrite(n, new_q); - new_pr = m_manager.mk_modus_ponens(pr, rw); + if (m.proofs_enabled()) { + proof * rw = m.mk_rewrite(n, new_q); + new_pr = m.mk_modus_ponens(pr, rw); } - if (m_manager.is_eq(body)) { - return m_macro_manager.insert(head->get_decl(), new_q, new_pr); + expr_dependency * new_dep = dep; + if (m.is_eq(body)) { + return m_macro_manager.insert(head->get_decl(), new_q, new_pr, new_dep); } // is ge or le - // + // TRACE("macro_finder", tout << "is_arith_macro: is_ge or is_le\n";); func_decl * f = head->get_decl(); - func_decl * k = m_manager.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range()); - app * k_app = m_manager.mk_app(k, head->get_num_args(), head->get_args()); - expr_ref_buffer new_rhs_args(m_manager); - expr_ref new_rhs2(m_autil.mk_add(def, k_app), m_manager); - expr * body1 = m_manager.mk_eq(head, new_rhs2); - expr * body2 = m_manager.mk_app(new_body->get_decl(), k_app, m_autil.mk_int(0)); - quantifier * q1 = m_manager.update_quantifier(new_q, body1); - expr * patterns[1] = { m_manager.mk_pattern(k_app) }; - quantifier * q2 = m_manager.update_quantifier(new_q, 1, patterns, body2); + func_decl * k = m.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range()); + app * k_app = m.mk_app(k, head->get_num_args(), head->get_args()); + expr_ref_buffer new_rhs_args(m); + expr_ref new_rhs2(m_autil.mk_add(def, k_app), m); + expr * body1 = m.mk_eq(head, new_rhs2); + expr * body2 = m.mk_app(new_body->get_decl(), k_app, m_autil.mk_int(0)); + quantifier * q1 = m.update_quantifier(new_q, body1); + expr * patterns[1] = { m.mk_pattern(k_app) }; + quantifier * q2 = m.update_quantifier(new_q, 1, patterns, body2); new_exprs.push_back(q1); new_exprs.push_back(q2); - if (m_manager.proofs_enabled()) { + if (m.proofs_enabled()) { // new_pr : new_q // rw : [rewrite] new_q ~ q1 & q2 // mp : [modus_pones new_pr rw] q1 & q2 // pr1 : [and-elim mp] q1 // pr2 : [and-elim mp] q2 - app * q1q2 = m_manager.mk_and(q1,q2); - proof * rw = m_manager.mk_oeq_rewrite(new_q, q1q2); - proof * mp = m_manager.mk_modus_ponens(new_pr, rw); - proof * pr1 = m_manager.mk_and_elim(mp, 0); - proof * pr2 = m_manager.mk_and_elim(mp, 1); + app * q1q2 = m.mk_and(q1,q2); + proof * rw = m.mk_oeq_rewrite(new_q, q1q2); + proof * mp = m.mk_modus_ponens(new_pr, rw); + proof * pr1 = m.mk_and_elim(mp, 0); + proof * pr2 = m.mk_and_elim(mp, 1); new_prs.push_back(pr1); new_prs.push_back(pr2); } + if (dep) { + new_deps.push_back(new_dep); + new_deps.push_back(new_dep); + } return true; } @@ -117,62 +122,62 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, vector& expr * body = to_quantifier(n)->get_expr(); unsigned num_decls = to_quantifier(n)->get_num_decls(); - if (!m_autil.is_le(body) && !m_autil.is_ge(body) && !m_manager.is_eq(body)) + if (!m_autil.is_le(body) && !m_autil.is_ge(body) && !m.is_eq(body)) return false; if (!m_autil.is_add(to_app(body)->get_arg(0))) return false; - app_ref head(m_manager); - expr_ref def(m_manager); + app_ref head(m); + expr_ref def(m); bool inv = false; if (!m_util.is_arith_macro(body, num_decls, head, def, inv)) return false; - app_ref new_body(m_manager); + app_ref new_body(m); - if (!inv || m_manager.is_eq(body)) - new_body = m_manager.mk_app(to_app(body)->get_decl(), head, def); + if (!inv || m.is_eq(body)) + new_body = m.mk_app(to_app(body)->get_decl(), head, def); else if (m_autil.is_le(body)) new_body = m_autil.mk_ge(head, def); else new_body = m_autil.mk_le(head, def); - quantifier_ref new_q(m_manager); - new_q = m_manager.update_quantifier(to_quantifier(n), new_body); + quantifier_ref new_q(m); + new_q = m.update_quantifier(to_quantifier(n), new_body); proof * new_pr = 0; - if (m_manager.proofs_enabled()) { - proof * rw = m_manager.mk_rewrite(n, new_q); - new_pr = m_manager.mk_modus_ponens(pr, rw); + if (m.proofs_enabled()) { + proof * rw = m.mk_rewrite(n, new_q); + new_pr = m.mk_modus_ponens(pr, rw); } - if (m_manager.is_eq(body)) { + if (m.is_eq(body)) { return m_macro_manager.insert(head->get_decl(), new_q, new_pr); } // is ge or le // TRACE("macro_finder", tout << "is_arith_macro: is_ge or is_le\n";); func_decl * f = head->get_decl(); - func_decl * k = m_manager.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range()); - app * k_app = m_manager.mk_app(k, head->get_num_args(), head->get_args()); - expr_ref_buffer new_rhs_args(m_manager); - expr_ref new_rhs2(m_autil.mk_add(def, k_app), m_manager); - expr * body1 = m_manager.mk_eq(head, new_rhs2); - expr * body2 = m_manager.mk_app(new_body->get_decl(), k_app, m_autil.mk_int(0)); - quantifier * q1 = m_manager.update_quantifier(new_q, body1); - expr * patterns[1] = { m_manager.mk_pattern(k_app) }; - quantifier * q2 = m_manager.update_quantifier(new_q, 1, patterns, body2); + func_decl * k = m.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range()); + app * k_app = m.mk_app(k, head->get_num_args(), head->get_args()); + expr_ref_buffer new_rhs_args(m); + expr_ref new_rhs2(m_autil.mk_add(def, k_app), m); + expr * body1 = m.mk_eq(head, new_rhs2); + expr * body2 = m.mk_app(new_body->get_decl(), k_app, m_autil.mk_int(0)); + quantifier * q1 = m.update_quantifier(new_q, body1); + expr * patterns[1] = { m.mk_pattern(k_app) }; + quantifier * q2 = m.update_quantifier(new_q, 1, patterns, body2); proof* pr1 = 0, *pr2 = 0; - if (m_manager.proofs_enabled()) { + if (m.proofs_enabled()) { // new_pr : new_q // rw : [rewrite] new_q ~ q1 & q2 // mp : [modus_pones new_pr rw] q1 & q2 // pr1 : [and-elim mp] q1 // pr2 : [and-elim mp] q2 - app * q1q2 = m_manager.mk_and(q1,q2); - proof * rw = m_manager.mk_oeq_rewrite(new_q, q1q2); - proof * mp = m_manager.mk_modus_ponens(new_pr, rw); - pr1 = m_manager.mk_and_elim(mp, 0); - pr2 = m_manager.mk_and_elim(mp, 1); + app * q1q2 = m.mk_and(q1,q2); + proof * rw = m.mk_oeq_rewrite(new_q, q1q2); + proof * mp = m.mk_modus_ponens(new_pr, rw); + pr1 = m.mk_and_elim(mp, 0); + pr2 = m.mk_and_elim(mp, 1); } - new_fmls.push_back(justified_expr(m_manager, q1, pr1)); - new_fmls.push_back(justified_expr(m_manager, q2, pr2)); + new_fmls.push_back(justified_expr(m, q1, pr1)); + new_fmls.push_back(justified_expr(m, q2, pr2)); return true; } @@ -180,7 +185,7 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, vector& n is of the form: (forall (X) (iff (= (f X) t) def[X])) Convert it into: - + (forall (X) (= (f X) (ite def[X] t (k X)))) (forall (X) (not (= (k X) t))) @@ -188,13 +193,13 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, vector& The new quantifiers and proofs are stored in new_exprs and new_prs */ -static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr, - expr_ref_vector & new_exprs, proof_ref_vector & new_prs) { +static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr, expr_dependency * dep, + expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps ) { func_decl * f = head->get_decl(); func_decl * k = m.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range()); app * k_app = m.mk_app(k, head->get_num_args(), head->get_args()); app * ite = m.mk_ite(def, t, k_app); - app * body_1 = m.mk_eq(head, ite); + app * body_1 = m.mk_eq(head, ite); app * body_2 = m.mk_not(m.mk_eq(k_app, t)); quantifier * q1 = m.update_quantifier(q, body_1); expr * pats[1] = { m.mk_pattern(k_app) }; @@ -215,6 +220,8 @@ static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, e new_prs.push_back(pr1); new_prs.push_back(pr2); } + new_deps.push_back(dep); + new_deps.push_back(dep); } static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr, @@ -246,7 +253,7 @@ static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, e } macro_finder::macro_finder(ast_manager & m, macro_manager & mm): - m_manager(m), + m(m), m_macro_manager(mm), m_util(mm.get_util()), m_autil(m) { @@ -255,57 +262,67 @@ macro_finder::macro_finder(ast_manager & m, macro_manager & mm): macro_finder::~macro_finder() { } -bool macro_finder::expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) { +bool macro_finder::expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) { TRACE("macro_finder", tout << "starting expand_macros:\n"; m_macro_manager.display(tout);); bool found_new_macro = false; for (unsigned i = 0; i < num; i++) { expr * n = exprs[i]; - proof * pr = m_manager.proofs_enabled() ? prs[i] : 0; - expr_ref new_n(m_manager), def(m_manager); - proof_ref new_pr(m_manager); - m_macro_manager.expand_macros(n, pr, new_n, new_pr); - app_ref head(m_manager), t(m_manager); - if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr)) { + proof * pr = m.proofs_enabled() ? prs[i] : 0; + expr_dependency * depi = deps != 0 ? deps[i] : 0; + expr_ref new_n(m), def(m); + proof_ref new_pr(m); + expr_dependency_ref new_dep(m); + m_macro_manager.expand_macros(n, pr, depi, new_n, new_pr, new_dep); + app_ref head(m), t(m); + if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr, new_dep)) { TRACE("macro_finder_found", tout << "found new macro: " << head->get_decl()->get_name() << "\n" << new_n << "\n";); found_new_macro = true; } - else if (is_arith_macro(new_n, new_pr, new_exprs, new_prs)) { + else if (is_arith_macro(new_n, new_pr, new_dep, new_exprs, new_prs, new_deps)) { TRACE("macro_finder_found", tout << "found new arith macro:\n" << new_n << "\n";); found_new_macro = true; } - else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) { + else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) { TRACE("macro_finder_found", tout << "found new pseudo macro:\n" << head << "\n" << t << "\n" << def << "\n";); - pseudo_predicate_macro2macro(m_manager, head, t, def, to_quantifier(new_n), new_pr, new_exprs, new_prs); + pseudo_predicate_macro2macro(m, head, t, def, to_quantifier(new_n), new_pr, new_dep, new_exprs, new_prs, new_deps); found_new_macro = true; } else { new_exprs.push_back(new_n); - if (m_manager.proofs_enabled()) + if (m.proofs_enabled()) new_prs.push_back(new_pr); + if (deps != 0) + new_deps.push_back(new_dep); } } return found_new_macro; } -void macro_finder::operator()(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) { +void macro_finder::operator()(unsigned num, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) { TRACE("macro_finder", tout << "processing macros...\n";); - expr_ref_vector _new_exprs(m_manager); - proof_ref_vector _new_prs(m_manager); - if (expand_macros(num, exprs, prs, _new_exprs, _new_prs)) { + expr_ref_vector _new_exprs(m); + proof_ref_vector _new_prs(m); + expr_dependency_ref_vector _new_deps(m); + if (expand_macros(num, exprs, prs, deps, _new_exprs, _new_prs, _new_deps)) { while (true) { - expr_ref_vector old_exprs(m_manager); - proof_ref_vector old_prs(m_manager); + expr_ref_vector old_exprs(m); + proof_ref_vector old_prs(m); + expr_dependency_ref_vector old_deps(m); _new_exprs.swap(old_exprs); _new_prs.swap(old_prs); + _new_deps.swap(old_deps); SASSERT(_new_exprs.empty()); SASSERT(_new_prs.empty()); - if (!expand_macros(old_exprs.size(), old_exprs.c_ptr(), old_prs.c_ptr(), _new_exprs, _new_prs)) + SASSERT(_new_deps.empty()); + if (!expand_macros(old_exprs.size(), old_exprs.c_ptr(), old_prs.c_ptr(), old_deps.c_ptr(), + _new_exprs, _new_prs, _new_deps)) break; } } new_exprs.append(_new_exprs); new_prs.append(_new_prs); + new_deps.append(_new_deps); } @@ -316,11 +333,12 @@ bool macro_finder::expand_macros(unsigned num, justified_expr const * fmls, vect bool found_new_macro = false; for (unsigned i = 0; i < num; i++) { expr * n = fmls[i].get_fml(); - proof * pr = m_manager.proofs_enabled() ? fmls[i].get_proof() : 0; - expr_ref new_n(m_manager), def(m_manager); - proof_ref new_pr(m_manager); - m_macro_manager.expand_macros(n, pr, new_n, new_pr); - app_ref head(m_manager), t(m_manager); + proof * pr = m.proofs_enabled() ? fmls[i].get_proof() : 0; + expr_ref new_n(m), def(m); + proof_ref new_pr(m); + expr_dependency_ref new_dep(m); + m_macro_manager.expand_macros(n, pr, 0, new_n, new_pr, new_dep); + app_ref head(m), t(m); if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr)) { TRACE("macro_finder_found", tout << "found new macro: " << head->get_decl()->get_name() << "\n" << new_n << "\n";); found_new_macro = true; @@ -331,11 +349,11 @@ bool macro_finder::expand_macros(unsigned num, justified_expr const * fmls, vect } else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) { TRACE("macro_finder_found", tout << "found new pseudo macro:\n" << head << "\n" << t << "\n" << def << "\n";); - pseudo_predicate_macro2macro(m_manager, head, t, def, to_quantifier(new_n), new_pr, new_fmls); + pseudo_predicate_macro2macro(m, head, t, def, to_quantifier(new_n), new_pr, new_fmls); found_new_macro = true; } else { - new_fmls.push_back(justified_expr(m_manager, new_n, new_pr)); + new_fmls.push_back(justified_expr(m, new_n, new_pr)); } } return found_new_macro; diff --git a/src/ast/macros/macro_finder.h b/src/ast/macros/macro_finder.h index 2bba07306..2dd72a27f 100644 --- a/src/ast/macros/macro_finder.h +++ b/src/ast/macros/macro_finder.h @@ -22,34 +22,28 @@ Revision History: #include "ast/macros/macro_manager.h" -bool is_macro_head(expr * n, unsigned num_decls); -bool is_simple_macro(ast_manager & m, expr * n, unsigned num_decls, obj_hashtable const * forbidden_set, app * & head, expr * & def); -inline bool is_simple_macro(ast_manager & m, expr * n, unsigned num_decls, app * & head, expr * & def) { - return is_simple_macro(m, n, num_decls, 0, head, def); -} - /** \brief Macro finder is responsible for finding universally quantified sub-formulas that can be used as macros. */ class macro_finder { - ast_manager & m_manager; + ast_manager & m; macro_manager & m_macro_manager; macro_util & m_util; arith_util m_autil; - bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); + bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_dependency * const* deps, + expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector& new_deps); bool expand_macros(unsigned n, justified_expr const * fmls, vector& new_fmls); bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); bool is_arith_macro(expr * n, proof * pr, vector& new_fmls); + bool is_arith_macro(expr * n, proof * pr, expr_dependency * dep, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps); bool is_macro(expr * n, app_ref & head, expr_ref & def); - bool is_pseudo_head(expr * n, unsigned num_decls, app * & head, app * & t); - bool is_pseudo_predicate_macro(expr * n, app * & head, app * & t, expr * & def); public: macro_finder(ast_manager & m, macro_manager & mm); ~macro_finder(); - void operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); + void operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const* deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps); void operator()(unsigned n, justified_expr const* fmls, vector& new_fmls); }; diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp index 7a2642fa3..b6ee62322 100644 --- a/src/ast/macros/macro_manager.cpp +++ b/src/ast/macros/macro_manager.cpp @@ -34,6 +34,7 @@ macro_manager::macro_manager(ast_manager & m): m_decls(m), m_macros(m), m_macro_prs(m), + m_macro_deps(m), m_forbidden(m), m_deps(m) { m_util.set_forbidden_set(&m_forbidden_set); @@ -64,11 +65,13 @@ void macro_manager::restore_decls(unsigned old_sz) { m_deps.erase(m_decls.get(i)); if (m.proofs_enabled()) m_decl2macro_pr.erase(m_decls.get(i)); + m_decl2macro_dep.erase(m_decls.get(i)); } m_decls.shrink(old_sz); m_macros.shrink(old_sz); if (m.proofs_enabled()) m_macro_prs.shrink(old_sz); + m_macro_deps.shrink(old_sz); } void macro_manager::restore_forbidden(unsigned old_sz) { @@ -81,16 +84,18 @@ void macro_manager::restore_forbidden(unsigned old_sz) { void macro_manager::reset() { m_decl2macro.reset(); m_decl2macro_pr.reset(); + m_decl2macro_dep.reset(); m_decls.reset(); m_macros.reset(); m_macro_prs.reset(); + m_macro_deps.reset(); m_scopes.reset(); m_forbidden_set.reset(); m_forbidden.reset(); m_deps.reset(); } -bool macro_manager::insert(func_decl * f, quantifier * q, proof * pr) { +bool macro_manager::insert(func_decl * f, quantifier * q, proof * pr, expr_dependency* dep) { TRACE("macro_insert", tout << "trying to create macro: " << f->get_name() << "\n" << mk_pp(q, m) << "\n";); // if we already have a macro for f then return false; @@ -117,6 +122,8 @@ bool macro_manager::insert(func_decl * f, quantifier * q, proof * pr) { m_macro_prs.push_back(pr); m_decl2macro_pr.insert(f, pr); } + m_macro_deps.push_back(dep); + m_decl2macro_dep.insert(f, dep); TRACE("macro_insert", tout << "A macro was successfully created for: " << f->get_name() << "\n";); @@ -307,7 +314,7 @@ struct macro_manager::macro_expander_rw : public rewriter_tpl m_decl2macro; // func-decl -> quantifier obj_map m_decl2macro_pr; // func-decl -> quantifier_proof + obj_map m_decl2macro_dep; // func-decl -> unsat core dependency func_decl_ref_vector m_decls; quantifier_ref_vector m_macros; proof_ref_vector m_macro_prs; + expr_dependency_ref_vector m_macro_deps; obj_hashtable m_forbidden_set; func_decl_ref_vector m_forbidden; struct scope { @@ -50,7 +52,7 @@ class macro_manager { unsigned m_forbidden_lim; }; svector m_scopes; - + func_decl_dependencies m_deps; void restore_decls(unsigned old_sz); @@ -64,7 +66,7 @@ public: ~macro_manager(); ast_manager & get_manager() const { return m; } macro_util & get_util() { return m_util; } - bool insert(func_decl * f, quantifier * m, proof * pr); + bool insert(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep = 0); bool has_macros() const { return !m_macros.empty(); } void push_scope(); void pop_scope(unsigned num_scopes); @@ -81,9 +83,9 @@ public: func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const; quantifier * get_macro_quantifier(func_decl * f) const { quantifier * q = 0; m_decl2macro.find(f, q); return q; } void get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def) const; - void expand_macros(expr * n, proof * pr, expr_ref & r, proof_ref & new_pr); - - + void expand_macros(expr * n, proof * pr, expr_dependency * dep, expr_ref & r, proof_ref & new_pr, expr_dependency_ref & new_dep); + + }; #endif /* MACRO_MANAGER_H_ */ diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp index 527b9656d..7d5e7c3db 100644 --- a/src/ast/macros/quasi_macros.cpp +++ b/src/ast/macros/quasi_macros.cpp @@ -31,7 +31,7 @@ quasi_macros::quasi_macros(ast_manager & m, macro_manager & mm) : m_new_qsorts(m) { } -quasi_macros::~quasi_macros() { +quasi_macros::~quasi_macros() { } void quasi_macros::find_occurrences(expr * e) { @@ -41,7 +41,7 @@ void quasi_macros::find_occurrences(expr * e) { // we remember whether we have seen an expr once, or more than once; // when we see it the second time, we don't have to visit it another time, - // as we are only interested in finding unique function applications. + // as we are only interested in finding unique function applications. m_visited_once.reset(); m_visited_more.reset(); @@ -64,8 +64,8 @@ void quasi_macros::find_occurrences(expr * e) { if (is_non_ground_uninterp(cur)) { func_decl * f = to_app(cur)->get_decl(); m_occurrences.insert_if_not_there(f, 0); - occurrences_map::iterator it = m_occurrences.find_iterator(f); - it->m_value++; + occurrences_map::iterator it = m_occurrences.find_iterator(f); + it->m_value++; } j = to_app(cur)->get_num_args(); while (j) @@ -84,16 +84,16 @@ bool quasi_macros::is_unique(func_decl * f) const { return m_occurrences.find(f) == 1; } -struct var_dep_proc { +struct var_dep_proc { bit_vector m_bitset; public: var_dep_proc(quantifier * q) { m_bitset.resize(q->get_num_decls(), false); } void operator()(var * n) { m_bitset.set(n->get_idx(), true); } void operator()(quantifier * n) {} void operator()(app * n) {} - bool all_used(void) { + bool all_used(void) { for (unsigned i = 0; i < m_bitset.size() ; i++) - if (!m_bitset.get(i)) + if (!m_bitset.get(i)) return false; return true; } @@ -101,7 +101,7 @@ public: bool quasi_macros::fully_depends_on(app * a, quantifier * q) const { // CMW: This checks whether all variables in q are used _somewhere_ deep down in the children of a - + /* var_dep_proc proc(q); for_each_expr(proc, a); return proc.all_used(); */ @@ -116,14 +116,14 @@ bool quasi_macros::fully_depends_on(app * a, quantifier * q) const { } for (unsigned i = 0; i < bitset.size() ; i++) { - if (!bitset.get(i)) + if (!bitset.get(i)) return false; } return true; } -bool quasi_macros::depends_on(expr * e, func_decl * f) const { +bool quasi_macros::depends_on(expr * e, func_decl * f) const { ptr_vector todo; expr_mark visited; todo.push_back(e); @@ -133,12 +133,12 @@ bool quasi_macros::depends_on(expr * e, func_decl * f) const { if (visited.is_marked(cur)) continue; - + if (is_app(cur)) { app * a = to_app(cur); - if (a->get_decl() == f) + if (a->get_decl() == f) return true; - + unsigned j = a->get_num_args(); while (j>0) todo.push_back(a->get_arg(--j)); @@ -151,7 +151,7 @@ bool quasi_macros::depends_on(expr * e, func_decl * f) const { bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const { // Our definition of a quasi-macro: - // Forall X. f[X] = T[X], where f[X] is a term starting with symbol f, f is uninterpreted, + // Forall X. f[X] = T[X], where f[X] is a term starting with symbol f, f is uninterpreted, // f[X] contains all universally quantified variables, and f does not occur in T[X]. TRACE("quasi_macros", tout << "Checking for quasi macro: " << mk_pp(e, m_manager) << std::endl;); @@ -165,14 +165,14 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const { if (is_non_ground_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) && !depends_on(rhs, to_app(lhs)->get_decl()) && fully_depends_on(to_app(lhs), q)) { a = to_app(lhs); - t = rhs; + t = rhs; return true; } else if (is_non_ground_uninterp(rhs) && is_unique(to_app(rhs)->get_decl()) && - !depends_on(lhs, to_app(rhs)->get_decl()) && fully_depends_on(to_app(rhs), q)) { + !depends_on(lhs, to_app(rhs)->get_decl()) && fully_depends_on(to_app(rhs), q)) { a = to_app(rhs); - t = lhs; + t = lhs; return true; - } + } } else if (m_manager.is_not(qe) && is_non_ground_uninterp(to_app(qe)->get_arg(0)) && is_unique(to_app(to_app(qe)->get_arg(0))->get_decl())) { // this is like f(...) = false a = to_app(to_app(qe)->get_arg(0)); @@ -189,7 +189,7 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const { } void quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quantifier_ref & macro) { - m_new_var_names.reset(); + m_new_var_names.reset(); m_new_vars.reset(); m_new_qsorts.reset(); m_new_eqs.reset(); @@ -197,19 +197,19 @@ void quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quant func_decl * f = a->get_decl(); // CMW: we rely on the fact that all variables in q appear at least once as - // a direct argument of `a'. + // a direct argument of `a'. bit_vector v_seen; - v_seen.resize(q->get_num_decls(), false); + v_seen.resize(q->get_num_decls(), false); for (unsigned i = 0 ; i < a->get_num_args() ; i++) { - if (!is_var(a->get_arg(i)) || + if (!is_var(a->get_arg(i)) || v_seen.get(to_var(a->get_arg(i))->get_idx())) { unsigned inx = m_new_var_names.size(); m_new_name.str(""); m_new_name << "X" << inx; - m_new_var_names.push_back(symbol(m_new_name.str().c_str())); + m_new_var_names.push_back(symbol(m_new_name.str().c_str())); m_new_qsorts.push_back(f->get_domain()[i]); - + m_new_vars.push_back(m_manager.mk_var(inx + q->get_num_decls(), f->get_domain()[i])); m_new_eqs.push_back(m_manager.mk_eq(m_new_vars.back(), a->get_arg(i))); } else { @@ -228,13 +228,13 @@ void quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quant new_var_names_rev.push_back(m_new_var_names.get(i)); new_qsorts_rev.push_back(m_new_qsorts.get(i)); } - + // We want to keep all the old variables [already reversed] for (unsigned i = 0 ; i < q->get_num_decls() ; i++) { new_var_names_rev.push_back(q->get_decl_name(i)); new_qsorts_rev.push_back(q->get_decl_sort(i)); } - + // Macro := Forall m_new_vars . appl = ITE( m_new_eqs, t, f_else) app_ref appl(m_manager); @@ -251,30 +251,29 @@ void quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quant eq = m_manager.mk_eq(appl, ite); - macro = m_manager.mk_quantifier(true, new_var_names_rev.size(), + macro = m_manager.mk_quantifier(true, new_var_names_rev.size(), new_qsorts_rev.c_ptr(), new_var_names_rev.c_ptr(), eq); } bool quasi_macros::find_macros(unsigned n, expr * const * exprs) { TRACE("quasi_macros", tout << "Finding quasi-macros in: " << std::endl; - for (unsigned i = 0 ; i < n ; i++) + for (unsigned i = 0 ; i < n ; i++) tout << i << ": " << mk_pp(exprs[i], m_manager) << std::endl; ); bool res = false; m_occurrences.reset(); - - // Find out how many non-ground appearences for each uninterpreted function there are - for ( unsigned i = 0 ; i < n ; i++ ) + + // Find out how many non-ground appearences for each uninterpreted function there are + for (unsigned i = 0 ; i < n ; i++) find_occurrences(exprs[i]); - TRACE("quasi_macros", tout << "Occurrences: " << std::endl; - for (occurrences_map::iterator it = m_occurrences.begin(); - it != m_occurrences.end(); - it++) - tout << it->m_key->get_name() << ": " << it->m_value << std::endl; ); - + TRACE("quasi_macros", + tout << "Occurrences: " << std::endl; + for (auto & kd : m_occurrences) + tout << kd.m_key->get_name() << ": " << kd.m_value << std::endl; ); + // Find all macros - for ( unsigned i = 0 ; i < n ; i++ ) { + for (unsigned i = 0 ; i < n ; i++) { app_ref a(m_manager); expr_ref t(m_manager); if (is_quasi_macro(exprs[i], a, t)) { @@ -285,7 +284,8 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) { proof * pr = 0; if (m_manager.proofs_enabled()) pr = m_manager.mk_def_axiom(macro); - if (m_macro_manager.insert(a->get_decl(), macro, pr)) + expr_dependency * dep = 0; + if (m_macro_manager.insert(a->get_decl(), macro, pr, dep)) res = true; } } @@ -331,31 +331,35 @@ bool quasi_macros::find_macros(unsigned n, justified_expr const * exprs) { return res; } -void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) { +void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const* deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector& new_deps) { for ( unsigned i = 0 ; i < n ; i++ ) { expr_ref r(m_manager), rs(m_manager); proof_ref pr(m_manager), ps(m_manager); + expr_dependency_ref dep(m_manager); proof * p = m_manager.proofs_enabled() ? prs[i] : 0; - m_macro_manager.expand_macros(exprs[i], p, r, pr); + + m_macro_manager.expand_macros(exprs[i], p, deps[i], r, pr, dep); m_rewriter(r); new_exprs.push_back(r); new_prs.push_back(ps); + new_deps.push_back(dep); } } -bool quasi_macros::operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) { +bool quasi_macros::operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) { if (find_macros(n, exprs)) { - apply_macros(n, exprs, prs, new_exprs, new_prs); + apply_macros(n, exprs, prs, deps, new_exprs, new_prs, new_deps); return true; - } else { + } + else { // just copy them over for ( unsigned i = 0 ; i < n ; i++ ) { new_exprs.push_back(exprs[i]); - if (m_manager.proofs_enabled()) + if (m_manager.proofs_enabled()) new_prs.push_back(prs[i]); } return false; - } + } } void quasi_macros::apply_macros(unsigned n, justified_expr const* fmls, vector& new_fmls) { @@ -363,7 +367,8 @@ void quasi_macros::apply_macros(unsigned n, justified_expr const* fmls, vector m_todo; + ptr_vector m_todo; vector m_new_var_names; expr_ref_vector m_new_vars; expr_ref_vector m_new_eqs; sort_ref_vector m_new_qsorts; - std::stringstream m_new_name; + std::stringstream m_new_name; expr_mark m_visited_once; expr_mark m_visited_more; - + bool is_unique(func_decl * f) const; bool is_non_ground_uninterp(expr const * e) const; - bool fully_depends_on(app * a, quantifier * q) const; + bool fully_depends_on(app * a, quantifier * q) const; bool depends_on(expr * e, func_decl * f) const; - bool is_quasi_macro(expr * e, app_ref & a, expr_ref &v) const; + bool is_quasi_macro(expr * e, app_ref & a, expr_ref &v) const; void quasi_macro_to_macro(quantifier * q, app * a, expr * t, quantifier_ref & macro); void find_occurrences(expr * e); bool find_macros(unsigned n, expr * const * exprs); bool find_macros(unsigned n, justified_expr const* expr); - void apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); + void apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const* deps, + expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector& new_deps); void apply_macros(unsigned n, justified_expr const* fmls, vector& new_fmls); public: quasi_macros(ast_manager & m, macro_manager & mm); ~quasi_macros(); - + /** \brief Find pure function macros and apply them. */ - bool operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); + // bool operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); bool operator()(unsigned n, justified_expr const* fmls, vector& new_fmls); + bool operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps); + }; #endif diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 3fb20d283..44ccd0bf6 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -76,7 +76,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p): void asserted_formulas::setup() { switch (m_params.m_lift_ite) { case LI_FULL: - m_params.m_ng_lift_ite = LI_NONE; + m_params.m_ng_lift_ite = LI_NONE; break; case LI_CONSERVATIVE: if (m_params.m_ng_lift_ite == LI_CONSERVATIVE) @@ -85,7 +85,7 @@ void asserted_formulas::setup() { default: break; } - + if (m_params.m_relevancy_lvl == 0) m_params.m_relevancy_lemma = false; } @@ -98,7 +98,7 @@ void asserted_formulas::setup_simplifier_plugins(simplifier & s, basic_simplifie s.register_plugin(alloc(array_simplifier_plugin, m, *bsimp, s, m_params)); bvsimp = alloc(bv_simplifier_plugin, m, *bsimp, m_params); s.register_plugin(bvsimp); - s.register_plugin(alloc(datatype_simplifier_plugin, m, *bsimp)); + s.register_plugin(alloc(datatype_simplifier_plugin, m, *bsimp)); s.register_plugin(alloc(fpa_simplifier_plugin, m, *bsimp)); s.register_plugin(alloc(seq_simplifier_plugin, m, *bsimp)); } @@ -141,7 +141,7 @@ void asserted_formulas::set_eliminate_and(bool flag) { void asserted_formulas::assert_expr(expr * e, proof * _in_pr) { - if (inconsistent()) + if (inconsistent()) return; m_has_quantifiers |= ::has_quantifiers(e); if (!m_params.m_preprocess) { @@ -177,7 +177,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) { } void asserted_formulas::assert_expr(expr * e) { - if (inconsistent()) + if (inconsistent()) return; assert_expr(e, m.mk_asserted(e)); } @@ -199,7 +199,7 @@ void asserted_formulas::push_scope() { m_bv_sharing.push_scope(); commit(); } - + void asserted_formulas::pop_scope(unsigned num_scopes) { TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << "\n"; display(tout);); m_bv_sharing.pop_scope(num_scopes); @@ -230,15 +230,15 @@ void asserted_formulas::reset() { #ifdef Z3DEBUG bool asserted_formulas::check_well_sorted() const { - for (unsigned i = 0; i < m_asserted_formulas.size(); i++) { - if (!is_well_sorted(m, m_asserted_formulas.get(i))) return false; + for (unsigned i = 0; i < m_asserted_formulas.size(); i++) { + if (!is_well_sorted(m, m_asserted_formulas.get(i))) return false; } return true; } #endif void asserted_formulas::reduce() { - if (inconsistent()) + if (inconsistent()) return; if (canceled()) { return; @@ -255,7 +255,7 @@ void asserted_formulas::reduce() { #define INVOKE(COND, FUNC) if (COND) { FUNC; IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";); } TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited);); TRACE("reduce_step", display(tout << #FUNC << " ");); CASSERT("well_sorted",check_well_sorted()); if (inconsistent() || canceled()) { TRACE("after_reduce", display(tout);); TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited);); return; } - + set_eliminate_and(false); // do not eliminate and before nnf. INVOKE(m_params.m_propagate_booleans, propagate_booleans()); INVOKE(m_params.m_propagate_values, propagate_values()); @@ -268,18 +268,18 @@ void asserted_formulas::reduce() { INVOKE(m_params.m_lift_ite != LI_NONE, lift_ite()); INVOKE(m_params.m_eliminate_term_ite && m_params.m_lift_ite != LI_FULL, eliminate_term_ite()); INVOKE(m_params.m_refine_inj_axiom && has_quantifiers(), refine_inj_axiom()); - INVOKE(m_params.m_distribute_forall && has_quantifiers(), apply_distribute_forall()); - TRACE("qbv_bug", tout << "after distribute_forall:\n"; display(tout);); + INVOKE(m_params.m_distribute_forall && has_quantifiers(), apply_distribute_forall()); + TRACE("qbv_bug", tout << "after distribute_forall:\n"; display(tout);); INVOKE(m_params.m_macro_finder && has_quantifiers(), find_macros()); - INVOKE(m_params.m_quasi_macros && has_quantifiers(), apply_quasi_macros()); + INVOKE(m_params.m_quasi_macros && has_quantifiers(), apply_quasi_macros()); INVOKE(m_params.m_simplify_bit2int, apply_bit2int()); INVOKE(m_params.m_eliminate_bounds && has_quantifiers(), cheap_quant_fourier_motzkin()); INVOKE(m_params.m_ematching && has_quantifiers(), infer_patterns()); INVOKE(m_params.m_max_bv_sharing && has_bv(), max_bv_sharing()); INVOKE(m_params.m_bb_quantifiers, elim_bvs_from_quantifiers()); - // temporary HACK: make sure that arith & bv are list-assoc + // temporary HACK: make sure that arith & bv are list-assoc // this may destroy some simplification steps such as max_bv_sharing - reduce_asserted_formulas(); + reduce_asserted_formulas(); CASSERT("well_sorted",check_well_sorted()); @@ -293,7 +293,7 @@ void asserted_formulas::reduce() { void asserted_formulas::eliminate_and() { IF_IVERBOSE(10, verbose_stream() << "(smt.eliminating-and)\n";); set_eliminate_and(true); - reduce_asserted_formulas(); + reduce_asserted_formulas(); TRACE("after_elim_and", display(tout);); } @@ -333,10 +333,10 @@ void asserted_formulas::display(std::ostream & out) const { void asserted_formulas::display_ll(std::ostream & out, ast_mark & pp_visited) const { if (!m_asserted_formulas.empty()) { unsigned sz = m_asserted_formulas.size(); - for (unsigned i = 0; i < sz; i++) + for (unsigned i = 0; i < sz; i++) ast_def_ll_pp(out, m, m_asserted_formulas.get(i), pp_visited, true, false); out << "asserted formulas:\n"; - for (unsigned i = 0; i < sz; i++) + for (unsigned i = 0; i < sz; i++) out << "#" << m_asserted_formulas[i]->get_id() << " "; out << "\n"; } @@ -389,8 +389,12 @@ void asserted_formulas::find_macros_core() { expr_ref_vector new_exprs(m); proof_ref_vector new_prs(m); unsigned sz = m_asserted_formulas.size(); - m_macro_finder->operator()(sz - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead, - m_asserted_formula_prs.c_ptr() + m_asserted_qhead, new_exprs, new_prs); + expr_dependency_ref_vector new_deps(m); + m_macro_finder->operator()(sz - m_asserted_qhead, + m_asserted_formulas.c_ptr() + m_asserted_qhead, + m_asserted_formula_prs.c_ptr() + m_asserted_qhead, + 0, // 0 == No dependency tracking + new_exprs, new_prs, new_deps); swap_asserted_formulas(new_exprs, new_prs); reduce_and_solve(); } @@ -412,14 +416,17 @@ void asserted_formulas::apply_quasi_macros() { TRACE("before_quasi_macros", display(tout);); expr_ref_vector new_exprs(m); proof_ref_vector new_prs(m); + expr_dependency_ref_vector new_deps(m); quasi_macros proc(m, m_macro_manager); while (proc(m_asserted_formulas.size() - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead, m_asserted_formula_prs.c_ptr() + m_asserted_qhead, - new_exprs, new_prs)) { + 0, // 0 == No dependency tracking + new_exprs, new_prs, new_deps)) { swap_asserted_formulas(new_exprs, new_prs); new_exprs.reset(); new_prs.reset(); + new_deps.reset(); } TRACE("after_quasi_macros", display(tout);); reduce_and_solve(); @@ -432,7 +439,7 @@ void asserted_formulas::nnf_cnf() { proof_ref_vector new_prs(m); expr_ref_vector push_todo(m); proof_ref_vector push_todo_prs(m); - + unsigned i = m_asserted_qhead; unsigned sz = m_asserted_formulas.size(); TRACE("nnf_bug", tout << "i: " << i << " sz: " << sz << "\n";); @@ -462,8 +469,8 @@ void asserted_formulas::nnf_cnf() { CASSERT("well_sorted",is_well_sorted(m, r1)); if (canceled()) { return; - } - + } + if (m.proofs_enabled()) pr = m.mk_modus_ponens(push_todo_prs.get(k), pr1); else @@ -600,7 +607,7 @@ void asserted_formulas::propagate_values() { // C is a set which contains formulas of the form // { x = n }, where x is a variable and n a numeral. // R contains the rest. - // + // // - new_exprs1 is the set C // - new_exprs2 is the set R // @@ -665,7 +672,7 @@ void asserted_formulas::propagate_values() { // x->n will be removed from m_cache. If we don't do that, the next transformation // may simplify constraints in C using these entries, and the variables x in C // will be (silently) eliminated, and models produced by Z3 will not contain them. - flush_cache(); + flush_cache(); } TRACE("propagate_values", tout << "after:\n"; display(tout);); } @@ -788,7 +795,7 @@ void asserted_formulas::refine_inj_axiom() { TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(n, m) << "\n" << mk_pp(new_n, m) << "\n";); m_asserted_formulas.set(i, new_n); if (m.proofs_enabled()) { - proof_ref new_pr(m); + proof_ref new_pr(m); new_pr = m.mk_rewrite(n, new_n); new_pr = m.mk_modus_ponens(pr, new_pr); m_asserted_formula_prs.set(i, new_pr); @@ -862,7 +869,7 @@ void asserted_formulas::max_bv_sharing() { } reduce_asserted_formulas(); TRACE("bv_sharing", display(tout);); - + } #ifdef Z3DEBUG diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h index 3c5f424fb..1e15e6300 100644 --- a/src/smt/asserted_formulas.h +++ b/src/smt/asserted_formulas.h @@ -51,7 +51,7 @@ class asserted_formulas { macro_manager m_macro_manager; scoped_ptr m_macro_finder; - + bit2int m_bit2int; maximise_bv_sharing m_bv_sharing; @@ -90,7 +90,7 @@ class asserted_formulas { bool apply_bit2int(); void lift_ite(); bool elim_bvs_from_quantifiers(); - void ng_lift_ite(); + void ng_lift_ite(); #ifdef Z3DEBUG bool check_well_sorted() const; #endif @@ -115,8 +115,8 @@ public: unsigned get_num_formulas() const { return m_asserted_formulas.size(); } unsigned get_formulas_last_level() const; unsigned get_qhead() const { return m_asserted_qhead; } - void commit(); - void commit(unsigned new_qhead); + void commit(); + void commit(unsigned new_qhead); expr * get_formula(unsigned idx) const { return m_asserted_formulas.get(idx); } proof * get_formula_proof(unsigned idx) const { return m.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; } expr * const * get_formulas() const { return m_asserted_formulas.c_ptr(); } @@ -133,7 +133,7 @@ public: void collect_statistics(statistics & st) const; // TODO: improve precision of the following method. bool has_quantifiers() const { return m_has_quantifiers; } - + // ----------------------------------- // // Macros @@ -144,9 +144,7 @@ public: func_decl * get_macro_func_decl(unsigned i) const { return m_macro_manager.get_macro_func_decl(i); } func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const { return m_macro_manager.get_macro_interpretation(i, interp); } quantifier * get_macro_quantifier(func_decl * f) const { return m_macro_manager.get_macro_quantifier(f); } - // auxiliary function used to create a logic context based on a model. - void insert_macro(func_decl * f, quantifier * m, proof * pr) { m_macro_manager.insert(f, m, pr); } - + void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) { m_macro_manager.insert(f, m, pr, dep); } }; #endif /* ASSERTED_FORMULAS_H_ */ diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp index fcdea850f..0b621870d 100644 --- a/src/smt/params/preprocessor_params.cpp +++ b/src/smt/params/preprocessor_params.cpp @@ -22,6 +22,8 @@ Revision History: void preprocessor_params::updt_local_params(params_ref const & _p) { smt_params_helper p(_p); m_macro_finder = p.macro_finder(); + m_quasi_macros = p.quasi_macros(); + m_restricted_quasi_macros = p.restricted_quasi_macros(); m_pull_nested_quantifiers = p.pull_nested_quantifiers(); m_refine_inj_axiom = p.refine_inj_axioms(); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 5b5c7328c..d6ca8c9b2 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -7,6 +7,8 @@ def_module_params(module_name='smt', ('random_seed', UINT, 0, 'random seed for the smt solver'), ('relevancy', UINT, 2, 'relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant'), ('macro_finder', BOOL, False, 'try to find universally quantified formulas that can be viewed as macros'), + ('quasi_macros', BOOL, False, 'try to find universally quantified formulas that are quasi-macros'), + ('restricted_quasi_macros', BOOL, False, 'try to find universally quantified formulas that are restricted quasi-macros'), ('ematching', BOOL, True, 'E-Matching based quantifier instantiation'), ('phase_selection', UINT, 3, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences'), ('restart_strategy', UINT, 1, '0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic'), diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index fbf7cbca3..a6a67702a 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -209,7 +209,7 @@ namespace smt { ~scoped_mk_model() { if (m_ctx.m_proto_model.get() != 0) { m_ctx.m_model = m_ctx.m_proto_model->mk_model(); - m_ctx.add_rec_funs_to_model(); + m_ctx.add_rec_funs_to_model(); m_ctx.m_proto_model = 0; // proto_model is not needed anymore. } } @@ -1566,7 +1566,7 @@ namespace smt { func_decl * get_macro_func_decl(unsigned i) const { return m_asserted_formulas.get_macro_func_decl(i); } func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const { return m_asserted_formulas.get_macro_interpretation(i, interp); } quantifier * get_macro_quantifier(func_decl * f) const { return m_asserted_formulas.get_macro_quantifier(f); } - void insert_macro(func_decl * f, quantifier * m, proof * pr) { m_asserted_formulas.insert_macro(f, m, pr); } + void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) { m_asserted_formulas.insert_macro(f, m, pr, dep); } }; }; diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index f678ee3e7..0536c200d 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -82,8 +82,8 @@ namespace smt { expr_mark m_visited; public: instantiation_set(ast_manager & m):m_manager(m) {} - - ~instantiation_set() { + + ~instantiation_set() { for (auto const& kv : m_elems) { m_manager.dec_ref(kv.m_key); } @@ -108,7 +108,7 @@ namespace smt { m_elems.erase(n); m_manager.dec_ref(n); } - + void display(std::ostream & out) const { for (auto const& kv : m_elems) { out << mk_bounded_pp(kv.m_key, m_manager) << " [" << kv.m_value << "]\n"; @@ -124,7 +124,7 @@ namespace smt { m_inv.find(v, t); return t; } - + unsigned get_generation(expr * t) const { unsigned gen = 0; m_elems.find(t, gen); @@ -185,15 +185,15 @@ namespace smt { }; /** - During model construction time, + During model construction time, we solve several constraints that impose restrictions on how the model for the ground formulas may be extended to a model to the relevant universal quantifiers. - + The class node and its subclasses are used to solve these constraints. */ - + // ----------------------------------- // // nodes @@ -207,14 +207,14 @@ namespace smt { unsigned m_id; node * m_find; unsigned m_eqc_size; - + sort * m_sort; // sort of the elements in the instantiation set. - + bool m_mono_proj; // relevant for integers & reals & bit-vectors bool m_signed_proj; // relevant for bit-vectors. ptr_vector m_avoid_set; ptr_vector m_exceptions; - + instantiation_set * m_set; expr * m_else; @@ -284,7 +284,7 @@ namespace smt { if (!ex.contains(n)) ex.push_back(n); } - + void set_mono_proj() { get_root()->m_mono_proj = true; } @@ -346,7 +346,7 @@ namespace smt { instantiation_set * get_instantiation_set() { return get_root()->m_set; } ptr_vector const & get_exceptions() const { return get_root()->m_exceptions; } - + ptr_vector const & get_avoid_set() const { return get_root()->m_avoid_set; } // return true if m_avoid_set.contains(this) @@ -364,8 +364,8 @@ namespace smt { SASSERT(get_root()->m_else == 0); get_root()->m_else = e; } - - expr * get_else() const { + + expr * get_else() const { return get_root()->m_else; } @@ -373,7 +373,7 @@ namespace smt { SASSERT(get_root()->m_proj == 0); get_root()->m_proj = f; } - + func_decl * get_proj() const { return get_root()->m_proj; } @@ -382,7 +382,7 @@ namespace smt { typedef std::pair ast_idx_pair; typedef pair_hash, unsigned_hash> ast_idx_pair_hash; typedef map > key2node; - + /** \brief Auxiliary class for processing the "Almost uninterpreted fragment" described in the paper: Complete instantiation for quantified SMT formulas @@ -400,16 +400,16 @@ namespace smt { context * m_context; - // Mapping from sort to auxiliary constant. - // This auxiliary constant is used as a "witness" that is asserted as different from a - // finite number of terms. + // Mapping from sort to auxiliary constant. + // This auxiliary constant is used as a "witness" that is asserted as different from a + // finite number of terms. // It is only safe to use this constant for infinite sorts. - obj_map m_sort2k; + obj_map m_sort2k; expr_ref_vector m_ks; // range of m_sort2k - + // Support for evaluating expressions in the current model. proto_model * m_model; - obj_map m_eval_cache[2]; + obj_map m_eval_cache[2]; expr_ref_vector m_eval_cache_range; ptr_vector m_root_nodes; @@ -426,7 +426,7 @@ namespace smt { m_eval_cache[1].reset(); m_eval_cache_range.reset(); } - + node * mk_node(key2node & m, ast * n, unsigned i, sort * s) { node * r = 0; ast_idx_pair k(n, i); @@ -480,7 +480,7 @@ namespace smt { flush_nodes(); reset_eval_cache(); } - + void set_context(context * ctx) { SASSERT(m_context==0); m_context = ctx; @@ -503,21 +503,21 @@ namespace smt { m_model = m; } - proto_model * get_model() const { + proto_model * get_model() const { SASSERT(m_model); return m_model; } - - node * get_uvar(quantifier * q, unsigned i) { + + node * get_uvar(quantifier * q, unsigned i) { SASSERT(i < q->get_num_decls()); sort * s = q->get_decl_sort(q->get_num_decls() - i - 1); - return mk_node(m_uvars, q, i, s); + return mk_node(m_uvars, q, i, s); } - node * get_A_f_i(func_decl * f, unsigned i) { + node * get_A_f_i(func_decl * f, unsigned i) { SASSERT(i < f->get_arity()); sort * s = f->get_domain(i); - return mk_node(m_A_f_is, f, i, s); + return mk_node(m_A_f_is, f, i, s); } instantiation_set const * get_uvar_inst_set(quantifier * q, unsigned i) const { @@ -528,7 +528,7 @@ namespace smt { return r->get_instantiation_set(); return 0; } - + void mk_instantiation_sets() { for (node* curr : m_nodes) { if (curr->is_root()) { @@ -560,7 +560,7 @@ namespace smt { void display_nodes(std::ostream & out) const { display_key2node(out, m_uvars); - display_A_f_is(out); + display_A_f_is(out); for (node* n : m_nodes) { n->display(out, m); } @@ -593,13 +593,13 @@ namespace smt { void collect_exceptions_values(node * n, ptr_buffer & r) { ptr_vector const & exceptions = n->get_exceptions(); ptr_vector const & avoid_set = n->get_avoid_set(); - + for (expr* e : exceptions) { expr * val = eval(e, true); SASSERT(val != 0); r.push_back(val); } - + for (node* a : avoid_set) { node * n = a->get_root(); if (!n->is_mono_proj() && n->get_else() != 0) { @@ -622,7 +622,7 @@ namespace smt { obj_map const & elems = s->get_elems(); expr * t_result = 0; - unsigned gen_result = UINT_MAX; + unsigned gen_result = UINT_MAX; for (auto const& kv : elems) { expr * t = kv.m_key; unsigned gen = kv.m_value; @@ -651,7 +651,7 @@ namespace smt { } /** - \brief Return a fresh constant k that is used as a witness for elements that must be different from + \brief Return a fresh constant k that is used as a witness for elements that must be different from a set of values. */ app * get_k_for(sort * s) { @@ -668,7 +668,7 @@ namespace smt { /** \brief Get the interpretation for k in m_model. - If m_model does not provide an interpretation for k, then + If m_model does not provide an interpretation for k, then create a fresh one. Remark: this method uses get_fresh_value, so it may fail. @@ -711,7 +711,7 @@ namespace smt { } return true; } - + void set_projection_else(node * n) { SASSERT(n->is_root()); SASSERT(!n->is_mono_proj()); @@ -738,7 +738,7 @@ namespace smt { return; } } - // TBD: add support for the else of bitvectors. + // TBD: add support for the else of bitvectors. // Idea: get the term t with the minimal interpreation and use t - 1. } n->set_else((*(elems.begin())).m_key); @@ -897,7 +897,7 @@ namespace smt { } n->set_proj(p); } - + void mk_projections() { for (node * n : m_root_nodes) { SASSERT(n->is_root()); @@ -907,7 +907,7 @@ namespace smt { mk_simple_proj(n); } } - + /** \brief Store in r the partial functions that have A_f_i nodes. */ @@ -927,7 +927,7 @@ namespace smt { } } } - + /** \brief Make sorts associated with nodes that must avoid themselves finite. Only uninterpreted sorts are considered. @@ -941,14 +941,14 @@ namespace smt { sort * s = n->get_sort(); if (m.is_uninterp(s) && // Making all uninterpreted sorts finite. - // n->must_avoid_itself() && + // n->must_avoid_itself() && !m_model->is_finite(s)) { m_model->freeze_universe(s); } } } - void add_elem_to_empty_inst_sets() { + void add_elem_to_empty_inst_sets() { obj_map sort2elems; ptr_vector need_fresh; for (node * n : m_root_nodes) { @@ -957,11 +957,11 @@ namespace smt { TRACE("model_finder", s->display(tout);); obj_map const & elems = s->get_elems(); if (elems.empty()) { - // The method get_some_value cannot be used if n->get_sort() is an uninterpreted sort or is a sort built using uninterpreted sorts + // The method get_some_value cannot be used if n->get_sort() is an uninterpreted sort or is a sort built using uninterpreted sorts // (e.g., (Array S S) where S is uninterpreted). The problem is that these sorts do not have a fixed interpretation. // Moreover, a model assigns an arbitrary intepretation to these sorts using "model_values" a model value. // If these module values "leak" inside the logical context, they may affect satisfiability. - // + // sort * ns = n->get_sort(); if (m.is_fully_interp(ns)) { n->insert(m_model->get_some_value(ns), 0); @@ -999,14 +999,14 @@ namespace smt { m_root_nodes.push_back(n); } } - + /** \brief Return the projection function for f at argument i. - Return 0, if there is none. + Return 0, if there is none. \remark This method assumes that mk_projections was already invoked. - + \remark f may have a non partial interpretation on m_model. This may happen because the evaluator uses model_completion. In the beginning of fix_model() we collected all f with @@ -1023,16 +1023,16 @@ namespace smt { return 0; return r->get_proj(); } - + /** - \brief Complete the interpretation of the functions that were + \brief Complete the interpretation of the functions that were collected in the beginning of fix_model(). */ void complete_partial_funcs(func_decl_set const & partial_funcs) { for (func_decl * f : partial_funcs) { // Complete the current interpretation m_model->complete_partial_func(f); - + unsigned arity = f->get_arity(); func_interp * fi = m_model->get_func_interp(f); if (fi->is_constant()) @@ -1068,7 +1068,7 @@ namespace smt { instantiation_set * s = n->get_instantiation_set(); s->mk_inverse(*this); } - + void mk_inverses() { for (node * n : m_root_nodes) { SASSERT(n->is_root()); @@ -1108,7 +1108,7 @@ namespace smt { information about the quantifier structure. These bits are instances of subclasses of qinfo. */ - + /** \brief Generic bit of information collected when analyzing quantifiers. The subclasses are defined in the .cpp file. @@ -1119,7 +1119,7 @@ namespace smt { virtual char const * get_kind() const = 0; virtual bool is_equal(qinfo const * qi) const = 0; virtual void display(std::ostream & out) const { out << "[" << get_kind() << "]"; } - + // AUF fragment solver virtual void process_auf(quantifier * q, auf_solver & s, context * ctx) = 0; virtual void populate_inst_sets(quantifier * q, auf_solver & s, context * ctx) = 0; @@ -1140,17 +1140,17 @@ namespace smt { f_var(func_decl * f, unsigned i, unsigned j):m_f(f), m_arg_i(i), m_var_j(j) {} virtual ~f_var() {} - virtual char const * get_kind() const { - return "f_var"; + virtual char const * get_kind() const { + return "f_var"; } - + virtual bool is_equal(qinfo const * qi) const { if (qi->get_kind() != get_kind()) return false; f_var const * other = static_cast(qi); return m_f == other->m_f && m_arg_i == other->m_arg_i && m_var_j == other->m_var_j; } - + virtual void display(std::ostream & out) const { out << "(" << m_f->get_name() << ":" << m_arg_i << " -> v!" << m_var_j << ")"; } @@ -1170,7 +1170,7 @@ namespace smt { for (unsigned i = 0; i < m_f->get_arity(); i++) tout << mk_pp(m_f->get_domain(i), m) << " "; tout << "-> " << mk_pp(m_f->get_range(), m) << "\n"; ); - + n1->merge(n2); } @@ -1192,7 +1192,7 @@ namespace smt { // a necessary instantiation. enode * e_arg = n->get_arg(m_arg_i); expr * arg = e_arg->get_owner(); - A_f_i->insert(arg, e_arg->get_generation()); + A_f_i->insert(arg, e_arg->get_generation()); } } } @@ -1205,7 +1205,7 @@ namespace smt { uvar_inst_sets[m_var_j] = alloc(instantiation_set, ctx->get_manager()); instantiation_set * s = uvar_inst_sets[m_var_j]; SASSERT(s != 0); - + enode_vector::const_iterator it = ctx->begin_enodes_of(m_f); enode_vector::const_iterator end = ctx->end_enodes_of(m_f); for (; it != end; it++) { @@ -1213,7 +1213,7 @@ namespace smt { if (ctx->is_relevant(n)) { enode * e_arg = n->get_arg(m_arg_i); expr * arg = e_arg->get_owner(); - s->insert(arg, e_arg->get_generation()); + s->insert(arg, e_arg->get_generation()); } } } @@ -1228,19 +1228,19 @@ namespace smt { } virtual ~f_var_plus_offset() {} - virtual char const * get_kind() const { - return "f_var_plus_offset"; + virtual char const * get_kind() const { + return "f_var_plus_offset"; } - + virtual bool is_equal(qinfo const * qi) const { if (qi->get_kind() != get_kind()) return false; f_var_plus_offset const * other = static_cast(qi); return m_f == other->m_f && m_arg_i == other->m_arg_i && m_var_j == other->m_var_j && m_offset.get() == other->m_offset.get(); } - + virtual void display(std::ostream & out) const { - out << "(" << m_f->get_name() << ":" << m_arg_i << " - " << + out << "(" << m_f->get_name() << ":" << m_arg_i << " - " << mk_bounded_pp(m_offset.get(), m_offset.get_manager()) << " -> v!" << m_var_j << ")"; } @@ -1344,11 +1344,11 @@ namespace smt { /** \brief auf_arr is a term (pattern) of the form: - + FORM := GROUND-TERM | (select FORM VAR) - - Store in arrays, all enodes that match the pattern + + Store in arrays, all enodes that match the pattern */ void get_auf_arrays(app * auf_arr, context * ctx, ptr_buffer & arrays) { if (is_ground(auf_arr)) { @@ -1375,10 +1375,10 @@ namespace smt { } } } - + class select_var : public qinfo { protected: - ast_manager & m_manager; + ast_manager & m_manager; array_util m_array; app * m_select; // It must satisfy is_auf_select... see bool is_auf_select(expr * t) const unsigned m_arg_i; @@ -1398,16 +1398,16 @@ namespace smt { virtual ~select_var() {} virtual char const * get_kind() const { - return "select_var"; + return "select_var"; } - + virtual bool is_equal(qinfo const * qi) const { if (qi->get_kind() != get_kind()) return false; select_var const * other = static_cast(qi); return m_select == other->m_select && m_arg_i == other->m_arg_i && m_var_j == other->m_var_j; } - + virtual void display(std::ostream & out) const { out << "(" << mk_bounded_pp(m_select, m_manager) << ":" << m_arg_i << " -> v!" << m_var_j << ")"; } @@ -1415,12 +1415,12 @@ namespace smt { virtual void process_auf(quantifier * q, auf_solver & s, context * ctx) { ptr_buffer arrays; get_auf_arrays(get_array(), ctx, arrays); - TRACE("select_var", + TRACE("select_var", tout << "enodes matching: "; display(tout); tout << "\n"; for (enode* n : arrays) { tout << "#" << n->get_owner()->get_id() << "\n" << mk_pp(n->get_owner(), m_manager) << "\n"; }); - node * n1 = s.get_uvar(q, m_var_j); + node * n1 = s.get_uvar(q, m_var_j); for (enode* n : arrays) { app * ground_array = n->get_owner(); func_decl * f = get_array_func_decl(ground_array, s); @@ -1443,7 +1443,7 @@ namespace smt { enode_vector::iterator it2 = curr->begin_parents(); enode_vector::iterator end2 = curr->end_parents(); for (; it2 != end2; ++it2) { - enode * p = *it2; + enode * p = *it2; if (ctx->is_relevant(p) && p->get_owner()->get_decl() == m_select->get_decl()) { SASSERT(m_arg_i < p->get_owner()->get_num_args()); enode * e_arg = p->get_arg(m_arg_i); @@ -1454,7 +1454,7 @@ namespace smt { } } }; - + class var_pair : public qinfo { protected: unsigned m_var_i; @@ -1464,16 +1464,16 @@ namespace smt { if (m_var_i > m_var_j) std::swap(m_var_i, m_var_j); } - + virtual ~var_pair() {} virtual bool is_equal(qinfo const * qi) const { if (qi->get_kind() != get_kind()) return false; var_pair const * other = static_cast(qi); - return m_var_i == other->m_var_i && m_var_j == other->m_var_j; + return m_var_i == other->m_var_i && m_var_j == other->m_var_j; } - + virtual void display(std::ostream & out) const { out << "(" << get_kind() << ":v!" << m_var_i << ":v!" << m_var_j << ")"; } @@ -1508,7 +1508,7 @@ namespace smt { n1->merge(n2); } }; - + class x_leq_y : public var_pair { public: x_leq_y(unsigned i, unsigned j):var_pair(i, j) {} @@ -1527,7 +1527,7 @@ namespace smt { public: x_sleq_y(unsigned i, unsigned j):x_leq_y(i, j) {} virtual char const * get_kind() const { return "x_sleq_y"; } - + virtual void process_auf(quantifier * q, auf_solver & s, context * ctx) { node * n1 = s.get_uvar(q, m_var_i); node * n2 = s.get_uvar(q, m_var_j); @@ -1536,7 +1536,7 @@ namespace smt { n1->set_signed_proj(); } }; - + class var_expr_pair : public qinfo { protected: unsigned m_var_i; @@ -1545,19 +1545,19 @@ namespace smt { var_expr_pair(ast_manager & m, unsigned i, expr * t): m_var_i(i), m_t(t, m) {} ~var_expr_pair() {} - + virtual bool is_equal(qinfo const * qi) const { if (qi->get_kind() != get_kind()) return false; var_expr_pair const * other = static_cast(qi); return m_var_i == other->m_var_i && m_t.get() == other->m_t.get(); } - + virtual void display(std::ostream & out) const { out << "(" << get_kind() << ":v!" << m_var_i << ":" << mk_bounded_pp(m_t.get(), m_t.get_manager()) << ")"; } }; - + class x_eq_t : public var_expr_pair { public: x_eq_t(ast_manager & m, unsigned i, expr * t): @@ -1605,7 +1605,7 @@ namespace smt { S_q_i->insert(m_t, 0); } }; - + class x_gle_t : public var_expr_pair { public: x_gle_t(ast_manager & m, unsigned i, expr * t): @@ -1648,16 +1648,16 @@ namespace smt { m_manager.inc_ref(m_cond); SASSERT(!m_hint || m_cond == 0); } - + ~cond_macro() { m_manager.dec_ref(m_def); m_manager.dec_ref(m_cond); } func_decl * get_f() const { return m_f; } - + expr * get_def() const { return m_def; } - + expr * get_cond() const { return m_cond; } bool is_unconditional() const { return m_cond == 0 || m_manager.is_true(m_cond); } @@ -1674,7 +1674,7 @@ namespace smt { out << "[" << m_f->get_name() << " -> " << mk_bounded_pp(m_def, m_manager, 6); if (m_hint) out << " *hint*"; - else + else out << " when " << mk_bounded_pp(m_cond, m_manager, 6); out << "] weight: " << m_weight; } @@ -1689,7 +1689,7 @@ namespace smt { // ----------------------------------- class quantifier_analyzer; - + /** \brief Store relevant information regarding a particular universal quantifier. This information is populated by quantifier_analyzer. @@ -1763,7 +1763,7 @@ namespace smt { tout << mk_pp(q, m) << "\n" << mk_pp(m_flat_q, m) << "\n";); SASSERT(!has_quantifiers(m_flat_q->get_expr())); } - + ~quantifier_info() { std::for_each(m_qinfo_vect.begin(), m_qinfo_vect.end(), delete_proc()); std::for_each(m_cond_macros.begin(), m_cond_macros.end(), delete_proc()); @@ -1773,7 +1773,7 @@ namespace smt { bool is_auf() const { return m_is_auf; } quantifier * get_flat_q() const { return m_flat_q; } - + bool unary_function_fragment() const { unsigned sz = m_ng_decls.size(); if (sz > 1) @@ -1857,7 +1857,7 @@ namespace smt { if (m_uvar_inst_sets != 0) return; m_uvar_inst_sets = alloc(ptr_vector); - for (qinfo* qi : m_qinfo_vect) + for (qinfo* qi : m_qinfo_vect) qi->populate_inst_sets(m_flat_q, m_the_one, *m_uvar_inst_sets, ctx); for (instantiation_set * s : *m_uvar_inst_sets) { if (s != 0) @@ -1881,7 +1881,7 @@ namespace smt { } } }; - + /** \brief Functor used to traverse/analyze a quantifier and fill the structure quantifier_info. @@ -1897,9 +1897,9 @@ namespace smt { quantifier_info * m_info; typedef enum { POS, NEG } polarity; - + polarity neg(polarity p) { return p == POS ? NEG : POS; } - + obj_hashtable m_pos_cache; obj_hashtable m_neg_cache; typedef std::pair entry; @@ -1935,22 +1935,22 @@ namespace smt { return m_mutil.is_times_minus_one(n, arg); } - bool is_le(expr * n) const { + bool is_le(expr * n) const { return m_mutil.is_le(n); } - + bool is_le_ge(expr * n) const { return m_mutil.is_le_ge(n); } - bool is_signed_le(expr * n) const { - return m_bv_util.is_bv_sle(n); + bool is_signed_le(expr * n) const { + return m_bv_util.is_bv_sle(n); } - - expr * mk_one(sort * s) { - return m_bv_util.is_bv_sort(s) ? m_bv_util.mk_numeral(rational(1), s) : m_arith_util.mk_numeral(rational(1), s); + + expr * mk_one(sort * s) { + return m_bv_util.is_bv_sort(s) ? m_bv_util.mk_numeral(rational(1), s) : m_arith_util.mk_numeral(rational(1), s); } - + void mk_sub(expr * t1, expr * t2, expr_ref & r) const { m_mutil.mk_sub(t1, t2, r); } @@ -2032,7 +2032,7 @@ namespace smt { v2 = to_var(rhs); return true; } - return + return (is_var_minus_var(lhs, v1, v2) && is_zero(rhs)) || (is_var_minus_var(rhs, v1, v2) && is_zero(lhs)); } @@ -2050,7 +2050,7 @@ namespace smt { return false; if (sign) { bool r = is_le_ge(atom) && is_var_and_ground(to_app(atom)->get_arg(0), to_app(atom)->get_arg(1), v, t); - CTRACE("is_x_gle_t", r, tout << "is_x_gle_t: " << mk_ismt2_pp(atom, m_manager) << "\n--->\n" + CTRACE("is_x_gle_t", r, tout << "is_x_gle_t: " << mk_ismt2_pp(atom, m_manager) << "\n--->\n" << mk_ismt2_pp(v, m_manager) << " " << mk_ismt2_pp(t, m_manager) << "\n"; tout << "sign: " << sign << "\n";); return r; @@ -2070,7 +2070,7 @@ namespace smt { mk_add(tmp, one, t); else mk_sub(tmp, one, t); - TRACE("is_x_gle_t", tout << "is_x_gle_t: " << mk_ismt2_pp(atom, m_manager) << "\n--->\n" + TRACE("is_x_gle_t", tout << "is_x_gle_t: " << mk_ismt2_pp(atom, m_manager) << "\n--->\n" << mk_ismt2_pp(v, m_manager) << " " << mk_ismt2_pp(t, m_manager) << "\n"; tout << "sign: " << sign << "\n";); return true; @@ -2084,19 +2084,19 @@ namespace smt { m_pos_cache.reset(); m_neg_cache.reset(); } - - obj_hashtable & get_cache(polarity pol) { - return pol == POS ? m_pos_cache : m_neg_cache; + + obj_hashtable & get_cache(polarity pol) { + return pol == POS ? m_pos_cache : m_neg_cache; } void visit_formula(expr * n, polarity pol) { if (is_ground(n)) return; // ground terms do not need to be visited. obj_hashtable & c = get_cache(pol); - if (!c.contains(n)) { - m_ftodo.push_back(entry(n, pol)); + if (!c.contains(n)) { + m_ftodo.push_back(entry(n, pol)); c.insert(n); - } + } } void visit_term(expr * n) { @@ -2106,7 +2106,7 @@ namespace smt { m_pos_cache.insert(n); } } - + /** \brief Process unintrepreted applications. */ @@ -2119,14 +2119,14 @@ namespace smt { insert_qinfo(alloc(f_var, t->get_decl(), i, to_var(arg)->get_idx())); continue; } - + var * v; expr_ref k(m_manager); if (is_var_plus_ground(arg, v, k)) { insert_qinfo(alloc(f_var_plus_offset, m_manager, t->get_decl(), i, v->get_idx(), k.get())); continue; } - + visit_term(arg); } } @@ -2135,9 +2135,9 @@ namespace smt { /** \brief A term \c t is said to be a auf_select if it is of ther form - + (select a i) Where: - + where a is ground or is_auf_select(a) == true and the indices are ground terms or variables. */ @@ -2181,11 +2181,11 @@ namespace smt { void process_app(app * t) { SASSERT(!is_ground(t)); - + if (t->get_family_id() != m_manager.get_basic_family_id()) { m_info->m_ng_decls.insert(t->get_decl()); } - + if (is_uninterp(t)) { process_u_app(t); } @@ -2193,19 +2193,19 @@ namespace smt { process_i_app(t); } } - + void process_terms_on_stack() { while (!m_ttodo.empty()) { expr * curr = m_ttodo.back(); m_ttodo.pop_back(); - + if (m_manager.is_bool(curr)) { // formula nested in a term. visit_formula(curr, POS); visit_formula(curr, NEG); continue; } - + if (is_app(curr)) { process_app(to_app(curr)); } @@ -2223,7 +2223,7 @@ namespace smt { CTRACE("model_finder_bug", is_ground(atom), tout << mk_pp(atom, m_manager) << "\n";); SASSERT(!is_ground(atom)); SASSERT(m_manager.is_bool(atom)); - + if (is_var(atom)) { if (sign) { // atom (not X) can be viewed as X != true @@ -2235,7 +2235,7 @@ namespace smt { } return; } - + if (is_app(atom)) { var * v, * v1, * v2; expr_ref t(m_manager); @@ -2267,18 +2267,18 @@ namespace smt { } return; } - + SASSERT(is_quantifier(atom)); UNREACHABLE(); } - void process_literal(expr * atom, polarity pol) { - process_literal(atom, pol == NEG); + void process_literal(expr * atom, polarity pol) { + process_literal(atom, pol == NEG); } - + void process_or(app * n, polarity p) { unsigned num_args = n->get_num_args(); - for (unsigned i = 0; i < num_args; i++) + for (unsigned i = 0; i < num_args; i++) visit_formula(n->get_arg(i), p); } @@ -2299,7 +2299,7 @@ namespace smt { void checkpoint() { m_mf.checkpoint("quantifier_analyzer"); } - + void process_formulas_on_stack() { while (!m_ftodo.empty()) { checkpoint(); @@ -2359,7 +2359,7 @@ namespace smt { SASSERT(m_manager.is_bool(n)); visit_formula(n, POS); } - + void process_clause(expr * cls) { SASSERT(is_clause(m_manager, cls)); unsigned num_lits = get_clause_num_literals(m_manager, cls); @@ -2379,13 +2379,13 @@ namespace smt { m_mutil.collect_macro_candidates(q, candidates); unsigned num_candidates = candidates.size(); for (unsigned i = 0; i < num_candidates; i++) { - cond_macro * m = alloc(cond_macro, m_manager, candidates.get_f(i), candidates.get_def(i), candidates.get_cond(i), + cond_macro * m = alloc(cond_macro, m_manager, candidates.get_f(i), candidates.get_def(i), candidates.get_cond(i), candidates.ineq(i), candidates.satisfy_atom(i), candidates.hint(i), q->get_weight()); m_info->insert_macro(m); } } - - + + public: quantifier_analyzer(model_finder& mf, ast_manager & m): m_mf(mf), @@ -2396,8 +2396,8 @@ namespace smt { m_bv_util(m), m_info(0) { } - - + + void operator()(quantifier_info * d) { m_info = d; quantifier * q = d->get_flat_q(); @@ -2406,7 +2406,7 @@ namespace smt { reset_cache(); SASSERT(m_ttodo.empty()); SASSERT(m_ftodo.empty()); - + if (is_clause(m_manager, e)) { process_clause(e); } @@ -2420,7 +2420,7 @@ namespace smt { } collect_macro_candidates(q); - + m_info = 0; } @@ -2460,7 +2460,7 @@ namespace smt { m_q2info(q2i), m_model(0) { } - + virtual ~base_macro_solver() {} /** @@ -2478,13 +2478,13 @@ namespace smt { } }; - + /** \brief The simple macro solver satisfies quantifiers that contain (conditional) macros for a function f that does not occur in any other quantifier. - + Since f does not occur in any other quantifier, I don't need to track the dependencies - of f. That is, recursive definition cannot be created. + of f. That is, recursive definition cannot be created. */ class simple_macro_solver : public base_macro_solver { protected: @@ -2519,7 +2519,7 @@ namespace smt { // I know the (partial) interpretation of f satisfied the ground part. // MBQI will force extra instantiations if the the (partial) interpretation of f // does not satisfy the quantifier. - // In all other cases the "else" of f will satisfy the quantifier. + // In all other cases the "else" of f will satisfy the quantifier. set_else_interp(f, f_else); TRACE("model_finder", tout << "satisfying the quantifier using simple macro:\n"; m->display(tout); tout << "\n";); @@ -2555,7 +2555,7 @@ namespace smt { Let Q_{f_i = def_i} be the set of quantifiers where f_i = def_i is a macro. Then, the set Q can be satisfied using f_1 = def_1 ... f_n = d_n when - + Q_{f_1} union ... union Q_{f_n} = Q_{f_1 = def_1} ... Q_{f_n = d_n} (*) So, given a set of macros f_1 = def_1, ..., f_n = d_n, it is very easy to check @@ -2591,8 +2591,8 @@ namespace smt { typedef obj_pair_map q_f_def; typedef obj_pair_hashtable f_def_set; typedef obj_hashtable expr_set; - typedef obj_map f2defs; - + typedef obj_map f2defs; + q_f m_q_f; q_f_def m_q_f_def; ptr_vector m_qsets; @@ -2728,14 +2728,14 @@ namespace smt { } } } - + static void display_quantifier_set(std::ostream & out, quantifier_set const * s) { for (quantifier* q : *s) { out << q->get_qid() << " "; } out << "\n"; } - + void display_qcandidates(std::ostream & out, ptr_vector const & qcandidates) const { for (quantifier * q : qcandidates) { out << q->get_qid() << " ->\n" << mk_pp(q, m_manager) << "\n"; @@ -2757,14 +2757,14 @@ namespace smt { out << f->get_name() << " " << mk_pp(def, m_manager) << " ->\n"; display_quantifier_set(out, s); } } - + // // Search: main procedures // struct ev_handler { hint_solver * m_owner; - + void operator()(quantifier * q, bool ins) { quantifier_info * qi = m_owner->get_qinfo(q); qi->set_the_one(0); @@ -2777,7 +2777,7 @@ namespace smt { typedef backtrackable_set qset; - typedef backtrackable_set qsset; + typedef backtrackable_set qsset; typedef obj_map f2def; qset m_residue; @@ -2801,7 +2801,7 @@ namespace smt { } out << "\n"; } - + bool check_satisfied_residue_invariant() { DEBUG_CODE( for (quantifier * q : m_satisfied) { @@ -2813,7 +2813,7 @@ namespace smt { return true; } - + bool update_satisfied_residue(func_decl * f, expr * def) { bool useful = false; SASSERT(check_satisfied_residue_invariant()); @@ -2839,7 +2839,7 @@ namespace smt { SASSERT(check_satisfied_residue_invariant()); return true; } - + /** \brief Extract from m_residue, func_decls that can be used as macros to satisfy it. The candidates must not be elements of m_fs. @@ -2869,13 +2869,13 @@ namespace smt { if (depth >= GREEDY_MAX_DEPTH) return; // failed - TRACE("model_finder_hint", + TRACE("model_finder_hint", tout << "greedy depth: " << depth << ", f: " << f->get_name() << "\n"; display_search_state(tout);); expr_set * s = get_f_defs(f); for (expr * def : *s) { - + SASSERT(!m_fs.contains(f)); m_satisfied.push_scope(); @@ -2887,7 +2887,7 @@ namespace smt { greedy(depth + 1); // greedy throws exception in case of success // reachable iff greedy failed. } - + m_satisfied.pop_scope(); m_residue.pop_scope(); m_fs.erase(f); @@ -2900,7 +2900,7 @@ namespace smt { */ void greedy(unsigned depth) { if (m_residue.empty()) { - TRACE("model_finder_hint", + TRACE("model_finder_hint", tout << "found subset that is satisfied by macros\n"; display_search_state(tout);); throw found_satisfied_subset(); @@ -2946,7 +2946,7 @@ namespace smt { quantifiers in m_satisfied. */ void set_interp() { - for (auto const& kv : m_fs) { + for (auto const& kv : m_fs) { func_decl * f = kv.m_key; expr * def = kv.m_value; set_else_interp(f, def); @@ -3034,7 +3034,7 @@ namespace smt { return true; return false; } - + cond_macro * get_macro_for(func_decl * f, quantifier * q) { cond_macro * r = 0; quantifier_info * qi = get_qinfo(q); @@ -3153,10 +3153,10 @@ namespace smt { } }; }; - + // ----------------------------------- // - // model finder + // model finder // // ----------------------------------- @@ -3171,11 +3171,11 @@ namespace smt { m_nm_solver(alloc(non_auf_macro_solver, m, m_q2info, m_dependencies)), m_new_constraints(m) { } - + model_finder::~model_finder() { reset(); } - + void model_finder::checkpoint() { checkpoint("model_finder"); } @@ -3192,14 +3192,14 @@ namespace smt { SASSERT(info != 0); return info; } - + void model_finder::set_context(context * ctx) { - SASSERT(m_context == 0); + SASSERT(m_context == 0); m_context = ctx; m_auf_solver->set_context(ctx); m_nm_solver->set_params(ctx->get_fparams()); } - + void model_finder::register_quantifier(quantifier * q) { TRACE("model_finder", tout << "registering:\n" << mk_pp(q, m_manager) << "\n";); quantifier_info * new_info = alloc(quantifier_info, *this, m_manager, q); @@ -3208,15 +3208,15 @@ namespace smt { m_analyzer->operator()(new_info); TRACE("model_finder", tout << "after analyzer:\n"; new_info->display(tout);); } - + void model_finder::push_scope() { m_scopes.push_back(scope()); scope & s = m_scopes.back(); s.m_quantifiers_lim = m_quantifiers.size(); } - + void model_finder::restore_quantifiers(unsigned old_size) { - unsigned curr_size = m_quantifiers.size(); + unsigned curr_size = m_quantifiers.size(); SASSERT(old_size <= curr_size); for (unsigned i = old_size; i < curr_size; i++) { quantifier * q = m_quantifiers[i]; @@ -3227,7 +3227,7 @@ namespace smt { } m_quantifiers.shrink(old_size); } - + void model_finder::pop_scope(unsigned num_scopes) { unsigned lvl = m_scopes.size(); SASSERT(num_scopes <= lvl); @@ -3236,7 +3236,7 @@ namespace smt { restore_quantifiers(s.m_quantifiers_lim); m_scopes.shrink(new_lvl); } - + void model_finder::reset() { m_scopes.reset(); m_dependencies.reset(); @@ -3244,7 +3244,7 @@ namespace smt { SASSERT(m_q2info.empty()); SASSERT(m_quantifiers.empty()); } - + void model_finder::init_search_eh() { // do nothing in the current version } @@ -3266,12 +3266,12 @@ namespace smt { } m_auf_solver->mk_instantiation_sets(); - for (quantifier * q : qs) { + for (quantifier * q : qs) { quantifier_info * qi = get_quantifier_info(q); qi->populate_inst_sets(*(m_auf_solver.get()), m_context); } m_auf_solver->fix_model(m_new_constraints); - TRACE("model_finder", + TRACE("model_finder", for (quantifier * q : qs) { quantifier_info * qi = get_quantifier_info(q); quantifier * fq = qi->get_flat_q(); @@ -3293,7 +3293,7 @@ namespace smt { qs.swap(new_qs); TRACE("model_finder", tout << "model after processing simple macros:\n"; model_pp(tout, *m);); } - + void model_finder::process_non_auf_macros(ptr_vector & qs, ptr_vector & residue, proto_model * m) { ptr_vector new_qs; m_nm_solver->operator()(m, qs, new_qs, residue); @@ -3355,12 +3355,12 @@ namespace smt { << "\ni: " << i << " " << flat_q->get_num_decls() - q->get_num_decls() + i << "\n";); if (r != 0) return r; - // quantifier was not processed by AUF solver... + // quantifier was not processed by AUF solver... // it must have been satisfied by "macro"/"hint". quantifier_info * qinfo = get_quantifier_info(q); SASSERT(qinfo); SASSERT(qinfo->get_the_one() != 0); - + return qinfo->get_macro_based_inst_set(i, m_context, *(m_auf_solver.get())); } @@ -3381,11 +3381,11 @@ namespace smt { } return t; } - + /** \brief Assert constraints restricting the possible values of the skolem constants can be assigned to. The idea is to restrict them to the values in the instantiation sets. - + \remark q is the quantifier before flattening. Return true if something was asserted. @@ -3433,7 +3433,7 @@ namespace smt { TRACE("model_finder_bug_detail", tout << "asserting new constraint: " << mk_pp(c, m_manager) << "\n";); m_context->internalize(c, true); literal l(m_context->get_literal(c)); - m_context->mark_as_relevant(l); + m_context->mark_as_relevant(l); // asserting it as an AXIOM m_context->assign(l, b_justification()); } diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp index 3832339a8..3a482f37c 100644 --- a/src/tactic/ufbv/macro_finder_tactic.cpp +++ b/src/tactic/ufbv/macro_finder_tactic.cpp @@ -22,48 +22,52 @@ Notes: #include "tactic/extension_model_converter.h" #include "tactic/ufbv/macro_finder_tactic.h" -class macro_finder_tactic : public tactic { +class macro_finder_tactic : public tactic { struct imp { ast_manager & m_manager; bool m_elim_and; - imp(ast_manager & m, params_ref const & p) : + imp(ast_manager & m, params_ref const & p) : m_manager(m), m_elim_and(false) { updt_params(p); } - + ast_manager & m() const { return m_manager; } - - - void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, + + + void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); mc = 0; pc = 0; core = 0; tactic_report report("macro-finder", *g); - fail_if_unsat_core_generation("macro-finder", g); bool produce_proofs = g->proofs_enabled(); + bool unsat_core_enabled = g->unsat_core_enabled(); macro_manager mm(m_manager); macro_finder mf(m_manager, mm); - + expr_ref_vector forms(m_manager), new_forms(m_manager); - proof_ref_vector proofs(m_manager), new_proofs(m_manager); - unsigned size = g->size(); + proof_ref_vector proofs(m_manager), new_proofs(m_manager); + expr_dependency_ref_vector deps(m_manager), new_deps(m_manager); + unsigned size = g->size(); for (unsigned idx = 0; idx < size; idx++) { forms.push_back(g->form(idx)); - proofs.push_back(g->pr(idx)); + proofs.push_back(g->pr(idx)); + deps.push_back(g->dep(idx)); } - mf(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs); - + mf(forms.size(), forms.c_ptr(), proofs.c_ptr(), deps.c_ptr(), new_forms, new_proofs, new_deps); + g->reset(); for (unsigned i = 0; i < new_forms.size(); i++) - g->assert_expr(new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0); + g->assert_expr(new_forms.get(i), + produce_proofs ? new_proofs.get(i) : 0, + unsat_core_enabled ? new_deps.get(i) : 0); extension_model_converter * evmc = alloc(extension_model_converter, mm.get_manager()); unsigned num = mm.get_num_macros(); @@ -73,7 +77,7 @@ class macro_finder_tactic : public tactic { evmc->insert(f, f_interp); } mc = evmc; - + g->inc_depth(); result.push_back(g.get()); TRACE("macro-finder", g->display(tout);); @@ -86,7 +90,7 @@ class macro_finder_tactic : public tactic { }; imp * m_imp; - params_ref m_params; + params_ref m_params; public: macro_finder_tactic(ast_manager & m, params_ref const & p): m_params(p) { @@ -96,7 +100,7 @@ public: virtual tactic * translate(ast_manager & m) { return alloc(macro_finder_tactic, m, m_params); } - + virtual ~macro_finder_tactic() { dealloc(m_imp); } @@ -112,19 +116,19 @@ public: insert_produce_proofs(r); r.insert("elim_and", CPK_BOOL, "(default: false) eliminate conjunctions during (internal) calls to the simplifier."); } - - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, + + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { (*m_imp)(in, result, mc, pc, core); } - + virtual void cleanup() { ast_manager & m = m_imp->m(); imp * d = alloc(imp, m, m_params); - std::swap(d, m_imp); + std::swap(d, m_imp); dealloc(d); } diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp index 8196dc664..925b5a5e3 100644 --- a/src/tactic/ufbv/quasi_macros_tactic.cpp +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -31,49 +31,55 @@ class quasi_macros_tactic : public tactic { imp(ast_manager & m, params_ref const & p) : m_manager(m) { updt_params(p); } - + ast_manager & m() const { return m_manager; } - - - void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, + + + void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); mc = 0; pc = 0; core = 0; tactic_report report("quasi-macros", *g); - fail_if_unsat_core_generation("quasi-macros", g); bool produce_proofs = g->proofs_enabled(); + bool produce_unsat_cores = g->unsat_core_enabled(); macro_manager mm(m_manager); quasi_macros qm(m_manager, mm); bool more = true; - + expr_ref_vector forms(m_manager), new_forms(m_manager); proof_ref_vector proofs(m_manager), new_proofs(m_manager); + expr_dependency_ref_vector deps(m_manager), new_deps(m_manager); unsigned size = g->size(); for (unsigned i = 0; i < size; i++) { forms.push_back(g->form(i)); proofs.push_back(g->pr(i)); + deps.push_back(g->dep(i)); } - + while (more) { // CMW: use repeat(...) ? if (m().canceled()) throw tactic_exception(m().limit().get_cancel_msg()); - + new_forms.reset(); new_proofs.reset(); - more = qm(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs); + new_deps.reset(); + more = qm(forms.size(), forms.c_ptr(), proofs.c_ptr(), deps.c_ptr(), new_forms, new_proofs, new_deps); forms.swap(new_forms); - proofs.swap(new_proofs); + proofs.swap(new_proofs); + deps.swap(new_deps); } g->reset(); for (unsigned i = 0; i < new_forms.size(); i++) - g->assert_expr(new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0); + g->assert_expr(forms.get(i), + produce_proofs ? proofs.get(i) : 0, + produce_unsat_cores ? deps.get(i) : 0); extension_model_converter * evmc = alloc(extension_model_converter, mm.get_manager()); unsigned num = mm.get_num_macros(); @@ -93,7 +99,7 @@ class quasi_macros_tactic : public tactic { void updt_params(params_ref const & p) { } }; - + imp * m_imp; params_ref m_params; @@ -106,7 +112,7 @@ public: virtual tactic * translate(ast_manager & m) { return alloc(quasi_macros_tactic, m, m_params); } - + virtual ~quasi_macros_tactic() { dealloc(m_imp); } @@ -121,19 +127,19 @@ public: insert_produce_models(r); insert_produce_proofs(r); } - - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, + + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { (*m_imp)(in, result, mc, pc, core); } - + virtual void cleanup() { ast_manager & m = m_imp->m(); imp * d = alloc(imp, m, m_params); - std::swap(d, m_imp); + std::swap(d, m_imp); dealloc(d); }