mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-01-18 12:32:10 +00:00
parent a334020f2c 16552d32cb
commit 81c3a7dabd
7 changed files with 41 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/opt/maxsmt.cpp
View file

@ -55,15 +55,18 @@ namespace opt {
void maxsmt_solver_base::commit_assignment() {
expr_ref tmp(m);
rational k(0);
rational k(0), cost(0);
for (unsigned i = 0; i < m_soft.size(); ++i) {
if (get_assignment(i)) {
k += m_weights[i];
}
else {
cost += m_weights[i];
}
}
pb_util pb(m);
tmp = pb.mk_ge(m_weights.size(), m_weights.c_ptr(), m_soft.c_ptr(), k);
TRACE("opt", tout << tmp << "\n";);
TRACE("opt", tout << "cost: " << cost << "\n" << tmp << "\n";);
s().assert_expr(tmp);
}
@ -140,7 +143,9 @@ namespace opt {
m_wth = s.ensure_wmax_theory();
}
maxsmt_solver_base::scoped_ensure_theory::~scoped_ensure_theory() {
//m_wth->reset_local();
if (m_wth) {
m_wth->reset_local();
}
}
smt::theory_wmaxsat& maxsmt_solver_base::scoped_ensure_theory::operator()() { return *m_wth; }
@ -226,7 +231,9 @@ namespace opt {
m_msolver = 0;
symbol const& maxsat_engine = m_c.maxsat_engine();
IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
TRACE("opt", tout << "maxsmt\n";);
TRACE("opt", tout << "maxsmt\n";
s().display(tout); tout << "\n";
);
if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) {
m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints);
}

7
src/opt/opt_solver.cpp
View file

@ -327,12 +327,7 @@ namespace opt {
SASSERT(idx < get_num_assertions());
return m_context.get_formulas()[idx];
}
std::ostream& opt_solver::display(std::ostream & out) const {
m_context.display(out);
return out;
}
smt::theory_var opt_solver::add_objective(app* term) {
smt::theory_var v = get_optimizer().add_objective(term);
m_objective_vars.push_back(v);

1
src/opt/opt_solver.h
View file

@ -104,7 +104,6 @@ namespace opt {
virtual void set_progress_callback(progress_callback * callback);
virtual unsigned get_num_assertions() const;
virtual expr * get_assertion(unsigned idx) const;
virtual std::ostream& display(std::ostream & out) const;
virtual ast_manager& get_manager() const { return m; }
virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes);
virtual lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores);

1
src/opt/wmax.cpp
View file

@ -64,6 +64,7 @@ namespace opt {
bool was_sat = false;
expr_ref_vector asms(m);
vector<expr_ref_vector> cores;
obj_map<expr, rational>::iterator it = soft.begin(), end = soft.end();
for (; it != end; ++it) {
expr* c = assert_weighted(wth(), it->m_key, it->m_value);

28
src/sat/sat_solver.cpp
View file

@ -3227,20 +3227,32 @@ namespace sat {
SASSERT(!inconsistent());
unsigned sz = m_trail.size();
for (unsigned i = start; i < sz && lvl(m_trail[i]) <= 1; ++i) {
extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq);
if (!extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq)) {
for (i = 0; i < sz && lvl(m_trail[i]) <= 1; ++i) {
VERIFY(extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq));
}
break;
}
}
start = sz;
}
void solver::extract_assumptions(literal lit, index_set& s) {
bool solver::check_domain(literal lit, literal lit2) {
return m_antecedents.contains(lit2.var());
}
bool solver::extract_assumptions(literal lit, index_set& s) {
justification js = m_justification[lit.var()];
switch (js.get_kind()) {
case justification::NONE:
break;
case justification::BINARY:
if (!check_domain(lit, js.get_literal())) return false;
s |= m_antecedents.find(js.get_literal().var());
break;
case justification::TERNARY:
if (!check_domain(lit, js.get_literal1())) return false;
if (!check_domain(lit, js.get_literal2())) return false;
s |= m_antecedents.find(js.get_literal1().var());
s |= m_antecedents.find(js.get_literal2().var());
break;
@ -3248,6 +3260,7 @@ namespace sat {
clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
for (unsigned i = 0; i < c.size(); ++i) {
if (c[i] != lit) {
if (!check_domain(lit, c[i])) return false;
s |= m_antecedents.find(c[i].var());
}
}
@ -3258,6 +3271,7 @@ namespace sat {
literal_vector::iterator it = m_ext_antecedents.begin();
literal_vector::iterator end = m_ext_antecedents.end();
for (; it != end; ++it) {
if (!check_domain(lit, *it)) return false;
s |= m_antecedents.find(it->var());
}
break;
@ -3267,6 +3281,7 @@ namespace sat {
break;
}
TRACE("sat", display_index_set(tout << lit << ": " , s) << "\n";);
return true;
}
std::ostream& solver::display_index_set(std::ostream& out, index_set const& s) const {
@ -3279,17 +3294,19 @@ namespace sat {
}
void solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq) {
bool solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq) {
index_set s;
if (m_antecedents.contains(lit.var())) {
return;
return true;
}
if (assumptions.contains(lit)) {
s.insert(lit.index());
}
else {
if (!extract_assumptions(lit, s)) {
return false;
}
add_assumption(lit);
extract_assumptions(lit, s);
}
m_antecedents.insert(lit.var(), s);
if (unfixed.contains(lit.var())) {
@ -3302,6 +3319,7 @@ namespace sat {
unfixed.remove(lit.var());
conseq.push_back(cons);
}
return true;
}
void solver::asymmetric_branching() {

6
src/sat/sat_solver.h
View file

@ -439,7 +439,9 @@ namespace sat {
u_map<index_set> m_antecedents;
vector<literal_vector> m_binary_clause_graph;
void extract_assumptions(literal lit, index_set& s);
bool extract_assumptions(literal lit, index_set& s);
bool check_domain(literal lit, literal lit2);
std::ostream& display_index_set(std::ostream& out, index_set const& s) const;
@ -451,7 +453,7 @@ namespace sat {
void extract_fixed_consequences(unsigned& start, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
void extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
bool extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
void update_unfixed_literals(literal_set& unfixed_lits, bool_var_set& unfixed_vars);

1
src/smt/smt_context.cpp
View file

@ -1795,6 +1795,7 @@ namespace smt {
void context::set_conflict(b_justification js, literal not_l) {
if (!inconsistent()) {
TRACE("set_conflict", display_literal_verbose(tout, not_l); display(tout, js); );
m_conflict = js;
m_not_l = not_l;
}