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

Bugfix for assumptions in inc_sat_solver

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-03-04 14:42:38 +00:00
parent b2eb5b7170
commit a51201298c
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -151,6 +151,7 @@ public:
lbool r = internalize_formulas(); lbool r = internalize_formulas();
if (r != l_true) return r; if (r != l_true) return r;
r = internalize_assumptions(sz, assumptions, dep2asm); r = internalize_assumptions(sz, assumptions, dep2asm);
SASSERT(sz == m_asms.size());
if (r != l_true) return r; if (r != l_true) return r;
r = m_solver.check(m_asms.size(), m_asms.c_ptr(), m_weights.c_ptr(), max_weight); r = m_solver.check(m_asms.size(), m_asms.c_ptr(), m_weights.c_ptr(), max_weight);
@ -300,6 +301,7 @@ private:
lbool internalize_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) { lbool internalize_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) {
if (sz == 0) { if (sz == 0) {
m_asms.shrink(0);
return l_true; return l_true;
} }
goal_ref g = alloc(goal, m, true, true); // models and cores are enabled. goal_ref g = alloc(goal, m, true, true); // models and cores are enabled.
@ -331,6 +333,7 @@ private:
sat::literal lit; sat::literal lit;
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
if (dep2asm.find(asms[i], lit)) { if (dep2asm.find(asms[i], lit)) {
SASSERT(lit.var() <= m_solver.num_vars());
m_asms.push_back(lit); m_asms.push_back(lit);
if (i != j && !m_weights.empty()) { if (i != j && !m_weights.empty()) {
m_weights[j] = m_weights[i]; m_weights[j] = m_weights[i];