Commit b8314541 authored by phlo's avatar phlo

improved namespaces

* moved BTOR2 and SMT-Lib encoders to the according namespace
* removed using namespace std declarations
parent 5401751d
......@@ -4,68 +4,67 @@
#include "parser.hh"
using namespace std;
std::string Boolector::name () const { return "boolector"; }
string Boolector::name () const { return "boolector"; }
string Boolector::build_command ()
std::string Boolector::build_command ()
{
// return "boolector --model-gen --output-number-format=dec";
return "boolector --model-gen";
}
optional<Boolector::Variable> Boolector::parse_line (istringstream & line)
std::optional<Boolector::Variable>
Boolector::parse_line (std::istringstream & line)
{
string token;
std::string token;
uint64_t nid;
word_t adr = 0, val = 0;
/* parse node id */
// parse node id
if (!(line >> nid))
{
line >> token;
throw runtime_error("parsing node id failed [" + token + ']');
throw std::runtime_error("parsing node id failed [" + token + ']');
}
/* parse value */
// parse value
if (!(line >> token))
throw runtime_error("missing value");
throw std::runtime_error("missing value");
try
{
val = stoul(token, nullptr, 2);
}
catch (const logic_error &)
catch (const std::logic_error &)
{
/* array element index */
// array element index
try
{
token = token.substr(1, token.size() - 2);
adr = stoul(token, nullptr, 2);
}
catch (const logic_error &)
catch (const std::logic_error &)
{
throw runtime_error("illegal array index [" + token + "]");
throw std::runtime_error("illegal array index [" + token + "]");
}
/* array element value */
// array element value
if (!(line >> token))
throw runtime_error("missing array value");
throw std::runtime_error("missing array value");
try
{
val = stoul(token, nullptr, 2);
}
catch (const logic_error &)
catch (const std::logic_error &)
{
throw runtime_error("illegal array value [" + token + "]");
throw std::runtime_error("illegal array value [" + token + "]");
}
}
/* parse variable */
optional<Variable> variable = parse_variable(line);
// parse variable
std::optional<Variable> variable = parse_variable(line);
/*
if (variable && variable->type == Variable::Type::EXEC && val)
......
......@@ -3,11 +3,12 @@
#include "solver.hh"
class Boolector : public ExternalSolver
class Boolector : public External
{
virtual std::string build_command ();
protected:
virtual std::optional<Variable> parse_line (std::istringstream & line);
public:
......@@ -15,6 +16,4 @@ public:
virtual std::string name () const;
};
typedef std::shared_ptr<Boolector> BoolectorPtr;
#endif
This diff is collapsed.
......@@ -2,23 +2,22 @@
#include "encoder.hh"
using namespace std;
BtorMC::BtorMC(bound_t b) : bound(b) {}
string BtorMC::name () const { return "btormc"; }
std::string BtorMC::name () const { return "btormc"; }
string BtorMC::build_command ()
std::string BtorMC::build_command ()
{
return "btormc --trace-gen-full -kmax " + to_string(bound);
return "btormc --trace-gen-full -kmax " + std::to_string(bound);
}
string BtorMC::build_formula (Encoder & formula, string & constraints)
std::string BtorMC::build_formula (Encoder & formula,
const std::string & constraints)
{
return formula.str() + (constraints.empty() ? "" : constraints + eol);
}
optional<BtorMC::Variable> BtorMC::parse_line (istringstream & line)
std::optional<BtorMC::Variable> BtorMC::parse_line (std::istringstream & line)
{
switch (line.peek())
{
......@@ -33,23 +32,25 @@ optional<BtorMC::Variable> BtorMC::parse_line (istringstream & line)
}
}
optional<BtorMC::Variable> BtorMC::parse_variable (istringstream & line)
std::optional<BtorMC::Variable> BtorMC::parse_variable (std::istringstream & line)
{
optional<Variable> variable {Variable()};
std::optional<Variable> variable {Variable()};
ostringstream os;
std::ostringstream os;
// cout << line.str() << eol;
// if (!getline(line >> ws, name, '_'))
// runtime_error("missing variable");
line >> ws;
line >> std::ws;
for (char c = line.get(); c != '@' && c != '#' && c != '_' && c != EOF; c = line.get())
for (char c = line.get();
c != '@' && c != '#' && c != '_' && c != EOF;
c = line.get())
os << c;
string name = os.str();
std::string name = os.str();
// cout << "BtorMC::parse_variable name = '" << name << '\'' << eol;
......
......@@ -7,19 +7,17 @@ struct BtorMC : public Boolector
{
BtorMC (bound_t);
const bound_t bound;
const bound_t bound;
virtual std::string build_command ();
virtual std::string build_command ();
virtual std::string build_formula (Encoder &, std::string &);
virtual std::string build_formula (Encoder &, const std::string &);
virtual std::optional<Variable> parse_line (std::istringstream &);
virtual std::optional<Variable> parse_variable (std::istringstream &);
virtual std::string name () const;
virtual std::string name () const;
};
typedef std::shared_ptr<BtorMC> BtorMCPtr;
#endif
......@@ -4,26 +4,37 @@
#include <cstdint>
#include <limits>
/* machine type ***************************************************************/
//==============================================================================
// types
//==============================================================================
// register value
//
using word_t = uint16_t;
using sword_t = int16_t; // signed
/* step type ******************************************************************/
// model checking step
//
using bound_t = uint64_t;
/* global variables ***********************************************************/
//==============================================================================
// global variables
//==============================================================================
/* word attributes */
// word attributes
//
const word_t word_size = std::numeric_limits<word_t>::digits;
const word_t word_max = std::numeric_limits<word_t>::max();
const sword_t sword_min = std::numeric_limits<sword_t>::min();
const sword_t sword_max = std::numeric_limits<sword_t>::max();
/* verbose output */
// verbose output
//
extern bool verbose;
/* end of line character */
// end of line character
//
const char eol = '\n';
#endif
......@@ -2,16 +2,15 @@
#include "smtlib.hh"
using namespace std;
std::string CVC4::name () const { return "cvc4"; }
string CVC4::name () const { return "cvc4"; }
string CVC4::build_command ()
std::string CVC4::build_command ()
{
return "cvc4 -L smt2 -m --output-lang=cvc4";
}
string CVC4::build_formula (Encoder & formula, string & constraints)
std::string CVC4::build_formula (Encoder & formula,
const std::string & constraints)
{
return
Solver::build_formula(formula, constraints) +
......@@ -19,7 +18,7 @@ string CVC4::build_formula (Encoder & formula, string & constraints)
smtlib::get_model();
}
optional<CVC4::Variable> CVC4::parse_line (istringstream & line)
std::optional<CVC4::Variable> CVC4::parse_line (std::istringstream & line)
{
// TODO
(void) line;
......
......@@ -3,11 +3,12 @@
#include "solver.hh"
class CVC4 : public ExternalSolver
class CVC4 : public External
{
virtual std::string build_command ();
virtual std::string build_formula (Encoder & encoder, std::string & constraints);
virtual std::string build_formula (Encoder & encoder,
const std::string & constraints);
virtual std::optional<Variable> parse_line (std::istringstream &);
......@@ -16,6 +17,4 @@ public:
virtual std::string name () const;
};
typedef std::shared_ptr<CVC4> CVC4Ptr;
#endif
#include "encoder.hh"
//==============================================================================
// using declarations
//==============================================================================
using std::string;
using std::ostringstream;
//==============================================================================
// Encoder
//==============================================================================
......@@ -15,39 +8,39 @@ using std::ostringstream;
// static members
//------------------------------------------------------------------------------
const string Encoder::accu_sym = "accu";
const string Encoder::mem_sym = "mem";
const string Encoder::sb_adr_sym = "sb-adr";
const string Encoder::sb_val_sym = "sb-val";
const string Encoder::sb_full_sym = "sb-full";
const string Encoder::stmt_sym = "stmt";
const string Encoder::block_sym = "block";
const string Encoder::heap_sym = "heap";
const string Encoder::exit_flag_sym = "exit";
const string Encoder::exit_code_sym = "exit-code";
const string Encoder::thread_sym = "thread";
const string Encoder::exec_sym = "exec";
const string Encoder::flush_sym = "flush";
const string Encoder::check_sym = "check";
const string Encoder::accu_comment = "accu variables";
const string Encoder::mem_comment = "mem variables";
const string Encoder::sb_adr_comment = "store buffer address variables";
const string Encoder::sb_val_comment = "store buffer value variables";
const string Encoder::sb_full_comment = "store buffer full variables";
const string Encoder::stmt_comment = "statement activation variables";
const string Encoder::block_comment = "blocking variables";
const string Encoder::heap_comment = "heap variable";
const string Encoder::exit_flag_comment = "exit flag variable";
const string Encoder::exit_code_comment = "exit code variable";
const string Encoder::thread_comment = "thread activation variables";
const string Encoder::exec_comment = "statement execution variables";
const string Encoder::flush_comment = "store buffer flush variables";
const string Encoder::check_comment = "checkpoint variables";
const std::string Encoder::accu_sym = "accu";
const std::string Encoder::mem_sym = "mem";
const std::string Encoder::sb_adr_sym = "sb-adr";
const std::string Encoder::sb_val_sym = "sb-val";
const std::string Encoder::sb_full_sym = "sb-full";
const std::string Encoder::stmt_sym = "stmt";
const std::string Encoder::block_sym = "block";
const std::string Encoder::heap_sym = "heap";
const std::string Encoder::exit_flag_sym = "exit";
const std::string Encoder::exit_code_sym = "exit-code";
const std::string Encoder::thread_sym = "thread";
const std::string Encoder::exec_sym = "exec";
const std::string Encoder::flush_sym = "flush";
const std::string Encoder::check_sym = "check";
const std::string Encoder::accu_comment = "accu variables";
const std::string Encoder::mem_comment = "mem variables";
const std::string Encoder::sb_adr_comment = "store buffer address variables";
const std::string Encoder::sb_val_comment = "store buffer value variables";
const std::string Encoder::sb_full_comment = "store buffer full variables";
const std::string Encoder::stmt_comment = "statement activation variables";
const std::string Encoder::block_comment = "blocking variables";
const std::string Encoder::heap_comment = "heap variable";
const std::string Encoder::exit_flag_comment = "exit flag variable";
const std::string Encoder::exit_code_comment = "exit code variable";
const std::string Encoder::thread_comment = "thread activation variables";
const std::string Encoder::exec_comment = "statement execution variables";
const std::string Encoder::flush_comment = "store buffer flush variables";
const std::string Encoder::check_comment = "checkpoint variables";
//------------------------------------------------------------------------------
// constructors
......@@ -90,15 +83,15 @@ Encoder::Encoder (const Program::List::ptr & p, bound_t b) :
// Encode::str -----------------------------------------------------------------
string Encoder::str () { return formula.str(); }
std::string Encoder::str () { return formula.str(); }
//------------------------------------------------------------------------------
// DEBUG
//------------------------------------------------------------------------------
string Encoder::predecessors_to_string ()
std::string Encoder::predecessors_to_string ()
{
ostringstream ss;
std::ostringstream ss;
for (word_t tid = 0; tid < programs->size(); tid++)
for (const auto & [_pc, _predecessors] : (*programs)[tid].predecessors)
......@@ -112,9 +105,9 @@ string Encoder::predecessors_to_string ()
return ss.str();
}
string Encoder::check_pcs_to_string ()
std::string Encoder::check_pcs_to_string ()
{
ostringstream ss;
std::ostringstream ss;
for (const auto & [id, threads] : check_pcs)
{
......@@ -131,9 +124,9 @@ string Encoder::check_pcs_to_string ()
return ss.str();
}
string Encoder::exit_pcs_to_string ()
std::string Encoder::exit_pcs_to_string ()
{
ostringstream ss;
std::ostringstream ss;
for (const auto & [_thread, pcs] : exit_pcs)
{
......
......@@ -229,11 +229,13 @@ struct Encoder
std::string exit_pcs_to_string ();
};
namespace smtlib {
//==============================================================================
// SMT-Lib v2.5 Encoder base class
//==============================================================================
struct SMTLib_Encoder : public Encoder
struct Encoder : public ::Encoder
{
//----------------------------------------------------------------------------
// static members
......@@ -282,7 +284,7 @@ struct SMTLib_Encoder : public Encoder
// constructors
//----------------------------------------------------------------------------
SMTLib_Encoder (const Program::List::ptr & programs, bound_t bound);
Encoder (const Program::List::ptr & programs, bound_t bound);
//----------------------------------------------------------------------------
// private member functions
......@@ -324,7 +326,8 @@ struct SMTLib_Encoder : public Encoder
// assignment expression generator
//
std::string assign (std::string variable, std::string expression);
std::string assign (const std::string & variable,
const std::string & expression) const;
// load expression generator
//
......@@ -427,15 +430,15 @@ struct SMTLib_Encoder : public Encoder
// SMT-Lib v2.5 Functional Encoder class
//==============================================================================
struct SMTLib_Encoder_Functional : public SMTLib_Encoder
struct Functional : public Encoder
{
//----------------------------------------------------------------------------
// constructors
//----------------------------------------------------------------------------
SMTLib_Encoder_Functional (const Program::List::ptr & programs,
bound_t bound,
bool encode = true);
Functional (const Program::List::ptr & programs,
bound_t bound,
bool encode = true);
//----------------------------------------------------------------------------
// private member functions
......@@ -466,7 +469,7 @@ struct SMTLib_Encoder_Functional : public SMTLib_Encoder
// SMT-Lib v2.5 Relational Encoder class
//==============================================================================
struct SMTLib_Encoder_Relational : public SMTLib_Encoder
struct Relational : public Encoder
{
//----------------------------------------------------------------------------
// member types
......@@ -474,23 +477,24 @@ struct SMTLib_Encoder_Relational : public SMTLib_Encoder
// captures frequently used expressions
//
struct State {
std::shared_ptr<std::string> accu;
std::shared_ptr<std::string> mem;
std::shared_ptr<std::string> sb_adr;
std::shared_ptr<std::string> sb_val;
std::shared_ptr<std::string> sb_full;
std::shared_ptr<std::string> stmt;
std::shared_ptr<std::string> block;
std::shared_ptr<std::string> heap;
std::shared_ptr<std::string> exit_flag;
std::shared_ptr<std::string> exit_code;
State () = default;
State (SMTLib_Encoder_Relational & encoder);
operator std::string () const;
};
struct State
{
std::shared_ptr<std::string> accu;
std::shared_ptr<std::string> mem;
std::shared_ptr<std::string> sb_adr;
std::shared_ptr<std::string> sb_val;
std::shared_ptr<std::string> sb_full;
std::shared_ptr<std::string> stmt;
std::shared_ptr<std::string> block;
std::shared_ptr<std::string> heap;
std::shared_ptr<std::string> exit_flag;
std::shared_ptr<std::string> exit_code;
State () = default;
State (Relational & encoder);
operator std::string () const;
};
//----------------------------------------------------------------------------
// members
......@@ -504,9 +508,9 @@ struct SMTLib_Encoder_Relational : public SMTLib_Encoder
// constructors
//----------------------------------------------------------------------------
SMTLib_Encoder_Relational (const Program::List::ptr & programs,
bound_t bound,
bool encode = true);
Relational (const Program::List::ptr & programs,
bound_t bound,
bool encode = true);
//----------------------------------------------------------------------------
// private member functions
......@@ -514,7 +518,7 @@ struct SMTLib_Encoder_Relational : public SMTLib_Encoder
// asserted implication expression generator
//
std::string imply (std::string ante, std::string cons) const;
std::string imply (const std::string & ante, const std::string & cons) const;
// state update helpers
//
......@@ -569,7 +573,7 @@ struct SMTLib_Encoder_Relational : public SMTLib_Encoder
// double-dispatched instruction encoding functions
//
using SMTLib_Encoder::encode; // use base class' main encoding function
using Encoder::encode; // use base class' main encoding function
virtual std::string encode (const Instruction::Load &);
virtual std::string encode (const Instruction::Store &);
......@@ -600,11 +604,15 @@ struct SMTLib_Encoder_Relational : public SMTLib_Encoder
virtual std::string encode (const Instruction::Exit &);
};
} // namespace smtlib
namespace btor2 {
//==============================================================================
// BTOR2 Encoder class
//==============================================================================
struct Btor2_Encoder : public Encoder
struct Encoder : public ::Encoder
{
//----------------------------------------------------------------------------
// member types
......@@ -766,9 +774,9 @@ struct Btor2_Encoder : public Encoder
// constructors
//----------------------------------------------------------------------------
Btor2_Encoder (const Program::List::ptr & programs,
bound_t bound,
bool encode = true);
Encoder (const Program::List::ptr & programs,
bound_t bound,
bool encode = true);
//----------------------------------------------------------------------------
// private member functions
......@@ -917,4 +925,7 @@ struct Btor2_Encoder : public Encoder
virtual std::string encode (const Instruction::Halt &);
virtual std::string encode (const Instruction::Exit &);
};
} // namespace btor2
#endif
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -5,19 +5,6 @@
#include "encoder.hh"
#include "simulator.hh"
//==============================================================================
// using declarations
//==============================================================================
using std::string;
using std::unique_ptr;
using std::make_unique;
using std::is_base_of;
using std::runtime_error;
//==============================================================================
// Instruction::Set
//==============================================================================
......@@ -26,15 +13,15 @@ using std::runtime_error;
// static members
//------------------------------------------------------------------------------
unique_ptr<Instruction::Set::nullary_t> Instruction::Set::nullary;
unique_ptr<Instruction::Set::unary_t> Instruction::Set::unary;
unique_ptr<Instruction::Set::memory_t> Instruction::Set::memory;
std::unique_ptr<Instruction::Set::nullary_t> Instruction::Set::nullary;
std::unique_ptr<Instruction::Set::unary_t> Instruction::Set::unary;
std::unique_ptr<Instruction::Set::memory_t> Instruction::Set::memory;
//------------------------------------------------------------------------------
// static member functions
//------------------------------------------------------------------------------
bool Instruction::Set::contains (const string & symbol)
bool Instruction::Set::contains (const std::string & symbol)
{
if (nullary->find(symbol) != nullary->end())
return true;
......@@ -49,10 +36,10 @@ bool Instruction::Set::contains (const string & symbol)
}
template <class POD>
const string & Instruction::Set::add_nullary (const string && symbol)
const std::string & Instruction::Set::add_nullary (const std::string && symbol)
{
if (!nullary)
nullary = make_unique<nullary_t>();
nullary = std::make_unique<nullary_t>();
return
nullary->emplace(
......@@ -62,10 +49,10 @@ const string & Instruction::Set::add_nullary (const string && symbol)
}
template <class POD>
const string & Instruction::Set::add_unary (const string && symbol)
const std::string & Instruction::Set::add_unary (const std::string && symbol)
{
if (!unary)
unary = make_unique<unary_t>();
unary = std::make_unique<unary_t>();
return
unary->emplace(
......@@ -75,12 +62,12 @@ const string & Instruction::Set::add_unary (const string && symbol)
}
template <class POD>
const string & Instruction::Set::add_memory (const string && symbol)
const std::string & Instruction::Set::add_memory (const std::string && symbol)
{
add_unary<POD>(string {symbol});
add_unary<POD>(std::string {symbol});
if (!memory)
memory = make_unique<memory_t>();
memory = std::make_unique<memory_t>();
return
memory->emplace(
......@@ -89,28 +76,29 @@ const string & Instruction::Set::add_memory (const string && symbol)
.first->first;
}
Instruction Instruction::Set::create (const string & symbol)
Instruction Instruction::Set::create (const std::string & symbol)
{
if (nullary->find(symbol) == nullary->end())
throw runtime_error("Instruction '" + symbol + "' unknown");
throw std::runtime_error("Instruction '" + symbol + "' unknown");
return (*nullary)[symbol]();
}
Instruction Instruction::Set::create (const string & symbol, const word_t arg)
Instruction Instruction::Set::create (const std::string & symbol,
const word_t arg)
{
if (unary->find(symbol) == unary->end())
throw runtime_error("Instruction '" + symbol + "' unknown");
throw std::runtime_error("Instruction '" + symbol + "' unknown");
return (*unary)[symbol](arg);
}
Instruction Instruction::Set::create (const string & symbol,
Instruction Instruction::Set::create (const std::string & symbol,
const word_t arg,
const bool indirect)
{
if (memory->find(symbol) == memory->end())
throw runtime_error("Instruction '" + symbol + "' unknown");
throw std::runtime_error("Instruction '" + symbol + "' unknown");
return (*memory)[symbol](arg, indirect);
}
......@@ -133,11 +121,11 @@ struct Model : public Instruction::Concept
Model (const T & p) : pod(p) {}
// Model (const T && pod) : obj(move(pod)) {}
virtual pointer clone () const { return make_unique<Model<T>>(pod); }
virtual pointer clone () const { return std::make_unique<Model<T>>(pod); }
virtual bool is_nullary () const { return is_base_of<Nullary, T>(); }
virtual bool is_unary () const { return is_base_of<Unary, T>(); }
virtual bool is_memory () const { return is_base_of<Memory, T>(); }
virtual bool is_nullary () const { return std::is_base_of<Nullary, T>(); }
virtual bool is_unary () const { return std::is_base_of<Unary, T>(); }
virtual bool is_memory () const { return std::is_base_of<Memory, T>(); }
virtual bool is_jump () const { return pod.type & Instruction::Type::jump; }
virtual bool requires_flush () const
......@@ -145,7 +133,7 @@ struct Model : public Instruction::Concept
return pod.type & (Instruction::Type::write | Instruction::Type::barrier);