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

add a display method

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-09-04 16:41:26 -10:00
parent 83019e3da5
commit 11be0c4ec5
1 changed files with 14 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/nlsat/levelwise.cpp
View file

@ -69,9 +69,20 @@ namespace nlsat {
init_property_relation();
}
// helper overload so callers can pass either raw poly* or polynomial_ref
unsigned max_var(poly* p) { return m_pm.max_var(p); }
unsigned max_var(polynomial_ref const & p) { return m_pm.max_var(p); }
// Helper to print out m_Q
void print_m_Q(std::ostream& out) const {
out << "m_Q: [\n";
for (const auto& pr : m_Q) {
display(out, pr);
out << "\n";
}
out << "]\n";
}
#ifdef Z3DEBUG
bool check_prop_init() {
@ -678,7 +689,7 @@ namespace nlsat {
void apply_pre(const property& p, bool has_repr) {
TRACE(levelwise,
tout << "apply_pre BEGIN m_Q:";
for (const auto& q : m_Q) { display(tout, q); tout << "; "; }
print_m_Q(tout);
tout << std::endl;
);
TRACE(levelwise, display(tout << "property p:", p) << std::endl;);
@ -692,7 +703,7 @@ namespace nlsat {
NOT_IMPLEMENTED_YET();
TRACE(levelwise,
tout << "apply_pre END m_Q:";
for (const auto& q : m_Q) { display(tout, q); tout << "; "; }
print_m_Q(tout);
tout << std::endl;
);
}
@ -743,7 +754,7 @@ namespace nlsat {
return "?";
}
std::ostream& display(std::ostream& out, const property & pr) {
std::ostream& display(std::ostream& out, const property & pr) const {
out << "{prop:" << prop_name(pr.prop_tag);
if (pr.level != -1) out << ", level:" << pr.level;
if (pr.s_idx != -1) out << ", s_idx:" << pr.s_idx;