Fixed issue with multi-layer variable stacks.
This commit is contained in:
parent
7aad8380d1
commit
664a57ec68
@ -62,11 +62,12 @@ struct BodyTermTranslateVisitor
|
|||||||
std::vector<std::unique_ptr<ast::VariableDeclaration>> parameters;
|
std::vector<std::unique_ptr<ast::VariableDeclaration>> parameters;
|
||||||
parameters.reserve(function.arguments.size());
|
parameters.reserve(function.arguments.size());
|
||||||
|
|
||||||
variableStack.push(¶meters);
|
|
||||||
|
|
||||||
for (size_t i = 0; i < function.arguments.size(); i++)
|
for (size_t i = 0; i < function.arguments.size(); i++)
|
||||||
parameters.emplace_back(std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::Body));
|
parameters.emplace_back(std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::Body));
|
||||||
|
|
||||||
|
// TODO: implement pushing with scoped guards to avoid bugs
|
||||||
|
variableStack.push(¶meters);
|
||||||
|
|
||||||
ast::And conjunction;
|
ast::And conjunction;
|
||||||
|
|
||||||
for (size_t i = 0; i < function.arguments.size(); i++)
|
for (size_t i = 0; i < function.arguments.size(); i++)
|
||||||
@ -75,6 +76,8 @@ struct BodyTermTranslateVisitor
|
|||||||
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[i].get()), translate(argument, context, ruleContext, variableStack)));
|
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[i].get()), translate(argument, context, ruleContext, variableStack)));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
variableStack.pop();
|
||||||
|
|
||||||
ast::Predicate predicate(std::string(function.name));
|
ast::Predicate predicate(std::string(function.name));
|
||||||
predicate.arguments.reserve(function.arguments.size());
|
predicate.arguments.reserve(function.arguments.size());
|
||||||
|
|
||||||
|
@ -29,7 +29,7 @@ void VariableStack::pop()
|
|||||||
|
|
||||||
std::experimental::optional<ast::VariableDeclaration *> VariableStack::findUserVariableDeclaration(const char *variableName) const
|
std::experimental::optional<ast::VariableDeclaration *> VariableStack::findUserVariableDeclaration(const char *variableName) const
|
||||||
{
|
{
|
||||||
const auto variableNameMatches =
|
const auto variableDeclarationMatches =
|
||||||
[&variableName](const auto &variableDeclaration)
|
[&variableName](const auto &variableDeclaration)
|
||||||
{
|
{
|
||||||
return variableDeclaration->type == VariableDeclaration::Type::UserDefined
|
return variableDeclaration->type == VariableDeclaration::Type::UserDefined
|
||||||
@ -39,7 +39,7 @@ std::experimental::optional<ast::VariableDeclaration *> VariableStack::findUserV
|
|||||||
for (auto i = m_layers.rbegin(); i != m_layers.rend(); i++)
|
for (auto i = m_layers.rbegin(); i != m_layers.rend(); i++)
|
||||||
{
|
{
|
||||||
auto &layer = **i;
|
auto &layer = **i;
|
||||||
const auto matchingVariableDeclaration = std::find_if(layer.begin(), layer.end(), variableNameMatches);
|
const auto matchingVariableDeclaration = std::find_if(layer.begin(), layer.end(), variableDeclarationMatches);
|
||||||
|
|
||||||
if (matchingVariableDeclaration != layer.end())
|
if (matchingVariableDeclaration != layer.end())
|
||||||
return matchingVariableDeclaration->get();
|
return matchingVariableDeclaration->get();
|
||||||
|
@ -181,6 +181,22 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
|
|||||||
CHECK(output.str() == "((V1 in U1 and V2 in 1..10 and exists X1, X2 (X1 in U1 and X2 in 6..12 and q(X1, X2))) -> p(V1, V2))\n");
|
CHECK(output.str() == "((V1 in U1 and V2 in 1..10 and exists X1, X2 (X1 in U1 and X2 in 6..12 and q(X1, X2))) -> p(V1, V2))\n");
|
||||||
}
|
}
|
||||||
|
|
||||||
|
SECTION("intervals with variable")
|
||||||
|
{
|
||||||
|
input << ":- q(N), 1 = 1..N.";
|
||||||
|
anthem::translate("input", input, context);
|
||||||
|
|
||||||
|
CHECK(output.str() == "((exists X1 (X1 in U1 and q(X1)) and exists X2, X3 (X2 in 1 and X3 in 1..U1 and X2 = X3)) -> #false)\n");
|
||||||
|
}
|
||||||
|
|
||||||
|
SECTION("intervals with two variables")
|
||||||
|
{
|
||||||
|
input << ":- q(M, N), M = 1..N.";
|
||||||
|
anthem::translate("input", input, context);
|
||||||
|
|
||||||
|
CHECK(output.str() == "((exists X1, X2 (X1 in U1 and X2 in U2 and q(X1, X2)) and exists X3, X4 (X3 in U1 and X4 in 1..U2 and X3 = X4)) -> #false)\n");
|
||||||
|
}
|
||||||
|
|
||||||
SECTION("comparisons")
|
SECTION("comparisons")
|
||||||
{
|
{
|
||||||
input << "p(M, N, O, P) :- M < N, P != O.";
|
input << "p(M, N, O, P) :- M < N, P != O.";
|
||||||
|
Loading…
Reference in New Issue
Block a user