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

Implemented #show statements for completed output.

Browse Source
This commit is contained in:
Patrick Lühne 2017-06-05 02:50:30 +02:00
parent 4fd143ef64
commit 14abc37116
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
8 changed files with 346 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
include/anthem/AST.h
View File

@ -241,8 +241,10 @@ struct PredicateSignature
PredicateSignature(const PredicateSignature &other) = delete;
PredicateSignature &operator=(const PredicateSignature &other) = delete;
PredicateSignature(PredicateSignature &&other) noexcept = default;
PredicateSignature &operator=(PredicateSignature &&other) noexcept = default;
// TODO: make noexcept again
// GCC versions before 7 don’t declare moving std::string noexcept and would complain here
PredicateSignature(PredicateSignature &&other) = default;
PredicateSignature &operator=(PredicateSignature &&other) = default;
std::string name;
size_t arity;

4
include/anthem/ASTUtils.h
View File

@ -38,7 +38,9 @@ class VariableStack
////////////////////////////////////////////////////////////////////////////////////////////////////
bool matches(const Predicate &lhs, const Predicate &rhs);
void collectPredicates(const Formula &formula, std::vector<const Predicate *> &predicates);
bool matches(const Predicate &predicate, const PredicateSignature &signature);
bool matches(const PredicateSignature &lhs, const PredicateSignature &rhs);
void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures);
////////////////////////////////////////////////////////////////////////////////////////////////////
// Replacing Variables

3
include/anthem/Completion.h
View File

@ -2,6 +2,7 @@
#define __ANTHEM__COMPLETION_H
#include <anthem/AST.h>
#include <anthem/Context.h>
namespace anthem
{
@ -12,7 +13,7 @@ namespace anthem
//
////////////////////////////////////////////////////////////////////////////////////////////////////
std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormulas);
std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormulas, Context &context);
////////////////////////////////////////////////////////////////////////////////////////////////////

22
include/anthem/HiddenPredicateElimination.h Normal file
View File

@ -0,0 +1,22 @@
#ifndef __ANTHEM__HIDDEN_PREDICATE_ELIMINATION_H
#define __ANTHEM__HIDDEN_PREDICATE_ELIMINATION_H
#include <anthem/AST.h>
#include <anthem/Context.h>
namespace anthem
{
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// HiddenPredicateElimination
//
////////////////////////////////////////////////////////////////////////////////////////////////////
void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predicateSignatures, std::vector<ast::Formula> &completedFormulas, Context &context);
////////////////////////////////////////////////////////////////////////////////////////////////////
}
#endif

37
src/anthem/ASTUtils.cpp
View File

@ -192,23 +192,26 @@ struct CollectFreeVariablesVisitor
////////////////////////////////////////////////////////////////////////////////////////////////////
struct CollectPredicatesVisitor : public RecursiveFormulaVisitor<CollectPredicatesVisitor>
struct CollectPredicateSignaturesVisitor : public RecursiveFormulaVisitor<CollectPredicateSignaturesVisitor>
{
static void accept(const Predicate &predicate, const Formula &, std::vector<const Predicate *> &predicates)
static void accept(const Predicate &predicate, const Formula &, std::vector<PredicateSignature> &predicateSignatures)
{
const auto predicateMatches =
[&predicate](const auto *otherPredicate)
const auto predicateSignatureMatches =
[&predicate](const auto &predicateSignature)
{
return matches(predicate, *otherPredicate);
return matches(predicate, predicateSignature);
};
if (std::find_if(predicates.cbegin(), predicates.cend(), predicateMatches) == predicates.cend())
predicates.emplace_back(&predicate);
if (std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), predicateSignatureMatches) != predicateSignatures.cend())
return;
// TODO: avoid copies
predicateSignatures.emplace_back(std::string(predicate.name), predicate.arity());
}
// Ignore all other types of expressions
template<class T>
static void accept(const T &, const Formula &, std::vector<const Predicate *> &)
static void accept(const T &, const Formula &, std::vector<PredicateSignature> &)
{
}
};
@ -222,11 +225,25 @@ bool matches(const Predicate &lhs, const Predicate &rhs)
////////////////////////////////////////////////////////////////////////////////////////////////////
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 collectPredicates(const Formula &formula, std::vector<const Predicate *> &predicates)
void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures)
{
auto &formulaMutable = const_cast<Formula &>(formula);
formulaMutable.accept(CollectPredicatesVisitor(), formulaMutable, predicates);
formulaMutable.accept(CollectPredicateSignaturesVisitor(), formulaMutable, predicateSignatures);
}
////////////////////////////////////////////////////////////////////////////////////////////////////

