mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f645f8d685
commit
a92c82d895
|
@ -971,6 +971,7 @@ namespace smt {
|
|||
//
|
||||
|
||||
void theory_pb::collect_statistics(::statistics& st) const {
|
||||
st.update("pb resolves", m_stats.m_num_resolves);
|
||||
st.update("pb conflicts", m_stats.m_num_conflicts);
|
||||
st.update("pb propagations", m_stats.m_num_propagations);
|
||||
st.update("pb predicates", m_stats.m_num_predicates);
|
||||
|
@ -1829,6 +1830,8 @@ namespace smt {
|
|||
|
||||
TRACE("pb", display(tout, c, true); );
|
||||
|
||||
return false;
|
||||
|
||||
bool_var v;
|
||||
context& ctx = get_context();
|
||||
ast_manager& m = get_manager();
|
||||
|
@ -2025,6 +2028,8 @@ namespace smt {
|
|||
}
|
||||
SASSERT(slack < 0);
|
||||
|
||||
++m_stats.m_num_resolves;
|
||||
|
||||
SASSERT(validate_antecedents(m_antecedents));
|
||||
TRACE("pb", tout << "assign " << m_antecedents << " ==> " << alit << "\n";);
|
||||
ctx.assign(alit, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), m_antecedents.size(), m_antecedents.c_ptr(), alit, 0, nullptr)));
|
||||
|
|
|
@ -97,6 +97,7 @@ namespace smt {
|
|||
unsigned m_num_conflicts;
|
||||
unsigned m_num_propagations;
|
||||
unsigned m_num_predicates;
|
||||
unsigned m_num_resolves;
|
||||
void reset() { memset(this, 0, sizeof(*this)); }
|
||||
stats() { reset(); }
|
||||
};
|
||||
|
|
Loading…
Reference in a new issue