literal_expr.h

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_SOLVERS_PROP_LITERAL_EXPR_H
#define CPROVER_SOLVERS_PROP_LITERAL_EXPR_H
 
#include <util/std_expr.h>
 
#include "literal.h"
 
class literal_exprt:public predicate_exprt
{
public:
  explicit literal_exprt(literalt a):
    predicate_exprt(ID_literal)
  {
    set_literal(a);
  }
 
  literalt get_literal() const
  {
    literalt result;
    result.set(literalt::var_not(get_long_long(ID_literal)));
    return result;
  }
 
  void set_literal(literalt a)
  {
    set(ID_literal, a.get());
  }
};
 
template <>
inline bool can_cast_expr<literal_exprt>(const exprt &base)
{
  return base.id() == ID_literal;
}
 
inline void validate_expr(const literal_exprt &literal)
{
  DATA_INVARIANT(
    !literal.has_operands(), "literal expression should not have operands");
}

inline const literal_exprt &to_literal_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_literal);
  DATA_INVARIANT(
    !expr.has_operands(), "literal expression should not have operands");
  return static_cast<const literal_exprt &>(expr);
}

inline literal_exprt &to_literal_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_literal);
  DATA_INVARIANT(
    !expr.has_operands(), "literal expression should not have operands");
  return static_cast<literal_exprt &>(expr);
}
 
#endif // CPROVER_SOLVERS_PROP_LITERAL_EXPR_H