mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 19:35:50 +00:00
ate/acce
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
a6ac6958a6
commit
e95840b640
5 changed files with 90 additions and 34 deletions
|
|
@ -344,23 +344,60 @@ public:
|
|||
};
|
||||
|
||||
class lp_parse {
|
||||
opt::context& opt;
|
||||
lp_tokenizer& tok;
|
||||
typedef svector<std::pair<int, symbol> > 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<indicator> m_ind;
|
||||
lin_term m_expr;
|
||||
rel_op m_rel;
|
||||
int m_bound;
|
||||
};
|
||||
|
||||
struct bound {
|
||||
symbol m_var;
|
||||
option<rational> m_lo, m_hi;
|
||||
};
|
||||
|
||||
opt::context& opt;
|
||||
lp_tokenizer& tok;
|
||||
objective m_objective;
|
||||
vector<constraint> m_constraints;
|
||||
vector<bound> m_bounds;
|
||||
hashtable<symbol, symbol_hash_proc, symbol_eq_proc> 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()
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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<literal>(s.s.m_rand, m_covered_clause);
|
||||
return cce<et>(blocked, k);
|
||||
}
|
||||
|
||||
|
|
@ -1537,7 +1542,7 @@ namespace sat {
|
|||
// always try to remove larger clauses.
|
||||
template<elim_type et>
|
||||
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();
|
||||
|
|
|
|||
|
|
@ -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'),
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue