diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index dd689dcb0..123d84ee5 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -291,10 +291,10 @@ extern "C" { } } else { - model_ref _m; - m_solver.get()->get_model(_m); + model_ref mr; + m_solver.get()->get_model(mr); Z3_model_ref *crap = alloc(Z3_model_ref); - crap->m_model = _m.get(); + crap->m_model = mr.get(); mk_c(c)->save_object(crap); *model = of_model(crap); } diff --git a/src/math/simplex/simplex.h b/src/math/simplex/simplex.h index 9685af589..d1d6320fc 100644 --- a/src/math/simplex/simplex.h +++ b/src/math/simplex/simplex.h @@ -141,7 +141,7 @@ namespace simplex { void unset_upper(var_t var); void set_value(var_t var, eps_numeral const& b); void set_cancel(bool f) { m_cancel = f; } - void set_max_iterations(unsigned m) { m_max_iterations = m; } + void set_max_iterations(unsigned n) { m_max_iterations = n; } void reset(); lbool make_feasible(); lbool minimize(var_t var); diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h index 80454a52c..ee28e1475 100644 --- a/src/math/simplex/sparse_matrix.h +++ b/src/math/simplex/sparse_matrix.h @@ -100,7 +100,7 @@ namespace simplex { _row_entry & add_row_entry(unsigned & pos_idx); void del_row_entry(unsigned idx); void compress(manager& m, vector & cols); - void compress_if_needed(manager& m, vector & cols); + void compress_if_needed(manager& _m, vector & cols); void save_var_pos(svector & result_map, unsigned_vector& idxs) const; //bool is_coeff_of(var_t v, numeral const & expected) const; int get_idx_of(var_t v) const; @@ -143,7 +143,7 @@ namespace simplex { public: - sparse_matrix(manager& m): m(m) {} + sparse_matrix(manager& _m): m(_m) {} ~sparse_matrix(); void reset(); diff --git a/src/opt/inc_sat_solver.cpp b/src/opt/inc_sat_solver.cpp index 65264e0d9..0dfb0aa5e 100644 --- a/src/opt/inc_sat_solver.cpp +++ b/src/opt/inc_sat_solver.cpp @@ -190,11 +190,11 @@ public: r.reset(); r.append(m_core.size(), m_core.c_ptr()); } - virtual void get_model(model_ref & m) { + virtual void get_model(model_ref & mdl) { if (!m_model.get()) { extract_model(); } - m = m_model; + mdl = m_model; } virtual proof * get_proof() { UNREACHABLE(); @@ -331,10 +331,10 @@ private: } sat::literal_vector const& core = m_solver.get_core(); TRACE("opt", - dep2asm_t::iterator it = dep2asm.begin(); - dep2asm_t::iterator end = dep2asm.end(); - for (; it != end; ++it) { - tout << mk_pp(it->m_key, m) << " |-> " << sat::literal(it->m_value) << "\n"; + dep2asm_t::iterator it2 = dep2asm.begin(); + dep2asm_t::iterator end2 = dep2asm.end(); + for (; it2 != end2; ++it2) { + tout << mk_pp(it2->m_key, m) << " |-> " << sat::literal(it2->m_value) << "\n"; } tout << "core: "; for (unsigned i = 0; i < core.size(); ++i) { diff --git a/src/opt/mus.cpp b/src/opt/mus.cpp index 0cf9786b2..f9190911a 100644 --- a/src/opt/mus.cpp +++ b/src/opt/mus.cpp @@ -58,7 +58,8 @@ struct mus::imp { unsigned idx = m_cls2expr.size(); m_expr2cls.insert(cls, idx); m_cls2expr.push_back(cls); - TRACE("opt", tout << idx << ": " << mk_pp(cls, m) << "\n";); + TRACE("opt", tout << idx << ": " << mk_pp(cls, m) << "\n"; + display_vec(tout, m_cls2expr);); return idx; } @@ -113,6 +114,11 @@ struct mus::imp { core.push_back(cls_id); } } + TRACE("opt", display_vec(tout << "core exprs:", core_exprs); + display_vec(tout << "core:", core); + display_vec(tout << "mus:", mus); + ); + } break; } @@ -144,6 +150,21 @@ struct mus::imp { out << "\n"; } + void display_vec(std::ostream& out, expr_ref_vector const& v) const { + for (unsigned i = 0; i < v.size(); ++i) { + out << mk_pp(v[i], m) << " "; + } + out << "\n"; + } + + + void display_vec(std::ostream& out, ptr_vector const& v) const { + for (unsigned i = 0; i < v.size(); ++i) { + out << mk_pp(v[i], m) << " "; + } + out << "\n"; + } + void set_soft(unsigned sz, expr* const* soft, rational const* weights) { m_model.reset(); m_weight.reset(); diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index ee4ce467a..2284f427b 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -146,9 +146,9 @@ namespace opt { virtual void cancel() { set_cancel(true); } virtual void set_hard_constraints(ptr_vector & hard); virtual lbool optimize(); - virtual void get_model(model_ref& m); - virtual void set_model(model_ref& m); - virtual void fix_model(model_ref& m); + virtual void get_model(model_ref& _m); + virtual void set_model(model_ref& _m); + virtual void fix_model(model_ref& _m); virtual void collect_statistics(statistics& stats) const; virtual proof* get_proof() { return 0; } virtual void get_labels(svector & r) {} @@ -186,7 +186,7 @@ namespace opt { void set_enable_sls(bool f) { m_enable_sls = f; } void set_soft_assumptions(); symbol const& maxsat_engine() const { return m_maxsat_engine; } - void get_base_model(model_ref& m); + void get_base_model(model_ref& _m); private: diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 986136d7b..f9702705f 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -94,7 +94,7 @@ namespace opt { virtual void pop_core(unsigned n); virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions); virtual void get_unsat_core(ptr_vector & r); - virtual void get_model(model_ref & m); + virtual void get_model(model_ref & _m); virtual proof * get_proof(); virtual std::string reason_unknown() const; virtual void get_labels(svector & r); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 6a5148192..1a089977a 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -923,9 +923,28 @@ namespace sat { m_assumption_set.insert(lit); if (m_config.m_soft_assumptions) { - if (value(lit) == l_undef) { + switch(value(lit)) { + case l_undef: m_assumptions.push_back(lit); assign(lit, justification()); + break; + case l_false: { + set_conflict(lit); + flet _min1(m_config.m_minimize_core, false); + flet _min2(m_config.m_minimize_core_partial, false); + resolve_conflict_for_unsat_core(); + SASSERT(m_core.size() <= m_assumptions.size()); + if (m_core.size() <= 3 || + m_core.size() <= i - m_assumptions.size() + 1) { + return; + } + else { + m_inconsistent = false; + } + break; + } + case l_true: + break; } propagate(false); } diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index ec62efa1c..1e5b4b81f 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -370,7 +370,12 @@ namespace smt { tout << "conflict_lvl: " << m_conflict_lvl << " scope_lvl: " << m_ctx.get_scope_level() << " base_lvl: " << m_ctx.get_base_level() << " search_lvl: " << m_ctx.get_search_level() << "\n"; tout << "js.kind: " << js.get_kind() << "\n"; - m_ctx.display_literal(tout, consequent); tout << "\n";); + tout << "consequent: " << consequent << "\n"; + for (unsigned i = 0; i < m_assigned_literals.size(); ++i) { + tout << m_assigned_literals[i] << " "; + } + tout << "\n"; + ); // m_conflict_lvl can be smaller than m_ctx.get_search_level() when: // there are user level scopes created using the Z3 API, and @@ -1310,8 +1315,11 @@ namespace smt { } void conflict_resolution::process_antecedent_for_unsat_core(literal antecedent) { - TRACE("conflict", tout << "processing antecedent: "; m_ctx.display_literal(tout, antecedent); tout << "\n";); bool_var var = antecedent.var(); + TRACE("conflict", tout << "processing antecedent: "; + m_ctx.display_literal_info(tout << antecedent << " ", antecedent); + tout << (m_ctx.is_marked(var)?"marked":"not marked"); + tout << "\n";); if (!m_ctx.is_marked(var)) { m_ctx.set_mark(var); @@ -1341,13 +1349,14 @@ namespace smt { b_justification js = conflict; literal consequent = false_literal; - if (not_l != null_literal) + if (not_l != null_literal) { consequent = ~not_l; + } int idx = skip_literals_above_conflict_level(); if (not_l != null_literal) - process_antecedent_for_unsat_core(not_l); + process_antecedent_for_unsat_core(consequent); if (m_assigned_literals.empty()) { goto end_unsat_core; diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 305e84518..3dca6a70b 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -103,9 +103,9 @@ namespace smt { void context::display_literal_info(std::ostream & out, literal l) const { l.display_compact(out, m_bool_var2expr.c_ptr()); if (l.sign()) - out << " (not " << mk_bounded_pp(bool_var2expr(l.var()), m_manager, 10) << ")\n"; + out << " (not " << mk_bounded_pp(bool_var2expr(l.var()), m_manager, 10) << ") "; else - out << " " << mk_bounded_pp(bool_var2expr(l.var()), m_manager, 10) << "\n"; + out << " " << mk_bounded_pp(bool_var2expr(l.var()), m_manager, 10) << " "; out << "relevant: " << is_relevant(bool_var2expr(l.var())) << ", val: " << get_assignment(l) << "\n"; } diff --git a/src/tactic/horn_subsume_model_converter.h b/src/tactic/horn_subsume_model_converter.h index 993f29cc9..8bad28e3d 100644 --- a/src/tactic/horn_subsume_model_converter.h +++ b/src/tactic/horn_subsume_model_converter.h @@ -72,7 +72,7 @@ public: void insert(func_decl* p, expr* body) { m_funcs.push_back(p); m_bodies.push_back(body); } - virtual void operator()(model_ref& m); + virtual void operator()(model_ref& _m); virtual model_converter * translate(ast_translation & translator); diff --git a/src/tactic/replace_proof_converter.h b/src/tactic/replace_proof_converter.h index cb97810f8..7fee27612 100644 --- a/src/tactic/replace_proof_converter.h +++ b/src/tactic/replace_proof_converter.h @@ -30,11 +30,11 @@ class replace_proof_converter : public proof_converter { proof_ref_vector m_proofs; public: - replace_proof_converter(ast_manager& m): m(m), m_proofs(m) {} + replace_proof_converter(ast_manager& _m): m(_m), m_proofs(m) {} virtual ~replace_proof_converter() {} - virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result); + virtual void operator()(ast_manager & _m, unsigned num_source, proof * const * source, proof_ref & result); virtual proof_converter * translate(ast_translation & translator); diff --git a/src/util/dependency.h b/src/util/dependency.h index 6ce9b2025..33a0e4d22 100644 --- a/src/util/dependency.h +++ b/src/util/dependency.h @@ -171,7 +171,7 @@ public: m_todo.push_back(d); unsigned qhead = 0; while (qhead < m_todo.size()) { - dependency * d = m_todo[qhead]; + d = m_todo[qhead]; qhead++; if (d->is_leaf()) { if (to_leaf(d)->m_value == v) { @@ -201,7 +201,7 @@ public: m_todo.push_back(d); unsigned qhead = 0; while (qhead < m_todo.size()) { - dependency * d = m_todo[qhead]; + d = m_todo[qhead]; qhead++; if (d->is_leaf()) { vs.push_back(to_leaf(d)->m_value); diff --git a/src/util/mpf.h b/src/util/mpf.h index 83646f9f3..ba4f237bd 100644 --- a/src/util/mpf.h +++ b/src/util/mpf.h @@ -46,7 +46,7 @@ class mpf { mpz significand; mpf_exp_t exponent; mpf & operator=(mpf const & other) { UNREACHABLE(); return *this; } - void set(unsigned ebits, unsigned sbits); + void set(unsigned _ebits, unsigned _sbits); public: mpf(); mpf(unsigned ebits, unsigned sbits);