mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
ea
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
b629960afb
commit
dca1dcca6d
|
@ -80,7 +80,7 @@ namespace arith {
|
|||
if (m_nla) m_nla->collect_statistics(st);
|
||||
}
|
||||
|
||||
void solver::add_assumptions() {
|
||||
void solver::explain_assumptions() {
|
||||
m_arith_hint.reset();
|
||||
unsigned i = 0;
|
||||
for (auto const & ev : m_explanation) {
|
||||
|
@ -119,7 +119,7 @@ namespace arith {
|
|||
if (!ctx.use_drat())
|
||||
return nullptr;
|
||||
m_arith_hint.m_ty = ty;
|
||||
add_assumptions();
|
||||
explain_assumptions();
|
||||
if (lit != sat::null_literal)
|
||||
m_arith_hint.m_literals.push_back({rational(1), ~lit});
|
||||
return &m_arith_hint;
|
||||
|
@ -129,7 +129,7 @@ namespace arith {
|
|||
if (!ctx.use_drat())
|
||||
return nullptr;
|
||||
m_arith_hint.m_ty = sat::hint_type::implied_eq_h;
|
||||
add_assumptions();
|
||||
explain_assumptions();
|
||||
m_arith_hint.m_diseqs.push_back({a->get_expr_id(), b->get_expr_id()});
|
||||
return &m_arith_hint;
|
||||
}
|
||||
|
|
|
@ -423,7 +423,7 @@ namespace arith {
|
|||
sat::proof_hint m_farkas2;
|
||||
sat::proof_hint const* explain(sat::hint_type ty, sat::literal lit = sat::null_literal);
|
||||
sat::proof_hint const* explain_implied_eq(euf::enode* a, euf::enode* b);
|
||||
void add_assumptions();
|
||||
void explain_assumptions();
|
||||
|
||||
|
||||
public:
|
||||
|
|
Loading…
Reference in a new issue