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

Fixed collect_param_descrs in pb2bv tactic.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-06-08 15:36:00 +01:00
parent 3e1042c680
commit 24a5ff825a
1 changed files with 7 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/tactic/arith/pb2bv_tactic.cpp
View file

@ -854,7 +854,7 @@ private:
m_temporary_ints(m),
m_used_dependencies(m),
m_rw(*this) {
updt_params(p);
updt_params(p);
m_b_rw.set_flat(false); // no flattening otherwise will blowup the memory
m_b_rw.set_elim_and(true);
}
@ -871,12 +871,17 @@ private:
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_all_clauses_limit = p.get_uint("pb2bv_all_clauses_limit", 8);
m_cardinality_limit = p.get_uint("pb2bv_cardinality_limit", UINT_MAX);
m_b_rw.updt_params(p);
}
void collect_param_descrs(param_descrs & r) {
insert_max_memory(r);
insert_max_memory(r);
r.insert("pb2bv_all_clauses_limit", CPK_UINT, "(default: 8) maximum number of literals for using equivalent CNF encoding of PB constraint.");
r.insert("pb2bv_cardinality_limit", CPK_UINT, "(default: inf) limit for using arc-consistent cardinality constraint encoding.");
m_b_rw.get_param_descrs(r);
r.erase("flat");
r.erase("elim_and");
}
void set_cancel(bool f) {