mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
small change in factor to support TRACE
This commit is contained in:
parent
a932e596eb
commit
eb817f779d
|
@ -35,8 +35,7 @@ class factor {
|
|||
bool m_sign{ false };
|
||||
public:
|
||||
factor(): factor(false) {}
|
||||
explicit factor(bool sign): m_sign(sign) {}
|
||||
factor(lpvar var): m_var(var), m_type(factor_type::VAR), m_sign(false) {}
|
||||
explicit factor(lpvar var): m_var(var), m_type(factor_type::VAR), m_sign(false) {}
|
||||
explicit factor(lpvar v, factor_type t) : m_var(v), m_type(t), m_sign(false) {}
|
||||
unsigned var() const { return m_var; }
|
||||
factor_type type() const { return m_type; }
|
||||
|
|
|
@ -232,6 +232,7 @@ public:
|
|||
|
||||
std::ostream & print_factor(const factor& f, std::ostream& out) const;
|
||||
std::ostream & print_factor_with_vars(const factor& f, std::ostream& out) const;
|
||||
std::ostream & print_factor_with_vars(lpvar j, std::ostream& out) const { return print_var(j, out); }
|
||||
std::ostream& print_monic(const monic& m, std::ostream& out) const;
|
||||
std::ostream& print_bfc(const factorization& m, std::ostream& out) const;
|
||||
std::ostream& print_monic_with_vars(unsigned i, std::ostream& out) const;
|
||||
|
|
Loading…
Reference in a new issue