SMTChecker: Move helper function towards its only usage

We don't need a separate file for a single, relatively small, helper
function.

Author: blishko

libsolidity/CMakeLists.txt

@@ -117,8 +117,6 @@ set(sources
 	formal/EncodingContext.h
 	formal/ExpressionFormatter.cpp
 	formal/ExpressionFormatter.h
-	formal/Invariants.cpp
-	formal/Invariants.h
 	formal/ModelChecker.cpp
 	formal/ModelChecker.h
 	formal/ModelCheckerSettings.cpp

libsolidity/formal/CHC.cpp

@@ -19,8 +19,8 @@
 #include <libsolidity/formal/CHC.h>
 
 #include <libsolidity/formal/ArraySlicePredicate.h>
+#include <libsolidity/formal/ExpressionFormatter.h>
 #include <libsolidity/formal/EldaricaCHCSmtLib2Interface.h>
-#include <libsolidity/formal/Invariants.h>
 #include <libsolidity/formal/ModelChecker.h>
 #include <libsolidity/formal/PredicateInstance.h>
 #include <libsolidity/formal/PredicateSort.h>
@@ -2134,6 +2134,58 @@ void CHC::checkVerificationTargets()
 		m_safeTargets[m_verificationTargets.at(id).errorNode].insert(m_verificationTargets.at(id));
 }
 
+namespace
+{
+std::map<Predicate const*, std::set<std::string>> collectInvariants(
+	smtutil::Expression const& _proof,
+	std::set<Predicate const*> const& _predicates,
+	ModelCheckerInvariants const& _invariantsSetting
+)
+{
+	std::set<std::string> targets;
+	if (_invariantsSetting.has(InvariantType::Contract))
+		targets.insert("interface_");
+	if (_invariantsSetting.has(InvariantType::Reentrancy))
+		targets.insert("nondet_interface_");
+
+	std::map<std::string, std::pair<smtutil::Expression, smtutil::Expression>> equalities;
+	// Collect equalities where one of the sides is a predicate we're interested in.
+	util::BreadthFirstSearch<smtutil::Expression const*>{{&_proof}}.run([&](auto&& _expr, auto&& _addChild) {
+		if (_expr->name == "=")
+			for (auto const& t: targets)
+			{
+				auto arg0 = _expr->arguments.at(0);
+				auto arg1 = _expr->arguments.at(1);
+				if (boost::algorithm::starts_with(arg0.name, t))
+					equalities.insert({arg0.name, {arg0, std::move(arg1)}});
+				else if (boost::algorithm::starts_with(arg1.name, t))
+					equalities.insert({arg1.name, {arg1, std::move(arg0)}});
+			}
+		for (auto const& arg: _expr->arguments)
+			_addChild(&arg);
+	});
+
+	std::map<Predicate const*, std::set<std::string>> invariants;
+	for (auto pred: _predicates)
+	{
+		auto predName = pred->functor().name;
+		if (!equalities.count(predName))
+			continue;
+
+		solAssert(pred->contextContract(), "");
+
+		auto const& [predExpr, invExpr] = equalities.at(predName);
+
+		static std::set<std::string> const ignore{"true", "false"};
+		auto r = substitute(invExpr, pred->expressionSubstitution(predExpr));
+		// No point in reporting true/false as invariants.
+		if (!ignore.count(r.name))
+			invariants[pred].insert(toSolidityStr(r));
+	}
+	return invariants;
+}
+} // namespace
+
 void CHC::checkAndReportTarget(
 	CHCVerificationTarget const& _target,
 	std::vector<CHCQueryPlaceholder> const& _placeholders,