mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 14:23:40 +00:00
Code Activity

working on HS

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-06-17 17:05:05 -07:00
parent b64b12cae3
commit 84d971b69a
2 changed files with 99 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

122
src/opt/hitting_sets.cpp
View file

@ -38,14 +38,23 @@ namespace opt {
private: private:
kind_t m_kind; kind_t m_kind;
unsigned m_value; unsigned m_value;
bool m_pos;
public: public:
justification(kind_t k):m_kind(k), m_value(0) {} explicit justification(kind_t k):m_kind(k), m_value(0), m_pos(false) {}
justification(unsigned v):m_kind(CLAUSE), m_value(v) {} explicit justification(unsigned v, bool pos):m_kind(CLAUSE), m_value(v), m_pos(pos) {}
explicit justification(justification const& other): m_kind(other.m_kind), m_value(other.m_value), m_pos(other.m_pos) {}
justification& operator=(justification const& other) {
m_kind = other.m_kind;
m_value = other.m_value;
m_pos = other.m_pos;
return *this;
}
unsigned clause() const { return m_value; } unsigned clause() const { return m_value; }
bool is_axiom() const { return m_kind == AXIOM; } bool is_axiom() const { return m_kind == AXIOM; }
bool is_decision() const { return m_kind == DECISION; } bool is_decision() const { return m_kind == DECISION; }
bool is_clause() const { return m_kind == CLAUSE; } bool is_clause() const { return m_kind == CLAUSE; }
kind_t kind() const { return m_kind; } kind_t kind() const { return m_kind; }
bool pos() const { return m_pos; }
}; };
volatile bool m_cancel; volatile bool m_cancel;
rational m_lower; rational m_lower;
@ -92,9 +101,7 @@ namespace opt {
sat::solver m_solver; sat::solver m_solver;
svector<sat::bool_var> m_vars; svector<sat::bool_var> m_vars;
static unsigned const null_clause = UINT_MAX; static unsigned const null_idx = UINT_MAX;
static unsigned const axiom = UINT_MAX-1;
static unsigned const decision = UINT_MAX-2;
imp(): imp():
m_cancel(false), m_cancel(false),
@ -102,6 +109,7 @@ namespace opt {
m_denominator(1), m_denominator(1),
m_weights_var(0), m_weights_var(0),
m_qhead(0), m_qhead(0),
m_scope_lvl(0),
m_conflict_j(justification(justification::AXIOM)), m_conflict_j(justification(justification::AXIOM)),
m_inconsistent(false), m_inconsistent(false),
m_solver(m_params,0) { m_solver(m_params,0) {
@ -118,13 +126,14 @@ namespace opt {
m_simplex.set_upper(var, mpq_inf(mpq(1),mpq(0))); m_simplex.set_upper(var, mpq_inf(mpq(1),mpq(0)));
m_weights.push_back(w); m_weights.push_back(w);
m_value.push_back(l_undef); m_value.push_back(l_undef);
m_justification.push_back(null_clause); m_justification.push_back(justification(justification::DECISION));
m_tuse_list.push_back(unsigned_vector()); m_tuse_list.push_back(unsigned_vector());
m_fuse_list.push_back(unsigned_vector()); m_fuse_list.push_back(unsigned_vector());
m_twatch.push_back(unsigned_vector()); m_twatch.push_back(unsigned_vector());
m_fwatch.push_back(unsigned_vector()); m_fwatch.push_back(unsigned_vector());
m_level.push_back(0); m_level.push_back(0);
m_indices.push_back(var); m_indices.push_back(var);
m_model.push_back(l_undef);
m_mark.push_back(false); m_mark.push_back(false);
m_scores.push_back(0); m_scores.push_back(0);
m_max_weight += w; m_max_weight += w;
@ -150,7 +159,7 @@ namespace opt {
} }
init_weights(); init_weights();
if (sz == 1) { if (sz == 1) {
assign(S[0], val, axiom); assign(S[0], val, justification(justification::AXIOM));
} }
else { else {
watch[S[0]].push_back(Sets.size()); watch[S[0]].push_back(Sets.size());
@ -179,7 +188,8 @@ namespace opt {
lbool compute_upper() { lbool compute_upper() {
m_upper = m_max_weight; m_upper = m_max_weight;
return U1(); return search();
// return U1();
} }
rational get_lower() { rational get_lower() {
@ -283,6 +293,25 @@ namespace opt {
out << "\n"; out << "\n";
} }
void display(std::ostream& out, justification const& j) const {
switch(j.kind()) {
case justification::AXIOM:
out << "axiom\n";
break;
case justification::DECISION:
out << "decision\n";
break;
case justification::CLAUSE: {
out << "clause: ";
set const& S = j.pos()?m_T[j.clause()]:m_F[j.clause()];
for (unsigned i = 0; i < S.size(); ++i) {
out << S[i] << " ";
}
out << "\n";
}
}
}
struct scoped_select { struct scoped_select {
imp& s; imp& s;
unsigned sz; unsigned sz;
@ -346,7 +375,7 @@ namespace opt {
} }
} }
IF_VERBOSE(1, verbose_stream() << "(hs.unselect " << j << ")\n";); IF_VERBOSE(1, verbose_stream() << "(hs.unselect " << j << ")\n";);
assign(j, l_false, decision); assign(j, l_false, justification(justification::DECISION));
for (i = 0; i < m_T.size(); ++i) { for (i = 0; i < m_T.size(); ++i) {
set const& S = m_T[i]; set const& S = m_T[i];
for (j = 0; j < S.size(); ++j) { for (j = 0; j < S.size(); ++j) {
@ -423,7 +452,7 @@ namespace opt {
if (m_scores[idx] == 0) { if (m_scores[idx] == 0) {
break; break;
} }
assign(idx, l_true, decision); assign(idx, l_true, justification(justification::DECISION));
} }
m_upper = m_weight; m_upper = m_weight;
m_model.reset(); m_model.reset();
@ -458,7 +487,7 @@ namespace opt {
if (!has_selected(S)) { if (!has_selected(S)) {
w += m_weights[select_min(S)]; w += m_weights[select_min(S)];
for (unsigned j = 0; j < S.size(); ++j) { for (unsigned j = 0; j < S.size(); ++j) {
assign(S[j], l_true, decision); assign(S[j], l_true, justification(justification::DECISION));
} }
} }
} }
@ -631,7 +660,7 @@ namespace opt {
} }
} }
void assign(unsigned j, lbool val, unsigned justification) { void assign(unsigned j, lbool val, justification const& justification) {
if (val == l_true) { if (val == l_true) {
m_weight += m_weights[j]; m_weight += m_weights[j];
} }
@ -652,6 +681,7 @@ namespace opt {
} }
TRACE("opt", tout << m_weight << "\n";); TRACE("opt", tout << m_weight << "\n";);
m_trail.shrink(sz); m_trail.shrink(sz);
m_qhead = sz;
} }
@ -669,13 +699,36 @@ namespace opt {
if (!decide()) { if (!decide()) {
m_model.reset(); m_model.reset();
m_model.append(m_value); m_model.append(m_value);
SASSERT(validate_model());
m_upper = m_weight; m_upper = m_weight;
SASSERT(m_weight < m_max_weight); // SASSERT(m_weight < m_max_weight);
return l_true; return l_true;
} }
} }
} }
bool validate_model() {
for (unsigned i = 0; i < m_T.size(); ++i) {
set const& S = m_T[i];
bool found = false;
for (unsigned j = 0; !found && j < S.size(); ++j) {
found = value(S[j]) == l_true;
}
SASSERT(found);
}
for (unsigned i = 0; i < m_F.size(); ++i) {
set const& S = m_F[i];
bool found = false;
for (unsigned j = 0; !found && j < S.size(); ++j) {
found = value(S[j]) != l_true;
}
CTRACE("opt", !found, display(tout << "not found: " << i << "\n", S););
SASSERT(found);
}
return true;
}
bool resolve_conflict() { bool resolve_conflict() {
while (true) { while (true) {
if (!resolve_conflict_core()) return false; if (!resolve_conflict_core()) return false;
@ -688,7 +741,7 @@ namespace opt {
unsigned r = lvl(conflict_l); unsigned r = lvl(conflict_l);
if (conflict_j.is_clause()) { if (conflict_j.is_clause()) {
unsigned clause = conflict_j.clause(); unsigned clause = conflict_j.clause();
vector<unsigned_vector> const& S = (value(clause) == l_true)?m_F:m_T; vector<unsigned_vector> const& S = conflict_j.pos()?m_T:m_F;
r = std::max(r, lvl(S[clause][0])); r = std::max(r, lvl(S[clause][0]));
r = std::max(r, lvl(S[clause][1])); r = std::max(r, lvl(S[clause][1]));
} }
@ -699,7 +752,7 @@ namespace opt {
SASSERT(inconsistent()); SASSERT(inconsistent());
TRACE("opt", display(tout);); TRACE("opt", display(tout););
unsigned conflict_l = m_conflict_l; unsigned conflict_l = m_conflict_l;
justification conflict_j = m_conflict_j; justification conflict_j(m_conflict_j);
m_conflict_lvl = get_max_lvl(conflict_l, conflict_j); m_conflict_lvl = get_max_lvl(conflict_l, conflict_j);
if (m_conflict_lvl == 0) { if (m_conflict_lvl == 0) {
return false; return false;
@ -710,12 +763,13 @@ namespace opt {
m_lemma.push_back(0); m_lemma.push_back(0);
process_antecedent(conflict_l, num_marks); process_antecedent(conflict_l, num_marks);
do { do {
TRACE("opt", tout << "conflict literal: " << conflict_l << "\n";
display(tout, conflict_j););
if (conflict_j.is_clause()) { if (conflict_j.is_clause()) {
lbool val = value(conflict_l);
unsigned cl = conflict_j.clause(); unsigned cl = conflict_j.clause();
unsigned i = 0; unsigned i = 0;
SASSERT(val != l_undef); SASSERT(value(conflict_l) != l_undef);
set const& T = (val == l_true)?m_T[cl]:m_F[cl]; set const& T = conflict_j.pos()?m_T[cl]:m_F[cl];
if (T[0] == conflict_l) { if (T[0] == conflict_l) {
i = 1; i = 1;
} }
@ -745,6 +799,11 @@ namespace opt {
m_lemma[0] = conflict_l; m_lemma[0] = conflict_l;
unsigned new_scope_lvl = 0; unsigned new_scope_lvl = 0;
TRACE("opt",
for (unsigned i = 0; i < m_lemma.size(); ++i) {
tout << m_lemma[i] << " ";
}
tout << "\n";);
for (unsigned i = 0; i < m_lemma.size(); ++i) { for (unsigned i = 0; i < m_lemma.size(); ++i) {
SASSERT(l_true == value(m_lemma[i])); SASSERT(l_true == value(m_lemma[i]));
new_scope_lvl = std::max(new_scope_lvl, lvl(m_lemma[i])); new_scope_lvl = std::max(new_scope_lvl, lvl(m_lemma[i]));
@ -757,13 +816,14 @@ namespace opt {
void process_antecedent(unsigned antecedent, unsigned& num_marks) { void process_antecedent(unsigned antecedent, unsigned& num_marks) {
unsigned alvl = lvl(antecedent); unsigned alvl = lvl(antecedent);
SASSERT(alvl <= m_conflict_lvl);
if (!is_marked(antecedent) && alvl > 0) { if (!is_marked(antecedent) && alvl > 0) {
mark(antecedent); mark(antecedent);
if (alvl <= m_conflict_lvl && value(antecedent) == l_true) { if (alvl == m_conflict_lvl) {
m_lemma.push_back(antecedent); ++num_marks;
} }
else { else {
++num_marks; m_lemma.push_back(antecedent);
} }
} }
} }
@ -782,8 +842,9 @@ namespace opt {
return idx; return idx;
} }
void set_conflict(unsigned idx, unsigned justification) { void set_conflict(unsigned idx, justification const& justification) {
if (!inconsistent()) { if (!inconsistent()) {
TRACE("opt", tout << "conflict: " << idx << "\n";);
m_inconsistent = true; m_inconsistent = true;
m_conflict_j = justification; m_conflict_j = justification;
m_conflict_l = idx; m_conflict_l = idx;
@ -809,7 +870,7 @@ namespace opt {
else { else {
push(); push();
TRACE("opt", tout << "decide " << idx << "\n";); TRACE("opt", tout << "decide " << idx << "\n";);
assign(idx, l_true, decision); assign(idx, l_true, justification(justification::DECISION));
return true; return true;
} }
} }
@ -830,11 +891,12 @@ namespace opt {
break; break;
} }
} }
prune_branch(); //prune_branch();
} }
void propagate(unsigned idx, lbool good_val, vector<unsigned_vector>& watch, vector<set>& Fs) void propagate(unsigned idx, lbool good_val, vector<unsigned_vector>& watch, vector<set>& Fs)
{ {
TRACE("opt", tout << idx << "\n";);
unsigned sz = watch[idx].size(); unsigned sz = watch[idx].size();
lbool bad_val = ~good_val; lbool bad_val = ~good_val;
unsigned l = 0; unsigned l = 0;
@ -862,11 +924,11 @@ namespace opt {
} }
if (!found) { if (!found) {
if (value(F[k2]) == bad_val) { if (value(F[k2]) == bad_val) {
set_conflict(F[k2], clause_id); set_conflict(F[k2], justification(clause_id, good_val == l_true));
return; return;
} }
SASSERT(value(F[k2]) == l_undef); SASSERT(value(F[k2]) == l_undef);
assign(F[k2], good_val, clause_id); assign(F[k2], good_val, justification(clause_id, good_val == l_true));
watch[idx][l] = watch[idx][i]; watch[idx][l] = watch[idx][i];
} }
} }
@ -878,6 +940,14 @@ namespace opt {
// by using L1, L2, L3 pruning criteria. // by using L1, L2, L3 pruning criteria.
if (m_weight >= m_max_weight) { if (m_weight >= m_max_weight) {
m_inconsistent = true; m_inconsistent = true;
for (unsigned i = m_trail.size(); i > 0; ) {
--i;
if (value(m_trail[i]) == l_true) {
m_conflict_l = m_trail[i];
m_conflict_j = m_justification[m_conflict_l];
break;
}
}
} }
} }

3
src/qe/qe_arith_plugin.cpp
View file

@ -2043,6 +2043,7 @@ public:
// z < d // z < d
expr* z_lt_d = m_util.m_arith.mk_le(z, m_util.m_arith.mk_numeral(d-rational(1), true)); expr* z_lt_d = m_util.m_arith.mk_le(z, m_util.m_arith.mk_numeral(d-rational(1), true));
m_ctx.add_constraint(false, z_lt_d); m_ctx.add_constraint(false, z_lt_d);
TRACE("qe", tout << mk_pp(z_lt_d, m) << "\n";);
// result <- result & z <= d - 1 // result <- result & z <= d - 1
SASSERT(!abs(d).is_one()); SASSERT(!abs(d).is_one());
@ -2056,9 +2057,11 @@ public:
t1 = m_util.mk_sub(x, z); t1 = m_util.mk_sub(x, z);
m_util.mk_divides(d, t1, new_atom); m_util.mk_divides(d, t1, new_atom);
m_ctx.add_constraint(false, new_atom); m_ctx.add_constraint(false, new_atom);
TRACE("qe", tout << mk_pp(new_atom, m) << "\n";);
// (c | ax + t <-> c | az + t) for each divisor. // (c | ax + t <-> c | az + t) for each divisor.
mk_div_equivs(bounds, z, result); mk_div_equivs(bounds, z, result);
TRACE("qe", tout << mk_pp(result, m) << "\n";);
// update x_t to map x |-> dx + z // update x_t to map x |-> dx + z
x_t.set_term(z); x_t.set_term(z);