diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index 7786def0b..c03ff1d0f 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -258,7 +258,6 @@ struct nnf::imp { // configuration ---------------- nnf_mode m_mode; bool m_ignore_labels; - bool m_skolemize; // ------------------------------ name_exprs * m_name_nested_formulas; @@ -312,7 +311,6 @@ struct nnf::imp { TRACE("nnf", tout << "nnf-mode: " << m_mode << " " << mode_sym << "\n" << _p << "\n";); m_ignore_labels = p.ignore_labels(); - m_skolemize = p.skolemize(); m_max_memory = megabytes_to_bytes(p.max_memory()); m_skolemizer.set_sk_hack(p.sk_hack()); } @@ -759,7 +757,7 @@ struct nnf::imp { if (!visit(q->get_expr(), fr.m_pol, true)) return false; } - else if (is_forall(q) == fr.m_pol || !m_skolemize) { + else if (is_forall(q) == fr.m_pol) { if (!visit(q->get_expr(), fr.m_pol, true)) return false; } @@ -788,7 +786,7 @@ struct nnf::imp { } return true; } - else if (is_forall(q) == fr.m_pol || !m_skolemize) { + else if (is_forall(q) == fr.m_pol) { expr * new_expr = m_result_stack.back(); proof * new_expr_pr = proofs_enabled() ? m_result_pr_stack.back() : nullptr; diff --git a/src/ast/normal_forms/nnf_params.pyg b/src/ast/normal_forms/nnf_params.pyg index aac8fbb86..999465efc 100644 --- a/src/ast/normal_forms/nnf_params.pyg +++ b/src/ast/normal_forms/nnf_params.pyg @@ -5,5 +5,4 @@ def_module_params('nnf', ('sk_hack', BOOL, False, 'hack for VCC'), ('mode', SYMBOL, 'skolem', 'NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full'), - ('ignore_labels', BOOL, False, 'remove/ignore labels in the input formula, this option is ignored if proofs are enabled'), - ('skolemize', BOOL, True, 'skolemize (existential force) quantifiers'))) + ('ignore_labels', BOOL, False, 'remove/ignore labels in the input formula, this option is ignored if proofs are enabled'))) diff --git a/src/ast/normal_forms/pull_quant.cpp b/src/ast/normal_forms/pull_quant.cpp index 9ff75ca25..441db5234 100644 --- a/src/ast/normal_forms/pull_quant.cpp +++ b/src/ast/normal_forms/pull_quant.cpp @@ -24,11 +24,11 @@ Notes: struct pull_quant::imp { struct rw_cfg : public default_rewriter_cfg { - ast_manager & m_manager; + ast_manager & m; shift_vars m_shift; rw_cfg(ast_manager & m): - m_manager(m), + m(m), m_shift(m) { } @@ -43,14 +43,14 @@ struct pull_quant::imp { // Remark: (AND a1 ...) may be represented (NOT (OR (NOT a1) ...))) // So, when pulling a quantifier over a NOT, it becomes an exists. - if (m_manager.is_not(d)) { + if (m.is_not(d)) { SASSERT(num_children == 1); expr * child = children[0]; if (is_quantifier(child)) { quantifier * q = to_quantifier(child); expr * body = q->get_expr(); quantifier_kind k = q->get_kind() == forall_k ? exists_k : forall_k; - result = m_manager.update_quantifier(q, k, m_manager.mk_not(body)); + result = m.update_quantifier(q, k, m.mk_not(body)); return true; } else { @@ -86,7 +86,7 @@ struct pull_quant::imp { var_sorts.push_back(nested_q->get_decl_sort(j)); symbol s = nested_q->get_decl_name(j); if (std::find(var_names.begin(), var_names.end(), s) != var_names.end()) - var_names.push_back(m_manager.mk_fresh_var_name(s.is_numerical() ? nullptr : s.bare_str())); + var_names.push_back(m.mk_fresh_var_name(s.is_numerical() ? nullptr : s.bare_str())); else var_names.push_back(s); } @@ -96,8 +96,8 @@ struct pull_quant::imp { if (!var_sorts.empty()) { SASSERT(found_quantifier); // adjust the variable ids in formulas in new_children - expr_ref_buffer new_adjusted_children(m_manager); - expr_ref adjusted_child(m_manager); + expr_ref_buffer new_adjusted_children(m); + expr_ref adjusted_child(m); unsigned num_decls = var_sorts.size(); unsigned shift_amount = 0; TRACE("pull_quant", tout << "Result num decls:" << num_decls << "\n";); @@ -108,7 +108,7 @@ struct pull_quant::imp { // child will be in the scope of num_decls bound variables. m_shift(child, num_decls, adjusted_child); TRACE("pull_quant", tout << "shifted by: " << num_decls << "\n" << - mk_pp(child, m_manager) << "\n---->\n" << mk_pp(adjusted_child, m_manager) << "\n";); + mk_pp(child, m) << "\n---->\n" << mk_pp(adjusted_child, m) << "\n";); } else { quantifier * nested_q = to_quantifier(child); @@ -130,8 +130,8 @@ struct pull_quant::imp { shift_amount, // shift2 (shift by this amount if var idx < bound) adjusted_child); TRACE("pull_quant", tout << "shifted bound: " << nested_q->get_num_decls() << " shift1: " << shift_amount << - " shift2: " << (num_decls - nested_q->get_num_decls()) << "\n" << mk_pp(nested_q->get_expr(), m_manager) << - "\n---->\n" << mk_pp(adjusted_child, m_manager) << "\n";); + " shift2: " << (num_decls - nested_q->get_num_decls()) << "\n" << mk_pp(nested_q->get_expr(), m) << + "\n---->\n" << mk_pp(adjusted_child, m) << "\n";); shift_amount += nested_q->get_num_decls(); } new_adjusted_children.push_back(adjusted_child); @@ -150,11 +150,11 @@ struct pull_quant::imp { // 3) MBQI std::reverse(var_sorts.begin(), var_sorts.end()); std::reverse(var_names.begin(), var_names.end()); - result = m_manager.mk_quantifier(forall_children ? forall_k : exists_k, + result = m.mk_quantifier(forall_children ? forall_k : exists_k, var_sorts.size(), var_sorts.c_ptr(), var_names.c_ptr(), - m_manager.mk_app(d, new_adjusted_children.size(), new_adjusted_children.c_ptr()), + m.mk_app(d, new_adjusted_children.size(), new_adjusted_children.c_ptr()), w, qid); return true; @@ -167,7 +167,7 @@ struct pull_quant::imp { void pull_quant1(func_decl * d, unsigned num_children, expr * const * children, expr_ref & result) { if (!pull_quant1_core(d, num_children, children, result)) { - result = m_manager.mk_app(d, num_children, children); + result = m.mk_app(d, num_children, children); } } @@ -185,7 +185,7 @@ struct pull_quant::imp { var_names.append(nested_q->get_num_decls(), const_cast(nested_q->get_decl_names())); // Remark: patterns are ignored. // See comment in reduce1_app - result = m_manager.mk_forall(var_sorts.size(), + result = m.mk_forall(var_sorts.size(), var_sorts.c_ptr(), var_names.c_ptr(), nested_q->get_expr(), @@ -201,7 +201,7 @@ struct pull_quant::imp { } else { SASSERT(!is_quantifier(new_expr)); - result = m_manager.update_quantifier(q, new_expr); + result = m.update_quantifier(q, new_expr); } } @@ -218,36 +218,36 @@ struct pull_quant::imp { void pull_quant2(expr * n, expr_ref & r, proof_ref & pr) { pr = nullptr; if (is_app(n)) { - expr_ref_buffer new_args(m_manager); - expr_ref new_arg(m_manager); + expr_ref_buffer new_args(m); + expr_ref new_arg(m); ptr_buffer proofs; for (expr * arg : *to_app(n)) { pull_quant1(arg , new_arg); new_args.push_back(new_arg); if (new_arg != arg) - proofs.push_back(m_manager.mk_pull_quant(arg, to_quantifier(new_arg))); + proofs.push_back(m.mk_pull_quant(arg, to_quantifier(new_arg))); } pull_quant1(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr(), r); - if (m_manager.proofs_enabled()) { - app * r1 = m_manager.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr()); - proof * p1 = proofs.empty() ? nullptr : m_manager.mk_congruence(to_app(n), r1, proofs.size(), proofs.c_ptr()); - proof * p2 = r1 == r ? nullptr : m_manager.mk_pull_quant(r1, to_quantifier(r)); - pr = m_manager.mk_transitivity(p1, p2); + if (m.proofs_enabled()) { + app * r1 = m.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr()); + proof * p1 = proofs.empty() ? nullptr : m.mk_congruence(to_app(n), r1, proofs.size(), proofs.c_ptr()); + proof * p2 = r1 == r ? nullptr : m.mk_pull_quant(r1, to_quantifier(r)); + pr = m.mk_transitivity(p1, p2); } } else if (is_quantifier(n)) { - expr_ref new_expr(m_manager); + expr_ref new_expr(m); pull_quant1(to_quantifier(n)->get_expr(), new_expr); pull_quant1(to_quantifier(n), new_expr, r); - if (m_manager.proofs_enabled()) { - quantifier * q1 = m_manager.update_quantifier(to_quantifier(n), new_expr); + if (m.proofs_enabled()) { + quantifier * q1 = m.update_quantifier(to_quantifier(n), new_expr); proof * p1 = nullptr; if (n != q1) { - proof * p0 = m_manager.mk_pull_quant(n, to_quantifier(new_expr)); - p1 = m_manager.mk_quant_intro(to_quantifier(n), q1, p0); + proof * p0 = m.mk_pull_quant(n, to_quantifier(new_expr)); + p1 = m.mk_quant_intro(to_quantifier(n), q1, p0); } - proof * p2 = q1 == r ? nullptr : m_manager.mk_pull_quant(q1, to_quantifier(r)); - pr = m_manager.mk_transitivity(p1, p2); + proof * p2 = q1 == r ? nullptr : m.mk_pull_quant(q1, to_quantifier(r)); + pr = m.mk_transitivity(p1, p2); } } else { @@ -256,14 +256,14 @@ struct pull_quant::imp { } br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - if (!m_manager.is_or(f) && !m_manager.is_and(f) && !m_manager.is_not(f)) + if (!m.is_or(f) && !m.is_and(f) && !m.is_not(f)) return BR_FAILED; if (!pull_quant1_core(f, num, args, result)) return BR_FAILED; - if (m_manager.proofs_enabled()) { - result_pr = m_manager.mk_pull_quant(m_manager.mk_app(f, num, args), + if (m.proofs_enabled()) { + result_pr = m.mk_pull_quant(m.mk_app(f, num, args), to_quantifier(result.get())); } return BR_DONE; @@ -277,8 +277,11 @@ struct pull_quant::imp { proof_ref & result_pr) { if (is_exists(old_q)) { - UNREACHABLE(); - return false; + result = m.mk_not(new_body); + result = m.mk_not(m.update_quantifier(old_q, exists_k, result)); + if (m.proofs_enabled()) + m.mk_rewrite(old_q, result); + return true; } if (is_lambda(old_q)) { return false; @@ -288,8 +291,8 @@ struct pull_quant::imp { return false; pull_quant1_core(old_q, new_body, result); - if (m_manager.proofs_enabled()) - result_pr = m_manager.mk_pull_quant(old_q, to_quantifier(result.get())); + if (m.proofs_enabled()) + result_pr = m.mk_pull_quant(old_q, to_quantifier(result.get())); return true; } }; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 8b0d23f9c..f48ac57a6 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1106,6 +1106,10 @@ namespace sat { m_restart_threshold = m_config.m_restart_initial; } + if (reached_max_conflicts()) { + return l_undef; + } + // iff3_finder(*this)(); simplify_problem(); if (check_inconsistent()) return l_false; @@ -1718,17 +1722,6 @@ namespace sat { #endif } - unsigned solver::get_hash() const { - unsigned result = 0; - for (clause* cp : m_clauses) { - result = combine_hash(cp->size(), combine_hash(result, cp->id())); - } - for (clause* cp : m_learned) { - result = combine_hash(cp->size(), combine_hash(result, cp->id())); - } - return result; - } - bool solver::set_root(literal l, literal r) { return !m_ext || m_ext->set_root(l, r); } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index fd9af4a02..a9a9fcee0 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -569,8 +569,6 @@ namespace sat { private: - unsigned get_hash() const; - typedef hashtable index_set; u_map m_antecedents;