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
typet
The type of an expression, extends irept.
Definition: type.h:29
exprt
Base class for all expressions.
Definition: expr.h:53
bool_typet
The Boolean type.
Definition: std_types.h:37
std_types.h
Pre-defined types.
source_locationt
Definition: source_location.h:20
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
get_nondet_bool
exprt get_nondet_bool(const typet &type, const source_locationt &source_location)
Definition: nondet_bool.h:22
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
std_expr.h
API to expression classes.