mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix #4143

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-04-28 14:11:39 -07:00
parent fa1197a78f
commit ccce599bad
5 changed files with 46 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/smt/diff_logic.h
View file

@ -263,7 +263,7 @@ class dl_graph {
public:
// An assignment is feasible if all edges are feasible.
bool is_feasible() const {
bool is_feasible_dbg() const {
for (unsigned i = 0; i < m_edges.size(); ++i) {
if (!is_feasible(m_edges[i])) {
return false;
@ -422,7 +422,7 @@ private:
}
if (m_heap.empty()) {
SASSERT(is_feasible());
SASSERT(is_feasible_dbg());
reset_marks();
m_assignment_stack.reset();
return true;
@ -498,7 +498,7 @@ public:
// Add an new weighted edge "source --weight--> target" with explanation ex.
edge_id add_edge(dl_var source, dl_var target, const numeral & weight, const explanation & ex) {
// SASSERT(is_feasible());
// SASSERT(is_feasible_dbg());
edge_id new_id = m_edges.size();
m_edges.push_back(edge(source, target, weight, m_timestamp, ex));
m_activity.push_back(0);
@ -513,7 +513,7 @@ public:
// The method assumes the graph is feasible before the invocation.
bool enable_edge(edge_id id) {
edge& e = m_edges[id];
SASSERT(is_feasible());
SASSERT(is_feasible_dbg());
bool r = true;
if (!e.is_enabled()) {
e.enable(m_timestamp);
@ -523,7 +523,7 @@ public:
r = make_feasible(id);
}
SASSERT(check_invariant());
SASSERT(!r || is_feasible());
SASSERT(!r || is_feasible_dbg());
m_enabled_edges.push_back(id);
}
return r;
@ -862,7 +862,7 @@ public:
// Create a new scope.
// That is, save the number of edges in the graph.
void push() {
// SASSERT(is_feasible()); <<< I relaxed this condition
// SASSERT(is_feasible_dbg()); <<< I relaxed this condition
m_trail_stack.push_back(scope(m_edges.size(), m_enabled_edges.size(), m_timestamp));
}
@ -896,20 +896,20 @@ public:
}
m_trail_stack.shrink(new_lvl);
SASSERT(check_invariant());
// SASSERT(is_feasible()); <<< I relaxed the condition in push(), so this assertion is not valid anymore.
// SASSERT(is_feasible_dbg()); <<< I relaxed the condition in push(), so this assertion is not valid anymore.
}
// Make m_assignment[v] == zero
// The whole assignment is adjusted in a way feasibility is preserved.
// This method should only be invoked if the current assignment if feasible.
void set_to_zero(dl_var v) {
SASSERT(is_feasible());
SASSERT(is_feasible_dbg());
if (!m_assignment[v].is_zero()) {
numeral k = m_assignment[v];
for (auto& a : m_assignment) {
a -= k;
}
SASSERT(is_feasible());
SASSERT(is_feasible_dbg());
}
}
@ -929,7 +929,7 @@ public:
if (!m_assignment[w].is_zero()) {
enable_edge(add_edge(v, w, numeral(0), explanation()));
enable_edge(add_edge(w, v, numeral(0), explanation()));
SASSERT(is_feasible());
SASSERT(is_feasible_dbg());
}
}
return;
@ -947,7 +947,7 @@ public:
if (!m_assignment[v].is_zero() || !m_assignment[w].is_zero()) {
enable_edge(add_edge(v, w, numeral(0), explanation()));
enable_edge(add_edge(w, v, numeral(0), explanation()));
SASSERT(is_feasible());
SASSERT(is_feasible_dbg());
}
}

2
src/smt/theory_diff_logic.h
View file

@ -171,6 +171,7 @@ namespace smt {
arith_eq_adapter m_arith_eq_adapter;
theory_diff_logic_statistics m_stats;
Graph m_graph;
bool m_consistent;
theory_var m_izero, m_rzero; // cache the variable representing the zero variable.
int_vector m_scc_id; // Cheap equality propagation
eq_prop_info_set m_eq_prop_info_set; // set of existing equality prop infos
@ -230,6 +231,7 @@ namespace smt {
m_params(params),
m_util(m),
m_arith_eq_adapter(*this, params, m_util),
m_consistent(true),
m_izero(null_theory_var),
m_rzero(null_theory_var),
m_terms(m),

34
src/smt/theory_diff_logic_def.h
View file

@ -72,6 +72,8 @@ void theory_diff_logic<Ext>::init(context * ctx) {
template<typename Ext>
bool theory_diff_logic<Ext>::internalize_term(app * term) {
if (!m_consistent)
return false;
bool result = null_theory_var != mk_term(term);
CTRACE("arith", !result, tout << "Did not internalize " << mk_pp(term, get_manager()) << "\n";);
if (!result) {
@ -161,6 +163,8 @@ void theory_diff_logic<Ext>::found_non_diff_logic_expr(expr * n) {
template<typename Ext>
bool theory_diff_logic<Ext>::internalize_atom(app * n, bool gate_ctx) {
if (!m_consistent)
return false;
context & ctx = get_context();
if (!m_util.is_le(n) && !m_util.is_ge(n)) {
found_non_diff_logic_expr(n);
@ -341,7 +345,7 @@ void theory_diff_logic<Ext>::pop_scope_eh(unsigned num_scopes) {
m_scopes.shrink(new_lvl);
unsigned num_edges = m_graph.get_num_edges();
m_graph.pop(num_scopes);
CTRACE("arith", !m_graph.is_feasible(), m_graph.display(tout););
CTRACE("arith", !m_graph.is_feasible_dbg(), m_graph.display(tout););
if (num_edges != m_graph.get_num_edges() && m_num_simplex_edges > 0) {
m_S.reset();
m_num_simplex_edges = 0;
@ -540,11 +544,13 @@ void theory_diff_logic<Ext>::propagate() {
template<typename Ext>
void theory_diff_logic<Ext>::inc_conflicts() {
m_stats.m_num_conflicts++;
if (m_params.m_arith_adaptive) {
double g = m_params.m_arith_adaptive_propagation_threshold;
m_agility = m_agility*g + 1 - g;
}
get_context().push_trail(value_trail<context, bool>(m_consistent));
m_consistent = false;
m_stats.m_num_conflicts++;
if (m_params.m_arith_adaptive) {
double g = m_params.m_arith_adaptive_propagation_threshold;
m_agility = m_agility*g + 1 - g;
}
}
template<typename Ext>
@ -568,6 +574,7 @@ bool theory_diff_logic<Ext>::propagate_atom(atom* a) {
if (!m_graph.enable_edge(edge_id)) {
TRACE("arith", display(tout););
set_neg_cycle_conflict();
return false;
}
return true;
@ -741,7 +748,6 @@ theory_var theory_diff_logic<Ext>::mk_term(app* n) {
TRACE("arith", tout << mk_pp(n, get_manager()) << "\n";);
rational r;
if (m_util.is_numeral(n, r)) {
return mk_num(n, r);
@ -944,10 +950,10 @@ void theory_diff_logic<Ext>::display(std::ostream & out) const {
}
template<typename Ext>
bool theory_diff_logic<Ext>::is_consistent() const {
bool theory_diff_logic<Ext>::is_consistent() const {
DEBUG_CODE(
context& ctx = get_context();
for (unsigned i = 0; m_graph.is_feasible() && i < m_atoms.size(); ++i) {
for (unsigned i = 0; m_graph.is_feasible_dbg() && i < m_atoms.size(); ++i) {
atom* a = m_atoms[i];
bool_var bv = a->get_bool_var();
lbool asgn = ctx.get_assignment(bv);
@ -958,7 +964,7 @@ bool theory_diff_logic<Ext>::is_consistent() const {
SASSERT(m_graph.is_feasible(edge_id));
}
});
return m_graph.is_feasible();
return m_consistent;
}
@ -1230,8 +1236,8 @@ theory_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker, bool& has_shar
Simplex& S = m_S;
ast_manager& m = get_manager();
CTRACE("arith",!m_graph.is_feasible(), m_graph.display(tout););
SASSERT(m_graph.is_feasible());
CTRACE("arith",!m_graph.is_feasible_dbg(), m_graph.display(tout););
SASSERT(m_graph.is_feasible_dbg());
update_simplex(S);
@ -1294,8 +1300,8 @@ theory_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker, bool& has_shar
rational r = rational(val.first);
m_graph.set_assignment(i, numeral(r));
}
CTRACE("arith",!m_graph.is_feasible(), m_graph.display(tout););
SASSERT(m_graph.is_feasible());
CTRACE("arith",!m_graph.is_feasible_dbg(), m_graph.display(tout););
SASSERT(m_graph.is_feasible_dbg());
inf_eps r1(rational(0), r);
blocker = mk_gt(v, r1);
return inf_eps(rational(0), r + m_objective_consts[v]);

1
src/smt/theory_utvpi.h
View file

@ -138,6 +138,7 @@ namespace smt {
smt_params m_params;
arith_util a;
arith_eq_adapter m_arith_eq_adapter;
bool m_consistent;
th_var m_izero, m_rzero; //cache the variable representing the zero variable.
dl_graph<GExt> m_graph;

17
src/smt/theory_utvpi_def.h
View file

@ -61,6 +61,7 @@ namespace smt {
theory(m.mk_family_id("arith")),
a(m),
m_arith_eq_adapter(*this, m_params, a),
m_consistent(true),
m_izero(null_theory_var),
m_rzero(null_theory_var),
m_nc_functor(*this),
@ -192,6 +193,8 @@ namespace smt {
template<typename Ext>
void theory_utvpi<Ext>::inc_conflicts() {
get_context().push_trail(value_trail<context, bool>(m_consistent));
m_consistent = false;
m_stats.m_num_conflicts++;
if (m_params.m_arith_adaptive) {
double g = m_params.m_arith_adaptive_propagation_threshold;
@ -312,6 +315,8 @@ namespace smt {
template<typename Ext>
bool theory_utvpi<Ext>::internalize_atom(app * n, bool) {
if (!m_consistent)
return false;
context & ctx = get_context();
if (!a.is_le(n) && !a.is_ge(n) && !a.is_lt(n) && !a.is_gt(n)) {
found_non_utvpi_expr(n);
@ -362,6 +367,8 @@ namespace smt {
template<typename Ext>
bool theory_utvpi<Ext>::internalize_term(app * term) {
if (!m_consistent)
return false;
bool result = !get_context().inconsistent() && null_theory_var != mk_term(term);
CTRACE("utvpi", !result, tout << "Did not internalize " << mk_pp(term, get_manager()) << "\n";);
return result;
@ -698,8 +705,8 @@ namespace smt {
}
template<typename Ext>
bool theory_utvpi<Ext>::is_consistent() const {
return m_graph.is_feasible();
bool theory_utvpi<Ext>::is_consistent() const {
return m_consistent;
}
@ -743,7 +750,7 @@ namespace smt {
*/
template<typename Ext>
void theory_utvpi<Ext>::enforce_parity() {
SASSERT(m_graph.is_feasible());
SASSERT(m_graph.is_feasible_dbg());
unsigned_vector todo;
unsigned sz = get_num_vars();
for (unsigned i = 0; i < sz; ++i) {
@ -788,7 +795,7 @@ namespace smt {
}
}
TRACE("utvpi", display(tout););
SASSERT(m_graph.is_feasible());
SASSERT(m_graph.is_feasible_dbg());
}
DEBUG_CODE(
for (unsigned i = 0; i < sz; ++i) {
@ -798,7 +805,7 @@ namespace smt {
UNREACHABLE();
}
});
SASSERT(m_graph.is_feasible());
SASSERT(m_graph.is_feasible_dbg());
}