mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

fixes to bugs exposed by regressions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-15 05:23:47 +02:00
parent 50f18a77af
commit fe5c42c90f
12 changed files with 325 additions and 85 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/ast/pb_decl_plugin.cpp
View file

@ -118,8 +118,8 @@ app * pb_util::mk_at_most_k(unsigned num_args, expr * const * args, unsigned k)
return m.mk_app(m_fid, OP_AT_MOST_K, 1, &param, num_args, args, m.mk_bool_sort());
}
bool pb_util::is_at_most_k(app *a) const {
return is_app_of(a, m_fid, OP_AT_MOST_K);
bool pb_util::is_at_most_k(func_decl *a) const {
return is_decl_of(a, m_fid, OP_AT_MOST_K);
}
bool pb_util::is_at_most_k(app *a, rational& k) const {
@ -138,8 +138,8 @@ app * pb_util::mk_at_least_k(unsigned num_args, expr * const * args, unsigned k)
return m.mk_app(m_fid, OP_AT_LEAST_K, 1, &param, num_args, args, m.mk_bool_sort());
}
bool pb_util::is_at_least_k(app *a) const {
return is_app_of(a, m_fid, OP_AT_LEAST_K);
bool pb_util::is_at_least_k(func_decl *a) const {
return is_decl_of(a, m_fid, OP_AT_LEAST_K);
}
bool pb_util::is_at_least_k(app *a, rational& k) const {
@ -152,8 +152,8 @@ bool pb_util::is_at_least_k(app *a, rational& k) const {
}
}
rational pb_util::get_k(app *a) const {
parameter const& p = a->get_decl()->get_parameter(0);
rational pb_util::get_k(func_decl *a) const {
parameter const& p = a->get_parameter(0);
if (is_at_most_k(a) || is_at_least_k(a)) {
return to_rational(p);
}
@ -164,8 +164,8 @@ rational pb_util::get_k(app *a) const {
}
bool pb_util::is_le(app *a) const {
return is_app_of(a, m_fid, OP_PB_LE);
bool pb_util::is_le(func_decl *a) const {
return is_decl_of(a, m_fid, OP_PB_LE);
}
bool pb_util::is_le(app* a, rational& k) const {
@ -178,8 +178,8 @@ bool pb_util::is_le(app* a, rational& k) const {
}
}
bool pb_util::is_ge(app *a) const {
return is_app_of(a, m_fid, OP_PB_GE);
bool pb_util::is_ge(func_decl *a) const {
return is_decl_of(a, m_fid, OP_PB_GE);
}
bool pb_util::is_ge(app* a, rational& k) const {
@ -192,13 +192,13 @@ bool pb_util::is_ge(app* a, rational& k) const {
}
}
rational pb_util::get_coeff(app* a, unsigned index) {
rational pb_util::get_coeff(func_decl* a, unsigned index) const {
if (is_at_most_k(a) || is_at_least_k(a)) {
return rational::one();
}
SASSERT(is_le(a) || is_ge(a));
SASSERT(1 + index < a->get_decl()->get_num_parameters());
return to_rational(a->get_decl()->get_parameter(index + 1));
SASSERT(1 + index < a->get_num_parameters());
return to_rational(a->get_parameter(index + 1));
}
rational pb_util::to_rational(parameter const& p) const {

18
src/ast/pb_decl_plugin.h
View file

@ -82,16 +82,22 @@ public:
app * mk_at_least_k(unsigned num_args, expr * const * args, unsigned k);
app * mk_le(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k);
app * mk_ge(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k);
bool is_at_most_k(app *a) const;
bool is_at_most_k(func_decl *a) const;
bool is_at_most_k(app *a) const { return is_at_most_k(a->get_decl()); }
bool is_at_most_k(app *a, rational& k) const;
bool is_at_least_k(app *a) const;
bool is_at_least_k(func_decl *a) const;
bool is_at_least_k(app *a) const { return is_at_most_k(a->get_decl()); }
bool is_at_least_k(app *a, rational& k) const;
rational get_k(app *a) const;
bool is_le(app *a) const;
rational get_k(func_decl *a) const;
rational get_k(app *a) const { return get_k(a->get_decl()); }
bool is_le(func_decl *a) const;
bool is_le(app *a) const { return is_le(a->get_decl()); }
bool is_le(app* a, rational& k) const;
bool is_ge(app* a) const;
bool is_ge(func_decl* a) const;
bool is_ge(app* a) const { return is_ge(a->get_decl()); }
bool is_ge(app* a, rational& k) const;
rational get_coeff(app* a, unsigned index);
rational get_coeff(app* a, unsigned index) const { return get_coeff(a->get_decl(), index); }
rational get_coeff(func_decl* a, unsigned index) const;
private:
rational to_rational(parameter const& p) const;
};

65
src/ast/rewriter/pb_rewriter.cpp Normal file
View file

@ -0,0 +1,65 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
pb_rewriter.cpp
Abstract:
Basic rewriting rules for PB constraints.
Author:
Nikolaj Bjorner (nbjorner) 2013-14-12
Notes:
--*/
#include "pb_rewriter.h"
br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
ast_manager& m = result.get_manager();
rational sum(0), maxsum(0);
for (unsigned i = 0; i < num_args; ++i) {
if (m.is_true(args[i])) {
sum += m_util.get_coeff(f, i);
maxsum += m_util.get_coeff(f, i);
}
else if (!m.is_false(args[i])) {
maxsum += m_util.get_coeff(f, i);
}
}
rational k = m_util.get_k(f);
switch(f->get_decl_kind()) {
case OP_AT_MOST_K:
case OP_PB_LE:
if (sum > k) {
result = m.mk_false();
return BR_DONE;
}
if (maxsum <= k) {
result = m.mk_true();
return BR_DONE;
}
return BR_FAILED;
case OP_AT_LEAST_K:
case OP_PB_GE:
if (sum >= k) {
result = m.mk_true();
return BR_DONE;
}
if (maxsum < k) {
result = m.mk_false();
return BR_DONE;
}
return BR_FAILED;
default:
UNREACHABLE();
return BR_FAILED;
}
}

45
src/ast/rewriter/pb_rewriter.h Normal file
View file

@ -0,0 +1,45 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
pb_rewriter.h
Abstract:
Basic rewriting rules for PB constraints.
Author:
Nikolaj Bjorner (nbjorner) 2013-14-12
Notes:
--*/
#ifndef _PB_REWRITER_H_
#define _PB_REWRITER_H_
#include"pb_decl_plugin.h"
#include"rewriter_types.h"
#include"params.h"
/**
\brief Cheap rewrite rules for PB constraints
*/
class pb_rewriter {
pb_util m_util;
public:
pb_rewriter(ast_manager & m, params_ref const & p = params_ref()):
m_util(m) {
}
ast_manager & m() const { return m_util.get_manager(); }
family_id get_fid() const { return m_util.get_family_id(); }
void updt_params(params_ref const & p) {}
static void get_param_descrs(param_descrs & r) {}
br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
};
#endif

5
src/ast/rewriter/th_rewriter.cpp
View file

@ -25,6 +25,7 @@ Notes:
#include"array_rewriter.h"
#include"float_rewriter.h"
#include"dl_rewriter.h"
#include"pb_rewriter.h"
#include"rewriter_def.h"
#include"expr_substitution.h"
#include"ast_smt2_pp.h"
@ -41,6 +42,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
datatype_rewriter m_dt_rw;
float_rewriter m_f_rw;
dl_rewriter m_dl_rw;
pb_rewriter m_pb_rw;
arith_util m_a_util;
bv_util m_bv_util;
unsigned long long m_max_memory; // in bytes
@ -195,6 +197,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
return m_f_rw.mk_app_core(f, num, args, result);
if (fid == m_dl_rw.get_fid())
return m_dl_rw.mk_app_core(f, num, args, result);
if (fid == m_pb_rw.get_fid())
return m_pb_rw.mk_app_core(f, num, args, result);
return BR_FAILED;
}
@ -644,6 +648,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
m_dt_rw(m),
m_f_rw(m, p),
m_dl_rw(m),
m_pb_rw(m),
m_a_util(m),
m_bv_util(m),
m_used_dependencies(m),

5
src/model/model_evaluator.cpp
View file

@ -23,6 +23,7 @@ Revision History:
#include"bool_rewriter.h"
#include"arith_rewriter.h"
#include"bv_rewriter.h"
#include"pb_rewriter.h"
#include"datatype_rewriter.h"
#include"array_rewriter.h"
#include"float_rewriter.h"
@ -36,6 +37,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
bv_rewriter m_bv_rw;
array_rewriter m_ar_rw;
datatype_rewriter m_dt_rw;
pb_rewriter m_pb_rw;
float_rewriter m_f_rw;
unsigned long long m_max_memory;
unsigned m_max_steps;
@ -52,6 +54,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
// See comment above. We want to allow customers to set :sort-store
m_ar_rw(m, p),
m_dt_rw(m),
m_pb_rw(m),
m_f_rw(m) {
m_b_rw.set_flat(false);
m_a_rw.set_flat(false);
@ -153,6 +156,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
return m_ar_rw.mk_app_core(f, num, args, result);
if (fid == m_dt_rw.get_fid())
return m_dt_rw.mk_app_core(f, num, args, result);
if (fid == m_pb_rw.get_fid())
return m_pb_rw.mk_app_core(f, num, args, result);
if (fid == m_f_rw.get_fid())
return m_f_rw.mk_app_core(f, num, args, result);
return BR_FAILED;

1
src/opt/fu_malik.cpp
View file

@ -322,6 +322,7 @@ namespace opt {
for (unsigned i = 0; i < m_orig_soft.size(); ++i) {
expr_ref val(m);
VERIFY(m_model->eval(m_orig_soft[i].get(), val));
TRACE("opt", tout << val << "\n";);
m_assignment.push_back(m.is_true(val));
}
TRACE("opt", tout << "maxsat cost: " << m_upper << "\n";

17
src/opt/maxsmt.cpp
View file

@ -112,25 +112,18 @@ namespace opt {
for (unsigned i = 0; i < m_soft_constraints.size(); ++i) {
expr_ref tmp(m);
tmp = m_soft_constraints[i].get();
if (get_assignment(i)) {
m_s->assert_expr(tmp);
}
else {
if (!get_assignment(i)) {
tmp = m.mk_not(tmp);
m_s->assert_expr(tmp);
}
TRACE("opt", tout << "asserting: " << tmp << "\n";);
m_s->assert_expr(tmp);
}
}
void maxsmt::display_answer(std::ostream& out) const {
for (unsigned i = 0; i < m_soft_constraints.size(); ++i) {
out << mk_pp(m_soft_constraints[i], m);
if (get_assignment(i)) {
out << " |-> true\n";
}
else {
out << " |-> false\n";
}
out << mk_pp(m_soft_constraints[i], m)
<< (get_assignment(i)?" |-> true\n":" |-> false\n");
}
}

4
src/opt/opt_context.cpp
View file

@ -121,7 +121,7 @@ namespace opt {
lbool context::execute_min_max(unsigned index, bool committed) {
lbool result = m_optsmt.lex(index);
if (committed) m_optsmt.commit_assignment(index);
if (result == l_true && committed) m_optsmt.commit_assignment(index);
if (result == l_true) m_optsmt.get_model(m_model);
return result;
}
@ -129,7 +129,7 @@ namespace opt {
lbool context::execute_maxsat(symbol const& id, bool committed) {
maxsmt& ms = *m_maxsmts.find(id);
lbool result = ms(get_solver());
if (committed) ms.commit_assignment();
if (result == l_true && committed) ms.commit_assignment();
if (result == l_true) ms.get_model(m_model);
return result;
}

136
src/opt/weighted_maxsat.cpp
View file

@ -48,6 +48,7 @@ namespace smt {
*/
void get_assignment(svector<bool>& result) {
result.reset();
std::sort(m_cost_save.begin(), m_cost_save.end());
for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) {
if (j < m_cost_save.size() && m_cost_save[j] == i) {
@ -58,43 +59,58 @@ namespace smt {
result.push_back(true);
}
}
TRACE("opt",
tout << "cost save: ";
for (unsigned i = 0; i < m_cost_save.size(); ++i) {
tout << m_cost_save[i] << " ";
}
tout << "\nvars: ";
for (unsigned i = 0; i < m_vars.size(); ++i) {
tout << mk_pp(m_vars[i].get(), get_manager()) << " ";
}
tout << "\nassignment";
for (unsigned i = 0; i < result.size(); ++i) {
tout << result[i] << " ";
}
tout << "\n";);
}
virtual void init_search_eh() {
context & ctx = get_context();
ast_manager& m = get_manager();
m_var2bool.reset();
for (unsigned i = 0; i < m_vars.size(); ++i) {
bool initialized = !m_var2bool.empty();
for (unsigned i = 0; !initialized && i < m_vars.size(); ++i) {
app* var = m_vars[i].get();
bool_var bv;
enode* x;
if (!ctx.e_internalized(var)) {
x = ctx.mk_enode(var, false, true, true);
}
else {
x = ctx.get_enode(var);
}
theory_var v;
SASSERT(!ctx.e_internalized(var));
enode* x = ctx.mk_enode(var, false, true, true);
if (ctx.b_internalized(var)) {
bv = ctx.get_bool_var(var);
}
else {
bv = ctx.mk_bool_var(var);
}
ctx.set_var_theory(bv, get_id());
ctx.set_var_theory(bv, get_id());
ctx.set_enode_flag(bv, true);
theory_var v = mk_var(x);
v = mk_var(x);
ctx.attach_th_var(x, this, v);
m_bool2var.insert(bv, v);
SASSERT(v == m_var2bool.size());
m_var2bool.push_back(bv);
SASSERT(ctx.bool_var2enode(bv));
}
for (unsigned i = 0; i < m_vars.size(); ++i) {
app* var = m_vars[i].get();
bool_var bv = ctx.get_bool_var(var);
lbool asgn = ctx.get_assignment(bv);
if (asgn == l_true) {
assign_eh(bv, true);
}
}
if (m_min_cost_atom) {
app* var = m_min_cost_atom;
if (!ctx.e_internalized(var)) {
@ -157,10 +173,7 @@ namespace smt {
}
virtual final_check_status final_check_eh() {
if (block(true)) {
return FC_DONE;
}
return FC_CONTINUE;
return FC_DONE;
}
virtual bool use_diseqs() const {
@ -171,7 +184,7 @@ namespace smt {
return false;
}
void reset() {
void reset() {
reset_eh();
}
@ -195,17 +208,9 @@ namespace smt {
virtual void new_eq_eh(theory_var v1, theory_var v2) { }
virtual void new_diseq_eh(theory_var v1, theory_var v2) { }
private:
class compare_cost {
theory_weighted_maxsat& m_th;
public:
compare_cost(theory_weighted_maxsat& t):m_th(t) {}
bool operator() (theory_var v, theory_var w) const {
return m_th.m_weights[v] > m_th.m_weights[w];
}
};
bool is_optimal() const {
return m_cost < m_min_cost;
}
bool block(bool is_final) {
if (m_vars.empty()) {
@ -225,18 +230,27 @@ namespace smt {
if (m_min_cost_atom) {
lits.push_back(~literal(m_min_cost_bv));
}
IF_VERBOSE(2,
verbose_stream() << "block: ";
for (unsigned i = 0; i < lits.size(); ++i) {
expr_ref tmp(m);
ctx.literal2expr(lits[i], tmp);
verbose_stream() << tmp << " ";
}
verbose_stream() << "\n";
);
TRACE("opt",
tout << "block" << (is_final?" final: ":": ");;
for (unsigned i = 0; i < lits.size(); ++i) {
expr_ref tmp(m);
ctx.literal2expr(lits[i], tmp);
tout << tmp << " ";
}
tout << "\n";
if (is_final && is_optimal()) {
tout << "costs: ";
for (unsigned i = 0; i < m_costs.size(); ++i) {
tout << mk_pp(get_enode(m_costs[i])->get_owner(), get_manager()) << " ";
}
tout << "\n";
ctx.display(tout);
}
);
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
if (is_final && m_cost < m_min_cost) {
if (is_final && is_optimal()) {
m_min_cost = weight;
m_cost_save.reset();
m_cost_save.append(m_costs);
@ -244,6 +258,19 @@ namespace smt {
return false;
}
private:
class compare_cost {
theory_weighted_maxsat& m_th;
public:
compare_cost(theory_weighted_maxsat& t):m_th(t) {}
bool operator() (theory_var v, theory_var w) const {
return m_th.m_weights[v] > m_th.m_weights[w];
}
};
};
}
@ -329,26 +356,36 @@ namespace opt {
lbool operator()() {
TRACE("opt", tout << "weighted maxsat\n";);
smt::theory_weighted_maxsat& wth = ensure_theory();
lbool result;
lbool is_sat = l_true;
{
solver::scoped_push _s(s);
for (unsigned i = 0; i < m_soft.size(); ++i) {
wth.assert_weighted(m_soft[i].get(), m_weights[i]);
}
result = s.check_sat_core(0,0);
SASSERT(result != l_true);
wth.get_assignment(m_assignment);
if (result == l_false) {
result = l_true;
while (l_true == is_sat) {
is_sat = s.check_sat_core(0,0);
if (is_sat == l_true) {
if (wth.is_optimal()) {
s.get_model(m_model);
}
wth.block(true);
if (s.get_context().inconsistent()) {
is_sat = l_false;
}
}
}
if (is_sat == l_false) {
wth.get_assignment(m_assignment);
is_sat = l_true;
}
}
m_upper = wth.get_min_cost();
if (result == l_true) {
if (is_sat == l_true) {
m_lower = m_upper;
}
TRACE("opt", tout << "min cost: " << m_upper << "\n";);
wth.reset();
return result;
return is_sat;
}
rational get_lower() const {
@ -360,10 +397,7 @@ namespace opt {
}
void get_model(model_ref& mdl) {
lbool is_sat = s.check_sat_core(0,0);
if (is_sat == l_true) {
s.get_model(mdl);
}
mdl = m_model.get();
}
};

84
src/smt/theory_pb.cpp
View file

@ -23,6 +23,7 @@ Notes:
#include "ast_pp.h"
#include "sorting_network.h"
#include "uint_set.h"
#include "smt_model_generator.h"
namespace smt {
@ -1458,6 +1459,89 @@ namespace smt {
return out;
}
class theory_pb::pb_model_value_proc : public model_value_proc {
app* m_app;
svector<model_value_dependency> m_dependencies;
public:
pb_model_value_proc(app* a):
m_app(a) {}
void add(enode* n) {
m_dependencies.push_back(model_value_dependency(n));
}
virtual void get_dependencies(buffer<model_value_dependency> & result) {
result.append(m_dependencies.size(), m_dependencies.c_ptr());
}
virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values) {
ast_manager& m = mg.get_manager();
SASSERT(values.size() == m_dependencies.size());
SASSERT(values.size() == m_app->get_num_args());
pb_util u(m);
rational sum(0);
for (unsigned i = 0; i < m_app->get_num_args(); ++i) {
if (!m.is_true(values[i]) && !m.is_false(values[i])) {
return m_app;
}
if (m.is_true(values[i])) {
sum += u.get_coeff(m_app, i);
}
}
rational k = u.get_k(m_app);
switch(m_app->get_decl_kind()) {
case OP_AT_MOST_K:
return (sum <= k)?m.mk_true():m.mk_false();
case OP_AT_LEAST_K:
return (sum >= k)?m.mk_true():m.mk_false();
case OP_PB_LE:
return (sum <= k)?m.mk_true():m.mk_false();
case OP_PB_GE:
return (sum >= k)?m.mk_true():m.mk_false();
default:
UNREACHABLE();
return 0;
}
return 0;
}
};
class pb_factory : public value_factory {
public:
pb_factory(ast_manager& m, family_id fid):
value_factory(m, fid) {}
virtual expr * get_some_value(sort * s) {
return m_manager.mk_true();
}
virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
v1 = m_manager.mk_true();
v2 = m_manager.mk_false();
return true;
}
virtual expr * get_fresh_value(sort * s) {
return 0;
}
virtual void register_value(expr * n) { }
};
void theory_pb::init_model(model_generator & m) {
std::cout << "init model\n";
m.register_factory(alloc(pb_factory, get_manager(), get_id()));
}
model_value_proc * theory_pb::mk_value(enode * n, model_generator & mg) {
std::cout << "mk-value " << mk_pp(n->get_owner(), get_manager()) << "\n";
context& ctx = get_context();
app* a = n->get_owner();
pb_model_value_proc* p = alloc(pb_model_value_proc, a);
for (unsigned i = 0; i < a->get_num_args(); ++i) {
p->add(ctx.get_enode(a->get_arg(i)));
}
return p;
}
void theory_pb::display(std::ostream& out) const {
u_map<ptr_vector<ineq>*>::iterator it = m_watch.begin(), end = m_watch.end();
for (; it != end; ++it) {

4
src/smt/theory_pb.h
View file

@ -29,6 +29,7 @@ namespace smt {
struct sort_expr;
class pb_justification;
class pb_model_value_proc;
typedef rational numeral;
typedef vector<std::pair<literal, numeral> > arg_t;
@ -181,6 +182,7 @@ namespace smt {
virtual void pop_scope_eh(unsigned num_scopes);
virtual void restart_eh();
virtual void collect_statistics(::statistics & st) const;
virtual model_value_proc * mk_value(enode * n, model_generator & mg);
virtual void init_model(model_generator & m);
};
};