From e1d5f484f15df705cf05d98c92d9ef11e5142bb1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Apr 2013 08:46:46 -0700 Subject: [PATCH] simplify result from tactics, remove unused features from difference logic solver Signed-off-by: Nikolaj Bjorner --- src/smt/theory_diff_logic.h | 15 +--- src/smt/theory_diff_logic_def.h | 97 +------------------------ src/tactic/core/ctx_simplify_tactic.cpp | 6 ++ 3 files changed, 11 insertions(+), 107 deletions(-) diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h index 4140f683c..9c80d8c34 100644 --- a/src/smt/theory_diff_logic.h +++ b/src/smt/theory_diff_logic.h @@ -259,8 +259,6 @@ namespace smt { theory_var m_zero_int; // cache the variable representing the zero variable. theory_var m_zero_real; // cache the variable representing the zero variable. int_vector m_scc_id; // Cheap equality propagation - bool m_modified_since_eq_prop; // true if new constraints were asserted - // since last eq propagation. eq_prop_info_set m_eq_prop_info_set; // set of existing equality prop infos ptr_vector m_eq_prop_infos; @@ -289,18 +287,14 @@ namespace smt { virtual theory_var mk_var(enode* n); virtual theory_var mk_var(app* n); - - void mark_as_modified_since_eq_prop(); - - void unmark_as_modified_since_eq_prop(); - - bool propagate_cheap_equalities(); - + void compute_delta(); void found_non_diff_logic_expr(expr * n); - bool is_interpreted(app* n) const; + bool is_interpreted(app* n) const { + return get_family_id() == n->get_family_id(); + } void del_clause_eh(clause* cls); @@ -312,7 +306,6 @@ namespace smt { m_arith_eq_adapter(*this, params, m_util), m_zero_int(null_theory_var), m_zero_real(null_theory_var), - m_modified_since_eq_prop(false), m_asserted_qhead(0), m_num_core_conflicts(0), m_num_propagation_calls(0), diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 9f2c97a84..28c14b18f 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -374,15 +374,7 @@ final_check_status theory_diff_logic::final_check_eh() { // either will already be zero (as we don't do mixed constraints). m_graph.set_to_zero(m_zero_int, m_zero_real); SASSERT(is_consistent()); - - -#if 0 - TBD: - if (propagate_cheap_equalities()) { - return FC_CONTINUE; - } -#endif - + if (m_non_diff_logic_exprs) { return FC_GIVEUP; } @@ -540,22 +532,6 @@ bool theory_diff_logic::propagate_atom(atom* a) { return true; } - - -template -void theory_diff_logic::mark_as_modified_since_eq_prop() { - if (!m_modified_since_eq_prop) { - get_context().push_trail(value_trail(m_modified_since_eq_prop)); - m_modified_since_eq_prop = true; - } -} - -template -void theory_diff_logic::unmark_as_modified_since_eq_prop() { - get_context().push_trail(value_trail(m_modified_since_eq_prop)); - m_modified_since_eq_prop = false; -} - template void theory_diff_logic::del_clause_eh(clause* cls) { @@ -802,7 +778,6 @@ theory_var theory_diff_logic::mk_num(app* n, rational const& r) { template theory_var theory_diff_logic::mk_var(enode* n) { - mark_as_modified_since_eq_prop(); theory_var v = theory::mk_var(n); TRACE("diff_logic_vars", tout << "mk_var: " << v << "\n";); m_graph.init_var(v); @@ -810,10 +785,6 @@ theory_var theory_diff_logic::mk_var(enode* n) { return v; } -template -bool theory_diff_logic::is_interpreted(app* n) const { - return n->get_family_id() == get_family_id(); -} template theory_var theory_diff_logic::mk_var(app* n) { @@ -854,7 +825,6 @@ void theory_diff_logic::reset_eh() { m_asserted_atoms .reset(); m_stats .reset(); m_scopes .reset(); - m_modified_since_eq_prop = false; m_asserted_qhead = 0; m_num_core_conflicts = 0; m_num_propagation_calls = 0; @@ -865,70 +835,6 @@ void theory_diff_logic::reset_eh() { } -template -bool theory_diff_logic::propagate_cheap_equalities() { - bool result = false; - TRACE("dl_new_eq", get_context().display(tout);); - context& ctx = get_context(); - region& reg = ctx.get_region(); - SASSERT(m_eq_prop_info_set.empty()); - SASSERT(m_eq_prop_infos.empty()); - if (m_modified_since_eq_prop) { - m_graph.compute_zero_edge_scc(m_scc_id); - int n = get_num_vars(); - for (theory_var v = 0; v < n; v++) { - rational delta_r; - theory_var x_v = expand(true, v, delta_r); - numeral delta(delta_r); - int scc_id = m_scc_id[x_v]; - if (scc_id != -1) { - delta += m_graph.get_assignment(x_v); - TRACE("eq_scc", tout << v << " " << x_v << " " << scc_id << " " << delta << "\n";); - eq_prop_info info(scc_id, delta); - typename eq_prop_info_set::entry * entry = m_eq_prop_info_set.find_core(&info); - if (entry == 0) { - eq_prop_info * new_info = alloc(eq_prop_info, scc_id, delta, v); - m_eq_prop_info_set.insert(new_info); - m_eq_prop_infos.push_back(new_info); - } - else { - // new equality found - theory_var r = entry->get_data()->get_root(); - - enode * n1 = get_enode(v); - enode * n2 = get_enode(r); - if (n1->get_root() != n2->get_root()) { - // r may be an alias (i.e., it is not realy in the graph). So, I should expand it. - // nsb: ?? - rational r_delta; - theory_var x_r = expand(true, r, r_delta); - - justification* j = new (reg) implied_eq_justification(*this, x_v, x_r, m_graph.get_timestamp()); - (void)j; - - m_stats.m_num_th2core_eqs++; - // TBD: get equality into core. - - NOT_IMPLEMENTED_YET(); - // new_eq_eh(x_v, x_r, *j); - result = true; - } - } - } - } - m_eq_prop_info_set.reset(); - std::for_each(m_eq_prop_infos.begin(), m_eq_prop_infos.end(), delete_proc()); - m_eq_prop_infos.reset(); - unmark_as_modified_since_eq_prop(); - } - - TRACE("dl_new_eq", get_context().display(tout);); - SASSERT(!m_modified_since_eq_prop); - - return result; -} - - template void theory_diff_logic::compute_delta() { m_delta = rational(1); @@ -1087,7 +993,6 @@ void theory_diff_logic::new_eq_or_diseq(bool is_eq, theory_var v1, theory_v // assign the corresponding equality literal. // - mark_as_modified_since_eq_prop(); app_ref eq(m), s2(m), t2(m); app* s1 = get_enode(s)->get_owner(); diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 831efa087..be4dfd516 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -371,6 +371,12 @@ struct ctx_simplify_tactic::imp { if (!modified) { r = t; } + if (new_new_args.empty()) { + r = OR?m.mk_false():m.mk_true(); + } + else if (new_new_args.size() == 1) { + r = new_new_args[0]; + } else { std::reverse(new_new_args.c_ptr(), new_new_args.c_ptr() + new_new_args.size()); m_mk_app(t->get_decl(), new_new_args.size(), new_new_args.c_ptr(), r);