Version bump for release 0.1.8 RC 3

Remove unnecessary parentheses
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).
2018-04-12 01:06:28 +02:00 · 2018-04-12 00:59:03 +02:00 · 2018-04-12 00:38:48 +02:00 · 2018-04-11 23:21:56 +02:00 · 2018-04-11 21:50:15 +02:00 · 2018-04-11 21:42:08 +02:00
19 changed files with 306 additions and 81 deletions
--- a/.ci/Dockerfile-ubuntu-18.04
+++ b/.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

--- a/CHANGELOG.md
+++ b/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)

--- a/README.md
+++ b/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

--- a/app/main.cpp
+++ b/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;
 	}

--- a/examples/graph-coloring.lp
+++ b/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.
--- a/examples/permutations.lp
+++ b/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.
--- a/examples/prime.lp
+++ b/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).
--- a/include/anthem/AST.h
+++ b/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)
--- a/include/anthem/ASTForward.h
+++ b/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>;

 ////////////////////////////////////////////////////////////////////////////////////////////////////
--- a/include/anthem/ASTVisitors.h
+++ b/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)
 	{
--- a/include/anthem/Equality.h
+++ b/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>())
--- a/include/anthem/Term.h
+++ b/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:
-			throw TranslationException(term.location, "“binary operation” terms currently unsupported");
+		case Clingo::AST::BinaryOperator::Power:
+			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);
--- a/include/anthem/output/AST.h
+++ b/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 &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 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 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 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 Formula &formula, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Term &term, 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);

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

 ////////////////////////////////////////////////////////////////////////////////////////////////////
--- a/lib/clingo
+++ b/lib/clingo
--- a/src/anthem/ASTCopy.cpp
+++ b/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)
 	{
--- a/src/anthem/ASTUtils.cpp
+++ b/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))
--- a/src/anthem/Simplification.cpp
+++ b/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
 	>;

 ////////////////////////////////////////////////////////////////////////////////////////////////////
--- a/tests/TestCompletion.cpp
+++ b/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");
+	}
 }
--- a/tests/TestTranslation.cpp
+++ b/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");
+	}
 }
Author	SHA1	Message	Date
Patrick Lühne	ec88d26922	Version bump for release 0.1.8 RC 3	2018-04-12 01:06:28 +02:00
Patrick Lühne	04094eee23	Remove unnecessary parentheses 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).	2018-04-12 00:59:03 +02:00
Patrick Lühne	8c250f5c59	Support modulus operation (absolute value) This adds support for computing the absolute value of a term along with an according unit test.	2018-04-12 00:38:48 +02:00
Patrick Lühne	0608748349	Describe --complete option in readme The readme was missing information on the --complete option. This adds a brief mention of Clark’s completion to the readme.	2018-04-11 23:21:56 +02:00
Patrick Lühne	31d4a20491	Update change log with recent additions This updates the change log with the advanced simplification rules, support for the exponentation operator, and the newly added examples.	2018-04-11 21:50:15 +02:00
Patrick Lühne	a01e78a467	Add example program for prime number detection	2018-04-11 21:42:08 +02:00
Patrick Lühne	797660d6de	Add new simplification rule This adds the rule “(not F [comparison] G) === (F [negated comparison] G)” to the simplification rule tableau.	2018-04-11 21:39:27 +02:00
Patrick Lühne	b63ef21849	Add example program generating permutations	2018-04-11 21:35:29 +02:00
Patrick Lühne	cc3c9b642c	Minor formatting in graph coloring example	2018-04-11 21:35:04 +02:00
Patrick Lühne	40ddee8444	Add new simplification rule This adds the rule “(not F or G) === (F -> G)” to the simplification rule tableau.	2018-04-10 22:34:47 +02:00
Patrick Lühne	6f7b021712	Add new simplification rule This adds the rule “(not (F and G)) === (not F or not G)” to the simplification rule tableau.	2018-04-10 22:34:47 +02:00
Patrick Lühne	23624007ec	Add new simplification rule This adds the rule “not not F === F” to the simplification rule tableau.	2018-04-10 22:34:47 +02:00
Patrick Lühne	6d7b91c391	Add new simplification rule This adds the rule “(F <-> (F and G)) === (F -> G)” to the simplification rule tableau.	2018-04-10 22:34:47 +02:00
Patrick Lühne	b88393655a	Iteratively apply simplification tableau rules With this change, the tableau rules for simplifying formula are applied iteratively until a fixpoint is reached.	2018-04-10 22:34:47 +02:00
Patrick Lühne	c4c3156e77	Move simplification rule to tableau This moves the rule “[primitive A] in [primitive B] === A = B” to the simplification rule tableau.	2018-04-10 22:34:47 +02:00
Patrick Lühne	107dae7287	Move simplification rule to tableau This moves the rule “exists () (F) === F” to the simplification rule tableau.	2018-04-10 22:34:47 +02:00
Patrick Lühne	827d6e40fe	Move simplification rule to tableau This moves the rule “[conjunction of only F] === F” to the simplification rule tableau.	2018-04-10 22:34:47 +02:00
Patrick Lühne	4a85fc4b23	Move simplification rule to tableau This moves the rule “exists ... ([#true/#false]) === [#true/#false]” to the simplification rule tableau along with “[empty conjunction] ===	2018-04-10 22:34:46 +02:00
Patrick Lühne	7e3fc007c8	Move simplification rule to tableau This moves the rule “exists X (X = t and F(X)) === exists () (F(t))” to the simplification rule tableau.	2018-04-10 22:34:46 +02:00
Patrick Lühne	5c5411c0ff	Implement simplification rule tableau This implements a tableau containing simplification rules that can be iteratively applied to input formulas until they remain unchanged. First, this moves the rule “exists X (X = Y) === #true” to the tableau as a reference implementation.	2018-04-10 22:34:46 +02:00
Patrick Lühne	eaabeb0c55	Support exponentiation operator Because of a bug in the Clingo API, the exponentation operator was not properly exposed to anthem. This updates Clingo to a version with a fixed API and adds proper support for exponentation within anthem along with a matching unit test.	2018-04-10 22:29:55 +02:00
Patrick Lühne	7b6729acaa	Add missing dependency to Ubuntu image For some reason, Bison is not implicitly installed along with the other dependencies in the Ubuntu 18.04 image used for continuous integration. This adds Bison explicitly.	2018-04-10 22:29:55 +02:00