expr_lowering.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Lower expressions to arithmetic and logic expressions
 
Author: Michael Tautschnig
 
\*******************************************************************/
 
#ifndef CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H
#define CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H
 
#include <util/expr.h>
 
class byte_extract_exprt;
class byte_update_exprt;
class namespacet;
 
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns);
 
exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns);
 
exprt lower_byte_operators(const exprt &src, const namespacet &ns);
 
bool has_byte_operator(const exprt &src);
 
#endif /* CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H */