mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
fix tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
81e5589bc8
commit
792bf6c10b
|
@ -321,10 +321,10 @@ public:
|
|||
void found_optimum() {
|
||||
IF_VERBOSE(1, verbose_stream() << "found optimum\n";);
|
||||
m_lower.reset();
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
m_assignment[i] = m_model->is_true(m_soft[i]);
|
||||
if (!m_assignment[i]) {
|
||||
m_lower += m_weights[i];
|
||||
for (soft& s : m_soft) {
|
||||
s.is_true = m_model->is_true(s.s);
|
||||
if (!s.is_true) {
|
||||
m_lower += s.weight;
|
||||
}
|
||||
}
|
||||
m_upper = m_lower;
|
||||
|
@ -375,24 +375,22 @@ public:
|
|||
}
|
||||
// 1. remove all core literals from m_asms
|
||||
// 2. re-add literals of higher weight than min-weight.
|
||||
// 3. 'core' stores the core literals that are split afterwards
|
||||
// 3. 'core' stores the core literals that are
|
||||
// re-encoded as assumptions, afterwards
|
||||
remove_soft(core, m_asms);
|
||||
split_core(core);
|
||||
cores.push_back(core);
|
||||
if (core.size() >= m_max_core_size) {
|
||||
break;
|
||||
}
|
||||
if (cores.size() >= m_max_num_cores) {
|
||||
break;
|
||||
}
|
||||
|
||||
if (core.size() >= m_max_core_size) break;
|
||||
if (cores.size() >= m_max_num_cores) break;
|
||||
|
||||
is_sat = check_sat_hill_climb(m_asms);
|
||||
}
|
||||
|
||||
TRACE("opt",
|
||||
tout << "num cores: " << cores.size() << "\n";
|
||||
for (auto const& c : cores) {
|
||||
display_vec(tout, c);
|
||||
}
|
||||
tout << "num satisfying: " << m_asms.size() << "\n";);
|
||||
tout << "sat: " << is_sat << " num cores: " << cores.size() << "\n";
|
||||
for (auto const& c : cores) display_vec(tout, c);
|
||||
tout << "num assumptions: " << m_asms.size() << "\n";);
|
||||
|
||||
return is_sat;
|
||||
}
|
||||
|
@ -411,7 +409,6 @@ public:
|
|||
if (mdl->is_false(a)) {
|
||||
cs.push_back(a);
|
||||
}
|
||||
// TRACE("opt", tout << mk_pp(a, m) << ": " << (*mdl)(a) << "\n";);
|
||||
}
|
||||
TRACE("opt", display_vec(tout << "new correction set: ", cs););
|
||||
}
|
||||
|
@ -475,8 +472,8 @@ public:
|
|||
|
||||
unsigned max_core_size(vector<exprs> const& cores) {
|
||||
unsigned result = 0;
|
||||
for (unsigned i = 0; i < cores.size(); ++i) {
|
||||
result = std::max(cores[i].size(), result);
|
||||
for (auto const& c : cores) {
|
||||
result = std::max(c.size(), result);
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
@ -725,13 +722,11 @@ public:
|
|||
|
||||
rational upper(0);
|
||||
|
||||
unsigned i = 0;
|
||||
for (expr* s : m_soft) {
|
||||
TRACE("opt", tout << mk_pp(s, m) << ": " << (*mdl)(s) << " " << m_weights[i] << "\n";);
|
||||
if (!mdl->is_true(s)) {
|
||||
upper += m_weights[i];
|
||||
for (soft& s : m_soft) {
|
||||
TRACE("opt", tout << s.s << ": " << (*mdl)(s.s) << " " << s.weight << "\n";);
|
||||
if (!mdl->is_true(s.s)) {
|
||||
upper += s.weight;
|
||||
}
|
||||
++i;
|
||||
}
|
||||
|
||||
if (upper > m_upper) {
|
||||
|
@ -748,9 +743,8 @@ public:
|
|||
|
||||
TRACE("opt", tout << "updated upper: " << upper << "\nmodel\n" << *m_model;);
|
||||
|
||||
i = 0;
|
||||
for (expr* s : m_soft) {
|
||||
m_assignment[i++] = m_model->is_true(s);
|
||||
for (soft& s : m_soft) {
|
||||
s.is_true = m_model->is_true(s.s);
|
||||
}
|
||||
|
||||
// DEBUG_CODE(verify_assignment(););
|
||||
|
@ -766,11 +760,13 @@ public:
|
|||
if (!m_add_upper_bound_block) return;
|
||||
pb_util u(m);
|
||||
expr_ref_vector nsoft(m);
|
||||
vector<rational> weights;
|
||||
expr_ref fml(m);
|
||||
for (expr* s : m_soft) {
|
||||
nsoft.push_back(mk_not(m, s));
|
||||
for (soft& s : m_soft) {
|
||||
nsoft.push_back(mk_not(m, s.s));
|
||||
weights.push_back(s.weight);
|
||||
}
|
||||
fml = u.mk_lt(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper);
|
||||
fml = u.mk_lt(nsoft.size(), weights.c_ptr(), nsoft.c_ptr(), m_upper);
|
||||
TRACE("opt", tout << "block upper bound " << fml << "\n";);;
|
||||
s().assert_expr(fml);
|
||||
}
|
||||
|
@ -832,9 +828,7 @@ public:
|
|||
void verify_core(exprs const& core) {
|
||||
IF_VERBOSE(3, verbose_stream() << "verify core\n";);
|
||||
ref<solver> smt_solver = mk_smt_solver(m, m_params, symbol());
|
||||
for (unsigned i = 0; i < s().get_num_assertions(); ++i) {
|
||||
smt_solver->assert_expr(s().get_assertion(i));
|
||||
}
|
||||
smt_solver->assert_expr(s().get_assertions());
|
||||
smt_solver->assert_expr(core);
|
||||
lbool is_sat = smt_solver->check_sat(0, nullptr);
|
||||
if (is_sat == l_true) {
|
||||
|
@ -845,13 +839,11 @@ public:
|
|||
void verify_assignment() {
|
||||
IF_VERBOSE(1, verbose_stream() << "verify assignment\n";);
|
||||
ref<solver> smt_solver = mk_smt_solver(m, m_params, symbol());
|
||||
for (unsigned i = 0; i < s().get_num_assertions(); ++i) {
|
||||
smt_solver->assert_expr(s().get_assertion(i));
|
||||
}
|
||||
smt_solver->assert_expr(s().get_assertions());
|
||||
expr_ref n(m);
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
n = m_soft[i];
|
||||
if (!m_assignment[i]) {
|
||||
for (soft& s : m_soft) {
|
||||
n = s.s;
|
||||
if (!s.is_true) {
|
||||
n = mk_not(m, n);
|
||||
}
|
||||
smt_solver->assert_expr(n);
|
||||
|
|
|
@ -34,16 +34,17 @@ Notes:
|
|||
namespace opt {
|
||||
|
||||
maxsmt_solver_base::maxsmt_solver_base(
|
||||
maxsat_context& c, vector<rational> const& ws, expr_ref_vector const& soft):
|
||||
maxsat_context& c, vector<rational> const& ws, expr_ref_vector const& softs):
|
||||
m(c.get_manager()),
|
||||
m_c(c),
|
||||
m_soft(soft),
|
||||
m_weights(ws),
|
||||
m_assertions(m),
|
||||
m_trail(m) {
|
||||
c.get_base_model(m_model);
|
||||
SASSERT(m_model);
|
||||
updt_params(c.params());
|
||||
for (unsigned i = 0; i < ws.size(); ++i) {
|
||||
m_soft.push_back(soft(expr_ref(softs.get(i), m), ws[i], false));
|
||||
}
|
||||
}
|
||||
|
||||
void maxsmt_solver_base::updt_params(params_ref& p) {
|
||||
|
@ -56,17 +57,21 @@ namespace opt {
|
|||
|
||||
void maxsmt_solver_base::commit_assignment() {
|
||||
expr_ref tmp(m);
|
||||
expr_ref_vector fmls(m);
|
||||
rational k(0), cost(0);
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
if (get_assignment(i)) {
|
||||
k += m_weights[i];
|
||||
vector<rational> weights;
|
||||
for (soft const& s : m_soft) {
|
||||
if (s.is_true) {
|
||||
k += s.weight;
|
||||
}
|
||||
else {
|
||||
cost += m_weights[i];
|
||||
cost += s.weight;
|
||||
}
|
||||
weights.push_back(s.weight);
|
||||
fmls.push_back(s.s);
|
||||
}
|
||||
pb_util pb(m);
|
||||
tmp = pb.mk_ge(m_weights.size(), m_weights.c_ptr(), m_soft.c_ptr(), k);
|
||||
tmp = pb.mk_ge(weights.size(), weights.c_ptr(), fmls.c_ptr(), k);
|
||||
TRACE("opt", tout << "cost: " << cost << "\n" << tmp << "\n";);
|
||||
s().assert_expr(tmp);
|
||||
}
|
||||
|
@ -74,19 +79,14 @@ namespace opt {
|
|||
bool maxsmt_solver_base::init() {
|
||||
m_lower.reset();
|
||||
m_upper.reset();
|
||||
m_assignment.reset();
|
||||
for (unsigned i = 0; i < m_weights.size(); ++i) {
|
||||
m_assignment.push_back(m.is_true(m_soft[i]));
|
||||
if (!m_assignment.back()) {
|
||||
m_upper += m_weights[i];
|
||||
}
|
||||
for (soft& s : m_soft) {
|
||||
s.is_true = m.is_true(s.s);
|
||||
if (!s.is_true) m_upper += s.weight;
|
||||
}
|
||||
|
||||
TRACE("opt",
|
||||
tout << "upper: " << m_upper << " assignments: ";
|
||||
for (unsigned i = 0; i < m_weights.size(); ++i) {
|
||||
tout << (m_assignment[i]?"T":"F");
|
||||
}
|
||||
for (soft& s : m_soft) tout << (s.is_true?"T":"F");
|
||||
tout << "\n";);
|
||||
return true;
|
||||
}
|
||||
|
@ -141,6 +141,7 @@ namespace opt {
|
|||
maxsmt_solver_base::scoped_ensure_theory::scoped_ensure_theory(maxsmt_solver_base& s) {
|
||||
m_wth = s.ensure_wmax_theory();
|
||||
}
|
||||
|
||||
maxsmt_solver_base::scoped_ensure_theory::~scoped_ensure_theory() {
|
||||
if (m_wth) {
|
||||
m_wth->reset_local();
|
||||
|
@ -159,11 +160,13 @@ namespace opt {
|
|||
|
||||
lbool maxsmt_solver_base::find_mutexes(obj_map<expr, rational>& new_soft) {
|
||||
m_lower.reset();
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
new_soft.insert(m_soft[i], m_weights[i]);
|
||||
expr_ref_vector fmls(m);
|
||||
for (soft& s : m_soft) {
|
||||
new_soft.insert(s.s, s.weight);
|
||||
fmls.push_back(s.s);
|
||||
}
|
||||
vector<expr_ref_vector> mutexes;
|
||||
lbool is_sat = s().find_mutexes(m_soft, mutexes);
|
||||
lbool is_sat = s().find_mutexes(fmls, mutexes);
|
||||
if (is_sat != l_true) {
|
||||
return is_sat;
|
||||
}
|
||||
|
|
|
@ -56,17 +56,26 @@ namespace opt {
|
|||
//
|
||||
class maxsmt_solver_base : public maxsmt_solver {
|
||||
protected:
|
||||
struct soft {
|
||||
expr_ref s;
|
||||
rational weight;
|
||||
bool is_true;
|
||||
soft(expr_ref& s, rational const& w, bool t): s(s), weight(w), is_true(t) {}
|
||||
soft(soft const& other):s(other.s), weight(other.weight), is_true(other.is_true) {}
|
||||
soft& operator=(soft const& other) { s = other.s; weight = other.weight; is_true = other.is_true; return *this; }
|
||||
};
|
||||
ast_manager& m;
|
||||
maxsat_context& m_c;
|
||||
const expr_ref_vector m_soft;
|
||||
vector<rational> m_weights;
|
||||
maxsat_context& m_c;
|
||||
vector<soft> m_soft;
|
||||
expr_ref_vector m_assertions;
|
||||
expr_ref_vector m_trail;
|
||||
rational m_lower;
|
||||
rational m_upper;
|
||||
model_ref m_model;
|
||||
svector<symbol> m_labels;
|
||||
svector<bool> m_assignment; // truth assignment to soft constraints
|
||||
//const expr_ref_vector m_soft;
|
||||
//vector<rational> m_weights;
|
||||
//svector<bool> m_assignment; // truth assignment to soft constraints
|
||||
params_ref m_params; // config
|
||||
|
||||
public:
|
||||
|
@ -75,7 +84,7 @@ namespace opt {
|
|||
~maxsmt_solver_base() override {}
|
||||
rational get_lower() const override { return m_lower; }
|
||||
rational get_upper() const override { return m_upper; }
|
||||
bool get_assignment(unsigned index) const override { return m_assignment[index]; }
|
||||
bool get_assignment(unsigned index) const override { return m_soft[index].is_true; }
|
||||
void collect_statistics(statistics& st) const override { }
|
||||
void get_model(model_ref& mdl, svector<symbol>& labels) override { mdl = m_model.get(); labels = m_labels;}
|
||||
virtual void commit_assignment();
|
||||
|
|
|
@ -114,9 +114,7 @@ namespace opt {
|
|||
}
|
||||
|
||||
void update_assignment() {
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
m_assignment[i] = is_true(m_soft[i]);
|
||||
}
|
||||
for (soft& s : m_soft) s.is_true = is_true(s.s);
|
||||
}
|
||||
|
||||
bool is_true(expr* e) {
|
||||
|
|
|
@ -124,10 +124,7 @@ namespace opt {
|
|||
}
|
||||
|
||||
void update_assignment() {
|
||||
m_assignment.reset();
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
m_assignment.push_back(is_true(m_soft[i]));
|
||||
}
|
||||
for (soft& s : m_soft) s.is_true = is_true(s.s);
|
||||
}
|
||||
|
||||
struct compare_asm {
|
||||
|
|
|
@ -64,6 +64,13 @@ void solver::get_assertions(expr_ref_vector& fmls) const {
|
|||
}
|
||||
}
|
||||
|
||||
expr_ref_vector solver::get_assertions() const {
|
||||
expr_ref_vector result(get_manager());
|
||||
get_assertions(result);
|
||||
return result;
|
||||
}
|
||||
|
||||
|
||||
struct scoped_assumption_push {
|
||||
expr_ref_vector& m_vec;
|
||||
scoped_assumption_push(expr_ref_vector& v, expr* e): m_vec(v) { v.push_back(e); }
|
||||
|
|
|
@ -179,6 +179,8 @@ public:
|
|||
*/
|
||||
void get_assertions(expr_ref_vector& fmls) const;
|
||||
|
||||
expr_ref_vector get_assertions() const;
|
||||
|
||||
/**
|
||||
\brief The number of tracked assumptions (see assert_expr(t, a)).
|
||||
*/
|
||||
|
|
|
@ -88,8 +88,7 @@ static void test(app* var, expr_ref& fml) {
|
|||
std::cout << "projected: " << mk_pp(pr, m) << "\n";
|
||||
|
||||
// projection is consistent with model.
|
||||
expr_ref tmp(m);
|
||||
VERIFY(md->eval(pr, tmp) && m.is_true(tmp));
|
||||
VERIFY(md->is_true(pr));
|
||||
|
||||
// projection implies E x. fml
|
||||
{
|
||||
|
|
Loading…
Reference in a new issue