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

Refactor predicate representation

Browse Source 
This refactoring separates predicates from their declarations. The
purpose of this is to avoid duplicating properties specific to the
predicate declaration and not its occurrences in the program.
This commit is contained in:
Patrick Lühne
2018-04-13 20:40:40 +02:00
parent 87dcd6ee93
commit 2372eb24c4
15 changed files with 187 additions and 242 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
src/anthem/ASTCopy.cpp
View File

@@ -140,7 +140,7 @@ Interval prepareCopy(const Interval &other)
Predicate prepareCopy(const Predicate &other)
{
return Predicate(std::string(other.name), prepareCopy(other.arguments));
return Predicate(other.declaration, prepareCopy(other.arguments));
}
////////////////////////////////////////////////////////////////////////////////////////////////////

79
src/anthem/ASTUtils.cpp
View File

@@ -197,84 +197,5 @@ struct CollectFreeVariablesVisitor
////////////////////////////////////////////////////////////////////////////////////////////////////
struct CollectPredicateSignaturesVisitor : public RecursiveFormulaVisitor<CollectPredicateSignaturesVisitor>
{
static void accept(const Predicate &predicate, const Formula &, std::vector<PredicateSignature> &predicateSignatures, Context &context)
{
const auto predicateSignatureMatches =
[&predicate](const auto &predicateSignature)
{
return matches(predicate, predicateSignature);
};
if (std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), predicateSignatureMatches) != predicateSignatures.cend())
return;
// TODO: avoid copies
auto predicateSignature = PredicateSignature(std::string(predicate.name), predicate.arity());
// Ignore predicates that are declared #external
if (context.externalPredicateSignatures)
{
const auto matchesPredicateSignature =
[&](const auto &otherPredicateSignature)
{
return ast::matches(predicateSignature, otherPredicateSignature.predicateSignature);
};
auto &externalPredicateSignatures = context.externalPredicateSignatures.value();
const auto matchingExternalPredicateSignature =
std::find_if(externalPredicateSignatures.begin(), externalPredicateSignatures.end(), matchesPredicateSignature);
if (matchingExternalPredicateSignature != externalPredicateSignatures.end())
{
matchingExternalPredicateSignature->used = true;
return;
}
}
predicateSignatures.emplace_back(std::move(predicateSignature));
}
// Ignore all other types of expressions
template<class T>
static void accept(const T &, const Formula &, std::vector<PredicateSignature> &, const Context &)
{
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
bool matches(const Predicate &lhs, const Predicate &rhs)
{
return (lhs.name == rhs.name && lhs.arity() == rhs.arity());
}
////////////////////////////////////////////////////////////////////////////////////////////////////
bool matches(const Predicate &predicate, const PredicateSignature &signature)
{
return (predicate.name == signature.name && predicate.arity() == signature.arity);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
bool matches(const PredicateSignature &lhs, const PredicateSignature &rhs)
{
return (lhs.name == rhs.name && lhs.arity == rhs.arity);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
// TODO: remove const_cast
void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures, Context &context)
{
auto &formulaMutable = const_cast<Formula &>(formula);
formulaMutable.accept(CollectPredicateSignaturesVisitor(), formulaMutable, predicateSignatures, context);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
}
}

35
src/anthem/Completion.cpp
View File

@@ -35,7 +35,7 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c
auto &otherPredicate = implies.consequent.get<ast::Predicate>();
if (!ast::matches(predicate, otherPredicate))
if (predicate.declaration != otherPredicate.declaration)
continue;
assert(otherPredicate.arguments.size() == parameters.size());
@@ -100,22 +100,22 @@ ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Fo
////////////////////////////////////////////////////////////////////////////////////////////////////
ast::Formula completePredicate(const ast::PredicateSignature &predicateSignature, std::vector<ast::ScopedFormula> &scopedFormulas)
ast::Formula completePredicate(ast::PredicateDeclaration &predicateDeclaration, std::vector<ast::ScopedFormula> &scopedFormulas)
{
// Create new set of parameters for the completed definition for the predicate
ast::VariableDeclarationPointers parameters;
parameters.reserve(predicateSignature.arity);
parameters.reserve(predicateDeclaration.arity);
std::vector<ast::Term> arguments;
arguments.reserve(predicateSignature.arity);
arguments.reserve(predicateDeclaration.arity);
for (size_t i = 0; i < predicateSignature.arity; i++)
for (size_t i = 0; i < predicateDeclaration.arity; i++)
{
parameters.emplace_back(std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::Head));
arguments.emplace_back(ast::Term::make<ast::Variable>(parameters.back().get()));
}
ast::Predicate predicateCopy(std::string(predicateSignature.name), std::move(arguments));
ast::Predicate predicateCopy(&predicateDeclaration, std::move(arguments));
auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicateCopy, parameters, scopedFormulas);
auto completedFormulaQuantified = buildCompletedFormulaQuantified(std::move(predicateCopy), std::move(completedFormulaDisjunction));
@@ -161,28 +161,27 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
throw CompletionException("cannot perform completion, only single predicates and Booleans supported as formula consequent currently");
}
std::vector<ast::PredicateSignature> predicateSignatures;
// Get a list of all predicates
for (const auto &scopedFormula : scopedFormulas)
ast::collectPredicateSignatures(scopedFormula.formula, predicateSignatures, context);
std::sort(predicateSignatures.begin(), predicateSignatures.end(),
std::sort(context.predicateDeclarations.begin(), context.predicateDeclarations.end(),
[](const auto &lhs, const auto &rhs)
{
const auto order = std::strcmp(lhs.name.c_str(), rhs.name.c_str());
const auto order = std::strcmp(lhs->name.c_str(), rhs->name.c_str());
if (order != 0)
return (order < 0);
return lhs.arity < rhs.arity;
return lhs->arity < rhs->arity;
});
std::vector<ast::Formula> completedFormulas;
// Complete predicates
for (const auto &predicateSignature : predicateSignatures)
completedFormulas.emplace_back(completePredicate(predicateSignature, scopedFormulas));
for (auto &predicateDeclaration : context.predicateDeclarations)
{
if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal)
continue;
completedFormulas.emplace_back(completePredicate(*predicateDeclaration, scopedFormulas));
}
// Complete integrity constraints
for (auto &scopedFormula : scopedFormulas)
@@ -202,7 +201,7 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
}
// Eliminate all predicates that should not be visible in the output
eliminateHiddenPredicates(predicateSignatures, completedFormulas, context);
eliminateHiddenPredicates(completedFormulas, context);
return completedFormulas;
}

