Version bump for release 0.1.7 RC 1

This adds support for declaring predicates as placeholders through the
“#external” directive in the input language of clingo.

Placeholders are not subject to completion. This prevents predicates
that represent instance-specific facts from being assumed as universally
false by default negation when translating an encoding.

This stretches clingo’s usual syntax a bit in order to make the
implementation lightweight. In order to declare a predicate with a
specific arity as a placeholder, the following statement needs to be
added to the input program:

.ci/Dockerfile-ubuntu-18.04

@@ -3,7 +3,7 @@ FROM ubuntu:18.04
 ARG toolchain
 
 RUN apt-get update
-RUN apt-get install -y bison cmake git ninja-build re2c
+RUN apt-get install -y cmake git ninja-build re2c
 RUN if [ "${toolchain}" = "gcc" ]; then apt-get install -y g++; fi
 RUN if [ "${toolchain}" = "clang" ]; then apt-get install -y clang; fi
 

CHANGELOG.md

@@ -1,26 +1,14 @@
 # Change Log
 
-## 0.1.8 RC 3 (2018-04-12)
+## 0.1.7 (2018-04-05)
 
-### Features
+Features:
-
-* more and advanced simplification rules
-* adds support for exponentiation (power) and modulus (absolute value)
-* new examples: prime numbers, permutation generator, and graph coloring (extended)
-
-## 0.1.7 (2018-04-08)
-
-### Features
 
 * support for declaring placeholders with the `#external` directive
 
-### Internal
-
-* drops Boost dependency in favor of the header-only command-line option library [cxxopts](https://github.com/jarro2783/cxxopts)
-
 ## 0.1.6 (2017-06-12)
 
-### Features
+Features:
 
 * unique IDs for all variables (user-defined variables are renamed)
 * support for hiding predicates from completed output by using `#show` statements
@@ -28,7 +16,7 @@
 * command-line option `--parentheses` to fully parenthesize the output
 * adds multiple example instances for experimenting
 
-### Bug Fixes
+Bug Fixes:
 
 * adds missing error message when attempting to read inaccessible file
 * removes unnecessary parentheses after simplification
@@ -36,52 +24,52 @@
 
 ## 0.1.5 (2017-05-04)
 
-### Bug Fixes
+Bug Fixes:
 
 * fixes lost signs with negated 0-ary predicates
 
 ## 0.1.4 (2017-04-12)
 
-### Features
+Features:
 
 * completion of input programs (optional)
 * command-line option `--complete` to turn on completion
 
 ## 0.1.3 (2017-03-30)
 
-### Features
+Features:
 
 * support for anonymous variables
 
-### Bug Fixes
+Bug Fixes:
 
 * fixes incorrectly simplified rules with comparisons
 * fixes misleading error message concerning negated, unsupported body literals
 
 ## 0.1.2 (2017-03-23)
 
-### Features
+Features:
 
 * simplification of output formulas (optional)
 * command-line option `--simplify` to turn on simplification
 
-### Bug Fixes
+Bug Fixes:
 
 * fixes incorrectly translated choice rules with multiple elements in the head aggregate
 
-### Internal
+Internal:
 
 * explicit syntax tree representation for first-order formulas
 
 ## 0.1.1 (2017-03-06)
 
-### Features
+Features:
 
 * support for choice rules (without guards)
 
 ## 0.1.0 (2016-11-24)
 
-### Features
+Features:
 
 * initial support for translating rules in *Essential Gringo* (excluding aggregates) to first-order logic formulas
 * command-line option `--color` to autodetect, enable, or disable color output

LICENSE.md

@@ -1,6 +1,6 @@
 # The MIT License (MIT)
 
-Copyright © 2016–2018 Patrick Lühne
+Copyright © 2016–2017 Patrick Lühne
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

README.md

@@ -9,11 +9,10 @@
 ## Usage
 
 ```bash
-$ anthem [--complete] [--simplify] file...
+$ anthem [--simplify] file...
 ```
 
-`--complete` instructs `anthem` to perform Clark’s completion on the translated formulas.
+With the option `--simplify`, output formulas are simplified by applying several basic transformation rules.
-With the option `--simplify`, the output formulas are simplified by applying several basic transformation rules.
 
 ## Building
 

app/main.cpp

@@ -70,7 +70,7 @@ int main(int argc, char **argv)
 
 	if (version)
 	{
-		std::cout << "anthem version 0.1.8-rc.3" << std::endl;
+		std::cout << "anthem version 0.1.7-rc.1" << std::endl;
 		return EXIT_SUCCESS;
 	}
 

examples/graph-coloring.lp

@@ -1,10 +1,12 @@
-#external color(1).
+colored(V, red) :- vertex(V), not colored(V, green), not colored(V, blue).
-#external edge(2).
+colored(V, green) :- vertex(V), not colored(V, red), not colored(V, blue).
-#external vertex(1).
+colored(V, blue) :- vertex(V), not colored(V, red), not colored(V, green).
-#show color/2.
 
-{color(V, C)} :- vertex(V), color(C).
+:- edge(V1, V2), colored(V1, C), colored(V2, C).
-covered(V) :- color(V, _).
+
-:- vertex(V), not covered(V).
+vertex(a).
-:- color(V1, C), color(V2, C), edge(V1, V2).
+vertex(b).
-:- color(V, C1), color(V, C2), C1 != C2.
+vertex(c).
+
+edge(a, b).
+edge(a, c).

examples/permutations.lp

@@ -1,12 +0,0 @@
-{p(1..n, 1..n)}.
-
-:- p(X, Y1), p(X, Y2), Y1 != Y2.
-:- p(X1, Y), p(X2, Y), X1 != X2.
-
-q1(X) :- p(X, _).
-q2(Y) :- p(_, Y).
-
-:- not q1(X), X = 1..n.
-:- not q2(Y), Y = 1..n.
-
-#show p/2.

examples/prime.lp

@@ -1,4 +0,0 @@
-#show prime/1.
-
-composite(I * J) :- I = 2..n, J = 2..n.
-prime(N) :- N = 2..n, not composite(N).

examples/schur-numbers.lp

@@ -3,5 +3,3 @@ covered(I) :- in(I, S).
 
 :- I = 1..n, not covered(I).
 :- in(I, S), in(J, S), in(I + J, S).
-
-#show in/2.

include/anthem/AST.h

@@ -32,8 +32,7 @@ struct BinaryOperation
 		Minus,
 		Multiplication,
 		Division,
-		Modulo,
+		Modulo
-		Power
 	};
 
 	explicit BinaryOperation(Operator operator_, Term &&left, Term &&right)
@@ -293,30 +292,6 @@ struct String
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct UnaryOperation
-{
-	enum class Operator
-	{
-		Absolute
-	};
-
-	explicit UnaryOperation(Operator operator_, Term &&argument)
-	:	operator_{operator_},
-		argument{std::move(argument)}
-	{
-	}
-
-	UnaryOperation(const UnaryOperation &other) = delete;
-	UnaryOperation &operator=(const UnaryOperation &other) = delete;
-	UnaryOperation(UnaryOperation &&other) noexcept = default;
-	UnaryOperation &operator=(UnaryOperation &&other) noexcept = default;
-
-	Operator operator_;
-	Term argument;
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 struct Variable
 {
 	explicit Variable(VariableDeclaration *declaration)

include/anthem/ASTForward.h

@@ -37,7 +37,6 @@ struct Or;
 struct Predicate;
 struct SpecialInteger;
 struct String;
-struct UnaryOperation;
 struct Variable;
 struct VariableDeclaration;
 using VariableDeclarationPointer = std::unique_ptr<VariableDeclaration>;
@@ -69,7 +68,6 @@ using Term = Clingo::Variant<
 	Interval,
 	SpecialInteger,
 	String,
-	UnaryOperation,
 	Variable>;
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

include/anthem/ASTUtils.h

@@ -5,7 +5,6 @@
 
 #include <anthem/AST.h>
 #include <anthem/ASTVisitors.h>
-#include <anthem/Context.h>
 
 namespace anthem
 {
@@ -41,7 +40,7 @@ class VariableStack
 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);
+void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures);
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 // Replacing Variables

include/anthem/ASTVisitors.h

@@ -165,14 +165,6 @@ struct RecursiveTermVisitor
 		return T::accept(string, term, std::forward<Arguments>(arguments)...);
 	}
 
-	template <class... Arguments>
-	ReturnType visit(UnaryOperation &unaryOperation, Term &term, Arguments &&... arguments)
-	{
-		unaryOperation.argument.accept(*this, unaryOperation.argument, std::forward<Arguments>(arguments)...);
-
-		return T::accept(unaryOperation, term, std::forward<Arguments>(arguments)...);
-	}
-
 	template <class... Arguments>
 	ReturnType visit(Variable &variable, Term &term, Arguments &&... arguments)
 	{

include/anthem/Context.h

@@ -16,14 +16,6 @@ namespace anthem
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct PredicateSignatureMeta
-{
-	ast::PredicateSignature predicateSignature;
-	bool used{false};
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 struct Context
 {
 	Context() = default;
@@ -38,8 +30,8 @@ struct Context
 	bool performSimplification = false;
 	bool performCompletion = false;
 
-	std::optional<std::vector<PredicateSignatureMeta>> visiblePredicateSignatures;
+	std::optional<std::vector<ast::PredicateSignature>> visiblePredicateSignatures;
-	std::optional<std::vector<PredicateSignatureMeta>> externalPredicateSignatures;
+	std::optional<std::vector<ast::PredicateSignature>> externalPredicateSignatures;
 
 	ast::ParenthesisStyle parenthesisStyle = ast::ParenthesisStyle::Normal;
 };

include/anthem/Equality.h

@@ -1,430 +0,0 @@
-#ifndef __ANTHEM__EQUALITY_H
-#define __ANTHEM__EQUALITY_H
-
-#include <anthem/AST.h>
-#include <anthem/ASTUtils.h>
-
-namespace anthem
-{
-namespace ast
-{
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-//
-// Equality
-//
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-// TODO: move to separate class
-enum class Tristate
-{
-	True,
-	False,
-	Unknown,
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-Tristate equal(const Formula &lhs, const Formula &rhs);
-Tristate equal(const Term &lhs, const Term &rhs);
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct FormulaEqualityVisitor
-{
-	Tristate visit(const And &and_, const Formula &otherFormula)
-	{
-		if (!otherFormula.is<And>())
-			return Tristate::Unknown;
-
-		const auto &otherAnd = otherFormula.get<And>();
-
-		for (const auto &argument : and_.arguments)
-		{
-			const auto match = std::find_if(
-				otherAnd.arguments.cbegin(), otherAnd.arguments.cend(),
-				[&](const auto &otherArgument)
-				{
-					return equal(argument, otherArgument) == Tristate::True;
-				});
-
-			if (match == otherAnd.arguments.cend())
-				return Tristate::Unknown;
-		}
-
-		for (const auto &otherArgument : otherAnd.arguments)
-		{
-			const auto match = std::find_if(
-				and_.arguments.cbegin(), and_.arguments.cend(),
-				[&](const auto &argument)
-				{
-					return equal(otherArgument, argument) == Tristate::True;
-				});
-
-			if (match == and_.arguments.cend())
-				return Tristate::Unknown;
-		}
-
-		return Tristate::True;
-	}
-
-	Tristate visit(const Biconditional &biconditional, const Formula &otherFormula)
-	{
-		if (!otherFormula.is<Biconditional>())
-			return Tristate::Unknown;
-
-		const auto &otherBiconditional = otherFormula.get<Biconditional>();
-
-		if (equal(biconditional.left, otherBiconditional.left) == Tristate::True
-		    && equal(biconditional.right, otherBiconditional.right) == Tristate::True)
-		{
-			return Tristate::True;
-		}
-
-		if (equal(biconditional.left, otherBiconditional.right) == Tristate::True
-		    && equal(biconditional.right, otherBiconditional.left) == Tristate::True)
-		{
-			return Tristate::True;
-		}
-
-		return Tristate::Unknown;
-	}
-
-	Tristate visit(const Boolean &boolean, const Formula &otherFormula)
-	{
-		if (!otherFormula.is<Boolean>())
-			return Tristate::Unknown;
-
-		const auto &otherBoolean = otherFormula.get<Boolean>();
-
-		return (boolean.value == otherBoolean.value)
-			? Tristate::True
-			: Tristate::False;
-	}
-
-	Tristate visit(const Comparison &comparison, const Formula &otherFormula)
-	{
-		if (!otherFormula.is<Comparison>())
-			return Tristate::Unknown;
-
-		const auto &otherComparison = otherFormula.get<Comparison>();
-
-		if (comparison.operator_ != otherComparison.operator_)
-			return Tristate::Unknown;
-
-		if (equal(comparison.left, otherComparison.left) == Tristate::True
-		    && equal(comparison.right, otherComparison.right) == Tristate::True)
-		{
-			return Tristate::True;
-		}
-
-		// Only = and != are commutative operators, all others don’t need to be checked with exchanged arguments
-		if (comparison.operator_ != Comparison::Operator::Equal
-		    && comparison.operator_ != Comparison::Operator::NotEqual)
-		{
-			return Tristate::Unknown;
-		}
-
-		if (equal(comparison.left, otherComparison.right) == Tristate::True
-		    && equal(comparison.right, otherComparison.left) == Tristate::True)
-		{
-			return Tristate::True;
-		}
-
-		return Tristate::Unknown;
-	}
-
-	Tristate visit(const Exists &, const Formula &otherFormula)
-	{
-		if (!otherFormula.is<Exists>())
-			return Tristate::Unknown;
-
-		// TODO: implement stronger check
-		return Tristate::Unknown;
-	}
-
-	Tristate visit(const ForAll &, const Formula &otherFormula)
-	{
-		if (!otherFormula.is<ForAll>())
-			return Tristate::Unknown;
-
-		// TODO: implement stronger check
-		return Tristate::Unknown;
-	}
-
-	Tristate visit(const Implies &implies, const Formula &otherFormula)
-	{
-		if (!otherFormula.is<Implies>())
-			return Tristate::Unknown;
-
-		const auto &otherImplies = otherFormula.get<Implies>();
-
-		if (equal(implies.antecedent, otherImplies.antecedent) == Tristate::True
-		    && equal(implies.consequent, otherImplies.consequent) == Tristate::True)
-		{
-			return Tristate::True;
-		}
-
-		return Tristate::Unknown;
-	}
-
-	Tristate visit(const In &in, const Formula &otherFormula)
-	{
-		if (!otherFormula.is<In>())
-			return Tristate::Unknown;
-
-		const auto &otherIn = otherFormula.get<In>();
-
-		if (equal(in.element, otherIn.element) == Tristate::True
-		    && equal(in.set, otherIn.set) == Tristate::True)
-		{
-			return Tristate::True;
-		}
-
-		return Tristate::Unknown;
-	}
-
-	Tristate visit(const Not &not_, const Formula &otherFormula)
-	{
-		if (!otherFormula.is<Not>())
-			return Tristate::Unknown;
-
-		const auto &otherNot = otherFormula.get<Not>();
-
-		return equal(not_.argument, otherNot.argument);
-	}
-
-	Tristate visit(const Or &or_, const Formula &otherFormula)
-	{
-		if (!otherFormula.is<Or>())
-			return Tristate::Unknown;
-
-		const auto &otherOr = otherFormula.get<Or>();
-
-		for (const auto &argument : or_.arguments)
-		{
-			const auto match = std::find_if(
-				otherOr.arguments.cbegin(), otherOr.arguments.cend(),
-				[&](const auto &otherArgument)
-				{
-					return equal(argument, otherArgument) == Tristate::True;
-				});
-
-			if (match == otherOr.arguments.cend())
-				return Tristate::Unknown;
-		}
-
-		for (const auto &otherArgument : otherOr.arguments)
-		{
-			const auto match = std::find_if(
-				or_.arguments.cbegin(), or_.arguments.cend(),
-				[&](const auto &argument)
-				{
-					return equal(otherArgument, argument) == Tristate::True;
-				});
-
-			if (match == or_.arguments.cend())
-				return Tristate::Unknown;
-		}
-
-		return Tristate::True;
-	}
-
-	Tristate visit(const Predicate &predicate, const Formula &otherFormula)
-	{
-		if (!otherFormula.is<Predicate>())
-			return Tristate::Unknown;
-
-		const auto &otherPredicate = otherFormula.get<Predicate>();
-
-		if (!matches(predicate, otherPredicate))
-			return Tristate::False;
-
-		assert(predicate.arguments.size() == otherPredicate.arguments.size());
-
-		for (size_t i = 0; i < predicate.arguments.size(); i++)
-			if (equal(predicate.arguments[i], otherPredicate.arguments[i]) != Tristate::True)
-				return Tristate::Unknown;
-
-		return Tristate::True;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct TermEqualityVisitor
-{
-	Tristate visit(const BinaryOperation &binaryOperation, const Term &otherTerm)
-	{
-		if (!otherTerm.is<BinaryOperation>())
-			return Tristate::Unknown;
-
-		const auto &otherBinaryOperation = otherTerm.get<BinaryOperation>();
-
-		if (binaryOperation.operator_ != otherBinaryOperation.operator_)
-			return Tristate::Unknown;
-
-		if (equal(binaryOperation.left, otherBinaryOperation.left) == Tristate::True
-		    && equal(binaryOperation.right, otherBinaryOperation.right) == Tristate::True)
-		{
-			return Tristate::True;
-		}
-
-		// Only + and * are commutative operators, all others don’t need to be checked with exchanged arguments
-		if (binaryOperation.operator_ != BinaryOperation::Operator::Plus
-		    && binaryOperation.operator_ != BinaryOperation::Operator::Multiplication)
-		{
-			return Tristate::Unknown;
-		}
-
-		if (equal(binaryOperation.left, binaryOperation.right) == Tristate::True
-		    && equal(binaryOperation.right, binaryOperation.left) == Tristate::True)
-		{
-			return Tristate::True;
-		}
-
-		return Tristate::Unknown;
-	}
-
-	Tristate visit(const Boolean &boolean, const Term &otherTerm)
-	{
-		if (!otherTerm.is<Boolean>())
-			return Tristate::Unknown;
-
-		const auto &otherBoolean = otherTerm.get<Boolean>();
-
-		return (boolean.value == otherBoolean.value)
-			? Tristate::True
-			: Tristate::False;
-	}
-
-	Tristate visit(const Constant &constant, const Term &otherTerm)
-	{
-		if (!otherTerm.is<Constant>())
-			return Tristate::Unknown;
-
-		const auto &otherConstant = otherTerm.get<Constant>();
-
-		return (constant.name == otherConstant.name)
-			? Tristate::True
-			: Tristate::False;
-	}
-
-	Tristate visit(const Function &function, const Term &otherTerm)
-	{
-		if (!otherTerm.is<Function>())
-			return Tristate::Unknown;
-
-		const auto &otherFunction = otherTerm.get<Function>();
-
-		if (function.name != otherFunction.name)
-			return Tristate::False;
-
-		if (function.arguments.size() != otherFunction.arguments.size())
-			return Tristate::False;
-
-		for (size_t i = 0; i < function.arguments.size(); i++)
-			if (equal(function.arguments[i], otherFunction.arguments[i]) != Tristate::True)
-				return Tristate::Unknown;
-
-		return Tristate::True;
-	}
-
-	Tristate visit(const Integer &integer, const Term &otherTerm)
-	{
-		if (!otherTerm.is<Integer>())
-			return Tristate::Unknown;
-
-		const auto &otherInteger = otherTerm.get<Integer>();
-
-		return (integer.value == otherInteger.value)
-			? Tristate::True
-			: Tristate::False;
-	}
-
-	Tristate visit(const Interval &interval, const Term &otherTerm)
-	{
-		if (!otherTerm.is<Interval>())
-			return Tristate::Unknown;
-
-		const auto &otherInterval = otherTerm.get<Interval>();
-
-		if (equal(interval.from, otherInterval.from) != Tristate::True)
-			return Tristate::Unknown;
-
-		if (equal(interval.to, otherInterval.to) != Tristate::True)
-			return Tristate::Unknown;
-
-		return Tristate::True;
-	}
-
-	Tristate visit(const SpecialInteger &specialInteger, const Term &otherTerm)
-	{
-		if (!otherTerm.is<SpecialInteger>())
-			return Tristate::Unknown;
-
-		const auto &otherSpecialInteger = otherTerm.get<SpecialInteger>();
-
-		return (specialInteger.type == otherSpecialInteger.type)
-			? Tristate::True
-			: Tristate::False;
-	}
-
-	Tristate visit(const String &string, const Term &otherTerm)
-	{
-		if (!otherTerm.is<String>())
-			return Tristate::Unknown;
-
-		const auto &otherString = otherTerm.get<String>();
-
-		return (string.text == otherString.text)
-			? Tristate::True
-			: Tristate::False;
-	}
-
-	Tristate visit(const UnaryOperation &unaryOperation, const Term &otherTerm)
-	{
-		if (!otherTerm.is<UnaryOperation>())
-			return Tristate::Unknown;
-
-		const auto &otherUnaryOperation = otherTerm.get<UnaryOperation>();
-
-		if (unaryOperation.operator_ != otherUnaryOperation.operator_)
-			return Tristate::Unknown;
-
-		return equal(unaryOperation.argument, otherUnaryOperation.argument);
-	}
-
-	Tristate visit(const Variable &variable, const Term &otherTerm)
-	{
-		if (!otherTerm.is<Variable>())
-			return Tristate::Unknown;
-
-		const auto &otherVariable = otherTerm.get<Variable>();
-
-		return (variable.declaration == otherVariable.declaration)
-			? Tristate::True
-			: Tristate::False;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-Tristate equal(const Formula &lhs, const Formula &rhs)
-{
-	return lhs.accept(FormulaEqualityVisitor(), rhs);
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-Tristate equal(const Term &lhs, const Term &rhs)
-{
-	return lhs.accept(TermEqualityVisitor(), rhs);
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-}
-}
-
-#endif

include/anthem/Simplification.h

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

include/anthem/SimplificationVisitors.h

@@ -1,198 +0,0 @@
-#ifndef __ANTHEM__SIMPLIFICATION_VISITORS_H
-#define __ANTHEM__SIMPLIFICATION_VISITORS_H
-
-#include <anthem/AST.h>
-#include <anthem/Simplification.h>
-
-namespace anthem
-{
-namespace ast
-{
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-//
-// Simplification Visitor
-//
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-template<class T>
-struct FormulaSimplificationVisitor
-{
-	template <class... Arguments>
-	SimplificationResult visit(And &and_, Formula &formula, Arguments &&... arguments)
-	{
-		for (auto &argument : and_.arguments)
-			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>
-	SimplificationResult visit(Biconditional &biconditional, Formula &formula, Arguments &&... arguments)
-	{
-		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)...) == SimplificationResult::Simplified)
-			return SimplificationResult::Simplified;
-
-		return T::accept(formula, std::forward<Arguments>(arguments)...);
-	}
-
-	template <class... Arguments>
-	SimplificationResult visit(Boolean &, Formula &formula, Arguments &&... arguments)
-	{
-		return T::accept(formula, std::forward<Arguments>(arguments)...);
-	}
-
-	template <class... Arguments>
-	SimplificationResult visit(Comparison &, Formula &formula, Arguments &&... arguments)
-	{
-		return T::accept(formula, std::forward<Arguments>(arguments)...);
-	}
-
-	template <class... Arguments>
-	SimplificationResult visit(Exists &exists, Formula &formula, Arguments &&... arguments)
-	{
-		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>
-	SimplificationResult visit(ForAll &forAll, Formula &formula, Arguments &&... arguments)
-	{
-		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>
-	SimplificationResult visit(Implies &implies, Formula &formula, Arguments &&... arguments)
-	{
-		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)...) == SimplificationResult::Simplified)
-			return SimplificationResult::Simplified;
-
-		return T::accept(formula, std::forward<Arguments>(arguments)...);
-	}
-
-	template <class... Arguments>
-	SimplificationResult visit(In &, Formula &formula, Arguments &&... arguments)
-	{
-		return T::accept(formula, std::forward<Arguments>(arguments)...);
-	}
-
-	template <class... Arguments>
-	SimplificationResult visit(Not &not_, Formula &formula, Arguments &&... arguments)
-	{
-		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>
-	SimplificationResult visit(Or &or_, Formula &formula, Arguments &&... arguments)
-	{
-		for (auto &argument : or_.arguments)
-			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>
-	SimplificationResult visit(Predicate &, Formula &formula, Arguments &&... arguments)
-	{
-		return T::accept(formula, std::forward<Arguments>(arguments)...);
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-template<class T, class SimplificationResult = void>
-struct TermSimplificationVisitor
-{
-	template <class... Arguments>
-	SimplificationResult visit(BinaryOperation &binaryOperation, Term &term, Arguments &&... arguments)
-	{
-		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)...) == SimplificationResult::Simplified)
-			return SimplificationResult::Simplified;
-
-		return T::accept(term, std::forward<Arguments>(arguments)...);
-	}
-
-	template <class... Arguments>
-	SimplificationResult visit(Boolean &, Term &term, Arguments &&... arguments)
-	{
-		return T::accept(term, std::forward<Arguments>(arguments)...);
-	}
-
-	template <class... Arguments>
-	SimplificationResult visit(Constant &, Term &term, Arguments &&... arguments)
-	{
-		return T::accept(term, std::forward<Arguments>(arguments)...);
-	}
-
-	template <class... Arguments>
-	SimplificationResult visit(Function &function, Term &term, Arguments &&... arguments)
-	{
-		for (auto &argument : function.arguments)
-			if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
-				return SimplificationResult::Simplified;
-
-		return T::accept(term, std::forward<Arguments>(arguments)...);
-	}
-
-	template <class... Arguments>
-	SimplificationResult visit(Integer &, Term &term, Arguments &&... arguments)
-	{
-		return T::accept(term, std::forward<Arguments>(arguments)...);
-	}
-
-	template <class... Arguments>
-	SimplificationResult visit(Interval &interval, Term &term, Arguments &&... arguments)
-	{
-		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)...) == SimplificationResult::Simplified)
-			return SimplificationResult::Simplified;
-
-		return T::accept(term, std::forward<Arguments>(arguments)...);
-	}
-
-	template <class... Arguments>
-	SimplificationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments)
-	{
-		return T::accept(term, std::forward<Arguments>(arguments)...);
-	}
-
-	template <class... Arguments>
-	SimplificationResult visit(String &, Term &term, Arguments &&... arguments)
-	{
-		return T::accept(term, std::forward<Arguments>(arguments)...);
-	}
-
-	template <class... Arguments>
-	SimplificationResult visit(Variable &, Term &term, Arguments &&... arguments)
-	{
-		return T::accept(term, std::forward<Arguments>(arguments)...);
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-}
-}
-
-#endif

include/anthem/StatementVisitor.h

@@ -176,8 +176,7 @@ struct StatementVisitor
 
 		context.logger.log(output::Priority::Debug, statement.location) << "showing “" << signature.name() << "/" << signature.arity() << "”";
 
-		auto predicateSignature = ast::PredicateSignature{std::string(signature.name()), signature.arity()};
+		context.visiblePredicateSignatures.value().emplace_back(std::string(signature.name()), signature.arity());
-		context.visiblePredicateSignatures.value().emplace_back(PredicateSignatureMeta{std::move(predicateSignature)});
 	}
 
 	void visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &)
@@ -214,13 +213,12 @@ struct StatementVisitor
 		if (aritySymbol.type() != Clingo::SymbolType::Number)
 			fail();
 
-		const size_t arity = arityArgument.data.get<Clingo::Symbol>().number();
+		const auto &arity = arityArgument.data.get<Clingo::Symbol>().number();
 
 		if (!context.externalPredicateSignatures)
 			context.externalPredicateSignatures.emplace();
 
-		auto predicateSignature = ast::PredicateSignature{std::string(predicate.name), arity};
+		context.externalPredicateSignatures->emplace_back(std::string(predicate.name), arity);
-		context.externalPredicateSignatures->emplace_back(PredicateSignatureMeta{std::move(predicateSignature)});
 	}
 
 	template<class T>

include/anthem/Term.h

@@ -23,12 +23,6 @@ ast::BinaryOperation::Operator translate(Clingo::AST::BinaryOperator binaryOpera
 {
 	switch (binaryOperator)
 	{
-		case Clingo::AST::BinaryOperator::XOr:
-			throw TranslationException(term.location, "binary operation “xor” currently unsupported");
-		case Clingo::AST::BinaryOperator::Or:
-			throw TranslationException(term.location, "binary operation “or” currently unsupported");
-		case Clingo::AST::BinaryOperator::And:
-			throw TranslationException(term.location, "binary operation “and” currently unsupported");
 		case Clingo::AST::BinaryOperator::Plus:
 			return ast::BinaryOperation::Operator::Plus;
 		case Clingo::AST::BinaryOperator::Minus:
@@ -39,28 +33,11 @@ ast::BinaryOperation::Operator translate(Clingo::AST::BinaryOperator binaryOpera
 			return ast::BinaryOperation::Operator::Division;
 		case Clingo::AST::BinaryOperator::Modulo:
 			return ast::BinaryOperation::Operator::Modulo;
-		case Clingo::AST::BinaryOperator::Power:
+		default:
-			return ast::BinaryOperation::Operator::Power;
+			throw TranslationException(term.location, "“binary operation” terms currently unsupported");
 	}
 
-	throw TranslationException(term.location, "unknown binary operation");
+	return ast::BinaryOperation::Operator::Plus;
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-ast::UnaryOperation::Operator translate(Clingo::AST::UnaryOperator unaryOperator, const Clingo::AST::Term &term)
-{
-	switch (unaryOperator)
-	{
-		case Clingo::AST::UnaryOperator::Absolute:
-			return ast::UnaryOperation::Operator::Absolute;
-		case Clingo::AST::UnaryOperator::Minus:
-			throw TranslationException(term.location, "binary operation “minus” currently unsupported");
-		case Clingo::AST::UnaryOperator::Negation:
-			throw TranslationException(term.location, "binary operation “negation” currently unsupported");
-	}
-
-	throw TranslationException(term.location, "unknown unary operation");
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -123,6 +100,12 @@ struct TermTranslateVisitor
 		return ast::Term::make<ast::Variable>(ruleContext.freeVariables.back().get());
 	}
 
+	std::optional<ast::Term> visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, RuleContext &, const ast::VariableStack &)
+	{
+		throw TranslationException(term.location, "“unary operation” terms currently unsupported");
+		return std::nullopt;
+	}
+
 	std::optional<ast::Term> visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 	{
 		const auto operator_ = translate(binaryOperation.binary_operator, term);
@@ -132,14 +115,6 @@ struct TermTranslateVisitor
 		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)
-	{
-		const auto operator_ = translate(unaryOperation.unary_operator, term);
-		auto argument = translate(unaryOperation.argument, ruleContext, variableStack);
-
-		return ast::Term::make<ast::UnaryOperation>(operator_, std::move(argument));
-	}
-
 	std::optional<ast::Term> visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 	{
 		auto left = translate(interval.left, ruleContext, variableStack);

include/anthem/output/AST.h

@@ -41,39 +41,37 @@ struct PrintContext
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-output::ColorStream &print(output::ColorStream &stream, const BinaryOperation::Operator operator_, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const BinaryOperation::Operator operator_, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext);
-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);
-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);
-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);
-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);
-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);
-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);
-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);
-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);
-output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &printContext);
-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);
-output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const UnaryOperation &unaryOperation, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext, bool omitParentheses = false);
 
-output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext);
 
-output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext);
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 // Primitives
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::Operator operator_, PrintContext &, bool)
+inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::Operator operator_, PrintContext &)
 {
 	switch (operator_)
 	{
@@ -87,8 +85,6 @@ inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::
 			return (stream << output::Operator("/"));
 		case BinaryOperation::Operator::Modulo:
 			return (stream << output::Operator("%"));
-		case BinaryOperation::Operator::Power:
-			return (stream << output::Operator("**"));
 	}
 
 	return stream;
@@ -96,26 +92,22 @@ inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext, bool omitParentheses)
+inline output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext)
 {
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+	stream << "(";
-		stream << "(";
-
 	print(stream, binaryOperation.left, printContext);
 	stream << " ";
 	print(stream, binaryOperation.operator_, printContext);
 	stream << " ";
 	print(stream, binaryOperation.right, printContext);
-
+	stream << ")";
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
-		stream << ")";
 
 	return stream;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &)
 {
 	if (boolean.value)
 		return (stream << output::Boolean("#true"));
@@ -125,7 +117,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Boolean &bo
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, Comparison::Operator operator_, PrintContext &, bool)
+inline output::ColorStream &print(output::ColorStream &stream, Comparison::Operator operator_, PrintContext &)
 {
 	switch (operator_)
 	{
@@ -148,7 +140,7 @@ inline output::ColorStream &print(output::ColorStream &stream, Comparison::Opera
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -167,14 +159,14 @@ inline output::ColorStream &print(output::ColorStream &stream, const Comparison
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &)
 {
 	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)
 {
 	stream << function.name;
 
@@ -201,7 +193,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Function &f
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -218,14 +210,14 @@ inline output::ColorStream &print(output::ColorStream &stream, const In &in, Pri
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &)
 {
 	return (stream << output::Number<int>(integer.value));
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -242,7 +234,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)
 {
 	stream << predicate.name;
 
@@ -266,7 +258,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Predicate &
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &)
 {
 	switch (specialInteger.type)
 	{
@@ -281,37 +273,14 @@ inline output::ColorStream &print(output::ColorStream &stream, const SpecialInte
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &)
 {
 	return (stream << output::String(string.text.c_str()));
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const UnaryOperation &unaryOperation, PrintContext &printContext, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext)
-{
-	switch (unaryOperation.operator_)
-	{
-		case UnaryOperation::Operator::Absolute:
-			stream << "|";
-			break;
-	}
-
-	print(stream, unaryOperation.argument, printContext, true);
-
-	switch (unaryOperation.operator_)
-	{
-		case UnaryOperation::Operator::Absolute:
-			stream << "|";
-			break;
-	}
-
-	return stream;
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-inline output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext, bool)
 {
 	assert(variable.declaration != nullptr);
 
@@ -320,7 +289,7 @@ 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)
 {
 	const auto printVariableDeclaration =
 		[&stream, &variableDeclaration](const auto *prefix, auto &variableIDs) -> output::ColorStream &
@@ -356,10 +325,9 @@ inline output::ColorStream &print(output::ColorStream &stream, const VariableDec
 // Expressions
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext, bool omitParentheses)
+inline output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext)
 {
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+	stream << "(";
-		stream << "(";
 
 	for (auto i = and_.arguments.cbegin(); i != and_.arguments.cend(); i++)
 	{
@@ -369,32 +337,27 @@ inline output::ColorStream &print(output::ColorStream &stream, const And &and_,
 		print(stream, *i, printContext);
 	}
 
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+	stream << ")";
-		stream << ")";
 
 	return stream;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext, bool omitParentheses)
+inline output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext)
 {
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+	stream << "(";
-		stream << "(";
-
 	print(stream, biconditional.left, printContext);
 	stream << " <-> ";
 	print(stream, biconditional.right, printContext);
-
+	stream << ")";
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
-		stream << ")";
 
 	return stream;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -420,7 +383,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Exists &exi
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -446,24 +409,20 @@ inline output::ColorStream &print(output::ColorStream &stream, const ForAll &for
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext, bool omitParentheses)
+inline output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext)
 {
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+	stream << "(";
-		stream << "(";
-
 	print(stream, implies.antecedent, printContext);
 	stream << " -> ";
 	print(stream, implies.consequent, printContext);
-
+	stream << ")";
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
-		stream << ")";
 
 	return stream;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -479,10 +438,9 @@ inline output::ColorStream &print(output::ColorStream &stream, const Not &not_,
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext, bool omitParentheses)
+inline output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext)
 {
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+	stream << "(";
-		stream << "(";
 
 	for (auto i = or_.arguments.cbegin(); i != or_.arguments.cend(); i++)
 	{
@@ -492,8 +450,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Or &or_, Pr
 		print(stream, *i, printContext);
 	}
 
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+	stream << ")";
-		stream << ")";
 
 	return stream;
 }
@@ -506,24 +463,24 @@ template<class Variant>
 struct VariantPrintVisitor
 {
 	template<class T>
-	output::ColorStream &visit(const T &x, output::ColorStream &stream, PrintContext &printContext, bool omitParentheses)
+	output::ColorStream &visit(const T &x, output::ColorStream &stream, PrintContext &printContext)
 	{
-		return print(stream, x, printContext, omitParentheses);
+		return print(stream, x, printContext);
 	}
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext, bool omitParentheses)
+inline output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext)
 {
-	return formula.accept(VariantPrintVisitor<Formula>(), stream, printContext, omitParentheses);
+	return formula.accept(VariantPrintVisitor<Formula>(), stream, printContext);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext, bool omitParentheses)
+inline output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext)
 {
-	return term.accept(VariantPrintVisitor<Term>(), stream, printContext, omitParentheses);
+	return term.accept(VariantPrintVisitor<Term>(), stream, printContext);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

src/anthem/ASTCopy.cpp

@@ -159,13 +159,6 @@ String prepareCopy(const String &other)
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-UnaryOperation prepareCopy(const UnaryOperation &other)
-{
-	return UnaryOperation(other.operator_, prepareCopy(other.argument));
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 Variable prepareCopy(const Variable &other)
 {
 	return Variable(other.declaration);
@@ -327,12 +320,6 @@ struct FixDanglingVariablesInTermVisitor
 	{
 	}
 
-	template <class... Arguments>
-	void visit(UnaryOperation &unaryOperation, Arguments &&... arguments)
-	{
-		unaryOperation.argument.accept(*this, std::forward<Arguments>(arguments)...);
-	}
-
 	void visit(Variable &variable, ScopedFormula &scopedFormula, VariableStack &variableStack,
 		std::map<VariableDeclaration *, VariableDeclaration *> &replacements)
 	{

src/anthem/ASTUtils.cpp

@@ -59,7 +59,7 @@ bool VariableStack::contains(const VariableDeclaration &variableDeclaration) con
 		};
 
 	const auto layerContainsVariableDeclaration =
-		[&variableDeclarationMatches](const auto &layer)
+		[&variableDeclaration, &variableDeclarationMatches](const auto &layer)
 		{
 			return (std::find_if(layer->cbegin(), layer->cend(), variableDeclarationMatches) != layer->cend());
 		};
@@ -178,11 +178,6 @@ struct CollectFreeVariablesVisitor
 	{
 	}
 
-	void visit(UnaryOperation &unaryOperation, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
-	{
-		unaryOperation.argument.accept(*this, variableStack, freeVariables);
-	}
-
 	void visit(Variable &variable, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
 	{
 		if (variableStack.contains(*variable.declaration))
@@ -199,7 +194,7 @@ struct CollectFreeVariablesVisitor
 
 struct CollectPredicateSignaturesVisitor : public RecursiveFormulaVisitor<CollectPredicateSignaturesVisitor>
 {
-	static void accept(const Predicate &predicate, const Formula &, std::vector<PredicateSignature> &predicateSignatures, Context &context)
+	static void accept(const Predicate &predicate, const Formula &, std::vector<PredicateSignature> &predicateSignatures)
 	{
 		const auto predicateSignatureMatches =
 			[&predicate](const auto &predicateSignature)
@@ -211,35 +206,12 @@ struct CollectPredicateSignaturesVisitor : public RecursiveFormulaVisitor<Collec
 			return;
 
 		// TODO: avoid copies
-		auto predicateSignature = PredicateSignature(std::string(predicate.name), predicate.arity());
+		predicateSignatures.emplace_back(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 &)
+	static void accept(const T &, const Formula &, std::vector<PredicateSignature> &)
 	{
 	}
 };
@@ -268,10 +240,10 @@ bool matches(const PredicateSignature &lhs, const PredicateSignature &rhs)
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 // TODO: remove const_cast
-void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures, Context &context)
+void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures)
 {
 	auto &formulaMutable = const_cast<Formula &>(formula);
-	formulaMutable.accept(CollectPredicateSignaturesVisitor(), formulaMutable, predicateSignatures, context);
+	formulaMutable.accept(CollectPredicateSignaturesVisitor(), formulaMutable, predicateSignatures);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

src/anthem/Completion.cpp

@@ -165,7 +165,7 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
 
 	// Get a list of all predicates
 	for (const auto &scopedFormula : scopedFormulas)
-		ast::collectPredicateSignatures(scopedFormula.formula, predicateSignatures, context);
+		ast::collectPredicateSignatures(scopedFormula.formula, predicateSignatures);
 
 	std::sort(predicateSignatures.begin(), predicateSignatures.end(),
 		[](const auto &lhs, const auto &rhs)
@@ -180,9 +180,47 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
 
 	std::vector<ast::Formula> completedFormulas;
 
+	// Warn about incorrect #external declarations
+	if (context.externalPredicateSignatures)
+		for (const auto &externalPredicateSignature : *context.externalPredicateSignatures)
+		{
+			// TODO: avoid code duplication
+			const auto matchesPredicateSignature =
+				[&](const auto &otherPredicateSignature)
+				{
+					return ast::matches(externalPredicateSignature, otherPredicateSignature);
+				};
+
+			const auto matchingPredicateSignature =
+				std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), matchesPredicateSignature);
+
+			if (matchingPredicateSignature == predicateSignatures.cend())
+				context.logger.log(output::Priority::Warning) << "#external declaration of “" << externalPredicateSignature.name << "/" << externalPredicateSignature.arity <<"” does not match any known predicate";
+		}
+
 	// Complete predicates
 	for (const auto &predicateSignature : predicateSignatures)
+	{
+		// Don’t complete predicates that are declared #external
+		if (context.externalPredicateSignatures)
+		{
+			const auto matchesPredicateSignature =
+				[&](const auto &otherPredicateSignature)
+				{
+					return ast::matches(predicateSignature, otherPredicateSignature);
+				};
+
+			const auto &externalPredicateSignatures = context.externalPredicateSignatures.value();
+
+			const auto matchingExternalPredicateSignature =
+				std::find_if(externalPredicateSignatures.cbegin(), externalPredicateSignatures.cend(), matchesPredicateSignature);
+
+			if (matchingExternalPredicateSignature != externalPredicateSignatures.cend())
+				continue;
+		}
+
 		completedFormulas.emplace_back(completePredicate(predicateSignature, scopedFormulas));
+	}
 
 	// Complete integrity constraints
 	for (auto &scopedFormula : scopedFormulas)

src/anthem/HiddenPredicateElimination.cpp

@@ -194,7 +194,23 @@ void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predi
 		return;
 	}
 
-	auto &visiblePredicateSignatures = context.visiblePredicateSignatures.value();
+	const auto &visiblePredicateSignatures = context.visiblePredicateSignatures.value();
+
+	// Check for undeclared predicates that are requested to be shown
+	for (const auto &visiblePredicateSignature : visiblePredicateSignatures)
+	{
+		const auto matchesPredicateSignature =
+			[&](const auto &predicateSignature)
+			{
+				return ast::matches(predicateSignature, visiblePredicateSignature);
+			};
+
+		const auto matchingPredicateSignature =
+			std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), matchesPredicateSignature);
+
+		if (matchingPredicateSignature == predicateSignatures.cend())
+			context.logger.log(output::Priority::Warning) << "cannot show undeclared predicate “" << visiblePredicateSignature.name << "/" << visiblePredicateSignature.arity <<"”";
+	}
 
 	// Replace all occurrences of hidden predicates
 	for (size_t i = 0; i < predicateSignatures.size(); i++)
@@ -204,18 +220,15 @@ void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predi
 		const auto matchesPredicateSignature =
 			[&](const auto &otherPredicateSignature)
 			{
-				return ast::matches(predicateSignature, otherPredicateSignature.predicateSignature);
+				return ast::matches(predicateSignature, otherPredicateSignature);
 			};
 
 		const auto matchingVisiblePredicateSignature =
-			std::find_if(visiblePredicateSignatures.begin(), visiblePredicateSignatures.end(), matchesPredicateSignature);
+			std::find_if(visiblePredicateSignatures.cbegin(), visiblePredicateSignatures.cend(), matchesPredicateSignature);
 
 		// If the predicate ought to be visible, don’t eliminate it
-		if (matchingVisiblePredicateSignature != visiblePredicateSignatures.end())
+		if (matchingVisiblePredicateSignature != visiblePredicateSignatures.cend())
-		{
-			matchingVisiblePredicateSignature->used = true;
 			continue;
-		}
 
 		// Check that the predicate is not declared #external
 		if (context.externalPredicateSignatures)

src/anthem/Simplification.cpp

@@ -3,9 +3,7 @@
 #include <optional>
 
 #include <anthem/ASTCopy.h>
-#include <anthem/Equality.h>
+#include <anthem/ASTVisitors.h>
-#include <anthem/output/AST.h>
-#include <anthem/SimplificationVisitors.h>
 
 namespace anthem
 {
@@ -99,65 +97,18 @@ struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<Rep
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-template<class SimplificationRule>
+// Simplifies exists statements by using the equivalence “exists X (X = t and F(X))” == “F(t)”
-SimplificationResult simplify(ast::Formula &formula)
+// The exists statement has to be of the form “exists <variables> <conjunction>”
+void simplify(ast::Exists &exists, ast::Formula &formula)
 {
-	return SimplificationRule::apply(formula);
+	// Simplify formulas like “exists X (X = Y)” to “#true”
-}
+	// TODO: check that this covers all cases
-
+	if (exists.argument.is<ast::Comparison>())
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-template<class FirstSimplificationRule, class SecondSimplificationRule, class... OtherSimplificationRules>
-SimplificationResult simplify(ast::Formula &formula)
-{
-	if (simplify<FirstSimplificationRule>(formula) == SimplificationResult::Simplified)
-		return SimplificationResult::Simplified;
-
-	return simplify<SecondSimplificationRule, OtherSimplificationRules...>(formula);
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct SimplificationRuleExistsWithoutQuantifiedVariables
-{
-	static constexpr const auto Description = "exists () (F) === F";
-
-	static SimplificationResult apply(ast::Formula &formula)
 	{
-		if (!formula.is<ast::Exists>())
-			return SimplificationResult::Unchanged;
-
-		auto &exists = formula.get<ast::Exists>();
-
-		if (!exists.variables.empty())
-			return SimplificationResult::Unchanged;
-
-		formula = std::move(exists.argument);
-
-		return SimplificationResult::Simplified;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct SimplificationRuleTrivialAssignmentInExists
-{
-	static constexpr const auto Description = "exists X (X = Y) === #true";
-
-	static SimplificationResult apply(ast::Formula &formula)
-	{
-		if (!formula.is<ast::Exists>())
-			return SimplificationResult::Unchanged;
-
-		const auto &exists = formula.get<ast::Exists>();
-
-		if (!exists.argument.is<ast::Comparison>())
-			return SimplificationResult::Unchanged;
-
 		const auto &comparison = exists.argument.get<ast::Comparison>();
 
 		if (comparison.operator_ != ast::Comparison::Operator::Equal)
-			return SimplificationResult::Unchanged;
+			return;
 
 		const auto matchingAssignment = std::find_if(exists.variables.cbegin(), exists.variables.cend(),
 			[&](const auto &variableDeclaration)
@@ -166,378 +117,107 @@ struct SimplificationRuleTrivialAssignmentInExists
 					|| matchesVariableDeclaration(comparison.right, *variableDeclaration);
 			});
 
-		if (matchingAssignment == exists.variables.cend())
+		if (matchingAssignment != exists.variables.cend())
-			return SimplificationResult::Unchanged;
+			formula = ast::Formula::make<ast::Boolean>(true);
 
-		formula = ast::Formula::make<ast::Boolean>(true);
+		return;
-
-		return SimplificationResult::Simplified;
 	}
-};
 
-////////////////////////////////////////////////////////////////////////////////////////////////////
+	if (!exists.argument.is<ast::And>())
+		return;
 
-struct SimplificationRuleAssignmentInExists
+	auto &conjunction = exists.argument.get<ast::And>();
-{
+	auto &arguments = conjunction.arguments;
-	static constexpr const auto Description = "exists X (X = t and F(X)) === exists () (F(t))";
 
-	static SimplificationResult apply(ast::Formula &formula)
+	// Simplify formulas of type “exists X (X = t and F(X))” to “F(t)”
+	for (auto i = exists.variables.begin(); i != exists.variables.end();)
 	{
-		if (!formula.is<ast::Exists>())
+		const auto &variableDeclaration = **i;
-			return SimplificationResult::Unchanged;
 
-		auto &exists = formula.get<ast::Exists>();
+		bool wasVariableReplaced = false;
 
-		if (!exists.argument.is<ast::And>())
+		// TODO: refactor
-			return SimplificationResult::Unchanged;
+		for (auto j = arguments.begin(); j != arguments.end(); j++)
-
-		auto &and_ = exists.argument.get<ast::And>();
-		auto &arguments = and_.arguments;
-
-		auto simplificationResult = SimplificationResult::Unchanged;
-
-		for (auto i = exists.variables.begin(); i != exists.variables.end();)
 		{
-			const auto &variableDeclaration = **i;
+			auto &argument = *j;
+			// Find term that is equivalent to the given variable
+			auto assignedTerm = extractAssignedTerm(argument, variableDeclaration);
 
-			bool wasVariableReplaced = false;
+			if (!assignedTerm)
+				continue;
 
-			// TODO: refactor
+			// Replace all occurrences of the variable with the equivalent term
-			for (auto j = arguments.begin(); j != arguments.end(); j++)
+			for (auto k = arguments.begin(); k != arguments.end(); k++)
 			{
-				auto &argument = *j;
+				if (k == j)
-				// Find term that is equivalent to the given variable
-				auto assignedTerm = extractAssignedTerm(argument, variableDeclaration);
-
-				if (!assignedTerm)
 					continue;
 
-				// Replace all occurrences of the variable with the equivalent term
+				auto &otherArgument = *k;
-				for (auto k = arguments.begin(); k != arguments.end(); k++)
+				otherArgument.accept(ReplaceVariableInFormulaVisitor(), otherArgument, variableDeclaration, assignedTerm.value());
-				{
-					if (k == j)
-						continue;
-
-					auto &otherArgument = *k;
-					otherArgument.accept(ReplaceVariableInFormulaVisitor(), otherArgument, variableDeclaration, assignedTerm.value());
-				}
-
-				arguments.erase(j);
-
-				wasVariableReplaced = true;
-				simplificationResult = SimplificationResult::Simplified;
-
-				break;
 			}
 
-			if (wasVariableReplaced)
+			arguments.erase(j);
-			{
+			wasVariableReplaced = true;
-				i = exists.variables.erase(i);
+			break;
-				continue;
-			}
-
-			i++;
 		}
 
-		return simplificationResult;
+		if (wasVariableReplaced)
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct SimplificationRuleEmptyConjunction
-{
-	static constexpr const auto Description = "[empty conjunction] === #true";
-
-	static SimplificationResult apply(ast::Formula &formula)
-	{
-		if (!formula.is<ast::And>())
-			return SimplificationResult::Unchanged;
-
-		auto &and_ = formula.get<ast::And>();
-
-		if (!and_.arguments.empty())
-			return SimplificationResult::Unchanged;
-
-		formula = ast::Formula::make<ast::Boolean>(true);
-
-		return SimplificationResult::Simplified;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct SimplificationRuleOneElementConjunction
-{
-	static constexpr const auto Description = "[conjunction of only F] === F";
-
-	static SimplificationResult apply(ast::Formula &formula)
-	{
-		if (!formula.is<ast::And>())
-			return SimplificationResult::Unchanged;
-
-		auto &and_ = formula.get<ast::And>();
-
-		if (and_.arguments.size() != 1)
-			return SimplificationResult::Unchanged;
-
-		formula = std::move(and_.arguments.front());
-
-		return SimplificationResult::Simplified;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct SimplificationRuleTrivialExists
-{
-	static constexpr const auto Description = "exists ... ([#true/#false]) === [#true/#false]";
-
-	static SimplificationResult apply(ast::Formula &formula)
-	{
-		if (!formula.is<ast::Exists>())
-			return SimplificationResult::Unchanged;
-
-		auto &exists = formula.get<ast::Exists>();
-
-		if (!exists.argument.is<ast::Boolean>())
-			return SimplificationResult::Unchanged;
-
-		formula = std::move(exists.argument);
-
-		return SimplificationResult::Simplified;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct SimplificationRuleInWithPrimitiveArguments
-{
-	static constexpr const auto Description = "[primitive A] in [primitive B] === A = B";
-
-	static SimplificationResult apply(ast::Formula &formula)
-	{
-		if (!formula.is<ast::In>())
-			return SimplificationResult::Unchanged;
-
-		auto &in = formula.get<ast::In>();
-
-		assert(ast::isPrimitive(in.element));
-
-		if (!ast::isPrimitive(in.element) || !ast::isPrimitive(in.set))
-			return SimplificationResult::Unchanged;
-
-		formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
-
-		return SimplificationResult::Simplified;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct SimplificationRuleSubsumptionInBiconditionals
-{
-	static constexpr const auto Description = "(F <-> (F and G)) === (F -> G)";
-
-	static SimplificationResult apply(ast::Formula &formula)
-	{
-		if (!formula.is<ast::Biconditional>())
-			return SimplificationResult::Unchanged;
-
-		auto &biconditional = formula.get<ast::Biconditional>();
-
-		const auto leftIsPredicate = biconditional.left.is<ast::Predicate>();
-		const auto rightIsPredicate = biconditional.right.is<ast::Predicate>();
-
-		const auto leftIsAnd = biconditional.left.is<ast::And>();
-		const auto rightIsAnd = biconditional.right.is<ast::And>();
-
-		if (!(leftIsPredicate && rightIsAnd) && !(rightIsPredicate && leftIsAnd))
-			return SimplificationResult::Unchanged;
-
-		auto &predicateSide = (leftIsPredicate ? biconditional.left : biconditional.right);
-		auto &andSide = (leftIsPredicate ? biconditional.right : biconditional.left);
-		auto &and_ = andSide.get<ast::And>();
-
-		const auto matchingPredicate =
-			std::find_if(and_.arguments.cbegin(), and_.arguments.cend(),
-			[&](const auto &argument)
-			{
-				return (ast::equal(predicateSide, argument) == ast::Tristate::True);
-			});
-
-		if (matchingPredicate == and_.arguments.cend())
-			return SimplificationResult::Unchanged;
-
-		and_.arguments.erase(matchingPredicate);
-
-		formula = ast::Formula::make<ast::Implies>(std::move(predicateSide), std::move(andSide));
-
-		return SimplificationResult::Simplified;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct SimplificationRuleDoubleNegation
-{
-	static constexpr const auto Description = "not not F === F";
-
-	static SimplificationResult apply(ast::Formula &formula)
-	{
-		if (!formula.is<ast::Not>())
-			return SimplificationResult::Unchanged;
-
-		auto &not_ = formula.get<ast::Not>();
-
-		if (!not_.argument.is<ast::Not>())
-			return SimplificationResult::Unchanged;
-
-		auto &notNot = not_.argument.get<ast::Not>();
-
-		formula = std::move(notNot.argument);
-
-		return SimplificationResult::Simplified;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct SimplificationRuleDeMorganForConjunctions
-{
-	static constexpr const auto Description = "(not (F and G)) === (not F or not G)";
-
-	static SimplificationResult apply(ast::Formula &formula)
-	{
-		if (!formula.is<ast::Not>())
-			return SimplificationResult::Unchanged;
-
-		auto &not_ = formula.get<ast::Not>();
-
-		if (!not_.argument.is<ast::And>())
-			return SimplificationResult::Unchanged;
-
-		auto &and_ = not_.argument.get<ast::And>();
-
-		for (auto &argument : and_.arguments)
-			argument = ast::Formula::make<ast::Not>(std::move(argument));
-
-		formula = ast::Formula::make<ast::Or>(std::move(and_.arguments));
-
-		return SimplificationResult::Simplified;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct SimplificationRuleImplicationFromDisjunction
-{
-	static constexpr const auto Description = "(not F or G) === (F -> G)";
-
-	static SimplificationResult apply(ast::Formula &formula)
-	{
-		if (!formula.is<ast::Or>())
-			return SimplificationResult::Unchanged;
-
-		auto &or_ = formula.get<ast::Or>();
-
-		if (or_.arguments.size() != 2)
-			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 SimplificationResult::Unchanged;
-
-		auto &negativeSide = leftIsNot ? or_.arguments[0] : or_.arguments[1];
-		auto &positiveSide = leftIsNot ? or_.arguments[1] : or_.arguments[0];
-
-		assert(negativeSide.is<ast::Not>());
-		assert(!positiveSide.is<ast::Not>());
-
-		auto &negativeSideArgument = negativeSide.get<ast::Not>().argument;
-
-		formula = ast::Formula::make<ast::Implies>(std::move(negativeSideArgument), std::move(positiveSide));
-
-		return SimplificationResult::Simplified;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct SimplificationRuleNegatedComparison
-{
-	static constexpr const auto Description = "(not F [comparison] G) === (F [negated comparison] G)";
-
-	static SimplificationResult apply(ast::Formula &formula)
-	{
-		if (!formula.is<ast::Not>())
-			return SimplificationResult::Unchanged;
-
-		auto &not_ = formula.get<ast::Not>();
-
-		if (!not_.argument.is<ast::Comparison>())
-			return SimplificationResult::Unchanged;
-
-		auto &comparison = not_.argument.get<ast::Comparison>();
-
-		switch (comparison.operator_)
 		{
-			case ast::Comparison::Operator::GreaterThan:
+			i = exists.variables.erase(i);
-				comparison.operator_ = ast::Comparison::Operator::LessEqual;
+			continue;
-				break;
-			case ast::Comparison::Operator::LessThan:
-				comparison.operator_ = ast::Comparison::Operator::GreaterEqual;
-				break;
-			case ast::Comparison::Operator::LessEqual:
-				comparison.operator_ = ast::Comparison::Operator::GreaterThan;
-				break;
-			case ast::Comparison::Operator::GreaterEqual:
-				comparison.operator_ = ast::Comparison::Operator::LessThan;
-				break;
-			case ast::Comparison::Operator::NotEqual:
-				comparison.operator_ = ast::Comparison::Operator::Equal;
-				break;
-			case ast::Comparison::Operator::Equal:
-				comparison.operator_ = ast::Comparison::Operator::NotEqual;
-				break;
 		}
 
-		formula = std::move(comparison);
+		i++;
-
-		return SimplificationResult::Simplified;
 	}
-};
 
-////////////////////////////////////////////////////////////////////////////////////////////////////
+	// If there are no arguments left, we had a formula of the form “exists X1, ..., Xn (X1 = Y1 and ... and Xn = Yn)”
+	// Such exists statements are useless and can be safely replaced with “#true”
+	if (arguments.empty())
+	{
+		formula = ast::Formula::make<ast::Boolean>(true);
+		return;
+	}
 
-const auto simplifyWithDefaultRules =
+	// If the argument now is a conjunction with just one element, directly replace the input formula with the argument
-	simplify
+	if (arguments.size() == 1)
-	<
+		exists.argument = std::move(arguments.front());
-		SimplificationRuleDoubleNegation,
+
-		SimplificationRuleTrivialAssignmentInExists,
+	// If there are still remaining variables, simplification is over
-		SimplificationRuleAssignmentInExists,
+	if (!exists.variables.empty())
-		SimplificationRuleEmptyConjunction,
+		return;
-		SimplificationRuleTrivialExists,
+
-		SimplificationRuleOneElementConjunction,
+	assert(!arguments.empty());
-		SimplificationRuleExistsWithoutQuantifiedVariables,
+
-		SimplificationRuleInWithPrimitiveArguments,
+	// If there is more than one element in the conjunction, replace the input formula with the conjunction
-		SimplificationRuleSubsumptionInBiconditionals,
+	formula = std::move(exists.argument);
-		SimplificationRuleDeMorganForConjunctions,
+}
-		SimplificationRuleImplicationFromDisjunction,
-		SimplificationRuleNegatedComparison
-	>;
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 // Performs the different simplification techniques
-struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<SimplifyFormulaVisitor>
+struct SimplifyFormulaVisitor : public ast::RecursiveFormulaVisitor<SimplifyFormulaVisitor>
 {
-	// Do nothing for all other types of expressions
+	// Forward exists statements to the dedicated simplification function
-	static SimplificationResult accept(ast::Formula &formula)
+	static void accept(ast::Exists &exists, ast::Formula &formula)
+	{
+		simplify(exists, formula);
+	}
+
+	// Simplify formulas of type “A in B” to “A = B” if A and B are primitive
+	static void accept(ast::In &in, ast::Formula &formula)
+	{
+		assert(ast::isPrimitive(in.element));
+
+		if (!ast::isPrimitive(in.element) || !ast::isPrimitive(in.set))
+			return;
+
+		formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
+	}
+
+	// Do nothing for all other types of expressions
+	template<class T>
+	static void accept(T &, ast::Formula &)
 	{
-		return simplifyWithDefaultRules(formula);
 	}
 };
 
@@ -545,7 +225,7 @@ struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<Simplif
 
 void simplify(ast::Formula &formula)
 {
-	while (formula.accept(SimplifyFormulaVisitor(), formula) == SimplificationResult::Simplified);
+	formula.accept(SimplifyFormulaVisitor(), formula);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

src/anthem/Translation.cpp

@@ -85,26 +85,6 @@ void translate(const char *fileName, std::istream &stream, Context &context)
 	// Perform completion
 	auto completedFormulas = complete(std::move(scopedFormulas), context);
 
-	// Check for #show statements with undeclared predicates
-	if (context.visiblePredicateSignatures)
-		for (const auto &predicateSignature : context.visiblePredicateSignatures.value())
-			if (!predicateSignature.used)
-				context.logger.log(output::Priority::Warning)
-					<< "#show declaration of “"
-					<< predicateSignature.predicateSignature.name
-					<< "/" << predicateSignature.predicateSignature.arity
-					<< "” does not match any eligible predicate";
-
-	// Check for #external statements with undeclared predicates
-	if (context.externalPredicateSignatures)
-		for (const auto &predicateSignature : context.externalPredicateSignatures.value())
-			if (!predicateSignature.used)
-				context.logger.log(output::Priority::Warning)
-					<< "#external declaration of “"
-					<< predicateSignature.predicateSignature.name
-					<< "/" << predicateSignature.predicateSignature.arity
-					<< "” does not match any eligible predicate";
-
 	// Simplify output if specified
 	if (context.performSimplification)
 		for (auto &completedFormula : completedFormulas)

tests/TestCompletion.cpp

@@ -152,9 +152,9 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
 
 		CHECK(output.str() ==
 			"forall V1 (covered(V1) <-> exists U1 in(V1, U1))\n"
-			"forall V2, V3 (in(V2, V3) -> (V2 in 1..n and V3 in 1..r))\n"
+			"forall V2, V3 (in(V2, V3) <-> (V2 in 1..n and V3 in 1..r and in(V2, V3)))\n"
-			"forall U2 (U2 in 1..n -> covered(U2))\n"
+			"forall U2 not (U2 in 1..n and not covered(U2))\n"
-			"forall U3, U4, U5 (not in(U3, U4) or not in(U5, U4) or not exists X1 (X1 in (U3 + U5) and in(X1, U4)))\n");
+			"forall U3, U4, U5 not (in(U3, U4) and in(U5, U4) and exists X1 (X1 in (U3 + U5) and in(X1, U4)))\n");
 	}
 
 	SECTION("binary operations with multiple variables")
@@ -176,20 +176,4 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
 		CHECK(output.str() ==
 			"forall V1, V2, V3 (p(V1, V2, V3) <-> #true)\n");
 	}
-
-	SECTION("negated comparisons")
-	{
-		input << ":- color(V, C1), color(V, C2), C1 != C2.";
-		anthem::translate("input", input, context);
-
-		CHECK(output.str() == "forall V1, V2 not color(V1, V2)\nforall U1, U2, U3 (not color(U1, U2) or not color(U1, U3) or U2 = U3)\n");
-	}
-
-	SECTION("absolute value operation")
-	{
-		input << "adj(X, Y) :- X = 1..n, Y = 1..n, |X - Y| = 1.";
-		anthem::translate("input", input, context);
-
-		CHECK(output.str() == "forall V1, V2 (adj(V1, V2) <-> (V1 in 1..n and V2 in 1..n and |V1 - V2| = 1))\n");
-	}
 }

tests/TestHiddenPredicateElimination.cpp

@@ -103,10 +103,9 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
 			"#show a/1.";
 		anthem::translate("input", input, context);
 
-		// TODO: simplify further
 		CHECK(output.str() ==
 			"forall V1 (a(V1) <-> not d(V1))\n"
-			"forall V2 (d(V2) <-> d(V2))\n"
+			"forall V2 (d(V2) <-> not not d(V2))\n"
 			"forall V3 (e(V3) <-> e(V3))\n");
 	}
 
@@ -165,11 +164,12 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
 			"#show t/0.";
 		anthem::translate("input", input, context);
 
+		// TODO: simplify further
 		CHECK(output.str() ==
-			"(s -> not #false)\n"
+			"(s <-> (not #false and s))\n"
-			"(t -> not #false)\n"
+			"(t <-> (not #false and t))\n"
-			"(s -> t)\n"
+			"not (s and not t)\n"
-			"(#false or #false or not #false)\n");
+			"not (not #false and not #false and #false)\n");
 	}
 
 	SECTION("predicate with more than one argument is hidden correctly")

tests/TestPlaceholders.cpp

@@ -1,62 +0,0 @@
-#include <catch.hpp>
-
-#include <sstream>
-
-#include <anthem/AST.h>
-#include <anthem/Context.h>
-#include <anthem/Translation.h>
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-TEST_CASE("[placeholders] Programs with placeholders are correctly completed", "[placeholders]")
-{
-	std::stringstream input;
-	std::stringstream output;
-	std::stringstream errors;
-
-	anthem::output::Logger logger(output, errors);
-	anthem::Context context(std::move(logger));
-	context.performSimplification = true;
-	context.performCompletion = true;
-
-	SECTION("no placeholders")
-	{
-		input <<
-			"colored(V, red) :- vertex(V), not colored(V, green), not colored(V, blue).";
-		anthem::translate("input", input, context);
-
-		CHECK(output.str() ==
-			"forall V1, V2 (colored(V1, V2) <-> (V2 = red and vertex(V1) and not colored(V1, green) and not colored(V1, blue)))\n"
-			"forall V3 not vertex(V3)\n");
-	}
-
-	SECTION("single placeholder")
-	{
-		input <<
-			"#external vertex(1).\n"
-			"colored(V, red) :- vertex(V), not colored(V, green), not colored(V, blue).";
-		anthem::translate("input", input, context);
-
-		CHECK(output.str() ==
-			"forall V1, V2 (colored(V1, V2) <-> (V2 = red and vertex(V1) and not colored(V1, green) and not colored(V1, blue)))\n");
-	}
-
-	SECTION("complex example: graph coloring")
-	{
-		input <<
-			"#external color(1).\n"
-			"#external edge(2).\n"
-			"#external vertex(1).\n"
-			"#show color/2.\n"
-			"{color(V, C)} :- vertex(V), color(C).\n"
-			"covered(V) :- color(V, _).\n"
-			":- vertex(V), not covered(V).\n"
-			":- color(V1, C), color(V2, C), edge(V1, V2).";
-		anthem::translate("input", input, context);
-
-		CHECK(output.str() ==
-			"forall V1, V2 (color(V1, V2) -> (vertex(V1) and color(V2)))\n"
-			"forall U1 (vertex(U1) -> exists U2 color(U1, U2))\n"
-			"forall U3, U4, U5 (not color(U3, U4) or not color(U5, U4) or not edge(U3, U5))\n");
-	}
-}

tests/TestTranslation.cpp

@@ -296,12 +296,4 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 
 		CHECK(output.str() == "((V1 in U1 and V2 in U2 and exists X1, X2 (X1 in U3 and X2 in U4 and q(X1, X2))) -> p(V1, V2))\n");
 	}
-
-	SECTION("exponentiation operator")
-	{
-		input << "p(N, N ** N) :- N = 1..n.";
-		anthem::translate("input", input, context);
-
-		CHECK(output.str() == "((V1 in U1 and V2 in (U1 ** U1) and exists X1, X2 (X1 in U1 and X2 in 1..n and X1 = X2)) -> p(V1, V2))\n");
-	}
 }