cprover
Loading...
Searching...
No Matches
nondet_bool.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Nondeterministic boolean helper
4
5Author: Chris Smowton, chris@smowton.net
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_UTIL_NONDET_BOOL_H
13#define CPROVER_UTIL_NONDET_BOOL_H
14
15#include "std_expr.h"
16
20inline exprt
21get_nondet_bool(const typet &type, const source_locationt &source_location)
22{
23 // We force this to 0 and 1 and won't consider
24 // other values.
25 return typecast_exprt(
26 side_effect_expr_nondett(bool_typet(), source_location), type);
27}
28
29#endif // CPROVER_UTIL_NONDET_BOOL_H
bool_typet
The Boolean type.
Definition std_types.h:36
exprt
Base class for all expressions.
Definition expr.h:57
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
source_locationt
Definition source_location.h:20
typecast_exprt
Semantic type conversion.
Definition std_expr.h:1985
typet
The type of an expression, extends irept.
Definition type.h:29
get_nondet_bool
exprt get_nondet_bool(const typet &type, const source_locationt &source_location)
Definition nondet_bool.h:21
std_expr.h
API to expression classes.