mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

expose enode pp convenciences

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-11-18 09:53:20 -08:00
parent 1710fe4927
commit 5ab1afe5c2
1 changed files with 9 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/smt/smt_context.h
View file

@ -61,9 +61,16 @@ Revision History:
namespace smt { namespace smt {
class model_generator; class model_generator;
class context;
struct cancel_exception {}; struct cancel_exception {};
struct enode_pp {
context const& ctx;
enode* n;
enode_pp(enode* n, context const& ctx): ctx(ctx), n(n) {}
};
class context { class context {
friend class model_generator; friend class model_generator;
friend class lookahead; friend class lookahead;
@ -1368,6 +1375,8 @@ namespace smt {
void display_asserted_formulas(std::ostream & out) const; void display_asserted_formulas(std::ostream & out) const;
enode_pp pp(enode* n) { return enode_pp(n, *this); }
std::ostream& display_literal(std::ostream & out, literal l) const; std::ostream& display_literal(std::ostream & out, literal l) const;
std::ostream& display_detailed_literal(std::ostream & out, literal l) const { return smt::display(out, l, m, m_bool_var2expr.data()); } std::ostream& display_detailed_literal(std::ostream & out, literal l) const { return smt::display(out, l, m, m_bool_var2expr.data()); }
@ -1844,11 +1853,6 @@ namespace smt {
std::ostream& operator<<(std::ostream& out, enode_eq_pp const& p); std::ostream& operator<<(std::ostream& out, enode_eq_pp const& p);
struct enode_pp {
context const& ctx;
enode* n;
enode_pp(enode* n, context const& ctx): ctx(ctx), n(n) {}
};
std::ostream& operator<<(std::ostream& out, enode_pp const& p); std::ostream& operator<<(std::ostream& out, enode_pp const& p);