CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
interval_constraint.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Interval constraint
4
5Author: 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
14class 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 ...