mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 09:26:15 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2013-06-14 11:35:22 +01:00
commit 8b43a1b5f6
3 changed files with 13 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz_qe/dl_instruction.cpp
View file

@ -528,9 +528,9 @@ namespace datalog {
class instr_filter_interpreted_and_project : public instruction { class instr_filter_interpreted_and_project : public instruction {
reg_idx m_src; reg_idx m_src;
reg_idx m_res;
app_ref m_cond; app_ref m_cond;
unsigned_vector m_cols; unsigned_vector m_cols;
reg_idx m_res;
public: public:
instr_filter_interpreted_and_project(reg_idx src, app_ref & condition, instr_filter_interpreted_and_project(reg_idx src, app_ref & condition,
unsigned col_cnt, const unsigned * removed_cols, reg_idx result) unsigned col_cnt, const unsigned * removed_cols, reg_idx result)

8
src/sat/sat_asymm_branch.cpp
View file

@ -72,11 +72,14 @@ namespace sat {
int limit = -static_cast<int>(m_asymm_branch_limit); int limit = -static_cast<int>(m_asymm_branch_limit);
std::stable_sort(s.m_clauses.begin(), s.m_clauses.end(), clause_size_lt()); std::stable_sort(s.m_clauses.begin(), s.m_clauses.end(), clause_size_lt());
m_counter -= s.m_clauses.size(); m_counter -= s.m_clauses.size();
SASSERT(s.m_qhead == s.m_trail.size());
clause_vector::iterator it = s.m_clauses.begin(); clause_vector::iterator it = s.m_clauses.begin();
clause_vector::iterator it2 = it; clause_vector::iterator it2 = it;
clause_vector::iterator end = s.m_clauses.end(); clause_vector::iterator end = s.m_clauses.end();
try { try {
for (; it != end; ++it) { for (; it != end; ++it) {
if (s.inconsistent())
break;
SASSERT(s.m_qhead == s.m_trail.size()); SASSERT(s.m_qhead == s.m_trail.size());
if (m_counter < limit || s.inconsistent()) { if (m_counter < limit || s.inconsistent()) {
*it2 = *it; *it2 = *it;
@ -111,6 +114,7 @@ namespace sat {
bool asymm_branch::process(clause & c) { bool asymm_branch::process(clause & c) {
TRACE("asymm_branch_detail", tout << "processing: " << c << "\n";); TRACE("asymm_branch_detail", tout << "processing: " << c << "\n";);
SASSERT(s.scope_lvl() == 0); SASSERT(s.scope_lvl() == 0);
SASSERT(s.m_qhead == s.m_trail.size());
#ifdef Z3DEBUG #ifdef Z3DEBUG
unsigned trail_sz = s.m_trail.size(); unsigned trail_sz = s.m_trail.size();
#endif #endif
@ -143,6 +147,7 @@ namespace sat {
SASSERT(!s.inconsistent()); SASSERT(!s.inconsistent());
SASSERT(s.scope_lvl() == 0); SASSERT(s.scope_lvl() == 0);
SASSERT(trail_sz == s.m_trail.size()); SASSERT(trail_sz == s.m_trail.size());
SASSERT(s.m_qhead == s.m_trail.size());
if (i == sz - 1) { if (i == sz - 1) {
// clause size can't be reduced. // clause size can't be reduced.
s.attach_clause(c); s.attach_clause(c);
@ -181,15 +186,18 @@ namespace sat {
s.assign(c[0], justification()); s.assign(c[0], justification());
s.del_clause(c); s.del_clause(c);
s.propagate_core(false); s.propagate_core(false);
SASSERT(s.inconsistent() || s.m_qhead == s.m_trail.size());
return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state. return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state.
case 2: case 2:
SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef); SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
s.mk_bin_clause(c[0], c[1], false); s.mk_bin_clause(c[0], c[1], false);
s.del_clause(c); s.del_clause(c);
SASSERT(s.m_qhead == s.m_trail.size());
return false; return false;
default: default:
c.shrink(new_sz); c.shrink(new_sz);
s.attach_clause(c); s.attach_clause(c);
SASSERT(s.m_qhead == s.m_trail.size());
return true; return true;
} }
} }

6
src/sat/sat_simplifier.cpp
View file

@ -632,7 +632,8 @@ namespace sat {
case 1: case 1:
TRACE("elim_lit", tout << "clause became unit: " << c[0] << "\n";); TRACE("elim_lit", tout << "clause became unit: " << c[0] << "\n";);
propagate_unit(c[0]); propagate_unit(c[0]);
remove_clause(c); // propagate_unit will delete c.
// remove_clause(c);
return; return;
case 2: case 2:
TRACE("elim_lit", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";); TRACE("elim_lit", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";);
@ -823,7 +824,8 @@ namespace sat {
} }
if (sz == 1) { if (sz == 1) {
propagate_unit(c[0]); propagate_unit(c[0]);
remove_clause(c); // propagate_unit will delete c.
// remove_clause(c);
continue; continue;
} }
if (sz == 2) { if (sz == 2) {