mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix coefficient extraction and passing in Farkas lemmas, thanks to H. F. Bryant
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
68663fd97a
commit
0ab102cbec
|
@ -136,9 +136,22 @@ namespace arith {
|
|||
arith_proof_hint const* solver::explain_conflict(sat::literal_vector const& core, euf::enode_pair_vector const& eqs) {
|
||||
arith_proof_hint* hint = nullptr;
|
||||
if (ctx.use_drat()) {
|
||||
m_coeffs.reset();
|
||||
for (auto const& e : m_explanation) {
|
||||
if (inequality_source == m_constraint_sources[e.ci()])
|
||||
m_coeffs.push_back(e.coeff());
|
||||
}
|
||||
|
||||
m_arith_hint.set_type(ctx, hint_type::farkas_h);
|
||||
for (auto lit : core)
|
||||
m_arith_hint.add_lit(rational::one(), lit);
|
||||
if (m_coeffs.size() == core.size()) {
|
||||
unsigned i = 0;
|
||||
for (auto lit : core)
|
||||
m_arith_hint.add_lit(m_coeffs[i], lit), ++i;
|
||||
}
|
||||
else {
|
||||
for (auto lit : core)
|
||||
m_arith_hint.add_lit(rational::one(), lit);
|
||||
}
|
||||
for (auto const& [a,b] : eqs)
|
||||
m_arith_hint.add_eq(a, b);
|
||||
hint = m_arith_hint.mk(ctx);
|
||||
|
|
|
@ -251,6 +251,7 @@ namespace arith {
|
|||
lp::explanation m_explanation;
|
||||
vector<nla::lemma> m_nla_lemma_vector;
|
||||
literal_vector m_core, m_core2;
|
||||
vector<rational> m_coeffs;
|
||||
svector<enode_pair> m_eqs;
|
||||
vector<parameter> m_params;
|
||||
nla::lemma m_lemma;
|
||||
|
|
|
@ -398,6 +398,8 @@ namespace smt {
|
|||
bool qi_queue::final_check_eh() {
|
||||
TRACE("qi_queue", display_delayed_instances_stats(tout); tout << "lazy threshold: " << m_params.m_qi_lazy_threshold
|
||||
<< ", scope_level: " << m_context.get_scope_level() << "\n";);
|
||||
|
||||
verbose_stream() << "delayed entries " << m_delayed_entries.size() << "\n";
|
||||
if (m_params.m_qi_conservative_final_check) {
|
||||
bool init = false;
|
||||
float min_cost = 0.0;
|
||||
|
|
Loading…
Reference in a new issue