mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-11 13:17:57 -07:00
parent 97f37613c2
commit 79ceaa1d13
4 changed files with 89 additions and 61 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/sat_solver.cpp
View file

@ -1468,11 +1468,14 @@ namespace sat {
lh.simplify(); lh.simplify();
lh.collect_statistics(m_aux_stats); lh.collect_statistics(m_aux_stats);
} }
#if 0
// Buggy
{ {
lookahead lh(*this); lookahead lh(*this);
lh.scc(); lh.scc();
lh.collect_statistics(m_aux_stats); lh.collect_statistics(m_aux_stats);
} }
#endif
} }
@ -3049,7 +3052,6 @@ namespace sat {
m_probing.updt_params(p); m_probing.updt_params(p);
m_scc.updt_params(p); m_scc.updt_params(p);
m_rand.set_seed(m_config.m_random_seed); m_rand.set_seed(m_config.m_random_seed);
m_step_size = m_config.m_step_size_init; m_step_size = m_config.m_step_size_init;
} }

29
src/sat/tactic/goal2sat.cpp
View file

@ -94,6 +94,12 @@ struct goal2sat::imp {
std::string s0 = "operator " + s + " not supported, apply simplifier before invoking translator"; std::string s0 = "operator " + s + " not supported, apply simplifier before invoking translator";
throw tactic_exception(s0.c_str()); throw tactic_exception(s0.c_str());
} }
sat::bool_var mk_var(expr* t, bool ext) {
sat::bool_var v = m_solver.mk_var(ext);
m_map.insert(t, v);
return v;
}
void mk_clause(sat::literal l) { void mk_clause(sat::literal l) {
TRACE("goal2sat", tout << "mk_clause: " << l << "\n";); TRACE("goal2sat", tout << "mk_clause: " << l << "\n";);
@ -120,7 +126,7 @@ struct goal2sat::imp {
sat::bool_var mk_true() { sat::bool_var mk_true() {
if (m_true == sat::null_bool_var) { if (m_true == sat::null_bool_var) {
// create fake variable to represent true; // create fake variable to represent true;
m_true = m_solver.mk_var(); m_true = mk_var(m.mk_true(), false);
mk_clause(sat::literal(m_true, false)); // v is true mk_clause(sat::literal(m_true, false)); // v is true
} }
return m_true; return m_true;
@ -139,8 +145,7 @@ struct goal2sat::imp {
} }
else { else {
bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t); bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t);
sat::bool_var v = m_solver.mk_var(ext); sat::bool_var v = mk_var(t, ext);
m_map.insert(t, v);
l = sat::literal(v, sign); l = sat::literal(v, sign);
TRACE("sat", tout << "new_var: " << v << ": " << mk_ismt2_pp(t, m) << "\n";); TRACE("sat", tout << "new_var: " << v << ": " << mk_ismt2_pp(t, m) << "\n";);
if (ext && !is_uninterp_const(t)) { if (ext && !is_uninterp_const(t)) {
@ -247,7 +252,7 @@ struct goal2sat::imp {
} }
else { else {
SASSERT(num <= m_result_stack.size()); SASSERT(num <= m_result_stack.size());
sat::bool_var k = m_solver.mk_var(); sat::bool_var k = mk_var(t, false);
sat::literal l(k, false); sat::literal l(k, false);
m_cache.insert(t, l); m_cache.insert(t, l);
sat::literal * lits = m_result_stack.end() - num; sat::literal * lits = m_result_stack.end() - num;
@ -286,7 +291,7 @@ struct goal2sat::imp {
} }
else { else {
SASSERT(num <= m_result_stack.size()); SASSERT(num <= m_result_stack.size());
sat::bool_var k = m_solver.mk_var(); sat::bool_var k = mk_var(t, false);
sat::literal l(k, false); sat::literal l(k, false);
m_cache.insert(t, l); m_cache.insert(t, l);
// l => /\ lits // l => /\ lits
@ -330,7 +335,7 @@ struct goal2sat::imp {
m_result_stack.reset(); m_result_stack.reset();
} }
else { else {
sat::bool_var k = m_solver.mk_var(); sat::bool_var k = mk_var(n, false);
sat::literal l(k, false); sat::literal l(k, false);
m_cache.insert(n, l); m_cache.insert(n, l);
mk_clause(~l, ~c, t); mk_clause(~l, ~c, t);
@ -367,7 +372,7 @@ struct goal2sat::imp {
m_result_stack.reset(); m_result_stack.reset();
} }
else { else {
sat::bool_var k = m_solver.mk_var(); sat::bool_var k = mk_var(t, false);
sat::literal l(k, false); sat::literal l(k, false);
m_cache.insert(t, l); m_cache.insert(t, l);
mk_clause(~l, l1, ~l2); mk_clause(~l, l1, ~l2);
@ -392,7 +397,7 @@ struct goal2sat::imp {
} }
sat::literal_vector lits; sat::literal_vector lits;
convert_pb_args(num, lits); convert_pb_args(num, lits);
sat::bool_var v = m_solver.mk_var(true); sat::bool_var v = mk_var(t, true);
ensure_extension(); ensure_extension();
if (lits.size() % 2 == 0) lits[0].neg(); if (lits.size() % 2 == 0) lits[0].neg();
m_ext->add_xor(v, lits); m_ext->add_xor(v, lits);
@ -451,7 +456,7 @@ struct goal2sat::imp {
m_ext->add_pb_ge(sat::null_bool_var, wlits, k.get_unsigned()); m_ext->add_pb_ge(sat::null_bool_var, wlits, k.get_unsigned());
} }
else { else {
sat::bool_var v = m_solver.mk_var(true); sat::bool_var v = mk_var(t, true);
sat::literal lit(v, sign); sat::literal lit(v, sign);
m_ext->add_pb_ge(v, wlits, k.get_unsigned()); m_ext->add_pb_ge(v, wlits, k.get_unsigned());
TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";); TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";);
@ -476,7 +481,7 @@ struct goal2sat::imp {
m_ext->add_pb_ge(sat::null_bool_var, wlits, k.get_unsigned()); m_ext->add_pb_ge(sat::null_bool_var, wlits, k.get_unsigned());
} }
else { else {
sat::bool_var v = m_solver.mk_var(true); sat::bool_var v = mk_var(t, true);
sat::literal lit(v, sign); sat::literal lit(v, sign);
m_ext->add_pb_ge(v, wlits, k.get_unsigned()); m_ext->add_pb_ge(v, wlits, k.get_unsigned());
TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";); TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";);
@ -525,7 +530,7 @@ struct goal2sat::imp {
m_ext->add_at_least(sat::null_bool_var, lits, k.get_unsigned()); m_ext->add_at_least(sat::null_bool_var, lits, k.get_unsigned());
} }
else { else {
sat::bool_var v = m_solver.mk_var(true); sat::bool_var v = mk_var(t, true);
sat::literal lit(v, sign); sat::literal lit(v, sign);
m_ext->add_at_least(v, lits, k.get_unsigned()); m_ext->add_at_least(v, lits, k.get_unsigned());
TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";); TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";);
@ -547,7 +552,7 @@ struct goal2sat::imp {
m_ext->add_at_least(sat::null_bool_var, lits, lits.size() - k.get_unsigned()); m_ext->add_at_least(sat::null_bool_var, lits, lits.size() - k.get_unsigned());
} }
else { else {
sat::bool_var v = m_solver.mk_var(true); sat::bool_var v = mk_var(t, true);
sat::literal lit(v, sign); sat::literal lit(v, sign);
m_ext->add_at_least(v, lits, lits.size() - k.get_unsigned()); m_ext->add_at_least(v, lits, lits.size() - k.get_unsigned());
m_result_stack.shrink(sz - t->get_num_args()); m_result_stack.shrink(sz - t->get_num_args());

1
src/tactic/portfolio/CMakeLists.txt
View file

@ -21,4 +21,5 @@ z3_add_component(portfolio
TACTIC_HEADERS TACTIC_HEADERS
default_tactic.h default_tactic.h
fd_solver.h fd_solver.h
parallel_tactic.h
) )

116
src/tactic/portfolio/parallel_tactic.cpp
View file

@ -30,12 +30,14 @@ Notes:
class parallel_tactic : public tactic { class parallel_tactic : public tactic {
class solver_state { class solver_state {
params_ref m_params;
scoped_ptr<ast_manager> m_manager; scoped_ptr<ast_manager> m_manager;
ref<solver> m_solver; ref<solver> m_solver;
expr_ref_vector m_cube; expr_ref_vector m_cube;
unsigned m_units; unsigned m_units;
public: public:
solver_state(ast_manager* m, solver* s): solver_state(ast_manager* m, solver* s, params_ref const& p):
m_params(p),
m_manager(m), m_manager(m),
m_solver(s), m_solver(s),
m_cube(s->get_manager()), m_cube(s->get_manager()),
@ -49,6 +51,7 @@ class parallel_tactic : public tactic {
for (unsigned i = st.size(); i-- > 0; ) { for (unsigned i = st.size(); i-- > 0; ) {
if (st.get_key(i) == units) { if (st.get_key(i) == units) {
m_units = st.get_uint_value(i); m_units = st.get_uint_value(i);
std::cout << "value for " << i << " is " << m_units << "\n";
break; break;
} }
} }
@ -64,15 +67,17 @@ class parallel_tactic : public tactic {
solver const& get_solver() const { return *m_solver; } solver const& get_solver() const { return *m_solver; }
solver_state* clone(params_ref& p, expr* cube) { params_ref const& params() const { return m_params; }
solver_state* clone(params_ref const& p, expr* cube) {
ast_manager& m = m_solver->get_manager(); ast_manager& m = m_solver->get_manager();
ast_manager* new_m = alloc(ast_manager, m, !m.proof_mode()); ast_manager* new_m = alloc(ast_manager, m, !m.proof_mode());
solver* s = m_solver->translate(*new_m, p); solver* s = m_solver->translate(*new_m, p);
solver_state* st = alloc(solver_state, new_m, s); solver_state* st = alloc(solver_state, new_m, s, m_params);
ast_translation translate(m, *new_m); ast_translation translate(m, *new_m);
for (expr* c : m_cube) { for (expr* c : m_cube) {
st->m_cube.push_back(translate(c)); st->m_cube.push_back(translate(c));
} }
expr_ref cube1(translate(cube), *new_m); expr_ref cube1(translate(cube), *new_m);
st->m_cube.push_back(cube1); st->m_cube.push_back(cube1);
s->assert_expr(cube1); s->assert_expr(cube1);
@ -109,7 +114,7 @@ private:
m_conflicts_decay_rate = 75; m_conflicts_decay_rate = 75;
m_max_conflicts = m_conflicts_lower_bound; m_max_conflicts = m_conflicts_lower_bound;
m_progress = 0; m_progress = 0;
m_num_threads = omp_get_num_threads(); // TBD adjust by possible threads used inside each solver. m_num_threads = omp_get_num_procs(); // TBD adjust by possible threads used inside each solver.
} }
unsigned get_max_conflicts() { unsigned get_max_conflicts() {
@ -173,40 +178,60 @@ private:
lbool simplify(solver& s) { lbool simplify(solver& s) {
params_ref p; params_ref p;
p.copy(m_params); p.copy(m_params);
p.set_uint("sat.max_conflicts", 10); p.set_uint("max_conflicts", 10);
p.set_bool("sat.lookahead_simplify", true); p.set_bool("lookahead_simplify", true);
s.updt_params(p); s.updt_params(p);
lbool is_sat = s.check_sat(0,0); lbool is_sat = s.check_sat(0,0);
p.set_uint("sat.max_conflicts", get_max_conflicts()); p.set_uint("max_conflicts", get_max_conflicts());
p.set_bool("sat.lookahead_simplify", false); p.set_bool("lookahead_simplify", false);
s.updt_params(p); s.updt_params(p);
return is_sat; return is_sat;
} }
void cube(solver& s, expr_ref_vector& cubes) { lbool cube(solver_state& s) {
ast_manager& m = s.get_manager(); ast_manager& m = s.get_solver().get_manager();
params_ref p; expr_ref_vector cubes(m);
p.copy(m_params); params_ref p;
p.set_uint("sat.lookahead.cube.cutoff", 1); p.copy(s.params());
s.updt_params(p); p.set_uint("lookahead.cube.cutoff", 1);
s.get_solver().updt_params(p);
SASSERT(&m == &cubes.get_manager());
while (true) { while (true) {
expr_ref c = s.cube(); expr_ref c = s.get_solver().cube();
if (m.is_false(c)) { VERIFY(c);
if (m.is_false(c)) {
break; break;
} }
if (m.is_true(c)) { if (m.is_true(c)) {
cubes.reset(); cubes.reset();
cubes.push_back(c); return l_undef;
break;
} }
cubes.push_back(c); cubes.push_back(c);
} }
IF_VERBOSE(1, verbose_stream() << "cubes: " << cubes << "\n";);
if (cubes.empty()) {
return l_false;
}
for (unsigned j = 1; j < cubes.size(); ++j) {
solver_state* s1 = s.clone(s.params(), cubes[j].get());
#pragma omp critical (parallel_tactic)
{
m_solvers.push_back(s1);
}
}
expr* cube0 = cubes[0].get();
s.add_cube(cube0);
s.get_solver().assert_expr(cube0);
return l_undef;
} }
lbool solve(solver& s) { lbool solve(solver& s) {
params_ref p; params_ref p;
p.copy(m_params); p.copy(m_params);
p.set_uint("sat.max_conflicts", get_max_conflicts()); p.set_uint("max_conflicts", get_max_conflicts());
s.updt_params(p); s.updt_params(p);
return s.check_sat(0, 0); return s.check_sat(0, 0);
} }
@ -238,6 +263,7 @@ private:
while (true) { while (true) {
int sz = pick_solvers(); int sz = pick_solvers();
if (sz == 0) { if (sz == 0) {
return l_false; return l_false;
} }
@ -246,6 +272,8 @@ private:
// Simplify phase. // Simplify phase.
IF_VERBOSE(1, verbose_stream() << "(solver.parallel :simplify " << sz << ")\n";); IF_VERBOSE(1, verbose_stream() << "(solver.parallel :simplify " << sz << ")\n";);
IF_VERBOSE(1, display(verbose_stream()); verbose_stream() << "Number of solvers: " << sz << "\n";);
#pragma omp parallel for #pragma omp parallel for
for (int i = 0; i < sz; ++i) { for (int i = 0; i < sz; ++i) {
lbool is_sat = simplify(m_solvers[i]->get_solver()); lbool is_sat = simplify(m_solvers[i]->get_solver());
@ -273,6 +301,8 @@ private:
// Solve phase. // Solve phase.
IF_VERBOSE(1, verbose_stream() << "(solver.parallel :solve " << sz << ")\n";); IF_VERBOSE(1, verbose_stream() << "(solver.parallel :solve " << sz << ")\n";);
IF_VERBOSE(1, display(verbose_stream()); verbose_stream() << "Number of solvers: " << sz << "\n";);
#pragma omp parallel for #pragma omp parallel for
for (int i = 0; i < sz; ++i) { for (int i = 0; i < sz; ++i) {
lbool is_sat = solve(m_solvers[i]->get_solver()); lbool is_sat = solve(m_solvers[i]->get_solver());
@ -287,10 +317,6 @@ private:
sat_index = i; sat_index = i;
break; break;
case l_undef: case l_undef:
#pragma omp critical (parallel_tactic)
{
update_progress(false);
}
break; break;
} }
} }
@ -304,35 +330,29 @@ private:
sz = std::min(max_num_splits(), sz); sz = std::min(max_num_splits(), sz);
if (sz == 0) continue; if (sz == 0) continue;
vector<expr_ref_vector> cubes;
for (int i = 0; i < sz; ++i) {
cubes.push_back(expr_ref_vector(m_solvers[i]->get_solver().get_manager()));
}
// Split phase. // Split phase.
IF_VERBOSE(1, verbose_stream() << "(solver.parallel :split " << sz << ")\n";); IF_VERBOSE(1, verbose_stream() << "(solver.parallel :split " << sz << ")\n";);
IF_VERBOSE(1, display(verbose_stream()); verbose_stream() << "Number of solvers: " << sz << "\n";);
#pragma omp parallel for #pragma omp parallel for
for (int i = 0; i < sz; ++i) { for (int i = 0; i < sz; ++i) {
cube(m_solvers[i]->get_solver(), cubes[i]); switch (cube(*m_solvers[i])) {
case l_false:
#pragma omp critical (parallel_tactic)
{
unsat.push_back(i);
}
break;
default:
#pragma omp critical (parallel_tactic)
{
update_progress(false);
}
break;
}
} }
for (int i = 0; i < sz; ++i) {
if (cubes[i].empty()) {
unsat.push_back(i);
continue;
}
solver& s = m_solvers[i]->get_solver();
ast_manager& m = s.get_manager();
if (cubes[i].size() == 1 && m.is_true(cubes[i][0].get())) {
continue;
}
for (unsigned j = 1; j < cubes[i].size(); ++j) {
m_solvers.push_back(m_solvers[i]->clone(m_params, cubes[i][j].get()));
}
expr* cube0 = cubes[i][0].get();
m_solvers[i]->add_cube(cube0);
s.assert_expr(cube0);
}
remove_unsat(unsat); remove_unsat(unsat);
update_max_conflicts(); update_max_conflicts();
} }
@ -341,7 +361,7 @@ private:
std::ostream& display(std::ostream& out) { std::ostream& display(std::ostream& out) {
for (solver_state* s : m_solvers) { for (solver_state* s : m_solvers) {
out << "solver units" << s->num_units() << "\n"; out << "solver units " << s->num_units() << "\n";
out << "cube " << s->cube() << "\n"; out << "cube " << s->cube() << "\n";
} }
m_stats.display(out); m_stats.display(out);
@ -359,7 +379,7 @@ public:
void operator ()(const goal_ref & g,goal_ref_buffer & result,model_converter_ref & mc,proof_converter_ref & pc,expr_dependency_ref & dep) { void operator ()(const goal_ref & g,goal_ref_buffer & result,model_converter_ref & mc,proof_converter_ref & pc,expr_dependency_ref & dep) {
ast_manager& m = g->m(); ast_manager& m = g->m();
solver* s = mk_fd_solver(m, m_params); solver* s = mk_fd_solver(m, m_params);
m_solvers.push_back(alloc(solver_state, 0, s)); m_solvers.push_back(alloc(solver_state, 0, s, m_params));
expr_ref_vector clauses(m); expr_ref_vector clauses(m);
ptr_vector<expr> assumptions; ptr_vector<expr> assumptions;
obj_map<expr, expr*> bool2dep; obj_map<expr, expr*> bool2dep;