mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
bug fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f698efa403
commit
f9f0b2221d
|
@ -26,6 +26,7 @@ Notes:
|
|||
#include"ast_pp.h"
|
||||
#include"lbool.h"
|
||||
#include"uint_set.h"
|
||||
#include"gparams.h"
|
||||
|
||||
const unsigned g_primes[7] = { 2, 3, 5, 7, 11, 13, 17};
|
||||
|
||||
|
@ -819,7 +820,9 @@ struct pb2bv_rewriter::imp {
|
|||
return
|
||||
p.get_bool("keep_cardinality_constraints", false) ||
|
||||
p.get_bool("sat.cardinality.solver", false) ||
|
||||
p.get_bool("cardinality.solver", false) || keep_pb();
|
||||
p.get_bool("cardinality.solver", false) ||
|
||||
gparams::get_module("sat").get_bool("cardinality.solver", false) ||
|
||||
keep_pb();
|
||||
}
|
||||
|
||||
bool keep_pb() const {
|
||||
|
@ -827,7 +830,8 @@ struct pb2bv_rewriter::imp {
|
|||
return
|
||||
p.get_bool("keep_pb_constraints", false) ||
|
||||
p.get_bool("sat.pb.solver", false) ||
|
||||
p.get_bool("pb.solver", false);
|
||||
p.get_bool("pb.solver", false) ||
|
||||
gparams::get_module("sat").get_bool("pb.solver", false);
|
||||
}
|
||||
|
||||
bool pb_num_system() const {
|
||||
|
|
|
@ -1025,7 +1025,6 @@ namespace sat {
|
|||
|
||||
m_lemma.reset();
|
||||
|
||||
#if 1
|
||||
m_lemma.push_back(null_literal);
|
||||
for (unsigned i = 0; 0 <= slack && i < m_active_vars.size(); ++i) {
|
||||
bool_var v = m_active_vars[i];
|
||||
|
@ -1048,6 +1047,7 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
#if 0
|
||||
if (jus.size() > 1) {
|
||||
std::cout << jus.size() << "\n";
|
||||
for (unsigned i = 0; i < jus.size(); ++i) {
|
||||
|
@ -1057,6 +1057,7 @@ namespace sat {
|
|||
active2pb(m_A);
|
||||
display(std::cout, m_A);
|
||||
}
|
||||
#endif
|
||||
|
||||
|
||||
if (slack >= 0) {
|
||||
|
@ -1067,7 +1068,7 @@ namespace sat {
|
|||
if (m_lemma[0] == null_literal) {
|
||||
m_lemma[0] = m_lemma.back();
|
||||
m_lemma.pop_back();
|
||||
unsigned level = lvl(m_lemma[0]);
|
||||
unsigned level = m_lemma.empty() ? 0 : lvl(m_lemma[0]);
|
||||
for (unsigned i = 1; i < m_lemma.size(); ++i) {
|
||||
if (lvl(m_lemma[i]) > level) {
|
||||
level = lvl(m_lemma[i]);
|
||||
|
@ -1076,37 +1077,6 @@ namespace sat {
|
|||
}
|
||||
IF_VERBOSE(2, verbose_stream() << "(sat.card set level to " << level << " < " << m_conflict_lvl << ")\n";);
|
||||
}
|
||||
#else
|
||||
++idx;
|
||||
while (0 <= slack) {
|
||||
literal lit = lits[idx];
|
||||
bool_var v = lit.var();
|
||||
if (m_active_var_set.contains(v)) {
|
||||
int coeff = get_coeff(v);
|
||||
if (coeff < 0 && !lit.sign()) {
|
||||
slack += coeff;
|
||||
m_lemma.push_back(~lit);
|
||||
}
|
||||
else if (coeff > 0 && lit.sign()) {
|
||||
slack -= coeff;
|
||||
m_lemma.push_back(~lit);
|
||||
}
|
||||
}
|
||||
if (idx == 0 && slack >= 0) {
|
||||
IF_VERBOSE(2, verbose_stream() << "(sat.card non-asserting)\n";);
|
||||
goto bail_out;
|
||||
}
|
||||
SASSERT(idx > 0 || slack < 0);
|
||||
--idx;
|
||||
}
|
||||
if (m_lemma.size() >= 2 && lvl(m_lemma[1]) == m_conflict_lvl) {
|
||||
// TRACE("sat", tout << "Bail out on no progress " << lit << "\n";);
|
||||
IF_VERBOSE(2, verbose_stream() << "(sat.card bail non-asserting resolvent)\n";);
|
||||
goto bail_out;
|
||||
}
|
||||
|
||||
#endif
|
||||
|
||||
|
||||
SASSERT(slack < 0);
|
||||
|
||||
|
@ -1118,7 +1088,7 @@ namespace sat {
|
|||
svector<drat::premise> ps; // TBD fill in
|
||||
s().m_drat.add(m_lemma, ps);
|
||||
}
|
||||
|
||||
|
||||
s().m_lemma.reset();
|
||||
s().m_lemma.append(m_lemma);
|
||||
for (unsigned i = 1; i < m_lemma.size(); ++i) {
|
||||
|
|
|
@ -1937,23 +1937,25 @@ namespace sat {
|
|||
void solver::learn_lemma_and_backjump() {
|
||||
TRACE("sat_lemma", tout << "new lemma size: " << m_lemma.size() << "\n" << m_lemma << "\n";);
|
||||
|
||||
if (m_config.m_minimize_lemmas) {
|
||||
minimize_lemma();
|
||||
reset_lemma_var_marks();
|
||||
if (m_config.m_dyn_sub_res)
|
||||
dyn_sub_res();
|
||||
TRACE("sat_lemma", tout << "new lemma (after minimization) size: " << m_lemma.size() << "\n" << m_lemma << "\n";);
|
||||
}
|
||||
else
|
||||
reset_lemma_var_marks();
|
||||
|
||||
literal_vector::iterator it = m_lemma.begin();
|
||||
literal_vector::iterator end = m_lemma.end();
|
||||
unsigned new_scope_lvl = 0;
|
||||
++it;
|
||||
for(; it != end; ++it) {
|
||||
bool_var var = (*it).var();
|
||||
new_scope_lvl = std::max(new_scope_lvl, lvl(var));
|
||||
if (!m_lemma.empty()) {
|
||||
if (m_config.m_minimize_lemmas) {
|
||||
minimize_lemma();
|
||||
reset_lemma_var_marks();
|
||||
if (m_config.m_dyn_sub_res)
|
||||
dyn_sub_res();
|
||||
TRACE("sat_lemma", tout << "new lemma (after minimization) size: " << m_lemma.size() << "\n" << m_lemma << "\n";);
|
||||
}
|
||||
else
|
||||
reset_lemma_var_marks();
|
||||
|
||||
literal_vector::iterator it = m_lemma.begin();
|
||||
literal_vector::iterator end = m_lemma.end();
|
||||
++it;
|
||||
for(; it != end; ++it) {
|
||||
bool_var var = (*it).var();
|
||||
new_scope_lvl = std::max(new_scope_lvl, lvl(var));
|
||||
}
|
||||
}
|
||||
|
||||
unsigned glue = num_diff_levels(m_lemma.size(), m_lemma.c_ptr());
|
||||
|
@ -2389,6 +2391,7 @@ namespace sat {
|
|||
assigned at level 0.
|
||||
*/
|
||||
void solver::minimize_lemma() {
|
||||
SASSERT(!m_lemma.empty());
|
||||
SASSERT(m_unmark.empty());
|
||||
//m_unmark.reset();
|
||||
updt_lemma_lvl_set();
|
||||
|
|
Loading…
Reference in a new issue