Compare commits

..

No commits in common. "develop" and "v0.1.8" have entirely different histories.

42 changed files with 539 additions and 1690 deletions

View File

@ -1,25 +1,5 @@
# Change Log
## (unreleased)
## 0.1.9 (2018-05-04)
### Changes
* turns on completion and simplification by default, which can now be switched off with `--no-complete` and `--no-simplify`
### Features
* detection of integer variables and integer predicate parameters
* command-line option `--no-detect-integers` to disable integer variable detection
* new simplification rule applying to integer variables
* support for declaring functions integer with the `#external` directive
### Bug Fixes
* fixes incorrect translation of unsupported choice rules with multiple elements by returning an error instead
* fixes precedence of intervals by enclosing them in parentheses
## 0.1.8 (2018-04-20)
### Features

View File

@ -9,12 +9,11 @@
## Usage
```bash
$ anthem [--no-complete] [--no-simplify] [--no-detect-integers] file...
$ anthem [--complete] [--simplify] file...
```
By default, `anthem` performs Clarks completion on the translated formulas, detects which variables are integer, and simplifies the output by applying several basic transformation rules.
These processing steps can be turned off with the options `--no-complete`, `--no-simplify`, and `--no-detect-integers`.
`--complete` instructs `anthem` to perform Clarks completion on the translated formulas.
With the option `--simplify`, the output formulas are simplified by applying several basic transformation rules.
## Building

View File

@ -16,9 +16,8 @@ int main(int argc, char **argv)
("h,help", "Display this help message")
("v,version", "Display version information")
("i,input", "Input files", cxxopts::value<std::vector<std::string>>())
("no-simplify", "Do not simplify the output")
("no-complete", "Do not perform completion")
("no-detect-integers", "Do not detect integer variables")
("s,simplify", "Simplify the output")
("c,complete", "Perform completion")
("color", "Colorize output (always, never, auto)", cxxopts::value<std::string>()->default_value("auto"))
("parentheses", "Parenthesis style (normal, full)", cxxopts::value<std::string>()->default_value("normal"))
("p,log-priority", "Log messages starting from this priority (debug, info, warning, error)", cxxopts::value<std::string>()->default_value("info"));
@ -49,9 +48,8 @@ int main(int argc, char **argv)
if (parseResult.count("input") > 0)
inputFiles = parseResult["input"].as<std::vector<std::string>>();
context.performSimplification = (parseResult.count("no-simplify") == 0);
context.performCompletion = (parseResult.count("no-complete") == 0);
context.performIntegerDetection = (parseResult.count("no-detect-integers") == 0);
context.performSimplification = (parseResult.count("simplify") > 0);
context.performCompletion = (parseResult.count("complete") > 0);
colorPolicyString = parseResult["color"].as<std::string>();
parenthesisStyleString = parseResult["parentheses"].as<std::string>();
logPriorityString = parseResult["log-priority"].as<std::string>();
@ -72,7 +70,7 @@ int main(int argc, char **argv)
if (version)
{
std::cout << "anthem version 0.1.9+git" << std::endl;
std::cout << "anthem version 0.1.8" << std::endl;
return EXIT_SUCCESS;
}

View File

@ -1,2 +0,0 @@
p(a).
{q(a)}.

View File

@ -1,18 +1,10 @@
% assign a set of colors to each vertex
{color(V, C)} :- vertex(V), color(C).
% at most one color per vertex
:- color(V, C1), color(V, C2), C1 != C2.
% at least one color per vertex
covered(V) :- color(V, _).
:- vertex(V), not covered(V).
% adjacent vertices dont share the same color
:- color(V1, C), color(V2, C), edge(V1, V2).
#external color(1).
#external edge(2).
#external vertex(1).
#show color/2.
#external vertex(1).
#external edge(2).
#external color(1).
{color(V, C)} :- vertex(V), color(C).
covered(V) :- color(V, _).
:- vertex(V), not covered(V).
:- color(V1, C), color(V2, C), edge(V1, V2).
:- color(V, C1), color(V, C2), C1 != C2.

View File

@ -1,11 +0,0 @@
letter(a).
letter(b).
letter(c).
{p(1..3, Y)} :- letter(Y).
:- p(X1, Y), p(X2, Y), X1 != X2.
q(X) :- p(X, _).
:- X = 1..3, not q(X).
#show p/2.

View File

@ -1,5 +1,3 @@
#show p/2.
{p(1..n, 1..n)}.
:- p(X, Y1), p(X, Y2), Y1 != Y2.
@ -10,3 +8,5 @@ q2(Y) :- p(_, Y).
:- not q1(X), X = 1..n.
:- not q2(Y), Y = 1..n.
#show p/2.

View File

@ -1,7 +1,7 @@
#show in/2.
{in(1..n, 1..r)}.
covered(I) :- in(I, S).
:- I = 1..n, not covered(I).
:- in(I, S), in(J, S), in(I + J, S).
#show in/2.

View File

@ -1,9 +0,0 @@
s(X) :- p(X).
s(X) :- q(X).
u(X) :- r(X), not s(X).
#show u/1.
#external p(1).
#external q(1).
#external r(1).

View File

@ -1,5 +0,0 @@
s(X) :- p(X).
s(X) :- q(X).
#external p(1).
#external q(1).

View File

