From 451168a3996c7e7012b53a6c553ab761aecbeb30 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 16 Oct 2019 17:12:53 -0700 Subject: [PATCH] port Grobner Signed-off-by: Lev Nachmanson --- src/math/lp/nla_grobner.h | 25 ++++++++++++++++++++++--- 1 file changed, 22 insertions(+), 3 deletions(-) diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 519a419c9..15d1e3d1d 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -46,9 +46,28 @@ class nla_grobner : common { friend class nla_grobner; equation() {} public: - unsigned get_num_monomials() const { return m_expr->size(); } - nex_mul* const * get_monomial(unsigned idx) const { NOT_IMPLEMENTED_YET(); - return nullptr; } + unsigned get_num_monomials() const { + switch(m_expr->type()) { + case expr_type::VAR: + case expr_type::SCALAR: return 0; + case expr_type::MUL: return 1; + case expr_type::SUM: return m_expr->size(); + default: return 0; + } + } + // can return not a nex_mul + nex* get_monomial(unsigned idx) const { + switch(m_expr->type()) { + case expr_type::VAR: + case expr_type::SCALAR: UNREACHABLE();; + case expr_type::MUL: + SASSERT(idx == 0); + return m_expr; + case expr_type::SUM: + return (*to_sum(m_expr))[idx]; + default: return 0; + } +} nex* & exp() { return m_expr; } const nex* exp() const { return m_expr; } ci_dependency * get_dependency() const { return m_dep; }