Compare commits
32 Commits
v0.1.9-rc.
...
develop
Author | SHA1 | Date | |
---|---|---|---|
e0aa3497ee | |||
64bab69a36 | |||
9566629237 | |||
c199f609bd | |||
1570432ee0 | |||
0ce4e54d1a | |||
fa3ed31eca | |||
e85807accb | |||
3393f84a4a | |||
7013b9ea54 | |||
c84ae51ff2 | |||
d60e2a736b | |||
bb9013e7c5 | |||
69688d1d39 | |||
a70b1fb726 | |||
a2c4d87852 | |||
b60c65a810 | |||
19e1e16e45 | |||
63f39e5162 | |||
811523e580 | |||
09ef64a0e1 | |||
43d2c153c7 | |||
541cb3fb47 | |||
921d5ed4f0 | |||
e0509f725a | |||
48cf8ee3e0 | |||
f7d99c82fa | |||
618189368c | |||
d0debc6ad1 | |||
3ba80e8c9d | |||
d66d3557c1 | |||
e15a6b2e88 |
18
CHANGELOG.md
18
CHANGELOG.md
@ -2,6 +2,24 @@
|
|||||||
|
|
||||||
## (unreleased)
|
## (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 (2018-04-20)
|
||||||
|
|
||||||
### Features
|
### Features
|
||||||
|
@ -9,11 +9,12 @@
|
|||||||
## Usage
|
## Usage
|
||||||
|
|
||||||
```bash
|
```bash
|
||||||
$ anthem [--complete] [--simplify] file...
|
$ anthem [--no-complete] [--no-simplify] [--no-detect-integers] file...
|
||||||
```
|
```
|
||||||
|
|
||||||
`--complete` instructs `anthem` to perform Clark’s completion on the translated formulas.
|
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.
|
||||||
With the option `--simplify`, the output formulas are simplified by applying several basic transformation rules.
|
|
||||||
|
These processing steps can be turned off with the options `--no-complete`, `--no-simplify`, and `--no-detect-integers`.
|
||||||
|
|
||||||
## Building
|
## Building
|
||||||
|
|
||||||
|
12
app/main.cpp
12
app/main.cpp
@ -16,8 +16,9 @@ int main(int argc, char **argv)
|
|||||||
("h,help", "Display this help message")
|
("h,help", "Display this help message")
|
||||||
("v,version", "Display version information")
|
("v,version", "Display version information")
|
||||||
("i,input", "Input files", cxxopts::value<std::vector<std::string>>())
|
("i,input", "Input files", cxxopts::value<std::vector<std::string>>())
|
||||||
("s,simplify", "Simplify the output")
|
("no-simplify", "Do not simplify the output")
|
||||||
("c,complete", "Perform completion")
|
("no-complete", "Do not perform completion")
|
||||||
|
("no-detect-integers", "Do not detect integer variables")
|
||||||
("color", "Colorize output (always, never, auto)", cxxopts::value<std::string>()->default_value("auto"))
|
("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"))
|
("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"));
|
("p,log-priority", "Log messages starting from this priority (debug, info, warning, error)", cxxopts::value<std::string>()->default_value("info"));
|
||||||
@ -48,8 +49,9 @@ int main(int argc, char **argv)
|
|||||||
if (parseResult.count("input") > 0)
|
if (parseResult.count("input") > 0)
|
||||||
inputFiles = parseResult["input"].as<std::vector<std::string>>();
|
inputFiles = parseResult["input"].as<std::vector<std::string>>();
|
||||||
|
|
||||||
context.performSimplification = (parseResult.count("simplify") > 0);
|
context.performSimplification = (parseResult.count("no-simplify") == 0);
|
||||||
context.performCompletion = (parseResult.count("complete") > 0);
|
context.performCompletion = (parseResult.count("no-complete") == 0);
|
||||||
|
context.performIntegerDetection = (parseResult.count("no-detect-integers") == 0);
|
||||||
colorPolicyString = parseResult["color"].as<std::string>();
|
colorPolicyString = parseResult["color"].as<std::string>();
|
||||||
parenthesisStyleString = parseResult["parentheses"].as<std::string>();
|
parenthesisStyleString = parseResult["parentheses"].as<std::string>();
|
||||||
logPriorityString = parseResult["log-priority"].as<std::string>();
|
logPriorityString = parseResult["log-priority"].as<std::string>();
|
||||||
@ -70,7 +72,7 @@ int main(int argc, char **argv)
|
|||||||
|
|
||||||
if (version)
|
if (version)
|
||||||
{
|
{
|
||||||
std::cout << "anthem version 0.1.8+git" << std::endl;
|
std::cout << "anthem version 0.1.9+git" << std::endl;
|
||||||
return EXIT_SUCCESS;
|
return EXIT_SUCCESS;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
2
examples/choice-rules.lp
Normal file
2
examples/choice-rules.lp
Normal file
@ -0,0 +1,2 @@
|
|||||||
|
p(a).
|
||||||
|
{q(a)}.
|
@ -1,10 +1,18 @@
|
|||||||
#external color(1).
|
% assign a set of colors to each vertex
|
||||||
#external edge(2).
|
|
||||||
#external vertex(1).
|
|
||||||
#show color/2.
|
|
||||||
|
|
||||||
{color(V, C)} :- vertex(V), color(C).
|
{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, _).
|
covered(V) :- color(V, _).
|
||||||
:- vertex(V), not covered(V).
|
:- vertex(V), not covered(V).
|
||||||
|
|
||||||
|
% adjacent vertices don’t share the same color
|
||||||
:- color(V1, C), color(V2, C), edge(V1, V2).
|
:- color(V1, C), color(V2, C), edge(V1, V2).
|
||||||
:- color(V, C1), color(V, C2), C1 != C2.
|
|
||||||
|
#show color/2.
|
||||||
|
|
||||||
|
#external vertex(1).
|
||||||
|
#external edge(2).
|
||||||
|
#external color(1).
|
||||||
|
11
examples/letters.lp
Normal file
11
examples/letters.lp
Normal file
@ -0,0 +1,11 @@
|
|||||||
|
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,3 +1,5 @@
|
|||||||
|
#show p/2.
|
||||||
|
|
||||||
{p(1..n, 1..n)}.
|
{p(1..n, 1..n)}.
|
||||||
|
|
||||||
:- p(X, Y1), p(X, Y2), Y1 != Y2.
|
:- p(X, Y1), p(X, Y2), Y1 != Y2.
|
||||||
@ -8,5 +10,3 @@ q2(Y) :- p(_, Y).
|
|||||||
|
|
||||||
:- not q1(X), X = 1..n.
|
:- not q1(X), X = 1..n.
|
||||||
:- not q2(Y), Y = 1..n.
|
:- not q2(Y), Y = 1..n.
|
||||||
|
|
||||||
#show p/2.
|
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
|
#show in/2.
|
||||||
|
|
||||||
{in(1..n, 1..r)}.
|
{in(1..n, 1..r)}.
|
||||||
covered(I) :- in(I, S).
|
covered(I) :- in(I, S).
|
||||||
|
|
||||||
:- I = 1..n, not covered(I).
|
:- I = 1..n, not covered(I).
|
||||||
:- in(I, S), in(J, S), in(I + J, S).
|
:- in(I, S), in(J, S), in(I + J, S).
|
||||||
|
|
||||||
#show in/2.
|
|
||||||
|
9
examples/simple-external-show.lp
Normal file
9
examples/simple-external-show.lp
Normal file
@ -0,0 +1,9 @@
|
|||||||
|
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).
|
5
examples/simple-external.lp
Normal file
5
examples/simple-external.lp
Normal file
@ -0,0 +1,5 @@
|
|||||||
|
s(X) :- p(X).
|
||||||
|
s(X) :- q(X).
|
||||||
|
|
||||||
|
#external p(1).
|
||||||
|
#external q(1).
|
@ -2,6 +2,7 @@
|
|||||||
#define __ANTHEM__AST_H
|
#define __ANTHEM__AST_H
|
||||||
|
|
||||||
#include <anthem/ASTForward.h>
|
#include <anthem/ASTForward.h>
|
||||||
|
#include <anthem/Utils.h>
|
||||||
|
|
||||||
namespace anthem
|
namespace anthem
|
||||||
{
|
{
|
||||||
@ -103,32 +104,15 @@ struct Comparison
|
|||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
struct Constant
|
|
||||||
{
|
|
||||||
explicit Constant(std::string &&name)
|
|
||||||
: name{std::move(name)}
|
|
||||||
{
|
|
||||||
}
|
|
||||||
|
|
||||||
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
|
struct Function
|
||||||
{
|
{
|
||||||
explicit Function(std::string &&name)
|
explicit Function(FunctionDeclaration *declaration)
|
||||||
: name{std::move(name)}
|
: declaration{declaration}
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
explicit Function(std::string &&name, std::vector<Term> &&arguments)
|
explicit Function(FunctionDeclaration *declaration, std::vector<Term> &&arguments)
|
||||||
: name{std::move(name)},
|
: declaration{declaration},
|
||||||
arguments{std::move(arguments)}
|
arguments{std::move(arguments)}
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
@ -138,12 +122,37 @@ struct Function
|
|||||||
Function(Function &&other) noexcept = default;
|
Function(Function &&other) noexcept = default;
|
||||||
Function &operator=(Function &&other) noexcept = default;
|
Function &operator=(Function &&other) noexcept = default;
|
||||||
|
|
||||||
std::string name;
|
FunctionDeclaration *declaration;
|
||||||
std::vector<Term> arguments;
|
std::vector<Term> arguments;
|
||||||
};
|
};
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
struct FunctionDeclaration
|
||||||
|
{
|
||||||
|
explicit FunctionDeclaration(std::string &&name)
|
||||||
|
: name{std::move(name)}
|
||||||
|
{
|
||||||
|
}
|
||||||
|
|
||||||
|
explicit FunctionDeclaration(std::string &&name, size_t arity)
|
||||||
|
: name{std::move(name)},
|
||||||
|
arity{arity}
|
||||||
|
{
|
||||||
|
}
|
||||||
|
|
||||||
|
FunctionDeclaration(const FunctionDeclaration &other) = delete;
|
||||||
|
FunctionDeclaration &operator=(const FunctionDeclaration &other) = delete;
|
||||||
|
FunctionDeclaration(FunctionDeclaration &&other) noexcept = default;
|
||||||
|
FunctionDeclaration &operator=(FunctionDeclaration &&other) noexcept = default;
|
||||||
|
|
||||||
|
std::string name;
|
||||||
|
size_t arity;
|
||||||
|
Domain domain{Domain::Noninteger};
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
// TODO: refactor (limit element type to primitive terms)
|
// TODO: refactor (limit element type to primitive terms)
|
||||||
struct In
|
struct In
|
||||||
{
|
{
|
||||||
@ -204,13 +213,13 @@ struct Interval
|
|||||||
|
|
||||||
struct Predicate
|
struct Predicate
|
||||||
{
|
{
|
||||||
explicit Predicate(std::string &&name)
|
explicit Predicate(PredicateDeclaration *declaration)
|
||||||
: name{std::move(name)}
|
: declaration{declaration}
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
explicit Predicate(std::string &&name, std::vector<Term> &&arguments)
|
explicit Predicate(PredicateDeclaration *declaration, std::vector<Term> &&arguments)
|
||||||
: name{std::move(name)},
|
: declaration{declaration},
|
||||||
arguments{std::move(arguments)}
|
arguments{std::move(arguments)}
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
@ -220,35 +229,47 @@ struct Predicate
|
|||||||
Predicate(Predicate &&other) noexcept = default;
|
Predicate(Predicate &&other) noexcept = default;
|
||||||
Predicate &operator=(Predicate &&other) noexcept = default;
|
Predicate &operator=(Predicate &&other) noexcept = default;
|
||||||
|
|
||||||
std::size_t arity() const
|
PredicateDeclaration *declaration{nullptr};
|
||||||
{
|
|
||||||
return arguments.size();
|
|
||||||
}
|
|
||||||
|
|
||||||
std::string name;
|
|
||||||
std::vector<Term> arguments;
|
std::vector<Term> arguments;
|
||||||
};
|
};
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
// TODO: make more use of this class
|
struct PredicateDeclaration
|
||||||
struct PredicateSignature
|
|
||||||
{
|
{
|
||||||
explicit PredicateSignature(std::string &&name, size_t arity)
|
enum class Visibility
|
||||||
|
{
|
||||||
|
Default,
|
||||||
|
Visible,
|
||||||
|
Hidden
|
||||||
|
};
|
||||||
|
|
||||||
|
struct Parameter
|
||||||
|
{
|
||||||
|
Domain domain{Domain::Unknown};
|
||||||
|
};
|
||||||
|
|
||||||
|
explicit PredicateDeclaration(std::string &&name, size_t arity)
|
||||||
: name{std::move(name)},
|
: name{std::move(name)},
|
||||||
arity{arity}
|
parameters{std::vector<Parameter>(arity)}
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
PredicateSignature(const PredicateSignature &other) = delete;
|
PredicateDeclaration(const PredicateDeclaration &other) = delete;
|
||||||
PredicateSignature &operator=(const PredicateSignature &other) = delete;
|
PredicateDeclaration &operator=(const PredicateDeclaration &other) = delete;
|
||||||
// TODO: make noexcept again
|
PredicateDeclaration(PredicateDeclaration &&other) noexcept = default;
|
||||||
// GCC versions before 7 don’t declare moving std::string noexcept and would complain here
|
PredicateDeclaration &operator=(PredicateDeclaration &&other) noexcept = default;
|
||||||
PredicateSignature(PredicateSignature &&other) = default;
|
|
||||||
PredicateSignature &operator=(PredicateSignature &&other) = default;
|
size_t arity() const noexcept
|
||||||
|
{
|
||||||
|
return parameters.size();
|
||||||
|
}
|
||||||
|
|
||||||
std::string name;
|
std::string name;
|
||||||
size_t arity;
|
std::vector<Parameter> parameters;
|
||||||
|
bool isUsed{false};
|
||||||
|
bool isExternal{false};
|
||||||
|
Visibility visibility{Visibility::Default};
|
||||||
};
|
};
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
@ -360,6 +381,7 @@ struct VariableDeclaration
|
|||||||
VariableDeclaration &operator=(VariableDeclaration &&other) = default;
|
VariableDeclaration &operator=(VariableDeclaration &&other) = default;
|
||||||
|
|
||||||
Type type;
|
Type type;
|
||||||
|
Domain domain{Domain::Unknown};
|
||||||
std::string name;
|
std::string name;
|
||||||
};
|
};
|
||||||
|
|
||||||
|
@ -22,7 +22,6 @@ namespace ast
|
|||||||
BinaryOperation prepareCopy(const BinaryOperation &other);
|
BinaryOperation prepareCopy(const BinaryOperation &other);
|
||||||
Boolean prepareCopy(const Boolean &other);
|
Boolean prepareCopy(const Boolean &other);
|
||||||
Comparison prepareCopy(const Comparison &other);
|
Comparison prepareCopy(const Comparison &other);
|
||||||
Constant prepareCopy(const Constant &other);
|
|
||||||
Function prepareCopy(const Function &other);
|
Function prepareCopy(const Function &other);
|
||||||
In prepareCopy(const In &other);
|
In prepareCopy(const In &other);
|
||||||
Integer prepareCopy(const Integer &other);
|
Integer prepareCopy(const Integer &other);
|
||||||
|
@ -24,10 +24,10 @@ struct BinaryOperation;
|
|||||||
struct Biconditional;
|
struct Biconditional;
|
||||||
struct Boolean;
|
struct Boolean;
|
||||||
struct Comparison;
|
struct Comparison;
|
||||||
struct Constant;
|
|
||||||
struct Exists;
|
struct Exists;
|
||||||
struct ForAll;
|
struct ForAll;
|
||||||
struct Function;
|
struct Function;
|
||||||
|
struct FunctionDeclaration;
|
||||||
struct Implies;
|
struct Implies;
|
||||||
struct In;
|
struct In;
|
||||||
struct Integer;
|
struct Integer;
|
||||||
@ -35,6 +35,7 @@ struct Interval;
|
|||||||
struct Not;
|
struct Not;
|
||||||
struct Or;
|
struct Or;
|
||||||
struct Predicate;
|
struct Predicate;
|
||||||
|
struct PredicateDeclaration;
|
||||||
struct SpecialInteger;
|
struct SpecialInteger;
|
||||||
struct String;
|
struct String;
|
||||||
struct UnaryOperation;
|
struct UnaryOperation;
|
||||||
@ -63,7 +64,6 @@ using Formula = Clingo::Variant<
|
|||||||
using Term = Clingo::Variant<
|
using Term = Clingo::Variant<
|
||||||
BinaryOperation,
|
BinaryOperation,
|
||||||
Boolean,
|
Boolean,
|
||||||
Constant,
|
|
||||||
Function,
|
Function,
|
||||||
Integer,
|
Integer,
|
||||||
Interval,
|
Interval,
|
||||||
|
@ -36,12 +36,6 @@ class VariableStack
|
|||||||
std::vector<Layer> m_layers;
|
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
|
// Replacing Variables
|
||||||
@ -96,6 +90,21 @@ struct ReplaceVariableInFormulaVisitor : public RecursiveFormulaVisitor<ReplaceV
|
|||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
// Accessing Variable Domains
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
struct DefaultVariableDomainAccessor
|
||||||
|
{
|
||||||
|
Domain operator()(const ast::Variable &variable)
|
||||||
|
{
|
||||||
|
return variable.declaration->domain;
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
#endif
|
#endif
|
||||||
|
@ -123,12 +123,6 @@ struct RecursiveTermVisitor
|
|||||||
return T::accept(boolean, term, std::forward<Arguments>(arguments)...);
|
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>
|
template <class... Arguments>
|
||||||
ReturnType visit(Function &function, Term &term, Arguments &&... arguments)
|
ReturnType visit(Function &function, Term &term, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
|
@ -43,19 +43,22 @@ ast::Comparison::Operator translate(Clingo::AST::ComparisonOperator comparisonOp
|
|||||||
struct BodyTermTranslateVisitor
|
struct BodyTermTranslateVisitor
|
||||||
{
|
{
|
||||||
// TODO: refactor
|
// TODO: refactor
|
||||||
std::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Literal &literal, const Clingo::AST::Term &, RuleContext &ruleContext, ast::VariableStack &variableStack)
|
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)
|
||||||
{
|
{
|
||||||
if (literal.sign == Clingo::AST::Sign::DoubleNegation)
|
if (literal.sign == Clingo::AST::Sign::DoubleNegation)
|
||||||
throw TranslationException(literal.location, "double-negated literals currently unsupported");
|
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())
|
if (function.arguments.empty())
|
||||||
{
|
{
|
||||||
auto predicate = ast::Formula::make<ast::Predicate>(std::string(function.name));
|
|
||||||
|
|
||||||
if (literal.sign == Clingo::AST::Sign::None)
|
if (literal.sign == Clingo::AST::Sign::None)
|
||||||
return std::move(predicate);
|
return ast::Predicate(predicateDeclaration);
|
||||||
else if (literal.sign == Clingo::AST::Sign::Negation)
|
else if (literal.sign == Clingo::AST::Sign::Negation)
|
||||||
return ast::Formula::make<ast::Not>(std::move(predicate));
|
return ast::Formula::make<ast::Not>(ast::Predicate(predicateDeclaration));
|
||||||
}
|
}
|
||||||
|
|
||||||
// Create new body variable declarations
|
// Create new body variable declarations
|
||||||
@ -73,12 +76,12 @@ struct BodyTermTranslateVisitor
|
|||||||
for (size_t i = 0; i < function.arguments.size(); i++)
|
for (size_t i = 0; i < function.arguments.size(); i++)
|
||||||
{
|
{
|
||||||
auto &argument = function.arguments[i];
|
auto &argument = function.arguments[i];
|
||||||
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[i].get()), translate(argument, ruleContext, variableStack)));
|
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[i].get()), translate(argument, ruleContext, context, variableStack)));
|
||||||
}
|
}
|
||||||
|
|
||||||
variableStack.pop();
|
variableStack.pop();
|
||||||
|
|
||||||
ast::Predicate predicate(std::string(function.name));
|
ast::Predicate predicate(predicateDeclaration);
|
||||||
predicate.arguments.reserve(function.arguments.size());
|
predicate.arguments.reserve(function.arguments.size());
|
||||||
|
|
||||||
for (size_t i = 0; i < function.arguments.size(); i++)
|
for (size_t i = 0; i < function.arguments.size(); i++)
|
||||||
@ -93,7 +96,8 @@ struct BodyTermTranslateVisitor
|
|||||||
}
|
}
|
||||||
|
|
||||||
template<class T>
|
template<class T>
|
||||||
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, RuleContext &, ast::VariableStack &)
|
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &,
|
||||||
|
const Clingo::AST::Term &term, RuleContext &, Context &, ast::VariableStack &)
|
||||||
{
|
{
|
||||||
assert(!term.data.is<Clingo::AST::Function>());
|
assert(!term.data.is<Clingo::AST::Function>());
|
||||||
|
|
||||||
@ -106,18 +110,18 @@ struct BodyTermTranslateVisitor
|
|||||||
|
|
||||||
struct BodyLiteralTranslateVisitor
|
struct BodyLiteralTranslateVisitor
|
||||||
{
|
{
|
||||||
std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, ast::VariableStack &)
|
std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, Context &, ast::VariableStack &)
|
||||||
{
|
{
|
||||||
return ast::Formula::make<ast::Boolean>(boolean.value);
|
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, ast::VariableStack &variableStack)
|
std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack)
|
||||||
{
|
{
|
||||||
return term.data.accept(BodyTermTranslateVisitor(), literal, term, ruleContext, variableStack);
|
return term.data.accept(BodyTermTranslateVisitor(), literal, term, ruleContext, context, variableStack);
|
||||||
}
|
}
|
||||||
|
|
||||||
// TODO: refactor
|
// TODO: refactor
|
||||||
std::optional<ast::Formula> visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack)
|
std::optional<ast::Formula> visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack)
|
||||||
{
|
{
|
||||||
// Comparisons should never have a sign, because these are converted to positive comparisons by clingo
|
// Comparisons should never have a sign, because these are converted to positive comparisons by clingo
|
||||||
if (literal.sign != Clingo::AST::Sign::None)
|
if (literal.sign != Clingo::AST::Sign::None)
|
||||||
@ -132,15 +136,15 @@ struct BodyLiteralTranslateVisitor
|
|||||||
|
|
||||||
ast::And conjunction;
|
ast::And conjunction;
|
||||||
conjunction.arguments.reserve(3);
|
conjunction.arguments.reserve(3);
|
||||||
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[0].get()), translate(comparison.left, ruleContext, variableStack)));
|
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[0].get()), translate(comparison.left, ruleContext, context, variableStack)));
|
||||||
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[1].get()), translate(comparison.right, ruleContext, variableStack)));
|
conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[1].get()), translate(comparison.right, ruleContext, context, variableStack)));
|
||||||
conjunction.arguments.emplace_back(ast::Formula::make<ast::Comparison>(operator_, ast::Variable(parameters[0].get()), ast::Variable(parameters[1].get())));
|
conjunction.arguments.emplace_back(ast::Formula::make<ast::Comparison>(operator_, ast::Variable(parameters[0].get()), ast::Variable(parameters[1].get())));
|
||||||
|
|
||||||
return ast::Formula::make<ast::Exists>(std::move(parameters), std::move(conjunction));
|
return ast::Formula::make<ast::Exists>(std::move(parameters), std::move(conjunction));
|
||||||
}
|
}
|
||||||
|
|
||||||
template<class T>
|
template<class T>
|
||||||
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, ast::VariableStack &)
|
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, Context &, ast::VariableStack &)
|
||||||
{
|
{
|
||||||
throw TranslationException(literal.location, "literal currently unsupported in this context, expected function or term");
|
throw TranslationException(literal.location, "literal currently unsupported in this context, expected function or term");
|
||||||
return std::nullopt;
|
return std::nullopt;
|
||||||
@ -151,16 +155,16 @@ struct BodyLiteralTranslateVisitor
|
|||||||
|
|
||||||
struct BodyBodyLiteralTranslateVisitor
|
struct BodyBodyLiteralTranslateVisitor
|
||||||
{
|
{
|
||||||
std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &ruleContext, ast::VariableStack &variableStack)
|
std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack)
|
||||||
{
|
{
|
||||||
if (bodyLiteral.sign != Clingo::AST::Sign::None)
|
if (bodyLiteral.sign != Clingo::AST::Sign::None)
|
||||||
throw TranslationException(bodyLiteral.location, "only positive body literals supported currently");
|
throw TranslationException(bodyLiteral.location, "only positive body literals supported currently");
|
||||||
|
|
||||||
return literal.data.accept(BodyLiteralTranslateVisitor(), literal, ruleContext, variableStack);
|
return literal.data.accept(BodyLiteralTranslateVisitor(), literal, ruleContext, context, variableStack);
|
||||||
}
|
}
|
||||||
|
|
||||||
template<class T>
|
template<class T>
|
||||||
std::optional<ast::Formula> visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &, ast::VariableStack &)
|
std::optional<ast::Formula> visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &, Context &, ast::VariableStack &)
|
||||||
{
|
{
|
||||||
throw TranslationException(bodyLiteral.location, "body literal currently unsupported in this context, expected literal");
|
throw TranslationException(bodyLiteral.location, "body literal currently unsupported in this context, expected literal");
|
||||||
return std::nullopt;
|
return std::nullopt;
|
||||||
|
@ -16,9 +16,9 @@ namespace anthem
|
|||||||
//
|
//
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
struct PredicateSignatureMeta
|
struct PredicateDeclarationMeta
|
||||||
{
|
{
|
||||||
ast::PredicateSignature predicateSignature;
|
ast::PredicateDeclaration *declaration;
|
||||||
bool used{false};
|
bool used{false};
|
||||||
};
|
};
|
||||||
|
|
||||||
@ -33,13 +33,59 @@ 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;
|
output::Logger logger;
|
||||||
|
|
||||||
bool performSimplification = false;
|
bool performSimplification{false};
|
||||||
bool performCompletion = false;
|
bool performCompletion{false};
|
||||||
|
bool performIntegerDetection{false};
|
||||||
|
|
||||||
std::optional<std::vector<PredicateSignatureMeta>> visiblePredicateSignatures;
|
std::vector<std::unique_ptr<ast::PredicateDeclaration>> predicateDeclarations;
|
||||||
std::optional<std::vector<PredicateSignatureMeta>> externalPredicateSignatures;
|
ast::PredicateDeclaration::Visibility defaultPredicateVisibility{ast::PredicateDeclaration::Visibility::Visible};
|
||||||
|
|
||||||
|
std::vector<std::unique_ptr<ast::FunctionDeclaration>> functionDeclarations;
|
||||||
|
|
||||||
|
bool externalStatementsUsed{false};
|
||||||
|
bool showStatementsUsed{false};
|
||||||
|
|
||||||
ast::ParenthesisStyle parenthesisStyle = ast::ParenthesisStyle::Normal;
|
ast::ParenthesisStyle parenthesisStyle = ast::ParenthesisStyle::Normal;
|
||||||
};
|
};
|
||||||
|
@ -3,6 +3,7 @@
|
|||||||
|
|
||||||
#include <anthem/AST.h>
|
#include <anthem/AST.h>
|
||||||
#include <anthem/ASTUtils.h>
|
#include <anthem/ASTUtils.h>
|
||||||
|
#include <anthem/Utils.h>
|
||||||
|
|
||||||
namespace anthem
|
namespace anthem
|
||||||
{
|
{
|
||||||
@ -15,16 +16,6 @@ namespace ast
|
|||||||
//
|
//
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
// TODO: move to separate class
|
|
||||||
enum class Tristate
|
|
||||||
{
|
|
||||||
True,
|
|
||||||
False,
|
|
||||||
Unknown,
|
|
||||||
};
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
Tristate equal(const Formula &lhs, const Formula &rhs);
|
Tristate equal(const Formula &lhs, const Formula &rhs);
|
||||||
Tristate equal(const Term &lhs, const Term &rhs);
|
Tristate equal(const Term &lhs, const Term &rhs);
|
||||||
|
|
||||||
@ -237,7 +228,7 @@ struct FormulaEqualityVisitor
|
|||||||
|
|
||||||
const auto &otherPredicate = otherFormula.get<Predicate>();
|
const auto &otherPredicate = otherFormula.get<Predicate>();
|
||||||
|
|
||||||
if (!matches(predicate, otherPredicate))
|
if (predicate.declaration != otherPredicate.declaration)
|
||||||
return Tristate::False;
|
return Tristate::False;
|
||||||
|
|
||||||
assert(predicate.arguments.size() == otherPredicate.arguments.size());
|
assert(predicate.arguments.size() == otherPredicate.arguments.size());
|
||||||
@ -277,8 +268,8 @@ struct TermEqualityVisitor
|
|||||||
return Tristate::Unknown;
|
return Tristate::Unknown;
|
||||||
}
|
}
|
||||||
|
|
||||||
if (equal(binaryOperation.left, binaryOperation.right) == Tristate::True
|
if (equal(binaryOperation.left, otherBinaryOperation.right) == Tristate::True
|
||||||
&& equal(binaryOperation.right, binaryOperation.left) == Tristate::True)
|
&& equal(binaryOperation.right, otherBinaryOperation.left) == Tristate::True)
|
||||||
{
|
{
|
||||||
return Tristate::True;
|
return Tristate::True;
|
||||||
}
|
}
|
||||||
@ -298,18 +289,6 @@ struct TermEqualityVisitor
|
|||||||
: Tristate::False;
|
: 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)
|
Tristate visit(const Function &function, const Term &otherTerm)
|
||||||
{
|
{
|
||||||
if (!otherTerm.is<Function>())
|
if (!otherTerm.is<Function>())
|
||||||
@ -317,7 +296,7 @@ struct TermEqualityVisitor
|
|||||||
|
|
||||||
const auto &otherFunction = otherTerm.get<Function>();
|
const auto &otherFunction = otherTerm.get<Function>();
|
||||||
|
|
||||||
if (function.name != otherFunction.name)
|
if (function.declaration != otherFunction.declaration)
|
||||||
return Tristate::False;
|
return Tristate::False;
|
||||||
|
|
||||||
if (function.arguments.size() != otherFunction.arguments.size())
|
if (function.arguments.size() != otherFunction.arguments.size())
|
||||||
|
244
include/anthem/Evaluation.h
Normal file
244
include/anthem/Evaluation.h
Normal file
@ -0,0 +1,244 @@
|
|||||||
|
#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,8 +118,7 @@ struct HeadLiteralCollectFunctionTermsVisitor
|
|||||||
|
|
||||||
struct FunctionTermTranslateVisitor
|
struct FunctionTermTranslateVisitor
|
||||||
{
|
{
|
||||||
// TODO: check correctness
|
std::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
|
||||||
std::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, size_t &headVariableIndex)
|
|
||||||
{
|
{
|
||||||
if (function.external)
|
if (function.external)
|
||||||
throw TranslationException(term.location, "external functions currently unsupported");
|
throw TranslationException(term.location, "external functions currently unsupported");
|
||||||
@ -130,11 +129,14 @@ struct FunctionTermTranslateVisitor
|
|||||||
for (size_t i = 0; i < function.arguments.size(); i++)
|
for (size_t i = 0; i < function.arguments.size(); i++)
|
||||||
arguments.emplace_back(ast::Variable(ruleContext.freeVariables[headVariableIndex++].get()));
|
arguments.emplace_back(ast::Variable(ruleContext.freeVariables[headVariableIndex++].get()));
|
||||||
|
|
||||||
return ast::Formula::make<ast::Predicate>(function.name, std::move(arguments));
|
auto predicateDeclaration = context.findOrCreatePredicateDeclaration(function.name, function.arguments.size());
|
||||||
|
predicateDeclaration->isUsed = true;
|
||||||
|
|
||||||
|
return ast::Predicate(predicateDeclaration, std::move(arguments));
|
||||||
}
|
}
|
||||||
|
|
||||||
template<class T>
|
template<class T>
|
||||||
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Term &term, RuleContext &, size_t &)
|
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Term &term, RuleContext &, Context &, size_t &)
|
||||||
{
|
{
|
||||||
throw TranslationException(term.location, "term currently unsupported in this context, function expected");
|
throw TranslationException(term.location, "term currently unsupported in this context, function expected");
|
||||||
return std::nullopt;
|
return std::nullopt;
|
||||||
@ -145,18 +147,18 @@ struct FunctionTermTranslateVisitor
|
|||||||
|
|
||||||
struct LiteralTranslateVisitor
|
struct LiteralTranslateVisitor
|
||||||
{
|
{
|
||||||
std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, size_t &)
|
std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, Context &, size_t &)
|
||||||
{
|
{
|
||||||
return ast::Formula::make<ast::Boolean>(boolean.value);
|
return ast::Formula::make<ast::Boolean>(boolean.value);
|
||||||
}
|
}
|
||||||
|
|
||||||
std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, RuleContext &ruleContext, size_t &headVariableIndex)
|
std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
|
||||||
{
|
{
|
||||||
return term.data.accept(FunctionTermTranslateVisitor(), term, ruleContext, headVariableIndex);
|
return term.data.accept(FunctionTermTranslateVisitor(), term, ruleContext, context, headVariableIndex);
|
||||||
}
|
}
|
||||||
|
|
||||||
template<class T>
|
template<class T>
|
||||||
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, size_t &)
|
std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, Context &, size_t &)
|
||||||
{
|
{
|
||||||
throw TranslationException(literal.location, "only disjunctions of literals allowed as head literals");
|
throw TranslationException(literal.location, "only disjunctions of literals allowed as head literals");
|
||||||
return std::nullopt;
|
return std::nullopt;
|
||||||
@ -167,12 +169,12 @@ struct LiteralTranslateVisitor
|
|||||||
|
|
||||||
struct HeadLiteralTranslateToConsequentVisitor
|
struct HeadLiteralTranslateToConsequentVisitor
|
||||||
{
|
{
|
||||||
std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, RuleContext &ruleContext, size_t &headVariableIndex)
|
std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
|
||||||
{
|
{
|
||||||
if (literal.sign == Clingo::AST::Sign::DoubleNegation)
|
if (literal.sign == Clingo::AST::Sign::DoubleNegation)
|
||||||
throw TranslationException(literal.location, "double-negated head literals currently unsupported");
|
throw TranslationException(literal.location, "double-negated head literals currently unsupported");
|
||||||
|
|
||||||
auto translatedLiteral = literal.data.accept(LiteralTranslateVisitor(), literal, ruleContext, headVariableIndex);
|
auto translatedLiteral = literal.data.accept(LiteralTranslateVisitor(), literal, ruleContext, context, headVariableIndex);
|
||||||
|
|
||||||
if (literal.sign == Clingo::AST::Sign::None)
|
if (literal.sign == Clingo::AST::Sign::None)
|
||||||
return translatedLiteral;
|
return translatedLiteral;
|
||||||
@ -183,7 +185,7 @@ struct HeadLiteralTranslateToConsequentVisitor
|
|||||||
return ast::Formula::make<ast::Not>(std::move(translatedLiteral.value()));
|
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, size_t &headVariableIndex)
|
std::optional<ast::Formula> visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
|
||||||
{
|
{
|
||||||
std::vector<ast::Formula> arguments;
|
std::vector<ast::Formula> arguments;
|
||||||
arguments.reserve(disjunction.elements.size());
|
arguments.reserve(disjunction.elements.size());
|
||||||
@ -193,7 +195,7 @@ struct HeadLiteralTranslateToConsequentVisitor
|
|||||||
if (!conditionalLiteral.condition.empty())
|
if (!conditionalLiteral.condition.empty())
|
||||||
throw TranslationException(headLiteral.location, "conditional head literals currently unsupported");
|
throw TranslationException(headLiteral.location, "conditional head literals currently unsupported");
|
||||||
|
|
||||||
auto argument = visit(conditionalLiteral.literal, headLiteral, ruleContext, headVariableIndex);
|
auto argument = visit(conditionalLiteral.literal, headLiteral, ruleContext, context, headVariableIndex);
|
||||||
|
|
||||||
if (!argument)
|
if (!argument)
|
||||||
throw TranslationException(headLiteral.location, "could not parse argument");
|
throw TranslationException(headLiteral.location, "could not parse argument");
|
||||||
@ -204,7 +206,7 @@ struct HeadLiteralTranslateToConsequentVisitor
|
|||||||
return ast::Formula::make<ast::Or>(std::move(arguments));
|
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, size_t &headVariableIndex)
|
std::optional<ast::Formula> visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
|
||||||
{
|
{
|
||||||
if (aggregate.left_guard || aggregate.right_guard)
|
if (aggregate.left_guard || aggregate.right_guard)
|
||||||
throw TranslationException(headLiteral.location, "aggregates with left or right guards currently unsupported");
|
throw TranslationException(headLiteral.location, "aggregates with left or right guards currently unsupported");
|
||||||
@ -215,7 +217,7 @@ struct HeadLiteralTranslateToConsequentVisitor
|
|||||||
if (!conditionalLiteral.condition.empty())
|
if (!conditionalLiteral.condition.empty())
|
||||||
throw TranslationException(headLiteral.location, "conditional head literals currently unsupported");
|
throw TranslationException(headLiteral.location, "conditional head literals currently unsupported");
|
||||||
|
|
||||||
return this->visit(conditionalLiteral.literal, headLiteral, ruleContext, headVariableIndex);
|
return this->visit(conditionalLiteral.literal, headLiteral, ruleContext, context, headVariableIndex);
|
||||||
};
|
};
|
||||||
|
|
||||||
if (aggregate.elements.size() == 1)
|
if (aggregate.elements.size() == 1)
|
||||||
@ -238,7 +240,7 @@ struct HeadLiteralTranslateToConsequentVisitor
|
|||||||
}
|
}
|
||||||
|
|
||||||
template<class T>
|
template<class T>
|
||||||
std::optional<ast::Formula> visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &, size_t &)
|
std::optional<ast::Formula> visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &, Context &, size_t &)
|
||||||
{
|
{
|
||||||
throw TranslationException(headLiteral.location, "head literal currently unsupported in this context, expected literal, disjunction, or aggregate");
|
throw TranslationException(headLiteral.location, "head literal currently unsupported in this context, expected literal, disjunction, or aggregate");
|
||||||
return std::nullopt;
|
return std::nullopt;
|
||||||
|
@ -13,7 +13,7 @@ namespace anthem
|
|||||||
//
|
//
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predicateSignatures, std::vector<ast::Formula> &completedFormulas, Context &context);
|
void eliminateHiddenPredicates(std::vector<ast::Formula> &completedFormulas, Context &context);
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
22
include/anthem/IntegerVariableDetection.h
Normal file
22
include/anthem/IntegerVariableDetection.h
Normal file
@ -0,0 +1,22 @@
|
|||||||
|
#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,14 +12,6 @@ namespace anthem
|
|||||||
//
|
//
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
enum class SimplificationResult
|
|
||||||
{
|
|
||||||
Simplified,
|
|
||||||
Unchanged,
|
|
||||||
};
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
void simplify(ast::Formula &formula);
|
void simplify(ast::Formula &formula);
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
@ -3,6 +3,7 @@
|
|||||||
|
|
||||||
#include <anthem/AST.h>
|
#include <anthem/AST.h>
|
||||||
#include <anthem/Simplification.h>
|
#include <anthem/Simplification.h>
|
||||||
|
#include <anthem/Utils.h>
|
||||||
|
|
||||||
namespace anthem
|
namespace anthem
|
||||||
{
|
{
|
||||||
@ -19,96 +20,96 @@ template<class T>
|
|||||||
struct FormulaSimplificationVisitor
|
struct FormulaSimplificationVisitor
|
||||||
{
|
{
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
SimplificationResult visit(And &and_, Formula &formula, Arguments &&... arguments)
|
OperationResult visit(And &and_, Formula &formula, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
for (auto &argument : and_.arguments)
|
for (auto &argument : and_.arguments)
|
||||||
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
|
|
||||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
SimplificationResult visit(Biconditional &biconditional, Formula &formula, Arguments &&... arguments)
|
OperationResult visit(Biconditional &biconditional, Formula &formula, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
if (biconditional.left.accept(*this, biconditional.left, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
if (biconditional.left.accept(*this, biconditional.left, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
|
|
||||||
if (biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
if (biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
|
|
||||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
SimplificationResult visit(Boolean &, Formula &formula, Arguments &&... arguments)
|
OperationResult visit(Boolean &, Formula &formula, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
SimplificationResult visit(Comparison &, Formula &formula, Arguments &&... arguments)
|
OperationResult visit(Comparison &, Formula &formula, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
SimplificationResult visit(Exists &exists, Formula &formula, Arguments &&... arguments)
|
OperationResult visit(Exists &exists, Formula &formula, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
if (exists.argument.accept(*this, exists.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
if (exists.argument.accept(*this, exists.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
|
|
||||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
SimplificationResult visit(ForAll &forAll, Formula &formula, Arguments &&... arguments)
|
OperationResult visit(ForAll &forAll, Formula &formula, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
if (forAll.argument.accept(*this, forAll.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
if (forAll.argument.accept(*this, forAll.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
|
|
||||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
SimplificationResult visit(Implies &implies, Formula &formula, Arguments &&... arguments)
|
OperationResult visit(Implies &implies, Formula &formula, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
if (implies.antecedent.accept(*this, implies.antecedent, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
if (implies.antecedent.accept(*this, implies.antecedent, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
|
|
||||||
if (implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
if (implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
|
|
||||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
SimplificationResult visit(In &, Formula &formula, Arguments &&... arguments)
|
OperationResult visit(In &, Formula &formula, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
SimplificationResult visit(Not ¬_, Formula &formula, Arguments &&... arguments)
|
OperationResult visit(Not ¬_, Formula &formula, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
if (not_.argument.accept(*this, not_.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
if (not_.argument.accept(*this, not_.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
|
|
||||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
SimplificationResult visit(Or &or_, Formula &formula, Arguments &&... arguments)
|
OperationResult visit(Or &or_, Formula &formula, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
for (auto &argument : or_.arguments)
|
for (auto &argument : or_.arguments)
|
||||||
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
|
|
||||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
SimplificationResult visit(Predicate &, Formula &formula, Arguments &&... arguments)
|
OperationResult visit(Predicate &, Formula &formula, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||||
}
|
}
|
||||||
@ -116,75 +117,69 @@ struct FormulaSimplificationVisitor
|
|||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
template<class T, class SimplificationResult = void>
|
template<class T, class OperationResult = void>
|
||||||
struct TermSimplificationVisitor
|
struct TermSimplificationVisitor
|
||||||
{
|
{
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
SimplificationResult visit(BinaryOperation &binaryOperation, Term &term, Arguments &&... arguments)
|
OperationResult visit(BinaryOperation &binaryOperation, Term &term, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
if (binaryOperation.left.accept(*this, binaryOperation.left, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
if (binaryOperation.left.accept(*this, binaryOperation.left, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
|
|
||||||
if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
|
|
||||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
SimplificationResult visit(Boolean &, Term &term, Arguments &&... arguments)
|
OperationResult visit(Boolean &, Term &term, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
SimplificationResult visit(Constant &, Term &term, Arguments &&... arguments)
|
OperationResult visit(Function &function, 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)
|
for (auto &argument : function.arguments)
|
||||||
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
|
|
||||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
SimplificationResult visit(Integer &, Term &term, Arguments &&... arguments)
|
OperationResult visit(Integer &, Term &term, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
SimplificationResult visit(Interval &interval, Term &term, Arguments &&... arguments)
|
OperationResult visit(Interval &interval, Term &term, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
if (interval.from.accept(*this, interval.from, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
if (interval.from.accept(*this, interval.from, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
|
|
||||||
if (interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
if (interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
|
|
||||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
SimplificationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments)
|
OperationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
SimplificationResult visit(String &, Term &term, Arguments &&... arguments)
|
OperationResult visit(String &, Term &term, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
SimplificationResult visit(Variable &, Term &term, Arguments &&... arguments)
|
OperationResult visit(Variable &, Term &term, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||||
}
|
}
|
||||||
|
@ -73,7 +73,7 @@ struct StatementVisitor
|
|||||||
|
|
||||||
// Compute consequent
|
// Compute consequent
|
||||||
auto headVariableIndex = ruleContext.headVariablesStartIndex;
|
auto headVariableIndex = ruleContext.headVariablesStartIndex;
|
||||||
auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, ruleContext, headVariableIndex);
|
auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, ruleContext, context, headVariableIndex);
|
||||||
|
|
||||||
assert(ruleContext.headTerms.size() == headVariableIndex - ruleContext.headVariablesStartIndex);
|
assert(ruleContext.headTerms.size() == headVariableIndex - ruleContext.headVariablesStartIndex);
|
||||||
|
|
||||||
@ -87,7 +87,7 @@ struct StatementVisitor
|
|||||||
|
|
||||||
const auto auxiliaryHeadVariableID = ruleContext.headVariablesStartIndex + i - ruleContext.headTerms.cbegin();
|
const auto auxiliaryHeadVariableID = ruleContext.headVariablesStartIndex + i - ruleContext.headTerms.cbegin();
|
||||||
auto element = ast::Variable(ruleContext.freeVariables[auxiliaryHeadVariableID].get());
|
auto element = ast::Variable(ruleContext.freeVariables[auxiliaryHeadVariableID].get());
|
||||||
auto set = translate(headTerm, ruleContext, variableStack);
|
auto set = translate(headTerm, ruleContext, context, variableStack);
|
||||||
auto in = ast::In(std::move(element), std::move(set));
|
auto in = ast::In(std::move(element), std::move(set));
|
||||||
|
|
||||||
antecedent.arguments.emplace_back(std::move(in));
|
antecedent.arguments.emplace_back(std::move(in));
|
||||||
@ -98,7 +98,7 @@ struct StatementVisitor
|
|||||||
{
|
{
|
||||||
const auto &bodyLiteral = *i;
|
const auto &bodyLiteral = *i;
|
||||||
|
|
||||||
auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, ruleContext, variableStack);
|
auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, ruleContext, context, variableStack);
|
||||||
|
|
||||||
if (!argument)
|
if (!argument)
|
||||||
throw TranslationException(bodyLiteral.location, "could not translate body literal");
|
throw TranslationException(bodyLiteral.location, "could not translate body literal");
|
||||||
@ -165,8 +165,8 @@ struct StatementVisitor
|
|||||||
if (signature.negative())
|
if (signature.negative())
|
||||||
throw LogicException(statement.location, "negative #show atom signatures are currently unsupported");
|
throw LogicException(statement.location, "negative #show atom signatures are currently unsupported");
|
||||||
|
|
||||||
if (!context.visiblePredicateSignatures)
|
context.showStatementsUsed = true;
|
||||||
context.visiblePredicateSignatures.emplace();
|
context.defaultPredicateVisibility = ast::PredicateDeclaration::Visibility::Hidden;
|
||||||
|
|
||||||
if (std::strlen(signature.name()) == 0)
|
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() << "”";
|
context.logger.log(output::Priority::Debug, statement.location) << "showing “" << signature.name() << "/" << signature.arity() << "”";
|
||||||
|
|
||||||
auto predicateSignature = ast::PredicateSignature{std::string(signature.name()), signature.arity()};
|
auto predicateDeclaration = context.findOrCreatePredicateDeclaration(signature.name(), signature.arity());
|
||||||
context.visiblePredicateSignatures.value().emplace_back(PredicateSignatureMeta{std::move(predicateSignature)});
|
predicateDeclaration->visibility = ast::PredicateDeclaration::Visibility::Visible;
|
||||||
}
|
}
|
||||||
|
|
||||||
void visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &)
|
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 =
|
const auto fail =
|
||||||
[&]()
|
[&]()
|
||||||
{
|
{
|
||||||
throw LogicException(statement.location, "only #external declarations of the form “#external <predicate name>(<arity>).” supported");
|
throw LogicException(statement.location, "only #external declarations of the form “#external <predicate name>(<arity>).” or “#external integer(<function name>(<arity>)).” supported");
|
||||||
};
|
};
|
||||||
|
|
||||||
if (!external.body.empty())
|
if (!external.body.empty())
|
||||||
@ -204,6 +204,47 @@ struct StatementVisitor
|
|||||||
if (predicate.arguments.size() != 1)
|
if (predicate.arguments.size() != 1)
|
||||||
fail();
|
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();
|
const auto &arityArgument = predicate.arguments.front();
|
||||||
|
|
||||||
if (!arityArgument.data.is<Clingo::Symbol>())
|
if (!arityArgument.data.is<Clingo::Symbol>())
|
||||||
@ -214,13 +255,12 @@ struct StatementVisitor
|
|||||||
if (aritySymbol.type() != Clingo::SymbolType::Number)
|
if (aritySymbol.type() != Clingo::SymbolType::Number)
|
||||||
fail();
|
fail();
|
||||||
|
|
||||||
const size_t arity = arityArgument.data.get<Clingo::Symbol>().number();
|
context.externalStatementsUsed = true;
|
||||||
|
|
||||||
if (!context.externalPredicateSignatures)
|
const size_t arity = aritySymbol.number();
|
||||||
context.externalPredicateSignatures.emplace();
|
|
||||||
|
|
||||||
auto predicateSignature = ast::PredicateSignature{std::string(predicate.name), arity};
|
auto predicateDeclaration = context.findOrCreatePredicateDeclaration(predicate.name, arity);
|
||||||
context.externalPredicateSignatures->emplace_back(PredicateSignatureMeta{std::move(predicateSignature)});
|
predicateDeclaration->isExternal = true;
|
||||||
}
|
}
|
||||||
|
|
||||||
template<class T>
|
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, const ast::VariableStack &variableStack);
|
ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack);
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
struct TermTranslateVisitor
|
struct TermTranslateVisitor
|
||||||
{
|
{
|
||||||
std::optional<ast::Term> visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
|
std::optional<ast::Term> visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
|
||||||
{
|
{
|
||||||
switch (symbol.type())
|
switch (symbol.type())
|
||||||
{
|
{
|
||||||
@ -85,19 +85,19 @@ struct TermTranslateVisitor
|
|||||||
return ast::Term::make<ast::String>(std::string(symbol.string()));
|
return ast::Term::make<ast::String>(std::string(symbol.string()));
|
||||||
case Clingo::SymbolType::Function:
|
case Clingo::SymbolType::Function:
|
||||||
{
|
{
|
||||||
auto function = ast::Term::make<ast::Function>(symbol.name());
|
auto functionDeclaration = context.findOrCreateFunctionDeclaration(symbol.name(), symbol.arguments().size());
|
||||||
// TODO: remove workaround
|
|
||||||
auto &functionRaw = function.get<ast::Function>();
|
auto function = ast::Function(functionDeclaration);
|
||||||
functionRaw.arguments.reserve(symbol.arguments().size());
|
function.arguments.reserve(symbol.arguments().size());
|
||||||
|
|
||||||
for (const auto &argument : symbol.arguments())
|
for (const auto &argument : symbol.arguments())
|
||||||
{
|
{
|
||||||
auto translatedArgument = visit(argument, term, ruleContext, variableStack);
|
auto translatedArgument = visit(argument, term, ruleContext, context, variableStack);
|
||||||
|
|
||||||
if (!translatedArgument)
|
if (!translatedArgument)
|
||||||
throw TranslationException(term.location, "could not translate argument");
|
throw TranslationException(term.location, "could not translate argument");
|
||||||
|
|
||||||
functionRaw.arguments.emplace_back(std::move(translatedArgument.value()));
|
function.arguments.emplace_back(std::move(translatedArgument.value()));
|
||||||
}
|
}
|
||||||
|
|
||||||
return std::move(function);
|
return std::move(function);
|
||||||
@ -107,7 +107,7 @@ struct TermTranslateVisitor
|
|||||||
return std::nullopt;
|
return std::nullopt;
|
||||||
}
|
}
|
||||||
|
|
||||||
std::optional<ast::Term> visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack)
|
std::optional<ast::Term> visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, RuleContext &ruleContext, Context &, const ast::VariableStack &variableStack)
|
||||||
{
|
{
|
||||||
const auto matchingVariableDeclaration = variableStack.findUserVariableDeclaration(variable.name);
|
const auto matchingVariableDeclaration = variableStack.findUserVariableDeclaration(variable.name);
|
||||||
const auto isAnonymousVariable = (strcmp(variable.name, "_") == 0);
|
const auto isAnonymousVariable = (strcmp(variable.name, "_") == 0);
|
||||||
@ -120,35 +120,36 @@ struct TermTranslateVisitor
|
|||||||
auto variableDeclaration = std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::UserDefined, std::string(variable.name));
|
auto variableDeclaration = std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::UserDefined, std::string(variable.name));
|
||||||
ruleContext.freeVariables.emplace_back(std::move(variableDeclaration));
|
ruleContext.freeVariables.emplace_back(std::move(variableDeclaration));
|
||||||
|
|
||||||
|
// TODO: ast::Term::make is unnecessary and can be removed
|
||||||
return ast::Term::make<ast::Variable>(ruleContext.freeVariables.back().get());
|
return ast::Term::make<ast::Variable>(ruleContext.freeVariables.back().get());
|
||||||
}
|
}
|
||||||
|
|
||||||
std::optional<ast::Term> visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
|
std::optional<ast::Term> visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
|
||||||
{
|
{
|
||||||
const auto operator_ = translate(binaryOperation.binary_operator, term);
|
const auto operator_ = translate(binaryOperation.binary_operator, term);
|
||||||
auto left = translate(binaryOperation.left, ruleContext, variableStack);
|
auto left = translate(binaryOperation.left, ruleContext, context, variableStack);
|
||||||
auto right = translate(binaryOperation.right, ruleContext, variableStack);
|
auto right = translate(binaryOperation.right, ruleContext, context, variableStack);
|
||||||
|
|
||||||
return ast::Term::make<ast::BinaryOperation>(operator_, std::move(left), std::move(right));
|
return ast::Term::make<ast::BinaryOperation>(operator_, std::move(left), std::move(right));
|
||||||
}
|
}
|
||||||
|
|
||||||
std::optional<ast::Term> visit(const Clingo::AST::UnaryOperation &unaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
|
std::optional<ast::Term> visit(const Clingo::AST::UnaryOperation &unaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
|
||||||
{
|
{
|
||||||
const auto operator_ = translate(unaryOperation.unary_operator, term);
|
const auto operator_ = translate(unaryOperation.unary_operator, term);
|
||||||
auto argument = translate(unaryOperation.argument, ruleContext, variableStack);
|
auto argument = translate(unaryOperation.argument, ruleContext, context, variableStack);
|
||||||
|
|
||||||
return ast::Term::make<ast::UnaryOperation>(operator_, std::move(argument));
|
return ast::Term::make<ast::UnaryOperation>(operator_, std::move(argument));
|
||||||
}
|
}
|
||||||
|
|
||||||
std::optional<ast::Term> visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack)
|
std::optional<ast::Term> visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
|
||||||
{
|
{
|
||||||
auto left = translate(interval.left, ruleContext, variableStack);
|
auto left = translate(interval.left, ruleContext, context, variableStack);
|
||||||
auto right = translate(interval.right, ruleContext, variableStack);
|
auto right = translate(interval.right, ruleContext, context, variableStack);
|
||||||
|
|
||||||
return ast::Term::make<ast::Interval>(std::move(left), std::move(right));
|
return ast::Term::make<ast::Interval>(std::move(left), std::move(right));
|
||||||
}
|
}
|
||||||
|
|
||||||
std::optional<ast::Term> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
|
std::optional<ast::Term> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
|
||||||
{
|
{
|
||||||
if (function.external)
|
if (function.external)
|
||||||
throw TranslationException(term.location, "external functions currently unsupported");
|
throw TranslationException(term.location, "external functions currently unsupported");
|
||||||
@ -157,12 +158,14 @@ struct TermTranslateVisitor
|
|||||||
arguments.reserve(function.arguments.size());
|
arguments.reserve(function.arguments.size());
|
||||||
|
|
||||||
for (const auto &argument : function.arguments)
|
for (const auto &argument : function.arguments)
|
||||||
arguments.emplace_back(translate(argument, ruleContext, variableStack));
|
arguments.emplace_back(translate(argument, ruleContext, context, variableStack));
|
||||||
|
|
||||||
return ast::Term::make<ast::Function>(function.name, std::move(arguments));
|
auto functionDeclaration = context.findOrCreateFunctionDeclaration(function.name, function.arguments.size());
|
||||||
|
|
||||||
|
return ast::Term::make<ast::Function>(functionDeclaration, std::move(arguments));
|
||||||
}
|
}
|
||||||
|
|
||||||
std::optional<ast::Term> visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, RuleContext &, const ast::VariableStack &)
|
std::optional<ast::Term> visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, RuleContext &, Context &, const ast::VariableStack &)
|
||||||
{
|
{
|
||||||
throw TranslationException(term.location, "“pool” terms currently unsupported");
|
throw TranslationException(term.location, "“pool” terms currently unsupported");
|
||||||
return std::nullopt;
|
return std::nullopt;
|
||||||
@ -171,9 +174,9 @@ struct TermTranslateVisitor
|
|||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
|
ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
|
||||||
{
|
{
|
||||||
auto translatedTerm = term.data.accept(TermTranslateVisitor(), term, ruleContext, variableStack);
|
auto translatedTerm = term.data.accept(TermTranslateVisitor(), term, ruleContext, context, variableStack);
|
||||||
|
|
||||||
if (!translatedTerm)
|
if (!translatedTerm)
|
||||||
throw TranslationException(term.location, "could not translate term");
|
throw TranslationException(term.location, "could not translate term");
|
||||||
|
157
include/anthem/Type.h
Normal file
157
include/anthem/Type.h
Normal file
@ -0,0 +1,157 @@
|
|||||||
|
#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,13 +1,6 @@
|
|||||||
#ifndef __ANTHEM__UTILS_H
|
#ifndef __ANTHEM__UTILS_H
|
||||||
#define __ANTHEM__UTILS_H
|
#define __ANTHEM__UTILS_H
|
||||||
|
|
||||||
#include <iostream>
|
|
||||||
|
|
||||||
#include <clingo.hh>
|
|
||||||
|
|
||||||
#include <anthem/Context.h>
|
|
||||||
#include <anthem/Location.h>
|
|
||||||
|
|
||||||
namespace anthem
|
namespace anthem
|
||||||
{
|
{
|
||||||
|
|
||||||
@ -20,6 +13,61 @@ namespace anthem
|
|||||||
constexpr const auto HeadVariablePrefix = "V";
|
constexpr const auto HeadVariablePrefix = "V";
|
||||||
constexpr const auto BodyVariablePrefix = "X";
|
constexpr const auto BodyVariablePrefix = "X";
|
||||||
constexpr const auto UserVariablePrefix = "U";
|
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,6 +35,7 @@ struct PrintContext
|
|||||||
std::map<const VariableDeclaration *, size_t> userVariableIDs;
|
std::map<const VariableDeclaration *, size_t> userVariableIDs;
|
||||||
std::map<const VariableDeclaration *, size_t> headVariableIDs;
|
std::map<const VariableDeclaration *, size_t> headVariableIDs;
|
||||||
std::map<const VariableDeclaration *, size_t> bodyVariableIDs;
|
std::map<const VariableDeclaration *, size_t> bodyVariableIDs;
|
||||||
|
std::map<const VariableDeclaration *, size_t> integerVariableIDs;
|
||||||
|
|
||||||
const Context &context;
|
const Context &context;
|
||||||
};
|
};
|
||||||
@ -46,12 +47,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 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, 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, 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 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 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 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 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 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 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 String &string, PrintContext &printContext, bool omitParentheses = false);
|
||||||
output::ColorStream &print(output::ColorStream &stream, const UnaryOperation &unaryOperation, PrintContext &printContext, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const UnaryOperation &unaryOperation, PrintContext &printContext, bool omitParentheses = false);
|
||||||
@ -167,16 +168,9 @@ 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)
|
inline output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext, bool)
|
||||||
{
|
{
|
||||||
stream << function.name;
|
stream << function.declaration->name;
|
||||||
|
|
||||||
if (function.arguments.empty())
|
if (function.arguments.empty())
|
||||||
return stream;
|
return stream;
|
||||||
@ -191,7 +185,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Function &f
|
|||||||
print(stream, *i, printContext);
|
print(stream, *i, printContext);
|
||||||
}
|
}
|
||||||
|
|
||||||
if (function.name.empty() && function.arguments.size() == 1)
|
if (function.declaration->name.empty() && function.arguments.size() == 1)
|
||||||
stream << ",";
|
stream << ",";
|
||||||
|
|
||||||
stream << ")";
|
stream << ")";
|
||||||
@ -225,16 +219,16 @@ inline output::ColorStream &print(output::ColorStream &stream, const Integer &in
|
|||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool)
|
inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool omitParentheses)
|
||||||
{
|
{
|
||||||
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
||||||
stream << "(";
|
stream << "(";
|
||||||
|
|
||||||
print(stream, interval.from, printContext);
|
print(stream, interval.from, printContext);
|
||||||
stream << "..";
|
stream << "..";
|
||||||
print(stream, interval.to, printContext);
|
print(stream, interval.to, printContext);
|
||||||
|
|
||||||
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
|
||||||
stream << ")";
|
stream << ")";
|
||||||
|
|
||||||
return stream;
|
return stream;
|
||||||
@ -244,7 +238,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Interval &i
|
|||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext, bool)
|
inline output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext, bool)
|
||||||
{
|
{
|
||||||
stream << predicate.name;
|
stream << predicate.declaration->name;
|
||||||
|
|
||||||
if (predicate.arguments.empty())
|
if (predicate.arguments.empty())
|
||||||
return stream;
|
return stream;
|
||||||
@ -266,6 +260,13 @@ 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)
|
inline output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &, bool)
|
||||||
{
|
{
|
||||||
switch (specialInteger.type)
|
switch (specialInteger.type)
|
||||||
@ -339,6 +340,9 @@ inline output::ColorStream &print(output::ColorStream &stream, const VariableDec
|
|||||||
return (stream << output::Variable(variableName.c_str()));
|
return (stream << output::Variable(variableName.c_str()));
|
||||||
};
|
};
|
||||||
|
|
||||||
|
if (variableDeclaration.domain == Domain::Integer)
|
||||||
|
return printVariableDeclaration(IntegerVariablePrefix, printContext.integerVariableIDs);
|
||||||
|
|
||||||
switch (variableDeclaration.type)
|
switch (variableDeclaration.type)
|
||||||
{
|
{
|
||||||
case VariableDeclaration::Type::UserDefined:
|
case VariableDeclaration::Type::UserDefined:
|
||||||
|
@ -103,16 +103,9 @@ Comparison prepareCopy(const Comparison &other)
|
|||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
Constant prepareCopy(const Constant &other)
|
|
||||||
{
|
|
||||||
return Constant(std::string(other.name));
|
|
||||||
}
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
Function prepareCopy(const Function &other)
|
Function prepareCopy(const Function &other)
|
||||||
{
|
{
|
||||||
return Function(std::string(other.name), prepareCopy(other.arguments));
|
return Function(other.declaration, prepareCopy(other.arguments));
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
@ -140,7 +133,7 @@ Interval prepareCopy(const Interval &other)
|
|||||||
|
|
||||||
Predicate prepareCopy(const Predicate &other)
|
Predicate prepareCopy(const Predicate &other)
|
||||||
{
|
{
|
||||||
return Predicate(std::string(other.name), prepareCopy(other.arguments));
|
return Predicate(other.declaration, prepareCopy(other.arguments));
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
@ -293,11 +286,6 @@ struct FixDanglingVariablesInTermVisitor
|
|||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
template <class... Arguments>
|
|
||||||
void visit(Constant &, Arguments &&...)
|
|
||||||
{
|
|
||||||
}
|
|
||||||
|
|
||||||
template <class... Arguments>
|
template <class... Arguments>
|
||||||
void visit(Function &function, Arguments &&... arguments)
|
void visit(Function &function, Arguments &&... arguments)
|
||||||
{
|
{
|
||||||
|
@ -150,10 +150,6 @@ struct CollectFreeVariablesVisitor
|
|||||||
binaryOperation.right.accept(*this, variableStack, freeVariables);
|
binaryOperation.right.accept(*this, variableStack, freeVariables);
|
||||||
}
|
}
|
||||||
|
|
||||||
void visit(Constant &, VariableStack &, std::vector<VariableDeclaration *> &)
|
|
||||||
{
|
|
||||||
}
|
|
||||||
|
|
||||||
void visit(Function &function, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
|
void visit(Function &function, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
|
||||||
{
|
{
|
||||||
for (auto &argument : function.arguments)
|
for (auto &argument : function.arguments)
|
||||||
@ -197,84 +193,5 @@ struct CollectFreeVariablesVisitor
|
|||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
struct CollectPredicateSignaturesVisitor : public RecursiveFormulaVisitor<CollectPredicateSignaturesVisitor>
|
|
||||||
{
|
|
||||||
static void accept(const Predicate &predicate, const Formula &, std::vector<PredicateSignature> &predicateSignatures, Context &context)
|
|
||||||
{
|
|
||||||
const auto predicateSignatureMatches =
|
|
||||||
[&predicate](const auto &predicateSignature)
|
|
||||||
{
|
|
||||||
return matches(predicate, predicateSignature);
|
|
||||||
};
|
|
||||||
|
|
||||||
if (std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), predicateSignatureMatches) != predicateSignatures.cend())
|
|
||||||
return;
|
|
||||||
|
|
||||||
// TODO: avoid copies
|
|
||||||
auto predicateSignature = PredicateSignature(std::string(predicate.name), predicate.arity());
|
|
||||||
|
|
||||||
// Ignore predicates that are declared #external
|
|
||||||
if (context.externalPredicateSignatures)
|
|
||||||
{
|
|
||||||
const auto matchesPredicateSignature =
|
|
||||||
[&](const auto &otherPredicateSignature)
|
|
||||||
{
|
|
||||||
return ast::matches(predicateSignature, otherPredicateSignature.predicateSignature);
|
|
||||||
};
|
|
||||||
|
|
||||||
auto &externalPredicateSignatures = context.externalPredicateSignatures.value();
|
|
||||||
|
|
||||||
const auto matchingExternalPredicateSignature =
|
|
||||||
std::find_if(externalPredicateSignatures.begin(), externalPredicateSignatures.end(), matchesPredicateSignature);
|
|
||||||
|
|
||||||
if (matchingExternalPredicateSignature != externalPredicateSignatures.end())
|
|
||||||
{
|
|
||||||
matchingExternalPredicateSignature->used = true;
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
predicateSignatures.emplace_back(std::move(predicateSignature));
|
|
||||||
}
|
|
||||||
|
|
||||||
// Ignore all other types of expressions
|
|
||||||
template<class T>
|
|
||||||
static void accept(const T &, const Formula &, std::vector<PredicateSignature> &, const Context &)
|
|
||||||
{
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
bool matches(const Predicate &lhs, const Predicate &rhs)
|
|
||||||
{
|
|
||||||
return (lhs.name == rhs.name && lhs.arity() == rhs.arity());
|
|
||||||
}
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
bool matches(const Predicate &predicate, const PredicateSignature &signature)
|
|
||||||
{
|
|
||||||
return (predicate.name == signature.name && predicate.arity() == signature.arity);
|
|
||||||
}
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
bool matches(const PredicateSignature &lhs, const PredicateSignature &rhs)
|
|
||||||
{
|
|
||||||
return (lhs.name == rhs.name && lhs.arity == rhs.arity);
|
|
||||||
}
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
// TODO: remove const_cast
|
|
||||||
void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures, Context &context)
|
|
||||||
{
|
|
||||||
auto &formulaMutable = const_cast<Formula &>(formula);
|
|
||||||
formulaMutable.accept(CollectPredicateSignaturesVisitor(), formulaMutable, predicateSignatures, context);
|
|
||||||
}
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -35,13 +35,41 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c
|
|||||||
|
|
||||||
auto &otherPredicate = implies.consequent.get<ast::Predicate>();
|
auto &otherPredicate = implies.consequent.get<ast::Predicate>();
|
||||||
|
|
||||||
if (!ast::matches(predicate, otherPredicate))
|
if (predicate.declaration != otherPredicate.declaration)
|
||||||
continue;
|
continue;
|
||||||
|
|
||||||
assert(otherPredicate.arguments.size() == parameters.size());
|
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
|
// 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
|
// 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++)
|
for (size_t i = 0; i < parameters.size(); i++)
|
||||||
{
|
{
|
||||||
assert(otherPredicate.arguments[i].is<ast::Variable>());
|
assert(otherPredicate.arguments[i].is<ast::Variable>());
|
||||||
@ -50,16 +78,6 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c
|
|||||||
scopedFormula.formula.accept(ast::ReplaceVariableInFormulaVisitor(), scopedFormula.formula, otherVariable.declaration, parameters[i].get());
|
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())
|
if (freeVariables.empty())
|
||||||
disjunction.get<ast::Or>().arguments.emplace_back(std::move(implies.antecedent));
|
disjunction.get<ast::Or>().arguments.emplace_back(std::move(implies.antecedent));
|
||||||
else
|
else
|
||||||
@ -100,22 +118,22 @@ ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Fo
|
|||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
ast::Formula completePredicate(const ast::PredicateSignature &predicateSignature, std::vector<ast::ScopedFormula> &scopedFormulas)
|
ast::Formula completePredicate(ast::PredicateDeclaration &predicateDeclaration, std::vector<ast::ScopedFormula> &scopedFormulas)
|
||||||
{
|
{
|
||||||
// Create new set of parameters for the completed definition for the predicate
|
// Create new set of parameters for the completed definition for the predicate
|
||||||
ast::VariableDeclarationPointers parameters;
|
ast::VariableDeclarationPointers parameters;
|
||||||
parameters.reserve(predicateSignature.arity);
|
parameters.reserve(predicateDeclaration.arity());
|
||||||
|
|
||||||
std::vector<ast::Term> arguments;
|
std::vector<ast::Term> arguments;
|
||||||
arguments.reserve(predicateSignature.arity);
|
arguments.reserve(predicateDeclaration.arity());
|
||||||
|
|
||||||
for (size_t i = 0; i < predicateSignature.arity; i++)
|
for (size_t i = 0; i < predicateDeclaration.arity(); i++)
|
||||||
{
|
{
|
||||||
parameters.emplace_back(std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::Head));
|
parameters.emplace_back(std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::Head));
|
||||||
arguments.emplace_back(ast::Term::make<ast::Variable>(parameters.back().get()));
|
arguments.emplace_back(ast::Term::make<ast::Variable>(parameters.back().get()));
|
||||||
}
|
}
|
||||||
|
|
||||||
ast::Predicate predicateCopy(std::string(predicateSignature.name), std::move(arguments));
|
ast::Predicate predicateCopy(&predicateDeclaration, std::move(arguments));
|
||||||
|
|
||||||
auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicateCopy, parameters, scopedFormulas);
|
auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicateCopy, parameters, scopedFormulas);
|
||||||
auto completedFormulaQuantified = buildCompletedFormulaQuantified(std::move(predicateCopy), std::move(completedFormulaDisjunction));
|
auto completedFormulaQuantified = buildCompletedFormulaQuantified(std::move(predicateCopy), std::move(completedFormulaDisjunction));
|
||||||
@ -161,28 +179,27 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
|
|||||||
throw CompletionException("cannot perform completion, only single predicates and Booleans supported as formula consequent currently");
|
throw CompletionException("cannot perform completion, only single predicates and Booleans supported as formula consequent currently");
|
||||||
}
|
}
|
||||||
|
|
||||||
std::vector<ast::PredicateSignature> predicateSignatures;
|
std::sort(context.predicateDeclarations.begin(), context.predicateDeclarations.end(),
|
||||||
|
|
||||||
// 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 &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)
|
if (order != 0)
|
||||||
return (order < 0);
|
return (order < 0);
|
||||||
|
|
||||||
return lhs.arity < rhs.arity;
|
return lhs->arity() < rhs->arity();
|
||||||
});
|
});
|
||||||
|
|
||||||
std::vector<ast::Formula> completedFormulas;
|
std::vector<ast::Formula> completedFormulas;
|
||||||
|
|
||||||
// Complete predicates
|
// Complete predicates
|
||||||
for (const auto &predicateSignature : predicateSignatures)
|
for (auto &predicateDeclaration : context.predicateDeclarations)
|
||||||
completedFormulas.emplace_back(completePredicate(predicateSignature, scopedFormulas));
|
{
|
||||||
|
if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal)
|
||||||
|
continue;
|
||||||
|
|
||||||
|
completedFormulas.emplace_back(completePredicate(*predicateDeclaration, scopedFormulas));
|
||||||
|
}
|
||||||
|
|
||||||
// Complete integrity constraints
|
// Complete integrity constraints
|
||||||
for (auto &scopedFormula : scopedFormulas)
|
for (auto &scopedFormula : scopedFormulas)
|
||||||
@ -202,7 +219,7 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
|
|||||||
}
|
}
|
||||||
|
|
||||||
// Eliminate all predicates that should not be visible in the output
|
// Eliminate all predicates that should not be visible in the output
|
||||||
eliminateHiddenPredicates(predicateSignatures, completedFormulas, context);
|
eliminateHiddenPredicates(completedFormulas, context);
|
||||||
|
|
||||||
return completedFormulas;
|
return completedFormulas;
|
||||||
}
|
}
|
||||||
|
@ -78,7 +78,7 @@ struct ReplacePredicateInFormulaVisitor : public ast::RecursiveFormulaVisitor<Re
|
|||||||
{
|
{
|
||||||
static void accept(ast::Predicate &predicate, ast::Formula &formula, const PredicateReplacement &predicateReplacement)
|
static void accept(ast::Predicate &predicate, ast::Formula &formula, const PredicateReplacement &predicateReplacement)
|
||||||
{
|
{
|
||||||
if (!ast::matches(predicate, predicateReplacement.predicate))
|
if (predicate.declaration != predicateReplacement.predicate.declaration)
|
||||||
return;
|
return;
|
||||||
|
|
||||||
auto formulaReplacement = ast::prepareCopy(predicateReplacement.replacement);
|
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
|
// Detect whether a formula contains a circular dependency on a given predicate
|
||||||
struct DetectCircularDependcyVisitor : public ast::RecursiveFormulaVisitor<DetectCircularDependcyVisitor>
|
struct DetectCircularDependcyVisitor : public ast::RecursiveFormulaVisitor<DetectCircularDependcyVisitor>
|
||||||
{
|
{
|
||||||
static void accept(ast::Predicate &predicate, ast::Formula &, const ast::PredicateSignature &predicateSignature, bool &hasCircularDependency)
|
static void accept(ast::Predicate &predicate, ast::Formula &, const ast::PredicateDeclaration &predicateDeclaration, bool &hasCircularDependency)
|
||||||
{
|
{
|
||||||
if (ast::matches(predicate, predicateSignature))
|
if (predicate.declaration == &predicateDeclaration)
|
||||||
hasCircularDependency = true;
|
hasCircularDependency = true;
|
||||||
}
|
}
|
||||||
|
|
||||||
// Ignore all other types of expressions
|
// Ignore all other types of expressions
|
||||||
template<class T>
|
template<class T>
|
||||||
static void accept(T &, ast::Formula &, const ast::PredicateSignature &, bool &)
|
static void accept(T &, ast::Formula &, const ast::PredicateDeclaration &, bool &)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
@ -125,12 +125,12 @@ struct DetectCircularDependcyVisitor : public ast::RecursiveFormulaVisitor<Detec
|
|||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
// Finds the replacement for predicates of the form “p(X1, ..., Xn) <-> q(X1, ..., Xn)”
|
// Finds the replacement for predicates of the form “p(X1, ..., Xn) <-> q(X1, ..., Xn)”
|
||||||
PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Predicate &predicate)
|
PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Predicate &predicate)
|
||||||
{
|
{
|
||||||
// Declare variable used, only used in debug mode
|
// Declare variable used, only used in debug mode
|
||||||
(void)(predicateSignature);
|
(void)(predicateDeclaration);
|
||||||
|
|
||||||
assert(ast::matches(predicate, predicateSignature));
|
assert(predicate.declaration == &predicateDeclaration);
|
||||||
|
|
||||||
// Replace with “#true”
|
// Replace with “#true”
|
||||||
return {predicate, ast::Formula::make<ast::Boolean>(true)};
|
return {predicate, ast::Formula::make<ast::Boolean>(true)};
|
||||||
@ -139,13 +139,13 @@ PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSig
|
|||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
// Finds the replacement for predicates of the form “p(X1, ..., Xn) <-> not q(X1, ..., Xn)”
|
// Finds the replacement for predicates of the form “p(X1, ..., Xn) <-> not q(X1, ..., Xn)”
|
||||||
PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Not ¬_)
|
PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Not ¬_)
|
||||||
{
|
{
|
||||||
// Declare variable used, only used in debug mode
|
// Declare variable used, only used in debug mode
|
||||||
(void)(predicateSignature);
|
(void)(predicateDeclaration);
|
||||||
|
|
||||||
assert(not_.argument.is<ast::Predicate>());
|
assert(not_.argument.is<ast::Predicate>());
|
||||||
assert(ast::matches(not_.argument.get<ast::Predicate>(), predicateSignature));
|
assert(not_.argument.get<ast::Predicate>().declaration == &predicateDeclaration);
|
||||||
|
|
||||||
// Replace with “#false”
|
// Replace with “#false”
|
||||||
return {not_.argument.get<ast::Predicate>(), ast::Formula::make<ast::Boolean>(false)};
|
return {not_.argument.get<ast::Predicate>(), ast::Formula::make<ast::Boolean>(false)};
|
||||||
@ -154,13 +154,13 @@ PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSig
|
|||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
// Finds the replacement for predicates of the form “forall X1, ..., Xn (p(X1, ..., Xn) <-> ...)”
|
// Finds the replacement for predicates of the form “forall X1, ..., Xn (p(X1, ..., Xn) <-> ...)”
|
||||||
PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Biconditional &biconditional)
|
PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Biconditional &biconditional)
|
||||||
{
|
{
|
||||||
// Declare variable used, only used in debug mode
|
// Declare variable used, only used in debug mode
|
||||||
(void)(predicateSignature);
|
(void)(predicateDeclaration);
|
||||||
|
|
||||||
assert(biconditional.left.is<ast::Predicate>());
|
assert(biconditional.left.is<ast::Predicate>());
|
||||||
assert(ast::matches(biconditional.left.get<ast::Predicate>(), predicateSignature));
|
assert(biconditional.left.get<ast::Predicate>().declaration == &predicateDeclaration);
|
||||||
|
|
||||||
// TODO: avoid copy
|
// TODO: avoid copy
|
||||||
return {biconditional.left.get<ast::Predicate>(), ast::prepareCopy(biconditional.right)};
|
return {biconditional.left.get<ast::Predicate>(), ast::prepareCopy(biconditional.right)};
|
||||||
@ -169,77 +169,65 @@ PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSig
|
|||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
// Finds a replacement for a predicate that should be hidden
|
// Finds a replacement for a predicate that should be hidden
|
||||||
PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Formula &completedPredicateDefinition)
|
PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Formula &completedPredicateDefinition)
|
||||||
{
|
{
|
||||||
// TODO: refactor
|
// TODO: refactor
|
||||||
if (completedPredicateDefinition.is<ast::ForAll>())
|
if (completedPredicateDefinition.is<ast::ForAll>())
|
||||||
return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::ForAll>().argument);
|
return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::ForAll>().argument);
|
||||||
else if (completedPredicateDefinition.is<ast::Biconditional>())
|
else if (completedPredicateDefinition.is<ast::Biconditional>())
|
||||||
return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::Biconditional>());
|
return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::Biconditional>());
|
||||||
else if (completedPredicateDefinition.is<ast::Predicate>())
|
else if (completedPredicateDefinition.is<ast::Predicate>())
|
||||||
return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::Predicate>());
|
return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::Predicate>());
|
||||||
else if (completedPredicateDefinition.is<ast::Not>())
|
else if (completedPredicateDefinition.is<ast::Not>())
|
||||||
return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::Not>());
|
return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::Not>());
|
||||||
|
|
||||||
throw CompletionException("unsupported completed definition for predicate “" + predicateSignature.name + "/" + std::to_string(predicateSignature.arity) + "” for hiding predicates");
|
throw CompletionException("unsupported completed definition for predicate “" + predicateDeclaration.name + "/" + std::to_string(predicateDeclaration.arity()) + "” for hiding predicates");
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predicateSignatures, std::vector<ast::Formula> &completedFormulas, Context &context)
|
void eliminateHiddenPredicates(std::vector<ast::Formula> &completedFormulas, Context &context)
|
||||||
{
|
{
|
||||||
if (!context.visiblePredicateSignatures)
|
if (context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Visible)
|
||||||
{
|
{
|
||||||
context.logger.log(output::Priority::Debug) << "no predicates to be eliminated";
|
context.logger.log(output::Priority::Debug) << "no predicates to be eliminated";
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
||||||
auto &visiblePredicateSignatures = context.visiblePredicateSignatures.value();
|
assert(context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Hidden);
|
||||||
|
|
||||||
|
// TODO: get rid of index-wise matching of completed formulas and predicate declarations
|
||||||
|
size_t i = -1;
|
||||||
|
|
||||||
// Replace all occurrences of hidden predicates
|
// Replace all occurrences of hidden predicates
|
||||||
for (size_t i = 0; i < predicateSignatures.size(); i++)
|
for (auto &predicateDeclaration : context.predicateDeclarations)
|
||||||
{
|
{
|
||||||
auto &predicateSignature = predicateSignatures[i];
|
// Check that the predicate is used and not declared #external
|
||||||
|
if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal)
|
||||||
|
continue;
|
||||||
|
|
||||||
const auto matchesPredicateSignature =
|
i++;
|
||||||
[&](const auto &otherPredicateSignature)
|
|
||||||
{
|
|
||||||
return ast::matches(predicateSignature, otherPredicateSignature.predicateSignature);
|
|
||||||
};
|
|
||||||
|
|
||||||
const auto matchingVisiblePredicateSignature =
|
const auto isPredicateVisible =
|
||||||
std::find_if(visiblePredicateSignatures.begin(), visiblePredicateSignatures.end(), matchesPredicateSignature);
|
(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 the predicate ought to be visible, don’t eliminate it
|
||||||
if (matchingVisiblePredicateSignature != visiblePredicateSignatures.end())
|
if (isPredicateVisible)
|
||||||
{
|
|
||||||
matchingVisiblePredicateSignature->used = true;
|
|
||||||
continue;
|
continue;
|
||||||
}
|
|
||||||
|
|
||||||
// Check that the predicate is not declared #external
|
context.logger.log(output::Priority::Debug) << "eliminating “" << predicateDeclaration->name << "/" << predicateDeclaration->arity() << "”";
|
||||||
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];
|
const auto &completedPredicateDefinition = completedFormulas[i];
|
||||||
auto replacement = findReplacement(predicateSignature, completedPredicateDefinition);
|
auto replacement = findReplacement(*predicateDeclaration, completedPredicateDefinition);
|
||||||
|
|
||||||
bool hasCircularDependency = false;
|
bool hasCircularDependency = false;
|
||||||
replacement.replacement.accept(DetectCircularDependcyVisitor(), replacement.replacement, predicateSignature, hasCircularDependency);
|
replacement.replacement.accept(DetectCircularDependcyVisitor(), replacement.replacement, *predicateDeclaration, hasCircularDependency);
|
||||||
|
|
||||||
if (hasCircularDependency)
|
if (hasCircularDependency)
|
||||||
{
|
{
|
||||||
context.logger.log(output::Priority::Warning) << "cannot hide predicate “" << predicateSignature.name << "/" << predicateSignature.arity << "” due to circular dependency";
|
context.logger.log(output::Priority::Warning) << "cannot hide predicate “" << predicateDeclaration->name << "/" << predicateDeclaration->arity() << "” due to circular dependency";
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
332
src/anthem/IntegerVariableDetection.cpp
Normal file
332
src/anthem/IntegerVariableDetection.cpp
Normal file
@ -0,0 +1,332 @@
|
|||||||
|
#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,8 +4,9 @@
|
|||||||
|
|
||||||
#include <anthem/ASTCopy.h>
|
#include <anthem/ASTCopy.h>
|
||||||
#include <anthem/Equality.h>
|
#include <anthem/Equality.h>
|
||||||
#include <anthem/output/AST.h>
|
|
||||||
#include <anthem/SimplificationVisitors.h>
|
#include <anthem/SimplificationVisitors.h>
|
||||||
|
#include <anthem/Type.h>
|
||||||
|
#include <anthem/output/AST.h>
|
||||||
|
|
||||||
namespace anthem
|
namespace anthem
|
||||||
{
|
{
|
||||||
@ -100,7 +101,7 @@ struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<Rep
|
|||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
template<class SimplificationRule>
|
template<class SimplificationRule>
|
||||||
SimplificationResult simplify(ast::Formula &formula)
|
OperationResult simplify(ast::Formula &formula)
|
||||||
{
|
{
|
||||||
return SimplificationRule::apply(formula);
|
return SimplificationRule::apply(formula);
|
||||||
}
|
}
|
||||||
@ -108,10 +109,10 @@ SimplificationResult simplify(ast::Formula &formula)
|
|||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
template<class FirstSimplificationRule, class SecondSimplificationRule, class... OtherSimplificationRules>
|
template<class FirstSimplificationRule, class SecondSimplificationRule, class... OtherSimplificationRules>
|
||||||
SimplificationResult simplify(ast::Formula &formula)
|
OperationResult simplify(ast::Formula &formula)
|
||||||
{
|
{
|
||||||
if (simplify<FirstSimplificationRule>(formula) == SimplificationResult::Simplified)
|
if (simplify<FirstSimplificationRule>(formula) == OperationResult::Changed)
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
|
|
||||||
return simplify<SecondSimplificationRule, OtherSimplificationRules...>(formula);
|
return simplify<SecondSimplificationRule, OtherSimplificationRules...>(formula);
|
||||||
}
|
}
|
||||||
@ -122,19 +123,19 @@ struct SimplificationRuleExistsWithoutQuantifiedVariables
|
|||||||
{
|
{
|
||||||
static constexpr const auto Description = "exists () (F) === F";
|
static constexpr const auto Description = "exists () (F) === F";
|
||||||
|
|
||||||
static SimplificationResult apply(ast::Formula &formula)
|
static OperationResult apply(ast::Formula &formula)
|
||||||
{
|
{
|
||||||
if (!formula.is<ast::Exists>())
|
if (!formula.is<ast::Exists>())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
auto &exists = formula.get<ast::Exists>();
|
auto &exists = formula.get<ast::Exists>();
|
||||||
|
|
||||||
if (!exists.variables.empty())
|
if (!exists.variables.empty())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
formula = std::move(exists.argument);
|
formula = std::move(exists.argument);
|
||||||
|
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
@ -144,20 +145,20 @@ struct SimplificationRuleTrivialAssignmentInExists
|
|||||||
{
|
{
|
||||||
static constexpr const auto Description = "exists X (X = Y) === #true";
|
static constexpr const auto Description = "exists X (X = Y) === #true";
|
||||||
|
|
||||||
static SimplificationResult apply(ast::Formula &formula)
|
static OperationResult apply(ast::Formula &formula)
|
||||||
{
|
{
|
||||||
if (!formula.is<ast::Exists>())
|
if (!formula.is<ast::Exists>())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
const auto &exists = formula.get<ast::Exists>();
|
const auto &exists = formula.get<ast::Exists>();
|
||||||
|
|
||||||
if (!exists.argument.is<ast::Comparison>())
|
if (!exists.argument.is<ast::Comparison>())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
const auto &comparison = exists.argument.get<ast::Comparison>();
|
const auto &comparison = exists.argument.get<ast::Comparison>();
|
||||||
|
|
||||||
if (comparison.operator_ != ast::Comparison::Operator::Equal)
|
if (comparison.operator_ != ast::Comparison::Operator::Equal)
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
const auto matchingAssignment = std::find_if(exists.variables.cbegin(), exists.variables.cend(),
|
const auto matchingAssignment = std::find_if(exists.variables.cbegin(), exists.variables.cend(),
|
||||||
[&](const auto &variableDeclaration)
|
[&](const auto &variableDeclaration)
|
||||||
@ -167,11 +168,11 @@ struct SimplificationRuleTrivialAssignmentInExists
|
|||||||
});
|
});
|
||||||
|
|
||||||
if (matchingAssignment == exists.variables.cend())
|
if (matchingAssignment == exists.variables.cend())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
formula = ast::Formula::make<ast::Boolean>(true);
|
formula = ast::Formula::make<ast::Boolean>(true);
|
||||||
|
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
@ -181,20 +182,20 @@ struct SimplificationRuleAssignmentInExists
|
|||||||
{
|
{
|
||||||
static constexpr const auto Description = "exists X (X = t and F(X)) === exists () (F(t))";
|
static constexpr const auto Description = "exists X (X = t and F(X)) === exists () (F(t))";
|
||||||
|
|
||||||
static SimplificationResult apply(ast::Formula &formula)
|
static OperationResult apply(ast::Formula &formula)
|
||||||
{
|
{
|
||||||
if (!formula.is<ast::Exists>())
|
if (!formula.is<ast::Exists>())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
auto &exists = formula.get<ast::Exists>();
|
auto &exists = formula.get<ast::Exists>();
|
||||||
|
|
||||||
if (!exists.argument.is<ast::And>())
|
if (!exists.argument.is<ast::And>())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
auto &and_ = exists.argument.get<ast::And>();
|
auto &and_ = exists.argument.get<ast::And>();
|
||||||
auto &arguments = and_.arguments;
|
auto &arguments = and_.arguments;
|
||||||
|
|
||||||
auto simplificationResult = SimplificationResult::Unchanged;
|
auto simplificationResult = OperationResult::Unchanged;
|
||||||
|
|
||||||
for (auto i = exists.variables.begin(); i != exists.variables.end();)
|
for (auto i = exists.variables.begin(); i != exists.variables.end();)
|
||||||
{
|
{
|
||||||
@ -225,7 +226,7 @@ struct SimplificationRuleAssignmentInExists
|
|||||||
arguments.erase(j);
|
arguments.erase(j);
|
||||||
|
|
||||||
wasVariableReplaced = true;
|
wasVariableReplaced = true;
|
||||||
simplificationResult = SimplificationResult::Simplified;
|
simplificationResult = OperationResult::Changed;
|
||||||
|
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
@ -249,19 +250,19 @@ struct SimplificationRuleEmptyConjunction
|
|||||||
{
|
{
|
||||||
static constexpr const auto Description = "[empty conjunction] === #true";
|
static constexpr const auto Description = "[empty conjunction] === #true";
|
||||||
|
|
||||||
static SimplificationResult apply(ast::Formula &formula)
|
static OperationResult apply(ast::Formula &formula)
|
||||||
{
|
{
|
||||||
if (!formula.is<ast::And>())
|
if (!formula.is<ast::And>())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
auto &and_ = formula.get<ast::And>();
|
auto &and_ = formula.get<ast::And>();
|
||||||
|
|
||||||
if (!and_.arguments.empty())
|
if (!and_.arguments.empty())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
formula = ast::Formula::make<ast::Boolean>(true);
|
formula = ast::Formula::make<ast::Boolean>(true);
|
||||||
|
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
@ -271,19 +272,19 @@ struct SimplificationRuleOneElementConjunction
|
|||||||
{
|
{
|
||||||
static constexpr const auto Description = "[conjunction of only F] === F";
|
static constexpr const auto Description = "[conjunction of only F] === F";
|
||||||
|
|
||||||
static SimplificationResult apply(ast::Formula &formula)
|
static OperationResult apply(ast::Formula &formula)
|
||||||
{
|
{
|
||||||
if (!formula.is<ast::And>())
|
if (!formula.is<ast::And>())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
auto &and_ = formula.get<ast::And>();
|
auto &and_ = formula.get<ast::And>();
|
||||||
|
|
||||||
if (and_.arguments.size() != 1)
|
if (and_.arguments.size() != 1)
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
formula = std::move(and_.arguments.front());
|
formula = std::move(and_.arguments.front());
|
||||||
|
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
@ -293,19 +294,19 @@ struct SimplificationRuleTrivialExists
|
|||||||
{
|
{
|
||||||
static constexpr const auto Description = "exists ... ([#true/#false]) === [#true/#false]";
|
static constexpr const auto Description = "exists ... ([#true/#false]) === [#true/#false]";
|
||||||
|
|
||||||
static SimplificationResult apply(ast::Formula &formula)
|
static OperationResult apply(ast::Formula &formula)
|
||||||
{
|
{
|
||||||
if (!formula.is<ast::Exists>())
|
if (!formula.is<ast::Exists>())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
auto &exists = formula.get<ast::Exists>();
|
auto &exists = formula.get<ast::Exists>();
|
||||||
|
|
||||||
if (!exists.argument.is<ast::Boolean>())
|
if (!exists.argument.is<ast::Boolean>())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
formula = std::move(exists.argument);
|
formula = std::move(exists.argument);
|
||||||
|
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
@ -315,21 +316,21 @@ struct SimplificationRuleInWithPrimitiveArguments
|
|||||||
{
|
{
|
||||||
static constexpr const auto Description = "[primitive A] in [primitive B] === A = B";
|
static constexpr const auto Description = "[primitive A] in [primitive B] === A = B";
|
||||||
|
|
||||||
static SimplificationResult apply(ast::Formula &formula)
|
static OperationResult apply(ast::Formula &formula)
|
||||||
{
|
{
|
||||||
if (!formula.is<ast::In>())
|
if (!formula.is<ast::In>())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
auto &in = formula.get<ast::In>();
|
auto &in = formula.get<ast::In>();
|
||||||
|
|
||||||
assert(ast::isPrimitive(in.element));
|
assert(ast::isPrimitive(in.element));
|
||||||
|
|
||||||
if (!ast::isPrimitive(in.element) || !ast::isPrimitive(in.set))
|
if (!ast::isPrimitive(in.element) || !ast::isPrimitive(in.set))
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
|
formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
|
||||||
|
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
@ -339,10 +340,10 @@ struct SimplificationRuleSubsumptionInBiconditionals
|
|||||||
{
|
{
|
||||||
static constexpr const auto Description = "(F <-> (F and G)) === (F -> G)";
|
static constexpr const auto Description = "(F <-> (F and G)) === (F -> G)";
|
||||||
|
|
||||||
static SimplificationResult apply(ast::Formula &formula)
|
static OperationResult apply(ast::Formula &formula)
|
||||||
{
|
{
|
||||||
if (!formula.is<ast::Biconditional>())
|
if (!formula.is<ast::Biconditional>())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
auto &biconditional = formula.get<ast::Biconditional>();
|
auto &biconditional = formula.get<ast::Biconditional>();
|
||||||
|
|
||||||
@ -353,7 +354,7 @@ struct SimplificationRuleSubsumptionInBiconditionals
|
|||||||
const auto rightIsAnd = biconditional.right.is<ast::And>();
|
const auto rightIsAnd = biconditional.right.is<ast::And>();
|
||||||
|
|
||||||
if (!(leftIsPredicate && rightIsAnd) && !(rightIsPredicate && leftIsAnd))
|
if (!(leftIsPredicate && rightIsAnd) && !(rightIsPredicate && leftIsAnd))
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
auto &predicateSide = (leftIsPredicate ? biconditional.left : biconditional.right);
|
auto &predicateSide = (leftIsPredicate ? biconditional.left : biconditional.right);
|
||||||
auto &andSide = (leftIsPredicate ? biconditional.right : biconditional.left);
|
auto &andSide = (leftIsPredicate ? biconditional.right : biconditional.left);
|
||||||
@ -363,17 +364,17 @@ struct SimplificationRuleSubsumptionInBiconditionals
|
|||||||
std::find_if(and_.arguments.cbegin(), and_.arguments.cend(),
|
std::find_if(and_.arguments.cbegin(), and_.arguments.cend(),
|
||||||
[&](const auto &argument)
|
[&](const auto &argument)
|
||||||
{
|
{
|
||||||
return (ast::equal(predicateSide, argument) == ast::Tristate::True);
|
return (ast::equal(predicateSide, argument) == Tristate::True);
|
||||||
});
|
});
|
||||||
|
|
||||||
if (matchingPredicate == and_.arguments.cend())
|
if (matchingPredicate == and_.arguments.cend())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
and_.arguments.erase(matchingPredicate);
|
and_.arguments.erase(matchingPredicate);
|
||||||
|
|
||||||
formula = ast::Formula::make<ast::Implies>(std::move(predicateSide), std::move(andSide));
|
formula = ast::Formula::make<ast::Implies>(std::move(predicateSide), std::move(andSide));
|
||||||
|
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
@ -383,21 +384,21 @@ struct SimplificationRuleDoubleNegation
|
|||||||
{
|
{
|
||||||
static constexpr const auto Description = "not not F === F";
|
static constexpr const auto Description = "not not F === F";
|
||||||
|
|
||||||
static SimplificationResult apply(ast::Formula &formula)
|
static OperationResult apply(ast::Formula &formula)
|
||||||
{
|
{
|
||||||
if (!formula.is<ast::Not>())
|
if (!formula.is<ast::Not>())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
auto ¬_ = formula.get<ast::Not>();
|
auto ¬_ = formula.get<ast::Not>();
|
||||||
|
|
||||||
if (!not_.argument.is<ast::Not>())
|
if (!not_.argument.is<ast::Not>())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
auto ¬Not = not_.argument.get<ast::Not>();
|
auto ¬Not = not_.argument.get<ast::Not>();
|
||||||
|
|
||||||
formula = std::move(notNot.argument);
|
formula = std::move(notNot.argument);
|
||||||
|
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
@ -407,15 +408,15 @@ struct SimplificationRuleDeMorganForConjunctions
|
|||||||
{
|
{
|
||||||
static constexpr const auto Description = "(not (F and G)) === (not F or not G)";
|
static constexpr const auto Description = "(not (F and G)) === (not F or not G)";
|
||||||
|
|
||||||
static SimplificationResult apply(ast::Formula &formula)
|
static OperationResult apply(ast::Formula &formula)
|
||||||
{
|
{
|
||||||
if (!formula.is<ast::Not>())
|
if (!formula.is<ast::Not>())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
auto ¬_ = formula.get<ast::Not>();
|
auto ¬_ = formula.get<ast::Not>();
|
||||||
|
|
||||||
if (!not_.argument.is<ast::And>())
|
if (!not_.argument.is<ast::And>())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
auto &and_ = not_.argument.get<ast::And>();
|
auto &and_ = not_.argument.get<ast::And>();
|
||||||
|
|
||||||
@ -424,7 +425,7 @@ struct SimplificationRuleDeMorganForConjunctions
|
|||||||
|
|
||||||
formula = ast::Formula::make<ast::Or>(std::move(and_.arguments));
|
formula = ast::Formula::make<ast::Or>(std::move(and_.arguments));
|
||||||
|
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
@ -434,21 +435,21 @@ struct SimplificationRuleImplicationFromDisjunction
|
|||||||
{
|
{
|
||||||
static constexpr const auto Description = "(not F or G) === (F -> G)";
|
static constexpr const auto Description = "(not F or G) === (F -> G)";
|
||||||
|
|
||||||
static SimplificationResult apply(ast::Formula &formula)
|
static OperationResult apply(ast::Formula &formula)
|
||||||
{
|
{
|
||||||
if (!formula.is<ast::Or>())
|
if (!formula.is<ast::Or>())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
auto &or_ = formula.get<ast::Or>();
|
auto &or_ = formula.get<ast::Or>();
|
||||||
|
|
||||||
if (or_.arguments.size() != 2)
|
if (or_.arguments.size() != 2)
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
const auto leftIsNot = or_.arguments[0].is<ast::Not>();
|
const auto leftIsNot = or_.arguments[0].is<ast::Not>();
|
||||||
const auto rightIsNot = or_.arguments[1].is<ast::Not>();
|
const auto rightIsNot = or_.arguments[1].is<ast::Not>();
|
||||||
|
|
||||||
if (leftIsNot == rightIsNot)
|
if (leftIsNot == rightIsNot)
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
auto &negativeSide = leftIsNot ? or_.arguments[0] : or_.arguments[1];
|
auto &negativeSide = leftIsNot ? or_.arguments[0] : or_.arguments[1];
|
||||||
auto &positiveSide = leftIsNot ? or_.arguments[1] : or_.arguments[0];
|
auto &positiveSide = leftIsNot ? or_.arguments[1] : or_.arguments[0];
|
||||||
@ -460,7 +461,7 @@ struct SimplificationRuleImplicationFromDisjunction
|
|||||||
|
|
||||||
formula = ast::Formula::make<ast::Implies>(std::move(negativeSideArgument), std::move(positiveSide));
|
formula = ast::Formula::make<ast::Implies>(std::move(negativeSideArgument), std::move(positiveSide));
|
||||||
|
|
||||||
return SimplificationResult::Simplified;
|
return OperationResult::Changed;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
@ -470,15 +471,15 @@ struct SimplificationRuleNegatedComparison
|
|||||||
{
|
{
|
||||||
static constexpr const auto Description = "(not F [comparison] G) === (F [negated comparison] G)";
|
static constexpr const auto Description = "(not F [comparison] G) === (F [negated comparison] G)";
|
||||||
|
|
||||||
static SimplificationResult apply(ast::Formula &formula)
|
static OperationResult apply(ast::Formula &formula)
|
||||||
{
|
{
|
||||||
if (!formula.is<ast::Not>())
|
if (!formula.is<ast::Not>())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
auto ¬_ = formula.get<ast::Not>();
|
auto ¬_ = formula.get<ast::Not>();
|
||||||
|
|
||||||
if (!not_.argument.is<ast::Comparison>())
|
if (!not_.argument.is<ast::Comparison>())
|
||||||
return SimplificationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
auto &comparison = not_.argument.get<ast::Comparison>();
|
auto &comparison = not_.argument.get<ast::Comparison>();
|
||||||
|
|
||||||
@ -506,7 +507,35 @@ struct SimplificationRuleNegatedComparison
|
|||||||
|
|
||||||
formula = std::move(comparison);
|
formula = std::move(comparison);
|
||||||
|
|
||||||
return SimplificationResult::Simplified;
|
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;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
@ -526,7 +555,8 @@ const auto simplifyWithDefaultRules =
|
|||||||
SimplificationRuleSubsumptionInBiconditionals,
|
SimplificationRuleSubsumptionInBiconditionals,
|
||||||
SimplificationRuleDeMorganForConjunctions,
|
SimplificationRuleDeMorganForConjunctions,
|
||||||
SimplificationRuleImplicationFromDisjunction,
|
SimplificationRuleImplicationFromDisjunction,
|
||||||
SimplificationRuleNegatedComparison
|
SimplificationRuleNegatedComparison,
|
||||||
|
SimplificationRuleIntegerSetInclusion
|
||||||
>;
|
>;
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
@ -535,7 +565,7 @@ const auto simplifyWithDefaultRules =
|
|||||||
struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<SimplifyFormulaVisitor>
|
struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<SimplifyFormulaVisitor>
|
||||||
{
|
{
|
||||||
// Do nothing for all other types of expressions
|
// Do nothing for all other types of expressions
|
||||||
static SimplificationResult accept(ast::Formula &formula)
|
static OperationResult accept(ast::Formula &formula)
|
||||||
{
|
{
|
||||||
return simplifyWithDefaultRules(formula);
|
return simplifyWithDefaultRules(formula);
|
||||||
}
|
}
|
||||||
@ -545,7 +575,7 @@ struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<Simplif
|
|||||||
|
|
||||||
void simplify(ast::Formula &formula)
|
void simplify(ast::Formula &formula)
|
||||||
{
|
{
|
||||||
while (formula.accept(SimplifyFormulaVisitor(), formula) == SimplificationResult::Simplified);
|
while (formula.accept(SimplifyFormulaVisitor(), formula) == OperationResult::Changed);
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
@ -8,6 +8,7 @@
|
|||||||
|
|
||||||
#include <anthem/Completion.h>
|
#include <anthem/Completion.h>
|
||||||
#include <anthem/Context.h>
|
#include <anthem/Context.h>
|
||||||
|
#include <anthem/IntegerVariableDetection.h>
|
||||||
#include <anthem/Simplification.h>
|
#include <anthem/Simplification.h>
|
||||||
#include <anthem/StatementVisitor.h>
|
#include <anthem/StatementVisitor.h>
|
||||||
#include <anthem/output/AST.h>
|
#include <anthem/output/AST.h>
|
||||||
@ -67,10 +68,10 @@ void translate(const char *fileName, std::istream &stream, Context &context)
|
|||||||
for (auto &scopedFormula : scopedFormulas)
|
for (auto &scopedFormula : scopedFormulas)
|
||||||
simplify(scopedFormula.formula);
|
simplify(scopedFormula.formula);
|
||||||
|
|
||||||
if (context.visiblePredicateSignatures)
|
if (context.showStatementsUsed)
|
||||||
context.logger.log(output::Priority::Warning) << "#show statements are ignored because completion is not enabled";
|
context.logger.log(output::Priority::Warning) << "#show statements are ignored because completion is not enabled";
|
||||||
|
|
||||||
if (context.externalPredicateSignatures)
|
if (context.externalStatementsUsed)
|
||||||
context.logger.log(output::Priority::Warning) << "#external statements are ignored because completion is not enabled";
|
context.logger.log(output::Priority::Warning) << "#external statements are ignored because completion is not enabled";
|
||||||
|
|
||||||
for (const auto &scopedFormula : scopedFormulas)
|
for (const auto &scopedFormula : scopedFormulas)
|
||||||
@ -85,25 +86,33 @@ void translate(const char *fileName, std::istream &stream, Context &context)
|
|||||||
// Perform completion
|
// Perform completion
|
||||||
auto completedFormulas = complete(std::move(scopedFormulas), context);
|
auto completedFormulas = complete(std::move(scopedFormulas), context);
|
||||||
|
|
||||||
|
for (const auto &predicateDeclaration : context.predicateDeclarations)
|
||||||
|
{
|
||||||
|
if (predicateDeclaration->isUsed)
|
||||||
|
continue;
|
||||||
|
|
||||||
// Check for #show statements with undeclared predicates
|
// Check for #show statements with undeclared predicates
|
||||||
if (context.visiblePredicateSignatures)
|
if (predicateDeclaration->visibility != ast::PredicateDeclaration::Visibility::Default)
|
||||||
for (const auto &predicateSignature : context.visiblePredicateSignatures.value())
|
|
||||||
if (!predicateSignature.used)
|
|
||||||
context.logger.log(output::Priority::Warning)
|
context.logger.log(output::Priority::Warning)
|
||||||
<< "#show declaration of “"
|
<< "#show declaration of “"
|
||||||
<< predicateSignature.predicateSignature.name
|
<< predicateDeclaration->name
|
||||||
<< "/" << predicateSignature.predicateSignature.arity
|
<< "/"
|
||||||
<< "” does not match any eligible predicate";
|
<< predicateDeclaration->arity()
|
||||||
|
<< "” does not match any declared predicate";
|
||||||
|
|
||||||
// Check for #external statements with undeclared predicates
|
// Check for #external statements with undeclared predicates
|
||||||
if (context.externalPredicateSignatures)
|
if (predicateDeclaration->isExternal && !predicateDeclaration->isUsed)
|
||||||
for (const auto &predicateSignature : context.externalPredicateSignatures.value())
|
|
||||||
if (!predicateSignature.used)
|
|
||||||
context.logger.log(output::Priority::Warning)
|
context.logger.log(output::Priority::Warning)
|
||||||
<< "#external declaration of “"
|
<< "#external declaration of “"
|
||||||
<< predicateSignature.predicateSignature.name
|
<< predicateDeclaration->name
|
||||||
<< "/" << predicateSignature.predicateSignature.arity
|
<< "/"
|
||||||
<< "” does not match any eligible predicate";
|
<< predicateDeclaration->arity()
|
||||||
|
<< "” does not match any declared predicate";
|
||||||
|
}
|
||||||
|
|
||||||
|
// Detect integer variables
|
||||||
|
if (context.performIntegerDetection)
|
||||||
|
detectIntegerVariables(completedFormulas);
|
||||||
|
|
||||||
// Simplify output if specified
|
// Simplify output if specified
|
||||||
if (context.performSimplification)
|
if (context.performSimplification)
|
||||||
@ -117,6 +126,38 @@ void translate(const char *fileName, std::istream &stream, Context &context)
|
|||||||
ast::print(context.logger.outputStream(), completedFormula, printContext);
|
ast::print(context.logger.outputStream(), completedFormula, printContext);
|
||||||
context.logger.outputStream() << std::endl;
|
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);
|
anthem::translate("input", input, context);
|
||||||
|
|
||||||
CHECK(output.str() ==
|
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")
|
SECTION("useless implications")
|
||||||
@ -152,8 +152,8 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
|
|||||||
|
|
||||||
CHECK(output.str() ==
|
CHECK(output.str() ==
|
||||||
"forall V1 (covered(V1) <-> exists U1 in(V1, U1))\n"
|
"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 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 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");
|
"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.";
|
input << "adj(X, Y) :- X = 1..n, Y = 1..n, |X - Y| = 1.";
|
||||||
anthem::translate("input", input, context);
|
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
|
// TODO: simplify further
|
||||||
CHECK(output.str() ==
|
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")
|
SECTION("simple propositions are hidden correctly")
|
||||||
|
117
tests/TestIntegerDetection.cpp
Normal file
117
tests/TestIntegerDetection.cpp
Normal file
@ -0,0 +1,117 @@
|
|||||||
|
#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.";
|
input << ":- not covered(I), I = 1..n.";
|
||||||
anthem::translate("input", input, context);
|
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")
|
SECTION("comparisons")
|
||||||
@ -50,4 +50,34 @@ TEST_CASE("[simplification] Rules are simplified correctly", "[simplification]")
|
|||||||
|
|
||||||
CHECK(output.str() == "(U1 > U2 -> #false)\n");
|
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).";
|
input << "p(1..5).";
|
||||||
anthem::translate("input", input, context);
|
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")
|
SECTION("simple example 2")
|
||||||
@ -32,7 +32,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
|
|||||||
input << "p(N) :- N = 1..5.";
|
input << "p(N) :- N = 1..5.";
|
||||||
anthem::translate("input", input, context);
|
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")
|
SECTION("simple example 3")
|
||||||
@ -48,7 +48,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
|
|||||||
input << "p(N, 1, 2) :- N = 1..5.";
|
input << "p(N, 1, 2) :- N = 1..5.";
|
||||||
anthem::translate("input", input, context);
|
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")
|
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.";
|
input << "q(3, N); p(N, 1, 2) :- N = 1..5.";
|
||||||
anthem::translate("input", input, context);
|
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)")
|
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.";
|
input << "q(3, N), p(N, 1, 2) :- N = 1..5.";
|
||||||
anthem::translate("input", input, context);
|
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")
|
SECTION("escaping conflicting variable names")
|
||||||
@ -98,7 +98,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
|
|||||||
input << ":- not p(I), I = 1..n.";
|
input << ":- not p(I), I = 1..n.";
|
||||||
anthem::translate("input", input, context);
|
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)")
|
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).";
|
input << "p(X, 1..10) :- q(X, 6..12).";
|
||||||
anthem::translate("input", input, context);
|
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")
|
SECTION("intervals with variable")
|
||||||
@ -186,7 +186,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
|
|||||||
input << ":- q(N), 1 = 1..N.";
|
input << ":- q(N), 1 = 1..N.";
|
||||||
anthem::translate("input", input, context);
|
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")
|
SECTION("intervals with two variables")
|
||||||
@ -194,7 +194,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
|
|||||||
input << ":- q(M, N), M = 1..N.";
|
input << ":- q(M, N), M = 1..N.";
|
||||||
anthem::translate("input", input, context);
|
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")
|
SECTION("comparisons")
|
||||||
@ -262,7 +262,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
|
|||||||
anthem::translate("input", input, context);
|
anthem::translate("input", input, context);
|
||||||
|
|
||||||
// TODO: eliminate V5: not needed
|
// 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")
|
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.";
|
input << "p(N, N ** N) :- N = 1..n.";
|
||||||
anthem::translate("input", input, context);
|
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");
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
73
tests/TestUnsupported.cpp
Normal file
73
tests/TestUnsupported.cpp
Normal file
@ -0,0 +1,73 @@
|
|||||||
|
#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
Block a user