Split functions from their declarations

This splits occurrences of functions from their declaration. This is
necessary to flag integer functions consistently and not just single
occurrences.
This commit is contained in:
Patrick Lühne 2018-04-19 15:41:36 +02:00 committed by Patrick Lühne
parent d0debc6ad1
commit 618189368c
No known key found for this signature in database
GPG Key ID: 05F3611E97A70ABF
9 changed files with 87 additions and 37 deletions

View File

@ -105,13 +105,13 @@ struct Comparison
struct Function struct Function
{ {
explicit Function(std::string &&name) explicit Function(FunctionDeclaration *declaration)
: name{std::move(name)} : declaration{declaration}
{ {
} }
explicit Function(std::string &&name, std::vector<Term> &&arguments) explicit Function(FunctionDeclaration *declaration, std::vector<Term> &&arguments)
: name{std::move(name)}, : declaration{declaration},
arguments{std::move(arguments)} arguments{std::move(arguments)}
{ {
} }
@ -121,12 +121,36 @@ struct Function
Function(Function &&other) noexcept = default; Function(Function &&other) noexcept = default;
Function &operator=(Function &&other) noexcept = default; Function &operator=(Function &&other) noexcept = default;
std::string name; FunctionDeclaration *declaration;
std::vector<Term> arguments; std::vector<Term> arguments;
}; };
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
struct FunctionDeclaration
{
explicit FunctionDeclaration(std::string &&name)
: name{std::move(name)}
{
}
explicit FunctionDeclaration(std::string &&name, size_t arity)
: name{std::move(name)},
arity{arity}
{
}
FunctionDeclaration(const FunctionDeclaration &other) = delete;
FunctionDeclaration &operator=(const FunctionDeclaration &other) = delete;
FunctionDeclaration(FunctionDeclaration &&other) noexcept = default;
FunctionDeclaration &operator=(FunctionDeclaration &&other) noexcept = default;
std::string name;
size_t arity;
};
////////////////////////////////////////////////////////////////////////////////////////////////////
// TODO: refactor (limit element type to primitive terms) // TODO: refactor (limit element type to primitive terms)
struct In struct In
{ {

View File

@ -27,6 +27,7 @@ struct Comparison;
struct Exists; struct Exists;
struct ForAll; struct ForAll;
struct Function; struct Function;
struct FunctionDeclaration;
struct Implies; struct Implies;
struct In; struct In;
struct Integer; struct Integer;

View File

@ -76,7 +76,7 @@ struct BodyTermTranslateVisitor
for (size_t i = 0; i < function.arguments.size(); i++) for (size_t i = 0; i < function.arguments.size(); i++)
{ {
auto &argument = function.arguments[i]; auto &argument = function.arguments[i];
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[i].get()), translate(argument, ruleContext, variableStack))); conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[i].get()), translate(argument, ruleContext, context, variableStack)));
} }
variableStack.pop(); variableStack.pop();
@ -121,7 +121,7 @@ struct BodyLiteralTranslateVisitor
} }
// TODO: refactor // TODO: refactor
std::optional<ast::Formula> visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, Context &, ast::VariableStack &variableStack) std::optional<ast::Formula> visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack)
{ {
// Comparisons should never have a sign, because these are converted to positive comparisons by clingo // Comparisons should never have a sign, because these are converted to positive comparisons by clingo
if (literal.sign != Clingo::AST::Sign::None) if (literal.sign != Clingo::AST::Sign::None)
@ -136,8 +136,8 @@ struct BodyLiteralTranslateVisitor
ast::And conjunction; ast::And conjunction;
conjunction.arguments.reserve(3); conjunction.arguments.reserve(3);
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[0].get()), translate(comparison.left, ruleContext, variableStack))); conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[0].get()), translate(comparison.left, ruleContext, context, variableStack)));
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[1].get()), translate(comparison.right, ruleContext, variableStack))); conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[1].get()), translate(comparison.right, ruleContext, context, variableStack)));
conjunction.arguments.emplace_back(ast::Formula::make<ast::Comparison>(operator_, ast::Variable(parameters[0].get()), ast::Variable(parameters[1].get()))); conjunction.arguments.emplace_back(ast::Formula::make<ast::Comparison>(operator_, ast::Variable(parameters[0].get()), ast::Variable(parameters[1].get())));
return ast::Formula::make<ast::Exists>(std::move(parameters), std::move(conjunction)); return ast::Formula::make<ast::Exists>(std::move(parameters), std::move(conjunction));

View File

