mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

add pb capabilities

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-11-09 16:19:49 -08:00
parent 3e8c7d85aa
commit e412d6175d
3 changed files with 18 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/card_decl_plugin.cpp
View file

@ -107,6 +107,9 @@ bool card_util::is_le(app* a, int& k) const {
}
int card_util::get_le_coeff(app* a, unsigned index) {
if (is_at_most_k(a)) {
return 1;
}
SASSERT(is_le(a));
SASSERT(1 + index < a->get_decl()->get_num_parameters());
return a->get_decl()->get_parameter(index + 1).get_int();

21
src/smt/theory_card.cpp
View file

@ -63,8 +63,8 @@ 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));
unsigned k = m_util.get_k(atom);
SASSERT(m_util.is_at_most_k(atom) || m_util.is_le(atom));
int k = m_util.get_k(atom);
if (ctx.b_internalized(atom)) {
@ -78,10 +78,16 @@ namespace smt {
SASSERT(!ctx.b_internalized(atom));
bool_var abv = ctx.mk_bool_var(atom);
if (k >= atom->get_num_args()) {
literal lit(abv);
ctx.mk_th_axiom(get_id(), 1, &lit);
return true;
if (k >= static_cast<int>(num_args)) {
bool all_pos = true;
for (unsigned i = 0; all_pos && i < num_args; ++i) {
all_pos = 0 < m_util.get_le_coeff(atom, i);
}
if (all_pos) {
literal lit(abv);
ctx.mk_th_axiom(get_id(), 1, &lit);
return true;
}
}
card* c = alloc(card, abv, k);
@ -118,7 +124,8 @@ namespace smt {
ctx.mk_th_axiom(get_id(), 1, &lit);
ctx.mark_as_relevant(tmp);
}
c->m_args.push_back(std::make_pair(bv,1));
int coeff = m_util.get_le_coeff(atom, i);
c->m_args.push_back(std::make_pair(bv, coeff));
}
add_card(c);
return true;

2
src/smt/theory_card.h
View file

@ -43,7 +43,7 @@ namespace smt {
int m_abs_min;
int m_abs_max;
arg_t m_args;
card(bool_var bv, unsigned k):
card(bool_var bv, int k):
m_k(k), m_bv(bv)
{}
};