mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-30 12:25:51 +00:00
Code Activity

adjust trace output

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-06-29 08:19:52 -07:00
parent 5afcb489e0
commit ff265235c1
2 changed files with 7 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/grobner/grobner.cpp
View file

@ -116,10 +116,13 @@ void grobner::reset() {
}
void grobner::display_var(std::ostream & out, expr * var) const {
out << "#" << var->get_id();
#if 0
if (is_app(var) && to_app(var)->get_num_args() > 0)
out << mk_bounded_pp(var, m_manager);
else
out << mk_pp(var, m_manager);
#endif
}
void grobner::display_vars(std::ostream & out, unsigned num_vars, expr * const * vars) const {

7
src/smt/theory_arith_nl.h
View file

@ -2154,13 +2154,14 @@ void theory_arith<Ext>::set_gb_exhausted() {
// Scan the grobner basis eqs, and look for inconsistencies.
template<typename Ext>
bool theory_arith<Ext>::get_gb_eqs_and_look_for_conflict(ptr_vector<grobner::equation>& eqs, grobner& gb) {
TRACE("grobner", );
eqs.reset();
gb.get_equations(eqs);
TRACE("grobner_bug", tout << "after gb\n";);
TRACE("grobner", tout << "after gb\n";
for (grobner::equation* eq : eqs)
gb.display_equation(tout, *eq);
);
for (grobner::equation* eq : eqs) {
TRACE("grobner_bug", gb.display_equation(tout, *eq););
if (is_inconsistent(eq, gb) || is_inconsistent2(eq, gb)) {
TRACE("grobner", tout << "inconsistent: "; gb.display_equation(tout, *eq););
return true;