Compare commits
36 Commits
develop
...
v0.1.9-rc.
Author | SHA1 | Date |
---|---|---|
Patrick Lühne | c4a457e9d8 | |
Patrick Lühne | ea885f5fdb | |
Patrick Lühne | 92cd114cf8 | |
Patrick Lühne | 2b62c6227d | |
Patrick Lühne | 529aec15af | |
Patrick Lühne | d950b8ec1a | |
Patrick Lühne | 97190ace71 | |
Patrick Lühne | d6a811e363 | |
Patrick Lühne | b1ca027de5 | |
Patrick Lühne | f190c28ea5 | |
Patrick Lühne | 28dbd407e2 | |
Patrick Lühne | 9c792ff079 | |
Patrick Lühne | f65d4dbbd8 | |
Patrick Lühne | 8f3ff23f38 | |
Patrick Lühne | 03c22d00f5 | |
Patrick Lühne | a9b00dfb7c | |
Patrick Lühne | d1ee6eca19 | |
Patrick Lühne | aedb7e9bbd | |
Patrick Lühne | 8b8dd1b57e | |
Patrick Lühne | 5bda14342b | |
Patrick Lühne | 2f54b7d60e | |
Patrick Lühne | 2245e139b2 | |
Patrick Lühne | 7ba48044ee | |
Patrick Lühne | 862d03881a | |
Patrick Lühne | 7bde7c498f | |
Patrick Lühne | 159717f51c | |
Patrick Lühne | 89aec98942 | |
Patrick Lühne | 55f7fd4ff3 | |
Patrick Lühne | ae918a0846 | |
Patrick Lühne | f48802842e | |
Patrick Lühne | b5b05b766c | |
Patrick Lühne | 165f6ac059 | |
Patrick Lühne | 504f7da4c3 | |
Patrick Lühne | d2b48f9679 | |
Patrick Lühne | 2372eb24c4 | |
Patrick Lühne | 87dcd6ee93 |
|
@ -1,6 +1,13 @@
|
||||||
# Change Log
|
# Change Log
|
||||||
|
|
||||||
## (unreleased)
|
## 0.1.9 RC 3 (2018-04-22)
|
||||||
|
|
||||||
|
### Features
|
||||||
|
|
||||||
|
* optional detection of integer variables and integer predicate parameters
|
||||||
|
* command-line option `--detect-integers` to enable integer variable detection
|
||||||
|
* support for declaring functions integer with the `#external` directive
|
||||||
|
* new simplification rule applying to integer variables
|
||||||
|
|
||||||
## 0.1.8 (2018-04-20)
|
## 0.1.8 (2018-04-20)
|
||||||
|
|
||||||
|
|
|
@ -18,6 +18,7 @@ int main(int argc, char **argv)
|
||||||
("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")
|
("s,simplify", "Simplify the output")
|
||||||
("c,complete", "Perform completion")
|
("c,complete", "Perform completion")
|
||||||
|
("d,detect-integers", "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"));
|
||||||
|
@ -50,6 +51,7 @@ int main(int argc, char **argv)
|
||||||
|
|
||||||
context.performSimplification = (parseResult.count("simplify") > 0);
|
context.performSimplification = (parseResult.count("simplify") > 0);
|
||||||
context.performCompletion = (parseResult.count("complete") > 0);
|
context.performCompletion = (parseResult.count("complete") > 0);
|
||||||
|
context.performIntegerDetection = (parseResult.count("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-rc.3" << std::endl;
|
||||||
return EXIT_SUCCESS;
|
return EXIT_SUCCESS;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -1,3 +1,6 @@
|
||||||
|
#show p/2.
|
||||||
|
%#external integer(n(0)).
|
||||||
|
|
||||||
{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 +11,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,4 +1,5 @@
|
||||||
#show prime/1.
|
#show prime/1.
|
||||||
|
%#external integer(n(0)).
|
||||||
|
|
||||||
composite(I * J) :- I = 2..n, J = 2..n.
|
composite(I * J) :- I = 2..n, J = 2..n.
|
||||||
prime(N) :- N = 2..n, not composite(N).
|
prime(N) :- N = 2..n, not composite(N).
|
||||||
|
|
|
@ -1,7 +1,9 @@
|
||||||
|
#show in/2.
|
||||||
|
%#external integer(n(0)).
|
||||||
|
%#external integer(r(0)).
|
||||||
|
|
||||||
{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.
|
|
||||||
|
|
|
@ -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
|
||||||
|
|
|
@ -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());
|
||||||
|
@ -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())
|
||||||
|
|
|
@ -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);
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
|
|
@ -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");
|
||||||
|
|
|
@ -0,0 +1,166 @@
|
||||||
|
#ifndef __ANTHEM__ARITHMETICS_H
|
||||||
|
#define __ANTHEM__ARITHMETICS_H
|
||||||
|
|
||||||
|
#include <anthem/AST.h>
|
||||||
|
#include <anthem/Utils.h>
|
||||||
|
|
||||||
|
namespace anthem
|
||||||
|
{
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
//
|
||||||
|
// Arithmetics
|
||||||
|
//
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
struct DefaultVariableDomainAccessor
|
||||||
|
{
|
||||||
|
Domain operator()(const ast::Variable &variable)
|
||||||
|
{
|
||||||
|
return variable.declaration->domain;
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
template <class VariableDomainAccessor = DefaultVariableDomainAccessor, class... Arguments>
|
||||||
|
Type type(const ast::Term &term, 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
|
||||||
{
|
{
|
||||||
|
|
||||||
|
@ -23,6 +16,60 @@ constexpr const auto UserVariablePrefix = "U";
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
enum class Tristate
|
||||||
|
{
|
||||||
|
True,
|
||||||
|
False,
|
||||||
|
Unknown,
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
enum class EvaluationResult
|
||||||
|
{
|
||||||
|
True,
|
||||||
|
False,
|
||||||
|
Unknown,
|
||||||
|
Error,
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
enum class OperationResult
|
||||||
|
{
|
||||||
|
Unchanged,
|
||||||
|
Changed,
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
enum class Domain
|
||||||
|
{
|
||||||
|
Noninteger,
|
||||||
|
Integer,
|
||||||
|
Unknown,
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
enum class SetSize
|
||||||
|
{
|
||||||
|
Empty,
|
||||||
|
Unit,
|
||||||
|
Multi,
|
||||||
|
Unknown,
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
struct Type
|
||||||
|
{
|
||||||
|
Domain domain{Domain::Unknown};
|
||||||
|
SetSize setSize{SetSize::Unknown};
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
#endif
|
#endif
|
||||||
|
|
|
@ -46,12 +46,12 @@ output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &b
|
||||||
output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &printContext, bool omitParentheses = false);
|
output::ColorStream &print(output::ColorStream &stream, const 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 +167,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 +184,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 << ")";
|
||||||
|
@ -244,7 +237,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 +259,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)
|
||||||
|
@ -322,8 +322,24 @@ inline output::ColorStream &print(output::ColorStream &stream, const Variable &v
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext, bool)
|
inline output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext, bool)
|
||||||
{
|
{
|
||||||
|
const auto domainSuffix =
|
||||||
|
[&variableDeclaration]()
|
||||||
|
{
|
||||||
|
switch (variableDeclaration.domain)
|
||||||
|
{
|
||||||
|
case Domain::Unknown:
|
||||||
|
return "";
|
||||||
|
case Domain::Noninteger:
|
||||||
|
return "n";
|
||||||
|
case Domain::Integer:
|
||||||
|
return "i";
|
||||||
|
}
|
||||||
|
|
||||||
|
return "";
|
||||||
|
};
|
||||||
|
|
||||||
const auto printVariableDeclaration =
|
const auto printVariableDeclaration =
|
||||||
[&stream, &variableDeclaration](const auto *prefix, auto &variableIDs) -> output::ColorStream &
|
[&](const auto *prefix, auto &variableIDs) -> output::ColorStream &
|
||||||
{
|
{
|
||||||
auto matchingVariableID = variableIDs.find(&variableDeclaration);
|
auto matchingVariableID = variableIDs.find(&variableDeclaration);
|
||||||
|
|
||||||
|
@ -334,7 +350,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const VariableDec
|
||||||
matchingVariableID = emplaceResult.first;
|
matchingVariableID = emplaceResult.first;
|
||||||
}
|
}
|
||||||
|
|
||||||
const auto variableName = std::string(prefix) + std::to_string(matchingVariableID->second);
|
const auto variableName = std::string(prefix) + std::to_string(matchingVariableID->second) + domainSuffix();
|
||||||
|
|
||||||
return (stream << output::Variable(variableName.c_str()));
|
return (stream << output::Variable(variableName.c_str()));
|
||||||
};
|
};
|
||||||
|
|
|
@ -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,7 +35,7 @@ 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());
|
||||||
|
@ -100,22 +100,22 @@ ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Fo
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
ast::Formula completePredicate(const ast::PredicateSignature &predicateSignature, std::vector<ast::ScopedFormula> &scopedFormulas)
|
ast::Formula completePredicate(ast::PredicateDeclaration &predicateDeclaration, std::vector<ast::ScopedFormula> &scopedFormulas)
|
||||||
{
|
{
|
||||||
// Create new set of parameters for the completed definition for the predicate
|
// 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 +161,27 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
|
||||||
throw CompletionException("cannot perform completion, only single predicates and Booleans supported as formula consequent currently");
|
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 +201,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;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -0,0 +1,540 @@
|
||||||
|
#include <anthem/IntegerVariableDetection.h>
|
||||||
|
|
||||||
|
#include <anthem/ASTCopy.h>
|
||||||
|
#include <anthem/ASTUtils.h>
|
||||||
|
#include <anthem/ASTVisitors.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);
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
struct EvaluateFormulaVisitor
|
||||||
|
{
|
||||||
|
static EvaluationResult visit(const ast::And &and_, VariableDomainMap &variableDomainMap)
|
||||||
|
{
|
||||||
|
bool someFalse = false;
|
||||||
|
bool someUnknown = false;
|
||||||
|
|
||||||
|
for (const auto &argument : and_.arguments)
|
||||||
|
{
|
||||||
|
const auto result = evaluate(argument, variableDomainMap);
|
||||||
|
|
||||||
|
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;
|
||||||
|
}
|
||||||
|
|
||||||
|
static EvaluationResult visit(const ast::Biconditional &biconditional, VariableDomainMap &variableDomainMap)
|
||||||
|
{
|
||||||
|
const auto leftResult = evaluate(biconditional.left, variableDomainMap);
|
||||||
|
const auto rightResult = evaluate(biconditional.right, variableDomainMap);
|
||||||
|
|
||||||
|
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);
|
||||||
|
}
|
||||||
|
|
||||||
|
static EvaluationResult visit(const ast::Boolean &boolean, VariableDomainMap &)
|
||||||
|
{
|
||||||
|
return (boolean.value == true ? EvaluationResult::True : EvaluationResult::False);
|
||||||
|
}
|
||||||
|
|
||||||
|
static EvaluationResult visit(const ast::Comparison &comparison, VariableDomainMap &variableDomainMap)
|
||||||
|
{
|
||||||
|
const auto leftType = type(comparison.left, variableDomainMap);
|
||||||
|
const auto rightType = type(comparison.right, variableDomainMap);
|
||||||
|
|
||||||
|
// 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;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
static EvaluationResult visit(const ast::Exists &exists, VariableDomainMap &variableDomainMap)
|
||||||
|
{
|
||||||
|
return evaluate(exists.argument, variableDomainMap);
|
||||||
|
}
|
||||||
|
|
||||||
|
static EvaluationResult visit(const ast::ForAll &forAll, VariableDomainMap &variableDomainMap)
|
||||||
|
{
|
||||||
|
return evaluate(forAll.argument, variableDomainMap);
|
||||||
|
}
|
||||||
|
|
||||||
|
static EvaluationResult visit(const ast::Implies &implies, VariableDomainMap &variableDomainMap)
|
||||||
|
{
|
||||||
|
const auto antecedentResult = evaluate(implies.antecedent, variableDomainMap);
|
||||||
|
const auto consequentResult = evaluate(implies.consequent, variableDomainMap);
|
||||||
|
|
||||||
|
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;
|
||||||
|
}
|
||||||
|
|
||||||
|
static EvaluationResult visit(const ast::In &in, VariableDomainMap &variableDomainMap)
|
||||||
|
{
|
||||||
|
const auto elementType = type(in.element, variableDomainMap);
|
||||||
|
const auto setType = type(in.set, variableDomainMap);
|
||||||
|
|
||||||
|
// 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;
|
||||||
|
}
|
||||||
|
|
||||||
|
static EvaluationResult visit(const ast::Not ¬_, VariableDomainMap &variableDomainMap)
|
||||||
|
{
|
||||||
|
const auto result = evaluate(not_.argument, variableDomainMap);
|
||||||
|
|
||||||
|
if (result == EvaluationResult::Error || result == EvaluationResult::Unknown)
|
||||||
|
return result;
|
||||||
|
|
||||||
|
return (result == EvaluationResult::True ? EvaluationResult::False : EvaluationResult::True);
|
||||||
|
}
|
||||||
|
|
||||||
|
static EvaluationResult visit(const ast::Or &or_, VariableDomainMap &variableDomainMap)
|
||||||
|
{
|
||||||
|
bool someTrue = false;
|
||||||
|
bool someUnknown = false;
|
||||||
|
|
||||||
|
for (const auto &argument : or_.arguments)
|
||||||
|
{
|
||||||
|
const auto result = evaluate(argument, variableDomainMap);
|
||||||
|
|
||||||
|
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;
|
||||||
|
}
|
||||||
|
|
||||||
|
static EvaluationResult visit(const ast::Predicate &predicate, VariableDomainMap &variableDomainMap)
|
||||||
|
{
|
||||||
|
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, variableDomainMap);
|
||||||
|
|
||||||
|
if (argumentType.domain == Domain::Noninteger || argumentType.setSize == SetSize::Empty)
|
||||||
|
return EvaluationResult::Error;
|
||||||
|
}
|
||||||
|
|
||||||
|
return EvaluationResult::Unknown;
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
EvaluationResult evaluate(const ast::Formula &formula, VariableDomainMap &variableDomainMap)
|
||||||
|
{
|
||||||
|
return formula.accept(EvaluateFormulaVisitor(), 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);
|
||||||
|
|
||||||
// Check for #show statements with undeclared predicates
|
for (const auto &predicateDeclaration : context.predicateDeclarations)
|
||||||
if (context.visiblePredicateSignatures)
|
{
|
||||||
for (const auto &predicateSignature : context.visiblePredicateSignatures.value())
|
if (predicateDeclaration->isUsed)
|
||||||
if (!predicateSignature.used)
|
continue;
|
||||||
context.logger.log(output::Priority::Warning)
|
|
||||||
<< "#show declaration of “"
|
|
||||||
<< predicateSignature.predicateSignature.name
|
|
||||||
<< "/" << predicateSignature.predicateSignature.arity
|
|
||||||
<< "” does not match any eligible predicate";
|
|
||||||
|
|
||||||
// Check for #external statements with undeclared predicates
|
// Check for #show statements with undeclared predicates
|
||||||
if (context.externalPredicateSignatures)
|
if (predicateDeclaration->visibility != ast::PredicateDeclaration::Visibility::Default)
|
||||||
for (const auto &predicateSignature : context.externalPredicateSignatures.value())
|
context.logger.log(output::Priority::Warning)
|
||||||
if (!predicateSignature.used)
|
<< "#show declaration of “"
|
||||||
context.logger.log(output::Priority::Warning)
|
<< predicateDeclaration->name
|
||||||
<< "#external declaration of “"
|
<< "/"
|
||||||
<< predicateSignature.predicateSignature.name
|
<< predicateDeclaration->arity()
|
||||||
<< "/" << predicateSignature.predicateSignature.arity
|
<< "” does not match any declared predicate";
|
||||||
<< "” does not match any eligible predicate";
|
|
||||||
|
// Check for #external statements with undeclared predicates
|
||||||
|
if (predicateDeclaration->isExternal && !predicateDeclaration->isUsed)
|
||||||
|
context.logger.log(output::Priority::Warning)
|
||||||
|
<< "#external declaration of “"
|
||||||
|
<< predicateDeclaration->name
|
||||||
|
<< "/"
|
||||||
|
<< predicateDeclaration->arity()
|
||||||
|
<< "” does not match any declared predicate";
|
||||||
|
}
|
||||||
|
|
||||||
|
// Detect integer variables
|
||||||
|
if (context.performIntegerDetection)
|
||||||
|
detectIntegerVariables(completedFormulas);
|
||||||
|
|
||||||
// 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;
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
Loading…
Reference in New Issue