patrick/anthem
1
0
Fork 0
Code Issues 15 Releases 21 Activity

Fixed incorrectly named auxiliary body variable counter.

Browse Source
This commit is contained in:
Patrick Lühne 2017-03-28 17:24:41 +02:00
parent 67864fedbd
commit 29233a7430
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
2 changed files with 13 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
include/anthem/Body.h
View File

@ -40,7 +40,7 @@ ast::Comparison::Operator translate(Clingo::AST::ComparisonOperator comparisonOp
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
ast::Variable makeAuxiliaryBodyVariable(const int i) ast::Variable makeAuxiliaryBodyVariable(int i)
{ {
auto variableName = std::string(AuxiliaryBodyVariablePrefix) + std::to_string(i); auto variableName = std::string(AuxiliaryBodyVariablePrefix) + std::to_string(i);
@ -94,28 +94,28 @@ struct BodyTermTranslateVisitor
variables.reserve(function.arguments.size()); variables.reserve(function.arguments.size());
for (size_t i = 0; i < function.arguments.size(); i++) for (size_t i = 0; i < function.arguments.size(); i++)
variables.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + i)); variables.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyVariableID + i));
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++)
{ {
const auto &argument = function.arguments[i]; const auto &argument = function.arguments[i];
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + i), translate(argument, context))); conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(makeAuxiliaryBodyVariable(context.auxiliaryBodyVariableID + i), translate(argument, context)));
} }
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());
for (size_t i = 0; i < function.arguments.size(); i++) for (size_t i = 0; i < function.arguments.size(); i++)
predicate.arguments.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + i)); predicate.arguments.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyVariableID + i));
if (literal.sign == Clingo::AST::Sign::None) if (literal.sign == Clingo::AST::Sign::None)
conjunction.arguments.emplace_back(std::move(predicate)); conjunction.arguments.emplace_back(std::move(predicate));
else else
conjunction.arguments.emplace_back(ast::Formula::make<ast::Not>(std::move(predicate))); conjunction.arguments.emplace_back(ast::Formula::make<ast::Not>(std::move(predicate)));
context.auxiliaryBodyLiteralID += function.arguments.size(); context.auxiliaryBodyVariableID += function.arguments.size();
return ast::Formula::make<ast::Exists>(std::move(variables), std::move(conjunction)); return ast::Formula::make<ast::Exists>(std::move(variables), std::move(conjunction));
} }
@ -154,16 +154,16 @@ struct BodyLiteralTranslateVisitor
std::vector<ast::Variable> variables; std::vector<ast::Variable> variables;
variables.reserve(2); variables.reserve(2);
variables.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID)); variables.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyVariableID));
variables.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + 1)); variables.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyVariableID + 1));
ast::And conjunction; ast::And conjunction;
conjunction.arguments.reserve(3); conjunction.arguments.reserve(3);
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID), translate(comparison.left, context))); conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(makeAuxiliaryBodyVariable(context.auxiliaryBodyVariableID), translate(comparison.left, context)));
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + 1), translate(comparison.right, context))); conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(makeAuxiliaryBodyVariable(context.auxiliaryBodyVariableID + 1), translate(comparison.right, context)));
conjunction.arguments.emplace_back(ast::Formula::make<ast::Comparison>(operator_, makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID), makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + 1))); conjunction.arguments.emplace_back(ast::Formula::make<ast::Comparison>(operator_, makeAuxiliaryBodyVariable(context.auxiliaryBodyVariableID), makeAuxiliaryBodyVariable(context.auxiliaryBodyVariableID + 1)));
context.auxiliaryBodyLiteralID += 2; context.auxiliaryBodyVariableID += 2;
return ast::Formula::make<ast::Exists>(std::move(variables), std::move(conjunction)); return ast::Formula::make<ast::Exists>(std::move(variables), std::move(conjunction));
} }

4
include/anthem/Context.h
View File

@ -21,7 +21,7 @@ struct Context
headTerms.clear(); headTerms.clear();
isChoiceRule = false; isChoiceRule = false;
numberOfHeadLiterals = 0; numberOfHeadLiterals = 0;
auxiliaryBodyLiteralID = 1; auxiliaryBodyVariableID = 1;
} }
output::Logger logger; output::Logger logger;
@ -29,7 +29,7 @@ struct Context
std::vector<const Clingo::AST::Term *> headTerms; std::vector<const Clingo::AST::Term *> headTerms;
bool isChoiceRule = false; bool isChoiceRule = false;
size_t numberOfHeadLiterals = 0; size_t numberOfHeadLiterals = 0;
size_t auxiliaryBodyLiteralID = 1; size_t auxiliaryBodyVariableID = 1;
bool simplify = false; bool simplify = false;
}; };