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

Merge branch 'opt' of https://github.com/NikolajBjorner/z3 into opt

Browse source
This commit is contained in:
Miguel Angelo Da Terra Neves 2017-12-13 16:55:18 -08:00
parent 42499eac1c d1854ab4d2
commit 3edf0590bc
6 changed files with 33 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_elim_eqs.cpp
View file

@ -182,7 +182,7 @@ namespace sat {
literal l(v, false);
literal r = roots[v];
SASSERT(v != r.var());
if (m_solver.is_external(v) && !m_solver.set_root(l, r)) {
if (m_solver.is_external(v) || !m_solver.set_root(l, r)) {
// 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);

26
src/sat/sat_model_converter.cpp
View file

@ -39,6 +39,22 @@ namespace sat {
return *this;
}
bool model_converter::legal_to_flip(bool_var v) const {
// std::cout << "check " << v << " " << m_solver << "\n";
if (m_solver && m_solver->is_assumption(v)) {
std::cout << "flipping assumption v" << v << "\n";
UNREACHABLE();
throw solver_exception("flipping assumption");
}
if (m_solver && m_solver->is_external(v) && m_solver->is_incremental()) {
std::cout << "flipping external v" << v << "\n";
UNREACHABLE();
throw solver_exception("flipping external");
}
return !m_solver || !m_solver->is_assumption(v);
}
void model_converter::process_stack(model & m, literal_vector const& c, elim_stackv const& stack) const {
SASSERT(!stack.empty());
unsigned sz = stack.size();
@ -50,6 +66,7 @@ namespace sat {
sat = value_at(c[j], m) == l_true;
}
if (!sat) {
VERIFY(legal_to_flip(lit.var()));
m[lit.var()] = lit.sign() ? l_false : l_true;
}
}
@ -59,7 +76,7 @@ namespace sat {
vector<entry>::const_iterator begin = m_entries.begin();
vector<entry>::const_iterator it = m_entries.end();
bool first = true;
//VERIFY(!m_solver || m_solver->check_clauses(m));
//SASSERT(!m_solver || m_solver->check_clauses(m));
while (it != begin) {
--it;
SASSERT(it->get_kind() != ELIM_VAR || m[it->var()] == l_undef);
@ -69,11 +86,13 @@ namespace sat {
bool var_sign = false;
unsigned index = 0;
literal_vector clause;
VERIFY(legal_to_flip(it->var()));
for (literal l : it->m_clauses) {
if (l == null_literal) {
// end of clause
elim_stack* st = it->m_elim_stack[index];
if (!sat) {
if (!sat) {
VERIFY(legal_to_flip(it->var()));
m[it->var()] = var_sign ? l_false : l_true;
}
if (st) {
@ -101,6 +120,7 @@ namespace sat {
if (value_at(l, m) == l_true)
sat = true;
else if (!sat && v != it->var() && m[v] == l_undef) {
VERIFY(legal_to_flip(v));
// clause can be satisfied by assigning v.
m[v] = sign ? l_false : l_true;
// if (first) std::cout << "set: " << l << "\n";
@ -170,6 +190,7 @@ namespace sat {
entry & e = m_entries.back();
SASSERT(e.var() == v);
SASSERT(e.get_kind() == k);
VERIFY(legal_to_flip(v));
return e;
}
@ -213,6 +234,7 @@ namespace sat {
for (literal l : c) e.m_clauses.push_back(l);
e.m_clauses.push_back(null_literal);
e.m_elim_stack.push_back(elims.empty() ? nullptr : alloc(elim_stack, elims));
for (auto const& s : elims) VERIFY(legal_to_flip(s.second.var()));
TRACE("sat_mc_bug", tout << "adding: " << c << "\n";);
}

2
src/sat/sat_model_converter.h
View file

@ -92,6 +92,8 @@ namespace sat {
std::ostream& display(std::ostream & out, entry const& entry) const;
bool legal_to_flip(bool_var v) const;
public:
model_converter();
~model_converter();

3
src/sat/sat_simplifier.cpp
View file

@ -970,11 +970,12 @@ namespace sat {
}
void insert(literal l) {
VERIFY(process_var(l.var()));
m_queue.insert(l);
}
bool process_var(bool_var v) {
return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v);
return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v);
}
void operator()() {

6
src/sat/sat_solver.cpp
View file

@ -61,7 +61,7 @@ namespace sat {
m_num_checkpoints = 0;
m_simplifications = 0;
m_cuber = nullptr;
m_mc.set_solver(nullptr);
m_mc.set_solver(this);
}
solver::~solver() {
@ -1544,7 +1544,7 @@ namespace sat {
if (m_config.m_drat) m_drat.check_model(m_model);
m_mc.set_solver(nullptr);
// m_mc.set_solver(nullptr);
m_mc(m_model);
@ -1601,7 +1601,7 @@ namespace sat {
for (literal l : m_assumptions) {
if (value_at(l, m) != l_true) {
VERIFY(is_external(l.var()));
IF_VERBOSE(0, verbose_stream() << l << " does not model check " << value_at(l, m) << "\n";);
IF_VERBOSE(0, verbose_stream() << "assumption: " << l << " does not model check " << value_at(l, m) << "\n";);
TRACE("sat",
tout << l << " does not model check\n";
tout << "trail: " << m_trail << "\n";

2
src/sat/sat_solver.h
View file

@ -353,6 +353,7 @@ namespace sat {
void set_model(model const& mdl);
char const* get_reason_unknown() const { return m_reason_unknown.c_str(); }
bool check_clauses(model const& m) const;
bool is_assumption(bool_var v) const;
literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
lbool cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level);
@ -389,7 +390,6 @@ namespace sat {
void reinit_assumptions();
bool tracking_assumptions() const;
bool is_assumption(literal l) const;
bool is_assumption(bool_var v) const;
void simplify_problem();
void mk_model();
bool check_model(model const & m) const;