replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

smt2_format can now format symbols and constants

This commit is contained in:
Daniel Kroening 2018-11-24 21:24:32 +00:00
parent 449a3f920f
commit d5db868770
2 changed files with 71 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

58
src/solvers/smt2/smt2_format.cpp
View File

@ -8,20 +8,64 @@ Author: Daniel Kroening, kroening@kroening.com
#include "smt2_format.h"
#include <util/arith_tools.h>
#include <util/std_expr.h>
#include <util/std_types.h>
std::ostream &operator<<(std::ostream &out, const smt2_format &f)
std::ostream &smt2_format_rec(std::ostream &out, const typet &type)
{
if(f.type.id() == ID_unsignedbv)
out << "(_ BitVec " << to_unsignedbv_type(f.type).get_width() << ')';
else if(f.type.id() == ID_bool)
if(type.id() == ID_unsignedbv)
out << "(_ BitVec " << to_unsignedbv_type(type).get_width() << ')';
else if(type.id() == ID_bool)
out << "Bool";
else if(f.type.id() == ID_integer)
else if(type.id() == ID_integer)
out << "Int";
else if(f.type.id() == ID_real)
else if(type.id() == ID_real)
out << "Real";
else
out << "? " << f.type.id();
out << "? " << type.id();
return out;
}
std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr)
{
if(expr.id() == ID_constant)
{
const auto &value = to_constant_expr(expr).get_value();
const typet &expr_type = expr.type();
if(expr_type.id() == ID_unsignedbv)
{
const std::size_t width = to_unsignedbv_type(expr_type).get_width();
const auto value = numeric_cast_v<mp_integer>(expr);
out << "(_ bv" << value << " " << width << ")";
}
else if(expr_type.id() == ID_bool)
{
if(expr.is_true())
out << "true";
else if(expr.is_false())
out << "false";
else
DATA_INVARIANT(false, "unknown Boolean constant");
}
else if(expr_type.id() == ID_integer)
{
out << value;
}
else
DATA_INVARIANT(false, "unhandled constant: " + expr_type.id_string());
}
else if(expr.id() == ID_symbol)
{
out << to_symbol_expr(expr).get_identifier();
}
else
out << "? " << expr.id();
return out;
}

25
src/solvers/smt2/smt2_format.h
View File

@ -9,17 +9,32 @@ Author: Daniel Kroening, kroening@kroening.com
#ifndef CPROVER_SOLVERS_SMT2_SMT2_FORMAT_H
#define CPROVER_SOLVERS_SMT2_SMT2_FORMAT_H
#include <util/type.h>
#include <util/expr.h>
struct smt2_format
template <typename T>
struct smt2_format_containert
{
explicit smt2_format(const typet &_type) : type(_type)
explicit smt2_format_containert(const T &_o) : o(_o)
{
}
const typet &type;
const T &o;
};
std::ostream &operator<<(std::ostream &, const smt2_format &);
template <typename T>
static inline smt2_format_containert<T> smt2_format(const T &_o)
{
return smt2_format_containert<T>(_o);
}
template <typename T>
static inline std::ostream &
operator<<(std::ostream &out, const smt2_format_containert<T> &c)
{
return smt2_format_rec(out, c.o);
}
std::ostream &smt2_format_rec(std::ostream &, const exprt &);
std::ostream &smt2_format_rec(std::ostream &, const typet &);
#endif // CPROVER_SOLVERS_SMT2_SMT2_FORMAT_H