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

local updates

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-11-14 20:21:33 -08:00
parent 5921628f53
commit f9164f4cb1
1 changed files with 13 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/smt/theory_card.cpp
View file

@ -36,8 +36,12 @@ Notes:
That is, during a propagation, assignment or conflict resolution That is, during a propagation, assignment or conflict resolution
step track cutting-planes. step track cutting-planes.
- TBD: profile overhead of (re)creating sorting circuits. - TBD: profile overhead of (re)creating sorting circuits.
Possibly delay creating them until restart. Possibly delay creating them until restart.
- TBD: deal with integer overflows.
-
--*/ --*/
@ -376,6 +380,7 @@ namespace smt {
SASSERT(curr_max <= k); SASSERT(curr_max <= k);
add_clause(c, lits); add_clause(c, lits);
} }
// min + min_increment > k
else if (min == k && aval == l_true) { else if (min == k && aval == l_true) {
literal_vector& lits = get_lits(); literal_vector& lits = get_lits();
lits.push_back(~literal(abv)); lits.push_back(~literal(abv));
@ -384,6 +389,7 @@ namespace smt {
add_clause(c, lits); add_clause(c, lits);
} }
else { else {
// curr_min + min_increment > k
SASSERT(curr_min == k); SASSERT(curr_min == k);
for (unsigned i = 0; i < args.size(); ++i) { for (unsigned i = 0; i < args.size(); ++i) {
bool_var bv = args[i].first; bool_var bv = args[i].first;
@ -396,6 +402,7 @@ namespace smt {
} }
} }
} }
// k < max && ... ?
else if (max == k + 1 && aval == l_false) { else if (max == k + 1 && aval == l_false) {
literal_vector& lits = get_lits(); literal_vector& lits = get_lits();
lits.push_back(literal(abv)); lits.push_back(literal(abv));
@ -493,7 +500,8 @@ namespace smt {
literal internalize(card& ca, expr* e) { literal internalize(card& ca, expr* e) {
obj_map<expr, literal> cache; obj_map<expr, literal> cache;
for (unsigned i = 0; i < ca.m_args.size(); ++i) { for (unsigned i = 0; i < ca.m_args.size(); ++i) {
cache.insert(ca.m_app->get_arg(i), literal(ca.m_args[i].first)); bool_var bv = ca.m_args[i].first;
cache.insert(ctx.bool_var2expr(bv), literal(bv));
} }
cache.insert(m.mk_false(), false_literal); cache.insert(m.mk_false(), false_literal);
cache.insert(m.mk_true(), true_literal); cache.insert(m.mk_true(), true_literal);
@ -622,7 +630,7 @@ namespace smt {
SASSERT(m_util.is_at_most_k(a)); SASSERT(m_util.is_at_most_k(a));
literal atmostk; literal atmostk;
int k = m_util.get_k(a); int k = m_util.get_k(a);
unsigned num_args = a->get_num_args(); unsigned num_args = ca.m_args.size();
sort_expr se(*this); sort_expr se(*this);
if (k >= static_cast<int>(num_args)) { if (k >= static_cast<int>(num_args)) {
@ -635,7 +643,7 @@ namespace smt {
sorting_network<sort_expr> sn(se); sorting_network<sort_expr> sn(se);
expr_ref_vector in(m), out(m); expr_ref_vector in(m), out(m);
for (unsigned i = 0; i < num_args; ++i) { for (unsigned i = 0; i < num_args; ++i) {
in.push_back(c.m_app->get_arg(i)); in.push_back(ctx.bool_var2expr(c.m_args[i].first));
} }
sn(in, out); sn(in, out);
atmostk = ~se.internalize(c, out[k].get()); // k'th output is 0. atmostk = ~se.internalize(c, out[k].get()); // k'th output is 0.