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

fix partial model tracking over cancellation/exceptions, reported by August Shi. Fix regression test for fp-to-real, reset the pre-processor in inc_sat_solver on exceptions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-03-07 16:42:29 -08:00
parent 4cd1efc50e
commit 5994c5a948
19 changed files with 239 additions and 193 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/cmd_context/cmd_context.cpp
View file

@ -1454,6 +1454,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
throw ex;
}
catch (z3_exception & ex) {
get_opt()->display_assignment(regular_stream());
throw cmd_exception(ex.msg());
}
if (was_pareto && r == l_false) {

3
src/opt/bcd2.cpp
View file

@ -233,8 +233,7 @@ namespace opt {
new_assignment.reset();
s().get_model(model);
for (unsigned i = 0; i < m_soft.size(); ++i) {
VERIFY(model->eval(m_soft[i], val));
new_assignment.push_back(m.is_true(val));
new_assignment.push_back(model->eval(m_soft[i], val) && m.is_true(val));
if (!new_assignment[i]) {
new_upper += m_weights[i];
}

2
src/opt/fu_malik.cpp
View file

@ -204,7 +204,7 @@ namespace opt {
m_assignment.reset();
for (unsigned i = 0; i < m_soft.size(); ++i) {
expr_ref val(m);
VERIFY(m_model->eval(m_soft[i], val));
if (!m_model->eval(m_soft[i], val)) return l_undef;
TRACE("opt", tout << val << "\n";);
m_assignment.push_back(m.is_true(val));
}

3
src/opt/maxhs.cpp
View file

@ -530,8 +530,7 @@ namespace opt {
bool is_true(model_ref& mdl, expr* e) {
expr_ref val(m);
VERIFY(mdl->eval(e, val));
return m.is_true(val);
return mdl->eval(e, val) && m.is_true(val);
}
bool is_active(unsigned i) const {

38
src/opt/maxres.cpp
View file

@ -82,6 +82,7 @@ private:
memset(this, 0, sizeof(*this));
}
};
unsigned m_index;
stats m_stats;
expr_ref_vector m_B;
expr_ref_vector m_asms;
@ -112,10 +113,11 @@ private:
typedef ptr_vector<expr> exprs;
public:
maxres(maxsat_context& c,
maxres(maxsat_context& c, unsigned index,
weights_t& ws, expr_ref_vector const& soft,
strategy_t st):
maxsmt_solver_base(c, ws, soft),
m_index(index),
m_B(m), m_asms(m), m_defs(m),
m_mus(c.get_solver(), m),
m_mss(c.get_solver(), m),
@ -189,7 +191,7 @@ public:
lbool mus_solver() {
lbool is_sat = l_true;
init();
if (!init()) return l_undef;
init_local();
trace();
while (m_lower < m_upper) {
@ -227,7 +229,7 @@ public:
}
lbool primal_dual_solver() {
init();
if (!init()) return l_undef;
init_local();
trace();
exprs cs;
@ -483,8 +485,9 @@ public:
if (m_csmodel) {
expr_ref val(m);
SASSERT(m_csmodel.get());
VERIFY(m_csmodel->eval(value, val));
m_csmodel->register_decl(to_app(def)->get_decl(), val);
if (m_csmodel->eval(value, val, true)) {
m_csmodel->register_decl(to_app(def)->get_decl(), val);
}
}
}
@ -724,17 +727,26 @@ public:
if (upper >= m_upper) {
return;
}
if (!m_c.verify_model(m_index, mdl, upper)) {
return;
}
m_model = mdl;
for (unsigned i = 0; i < m_soft.size(); ++i) {
m_assignment[i] = is_true(m_soft[i]);
}
DEBUG_CODE(verify_assignment(););
m_upper = upper;
trace();
add_upper_bound_block();
}
void add_upper_bound_block() {
@ -751,14 +763,12 @@ public:
bool is_true(model* mdl, expr* e) {
expr_ref tmp(m);
VERIFY(mdl->eval(e, tmp));
return m.is_true(tmp);
return mdl->eval(e, tmp, true) && m.is_true(tmp);
}
bool is_false(model* mdl, expr* e) {
expr_ref tmp(m);
VERIFY(mdl->eval(e, tmp));
return m.is_false(tmp);
return mdl->eval(e, tmp, true) && m.is_false(tmp);
}
bool is_true(expr* e) {
@ -870,12 +880,12 @@ public:
};
opt::maxsmt_solver_base* opt::mk_maxres(
maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) {
return alloc(maxres, c, ws, soft, maxres::s_primal);
maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft) {
return alloc(maxres, c, id, ws, soft, maxres::s_primal);
}
opt::maxsmt_solver_base* opt::mk_primal_dual_maxres(
maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) {
return alloc(maxres, c, ws, soft, maxres::s_primal_dual);
maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft) {
return alloc(maxres, c, id, ws, soft, maxres::s_primal_dual);
}

4
src/opt/maxres.h
View file

@ -22,9 +22,9 @@ Notes:
namespace opt {
maxsmt_solver_base* mk_maxres(maxsat_context& c, weights_t & ws, expr_ref_vector const& soft);
maxsmt_solver_base* mk_maxres(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft);
maxsmt_solver_base* mk_primal_dual_maxres(maxsat_context& c, weights_t & ws, expr_ref_vector const& soft);
maxsmt_solver_base* mk_primal_dual_maxres(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft);
};

34
src/opt/maxsmt.cpp
View file

@ -69,13 +69,13 @@ namespace opt {
s().assert_expr(tmp);
}
void maxsmt_solver_base::init() {
bool maxsmt_solver_base::init() {
m_lower.reset();
m_upper.reset();
m_assignment.reset();
for (unsigned i = 0; i < m_weights.size(); ++i) {
expr_ref val(m);
VERIFY(m_model->eval(m_soft[i], val));
if (!m_model->eval(m_soft[i], val)) return false;
m_assignment.push_back(m.is_true(val));
if (!m_assignment.back()) {
m_upper += m_weights[i];
@ -88,6 +88,7 @@ namespace opt {
tout << (m_assignment[i]?"T":"F");
}
tout << "\n";);
return true;
}
void maxsmt_solver_base::set_mus(bool f) {
@ -137,7 +138,8 @@ namespace opt {
//m_wth->reset_local();
}
smt::theory_wmaxsat& maxsmt_solver_base::scoped_ensure_theory::operator()() { return *m_wth; }
void maxsmt_solver_base::trace_bounds(char const * solver) {
IF_VERBOSE(1,
rational l = m_adjust_value(m_lower);
@ -148,8 +150,8 @@ namespace opt {
maxsmt::maxsmt(maxsat_context& c):
m(c.get_manager()), m_c(c),
maxsmt::maxsmt(maxsat_context& c, unsigned index):
m(c.get_manager()), m_c(c), m_index(index),
m_soft_constraints(m), m_answer(m) {}
lbool maxsmt::operator()() {
@ -159,10 +161,10 @@ namespace opt {
IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
TRACE("opt", tout << "maxsmt\n";);
if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres")) {
m_msolver = mk_maxres(m_c, m_weights, m_soft_constraints);
m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints);
}
else if (maxsat_engine == symbol("pd-maxres")) {
m_msolver = mk_primal_dual_maxres(m_c, m_weights, m_soft_constraints);
m_msolver = mk_primal_dual_maxres(m_c, m_index, m_weights, m_soft_constraints);
}
else if (maxsat_engine == symbol("bcd2")) {
m_msolver = mk_bcd2(m_c, m_weights, m_soft_constraints);
@ -188,7 +190,13 @@ namespace opt {
if (m_msolver) {
m_msolver->updt_params(m_params);
m_msolver->set_adjust_value(m_adjust_value);
is_sat = (*m_msolver)();
is_sat = l_undef;
try {
is_sat = (*m_msolver)();
}
catch (z3_exception&) {
is_sat = l_undef;
}
if (is_sat != l_false) {
m_msolver->get_model(m_model, m_labels);
}
@ -205,6 +213,14 @@ namespace opt {
return is_sat;
}
void maxsmt::set_adjust_value(adjust_value& adj) {
m_adjust_value = adj;
if (m_msolver) {
m_msolver->set_adjust_value(m_adjust_value);
}
}
void maxsmt::verify_assignment() {
// TBD: have to use a different solver
// because we don't push local scope any longer.
@ -233,7 +249,7 @@ namespace opt {
rational r = m_upper;
if (m_msolver) {
rational q = m_msolver->get_upper();
if (q < r) r = q;
if (q < r) r = q;
}
return m_adjust_value(r);
}

7
src/opt/maxsmt.h
View file

@ -82,7 +82,7 @@ namespace opt {
void set_model() { s().get_model(m_model); s().get_labels(m_labels); }
virtual void updt_params(params_ref& p);
solver& s();
void init();
bool init();
void set_mus(bool f);
app* mk_fresh_bool(char const* name);
@ -111,6 +111,7 @@ namespace opt {
class maxsmt {
ast_manager& m;
maxsat_context& m_c;
unsigned m_index;
scoped_ptr<maxsmt_solver_base> m_msolver;
expr_ref_vector m_soft_constraints;
expr_ref_vector m_answer;
@ -122,11 +123,11 @@ namespace opt {
svector<symbol> m_labels;
params_ref m_params;
public:
maxsmt(maxsat_context& c);
maxsmt(maxsat_context& c, unsigned id);
lbool operator()();
void updt_params(params_ref& p);
void add(expr* f, rational const& w);
void set_adjust_value(adjust_value& adj) { m_adjust_value = adj; }
void set_adjust_value(adjust_value& adj);
unsigned size() const { return m_soft_constraints.size(); }
expr* operator[](unsigned idx) const { return m_soft_constraints[idx]; }
rational weight(unsigned idx) const { return m_weights[idx]; }

11
src/opt/mss.cpp
View file

@ -73,8 +73,7 @@ namespace opt {
expr* n = core[j];
if (!core_lits.contains(n)) {
core_lits.insert(n);
VERIFY(m_model->eval(n, tmp));
if (m.is_true(tmp)) {
if (m_model->eval(n, tmp) && m.is_true(tmp)) {
add_mss(n);
}
else {
@ -86,8 +85,7 @@ namespace opt {
for (unsigned i = 0; i < literals.size(); ++i) {
expr* n = literals[i];
if (!core_lits.contains(n)) {
VERIFY(m_model->eval(n, tmp));
if (m.is_true(tmp)) {
if (m_model->eval(n, tmp) && m.is_true(tmp)) {
m_mss.push_back(n);
}
else {
@ -130,8 +128,7 @@ namespace opt {
if (m_mcs.contains(n)) {
continue; // remove from cores.
}
VERIFY(m_model->eval(n, tmp));
if (m.is_true(tmp)) {
if (m_model->eval(n, tmp) && m.is_true(tmp)) {
add_mss(n);
}
else {
@ -275,7 +272,7 @@ namespace opt {
expr_ref tmp(m);
for (unsigned i = 0; i < m_mss.size(); ++i) {
expr* n = m_mss[i];
VERIFY(m_model->eval(n, tmp));
if (!m_model->eval(n, tmp)) return true;
CTRACE("opt", !m.is_true(tmp), tout << mk_pp(n, m) << " |-> " << mk_pp(tmp, m) << "\n";);
SASSERT(!m.is_false(tmp));
}

80
src/opt/opt_context.cpp
View file

@ -203,7 +203,7 @@ namespace opt {
objective& obj = s.m_objectives[i];
m_objectives.push_back(obj);
if (obj.m_type == O_MAXSMT) {
add_maxsmt(obj.m_id);
add_maxsmt(obj.m_id, i);
}
}
m_hard_constraints.append(s.m_hard);
@ -311,7 +311,9 @@ namespace opt {
maxsmt& ms = *m_maxsmts.find(id);
if (scoped) get_solver().push();
lbool result = ms();
if (result != l_false && (ms.get_model(tmp, m_labels), tmp.get())) ms.get_model(m_model, m_labels);
if (result != l_false && (ms.get_model(tmp, m_labels), tmp.get())) {
ms.get_model(m_model, m_labels);
}
if (scoped) get_solver().pop(1);
if (result == l_true && committed) ms.commit_assignment();
return result;
@ -414,12 +416,16 @@ namespace opt {
case O_MINIMIZE:
is_ge = !is_ge;
case O_MAXIMIZE:
VERIFY(mdl->eval(obj.m_term, val) && is_numeral(val, k));
if (is_ge) {
result = mk_ge(obj.m_term, val);
if (mdl->eval(obj.m_term, val) && is_numeral(val, k)) {
if (is_ge) {
result = mk_ge(obj.m_term, val);
}
else {
result = mk_ge(val, obj.m_term);
}
}
else {
result = mk_ge(val, obj.m_term);
result = m.mk_true();
}
break;
case O_MAXSMT: {
@ -430,8 +436,7 @@ namespace opt {
for (unsigned i = 0; i < sz; ++i) {
terms.push_back(obj.m_terms[i]);
coeffs.push_back(obj.m_weights[i]);
VERIFY(mdl->eval(obj.m_terms[i], val));
if (m.is_true(val)) {
if (mdl->eval(obj.m_terms[i], val) && m.is_true(val)) {
k += obj.m_weights[i];
}
}
@ -469,8 +474,7 @@ namespace opt {
update_bound(false);
}
lbool context::execute_pareto() {
lbool context::execute_pareto() {
if (!m_pareto) {
set_pareto(alloc(gia_pareto, m, *this, m_solver.get(), m_params));
}
@ -642,8 +646,8 @@ namespace opt {
}
void context::add_maxsmt(symbol const& id) {
maxsmt* ms = alloc(maxsmt, *this);
void context::add_maxsmt(symbol const& id, unsigned index) {
maxsmt* ms = alloc(maxsmt, *this, index);
ms->updt_params(m_params);
#pragma omp critical (opt_context)
{
@ -708,7 +712,7 @@ namespace opt {
}
}
bool context::is_maximize(expr* fml, app_ref& term, expr*& orig_term, unsigned& index) {
bool context::is_maximize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index) {
if (is_app(fml) && m_objective_fns.find(to_app(fml)->get_decl(), index) &&
m_objectives[index].m_type == O_MAXIMIZE) {
term = to_app(to_app(fml)->get_arg(0));
@ -718,7 +722,7 @@ namespace opt {
return false;
}
bool context::is_minimize(expr* fml, app_ref& term, expr*& orig_term, unsigned& index) {
bool context::is_minimize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index) {
if (is_app(fml) && m_objective_fns.find(to_app(fml)->get_decl(), index) &&
m_objectives[index].m_type == O_MINIMIZE) {
term = to_app(to_app(fml)->get_arg(0));
@ -730,7 +734,7 @@ namespace opt {
bool context::is_maxsat(expr* fml, expr_ref_vector& terms,
vector<rational>& weights, rational& offset,
bool& neg, symbol& id, unsigned& index) {
bool& neg, symbol& id, expr_ref& orig_term, unsigned& index) {
if (!is_app(fml)) return false;
neg = false;
app* a = to_app(fml);
@ -752,7 +756,6 @@ namespace opt {
return true;
}
app_ref term(m);
expr* orig_term;
offset = rational::zero();
bool is_max = is_maximize(fml, term, orig_term, index);
bool is_min = !is_max && is_minimize(fml, term, orig_term, index);
@ -773,7 +776,7 @@ namespace opt {
}
}
TRACE("opt",
tout << "Convert minimization " << mk_pp(orig_term, m) << "\n";
tout << "Convert minimization " << orig_term << "\n";
tout << "to maxsat: " << term << "\n";
for (unsigned i = 0; i < weights.size(); ++i) {
tout << mk_pp(terms[i].get(), m) << ": " << weights[i] << "\n";
@ -781,7 +784,7 @@ namespace opt {
tout << "offset: " << offset << "\n";
);
std::ostringstream out;
out << mk_pp(orig_term, m) << ":" << index;
out << orig_term << ":" << index;
id = symbol(out.str().c_str());
return true;
}
@ -804,7 +807,7 @@ namespace opt {
}
neg = true;
std::ostringstream out;
out << mk_pp(orig_term, m) << ":" << index;
out << orig_term << ":" << index;
id = symbol(out.str().c_str());
return true;
}
@ -823,7 +826,7 @@ namespace opt {
}
neg = is_max;
std::ostringstream out;
out << mk_pp(orig_term, m) << ":" << index;
out << orig_term << ":" << index;
id = symbol(out.str().c_str());
return true;
}
@ -871,7 +874,7 @@ namespace opt {
tout << mk_pp(fmls[i], m) << "\n";
});
m_hard_constraints.reset();
expr* orig_term;
expr_ref orig_term(m);
for (unsigned i = 0; i < fmls.size(); ++i) {
expr* fml = fmls[i];
app_ref tr(m);
@ -881,7 +884,7 @@ namespace opt {
unsigned index;
symbol id;
bool neg;
if (is_maxsat(fml, terms, weights, offset, neg, id, index)) {
if (is_maxsat(fml, terms, weights, offset, neg, id, orig_term, index)) {
objective& obj = m_objectives[index];
if (obj.m_type != O_MAXSMT) {
@ -889,10 +892,11 @@ namespace opt {
obj.m_id = id;
obj.m_type = O_MAXSMT;
SASSERT(!m_maxsmts.contains(id));
add_maxsmt(id);
add_maxsmt(id, index);
}
mk_atomic(terms);
SASSERT(obj.m_id == id);
obj.m_term = to_app(orig_term);
obj.m_terms.reset();
obj.m_terms.append(terms);
obj.m_weights.reset();
@ -933,6 +937,32 @@ namespace opt {
}
}
bool context::verify_model(unsigned index, model* md, rational const& _v) {
rational r;
app_ref term = m_objectives[index].m_term;
rational v = m_objectives[index].m_adjust_value(_v);
expr_ref val(m);
model_ref mdl = md;
fix_model(mdl);
if (!mdl->eval(term, val)) {
TRACE("opt", tout << "Term does not evaluate " << term << "\n";);
return false;
}
if (!m_arith.is_numeral(val, r)) {
TRACE("opt", tout << "model does not evaluate objective to a value\n";);
return false;
}
if (r != v) {
TRACE("opt", tout << "Out of bounds: " << term << " " << val << " != " << v << "\n";);
return false;
}
else {
TRACE("opt", tout << "validated: " << term << " = " << val << "\n";);
}
return true;
}
void context::purify(app_ref& term) {
filter_model_converter_ref fm;
if (m_arith.is_add(term)) {
@ -1395,8 +1425,8 @@ namespace opt {
case O_MAXSMT: {
rational value(0);
for (unsigned i = 0; i < obj.m_terms.size(); ++i) {
VERIFY(m_model->eval(obj.m_terms[i], val));
if (!m.is_true(val)) {
bool evaluated = m_model->eval(obj.m_terms[i], val);
if (evaluated && !m.is_true(val)) {
value += obj.m_weights[i];
}
// TBD: check that optimal was not changed.

14
src/opt/opt_context.h
View file

@ -55,6 +55,8 @@ namespace opt {
virtual void get_base_model(model_ref& _m) = 0; // retrieve model from initial satisfiability call.
virtual smt::context& smt_context() = 0; // access SMT context for SMT based MaxSMT solver (wmax requires SMT core)
virtual unsigned num_objectives() = 0;
virtual bool verify_model(unsigned id, model* mdl, rational const& v) = 0;
virtual void set_model(model_ref& _m) = 0;
};
/**
@ -132,6 +134,7 @@ namespace opt {
bool set(ptr_vector<expr> & hard);
unsigned add(expr* soft, rational const& weight, symbol const& id);
unsigned add(app* obj, bool is_max);
unsigned get_index(symbol const& id) { return m_indices[id]; }
};
ast_manager& m;
@ -178,6 +181,7 @@ namespace opt {
virtual void set_hard_constraints(ptr_vector<expr> & hard);
virtual lbool optimize();
virtual bool print_model() const;
virtual void set_model(model_ref& _m) { m_model = _m; }
virtual void get_model(model_ref& _m);
virtual void fix_model(model_ref& _m);
virtual void collect_statistics(statistics& stats) const;
@ -219,6 +223,8 @@ namespace opt {
virtual void get_base_model(model_ref& _m);
virtual bool verify_model(unsigned id, model* mdl, rational const& v);
private:
void validate_feasibility(maxsmt& ms);
@ -236,11 +242,11 @@ namespace opt {
void import_scoped_state();
void normalize();
void internalize();
bool is_maximize(expr* fml, app_ref& term, expr*& orig_term, unsigned& index);
bool is_minimize(expr* fml, app_ref& term, expr*& orig_term, unsigned& index);
bool is_maximize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index);
bool is_minimize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index);
bool is_maxsat(expr* fml, expr_ref_vector& terms,
vector<rational>& weights, rational& offset, bool& neg,
symbol& id, unsigned& index);
symbol& id, expr_ref& orig_term, unsigned& index);
void purify(app_ref& term);
app* purify(filter_model_converter_ref& fm, expr* e);
bool is_mul_const(expr* e);
@ -269,7 +275,7 @@ namespace opt {
void init_solver();
void update_solver();
void setup_arith_solver();
void add_maxsmt(symbol const& id);
void add_maxsmt(symbol const& id, unsigned index);
void set_simplify(tactic *simplify);
void set_pareto(pareto_base* p);
void clear_state();

3
src/opt/optsmt.cpp
View file

@ -156,8 +156,7 @@ namespace opt {
m_s->get_labels(m_labels);
for (unsigned i = 0; i < ors.size(); ++i) {
expr_ref tmp(m);
m_model->eval(ors[i].get(), tmp);
if (m.is_true(tmp)) {
if (m_model->eval(ors[i].get(), tmp) && m.is_true(tmp)) {
m_lower[i] = m_upper[i];
ors[i] = m.mk_false();
disj[i] = m.mk_false();

10
src/opt/pb_sls.cpp
View file

@ -139,8 +139,7 @@ namespace smt {
m_orig_model = mdl;
for (unsigned i = 0; i < m_var2decl.size(); ++i) {
expr_ref tmp(m);
VERIFY(mdl->eval(m_var2decl[i], tmp));
m_assignment[i] = m.is_true(tmp);
m_assignment[i] = mdl->eval(m_var2decl[i], tmp) && m.is_true(tmp);
}
}
@ -305,7 +304,9 @@ namespace smt {
if (!eval(m_clauses[i])) {
m_hard_false.insert(i);
expr_ref tmp(m);
VERIFY(m_orig_model->eval(m_orig_clauses[i].get(), tmp));
if (!m_orig_model->eval(m_orig_clauses[i].get(), tmp)) {
return;
}
IF_VERBOSE(0,
verbose_stream() << "original evaluation: " << tmp << "\n";
verbose_stream() << mk_pp(m_orig_clauses[i].get(), m) << "\n";
@ -487,8 +488,7 @@ namespace smt {
SASSERT(m_soft_occ.size() == var);
m_hard_occ.push_back(unsigned_vector());
m_soft_occ.push_back(unsigned_vector());
VERIFY(m_orig_model->eval(f, tmp));
m_assignment.push_back(m.is_true(tmp));
m_assignment.push_back(m_orig_model->eval(f, tmp) && m.is_true(tmp));
m_decl2var.insert(f, var);
m_var2decl.push_back(f);
}

4
src/sat/sat_mus.cpp
View file

@ -97,7 +97,7 @@ namespace sat {
break;
}
if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
IF_VERBOSE(1, verbose_stream() << "restart budget exceeded\n";);
IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";);
set_core();
return l_true;
}
@ -173,7 +173,7 @@ namespace sat {
lbool mus::qx(literal_set& assignment, literal_set& support, bool has_support) {
lbool is_sat = l_true;
if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
IF_VERBOSE(1, verbose_stream() << "restart budget exceeded\n";);
IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";);
return l_true;
}
if (has_support) {

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

@ -50,14 +50,14 @@ class inc_sat_solver : public solver {
expr_ref_vector m_core;
atom2bool_var m_map;
model_ref m_model;
model_converter_ref m_mc;
bit_blaster_rewriter m_bb_rewriter;
scoped_ptr<bit_blaster_rewriter> m_bb_rewriter;
tactic_ref m_preprocess;
unsigned m_num_scopes;
sat::literal_vector m_asms;
goal_ref_buffer m_subgoals;
proof_converter_ref m_pc;
model_converter_ref m_mc2;
model_converter_ref m_mc;
model_converter_ref m_mc0;
expr_dependency_ref m_dep_core;
svector<double> m_weights;
std::string m_unknown;
@ -72,29 +72,13 @@ public:
m_asmsf(m),
m_fmls_head(0),
m_core(m),
m_map(m),
m_bb_rewriter(m, p),
m_map(m),
m_num_scopes(0),
m_dep_core(m),
m_unknown("no reason given") {
m_params.set_bool("elim_vars", false);
m_solver.updt_params(m_params);
params_ref simp2_p = p;
simp2_p.set_bool("som", true);
simp2_p.set_bool("pull_cheap_ite", true);
simp2_p.set_bool("push_ite_bv", false);
simp2_p.set_bool("local_ctx", true);
simp2_p.set_uint("local_ctx_limit", 10000000);
simp2_p.set_bool("flat", true); // required by som
simp2_p.set_bool("hoist_mul", false); // required by som
simp2_p.set_bool("elim_and", true);
m_preprocess =
and_then(mk_card2bv_tactic(m, m_params),
using_params(mk_simplify_tactic(m), simp2_p),
mk_max_bv_sharing_tactic(m),
mk_bit_blaster_tactic(m, &m_bb_rewriter),
//mk_aig_tactic(),
using_params(mk_simplify_tactic(m), simp2_p));
init_preprocess();
}
virtual ~inc_sat_solver() {}
@ -179,14 +163,14 @@ public:
m_fmls_lim.push_back(m_fmls.size());
m_asms_lim.push_back(m_asmsf.size());
m_fmls_head_lim.push_back(m_fmls_head);
m_bb_rewriter.push();
m_bb_rewriter->push();
m_map.push();
}
virtual void pop(unsigned n) {
if (n > m_num_scopes) { // allow inc_sat_solver to
n = m_num_scopes; // take over for another solver.
}
m_bb_rewriter.pop(n);
m_bb_rewriter->pop(n);
m_map.pop(n);
SASSERT(n <= m_num_scopes);
m_solver.user_pop(n);
@ -269,30 +253,58 @@ public:
return m_asmsf[idx];
}
void init_preprocess() {
if (m_preprocess) {
m_preprocess->reset();
}
params_ref simp2_p = m_params;
m_bb_rewriter = alloc(bit_blaster_rewriter, m, m_params);
simp2_p.set_bool("som", true);
simp2_p.set_bool("pull_cheap_ite", true);
simp2_p.set_bool("push_ite_bv", false);
simp2_p.set_bool("local_ctx", true);
simp2_p.set_uint("local_ctx_limit", 10000000);
simp2_p.set_bool("flat", true); // required by som
simp2_p.set_bool("hoist_mul", false); // required by som
simp2_p.set_bool("elim_and", true);
m_preprocess =
and_then(mk_card2bv_tactic(m, m_params),
using_params(mk_simplify_tactic(m), simp2_p),
mk_max_bv_sharing_tactic(m),
mk_bit_blaster_tactic(m, m_bb_rewriter.get()),
//mk_aig_tactic(),
using_params(mk_simplify_tactic(m), simp2_p));
for (unsigned i = 0; i < m_num_scopes; ++i) {
m_bb_rewriter->push();
}
m_preprocess->reset();
}
private:
lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm) {
m_mc2.reset();
m_mc.reset();
m_pc.reset();
m_dep_core.reset();
m_subgoals.reset();
m_preprocess->reset();
init_preprocess();
SASSERT(g->models_enabled());
SASSERT(!g->proofs_enabled());
TRACE("sat", g->display(tout););
try {
(*m_preprocess)(g, m_subgoals, m_mc2, m_pc, m_dep_core);
(*m_preprocess)(g, m_subgoals, m_mc, m_pc, m_dep_core);
}
catch (tactic_exception & ex) {
IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
m_preprocess = 0;
m_bb_rewriter = 0;
return l_undef;
}
if (m_subgoals.size() != 1) {
IF_VERBOSE(0, verbose_stream() << "size of subgoals is not 1, it is: " << m_subgoals.size() << "\n";);
return l_undef;
}
CTRACE("sat", m_mc.get(), m_mc->display(tout); );
g = m_subgoals[0];
TRACE("sat", g->display_with_dependencies(tout););
m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true);
@ -416,24 +428,25 @@ private:
}
}
m_model = md;
if (m_mc || !m_bb_rewriter.const2bits().empty()) {
model_converter_ref mc = m_mc;
if (!m_bb_rewriter.const2bits().empty()) {
mc = concat(mc.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter.const2bits()));
}
(*mc)(m_model);
if (!m_bb_rewriter->const2bits().empty()) {
m_mc0 = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits()));
}
if (m_mc0) {
(*m_mc0)(m_model);
}
SASSERT(m_model);
DEBUG_CODE(
for (unsigned i = 0; i < m_fmls.size(); ++i) {
expr_ref tmp(m);
VERIFY(m_model->eval(m_fmls[i].get(), tmp, true));
CTRACE("sat", !m.is_true(tmp),
tout << "Evaluation failed: " << mk_pp(m_fmls[i].get(), m)
<< " to " << tmp << "\n";
model_smt2_pp(tout, m, *(m_model.get()), 0););
SASSERT(m.is_true(tmp));
if (m_model->eval(m_fmls[i].get(), tmp, true)) {
CTRACE("sat", !m.is_true(tmp),
tout << "Evaluation failed: " << mk_pp(m_fmls[i].get(), m)
<< " to " << tmp << "\n";
model_smt2_pp(tout, m, *(m_model.get()), 0););
SASSERT(m.is_true(tmp));
}
});
}
};

52
src/smt/theory_bv.cpp
View file

@ -95,10 +95,9 @@ namespace smt {
enode * first_arg_enode = ctx.get_enode(first_arg);
get_var(first_arg_enode);
// numerals are not blasted into bit2bool, so we do this directly.
if (!ctx.b_internalized(n)) {
rational val;
unsigned sz;
VERIFY(m_util.is_numeral(first_arg, val, sz));
rational val;
unsigned sz;
if (!ctx.b_internalized(n) && m_util.is_numeral(first_arg, val, sz)) {
theory_var v = first_arg_enode->get_th_var(get_id());
app* owner = first_arg_enode->get_owner();
for (unsigned i = 0; i < sz; ++i) {
@ -113,29 +112,28 @@ namespace smt {
}
}
}
else {
enode * arg = ctx.get_enode(first_arg);
// The argument was already internalized, but it may not have a theory variable associated with it.
// For example, for ite-terms the method apply_sort_cnstr is not invoked.
// See comment in the then-branch.
theory_var v_arg = arg->get_th_var(get_id());
if (v_arg == null_theory_var) {
// The method get_var will create a theory variable for arg.
// As a side-effect the bits for arg will also be created.
get_var(arg);
SASSERT(ctx.b_internalized(n));
}
else {
SASSERT(v_arg != null_theory_var);
bool_var bv = ctx.mk_bool_var(n);
ctx.set_var_theory(bv, get_id());
bit_atom * a = new (get_region()) bit_atom();
insert_bv2a(bv, a);
m_trail_stack.push(mk_atom_trail(bv));
unsigned idx = n->get_decl()->get_parameter(0).get_int();
SASSERT(a->m_occs == 0);
a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
}
enode * arg = ctx.get_enode(first_arg);
// The argument was already internalized, but it may not have a theory variable associated with it.
// For example, for ite-terms the method apply_sort_cnstr is not invoked.
// See comment in the then-branch.
theory_var v_arg = arg->get_th_var(get_id());
if (v_arg == null_theory_var) {
// The method get_var will create a theory variable for arg.
// As a side-effect the bits for arg will also be created.
get_var(arg);
SASSERT(ctx.b_internalized(n));
}
else if (!ctx.b_internalized(n)) {
SASSERT(v_arg != null_theory_var);
bool_var bv = ctx.mk_bool_var(n);
ctx.set_var_theory(bv, get_id());
bit_atom * a = new (get_region()) bit_atom();
insert_bv2a(bv, a);
m_trail_stack.push(mk_atom_trail(bv));
unsigned idx = n->get_decl()->get_parameter(0).get_int();
SASSERT(a->m_occs == 0);
a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
}
}

3
src/tactic/arith/lia2pb_tactic.cpp
View file

@ -272,8 +272,9 @@ class lia2pb_tactic : public tactic {
}
TRACE("lia2pb", tout << mk_ismt2_pp(x, m) << " -> " << dep << "\n";);
subst.insert(x, def, 0, dep);
if (m_produce_models)
if (m_produce_models) {
mc1->insert(to_app(x)->get_decl(), def);
}
}
}

62
src/tactic/extension_model_converter.cpp
View file

@ -25,25 +25,6 @@ Notes:
extension_model_converter::~extension_model_converter() {
}
struct extension_model_converter::set_eval {
extension_model_converter * m_owner;
model_evaluator * m_old;
set_eval(extension_model_converter * owner, model_evaluator * ev) {
m_owner = owner;
m_old = owner->m_eval;
#pragma omp critical (extension_model_converter)
{
owner->m_eval = ev;
}
}
~set_eval() {
#pragma omp critical (extension_model_converter)
{
m_owner->m_eval = m_old;
}
}
};
static void display_decls_info(std::ostream & out, model_ref & md) {
ast_manager & m = md->get_manager();
@ -68,36 +49,38 @@ void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) {
model_evaluator ev(*(md.get()));
ev.set_model_completion(true);
expr_ref val(m());
{
set_eval setter(this, &ev);
unsigned i = m_vars.size();
while (i > 0) {
--i;
expr * def = m_defs.get(i);
ev(def, val);
TRACE("extension_mc", tout << m_vars.get(i)->get_name() << " ->\n" << mk_ismt2_pp(def, m()) << "\n==>\n" << mk_ismt2_pp(val, m()) << "\n";);
func_decl * f = m_vars.get(i);
unsigned arity = f->get_arity();
if (arity == 0) {
md->register_decl(f, val);
}
else {
func_interp * new_fi = alloc(func_interp, m(), arity);
new_fi->set_else(val);
md->register_decl(f, new_fi);
}
unsigned i = m_vars.size();
while (i > 0) {
--i;
expr * def = m_defs.get(i);
ev(def, val);
TRACE("extension_mc", tout << m_vars.get(i)->get_name() << " ->\n" << mk_ismt2_pp(def, m()) << "\n==>\n" << mk_ismt2_pp(val, m()) << "\n";);
func_decl * f = m_vars.get(i);
unsigned arity = f->get_arity();
if (arity == 0) {
md->register_decl(f, val);
}
else {
func_interp * new_fi = alloc(func_interp, m(), arity);
new_fi->set_else(val);
md->register_decl(f, new_fi);
}
}
TRACE("extension_mc", model_v2_pp(tout, *md); display_decls_info(tout, md););
}
void extension_model_converter::insert(func_decl * v, expr * def) {
m_vars.push_back(v);
m_defs.push_back(def);
}
void extension_model_converter::display(std::ostream & out) {
ast_manager & m = m_vars.get_manager();
out << "(extension-model-converter";
for (unsigned i = 0; i < m_vars.size(); i++) {
out << "\n (" << m_vars.get(i)->get_name() << " ";
unsigned indent = m_vars.get(i)->get_name().size() + 4;
out << mk_ismt2_pp(m_defs.get(i), m, indent) << ")";
out << mk_ismt2_pp(m_defs.get(i), m(), indent) << ")";
}
out << ")" << std::endl;
}
@ -108,6 +91,5 @@ model_converter * extension_model_converter::translate(ast_translation & transla
res->m_vars.push_back(translator(m_vars[i].get()));
for (unsigned i = 0; i < m_defs.size(); i++)
res->m_defs.push_back(translator(m_defs[i].get()));
// m_eval is a transient object. So, it doesn't need to be translated.
return res;
}

10
src/tactic/extension_model_converter.h
View file

@ -23,15 +23,12 @@ Notes:
#include"ast.h"
#include"model_converter.h"
class model_evaluator;
class extension_model_converter : public model_converter {
func_decl_ref_vector m_vars;
expr_ref_vector m_defs;
model_evaluator * m_eval;
struct set_eval;
public:
extension_model_converter(ast_manager & m):m_vars(m), m_defs(m), m_eval(0) {
extension_model_converter(ast_manager & m):m_vars(m), m_defs(m) {
}
virtual ~extension_model_converter();
@ -43,10 +40,7 @@ public:
virtual void display(std::ostream & out);
// register a variable that was eliminated
void insert(func_decl * v, expr * def) {
m_vars.push_back(v);
m_defs.push_back(def);
}
void insert(func_decl * v, expr * def);
virtual model_converter * translate(ast_translation & translator);
};