cprover
nondet_bool.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Nondeterministic boolean helper
4 
5 Author: 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 #include "std_types.h"
17 
21 inline exprt
22 get_nondet_bool(const typet &type, const source_locationt &source_location)
23 {
24  // We force this to 0 and 1 and won't consider
25  // other values.
26  return typecast_exprt(
27  side_effect_expr_nondett(bool_typet(), source_location), type);
28 }
29 
30 #endif // CPROVER_UTIL_NONDET_BOOL_H
The Boolean type.
Definition: std_types.h:37
Base class for all expressions.
Definition: expr.h:54
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1968
Semantic type conversion.
Definition: std_expr.h:1781
The type of an expression, extends irept.
Definition: type.h:28
exprt get_nondet_bool(const typet &type, const source_locationt &source_location)
Definition: nondet_bool.h:22
API to expression classes.
Pre-defined types.