Version bump for release 0.1.8 RC 1

This adds the rule “(not F or G) === (F -> G)” to the simplification
rule tableau.

.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,12 +1,10 @@
 # Change Log
 
-## 0.1.8 RC 3 (2018-04-12)
+## 0.1.8 RC 1 (2018-04-10)
 
 ### 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)
+* more, advanced simplification rules
 
 ## 0.1.7 (2018-04-08)
 

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`, the output formulas are simplified by applying several basic transformation rules.
+With the option `--simplify`, 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.8-rc.1" << std::endl;
 		return EXIT_SUCCESS;
 	}
 

examples/graph-coloring.lp

@@ -3,8 +3,7 @@
 #external vertex(1).
 #show color/2.
 
-{color(V, C)} :- vertex(V), color(C).
+{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.
+:- color(V1,C), color(V2,C), edge(V1,V2).

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).

include/anthem/AST.h

@@ -32,8 +32,7 @@ struct BinaryOperation
 		Minus,
 		Multiplication,
 		Division,
-		Modulo,
-		Power
+		Modulo
 	};
 
 	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/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/Equality.h

@@ -382,19 +382,6 @@ struct TermEqualityVisitor
 			: 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>())

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:
-			return ast::BinaryOperation::Operator::Power;
+		default:
+			throw TranslationException(term.location, "“binary operation” terms currently unsupported");
 	}
 
-	throw TranslationException(term.location, "unknown binary operation");
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-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");
+	return ast::BinaryOperation::Operator::Plus;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -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 &binaryOperation, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, Comparison::Operator operator_, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const UnaryOperation &unaryOperation, PrintContext &printContext, bool omitParentheses = false);
-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 BinaryOperation::Operator operator_, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext);
 
-output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Or &or_, 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);
+output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext);
+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 Term &term, 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);
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 // 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);
-
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
-		stream << ")";
+	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)
-{
-	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)
+inline output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext)
 {
 	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);
-
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
-		stream << ")";
+	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);
-
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
-		stream << ")";
+	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

@@ -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))

src/anthem/Simplification.cpp

@@ -466,52 +466,6 @@ struct SimplificationRuleImplicationFromDisjunction
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-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:
-				comparison.operator_ = ast::Comparison::Operator::LessEqual;
-				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);
-
-		return SimplificationResult::Simplified;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 const auto simplifyWithDefaultRules =
 	simplify
 	<
@@ -525,8 +479,7 @@ const auto simplifyWithDefaultRules =
 		SimplificationRuleInWithPrimitiveArguments,
 		SimplificationRuleSubsumptionInBiconditionals,
 		SimplificationRuleDeMorganForConjunctions,
-		SimplificationRuleImplicationFromDisjunction,
-		SimplificationRuleNegatedComparison
+		SimplificationRuleImplicationFromDisjunction
 	>;
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

tests/TestCompletion.cpp

@@ -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/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");
-	}
 }