mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

fix and enable learning

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-11-19 20:47:16 -08:00
parent 696db3a6a4
commit 33895d522b
6 changed files with 91 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/api/api_ast.cpp
View file

@ -1126,6 +1126,7 @@ extern "C" {
if (mk_c(c)->get_pb_fid() == _d->get_family_id()) {
switch(_d->get_decl_kind()) {
case OP_PB_LE: return Z3_OP_PB_LE;
case OP_PB_GE: return Z3_OP_PB_GE;
case OP_AT_MOST_K: return Z3_OP_PB_AT_MOST;
default: UNREACHABLE();
}

4
src/api/z3_api.h
View file

@ -880,6 +880,9 @@ typedef enum
- Z3_OP_PB_LE: Generalized Pseudo-Boolean cardinality constraint.
Example 2*x + 3*y <= 4
- Z3_OP_PB_GE: Generalized Pseudo-Boolean cardinality constraint.
Example 2*x + 3*y + 2*z >= 4
- Z3_OP_UNINTERPRETED: kind used for uninterpreted symbols.
*/
typedef enum {
@ -1063,6 +1066,7 @@ typedef enum {
// Pseudo Booleans
Z3_OP_PB_AT_MOST=0x900,
Z3_OP_PB_LE,
Z3_OP_PB_GE,
Z3_OP_UNINTERPRETED
} Z3_decl_kind;

59
src/ast/pb_decl_plugin.cpp
View file

@ -21,7 +21,8 @@ Revision History:
pb_decl_plugin::pb_decl_plugin():
m_at_most_sym("at-most"),
m_pble_sym("pble")
m_pble_sym("pble"),
m_pbge_sym("pbge")
{}
func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
@ -53,6 +54,18 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
func_decl_info info(m_family_id, OP_PB_LE, num_parameters, parameters);
return m.mk_func_decl(m_pble_sym, arity, domain, m.mk_bool_sort(), info);
}
case OP_PB_GE: {
if (num_parameters != 1 + arity || !parameters[0].is_int()) {
m.raise_exception("function 'pbge' expects arity+1 integer parameters");
}
for (unsigned i = 1; i < num_parameters; ++i) {
if (!parameters[i].is_int()) {
m.raise_exception("function 'pbge' expects arity+1 integer parameters");
}
}
func_decl_info info(m_family_id, OP_PB_GE, num_parameters, parameters);
return m.mk_func_decl(m_pbge_sym, arity, domain, m.mk_bool_sort(), info);
}
default:
UNREACHABLE();
return 0;
@ -63,15 +76,10 @@ void pb_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
if (logic == symbol::null) {
op_names.push_back(builtin_name(m_at_most_sym.bare_str(), OP_AT_MOST_K));
op_names.push_back(builtin_name(m_pble_sym.bare_str(), OP_PB_LE));
op_names.push_back(builtin_name(m_pbge_sym.bare_str(), OP_PB_GE));
}
}
app * pb_util::mk_at_most_k(unsigned num_args, expr * const * args, unsigned k) {
parameter param(k);
return m.mk_app(m_fid, OP_AT_MOST_K, 1, &param, num_args, args, m.mk_bool_sort());
}
app * pb_util::mk_le(unsigned num_args, int const * coeffs, expr * const * args, int k) {
vector<parameter> params;
params.push_back(parameter(k));
@ -81,6 +89,23 @@ app * pb_util::mk_le(unsigned num_args, int const * coeffs, expr * const * args,
return m.mk_app(m_fid, OP_PB_LE, params.size(), params.c_ptr(), num_args, args, m.mk_bool_sort());
}
app * pb_util::mk_ge(unsigned num_args, int const * coeffs, expr * const * args, int k) {
vector<parameter> params;
params.push_back(parameter(k));
for (unsigned i = 0; i < num_args; ++i) {
params.push_back(parameter(coeffs[i]));
}
return m.mk_app(m_fid, OP_PB_GE, params.size(), params.c_ptr(), num_args, args, m.mk_bool_sort());
}
app * pb_util::mk_at_most_k(unsigned num_args, expr * const * args, unsigned k) {
parameter param(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);
@ -97,7 +122,7 @@ bool pb_util::is_at_most_k(app *a, unsigned& k) const {
}
int pb_util::get_k(app *a) const {
SASSERT(is_at_most_k(a) || is_le(a));
SASSERT(is_at_most_k(a) || is_le(a) || is_ge(a));
return a->get_decl()->get_parameter(0).get_int();
}
@ -116,11 +141,25 @@ bool pb_util::is_le(app* a, int& k) const {
}
}
int pb_util::get_le_coeff(app* a, unsigned index) {
bool pb_util::is_ge(app *a) const {
return is_app_of(a, m_fid, OP_PB_GE);
}
bool pb_util::is_ge(app* a, int& k) const {
if (is_ge(a)) {
k = get_k(a);
return true;
}
else {
return false;
}
}
int pb_util::get_coeff(app* a, unsigned index) {
if (is_at_most_k(a)) {
return 1;
}
SASSERT(is_le(a));
SASSERT(is_le(a) || is_ge(a));
SASSERT(1 + index < a->get_decl()->get_num_parameters());
return a->get_decl()->get_parameter(index + 1).get_int();
}

10
src/ast/pb_decl_plugin.h
View file

@ -32,6 +32,7 @@ hence:
enum pb_op_kind {
OP_AT_MOST_K, // at most K Booleans are true.
OP_PB_LE, // pseudo-Boolean <= (generalizes at_most_k)
OP_PB_GE, // pseudo-Boolean >=
LAST_PB_OP
};
@ -39,8 +40,10 @@ enum pb_op_kind {
class pb_decl_plugin : public decl_plugin {
symbol m_at_most_sym;
symbol m_pble_sym;
symbol m_pbge_sym;
func_decl * mk_at_most(unsigned arity, unsigned k);
func_decl * mk_le(unsigned arity, int const* coeffs, int k);
func_decl * mk_ge(unsigned arity, int const* coeffs, int k);
public:
pb_decl_plugin();
virtual ~pb_decl_plugin() {}
@ -74,14 +77,19 @@ public:
family_id get_family_id() const { return m_fid; }
app * mk_at_most_k(unsigned num_args, expr * const * args, unsigned k);
app * mk_le(unsigned num_args, int const * coeffs, expr * const * args, int k);
app * mk_ge(unsigned num_args, int const * coeffs, expr * const * args, int k);
bool is_at_most_k(app *a) const;
bool is_at_most_k(app *a, unsigned& k) const;
int get_k(app *a) const;
bool is_le(app *a) const;
bool is_le(app* a, int& k) const;
int get_le_coeff(app* a, unsigned index);
bool is_ge(app* a) const;
bool is_ge(app* a, int& k) const;
int get_coeff(app* a, unsigned index);
};
#endif /* _PB_DECL_PLUGIN_H_ */

43
src/smt/theory_pb.cpp
View file

@ -26,7 +26,7 @@ Notes:
namespace smt {
bool theory_pb::s_debug_conflict = false; // true; //
bool theory_pb::s_debug_conflict = true; // false; // true; //
void theory_pb::ineq::negate() {
m_lit.neg();
@ -243,7 +243,7 @@ namespace smt {
context& ctx = get_context();
ast_manager& m = get_manager();
unsigned num_args = atom->get_num_args();
SASSERT(m_util.is_at_most_k(atom) || m_util.is_le(atom));
SASSERT(m_util.is_at_most_k(atom) || m_util.is_le(atom) || m_util.is_ge(atom));
if (ctx.b_internalized(atom)) {
return false;
@ -264,14 +264,16 @@ namespace smt {
for (unsigned i = 0; i < num_args; ++i) {
expr* arg = atom->get_arg(i);
literal l = compile_arg(arg);
numeral c = m_util.get_le_coeff(atom, i);
numeral c = m_util.get_coeff(atom, i);
args.push_back(std::make_pair(l, c));
}
// turn W <= k into -W >= -k
for (unsigned i = 0; i < args.size(); ++i) {
args[i].second = -args[i].second;
if (m_util.is_at_most_k(atom) || m_util.is_le(atom)) {
// turn W <= k into -W >= -k
for (unsigned i = 0; i < args.size(); ++i) {
args[i].second = -args[i].second;
}
k = -k;
}
k = -k;
c->unique();
lbool is_true = c->normalize();
@ -921,7 +923,10 @@ namespace smt {
}
for (unsigned i = 0; i < c.size(); ++i) {
literal l(c.lit(i));
out << c.coeff(i) << "*" << l;
if (c.coeff(i) != 1) {
out << c.coeff(i) << "*";
}
out << l;
if (values) {
out << "@(" << ctx.get_assignment(l);
if (ctx.get_assignment(l) != l_undef) {
@ -1091,7 +1096,7 @@ namespace smt {
SASSERT(ctx.get_assignment(c.lit()) == l_true);
if (ctx.get_assign_level(c.lit().var()) > ctx.get_base_level()) {
m_antecedents.push_back(~c.lit());
m_ineq_literals.push_back(c.lit());
}
}
@ -1100,7 +1105,7 @@ namespace smt {
//
void theory_pb::resolve_conflict(literal conseq, ineq& c) {
TRACE("pb", tout << "RESOLVE: " << conseq << "\n"; display(verbose_stream(), c, true););
TRACE("pb", tout << "RESOLVE: " << conseq << "\n"; display(tout, c, true););
bool_var v;
context& ctx = get_context();
@ -1120,7 +1125,7 @@ namespace smt {
m_num_marks = 0;
m_lemma.reset();
m_antecedents.reset();
m_ineq_literals.reset();
process_ineq(c, null_literal, 1); // add consequent to lemma.
// point into stack of assigned literals
@ -1221,7 +1226,7 @@ namespace smt {
IF_VERBOSE(1, display(verbose_stream() << "lemma: ", m_lemma););
// TBD:
// create clause m_antecedents \/ m_lemma;
// create clause m_literals \/ m_lemma;
//
#if 1
ast_manager& m = get_manager();
@ -1234,11 +1239,17 @@ namespace smt {
coeffs.push_back(static_cast<int>(m_lemma.coeff(i)));
}
int k = static_cast<int>(m_lemma.k());
tmp = m_util.mk_le(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), k);
tmp = m_util.mk_ge(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), k);
internalize_atom(to_app(tmp), false);
m_antecedents.push_back(literal(ctx.get_bool_var(tmp)));
justification* mjs = 0;
ctx.mk_clause(m_antecedents.size(), m_antecedents.c_ptr(), mjs, CLS_AUX_LEMMA, 0);
//m_ineq_literals.push_back(literal(ctx.get_bool_var(tmp)));
ctx.mark_as_relevant(tmp);
//justification* mjs = 0;
//ctx.mk_clause(m_ineq_literals.size(), m_ineq_literals.c_ptr(), mjs, CLS_AUX_LEMMA, 0);
literal l(ctx.get_bool_var(tmp));
ineq* cc = 0;
if (m_ineqs.find(l.var(), cc)) {
add_assign(*cc, m_ineq_literals, l);
}
#endif
}
}

2
src/smt/theory_pb.h
View file

@ -140,7 +140,7 @@ namespace smt {
unsigned m_num_marks;
unsigned m_conflict_lvl;
ineq m_lemma;
literal_vector m_antecedents;
literal_vector m_ineq_literals;
// bool_var |-> index into m_lemma
unsigned_vector m_conseq_index;