CBMC
interval_constraint.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Interval constraint
4 
5 Author: Jeannie Moulton
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_INTERVAL_CONSTRAINT_H
10 #define CPROVER_UTIL_INTERVAL_CONSTRAINT_H
11 
12 #include "integer_interval.h"
13 
14 class exprt;
15 
19 
20 #endif // CPROVER_UTIL_INTERVAL_CONSTRAINT_H
Base class for all expressions.
Definition: expr.h:56
exprt interval_constraint(const exprt &expr, const integer_intervalt &interval)
Given an exprt and an integer interval return an exprt that represents restricting the expression to ...