5 Commits

Author SHA1 Message Date
582b6ade6d Version bump for release 0.1.7 2018-04-08 20:44:43 +02:00
e64b2e70de Remove unused captured lambda reference 2018-04-08 20:44:43 +02:00
d7e4af98d7 Update copyright year in license file 2018-04-08 20:35:03 +02:00
a406cb43bd Update graph coloring example with placeholders
This replaces the former graph coloring example with a new formulation
that makes use of the newly supported placeholders.
2018-04-08 20:28:57 +02:00
c294a29cb2 Support placeholders with #external declarations
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 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 program:

    #external <predicate name>(<arity>).

Multiple unit tests cover cases where placeholders are used or not as
well as a more complex graph coloring example.
2018-04-08 20:28:57 +02:00
6 changed files with 74 additions and 15 deletions

View File

@@ -1,6 +1,6 @@
# Change Log
## 0.1.7 RC 3 (2018-04-07)
## 0.1.7 (2018-04-08)
### Features

View File

@@ -1,6 +1,6 @@
# The MIT License (MIT)
Copyright © 20162017 Patrick Lühne
Copyright © 20162018 Patrick Lühne
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal

View File

@@ -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" << std::endl;
return EXIT_SUCCESS;
}

View File

@@ -1,12 +1,9 @@
colored(V, red) :- vertex(V), not colored(V, green), not colored(V, blue).
colored(V, green) :- vertex(V), not colored(V, red), not colored(V, blue).
colored(V, blue) :- vertex(V), not colored(V, red), not colored(V, green).
#external color(1).
#external edge(2).
#external vertex(1).
#show color/2.
:- edge(V1, V2), colored(V1, C), colored(V2, C).
vertex(a).
vertex(b).
vertex(c).
edge(a, b).
edge(a, 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).

View File

@@ -59,7 +59,7 @@ bool VariableStack::contains(const VariableDeclaration &variableDeclaration) con
};
const auto layerContainsVariableDeclaration =
[&variableDeclaration, &variableDeclarationMatches](const auto &layer)
[&variableDeclarationMatches](const auto &layer)
{
return (std::find_if(layer->cbegin(), layer->cend(), variableDeclarationMatches) != layer->cend());
};

View File

@@ -0,0 +1,62 @@
#include <catch.hpp>
#include <sstream>
#include <anthem/AST.h>
#include <anthem/Context.h>
#include <anthem/Translation.h>
////////////////////////////////////////////////////////////////////////////////////////////////////
TEST_CASE("[placeholders] Programs with placeholders are correctly completed", "[placeholders]")
{
std::stringstream input;
std::stringstream output;
std::stringstream errors;
anthem::output::Logger logger(output, errors);
anthem::Context context(std::move(logger));
context.performSimplification = true;
context.performCompletion = true;
SECTION("no placeholders")
{
input <<
"colored(V, red) :- vertex(V), not colored(V, green), not colored(V, blue).";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall V1, V2 (colored(V1, V2) <-> (V2 = red and vertex(V1) and not colored(V1, green) and not colored(V1, blue)))\n"
"forall V3 not vertex(V3)\n");
}
SECTION("single placeholder")
{
input <<
"#external vertex(1).\n"
"colored(V, red) :- vertex(V), not colored(V, green), not colored(V, blue).";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall V1, V2 (colored(V1, V2) <-> (V2 = red and vertex(V1) and not colored(V1, green) and not colored(V1, blue)))\n");
}
SECTION("complex example: graph coloring")
{
input <<
"#external color(1).\n"
"#external edge(2).\n"
"#external vertex(1).\n"
"#show color/2.\n"
"{color(V, C)} :- vertex(V), color(C).\n"
"covered(V) :- color(V, _).\n"
":- vertex(V), not covered(V).\n"
":- color(V1, C), color(V2, C), edge(V1, V2).";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall V1, V2 (color(V1, V2) <-> (vertex(V1) and color(V2) and color(V1, V2)))\n"
"forall U1 not (vertex(U1) and not exists U2 color(U1, U2))\n"
"forall U3, U4, U5 not (color(U3, U4) and color(U5, U4) and edge(U3, U5))\n");
}
}