cerc-io/solidity
11
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

[SMTChecker] SMTPortfolio: use all SMT solvers available

Browse Source
This commit is contained in:
Leonardo Alt
2018-07-27 16:15:34 +01:00
committed by Alex Beregszaszi
parent 5faa60e883
commit 87a38e1abe
11 changed files with 262 additions and 58 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/CVC4Interface.cpp
+3 -6
View File
@@ -50,23 +50,20 @@ void CVC4Interface::pop()
m_solver.pop();
}
Expression CVC4Interface::newFunction(string _name, Sort _domain, Sort _codomain)
void CVC4Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
{
CVC4::Type fType = m_context.mkFunctionType(cvc4Sort(_domain), cvc4Sort(_codomain));
m_functions.insert({_name, m_context.mkVar(_name.c_str(), fType)});
return SolverInterface::newFunction(move(_name), _domain, _codomain);
}
Expression CVC4Interface::newInteger(string _name)
void CVC4Interface::declareInteger(string _name)
{
m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.integerType())});
return SolverInterface::newInteger(move(_name));
}
Expression CVC4Interface::newBool(string _name)
void CVC4Interface::declareBool(string _name)
{
m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.booleanType())});
return SolverInterface::newBool(std::move(_name));
}
void CVC4Interface::addAssertion(Expression const& _expr)