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 
20 inline exprt get_nondet_bool(const typet &type)
21 {
22  // We force this to 0 and 1 and won't consider
23  // other values.
25 }
26 
27 #endif // CPROVER_UTIL_NONDET_BOOL_H
The type of an expression.
Definition: type.h:22
semantic type conversion
Definition: std_expr.h:2111
The proper Booleans.
Definition: std_types.h:34
exprt get_nondet_bool(const typet &type)
Definition: nondet_bool.h:20
API to expression classes.
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
API to type classes.
Base class for all expressions.
Definition: expr.h:42