From 33f952dc5faf7afe2e7053064a7aa5601669dc73 Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Tue, 10 May 2022 09:43:47 +0200
Subject: [PATCH] More solsmt.

---
 libsolutil/BooleanLP.cpp |  4 ++--
 tools/solsmt.cpp         | 36 +++++++++++++++++++++++++++++++++---
 2 files changed, 35 insertions(+), 5 deletions(-)

diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp
index e313cbacd..251bd57d0 100644
--- a/libsolutil/BooleanLP.cpp
+++ b/libsolutil/BooleanLP.cpp
@@ -289,8 +289,8 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
 	{
 		cout << "==============> CDCL final result: SATisfiable / UNKNOWN." << endl;
 		// TODO should be "unknown" later on
-		//return {CheckResult::SATISFIABLE, {}};
-		return {CheckResult::UNKNOWN, {}};
+		return {CheckResult::SATISFIABLE, {}};
+		//return {CheckResult::UNKNOWN, {}};
 	}
 }
 
diff --git a/tools/solsmt.cpp b/tools/solsmt.cpp
index 7b8afd03c..e93d53e76 100644
--- a/tools/solsmt.cpp
+++ b/tools/solsmt.cpp
@@ -59,7 +59,6 @@ public:
 	SMTLib2Expression parseExpression()
 	{
 		skipWhitespace();
-		// TODO This does not check if there is trailing data after the closing ')'
 		if (token() == '(')
 		{
 			advance();
@@ -87,10 +86,13 @@ private:
 	{
 		skipWhitespace();
 		size_t start = m_pos;
+		bool isPipe = token() == '|';
 		while (m_pos < m_data.size())
 		{
 			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;
 			advance();
 		}
@@ -160,6 +162,30 @@ smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr)
 	}, _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)
@@ -170,7 +196,7 @@ int main(int argc, char** argv)
 		return -1;
 	}
 
-	string input = readFileAsString(argv[1]);
+	string input = removeComments(readFileAsString(argv[1]));
 	string_view inputToParse = input;
 
 	BooleanLPSolver solver;
@@ -196,6 +222,10 @@ int main(int argc, char** argv)
 			SortPointer sort = type == "Real" ? SortProvider::intSort() : SortProvider::boolSort;
 			solver.declareVariable(variableName, move(sort));
 		}
+		else if (cmd == "define-fun")
+		{
+			cerr << "Ignoring 'define-fun'" << endl;
+		}
 		else if (cmd == "assert")
 		{
 			solAssert(items.size() == 2);