From d5f00842d984cca139fd74d2d3d37ca5f8c24014 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Fri, 17 Jul 2020 12:26:55 +0200
Subject: [PATCH] cex2dot debug

---
 libsolidity/formal/CHC.cpp | 16 ++++++++++++++++
 libsolidity/formal/CHC.h   |  4 ++++
 2 files changed, 20 insertions(+)

diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index 3a865c4bc..2615cf9d7 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -1471,6 +1471,22 @@ string CHC::formatFunctionCallCounterexample(vector<VariableDeclaration const*>
 	return fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")";
 }
 
+string CHC::cex2dot(smtutil::CHCSolverInterface::CexGraph const& _cex)
+{
+	string dot = "digraph {\n";
+
+	auto pred = [&](CHCSolverInterface::CexNode const& _node) {
+		return "\"" + _node.first + "(" + boost::algorithm::join(_node.second, ", ") + ")\"";
+	};
+
+	for (auto const& [u, vs]: _cex.edges)
+		for (auto v: vs)
+			dot += pred(_cex.nodes.at(v)) + " -> " + pred(_cex.nodes.at(u)) + "\n";
+
+	dot += "}";
+	return dot;
+}
+
 string CHC::uniquePrefix()
 {
 	return to_string(m_blockCounter++);
diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h
index 1b2ec493d..8342524bb 100644
--- a/libsolidity/formal/CHC.h
+++ b/libsolidity/formal/CHC.h
@@ -223,6 +223,10 @@ private:
 	/// with the concrete values for value type parameters and
 	/// the parameter name for reference types.
 	std::string formatFunctionCallCounterexample(std::vector<VariableDeclaration const*> const& _stateVariables, FunctionDefinition const& _function, std::vector<std::string> const& _summaryValues);
+
+	/// @returns a DAG in the dot format.
+	/// Used for debugging purposes.
+	std::string cex2dot(smtutil::CHCSolverInterface::CexGraph const& _graph);
 	//@}
 
 	/// Misc.