34
src/anthem/Completion.cpp
View File

@ -5,6 +5,7 @@
#include <anthem/ASTUtils.h>
#include <anthem/ASTVisitors.h>
#include <anthem/Exception.h>
#include <anthem/HiddenPredicateElimination.h>
#include <anthem/Utils.h>
namespace anthem
@ -99,22 +100,22 @@ ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Fo
////////////////////////////////////////////////////////////////////////////////////////////////////
ast::Formula completePredicate(const ast::Predicate &predicate, std::vector<ast::ScopedFormula> &scopedFormulas)
ast::Formula completePredicate(const ast::PredicateSignature &predicateSignature, std::vector<ast::ScopedFormula> &scopedFormulas)
{
// Create new set of parameters for the completed definition for the predicate
ast::VariableDeclarationPointers parameters;
parameters.reserve(predicate.arguments.size());
parameters.reserve(predicateSignature.arity);
std::vector<ast::Term> arguments;
arguments.reserve(predicate.arguments.size());
arguments.reserve(predicateSignature.arity);
for (size_t i = 0; i < predicate.arguments.size(); i++)
for (size_t i = 0; i < predicateSignature.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(predicate.name), std::move(arguments));
ast::Predicate predicateCopy(std::string(predicateSignature.name), std::move(arguments));
auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicateCopy, parameters, scopedFormulas);
auto completedFormulaQuantified = buildCompletedFormulaQuantified(std::move(predicateCopy), std::move(completedFormulaDisjunction));
@ -146,7 +147,7 @@ ast::Formula completeIntegrityConstraint(ast::ScopedFormula &scopedFormula)
////////////////////////////////////////////////////////////////////////////////////////////////////
std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormulas)
std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormulas, Context &context)
{
// Check whether formulas are in normal form
for (const auto &scopedFormula : scopedFormulas)
@ -160,28 +161,28 @@ 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<const ast::Predicate *> predicates;
std::vector<ast::PredicateSignature> predicateSignatures;
// Get a list of all predicates
for (const auto &scopedFormula : scopedFormulas)
ast::collectPredicates(scopedFormula.formula, predicates);
ast::collectPredicateSignatures(scopedFormula.formula, predicateSignatures);
std::sort(predicates.begin(), predicates.end(),
[](const auto *lhs, const auto *rhs)
std::sort(predicateSignatures.begin(), predicateSignatures.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 (order < 0);
return lhs->arity() < rhs->arity();
return lhs.arity < rhs.arity;
});
std::vector<ast::Formula> completedFormulas;
// Complete predicates
for (const auto *predicate : predicates)
completedFormulas.emplace_back(completePredicate(*predicate, scopedFormulas));
for (const auto &predicateSignature : predicateSignatures)
completedFormulas.emplace_back(completePredicate(predicateSignature, scopedFormulas));
// Complete integrity constraints
for (auto &scopedFormula : scopedFormulas)
@ -200,6 +201,9 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
completedFormulas.emplace_back(completeIntegrityConstraint(scopedFormula));
}
// Eliminate all predicates that should not be visible in the output
eliminateHiddenPredicates(predicateSignatures, completedFormulas, context);
return completedFormulas;
}

268
src/anthem/HiddenPredicateElimination.cpp Normal file
View File

