Commit 51a1e208 authored by phlo's avatar phlo

updated Solver class visibility

parent 19eed0bc
#include "boolector.hh"
#include "parser.hh"
#include "shell.hh"
#include "trace.hh"
namespace ConcuBinE {
......@@ -9,6 +9,30 @@ namespace ConcuBinE {
// Boolector
//==============================================================================
//------------------------------------------------------------------------------
// public member functions inherited from Solver
//------------------------------------------------------------------------------
// Boolector::name -------------------------------------------------------------
std::string Boolector::name () const { return "boolector"; }
// Boolector::version ----------------------------------------------------------
std::string Boolector::version () const
{
static std::string version;
if (version.empty())
shell::run({name(), "--version"}).stdout >> version;
return version;
}
//------------------------------------------------------------------------------
// public member functions inherited from External
//------------------------------------------------------------------------------
// Boolector::command ----------------------------------------------------------
const std::vector<std::string> & Boolector::command () const
......@@ -17,6 +41,10 @@ const std::vector<std::string> & Boolector::command () const
return cmd;
}
//------------------------------------------------------------------------------
// protected member functions inherited from External
//------------------------------------------------------------------------------
// Boolector::parse ------------------------------------------------------------
Boolector::Symbol Boolector::parse (std::istringstream & line)
......@@ -84,21 +112,4 @@ Boolector::Symbol Boolector::parse (std::istringstream & line)
return Symbol::ignore;
}
// Boolector::name -------------------------------------------------------------
std::string Boolector::name () const { return "boolector"; }
// Boolector::version ----------------------------------------------------------
std::string Boolector::version () const
{
static const std::vector<std::string> cmd({name(), "--version"});
static std::string version;
if (version.empty())
shell::run(cmd).stdout >> version;
return version;
}
} // namespace ConcuBinE
......@@ -6,36 +6,42 @@
namespace ConcuBinE {
//==============================================================================
// Boolector class
// Boolector
//==============================================================================
class Boolector : public External
{
public: //======================================================================
//----------------------------------------------------------------------------
// member functions
// public member functions inherited from Solver
//----------------------------------------------------------------------------
private: //---------------------------------------------------------------------
// get name
//
virtual std::string name () const;
// build command line for running boolector
// get version
//
virtual const std::vector<std::string> & command () const;
virtual std::string version () const;
protected: //-------------------------------------------------------------------
//----------------------------------------------------------------------------
// public member functions inherited from External
//----------------------------------------------------------------------------
// parse variable
// get command line
//
virtual Symbol parse (std::istringstream & line);
virtual const std::vector<std::string> & command () const;
public: //----------------------------------------------------------------------
protected: //===================================================================
// return boolector's name
//
virtual std::string name () const;
//----------------------------------------------------------------------------
// protected member functions inherited from External
//----------------------------------------------------------------------------
// return boolector's version
// parse variable
//
virtual std::string version () const;
virtual Symbol parse (std::istringstream & line);
};
} // namespace ConcuBinE
......
#include "btormc.hh"
#include "encoder.hh"
#include "trace.hh"
namespace ConcuBinE {
......@@ -8,10 +9,34 @@ namespace ConcuBinE {
// BtorMC
//==============================================================================
//------------------------------------------------------------------------------
// public member functions inherited from Solver
//------------------------------------------------------------------------------
// BtorMC::name ----------------------------------------------------------------
std::string BtorMC::name () const { return "btormc"; }
// BtorMC::sat -----------------------------------------------------------------
bool BtorMC::sat (const std::string & formula, const size_t k)
{
kmax = std::to_string(k);
return Boolector::sat(formula);
}
// BtorMC::solve ---------------------------------------------------------------
std::unique_ptr<Trace> BtorMC::solve (Encoder & encoder)
{
kmax = std::to_string(encoder.bound);
return Boolector::solve(encoder);
}
//------------------------------------------------------------------------------
// public member functions inherited from External
//------------------------------------------------------------------------------
// BtorMC::command -------------------------------------------------------------
const std::vector<std::string> & BtorMC::command () const
......@@ -20,30 +45,17 @@ const std::vector<std::string> & BtorMC::command () const
name(),
"--trace-gen-full",
"-kmax",
""});
kmax});
// TODO: improve
cmd.back() = std::to_string(bound);
if (cmd.back() != kmax)
cmd.back() = kmax;
return cmd;
}
// BtorMC::parse ---------------------------------------------------------------
BtorMC::Symbol BtorMC::parse (std::istringstream & line)
{
switch (line.peek())
{
case 'b':
case 'j':
case '#':
case '@':
case '.':
return {};
default:
return Boolector::parse(line);
}
}
//------------------------------------------------------------------------------
// private member functions inherited from External
//------------------------------------------------------------------------------
// BtorMC::symbol --------------------------------------------------------------
......@@ -57,13 +69,14 @@ BtorMC::Symbol BtorMC::symbol (std::istringstream & line)
{
line >> std::ws;
std::ostringstream os;
std::ostringstream oss;
for (char c = line.get();
c != '@' && c != '#' && c != '_' && c != EOF;
c = line.get())
os << c;
oss << c;
std::string name = os.str();
std::string name = oss.str();
if (name.empty())
throw std::runtime_error("missing symbol");
......@@ -138,20 +151,21 @@ BtorMC::Symbol BtorMC::symbol (std::istringstream & line)
return Symbol::ignore;
}
// BtorMC::sat -----------------------------------------------------------------
bool BtorMC::sat (const std::string & formula, const size_t b)
{
bound = b;
return Boolector::sat(formula);
}
// BtorMC::solve ---------------------------------------------------------------
// BtorMC::parse ---------------------------------------------------------------
std::unique_ptr<Trace> BtorMC::solve (Encoder & encoder)
BtorMC::Symbol BtorMC::parse (std::istringstream & line)
{
bound = encoder.bound;
return Boolector::solve(encoder);
switch (line.peek())
{
case 'b':
case 'j':
case '#':
case '@':
case '.':
return {};
default:
return Boolector::parse(line);
}
}
} // namespace ConcuBinE
......@@ -5,26 +5,46 @@
namespace ConcuBinE {
struct BtorMC : public Boolector
{
//----------------------------------------------------------------------------
// members
//----------------------------------------------------------------------------
//==============================================================================
// BtorMC
//==============================================================================
size_t bound = 20;
class BtorMC : public Boolector
{
public: //======================================================================
//----------------------------------------------------------------------------
// member functions
// public member functions inherited from Solver
//----------------------------------------------------------------------------
// return btormc's name
// get name
//
virtual std::string name () const;
// build command line for running btormc
// evaluate arbitrary formula
//
using Boolector::sat;
virtual bool sat (const std::string & formula, size_t bound);
// solve given encoding and return trace
//
virtual std::unique_ptr<Trace> solve (Encoder & encoder);
//----------------------------------------------------------------------------
// public member functions inherited from External
//----------------------------------------------------------------------------
// get command line
//
virtual const std::vector<std::string> & command () const;
private: //=====================================================================
//----------------------------------------------------------------------------
// private member functions inherited from External
//----------------------------------------------------------------------------
// parse current variable's symbol
//
virtual Symbol symbol (std::istringstream &);
......@@ -33,15 +53,13 @@ struct BtorMC : public Boolector
//
virtual Symbol parse (std::istringstream &);
// evaluate arbitrary formula
//
using Boolector::sat;
virtual bool sat (const std::string & formula, size_t bound);
//----------------------------------------------------------------------------
// private data members
//----------------------------------------------------------------------------
// run btormc and return trace
// bound for setting -kmax
//
virtual std::unique_ptr<Trace> solve (Encoder & encoder);
std::string kmax = "20";
};
} // namespace ConcuBinE
......
......@@ -2,6 +2,7 @@
#include "shell.hh"
#include "smtlib.hh"
#include "trace.hh"
namespace ConcuBinE {
......@@ -9,6 +10,10 @@ namespace ConcuBinE {
// CVC4
//==============================================================================
//------------------------------------------------------------------------------
// public member functions inherited from Solver
//------------------------------------------------------------------------------
// CVC4::name ------------------------------------------------------------------
std::string CVC4::name () const { return "cvc4"; }
......@@ -17,12 +22,11 @@ std::string CVC4::name () const { return "cvc4"; }
std::string CVC4::version () const
{
static const std::vector<std::string> cmd({name(), "--version"});
static std::string version;
if (version.empty())
{
auto out = shell::run(cmd);
auto out = shell::run({name(), "--version"});
do out.stdout >> version; while (out.stdout && version != "version");
out.stdout >> version;
}
......@@ -41,6 +45,10 @@ std::string CVC4::formula (Encoder & encoder) const
smtlib::get_model();
}
//------------------------------------------------------------------------------
// public member functions inherited from External
//------------------------------------------------------------------------------
// CVC4::command ---------------------------------------------------------------
const std::vector<std::string> & CVC4::command () const
......@@ -54,6 +62,10 @@ const std::vector<std::string> & CVC4::command () const
return cmd;
}
//------------------------------------------------------------------------------
// private member functions inherited from External
//------------------------------------------------------------------------------
// CVC4::parse -----------------------------------------------------------------
inline bool parse_bool (std::istringstream & line, std::string & token)
......@@ -71,9 +83,8 @@ inline word_t parse_bv (std::istringstream & line, std::string & token)
CVC4::Symbol CVC4::parse (std::istringstream & line)
{
Symbol sym = symbol(line);
std::string token;
Symbol sym = symbol(line);
if (!std::getline(line, token, '='))
throw std::runtime_error("missing value");
......
......@@ -6,33 +6,45 @@
namespace ConcuBinE {
//==============================================================================
// CVC4 class
// CVC4
//
// NOTE: seems like CVC4 always assigns uninitialized array elements with zero
//==============================================================================
struct CVC4 : public External
class CVC4 : public External
{
public: //======================================================================
//----------------------------------------------------------------------------
// member functions
// public member functions inherited from Solver
//----------------------------------------------------------------------------
// return cvc4's name
// get name
//
virtual std::string name () const;
// return cvc4's version
// get version
//
virtual std::string version () const;
// build formula for cvc4
// build formula from given encoding
//
virtual std::string formula (Encoder & encoder) const;
// build command line for the specific solver
//----------------------------------------------------------------------------
// public member functions inherited from External
//----------------------------------------------------------------------------
// get command line
//
virtual const std::vector<std::string> & command () const;
private: //=====================================================================
//----------------------------------------------------------------------------
// private member functions inherited from External
//----------------------------------------------------------------------------
// parse variable
//
virtual Symbol parse (std::istringstream &);
......
#include <cstring>
#include <iostream>
#include "btor2.hh"
#include "smtlib.hh"
......
#ifndef RUNTIME_HH_
#define RUNTIME_HH_
#include <chrono>
namespace ConcuBinE::runtime {
//==============================================================================
// functions
//==============================================================================
// measure runtime of a given function
//
template <class Functor, class Duration = std::chrono::milliseconds>
inline long measure (const Functor & fun)
{
const auto begin = std::chrono::high_resolution_clock::now();
fun();
const auto end = std::chrono::high_resolution_clock::now();
return std::chrono::duration_cast<Duration>(end - begin).count();
}
} // namespace ConcuBinE::runtime
#endif
#include "solver.hh"
#include <cassert>
#include <chrono>
#include "encoder.hh"
#include "parser.hh"
#include "runtime.hh"
#include "shell.hh"
#include "trace.hh"
namespace ConcuBinE {
......@@ -21,6 +20,36 @@ std::string Solver::formula (Encoder & encoder) const { return encoder.str(); }
// External
//==============================================================================
//------------------------------------------------------------------------------
// public member functions inherited from Solver
//------------------------------------------------------------------------------
// External::sat ---------------------------------------------------------------
bool External::sat (const std::string & input)
{
const auto & cmd = command();
time = runtime::measure([this, &input, &cmd] {
stdout = std::move(shell::run(cmd, input).stdout);
});
std::string sat;
return (stdout >> sat) && sat == "sat";
}
// External::solve -------------------------------------------------------------
std::unique_ptr<Trace> External::solve (Encoder & encoder)
{
sat(formula(encoder));
return trace(encoder);
}
//------------------------------------------------------------------------------
// protected member functions
//------------------------------------------------------------------------------
// External::attribute ---------------------------------------------------------
size_t External::attribute (std::istringstream & line,
......@@ -122,13 +151,15 @@ External::Symbol External::symbol (std::istringstream & line)
return Symbol::ignore;
}
//------------------------------------------------------------------------------
// private member functions
//------------------------------------------------------------------------------
// External::update_heap -------------------------------------------------------
void External::update_heap (Trace & trace, const size_t prev, const size_t cur)
{
const word_t t = trace.thread(prev);
// instruction responsible for state in the previous step
const Instruction & op = (*trace.programs)[t][trace.pc(prev, t)];
// store buffer has been flushed
......@@ -168,11 +199,10 @@ std::unique_ptr<Trace> External::trace (const Encoder & encoder)
{
size_t lineno = 2;
size_t next = 2;
const std::shared_ptr<Program::List> & programs = encoder.programs;
const auto & programs = encoder.programs;
auto trace = std::make_unique<Trace>(programs, encoder.mmap);
for (std::string line_buf; getline(std_out, line_buf); lineno++)
for (std::string line_buf; getline(stdout, line_buf); lineno++)
{
// skip empty lines
if (line_buf.empty())
......@@ -247,28 +277,4 @@ std::unique_ptr<Trace> External::trace (const Encoder & encoder)
return trace;
}
// External::sat ---------------------------------------------------------------
bool External::sat (const std::string & input)
{
using namespace std::chrono;
high_resolution_clock::time_point t = high_resolution_clock::now();
std_out = std::move(shell::run(command(), input).stdout);
time = duration_cast<milliseconds>(high_resolution_clock::now() - t).count();
std::string sat;
return (std_out >> sat) && sat == "sat";
}
// External::solve -------------------------------------------------------------
std::unique_ptr<Trace> External::solve (Encoder & encoder)
{
sat(formula(encoder));
return trace(encoder);
}
} // namespace ConcuBinE
......@@ -3,8 +3,9 @@
#include <memory>
#include <sstream>
#include <unordered_map>
#include "trace.hh"
#include "common.hh"
namespace ConcuBinE {
......@@ -13,34 +14,29 @@ namespace ConcuBinE {
//==============================================================================
struct Encoder;
struct Trace;
//==============================================================================
// Solver base class
// Solver
//
// * abstract base class
//==============================================================================
struct Solver
{
//----------------------------------------------------------------------------
// members
//----------------------------------------------------------------------------
// solving time in milliseconds
//
long time;
//----------------------------------------------------------------------------
// member functions
// public member functions
//----------------------------------------------------------------------------
// return the solver's name
// get name
//
virtual std::string name () const = 0;
// return the solver's version
// get version
//
virtual std::string version () const = 0;
// build formula for the specific solver
// build formula from given encoding
//
virtual std::string formula (Encoder & encoder) const;
......@@ -48,23 +44,57 @@ struct Solver
//
virtual bool sat (const std::string & formula) = 0;
// run solver and return trace
// solve given encoding and return trace
//
virtual std::unique_ptr<Trace> solve (Encoder & encoder) = 0;
//----------------------------------------------------------------------------
// public data members
//----------------------------------------------------------------------------
// runtime in milliseconds
//
long time;
};
//==============================================================================
// External base class
// External
//
// Base class for solvers running in a forked process.
// * abstract base class for solvers running in a forked process
//==============================================================================
struct External : public Solver
class External : public Solver
{
public: //======================================================================
//----------------------------------------------------------------------------
// public member functions
//----------------------------------------------------------------------------
// get command line
//
virtual const std::vector<std::string> & command () const = 0;
//----------------------------------------------------------------------------
// member types
// public member functions inherited from Solver
//----------------------------------------------------------------------------
// evaluate arbitrary formula
//
virtual bool sat (const std::string & formula);
// solve given encoding and return trace
//
virtual std::unique_ptr<Trace> solve (Encoder & encoder);
protected: //===================================================================
//----------------------------------------------------------------------------
// protected member types
//----------------------------------------------------------------------------
// current symbol while parsing
//
enum class Symbol
{
ignore,
......@@ -82,7 +112,25 @@ struct External : public Solver
};
//----------------------------------------------------------------------------
// members
// protected member functions
//----------------------------------------------------------------------------
// parse integer attribute of current symbol
//
size_t attribute (std::istringstream & line,