mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

#5454

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-11 04:55:20 -07:00
parent 4f2211baab
commit d1d64bbe59
2 changed files with 16 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/sat/sat_simplifier.cpp
View file

@ -2022,10 +2022,14 @@ namespace sat {
} }
remove_bin_clauses(pos_l); remove_bin_clauses(pos_l);
remove_bin_clauses(neg_l); remove_bin_clauses(neg_l);
{
clause_use_list& pos_occs = m_use_list.get(pos_l);
clause_use_list& neg_occs = m_use_list.get(neg_l);
remove_clauses(pos_occs, pos_l); remove_clauses(pos_occs, pos_l);
remove_clauses(neg_occs, neg_l); remove_clauses(neg_occs, neg_l);
pos_occs.reset(); pos_occs.reset();
neg_occs.reset(); neg_occs.reset();
}
return true; return true;
} }

16
src/tactic/portfolio/solver_subsumption_tactic.cpp
View file

@ -53,7 +53,7 @@ class solver_subsumption_tactic : public tactic {
*/ */
bool simplify(expr_ref& f) { bool simplify(expr_ref& f) {
expr_ref_vector fmls(m), ors(m), nprefix(m), prefix(m); expr_ref_vector fmls(m), ors(m), nors(m), prefix(m);
expr_ref nf(m.mk_not(f), m); expr_ref nf(m.mk_not(f), m);
fmls.push_back(nf); fmls.push_back(nf);
lbool is_sat = m_solver->check_sat(fmls); lbool is_sat = m_solver->check_sat(fmls);
@ -65,15 +65,15 @@ class solver_subsumption_tactic : public tactic {
return false; return false;
ors.append(to_app(f)->get_num_args(), to_app(f)->get_args()); ors.append(to_app(f)->get_num_args(), to_app(f)->get_args());
for (expr* arg : ors) for (expr* arg : ors)
nprefix.push_back(mk_not(m, arg)); nors.push_back(mk_not(m, arg));
for (unsigned i = 0; i < ors.size(); ++i) { for (unsigned i = 0; i < ors.size(); ++i) {
expr* arg = ors.get(i); expr* arg = ors.get(i);
expr_ref save(nprefix.get(i), m); expr_ref save(nors.get(i), m);
nprefix[i] = arg; nors[i] = arg;
is_sat = m_solver->check_sat(nprefix); is_sat = m_solver->check_sat(nors);
nprefix[i] = save; nors[i] = save;
if (is_sat == l_false) if (is_sat == l_false)
nprefix[i] = m.mk_true(); nors[i] = m.mk_true();
else else
prefix.push_back(arg); prefix.push_back(arg);
} }
@ -141,7 +141,7 @@ public:
} }
void collect_param_descrs(param_descrs& r) override { void collect_param_descrs(param_descrs& r) override {
r.insert("max_conflicts", CPK_UINT, "(default: 10) maximal number of conflicts allowed per solver call."); r.insert("max_conflicts", CPK_UINT, "(default: 2) maximal number of conflicts allowed per solver call.");
} }
void operator()(goal_ref const& g, goal_ref_buffer& result) override { void operator()(goal_ref const& g, goal_ref_buffer& result) override {