mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

tuning based on benchmarks from Robert White

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-05-05 14:43:06 -07:00
parent 182fea2d7b
commit 25ad9d2ee1
5 changed files with 65 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

52
src/ast/rewriter/expr_safe_replace.cpp
View file

@ -29,43 +29,39 @@ void expr_safe_replace::insert(expr* src, expr* dst) {
} }
void expr_safe_replace::operator()(expr* e, expr_ref& res) { void expr_safe_replace::operator()(expr* e, expr_ref& res) {
obj_map<expr,expr*> cache; m_todo.push_back(e);
ptr_vector<expr> todo, args;
expr_ref_vector refs(m);
todo.push_back(e);
expr* a, *b, *d; expr* a, *b, *d;
todo.push_back(e);
while (!todo.empty()) { while (!m_todo.empty()) {
a = todo.back(); a = m_todo.back();
if (cache.contains(a)) { if (m_cache.contains(a)) {
todo.pop_back(); m_todo.pop_back();
} }
else if (m_subst.find(a, b)) { else if (m_subst.find(a, b)) {
cache.insert(a, b); m_cache.insert(a, b);
todo.pop_back(); m_todo.pop_back();
} }
else if (is_var(a)) { else if (is_var(a)) {
cache.insert(a, a); m_cache.insert(a, a);
todo.pop_back(); m_todo.pop_back();
} }
else if (is_app(a)) { else if (is_app(a)) {
app* c = to_app(a); app* c = to_app(a);
unsigned n = c->get_num_args(); unsigned n = c->get_num_args();
args.reset(); m_args.reset();
for (unsigned i = 0; i < n; ++i) { for (unsigned i = 0; i < n; ++i) {
if (cache.find(c->get_arg(i), d)) { if (m_cache.find(c->get_arg(i), d)) {
args.push_back(d); m_args.push_back(d);
} }
else { else {
todo.push_back(c->get_arg(i)); m_todo.push_back(c->get_arg(i));
} }
} }
if (args.size() == n) { if (m_args.size() == n) {
b = m.mk_app(c->get_decl(), args.size(), args.c_ptr()); b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr());
refs.push_back(b); m_refs.push_back(b);
cache.insert(a, b); m_cache.insert(a, b);
todo.pop_back(); m_todo.pop_back();
} }
} }
else { else {
@ -93,12 +89,16 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
} }
replace(q->get_expr(), new_body); replace(q->get_expr(), new_body);
b = m.update_quantifier(q, pats.size(), pats.c_ptr(), nopats.size(), nopats.c_ptr(), new_body); b = m.update_quantifier(q, pats.size(), pats.c_ptr(), nopats.size(), nopats.c_ptr(), new_body);
refs.push_back(b); m_refs.push_back(b);
cache.insert(a, b); m_cache.insert(a, b);
todo.pop_back(); m_todo.pop_back();
} }
} }
res = cache.find(e); res = m_cache.find(e);
m_cache.reset();
m_todo.reset();
m_args.reset();
m_refs.reset();
} }
void expr_safe_replace::reset() { void expr_safe_replace::reset() {

7
src/ast/rewriter/expr_safe_replace.h
View file

@ -29,9 +29,12 @@ class expr_safe_replace {
expr_ref_vector m_src; expr_ref_vector m_src;
expr_ref_vector m_dst; expr_ref_vector m_dst;
obj_map<expr, expr*> m_subst; obj_map<expr, expr*> m_subst;
obj_map<expr,expr*> m_cache;
ptr_vector<expr> m_todo, m_args;
expr_ref_vector m_refs;
public: public:
expr_safe_replace(ast_manager& m): m(m), m_src(m), m_dst(m) {} expr_safe_replace(ast_manager& m): m(m), m_src(m), m_dst(m), m_refs(m) {}
void insert(expr* src, expr* dst); void insert(expr* src, expr* dst);
@ -42,6 +45,8 @@ public:
void apply_substitution(expr* s, expr* def, expr_ref& t); void apply_substitution(expr* s, expr* def, expr_ref& t);
void reset(); void reset();
bool empty() const { return m_subst.empty(); }
}; };
#endif /* __EXPR_SAFE_REPLACE_H__ */ #endif /* __EXPR_SAFE_REPLACE_H__ */

7
src/opt/pb_sls.cpp
View file

@ -90,6 +90,8 @@ namespace smt {
struct stats { struct stats {
stats() { reset(); } stats() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); } void reset() { memset(this, 0, sizeof(*this)); }
unsigned m_num_flips;
unsigned m_num_improvements;
}; };
ast_manager& m; ast_manager& m;
@ -116,6 +118,7 @@ namespace smt {
unsigned m_non_greedy_percent; // percent of moves to do non-greedy style unsigned m_non_greedy_percent; // percent of moves to do non-greedy style
random_gen m_rng; random_gen m_rng;
scoped_mpz one; scoped_mpz one;
stats m_stats;
imp(ast_manager& m): imp(ast_manager& m):
m(m), m(m),
@ -238,6 +241,8 @@ namespace smt {
} }
void collect_statistics(::statistics& st) const { void collect_statistics(::statistics& st) const {
st.update("sls.num_flips", m_stats.m_num_flips);
st.update("sls.num_improvements", m_stats.m_num_improvements);
} }
void updt_params(params_ref& p) { void updt_params(params_ref& p) {
@ -347,6 +352,7 @@ namespace smt {
} }
literal flip() { literal flip() {
m_stats.m_num_flips++;
literal result; literal result;
if (m_hard_false.empty()) { if (m_hard_false.empty()) {
result = flip_soft(); result = flip_soft();
@ -359,6 +365,7 @@ namespace smt {
m_best_assignment.reset(); m_best_assignment.reset();
m_best_assignment.append(m_assignment); m_best_assignment.append(m_assignment);
m_best_penalty = m_penalty; m_best_penalty = m_penalty;
m_stats.m_num_improvements++;
init_max_flips(); init_max_flips();
} }
if (!m_assignment[result.var()]) { if (!m_assignment[result.var()]) {

34
src/opt/weighted_maxsat.cpp
View file

@ -60,17 +60,24 @@ namespace opt {
params_ref m_params; // config params_ref m_params; // config
bool m_enable_sls; // config bool m_enable_sls; // config
bool m_enable_sat; // config bool m_enable_sat; // config
bool m_sls_enabled;
bool m_sat_enabled;
public: public:
maxsmt_solver_base(solver* s, ast_manager& m): maxsmt_solver_base(solver* s, ast_manager& m):
m_s(s), m(m), m_cancel(false), m_soft(m), m_s(s), m(m), m_cancel(false), m_soft(m),
m_enable_sls(false), m_enable_sat(false) {} m_enable_sls(false), m_enable_sat(false),
m_sls_enabled(false), m_sat_enabled(false) {}
virtual ~maxsmt_solver_base() {} virtual ~maxsmt_solver_base() {}
virtual rational get_lower() const { return m_lower; } virtual rational get_lower() const { return m_lower; }
virtual rational get_upper() const { return m_upper; } virtual rational get_upper() const { return m_upper; }
virtual bool get_assignment(unsigned index) const { return m_assignment[index]; } virtual bool get_assignment(unsigned index) const { return m_assignment[index]; }
virtual void set_cancel(bool f) { m_cancel = f; m_s->set_cancel(f); } virtual void set_cancel(bool f) { m_cancel = f; m_s->set_cancel(f); }
virtual void collect_statistics(statistics& st) const { } virtual void collect_statistics(statistics& st) const {
if (m_sls_enabled || m_sat_enabled) {
m_s->collect_statistics(st);
}
}
virtual void get_model(model_ref& mdl) { mdl = m_model.get(); } virtual void get_model(model_ref& mdl) { mdl = m_model.get(); }
virtual void updt_params(params_ref& p) { virtual void updt_params(params_ref& p) {
m_params.copy(p); m_params.copy(p);
@ -121,7 +128,6 @@ namespace opt {
fid != pb.get_family_id() && fid != pb.get_family_id() &&
fid != bv.get_family_id() && fid != bv.get_family_id() &&
!is_uninterp_const(n)) { !is_uninterp_const(n)) {
std::cout << mk_pp(n, m) << "\n";
throw found(); throw found();
} }
} }
@ -147,7 +153,7 @@ namespace opt {
} }
void enable_bvsat() { void enable_bvsat() {
if (probe_bv()) { if (m_enable_sat && !m_sat_enabled && probe_bv()) {
tactic_ref pb2bv = mk_card2bv_tactic(m, m_params); tactic_ref pb2bv = mk_card2bv_tactic(m, m_params);
tactic_ref bv2sat = mk_qfbv_tactic(m, m_params); tactic_ref bv2sat = mk_qfbv_tactic(m, m_params);
tactic_ref tac = and_then(pb2bv.get(), bv2sat.get()); tactic_ref tac = and_then(pb2bv.get(), bv2sat.get());
@ -159,15 +165,17 @@ namespace opt {
unsigned lvl = m_s->get_scope_level(); unsigned lvl = m_s->get_scope_level();
while (lvl > 0) { sat_solver->push(); --lvl; } while (lvl > 0) { sat_solver->push(); --lvl; }
m_s = sat_solver; m_s = sat_solver;
m_sat_enabled = true;
} }
} }
void enable_sls() { void enable_sls() {
if (m_enable_sls && probe_bv()) { if (m_enable_sls && !m_sls_enabled && probe_bv()) {
m_params.set_uint("restarts", 20); m_params.set_uint("restarts", 20);
unsigned lvl = m_s->get_scope_level(); unsigned lvl = m_s->get_scope_level();
m_s = alloc(sls_solver, m, m_s.get(), m_soft, m_weights, m_params); m_s = alloc(sls_solver, m, m_s.get(), m_soft, m_weights, m_params);
while (lvl > 0) { m_s->push(); --lvl; } while (lvl > 0) { m_s->push(); --lvl; }
m_sls_enabled = true;
} }
} }
@ -249,19 +257,18 @@ namespace opt {
m_soft_aux(m), m_soft_aux(m),
m_trail(m), m_trail(m),
m_soft_constraints(m), m_soft_constraints(m),
m_enable_lazy(false) { m_enable_lazy(true) {
m_enable_lazy = true; m_enable_lazy = true;
enable_sls();
} }
virtual ~bcd2() {} virtual ~bcd2() {}
virtual lbool operator()() { virtual lbool operator()() {
expr_ref fml(m), r(m); expr_ref fml(m), r(m);
lbool is_sat = l_undef; lbool is_sat = l_undef;
expr_ref_vector asms(m); expr_ref_vector asms(m);
bool first = true; bool first = true;
enable_sls();
solver::scoped_push _scope1(s()); solver::scoped_push _scope1(s());
init(); init();
init_bcd(); init_bcd();
@ -557,13 +564,14 @@ namespace opt {
public: public:
pbmax(solver* s, ast_manager& m, bool use_aux): pbmax(solver* s, ast_manager& m, bool use_aux):
maxsmt_solver_base(s, m), m_use_aux(use_aux) { maxsmt_solver_base(s, m), m_use_aux(use_aux) {
enable_bvsat();
enable_sls();
} }
virtual ~pbmax() {} virtual ~pbmax() {}
lbool operator()() { lbool operator()() {
enable_bvsat();
enable_sls();
TRACE("opt", s().display(tout); tout << "\n"; TRACE("opt", s().display(tout); tout << "\n";
for (unsigned i = 0; i < m_soft.size(); ++i) { for (unsigned i = 0; i < m_soft.size(); ++i) {
tout << mk_pp(m_soft[i].get(), m) << " " << m_weights[i] << "\n"; tout << mk_pp(m_soft[i].get(), m) << " " << m_weights[i] << "\n";
@ -636,12 +644,12 @@ namespace opt {
public: public:
wpm2(solver* s, ast_manager& m, maxsmt_solver_base* _maxs): wpm2(solver* s, ast_manager& m, maxsmt_solver_base* _maxs):
maxsmt_solver_base(s, m), maxs(_maxs) { maxsmt_solver_base(s, m), maxs(_maxs) {
enable_sls();
} }
virtual ~wpm2() {} virtual ~wpm2() {}
lbool operator()() { lbool operator()() {
enable_sls();
IF_VERBOSE(1, verbose_stream() << "(wmaxsat.wpm2 solve)\n";); IF_VERBOSE(1, verbose_stream() << "(wmaxsat.wpm2 solve)\n";);
solver::scoped_push _s(s()); solver::scoped_push _s(s());
pb_util u(m); pb_util u(m);
@ -839,12 +847,12 @@ namespace opt {
public: public:
sls(solver* s, ast_manager& m): sls(solver* s, ast_manager& m):
maxsmt_solver_base(s, m) { maxsmt_solver_base(s, m) {
enable_bvsat();
enable_sls();
} }
virtual ~sls() {} virtual ~sls() {}
lbool operator()() { lbool operator()() {
IF_VERBOSE(1, verbose_stream() << "(sls solve)\n";); IF_VERBOSE(1, verbose_stream() << "(sls solve)\n";);
enable_bvsat();
enable_sls();
init(); init();
lbool is_sat = s().check_sat(0, 0); lbool is_sat = s().check_sat(0, 0);
if (is_sat == l_true) { if (is_sat == l_true) {

5
src/tactic/arith/elim01_tactic.cpp
View file

@ -185,6 +185,11 @@ public:
<< bounds.has_upper(x, hi, s2) << " " << hi << "\n";); << bounds.has_upper(x, hi, s2) << " " << hi << "\n";);
} }
} }
if (sub.empty()) {
result.push_back(g.get());
return;
}
expr_ref new_curr(m), tmp_curr(m); expr_ref new_curr(m), tmp_curr(m);
proof_ref new_pr(m); proof_ref new_pr(m);