@ -53,6 +53,26 @@ struct Context
return predicateDeclarations.back().get(); return predicateDeclarations.back().get();
} }
ast::FunctionDeclaration *findOrCreateFunctionDeclaration(const char *name, size_t arity)
{
const auto matchesExistingFunctionDeclaration =
[&](const auto &functionDeclarations)
{
return (functionDeclarations->arity == arity
&& strcmp(functionDeclarations->name.c_str(), name) == 0);
};
auto matchingFunctionDeclaration = std::find_if(functionDeclarations.begin(),
functionDeclarations.end(), matchesExistingFunctionDeclaration);
if (matchingFunctionDeclaration != functionDeclarations.end())
return matchingFunctionDeclaration->get();
functionDeclarations.emplace_back(std::make_unique<ast::FunctionDeclaration>(name, arity));
return functionDeclarations.back().get();
}
output::Logger logger; output::Logger logger;
bool performSimplification{false}; bool performSimplification{false};
@ -61,6 +81,8 @@ struct Context
std::vector<std::unique_ptr<ast::PredicateDeclaration>> predicateDeclarations; std::vector<std::unique_ptr<ast::PredicateDeclaration>> predicateDeclarations;
ast::PredicateDeclaration::Visibility defaultPredicateVisibility{ast::PredicateDeclaration::Visibility::Visible}; ast::PredicateDeclaration::Visibility defaultPredicateVisibility{ast::PredicateDeclaration::Visibility::Visible};
std::vector<std::unique_ptr<ast::FunctionDeclaration>> functionDeclarations;
bool externalStatementsUsed{false}; bool externalStatementsUsed{false};
bool showStatementsUsed{false}; bool showStatementsUsed{false};

View File

@ -305,7 +305,7 @@ struct TermEqualityVisitor
const auto &otherFunction = otherTerm.get<Function>(); const auto &otherFunction = otherTerm.get<Function>();
if (function.name != otherFunction.name) if (function.declaration != otherFunction.declaration)
return Tristate::False; return Tristate::False;
if (function.arguments.size() != otherFunction.arguments.size()) if (function.arguments.size() != otherFunction.arguments.size())

View File

@ -87,7 +87,7 @@ struct StatementVisitor
const auto auxiliaryHeadVariableID = ruleContext.headVariablesStartIndex + i - ruleContext.headTerms.cbegin(); const auto auxiliaryHeadVariableID = ruleContext.headVariablesStartIndex + i - ruleContext.headTerms.cbegin();
auto element = ast::Variable(ruleContext.freeVariables[auxiliaryHeadVariableID].get()); auto element = ast::Variable(ruleContext.freeVariables[auxiliaryHeadVariableID].get());
auto set = translate(headTerm, ruleContext, variableStack); auto set = translate(headTerm, ruleContext, context, variableStack);
auto in = ast::In(std::move(element), std::move(set)); auto in = ast::In(std::move(element), std::move(set));
antecedent.arguments.emplace_back(std::move(in)); antecedent.arguments.emplace_back(std::move(in));

View File

