Commit fc5b110f authored by phlo's avatar phlo

shortened Solver member function names

parent b44bed29
......@@ -12,16 +12,16 @@ namespace ConcuBinE {
// member functions
//------------------------------------------------------------------------------
// Boolector::build_command ----------------------------------------------------
// Boolector::command ----------------------------------------------------------
std::string Boolector::build_command ()
std::string Boolector::command ()
{
return "boolector --model-gen"; // --output-number-format=dec
}
// Boolector::parse_line -------------------------------------------------------
// Boolector::parse ------------------------------------------------------------
Boolector::Symbol Boolector::parse_line (std::istringstream & line)
Boolector::Symbol Boolector::parse (std::istringstream & line)
{
std::string token;
......@@ -68,19 +68,19 @@ Boolector::Symbol Boolector::parse_line (std::istringstream & line)
}
// parse symbol
Symbol symbol = parse_symbol(line);
Symbol sym = symbol(line);
switch (symbol)
switch (sym)
{
case Symbol::stmt:
case Symbol::exit_flag:
case Symbol::thread:
case Symbol::flush:
if (value)
return symbol;
return sym;
break;
default: return symbol;
default: return sym;
}
return Symbol::ignore;
......
......@@ -13,11 +13,11 @@ class Boolector : public External
{
private: //---------------------------------------------------------------------
virtual std::string build_command ();
virtual std::string command ();
protected: //-------------------------------------------------------------------
virtual Symbol parse_line (std::istringstream & line);
virtual Symbol parse (std::istringstream & line);
public: //----------------------------------------------------------------------
......
......@@ -22,24 +22,16 @@ BtorMC::BtorMC(size_t b) : bound(b) {}
std::string BtorMC::name () const { return "btormc"; }
// BtorMC::build_command -------------------------------------------------------
// BtorMC::command -------------------------------------------------------------
std::string BtorMC::build_command ()
std::string BtorMC::command ()
{
return "btormc --trace-gen-full -kmax " + std::to_string(bound);
}
// BtorMC::build_formula -------------------------------------------------------
// BtorMC::parse ---------------------------------------------------------------
std::string BtorMC::build_formula (Encoder & formula,
const std::string & constraints)
{
return formula.str() + (constraints.empty() ? "" : constraints + eol);
}
// BtorMC::parse_line ----------------------------------------------------------
BtorMC::Symbol BtorMC::parse_line (std::istringstream & line)
BtorMC::Symbol BtorMC::parse (std::istringstream & line)
{
switch (line.peek())
{
......@@ -50,11 +42,11 @@ BtorMC::Symbol BtorMC::parse_line (std::istringstream & line)
case '.':
return {};
default:
return Boolector::parse_line(line);
return Boolector::parse(line);
}
}
// BtorMC::parse_symbol --------------------------------------------------------
// BtorMC::symbol --------------------------------------------------------------
inline
bool starts_with (const std::string & str, const std::string & prefix)
......@@ -62,7 +54,7 @@ bool starts_with (const std::string & str, const std::string & prefix)
return str.find(prefix) != std::string::npos;
}
BtorMC::Symbol BtorMC::parse_symbol (std::istringstream & line)
BtorMC::Symbol BtorMC::symbol (std::istringstream & line)
{
line >> std::ws;
......@@ -81,66 +73,66 @@ BtorMC::Symbol BtorMC::parse_symbol (std::istringstream & line)
if (name == Encoder::accu_sym)
{
thread = parse_symbol(line, "thread");
step = parse_symbol(line, "step", '#');
thread = attribute(line, "thread");
step = attribute(line, "step", '#');
return Symbol::accu;
}
else if (name == Encoder::mem_sym)
{
thread = parse_symbol(line, "thread");
step = parse_symbol(line, "step", '#');
thread = attribute(line, "thread");
step = attribute(line, "step", '#');
return Symbol::mem;
}
else if (name == Encoder::sb_adr_sym)
{
thread = parse_symbol(line, "thread");
step = parse_symbol(line, "step", '#');
thread = attribute(line, "thread");
step = attribute(line, "step", '#');
return Symbol::sb_adr;
}
else if (name == Encoder::sb_val_sym)
{
thread = parse_symbol(line, "thread");
step = parse_symbol(line, "step", '#');
thread = attribute(line, "thread");
step = attribute(line, "step", '#');
return Symbol::sb_val;
}
else if (name == Encoder::sb_full_sym)
{
thread = parse_symbol(line, "thread");
step = parse_symbol(line, "step", '#');
thread = attribute(line, "thread");
step = attribute(line, "step", '#');
return Symbol::sb_full;
}
else if (name == Encoder::stmt_sym)
{
thread = parse_symbol(line, "thread");
pc = parse_symbol(line, "pc");
step = parse_symbol(line, "step", '#');
thread = attribute(line, "thread");
pc = attribute(line, "pc");
step = attribute(line, "step", '#');
return Symbol::stmt;
}
else if (name == Encoder::heap_sym)
{
step = parse_symbol(line, "step", '@');
step = attribute(line, "step", '@');
return Symbol::heap;
}
else if (name == Encoder::exit_flag_sym)
{
step = parse_symbol(line, "step", '#');
step = attribute(line, "step", '#');
return Symbol::exit_flag;
}
else if (name == Encoder::exit_code_sym)
{
step = parse_symbol(line, "step", '#');
step = attribute(line, "step", '#');
return Symbol::exit_code;
}
else if (name == Encoder::thread_sym)
{
thread = parse_symbol(line, "thread");
step = parse_symbol(line, "step", '@');
thread = attribute(line, "thread");
step = attribute(line, "step", '@');
return Symbol::thread;
}
else if (name == Encoder::flush_sym)
{
thread = parse_symbol(line, "thread");
step = parse_symbol(line, "step", '@');
thread = attribute(line, "thread");
step = attribute(line, "step", '@');
return Symbol::flush;
}
......
......@@ -25,15 +25,11 @@ struct BtorMC : public Boolector
virtual std::string name () const;
virtual std::string build_formula (Encoder &, const std::string &);
virtual std::string command ();
virtual std::string build_command ();
virtual Symbol symbol (std::istringstream &);
using Boolector::parse_symbol;
virtual Symbol parse_symbol (std::istringstream &);
virtual Symbol parse_line (std::istringstream &);
virtual Symbol parse (std::istringstream &);
};
} // namespace ConcuBinE
......
......@@ -16,25 +16,24 @@ namespace ConcuBinE {
std::string CVC4::name () const { return "cvc4"; }
// CVC4::build_command ---------------------------------------------------------
// CVC4::command ---------------------------------------------------------------
std::string CVC4::build_command ()
std::string CVC4::command ()
{
return "cvc4 -L smt2 -m --output-lang=cvc4";
}
// CVC4::build_formula ---------------------------------------------------------
std::string CVC4::build_formula (Encoder & formula,
const std::string & constraints)
std::string CVC4::formula (Encoder & encoder, const std::string & constraints)
{
return
Solver::build_formula(formula, constraints) +
Solver::formula(encoder, constraints) +
smtlib::check_sat() + eol +
smtlib::get_model();
}
// CVC4::parse_line ------------------------------------------------------------
// CVC4::parse -----------------------------------------------------------------
inline
bool parse_bool (std::istringstream & line, std::string & token)
......@@ -51,16 +50,16 @@ word_t parse_bv (std::istringstream & line, std::string & token)
catch (...) { throw std::runtime_error("illegal value [" + token + "]"); }
}
CVC4::Symbol CVC4::parse_line (std::istringstream & line)
CVC4::Symbol CVC4::parse (std::istringstream & line)
{
Symbol symbol = parse_symbol(line);
Symbol sym = symbol(line);
std::string token;
if (!std::getline(line, token, '='))
throw std::runtime_error("missing value");
switch (symbol)
switch (sym)
{
case Symbol::accu:
case Symbol::mem:
......@@ -68,11 +67,11 @@ CVC4::Symbol CVC4::parse_line (std::istringstream & line)
case Symbol::sb_val:
case Symbol::exit_code:
value = parse_bv(line, token);
return symbol;
return sym;
case Symbol::sb_full:
value = parse_bool(line, token);
return symbol;
return sym;
case Symbol::heap:
while (line && token != "WITH")
......@@ -93,18 +92,18 @@ CVC4::Symbol CVC4::parse_line (std::istringstream & line)
heap[address] = value;
}
return symbol;
return sym;
case Symbol::stmt:
case Symbol::exit_flag:
case Symbol::thread:
case Symbol::flush:
if (parse_bool(line, token))
return symbol;
return sym;
else
return Symbol::ignore;
default: return symbol;
default: return sym;
}
}
......
......@@ -19,12 +19,12 @@ struct CVC4 : public External
virtual std::string name () const;
virtual std::string build_command ();
virtual std::string command ();
virtual std::string build_formula (Encoder & encoder,
const std::string & constraints);
virtual std::string formula (Encoder & encoder,
const std::string & constraints);
virtual Symbol parse_line (std::istringstream &);
virtual Symbol parse (std::istringstream &);
};
} // namespace ConcuBinE
......
......@@ -435,7 +435,7 @@ int solve (const char * name, const int argc, const char ** argv)
// print formula if we're pretending
if (pretend)
std::cout << solver->build_formula(*encoder, constraints);
std::cout << solver->formula(*encoder, constraints);
else
std::cout << solver->solve(*encoder, constraints)->print();
}
......
......@@ -13,12 +13,11 @@ namespace ConcuBinE {
// Solver
//==============================================================================
// Solver::build_formula -------------------------------------------------------
// Solver::formula -------------------------------------------------------------
std::string Solver::build_formula (Encoder & formula,
const std::string & constraints)
std::string Solver::formula (Encoder & encoder, const std::string & constraints)
{
return formula.str() + eol + (constraints.empty() ? "" : constraints + eol);
return encoder.str() + (constraints.empty() ? "" : eol + constraints);
}
//==============================================================================
......@@ -35,7 +34,7 @@ bool External::sat (const std::string & input)
high_resolution_clock::time_point t = high_resolution_clock::now();
std_out = shell.run(build_command(), input);
std_out = shell.run(command(), input);
time = duration_cast<milliseconds>(high_resolution_clock::now() - t).count();
......@@ -45,15 +44,15 @@ bool External::sat (const std::string & input)
// External::solve -------------------------------------------------------------
Trace::ptr External::solve (Encoder & formula, const std::string & constraints)
Trace::ptr External::solve (Encoder & encoder, const std::string & constraints)
{
sat(build_formula(formula, constraints));
return build_trace(formula.programs);
sat(formula(encoder, constraints));
return trace(encoder.programs);
}
// External::build_trace -------------------------------------------------------
// External::trace -------------------------------------------------------------
Trace::ptr External::build_trace (const Program::List::ptr & programs)
Trace::ptr External::trace (const Program::List::ptr & programs)
{
size_t lineno = 2;
size_t next = 2;
......@@ -69,7 +68,7 @@ Trace::ptr External::build_trace (const Program::List::ptr & programs)
try
{
std::istringstream line(line_buf);
Symbol symbol = parse_line(line);
Symbol symbol = parse(line);
if (symbol == Symbol::ignore)
continue;
......@@ -166,11 +165,11 @@ Trace::ptr External::build_trace (const Program::List::ptr & programs)
return trace;
}
// External::parse_symbol ------------------------------------------------------
// External::attribute ---------------------------------------------------------
size_t External::parse_symbol (std::istringstream & line,
const std::string & name,
const char delimiter)
size_t External::attribute (std::istringstream & line,
const std::string & name,
const char delimiter)
{
if (line.peek() != delimiter)
{
......@@ -189,7 +188,9 @@ size_t External::parse_symbol (std::istringstream & line,
return val;
}
External::Symbol External::parse_symbol (std::istringstream & line)
// External::symbol ------------------------------------------------------------
External::Symbol External::symbol (std::istringstream & line)
{
std::string name;
......@@ -200,49 +201,49 @@ External::Symbol External::parse_symbol (std::istringstream & line)
if (name == Encoder::accu_sym)
{
step = parse_symbol(line, "step");
thread = parse_symbol(line, "thread");
step = attribute(line, "step");
thread = attribute(line, "thread");
return Symbol::accu;
}
else if (name == Encoder::mem_sym)
{
step = parse_symbol(line, "step");
thread = parse_symbol(line, "thread");
step = attribute(line, "step");
thread = attribute(line, "thread");
return Symbol::mem;
}
else if (name == Encoder::sb_adr_sym)
{
step = parse_symbol(line, "step");
thread = parse_symbol(line, "thread");
step = attribute(line, "step");
thread = attribute(line, "thread");
return Symbol::sb_adr;
}
else if (name == Encoder::sb_val_sym)
{
step = parse_symbol(line, "step");
thread = parse_symbol(line, "thread");
step = attribute(line, "step");
thread = attribute(line, "thread");
return Symbol::sb_val;
}
else if (name == Encoder::sb_full_sym)
{
step = parse_symbol(line, "step");
thread = parse_symbol(line, "thread");
step = attribute(line, "step");
thread = attribute(line, "thread");
return Symbol::sb_full;
}
else if (name == Encoder::stmt_sym)
{
step = parse_symbol(line, "step");
thread = parse_symbol(line, "thread");
pc = parse_symbol(line, "pc");
step = attribute(line, "step");
thread = attribute(line, "thread");
pc = attribute(line, "pc");
return Symbol::stmt;
}
else if (name == Encoder::heap_sym)
{
step = parse_symbol(line, "step");
step = attribute(line, "step");
return Symbol::heap;
}
else if (name == Encoder::exit_flag_sym)
{
step = parse_symbol(line, "step");
step = attribute(line, "step");
return Symbol::exit_flag; // TODO
}
else if (name == Encoder::exit_code_sym)
......@@ -251,14 +252,14 @@ External::Symbol External::parse_symbol (std::istringstream & line)
}
else if (name == Encoder::thread_sym)
{
step = parse_symbol(line, "step");
thread = parse_symbol(line, "thread");
step = attribute(line, "step");
thread = attribute(line, "thread");
return Symbol::thread;
}
else if (name == Encoder::flush_sym)
{
step = parse_symbol(line, "step");
thread = parse_symbol(line, "thread");
step = attribute(line, "step");
thread = attribute(line, "thread");
return Symbol::flush;
}
......
......@@ -38,8 +38,8 @@ struct Solver
// build formula for the specific solver
//
virtual std::string build_formula (Encoder & encoder,
const std::string & constraints);
virtual std::string formula (Encoder & encoder,
const std::string & constraints);
// evaluate arbitrary formula
//
......@@ -118,25 +118,25 @@ struct External : Solver
// build command line for the specific solver
//
virtual std::string build_command () = 0;
virtual std::string command () = 0;
// build trace based on the specific solver's output
//
Trace::ptr build_trace (const Program::List::ptr & programs);
Trace::ptr trace (const Program::List::ptr & programs);
// parse integer attribute of current symbol
//
size_t parse_symbol (std::istringstream & line,
const std::string & name,
char delimiter = '_');
size_t attribute (std::istringstream & line,
const std::string & name,
char delimiter = '_');
// parse current variable's symbol
//
virtual Symbol parse_symbol (std::istringstream & line);
virtual Symbol symbol (std::istringstream & line);
// parse variable
//
virtual Symbol parse_line (std::istringstream & line) = 0;
virtual Symbol parse (std::istringstream & line) = 0;
};
} // namespace ConcuBinE
......
......@@ -47,11 +47,11 @@ GTEST_FILTER = --gtest_filter=
# GTEST_FILTER += "*"
# GTEST_FILTER += Encoder.*
# GTEST_FILTER += smtlib.*
GTEST_FILTER += smtlib_Encoder.*
# GTEST_FILTER += smtlib_Encoder.*
# GTEST_FILTER += smtlib_Functional.*
# GTEST_FILTER += smtlib_Relational.*
# GTEST_FILTER += btor2.*
GTEST_FILTER += btor2_Encoder.*
# GTEST_FILTER += btor2_Encoder.*
# GTEST_FILTER += Simulator.*
# GTEST_FILTER += Main.*
# GTEST_FILTER += Experimental.*
......@@ -60,10 +60,10 @@ GTEST_FILTER += btor2_Encoder.*
# GTEST_FILTER += Trace.*
# GTEST_FILTER += MMap.*
# GTEST_FILTER += Shell.*
# GTEST_FILTER += Boolector.*
# GTEST_FILTER += BtorMC.*
# GTEST_FILTER += Z3.*
# GTEST_FILTER += CVC4.*
GTEST_FILTER += Boolector.*
GTEST_FILTER += BtorMC.*
GTEST_FILTER += Z3.*
GTEST_FILTER += CVC4.*
GTEST_FILTER := $(shell echo ${GTEST_FILTER} | sed -e 's/ /:/g')
......
......@@ -127,7 +127,7 @@ TEST_F(Boolector, print_model_check)
encoder = std::make_unique<smtlib::Functional>(programs, nullptr, 16);
std::string formula = boolector.build_formula(*encoder, "");
std::string formula = boolector.formula(*encoder, "");
bool sat = boolector.sat(formula);
......@@ -149,7 +149,7 @@ TEST_F(Boolector, print_model_cas)
encoder = std::make_unique<smtlib::Functional>(programs, nullptr, 16);
std::string formula = boolector.build_formula(*encoder, "");
std::string formula = boolector.formula(*encoder, "");
bool sat = boolector.sat(formula);
......
......@@ -139,7 +139,7 @@ TEST_F(BtorMC, print_model_check)
encoder = std::make_unique<btor2::Encoder>(programs, nullptr, 16);
std::string formula = btormc.build_formula(*encoder, "");
std::string formula = btormc.formula(*encoder, "");
bool sat = btormc.sat(formula);
......@@ -161,7 +161,7 @@ TEST_F(BtorMC, print_model_cas)
encoder = std::make_unique<btor2::Encoder>(programs, nullptr, 16);
std::string formula = btormc.build_formula(*encoder, "");
std::string formula = btormc.formula(*encoder, "");
bool sat = btormc.sat(formula);
......
......@@ -124,7 +124,7 @@ TEST_F(CVC4, print_model_check)
encoder = std::make_unique<smtlib::Functional>(programs, nullptr, 16);
bool sat = cvc4.sat(cvc4.build_formula(*encoder, constraints));
bool sat = cvc4.sat(cvc4.formula(*encoder, constraints));
std::ofstream outfile("/tmp/cvc4.check.out");
outfile << cvc4.std_out.str();
......@@ -143,7 +143,7 @@ TEST_F(CVC4, print_model_cas)
encoder = std::make_unique<smtlib::Functional>(programs, nullptr, 16);
bool sat = cvc4.sat(cvc4.build_formula(*encoder, constraints));
bool sat = cvc4.sat(cvc4.formula(*encoder, constraints));
std::ofstream outfile("/tmp/cvc4.cas.out");
outfile << cvc4.std_out.str();
......
......@@ -80,7 +80,7 @@ Trace::ptr Z3::solve (Encoder & encoder, const std::string & constraints)
high_resolution_clock::time_point t = high_resolution_clock::now();
s.from_string(build_formula(encoder, constraints).c_str());
s.from_string(formula(encoder, constraints).c_str());
if (s.check() != z3::sat)
throw std::runtime_error("formula is not sat");
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment