Compare commits
1 Commits
v0.1.9-rc.
...
v0.1.9-rc.
| Author | SHA1 | Date | |
|---|---|---|---|
53c96f0fe7
|
@@ -1,13 +1,11 @@
|
||||
# Change Log
|
||||
|
||||
## 0.1.9 RC 5 (2018-04-22)
|
||||
## 0.1.9 RC 1 (2018-04-20)
|
||||
|
||||
### 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)
|
||||
|
||||
|
||||
@@ -72,7 +72,7 @@ int main(int argc, char **argv)
|
||||
|
||||
if (version)
|
||||
{
|
||||
std::cout << "anthem version 0.1.9-rc.5" << std::endl;
|
||||
std::cout << "anthem version 0.1.9-rc.1" << std::endl;
|
||||
return EXIT_SUCCESS;
|
||||
}
|
||||
|
||||
|
||||
@@ -1,2 +0,0 @@
|
||||
p(a).
|
||||
{q(a)}.
|
||||
@@ -1,18 +1,10 @@
|
||||
% assign a set of colors to each vertex
|
||||
{color(V, C)} :- vertex(V), color(C).
|
||||
|
||||
% at most one color per vertex
|
||||
:- color(V, C1), color(V, C2), C1 != C2.
|
||||
|
||||
% at least one color per vertex
|
||||
covered(V) :- color(V, _).
|
||||
:- vertex(V), not covered(V).
|
||||
|
||||
% adjacent vertices don’t share the same color
|
||||
:- color(V1, C), color(V2, C), edge(V1, V2).
|
||||
|
||||
#external color(1).
|
||||
#external edge(2).
|
||||
#external vertex(1).
|
||||
#show color/2.
|
||||
|
||||
#external vertex(1).
|
||||
#external edge(2).
|
||||
#external color(1).
|
||||
{color(V, C)} :- vertex(V), color(C).
|
||||
covered(V) :- color(V, _).
|
||||
:- vertex(V), not covered(V).
|
||||
:- color(V1, C), color(V2, C), edge(V1, V2).
|
||||
:- color(V, C1), color(V, C2), C1 != C2.
|
||||
|
||||
@@ -1,11 +0,0 @@
|
||||
letter(a).
|
||||
letter(b).
|
||||
letter(c).
|
||||
|
||||
{p(1..3, Y)} :- letter(Y).
|
||||
:- p(X1, Y), p(X2, Y), X1 != X2.
|
||||
|
||||
q(X) :- p(X, _).
|
||||
:- X = 1..3, not q(X).
|
||||
|
||||
#show p/2.
|
||||
@@ -1,4 +1,5 @@
|
||||
#show p/2.
|
||||
#external integer(n(0)).
|
||||
|
||||
{p(1..n, 1..n)}.
|
||||
|
||||
|
||||
@@ -1,4 +1,5 @@
|
||||
#show prime/1.
|
||||
#external integer(n(0)).
|
||||
|
||||
composite(I * J) :- I = 2..n, J = 2..n.
|
||||
prime(N) :- N = 2..n, not composite(N).
|
||||
|
||||
#show prime/1.
|
||||
|
||||
@@ -1,7 +1,9 @@
|
||||
#show in/2.
|
||||
#external integer(n(0)).
|
||||
#external integer(r(0)).
|
||||
|
||||
{in(1..n, 1..r)}.
|
||||
covered(I) :- in(I, S).
|
||||
|
||||
:- I = 1..n, not covered(I).
|
||||
:- in(I, S), in(J, S), in(I + J, S).
|
||||
|
||||
#show in/2.
|
||||
|
||||
@@ -1,9 +0,0 @@
|
||||
s(X) :- p(X).
|
||||
s(X) :- q(X).
|
||||
u(X) :- r(X), not s(X).
|
||||
|
||||
#show u/1.
|
||||
|
||||
#external p(1).
|
||||
#external q(1).
|
||||
#external r(1).
|
||||
@@ -1,5 +0,0 @@
|
||||
s(X) :- p(X).
|
||||
s(X) :- q(X).
|
||||
|
||||
#external p(1).
|
||||
#external q(1).
|
||||
@@ -2,7 +2,8 @@
|
||||
#define __ANTHEM__AST_H
|
||||
|
||||
#include <anthem/ASTForward.h>
|
||||
#include <anthem/Utils.h>
|
||||
#include <anthem/Domain.h>
|
||||
#include <anthem/Tristate.h>
|
||||
|
||||
namespace anthem
|
||||
{
|
||||
@@ -148,7 +149,7 @@ struct FunctionDeclaration
|
||||
|
||||
std::string name;
|
||||
size_t arity;
|
||||
Domain domain{Domain::Noninteger};
|
||||
Domain domain{Domain::General};
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
27
include/anthem/Domain.h
Normal file
27
include/anthem/Domain.h
Normal file
@@ -0,0 +1,27 @@
|
||||
#ifndef __ANTHEM__DOMAIN_H
|
||||
#define __ANTHEM__DOMAIN_H
|
||||
|
||||
namespace anthem
|
||||
{
|
||||
namespace ast
|
||||
{
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
//
|
||||
// Domain
|
||||
//
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
enum class Domain
|
||||
{
|
||||
General,
|
||||
Integer,
|
||||
Unknown,
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
#endif
|
||||
@@ -3,7 +3,7 @@
|
||||
|
||||
#include <anthem/AST.h>
|
||||
#include <anthem/ASTUtils.h>
|
||||
#include <anthem/Utils.h>
|
||||
#include <anthem/Tristate.h>
|
||||
|
||||
namespace anthem
|
||||
{
|
||||
|
||||
@@ -12,6 +12,14 @@ namespace anthem
|
||||
//
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
enum class SimplificationResult
|
||||
{
|
||||
Simplified,
|
||||
Unchanged,
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
void simplify(ast::Formula &formula);
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
@@ -3,7 +3,6 @@
|
||||
|
||||
#include <anthem/AST.h>
|
||||
#include <anthem/Simplification.h>
|
||||
#include <anthem/Utils.h>
|
||||
|
||||
namespace anthem
|
||||
{
|
||||
@@ -20,96 +19,96 @@ template<class T>
|
||||
struct FormulaSimplificationVisitor
|
||||
{
|
||||
template <class... Arguments>
|
||||
OperationResult visit(And &and_, Formula &formula, Arguments &&... arguments)
|
||||
SimplificationResult visit(And &and_, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
for (auto &argument : and_.arguments)
|
||||
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
return OperationResult::Changed;
|
||||
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
OperationResult visit(Biconditional &biconditional, Formula &formula, Arguments &&... arguments)
|
||||
SimplificationResult visit(Biconditional &biconditional, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
if (biconditional.left.accept(*this, biconditional.left, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
return OperationResult::Changed;
|
||||
if (biconditional.left.accept(*this, biconditional.left, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
if (biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
return OperationResult::Changed;
|
||||
if (biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
OperationResult visit(Boolean &, Formula &formula, Arguments &&... arguments)
|
||||
SimplificationResult visit(Boolean &, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
OperationResult visit(Comparison &, Formula &formula, Arguments &&... arguments)
|
||||
SimplificationResult visit(Comparison &, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
OperationResult visit(Exists &exists, Formula &formula, Arguments &&... arguments)
|
||||
SimplificationResult visit(Exists &exists, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
if (exists.argument.accept(*this, exists.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
return OperationResult::Changed;
|
||||
if (exists.argument.accept(*this, exists.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
OperationResult visit(ForAll &forAll, Formula &formula, Arguments &&... arguments)
|
||||
SimplificationResult visit(ForAll &forAll, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
if (forAll.argument.accept(*this, forAll.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
return OperationResult::Changed;
|
||||
if (forAll.argument.accept(*this, forAll.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
OperationResult visit(Implies &implies, Formula &formula, Arguments &&... arguments)
|
||||
SimplificationResult visit(Implies &implies, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
if (implies.antecedent.accept(*this, implies.antecedent, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
return OperationResult::Changed;
|
||||
if (implies.antecedent.accept(*this, implies.antecedent, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
if (implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
return OperationResult::Changed;
|
||||
if (implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
OperationResult visit(In &, Formula &formula, Arguments &&... arguments)
|
||||
SimplificationResult visit(In &, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
OperationResult visit(Not ¬_, Formula &formula, Arguments &&... arguments)
|
||||
SimplificationResult visit(Not ¬_, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
if (not_.argument.accept(*this, not_.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
return OperationResult::Changed;
|
||||
if (not_.argument.accept(*this, not_.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
OperationResult visit(Or &or_, Formula &formula, Arguments &&... arguments)
|
||||
SimplificationResult visit(Or &or_, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
for (auto &argument : or_.arguments)
|
||||
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
return OperationResult::Changed;
|
||||
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
OperationResult visit(Predicate &, Formula &formula, Arguments &&... arguments)
|
||||
SimplificationResult visit(Predicate &, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
@@ -117,69 +116,69 @@ struct FormulaSimplificationVisitor
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class T, class OperationResult = void>
|
||||
template<class T, class SimplificationResult = void>
|
||||
struct TermSimplificationVisitor
|
||||
{
|
||||
template <class... Arguments>
|
||||
OperationResult visit(BinaryOperation &binaryOperation, Term &term, Arguments &&... arguments)
|
||||
SimplificationResult visit(BinaryOperation &binaryOperation, Term &term, Arguments &&... arguments)
|
||||
{
|
||||
if (binaryOperation.left.accept(*this, binaryOperation.left, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
return OperationResult::Changed;
|
||||
if (binaryOperation.left.accept(*this, binaryOperation.left, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
return OperationResult::Changed;
|
||||
if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
OperationResult visit(Boolean &, Term &term, Arguments &&... arguments)
|
||||
SimplificationResult visit(Boolean &, Term &term, Arguments &&... arguments)
|
||||
{
|
||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
OperationResult visit(Function &function, Term &term, Arguments &&... arguments)
|
||||
SimplificationResult visit(Function &function, Term &term, Arguments &&... arguments)
|
||||
{
|
||||
for (auto &argument : function.arguments)
|
||||
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
return OperationResult::Changed;
|
||||
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
OperationResult visit(Integer &, Term &term, Arguments &&... arguments)
|
||||
SimplificationResult visit(Integer &, Term &term, Arguments &&... arguments)
|
||||
{
|
||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
OperationResult visit(Interval &interval, Term &term, Arguments &&... arguments)
|
||||
SimplificationResult visit(Interval &interval, Term &term, Arguments &&... arguments)
|
||||
{
|
||||
if (interval.from.accept(*this, interval.from, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
return OperationResult::Changed;
|
||||
if (interval.from.accept(*this, interval.from, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
if (interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
return OperationResult::Changed;
|
||||
if (interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
OperationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments)
|
||||
SimplificationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments)
|
||||
{
|
||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
OperationResult visit(String &, Term &term, Arguments &&... arguments)
|
||||
SimplificationResult visit(String &, Term &term, Arguments &&... arguments)
|
||||
{
|
||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
OperationResult visit(Variable &, Term &term, Arguments &&... arguments)
|
||||
SimplificationResult visit(Variable &, Term &term, Arguments &&... arguments)
|
||||
{
|
||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
@@ -237,7 +237,7 @@ struct StatementVisitor
|
||||
const size_t arity = aritySymbol.number();
|
||||
|
||||
auto functionDeclaration = context.findOrCreateFunctionDeclaration(function.name, arity);
|
||||
functionDeclaration->domain = Domain::Integer;
|
||||
functionDeclaration->domain = ast::Domain::Integer;
|
||||
|
||||
return true;
|
||||
};
|
||||
|
||||
24
include/anthem/Tristate.h
Normal file
24
include/anthem/Tristate.h
Normal file
@@ -0,0 +1,24 @@
|
||||
#ifndef __ANTHEM__TRISTATE_H
|
||||
#define __ANTHEM__TRISTATE_H
|
||||
|
||||
namespace anthem
|
||||
{
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
//
|
||||
// Tristate
|
||||
//
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
enum class Tristate
|
||||
{
|
||||
True,
|
||||
False,
|
||||
Unknown,
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
}
|
||||
|
||||
#endif
|
||||
@@ -1,166 +0,0 @@
|
||||
#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,6 +1,13 @@
|
||||
#ifndef __ANTHEM__UTILS_H
|
||||
#define __ANTHEM__UTILS_H
|
||||
|
||||
#include <iostream>
|
||||
|
||||
#include <clingo.hh>
|
||||
|
||||
#include <anthem/Context.h>
|
||||
#include <anthem/Location.h>
|
||||
|
||||
namespace anthem
|
||||
{
|
||||
|
||||
@@ -13,61 +20,6 @@ namespace anthem
|
||||
constexpr const auto HeadVariablePrefix = "V";
|
||||
constexpr const auto BodyVariablePrefix = "X";
|
||||
constexpr const auto UserVariablePrefix = "U";
|
||||
constexpr const auto IntegerVariablePrefix = "N";
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
enum class Tristate
|
||||
{
|
||||
True,
|
||||
False,
|
||||
Unknown,
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
enum class 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};
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
@@ -35,7 +35,6 @@ struct PrintContext
|
||||
std::map<const VariableDeclaration *, size_t> userVariableIDs;
|
||||
std::map<const VariableDeclaration *, size_t> headVariableIDs;
|
||||
std::map<const VariableDeclaration *, size_t> bodyVariableIDs;
|
||||
std::map<const VariableDeclaration *, size_t> integerVariableIDs;
|
||||
|
||||
const Context &context;
|
||||
};
|
||||
@@ -323,6 +322,22 @@ inline output::ColorStream &print(output::ColorStream &stream, const Variable &v
|
||||
|
||||
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::General:
|
||||
return "g";
|
||||
case Domain::Integer:
|
||||
return "i";
|
||||
}
|
||||
|
||||
return "";
|
||||
};
|
||||
|
||||
const auto printVariableDeclaration =
|
||||
[&](const auto *prefix, auto &variableIDs) -> output::ColorStream &
|
||||
{
|
||||
@@ -335,14 +350,11 @@ inline output::ColorStream &print(output::ColorStream &stream, const VariableDec
|
||||
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()));
|
||||
};
|
||||
|
||||
if (variableDeclaration.domain == Domain::Integer)
|
||||
return printVariableDeclaration(IntegerVariablePrefix, printContext.integerVariableIDs);
|
||||
|
||||
switch (variableDeclaration.type)
|
||||
{
|
||||
case VariableDeclaration::Type::UserDefined:
|
||||
|
||||
@@ -5,8 +5,6 @@
|
||||
#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
|
||||
@@ -18,19 +16,19 @@ namespace anthem
|
||||
//
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
using VariableDomainMap = std::map<const ast::VariableDeclaration *, Domain>;
|
||||
using VariableDomainMap = std::map<const ast::VariableDeclaration *, ast::Domain>;
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
Domain domain(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
|
||||
ast::Domain domain(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
|
||||
{
|
||||
if (variable.declaration->domain != Domain::Unknown)
|
||||
if (variable.declaration->domain != ast::Domain::Unknown)
|
||||
return variable.declaration->domain;
|
||||
|
||||
const auto match = variableDomainMap.find(variable.declaration);
|
||||
|
||||
if (match == variableDomainMap.end())
|
||||
return Domain::Unknown;
|
||||
return ast::Domain::Unknown;
|
||||
|
||||
return match->second;
|
||||
}
|
||||
@@ -40,24 +38,138 @@ Domain domain(const ast::Variable &variable, VariableDomainMap &variableDomainMa
|
||||
void clearVariableDomainMap(VariableDomainMap &variableDomainMap)
|
||||
{
|
||||
for (auto &variableDeclaration : variableDomainMap)
|
||||
variableDeclaration.second = Domain::Unknown;
|
||||
variableDeclaration.second = ast::Domain::Unknown;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
struct VariableDomainMapAccessor
|
||||
enum class OperationResult
|
||||
{
|
||||
Domain operator()(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
|
||||
Unchanged,
|
||||
Changed,
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
enum class EvaluationResult
|
||||
{
|
||||
True,
|
||||
False,
|
||||
Unknown,
|
||||
Error,
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
EvaluationResult isArithmetic(const ast::Term &term, VariableDomainMap &variableDomainMap);
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
struct IsTermArithmeticVisitor
|
||||
{
|
||||
static EvaluationResult visit(const ast::BinaryOperation &binaryOperation, VariableDomainMap &variableDomainMap)
|
||||
{
|
||||
return domain(variable, variableDomainMap);
|
||||
const auto isLeftArithemtic = isArithmetic(binaryOperation.left, variableDomainMap);
|
||||
const auto isRightArithmetic = isArithmetic(binaryOperation.right, variableDomainMap);
|
||||
|
||||
if (isLeftArithemtic == EvaluationResult::Error || isRightArithmetic == EvaluationResult::Error)
|
||||
return EvaluationResult::Error;
|
||||
|
||||
if (isLeftArithemtic == EvaluationResult::False || isRightArithmetic == EvaluationResult::False)
|
||||
return EvaluationResult::Error;
|
||||
|
||||
if (isLeftArithemtic == EvaluationResult::Unknown || isRightArithmetic == EvaluationResult::Unknown)
|
||||
return EvaluationResult::Unknown;
|
||||
|
||||
return EvaluationResult::True;
|
||||
}
|
||||
|
||||
static EvaluationResult visit(const ast::Boolean &, VariableDomainMap &)
|
||||
{
|
||||
return EvaluationResult::False;
|
||||
}
|
||||
|
||||
static EvaluationResult visit(const ast::Function &function, VariableDomainMap &)
|
||||
{
|
||||
switch (function.declaration->domain)
|
||||
{
|
||||
case ast::Domain::General:
|
||||
return EvaluationResult::False;
|
||||
case ast::Domain::Integer:
|
||||
return EvaluationResult::True;
|
||||
case ast::Domain::Unknown:
|
||||
return EvaluationResult::Unknown;
|
||||
}
|
||||
|
||||
return EvaluationResult::Unknown;
|
||||
}
|
||||
|
||||
static EvaluationResult visit(const ast::Integer &, VariableDomainMap &)
|
||||
{
|
||||
return EvaluationResult::True;
|
||||
}
|
||||
|
||||
static EvaluationResult visit(const ast::Interval &interval, VariableDomainMap &variableDomainMap)
|
||||
{
|
||||
const auto isFromArithmetic = isArithmetic(interval.from, variableDomainMap);
|
||||
const auto isToArithmetic = isArithmetic(interval.to, variableDomainMap);
|
||||
|
||||
if (isFromArithmetic == EvaluationResult::Error || isToArithmetic == EvaluationResult::Error)
|
||||
return EvaluationResult::Error;
|
||||
|
||||
if (isFromArithmetic == EvaluationResult::False || isToArithmetic == EvaluationResult::False)
|
||||
return EvaluationResult::Error;
|
||||
|
||||
if (isFromArithmetic == EvaluationResult::Unknown || isToArithmetic == EvaluationResult::Unknown)
|
||||
return EvaluationResult::Unknown;
|
||||
|
||||
return EvaluationResult::True;
|
||||
}
|
||||
|
||||
static EvaluationResult visit(const ast::SpecialInteger &, VariableDomainMap &)
|
||||
{
|
||||
return EvaluationResult::False;
|
||||
}
|
||||
|
||||
static EvaluationResult visit(const ast::String &, VariableDomainMap &)
|
||||
{
|
||||
return EvaluationResult::False;
|
||||
}
|
||||
|
||||
static EvaluationResult visit(const ast::UnaryOperation &unaryOperation, VariableDomainMap &variableDomainMap)
|
||||
{
|
||||
const auto isArgumentArithmetic = isArithmetic(unaryOperation.argument, variableDomainMap);
|
||||
|
||||
switch (unaryOperation.operator_)
|
||||
{
|
||||
case ast::UnaryOperation::Operator::Absolute:
|
||||
return (isArgumentArithmetic == EvaluationResult::False ? EvaluationResult::Error : isArgumentArithmetic);
|
||||
}
|
||||
|
||||
return EvaluationResult::Unknown;
|
||||
}
|
||||
|
||||
static EvaluationResult visit(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
|
||||
{
|
||||
switch (domain(variable, variableDomainMap))
|
||||
{
|
||||
case ast::Domain::General:
|
||||
return EvaluationResult::False;
|
||||
case ast::Domain::Integer:
|
||||
return EvaluationResult::True;
|
||||
case ast::Domain::Unknown:
|
||||
return EvaluationResult::Unknown;
|
||||
}
|
||||
|
||||
return EvaluationResult::Unknown;
|
||||
}
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
Type type(const ast::Term &term, VariableDomainMap &variableDomainMap)
|
||||
EvaluationResult isArithmetic(const ast::Term &term, VariableDomainMap &variableDomainMap)
|
||||
{
|
||||
return type<VariableDomainMapAccessor>(term, variableDomainMap);
|
||||
return term.accept(IsTermArithmeticVisitor(), variableDomainMap);
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
@@ -122,22 +234,19 @@ struct EvaluateFormulaVisitor
|
||||
|
||||
static EvaluationResult visit(const ast::Comparison &comparison, VariableDomainMap &variableDomainMap)
|
||||
{
|
||||
const auto leftType = type(comparison.left, variableDomainMap);
|
||||
const auto rightType = type(comparison.right, variableDomainMap);
|
||||
const auto isLeftArithmetic = isArithmetic(comparison.left, variableDomainMap);
|
||||
const auto isRightArithmetic = isArithmetic(comparison.right, variableDomainMap);
|
||||
|
||||
// Comparisons with empty sets always return false
|
||||
if (leftType.setSize == SetSize::Empty || rightType.setSize == SetSize::Empty)
|
||||
return EvaluationResult::False;
|
||||
if (isLeftArithmetic == EvaluationResult::Error || isRightArithmetic == EvaluationResult::Error)
|
||||
return EvaluationResult::Error;
|
||||
|
||||
// If either side has an unknown domain, the result is unknown
|
||||
if (leftType.domain == Domain::Unknown || rightType.domain == Domain::Unknown)
|
||||
if (isLeftArithmetic == EvaluationResult::Unknown || isRightArithmetic == EvaluationResult::Unknown)
|
||||
return EvaluationResult::Unknown;
|
||||
|
||||
// If both sides have the same domain, the result is unknown
|
||||
if (leftType.domain == rightType.domain)
|
||||
if (isLeftArithmetic == isRightArithmetic)
|
||||
return EvaluationResult::Unknown;
|
||||
|
||||
// If one side is integer, but the other one isn’t, they are not equal
|
||||
// Handle the case where one side is arithmetic but the other one isn’t
|
||||
switch (comparison.operator_)
|
||||
{
|
||||
case ast::Comparison::Operator::Equal:
|
||||
@@ -182,25 +291,19 @@ struct EvaluateFormulaVisitor
|
||||
|
||||
static EvaluationResult visit(const ast::In &in, VariableDomainMap &variableDomainMap)
|
||||
{
|
||||
const auto elementType = type(in.element, variableDomainMap);
|
||||
const auto setType = type(in.set, variableDomainMap);
|
||||
const auto isElementArithmetic = isArithmetic(in.element, variableDomainMap);
|
||||
const auto isSetArithmetic = isArithmetic(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 (isElementArithmetic == EvaluationResult::Error || isSetArithmetic == EvaluationResult::Error)
|
||||
return EvaluationResult::Error;
|
||||
|
||||
// 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)
|
||||
if (isElementArithmetic == EvaluationResult::Unknown || isSetArithmetic == EvaluationResult::Unknown)
|
||||
return EvaluationResult::Unknown;
|
||||
|
||||
// If both sides have the same domain, the result is unknown
|
||||
if (elementType.domain == setType.domain)
|
||||
if (isElementArithmetic == isSetArithmetic)
|
||||
return EvaluationResult::Unknown;
|
||||
|
||||
// If one side is integer, but the other one isn’t, set inclusion is never satisfied
|
||||
// If one side is arithmetic, but the other one isn’t, set inclusion is never satisfied
|
||||
return EvaluationResult::False;
|
||||
}
|
||||
|
||||
@@ -256,13 +359,13 @@ struct EvaluateFormulaVisitor
|
||||
const auto &argument = predicate.arguments[i];
|
||||
const auto ¶meter = predicate.declaration->parameters[i];
|
||||
|
||||
if (parameter.domain != Domain::Integer)
|
||||
if (parameter.domain != ast::Domain::Integer)
|
||||
continue;
|
||||
|
||||
const auto argumentType = type(argument, variableDomainMap);
|
||||
const auto isArgumentArithmetic = isArithmetic(argument, variableDomainMap);
|
||||
|
||||
if (argumentType.domain == Domain::Noninteger || argumentType.setSize == SetSize::Empty)
|
||||
return EvaluationResult::Error;
|
||||
if (isArgumentArithmetic == EvaluationResult::Error || isArgumentArithmetic == EvaluationResult::False)
|
||||
return isArgumentArithmetic;
|
||||
}
|
||||
|
||||
return EvaluationResult::Unknown;
|
||||
@@ -278,205 +381,199 @@ EvaluationResult evaluate(const ast::Formula &formula, VariableDomainMap &variab
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template <class Functor>
|
||||
struct ForEachVariableDeclarationVisitor
|
||||
OperationResult detectIntegerVariables(ast::Formula &formula, ast::Formula &definition, VariableDomainMap &variableDomainMap);
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
struct DetectIntegerVariablesVisitor
|
||||
{
|
||||
template <class... Arguments>
|
||||
static OperationResult visit(ast::And &and_, Arguments &&... arguments)
|
||||
static OperationResult visit(ast::And &and_, ast::Formula &definition, VariableDomainMap &variableDomainMap)
|
||||
{
|
||||
auto operationResult = OperationResult::Unchanged;
|
||||
|
||||
for (auto &argument : and_.arguments)
|
||||
if (argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
if (detectIntegerVariables(argument, definition, variableDomainMap) == OperationResult::Changed)
|
||||
operationResult = OperationResult::Changed;
|
||||
|
||||
return operationResult;
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
static OperationResult visit(ast::Biconditional &biconditional, Arguments &&... arguments)
|
||||
static OperationResult visit(ast::Biconditional &biconditional, ast::Formula &definition, VariableDomainMap &variableDomainMap)
|
||||
{
|
||||
auto operationResult = OperationResult::Unchanged;
|
||||
|
||||
if (biconditional.left.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
if (detectIntegerVariables(biconditional.left, definition, variableDomainMap) == OperationResult::Changed)
|
||||
operationResult = OperationResult::Changed;
|
||||
|
||||
if (biconditional.right.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
if (detectIntegerVariables(biconditional.right, definition, variableDomainMap) == OperationResult::Changed)
|
||||
operationResult = OperationResult::Changed;
|
||||
|
||||
return operationResult;
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
static OperationResult visit(ast::Boolean &, Arguments &&...)
|
||||
static OperationResult visit(ast::Boolean &, ast::Formula &, VariableDomainMap &)
|
||||
{
|
||||
return OperationResult::Unchanged;
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
static OperationResult visit(ast::Comparison &, Arguments &&...)
|
||||
static OperationResult visit(ast::Comparison &, ast::Formula &, VariableDomainMap &)
|
||||
{
|
||||
return OperationResult::Unchanged;
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
static OperationResult visit(ast::Exists &exists, Arguments &&... arguments)
|
||||
static OperationResult visit(ast::Exists &exists, ast::Formula &definition, VariableDomainMap &variableDomainMap)
|
||||
{
|
||||
auto operationResult = OperationResult::Unchanged;
|
||||
|
||||
if (exists.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
if (detectIntegerVariables(exists.argument, definition, variableDomainMap) == OperationResult::Changed)
|
||||
operationResult = OperationResult::Changed;
|
||||
|
||||
for (auto &variableDeclaration : exists.variables)
|
||||
if (Functor()(*variableDeclaration, exists.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
{
|
||||
if (variableDeclaration->domain != ast::Domain::Unknown)
|
||||
continue;
|
||||
|
||||
clearVariableDomainMap(variableDomainMap);
|
||||
|
||||
auto argumentResult = evaluate(exists.argument, variableDomainMap);
|
||||
auto definitionResult = evaluate(definition, variableDomainMap);
|
||||
|
||||
if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
|
||||
|| definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
|
||||
{
|
||||
continue;
|
||||
}
|
||||
|
||||
// As a hypothesis, make the parameter’s domain noninteger
|
||||
variableDomainMap[variableDeclaration.get()] = ast::Domain::General;
|
||||
|
||||
argumentResult = evaluate(exists.argument, variableDomainMap);
|
||||
definitionResult = evaluate(definition, variableDomainMap);
|
||||
|
||||
if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
|
||||
|| definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
|
||||
{
|
||||
// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
|
||||
operationResult = OperationResult::Changed;
|
||||
variableDeclaration->domain = ast::Domain::Integer;
|
||||
}
|
||||
}
|
||||
|
||||
return operationResult;
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
static OperationResult visit(ast::ForAll &forAll, Arguments &&... arguments)
|
||||
static OperationResult visit(ast::ForAll &forAll, ast::Formula &definition, VariableDomainMap &variableDomainMap)
|
||||
{
|
||||
auto operationResult = OperationResult::Unchanged;
|
||||
|
||||
if (forAll.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
if (detectIntegerVariables(forAll.argument, definition, variableDomainMap) == OperationResult::Changed)
|
||||
operationResult = OperationResult::Changed;
|
||||
|
||||
for (auto &variableDeclaration : forAll.variables)
|
||||
if (Functor()(*variableDeclaration, forAll.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
{
|
||||
if (variableDeclaration->domain != ast::Domain::Unknown)
|
||||
continue;
|
||||
|
||||
clearVariableDomainMap(variableDomainMap);
|
||||
|
||||
auto argumentResult = evaluate(forAll.argument, variableDomainMap);
|
||||
auto definitionResult = evaluate(definition, variableDomainMap);
|
||||
|
||||
if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
|
||||
|| definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
|
||||
{
|
||||
continue;
|
||||
}
|
||||
|
||||
// As a hypothesis, make the parameter’s domain noninteger
|
||||
variableDomainMap[variableDeclaration.get()] = ast::Domain::General;
|
||||
|
||||
argumentResult = evaluate(forAll.argument, variableDomainMap);
|
||||
definitionResult = evaluate(definition, variableDomainMap);
|
||||
|
||||
if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
|
||||
|| definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
|
||||
{
|
||||
// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
|
||||
operationResult = OperationResult::Changed;
|
||||
variableDeclaration->domain = ast::Domain::Integer;
|
||||
}
|
||||
}
|
||||
|
||||
return operationResult;
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
static OperationResult visit(ast::Implies &implies, Arguments &&... arguments)
|
||||
static OperationResult visit(ast::Implies &implies, ast::Formula &definition, VariableDomainMap &variableDomainMap)
|
||||
{
|
||||
auto operationResult = OperationResult::Unchanged;
|
||||
|
||||
if (implies.antecedent.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
if (detectIntegerVariables(implies.antecedent, definition, variableDomainMap) == OperationResult::Changed)
|
||||
operationResult = OperationResult::Changed;
|
||||
|
||||
if (implies.consequent.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
if (detectIntegerVariables(implies.consequent, definition, variableDomainMap) == OperationResult::Changed)
|
||||
operationResult = OperationResult::Changed;
|
||||
|
||||
return operationResult;
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
static OperationResult visit(ast::In &, Arguments &&...)
|
||||
static OperationResult visit(ast::In &, ast::Formula &, VariableDomainMap &)
|
||||
{
|
||||
return OperationResult::Unchanged;
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
static OperationResult visit(ast::Not ¬_, Arguments &&... arguments)
|
||||
static OperationResult visit(ast::Not ¬_, ast::Formula &definition, VariableDomainMap &variableDomainMap)
|
||||
{
|
||||
return not_.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...);
|
||||
return detectIntegerVariables(not_.argument, definition, variableDomainMap);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
static OperationResult visit(ast::Or &or_, Arguments &&... arguments)
|
||||
static OperationResult visit(ast::Or &or_, ast::Formula &definition, VariableDomainMap &variableDomainMap)
|
||||
{
|
||||
auto operationResult = OperationResult::Unchanged;
|
||||
|
||||
for (auto &argument : or_.arguments)
|
||||
if (argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
|
||||
if (detectIntegerVariables(argument, definition, variableDomainMap) == OperationResult::Changed)
|
||||
operationResult = OperationResult::Changed;
|
||||
|
||||
return operationResult;
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
static OperationResult visit(ast::Predicate &, Arguments &&...)
|
||||
static OperationResult visit(ast::Predicate &predicate, ast::Formula &, VariableDomainMap &)
|
||||
{
|
||||
return OperationResult::Unchanged;
|
||||
auto operationResult = OperationResult::Unchanged;
|
||||
|
||||
assert(predicate.arguments.size() == predicate.declaration->arity());
|
||||
|
||||
// Propagate integer domains from predicates to variables
|
||||
for (size_t i = 0; i < predicate.arguments.size(); i++)
|
||||
{
|
||||
auto &variableArgument = predicate.arguments[i];
|
||||
auto ¶meter = predicate.declaration->parameters[i];
|
||||
|
||||
if (parameter.domain != ast::Domain::Integer)
|
||||
continue;
|
||||
|
||||
if (!variableArgument.is<ast::Variable>())
|
||||
continue;
|
||||
|
||||
auto &variable = variableArgument.get<ast::Variable>();
|
||||
|
||||
if (variable.declaration->domain == ast::Domain::Integer)
|
||||
continue;
|
||||
|
||||
operationResult = OperationResult::Changed;
|
||||
variable.declaration->domain = ast::Domain::Integer;
|
||||
}
|
||||
|
||||
return operationResult;
|
||||
}
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
struct CheckIfDefinitionFalseFunctor
|
||||
OperationResult detectIntegerVariables(ast::Formula &formula, ast::Formula &definition, VariableDomainMap &variableDomainMap)
|
||||
{
|
||||
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;
|
||||
}
|
||||
};
|
||||
return formula.accept(DetectIntegerVariablesVisitor(), definition, variableDomainMap);
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
@@ -493,10 +590,7 @@ void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas)
|
||||
|
||||
for (auto &completedFormula : completedFormulas)
|
||||
{
|
||||
if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfQuantifiedFormulaFalseFunctor>(), variableDomainMap) == OperationResult::Changed)
|
||||
operationResult = OperationResult::Changed;
|
||||
|
||||
if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfCompletedFormulaTrueFunctor>(), completedFormula, variableDomainMap) == OperationResult::Changed)
|
||||
if (detectIntegerVariables(completedFormula, completedFormula, variableDomainMap) == OperationResult::Changed)
|
||||
operationResult = OperationResult::Changed;
|
||||
|
||||
if (!completedFormula.is<ast::ForAll>())
|
||||
@@ -515,11 +609,11 @@ void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas)
|
||||
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());
|
||||
|
||||
if (detectIntegerVariables(definition, definition, variableDomainMap) == OperationResult::Changed)
|
||||
operationResult = OperationResult::Changed;
|
||||
|
||||
for (size_t i = 0; i < predicate.arguments.size(); i++)
|
||||
{
|
||||
auto &variableArgument = predicate.arguments[i];
|
||||
@@ -529,7 +623,28 @@ void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas)
|
||||
|
||||
auto &variable = variableArgument.get<ast::Variable>();
|
||||
|
||||
parameter.domain = variable.declaration->domain;
|
||||
if (parameter.domain != ast::Domain::Unknown)
|
||||
continue;
|
||||
|
||||
clearVariableDomainMap(variableDomainMap);
|
||||
|
||||
auto result = evaluate(definition, variableDomainMap);
|
||||
|
||||
if (result == EvaluationResult::Error || result == EvaluationResult::False)
|
||||
continue;
|
||||
|
||||
// As a hypothesis, make the parameter’s domain noninteger
|
||||
variableDomainMap[variable.declaration] = ast::Domain::General;
|
||||
|
||||
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
|
||||
operationResult = OperationResult::Changed;
|
||||
variable.declaration->domain = ast::Domain::Integer;
|
||||
parameter.domain = ast::Domain::Integer;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@@ -4,9 +4,8 @@
|
||||
|
||||
#include <anthem/ASTCopy.h>
|
||||
#include <anthem/Equality.h>
|
||||
#include <anthem/SimplificationVisitors.h>
|
||||
#include <anthem/Type.h>
|
||||
#include <anthem/output/AST.h>
|
||||
#include <anthem/SimplificationVisitors.h>
|
||||
|
||||
namespace anthem
|
||||
{
|
||||
@@ -101,7 +100,7 @@ struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<Rep
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class SimplificationRule>
|
||||
OperationResult simplify(ast::Formula &formula)
|
||||
SimplificationResult simplify(ast::Formula &formula)
|
||||
{
|
||||
return SimplificationRule::apply(formula);
|
||||
}
|
||||
@@ -109,10 +108,10 @@ OperationResult simplify(ast::Formula &formula)
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class FirstSimplificationRule, class SecondSimplificationRule, class... OtherSimplificationRules>
|
||||
OperationResult simplify(ast::Formula &formula)
|
||||
SimplificationResult simplify(ast::Formula &formula)
|
||||
{
|
||||
if (simplify<FirstSimplificationRule>(formula) == OperationResult::Changed)
|
||||
return OperationResult::Changed;
|
||||
if (simplify<FirstSimplificationRule>(formula) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return simplify<SecondSimplificationRule, OtherSimplificationRules...>(formula);
|
||||
}
|
||||
@@ -123,19 +122,19 @@ struct SimplificationRuleExistsWithoutQuantifiedVariables
|
||||
{
|
||||
static constexpr const auto Description = "exists () (F) === F";
|
||||
|
||||
static OperationResult apply(ast::Formula &formula)
|
||||
static SimplificationResult apply(ast::Formula &formula)
|
||||
{
|
||||
if (!formula.is<ast::Exists>())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
auto &exists = formula.get<ast::Exists>();
|
||||
|
||||
if (!exists.variables.empty())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
formula = std::move(exists.argument);
|
||||
|
||||
return OperationResult::Changed;
|
||||
return SimplificationResult::Simplified;
|
||||
}
|
||||
};
|
||||
|
||||
@@ -145,20 +144,20 @@ struct SimplificationRuleTrivialAssignmentInExists
|
||||
{
|
||||
static constexpr const auto Description = "exists X (X = Y) === #true";
|
||||
|
||||
static OperationResult apply(ast::Formula &formula)
|
||||
static SimplificationResult apply(ast::Formula &formula)
|
||||
{
|
||||
if (!formula.is<ast::Exists>())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
const auto &exists = formula.get<ast::Exists>();
|
||||
|
||||
if (!exists.argument.is<ast::Comparison>())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
const auto &comparison = exists.argument.get<ast::Comparison>();
|
||||
|
||||
if (comparison.operator_ != ast::Comparison::Operator::Equal)
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
const auto matchingAssignment = std::find_if(exists.variables.cbegin(), exists.variables.cend(),
|
||||
[&](const auto &variableDeclaration)
|
||||
@@ -168,11 +167,11 @@ struct SimplificationRuleTrivialAssignmentInExists
|
||||
});
|
||||
|
||||
if (matchingAssignment == exists.variables.cend())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
formula = ast::Formula::make<ast::Boolean>(true);
|
||||
|
||||
return OperationResult::Changed;
|
||||
return SimplificationResult::Simplified;
|
||||
}
|
||||
};
|
||||
|
||||
@@ -182,20 +181,20 @@ struct SimplificationRuleAssignmentInExists
|
||||
{
|
||||
static constexpr const auto Description = "exists X (X = t and F(X)) === exists () (F(t))";
|
||||
|
||||
static OperationResult apply(ast::Formula &formula)
|
||||
static SimplificationResult apply(ast::Formula &formula)
|
||||
{
|
||||
if (!formula.is<ast::Exists>())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
auto &exists = formula.get<ast::Exists>();
|
||||
|
||||
if (!exists.argument.is<ast::And>())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
auto &and_ = exists.argument.get<ast::And>();
|
||||
auto &arguments = and_.arguments;
|
||||
|
||||
auto simplificationResult = OperationResult::Unchanged;
|
||||
auto simplificationResult = SimplificationResult::Unchanged;
|
||||
|
||||
for (auto i = exists.variables.begin(); i != exists.variables.end();)
|
||||
{
|
||||
@@ -226,7 +225,7 @@ struct SimplificationRuleAssignmentInExists
|
||||
arguments.erase(j);
|
||||
|
||||
wasVariableReplaced = true;
|
||||
simplificationResult = OperationResult::Changed;
|
||||
simplificationResult = SimplificationResult::Simplified;
|
||||
|
||||
break;
|
||||
}
|
||||
@@ -250,19 +249,19 @@ struct SimplificationRuleEmptyConjunction
|
||||
{
|
||||
static constexpr const auto Description = "[empty conjunction] === #true";
|
||||
|
||||
static OperationResult apply(ast::Formula &formula)
|
||||
static SimplificationResult apply(ast::Formula &formula)
|
||||
{
|
||||
if (!formula.is<ast::And>())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
auto &and_ = formula.get<ast::And>();
|
||||
|
||||
if (!and_.arguments.empty())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
formula = ast::Formula::make<ast::Boolean>(true);
|
||||
|
||||
return OperationResult::Changed;
|
||||
return SimplificationResult::Simplified;
|
||||
}
|
||||
};
|
||||
|
||||
@@ -272,19 +271,19 @@ struct SimplificationRuleOneElementConjunction
|
||||
{
|
||||
static constexpr const auto Description = "[conjunction of only F] === F";
|
||||
|
||||
static OperationResult apply(ast::Formula &formula)
|
||||
static SimplificationResult apply(ast::Formula &formula)
|
||||
{
|
||||
if (!formula.is<ast::And>())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
auto &and_ = formula.get<ast::And>();
|
||||
|
||||
if (and_.arguments.size() != 1)
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
formula = std::move(and_.arguments.front());
|
||||
|
||||
return OperationResult::Changed;
|
||||
return SimplificationResult::Simplified;
|
||||
}
|
||||
};
|
||||
|
||||
@@ -294,19 +293,19 @@ struct SimplificationRuleTrivialExists
|
||||
{
|
||||
static constexpr const auto Description = "exists ... ([#true/#false]) === [#true/#false]";
|
||||
|
||||
static OperationResult apply(ast::Formula &formula)
|
||||
static SimplificationResult apply(ast::Formula &formula)
|
||||
{
|
||||
if (!formula.is<ast::Exists>())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
auto &exists = formula.get<ast::Exists>();
|
||||
|
||||
if (!exists.argument.is<ast::Boolean>())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
formula = std::move(exists.argument);
|
||||
|
||||
return OperationResult::Changed;
|
||||
return SimplificationResult::Simplified;
|
||||
}
|
||||
};
|
||||
|
||||
@@ -316,21 +315,21 @@ struct SimplificationRuleInWithPrimitiveArguments
|
||||
{
|
||||
static constexpr const auto Description = "[primitive A] in [primitive B] === A = B";
|
||||
|
||||
static OperationResult apply(ast::Formula &formula)
|
||||
static SimplificationResult apply(ast::Formula &formula)
|
||||
{
|
||||
if (!formula.is<ast::In>())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
auto &in = formula.get<ast::In>();
|
||||
|
||||
assert(ast::isPrimitive(in.element));
|
||||
|
||||
if (!ast::isPrimitive(in.element) || !ast::isPrimitive(in.set))
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
|
||||
|
||||
return OperationResult::Changed;
|
||||
return SimplificationResult::Simplified;
|
||||
}
|
||||
};
|
||||
|
||||
@@ -340,10 +339,10 @@ struct SimplificationRuleSubsumptionInBiconditionals
|
||||
{
|
||||
static constexpr const auto Description = "(F <-> (F and G)) === (F -> G)";
|
||||
|
||||
static OperationResult apply(ast::Formula &formula)
|
||||
static SimplificationResult apply(ast::Formula &formula)
|
||||
{
|
||||
if (!formula.is<ast::Biconditional>())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
auto &biconditional = formula.get<ast::Biconditional>();
|
||||
|
||||
@@ -354,7 +353,7 @@ struct SimplificationRuleSubsumptionInBiconditionals
|
||||
const auto rightIsAnd = biconditional.right.is<ast::And>();
|
||||
|
||||
if (!(leftIsPredicate && rightIsAnd) && !(rightIsPredicate && leftIsAnd))
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
auto &predicateSide = (leftIsPredicate ? biconditional.left : biconditional.right);
|
||||
auto &andSide = (leftIsPredicate ? biconditional.right : biconditional.left);
|
||||
@@ -368,13 +367,13 @@ struct SimplificationRuleSubsumptionInBiconditionals
|
||||
});
|
||||
|
||||
if (matchingPredicate == and_.arguments.cend())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
and_.arguments.erase(matchingPredicate);
|
||||
|
||||
formula = ast::Formula::make<ast::Implies>(std::move(predicateSide), std::move(andSide));
|
||||
|
||||
return OperationResult::Changed;
|
||||
return SimplificationResult::Simplified;
|
||||
}
|
||||
};
|
||||
|
||||
@@ -384,21 +383,21 @@ struct SimplificationRuleDoubleNegation
|
||||
{
|
||||
static constexpr const auto Description = "not not F === F";
|
||||
|
||||
static OperationResult apply(ast::Formula &formula)
|
||||
static SimplificationResult apply(ast::Formula &formula)
|
||||
{
|
||||
if (!formula.is<ast::Not>())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
auto ¬_ = formula.get<ast::Not>();
|
||||
|
||||
if (!not_.argument.is<ast::Not>())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
auto ¬Not = not_.argument.get<ast::Not>();
|
||||
|
||||
formula = std::move(notNot.argument);
|
||||
|
||||
return OperationResult::Changed;
|
||||
return SimplificationResult::Simplified;
|
||||
}
|
||||
};
|
||||
|
||||
@@ -408,15 +407,15 @@ struct SimplificationRuleDeMorganForConjunctions
|
||||
{
|
||||
static constexpr const auto Description = "(not (F and G)) === (not F or not G)";
|
||||
|
||||
static OperationResult apply(ast::Formula &formula)
|
||||
static SimplificationResult apply(ast::Formula &formula)
|
||||
{
|
||||
if (!formula.is<ast::Not>())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
auto ¬_ = formula.get<ast::Not>();
|
||||
|
||||
if (!not_.argument.is<ast::And>())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
auto &and_ = not_.argument.get<ast::And>();
|
||||
|
||||
@@ -425,7 +424,7 @@ struct SimplificationRuleDeMorganForConjunctions
|
||||
|
||||
formula = ast::Formula::make<ast::Or>(std::move(and_.arguments));
|
||||
|
||||
return OperationResult::Changed;
|
||||
return SimplificationResult::Simplified;
|
||||
}
|
||||
};
|
||||
|
||||
@@ -435,21 +434,21 @@ struct SimplificationRuleImplicationFromDisjunction
|
||||
{
|
||||
static constexpr const auto Description = "(not F or G) === (F -> G)";
|
||||
|
||||
static OperationResult apply(ast::Formula &formula)
|
||||
static SimplificationResult apply(ast::Formula &formula)
|
||||
{
|
||||
if (!formula.is<ast::Or>())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
auto &or_ = formula.get<ast::Or>();
|
||||
|
||||
if (or_.arguments.size() != 2)
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
const auto leftIsNot = or_.arguments[0].is<ast::Not>();
|
||||
const auto rightIsNot = or_.arguments[1].is<ast::Not>();
|
||||
|
||||
if (leftIsNot == rightIsNot)
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
auto &negativeSide = leftIsNot ? or_.arguments[0] : or_.arguments[1];
|
||||
auto &positiveSide = leftIsNot ? or_.arguments[1] : or_.arguments[0];
|
||||
@@ -461,7 +460,7 @@ struct SimplificationRuleImplicationFromDisjunction
|
||||
|
||||
formula = ast::Formula::make<ast::Implies>(std::move(negativeSideArgument), std::move(positiveSide));
|
||||
|
||||
return OperationResult::Changed;
|
||||
return SimplificationResult::Simplified;
|
||||
}
|
||||
};
|
||||
|
||||
@@ -471,15 +470,15 @@ struct SimplificationRuleNegatedComparison
|
||||
{
|
||||
static constexpr const auto Description = "(not F [comparison] G) === (F [negated comparison] G)";
|
||||
|
||||
static OperationResult apply(ast::Formula &formula)
|
||||
static SimplificationResult apply(ast::Formula &formula)
|
||||
{
|
||||
if (!formula.is<ast::Not>())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
auto ¬_ = formula.get<ast::Not>();
|
||||
|
||||
if (!not_.argument.is<ast::Comparison>())
|
||||
return OperationResult::Unchanged;
|
||||
return SimplificationResult::Unchanged;
|
||||
|
||||
auto &comparison = not_.argument.get<ast::Comparison>();
|
||||
|
||||
@@ -507,35 +506,7 @@ struct SimplificationRuleNegatedComparison
|
||||
|
||||
formula = std::move(comparison);
|
||||
|
||||
return OperationResult::Changed;
|
||||
}
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
struct SimplificationRuleIntegerSetInclusion
|
||||
{
|
||||
static constexpr const auto Description = "(F in G) === (F = G) if F and G are integer variables";
|
||||
|
||||
static OperationResult apply(ast::Formula &formula)
|
||||
{
|
||||
if (!formula.is<ast::In>())
|
||||
return OperationResult::Unchanged;
|
||||
|
||||
auto &in = formula.get<ast::In>();
|
||||
|
||||
const auto elementType = type(in.element);
|
||||
const auto setType = type(in.set);
|
||||
|
||||
if (elementType.domain != Domain::Integer || setType.domain != Domain::Integer
|
||||
|| elementType.setSize != SetSize::Unit || setType.setSize != SetSize::Unit)
|
||||
{
|
||||
return OperationResult::Unchanged;
|
||||
}
|
||||
|
||||
formula = ast::Formula::make<ast::Comparison>(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
|
||||
|
||||
return OperationResult::Changed;
|
||||
return SimplificationResult::Simplified;
|
||||
}
|
||||
};
|
||||
|
||||
@@ -555,8 +526,7 @@ const auto simplifyWithDefaultRules =
|
||||
SimplificationRuleSubsumptionInBiconditionals,
|
||||
SimplificationRuleDeMorganForConjunctions,
|
||||
SimplificationRuleImplicationFromDisjunction,
|
||||
SimplificationRuleNegatedComparison,
|
||||
SimplificationRuleIntegerSetInclusion
|
||||
SimplificationRuleNegatedComparison
|
||||
>;
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
@@ -565,7 +535,7 @@ const auto simplifyWithDefaultRules =
|
||||
struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<SimplifyFormulaVisitor>
|
||||
{
|
||||
// Do nothing for all other types of expressions
|
||||
static OperationResult accept(ast::Formula &formula)
|
||||
static SimplificationResult accept(ast::Formula &formula)
|
||||
{
|
||||
return simplifyWithDefaultRules(formula);
|
||||
}
|
||||
@@ -575,7 +545,7 @@ struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<Simplif
|
||||
|
||||
void simplify(ast::Formula &formula)
|
||||
{
|
||||
while (formula.accept(SimplifyFormulaVisitor(), formula) == OperationResult::Changed);
|
||||
while (formula.accept(SimplifyFormulaVisitor(), formula) == SimplificationResult::Simplified);
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
@@ -147,15 +147,15 @@ void translate(const char *fileName, std::istream &stream, Context &context)
|
||||
{
|
||||
auto ¶meter = predicateDeclaration->parameters[i];
|
||||
|
||||
if (parameter.domain != Domain::Integer)
|
||||
if (parameter.domain != ast::Domain::Integer)
|
||||
continue;
|
||||
|
||||
context.logger.outputStream()
|
||||
<< output::Keyword("int")
|
||||
<< "(" << predicateDeclaration->name
|
||||
<< "/" << output::Number(predicateDeclaration->arity())
|
||||
<< "@" << output::Number(i + 1)
|
||||
<< ")" << std::endl;
|
||||
<< "@" << output::Number(i)
|
||||
<< ")." << std::endl;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user