mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 19:51:22 +00:00
Code Activity

port Grobner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-16 17:12:53 -07:00
parent 3ec0fc2345
commit 451168a399
1 changed files with 22 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/math/lp/nla_grobner.h
View file

@ -46,9 +46,28 @@ class nla_grobner : common {
friend class nla_grobner; friend class nla_grobner;
equation() {} equation() {}
public: public:
unsigned get_num_monomials() const { return m_expr->size(); } unsigned get_num_monomials() const {
nex_mul* const * get_monomial(unsigned idx) const { NOT_IMPLEMENTED_YET(); switch(m_expr->type()) {
return nullptr; } 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; } nex* & exp() { return m_expr; }
const nex* exp() const { return m_expr; } const nex* exp() const { return m_expr; }
ci_dependency * get_dependency() const { return m_dep; } ci_dependency * get_dependency() const { return m_dep; }