mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

fix sign for binary propagation hints

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-05-29 10:32:05 -07:00
parent bffa7ff2f6
commit cb279fba2b
3 changed files with 8 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/sat/sat_drat.cpp
View file

@ -946,6 +946,11 @@ namespace sat {
s += 6; s += 6;
return true; return true;
} }
if (0 == strncmp(s, "cut", 3)) {
h.m_ty = hint_type::cut_h;
s += 3;
return true;
}
return false; return false;
}; };
@ -999,7 +1004,6 @@ namespace sat {
return; return;
ws(); ws();
} }
return;
} }
} }

4
src/sat/smt/arith_axioms.cpp
View file

@ -238,8 +238,8 @@ namespace arith {
sat::proof_hint* bound_params = nullptr; sat::proof_hint* bound_params = nullptr;
if (ctx.use_drat()) { if (ctx.use_drat()) {
bound_params = &m_farkas2; bound_params = &m_farkas2;
m_farkas2.m_literals[0] = std::make_pair(rational(1), l1); m_farkas2.m_literals[0] = std::make_pair(rational(1), ~l1);
m_farkas2.m_literals[1] = std::make_pair(rational(1), l2); m_farkas2.m_literals[1] = std::make_pair(rational(1), ~l2);
} }
add_clause(l1, l2, bound_params); add_clause(l1, l2, bound_params);
}; };

2
src/sat/smt/arith_solver.cpp
View file

@ -201,7 +201,7 @@ namespace arith {
if (ctx.use_drat()) { if (ctx.use_drat()) {
ph = &m_farkas2; ph = &m_farkas2;
m_farkas2.m_literals[0] = std::make_pair(rational(1), lit1); m_farkas2.m_literals[0] = std::make_pair(rational(1), lit1);
m_farkas2.m_literals[1] = std::make_pair(rational(1), lit2); m_farkas2.m_literals[1] = std::make_pair(rational(1), ~lit2);
} }
assign(lit2, m_core, m_eqs, ph); assign(lit2, m_core, m_eqs, ph);
++m_stats.m_bounds_propagations; ++m_stats.m_bounds_propagations;