90
src/anthem/HiddenPredicateElimination.cpp
View File

@@ -78,7 +78,7 @@ struct ReplacePredicateInFormulaVisitor : public ast::RecursiveFormulaVisitor<Re
{
static void accept(ast::Predicate &predicate, ast::Formula &formula, const PredicateReplacement &predicateReplacement)
{
if (!ast::matches(predicate, predicateReplacement.predicate))
if (predicate.declaration != predicateReplacement.predicate.declaration)
return;
auto formulaReplacement = ast::prepareCopy(predicateReplacement.replacement);
@@ -109,15 +109,15 @@ struct ReplacePredicateInFormulaVisitor : public ast::RecursiveFormulaVisitor<Re
// Detect whether a formula contains a circular dependency on a given predicate
struct DetectCircularDependcyVisitor : public ast::RecursiveFormulaVisitor<DetectCircularDependcyVisitor>
{
static void accept(ast::Predicate &predicate, ast::Formula &, const ast::PredicateSignature &predicateSignature, bool &hasCircularDependency)
static void accept(ast::Predicate &predicate, ast::Formula &, const ast::PredicateDeclaration &predicateDeclaration, bool &hasCircularDependency)
{
if (ast::matches(predicate, predicateSignature))
if (predicate.declaration == &predicateDeclaration)
hasCircularDependency = true;
}
// Ignore all other types of expressions
template<class T>
static void accept(T &, ast::Formula &, const ast::PredicateSignature &, bool &)
static void accept(T &, ast::Formula &, const ast::PredicateDeclaration &, bool &)
{
}
};
@@ -125,12 +125,12 @@ struct DetectCircularDependcyVisitor : public ast::RecursiveFormulaVisitor<Detec
////////////////////////////////////////////////////////////////////////////////////////////////////
// Finds the replacement for predicates of the form “p(X1, ..., Xn) <-> q(X1, ..., Xn)”
PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Predicate &predicate)
PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Predicate &predicate)
{
// Declare variable used, only used in debug mode
(void)(predicateSignature);
(void)(predicateDeclaration);
assert(ast::matches(predicate, predicateSignature));
assert(predicate.declaration == &predicateDeclaration);
// Replace with “#true”
return {predicate, ast::Formula::make<ast::Boolean>(true)};
@@ -139,13 +139,13 @@ PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSig
////////////////////////////////////////////////////////////////////////////////////////////////////
// Finds the replacement for predicates of the form “p(X1, ..., Xn) <-> not q(X1, ..., Xn)”
PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Not &not_)
PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Not &not_)
{
// Declare variable used, only used in debug mode
(void)(predicateSignature);
(void)(predicateDeclaration);
assert(not_.argument.is<ast::Predicate>());
assert(ast::matches(not_.argument.get<ast::Predicate>(), predicateSignature));
assert(not_.argument.get<ast::Predicate>().declaration == &predicateDeclaration);
// Replace with “#false”
return {not_.argument.get<ast::Predicate>(), ast::Formula::make<ast::Boolean>(false)};
@@ -154,13 +154,13 @@ PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSig
////////////////////////////////////////////////////////////////////////////////////////////////////
// Finds the replacement for predicates of the form “forall X1, ..., Xn (p(X1, ..., Xn) <-> ...)”
PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Biconditional &biconditional)
PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Biconditional &biconditional)
{
// Declare variable used, only used in debug mode
(void)(predicateSignature);
(void)(predicateDeclaration);
assert(biconditional.left.is<ast::Predicate>());
assert(ast::matches(biconditional.left.get<ast::Predicate>(), predicateSignature));
assert(biconditional.left.get<ast::Predicate>().declaration == &predicateDeclaration);
// TODO: avoid copy
return {biconditional.left.get<ast::Predicate>(), ast::prepareCopy(biconditional.right)};
@@ -169,77 +169,65 @@ PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSig
////////////////////////////////////////////////////////////////////////////////////////////////////
// Finds a replacement for a predicate that should be hidden
PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Formula &completedPredicateDefinition)
PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Formula &completedPredicateDefinition)
{
// TODO: refactor
if (completedPredicateDefinition.is<ast::ForAll>())
return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::ForAll>().argument);
return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::ForAll>().argument);
else if (completedPredicateDefinition.is<ast::Biconditional>())
return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::Biconditional>());
return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::Biconditional>());
else if (completedPredicateDefinition.is<ast::Predicate>())
return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::Predicate>());
return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::Predicate>());
else if (completedPredicateDefinition.is<ast::Not>())
return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::Not>());
return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::Not>());
throw CompletionException("unsupported completed definition for predicate “" + predicateSignature.name + "/" + std::to_string(predicateSignature.arity) + "” for hiding predicates");
throw CompletionException("unsupported completed definition for predicate “" + predicateDeclaration.name + "/" + std::to_string(predicateDeclaration.arity) + "” for hiding predicates");
}
////////////////////////////////////////////////////////////////////////////////////////////////////
void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predicateSignatures, std::vector<ast::Formula> &completedFormulas, Context &context)
void eliminateHiddenPredicates(std::vector<ast::Formula> &completedFormulas, Context &context)
{
if (!context.visiblePredicateSignatures)
if (context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Visible)
{
context.logger.log(output::Priority::Debug) << "no predicates to be eliminated";
return;
}
auto &visiblePredicateSignatures = context.visiblePredicateSignatures.value();
assert(context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Hidden);
// TODO: get rid of index-wise matching of completed formulas and predicate declarations
size_t i = -1;
// Replace all occurrences of hidden predicates
for (size_t i = 0; i < predicateSignatures.size(); i++)
for (auto &predicateDeclaration : context.predicateDeclarations)
{
auto &predicateSignature = predicateSignatures[i];
// Check that the predicate is used and not declared #external
if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal)
continue;
const auto matchesPredicateSignature =
[&](const auto &otherPredicateSignature)
{
return ast::matches(predicateSignature, otherPredicateSignature.predicateSignature);
};
i++;
const auto matchingVisiblePredicateSignature =
std::find_if(visiblePredicateSignatures.begin(), visiblePredicateSignatures.end(), matchesPredicateSignature);
const auto isPredicateVisible =
(predicateDeclaration->visibility == ast::PredicateDeclaration::Visibility::Visible)
|| (predicateDeclaration->visibility == ast::PredicateDeclaration::Visibility::Default
&& context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Visible);
// If the predicate ought to be visible, don’t eliminate it
if (matchingVisiblePredicateSignature != visiblePredicateSignatures.end())
{
matchingVisiblePredicateSignature->used = true;
if (isPredicateVisible)
continue;
}
// Check that the predicate is not declared #external
if (context.externalPredicateSignatures)
{
const auto &externalPredicateSignatures = context.externalPredicateSignatures.value();
const auto matchingExternalPredicateSignature =
std::find_if(externalPredicateSignatures.cbegin(), externalPredicateSignatures.cend(), matchesPredicateSignature);
if (matchingExternalPredicateSignature != externalPredicateSignatures.cend())
continue;
}
context.logger.log(output::Priority::Debug) << "eliminating “" << predicateSignature.name << "/" << predicateSignature.arity << "”";
context.logger.log(output::Priority::Debug) << "eliminating “" << predicateDeclaration->name << "/" << predicateDeclaration->arity << "”";
const auto &completedPredicateDefinition = completedFormulas[i];
auto replacement = findReplacement(predicateSignature, completedPredicateDefinition);
auto replacement = findReplacement(*predicateDeclaration, completedPredicateDefinition);
bool hasCircularDependency = false;
replacement.replacement.accept(DetectCircularDependcyVisitor(), replacement.replacement, predicateSignature, hasCircularDependency);
replacement.replacement.accept(DetectCircularDependcyVisitor(), replacement.replacement, *predicateDeclaration, hasCircularDependency);
if (hasCircularDependency)
{
context.logger.log(output::Priority::Warning) << "cannot hide predicate “" << predicateSignature.name << "/" << predicateSignature.arity << "” due to circular dependency";
context.logger.log(output::Priority::Warning) << "cannot hide predicate “" << predicateDeclaration->name << "/" << predicateDeclaration->arity << "” due to circular dependency";
continue;
}

44
src/anthem/Translation.cpp
View File

@@ -67,10 +67,10 @@ void translate(const char *fileName, std::istream &stream, Context &context)
for (auto &scopedFormula : scopedFormulas)
simplify(scopedFormula.formula);
if (context.visiblePredicateSignatures)
if (context.showStatementsUsed)
context.logger.log(output::Priority::Warning) << "#show statements are ignored because completion is not enabled";
if (context.externalPredicateSignatures)
if (context.externalStatementsUsed)
context.logger.log(output::Priority::Warning) << "#external statements are ignored because completion is not enabled";
for (const auto &scopedFormula : scopedFormulas)
@@ -85,25 +85,29 @@ void translate(const char *fileName, std::istream &stream, Context &context)
// Perform completion
auto completedFormulas = complete(std::move(scopedFormulas), context);
// Check for #show statements with undeclared predicates
if (context.visiblePredicateSignatures)
for (const auto &predicateSignature : context.visiblePredicateSignatures.value())
if (!predicateSignature.used)
context.logger.log(output::Priority::Warning)
<< "#show declaration of “"
<< predicateSignature.predicateSignature.name
<< "/" << predicateSignature.predicateSignature.arity
<< "” does not match any eligible predicate";
for (const auto &predicateDeclaration : context.predicateDeclarations)
{
if (predicateDeclaration->isUsed)
continue;
// Check for #external statements with undeclared predicates
if (context.externalPredicateSignatures)
for (const auto &predicateSignature : context.externalPredicateSignatures.value())
if (!predicateSignature.used)
context.logger.log(output::Priority::Warning)
<< "#external declaration of “"
<< predicateSignature.predicateSignature.name
<< "/" << predicateSignature.predicateSignature.arity
<< "” does not match any eligible predicate";
// Check for #show statements with undeclared predicates
if (predicateDeclaration->visibility != ast::PredicateDeclaration::Visibility::Default)
context.logger.log(output::Priority::Warning)
<< "#show declaration of “"
<< predicateDeclaration->name
<< "/"
<< predicateDeclaration->arity
<< "” does not match any declared predicate";
// Check for #external statements with undeclared predicates
if (predicateDeclaration->isExternal && !predicateDeclaration->isUsed)
context.logger.log(output::Priority::Warning)
<< "#external declaration of “"
<< predicateDeclaration->name
<< "/"
<< predicateDeclaration->arity
<< "” does not match any declared predicate";
}
// Simplify output if specified
if (context.performSimplification)