Version bump for release 0.1.7 RC 1

This adds support for declaring predicates as placeholders through the
“#external” directive in the input language of clingo.

Placeholders are not subject to completion. This prevents predicates
that represent instance-specific facts from being assumed as universally
false by default negation when translating an encoding.

This stretches clingo’s usual syntax a bit in order to make the
implementation lightweight. In order to declare a predicate with a
specific arity as a placeholder, the following statement needs to be
added to the input program:

CHANGELOG.md

@@ -1,18 +1,14 @@
 # Change Log
 
-## 0.1.7 RC 3 (2018-04-07)
+## 0.1.7 (2018-04-05)
 
-### Features
+Features:
 
 * support for declaring placeholders with the `#external` directive
 
-### Internal
-
-* drops Boost dependency in favor of the header-only command-line option library [cxxopts](https://github.com/jarro2783/cxxopts)
-
 ## 0.1.6 (2017-06-12)
 
-### Features
+Features:
 
 * unique IDs for all variables (user-defined variables are renamed)
 * support for hiding predicates from completed output by using `#show` statements
@@ -20,7 +16,7 @@
 * command-line option `--parentheses` to fully parenthesize the output
 * adds multiple example instances for experimenting
 
-### Bug Fixes
+Bug Fixes:
 
 * adds missing error message when attempting to read inaccessible file
 * removes unnecessary parentheses after simplification
@@ -28,52 +24,52 @@
 
 ## 0.1.5 (2017-05-04)
 
-### Bug Fixes
+Bug Fixes:
 
 * fixes lost signs with negated 0-ary predicates
 
 ## 0.1.4 (2017-04-12)
 
-### Features
+Features:
 
 * completion of input programs (optional)
 * command-line option `--complete` to turn on completion
 
 ## 0.1.3 (2017-03-30)
 
-### Features
+Features:
 
 * support for anonymous variables
 
-### Bug Fixes
+Bug Fixes:
 
 * fixes incorrectly simplified rules with comparisons
 * fixes misleading error message concerning negated, unsupported body literals
 
 ## 0.1.2 (2017-03-23)
 
-### Features
+Features:
 
 * simplification of output formulas (optional)
 * command-line option `--simplify` to turn on simplification
 
-### Bug Fixes
+Bug Fixes:
 
 * fixes incorrectly translated choice rules with multiple elements in the head aggregate
 
-### Internal
+Internal:
 
 * explicit syntax tree representation for first-order formulas
 
 ## 0.1.1 (2017-03-06)
 
-### Features
+Features:
 
 * support for choice rules (without guards)
 
 ## 0.1.0 (2016-11-24)
 
-### Features
+Features:
 
 * initial support for translating rules in *Essential Gringo* (excluding aggregates) to first-order logic formulas
 * command-line option `--color` to autodetect, enable, or disable color output

app/main.cpp

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

include/anthem/ASTUtils.h

@@ -5,7 +5,6 @@
 
 #include <anthem/AST.h>
 #include <anthem/ASTVisitors.h>
-#include <anthem/Context.h>
 
 namespace anthem
 {
@@ -41,7 +40,7 @@ class VariableStack
 bool matches(const Predicate &lhs, const Predicate &rhs);
 bool matches(const Predicate &predicate, const PredicateSignature &signature);
 bool matches(const PredicateSignature &lhs, const PredicateSignature &rhs);
-void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures, Context &context);
+void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures);
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 // Replacing Variables

include/anthem/Context.h

@@ -16,14 +16,6 @@ namespace anthem
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct PredicateSignatureMeta
-{
-	ast::PredicateSignature predicateSignature;
-	bool used{false};
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 struct Context
 {
 	Context() = default;
@@ -38,8 +30,8 @@ struct Context
 	bool performSimplification = false;
 	bool performCompletion = false;
 
-	std::optional<std::vector<PredicateSignatureMeta>> visiblePredicateSignatures;
-	std::optional<std::vector<PredicateSignatureMeta>> externalPredicateSignatures;
+	std::optional<std::vector<ast::PredicateSignature>> visiblePredicateSignatures;
+	std::optional<std::vector<ast::PredicateSignature>> externalPredicateSignatures;
 
 	ast::ParenthesisStyle parenthesisStyle = ast::ParenthesisStyle::Normal;
 };

include/anthem/StatementVisitor.h

@@ -176,8 +176,7 @@ struct StatementVisitor
 
 		context.logger.log(output::Priority::Debug, statement.location) << "showing “" << signature.name() << "/" << signature.arity() << "”";
 
-		auto predicateSignature = ast::PredicateSignature{std::string(signature.name()), signature.arity()};
-		context.visiblePredicateSignatures.value().emplace_back(PredicateSignatureMeta{std::move(predicateSignature)});
+		context.visiblePredicateSignatures.value().emplace_back(std::string(signature.name()), signature.arity());
 	}
 
 	void visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &)
