mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 19:35:50 +00:00
Fixed bug in sat model converter. Fixes #1148.
This commit is contained in:
Christoph M. Wintersteiger
parent
8a57e081f7
commit
da34de340d
4 changed files with 45 additions and 24 deletions
|
|
@ -32,7 +32,7 @@ namespace sat {
|
|||
void model_converter::reset() {
|
||||
m_entries.finalize();
|
||||
}
|
||||
|
||||
|
||||
void model_converter::operator()(model & m) const {
|
||||
vector<entry>::const_iterator begin = m_entries.begin();
|
||||
vector<entry>::const_iterator it = m_entries.end();
|
||||
|
|
@ -46,7 +46,7 @@ namespace sat {
|
|||
literal_vector::const_iterator it2 = it->m_clauses.begin();
|
||||
literal_vector::const_iterator end2 = it->m_clauses.end();
|
||||
for (; it2 != end2; ++it2) {
|
||||
literal l = *it2;
|
||||
literal l = *it2;
|
||||
if (l == null_literal) {
|
||||
// end of clause
|
||||
if (!sat) {
|
||||
|
|
@ -56,6 +56,7 @@ namespace sat {
|
|||
sat = false;
|
||||
continue;
|
||||
}
|
||||
|
||||
if (sat)
|
||||
continue;
|
||||
bool sign = l.sign();
|
||||
|
|
@ -125,7 +126,7 @@ namespace sat {
|
|||
}
|
||||
return ok;
|
||||
}
|
||||
|
||||
|
||||
model_converter::entry & model_converter::mk(kind k, bool_var v) {
|
||||
m_entries.push_back(entry(k, v));
|
||||
entry & e = m_entries.back();
|
||||
|
|
@ -218,7 +219,7 @@ namespace sat {
|
|||
out << *it2;
|
||||
}
|
||||
out << ")";
|
||||
}
|
||||
}
|
||||
out << ")\n";
|
||||
}
|
||||
|
||||
|
|
@ -237,4 +238,22 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
unsigned model_converter::max_var(unsigned min) const {
|
||||
unsigned result = min;
|
||||
vector<entry>::const_iterator it = m_entries.begin();
|
||||
vector<entry>::const_iterator end = m_entries.end();
|
||||
for (; it != end; ++it) {
|
||||
literal_vector::const_iterator lvit = it->m_clauses.begin();
|
||||
literal_vector::const_iterator lvend = it->m_clauses.end();
|
||||
for (; lvit != lvend; ++lvit) {
|
||||
literal l = *lvit;
|
||||
if (l != null_literal) {
|
||||
if (l.var() > result)
|
||||
result = l.var();
|
||||
}
|
||||
}
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -26,7 +26,7 @@ namespace sat {
|
|||
\brief Stores eliminated variables and Blocked clauses.
|
||||
It uses these clauses to extend/patch the model produced for the
|
||||
simplified CNF formula.
|
||||
|
||||
|
||||
This information may also be used to support incremental solving.
|
||||
If new clauses are asserted into the SAT engine, then we can
|
||||
restore the state by re-asserting all clauses in the model
|
||||
|
|
@ -50,7 +50,7 @@ namespace sat {
|
|||
m_kind(src.m_kind),
|
||||
m_clauses(src.m_clauses) {
|
||||
}
|
||||
bool_var var() const { return m_var; }
|
||||
bool_var var() const { return m_var; }
|
||||
kind get_kind() const { return static_cast<kind>(m_kind); }
|
||||
};
|
||||
private:
|
||||
|
|
@ -74,8 +74,9 @@ namespace sat {
|
|||
|
||||
void copy(model_converter const & src);
|
||||
void collect_vars(bool_var_set & s) const;
|
||||
unsigned max_var(unsigned min) const;
|
||||
};
|
||||
|
||||
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -2628,7 +2628,7 @@ namespace sat {
|
|||
unsigned j = 0;
|
||||
for (unsigned i = 0; i < clauses.size(); ++i) {
|
||||
clause & c = *(clauses[i]);
|
||||
if (c.contains(lit)) {
|
||||
if (c.contains(lit) || c.contains(~lit)) {
|
||||
detach_clause(c);
|
||||
del_clause(c);
|
||||
}
|
||||
|
|
@ -2684,6 +2684,7 @@ namespace sat {
|
|||
w = max_var(m_clauses, w);
|
||||
w = max_var(true, w);
|
||||
w = max_var(false, w);
|
||||
v = m_mc.max_var(w);
|
||||
for (unsigned i = 0; i < m_trail.size(); ++i) {
|
||||
if (m_trail[i].var() > w) w = m_trail[i].var();
|
||||
}
|
||||
|
|
@ -3150,9 +3151,9 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// Algorithm 7: Corebased Algorithm with Chunking
|
||||
|
||||
|
||||
static void back_remove(sat::literal_vector& lits, sat::literal l) {
|
||||
for (unsigned i = lits.size(); i > 0; ) {
|
||||
--i;
|
||||
|
|
@ -3176,7 +3177,7 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
static lbool core_chunking(sat::solver& s, model const& m, sat::bool_var_vector const& vars, sat::literal_vector const& asms, vector<sat::literal_vector>& conseq, unsigned K) {
|
||||
sat::literal_vector lambda;
|
||||
for (unsigned i = 0; i < vars.size(); i++) {
|
||||
|
|
@ -3375,7 +3376,7 @@ namespace sat {
|
|||
if (check_inconsistent()) return l_false;
|
||||
|
||||
unsigned num_iterations = 0;
|
||||
extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq);
|
||||
extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq);
|
||||
update_unfixed_literals(unfixed_lits, unfixed_vars);
|
||||
while (!unfixed_lits.empty()) {
|
||||
if (scope_lvl() > 1) {
|
||||
|
|
@ -3390,7 +3391,7 @@ namespace sat {
|
|||
unsigned num_assigned = 0;
|
||||
lbool is_sat = l_true;
|
||||
for (; it != end; ++it) {
|
||||
literal lit = *it;
|
||||
literal lit = *it;
|
||||
if (value(lit) != l_undef) {
|
||||
++num_fixed;
|
||||
if (lvl(lit) <= 1 && value(lit) == l_true) {
|
||||
|
|
@ -3445,8 +3446,8 @@ namespace sat {
|
|||
<< " iterations: " << num_iterations
|
||||
<< " variables: " << unfixed_lits.size()
|
||||
<< " fixed: " << conseq.size()
|
||||
<< " status: " << is_sat
|
||||
<< " pre-assigned: " << num_fixed
|
||||
<< " status: " << is_sat
|
||||
<< " pre-assigned: " << num_fixed
|
||||
<< " unfixed: " << lits.size() - conseq.size() - unfixed_lits.size()
|
||||
<< ")\n";);
|
||||
|
||||
|
|
|
|||
|
|
@ -131,7 +131,7 @@ public:
|
|||
}
|
||||
|
||||
bool is_literal(expr* e) const {
|
||||
return
|
||||
return
|
||||
is_uninterp_const(e) ||
|
||||
(m.is_not(e, e) && is_uninterp_const(e));
|
||||
}
|
||||
|
|
@ -153,7 +153,7 @@ public:
|
|||
asm2fml.insert(assumptions[i], assumptions[i]);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
TRACE("sat", tout << _assumptions << "\n";);
|
||||
dep2asm_t dep2asm;
|
||||
m_model = 0;
|
||||
|
|
@ -163,7 +163,7 @@ public:
|
|||
if (r != l_true) return r;
|
||||
|
||||
r = m_solver.check(m_asms.size(), m_asms.c_ptr());
|
||||
|
||||
|
||||
switch (r) {
|
||||
case l_true:
|
||||
if (sz > 0) {
|
||||
|
|
@ -280,14 +280,14 @@ public:
|
|||
return r;
|
||||
}
|
||||
|
||||
// build map from bound variables to
|
||||
// build map from bound variables to
|
||||
// the consequences that cover them.
|
||||
u_map<unsigned> bool_var2conseq;
|
||||
for (unsigned i = 0; i < lconseq.size(); ++i) {
|
||||
TRACE("sat", tout << lconseq[i] << "\n";);
|
||||
bool_var2conseq.insert(lconseq[i][0].var(), i);
|
||||
}
|
||||
|
||||
|
||||
// extract original fixed variables
|
||||
u_map<expr*> asm2dep;
|
||||
extract_asm2dep(dep2asm, asm2dep);
|
||||
|
|
@ -441,7 +441,7 @@ private:
|
|||
|
||||
lbool internalize_vars(expr_ref_vector const& vars, sat::bool_var_vector& bvars) {
|
||||
for (unsigned i = 0; i < vars.size(); ++i) {
|
||||
internalize_var(vars[i], bvars);
|
||||
internalize_var(vars[i], bvars);
|
||||
}
|
||||
return l_true;
|
||||
}
|
||||
|
|
@ -453,7 +453,7 @@ private:
|
|||
bool internalized = false;
|
||||
if (is_uninterp_const(v) && m.is_bool(v)) {
|
||||
sat::bool_var b = m_map.to_bool_var(v);
|
||||
|
||||
|
||||
if (b != sat::null_bool_var) {
|
||||
bvars.push_back(b);
|
||||
internalized = true;
|
||||
|
|
@ -479,7 +479,7 @@ private:
|
|||
else if (is_uninterp_const(v) && bvutil.is_bv(v)) {
|
||||
// variable does not occur in assertions, so is unconstrained.
|
||||
}
|
||||
CTRACE("sat", !internalized, tout << "unhandled variable " << mk_pp(v, m) << "\n";);
|
||||
CTRACE("sat", !internalized, tout << "unhandled variable " << mk_pp(v, m) << "\n";);
|
||||
return internalized;
|
||||
}
|
||||
|
||||
|
|
@ -506,7 +506,7 @@ private:
|
|||
}
|
||||
expr_ref val(m);
|
||||
expr_ref_vector conj(m);
|
||||
internalize_value(value, v, val);
|
||||
internalize_value(value, v, val);
|
||||
while (!premises.empty()) {
|
||||
expr* e = 0;
|
||||
VERIFY(asm2dep.find(premises.pop().index(), e));
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue