mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-12-06 10:50:27 -08:00
parent 2e5eb2dde2
commit c3c7aad1a8
3 changed files with 9 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/python/z3/z3.py
View file

@ -10656,7 +10656,7 @@ class UserPropagateBase:
return Z3_solver_propagate_register(self.ctx_ref(), self.solver.solver, e.ast)
#
# Propagation can only be invoked as during a fixed-callback.
# Propagation can only be invoked as during a fixed or final callback.
#
def propagate(self, e, ids, eqs = []):
num_fixed = len(ids)

5
src/math/lp/lar_solver.cpp
View file

@ -1823,8 +1823,9 @@ namespace lp {
}
}
SASSERT(column_is_fixed(k));
if (j != k) {
CTRACE("arith", !column_is_fixed(k), print_terms(tout););
// SASSERT(column_is_fixed(k));
if (j != k && column_is_fixed(k)) {
SASSERT(column_is_int(j) == column_is_int(k));
equal_to_j = column_to_reported_index(k);
TRACE("lar_solver", tout << "found equal column k = " << k <<

11
src/smt/user_propagator.cpp
View file

@ -69,9 +69,12 @@ theory * user_propagator::mk_fresh(context * new_ctx) {
final_check_status user_propagator::final_check_eh() {
if (!(bool)m_final_eh)
return FC_DONE;
force_push();
unsigned sz = m_prop.size();
m_final_eh(m_user_context, this);
return sz == m_prop.size() ? FC_DONE : FC_CONTINUE;
propagate();
bool done = (sz == m_prop.size()) && !ctx.inconsistent();
return done ? FC_DONE : FC_CONTINUE;
}
void user_propagator::new_fixed_eh(theory_var v, expr* value, unsigned num_lits, literal const* jlits) {
@ -122,11 +125,7 @@ void user_propagator::propagate() {
for (auto const& p : prop.m_eqs)
m_eqs.push_back(enode_pair(get_enode(p.first), get_enode(p.second)));
DEBUG_CODE(for (auto const& p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root()););
IF_VERBOSE(5,
for (auto lit : m_lits)
verbose_stream() << lit << ":" << ctx.get_assignment(lit) << " ";
verbose_stream() << "\n";);
if (m.is_false(prop.m_conseq)) {
js = ctx.mk_justification(
ext_theory_conflict_justification(