From 66acbb8965692446c98491e34081a497aa7e5fff Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick-github@luehne.de>
Date: Thu, 24 Nov 2016 13:42:36 +0100
Subject: [PATCH] Changed output format of auxiliary variables and treated
 potential name collisions.

---
 include/anthem/Utils.h             | 44 ++++++++++++++++++++++++++++--
 src/anthem/output/ClingoOutput.cpp |  8 +++++-
 2 files changed, 49 insertions(+), 3 deletions(-)

diff --git a/include/anthem/Utils.h b/include/anthem/Utils.h
index 97785d7..4c90aad 100644
--- a/include/anthem/Utils.h
+++ b/include/anthem/Utils.h
@@ -43,8 +43,48 @@ inline void throwErrorAtLocation(const Clingo::Location &clingoLocation, const c
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-constexpr const auto AuxiliaryHeadVariablePrefix = "AUX_H";
-constexpr const auto AuxiliaryBodyVariablePrefix = "AUX_B";
+inline bool isPrefix(const char *prefix, const char *string)
+{
+	const auto prefixLength = std::strlen(prefix);
+	const auto stringLength = std::strlen(string);
+
+	if (stringLength < prefixLength)
+		return false;
+
+	return std::strncmp(prefix, string, prefixLength) == 0;
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+constexpr const auto AuxiliaryHeadVariablePrefix = "H";
+constexpr const auto AuxiliaryBodyVariablePrefix = "B";
+constexpr const auto UserVariablePrefix = "_";
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+inline bool isReservedVariableName(const char *variableName)
+{
+	if (!isPrefix(AuxiliaryBodyVariablePrefix, variableName)
+	    && !isPrefix(AuxiliaryHeadVariablePrefix, variableName))
+	{
+		return false;
+	}
+
+	assert(std::strlen(AuxiliaryBodyVariablePrefix) == std::strlen(AuxiliaryHeadVariablePrefix));
+
+	const auto prefixLength = std::strlen(AuxiliaryBodyVariablePrefix);
+
+	if (strlen(variableName) == prefixLength)
+		return false;
+
+	const char *suffix = variableName + prefixLength;
+
+	for (const auto *i = suffix; *i != '\0'; i++)
+		if (!std::isdigit(*i))
+			return false;
+
+	return true;
+}
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
diff --git a/src/anthem/output/ClingoOutput.cpp b/src/anthem/output/ClingoOutput.cpp
index 1c1d0d4..dd6cf39 100644
--- a/src/anthem/output/ClingoOutput.cpp
+++ b/src/anthem/output/ClingoOutput.cpp
@@ -1,5 +1,6 @@
 #include <anthem/output/ClingoOutput.h>
 
+#include <anthem/Utils.h>
 #include <anthem/output/Formatting.h>
 
 namespace anthem
@@ -108,7 +109,12 @@ ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Boolean &boolean
 
 ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Variable &variable)
 {
-	return (stream << Variable(variable.name));
+	if (!isReservedVariableName(variable.name))
+		return (stream << Variable(variable.name));
+
+	const auto variableName = std::string(UserVariablePrefix) + variable.name;
+
+	return (stream << Variable(variableName.c_str()));
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////