Version bump for release 0.1.8 RC 2

The readme was missing information on the --complete option. This adds a
brief mention of Clark’s completion to the readme.

.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 2 (2018-04-11)
 
 ### Features
 
-* more, advanced simplification rules
+* more and advanced simplification rules
+* adds support for exponentiation operator
+* 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.2" << 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)

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

include/anthem/output/AST.h

@@ -85,6 +85,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;

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

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