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 
18 exprt interval_constraint(const exprt &expr, const integer_intervalt &interval);
19 
20 #endif // CPROVER_UTIL_INTERVAL_CONSTRAINT_H
exprt
Base class for all expressions.
Definition: expr.h:56
interval_templatet
Definition: interval_template.h:20
integer_interval.h
interval_constraint
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 ...
Definition: interval_constraint.cpp:12