diff --git a/include/anthem/Context.h b/include/anthem/Context.h index 7867ef1..3129f37 100644 --- a/include/anthem/Context.h +++ b/include/anthem/Context.h @@ -22,6 +22,7 @@ struct Context isChoiceRule = false; numberOfHeadLiterals = 0; auxiliaryBodyVariableID = 1; + anonymousVariableID = 1; } output::Logger logger; @@ -30,6 +31,7 @@ struct Context bool isChoiceRule = false; size_t numberOfHeadLiterals = 0; size_t auxiliaryBodyVariableID = 1; + size_t anonymousVariableID = 1; bool simplify = false; }; diff --git a/include/anthem/Term.h b/include/anthem/Term.h index 1904240..6caae0e 100644 --- a/include/anthem/Term.h +++ b/include/anthem/Term.h @@ -83,8 +83,16 @@ struct TermTranslateVisitor return std::experimental::nullopt; } - std::experimental::optional visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, Context &) + std::experimental::optional visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, Context &context) { + if (strcmp(variable.name, "_") == 0) + { + std::string variableName = AnonymousVariablePrefix + std::to_string(context.anonymousVariableID); + context.anonymousVariableID++; + + return ast::Term::make(std::move(variableName), ast::Variable::Type::Reserved); + } + return ast::Term::make(std::string(variable.name), ast::Variable::Type::UserDefined); } diff --git a/include/anthem/Utils.h b/include/anthem/Utils.h index d62186e..a6f4fdd 100644 --- a/include/anthem/Utils.h +++ b/include/anthem/Utils.h @@ -58,6 +58,7 @@ inline bool isPrefix(const char *prefix, const char *string) constexpr const auto AuxiliaryHeadVariablePrefix = "V"; constexpr const auto AuxiliaryBodyVariablePrefix = "X"; +constexpr const auto AnonymousVariablePrefix = "A"; constexpr const auto UserVariablePrefix = "_"; //////////////////////////////////////////////////////////////////////////////////////////////////// @@ -65,12 +66,14 @@ constexpr const auto UserVariablePrefix = "_"; inline bool isReservedVariableName(const char *variableName) { if (!isPrefix(AuxiliaryBodyVariablePrefix, variableName) - && !isPrefix(AuxiliaryHeadVariablePrefix, variableName)) + && !isPrefix(AuxiliaryHeadVariablePrefix, variableName) + && !isPrefix(AnonymousVariablePrefix, variableName)) { return false; } assert(std::strlen(AuxiliaryBodyVariablePrefix) == std::strlen(AuxiliaryHeadVariablePrefix)); + assert(std::strlen(AuxiliaryBodyVariablePrefix) == std::strlen(AnonymousVariablePrefix)); const auto prefixLength = std::strlen(AuxiliaryBodyVariablePrefix); diff --git a/include/anthem/output/AST.h b/include/anthem/output/AST.h index b27bf93..cbad6be 100644 --- a/include/anthem/output/AST.h +++ b/include/anthem/output/AST.h @@ -216,6 +216,7 @@ inline output::ColorStream &operator<<(output::ColorStream &stream, const String inline output::ColorStream &operator<<(output::ColorStream &stream, const Variable &variable) { assert(!variable.name.empty()); + assert(variable.name != "_"); if (variable.type == ast::Variable::Type::Reserved || !isReservedVariableName(variable.name.c_str())) return (stream << output::Variable(variable.name.c_str())); diff --git a/tests/TestTranslation.cpp b/tests/TestTranslation.cpp index 19b66d8..9146b0d 100644 --- a/tests/TestTranslation.cpp +++ b/tests/TestTranslation.cpp @@ -69,10 +69,10 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("escaping conflicting variable names") { - input << "p(X1, V1) :- q(X1), q(V1)."; + input << "p(X1, V1, A1) :- q(X1), q(V1), q(A1)."; anthem::translate("input", input, context); - REQUIRE(output.str() == "((V1 in _X1 and V2 in _V1 and exists X1 (X1 in _X1 and q(X1)) and exists X2 (X2 in _V1 and q(X2))) -> p(V1, V2))\n"); + REQUIRE(output.str() == "((V1 in _X1 and V2 in _V1 and V3 in _A1 and exists X1 (X1 in _X1 and q(X1)) and exists X2 (X2 in _V1 and q(X2)) and exists X3 (X3 in _A1 and q(X3))) -> p(V1, V2, V3))\n"); } SECTION("fact") @@ -201,8 +201,8 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "f; q(A1, A2); p(A3, r(A4)); g(g(A5)) :- g(A3), f, q(A4, A1), p(A2, A5)."; anthem::translate("input", input, context); - REQUIRE(output.str() == "((V1 in A1 and V2 in A2 and V3 in A3 and V4 in r(A4) and V5 in g(A5)" - " and exists X1 (X1 in A3 and g(X1)) and f and exists X2, X3 (X2 in A4 and X3 in A1 and q(X2, X3)) and exists X4, X5 (X4 in A2 and X5 in A5 and p(X4, X5)))" + REQUIRE(output.str() == "((V1 in _A1 and V2 in _A2 and V3 in _A3 and V4 in r(_A4) and V5 in g(_A5)" + " and exists X1 (X1 in _A3 and g(X1)) and f and exists X2, X3 (X2 in _A4 and X3 in _A1 and q(X2, X3)) and exists X4, X5 (X4 in _A2 and X5 in _A5 and p(X4, X5)))" " -> (q(V1, V2) or p(V3, V4) or g(V5) or f))\n"); } @@ -261,4 +261,12 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") REQUIRE(output.str() == "((V1 in X and V2 in 1 and exists X1, X2 (X1 in X and X2 in 2 and not q(X1, X2)) and not p(V1, V2)) -> not p(V1, V2))\n((V1 in X and V2 in 1 and exists X1, X2 (X1 in X and X2 in 2 and not q(X1, X2)) and not s) -> not s)\n"); } + + SECTION("anonymous variables") + { + input << "p(_, _) :- q(_, _)."; + anthem::translate("input", input, context); + + REQUIRE(output.str() == "((V1 in A1 and V2 in A2 and exists X1, X2 (X1 in A3 and X2 in A4 and q(X1, X2))) -> p(V1, V2))\n"); + } }