nondet_bool.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Nondeterministic boolean helper
 
Author: Chris Smowton, chris@smowton.net
 
\*******************************************************************/
 
 
#ifndef CPROVER_UTIL_NONDET_BOOL_H
#define CPROVER_UTIL_NONDET_BOOL_H
 
#include "std_expr.h"
 
inline exprt
get_nondet_bool(const typet &type, const source_locationt &source_location)
{
  // We force this to 0 and 1 and won't consider
  // other values.
  return typecast_exprt(
    side_effect_expr_nondett(bool_typet(), source_location), type);
}
get_nondet_bool(const typet &type, const source_locationt &source_location) {…}
 
#endif // CPROVER_UTIL_NONDET_BOOL_H