@ -2,7 +2,6 @@
#define __ANTHEM__AST_H
#include <anthem/ASTForward.h>
#include <anthem/Utils.h>
namespace anthem
{
@ -104,15 +103,32 @@ struct Comparison
////////////////////////////////////////////////////////////////////////////////////////////////////
struct Function
struct Constant
{
explicit Function(FunctionDeclaration *declaration)
: declaration{declaration}
explicit Constant(std::string &&name)
: name{std::move(name)}
{
}
explicit Function(FunctionDeclaration *declaration, std::vector<Term> &&arguments)
: declaration{declaration},
Constant(const Constant &other) = delete;
Constant &operator=(const Constant &other) = delete;
Constant(Constant &&other) = default;
Constant &operator=(Constant &&other) = default;
std::string name;
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct Function
{
explicit Function(std::string &&name)
: name{std::move(name)}
{
}
explicit Function(std::string &&name, std::vector<Term> &&arguments)
: name{std::move(name)},
arguments{std::move(arguments)}
{
}
@ -122,33 +138,8 @@ struct Function
Function(Function &&other) noexcept = default;
Function &operator=(Function &&other) noexcept = default;
FunctionDeclaration *declaration;
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;
Domain domain{Domain::Noninteger};
std::vector<Term> arguments;
};
////////////////////////////////////////////////////////////////////////////////////////////////////
@ -213,13 +204,13 @@ struct Interval
struct Predicate
{
explicit Predicate(PredicateDeclaration *declaration)
: declaration{declaration}
explicit Predicate(std::string &&name)
: name{std::move(name)}
{
}
explicit Predicate(PredicateDeclaration *declaration, std::vector<Term> &&arguments)
: declaration{declaration},
explicit Predicate(std::string &&name, std::vector<Term> &&arguments)
: name{std::move(name)},
arguments{std::move(arguments)}
{
}
@ -229,47 +220,35 @@ struct Predicate
Predicate(Predicate &&other) noexcept = default;
Predicate &operator=(Predicate &&other) noexcept = default;
PredicateDeclaration *declaration{nullptr};
std::size_t arity() const
{
return arguments.size();
}
std::string name;
std::vector<Term> arguments;
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct PredicateDeclaration
// TODO: make more use of this class
struct PredicateSignature
{
enum class Visibility
{
Default,
Visible,
Hidden
};
struct Parameter
{
Domain domain{Domain::Unknown};
};
explicit PredicateDeclaration(std::string &&name, size_t arity)
explicit PredicateSignature(std::string &&name, size_t arity)
: name{std::move(name)},
parameters{std::vector<Parameter>(arity)}
arity{arity}
{
}
PredicateDeclaration(const PredicateDeclaration &other) = delete;
PredicateDeclaration &operator=(const PredicateDeclaration &other) = delete;
PredicateDeclaration(PredicateDeclaration &&other) noexcept = default;
PredicateDeclaration &operator=(PredicateDeclaration &&other) noexcept = default;
size_t arity() const noexcept
{
return parameters.size();
}
PredicateSignature(const PredicateSignature &other) = delete;
PredicateSignature &operator=(const PredicateSignature &other) = delete;
// TODO: make noexcept again
// GCC versions before 7 dont declare moving std::string noexcept and would complain here
PredicateSignature(PredicateSignature &&other) = default;
PredicateSignature &operator=(PredicateSignature &&other) = default;
std::string name;
std::vector<Parameter> parameters;
bool isUsed{false};
bool isExternal{false};
Visibility visibility{Visibility::Default};
size_t arity;
};
////////////////////////////////////////////////////////////////////////////////////////////////////
@ -381,7 +360,6 @@ struct VariableDeclaration
VariableDeclaration &operator=(VariableDeclaration &&other) = default;
Type type;
Domain domain{Domain::Unknown};
std::string name;
};

View File

@ -22,6 +22,7 @@ namespace ast
BinaryOperation prepareCopy(const BinaryOperation &other);
Boolean prepareCopy(const Boolean &other);
Comparison prepareCopy(const Comparison &other);
Constant prepareCopy(const Constant &other);
Function prepareCopy(const Function &other);
In prepareCopy(const In &other);
Integer prepareCopy(const Integer &other);

View File

@ -24,10 +24,10 @@ struct BinaryOperation;
struct Biconditional;
struct Boolean;
struct Comparison;
struct Constant;
struct Exists;
struct ForAll;
struct Function;
struct FunctionDeclaration;
struct Implies;
struct In;
struct Integer;
@ -35,7 +35,6 @@ struct Interval;
struct Not;
struct Or;
struct Predicate;
struct PredicateDeclaration;
struct SpecialInteger;
struct String;
struct UnaryOperation;
@ -64,6 +63,7 @@ using Formula = Clingo::Variant<
using Term = Clingo::Variant<
BinaryOperation,
Boolean,
Constant,
Function,
Integer,
Interval,

View File

@ -36,6 +36,12 @@ class VariableStack
std::vector<Layer> m_layers;
};
////////////////////////////////////////////////////////////////////////////////////////////////////
bool matches(const Predicate &lhs, const Predicate &rhs);
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, Context &context);
////////////////////////////////////////////////////////////////////////////////////////////////////
// Replacing Variables
@ -90,21 +96,6 @@ struct ReplaceVariableInFormulaVisitor : public RecursiveFormulaVisitor<ReplaceV
////////////////////////////////////////////////////////////////////////////////////////////////////
}
////////////////////////////////////////////////////////////////////////////////////////////////////
// Accessing Variable Domains
////////////////////////////////////////////////////////////////////////////////////////////////////
struct DefaultVariableDomainAccessor
{
Domain operator()(const ast::Variable &variable)
{
return variable.declaration->domain;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
}
#endif

View File

@ -123,6 +123,12 @@ struct RecursiveTermVisitor
return T::accept(boolean, term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
ReturnType visit(Constant &constant, Term &term, Arguments &&... arguments)
{
return T::accept(constant, term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
ReturnType visit(Function &function, Term &term, Arguments &&... arguments)
{

View File

@ -43,22 +43,19 @@ ast::Comparison::Operator translate(Clingo::AST::ComparisonOperator comparisonOp
struct BodyTermTranslateVisitor
{
// TODO: refactor
std::optional<ast::Formula> visit(const Clingo::AST::Function &function,
const Clingo::AST::Literal &literal, const Clingo::AST::Term &, RuleContext &ruleContext,
Context &context, ast::VariableStack &variableStack)
std::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Literal &literal, const Clingo::AST::Term &, RuleContext &ruleContext, ast::VariableStack &variableStack)
{
if (literal.sign == Clingo::AST::Sign::DoubleNegation)
throw TranslationException(literal.location, "double-negated literals currently unsupported");
auto predicateDeclaration = context.findOrCreatePredicateDeclaration(function.name, function.arguments.size());
predicateDeclaration->isUsed = true;
if (function.arguments.empty())
{
auto predicate = ast::Formula::make<ast::Predicate>(std::string(function.name));
if (literal.sign == Clingo::AST::Sign::None)
return ast::Predicate(predicateDeclaration);
return std::move(predicate);
else if (literal.sign == Clingo::AST::Sign::Negation)
return ast::Formula::make<ast::Not>(ast::Predicate(predicateDeclaration));
return ast::Formula::make<ast::Not>(std::move(predicate));
}
// Create new body variable declarations
@ -76,12 +73,12 @@ struct BodyTermTranslateVisitor
for (size_t i = 0; i < function.arguments.size(); i++)
{
auto &argument = function.arguments[i];
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[i].get()), translate(argument, ruleContext, context, variableStack)));
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[i].get()), translate(argument, ruleContext, variableStack)));
}
variableStack.pop();
ast::Predicate predicate(predicateDeclaration);
ast::Predicate predicate(std::string(function.name));
predicate.arguments.reserve(function.arguments.size());
for (size_t i = 0; i < function.arguments.size(); i++)
@ -96,8 +93,7 @@ struct BodyTermTranslateVisitor
}
template<class T>
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &,
const Clingo::AST::Term &term, RuleContext &, Context &, ast::VariableStack &)
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, RuleContext &, ast::VariableStack &)
{
assert(!term.data.is<Clingo::AST::Function>());
@ -110,18 +106,18 @@ struct BodyTermTranslateVisitor
struct BodyLiteralTranslateVisitor
{
std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, Context &, ast::VariableStack &)
std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, ast::VariableStack &)
{
return ast::Formula::make<ast::Boolean>(boolean.value);
}
std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack)
std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack)
{
return term.data.accept(BodyTermTranslateVisitor(), literal, term, ruleContext, context, variableStack);
return term.data.accept(BodyTermTranslateVisitor(), literal, term, ruleContext, variableStack);
}
// TODO: refactor
std::optional<ast::Formula> visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack)
std::optional<ast::Formula> visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack)
{
// Comparisons should never have a sign, because these are converted to positive comparisons by clingo
if (literal.sign != Clingo::AST::Sign::None)
@ -136,15 +132,15 @@ struct BodyLiteralTranslateVisitor
ast::And conjunction;
conjunction.arguments.reserve(3);
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, context, variableStack)));
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[1].get()), translate(comparison.right, ruleContext, variableStack)));
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));
}
template<class T>
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, Context &, ast::VariableStack &)
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, ast::VariableStack &)
{
throw TranslationException(literal.location, "literal currently unsupported in this context, expected function or term");
return std::nullopt;
@ -155,16 +151,16 @@ struct BodyLiteralTranslateVisitor
struct BodyBodyLiteralTranslateVisitor
{
std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack)
std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &ruleContext, ast::VariableStack &variableStack)
{
if (bodyLiteral.sign != Clingo::AST::Sign::None)
throw TranslationException(bodyLiteral.location, "only positive body literals supported currently");
return literal.data.accept(BodyLiteralTranslateVisitor(), literal, ruleContext, context, variableStack);
return literal.data.accept(BodyLiteralTranslateVisitor(), literal, ruleContext, variableStack);
}
template<class T>
std::optional<ast::Formula> visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &, Context &, ast::VariableStack &)
std::optional<ast::Formula> visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &, ast::VariableStack &)
{
throw TranslationException(bodyLiteral.location, "body literal currently unsupported in this context, expected literal");
return std::nullopt;

View File

@ -16,9 +16,9 @@ namespace anthem
//
////////////////////////////////////////////////////////////////////////////////////////////////////
struct PredicateDeclarationMeta
struct PredicateSignatureMeta
{
ast::PredicateDeclaration *declaration;
ast::PredicateSignature predicateSignature;
bool used{false};
};
@ -33,59 +33,13 @@ struct Context
{
}
ast::PredicateDeclaration *findOrCreatePredicateDeclaration(const char *name, size_t arity)
{
const auto matchesExistingPredicateDeclaration =
[&](const auto &predicateDeclaration)
{
return (predicateDeclaration->arity() == arity
&& strcmp(predicateDeclaration->name.c_str(), name) == 0);
};
auto matchingPredicateDeclaration = std::find_if(predicateDeclarations.begin(),
predicateDeclarations.end(), matchesExistingPredicateDeclaration);
if (matchingPredicateDeclaration != predicateDeclarations.end())
return matchingPredicateDeclaration->get();
predicateDeclarations.emplace_back(std::make_unique<ast::PredicateDeclaration>(name, arity));
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;
bool performSimplification{false};
bool performCompletion{false};
bool performIntegerDetection{false};
bool performSimplification = false;
bool performCompletion = false;
std::vector<std::unique_ptr<ast::PredicateDeclaration>> predicateDeclarations;
ast::PredicateDeclaration::Visibility defaultPredicateVisibility{ast::PredicateDeclaration::Visibility::Visible};
std::vector<std::unique_ptr<ast::FunctionDeclaration>> functionDeclarations;
bool externalStatementsUsed{false};
bool showStatementsUsed{false};
std::optional<std::vector<PredicateSignatureMeta>> visiblePredicateSignatures;
std::optional<std::vector<PredicateSignatureMeta>> externalPredicateSignatures;
ast::ParenthesisStyle parenthesisStyle = ast::ParenthesisStyle::Normal;
};

View File

@ -3,7 +3,6 @@
#include <anthem/AST.h>
#include <anthem/ASTUtils.h>
#include <anthem/Utils.h>
namespace anthem
{
@ -16,6 +15,16 @@ namespace ast
//
////////////////////////////////////////////////////////////////////////////////////////////////////
// TODO: move to separate class
enum class Tristate
{
True,
False,
Unknown,
};
////////////////////////////////////////////////////////////////////////////////////////////////////
Tristate equal(const Formula &lhs, const Formula &rhs);
Tristate equal(const Term &lhs, const Term &rhs);
@ -228,7 +237,7 @@ struct FormulaEqualityVisitor
const auto &otherPredicate = otherFormula.get<Predicate>();
if (predicate.declaration != otherPredicate.declaration)
if (!matches(predicate, otherPredicate))
return Tristate::False;
assert(predicate.arguments.size() == otherPredicate.arguments.size());
@ -268,8 +277,8 @@ struct TermEqualityVisitor
return Tristate::Unknown;
}
if (equal(binaryOperation.left, otherBinaryOperation.right) == Tristate::True
&& equal(binaryOperation.right, otherBinaryOperation.left) == Tristate::True)
if (equal(binaryOperation.left, binaryOperation.right) == Tristate::True
&& equal(binaryOperation.right, binaryOperation.left) == Tristate::True)
{
return Tristate::True;
}
@ -289,6 +298,18 @@ struct TermEqualityVisitor
: Tristate::False;
}
Tristate visit(const Constant &constant, const Term &otherTerm)
{
if (!otherTerm.is<Constant>())
return Tristate::Unknown;
const auto &otherConstant = otherTerm.get<Constant>();
return (constant.name == otherConstant.name)
? Tristate::True
: Tristate::False;
}
Tristate visit(const Function &function, const Term &otherTerm)
{
if (!otherTerm.is<Function>())
@ -296,7 +317,7 @@ struct TermEqualityVisitor
const auto &otherFunction = otherTerm.get<Function>();
if (function.declaration != otherFunction.declaration)
if (function.name != otherFunction.name)
return Tristate::False;
if (function.arguments.size() != otherFunction.arguments.size())

View File

@ -1,244 +0,0 @@
#ifndef __ANTHEM__EVALUATION_H
#define __ANTHEM__EVALUATION_H
#include <anthem/AST.h>
#include <anthem/ASTUtils.h>
#include <anthem/Utils.h>
namespace anthem
{
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// Evaluation
//
////////////////////////////////////////////////////////////////////////////////////////////////////
template <class VariableDomainAccessor = DefaultVariableDomainAccessor>
struct EvaluateFormulaVisitor
{
template <class... Arguments>
static EvaluationResult visit(const ast::And &and_, Arguments &&... arguments)
{
bool someFalse = false;
bool someUnknown = false;
for (const auto &argument : and_.arguments)
{
const auto result = evaluate(argument, std::forward<Arguments>(arguments)...);
switch (result)
{
case EvaluationResult::Error:
return EvaluationResult::Error;
case EvaluationResult::True:
break;
case EvaluationResult::False:
someFalse = true;
break;
case EvaluationResult::Unknown:
someUnknown = true;
break;
}
}
if (someFalse)
return EvaluationResult::False;
if (someUnknown)
return EvaluationResult::Unknown;
return EvaluationResult::True;
}
template <class... Arguments>
static EvaluationResult visit(const ast::Biconditional &biconditional, Arguments &&... arguments)
{
const auto leftResult = evaluate(biconditional.left, std::forward<Arguments>(arguments)...);
const auto rightResult = evaluate(biconditional.right, std::forward<Arguments>(arguments)...);
if (leftResult == EvaluationResult::Error || rightResult == EvaluationResult::Error)
return EvaluationResult::Error;
if (leftResult == EvaluationResult::Unknown || rightResult == EvaluationResult::Unknown)
return EvaluationResult::Unknown;
return (leftResult == rightResult ? EvaluationResult::True : EvaluationResult::False);
}
template <class... Arguments>
static EvaluationResult visit(const ast::Boolean &boolean, Arguments &&...)
{
return (boolean.value == true ? EvaluationResult::True : EvaluationResult::False);
}
template <class... Arguments>
static EvaluationResult visit(const ast::Comparison &comparison, Arguments &&... arguments)
{
const auto leftType = type(comparison.left, std::forward<Arguments>(arguments)...);
const auto rightType = type(comparison.right, std::forward<Arguments>(arguments)...);
// Comparisons with empty sets always return false
if (leftType.setSize == SetSize::Empty || rightType.setSize == SetSize::Empty)
return EvaluationResult::False;
// If either side has an unknown domain, the result is unknown
if (leftType.domain == Domain::Unknown || rightType.domain == Domain::Unknown)
return EvaluationResult::Unknown;
// If both sides have the same domain, the result is unknown
if (leftType.domain == rightType.domain)
return EvaluationResult::Unknown;
// If one side is integer, but the other one isnt, they are not equal
switch (comparison.operator_)
{
case ast::Comparison::Operator::Equal:
return EvaluationResult::False;
case ast::Comparison::Operator::NotEqual:
return EvaluationResult::True;
default:
// TODO: implement more cases
return EvaluationResult::Unknown;
}
}
template <class... Arguments>
static EvaluationResult visit(const ast::Exists &exists, Arguments &&... arguments)
{
return evaluate(exists.argument, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
static EvaluationResult visit(const ast::ForAll &forAll, Arguments &&... arguments)
{
return evaluate(forAll.argument, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
static EvaluationResult visit(const ast::Implies &implies, Arguments &&... arguments)
{
const auto antecedentResult = evaluate(implies.antecedent, std::forward<Arguments>(arguments)...);
const auto consequentResult = evaluate(implies.consequent, std::forward<Arguments>(arguments)...);
if (antecedentResult == EvaluationResult::Error || consequentResult == EvaluationResult::Error)
return EvaluationResult::Error;
if (antecedentResult == EvaluationResult::False)
return EvaluationResult::True;
if (consequentResult == EvaluationResult::True)
return EvaluationResult::True;
if (antecedentResult == EvaluationResult::True && consequentResult == EvaluationResult::False)
return EvaluationResult::False;
return EvaluationResult::Unknown;
}
template <class... Arguments>
static EvaluationResult visit(const ast::In &in, Arguments &&... arguments)
{
const auto elementType = type(in.element, std::forward<Arguments>(arguments)...);
const auto setType = type(in.set, std::forward<Arguments>(arguments)...);
// The element to test shouldnt be empty or a proper set by itself
assert(elementType.setSize != SetSize::Empty && elementType.setSize != SetSize::Multi);
// If the set is empty, no element can be selected
if (setType.setSize == SetSize::Empty)
return EvaluationResult::False;
// If one of the sides has an unknown type, the result is unknown
if (elementType.domain == Domain::Unknown || setType.domain == Domain::Unknown)
return EvaluationResult::Unknown;
// If both sides have the same domain, the result is unknown
if (elementType.domain == setType.domain)
return EvaluationResult::Unknown;
// If one side is integer, but the other one isnt, set inclusion is never satisfied
return EvaluationResult::False;
}
template <class... Arguments>
static EvaluationResult visit(const ast::Not &not_, Arguments &&... arguments)
{
const auto result = evaluate(not_.argument, std::forward<Arguments>(arguments)...);
if (result == EvaluationResult::Error || result == EvaluationResult::Unknown)
return result;
return (result == EvaluationResult::True ? EvaluationResult::False : EvaluationResult::True);
}
template <class... Arguments>
static EvaluationResult visit(const ast::Or &or_, Arguments &&... arguments)
{
bool someTrue = false;
bool someUnknown = false;
for (const auto &argument : or_.arguments)
{
const auto result = evaluate(argument, std::forward<Arguments>(arguments)...);
switch (result)
{
case EvaluationResult::Error:
return EvaluationResult::Error;
case EvaluationResult::True:
someTrue = true;
break;
case EvaluationResult::False:
break;
case EvaluationResult::Unknown:
someUnknown = true;
break;
}
}
if (someTrue)
return EvaluationResult::True;
if (someUnknown)
return EvaluationResult::Unknown;
return EvaluationResult::False;
}
template <class... Arguments>
static EvaluationResult visit(const ast::Predicate &predicate, Arguments &&... arguments)
{
assert(predicate.arguments.size() == predicate.declaration->arity());
for (size_t i = 0; i < predicate.arguments.size(); i++)
{
const auto &argument = predicate.arguments[i];
const auto &parameter = predicate.declaration->parameters[i];
if (parameter.domain != Domain::Integer)
continue;
const auto argumentType = type(argument, std::forward<Arguments>(arguments)...);
if (argumentType.domain == Domain::Noninteger || argumentType.setSize == SetSize::Empty)
return EvaluationResult::Error;
}
return EvaluationResult::Unknown;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
template <class VariableDomainAccessor = DefaultVariableDomainAccessor, class... Arguments>
EvaluationResult evaluate(const ast::Formula &formula, Arguments &&... arguments)
{
return formula.accept(EvaluateFormulaVisitor<VariableDomainAccessor>(), std::forward<Arguments>(arguments)...);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
}
#endif

View File

@ -118,7 +118,8 @@ struct HeadLiteralCollectFunctionTermsVisitor
struct FunctionTermTranslateVisitor
{
std::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
// TODO: check correctness
std::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, size_t &headVariableIndex)
{
if (function.external)
throw TranslationException(term.location, "external functions currently unsupported");
@ -129,14 +130,11 @@ struct FunctionTermTranslateVisitor
for (size_t i = 0; i < function.arguments.size(); i++)
arguments.emplace_back(ast::Variable(ruleContext.freeVariables[headVariableIndex++].get()));
auto predicateDeclaration = context.findOrCreatePredicateDeclaration(function.name, function.arguments.size());
predicateDeclaration->isUsed = true;
return ast::Predicate(predicateDeclaration, std::move(arguments));
return ast::Formula::make<ast::Predicate>(function.name, std::move(arguments));
}
template<class T>
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Term &term, RuleContext &, Context &, size_t &)
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Term &term, RuleContext &, size_t &)
{
throw TranslationException(term.location, "term currently unsupported in this context, function expected");
return std::nullopt;
@ -147,18 +145,18 @@ struct FunctionTermTranslateVisitor
struct LiteralTranslateVisitor
{
std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, Context &, size_t &)
std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, size_t &)
{
return ast::Formula::make<ast::Boolean>(boolean.value);
}
std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, RuleContext &ruleContext, size_t &headVariableIndex)
{
return term.data.accept(FunctionTermTranslateVisitor(), term, ruleContext, context, headVariableIndex);
return term.data.accept(FunctionTermTranslateVisitor(), term, ruleContext, headVariableIndex);
}
template<class T>
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, Context &, size_t &)
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, size_t &)
{
throw TranslationException(literal.location, "only disjunctions of literals allowed as head literals");
return std::nullopt;
@ -169,12 +167,12 @@ struct LiteralTranslateVisitor
struct HeadLiteralTranslateToConsequentVisitor
{
std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, RuleContext &ruleContext, size_t &headVariableIndex)
{
if (literal.sign == Clingo::AST::Sign::DoubleNegation)
throw TranslationException(literal.location, "double-negated head literals currently unsupported");
auto translatedLiteral = literal.data.accept(LiteralTranslateVisitor(), literal, ruleContext, context, headVariableIndex);
auto translatedLiteral = literal.data.accept(LiteralTranslateVisitor(), literal, ruleContext, headVariableIndex);
if (literal.sign == Clingo::AST::Sign::None)
return translatedLiteral;
@ -185,7 +183,7 @@ struct HeadLiteralTranslateToConsequentVisitor
return ast::Formula::make<ast::Not>(std::move(translatedLiteral.value()));
}
std::optional<ast::Formula> visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
std::optional<ast::Formula> visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, size_t &headVariableIndex)
{
std::vector<ast::Formula> arguments;
arguments.reserve(disjunction.elements.size());
@ -195,7 +193,7 @@ struct HeadLiteralTranslateToConsequentVisitor
if (!conditionalLiteral.condition.empty())
throw TranslationException(headLiteral.location, "conditional head literals currently unsupported");
auto argument = visit(conditionalLiteral.literal, headLiteral, ruleContext, context, headVariableIndex);
auto argument = visit(conditionalLiteral.literal, headLiteral, ruleContext, headVariableIndex);
if (!argument)
throw TranslationException(headLiteral.location, "could not parse argument");
@ -206,7 +204,7 @@ struct HeadLiteralTranslateToConsequentVisitor
return ast::Formula::make<ast::Or>(std::move(arguments));
}
std::optional<ast::Formula> visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
std::optional<ast::Formula> visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, size_t &headVariableIndex)
{
if (aggregate.left_guard || aggregate.right_guard)
throw TranslationException(headLiteral.location, "aggregates with left or right guards currently unsupported");
@ -217,7 +215,7 @@ struct HeadLiteralTranslateToConsequentVisitor
if (!conditionalLiteral.condition.empty())
throw TranslationException(headLiteral.location, "conditional head literals currently unsupported");
return this->visit(conditionalLiteral.literal, headLiteral, ruleContext, context, headVariableIndex);
return this->visit(conditionalLiteral.literal, headLiteral, ruleContext, headVariableIndex);
};
if (aggregate.elements.size() == 1)
@ -240,7 +238,7 @@ struct HeadLiteralTranslateToConsequentVisitor
}
template<class T>
std::optional<ast::Formula> visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &, Context &, size_t &)
std::optional<ast::Formula> visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &, size_t &)
{
throw TranslationException(headLiteral.location, "head literal currently unsupported in this context, expected literal, disjunction, or aggregate");
return std::nullopt;

View File

@ -13,7 +13,7 @@ namespace anthem
//
////////////////////////////////////////////////////////////////////////////////////////////////////
void eliminateHiddenPredicates(std::vector<ast::Formula> &completedFormulas, Context &context);
void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predicateSignatures, std::vector<ast::Formula> &completedFormulas, Context &context);
////////////////////////////////////////////////////////////////////////////////////////////////////

