From e95840b640658557a278ea6f881ce2bbfc2c8b7a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 2 Feb 2018 20:51:41 -0800 Subject: [PATCH] ate/acce Signed-off-by: Nikolaj Bjorner --- src/opt/opt_parse.cpp | 78 +++++++++++++++++++++++++------ src/sat/sat_asymm_branch.cpp | 21 ++++----- src/sat/sat_asymm_branch.h | 2 +- src/sat/sat_simplifier.cpp | 13 ++++-- src/sat/sat_simplifier_params.pyg | 10 ++-- 5 files changed, 90 insertions(+), 34 deletions(-) diff --git a/src/opt/opt_parse.cpp b/src/opt/opt_parse.cpp index 6a7ea3614..9ac0f77a0 100644 --- a/src/opt/opt_parse.cpp +++ b/src/opt/opt_parse.cpp @@ -344,23 +344,60 @@ public: }; class lp_parse { - opt::context& opt; - lp_tokenizer& tok; + typedef svector > lin_term; + + struct objective { + bool m_is_max; + symbol m_name; + lin_term m_expr; + }; + + enum rel_op { + le, ge, eq + }; + + struct indicator { + symbol m_var; + bool m_true; + }; + + struct constraint { + optional m_ind; + lin_term m_expr; + rel_op m_rel; + int m_bound; + }; + + struct bound { + symbol m_var; + option m_lo, m_hi; + }; + + opt::context& opt; + lp_tokenizer& tok; + objective m_objective; + vector m_constraints; + vector m_bounds; + hashtable m_binary; + public: - lp_parse(opt::context& opt, lp_stream_buffer& in): opt(opt), tok(is) {} + + lp_parse(opt::context& opt, lp_stream_buffer& in): + opt(opt), tok(is) {} void parse() { - objective(); - subject_to(); - bounds(); - general(); - binary(); + parse_objective(); + parse_subject_to(); + parse_bounds(); + parse_general(); + parse_binary(); + post_process(); } - void objective() { + void parse_objective() { m_objective.m_is_max = minmax(); m_objective.m_name = try_name(); - m_objective.m_expr = expr(); + parse_expr(m_objective.m_expr); } bool minmax() { @@ -376,16 +413,31 @@ public: return false; } + bool try_accept(char const* token) { return false; } - bool indicator(symbol& var, bool& val) { - if (!try_variable(var)) return false; - check(in.parse_token("=")); + bool parse_indicator(symbol& var, bool& val) { + if (!peek("=", 1)) return false; + if (!peek(":", 3)) return false; + if (!peek("1", 2) && !peek("0", 2)) return false; + val = peek("1",2); + parse_variable(var); + accept("="); + accept(); + accept(":"); + return true; + } + + void parse_bounds() { + if (!try_accept("bounds")) return; } + void parse_indicator() { + + } def indicator(self): v = self.variable() diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index a94ea461a..64b1d5e67 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -43,12 +43,12 @@ namespace sat { stopwatch m_watch; unsigned m_elim_literals; unsigned m_elim_learned_literals; - unsigned m_hidden_tautologies; + unsigned m_tr; report(asymm_branch & a): m_asymm_branch(a), m_elim_literals(a.m_elim_literals), m_elim_learned_literals(a.m_elim_learned_literals), - m_hidden_tautologies(a.m_hidden_tautologies) { + m_tr(a.m_tr) { m_watch.start(); } @@ -60,7 +60,7 @@ namespace sat { verbose_stream() << " (sat-asymm-branch :elim-literals " << (num_total - num_learned) << " :elim-learned-literals " << num_learned - << " :hte " << (m_asymm_branch.m_hidden_tautologies - m_hidden_tautologies) + << " :hte " << (m_asymm_branch.m_tr - m_tr) << " :cost " << m_asymm_branch.m_counter << mem_stat() << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";); @@ -68,15 +68,14 @@ namespace sat { }; void asymm_branch::process_bin(big& big) { - unsigned elim = big.reduce_tr(s); - m_hidden_tautologies += elim; + m_tr += big.reduce_tr(s); } bool asymm_branch::process(big& big, bool learned) { unsigned elim0 = m_elim_literals; unsigned eliml0 = m_elim_learned_literals; for (unsigned i = 0; i < m_asymm_branch_rounds; ++i) { - unsigned elim = m_elim_literals + m_hidden_tautologies; + unsigned elim = m_elim_literals + m_tr; big.init(s, learned); process(&big, s.m_clauses); process(&big, s.m_learned); @@ -84,11 +83,11 @@ namespace sat { s.propagate(false); if (s.m_inconsistent) break; - unsigned num_elim = m_elim_literals + m_hidden_tautologies - elim; + unsigned num_elim = m_elim_literals + m_tr - elim; IF_VERBOSE(1, verbose_stream() << "(sat-asymm-branch-step :elim " << num_elim << ")\n";); if (num_elim == 0) break; - if (num_elim > 100) + if (false && num_elim > 1000) i = 0; } IF_VERBOSE(1, if (m_elim_learned_literals > eliml0) @@ -149,7 +148,7 @@ namespace sat { throw ex; } } - + void asymm_branch::operator()(bool force) { ++m_calls; @@ -480,13 +479,13 @@ namespace sat { void asymm_branch::collect_statistics(statistics & st) const { st.update("elim literals", m_elim_literals); - st.update("hte", m_hidden_tautologies); + st.update("tr", m_tr); } void asymm_branch::reset_statistics() { m_elim_literals = 0; m_elim_learned_literals = 0; - m_hidden_tautologies = 0; + m_tr = 0; } }; diff --git a/src/sat/sat_asymm_branch.h b/src/sat/sat_asymm_branch.h index 1a57f8800..cc354a5c8 100644 --- a/src/sat/sat_asymm_branch.h +++ b/src/sat/sat_asymm_branch.h @@ -48,7 +48,7 @@ namespace sat { // stats unsigned m_elim_literals; unsigned m_elim_learned_literals; - unsigned m_hidden_tautologies; + unsigned m_tr; literal_vector m_pos, m_neg; // literals (complements of literals) in clauses sorted by discovery time (m_left in BIG). literal_vector m_to_delete; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index f439036b2..dee2afb87 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1394,11 +1394,17 @@ namespace sat { while (!is_tautology && m_covered_clause.size() > sz && !above_threshold(sz0)) { SASSERT(!is_tautology); + if ((et == abce_t || et == acce_t || et == ate_t) && add_ala()) { for (literal l : m_covered_clause) s.unmark_visited(l); return ate_t; } + if (et == ate_t) { + for (literal l : m_covered_clause) s.unmark_visited(l); + return no_t; + } + if (first) { for (unsigned i = 0; i < sz0; ++i) { if (check_abce_tautology(m_covered_clause[i])) { @@ -1440,7 +1446,6 @@ namespace sat { m_covered_clause.push_back(l); m_covered_antecedent.push_back(clause_ante()); } - // shuffle(s.s.m_rand, m_covered_clause); return cce(blocked, k); } @@ -1537,7 +1542,7 @@ namespace sat { // always try to remove larger clauses. template bool select_clause(unsigned sz) { - return et == ate_t || (sz > 3) || s.s.m_rand(4) == 0; + return (sz > 3) || s.s.m_rand(4) == 0; } void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry, model_converter::kind k) { @@ -2080,8 +2085,8 @@ namespace sat { m_abce = p.abce(); m_ate = p.ate(); m_bce_delay = p.bce_delay(); - m_bce = p.elim_blocked_clauses(); - m_bce_at = p.elim_blocked_clauses_at(); + m_bce = p.bce(); + m_bce_at = p.bce_at(); m_retain_blocked_clauses = p.retain_blocked_clauses(); m_blocked_clause_limit = p.blocked_clause_limit(); m_res_limit = p.resolution_limit(); diff --git a/src/sat/sat_simplifier_params.pyg b/src/sat/sat_simplifier_params.pyg index 4bbc490cc..3757aad2d 100644 --- a/src/sat/sat_simplifier_params.pyg +++ b/src/sat/sat_simplifier_params.pyg @@ -1,14 +1,14 @@ def_module_params(module_name='sat', class_name='sat_simplifier_params', export=True, - params=(('elim_blocked_clauses', BOOL, False, 'eliminate blocked clauses'), + params=(('bce', BOOL, False, 'eliminate blocked clauses'), ('abce', BOOL, False, 'eliminate blocked clauses using asymmmetric literals'), - ('cce', BOOL, False, 'eliminate covered clauses'), - ('ate', BOOL, True, 'asymmetric tautology elimination'), + ('cce', BOOL, False, 'eliminate covered clauses'), + ('ate', BOOL, True, 'asymmetric tautology elimination'), ('acce', BOOL, False, 'eliminate covered clauses using asymmetric added literals'), - ('elim_blocked_clauses_at', UINT, 2, 'eliminate blocked clauses only once at the given simplification round'), + ('bce_at', UINT, 2, 'eliminate blocked clauses only once at the given simplification round'), ('bca', BOOL, False, 'blocked clause addition - add blocked binary clauses'), - ('bce_delay', UINT, 0, 'delay eliminate blocked clauses until simplification round'), + ('bce_delay', UINT, 2, 'delay eliminate blocked clauses until simplification round'), ('retain_blocked_clauses', BOOL, True, 'retain blocked clauses as lemmas'), ('blocked_clause_limit', UINT, 100000000, 'maximum number of literals visited during blocked clause elimination'), ('override_incremental', BOOL, False, 'override incemental safety gaps. Enable elimination of blocked clauses and variables even if solver is reused'),