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.
util
nondet_bool.h
Generated by
1.8.20