diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index 34d295898..fc075af6e 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -164,8 +164,8 @@ extern "C" { return ""; } std::string s = str.as_string(); - *length = static_cast(s.size()); - return mk_c(c)->mk_external_string(s.c_str(), s.size()); + *length = (unsigned)(s.size()); + return mk_c(c)->mk_external_string(s.c_str(), *length); Z3_CATCH_RETURN(""); } diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index 130184a6e..2900aea85 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -188,6 +188,14 @@ public: return m_manager.mk_app(m_fid, OP_SELECT, 0, nullptr, num_args, args); } + app * mk_select(ptr_vector const& args) { + return mk_select(args.size(), args.c_ptr()); + } + + app * mk_select(expr_ref_vector const& args) { + return mk_select(args.size(), args.c_ptr()); + } + app * mk_map(func_decl * f, unsigned num_args, expr * const * args) { parameter p(f); return m_manager.mk_app(m_fid, OP_ARRAY_MAP, 1, &p, num_args, args); @@ -229,6 +237,10 @@ public: return m_manager.mk_app(m_fid, OP_SET_HAS_SIZE, set, n); } + app* mk_card(expr* set) { + return m_manager.mk_app(m_fid, OP_SET_CARD, set); + } + func_decl * mk_array_ext(sort* domain, unsigned i); sort * mk_array_sort(sort* dom, sort* range) { return mk_array_sort(1, &dom, range); } diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 9d5c50827..2fe59d608 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -738,7 +738,13 @@ basic_decl_plugin::basic_decl_plugin(): m_iff_oeq_decl(nullptr), m_skolemize_decl(nullptr), m_mp_oeq_decl(nullptr), - m_hyper_res_decl0(nullptr) { + m_hyper_res_decl0(nullptr), + m_assumption_add_decl(nullptr), + m_lemma_add_decl(nullptr), + m_th_assumption_add_decl(nullptr), + m_th_lemma_add_decl(nullptr), + m_redundant_del_decl(nullptr), + m_clause_trail_decl(nullptr) { } bool basic_decl_plugin::check_proof_sorts(basic_op_kind k, unsigned arity, sort * const * domain) const { @@ -908,6 +914,12 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren case PR_MODUS_PONENS_OEQ: return mk_proof_decl("mp~", k, 2, m_mp_oeq_decl); case PR_TH_LEMMA: return mk_proof_decl("th-lemma", k, num_parents, m_th_lemma_decls); case PR_HYPER_RESOLVE: return mk_proof_decl("hyper-res", k, num_parents, m_hyper_res_decl0); + case PR_ASSUMPTION_ADD: return mk_proof_decl("add-assume", k, num_parents, m_assumption_add_decl); + case PR_LEMMA_ADD: return mk_proof_decl("add-lemma", k, num_parents, m_lemma_add_decl); + case PR_TH_ASSUMPTION_ADD: return mk_proof_decl("add-th-assume", k, num_parents, m_th_assumption_add_decl); + case PR_TH_LEMMA_ADD: return mk_proof_decl("add-th-lemma", k, num_parents, m_th_lemma_add_decl); + case PR_REDUNDANT_DEL: return mk_proof_decl("del-redundant", k, num_parents, m_redundant_del_decl); + case PR_CLAUSE_TRAIL: return mk_proof_decl("proof-trail", k, num_parents, m_clause_trail_decl); default: UNREACHABLE(); return nullptr; @@ -1023,6 +1035,12 @@ void basic_decl_plugin::finalize() { DEC_REF(m_iff_oeq_decl); DEC_REF(m_skolemize_decl); DEC_REF(m_mp_oeq_decl); + DEC_REF(m_assumption_add_decl); + DEC_REF(m_lemma_add_decl); + DEC_REF(m_th_assumption_add_decl); + DEC_REF(m_th_lemma_add_decl); + DEC_REF(m_redundant_del_decl); + DEC_REF(m_clause_trail_decl); DEC_ARRAY_REF(m_apply_def_decls); DEC_ARRAY_REF(m_nnf_pos_decls); DEC_ARRAY_REF(m_nnf_neg_decls); @@ -3277,6 +3295,39 @@ proof * ast_manager::mk_not_or_elim(proof * p, unsigned i) { return mk_app(m_basic_family_id, PR_NOT_OR_ELIM, p, f); } +proof* ast_manager::mk_clause_trail_elem(proof *pr, expr* e, decl_kind k) { + ptr_buffer args; + if (pr) args.push_back(pr); + args.push_back(e); + return mk_app(m_basic_family_id, k, 0, nullptr, args.size(), args.c_ptr()); +} + +proof * ast_manager::mk_assumption_add(proof* pr, expr* e) { + return mk_clause_trail_elem(pr, e, PR_ASSUMPTION_ADD); +} + +proof * ast_manager::mk_lemma_add(proof* pr, expr* e) { + return mk_clause_trail_elem(pr, e, PR_LEMMA_ADD); +} + +proof * ast_manager::mk_th_assumption_add(proof* pr, expr* e) { + return mk_clause_trail_elem(pr, e, PR_TH_ASSUMPTION_ADD); +} + +proof * ast_manager::mk_th_lemma_add(proof* pr, expr* e) { + return mk_clause_trail_elem(pr, e, PR_TH_LEMMA_ADD); +} + +proof * ast_manager::mk_redundant_del(expr* e) { + return mk_clause_trail_elem(nullptr, e, PR_REDUNDANT_DEL); +} + +proof * ast_manager::mk_clause_trail(unsigned n, proof* const* ps) { + ptr_buffer args; + args.append(n, (expr**) ps); + args.push_back(mk_false()); + return mk_app(m_basic_family_id, PR_CLAUSE_TRAIL, 0, nullptr, args.size(), args.c_ptr()); +} proof * ast_manager::mk_th_lemma( family_id tid, diff --git a/src/ast/ast.h b/src/ast/ast.h index e654ef1d6..a551b8928 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -19,6 +19,7 @@ Revision History: #ifndef AST_H_ #define AST_H_ + #include "util/vector.h" #include "util/hashtable.h" #include "util/buffer.h" @@ -1105,6 +1106,8 @@ enum basic_op_kind { PR_HYPOTHESIS, PR_LEMMA, PR_UNIT_RESOLUTION, PR_IFF_TRUE, PR_IFF_FALSE, PR_COMMUTATIVITY, PR_DEF_AXIOM, + PR_ASSUMPTION_ADD, PR_TH_ASSUMPTION_ADD, PR_LEMMA_ADD, PR_TH_LEMMA_ADD, PR_REDUNDANT_DEL, PR_CLAUSE_TRAIL, + PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_SKOLEMIZE, PR_MODUS_PONENS_OEQ, PR_TH_LEMMA, PR_HYPER_RESOLVE, LAST_BASIC_PR }; @@ -1159,6 +1162,12 @@ protected: func_decl * m_iff_oeq_decl; func_decl * m_skolemize_decl; func_decl * m_mp_oeq_decl; + func_decl * m_assumption_add_decl; + func_decl * m_lemma_add_decl; + func_decl * m_th_assumption_add_decl; + func_decl * m_th_lemma_add_decl; + func_decl * m_redundant_del_decl; + func_decl * m_clause_trail_decl; ptr_vector m_apply_def_decls; ptr_vector m_nnf_pos_decls; ptr_vector m_nnf_neg_decls; @@ -2298,6 +2307,14 @@ public: proof * mk_der(quantifier * q, expr * r); proof * mk_quant_inst(expr * not_q_or_i, unsigned num_bind, expr* const* binding); + proof * mk_clause_trail_elem(proof* p, expr* e, decl_kind k); + proof * mk_assumption_add(proof* pr, expr* e); + proof * mk_lemma_add(proof* pr, expr* e); + proof * mk_th_assumption_add(proof* pr, expr* e); + proof * mk_th_lemma_add(proof* pr, expr* e); + proof * mk_redundant_del(expr* e); + proof * mk_clause_trail(unsigned n, proof* const* ps); + proof * mk_def_axiom(expr * ax); proof * mk_unit_resolution(unsigned num_proofs, proof * const * proofs); proof * mk_unit_resolution(unsigned num_proofs, proof * const * proofs, expr * new_fact); diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index f148fb608..32ba18870 100644 --- a/src/smt/CMakeLists.txt +++ b/src/smt/CMakeLists.txt @@ -18,6 +18,7 @@ z3_add_component(smt smt_cg_table.cpp smt_checker.cpp smt_clause.cpp + smt_clause_proof.cpp smt_conflict_resolution.cpp smt_consequences.cpp smt_context.cpp diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp index a006c9dd5..b9bb54f0d 100644 --- a/src/smt/dyn_ack.cpp +++ b/src/smt/dyn_ack.cpp @@ -374,7 +374,7 @@ namespace smt { justification * js = nullptr; if (m_manager.proofs_enabled()) js = alloc(dyn_ack_justification, n1, n2); - clause * cls = m_context.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, del_eh); + clause * cls = m_context.mk_clause(lits.size(), lits.c_ptr(), js, CLS_TH_LEMMA, del_eh); if (!cls) { dealloc(del_eh); return; @@ -426,7 +426,7 @@ namespace smt { justification * js = nullptr; if (m_manager.proofs_enabled()) js = alloc(dyn_ack_justification, n1, n2); - clause * cls = m_context.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, del_eh); + clause * cls = m_context.mk_clause(lits.size(), lits.c_ptr(), js, CLS_TH_LEMMA, del_eh); if (!cls) { dealloc(del_eh); return; diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 650afda25..4b42e0339 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -27,6 +27,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_random_seed = p.random_seed(); m_relevancy_lvl = p.relevancy(); m_ematching = p.ematching(); + m_clause_proof = p.clause_proof(); m_phase_selection = static_cast(p.phase_selection()); m_restart_strategy = static_cast(p.restart_strategy()); m_restart_factor = p.restart_factor(); @@ -107,6 +108,7 @@ void smt_params::display(std::ostream & out) const { DISPLAY_PARAM(m_display_features); DISPLAY_PARAM(m_new_core2th_eq); DISPLAY_PARAM(m_ematching); + DISPLAY_PARAM(m_clause_proof); DISPLAY_PARAM(m_case_split_strategy); DISPLAY_PARAM(m_rel_case_split_order); diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 8901697b7..b4423f933 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -107,6 +107,7 @@ struct smt_params : public preprocessor_params, bool m_display_features; bool m_new_core2th_eq; bool m_ematching; + bool m_clause_proof; // ----------------------------------- // @@ -261,6 +262,7 @@ struct smt_params : public preprocessor_params, m_display_features(false), m_new_core2th_eq(true), m_ematching(true), + m_clause_proof(false), m_case_split_strategy(CS_ACTIVITY_DELAY_NEW), m_rel_case_split_order(0), m_lookahead_diseq(false), diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 8eac65587..41adc907e 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -60,6 +60,7 @@ def_module_params(module_name='smt', ('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'), ('array.weak', BOOL, False, 'weak array theory'), ('array.extensional', BOOL, True, 'extensional array theory'), + ('clause_proof', BOOL, False, 'record a clausal proof'), ('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'), ('dack.eq', BOOL, False, 'enable dynamic ackermannization for transtivity of equalities'), ('dack.factor', DOUBLE, 0.1, 'number of instance per conflict'), diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index 88d1f73e7..9048a0893 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -29,15 +29,15 @@ namespace smt { qi_queue::qi_queue(quantifier_manager & qm, context & ctx, qi_params & params): m_qm(qm), m_context(ctx), - m_manager(m_context.get_manager()), + m(m_context.get_manager()), m_params(params), m_checker(m_context), - m_cost_function(m_manager), - m_new_gen_function(m_manager), - m_parser(m_manager), - m_evaluator(m_manager), - m_subst(m_manager), - m_instances(m_manager) { + m_cost_function(m), + m_new_gen_function(m), + m_parser(m), + m_evaluator(m), + m_subst(m), + m_instances(m) { init_parser_vars(); m_vals.resize(15, 0.0f); } @@ -158,11 +158,11 @@ namespace smt { } else if (m_params.m_qi_promote_unsat && m_checker.is_unsat(qa->get_expr(), f->get_num_args(), f->get_args())) { // do not delay instances that produce a conflict. - TRACE("qi_unsat", tout << "promoting instance that produces a conflict\n" << mk_pp(qa, m_manager) << "\n";); + TRACE("qi_unsat", tout << "promoting instance that produces a conflict\n" << mk_pp(qa, m) << "\n";); instantiate(curr); } else { - TRACE("qi_queue", tout << "delaying quantifier instantiation... " << f << "\n" << mk_pp(qa, m_manager) << "\ncost: " << curr.m_cost << "\n";); + TRACE("qi_queue", tout << "delaying quantifier instantiation... " << f << "\n" << mk_pp(qa, m) << "\ncost: " << curr.m_cost << "\n";); m_delayed_entries.push_back(curr); } @@ -179,13 +179,13 @@ namespace smt { } void qi_queue::display_instance_profile(fingerprint * f, quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned proof_id, unsigned generation) { - if (m_manager.has_trace_stream()) { - m_manager.trace_stream() << "[instance] "; - m_manager.trace_stream() << static_cast(f); - if (m_manager.proofs_enabled()) - m_manager.trace_stream() << " #" << proof_id; - m_manager.trace_stream() << " ; " << generation; - m_manager.trace_stream() << "\n"; + if (m.has_trace_stream()) { + m.trace_stream() << "[instance] "; + m.trace_stream() << static_cast(f); + if (m.proofs_enabled()) + m.trace_stream() << " #" << proof_id; + m.trace_stream() << " ; " << generation; + m.trace_stream() << "\n"; } } @@ -204,21 +204,21 @@ namespace smt { TRACE("checker", tout << "instance already satisfied\n";); return; } - expr_ref instance(m_manager); + expr_ref instance(m); m_subst(q, num_bindings, bindings, instance); - TRACE("qi_queue", tout << "new instance:\n" << mk_pp(instance, m_manager) << "\n";); - TRACE("qi_queue_instance", tout << "new instance:\n" << mk_pp(instance, m_manager) << "\n";); - expr_ref s_instance(m_manager); - proof_ref pr(m_manager); + TRACE("qi_queue", tout << "new instance:\n" << mk_pp(instance, m) << "\n";); + TRACE("qi_queue_instance", tout << "new instance:\n" << mk_pp(instance, m) << "\n";); + expr_ref s_instance(m); + proof_ref pr(m); m_context.get_rewriter()(instance, s_instance, pr); TRACE("qi_queue_bug", tout << "new instance after simplification:\n" << s_instance << "\n";); - if (m_manager.is_true(s_instance)) { - TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m_manager);); + if (m.is_true(s_instance)) { + TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m);); - if (m_manager.has_trace_stream()) { + if (m.has_trace_stream()) { display_instance_profile(f, q, num_bindings, bindings, pr->get_id(), generation); - m_manager.trace_stream() << "[end-of-instance]\n"; + m.trace_stream() << "[end-of-instance]\n"; } return; @@ -228,51 +228,51 @@ namespace smt { if (stat->get_num_instances() % m_params.m_qi_profile_freq == 0) { m_qm.display_stats(verbose_stream(), q); } - expr_ref lemma(m_manager); - if (m_manager.is_or(s_instance)) { + expr_ref lemma(m); + if (m.is_or(s_instance)) { ptr_vector args; - args.push_back(m_manager.mk_not(q)); + args.push_back(m.mk_not(q)); args.append(to_app(s_instance)->get_num_args(), to_app(s_instance)->get_args()); - lemma = m_manager.mk_or(args.size(), args.c_ptr()); + lemma = m.mk_or(args.size(), args.c_ptr()); } - else if (m_manager.is_false(s_instance)) { - lemma = m_manager.mk_not(q); + else if (m.is_false(s_instance)) { + lemma = m.mk_not(q); } - else if (m_manager.is_true(s_instance)) { + else if (m.is_true(s_instance)) { lemma = s_instance; } else { - lemma = m_manager.mk_or(m_manager.mk_not(q), s_instance); + lemma = m.mk_or(m.mk_not(q), s_instance); } m_instances.push_back(lemma); - proof_ref pr1(m_manager); + proof_ref pr1(m); unsigned proof_id = 0; - if (m_manager.proofs_enabled()) { - expr_ref_vector bindings_e(m_manager); + if (m.proofs_enabled()) { + expr_ref_vector bindings_e(m); for (unsigned i = 0; i < num_bindings; ++i) { bindings_e.push_back(bindings[i]->get_owner()); } - app * bare_lemma = m_manager.mk_or(m_manager.mk_not(q), instance); - proof * qi_pr = m_manager.mk_quant_inst(bare_lemma, num_bindings, bindings_e.c_ptr()); + app * bare_lemma = m.mk_or(m.mk_not(q), instance); + proof * qi_pr = m.mk_quant_inst(bare_lemma, num_bindings, bindings_e.c_ptr()); proof_id = qi_pr->get_id(); if (bare_lemma == lemma) { pr1 = qi_pr; } else if (instance == s_instance) { - proof * rw = m_manager.mk_rewrite(bare_lemma, lemma); - pr1 = m_manager.mk_modus_ponens(qi_pr, rw); + proof * rw = m.mk_rewrite(bare_lemma, lemma); + pr1 = m.mk_modus_ponens(qi_pr, rw); } else { - app * bare_s_lemma = m_manager.mk_or(m_manager.mk_not(q), s_instance); + app * bare_s_lemma = m.mk_or(m.mk_not(q), s_instance); proof * prs[1] = { pr.get() }; - proof * cg = m_manager.mk_congruence(bare_lemma, bare_s_lemma, 1, prs); - proof * rw = m_manager.mk_rewrite(bare_s_lemma, lemma); - proof * tr = m_manager.mk_transitivity(cg, rw); - pr1 = m_manager.mk_modus_ponens(qi_pr, tr); + proof * cg = m.mk_congruence(bare_lemma, bare_s_lemma, 1, prs); + proof * rw = m.mk_rewrite(bare_s_lemma, lemma); + proof * tr = m.mk_transitivity(cg, rw); + pr1 = m.mk_modus_ponens(qi_pr, tr); } m_instances.push_back(pr1); } - TRACE("qi_queue", tout << mk_pp(lemma, m_manager) << "\n#" << lemma->get_id() << ":=\n" << mk_ll_pp(lemma, m_manager);); + TRACE("qi_queue", tout << mk_pp(lemma, m) << "\n#" << lemma->get_id() << ":=\n" << mk_ll_pp(lemma, m);); m_stats.m_num_instances++; unsigned gen = get_new_gen(q, generation, ent.m_cost); display_instance_profile(f, q, num_bindings, bindings, proof_id, gen); @@ -282,7 +282,7 @@ namespace smt { } TRACE_CODE({ static unsigned num_useless = 0; - if (m_manager.is_or(lemma)) { + if (m.is_or(lemma)) { app * n = to_app(lemma); bool has_unassigned = false; expr * true_child = 0; @@ -296,7 +296,7 @@ namespace smt { } } if (true_child && has_unassigned) { - TRACE("qi_queue_profile_detail", tout << "missed:\n" << mk_ll_pp(s_instance, m_manager) << "\n#" << true_child->get_id() << "\n";); + TRACE("qi_queue_profile_detail", tout << "missed:\n" << mk_ll_pp(s_instance, m) << "\n#" << true_child->get_id() << "\n";); num_useless++; if (num_useless % 10 == 0) { TRACE("qi_queue_profile", tout << "num useless: " << num_useless << "\n";); @@ -305,8 +305,8 @@ namespace smt { } }); - if (m_manager.has_trace_stream()) - m_manager.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) + m.trace_stream() << "[end-of-instance]\n"; } @@ -368,7 +368,7 @@ namespace smt { TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); if (!e.m_instantiated && e.m_cost <= min_cost) { TRACE("qi_queue", - tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";); + tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m) << "\ncost: " << e.m_cost << "\n";); result = false; m_instantiated_trail.push_back(i); m_stats.m_num_lazy_instances++; @@ -384,7 +384,7 @@ namespace smt { TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); if (!e.m_instantiated && e.m_cost <= m_params.m_qi_lazy_threshold) { TRACE("qi_queue", - tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";); + tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m) << "\ncost: " << e.m_cost << "\n";); result = false; m_instantiated_trail.push_back(i); m_stats.m_num_lazy_instances++; diff --git a/src/smt/qi_queue.h b/src/smt/qi_queue.h index 171466e42..72cc0feb9 100644 --- a/src/smt/qi_queue.h +++ b/src/smt/qi_queue.h @@ -42,7 +42,7 @@ namespace smt { class qi_queue { quantifier_manager & m_qm; context & m_context; - ast_manager & m_manager; + ast_manager & m; qi_params & m_params; qi_queue_stats m_stats; checker m_checker; diff --git a/src/smt/smt_clause.cpp b/src/smt/smt_clause.cpp index a1f1f9f03..409827d43 100644 --- a/src/smt/smt_clause.cpp +++ b/src/smt/smt_clause.cpp @@ -28,7 +28,7 @@ namespace smt { */ clause * clause::mk(ast_manager & m, unsigned num_lits, literal * lits, clause_kind k, justification * js, clause_del_eh * del_eh, bool save_atoms, expr * const * bool_var2expr_map) { - SASSERT(k == CLS_AUX || js == 0 || !js->in_region()); + SASSERT(smt::is_axiom(k) || js == nullptr || !js->in_region()); SASSERT(num_lits >= 2); unsigned sz = get_obj_size(num_lits, k, save_atoms, del_eh != nullptr, js != nullptr); void * mem = m.get_allocator().allocate(sz); @@ -63,7 +63,7 @@ namespace smt { SASSERT(cls->get_del_eh() == del_eh); SASSERT(cls->get_justification() == js); for (unsigned i = 0; i < num_lits; i++) { - SASSERT(cls->get_literal(i) == lits[i]); + SASSERT((*cls)[i] == lits[i]); SASSERT(!save_atoms || cls->get_atom(i) == bool_var2expr_map[lits[i].var()]); }}); return cls; diff --git a/src/smt/smt_clause.h b/src/smt/smt_clause.h index 025e2389d..5c4f5b111 100644 --- a/src/smt/smt_clause.h +++ b/src/smt/smt_clause.h @@ -39,10 +39,14 @@ namespace smt { }; enum clause_kind { - CLS_AUX, - CLS_LEARNED, - CLS_AUX_LEMMA + CLS_AUX, // an input assumption + CLS_TH_AXIOM, // a theory axiom + CLS_LEARNED, // learned through conflict resolution + CLS_TH_LEMMA // a theory lemma }; + + inline bool is_axiom(clause_kind k) { return k == CLS_AUX || k == CLS_TH_AXIOM; } + inline bool is_lemma(clause_kind k) { return k == CLS_LEARNED || k == CLS_TH_LEMMA; } /** \brief A SMT clause. @@ -63,7 +67,7 @@ namespace smt { static unsigned get_obj_size(unsigned num_lits, clause_kind k, bool has_atoms, bool has_del_eh, bool has_justification) { unsigned r = sizeof(clause) + sizeof(literal) * num_lits; - if (k != CLS_AUX) + if (smt::is_lemma(k)) r += sizeof(unsigned); /* dvitek: Fix alignment issues on 64-bit platforms. The * 'if' statement below probably isn't worthwhile since @@ -119,9 +123,9 @@ namespace smt { friend class context; void swap_lits(unsigned idx1, unsigned idx2) { - literal tmp = get_literal(idx1); - set_literal(idx1, get_literal(idx2)); - set_literal(idx2, tmp); + SASSERT(idx1 < m_num_literals); + SASSERT(idx2 < m_num_literals); + std::swap(m_lits[idx1], m_lits[idx2]); } bool is_watch(literal l) const { @@ -133,7 +137,6 @@ namespace smt { } void set_num_literals(unsigned n) { - SASSERT(n <= m_num_literals); SASSERT(!m_reinit); m_num_literals = n; } @@ -159,17 +162,18 @@ namespace smt { } bool is_lemma() const { - return get_kind() != CLS_AUX; + return smt::is_lemma(get_kind()); } bool is_learned() const { return get_kind() == CLS_LEARNED; } - bool is_aux_lemma() const { - return get_kind() == CLS_AUX_LEMMA; + bool is_th_lemma() const { + return get_kind() == CLS_TH_LEMMA; } + bool in_reinit_stack() const { return m_reinit; } @@ -182,14 +186,22 @@ namespace smt { return m_num_literals; } - literal get_literal(unsigned idx) const { + literal & operator[](unsigned idx) { SASSERT(idx < m_num_literals); - return m_lits[idx]; + return m_lits[idx]; + } + + literal operator[](unsigned idx) const { + SASSERT(idx < m_num_literals); + return m_lits[idx]; + } + + literal get_literal(unsigned idx) const { + return (*this)[idx]; } literal & get_literal(unsigned idx) { - SASSERT(idx < m_num_literals); - return m_lits[idx]; + return (*this)[idx]; } literal * begin() { return m_lits; } @@ -248,7 +260,7 @@ namespace smt { unsigned hash() const { return get_ptr_hash(this); } - + void mark_as_deleted(ast_manager & m) { SASSERT(!m_deleted); m_deleted = true; @@ -262,6 +274,7 @@ namespace smt { bool deleted() const { return m_deleted; } + }; typedef ptr_vector clause_vector; diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp new file mode 100644 index 000000000..390a54029 --- /dev/null +++ b/src/smt/smt_clause_proof.cpp @@ -0,0 +1,166 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + smt_clause_proof.cpp + +Author: + + Nikolaj Bjorner (nbjorner) 2019-03-15 + +Revision History: + +--*/ +#include "smt/smt_clause_proof.h" +#include "smt/smt_context.h" +#include "ast/ast_pp.h" + +namespace smt { + clause_proof::clause_proof(context& ctx): ctx(ctx), m(ctx.get_manager()), m_lits(m) {} + + clause_proof::status clause_proof::kind2st(clause_kind k) { + switch (k) { + case CLS_AUX: + return status::assumption; + case CLS_TH_AXIOM: + return status::th_assumption; + case CLS_LEARNED: + return status::lemma; + case CLS_TH_LEMMA: + return status::th_lemma; + default: + UNREACHABLE(); + return status::lemma; + } + } + + proof* clause_proof::justification2proof(justification* j) { + return (m.proofs_enabled() && j) ? j->mk_proof(ctx.get_cr()) : nullptr; + } + + void clause_proof::add(clause& c) { + if (ctx.get_fparams().m_clause_proof) { + justification* j = c.get_justification(); + proof* pr = justification2proof(j); + update(c, kind2st(c.get_kind()), pr); + } + } + + void clause_proof::add(unsigned n, literal const* lits, clause_kind k, justification* j) { + if (ctx.get_fparams().m_clause_proof) { + proof* pr = justification2proof(j); + m_lits.reset(); + for (unsigned i = 0; i < n; ++i) { + literal lit = lits[i]; + m_lits.push_back(ctx.literal2expr(lit)); + } + update(kind2st(k), m_lits, pr); + } + } + + + void clause_proof::shrink(clause& c, unsigned new_size) { + if (ctx.get_fparams().m_clause_proof) { + m_lits.reset(); + for (unsigned i = 0; i < new_size; ++i) { + m_lits.push_back(ctx.literal2expr(c[i])); + } + update(status::lemma, m_lits, nullptr); + for (unsigned i = new_size; i < c.get_num_literals(); ++i) { + m_lits.push_back(ctx.literal2expr(c[i])); + } + update(status::deleted, m_lits, nullptr); + } + } + + void clause_proof::add(literal lit, clause_kind k, justification* j) { + if (ctx.get_fparams().m_clause_proof) { + m_lits.reset(); + m_lits.push_back(ctx.literal2expr(lit)); + proof* pr = justification2proof(j); + update(kind2st(k), m_lits, pr); + } + } + + void clause_proof::add(literal lit1, literal lit2, clause_kind k, justification* j) { + if (ctx.get_fparams().m_clause_proof) { + m_lits.reset(); + m_lits.push_back(ctx.literal2expr(lit1)); + m_lits.push_back(ctx.literal2expr(lit2)); + proof* pr = justification2proof(j); + m_trail.push_back(info(kind2st(k), m_lits, pr)); + } + } + + + void clause_proof::del(clause& c) { + update(c, status::deleted, nullptr); + } + + void clause_proof::update(status st, expr_ref_vector& v, proof* p) { + TRACE("clause_proof", tout << st << " " << v << "\n";); + IF_VERBOSE(3, verbose_stream() << st << " " << v << "\n"); + m_trail.push_back(info(st, v, p)); + } + + void clause_proof::update(clause& c, status st, proof* p) { + if (ctx.get_fparams().m_clause_proof) { + m_lits.reset(); + for (literal lit : c) { + m_lits.push_back(ctx.literal2expr(lit)); + } + update(st, m_lits, p); + } + } + + proof_ref clause_proof::get_proof() { + TRACE("context", tout << "get-proof " << ctx.get_fparams().m_clause_proof << "\n";); + if (!ctx.get_fparams().m_clause_proof) { + return proof_ref(m); + } + proof_ref_vector ps(m); + for (auto& info : m_trail) { + expr_ref fact = mk_or(info.m_clause); + proof* pr = info.m_proof; + switch (info.m_status) { + case status::assumption: + ps.push_back(m.mk_assumption_add(pr, fact)); + break; + case status::lemma: + ps.push_back(m.mk_lemma_add(pr, fact)); + break; + case status::th_assumption: + ps.push_back(m.mk_th_assumption_add(pr, fact)); + break; + case status::th_lemma: + ps.push_back(m.mk_th_lemma_add(pr, fact)); + break; + case status::deleted: + ps.push_back(m.mk_redundant_del(fact)); + break; + } + } + return proof_ref(m.mk_clause_trail(ps.size(), ps.c_ptr()), m); + } + + std::ostream& operator<<(std::ostream& out, clause_proof::status st) { + switch (st) { + case clause_proof::status::assumption: + return out << "asm"; + case clause_proof::status::th_assumption: + return out << "th_asm"; + case clause_proof::status::lemma: + return out << "lem"; + case clause_proof::status::th_lemma: + return out << "th_lem"; + case clause_proof::status::deleted: + return out << "del"; + default: + return out << "unkn"; + } + } + +}; + + diff --git a/src/smt/smt_clause_proof.h b/src/smt/smt_clause_proof.h new file mode 100644 index 000000000..972b19bd0 --- /dev/null +++ b/src/smt/smt_clause_proof.h @@ -0,0 +1,77 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + smt_clause_proof.h + +Abstract: + + This module tracks clausal proof objects as a trail of added and removed assumptions (input clauses) + theory lemmas and axioms, and lemmas produced from conflict resolution (possibly using theory propagation). + + Clausal proofs may serve a set of purposes: + - detailed diagnostics of general properties of the search. + - an interface to proof checking + - an interface to replay in trusted bases + - an interface to proof pruning methods + - an interface to clausal interpolation methods. + +Author: + + Nikolaj Bjorner (nbjorner) 2019-03-15 + +Revision History: + +--*/ +#ifndef SMT_CLAUSE_PROOF_H_ +#define SMT_CLAUSE_PROOF_H_ + +#include "smt/smt_theory.h" +#include "smt/smt_clause.h" + +namespace smt { + class context; + class justification; + + class clause_proof { + public: + enum status { + lemma, + assumption, + th_lemma, + th_assumption, + deleted + }; + private: + + struct info { + status m_status; + expr_ref_vector m_clause; + proof_ref m_proof; + info(status st, expr_ref_vector& v, proof* p): m_status(st), m_clause(v), m_proof(p, m_clause.m()) {} + }; + context& ctx; + ast_manager& m; + expr_ref_vector m_lits; + vector m_trail; + void update(status st, expr_ref_vector& v, proof* p); + void update(clause& c, status st, proof* p); + status kind2st(clause_kind k); + proof* justification2proof(justification* j); + public: + clause_proof(context& ctx); + void shrink(clause& c, unsigned new_size); + void add(literal lit, clause_kind k, justification* j); + void add(literal lit1, literal lit2, clause_kind k, justification* j); + void add(clause& c); + void add(unsigned n, literal const* lits, clause_kind k, justification* j); + void del(clause& c); + proof_ref get_proof(); + }; + + std::ostream& operator<<(std::ostream& out, clause_proof::status st); +}; + +#endif /* SMT_CLAUSE_PROOF_H_ */ + diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 9a3ae7728..51cab8949 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -277,17 +277,17 @@ namespace smt { unsigned num_lits = cls->get_num_literals(); unsigned i = 0; if (consequent != false_literal) { - SASSERT(cls->get_literal(0) == consequent || cls->get_literal(1) == consequent); - if (cls->get_literal(0) == consequent) { + SASSERT((*cls)[0] == consequent || (*cls)[1] == consequent); + if ((*cls)[0] == consequent) { i = 1; } else { - r = std::max(r, m_ctx.get_assign_level(cls->get_literal(0))); + r = std::max(r, m_ctx.get_assign_level((*cls)[0])); i = 2; } } for(; i < num_lits; i++) - r = std::max(r, m_ctx.get_assign_level(cls->get_literal(i))); + r = std::max(r, m_ctx.get_assign_level((*cls)[i])); justification * js = cls->get_justification(); if (js) r = std::max(r, get_justification_max_lvl(js)); @@ -471,8 +471,9 @@ namespace smt { b_justification js; literal consequent; - if (!initialize_resolve(conflict, not_l, js, consequent)) + if (!initialize_resolve(conflict, not_l, js, consequent)) { return false; + } unsigned idx = skip_literals_above_conflict_level(); @@ -510,19 +511,19 @@ namespace smt { unsigned num_lits = cls->get_num_literals(); unsigned i = 0; if (consequent != false_literal) { - SASSERT(cls->get_literal(0) == consequent || cls->get_literal(1) == consequent); - if (cls->get_literal(0) == consequent) { + SASSERT((*cls)[0] == consequent || (*cls)[1] == consequent); + if ((*cls)[0] == consequent) { i = 1; } else { - literal l = cls->get_literal(0); + literal l = (*cls)[0]; SASSERT(consequent.var() != l.var()); process_antecedent(~l, num_marks); i = 2; } } for(; i < num_lits; i++) { - literal l = cls->get_literal(i); + literal l = (*cls)[i]; SASSERT(consequent.var() != l.var()); process_antecedent(~l, num_marks); } @@ -671,10 +672,10 @@ namespace smt { case b_justification::CLAUSE: { clause * cls = js.get_clause(); unsigned num_lits = cls->get_num_literals(); - unsigned pos = cls->get_literal(1).var() == var; + unsigned pos = (*cls)[1].var() == var; for (unsigned i = 0; i < num_lits; i++) { if (pos != i) { - literal l = cls->get_literal(i); + literal l = (*cls)[i]; SASSERT(l.var() != var); if (!process_antecedent_for_minimization(~l)) { reset_unmark_and_justifications(old_size, old_js_qhead); diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index 4cb331661..259b3ccf4 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -110,9 +110,7 @@ namespace smt { case b_justification::CLAUSE: { clause * cls = js.get_clause(); if (!cls) break; - unsigned num_lits = cls->get_num_literals(); - for (unsigned j = 0; j < num_lits; ++j) { - literal lit2 = cls->get_literal(j); + for (literal lit2 : *cls) { if (lit2.var() != lit.var()) { s |= m_antecedents.find(lit2.var()); } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 29e33fc99..a80c6b5aa 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -55,6 +55,7 @@ namespace smt { m_lemma_id(0), m_progress_callback(nullptr), m_next_progress_sample(0), + m_clause_proof(*this), m_fingerprints(m, m_region), m_b_internalized_stack(m), m_e_internalized_stack(m), @@ -1878,7 +1879,7 @@ namespace smt { } } - TRACE("decide", tout << "case split pos: " << is_pos << " p" << var << "\n" + TRACE("decide", tout << "case split " << (is_pos?"pos":"neg") << " p" << var << "\n" << "activity: " << get_activity(var) << "\n";); assign(literal(var, !is_pos), b_justification::mk_axiom(), true); @@ -1987,8 +1988,10 @@ namespace smt { \pre Clause is not in the reinit stack. */ - void context::del_clause(clause * cls) { + void context::del_clause(bool log, clause * cls) { SASSERT(m_flushing || !cls->in_reinit_stack()); + if (log) + m_clause_proof.del(*cls); if (!cls->deleted()) remove_cls_occs(cls); cls->deallocate(m_manager); @@ -2005,18 +2008,11 @@ namespace smt { clause_vector::iterator it = v.end(); while (it != begin) { --it; - del_clause(*it); + del_clause(false, *it); } v.shrink(old_size); } -#if 0 - void context::mark_as_deleted(clause * cls) { - SASSERT(!cls->deleted()); - remove_cls_occs(cls); - cls->mark_as_deleted(m_manager); - } -#endif /** \brief Undo variable assignments. @@ -2221,7 +2217,6 @@ namespace smt { cls->m_reinternalize_atoms = false; continue; } - SASSERT(cls->in_reinit_stack()); bool keep = false; if (cls->reinternalize_atoms()) { @@ -2473,11 +2468,11 @@ namespace smt { \remark This method should only be invoked if we are at the base level. */ - bool context::simplify_clause(clause * cls) { + bool context::simplify_clause(clause& cls) { SASSERT(m_scope_lvl == m_base_lvl); - unsigned s = cls->get_num_literals(); - if (get_assignment(cls->get_literal(0)) == l_true || - get_assignment(cls->get_literal(1)) == l_true) { + unsigned s = cls.get_num_literals(); + if (get_assignment(cls[0]) == l_true || + get_assignment(cls[1]) == l_true) { // clause is already satisfied. return true; } @@ -2487,16 +2482,18 @@ namespace smt { unsigned i = 2; unsigned j = i; for(; i < s; i++) { - literal l = cls->get_literal(i); + literal l = cls[i]; switch(get_assignment(l)) { case l_false: if (m_manager.proofs_enabled()) simp_lits.push_back(~l); if (lit_occs_enabled()) - m_lit_occs[l.index()].erase(cls); + m_lit_occs[l.index()].erase(&cls); break; case l_undef: - cls->set_literal(j, l); + if (i != j) { + cls.swap_lits(i, j); + } j++; break; case l_true: @@ -2505,13 +2502,14 @@ namespace smt { } if (j < s) { - cls->set_num_literals(j); + m_clause_proof.shrink(cls, j); + cls.set_num_literals(j); SASSERT(j >= 2); } if (m_manager.proofs_enabled() && !simp_lits.empty()) { SASSERT(m_scope_lvl == m_base_lvl); - justification * js = cls->get_justification(); + justification * js = cls.get_justification(); justification * new_js = nullptr; if (js->in_region()) new_js = mk_justification(unit_resolution_justification(m_region, @@ -2520,7 +2518,7 @@ namespace smt { simp_lits.c_ptr())); else new_js = alloc(unit_resolution_justification, js, simp_lits.size(), simp_lits.c_ptr()); - cls->set_justification(new_js); + cls.set_justification(new_js); } return false; } @@ -2539,13 +2537,14 @@ namespace smt { clause * cls = *it; SASSERT(!cls->in_reinit_stack()); TRACE("simplify_clauses_bug", display_clause(tout, cls); tout << "\n";); + if (cls->deleted()) { - del_clause(cls); + del_clause(true, cls); num_del_clauses++; } - else if (simplify_clause(cls)) { + else if (simplify_clause(*cls)) { for (unsigned idx = 0; idx < 2; idx++) { - literal l0 = cls->get_literal(idx); + literal l0 = (*cls)[idx]; b_justification l0_js = get_justification(l0.var()); if (l0_js != null_b_justification && l0_js.get_kind() == b_justification::CLAUSE && @@ -2560,7 +2559,7 @@ namespace smt { unsigned num_lits = cls->get_num_literals(); for(unsigned i = 0; i < num_lits; i++) { if (i != idx) { - literal l = cls->get_literal(i); + literal l = (*cls)[i]; SASSERT(l != l0); simp_lits.push_back(~l); } @@ -2587,7 +2586,7 @@ namespace smt { m_bdata[v0].set_axiom(); } } - del_clause(cls); + del_clause(true, cls); num_del_clauses++; } else { @@ -2707,7 +2706,7 @@ namespace smt { if (can_delete(cls)) { TRACE("del_inactive_lemmas", tout << "deleting: "; display_clause(tout, cls); tout << ", activity: " << cls->get_activity() << "\n";); - del_clause(cls); + del_clause(true, cls); num_del_cls++; } else { @@ -2719,12 +2718,11 @@ namespace smt { for (; i < sz; i++) { clause * cls = m_lemmas[i]; if (cls->deleted() && can_delete(cls)) { - del_clause(cls); + del_clause(true, cls); num_del_cls++; } else { - m_lemmas[j] = cls; - j++; + m_lemmas[j++] = cls; } } m_lemmas.shrink(j); @@ -2762,7 +2760,7 @@ namespace smt { if (can_delete(cls)) { if (cls->deleted()) { // clause is already marked for deletion - del_clause(cls); + del_clause(true, cls); num_del_cls++; continue; } @@ -2773,7 +2771,7 @@ namespace smt { if (cls->get_activity() < act_threshold) { unsigned rel_threshold = (i >= new_first_idx ? m_fparams.m_new_clause_relevancy : m_fparams.m_old_clause_relevancy); if (more_than_k_unassigned_literals(cls, rel_threshold)) { - del_clause(cls); + del_clause(true, cls); num_del_cls++; continue; } @@ -2793,9 +2791,7 @@ namespace smt { */ bool context::more_than_k_unassigned_literals(clause * cls, unsigned k) { SASSERT(k > 0); - unsigned num_lits = cls->get_num_literals(); - for(unsigned i = 0; i < num_lits; i++) { - literal l = cls->get_literal(i); + for (literal l : *cls) { if (get_assignment(l) == l_undef) { k--; if (k == 0) { @@ -3150,7 +3146,7 @@ namespace smt { void context::reset_tmp_clauses() { for (auto& p : m_tmp_clauses) { - if (p.first) del_clause(p.first); + if (p.first) del_clause(false, p.first); } m_tmp_clauses.reset(); } @@ -3342,18 +3338,18 @@ namespace smt { SASSERT(!m_setup.already_configured()); setup_context(m_fparams.m_auto_config); + + internalize_assertions(); expr_ref_vector theory_assumptions(m_manager); add_theory_assumptions(theory_assumptions); if (!theory_assumptions.empty()) { TRACE("search", tout << "Adding theory assumptions to context" << std::endl;); return check(0, nullptr, reset_cancel); } - - internalize_assertions(); - TRACE("before_search", display(tout);); - lbool r = search(); - r = check_finalize(r); - return r; + else { + TRACE("before_search", display(tout);); + return check_finalize(search()); + } } config_mode context::get_config_mode(bool use_static_features) const { @@ -3408,10 +3404,9 @@ namespace smt { do { pop_to_base_lvl(); expr_ref_vector asms(m_manager, num_assumptions, assumptions); - add_theory_assumptions(asms); - // introducing proxies: if (!validate_assumptions(asms)) return l_undef; - TRACE("unsat_core_bug", tout << asms << "\n";); internalize_assertions(); + add_theory_assumptions(asms); + TRACE("unsat_core_bug", tout << asms << "\n";); init_assumptions(asms); TRACE("before_search", display(tout);); r = search(); @@ -3430,10 +3425,10 @@ namespace smt { do { pop_to_base_lvl(); expr_ref_vector asms(cube); + internalize_assertions(); add_theory_assumptions(asms); // introducing proxies: if (!validate_assumptions(asms)) return l_undef; for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef; - internalize_assertions(); init_assumptions(asms); for (auto const& clause : clauses) init_clause(clause); r = search(); @@ -3731,8 +3726,8 @@ namespace smt { if (m_last_search_failure != OK) return true; - if (m_timer.ms_timeout(m_fparams.m_timeout)) { - m_last_search_failure = TIMEOUT; + if (get_cancel_flag()) { + m_last_search_failure = CANCELED; return true; } @@ -4057,6 +4052,9 @@ namespace smt { update_phase_cache_counter(); return true; } + else if (m_fparams.m_clause_proof) { + m_unsat_proof = m_clause_proof.get_proof(); + } else if (m_manager.proofs_enabled()) { m_unsat_proof = m_conflict_resolution->get_lemma_proof(); check_proof(m_unsat_proof); @@ -4362,7 +4360,7 @@ namespace smt { m_fingerprints.display(tout); ); failure fl = get_last_search_failure(); - if (fl == MEMOUT || fl == CANCELED || fl == TIMEOUT || fl == NUM_CONFLICTS || fl == RESOURCE_LIMIT) { + if (fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS || fl == RESOURCE_LIMIT) { TRACE("get_model", tout << "last search failure: " << fl << "\n";); } else if (m_fparams.m_model || m_fparams.m_model_on_final_check || m_qmanager->model_based()) { @@ -4381,8 +4379,11 @@ namespace smt { } proof * context::get_proof() { - if (!m_manager.proofs_enabled()) - return nullptr; + + if (!m_unsat_proof) { + m_unsat_proof = m_clause_proof.get_proof(); + } + TRACE("context", tout << m_unsat_proof << "\n";); return m_unsat_proof; } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index a7675a1d5..2eef102c9 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -27,6 +27,7 @@ Revision History: #include "smt/smt_eq_justification.h" #include "smt/smt_justification.h" #include "smt/smt_bool_var_data.h" +#include "smt/smt_clause_proof.h" #include "smt/smt_theory.h" #include "smt/smt_quantifier.h" #include "smt/smt_quantifier_stat.h" @@ -92,6 +93,7 @@ namespace smt { mutable unsigned m_lemma_id; progress_callback * m_progress_callback; unsigned m_next_progress_sample; + clause_proof m_clause_proof; region m_region; @@ -525,6 +527,12 @@ namespace smt { result = bool_var2expr(l.var()); } + expr_ref literal2expr(literal l) const { + expr_ref result(m_manager); + literal2expr(l, result); + return result; + } + bool is_true(enode const * n) const { return n == m_true_enode; } @@ -652,7 +660,7 @@ namespace smt { void remove_cls_occs(clause * cls); - void del_clause(clause * cls); + void del_clause(bool log, clause * cls); void del_clauses(clause_vector & v, unsigned old_size); @@ -681,9 +689,6 @@ namespace smt { void remove_watch(bool_var v); - void mark_as_deleted(clause * cls); - - // ----------------------------------- // // Internalization @@ -859,6 +864,9 @@ namespace smt { void add_lit_occs(clause * cls); public: + + void ensure_internalized(expr* e); + void internalize(expr * n, bool gate_ctx); void internalize(expr * n, bool gate_ctx, unsigned generation); @@ -1101,7 +1109,7 @@ namespace smt { m_bvar_inc *= m_fparams.m_inv_decay; } - bool simplify_clause(clause * cls); + bool simplify_clause(clause& cls); unsigned simplify_clauses(clause_vector & clauses, unsigned starting_at); @@ -1113,7 +1121,7 @@ namespace smt { bool is_justifying(clause * cls) const { for (unsigned i = 0; i < 2; i++) { b_justification js; - js = get_justification(cls->get_literal(i).var()); + js = get_justification((*cls)[i].var()); if (js.get_kind() == b_justification::CLAUSE && js.get_clause() == cls) return true; } @@ -1561,6 +1569,8 @@ namespace smt { proof * get_proof(); + conflict_resolution& get_cr() { return *m_conflict_resolution.get(); } + void get_relevant_labels(expr* cnstr, buffer & result); void get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result); diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp index a6c4f49b4..474c44821 100644 --- a/src/smt/smt_context_inv.cpp +++ b/src/smt/smt_context_inv.cpp @@ -33,9 +33,7 @@ namespace smt { SASSERT(is_watching_clause(~cls->get_literal(0), cls)); SASSERT(is_watching_clause(~cls->get_literal(1), cls)); if (lit_occs_enabled()) { - unsigned num_lits = cls->get_num_literals(); - for (unsigned i = 0; i < num_lits; i++) { - literal l = cls->get_literal(i); + for (literal l : *cls) { SASSERT(m_lit_occs[l.index()].contains(const_cast(cls))); } } diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index c40b829a7..8ae464404 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -31,8 +31,6 @@ namespace smt { return out << "OK"; case UNKNOWN: return out << "UNKNOWN"; - case TIMEOUT: - return out << "TIMEOUT"; case MEMOUT: return out << "MEMOUT"; case CANCELED: @@ -64,7 +62,6 @@ namespace smt { std::string r; switch(m_last_search_failure) { case OK: r = m_unknown; break; - case TIMEOUT: r = "timeout"; break; case MEMOUT: r = "memout"; break; case CANCELED: r = "canceled"; break; case NUM_CONFLICTS: r = "max-conflicts-reached"; break; @@ -149,9 +146,7 @@ namespace smt { void context::display_clause_detail(std::ostream & out, clause const * cls) const { out << "lemma: " << cls->is_lemma() << "\n"; - unsigned num_lits = cls->get_num_literals(); - for (unsigned i = 0; i < num_lits; i++) { - literal l = cls->get_literal(i); + for (literal l : *cls) { display_literal(out, l); out << ", val: " << get_assignment(l) << ", lvl: " << get_assign_level(l) << ", ilvl: " << get_intern_level(l.var()) << ", var: " << l.var() << "\n" diff --git a/src/smt/smt_context_stat.cpp b/src/smt/smt_context_stat.cpp index 968d84b73..770a6451b 100644 --- a/src/smt/smt_context_stat.cpp +++ b/src/smt/smt_context_stat.cpp @@ -33,9 +33,7 @@ namespace smt { } static void acc_num_occs(clause * cls, unsigned_vector & lit2num_occs) { - unsigned num_lits = cls->get_num_literals(); - for (unsigned i = 0; i < num_lits; i++) { - literal l = cls->get_literal(i); + for (literal l : *cls) { lit2num_occs[l.index()]++; } } @@ -80,9 +78,7 @@ namespace smt { } static void acc_var_num_occs(clause * cls, unsigned_vector & var2num_occs) { - unsigned num_lits = cls->get_num_literals(); - for (unsigned i = 0; i < num_lits; i++) { - literal l = cls->get_literal(i); + for (literal l : *cls) { var2num_occs[l.var()]++; } } @@ -116,9 +112,9 @@ namespace smt { static void acc_var_num_min_occs(clause * cls, unsigned_vector & var2num_min_occs) { unsigned num_lits = cls->get_num_literals(); - bool_var min_var = cls->get_literal(0).var(); + bool_var min_var = (*cls)[0].var(); for (unsigned i = 1; i < num_lits; i++) { - bool_var v = cls->get_literal(i).var(); + bool_var v = (*cls)[i].var(); if (v < min_var) min_var = v; } diff --git a/src/smt/smt_failure.h b/src/smt/smt_failure.h index 9e332ac89..bd29fbafb 100644 --- a/src/smt/smt_failure.h +++ b/src/smt/smt_failure.h @@ -27,7 +27,6 @@ namespace smt { enum failure { OK, UNKNOWN, - TIMEOUT, MEMOUT, CANCELED, //!< External cancel flag was set NUM_CONFLICTS, //!< Maximum number of conflicts was reached diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 0ed69c03c..d16b1bef5 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -281,7 +281,9 @@ namespace smt { set_conflict(mk_justification(justification_proof_wrapper(*this, pr))); } else { - assign(l, mk_justification(justification_proof_wrapper(*this, pr))); + justification* j = mk_justification(justification_proof_wrapper(*this, pr)); + m_clause_proof.add(l, CLS_AUX, j); + assign(l, j); mark_as_relevant(l); } } @@ -317,6 +319,12 @@ namespace smt { internalize(n, gate_ctx); } + void context::ensure_internalized(expr* e) { + if (!e_internalized(e)) { + internalize(e, false); + } + } + /** \brief Internalize the given expression into the logical context. @@ -1304,8 +1312,10 @@ namespace smt { */ clause * context::mk_clause(unsigned num_lits, literal * lits, justification * j, clause_kind k, clause_del_eh * del_eh) { TRACE("mk_clause", tout << "creating clause:\n"; display_literals_verbose(tout, num_lits, lits); tout << "\n";); + m_clause_proof.add(num_lits, lits, k, j); switch (k) { - case CLS_AUX: { + case CLS_AUX: + case CLS_TH_AXIOM: { literal_buffer simp_lits; if (!simplify_aux_clause_literals(num_lits, lits, simp_lits)) return nullptr; // clause is equivalent to true; @@ -1319,7 +1329,7 @@ namespace smt { } break; } - case CLS_AUX_LEMMA: { + case CLS_TH_LEMMA: { if (!simplify_aux_lemma_literals(num_lits, lits)) return nullptr; // clause is equivalent to true // simplify_aux_lemma_literals does not delete literals assigned to false, so @@ -1333,7 +1343,7 @@ namespace smt { unsigned activity = 0; if (activity == 0) activity = 1; - bool lemma = k != CLS_AUX; + bool lemma = is_lemma(k); m_stats.m_num_mk_lits += num_lits; switch (num_lits) { case 0: @@ -1354,9 +1364,10 @@ namespace smt { literal l2 = lits[1]; m_watches[(~l1).index()].insert_literal(l2); m_watches[(~l2).index()].insert_literal(l1); - if (get_assignment(l2) == l_false) + if (get_assignment(l2) == l_false) { assign(l1, b_justification(~l2)); - + } + m_clause_proof.add(l1, l2, k, j); m_stats.m_num_mk_bin_clause++; return nullptr; } @@ -1368,6 +1379,7 @@ namespace smt { bool reinit = save_atoms; SASSERT(!lemma || j == 0 || !j->in_region()); clause * cls = clause::mk(m_manager, num_lits, lits, k, j, del_eh, save_atoms, m_bool_var2expr.c_ptr()); + m_clause_proof.add(*cls); if (lemma) { cls->set_activity(activity); if (k == CLS_LEARNED) { @@ -1375,7 +1387,7 @@ namespace smt { cls->swap_lits(1, w2_idx); } else { - SASSERT(k == CLS_AUX_LEMMA); + SASSERT(k == CLS_TH_LEMMA); int w1_idx = select_watch_lit(cls, 0); cls->swap_lits(0, w1_idx); int w2_idx = select_watch_lit(cls, 1); @@ -1388,14 +1400,14 @@ namespace smt { add_watch_literal(cls, 1); if (get_assignment(cls->get_literal(0)) == l_false) { set_conflict(b_justification(cls)); - if (k == CLS_AUX_LEMMA && m_scope_lvl > m_base_lvl) { + if (k == CLS_TH_LEMMA && m_scope_lvl > m_base_lvl) { reinit = true; iscope_lvl = m_scope_lvl; } } else if (get_assignment(cls->get_literal(1)) == l_false) { assign(cls->get_literal(0), b_justification(cls)); - if (k == CLS_AUX_LEMMA && m_scope_lvl > m_base_lvl) { + if (k == CLS_TH_LEMMA && m_scope_lvl > m_base_lvl) { reinit = true; iscope_lvl = m_scope_lvl; } @@ -1441,9 +1453,7 @@ namespace smt { void context::mk_th_axiom(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params, parameter * params) { justification * js = nullptr; - TRACE("mk_th_axiom", - display_literals_verbose(tout, num_lits, lits); - tout << "\n";); + TRACE("mk_th_axiom", display_literals_verbose(tout, num_lits, lits) << "\n";); if (m_manager.proofs_enabled()) { js = mk_justification(theory_axiom_justification(tid, m_region, num_lits, lits, num_params, params)); @@ -1454,7 +1464,7 @@ namespace smt { SASSERT(tmp.size() == num_lits); display_lemma_as_smt_problem(tmp.size(), tmp.c_ptr(), false_literal, m_fparams.m_logic); } - mk_clause(num_lits, lits, js); + mk_clause(num_lits, lits, js, CLS_TH_AXIOM); } void context::mk_th_axiom(theory_id tid, literal l1, literal l2, unsigned num_params, parameter * params) { diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 2d894d3ee..dea1a6c0b 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -144,6 +144,9 @@ public: } }; + void handle_canceled(goal_ref const & in, + goal_ref_buffer & result) { + } void operator()(goal_ref const & in, goal_ref_buffer & result) override { @@ -189,7 +192,7 @@ public: m_ctx->assert_expr(in->form(i)); } } - if (m_ctx->canceled()) { + if (m_ctx->canceled()) { throw tactic_exception(Z3_CANCELED_MSG); } @@ -201,10 +204,13 @@ public: r = m_ctx->check(assumptions.size(), assumptions.c_ptr()); } catch(...) { + TRACE("smt_tactic", tout << "exception\n";); m_ctx->collect_statistics(m_stats); throw; } m_ctx->collect_statistics(m_stats); + proof * pr = m_ctx->get_proof(); + TRACE("smt_tactic", tout << r << " " << pr << "\n";); switch (r) { case l_true: { if (m_fail_if_inconclusive && !in->sat_preserved()) @@ -234,10 +240,7 @@ public: } // formula is unsat, reset the goal, and store false there. in->reset(); - proof * pr = nullptr; expr_dependency * lcore = nullptr; - if (in->proofs_enabled()) - pr = m_ctx->get_proof(); if (in->unsat_core_enabled()) { unsigned sz = m_ctx->get_unsat_core_size(); for (unsigned i = 0; i < sz; i++) { @@ -252,15 +255,21 @@ public: return; } case l_undef: - if (m_ctx->canceled()) { + + if (m_ctx->canceled() && !pr) { throw tactic_exception(Z3_CANCELED_MSG); } - if (m_fail_if_inconclusive && !m_candidate_models) { + + if (m_fail_if_inconclusive && !m_candidate_models && !pr) { std::stringstream strm; strm << "smt tactic failed to show goal to be sat/unsat " << m_ctx->last_failure_as_string(); throw tactic_exception(strm.str()); } result.push_back(in.get()); + if (pr) { + in->reset(); + in->assert_expr(m.mk_const(symbol("trail"), m.mk_bool_sort()), pr, nullptr); + } if (m_candidate_models) { switch (m_ctx->last_failure()) { case smt::NUM_CONFLICTS: @@ -280,6 +289,9 @@ public: break; } } + if (pr) { + return; + } throw tactic_exception(m_ctx->last_failure_as_string()); } } diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index effc0677b..d148daaa1 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -3004,7 +3004,7 @@ namespace smt { js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr(), ante.num_params(), ante.params("assign-bounds")); } - ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, nullptr); + ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_TH_LEMMA, nullptr); } else { region & r = ctx.get_region(); diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp index a0dfc79cc..e79c64755 100644 --- a/src/smt/theory_array_bapa.cpp +++ b/src/smt/theory_array_bapa.cpp @@ -19,7 +19,7 @@ Abstract: S, T are intersecting. n != m or S != T D --------------------------------------------------------- Size(S, n) => Size(S\T, k1), Size(S n T, k2), n = k1 + k2 - Size(T, m) => Size(T\S, k3), SIze(S n T, k2), m = k2 + k3 + Size(T, m) => Size(T\S, k3), SIze(S n T, k2), m = k2 + k3 Size(S, n) P -------------------- @@ -85,29 +85,40 @@ Revision History: #include "smt/theory_array_full.h" #include "smt/theory_array_bapa.h" +#if 0 +- set of native select terms that are true +- set of auxiliary select terms. +- n1, n2, n3, n4. +- a1, a2, a3, a4, a5. +- +- add select terms, such that first +#endif + namespace smt { class theory_array_bapa::imp { struct sz_info { - bool m_is_leaf; // has it been split into disjoint subsets already? - rational m_value; // set to >= integer if fixed in final check, otherwise -1 - literal m_literal; // literal that enforces value is set. + bool m_is_leaf; // has it been split into disjoint subsets already? + rational m_size; // set to >= integer if fixed in final check, otherwise -1 + literal m_literal; // literal that enforces value is set. obj_map m_selects; - sz_info(): m_is_leaf(true), m_value(rational::minus_one()), m_literal(null_literal) {} + sz_info(): m_is_leaf(true), m_size(rational::minus_one()), m_literal(null_literal) {} }; typedef std::pair func_decls; - ast_manager& m; - theory_array_full& th; - arith_util m_arith; - array_util m_autil; - th_rewriter m_rw; - arith_value m_arith_value; - ast_ref_vector m_pinned; - obj_map m_sizeof; + ast_manager& m; + theory_array_full& th; + arith_util m_arith; + array_util m_autil; + th_rewriter m_rw; + arith_value m_arith_value; + ast_ref_vector m_pinned; + obj_map m_sizeof; + obj_map m_size_limit; obj_map m_index_skolems; - unsigned m_max_set_enumeration; + obj_map m_size_limit_sort2skolems; + unsigned m_max_set_enumeration; context& ctx() { return th.get_context(); } @@ -126,8 +137,8 @@ namespace smt { bool is_select(enode* n) { return th.is_select(n); } app_ref mk_select(expr* a, expr* i) { expr* args[2] = { a, i }; return app_ref(m_autil.mk_select(2, args), m); } literal get_literal(expr* e) { return ctx().get_literal(e); } - literal mk_literal(expr* e) { if (!ctx().e_internalized(e)) ctx().internalize(e, false); ctx().mark_as_relevant(e); return get_literal(e); } - literal mk_eq(expr* a, expr* b) { return th.mk_eq(a, b, false); } + literal mk_literal(expr* e) { if (!ctx().e_internalized(e)) ctx().internalize(e, false); literal lit = get_literal(e); ctx().mark_as_relevant(lit); return lit; } + literal mk_eq(expr* a, expr* b) { literal lit = th.mk_eq(a, b, false); ctx().mark_as_relevant(lit); return lit; } void mk_th_axiom(literal l1, literal l2) { literal lits[2] = { l1, l2 }; mk_th_axiom(2, lits); @@ -147,10 +158,12 @@ namespace smt { sz_info& v = *kv.m_value; v.m_selects.reset(); if (is_true(k) && is_leaf(v)) { - expr* set = k->get_arg(0); - for (enode* parent : enode::parents(get_root(set))) { - if (is_select(parent) && is_true(parent)) { - v.m_selects.insert(parent->get_arg(1)->get_root(), parent->get_owner()); + enode* set = get_root(k->get_arg(0)); + for (enode* parent : enode::parents(set)) { + if (is_select(parent) && parent->get_arg(0)->get_root() == set) { + if (is_true(parent)) { + v.m_selects.insert(parent->get_arg(1)->get_root(), parent->get_owner()); + } } } } @@ -211,9 +224,9 @@ namespace smt { SASSERT(i2.m_is_leaf); expr* s = sz1->get_arg(0); expr* t = sz2->get_arg(0); - if (m.get_sort(s) != m.get_sort(t)) { - return true; - } + if (m.get_sort(s) != m.get_sort(t)) { + return true; + } enode* r1 = get_root(s); enode* r2 = get_root(t); if (r1 == r2) { @@ -249,13 +262,24 @@ namespace smt { expr_ref tms = mk_subtract(t, s); expr_ref smt = mk_subtract(s, t); expr_ref tns = mk_intersect(t, s); +#if 0 + std::cout << tms << "\n"; + std::cout << smt << "\n"; + std::cout << tns << "\n"; +#endif + if (tns == sz1) { + std::cout << "SEEN " << tms << "\n"; + } + if (tns == sz2) { + std::cout << "SEEN " << smt << "\n"; + } ctx().push_trail(value_trail(i1.m_is_leaf, false)); ctx().push_trail(value_trail(i2.m_is_leaf, false)); expr_ref k1(m), k2(m), k3(m); expr_ref sz_tms(m), sz_tns(m), sz_smt(m); - k1 = m.mk_fresh_const("K", m_arith.mk_int()); - k2 = m.mk_fresh_const("K", m_arith.mk_int()); - k3 = m.mk_fresh_const("K", m_arith.mk_int()); + k1 = m_autil.mk_card(tms); + k2 = m_autil.mk_card(tns); + k3 = m_autil.mk_card(smt); sz_tms = m_autil.mk_has_size(tms, k1); sz_tns = m_autil.mk_has_size(tns, k2); sz_smt = m_autil.mk_has_size(smt, k3); @@ -264,7 +288,7 @@ namespace smt { propagate(sz2, sz_smt); propagate(sz2, sz_tns); propagate(sz1, mk_eq(k1 + k2, sz1->get_arg(1))); - propagate(sz2, mk_eq(k3 + k2, sz2->get_arg(1))); + propagate(sz2, mk_eq(k3 + k2, sz2->get_arg(1))); } expr_ref mk_subtract(expr* t, expr* s) { @@ -295,16 +319,17 @@ namespace smt { for (auto const& kv : m_sizeof) { app* k = kv.m_key; sz_info& i = *kv.m_value; - if (is_leaf(kv.m_value) && (i.m_literal == null_literal || !is_true(i.m_literal))) { + if (is_leaf(&i) && (i.m_literal == null_literal || !is_true(i.m_literal))) { rational value; - if (!m_arith_value.get_value(k->get_arg(1), value)) { + expr* set = k->get_arg(0); + expr* sz = k->get_arg(1); + if (!m_arith_value.get_value(sz, value)) { return l_undef; } - literal lit = mk_eq(k->get_arg(1), m_arith.mk_int(value)); - ctx().mark_as_relevant(lit); + literal lit = mk_eq(sz, m_arith.mk_int(value)); ctx().set_true_first_flag(lit.var()); ctx().push_trail(value_trail(i.m_literal, lit)); - i.m_value = value; + ctx().push_trail(value_trail(i.m_size, value)); result = l_false; } } @@ -312,21 +337,23 @@ namespace smt { } /** - Enforce Ak, k <= m_max_set_enumeration + Enforce Ak, */ lbool ensure_non_empty() { for (auto const& kv : m_sizeof) { sz_info& i = *kv.m_value; - app* sz = kv.m_key; - if (is_true(sz) && is_leaf(i) && i.m_selects.size() < i.m_value && i.m_selects.size() < m_max_set_enumeration) { - expr* a = sz->get_arg(0); - expr_ref le(m_arith.mk_le(sz->get_arg(1), m_arith.mk_int(0)), m); + app* set_sz = kv.m_key; + if (is_true(set_sz) && is_leaf(i) && i.m_selects.size() < i.m_size) { + expr* set = set_sz->get_arg(0); + expr_ref le(m_arith.mk_le(set_sz->get_arg(1), m_arith.mk_int(0)), m); literal le_lit = mk_literal(le); - literal sz_lit = mk_literal(sz); - for (unsigned k = 0; k < m_max_set_enumeration && rational(k) < i.m_value; ++k) { - expr_ref idx = mk_index_skolem(sz, a, k); - app_ref sel(mk_select(a, idx)); + literal sz_lit = mk_literal(set_sz); + unsigned k = i.m_selects.size(); + for (unsigned k = i.m_selects.size(); rational(k) < i.m_size; ++k) { + expr_ref idx = mk_index_skolem(set_sz, set, k); + app_ref sel(mk_select(set, idx), m); mk_th_axiom(~sz_lit, le_lit, mk_literal(sel)); + TRACE("array", tout << idx << " " << sel << " " << i.m_size << "\n";); } return l_false; } @@ -373,8 +400,8 @@ namespace smt { } lbool ensure_no_overflow(app* sz, sz_info& info) { - SASSERT(!info.m_value.is_neg()); - if (info.m_value < info.m_selects.size()) { + SASSERT(!info.m_size.is_neg()); + if (info.m_size < info.m_selects.size()) { for (auto i = info.m_selects.begin(), e = info.m_selects.end(); i != e; ++i) { for (auto j = i; ++j != e; ) { if (ctx().assume_eq(i->m_key, j->m_key)) { @@ -421,7 +448,7 @@ namespace smt { } std::ostream& display(std::ostream& out, sz_info& sz) { - return out << (sz.m_is_leaf ? "leaf": "") << " value: " << sz.m_value << " selects: " << sz.m_selects.size() << "\n"; + return out << (sz.m_is_leaf ? "leaf": "") << " size: " << sz.m_size << " selects: " << sz.m_selects.size() << "\n"; } public: @@ -471,6 +498,8 @@ namespace smt { // add case where default(S) = true, and add negative elements. } m_sizeof.insert(term, alloc(sz_info)); + m_size_limit.insert(s, rational(2)); + assert_size_limit(s, n); ctx().push_trail(remove_sz(m_sizeof, term)); } @@ -485,13 +514,22 @@ namespace smt { ctx().assign(lit, nullptr); } + lbool trace_call(char const* msg, lbool r) { + if (r != l_true) { + IF_VERBOSE(2, verbose_stream() << msg << "\n"); + } + return r; + } + final_check_status final_check() { - lbool r = ensure_functional(); + final_check_status st = m_arith_value.final_check(); + if (st != FC_DONE) return st; + lbool r = trace_call("ensure_functional", ensure_functional()); if (r == l_true) update_indices(); - if (r == l_true) r = ensure_disjoint(); - if (r == l_true) r = ensure_values_assigned(); - if (r == l_true) r = ensure_non_empty(); - if (r == l_true) r = ensure_no_overflow(); + if (r == l_true) r = trace_call("ensure_disjoint", ensure_disjoint()); + if (r == l_true) r = trace_call("eensure_values_assigned", ensure_values_assigned()); + if (r == l_true) r = trace_call("ensure_non_empty", ensure_non_empty()); + if (r == l_true) r = trace_call("ensure_no_overflow", ensure_no_overflow()); CTRACE("array", r != l_true, display(tout);); switch (r) { case l_true: @@ -508,13 +546,72 @@ namespace smt { for (auto const& kv : m_sizeof) { sz_info& i = *kv.m_value; app* sz = kv.m_key; - if (is_true(sz) && is_leaf(i) && rational(i.m_selects.size()) != i.m_value) { + if (is_true(sz) && is_leaf(i) && rational(i.m_selects.size()) != i.m_size) { warning_msg("models for BAPA is TBD"); break; } } } + bool should_research(expr_ref_vector & unsat_core) { + expr* set, *sz; + for (auto & e : unsat_core) { + if (is_app(e) && is_size_limit(to_app(e), set, sz)) { + inc_size_limit(set, sz); + return true; + } + } + return false; + } + + void inc_size_limit(expr* set, expr* sz) { + IF_VERBOSE(2, verbose_stream() << "inc value " << mk_pp(set, m) << "\n"); + m_size_limit[set] *= rational(2); + assert_size_limit(set, sz); + } + + bool is_size_limit(app* e, expr*& set, expr*& sz) { + func_decl* d = nullptr; + if (e->get_num_args() > 0 && m_size_limit_sort2skolems.find(m.get_sort(e->get_arg(0)), d) && d == e->get_decl()) { + set = e->get_arg(0); + sz = e->get_arg(1); + return true; + } + else { + return false; + } + } + + // has-size(s,n) & size-limit(s, n, k) => n <= k + + app_ref mk_size_limit(expr* set, expr* sz) { + func_decl* sk = nullptr; + sort* s = m.get_sort(set); + if (!m_size_limit_sort2skolems.find(s, sk)) { + sort* dom[3] = { s, m_arith.mk_int(), m_arith.mk_int() }; + sk = m.mk_fresh_func_decl("value-limit", "", 3, dom, m.mk_bool_sort()); + m_pinned.push_back(sk); + m_size_limit_sort2skolems.insert(s, sk); + } + return app_ref(m.mk_app(sk, set, sz, m_arith.mk_int(m_size_limit[set])), m); + } + + void assert_size_limit(expr* set, expr* sz) { + app_ref set_sz(m_autil.mk_has_size(set, sz), m); + app_ref lim(m_arith.mk_int(m_size_limit[set]), m); + app_ref size_limit = mk_size_limit(set, sz); + mk_th_axiom(~mk_literal(set_sz), ~mk_literal(size_limit), mk_literal(m_arith.mk_le(sz, lim))); + } + + void add_theory_assumptions(expr_ref_vector & assumptions) { + for (auto const& kv : m_sizeof) { + expr* set = kv.m_key->get_arg(0); + expr* sz = kv.m_key->get_arg(1); + assumptions.push_back(mk_size_limit(set, sz)); + } + TRACE("array", tout << "ASSUMPTIONS: " << assumptions << "\n";); + } + }; theory_array_bapa::theory_array_bapa(theory_array_full& th) { m_imp = alloc(imp, th); } @@ -526,4 +623,9 @@ namespace smt { final_check_status theory_array_bapa::final_check() { return m_imp->final_check(); } void theory_array_bapa::init_model() { m_imp->init_model(); } + + bool theory_array_bapa::should_research(expr_ref_vector & unsat_core) { return m_imp->should_research(unsat_core); } + + void theory_array_bapa::add_theory_assumptions(expr_ref_vector & assumptions) { m_imp->add_theory_assumptions(assumptions); } + } diff --git a/src/smt/theory_array_bapa.h b/src/smt/theory_array_bapa.h index 5ac51f8a9..0a1e39066 100644 --- a/src/smt/theory_array_bapa.h +++ b/src/smt/theory_array_bapa.h @@ -35,6 +35,8 @@ namespace smt { void internalize_term(app* term); final_check_status final_check(); void init_model(); + bool should_research(expr_ref_vector & unsat_core); + void add_theory_assumptions(expr_ref_vector & assumptions); }; }; diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 6d9969e8d..e91d8f340 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -332,12 +332,12 @@ namespace smt { args1.push_back(e1); args2.push_back(e2); for (unsigned i = 0; i < dimension; i++) { - expr * k = m.mk_app((*funcs)[i].get(), e1, e2); + expr * k = m.mk_app(funcs->get(i), e1, e2); args1.push_back(k); args2.push_back(k); } - expr * sel1 = mk_select(dimension+1, args1.c_ptr()); - expr * sel2 = mk_select(dimension+1, args2.c_ptr()); + expr * sel1 = mk_select(args1.size(), args1.c_ptr()); + expr * sel2 = mk_select(args2.size(), args2.c_ptr()); TRACE("ext", tout << mk_bounded_pp(sel1, m) << "\n" << mk_bounded_pp(sel2, m) << "\n";); literal n1_eq_n2 = mk_eq(e1, e2, true); literal sel1_eq_sel2 = mk_eq(sel1, sel2, true); diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index ce8def177..156a9aefb 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -427,6 +427,13 @@ namespace smt { } } + bool theory_array_full::should_research(expr_ref_vector & unsat_core) { + return m_bapa && m_bapa->should_research(unsat_core); + } + + void theory_array_full::add_theory_assumptions(expr_ref_vector & assumptions) { + if (m_bapa) m_bapa->add_theory_assumptions(assumptions); + } // // Assert axiom: diff --git a/src/smt/theory_array_full.h b/src/smt/theory_array_full.h index b249ec0b4..14c1d891e 100644 --- a/src/smt/theory_array_full.h +++ b/src/smt/theory_array_full.h @@ -61,6 +61,9 @@ namespace smt { theory_var mk_var(enode * n) override; void relevant_eh(app * n) override; + bool should_research(expr_ref_vector & unsat_core) override; + void add_theory_assumptions(expr_ref_vector & assumptions) override; + void add_const(theory_var v, enode* c); void add_map(theory_var v, enode* s); void add_parent_map(theory_var v, enode* s); diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 3a9553f95..bcfb3e845 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -630,7 +630,7 @@ void theory_diff_logic::new_edge(dl_var src, dl_var dst, unsigned num_edges lits.size(), lits.c_ptr(), params.size(), params.c_ptr()); } - ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, nullptr); + ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_TH_LEMMA, nullptr); if (dump_lemmas()) { symbol logic(m_is_lia ? "QF_LIA" : "QF_LRA"); ctx.display_lemma_as_smt_problem(lits.size(), lits.c_ptr(), false_literal, logic); diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp index 000a459d1..cf5d0b49e 100644 --- a/src/smt/theory_jobscheduler.cpp +++ b/src/smt/theory_jobscheduler.cpp @@ -385,7 +385,7 @@ namespace smt { expr_ref rhs(a.mk_add(start_e->get_owner(), a.mk_int(rational(delta, rational::ui64()))), m); lits.push_back(mk_eq_lit(end_e->get_owner(), rhs)); context& ctx = get_context(); - ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, CLS_AUX_LEMMA, nullptr); + ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, CLS_TH_LEMMA, nullptr); ast_manager& m = get_manager(); if (m.has_trace_stream()) { app_ref body(m); @@ -458,7 +458,7 @@ namespace smt { if (j == last_job) break; } context& ctx = get_context(); - ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, CLS_AUX_LEMMA, nullptr); + ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, CLS_TH_LEMMA, nullptr); } void theory_jobscheduler::propagate() { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 13b4dd6c2..00b6260fc 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2208,7 +2208,7 @@ public: js = alloc(theory_lemma_justification, get_id(), ctx(), m_core2.size(), m_core2.c_ptr(), m_params.size(), m_params.c_ptr()); } - ctx().mk_clause(m_core2.size(), m_core2.c_ptr(), js, CLS_AUX_LEMMA, nullptr); + ctx().mk_clause(m_core2.size(), m_core2.c_ptr(), js, CLS_TH_LEMMA, nullptr); } else { ctx().assign( diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 875fe8de4..209b78830 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -943,7 +943,7 @@ namespace smt { if (proofs_enabled()) { js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr()); } - ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, nullptr); + ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_TH_LEMMA, nullptr); } SASSERT(ctx.inconsistent()); } @@ -1373,12 +1373,8 @@ namespace smt { for (unsigned i = 0; i < lemmas.size(); ++i) { clause* cl = lemmas[i]; if (!cl->deleted()) { - unsigned sz = cl->get_num_literals(); - for (unsigned j = 0; j < sz; ++j) { - literal lit = cl->get_literal(j); + for (literal lit : *cl) { if (m_occs.contains(lit.var())) { - //std::cout << "deleting clause " << lit << " " << sz << "\n"; - //ctx.mark_as_deleted(cl); break; } } @@ -1537,7 +1533,7 @@ namespace smt { if (proofs_enabled()) { js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr()); } - ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, nullptr); + ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_TH_LEMMA, nullptr); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 673dbb02b..1c4b08371 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -320,7 +320,7 @@ void theory_seq::init(context* ctx) { m_arith_value.init(ctx); } -#define TRACEFIN(s) { TRACE("seq", tout << ">>" << s << "\n";); IF_VERBOSE(11, verbose_stream() << s << "\n"); } +#define TRACEFIN(s) { TRACE("seq", tout << ">>" << s << "\n";); IF_VERBOSE(31, verbose_stream() << s << "\n"); } final_check_status theory_seq::final_check_eh() {