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 2 (2018-04-11)
+## 0.1.8 RC 1 (2018-04-10)
 
 ### Features
 
-* more and advanced simplification rules
+* more, 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,11 +9,10 @@
 ## Usage
 
 ```bash
-$ anthem [--complete] [--simplify] file...
+$ anthem [--simplify] file...
 ```
 
-`--complete` instructs `anthem` to perform Clark’s completion on the translated formulas.
+With the option `--simplify`, output formulas are simplified by applying several basic transformation rules.
-With the option `--simplify`, the output formulas are simplified by applying several basic transformation rules.
 
 ## Building
 

app/main.cpp

@@ -70,7 +70,7 @@ int main(int argc, char **argv)
 
 	if (version)
 	{
-		std::cout << "anthem version 0.1.8-rc.2" << 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(V1,C), color(V2,C), edge(V1,V2).
-:- color(V, C1), color(V, C2), C1 != C2.

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,
+		Modulo
-		Power
 	};
 
 	explicit BinaryOperation(Operator operator_, Term &&left, Term &&right)

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,11 +33,11 @@ ast::BinaryOperation::Operator translate(Clingo::AST::BinaryOperator binaryOpera
 			return ast::BinaryOperation::Operator::Division;
 		case Clingo::AST::BinaryOperator::Modulo:
 			return ast::BinaryOperation::Operator::Modulo;
-		case Clingo::AST::BinaryOperator::Power:
+		default:
-			return ast::BinaryOperation::Operator::Power;
+			throw TranslationException(term.location, "“binary operation” terms currently unsupported");
 	}
 
-	throw TranslationException(term.location, "unknown binary operation");
+	return ast::BinaryOperation::Operator::Plus;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

include/anthem/output/AST.h

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

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,
+		SimplificationRuleImplicationFromDisjunction
-		SimplificationRuleNegatedComparison
 	>;
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

tests/TestCompletion.cpp

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

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