mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

local

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-02-01 12:09:16 -08:00
parent 669c018242
commit becce1d043
3 changed files with 10 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/sat/card_extension.cpp
View file

@ -676,14 +676,6 @@ namespace sat {
} }
result->add_at_least(c.lit().var(), lits, c.k()); result->add_at_least(c.lit().var(), lits, c.k());
} }
for (unsigned i = 0; i < m_var_trail.size(); ++i) {
bool_var v = m_var_trail[i];
if (v != null_bool_var) {
card* c = m_var_infos[v].m_card;
card* c2 = m_constraints[c->index()];
NOT_IMPLEMENTED_YET();
}
}
return result; return result;
} }

14
src/sat/sat_solver.cpp
View file

@ -75,7 +75,7 @@ namespace sat {
void solver::copy(solver const & src) { void solver::copy(solver const & src) {
pop_to_base_level(); pop_to_base_level();
SASSERT(m_mc.empty() && src.m_mc.empty()); SASSERT(m_mc.empty() && src.m_mc.empty());
SASSERT(scope_lvl() == 0); SASSERT(at_search_lvl());
// create new vars // create new vars
if (num_vars() < src.num_vars()) { if (num_vars() < src.num_vars()) {
for (bool_var v = num_vars(); v < src.num_vars(); v++) { for (bool_var v = num_vars(); v < src.num_vars(); v++) {
@ -85,8 +85,15 @@ namespace sat {
VERIFY(v == mk_var(ext, dvar)); VERIFY(v == mk_var(ext, dvar));
} }
} }
//
// register the extension before performing assignments.
// the assignments may call back into the extension.
//
if (src.get_extension()) {
m_ext = src.get_extension()->copy(this);
}
{ {
unsigned sz = src.scope_lvl() == 0 ? src.m_trail.size() : src.m_scopes[0].m_trail_lim; unsigned sz = scope_lvl() == 0 ? src.m_trail.size() : src.m_scopes[0].m_trail_lim;
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
assign(src.m_trail[i], justification()); assign(src.m_trail[i], justification());
} }
@ -125,9 +132,6 @@ namespace sat {
} }
} }
if (src.get_extension()) {
m_ext = src.get_extension()->copy(this);
}
m_user_scope_literals.reset(); m_user_scope_literals.reset();
m_user_scope_literals.append(src.m_user_scope_literals); m_user_scope_literals.append(src.m_user_scope_literals);
} }

1
src/sat/sat_solver.h
View file

@ -220,6 +220,7 @@ namespace sat {
bool is_external(bool_var v) const { return m_external[v] != 0; } bool is_external(bool_var v) const { return m_external[v] != 0; }
bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; } bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
unsigned scope_lvl() const { return m_scope_lvl; } unsigned scope_lvl() const { return m_scope_lvl; }
bool at_search_lvl() const { return m_scope_lvl == 0; }
lbool value(literal l) const { return static_cast<lbool>(m_assignment[l.index()]); } lbool value(literal l) const { return static_cast<lbool>(m_assignment[l.index()]); }
lbool value(bool_var v) const { return static_cast<lbool>(m_assignment[literal(v, false).index()]); } lbool value(bool_var v) const { return static_cast<lbool>(m_assignment[literal(v, false).index()]); }
unsigned lvl(bool_var v) const { return m_level[v]; } unsigned lvl(bool_var v) const { return m_level[v]; }