Compare commits
1 Commits
develop
...
v0.1.8-rc.
| Author | SHA1 | Date |
|---|---|---|
 Patrick Lühne
|
ec88d26922
|
22
CHANGELOG.md
22
CHANGELOG.md
|
|
@ -1,26 +1,6 @@
|
|||
# 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)
|
||||
## 0.1.8 RC 3 (2018-04-12)
|
||||
|
||||
### Features
|
||||
|
||||
|
|
|
|||
|
|
@ -9,12 +9,11 @@
|
|||
## Usage
|
||||
|
||||
```bash
|
||||
$ anthem [--no-complete] [--no-simplify] [--no-detect-integers] file...
|
||||
$ anthem [--complete] [--simplify] file...
|
||||
```
|
||||
|
||||
By default, `anthem` performs Clark’s 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 Clark’s completion on the translated formulas.
|
||||
With the option `--simplify`, the output formulas are simplified by applying several basic transformation rules.
|
||||
|
||||
## Building
|
||||
|
||||
|
|
|
|||
12
app/main.cpp
12
app/main.cpp
|
|
@ -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-rc.3" << std::endl;
|
||||
return EXIT_SUCCESS;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -1,2 +0,0 @@
|
|||
p(a).
|
||||
{q(a)}.
|
||||
|
|
@ -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 don’t 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.
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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).
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
s(X) :- p(X).
|
||||
s(X) :- q(X).
|
||||
|
||||
#external p(1).
|
||||
#external q(1).
|
||||
|
|
@ -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 don’t 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;
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
{
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
};
|
||||
|
|
|
|||
|
|
@ -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())
|
||||
|
|
|
|||
|
|
@ -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 isn’t, 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 shouldn’t 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 isn’t, set inclusion is never satisfied
|
||||
return EvaluationResult::False;
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
static EvaluationResult visit(const ast::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 ¶meter = 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
|
||||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -12,6 +12,14 @@ namespace anthem
|
|||
//
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
enum class SimplificationResult
|
||||
{
|
||||
Simplified,
|
||||
Unchanged,
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
void simplify(ast::Formula &formula);
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -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 ¬_, Formula &formula, Arguments &&... arguments)
|
||||
SimplificationResult visit(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)...);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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>
|
||||
|
|
|
|||
|
|
@ -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");
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -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};
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
|
|||
|
|
@ -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:
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
Subproject commit ca6e9f70eb6b5fab44504daf57d92a9412ab301c
|
||||
Subproject commit abe9ebd6b4084d576ceb79904c94ef8c9c0e6c56
|
||||
|
|
@ -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)
|
||||
{
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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 predicate’s 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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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 ¬_)
|
||||
PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::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, don’t 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;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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 ¬_, 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 parameter’s 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, it’s 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 parameter’s 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, it’s 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 parameter’s 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, it’s 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 ¶meter = predicate.declaration->parameters[i];
|
||||
|
||||
assert(variableArgument.is<ast::Variable>());
|
||||
|
||||
auto &variable = variableArgument.get<ast::Variable>();
|
||||
|
||||
parameter.domain = variable.declaration->domain;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
}
|
||||
|
|
@ -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 ¬_ = formula.get<ast::Not>();
|
||||
|
||||
if (!not_.argument.is<ast::Not>())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
auto ¬Not = 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 ¬_ = 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 ¬_ = 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);
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -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, don’t eliminate it
|
||||
if (!isPredicateVisible)
|
||||
continue;
|
||||
|
||||
for (size_t i = 0; i < predicateDeclaration->parameters.size(); i++)
|
||||
{
|
||||
auto ¶meter = 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;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -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");
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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")
|
||||
|
|
|
|||
|
|
@ -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");
|
||||
}
|
||||
}
|
||||
|
|
@ -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");
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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");
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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));
|
||||
}
|
||||
}
|
||||
Loading…
Reference in New Issue