threeval.h

Go to the documentation of this file.

#ifndef CPROVER_THREEVAL_H
#define CPROVER_THREEVAL_H
#include <ostream>
 
//
// three valued logic
//
 
class tvt
{
public:
  typedef enum
  {
    TV_FALSE,
    TV_UNKNOWN,
    TV_TRUE
  } tv_enumt;
 
  bool is_true() const
  {
    return value == TV_TRUE;
  }
  bool is_false() const
  {
    return value == TV_FALSE;
  }
  bool is_unknown() const
  {
    return value == TV_UNKNOWN;
  }
  bool is_known() const
  {
    return value == TV_TRUE || value == TV_FALSE;
  }
 
  const char *to_string() const;
 
  tv_enumt get_value() const
  {
    return value;
  }
 
  tvt() = default;
 
  explicit tvt(bool b) : value(b ? TV_TRUE : TV_FALSE)
  {
  }
 
  explicit tvt(tv_enumt v) : value(v)
  {
  }
 
  tvt invert()
  {
    if (value == TV_TRUE)
      return tvt(TV_FALSE);
    if (value == TV_FALSE)
      return tvt(TV_TRUE);
 
    return tvt(value);
  }
 
  friend bool operator==(const tvt a, const tvt b)
  {
    return a.value == b.value;
  }
 
  friend bool operator!=(const tvt a, const tvt b)
  {
    return a.value != b.value;
  }
 
  friend tvt operator&&(const tvt a, const tvt b)
  {
    if (a.value == TV_FALSE || b.value == TV_FALSE)
      return tvt(TV_FALSE);
    if (a.value == TV_TRUE && b.value == TV_TRUE)
      return tvt(TV_TRUE);
    return tvt(TV_UNKNOWN);
  }
 
  friend tvt operator||(const tvt a, const tvt b)
  {
    if (a.value == TV_TRUE || b.value == TV_TRUE)
      return tvt(TV_TRUE);
    if (a.value == TV_FALSE && b.value == TV_FALSE)
      return tvt(TV_FALSE);
    return tvt(TV_UNKNOWN);
  }
 
  friend tvt operator!(const tvt a)
  {
    if (a.value == TV_UNKNOWN)
      return tvt(TV_UNKNOWN);
    if (a.value == TV_TRUE)
      return tvt(TV_FALSE);
    return tvt(TV_TRUE);
  }
 
  friend std::ostream &operator<<(std::ostream &out, const tvt &a)
  {
    return out << a.to_string();
  }
 
protected:
  tv_enumt value;
};
 
#endif