mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

#5429

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-30 13:42:22 -07:00
parent 5ca8628e0d
commit f3f83d0445
5 changed files with 34 additions and 42 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

61
src/sat/sat_drat.cpp
View file

@ -37,9 +37,8 @@ namespace sat {
if (s.get_config().m_drat && s.get_config().m_drat_file.is_non_empty_string()) {
auto mode = s.get_config().m_drat_binary ? (std::ios_base::binary | std::ios_base::out | std::ios_base::trunc) : std::ios_base::out;
m_out = alloc(std::ofstream, s.get_config().m_drat_file.str(), mode);
if (s.get_config().m_drat_binary) {
std::swap(m_out, m_bout);
}
if (s.get_config().m_drat_binary)
std::swap(m_out, m_bout);
}
}
@ -50,9 +49,8 @@ namespace sat {
dealloc(m_bout);
for (unsigned i = 0; i < m_proof.size(); ++i) {
clause* c = m_proof[i];
if (c) {
m_alloc.del_clause(c);
}
if (c)
m_alloc.del_clause(c);
}
m_proof.reset();
m_out = nullptr;
@ -93,6 +91,7 @@ namespace sat {
unsigned len = 0;
if (st.is_deleted()) {
buffer[len++] = 'd';
buffer[len++] = ' ';
@ -133,7 +132,7 @@ namespace sat {
memcpy(buffer + len, d, lastd - d);
len += static_cast<unsigned>(lastd - d);
buffer[len++] = ' ';
if (len + 50 > sizeof(buffer)) {
if (static_cast<size_t>(len) + 50 > sizeof(buffer)) {
m_out->write(buffer, len);
len = 0;
}
@ -208,15 +207,14 @@ namespace sat {
declare(l);
IF_VERBOSE(20, trace(verbose_stream(), 1, &l, st););
if (st.is_redundant() && st.is_sat()) {
if (st.is_redundant() && st.is_sat())
verify(1, &l);
}
if (st.is_deleted()) {
if (st.is_deleted())
return;
}
if (m_check_unsat) {
assign_propagate(l);
}
if (m_check_unsat)
assign_propagate(l);
m_units.push_back(l);
}
@ -233,9 +231,9 @@ namespace sat {
// don't record binary as deleted.
}
else {
if (st.is_redundant() && st.is_sat()) {
if (st.is_redundant() && st.is_sat())
verify(2, lits);
}
clause* c = m_alloc.mk_clause(2, lits, st.is_redundant());
m_proof.push_back(c);
m_status.push_back(st);
@ -245,15 +243,12 @@ namespace sat {
m_watches[(~l1).index()].push_back(idx);
m_watches[(~l2).index()].push_back(idx);
if (value(l1) == l_false && value(l2) == l_false) {
m_inconsistent = true;
}
else if (value(l1) == l_false) {
assign_propagate(l2);
}
else if (value(l2) == l_false) {
assign_propagate(l1);
}
if (value(l1) == l_false && value(l2) == l_false)
m_inconsistent = true;
else if (value(l1) == l_false)
assign_propagate(l2);
else if (value(l2) == l_false)
assign_propagate(l1);
}
}
@ -403,16 +398,14 @@ namespace sat {
if (n == 0)
return false;
unsigned num_units = m_units.size();
for (unsigned i = 0; !m_inconsistent && i < n; ++i) {
for (unsigned i = 0; !m_inconsistent && i < n; ++i)
assign_propagate(~c[i]);
}
if (!m_inconsistent) {
DEBUG_CODE(validate_propagation(););
}
DEBUG_CODE(if (!m_inconsistent) validate_propagation(););
DEBUG_CODE(
for (literal u : m_units) {
for (literal u : m_units)
SASSERT(m_assignment[u.var()] != l_undef);
});
);
#if 0
if (!m_inconsistent) {
@ -465,9 +458,9 @@ namespace sat {
}
#endif
for (unsigned i = num_units; i < m_units.size(); ++i) {
for (unsigned i = num_units; i < m_units.size(); ++i)
m_assignment[m_units[i].var()] = l_undef;
}
m_units.shrink(num_units);
bool ok = m_inconsistent;
m_inconsistent = false;

3
src/sat/sat_solver.cpp
View file

@ -1304,7 +1304,8 @@ namespace sat {
flet<bool> _searching(m_searching, true);
m_clone = nullptr;
if (m_mc.empty() && gparams::get_ref().get_bool("model_validate", false)) {
m_clone = alloc(solver, m_params, m_rlimit);
m_clone = alloc(solver, m_no_drat_params, m_rlimit);
m_clone->copy(*this);
m_clone->set_extension(nullptr);
}

5
src/sat/sat_solver.h
View file

@ -82,6 +82,10 @@ namespace sat {
void reset();
void collect_statistics(statistics & st) const;
};
struct no_drat_params : public params_ref {
no_drat_params() { set_sym("drat.file", symbol()); }
};
class solver : public solver_core {
public:
@ -183,6 +187,7 @@ namespace sat {
scoped_limit_trail m_vars_lim;
stopwatch m_stopwatch;
params_ref m_params;
no_drat_params m_no_drat_params;
scoped_ptr<solver> m_clone; // for debugging purposes
literal_vector m_assumptions; // additional assumptions during check
literal_set m_assumption_set; // set of enabled assumptions

4
src/sat/smt/sat_dual_solver.cpp
View file

@ -18,10 +18,6 @@ Author:
namespace sat {
dual_solver::no_drat_params::no_drat_params() {
set_sym("drat.file", symbol());
}
dual_solver::dual_solver(reslimit& l):
m_solver(m_params, l)
{

3
src/sat/smt/sat_dual_solver.h
View file

@ -23,9 +23,6 @@ Author:
namespace sat {
class dual_solver {
struct no_drat_params : public params_ref {
no_drat_params();
};
no_drat_params m_params;
solver m_solver;
lim_svector<literal> m_units, m_roots;