Changed output format of auxiliary variables and treated potential name collisions.

include/anthem/Utils.h

@@ -43,8 +43,48 @@ inline void throwErrorAtLocation(const Clingo::Location &clingoLocation, const c
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-constexpr const auto AuxiliaryHeadVariablePrefix = "AUX_H";
+inline bool isPrefix(const char *prefix, const char *string)
-constexpr const auto AuxiliaryBodyVariablePrefix = "AUX_B";
+{
+	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;
+}
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 

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()));
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////