@@ -214,13 +213,12 @@ struct StatementVisitor
 		if (aritySymbol.type() != Clingo::SymbolType::Number)
 			fail();
 
-		const size_t arity = arityArgument.data.get<Clingo::Symbol>().number();
+		const auto &arity = arityArgument.data.get<Clingo::Symbol>().number();
 
 		if (!context.externalPredicateSignatures)
 			context.externalPredicateSignatures.emplace();
 
-		auto predicateSignature = ast::PredicateSignature{std::string(predicate.name), arity};
-		context.externalPredicateSignatures->emplace_back(PredicateSignatureMeta{std::move(predicateSignature)});
+		context.externalPredicateSignatures->emplace_back(std::string(predicate.name), arity);
 	}
 
 	template<class T>

src/anthem/ASTUtils.cpp

@@ -194,7 +194,7 @@ struct CollectFreeVariablesVisitor
 
 struct CollectPredicateSignaturesVisitor : public RecursiveFormulaVisitor<CollectPredicateSignaturesVisitor>
 {
-	static void accept(const Predicate &predicate, const Formula &, std::vector<PredicateSignature> &predicateSignatures, Context &context)
+	static void accept(const Predicate &predicate, const Formula &, std::vector<PredicateSignature> &predicateSignatures)
 	{
 		const auto predicateSignatureMatches =
 			[&predicate](const auto &predicateSignature)
@@ -206,35 +206,12 @@ struct CollectPredicateSignaturesVisitor : public RecursiveFormulaVisitor<Collec
 			return;
 
 		// TODO: avoid copies
-		auto predicateSignature = PredicateSignature(std::string(predicate.name), predicate.arity());
-
-		// Ignore predicates that are declared #external
-		if (context.externalPredicateSignatures)
-		{
-			const auto matchesPredicateSignature =
-				[&](const auto &otherPredicateSignature)
-				{
-					return ast::matches(predicateSignature, otherPredicateSignature.predicateSignature);
-				};
-
-			auto &externalPredicateSignatures = context.externalPredicateSignatures.value();
-
-			const auto matchingExternalPredicateSignature =
-				std::find_if(externalPredicateSignatures.begin(), externalPredicateSignatures.end(), matchesPredicateSignature);
-
-			if (matchingExternalPredicateSignature != externalPredicateSignatures.end())
-			{
-				matchingExternalPredicateSignature->used = true;
-				return;
-			}
-		}
-
-		predicateSignatures.emplace_back(std::move(predicateSignature));
+		predicateSignatures.emplace_back(std::string(predicate.name), predicate.arity());
 	}
 
 	// Ignore all other types of expressions
 	template<class T>
-	static void accept(const T &, const Formula &, std::vector<PredicateSignature> &, const Context &)
+	static void accept(const T &, const Formula &, std::vector<PredicateSignature> &)
 	{
 	}
 };
@@ -263,10 +240,10 @@ bool matches(const PredicateSignature &lhs, const PredicateSignature &rhs)
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 // TODO: remove const_cast
-void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures, Context &context)
+void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures)
 {
 	auto &formulaMutable = const_cast<Formula &>(formula);
-	formulaMutable.accept(CollectPredicateSignaturesVisitor(), formulaMutable, predicateSignatures, context);
+	formulaMutable.accept(CollectPredicateSignaturesVisitor(), formulaMutable, predicateSignatures);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

src/anthem/Completion.cpp

@@ -165,7 +165,7 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
 
 	// Get a list of all predicates
 	for (const auto &scopedFormula : scopedFormulas)
-		ast::collectPredicateSignatures(scopedFormula.formula, predicateSignatures, context);
+		ast::collectPredicateSignatures(scopedFormula.formula, predicateSignatures);
 
 	std::sort(predicateSignatures.begin(), predicateSignatures.end(),
 		[](const auto &lhs, const auto &rhs)
@@ -180,9 +180,47 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
 
 	std::vector<ast::Formula> completedFormulas;
 
+	// Warn about incorrect #external declarations
+	if (context.externalPredicateSignatures)
+		for (const auto &externalPredicateSignature : *context.externalPredicateSignatures)
+		{
+			// TODO: avoid code duplication
+			const auto matchesPredicateSignature =
+				[&](const auto &otherPredicateSignature)
+				{
+					return ast::matches(externalPredicateSignature, otherPredicateSignature);
+				};
+
+			const auto matchingPredicateSignature =
+				std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), matchesPredicateSignature);
+
+			if (matchingPredicateSignature == predicateSignatures.cend())
+				context.logger.log(output::Priority::Warning) << "#external declaration of “" << externalPredicateSignature.name << "/" << externalPredicateSignature.arity <<"” does not match any known predicate";
+		}
+
 	// Complete predicates
 	for (const auto &predicateSignature : predicateSignatures)
