Commit cb75c7d1 authored by phlo's avatar phlo

added Solver::time

parent 083c70d5
#include "solver.hh"
#include <cassert>
#include <chrono>
#include "encoder.hh"
#include "parser.hh"
......@@ -28,12 +29,17 @@ std::string Solver::build_formula (Encoder & formula,
bool External::sat (const std::string & input)
{
using namespace std::chrono;
Shell shell;
high_resolution_clock::time_point t = high_resolution_clock::now();
std_out = shell.run(build_command(), input);
std::string sat;
time = duration_cast<milliseconds>(high_resolution_clock::now() - t).count();
std::string sat;
return (std_out >> sat) && sat == "sat";
}
......@@ -41,10 +47,7 @@ bool External::sat (const std::string & input)
Trace::ptr External::solve (Encoder & formula, const std::string & constraints)
{
std::string input = build_formula(formula, constraints);
sat(input);
sat(build_formula(formula, constraints));
return build_trace(formula.programs);
}
......
......@@ -20,6 +20,14 @@ struct Encoder;
struct Solver
{
//----------------------------------------------------------------------------
// members
//----------------------------------------------------------------------------
// solving time in milliseconds
//
long time;
//----------------------------------------------------------------------------
// member functions
//----------------------------------------------------------------------------
......
......@@ -53,6 +53,8 @@ TEST_F(Boolector, solve_check)
trace = boolector.solve(*encoder, constraints);
std::cout << "time to solve = " << boolector.time << "ms" << eol;
// std::cout << trace->print();
Simulator simulator (programs);
......@@ -78,6 +80,8 @@ TEST_F(Boolector, solve_cas)
trace = boolector.solve(*encoder, constraints);
std::cout << "time to solve = " << boolector.time << "ms" << eol;
// std::cout << trace->print();
Simulator simulator (programs);
......
......@@ -63,6 +63,8 @@ TEST_F(BtorMC, solve_check)
trace = btormc.solve(*encoder, constraints);
std::cout << "time to solve = " << btormc.time << "ms" << eol;
// std::cout << trace->print();
Simulator simulator {programs};
......@@ -89,6 +91,8 @@ TEST_F(BtorMC, solve_cas)
trace = btormc.solve(*encoder, constraints);
std::cout << "time to solve = " << btormc.time << "ms" << eol;
// std::cout << trace->print();
Simulator simulator {programs};
......
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