diff options
Diffstat (limited to 'src/expr/expr_manager_template.h')
-rw-r--r-- | src/expr/expr_manager_template.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 2fabea0ff..8acb7489f 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -139,6 +139,9 @@ public: /** Get the type for integers */ IntegerType integerType() const; + /** Get the type for rounding modes */ + RoundingModeType roundingModeType() const; + /** * Make a unary expression of a given kind (NOT, BVNOT, ...). * @param kind the kind of expression @@ -361,6 +364,9 @@ public: */ SExprType mkSExprType(const std::vector<Type>& types); + /** Make a type representing a floating-point type with the given parameters. */ + FloatingPointType mkFloatingPointType(unsigned exp, unsigned sig) const; + /** Make a type representing a bit-vector of the given size. */ BitVectorType mkBitVectorType(unsigned size) const; |