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

More solsmt.

Browse Source
This commit is contained in:
chriseth 2022-05-10 09:43:47 +02:00
parent 91f32a7beb
commit 33f952dc5f
2 changed files with 35 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libsolutil/BooleanLP.cpp
View File

@ -289,8 +289,8 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
{ {
cout << "==============> CDCL final result: SATisfiable / UNKNOWN." << endl; cout << "==============> CDCL final result: SATisfiable / UNKNOWN." << endl;
// TODO should be "unknown" later on // TODO should be "unknown" later on
//return {CheckResult::SATISFIABLE, {}}; return {CheckResult::SATISFIABLE, {}};
return {CheckResult::UNKNOWN, {}}; //return {CheckResult::UNKNOWN, {}};
} }
} }

36
tools/solsmt.cpp
View File

@ -59,7 +59,6 @@ public:
SMTLib2Expression parseExpression() SMTLib2Expression parseExpression()
{ {
skipWhitespace(); skipWhitespace();
// TODO This does not check if there is trailing data after the closing ')'
if (token() == '(') if (token() == '(')
{ {
advance(); advance();
@ -87,10 +86,13 @@ private:
{ {
skipWhitespace(); skipWhitespace();
size_t start = m_pos; size_t start = m_pos;
bool isPipe = token() == '|';
while (m_pos < m_data.size()) while (m_pos < m_data.size())
{ {
char c = token(); char c = token();
if (langutil::isWhiteSpace(c) || c == '(' || c == ')') if (isPipe && (m_pos > start && c == '|'))
break;
else if (!isPipe && (langutil::isWhiteSpace(c) || c == '(' || c == ')'))
break; break;
advance(); advance();
} }
@ -160,6 +162,30 @@ smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr)
}, _expr.data); }, _expr.data);
} }
string removeComments(string _input)
{
string result;
auto it = _input.begin();
auto end = _input.end();
while (it != end)
{
if (*it == ';')
{
while (it != end && *it != '\n')
++it;
if (it != end)
++it;
}
else
{
result.push_back(*it);
it++;
}
}
return result;
}
} }
int main(int argc, char** argv) int main(int argc, char** argv)
@ -170,7 +196,7 @@ int main(int argc, char** argv)
return -1; return -1;
} }
string input = readFileAsString(argv[1]); string input = removeComments(readFileAsString(argv[1]));
string_view inputToParse = input; string_view inputToParse = input;
BooleanLPSolver solver; BooleanLPSolver solver;
@ -196,6 +222,10 @@ int main(int argc, char** argv)
SortPointer sort = type == "Real" ? SortProvider::intSort() : SortProvider::boolSort; SortPointer sort = type == "Real" ? SortProvider::intSort() : SortProvider::boolSort;
solver.declareVariable(variableName, move(sort)); solver.declareVariable(variableName, move(sort));
} }
else if (cmd == "define-fun")
{
cerr << "Ignoring 'define-fun'" << endl;
}
else if (cmd == "assert") else if (cmd == "assert")
{ {
solAssert(items.size() == 2); solAssert(items.size() == 2);