30 for(std::vector<monomialt>::iterator m_it=
monomials.begin();
34 for(std::vector<monomialt::termt>::iterator t_it=m_it->terms.begin();
35 t_it!=m_it->terms.end();
40 itype=t_it->var.type();
49 for(std::vector<monomialt>::iterator m_it=
monomials.begin();
53 int coeff=m_it->coeff;
64 for(std::vector<monomialt::termt>::iterator t_it=m_it->terms.begin();
65 t_it!=m_it->terms.end();
68 for(
unsigned int i=0; i < t_it->exp; i++)
103 if(expr.
id()==ID_symbol)
109 term.
var=symbol_expr;
111 monomial.
terms.push_back(term);
116 else if(expr.
id()==ID_plus ||
117 expr.
id()==ID_minus ||
125 if(expr.
id()==ID_minus)
130 else if(expr.
id()==ID_plus)
134 else if(expr.
id()==ID_mult)
139 else if(expr.
id()==ID_constant)
153 else if(expr.
id()==ID_typecast)
163 throw "couldn't polynomialize";
169 for(std::vector<monomialt>::iterator m_it=
monomials.begin();
173 for(std::vector<monomialt::termt>::iterator t_it=m_it->terms.begin();
174 t_it!=m_it->terms.end();
177 if(substitution.find(t_it->var)!=substitution.end())
191 std::vector<monomialt>::iterator it, jt;
192 std::vector<monomialt> new_monomials;
201 int res=it->compare(*jt);
207 new_monomial.
coeff += jt->coeff;
209 if(new_monomial.
coeff!=0)
211 new_monomials.push_back(new_monomial);
221 new_monomials.push_back(*it);
226 new_monomials.push_back(*jt);
237 new_monomials.push_back(*it);
243 new_monomials.push_back(*jt);
262 for(std::vector<monomialt>::iterator it=
monomials.begin();
272 std::vector<monomialt> my_monomials=
monomials;
275 for(std::vector<monomialt>::iterator it=my_monomials.begin();
276 it!=my_monomials.end();
279 for(std::vector<monomialt>::iterator jt=other.
monomials.begin();
285 product.
coeff=it->coeff * jt->coeff;
293 std::vector<monomialt::termt>::iterator t1, t2;
295 t1=it->terms.begin();
296 t2=jt->terms.begin();
298 while(t1!=it->terms.end() && t2 != jt->terms.end())
301 int res=t1->var.compare(t2->var);
307 term.
exp=t1->exp + t2->exp;
325 product.
terms.push_back(term);
330 while(t1!=it->terms.end())
332 product.
terms.push_back(*t1);
336 while(t2!=jt->terms.end())
338 product.
terms.push_back(*t2);
352 std::vector<termt>::iterator it, jt;
355 jt=other.
terms.begin();
359 while(it!=
terms.end() && jt != other.
terms.end())
361 unsigned int e1=it->exp;
362 unsigned int e2=it->exp;
363 int res=it->var.compare(jt->var);
377 assert(it->var==jt->var);
397 if(it==
terms.end() && jt == other.
terms.end())
402 else if(it!=
terms.end() && jt == other.
terms.end())
407 else if(it==
terms.end() && jt != other.
terms.end())
412 assert(!
"NOTREACHEDBITCHES");
420 for(std::vector<monomialt>::iterator it=
monomials.begin();
424 if(it->contains(var))
426 maxd=std::max(maxd, it->degree());
446 for(std::vector<monomialt>::iterator it=
monomials.begin();
467 for(std::vector<termt>::iterator it=
terms.begin();
480 if(var.
id()!=ID_symbol)
486 for(std::vector<termt>::iterator it=
terms.begin();
The type of an expression.
void substitute(substitutiont &substitution)
const irep_idt & get_value() const
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
A constant literal expression.
std::vector< termt > terms
const irep_idt & id() const
API to expression classes.
typet join_types(const typet &t1, const typet &t2)
Return the smallest type that both t1 and t2 can be cast to without losing information.
The unary minus expression.
int max_degree(const exprt &var)
bool contains(const exprt &var)
int coeff(const exprt &expr)
void from_expr(const exprt &expr)
Base class for all expressions.
std::map< exprt, exprt > substitutiont
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
int compare(monomialt &other)
void add(polynomialt &other)
Expression to hold a symbol (variable)
const char * c_str() const
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
std::vector< monomialt > monomials