mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

disable bdd variable elimination

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-31 17:05:22 -07:00
parent 55eb11d91b
commit 528dc8a3f8
10 changed files with 58 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/sat/sat_clause_use_list.h
View file

@ -124,6 +124,15 @@ namespace sat {
};
iterator mk_iterator() const { return iterator(const_cast<clause_use_list*>(this)->m_clauses); }
std::ostream& display(std::ostream& out) const {
iterator it = mk_iterator();
while (!it.at_end()) {
out << it.curr() << "\n";
it.next();
}
return out;
}
};
};

2
src/sat/sat_elim_eqs.cpp
View file

@ -199,7 +199,7 @@ namespace sat {
literal r = roots[v];
SASSERT(v != r.var());
bool root_ok = !m_solver.is_external(v) || m_solver.set_root(l, r);
if (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok)) {
if (m_solver.is_assumption(v) || (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok))) {
// cannot really eliminate v, since we have to notify extension of future assignments
m_solver.mk_bin_clause(~l, r, false);
m_solver.mk_bin_clause(l, ~r, false);

9
src/sat/sat_elim_vars.cpp
View file

@ -101,7 +101,7 @@ namespace sat{
pos_occs.reset();
neg_occs.reset();
literal_vector lits;
add_clauses(b, lits);
add_clauses(v, b, lits);
return true;
}
@ -157,7 +157,7 @@ namespace sat{
return b;
}
void elim_vars::add_clauses(bdd const& b, literal_vector& lits) {
void elim_vars::add_clauses(bool_var v0, bdd const& b, literal_vector& lits) {
if (b.is_true()) {
// no-op
}
@ -167,6 +167,7 @@ namespace sat{
if (simp.cleanup_clause(c))
return;
if (v0 == 39063) IF_VERBOSE(0, verbose_stream() << "bdd: " << c << "\n");
switch (c.size()) {
case 0:
s.set_conflict(justification());
@ -198,10 +199,10 @@ namespace sat{
else {
unsigned v = m_vars[b.var()];
lits.push_back(literal(v, false));
add_clauses(b.lo(), lits);
add_clauses(v0, b.lo(), lits);
lits.pop_back();
lits.push_back(literal(v, true));
add_clauses(b.hi(), lits);
add_clauses(v0, b.hi(), lits);
lits.pop_back();
}
}

2
src/sat/sat_elim_vars.h
View file

@ -57,7 +57,7 @@ namespace sat {
bdd make_clauses(literal lit);
bdd mk_literal(literal l);
void get_clauses(bdd const& b, literal_vector& lits, clause_vector& clauses, literal_vector& units);
void add_clauses(bdd const& b, literal_vector& lits);
void add_clauses(bool_var v, bdd const& b, literal_vector& lits);
bool elim_var(bool_var v, bdd const& b);
bdd elim_var(bool_var v);

5
src/sat/sat_model_converter.cpp
View file

@ -91,11 +91,6 @@ namespace sat {
for (literal l : it->m_clauses) {
if (l == null_literal) {
// end of clause
if (v0 == 36858)
IF_VERBOSE(0, verbose_stream() << "clause: " << clause << "\n";
for (literal lit : clause) verbose_stream() << m[lit.var()] << " ";
verbose_stream() << "\n";);
elim_stack* st = it->m_elim_stack[index];
if (!sat) {
VERIFY(legal_to_flip(v0));

12
src/sat/sat_simplifier.cpp
View file

@ -1518,6 +1518,14 @@ namespace sat {
}
void block_covered_clause(clause& c, literal l, model_converter::kind k) {
if (false && l.var() == 39021) {
IF_VERBOSE(0, verbose_stream() << "blocked: " << l << " @ " << c << " :covered " << m_covered_clause << "\n";
s.m_use_list.display(verbose_stream() << "use " << l << ":", l);
s.m_use_list.display(verbose_stream() << "use " << ~l << ":", ~l);
/*s.s.display(verbose_stream());*/
);
}
TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
SASSERT(!s.is_external(l));
model_converter::entry& new_entry = mc.mk(k, l.var());
@ -1563,7 +1571,6 @@ namespace sat {
for (literal l2 : m_intersection) {
watched* w = find_binary_watch(s.get_wlist(~l), ~l2);
if (!w) {
IF_VERBOSE(10, verbose_stream() << "bca " << l << " " << ~l2 << "\n";);
s.s.mk_bin_clause(l, ~l2, true);
++s.m_num_bca;
}
@ -1934,6 +1941,7 @@ namespace sat {
m_new_cls.reset();
if (!resolve(c1, c2, pos_l, m_new_cls))
continue;
// if (v == 39063) IF_VERBOSE(0, verbose_stream() << "elim: " << c1 << " + " << c2 << " -> " << m_new_cls << "\n");
TRACE("resolution_new_cls", tout << c1 << "\n" << c2 << "\n-->\n" << m_new_cls << "\n";);
if (cleanup_clause(m_new_cls))
continue; // clause is already satisfied.
@ -2045,7 +2053,7 @@ namespace sat {
m_subsumption = p.subsumption();
m_subsumption_limit = p.subsumption_limit();
m_elim_vars = p.elim_vars();
m_elim_vars_bdd = p.elim_vars_bdd();
m_elim_vars_bdd = false && p.elim_vars_bdd(); // buggy
m_elim_vars_bdd_delay = p.elim_vars_bdd_delay();
m_incremental_mode = s.get_config().m_incremental && !p.override_incremental();
}

1
src/sat/sat_simplifier.h
View file

@ -47,6 +47,7 @@ namespace sat {
clause_use_list & get(literal l) { return m_use_list[l.index()]; }
clause_use_list const & get(literal l) const { return m_use_list[l.index()]; }
void finalize() { m_use_list.finalize(); }
std::ostream& display(std::ostream& out, literal l) const { return m_use_list[l.index()].display(out); }
};
class simplifier {

3
src/sat/sat_solver.cpp
View file

@ -1654,11 +1654,10 @@ namespace sat {
// m_mc.set_solver(nullptr);
m_mc(m_model);
if (!check_clauses(m_model)) {
IF_VERBOSE(0, verbose_stream() << "failure checking clauses on transformed model\n";);
IF_VERBOSE(10, m_mc.display(verbose_stream()));
// IF_VERBOSE(10, m_mc.display(verbose_stream()));
throw solver_exception("check model failed");
}

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

@ -114,10 +114,10 @@ class parallel_tactic : public tactic {
dec_wait();
return st;
}
{
std::unique_lock<std::mutex> lock(m_mutex);
m_cond.wait(lock);
}
{
std::unique_lock<std::mutex> lock(m_mutex);
m_cond.wait(lock);
}
dec_wait();
}
return nullptr;
@ -233,7 +233,9 @@ class parallel_tactic : public tactic {
void inc_depth(unsigned inc) { m_depth += inc; }
void inc_width(unsigned w) { m_width *= w; }
void inc_width(unsigned w) {
m_width *= w;
}
double get_width() const { return m_width; }
@ -280,14 +282,14 @@ class parallel_tactic : public tactic {
void set_cube_params() {
unsigned cutoff = m_cube_cutoff;
double fraction = m_cube_fraction;
if (m_depth == 1 && cutoff > 0) {
fraction = 0; // use fixed cubing at depth 1.
if (true || (m_depth == 1 && cutoff > 0)) {
m_params.set_sym("lookahead.cube.cutoff", symbol("depth"));
m_params.set_uint("lookahead.cube.depth", std::max(m_depth, 10u));
}
else {
cutoff = 0; // use dynamic cubing beyond depth 1
m_params.set_sym("lookahead.cube.cutoff", symbol("adaptive_psat"));
m_params.set_double("lookahead.cube.fraction", fraction);
}
m_params.set_uint ("lookahead.cube.cutoff", cutoff);
m_params.set_double("lookahead.cube.fraction", fraction);
get_solver().updt_params(m_params);
}
@ -329,6 +331,7 @@ private:
task_queue m_queue;
std::mutex m_mutex;
double m_progress;
unsigned m_branches;
bool m_has_undef;
bool m_allsat;
unsigned m_num_unsat;
@ -341,20 +344,27 @@ private:
m_has_undef = false;
m_allsat = false;
m_num_unsat = 0;
m_branches = 0;
m_exn_code = 0;
m_params.set_bool("override_incremental", true);
}
void add_branches(unsigned b) {
std::lock_guard<std::mutex> lock(m_mutex);
m_branches += b;
}
void close_branch(solver_state& s, lbool status) {
double f = 100.0 / s.get_width();
{
std::lock_guard<std::mutex> lock(m_mutex);
m_progress += f;
--m_branches;
}
IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :progress " << m_progress << "% ";
IF_VERBOSE(0, verbose_stream() << "(tactic.parallel :progress " << m_progress << "% ";
if (status == l_true) verbose_stream() << ":status sat ";
if (status == l_undef) verbose_stream() << ":status unknown ";
verbose_stream() << ":unsat " << m_num_unsat << ")\n";);
verbose_stream() << ":unsat " << m_num_unsat << " :branches " << m_branches << ")\n";);
}
void report_sat(solver_state& s) {
@ -401,7 +411,7 @@ private:
cube.reset();
cube.append(s.split_cubes(1));
SASSERT(cube.size() <= 1);
IF_VERBOSE(2, verbose_stream() << "(sat.parallel :split-cube " << cube.size() << ")\n";);
IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :split-cube " << cube.size() << ")\n";);
if (!s.cubes().empty()) m_queue.add_task(s.clone());
if (!cube.empty()) s.assert_cube(cube.get(0));
s.inc_depth(1);
@ -430,8 +440,8 @@ private:
cubes.push_back(mk_and(c));
}
IF_VERBOSE(1, verbose_stream() << "(parallel_tactic :cubes " << cubes.size() << ")\n";);
IF_VERBOSE(10, verbose_stream() << "(parallel_tactic :cubes " << cubes << ")\n";);
IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :cubes " << cubes.size() << ")\n";);
IF_VERBOSE(12, verbose_stream() << "(tactic.parallel :cubes " << cubes << ")\n";);
if (cubes.empty()) {
report_unsat(s);
@ -439,6 +449,7 @@ private:
}
else {
s.inc_width(cubes.size());
add_branches(cubes.size());
s.set_cubes(cubes);
s.set_type(conquer_task);
goto conquer;
@ -462,7 +473,7 @@ private:
}
if (canceled(s)) return;
}
IF_VERBOSE(1, verbose_stream() << "(parallel_tactic :cubes " << cubes.size() << " :hard-cubes " << hard_cubes.size() << ")\n";);
IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :cubes " << cubes.size() << " :hard-cubes " << hard_cubes.size() << ")\n";);
if (hard_cubes.empty()) return;
s.set_cubes(hard_cubes);
@ -534,7 +545,7 @@ private:
m_stats.display(out);
m_queue.display(out);
std::lock_guard<std::mutex> lock(m_mutex);
out << "(parallel_tactic :unsat " << m_num_unsat << " :progress " << m_progress << "% :models " << m_models.size() << ")\n";
out << "(tactic.parallel :unsat " << m_num_unsat << " :progress " << m_progress << "% :models " << m_models.size() << ")\n";
return out;
}

2
src/tactic/smtlogics/qfbv_tactic.cpp
View file

@ -28,6 +28,7 @@ Notes:
#include "tactic/bv/bv_size_reduction_tactic.h"
#include "tactic/aig/aig_tactic.h"
#include "sat/tactic/sat_tactic.h"
#include "tactic/portfolio/parallel_tactic.h"
#include "ackermannization/ackermannize_bv_tactic.h"
#define MEMLIMIT 300
@ -130,6 +131,7 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
tactic * new_sat = cond(mk_produce_proofs_probe(),
and_then(mk_simplify_tactic(m), mk_smt_tactic()),
//mk_parallel_tactic(m, p));
mk_sat_tactic(m));
return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic());