cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Fix Windows build

Browse Source
This commit is contained in:
Leonardo Alt 2019-09-02 14:27:35 +02:00
parent a774b2d905
commit a51577facf
4 changed files with 13 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
libsolidity/formal/SMTLib2Interface.cpp
View File

@ -93,12 +93,12 @@ void SMTLib2Interface::declareFunction(string const& _name, Sort const& _sort)
} }
} }
void SMTLib2Interface::addAssertion(Expression const& _expr) void SMTLib2Interface::addAssertion(smt::Expression const& _expr)
{ {
write("(assert " + toSExpr(_expr) + ")"); write("(assert " + toSExpr(_expr) + ")");
} }
pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> const& _expressionsToEvaluate) pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<smt::Expression> const& _expressionsToEvaluate)
{ {
string response = querySolver( string response = querySolver(
boost::algorithm::join(m_accumulatedOutput, "\n") + boost::algorithm::join(m_accumulatedOutput, "\n") +
@ -122,7 +122,7 @@ pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> con
return make_pair(result, values); return make_pair(result, values);
} }
string SMTLib2Interface::toSExpr(Expression const& _expr) string SMTLib2Interface::toSExpr(smt::Expression const& _expr)
{ {
if (_expr.arguments.empty()) if (_expr.arguments.empty())
return _expr.name; return _expr.name;
@ -166,7 +166,7 @@ void SMTLib2Interface::write(string _data)
m_accumulatedOutput.back() += move(_data) + "\n"; m_accumulatedOutput.back() += move(_data) + "\n";
} }
string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _expressionsToEvaluate) string SMTLib2Interface::checkSatAndGetValuesCommand(vector<smt::Expression> const& _expressionsToEvaluate)
{ {
string command; string command;
if (_expressionsToEvaluate.empty()) if (_expressionsToEvaluate.empty())

8
libsolidity/formal/SMTLib2Interface.h
View File

@ -50,21 +50,21 @@ public:
void declareVariable(std::string const&, Sort const&) override; void declareVariable(std::string const&, Sort const&) override;
void addAssertion(Expression const& _expr) override; void addAssertion(smt::Expression const& _expr) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override; std::pair<CheckResult, std::vector<std::string>> check(std::vector<smt::Expression> const& _expressionsToEvaluate) override;
std::vector<std::string> unhandledQueries() override { return m_unhandledQueries; } std::vector<std::string> unhandledQueries() override { return m_unhandledQueries; }
private: private:
void declareFunction(std::string const&, Sort const&); void declareFunction(std::string const&, Sort const&);
std::string toSExpr(Expression const& _expr); std::string toSExpr(smt::Expression const& _expr);
std::string toSmtLibSort(Sort const& _sort); std::string toSmtLibSort(Sort const& _sort);
std::string toSmtLibSort(std::vector<SortPointer> const& _sort); std::string toSmtLibSort(std::vector<SortPointer> const& _sort);
void write(std::string _data); void write(std::string _data);
std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate); std::string checkSatAndGetValuesCommand(std::vector<smt::Expression> const& _expressionsToEvaluate);
std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end); std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end);
/// Communicates with the solver via the callback. Throws SMTSolverError on error. /// Communicates with the solver via the callback. Throws SMTSolverError on error.

4
libsolidity/formal/SMTPortfolio.cpp
View File

@ -65,7 +65,7 @@ void SMTPortfolio::declareVariable(string const& _name, Sort const& _sort)
s->declareVariable(_name, _sort); s->declareVariable(_name, _sort);
} }
void SMTPortfolio::addAssertion(Expression const& _expr) void SMTPortfolio::addAssertion(smt::Expression const& _expr)
{ {
for (auto const& s: m_solvers) for (auto const& s: m_solvers)
s->addAssertion(_expr); s->addAssertion(_expr);
@ -101,7 +101,7 @@ void SMTPortfolio::addAssertion(Expression const& _expr)
* *
* If all solvers return ERROR, the result is ERROR. * If all solvers return ERROR, the result is ERROR.
*/ */
pair<CheckResult, vector<string>> SMTPortfolio::check(vector<Expression> const& _expressionsToEvaluate) pair<CheckResult, vector<string>> SMTPortfolio::check(vector<smt::Expression> const& _expressionsToEvaluate)
{ {
CheckResult lastResult = CheckResult::ERROR; CheckResult lastResult = CheckResult::ERROR;
vector<string> finalValues; vector<string> finalValues;

6
libsolidity/formal/SMTPortfolio.h
View File

@ -51,9 +51,9 @@ public:
void declareVariable(std::string const&, Sort const&) override; void declareVariable(std::string const&, Sort const&) override;
void addAssertion(Expression const& _expr) override; void addAssertion(smt::Expression const& _expr) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override; std::pair<CheckResult, std::vector<std::string>> check(std::vector<smt::Expression> const& _expressionsToEvaluate) override;
std::vector<std::string> unhandledQueries() override; std::vector<std::string> unhandledQueries() override;
unsigned solvers() override { return m_solvers.size(); } unsigned solvers() override { return m_solvers.size(); }
@ -62,7 +62,7 @@ private:
std::vector<std::unique_ptr<smt::SolverInterface>> m_solvers; std::vector<std::unique_ptr<smt::SolverInterface>> m_solvers;
std::vector<Expression> m_assertions; std::vector<smt::Expression> m_assertions;
}; };
} }