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

Print success.

Browse Source
This commit is contained in:
chriseth 2022-06-27 17:43:58 +02:00
parent cc3c2138a6
commit 7abe2750c6
1 changed files with 21 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
tools/solsmt.cpp
View File

@ -232,9 +232,12 @@ int main(int argc, char** argv)
string input = removeComments(readFileAsString(argv[1]));
string_view inputToParse = input;
bool printSuccess = false;
// bool produceModels = false;
map<string, SortPointer> variableSorts;
BooleanLPSolver solver;
while (true)
bool doExit = false;
while (!doExit)
{
while (!inputToParse.empty() && isWhiteSpace(inputToParse.front()))
inputToParse = inputToParse.substr(1);
@ -252,10 +255,19 @@ int main(int argc, char** argv)
vector<SMTLib2Expression> const& items = get<vector<SMTLib2Expression>>(expr.data);
string_view cmd = command(expr);
if (cmd == "set-info")
continue; // ignore
{
// ignore
}
else if (cmd == "set-option")
// TODO we sholud handle print-success
continue; // ignore
{
solAssert(items.size() >= 2);
string_view option = get<string_view>(items[1].data);
if (option == ":print-success")
printSuccess = (get<string_view>(items[2].data) == "true");
// else if (option == ":produce-models")
// produceModels = (get<string_view>(items[2].data) == "true");
// ignore the rest
}
else if (cmd == "declare-fun")
{
solAssert(items.size() == 4);
@ -301,11 +313,15 @@ int main(int argc, char** argv)
cout << "unsat" << endl;
else
cout << "unknown" << endl;
// do not print "success"
continue;
}
else if (cmd == "exit")
return 0;
doExit = true;
else
solAssert(false, "Unknown instruction: " + string(cmd));
if (printSuccess)
cout << "success" << endl;
}
return 0;