@ -65,13 +65,13 @@ ast::UnaryOperation::Operator translate(Clingo::AST::UnaryOperator unaryOperator
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack); ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack);
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
struct TermTranslateVisitor struct TermTranslateVisitor
{ {
std::optional<ast::Term> visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack) std::optional<ast::Term> visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
{ {
switch (symbol.type()) switch (symbol.type())
{ {
@ -85,19 +85,19 @@ struct TermTranslateVisitor
return ast::Term::make<ast::String>(std::string(symbol.string())); return ast::Term::make<ast::String>(std::string(symbol.string()));
case Clingo::SymbolType::Function: case Clingo::SymbolType::Function:
{ {
auto function = ast::Term::make<ast::Function>(symbol.name()); auto functionDeclaration = context.findOrCreateFunctionDeclaration(symbol.name(), symbol.arguments().size());
// TODO: remove workaround
auto &functionRaw = function.get<ast::Function>(); auto function = ast::Function(functionDeclaration);
functionRaw.arguments.reserve(symbol.arguments().size()); function.arguments.reserve(symbol.arguments().size());
for (const auto &argument : symbol.arguments()) for (const auto &argument : symbol.arguments())
{ {
auto translatedArgument = visit(argument, term, ruleContext, variableStack); auto translatedArgument = visit(argument, term, ruleContext, context, variableStack);
if (!translatedArgument) if (!translatedArgument)
throw TranslationException(term.location, "could not translate argument"); throw TranslationException(term.location, "could not translate argument");
functionRaw.arguments.emplace_back(std::move(translatedArgument.value())); function.arguments.emplace_back(std::move(translatedArgument.value()));
} }
return std::move(function); return std::move(function);
@ -107,7 +107,7 @@ struct TermTranslateVisitor
return std::nullopt; return std::nullopt;
} }
std::optional<ast::Term> visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack) std::optional<ast::Term> visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, RuleContext &ruleContext, Context &, const ast::VariableStack &variableStack)
{ {
const auto matchingVariableDeclaration = variableStack.findUserVariableDeclaration(variable.name); const auto matchingVariableDeclaration = variableStack.findUserVariableDeclaration(variable.name);
const auto isAnonymousVariable = (strcmp(variable.name, "_") == 0); const auto isAnonymousVariable = (strcmp(variable.name, "_") == 0);
@ -120,35 +120,36 @@ struct TermTranslateVisitor
auto variableDeclaration = std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::UserDefined, std::string(variable.name)); auto variableDeclaration = std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::UserDefined, std::string(variable.name));
ruleContext.freeVariables.emplace_back(std::move(variableDeclaration)); ruleContext.freeVariables.emplace_back(std::move(variableDeclaration));
// TODO: ast::Term::make is unnecessary and can be removed
return ast::Term::make<ast::Variable>(ruleContext.freeVariables.back().get()); return ast::Term::make<ast::Variable>(ruleContext.freeVariables.back().get());
} }
std::optional<ast::Term> visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack) std::optional<ast::Term> visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
{ {
const auto operator_ = translate(binaryOperation.binary_operator, term); const auto operator_ = translate(binaryOperation.binary_operator, term);
auto left = translate(binaryOperation.left, ruleContext, variableStack); auto left = translate(binaryOperation.left, ruleContext, context, variableStack);
auto right = translate(binaryOperation.right, ruleContext, variableStack); auto right = translate(binaryOperation.right, ruleContext, context, variableStack);
return ast::Term::make<ast::BinaryOperation>(operator_, std::move(left), std::move(right)); return ast::Term::make<ast::BinaryOperation>(operator_, std::move(left), std::move(right));
} }
std::optional<ast::Term> visit(const Clingo::AST::UnaryOperation &unaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack) std::optional<ast::Term> visit(const Clingo::AST::UnaryOperation &unaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
{ {
const auto operator_ = translate(unaryOperation.unary_operator, term); const auto operator_ = translate(unaryOperation.unary_operator, term);
auto argument = translate(unaryOperation.argument, ruleContext, variableStack); auto argument = translate(unaryOperation.argument, ruleContext, context, variableStack);
return ast::Term::make<ast::UnaryOperation>(operator_, std::move(argument)); return ast::Term::make<ast::UnaryOperation>(operator_, std::move(argument));
} }
std::optional<ast::Term> visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack) std::optional<ast::Term> visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
{ {
auto left = translate(interval.left, ruleContext, variableStack); auto left = translate(interval.left, ruleContext, context, variableStack);
auto right = translate(interval.right, ruleContext, variableStack); auto right = translate(interval.right, ruleContext, context, variableStack);
return ast::Term::make<ast::Interval>(std::move(left), std::move(right)); return ast::Term::make<ast::Interval>(std::move(left), std::move(right));
} }
std::optional<ast::Term> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack) std::optional<ast::Term> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
{ {
if (function.external) if (function.external)
throw TranslationException(term.location, "external functions currently unsupported"); throw TranslationException(term.location, "external functions currently unsupported");
@ -157,12 +158,14 @@ struct TermTranslateVisitor
arguments.reserve(function.arguments.size()); arguments.reserve(function.arguments.size());
for (const auto &argument : function.arguments) for (const auto &argument : function.arguments)
arguments.emplace_back(translate(argument, ruleContext, variableStack)); arguments.emplace_back(translate(argument, ruleContext, context, variableStack));
return ast::Term::make<ast::Function>(function.name, std::move(arguments)); auto functionDeclaration = context.findOrCreateFunctionDeclaration(function.name, function.arguments.size());
return ast::Term::make<ast::Function>(functionDeclaration, std::move(arguments));
} }
std::optional<ast::Term> visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, RuleContext &, const ast::VariableStack &) std::optional<ast::Term> visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, RuleContext &, Context &, const ast::VariableStack &)
{ {
throw TranslationException(term.location, "“pool” terms currently unsupported"); throw TranslationException(term.location, "“pool” terms currently unsupported");
return std::nullopt; return std::nullopt;
@ -171,9 +174,9 @@ struct TermTranslateVisitor
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack) ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
{ {
auto translatedTerm = term.data.accept(TermTranslateVisitor(), term, ruleContext, variableStack); auto translatedTerm = term.data.accept(TermTranslateVisitor(), term, ruleContext, context, variableStack);
if (!translatedTerm) if (!translatedTerm)
throw TranslationException(term.location, "could not translate term"); throw TranslationException(term.location, "could not translate term");

View File

@ -169,7 +169,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Comparison
inline output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext, bool) inline output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext, bool)
{ {
stream << function.name; stream << function.declaration->name;
if (function.arguments.empty()) if (function.arguments.empty())
return stream; return stream;
@ -184,7 +184,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Function &f
print(stream, *i, printContext); print(stream, *i, printContext);
} }
if (function.name.empty() && function.arguments.size() == 1) if (function.declaration->name.empty() && function.arguments.size() == 1)
stream << ","; stream << ",";
stream << ")"; stream << ")";

View File

@ -105,7 +105,7 @@ Comparison prepareCopy(const Comparison &other)
Function prepareCopy(const Function &other) Function prepareCopy(const Function &other)
{ {
return Function(std::string(other.name), prepareCopy(other.arguments)); return Function(other.declaration, prepareCopy(other.arguments));
} }
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////