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

debug messages and gating

Browse source
This commit is contained in:
Simon Cruanes 2017-12-14 20:17:02 +01:00
parent 3b4718b99a
commit b877bd8286
1 changed files with 13 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/smt/theory_recfun.cpp
View file

@ -4,6 +4,8 @@
#include "smt/theory_recfun.h" #include "smt/theory_recfun.h"
#include "smt/params/smt_params_helper.hpp" #include "smt/params/smt_params_helper.hpp"
#ifdef Z3DEBUG
#define DEBUG(x) TRACE("recfun", tout << x << '\n';) #define DEBUG(x) TRACE("recfun", tout << x << '\n';)
struct pp_lit { struct pp_lit {
@ -17,7 +19,6 @@ std::ostream & operator<<(std::ostream & out, pp_lit const & pp) {
return out; return out;
} }
// NOTE: debug
struct pp_lits { struct pp_lits {
smt::context & ctx; smt::context & ctx;
smt::literal *lits; smt::literal *lits;
@ -35,6 +36,14 @@ std::ostream & operator<<(std::ostream & out, pp_lits const & pp) {
return out << "}"; return out << "}";
} }
#else
#define DEBUG(x) do{}while(0)
#endif
namespace smt { namespace smt {
theory_recfun::theory_recfun(ast_manager & m) theory_recfun::theory_recfun(ast_manager & m)
@ -147,6 +156,7 @@ namespace smt {
context & ctx = get_context(); context & ctx = get_context();
for (literal_vector & c : m_q_clauses) { for (literal_vector & c : m_q_clauses) {
DEBUG("add axiom " << pp_lits(ctx, c.size(), c.c_ptr()));
ctx.mk_th_axiom(get_id(), c.size(), c.c_ptr()); ctx.mk_th_axiom(get_id(), c.size(), c.c_ptr());
} }
m_q_clauses.clear(); m_q_clauses.clear();
@ -379,6 +389,7 @@ namespace smt {
st.update("recfun body expansion", m_stats.m_body_expansions); st.update("recfun body expansion", m_stats.m_body_expansions);
} }
#ifdef Z3DEBUG
std::ostream& operator<<(std::ostream & out, theory_recfun::pp_case_expansion const & e) { std::ostream& operator<<(std::ostream & out, theory_recfun::pp_case_expansion const & e) {
return out << "case_exp(" << mk_pp(e.e.m_lhs, e.m) << ")"; return out << "case_exp(" << mk_pp(e.e.m_lhs, e.m) << ")";
} }
@ -390,4 +401,5 @@ namespace smt {
} }
return out << ")"; return out << ")";
} }
#endif
} }