+	{
+		// Don’t complete predicates that are declared #external
+		if (context.externalPredicateSignatures)
+		{
+			const auto matchesPredicateSignature =
+				[&](const auto &otherPredicateSignature)
+				{
+					return ast::matches(predicateSignature, otherPredicateSignature);
+				};
+
+			const auto &externalPredicateSignatures = context.externalPredicateSignatures.value();
+
+			const auto matchingExternalPredicateSignature =
+				std::find_if(externalPredicateSignatures.cbegin(), externalPredicateSignatures.cend(), matchesPredicateSignature);
+
+			if (matchingExternalPredicateSignature != externalPredicateSignatures.cend())
+				continue;
+		}
+
 		completedFormulas.emplace_back(completePredicate(predicateSignature, scopedFormulas));
+	}
 
 	// Complete integrity constraints
 	for (auto &scopedFormula : scopedFormulas)

src/anthem/HiddenPredicateElimination.cpp

@@ -194,7 +194,23 @@ void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predi
 		return;
 	}
 
-	auto &visiblePredicateSignatures = context.visiblePredicateSignatures.value();
+	const auto &visiblePredicateSignatures = context.visiblePredicateSignatures.value();
+
+	// Check for undeclared predicates that are requested to be shown
+	for (const auto &visiblePredicateSignature : visiblePredicateSignatures)
+	{
+		const auto matchesPredicateSignature =
+			[&](const auto &predicateSignature)
+			{
+				return ast::matches(predicateSignature, visiblePredicateSignature);
+			};
+
+		const auto matchingPredicateSignature =
+			std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), matchesPredicateSignature);
+
+		if (matchingPredicateSignature == predicateSignatures.cend())
+			context.logger.log(output::Priority::Warning) << "cannot show undeclared predicate “" << visiblePredicateSignature.name << "/" << visiblePredicateSignature.arity <<"”";
+	}
 
 	// Replace all occurrences of hidden predicates
 	for (size_t i = 0; i < predicateSignatures.size(); i++)
@@ -204,18 +220,15 @@ void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predi
 		const auto matchesPredicateSignature =
 			[&](const auto &otherPredicateSignature)
 			{
-				return ast::matches(predicateSignature, otherPredicateSignature.predicateSignature);
+				return ast::matches(predicateSignature, otherPredicateSignature);
 			};
 
 		const auto matchingVisiblePredicateSignature =
-			std::find_if(visiblePredicateSignatures.begin(), visiblePredicateSignatures.end(), matchesPredicateSignature);
+			std::find_if(visiblePredicateSignatures.cbegin(), visiblePredicateSignatures.cend(), matchesPredicateSignature);
 
 		// If the predicate ought to be visible, don’t eliminate it
-		if (matchingVisiblePredicateSignature != visiblePredicateSignatures.end())
-		{
-			matchingVisiblePredicateSignature->used = true;
+		if (matchingVisiblePredicateSignature != visiblePredicateSignatures.cend())
 			continue;
-		}
 
 		// Check that the predicate is not declared #external
 		if (context.externalPredicateSignatures)

src/anthem/Translation.cpp

@@ -85,26 +85,6 @@ void translate(const char *fileName, std::istream &stream, Context &context)
 	// Perform completion
 	auto completedFormulas = complete(std::move(scopedFormulas), context);
 
-	// Check for #show statements with undeclared predicates
-	if (context.visiblePredicateSignatures)
-		for (const auto &predicateSignature : context.visiblePredicateSignatures.value())
-			if (!predicateSignature.used)
-				context.logger.log(output::Priority::Warning)
-					<< "#show declaration of “"
-					<< predicateSignature.predicateSignature.name
-					<< "/" << predicateSignature.predicateSignature.arity
-					<< "” does not match any eligible predicate";
-
-	// Check for #external statements with undeclared predicates
-	if (context.externalPredicateSignatures)
-		for (const auto &predicateSignature : context.externalPredicateSignatures.value())
-			if (!predicateSignature.used)
-				context.logger.log(output::Priority::Warning)
-					<< "#external declaration of “"
-					<< predicateSignature.predicateSignature.name
-					<< "/" << predicateSignature.predicateSignature.arity
-					<< "” does not match any eligible predicate";
-
 	// Simplify output if specified
 	if (context.performSimplification)
 		for (auto &completedFormula : completedFormulas)