View File

@ -1,22 +0,0 @@
#ifndef __ANTHEM__INTEGER_VARIABLE_DETECTION_H
#define __ANTHEM__INTEGER_VARIABLE_DETECTION_H
#include <anthem/AST.h>
#include <anthem/Context.h>
namespace anthem
{
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// IntegerVariableDetection
//
////////////////////////////////////////////////////////////////////////////////////////////////////
void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas);
////////////////////////////////////////////////////////////////////////////////////////////////////
}
#endif

View File

@ -12,6 +12,14 @@ namespace anthem
//
////////////////////////////////////////////////////////////////////////////////////////////////////
enum class SimplificationResult
{
Simplified,
Unchanged,
};
////////////////////////////////////////////////////////////////////////////////////////////////////
void simplify(ast::Formula &formula);
////////////////////////////////////////////////////////////////////////////////////////////////////

View File

@ -3,7 +3,6 @@
#include <anthem/AST.h>
#include <anthem/Simplification.h>
#include <anthem/Utils.h>
namespace anthem
{
@ -20,96 +19,96 @@ template<class T>
struct FormulaSimplificationVisitor
{
template <class... Arguments>
OperationResult visit(And &and_, Formula &formula, Arguments &&... arguments)
SimplificationResult visit(And &and_, Formula &formula, Arguments &&... arguments)
{
for (auto &argument : and_.arguments)
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
return SimplificationResult::Simplified;
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Biconditional &biconditional, Formula &formula, Arguments &&... arguments)
SimplificationResult visit(Biconditional &biconditional, Formula &formula, Arguments &&... arguments)
{
if (biconditional.left.accept(*this, biconditional.left, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
if (biconditional.left.accept(*this, biconditional.left, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
return SimplificationResult::Simplified;
if (biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
if (biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
return SimplificationResult::Simplified;
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Boolean &, Formula &formula, Arguments &&... arguments)
SimplificationResult visit(Boolean &, Formula &formula, Arguments &&... arguments)
{
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Comparison &, Formula &formula, Arguments &&... arguments)
SimplificationResult visit(Comparison &, Formula &formula, Arguments &&... arguments)
{
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Exists &exists, Formula &formula, Arguments &&... arguments)
SimplificationResult visit(Exists &exists, Formula &formula, Arguments &&... arguments)
{
if (exists.argument.accept(*this, exists.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
if (exists.argument.accept(*this, exists.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
return SimplificationResult::Simplified;
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(ForAll &forAll, Formula &formula, Arguments &&... arguments)
SimplificationResult visit(ForAll &forAll, Formula &formula, Arguments &&... arguments)
{
if (forAll.argument.accept(*this, forAll.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
if (forAll.argument.accept(*this, forAll.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
return SimplificationResult::Simplified;
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Implies &implies, Formula &formula, Arguments &&... arguments)
SimplificationResult visit(Implies &implies, Formula &formula, Arguments &&... arguments)
{
if (implies.antecedent.accept(*this, implies.antecedent, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
if (implies.antecedent.accept(*this, implies.antecedent, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
return SimplificationResult::Simplified;
if (implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
if (implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
return SimplificationResult::Simplified;
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(In &, Formula &formula, Arguments &&... arguments)
SimplificationResult visit(In &, Formula &formula, Arguments &&... arguments)
{
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Not &not_, Formula &formula, Arguments &&... arguments)
SimplificationResult visit(Not &not_, Formula &formula, Arguments &&... arguments)
{
if (not_.argument.accept(*this, not_.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
if (not_.argument.accept(*this, not_.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
return SimplificationResult::Simplified;
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Or &or_, Formula &formula, Arguments &&... arguments)
SimplificationResult visit(Or &or_, Formula &formula, Arguments &&... arguments)
{
for (auto &argument : or_.arguments)
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
return SimplificationResult::Simplified;
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Predicate &, Formula &formula, Arguments &&... arguments)
SimplificationResult visit(Predicate &, Formula &formula, Arguments &&... arguments)
{
return T::accept(formula, std::forward<Arguments>(arguments)...);
}
@ -117,69 +116,75 @@ struct FormulaSimplificationVisitor
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class T, class OperationResult = void>
template<class T, class SimplificationResult = void>
struct TermSimplificationVisitor
{
template <class... Arguments>
OperationResult visit(BinaryOperation &binaryOperation, Term &term, Arguments &&... arguments)
SimplificationResult visit(BinaryOperation &binaryOperation, Term &term, Arguments &&... arguments)
{
if (binaryOperation.left.accept(*this, binaryOperation.left, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
if (binaryOperation.left.accept(*this, binaryOperation.left, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
return SimplificationResult::Simplified;
if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
return SimplificationResult::Simplified;
return T::accept(term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Boolean &, Term &term, Arguments &&... arguments)
SimplificationResult visit(Boolean &, Term &term, Arguments &&... arguments)
{
return T::accept(term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Function &function, Term &term, Arguments &&... arguments)
SimplificationResult visit(Constant &, Term &term, Arguments &&... arguments)
{
return T::accept(term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
SimplificationResult visit(Function &function, Term &term, Arguments &&... arguments)
{
for (auto &argument : function.arguments)
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
return SimplificationResult::Simplified;
return T::accept(term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Integer &, Term &term, Arguments &&... arguments)
SimplificationResult visit(Integer &, Term &term, Arguments &&... arguments)
{
return T::accept(term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Interval &interval, Term &term, Arguments &&... arguments)
SimplificationResult visit(Interval &interval, Term &term, Arguments &&... arguments)
{
if (interval.from.accept(*this, interval.from, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
if (interval.from.accept(*this, interval.from, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
return SimplificationResult::Simplified;
if (interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return OperationResult::Changed;
if (interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
return SimplificationResult::Simplified;
return T::accept(term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments)
SimplificationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments)
{
return T::accept(term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(String &, Term &term, Arguments &&... arguments)
SimplificationResult visit(String &, Term &term, Arguments &&... arguments)
{
return T::accept(term, std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
OperationResult visit(Variable &, Term &term, Arguments &&... arguments)
SimplificationResult visit(Variable &, Term &term, Arguments &&... arguments)
{
return T::accept(term, std::forward<Arguments>(arguments)...);
}

View File

@ -73,7 +73,7 @@ struct StatementVisitor
// Compute consequent
auto headVariableIndex = ruleContext.headVariablesStartIndex;
auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, ruleContext, context, headVariableIndex);
auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, ruleContext, headVariableIndex);
assert(ruleContext.headTerms.size() == headVariableIndex - ruleContext.headVariablesStartIndex);
@ -87,7 +87,7 @@ struct StatementVisitor
const auto auxiliaryHeadVariableID = ruleContext.headVariablesStartIndex + i - ruleContext.headTerms.cbegin();
auto element = ast::Variable(ruleContext.freeVariables[auxiliaryHeadVariableID].get());
auto set = translate(headTerm, ruleContext, context, variableStack);
auto set = translate(headTerm, ruleContext, variableStack);
auto in = ast::In(std::move(element), std::move(set));
antecedent.arguments.emplace_back(std::move(in));
@ -98,7 +98,7 @@ struct StatementVisitor
{
const auto &bodyLiteral = *i;
auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, ruleContext, context, variableStack);
auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, ruleContext, variableStack);
if (!argument)
throw TranslationException(bodyLiteral.location, "could not translate body literal");
@ -165,8 +165,8 @@ struct StatementVisitor
if (signature.negative())
throw LogicException(statement.location, "negative #show atom signatures are currently unsupported");
context.showStatementsUsed = true;
context.defaultPredicateVisibility = ast::PredicateDeclaration::Visibility::Hidden;
if (!context.visiblePredicateSignatures)
context.visiblePredicateSignatures.emplace();
if (std::strlen(signature.name()) == 0)
{
@ -176,8 +176,8 @@ struct StatementVisitor
context.logger.log(output::Priority::Debug, statement.location) << "showing “" << signature.name() << "/" << signature.arity() << "";
auto predicateDeclaration = context.findOrCreatePredicateDeclaration(signature.name(), signature.arity());
predicateDeclaration->visibility = ast::PredicateDeclaration::Visibility::Visible;
auto predicateSignature = ast::PredicateSignature{std::string(signature.name()), signature.arity()};
context.visiblePredicateSignatures.value().emplace_back(PredicateSignatureMeta{std::move(predicateSignature)});
}
void visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &)
@ -190,7 +190,7 @@ struct StatementVisitor
const auto fail =
[&]()
{
throw LogicException(statement.location, "only #external declarations of the form “#external <predicate name>(<arity>). or #external integer(<function name>(<arity>)). supported");
throw LogicException(statement.location, "only #external declarations of the form “#external <predicate name>(<arity>). supported");
};
if (!external.body.empty())
@ -204,47 +204,6 @@ struct StatementVisitor
if (predicate.arguments.size() != 1)
fail();
const auto handleIntegerDeclaration =
[&]()
{
// Integer function declarations are treated separately if applicable
if (strcmp(predicate.name, "integer") != 0)
return false;
if (predicate.arguments.size() != 1)
return false;
const auto &functionArgument = predicate.arguments.front();
if (!functionArgument.data.is<Clingo::AST::Function>())
return false;
const auto &function = functionArgument.data.get<Clingo::AST::Function>();
if (function.arguments.size() != 1)
return false;
const auto &arityArgument = function.arguments.front();
if (!arityArgument.data.is<Clingo::Symbol>())
return false;
const auto &aritySymbol = arityArgument.data.get<Clingo::Symbol>();
if (aritySymbol.type() != Clingo::SymbolType::Number)
return false;
const size_t arity = aritySymbol.number();
auto functionDeclaration = context.findOrCreateFunctionDeclaration(function.name, arity);
functionDeclaration->domain = Domain::Integer;
return true;
};
if (handleIntegerDeclaration())
return;
const auto &arityArgument = predicate.arguments.front();
if (!arityArgument.data.is<Clingo::Symbol>())
@ -255,12 +214,13 @@ struct StatementVisitor
if (aritySymbol.type() != Clingo::SymbolType::Number)
fail();
context.externalStatementsUsed = true;
const size_t arity = arityArgument.data.get<Clingo::Symbol>().number();
const size_t arity = aritySymbol.number();
if (!context.externalPredicateSignatures)
context.externalPredicateSignatures.emplace();
auto predicateDeclaration = context.findOrCreatePredicateDeclaration(predicate.name, arity);
predicateDeclaration->isExternal = true;
auto predicateSignature = ast::PredicateSignature{std::string(predicate.name), arity};
context.externalPredicateSignatures->emplace_back(PredicateSignatureMeta{std::move(predicateSignature)});
}
template<class T>

View File

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

View File

@ -1,157 +0,0 @@
#ifndef __ANTHEM__TYPE_H
#define __ANTHEM__TYPE_H
#include <anthem/AST.h>
#include <anthem/ASTUtils.h>
#include <anthem/Utils.h>
namespace anthem
{
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// Type
//
////////////////////////////////////////////////////////////////////////////////////////////////////
template <class VariableDomainAccessor = DefaultVariableDomainAccessor, class... Arguments>
Type type(const ast::Term &term, Arguments &&... arguments);
////////////////////////////////////////////////////////////////////////////////////////////////////
template <class VariableDomainAccessor = DefaultVariableDomainAccessor>
struct TermTypeVisitor
{
template <class... Arguments>
static Type visit(const ast::BinaryOperation &binaryOperation, Arguments &&... arguments)
{
const auto leftType = type<VariableDomainAccessor>(binaryOperation.left, std::forward<Arguments>(arguments)...);
const auto rightType = type<VariableDomainAccessor>(binaryOperation.right, std::forward<Arguments>(arguments)...);
// Binary operations on empty sets return an empty set (also with division)
if (leftType.setSize == SetSize::Empty || rightType.setSize == SetSize::Empty)
return {Domain::Unknown, SetSize::Empty};
// Binary operations on nonintegers return an empty set (also with division)
if (leftType.domain == Domain::Noninteger || rightType.domain == Domain::Noninteger)
return {Domain::Unknown, SetSize::Empty};
// Binary operations on unknown types return an unknown set
if (leftType.domain == Domain::Unknown || rightType.domain == Domain::Unknown)
return {Domain::Unknown, SetSize::Unknown};
// Divisions return an unknown set
if (binaryOperation.operator_ == ast::BinaryOperation::Operator::Division)
return {Domain::Integer, SetSize::Unknown};
// Binary operations on integer sets of unknown size return an integer set of unknown size
if (leftType.setSize == SetSize::Unknown || rightType.setSize == SetSize::Unknown)
return {Domain::Integer, SetSize::Unknown};
// Binary operations on integer sets with multiple elements return an integer set with multiple elements
if (leftType.setSize == SetSize::Multi || rightType.setSize == SetSize::Multi)
return {Domain::Integer, SetSize::Multi};
// Binary operations on plain integers return a plain integer
return {Domain::Integer, SetSize::Unit};
}
template <class... Arguments>
static Type visit(const ast::Boolean &, Arguments &&...)
{
return {Domain::Noninteger, SetSize::Unit};
}
template <class... Arguments>
static Type visit(const ast::Function &function, Arguments &&...)
{
// TODO: check that functions cannot return sets
return {function.declaration->domain, SetSize::Unit};
}
template <class... Arguments>
static Type visit(const ast::Integer &, Arguments &&...)
{
return {Domain::Integer, SetSize::Unit};
}
template <class... Arguments>
static Type visit(const ast::Interval &interval, Arguments &&... arguments)
{
const auto fromType = type<VariableDomainAccessor>(interval.from, std::forward<Arguments>(arguments)...);
const auto toType = type<VariableDomainAccessor>(interval.to, std::forward<Arguments>(arguments)...);
// Intervals with empty sets return an empty set
if (fromType.setSize == SetSize::Empty || toType.setSize == SetSize::Empty)
return {Domain::Unknown, SetSize::Empty};
// Intervals with nonintegers return an empty set
if (fromType.domain == Domain::Noninteger || toType.domain == Domain::Noninteger)
return {Domain::Unknown, SetSize::Empty};
// Intervals with unknown types return an unknown set
if (fromType.domain == Domain::Unknown || toType.domain == Domain::Unknown)
return {Domain::Unknown, SetSize::Unknown};
// Intervals with integers generally return integer sets
// TODO: handle 1-element intervals such as 1..1 and empty intervals such as 2..1
return {Domain::Integer, SetSize::Unknown};
}
template <class... Arguments>
static Type visit(const ast::SpecialInteger &, Arguments &&...)
{
return {Domain::Noninteger, SetSize::Unit};
}
template <class... Arguments>
static Type visit(const ast::String &, Arguments &&...)
{
return {Domain::Noninteger, SetSize::Unit};
}
template <class... Arguments>
static Type visit(const ast::UnaryOperation &unaryOperation, Arguments &&... arguments)
{
assert(unaryOperation.operator_ == ast::UnaryOperation::Operator::Absolute);
const auto argumentType = type<VariableDomainAccessor>(unaryOperation.argument, std::forward<Arguments>(arguments)...);
// Absolute value of an empty set returns an empty set
if (argumentType.setSize == SetSize::Empty)
return {Domain::Unknown, SetSize::Empty};
// Absolute value of nonintegers returns an empty set
if (argumentType.domain == Domain::Noninteger)
return {Domain::Unknown, SetSize::Empty};
// Absolute value of integers returns the same type
if (argumentType.domain == Domain::Integer)
return argumentType;
return {Domain::Unknown, SetSize::Unknown};
}
template <class... Arguments>
static Type visit(const ast::Variable &variable, Arguments &&... arguments)
{
const auto domain = VariableDomainAccessor()(variable, std::forward<Arguments>(arguments)...);
return {domain, SetSize::Unit};
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
template <class VariableDomainAccessor, class... Arguments>
Type type(const ast::Term &term, Arguments &&... arguments)
{
return term.accept(TermTypeVisitor<VariableDomainAccessor>(), std::forward<Arguments>(arguments)...);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
}
#endif

View File

@ -1,6 +1,13 @@
#ifndef __ANTHEM__UTILS_H
#define __ANTHEM__UTILS_H
#include <iostream>
#include <clingo.hh>
#include <anthem/Context.h>
#include <anthem/Location.h>
namespace anthem
{
@ -13,61 +20,6 @@ namespace anthem
constexpr const auto HeadVariablePrefix = "V";
constexpr const auto BodyVariablePrefix = "X";
constexpr const auto UserVariablePrefix = "U";
constexpr const auto IntegerVariablePrefix = "N";
////////////////////////////////////////////////////////////////////////////////////////////////////
enum class Tristate
{
True,
False,
Unknown,
};
////////////////////////////////////////////////////////////////////////////////////////////////////
enum class OperationResult
{
Unchanged,
Changed,
};
////////////////////////////////////////////////////////////////////////////////////////////////////
enum class EvaluationResult
{
True,
False,
Unknown,
Error,
};
////////////////////////////////////////////////////////////////////////////////////////////////////
enum class Domain
{
Noninteger,
Integer,
Unknown,
};
////////////////////////////////////////////////////////////////////////////////////////////////////
enum class SetSize
{
Empty,
Unit,
Multi,
Unknown,
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct Type
{
Domain domain{Domain::Unknown};
SetSize setSize{SetSize::Unknown};
};
////////////////////////////////////////////////////////////////////////////////////////////////////

View File

@ -35,7 +35,6 @@ struct PrintContext
std::map<const VariableDeclaration *, size_t> userVariableIDs;
std::map<const VariableDeclaration *, size_t> headVariableIDs;
std::map<const VariableDeclaration *, size_t> bodyVariableIDs;
std::map<const VariableDeclaration *, size_t> integerVariableIDs;
const Context &context;
};
@ -47,12 +46,12 @@ output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &b
output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, Comparison::Operator operator_, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const PredicateDeclaration &predicateDeclaration, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &printContext, bool omitParentheses = false);
output::ColorStream &print(output::ColorStream &stream, const UnaryOperation &unaryOperation, PrintContext &printContext, bool omitParentheses = false);
@ -168,9 +167,16 @@ inline output::ColorStream &print(output::ColorStream &stream, const Comparison
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &, bool)
{
return (stream << constant.name);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext, bool)
{
stream << function.declaration->name;
stream << function.name;
if (function.arguments.empty())
return stream;
@ -185,7 +191,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Function &f
print(stream, *i, printContext);
}
if (function.declaration->name.empty() && function.arguments.size() == 1)
if (function.name.empty() && function.arguments.size() == 1)
stream << ",";
stream << ")";
@ -219,16 +225,16 @@ inline output::ColorStream &print(output::ColorStream &stream, const Integer &in
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool omitParentheses)
inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool)
{
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << "(";
print(stream, interval.from, printContext);
stream << "..";
print(stream, interval.to, printContext);
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << ")";
return stream;
@ -238,7 +244,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Interval &i
inline output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext, bool)
{
stream << predicate.declaration->name;
stream << predicate.name;
if (predicate.arguments.empty())
return stream;
@ -260,13 +266,6 @@ inline output::ColorStream &print(output::ColorStream &stream, const Predicate &
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const PredicateDeclaration &predicateDeclaration, PrintContext &, bool)
{
return (stream << predicateDeclaration.name << "/" << predicateDeclaration.arity());
}
////////////////////////////////////////////////////////////////////////////////////////////////////
inline output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &, bool)
{
switch (specialInteger.type)
@ -340,9 +339,6 @@ inline output::ColorStream &print(output::ColorStream &stream, const VariableDec
return (stream << output::Variable(variableName.c_str()));
};
if (variableDeclaration.domain == Domain::Integer)
return printVariableDeclaration(IntegerVariablePrefix, printContext.integerVariableIDs);
switch (variableDeclaration.type)
{
case VariableDeclaration::Type::UserDefined:

View File

@ -103,9 +103,16 @@ Comparison prepareCopy(const Comparison &other)
////////////////////////////////////////////////////////////////////////////////////////////////////
Constant prepareCopy(const Constant &other)
{
return Constant(std::string(other.name));
}
////////////////////////////////////////////////////////////////////////////////////////////////////
Function prepareCopy(const Function &other)
{
return Function(other.declaration, prepareCopy(other.arguments));
return Function(std::string(other.name), prepareCopy(other.arguments));
}
////////////////////////////////////////////////////////////////////////////////////////////////////
@ -133,7 +140,7 @@ Interval prepareCopy(const Interval &other)
Predicate prepareCopy(const Predicate &other)
{
return Predicate(other.declaration, prepareCopy(other.arguments));
return Predicate(std::string(other.name), prepareCopy(other.arguments));
}
////////////////////////////////////////////////////////////////////////////////////////////////////
@ -286,6 +293,11 @@ struct FixDanglingVariablesInTermVisitor
{
}
template <class... Arguments>
void visit(Constant &, Arguments &&...)
{
}
template <class... Arguments>
void visit(Function &function, Arguments &&... arguments)
{

View File

@ -150,6 +150,10 @@ struct CollectFreeVariablesVisitor
binaryOperation.right.accept(*this, variableStack, freeVariables);
}
void visit(Constant &, VariableStack &, std::vector<VariableDeclaration *> &)
{
}
void visit(Function &function, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
{
for (auto &argument : function.arguments)
@ -193,5 +197,84 @@ 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);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
}
}

View File

@ -35,41 +35,13 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c
auto &otherPredicate = implies.consequent.get<ast::Predicate>();
if (predicate.declaration != otherPredicate.declaration)
if (!ast::matches(predicate, otherPredicate))
continue;
assert(otherPredicate.arguments.size() == parameters.size());
auto &freeVariables = scopedFormula.freeVariables;
// Each formula with the predicate as its consequent currently has its own copy of the predicates parameters
// These need to be linked to the new, unique set of parameters
// First, remove the free variables whose occurrences will be relinked, which is why they are no longer needed
const auto isFreeVariableUnneeded =
[&](const auto &freeVariable)
{
const auto matchesVariableToBeReplaced = std::find_if(otherPredicate.arguments.cbegin(), otherPredicate.arguments.cend(),
[&](const ast::Term &argument)
{
assert(argument.is<ast::Variable>());
const auto &otherVariable = argument.get<ast::Variable>();
return (freeVariable.get() == otherVariable.declaration);
});
return (matchesVariableToBeReplaced != otherPredicate.arguments.cend());
};
freeVariables.erase(std::remove_if(freeVariables.begin(), freeVariables.end(), isFreeVariableUnneeded), freeVariables.end());
// Currently, only rules with singleton heads are supported
// Rules with multiple elements in the head are not yet handled correctly by the head variable detection mechanism
for (const auto &freeVariable : freeVariables)
if (freeVariable->type == ast::VariableDeclaration::Type::Head)
throw CompletionException("cannot perform completion, only singleton rule heads supported currently");
// Second, link all occurrences of the deleted free variable to the new, unique parameter
for (size_t i = 0; i < parameters.size(); i++)
{
assert(otherPredicate.arguments[i].is<ast::Variable>());
@ -78,6 +50,16 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c
scopedFormula.formula.accept(ast::ReplaceVariableInFormulaVisitor(), scopedFormula.formula, otherVariable.declaration, parameters[i].get());
}
// Remove all the head variables, because they are not free variables after completion
const auto isHeadVariable =
[](const auto &variableDeclaration)
{
return variableDeclaration->type == ast::VariableDeclaration::Type::Head;
};
auto &freeVariables = scopedFormula.freeVariables;
freeVariables.erase(std::remove_if(freeVariables.begin(), freeVariables.end(), isHeadVariable), freeVariables.end());
if (freeVariables.empty())
disjunction.get<ast::Or>().arguments.emplace_back(std::move(implies.antecedent));
else
@ -118,22 +100,22 @@ ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Fo
////////////////////////////////////////////////////////////////////////////////////////////////////
ast::Formula completePredicate(ast::PredicateDeclaration &predicateDeclaration, 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(predicateDeclaration.arity());
parameters.reserve(predicateSignature.arity);
std::vector<ast::Term> arguments;
arguments.reserve(predicateDeclaration.arity());
arguments.reserve(predicateSignature.arity);
for (size_t i = 0; i < predicateDeclaration.arity(); 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(&predicateDeclaration, 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));
@ -179,27 +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::sort(context.predicateDeclarations.begin(), context.predicateDeclarations.end(),
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(),
[](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 (auto &predicateDeclaration : context.predicateDeclarations)
{
if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal)
continue;
completedFormulas.emplace_back(completePredicate(*predicateDeclaration, scopedFormulas));
}
for (const auto &predicateSignature : predicateSignatures)
completedFormulas.emplace_back(completePredicate(predicateSignature, scopedFormulas));
// Complete integrity constraints
for (auto &scopedFormula : scopedFormulas)
@ -219,7 +202,7 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
}
// Eliminate all predicates that should not be visible in the output
eliminateHiddenPredicates(completedFormulas, context);
eliminateHiddenPredicates(predicateSignatures, completedFormulas, context);
return completedFormulas;
}

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

View File

@ -1,332 +0,0 @@
#include <anthem/IntegerVariableDetection.h>
#include <anthem/ASTCopy.h>
#include <anthem/ASTUtils.h>
#include <anthem/ASTVisitors.h>
#include <anthem/Evaluation.h>
#include <anthem/Exception.h>
#include <anthem/Simplification.h>
#include <anthem/Type.h>
#include <anthem/Utils.h>
#include <anthem/output/AST.h>
namespace anthem
{
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// IntegerVariableDetection
//
////////////////////////////////////////////////////////////////////////////////////////////////////
using VariableDomainMap = std::map<const ast::VariableDeclaration *, Domain>;
////////////////////////////////////////////////////////////////////////////////////////////////////
Domain domain(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
{
if (variable.declaration->domain != Domain::Unknown)
return variable.declaration->domain;
const auto match = variableDomainMap.find(variable.declaration);
if (match == variableDomainMap.end())
return Domain::Unknown;
return match->second;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
void clearVariableDomainMap(VariableDomainMap &variableDomainMap)
{
for (auto &variableDeclaration : variableDomainMap)
variableDeclaration.second = Domain::Unknown;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
struct VariableDomainMapAccessor
{
Domain operator()(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
{
return domain(variable, variableDomainMap);
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
Type type(const ast::Term &term, VariableDomainMap &variableDomainMap)
{
return type<VariableDomainMapAccessor>(term, variableDomainMap);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
EvaluationResult evaluate(const ast::Formula &formula, VariableDomainMap &variableDomainMap)
{
return evaluate<VariableDomainMap>(formula, variableDomainMap);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
template <class Functor>
struct ForEachVariableDeclarationVisitor
{
template <class... Arguments>
static OperationResult visit(ast::And &and_, Arguments &&... arguments)
{
auto operationResult = OperationResult::Unchanged;
for (auto &argument : and_.arguments)
if (argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed;
return operationResult;
}
template <class... Arguments>
static OperationResult visit(ast::Biconditional &biconditional, Arguments &&... arguments)
{
auto operationResult = OperationResult::Unchanged;
if (biconditional.left.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed;
if (biconditional.right.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed;
return operationResult;
}
template <class... Arguments>
static OperationResult visit(ast::Boolean &, Arguments &&...)
{
return OperationResult::Unchanged;
}
template <class... Arguments>
static OperationResult visit(ast::Comparison &, Arguments &&...)
{
return OperationResult::Unchanged;
}
template <class... Arguments>
static OperationResult visit(ast::Exists &exists, Arguments &&... arguments)
{
auto operationResult = OperationResult::Unchanged;
if (exists.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed;
for (auto &variableDeclaration : exists.variables)
if (Functor()(*variableDeclaration, exists.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed;
return operationResult;
}
template <class... Arguments>
static OperationResult visit(ast::ForAll &forAll, Arguments &&... arguments)
{
auto operationResult = OperationResult::Unchanged;
if (forAll.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed;
for (auto &variableDeclaration : forAll.variables)
if (Functor()(*variableDeclaration, forAll.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed;
return operationResult;
}
template <class... Arguments>
static OperationResult visit(ast::Implies &implies, Arguments &&... arguments)
{
auto operationResult = OperationResult::Unchanged;
if (implies.antecedent.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed;
if (implies.consequent.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed;
return operationResult;
}
template <class... Arguments>
static OperationResult visit(ast::In &, Arguments &&...)
{
return OperationResult::Unchanged;
}
template <class... Arguments>
static OperationResult visit(ast::Not &not_, Arguments &&... arguments)
{
return not_.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...);
}
template <class... Arguments>
static OperationResult visit(ast::Or &or_, Arguments &&... arguments)
{
auto operationResult = OperationResult::Unchanged;
for (auto &argument : or_.arguments)
if (argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed;
return operationResult;
}
template <class... Arguments>
static OperationResult visit(ast::Predicate &, Arguments &&...)
{
return OperationResult::Unchanged;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct CheckIfDefinitionFalseFunctor
{
OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
ast::Formula &, ast::Formula &definition, VariableDomainMap &variableDomainMap)
{
if (variableDeclaration.domain != Domain::Unknown)
return OperationResult::Unchanged;
clearVariableDomainMap(variableDomainMap);
// As a hypothesis, make the parameters domain noninteger
variableDomainMap[&variableDeclaration] = Domain::Noninteger;
const auto result = evaluate(definition, variableDomainMap);
if (result == EvaluationResult::Error || result == EvaluationResult::False)
{
// If making the variable noninteger leads to a false or erroneous result, its proven to be integer
variableDeclaration.domain = Domain::Integer;
return OperationResult::Changed;
}
return OperationResult::Unchanged;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct CheckIfQuantifiedFormulaFalseFunctor
{
OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
ast::Formula &quantifiedFormula, VariableDomainMap &variableDomainMap)
{
if (variableDeclaration.domain != Domain::Unknown)
return OperationResult::Unchanged;
clearVariableDomainMap(variableDomainMap);
// As a hypothesis, make the parameters domain noninteger
variableDomainMap[&variableDeclaration] = Domain::Noninteger;
const auto result = evaluate(quantifiedFormula, variableDomainMap);
if (result == EvaluationResult::Error || result == EvaluationResult::False)
{
// If making the variable noninteger leads to a false or erroneous result, its proven to be integer
variableDeclaration.domain = Domain::Integer;
return OperationResult::Changed;
}
return OperationResult::Unchanged;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct CheckIfCompletedFormulaTrueFunctor
{
OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
ast::Formula &, ast::Formula &completedFormula, VariableDomainMap &variableDomainMap)
{
if (variableDeclaration.domain != Domain::Unknown)
return OperationResult::Unchanged;
clearVariableDomainMap(variableDomainMap);
// As a hypothesis, make the parameters domain noninteger
variableDomainMap[&variableDeclaration] = Domain::Noninteger;
const auto result = evaluate(completedFormula, variableDomainMap);
if (result == EvaluationResult::Error || result == EvaluationResult::True)
{
// If making the variable noninteger leads to a false or erroneous result, its proven to be integer
variableDeclaration.domain = Domain::Integer;
return OperationResult::Changed;
}
return OperationResult::Unchanged;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
// Assumes the completed formulas to be in translated but not simplified form.
// That is, completed formulas are either variable-free or universally quantified
void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas)
{
VariableDomainMap variableDomainMap;
auto operationResult = OperationResult::Changed;
while (operationResult == OperationResult::Changed)
{
operationResult = OperationResult::Unchanged;
for (auto &completedFormula : completedFormulas)
{
if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfQuantifiedFormulaFalseFunctor>(), variableDomainMap) == OperationResult::Changed)
operationResult = OperationResult::Changed;
if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfCompletedFormulaTrueFunctor>(), completedFormula, variableDomainMap) == OperationResult::Changed)
operationResult = OperationResult::Changed;
if (!completedFormula.is<ast::ForAll>())
continue;
auto &forAll = completedFormula.get<ast::ForAll>();
if (!forAll.argument.is<ast::Biconditional>())
continue;
auto &biconditional = forAll.argument.get<ast::Biconditional>();
if (!biconditional.left.is<ast::Predicate>())
continue;
auto &predicate = biconditional.left.get<ast::Predicate>();
auto &definition = biconditional.right;
if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfDefinitionFalseFunctor>(), definition, variableDomainMap) == OperationResult::Changed)
operationResult = OperationResult::Changed;
assert(predicate.arguments.size() == predicate.declaration->arity());
for (size_t i = 0; i < predicate.arguments.size(); i++)
{
auto &variableArgument = predicate.arguments[i];
auto &parameter = predicate.declaration->parameters[i];
assert(variableArgument.is<ast::Variable>());
auto &variable = variableArgument.get<ast::Variable>();
parameter.domain = variable.declaration->domain;
}
}
}
}
////////////////////////////////////////////////////////////////////////////////////////////////////
}

View File

@ -4,9 +4,8 @@
#include <anthem/ASTCopy.h>
#include <anthem/Equality.h>
#include <anthem/SimplificationVisitors.h>
#include <anthem/Type.h>
#include <anthem/output/AST.h>
#include <anthem/SimplificationVisitors.h>
namespace anthem
{
@ -101,7 +100,7 @@ struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<Rep
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class SimplificationRule>
OperationResult simplify(ast::Formula &formula)
SimplificationResult simplify(ast::Formula &formula)
{
return SimplificationRule::apply(formula);
}
@ -109,10 +108,10 @@ OperationResult simplify(ast::Formula &formula)
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class FirstSimplificationRule, class SecondSimplificationRule, class... OtherSimplificationRules>
OperationResult simplify(ast::Formula &formula)
SimplificationResult simplify(ast::Formula &formula)
{
if (simplify<FirstSimplificationRule>(formula) == OperationResult::Changed)
return OperationResult::Changed;
if (simplify<FirstSimplificationRule>(formula) == SimplificationResult::Simplified)
return SimplificationResult::Simplified;
return simplify<SecondSimplificationRule, OtherSimplificationRules...>(formula);
}
@ -123,19 +122,19 @@ struct SimplificationRuleExistsWithoutQuantifiedVariables
{
static constexpr const auto Description = "exists () (F) === F";
static OperationResult apply(ast::Formula &formula)
static SimplificationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::Exists>())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
auto &exists = formula.get<ast::Exists>();
if (!exists.variables.empty())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
formula = std::move(exists.argument);
return OperationResult::Changed;
return SimplificationResult::Simplified;
}
};
@ -145,20 +144,20 @@ struct SimplificationRuleTrivialAssignmentInExists
{
static constexpr const auto Description = "exists X (X = Y) === #true";
static OperationResult apply(ast::Formula &formula)
static SimplificationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::Exists>())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
const auto &exists = formula.get<ast::Exists>();
if (!exists.argument.is<ast::Comparison>())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
const auto &comparison = exists.argument.get<ast::Comparison>();
if (comparison.operator_ != ast::Comparison::Operator::Equal)
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
const auto matchingAssignment = std::find_if(exists.variables.cbegin(), exists.variables.cend(),
[&](const auto &variableDeclaration)
@ -168,11 +167,11 @@ struct SimplificationRuleTrivialAssignmentInExists
});
if (matchingAssignment == exists.variables.cend())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
formula = ast::Formula::make<ast::Boolean>(true);
return OperationResult::Changed;
return SimplificationResult::Simplified;
}
};
@ -182,20 +181,20 @@ struct SimplificationRuleAssignmentInExists
{
static constexpr const auto Description = "exists X (X = t and F(X)) === exists () (F(t))";
static OperationResult apply(ast::Formula &formula)
static SimplificationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::Exists>())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
auto &exists = formula.get<ast::Exists>();
if (!exists.argument.is<ast::And>())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
auto &and_ = exists.argument.get<ast::And>();
auto &arguments = and_.arguments;
auto simplificationResult = OperationResult::Unchanged;
auto simplificationResult = SimplificationResult::Unchanged;
for (auto i = exists.variables.begin(); i != exists.variables.end();)
{
@ -226,7 +225,7 @@ struct SimplificationRuleAssignmentInExists
arguments.erase(j);
wasVariableReplaced = true;
simplificationResult = OperationResult::Changed;
simplificationResult = SimplificationResult::Simplified;
break;
}
@ -250,19 +249,19 @@ struct SimplificationRuleEmptyConjunction
{
static constexpr const auto Description = "[empty conjunction] === #true";
static OperationResult apply(ast::Formula &formula)
static SimplificationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::And>())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
auto &and_ = formula.get<ast::And>();
if (!and_.arguments.empty())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
formula = ast::Formula::make<ast::Boolean>(true);
return OperationResult::Changed;
return SimplificationResult::Simplified;
}
};
@ -272,19 +271,19 @@ struct SimplificationRuleOneElementConjunction
{
static constexpr const auto Description = "[conjunction of only F] === F";
static OperationResult apply(ast::Formula &formula)
static SimplificationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::And>())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
auto &and_ = formula.get<ast::And>();
if (and_.arguments.size() != 1)
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
formula = std::move(and_.arguments.front());
return OperationResult::Changed;
return SimplificationResult::Simplified;
}
};
@ -294,19 +293,19 @@ struct SimplificationRuleTrivialExists
{
static constexpr const auto Description = "exists ... ([#true/#false]) === [#true/#false]";
static OperationResult apply(ast::Formula &formula)
static SimplificationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::Exists>())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
auto &exists = formula.get<ast::Exists>();
if (!exists.argument.is<ast::Boolean>())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
formula = std::move(exists.argument);
return OperationResult::Changed;
return SimplificationResult::Simplified;
}
};
@ -316,21 +315,21 @@ struct SimplificationRuleInWithPrimitiveArguments
{
static constexpr const auto Description = "[primitive A] in [primitive B] === A = B";
static OperationResult apply(ast::Formula &formula)
static SimplificationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::In>())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
auto &in = formula.get<ast::In>();
assert(ast::isPrimitive(in.element));
if (!ast::isPrimitive(in.element) || !ast::isPrimitive(in.set))
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
return OperationResult::Changed;
return SimplificationResult::Simplified;
}
};
@ -340,10 +339,10 @@ struct SimplificationRuleSubsumptionInBiconditionals
{
static constexpr const auto Description = "(F <-> (F and G)) === (F -> G)";
static OperationResult apply(ast::Formula &formula)
static SimplificationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::Biconditional>())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
auto &biconditional = formula.get<ast::Biconditional>();
@ -354,7 +353,7 @@ struct SimplificationRuleSubsumptionInBiconditionals
const auto rightIsAnd = biconditional.right.is<ast::And>();
if (!(leftIsPredicate && rightIsAnd) && !(rightIsPredicate && leftIsAnd))
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
auto &predicateSide = (leftIsPredicate ? biconditional.left : biconditional.right);
auto &andSide = (leftIsPredicate ? biconditional.right : biconditional.left);
@ -364,17 +363,17 @@ struct SimplificationRuleSubsumptionInBiconditionals
std::find_if(and_.arguments.cbegin(), and_.arguments.cend(),
[&](const auto &argument)
{
return (ast::equal(predicateSide, argument) == Tristate::True);
return (ast::equal(predicateSide, argument) == ast::Tristate::True);
});
if (matchingPredicate == and_.arguments.cend())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
and_.arguments.erase(matchingPredicate);
formula = ast::Formula::make<ast::Implies>(std::move(predicateSide), std::move(andSide));
return OperationResult::Changed;
return SimplificationResult::Simplified;
}
};
@ -384,21 +383,21 @@ struct SimplificationRuleDoubleNegation
{
static constexpr const auto Description = "not not F === F";
static OperationResult apply(ast::Formula &formula)
static SimplificationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::Not>())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
auto &not_ = formula.get<ast::Not>();
if (!not_.argument.is<ast::Not>())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
auto &notNot = not_.argument.get<ast::Not>();
formula = std::move(notNot.argument);
return OperationResult::Changed;
return SimplificationResult::Simplified;
}
};
@ -408,15 +407,15 @@ struct SimplificationRuleDeMorganForConjunctions
{
static constexpr const auto Description = "(not (F and G)) === (not F or not G)";
static OperationResult apply(ast::Formula &formula)
static SimplificationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::Not>())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
auto &not_ = formula.get<ast::Not>();
if (!not_.argument.is<ast::And>())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
auto &and_ = not_.argument.get<ast::And>();
@ -425,7 +424,7 @@ struct SimplificationRuleDeMorganForConjunctions
formula = ast::Formula::make<ast::Or>(std::move(and_.arguments));
return OperationResult::Changed;
return SimplificationResult::Simplified;
}
};
@ -435,21 +434,21 @@ struct SimplificationRuleImplicationFromDisjunction
{
static constexpr const auto Description = "(not F or G) === (F -> G)";
static OperationResult apply(ast::Formula &formula)
static SimplificationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::Or>())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
auto &or_ = formula.get<ast::Or>();
if (or_.arguments.size() != 2)
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
const auto leftIsNot = or_.arguments[0].is<ast::Not>();
const auto rightIsNot = or_.arguments[1].is<ast::Not>();
if (leftIsNot == rightIsNot)
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
auto &negativeSide = leftIsNot ? or_.arguments[0] : or_.arguments[1];
auto &positiveSide = leftIsNot ? or_.arguments[1] : or_.arguments[0];
@ -461,7 +460,7 @@ struct SimplificationRuleImplicationFromDisjunction
formula = ast::Formula::make<ast::Implies>(std::move(negativeSideArgument), std::move(positiveSide));
return OperationResult::Changed;
return SimplificationResult::Simplified;
}
};
@ -471,15 +470,15 @@ struct SimplificationRuleNegatedComparison
{
static constexpr const auto Description = "(not F [comparison] G) === (F [negated comparison] G)";
static OperationResult apply(ast::Formula &formula)
static SimplificationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::Not>())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
auto &not_ = formula.get<ast::Not>();
if (!not_.argument.is<ast::Comparison>())
return OperationResult::Unchanged;
return SimplificationResult::Unchanged;
auto &comparison = not_.argument.get<ast::Comparison>();
@ -507,35 +506,7 @@ struct SimplificationRuleNegatedComparison
formula = std::move(comparison);
return OperationResult::Changed;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleIntegerSetInclusion
{
static constexpr const auto Description = "(F in G) === (F = G) if F and G are integer variables";
static OperationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::In>())
return OperationResult::Unchanged;
auto &in = formula.get<ast::In>();
const auto elementType = type(in.element);
const auto setType = type(in.set);
if (elementType.domain != Domain::Integer || setType.domain != Domain::Integer
|| elementType.setSize != SetSize::Unit || setType.setSize != SetSize::Unit)
{
return OperationResult::Unchanged;
}
formula = ast::Formula::make<ast::Comparison>(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
return OperationResult::Changed;
return SimplificationResult::Simplified;
}
};
@ -555,8 +526,7 @@ const auto simplifyWithDefaultRules =
SimplificationRuleSubsumptionInBiconditionals,
SimplificationRuleDeMorganForConjunctions,
SimplificationRuleImplicationFromDisjunction,
SimplificationRuleNegatedComparison,
SimplificationRuleIntegerSetInclusion
SimplificationRuleNegatedComparison
>;
////////////////////////////////////////////////////////////////////////////////////////////////////
@ -565,7 +535,7 @@ const auto simplifyWithDefaultRules =
struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<SimplifyFormulaVisitor>
{
// Do nothing for all other types of expressions
static OperationResult accept(ast::Formula &formula)
static SimplificationResult accept(ast::Formula &formula)
{
return simplifyWithDefaultRules(formula);
}
@ -575,7 +545,7 @@ struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<Simplif
void simplify(ast::Formula &formula)
{
while (formula.accept(SimplifyFormulaVisitor(), formula) == OperationResult::Changed);
while (formula.accept(SimplifyFormulaVisitor(), formula) == SimplificationResult::Simplified);
}
////////////////////////////////////////////////////////////////////////////////////////////////////

View File

@ -8,7 +8,6 @@
#include <anthem/Completion.h>
#include <anthem/Context.h>
#include <anthem/IntegerVariableDetection.h>
#include <anthem/Simplification.h>
#include <anthem/StatementVisitor.h>
#include <anthem/output/AST.h>
@ -68,10 +67,10 @@ void translate(const char *fileName, std::istream &stream, Context &context)
for (auto &scopedFormula : scopedFormulas)
simplify(scopedFormula.formula);
if (context.showStatementsUsed)
if (context.visiblePredicateSignatures)
context.logger.log(output::Priority::Warning) << "#show statements are ignored because completion is not enabled";
if (context.externalStatementsUsed)
if (context.externalPredicateSignatures)
context.logger.log(output::Priority::Warning) << "#external statements are ignored because completion is not enabled";
for (const auto &scopedFormula : scopedFormulas)
@ -86,33 +85,25 @@ void translate(const char *fileName, std::istream &stream, Context &context)
// Perform completion
auto completedFormulas = complete(std::move(scopedFormulas), context);
for (const auto &predicateDeclaration : context.predicateDeclarations)
{
if (predicateDeclaration->isUsed)
continue;
// 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";
// 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";
}
// Detect integer variables
if (context.performIntegerDetection)
detectIntegerVariables(completedFormulas);
// 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";
// Simplify output if specified
if (context.performSimplification)
@ -126,38 +117,6 @@ void translate(const char *fileName, std::istream &stream, Context &context)
ast::print(context.logger.outputStream(), completedFormula, printContext);
context.logger.outputStream() << std::endl;
}
// Print specifiers for integer predicate parameters
for (auto &predicateDeclaration : context.predicateDeclarations)
{
// Check that the predicate is used and not declared #external
if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal)
continue;
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, dont eliminate it
if (!isPredicateVisible)
continue;
for (size_t i = 0; i < predicateDeclaration->parameters.size(); i++)
{
auto &parameter = predicateDeclaration->parameters[i];
if (parameter.domain != Domain::Integer)
continue;
context.logger.outputStream()
<< output::Keyword("int")
<< "(" << predicateDeclaration->name
<< "/" << output::Number(predicateDeclaration->arity())
<< "@" << output::Number(i + 1)
<< ")" << std::endl;
}
}
}
////////////////////////////////////////////////////////////////////////////////////////////////////

View File

@ -123,7 +123,7 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall V1 (f(V1) <-> (exists U1 (V1 = f(f(f(f(U1)))) and f(U1)) or V1 in (1..5)))\n");
"forall V1 (f(V1) <-> (exists U1 (V1 = f(f(f(f(U1)))) and f(U1)) or V1 in 1..5))\n");
}
SECTION("useless implications")
@ -152,8 +152,8 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
CHECK(output.str() ==
"forall V1 (covered(V1) <-> exists U1 in(V1, U1))\n"
"forall V2, V3 (in(V2, V3) -> (V2 in (1..n) and V3 in (1..r)))\n"
"forall U2 (U2 in (1..n) -> covered(U2))\n"
"forall V2, V3 (in(V2, V3) -> (V2 in 1..n and V3 in 1..r))\n"
"forall U2 (U2 in 1..n -> covered(U2))\n"
"forall U3, U4, U5 (not in(U3, U4) or not in(U5, U4) or not exists X1 (X1 in (U3 + U5) and in(X1, U4)))\n");
}
@ -190,6 +190,6 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
input << "adj(X, Y) :- X = 1..n, Y = 1..n, |X - Y| = 1.";
anthem::translate("input", input, context);
CHECK(output.str() == "forall V1, V2 (adj(V1, V2) <-> (V1 in (1..n) and V2 in (1..n) and |V1 - V2| = 1))\n");
CHECK(output.str() == "forall V1, V2 (adj(V1, V2) <-> (V1 in 1..n and V2 in 1..n and |V1 - V2| = 1))\n");
}
}

View File

@ -150,7 +150,7 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
// TODO: simplify further
CHECK(output.str() ==
"forall V1 (a(V1) <-> exists U1 (c(V1) = c(U1) and U1 in (1..4)))\n");
"forall V1 (a(V1) <-> exists U1 (c(V1) = c(U1) and U1 in 1..4))\n");
}
SECTION("simple propositions are hidden correctly")

View File

@ -1,117 +0,0 @@
#include <catch.hpp>
#include <sstream>
#include <anthem/AST.h>
#include <anthem/Context.h>
#include <anthem/Translation.h>
////////////////////////////////////////////////////////////////////////////////////////////////////
TEST_CASE("[integer detection] Integer variables are correctly detected", "[integer detection]")
{
std::stringstream input;
std::stringstream output;
std::stringstream errors;
anthem::output::Logger logger(output, errors);
anthem::Context context(std::move(logger));
context.performSimplification = true;
context.performCompletion = true;
context.performIntegerDetection = true;
SECTION("simple-to-detect integer parameter")
{
input << "p(X) :- X = 1..5.";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall N1 (p(N1) <-> N1 in (1..5))\n"
"int(p/1@1)\n");
}
SECTION("simple noninteger parameter")
{
input <<
"p(X) :- X = 1..5.\n"
"p(X) :- X = error.";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall V1 (p(V1) <-> (V1 in (1..5) or V1 = error))\n");
}
SECTION("integer parameter with arithmetics")
{
input << "p(X) :- X = (2 + (1..5)) * 2.";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall N1 (p(N1) <-> N1 in ((2 + (1..5)) * 2))\n"
"int(p/1@1)\n");
}
SECTION("integer parameter with arithmetics depending on another integer parameter")
{
input
<< "p(X) :- X = 1..5."
<< "q(X) :- p(Y), X = (Y + 5) / 3.";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall N1 (p(N1) <-> N1 in (1..5))\n"
"forall N2 (q(N2) <-> exists N3 (p(N3) and N2 in ((N3 + 5) / 3)))\n"
"int(p/1@1)\n"
"int(q/1@1)\n");
}
SECTION("multiple mixed parameters")
{
input
<< "p(X) :- X = 1..5."
<< "q(X) :- X = error."
<< "r(A, B, C) :- p(X), A = X ** 2, q(B), p(C).";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall N1 (p(N1) <-> N1 in (1..5))\n"
"forall V1 (q(V1) <-> V1 = error)\n"
"forall N2, V2, N3 (r(N2, V2, N3) <-> exists N4 (p(N4) and N2 = (N4 ** 2) and q(V2) and p(N3)))\n"
"int(p/1@1)\n"
"int(r/3@1)\n"
"int(r/3@3)\n");
}
SECTION("integer parameter despite usage of constant symbol")
{
input
<< "p(X) :- X = 2..n.";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall N1 (p(N1) <-> N1 in (2..n))\n"
"int(p/1@1)\n");
}
SECTION("integer arithmetics are correctly simplified for operators other than division")
{
input
<< "p(X) :- X = 5 + 9 ** 2.";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall N1 (p(N1) <-> N1 = (5 + (9 ** 2)))\n"
"int(p/1@1)\n");
}
SECTION("integer arithmetics are not simplified with the division operator")
{
input
<< "p(X) :- X = 5 + 9 / 0.";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall N1 (p(N1) <-> N1 in (5 + (9 / 0)))\n"
"int(p/1@1)\n");
}
}

View File

@ -40,7 +40,7 @@ TEST_CASE("[simplification] Rules are simplified correctly", "[simplification]")
input << ":- not covered(I), I = 1..n.";
anthem::translate("input", input, context);
CHECK(output.str() == "((not covered(U1) and U1 in (1..n)) -> #false)\n");
CHECK(output.str() == "((not covered(U1) and U1 in 1..n) -> #false)\n");
}
SECTION("comparisons")
@ -50,34 +50,4 @@ TEST_CASE("[simplification] Rules are simplified correctly", "[simplification]")
CHECK(output.str() == "(U1 > U2 -> #false)\n");
}
SECTION("biconditionals are replaced with implifactions with choice rules")
{
context.performCompletion = true;
input << "{p(a)}.";
anthem::translate("input", input, context);
CHECK(output.str() == "forall V1 (p(V1) -> V1 = a)\n");
}
SECTION("biconditionals are replaced with implifactions with complicated choice rules")
{
context.performCompletion = true;
input << "{p(n + 5)}.";
anthem::translate("input", input, context);
CHECK(output.str() == "forall V1 (p(V1) -> V1 in (n + 5))\n");
}
SECTION("biconditionals are not replaced with implifactions with nonchoice rules")
{
context.performCompletion = true;
input << "p(a).";
anthem::translate("input", input, context);
CHECK(output.str() == "forall V1 (p(V1) <-> V1 = a)\n");
}
}

View File

@ -24,7 +24,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
input << "p(1..5).";
anthem::translate("input", input, context);
CHECK(output.str() == "(V1 in (1..5) -> p(V1))\n");
CHECK(output.str() == "(V1 in 1..5 -> p(V1))\n");
}
SECTION("simple example 2")
@ -32,7 +32,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
input << "p(N) :- N = 1..5.";
anthem::translate("input", input, context);
CHECK(output.str() == "((V1 in U1 and exists X1, X2 (X1 in U1 and X2 in (1..5) and X1 = X2)) -> p(V1))\n");
CHECK(output.str() == "((V1 in U1 and exists X1, X2 (X1 in U1 and X2 in 1..5 and X1 = X2)) -> p(V1))\n");
}
SECTION("simple example 3")
@ -48,7 +48,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
input << "p(N, 1, 2) :- N = 1..5.";
anthem::translate("input", input, context);
CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and exists X1, X2 (X1 in U1 and X2 in (1..5) and X1 = X2)) -> p(V1, V2, V3))\n");
CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and exists X1, X2 (X1 in U1 and X2 in 1..5 and X1 = X2)) -> p(V1, V2, V3))\n");
}
SECTION("disjunctive head")
@ -57,7 +57,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
input << "q(3, N); p(N, 1, 2) :- N = 1..5.";
anthem::translate("input", input, context);
CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and V4 in 3 and V5 in U1 and exists X1, X2 (X1 in U1 and X2 in (1..5) and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n");
CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and V4 in 3 and V5 in U1 and exists X1, X2 (X1 in U1 and X2 in 1..5 and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n");
}
SECTION("disjunctive head (alternative syntax)")
@ -66,7 +66,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
input << "q(3, N), p(N, 1, 2) :- N = 1..5.";
anthem::translate("input", input, context);
CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and V4 in 3 and V5 in U1 and exists X1, X2 (X1 in U1 and X2 in (1..5) and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n");
CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and V4 in 3 and V5 in U1 and exists X1, X2 (X1 in U1 and X2 in 1..5 and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n");
}
SECTION("escaping conflicting variable names")
@ -98,7 +98,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
input << ":- not p(I), I = 1..n.";
anthem::translate("input", input, context);
CHECK(output.str() == "((exists X1 (X1 in U1 and not p(X1)) and exists X2, X3 (X2 in U1 and X3 in (1..n) and X2 = X3)) -> #false)\n");
CHECK(output.str() == "((exists X1 (X1 in U1 and not p(X1)) and exists X2, X3 (X2 in U1 and X3 in 1..n and X2 = X3)) -> #false)\n");
}
SECTION("disjunctive fact (no arguments)")
@ -178,7 +178,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
input << "p(X, 1..10) :- q(X, 6..12).";
anthem::translate("input", input, context);
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")
@ -186,7 +186,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
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");
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")
@ -194,7 +194,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
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");
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")
@ -262,7 +262,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
anthem::translate("input", input, context);
// TODO: eliminate V5: not needed
CHECK(output.str() == "((V1 in (1..3) and V2 in U1 and V3 in (2..4) and p(V1, V2)) -> p(V1, V2))\n((V4 in (1..3) and V5 in U2 and V6 in (2..4) and q(V6)) -> q(V6))\n");
CHECK(output.str() == "((V1 in 1..3 and V2 in U1 and V3 in 2..4 and p(V1, V2)) -> p(V1, V2))\n((V4 in 1..3 and V5 in U2 and V6 in 2..4 and q(V6)) -> q(V6))\n");
}
SECTION("choice rule with body")
@ -302,6 +302,6 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
input << "p(N, N ** N) :- N = 1..n.";
anthem::translate("input", input, context);
CHECK(output.str() == "((V1 in U1 and V2 in (U1 ** U1) and exists X1, X2 (X1 in U1 and X2 in (1..n) and X1 = X2)) -> p(V1, V2))\n");
CHECK(output.str() == "((V1 in U1 and V2 in (U1 ** U1) and exists X1, X2 (X1 in U1 and X2 in 1..n and X1 = X2)) -> p(V1, V2))\n");
}
}

View File

@ -1,73 +0,0 @@
#include <catch.hpp>
#include <sstream>
#include <anthem/AST.h>
#include <anthem/Context.h>
#include <anthem/Translation.h>
////////////////////////////////////////////////////////////////////////////////////////////////////
TEST_CASE("[unsupported] Errors are correctly issued when using unsupported features", "[unsupported]")
{
std::stringstream input;
std::stringstream output;
std::stringstream errors;
anthem::output::Logger logger(output, errors);
anthem::Context context(std::move(logger));
SECTION("rules with disjunctive head are unsupported")
{
context.performCompletion = true;
input << "a; b.";
CHECK_THROWS(anthem::translate("input", input, context));
}
SECTION("rules with disjunctive head containing elements with arguments are unsupported")
{
context.performCompletion = true;
input << "p(a); p(b).";
CHECK_THROWS(anthem::translate("input", input, context));
}
SECTION("singleton choice rules are supported")
{
context.performCompletion = true;
input << "{a}.";
CHECK_NOTHROW(anthem::translate("input", input, context));
}
SECTION("singleton choice rules containing an element with arguments are supported")
{
context.performCompletion = true;
input << "{p(a)}.";
CHECK_NOTHROW(anthem::translate("input", input, context));
}
SECTION("choice rules with multiple simple elements are supported")
{
context.performCompletion = true;
input << "{a; b}.";
CHECK_NOTHROW(anthem::translate("input", input, context));
}
SECTION("choice rules with multiple elements with arguments are unsupported")
{
context.performCompletion = true;
input << "{p(a); p(b)}.";
CHECK_THROWS(anthem::translate("input", input, context));
}
}