@ -0,0 +1,268 @@
#include <anthem/HiddenPredicateElimination.h>
#include <anthem/ASTCopy.h>
#include <anthem/ASTUtils.h>
#include <anthem/ASTVisitors.h>
#include <anthem/Exception.h>
#include <anthem/Simplification.h>
#include <anthem/output/AST.h>
namespace anthem
{
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// HiddenPredicateElimination
//
////////////////////////////////////////////////////////////////////////////////////////////////////
struct PredicateReplacement
{
const ast::Predicate &predicate;
ast::Formula replacement;
};
////////////////////////////////////////////////////////////////////////////////////////////////////
// Replaces all occurrences of a variable in a given term with another variable
struct ReplaceVariableInTermVisitor : public ast::RecursiveTermVisitor<ReplaceVariableInTermVisitor>
{
static void accept(ast::Variable &variable, ast::Term &, const ast::VariableDeclaration &original, ast::VariableDeclaration &replacement)
{
if (variable.declaration == &original)
// No dangling variables can result from this operation, and hence, fixing them is not necessary
variable.declaration = &replacement;
}
// Ignore all other types of expressions
template<class T>
static void accept(T &, ast::Term &, const ast::VariableDeclaration &, ast::VariableDeclaration &)
{
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
// Replaces all occurrences of a variable in a given formula with another variable
struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<ReplaceVariableInFormulaVisitor>
{
static void accept(ast::Comparison &comparison, ast::Formula &, const ast::VariableDeclaration &original, ast::VariableDeclaration &replacement)
{
comparison.left.accept(ReplaceVariableInTermVisitor(), comparison.left, original, replacement);
comparison.right.accept(ReplaceVariableInTermVisitor(), comparison.right, original, replacement);
}
static void accept(ast::In &in, ast::Formula &, const ast::VariableDeclaration &original, ast::VariableDeclaration &replacement)
{
in.element.accept(ReplaceVariableInTermVisitor(), in.element, original, replacement);
in.set.accept(ReplaceVariableInTermVisitor(), in.set, original, replacement);
}
static void accept(ast::Predicate &predicate, ast::Formula &, const ast::VariableDeclaration &original, ast::VariableDeclaration &replacement)
{
for (auto &argument : predicate.arguments)
argument.accept(ReplaceVariableInTermVisitor(), argument, original, replacement);
}
// Ignore all other types of expressions
template<class T>
static void accept(T &, ast::Formula &, const ast::VariableDeclaration &, ast::VariableDeclaration &)
{
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
// Replace a predicate in a term with a formula
struct ReplacePredicateInFormulaVisitor : public ast::RecursiveFormulaVisitor<ReplacePredicateInFormulaVisitor>
{
static void accept(ast::Predicate &predicate, ast::Formula &formula, const PredicateReplacement &predicateReplacement)
{
if (!ast::matches(predicate, predicateReplacement.predicate))
return;
auto formulaReplacement = ast::prepareCopy(predicateReplacement.replacement);
for (size_t i = 0; i < predicate.arguments.size(); i++)
{
assert(predicateReplacement.predicate.arguments[i].is<ast::Variable>());
const auto &original = *predicateReplacement.predicate.arguments[i].get<ast::Variable>().declaration;
assert(predicate.arguments[i].is<ast::Variable>());
auto &replacement = *predicate.arguments[i].get<ast::Variable>().declaration;
formulaReplacement.accept(ReplaceVariableInFormulaVisitor(), formulaReplacement, original, replacement);
}
formula = std::move(formulaReplacement);
}
// Ignore all other types of expressions
template<class T>
static void accept(T &, ast::Formula &, const PredicateReplacement &)
{
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
// 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)
{
if (ast::matches(predicate, predicateSignature))
hasCircularDependency = true;
}
// Ignore all other types of expressions
template<class T>
static void accept(T &, ast::Formula &, const ast::PredicateSignature &, bool &)
{
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
// Finds the replacement for predicates of the form “forall X1, ..., Xn (p(X1, ..., Xn) <-> ...)”
PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::ForAll &forAll)
{
// Declare variable used, only used in debug mode
(void)(predicateSignature);
// Form: “forall X1, ..., Xn p(X1, ..., Xn)”
// Replace with “#true”
if (forAll.argument.is<ast::Predicate>())
{
assert(ast::matches(forAll.argument.get<ast::Predicate>(), predicateSignature));
return {forAll.argument.get<ast::Predicate>(), ast::Formula::make<ast::Boolean>(true)};
}
// Form: “forall X1, ..., Xn (p(X1, ..., Xn) <-> ...)”
// Replace with “#false”
if (forAll.argument.is<ast::Not>())
{
auto &notArgument = forAll.argument.get<ast::Not>().argument;
assert(notArgument.is<ast::Predicate>());
assert(ast::matches(notArgument.get<ast::Predicate>(), predicateSignature));
return {notArgument.get<ast::Predicate>(), ast::Formula::make<ast::Boolean>(false)};
}
assert(forAll.argument.is<ast::Biconditional>());
const auto &biconditional = forAll.argument.get<ast::Biconditional>();
assert(biconditional.left.is<ast::Predicate>());
assert(ast::matches(biconditional.left.get<ast::Predicate>(), predicateSignature));
// TODO: avoid copy
return {biconditional.left.get<ast::Predicate>(), ast::prepareCopy(biconditional.right)};
}
////////////////////////////////////////////////////////////////////////////////////////////////////
// Finds a replacement for a predicate that should be hidden
PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Formula &completedPredicateDefinition)
{
if (completedPredicateDefinition.is<ast::ForAll>())
return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::ForAll>());
else if (completedPredicateDefinition.is<ast::Predicate>())
return {completedPredicateDefinition.get<ast::Predicate>(), ast::Formula::make<ast::Boolean>(true)};
else if (completedPredicateDefinition.is<ast::Not>())
{
const auto &notArgument = completedPredicateDefinition.get<ast::Not>().argument;
assert(notArgument.is<ast::Predicate>());
return {notArgument.get<ast::Predicate>(), ast::Formula::make<ast::Boolean>(false)};
}
throw CompletionException("invalid completed predicate definition for predicate “" + predicateSignature.name + "/" + std::to_string(predicateSignature.arity) + "”");
}
////////////////////////////////////////////////////////////////////////////////////////////////////
void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predicateSignatures, std::vector<ast::Formula> &completedFormulas, Context &context)
{
if (!context.visiblePredicateSignatures)
{
context.logger.log(output::Priority::Debug) << "no predicates to be eliminated";
return;
}
const auto &visiblePredicateSignatures = context.visiblePredicateSignatures.value();
// Check for undeclared predicates that are requested to be shown
for (const auto &visiblePredicateSignature : visiblePredicateSignatures)
{
const auto matchesPredicateSignature =
[&](const auto &predicateSignature)
{
return ast::matches(predicateSignature, visiblePredicateSignature);
};
const auto matchingPredicateSignature =
std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), matchesPredicateSignature);
if (matchingPredicateSignature == predicateSignatures.cend())
context.logger.log(output::Priority::Warning) << "cannot show undeclared predicate “" << visiblePredicateSignature.name << "/" << visiblePredicateSignature.arity <<"”";
}
// Replace all occurrences of hidden predicates
for (size_t i = 0; i < predicateSignatures.size(); i++)
{
auto &predicateSignature = predicateSignatures[i];
const auto matchesVisiblePredicateSignature =
[&](const auto &visiblePredicateSignature)
{
return ast::matches(predicateSignature, visiblePredicateSignature);
};
const auto matchingPredicateSignature =
std::find_if(visiblePredicateSignatures.cbegin(), visiblePredicateSignatures.cend(), matchesVisiblePredicateSignature);
// If the predicate ought to be visible, don’t eliminate it
if (matchingPredicateSignature != visiblePredicateSignatures.cend())
continue;
context.logger.log(output::Priority::Debug) << "eliminating “" << predicateSignature.name << "/" << predicateSignature.arity << "”";
const auto &completedPredicateDefinition = completedFormulas[i];
auto replacement = findReplacement(predicateSignature, completedPredicateDefinition);
bool hasCircularDependency = false;
replacement.replacement.accept(DetectCircularDependcyVisitor(), replacement.replacement, predicateSignature, hasCircularDependency);
if (hasCircularDependency)
{
context.logger.log(output::Priority::Warning) << "cannot hide predicate “" << predicateSignature.name << "/" << predicateSignature.arity << "” due to circular dependency";
continue;
}
for (size_t j = 0; j < completedFormulas.size(); j++)
if (j != i)
completedFormulas[j].accept(ReplacePredicateInFormulaVisitor(), completedFormulas[j], replacement);
// TODO: refactor
completedFormulas[i] = ast::Formula::make<ast::Boolean>(true);
}
const auto canBeRemoved =
[&](const ast::Formula &completedFormula)
{
if (!completedFormula.is<ast::Boolean>())
return false;
return completedFormula.get<ast::Boolean>().value == true;
};
auto removedFormulas = std::remove_if(completedFormulas.begin(), completedFormulas.end(), canBeRemoved);
completedFormulas.erase(removedFormulas, completedFormulas.end());
}
////////////////////////////////////////////////////////////////////////////////////////////////////
}

2
src/anthem/Translation.cpp
View File

@ -77,7 +77,7 @@ void translate(const char *fileName, std::istream &stream, Context &context)
return;
}
auto completedFormulas = complete(std::move(scopedFormulas));
auto completedFormulas = complete(std::move(scopedFormulas), context);
// TODO: rethink simplification steps
if (context.simplify)