Version bump for release 0.1.8 RC 3

The unary modulus operation does not require extra parentheses to be
printed in cases like “|X + Y|”. This adds a new option to the printing
routine to omit parentheses in cases where the parent expression already
defines a parenthesis-like scope (currently only with unary operations).

.ci/Dockerfile-ubuntu-18.04

@@ -3,7 +3,7 @@ FROM ubuntu:18.04
 ARG toolchain
 
 RUN apt-get update
-RUN apt-get install -y cmake git ninja-build re2c
+RUN apt-get install -y bison 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,10 +1,12 @@
 # Change Log
 
-## 0.1.8 RC 1 (2018-04-10)
+## 0.1.8 RC 3 (2018-04-12)
 
 ### Features
 
-* more, advanced simplification rules
+* 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)
 

README.md

@@ -9,10 +9,11 @@
 ## Usage
 
 ```bash
-$ anthem [--simplify] file...
+$ anthem [--complete] [--simplify] file...
 ```
 
-With the option `--simplify`, output formulas are simplified by applying several basic transformation rules.
+`--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.
 
 ## Building
 

app/main.cpp

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

examples/graph-coloring.lp

@@ -3,7 +3,8 @@
 #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(V1, C), color(V2, C), edge(V1, V2).
+:- color(V, C1), color(V, C2), C1 != C2.

examples/permutations.lp

@@ -0,0 +1,12 @@
+{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

@@ -0,0 +1,4 @@
+#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,7 +32,8 @@ struct BinaryOperation
 		Minus,
 		Multiplication,
 		Division,
-		Modulo
+		Modulo,
+		Power
 	};
 
 	explicit BinaryOperation(Operator operator_, Term &&left, Term &&right)
@@ -292,6 +293,30 @@ 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,6 +37,7 @@ struct Or;
 struct Predicate;
 struct SpecialInteger;
 struct String;
+struct UnaryOperation;
 struct Variable;
 struct VariableDeclaration;
 using VariableDeclarationPointer = std::unique_ptr<VariableDeclaration>;
@@ -68,6 +69,7 @@ using Term = Clingo::Variant<
 	Interval,
 	SpecialInteger,
 	String,
+	UnaryOperation,
 	Variable>;
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

include/anthem/ASTVisitors.h

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

src/anthem/ASTCopy.cpp

@@ -159,6 +159,13 @@ 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);
@@ -320,6 +327,12 @@ 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,6 +178,11 @@ 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,6 +466,52 @@ 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
 	<
@@ -479,7 +525,8 @@ const auto simplifyWithDefaultRules =
 		SimplificationRuleInWithPrimitiveArguments,
 		SimplificationRuleSubsumptionInBiconditionals,
 		SimplificationRuleDeMorganForConjunctions,
-		SimplificationRuleImplicationFromDisjunction
+		SimplificationRuleImplicationFromDisjunction,
+		SimplificationRuleNegatedComparison
 	>;
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

tests/TestCompletion.cpp

@@ -176,4 +176,20 @@ 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,4 +296,12 @@ 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");
+	}
 }