From de69874076673996685c6d1fbb49f821106d4668 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 Oct 2022 09:46:22 +0200 Subject: [PATCH] wip - adding proof checkers, fixes to quantifier proof certificates --- src/cmd_context/extra_cmds/proof_cmds.cpp | 15 ++++- src/sat/smt/CMakeLists.txt | 1 + src/sat/smt/euf_internalize.cpp | 21 +++--- src/sat/smt/euf_proof.cpp | 9 +++ src/sat/smt/euf_proof_checker.cpp | 21 +++--- src/sat/smt/euf_proof_checker.h | 4 +- src/sat/smt/euf_solver.h | 4 +- src/sat/smt/q_ematch.cpp | 2 +- src/sat/smt/q_mbi.cpp | 9 +++ src/sat/smt/q_proof_checker.cpp | 22 ++++--- src/sat/smt/q_proof_checker.h | 2 +- src/sat/smt/q_solver.cpp | 2 + src/sat/smt/sat_th.cpp | 7 +- src/sat/smt/tseitin_proof_checker.cpp | 78 +++++++++++++++++++++++ src/sat/smt/tseitin_proof_checker.h | 50 +++++++++++++++ src/sat/tactic/goal2sat.cpp | 52 +++++++++------ 16 files changed, 241 insertions(+), 58 deletions(-) create mode 100644 src/sat/smt/tseitin_proof_checker.cpp create mode 100644 src/sat/smt/tseitin_proof_checker.h diff --git a/src/cmd_context/extra_cmds/proof_cmds.cpp b/src/cmd_context/extra_cmds/proof_cmds.cpp index d792637ea..6c5f90f0e 100644 --- a/src/cmd_context/extra_cmds/proof_cmds.cpp +++ b/src/cmd_context/extra_cmds/proof_cmds.cpp @@ -158,10 +158,15 @@ public: // then check the simplified VC: phi(t) => psi. // in case psi is the literal instantiation, then the clause is a propositional tautology. // The VC function is a no-op if the proof hint does not have an associated vc generator. - m_checker.vc(proof_hint, clause); + expr_ref_vector vc(clause); + if (m_checker.vc(proof_hint, clause, vc)) { + std::cout << "(verified-" << proof_hint->get_name() << ")\n"; + add_clause(clause); + return; + } m_solver->push(); - for (expr* lit : clause) + for (expr* lit : vc) m_solver->assert_expr(m.mk_not(lit)); lbool is_sat = m_solver->check_sat(); if (is_sat != l_false) { @@ -175,7 +180,11 @@ public: exit(0); } m_solver->pop(1); - std::cout << "(verified-smt)\n"; + std::cout << "(verified-smt"; + if (proof_hint) std::cout << " " << mk_pp(proof_hint, m); + for (expr* arg : clause) + std::cout << " " << mk_pp(arg, m); + std::cout << ")\n"; add_clause(clause); } diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index 26bd835cc..6d75c0f1f 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -41,6 +41,7 @@ z3_add_component(sat_smt q_solver.cpp recfun_solver.cpp sat_th.cpp + tseitin_proof_checker.cpp user_solver.cpp COMPONENT_DEPENDENCIES sat diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index c8ae2a7c6..3c8956751 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -160,8 +160,13 @@ namespace euf { s().set_external(v); s().set_eliminated(v, false); sat::literal lit2 = literal(v, false); - s().mk_clause(~lit, lit2, sat::status::th(m_is_redundant, m.get_basic_family_id())); - s().mk_clause(lit, ~lit2, sat::status::th(m_is_redundant, m.get_basic_family_id())); + th_proof_hint* ph1 = nullptr, * ph2 = nullptr; + if (use_drat()) { + ph1 = mk_smt_hint(symbol("tseitin"), ~lit, lit2); + ph2 = mk_smt_hint(symbol("tseitin"), lit, ~lit2); + } + s().mk_clause(~lit, lit2, sat::status::th(m_is_redundant, m.get_basic_family_id(), ph1)); + s().mk_clause(lit, ~lit2, sat::status::th(m_is_redundant, m.get_basic_family_id(), ph2)); add_aux(~lit, lit2); add_aux(lit, ~lit2); lit = lit2; @@ -310,8 +315,8 @@ namespace euf { sat::literal lit_el = mk_literal(eq_el); add_root(~lit_c, lit_th); add_root(lit_c, lit_el); - s().add_clause(~lit_c, lit_th, st); - s().add_clause(lit_c, lit_el, st); + s().add_clause(~lit_c, lit_th, mk_tseitin_status(~lit_c, lit_th)); + s().add_clause(lit_c, lit_el, mk_tseitin_status(lit_c, lit_el)); } } else if (m.is_distinct(e)) { @@ -329,8 +334,8 @@ namespace euf { sat::literal some_eq = si.internalize(fml, m_is_redundant); add_root(~dist, ~some_eq); add_root(dist, some_eq); - s().add_clause(~dist, ~some_eq, st); - s().add_clause(dist, some_eq, st); + s().add_clause(~dist, ~some_eq, mk_tseitin_status(~dist, ~some_eq)); + s().add_clause(dist, some_eq, mk_tseitin_status(dist, some_eq)); } else if (m.is_eq(e, th, el) && !m.is_iff(e)) { sat::literal lit1 = expr2literal(e); @@ -341,8 +346,8 @@ namespace euf { sat::literal lit2 = expr2literal(e2); add_root(~lit1, lit2); add_root(lit1, ~lit2); - s().add_clause(~lit1, lit2, st); - s().add_clause(lit1, ~lit2, st); + s().add_clause(~lit1, lit2, mk_tseitin_status(~lit1, lit2)); + s().add_clause(lit1, ~lit2, mk_tseitin_status(lit1, ~lit2)); } } } diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index 73037fc8b..cc675e589 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -164,7 +164,16 @@ namespace euf { return mk_smt_hint(n, nl, lits, ne, m_expr_pairs.data()); } + sat::status solver::mk_tseitin_status(sat::literal a, sat::literal b) { + sat::literal lits[2] = { a, b }; + return mk_tseitin_status(2, lits); + } + sat::status solver::mk_tseitin_status(unsigned n, sat::literal const* lits) { + th_proof_hint* ph = use_drat() ? mk_smt_hint(symbol("tseitin"), n, lits) : nullptr; + return sat::status::th(m_is_redundant, m.get_basic_family_id(), ph); + } + expr* smt_proof_hint::get_hint(euf::solver& s) const { ast_manager& m = s.get_manager(); sort* proof = m.mk_proof_sort(); diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp index befde07bf..9b0f37c5e 100644 --- a/src/sat/smt/euf_proof_checker.cpp +++ b/src/sat/smt/euf_proof_checker.cpp @@ -22,6 +22,7 @@ Author: #include "sat/smt/euf_proof_checker.h" #include "sat/smt/arith_proof_checker.h" #include "sat/smt/q_proof_checker.h" +#include "sat/smt/tseitin_proof_checker.h" #include namespace euf { @@ -145,10 +146,7 @@ namespace euf { else merge(x, y); } - else if (m.is_not(arg, arg)) - merge(arg, m.mk_false()); - else - merge(arg, m.mk_true()); + merge(arg, sign ? m.mk_false() : m.mk_true()); } else if (m.is_proof(arg)) { if (!is_app(arg)) @@ -277,6 +275,7 @@ namespace euf { add_plugin(alloc(res_proof_checker, m, *this)); add_plugin(alloc(q::proof_checker, m)); add_plugin(alloc(smt_proof_checker_plugin, m, symbol("datatype"))); // no-op datatype proof checker + add_plugin(alloc(tseitin::proof_checker, m)); } proof_checker::~proof_checker() { @@ -302,10 +301,8 @@ namespace euf { proof_checker_plugin* p = nullptr; if (!m_map.find(a->get_decl()->get_name(), p)) return false; - if (!p->check(a)) { - std::cout << "(missed-hint " << mk_pp(e, m) << ")\n"; - return false; - } + if (!p->check(a)) + return false; return true; } @@ -319,14 +316,14 @@ namespace euf { return r; } - void proof_checker::vc(expr* e, expr_ref_vector& clause) { + bool proof_checker::vc(expr* e, expr_ref_vector const& clause, expr_ref_vector& v) { SASSERT(is_app(e)); app* a = to_app(e); proof_checker_plugin* p = nullptr; if (m_map.find(a->get_name(), p)) - p->vc(a, clause); - else - IF_VERBOSE(0, verbose_stream() << "there is no proof plugin for " << mk_pp(e, m) << "\n"); + return p->vc(a, clause, v); + IF_VERBOSE(0, verbose_stream() << "there is no proof plugin for " << mk_pp(e, m) << "\n"); + return false; } bool proof_checker::check(expr_ref_vector const& clause1, expr* e, expr_ref_vector & units) { diff --git a/src/sat/smt/euf_proof_checker.h b/src/sat/smt/euf_proof_checker.h index 530644488..0d3dbcb9e 100644 --- a/src/sat/smt/euf_proof_checker.h +++ b/src/sat/smt/euf_proof_checker.h @@ -30,7 +30,7 @@ namespace euf { virtual bool check(app* jst) = 0; virtual expr_ref_vector clause(app* jst) = 0; virtual void register_plugins(proof_checker& pc) = 0; - virtual void vc(app* jst, expr_ref_vector& clause) { } + virtual bool vc(app* jst, expr_ref_vector const& clause, expr_ref_vector& v) { return false; } }; class proof_checker { @@ -45,7 +45,7 @@ namespace euf { void register_plugin(symbol const& rule, proof_checker_plugin*); bool check(expr* jst); expr_ref_vector clause(expr* jst); - void vc(expr* jst, expr_ref_vector& clause); + bool vc(expr* jst, expr_ref_vector const& clause, expr_ref_vector& v); bool check(expr_ref_vector const& clause, expr* e, expr_ref_vector& units); }; diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 1a8186eaa..d6fac4aff 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -390,7 +390,7 @@ namespace euf { return mk_smt_hint(n, lits.size(), lits.data(), 0, (expr_pair const*) nullptr); } smt_proof_hint* mk_smt_hint(symbol const& n, unsigned nl, literal const* lits, unsigned ne, expr_pair const* eqs, unsigned nd = 0, expr_pair const* deqs = nullptr); - smt_proof_hint* mk_smt_hint(symbol const& n, unsigned nl, literal const* lits, unsigned ne, enode_pair const* eqs); + smt_proof_hint* mk_smt_hint(symbol const& n, unsigned nl, literal const* lits, unsigned ne = 0, enode_pair const* eqs = nullptr); smt_proof_hint* mk_smt_hint(symbol const& n, literal lit, unsigned ne, expr_pair const* eqs) { return mk_smt_hint(n, 1, &lit, ne, eqs); } smt_proof_hint* mk_smt_hint(symbol const& n, literal lit) { return mk_smt_hint(n, 1, &lit, 0, (expr_pair const*)nullptr); } smt_proof_hint* mk_smt_hint(symbol const& n, literal l1, literal l2) { literal ls[2] = {l1,l2}; return mk_smt_hint(n, 2, ls, 0, (expr_pair const*)nullptr); } @@ -399,6 +399,8 @@ namespace euf { smt_proof_hint* mk_smt_prop_hint(symbol const& n, literal lit, expr* a, expr* b) { expr_pair e(a, b); return mk_smt_hint(n, 1, &lit, 0, nullptr, 1, &e); } smt_proof_hint* mk_smt_prop_hint(symbol const& n, literal lit, enode* a, enode* b) { return mk_smt_prop_hint(n, lit, a->get_expr(), b->get_expr()); } smt_proof_hint* mk_smt_hint(symbol const& n, enode* a, enode* b) { expr_pair e(a->get_expr(), b->get_expr()); return mk_smt_hint(n, 0, nullptr, 1, &e); } + sat::status mk_tseitin_status(sat::literal a, sat::literal b); + sat::status mk_tseitin_status(unsigned n, sat::literal const* lits); scoped_ptr m_proof_out; diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index 4a834d355..2c5ab80ae 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -387,7 +387,7 @@ namespace q { m_qs.log_instantiation(lits, &j); euf::th_proof_hint* ph = nullptr; if (ctx.use_drat()) - ph = q_proof_hint::mk(ctx, lits, j.m_clause.size(), j.m_binding); + ph = q_proof_hint::mk(ctx, lits, j.m_clause.num_decls(), j.m_binding); m_qs.add_clause(lits, ph); } diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index 0802f71c9..03f887ac1 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -232,6 +232,7 @@ namespace q { } expr_ref_vector mbqi::extract_binding(quantifier* q) { + SASSERT(!ctx.use_drat() || !m_defs.empty()); if (!m_defs.empty()) { expr_safe_replace sub(m); for (unsigned i = m_defs.size(); i-- > 0; ) { @@ -543,6 +544,14 @@ namespace q { body = subst(q_flat->get_expr(), binding); if (is_forall(q)) body = ::mk_not(m, body); + if (ctx.use_drat()) { + m_defs.reset(); + for (unsigned i = 0; i < binding.size(); ++i) { + expr_ref v(qb.vars.get(i), m); + expr_ref t(binding.get(i), m); + m_defs.push_back(mbp::def(v, t)); + } + } add_instantiation(q, body); ++num_bindings; } diff --git a/src/sat/smt/q_proof_checker.cpp b/src/sat/smt/q_proof_checker.cpp index eecf10fe6..8ddd3d75a 100644 --- a/src/sat/smt/q_proof_checker.cpp +++ b/src/sat/smt/q_proof_checker.cpp @@ -25,27 +25,33 @@ namespace q { expr_ref_vector result(m); for (expr* arg : *jst) if (!is_bind(arg)) - result.push_back(arg); + result.push_back(mk_not(m, arg)); return result; } expr_ref_vector proof_checker::binding(app* jst) { expr_ref_vector result(m); for (expr* arg : *jst) - if (is_bind(arg)) - result.push_back(to_app(arg)->get_arg(0)); + if (is_bind(arg)) { + result.append(to_app(arg)->get_num_args(), to_app(arg)->get_args()); + break; + } return result; } - void proof_checker::vc(app* jst, expr_ref_vector& clause) { + bool proof_checker::vc(app* jst, expr_ref_vector const& clause0, expr_ref_vector& v) { expr* q = nullptr; if (!is_inst(jst)) - return; - SASSERT(clause.size() >= 2); - VERIFY(m.is_not(clause.get(0), q) && is_forall(q)); + return false; + auto clause1 = clause(jst); + SASSERT(clause1.size() >= 2); + VERIFY(m.is_not(clause1.get(0), q) && is_forall(q)); auto inst = binding(jst); expr_ref qi = instantiate(m, to_quantifier(q), inst.begin()); - clause[0] = m.mk_not(qi); + clause1[0] = m.mk_not(qi); + v.reset(); + v.append(clause1); + return qi == clause1.get(1); } bool proof_checker::is_inst(expr* jst) { diff --git a/src/sat/smt/q_proof_checker.h b/src/sat/smt/q_proof_checker.h index d60737585..6b309d1c6 100644 --- a/src/sat/smt/q_proof_checker.h +++ b/src/sat/smt/q_proof_checker.h @@ -53,7 +53,7 @@ namespace q { pc.register_plugin(symbol("inst"), this); } - void vc(app* jst, expr_ref_vector& clause) override; + bool vc(app* jst, expr_ref_vector const& clause, expr_ref_vector& v) override; }; diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index c99311f4e..7fd7be97e 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -365,6 +365,7 @@ namespace q { } q_proof_hint* q_proof_hint::mk(euf::solver& s, sat::literal_vector const& lits, unsigned n, euf::enode* const* bindings) { + SASSERT(n > 0); auto* mem = s.get_region().allocate(q_proof_hint::get_obj_size(n, lits.size())); q_proof_hint* ph = new (mem) q_proof_hint(n, lits.size()); for (unsigned i = 0; i < n; ++i) @@ -375,6 +376,7 @@ namespace q { } q_proof_hint* q_proof_hint::mk(euf::solver& s, sat::literal l1, sat::literal l2, unsigned n, expr* const* bindings) { + SASSERT(n > 0); auto* mem = s.get_region().allocate(q_proof_hint::get_obj_size(n, 2)); q_proof_hint* ph = new (mem) q_proof_hint(n, 2); for (unsigned i = 0; i < n; ++i) diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index 7fc54f7cd..bf2e04dc5 100644 --- a/src/sat/smt/sat_th.cpp +++ b/src/sat/smt/sat_th.cpp @@ -144,10 +144,9 @@ namespace euf { return is_new; } - bool th_euf_solver::add_clause(sat::literal a, sat::literal b, th_proof_hint const* ps) { - SASSERT(ps); + bool th_euf_solver::add_clause(sat::literal a, sat::literal b, th_proof_hint const* ph) { sat::literal lits[2] = { a, b }; - return add_clause(2, lits, ps); + return add_clause(2, lits, ph); } bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c, th_proof_hint const* ps) { @@ -161,7 +160,7 @@ namespace euf { } bool th_euf_solver::add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps) { - //SASSERT(!ctx.use_drat() || ps); - very far from true, and isn't a requirement + SASSERT(!ctx.use_drat() || ps); // - very far from true, and isn't a requirement bool was_true = false; for (unsigned i = 0; i < n; ++i) was_true |= is_true(lits[i]); diff --git a/src/sat/smt/tseitin_proof_checker.cpp b/src/sat/smt/tseitin_proof_checker.cpp new file mode 100644 index 000000000..658a8d72c --- /dev/null +++ b/src/sat/smt/tseitin_proof_checker.cpp @@ -0,0 +1,78 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + tseitin_proof_checker.cpp + +Abstract: + + Plugin for checking quantifier instantiations + +Author: + + Nikolaj Bjorner (nbjorner) 2022-10-07 + + +--*/ + +#include "sat/smt/tseitin_proof_checker.h" + +namespace tseitin { + + + expr_ref_vector proof_checker::clause(app* jst) { + expr_ref_vector result(m); + result.append(jst->get_num_args(), jst->get_args()); + return result; + } + + bool proof_checker::check(app* jst) { + expr* main_expr = nullptr; + unsigned max_depth = 0; + for (expr* arg : *jst) { + if (get_depth(arg) > max_depth) { + main_expr = arg; + max_depth = get_depth(arg); + } + } + if (!main_expr) + return false; + + expr* a; + if (m.is_not(main_expr, a)) { + for (expr* arg : *jst) + if (equiv(a, arg)) + return true; + + if (m.is_and(a)) + for (expr* arg1 : *to_app(a)) + for (expr* arg2 : *jst) + if (equiv(arg1, arg2)) + return true; + + if (m.is_or(a)) + return false; + if (m.is_implies(a)) + return false; + if (m.is_eq(a)) + return false; + if (m.is_ite(a)) + return false; + if (m.is_distinct(a)) + return false; + } + return false; + } + + bool proof_checker::equiv(expr* a, expr* b) { + if (a == b) + return true; + expr* x, *y, *z, *u; + if (m.is_eq(a, x, y) && m.is_eq(b, z, u)) + return x == u && y == z; + return false; + } + + +} diff --git a/src/sat/smt/tseitin_proof_checker.h b/src/sat/smt/tseitin_proof_checker.h new file mode 100644 index 000000000..8b975dbb6 --- /dev/null +++ b/src/sat/smt/tseitin_proof_checker.h @@ -0,0 +1,50 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + tseitin_proof_checker.h + +Abstract: + + Plugin for checking quantifier instantiations + +Author: + + Nikolaj Bjorner (nbjorner) 2022-10-07 + + +--*/ +#pragma once + +#include "util/obj_pair_set.h" +#include "ast/ast_trail.h" +#include "ast/ast_util.h" +#include "sat/smt/euf_proof_checker.h" +#include + +namespace tseitin { + + class proof_checker : public euf::proof_checker_plugin { + ast_manager& m; + + bool equiv(expr* a, expr* b); + + public: + proof_checker(ast_manager& m): + m(m) { + } + + ~proof_checker() override {} + + expr_ref_vector clause(app* jst) override; + + bool check(app* jst) override; + + void register_plugins(euf::proof_checker& pc) override { + pc.register_plugin(symbol("tseitin"), this); + } + + }; + +} diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 2d390b4f2..ef156fbd5 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -68,15 +68,15 @@ struct goal2sat::imp : public sat::sat_internalizer { sat::solver_core & m_solver; atom2bool_var & m_map; dep2asm_map & m_dep2asm; - obj_map* m_expr2var_replay { nullptr }; + obj_map* m_expr2var_replay = nullptr; bool m_ite_extra; unsigned long long m_max_memory; expr_ref_vector m_trail; func_decl_ref_vector m_unhandled_funs; bool m_default_external; - bool m_euf { false }; - bool m_is_redundant { false }; - bool m_top_level { false }; + bool m_euf = false; + bool m_is_redundant = false; + bool m_top_level = false; sat::literal_vector aig_lits; imp(ast_manager & _m, params_ref const & p, sat::solver_core & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external): @@ -108,8 +108,24 @@ struct goal2sat::imp : public sat::sat_internalizer { throw tactic_exception(std::move(s0)); } - sat::status mk_status() const { - return sat::status::th(m_is_redundant, m.get_basic_family_id()); + symbol m_tseitin = symbol("tseitin"); + + euf::th_proof_hint* mk_tseitin(unsigned n, sat::literal const* lits) { + if (m_euf && ensure_euf()->use_drat()) + return ensure_euf()->mk_smt_hint(m_tseitin, n, lits); + return nullptr; + } + + euf::th_proof_hint* mk_tseitin(sat::literal a, sat::literal b) { + if (m_euf && ensure_euf()->use_drat()) { + sat::literal lits[2] = { a, b }; + return ensure_euf()->mk_smt_hint(m_tseitin, 2, lits); + } + return nullptr; + } + + sat::status mk_status(euf::th_proof_hint* ph = nullptr) const { + return sat::status::th(m_is_redundant, m.get_basic_family_id(), ph); } bool relevancy_enabled() { @@ -124,42 +140,42 @@ struct goal2sat::imp : public sat::sat_internalizer { mk_clause(1, &l); } - void mk_clause(sat::literal l1, sat::literal l2) { + void mk_clause(sat::literal l1, sat::literal l2, euf::th_proof_hint* ph = nullptr) { sat::literal lits[2] = { l1, l2 }; - mk_clause(2, lits); + mk_clause(2, lits, ph); } - void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3) { + void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3, euf::th_proof_hint* ph = nullptr) { sat::literal lits[3] = { l1, l2, l3 }; - mk_clause(3, lits); + mk_clause(3, lits, ph); } - void mk_clause(unsigned n, sat::literal * lits) { + void mk_clause(unsigned n, sat::literal * lits, euf::th_proof_hint* ph = nullptr) { TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";); if (relevancy_enabled()) ensure_euf()->add_aux(n, lits); - m_solver.add_clause(n, lits, mk_status()); + m_solver.add_clause(n, lits, mk_status(ph)); } void mk_root_clause(sat::literal l) { mk_root_clause(1, &l); } - void mk_root_clause(sat::literal l1, sat::literal l2) { + void mk_root_clause(sat::literal l1, sat::literal l2, euf::th_proof_hint* ph = nullptr) { sat::literal lits[2] = { l1, l2 }; - mk_root_clause(2, lits); + mk_root_clause(2, lits, ph); } - void mk_root_clause(sat::literal l1, sat::literal l2, sat::literal l3) { + void mk_root_clause(sat::literal l1, sat::literal l2, sat::literal l3, euf::th_proof_hint* ph = nullptr) { sat::literal lits[3] = { l1, l2, l3 }; - mk_root_clause(3, lits); + mk_root_clause(3, lits, ph); } - void mk_root_clause(unsigned n, sat::literal * lits) { + void mk_root_clause(unsigned n, sat::literal * lits, euf::th_proof_hint* ph = nullptr) { TRACE("goal2sat", tout << "mk_root_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";); if (relevancy_enabled()) ensure_euf()->add_root(n, lits); - m_solver.add_clause(n, lits, m_is_redundant ? mk_status() : sat::status::input()); + m_solver.add_clause(n, lits, m_is_redundant ? mk_status(ph) : sat::status::input()); } sat::bool_var add_var(bool is_ext, expr* n) {