mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

debug output

Browse source
This commit is contained in:
Jakob Rath 2023-01-18 18:46:04 +01:00
parent 905144cdbb
commit 85a8d8b005
3 changed files with 19 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/clause_builder.cpp
View file

@ -69,6 +69,7 @@ namespace polysat {
if (c.is_always_false()) // filter out trivial constraints such as "4 < 2" if (c.is_always_false()) // filter out trivial constraints such as "4 < 2"
return; return;
if (c.is_always_true()) { if (c.is_always_true()) {
IF_VERBOSE(10, verbose_stream() << "Clause is tautology because of " << lit_pp(s(), c) << "\n");
m_is_tautology = true; m_is_tautology = true;
return; return;
} }

22
src/math/polysat/viable.cpp
View file

@ -1121,6 +1121,7 @@ namespace {
if (!added.contains(lit)) { if (!added.contains(lit)) {
added.insert(lit); added.insert(lit);
LOG("Adding " << lit_pp(s, lit)); LOG("Adding " << lit_pp(s, lit));
IF_VERBOSE(10, verbose_stream() << ";; " << lit_pp(s, lit) << "\n");
c.add_to_univariate_solver(v, s, *us, lit.to_uint()); c.add_to_univariate_solver(v, s, *us, lit.to_uint());
} }
e = e->next(); e = e->next();
@ -1147,6 +1148,7 @@ namespace {
if (added.contains(lit)) if (added.contains(lit))
continue; continue;
LOG("Adding " << lit_pp(s, lit)); LOG("Adding " << lit_pp(s, lit));
IF_VERBOSE(10, verbose_stream() << ";; " << lit_pp(s, lit) << "\n");
added.insert(lit); added.insert(lit);
cs[i].add_to_univariate_solver(v, s, *us, lit.to_uint()); cs[i].add_to_univariate_solver(v, s, *us, lit.to_uint());
} }
@ -1319,14 +1321,18 @@ namespace {
log(v); log(v);
} }
std::ostream& viable::display(std::ostream& out, pvar v, entry* e) const { std::ostream& viable::display_one(std::ostream& out, pvar v, entry const* e) const {
if (!e)
return out;
entry* first = e;
do {
if (e->coeff != 1) if (e->coeff != 1)
out << e->coeff << " * v" << v << " "; out << e->coeff << " * v" << v << " ";
out << e->interval << " " << e->side_cond << " " << e->src << "; "; out << e->interval << " " << e->side_cond << " " << e->src << "; ";
return out;
}
std::ostream& viable::display_all(std::ostream& out, pvar v, entry const* e) const {
if (!e)
return out;
entry const* first = e;
do {
display_one(out, v, e);
e = e->next(); e = e->next();
} }
while (e != first); while (e != first);
@ -1334,9 +1340,9 @@ namespace {
} }
std::ostream& viable::display(std::ostream& out, pvar v) const { std::ostream& viable::display(std::ostream& out, pvar v) const {
display(out, v, m_units[v]); display_all(out, v, m_units[v]);
display(out, v, m_equal_lin[v]); display_all(out, v, m_equal_lin[v]);
display(out, v, m_diseq_lin[v]); display_all(out, v, m_diseq_lin[v]);
return out; return out;
} }

7
src/math/polysat/viable.h
View file

@ -40,6 +40,8 @@ namespace polysat {
resource_out, resource_out,
}; };
std::ostream& operator<<(std::ostream& out, find_t x);
namespace viable_query { namespace viable_query {
enum class query_t { enum class query_t {
has_viable, // currently only used internally in resolve_viable has_viable, // currently only used internally in resolve_viable
@ -68,8 +70,6 @@ namespace polysat {
}; };
} }
std::ostream& operator<<(std::ostream& out, find_t x);
class viable { class viable {
friend class test_fi; friend class test_fi;
@ -99,7 +99,8 @@ namespace polysat {
bool refine_disequal_lin(pvar v, rational const& val); bool refine_disequal_lin(pvar v, rational const& val);
std::ostream& display(std::ostream& out, pvar v, entry* e) const; std::ostream& display_one(std::ostream& out, pvar v, entry const* e) const;
std::ostream& display_all(std::ostream& out, pvar v, entry const* e) const;
void insert(entry* e, pvar v, ptr_vector<entry>& entries, entry_kind k); void insert(entry* e, pvar v, ptr_vector<entry>& entries, entry_kind k);