mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

expose model update

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-03-19 09:23:01 -07:00
parent a9d7026724
commit 6d836e7e2f
2 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -223,7 +223,7 @@ class lar_solver : public column_namer {
void insert_row_with_changed_bounds(unsigned rid);
void detect_rows_with_changed_bounds_for_column(unsigned j);
void detect_rows_with_changed_bounds();
void set_value_for_nbasic_column(unsigned j, const impq & new_val);
void update_x_and_inf_costs_for_columns_with_changed_bounds();
void update_x_and_inf_costs_for_columns_with_changed_bounds_tableau();
void solve_with_core_solver();
@ -355,6 +355,9 @@ public:
bp.consume(a, witness);
}
}
void set_value_for_nbasic_column(unsigned j, const impq& new_val);
// lp_assert(implied_bound_is_correctly_explained(ib, explanation)); }
constraint_index mk_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side);
void activate_check_on_equal(constraint_index, var_index&);

8
src/sat/sat_solver.cpp
View file

@ -2967,11 +2967,9 @@ namespace sat {
}
break;
case PS_SAT_CACHING:
if (m_search_state == s_sat) {
for (unsigned i = 0; i < m_phase.size(); ++i) {
m_phase[i] = m_best_phase[i];
}
}
if (m_search_state == s_sat)
for (unsigned i = 0; i < m_phase.size(); ++i)
m_phase[i] = m_best_phase[i];
break;
case PS_RANDOM:
for (auto& p : m_phase) p = (m_rand() % 2) == 0;