[gringo] 13/20: gringo-fix-body-literals-as-auxiliary.patch: add upstream patch
Thomas Krennwallner
tkren-guest at moszumanska.debian.org
Sun Dec 11 21:06:58 UTC 2016
This is an automated email from the git hooks/post-receive script.
tkren-guest pushed a commit to branch devel
in repository gringo.
commit 60190a8eaad338f1eff11609e04db81473d31923
Author: Thomas Krennwallner <tkren at kr.tuwien.ac.at>
Date: Sat Dec 10 10:01:25 2016 +0100
gringo-fix-body-literals-as-auxiliary.patch: add upstream patch
cherry-picked from d6cfb89df6bbf138ca3e259d71ca7050b322b5d5
---
.../gringo-fix-body-literals-as-auxiliary.patch | 302 +++++++++++++++++++++
debian/patches/series | 1 +
2 files changed, 303 insertions(+)
diff --git a/debian/patches/gringo-fix-body-literals-as-auxiliary.patch b/debian/patches/gringo-fix-body-literals-as-auxiliary.patch
new file mode 100644
index 0000000..a3ce644
--- /dev/null
+++ b/debian/patches/gringo-fix-body-literals-as-auxiliary.patch
@@ -0,0 +1,302 @@
+From: Roland Kaminski <kaminski at cs.uni-potsdam.de>
+Date: Wed, 16 Nov 2016 12:12:52 +0100
+Subject: bugfix: correctly mark body literals as auxiliary in all cases
+Origin: upstream, https://github.com/potassco/clingo/commit/d6cfb89df6bbf138ca3e259d71ca7050b322b5d5
+Bug: https://sourceforge.net/p/potassco/mailman/message/35493632/
+
+---
+ app/clingo/tests/lp/aggregates.lp | 38 +++++++++++++++++++++++++++++++++
+ app/clingo/tests/lp/aggregates.sol | 2 ++
+ libgringo/gringo/ground/statements.hh | 20 ++++++++++-------
+ libgringo/src/ground/statements.cc | 20 ++++++++++-------
+ libgringo/src/input/aggregates.cc | 16 +++++++-------
+ libgringo/tests/ground/instantiation.cc | 8 +++++++
+ 6 files changed, 80 insertions(+), 24 deletions(-)
+ create mode 100644 app/clingo/tests/lp/aggregates.lp
+ create mode 100644 app/clingo/tests/lp/aggregates.sol
+
+diff --git a/app/clingo/tests/lp/aggregates.lp b/app/clingo/tests/lp/aggregates.lp
+new file mode 100644
+index 0000000..40d6748
+--- /dev/null
++++ b/app/clingo/tests/lp/aggregates.lp
+@@ -0,0 +1,38 @@
++arg(s3). sat(s3):-ass(s3,Y_s3),lt(Y_s3,Z_s3),V_t_0=0, V_3_1=-V_t_0, V_t_2=0, V_2_1=-2*V_t_2+V_3_1, dom(V_t_3), V_t_3 #sum{Z_s3,s3}V_t_3, V_1_1=1*V_t_3+V_2_1, V_t_4=0, V_0_1=2*V_t_4+V_1_1, dom(V_1), V_1 #sum{1:V_0_1>0} V_1, V_1=1.
++inv(s3):-ass(s3,Y_s3),lt(Y_s3,Z_s3),V_t_0=0, V_3_1=-V_t_0, V_t_2=0, V_2_1=-2*V_t_2+V_3_1, dom(V_t_3), V_t_3 #sum{Z_s3,s3} V_t_3, V_1_1=1*V_t_3+V_2_1, V_t_4=0, V_0_1=2*V_t_4+V_1_1, dom(V_1), V_1 #sum{1:V_0_1>0}V_1, V_1=0.
++sattwo(s3):-asstwo(s3,Y_s3),lt(Y_s3,Z_s3),V_t_0=0, V_3_1=-V_t_0, V_t_2=0, V_2_1=-2*V_t_2+V_3_1, dom(V_t_3), V_t_3#sum{Z_s3,s3}V_t_3, V_1_1=1*V_t_3+V_2_1, V_t_4=0, V_0_1=2*V_t_4+V_1_1, dom(V_1), V_1 #sum{1:V_0_1>0}V_1, V_1=1.
++invtwo(s3):-asstwo(s3,Y_s3),lt(Y_s3,Z_s3),V_t_0=0, V_3_1=-V_t_0, V_t_2=0, V_2_1=-2*V_t_2+V_3_1, dom(V_t_3), V_t_3#sum{Z_s3,s3}V_t_3, V_1_1=1*V_t_3+V_2_1, V_t_4=0, V_0_1=2*V_t_4+V_1_1, dom(V_1), V_1 #sum{1:V_0_1>0}V_1, V_1=0.
++arg(s2).
++sat(s2):-V_t_5=0, V_3_6=-V_t_5, V_t_7=0, V_2_6=-2*V_t_7+V_3_6, V_t_8=0, V_1_6=1*V_t_8+V_2_6, V_t_9=0, V_0_6=2*V_t_9+V_1_6, dom(V_6), V_6#sum{1:V_0_6>0}V_6, V_6=1.
++inv(s2):-V_t_5=0, V_3_6=-V_t_5, V_t_7=0, V_2_6=-2*V_t_7+V_3_6, V_t_8=0, V_1_6=1*V_t_8+V_2_6, V_t_9=0, V_0_6=2*V_t_9+V_1_6, dom(V_6), V_6#sum{1:V_0_6>0}V_6, V_6=0.
++sattwo(s2):-V_t_5=0, V_3_6=-V_t_5, V_t_7=0, V_2_6=-2*V_t_7+V_3_6, V_t_8=0, V_1_6=1*V_t_8+V_2_6, V_t_9=0, V_0_6=2*V_t_9+V_1_6, dom(V_6), V_6#sum{1:V_0_6>0}V_6, V_6=1.
++invtwo(s2):-V_t_5=0, V_3_6=-V_t_5, V_t_7=0, V_2_6=-2*V_t_7+V_3_6, V_t_8=0, V_1_6=1*V_t_8+V_2_6, V_t_9=0, V_0_6=2*V_t_9+V_1_6, dom(V_6), V_6#sum{1:V_0_6>0}V_6, V_6=0.
++arg(s1).
++sat(s1):-ass(s2,Y_s2),lt(Y_s2,Z_s2),ass(s3,Y_s3),lt(Y_s3,Z_s3),dom(V_t_10), V_t_10#sum{Z_s2,s2}V_t_10, V_3_11=-V_t_10, V_t_12=0, V_2_11=-2*V_t_12+V_3_11, dom(V_t_13), V_t_13 #sum{Z_s3,s3}V_t_13, V_1_11=1*V_t_13+V_2_11, V_t_14=0, V_0_11=2*V_t_14+V_1_11, dom(V_11), V_11#sum{1:V_0_11>0}V_11, V_11=1.
++inv(s1):-ass(s2,Y_s2),lt(Y_s2,Z_s2),ass(s3,Y_s3),lt(Y_s3,Z_s3),dom(V_t_10), V_t_10#sum{Z_s2,s2}V_t_10, V_3_11=-V_t_10, V_t_12=0, V_2_11=-2*V_t_12+V_3_11, dom(V_t_13), V_t_13 #sum{Z_s3,s3}V_t_13, V_1_11=1*V_t_13+V_2_11, V_t_14=0, V_0_11=2*V_t_14+V_1_11, dom(V_11), V_11#sum{1:V_0_11>0}V_11, V_11=0.
++sattwo(s1):-asstwo(s2,Y_s2),lt(Y_s2,Z_s2),asstwo(s3,Y_s3),lt(Y_s3,Z_s3),dom(V_t_10), V_t_10#sum{Z_s2,s2}V_t_10, V_3_11=-V_t_10, V_t_12=0, V_2_11=-2*V_t_12+V_3_11, dom(V_t_13), V_t_13#sum{Z_s3,s3}V_t_13, V_1_11=1*V_t_13+V_2_11, V_t_14=0, V_0_11=2*V_t_14+V_1_11, dom(V_11), V_11#sum{1:V_0_11>0}V_11, V_11=1.
++invtwo(s1):-asstwo(s2,Y_s2),lt(Y_s2,Z_s2),asstwo(s3,Y_s3),lt(Y_s3,Z_s3),dom(V_t_10), V_t_10#sum{Z_s2,s2}V_t_10, V_3_11=-V_t_10, V_t_12=0, V_2_11=-2*V_t_12+V_3_11, dom(V_t_13), V_t_13#sum{Z_s3,s3}V_t_13, V_1_11=1*V_t_13+V_2_11, V_t_14=0, V_0_11=2*V_t_14+V_1_11, dom(V_11), V_11#sum{1:V_0_11>0}V_11, V_11=0.
++saturate:-ass(s3,X_1),asstwo(s3,X_1),ass(s2,X_2),asstwo(s2,X_2),ass(s1,X_3),asstwo(s1,X_3).
++dom(0..1).
++lt(u,0).lt(u,1).lt(1,1).lt(0,0).
++ass(S,0):-not ass(S,1),not ass(S,u),arg(S).
++ass(S,1):-not ass(S,u),not ass(S,0),arg(S).
++ass(S,u):-not ass(S,0),not ass(S,1),arg(S).
++:-arg(S),ass(S,1),inv(S).
++:-arg(S),ass(S,0),sat(S).
++asstwo(S,0):-ass(S,0).
++asstwo(S,1):-ass(S,1).
++asstwo(S,0)|asstwo(S,1)|asstwo(S,u):-ass(S,u).
++saturate:-arg(S),asstwo(S,1),invtwo(S).
++saturate:-arg(S),asstwo(S,0),sattwo(S).
++asstwo(S,0):-arg(S),ass(S,u),saturate.
++asstwo(S,1):-arg(S),ass(S,u),saturate.
++asstwo(S,u):-arg(S),ass(S,u),saturate.
++sattwo(S):-arg(S),ass(S,u),saturate.
++:-not saturate.
++#show ass/2.
++
++:-ass(s1, 0),ass(s2, 0),ass(s3, 0).
++:-ass(s1, 1),ass(s2, 0),ass(s3, 1).
++
++%unfounded: saturate, asstwo(s1,0), asstwo(s1,0)
+\ No newline at end of file
+diff --git a/app/clingo/tests/lp/aggregates.sol b/app/clingo/tests/lp/aggregates.sol
+new file mode 100644
+index 0000000..94dc765
+--- /dev/null
++++ b/app/clingo/tests/lp/aggregates.sol
+@@ -0,0 +1,2 @@
++Step: 1
++UNSAT
+diff --git a/libgringo/gringo/ground/statements.hh b/libgringo/gringo/ground/statements.hh
+index 5b26c65..f1804e7 100644
+--- a/libgringo/gringo/ground/statements.hh
++++ b/libgringo/gringo/ground/statements.hh
+@@ -376,7 +376,7 @@ private:
+
+ class BodyAggregateLiteral : public Literal, private BodyOcc {
+ public:
+- BodyAggregateLiteral(BodyAggregateComplete &complete, NAF naf);
++ BodyAggregateLiteral(BodyAggregateComplete &complete, NAF naf, bool auxiliary);
+ virtual ~BodyAggregateLiteral() noexcept;
+
+ // {{{2 Printable interface
+@@ -388,7 +388,7 @@ public:
+ void collect(VarTermBoundVec &vars) const override;
+ Score score(Term::VarSet const &bound, Logger &log) override;
+ std::pair<Output::LiteralId, bool> toOutput(Logger &log) override;
+- bool auxiliary() const override { return false; } // by construction
++ bool auxiliary() const override { return auxiliary_; }
+ // }}}2
+
+ private:
+@@ -407,6 +407,7 @@ private:
+ DefinedBy defs_;
+ Potassco::Id_t offset_ = 0;
+ NAF naf_;
++ bool auxiliary_;
+ OccurrenceType type_ = OccurrenceType::POSITIVELY_STRATIFIED;
+ };
+
+@@ -499,7 +500,7 @@ private:
+
+ class AssignmentAggregateLiteral : public Literal, private BodyOcc {
+ public:
+- AssignmentAggregateLiteral(AssignmentAggregateComplete &complete);
++ AssignmentAggregateLiteral(AssignmentAggregateComplete &complete, bool auxiliary);
+ virtual ~AssignmentAggregateLiteral() noexcept;
+ // {{{2 Printable interface
+ void print(std::ostream &out) const override;
+@@ -510,7 +511,7 @@ public:
+ void collect(VarTermBoundVec &vars) const override;
+ Score score(Term::VarSet const &bound, Logger &log) override;
+ std::pair<Output::LiteralId,bool> toOutput(Logger &log) override;
+- bool auxiliary() const override { return false; } // by construction
++ bool auxiliary() const override { return auxiliary_; }
+ // }}}2
+
+ private:
+@@ -529,6 +530,7 @@ private:
+ DefinedBy defs_;
+ Id_t offset_ = InvalidId;
+ OccurrenceType type_ = OccurrenceType::POSITIVELY_STRATIFIED;
++ bool auxiliary_;
+ };
+
+ // }}}1
+@@ -667,7 +669,7 @@ private:
+
+ class ConjunctionLiteral : public Literal, private BodyOcc {
+ public:
+- ConjunctionLiteral(ConjunctionComplete &complete);
++ ConjunctionLiteral(ConjunctionComplete &complete, bool auxiliary);
+ virtual ~ConjunctionLiteral() noexcept;
+ // {{{2 Printable interface
+ void print(std::ostream &out) const override;
+@@ -678,7 +680,7 @@ public:
+ void collect(VarTermBoundVec &vars) const override;
+ Score score(Term::VarSet const &bound, Logger &log) override;
+ std::pair<Output::LiteralId,bool> toOutput(Logger &log) override;
+- bool auxiliary() const override { return false; } // by construction
++ bool auxiliary() const override { return auxiliary_; }
+ // }}}2
+
+ private:
+@@ -697,6 +699,7 @@ private:
+ DefinedBy defs_;
+ Id_t offset_;
+ OccurrenceType type_ = OccurrenceType::POSITIVELY_STRATIFIED;
++ bool auxiliary_;
+ };
+
+ // }}}1
+@@ -786,7 +789,7 @@ private:
+
+ class DisjointLiteral : public Literal, private BodyOcc {
+ public:
+- DisjointLiteral(DisjointComplete &complete, NAF naf);
++ DisjointLiteral(DisjointComplete &complete, NAF naf, bool auxiliary);
+ virtual ~DisjointLiteral() noexcept;
+ // {{{2 Printable interface
+ void print(std::ostream &out) const override;
+@@ -797,7 +800,7 @@ public:
+ void collect(VarTermBoundVec &vars) const override;
+ Score score(Term::VarSet const &bound, Logger &log) override;
+ std::pair<Output::LiteralId,bool> toOutput(Logger &log) override;
+- bool auxiliary() const override { return false; } // by construction
++ bool auxiliary() const override { return auxiliary_; }
+ // }}}2
+ private:
+ // {{{2 BodyOcc interface
+@@ -816,6 +819,7 @@ private:
+ Id_t offset_ = InvalidId;
+ OccurrenceType type_ = OccurrenceType::POSITIVELY_STRATIFIED;
+ NAF naf_;
++ bool auxiliary_;
+ };
+
+ // }}}1
+diff --git a/libgringo/src/ground/statements.cc b/libgringo/src/ground/statements.cc
+index 17bbf6e..38a4562 100644
+--- a/libgringo/src/ground/statements.cc
++++ b/libgringo/src/ground/statements.cc
+@@ -888,9 +888,10 @@ void BodyAggregateAccumulate::printHead(std::ostream &out) const {
+
+ // {{{1 definition of BodyAggregateLiteral
+
+-BodyAggregateLiteral::BodyAggregateLiteral(BodyAggregateComplete &complete, NAF naf)
++BodyAggregateLiteral::BodyAggregateLiteral(BodyAggregateComplete &complete, NAF naf, bool auxiliary)
+ : complete_(complete)
+-, naf_(naf) { }
++, naf_(naf)
++, auxiliary_(auxiliary) { }
+
+ BodyAggregateLiteral::~BodyAggregateLiteral() noexcept = default;
+
+@@ -1138,8 +1139,9 @@ void AssignmentAggregateAccumulate::printHead(std::ostream &out) const {
+
+ // {{{1 Definition of AssignmentAggregateLiteral
+
+-AssignmentAggregateLiteral::AssignmentAggregateLiteral(AssignmentAggregateComplete &complete)
+-: complete_(complete) { }
++AssignmentAggregateLiteral::AssignmentAggregateLiteral(AssignmentAggregateComplete &complete, bool auxiliary)
++: complete_(complete)
++, auxiliary_(auxiliary) { }
+
+ AssignmentAggregateLiteral::~AssignmentAggregateLiteral() noexcept = default;
+
+@@ -1206,8 +1208,9 @@ std::pair<Output::LiteralId,bool> AssignmentAggregateLiteral::toOutput(Logger &)
+
+ // {{{1 definition of ConjunctionLiteral
+
+-ConjunctionLiteral::ConjunctionLiteral(ConjunctionComplete &complete)
+-: complete_(complete) { }
++ConjunctionLiteral::ConjunctionLiteral(ConjunctionComplete &complete, bool auxiliary)
++: complete_(complete)
++, auxiliary_(auxiliary) { }
+
+ ConjunctionLiteral::~ConjunctionLiteral() noexcept = default;
+
+@@ -1663,9 +1666,10 @@ void DisjointAccumulate::printHead(std::ostream &out) const {
+
+ // {{{1 definition of DisjointLiteral
+
+-DisjointLiteral::DisjointLiteral(DisjointComplete &complete, NAF naf)
++DisjointLiteral::DisjointLiteral(DisjointComplete &complete, NAF naf, bool auxiliary)
+ : complete_(complete)
+-, naf_(naf) {
++, naf_(naf)
++, auxiliary_(auxiliary) {
+ }
+
+ DisjointLiteral::~DisjointLiteral() noexcept = default;
+diff --git a/libgringo/src/input/aggregates.cc b/libgringo/src/input/aggregates.cc
+index a77d5d9..98469a8 100644
+--- a/libgringo/src/input/aggregates.cc
++++ b/libgringo/src/input/aggregates.cc
+@@ -324,8 +324,8 @@ CreateBody TupleBodyAggregate::toGround(ToGroundArg &x, Ground::UStmVec &stms) c
+ return std::move(ret);
+ });
+ }
+- return CreateBody([&completeRef, this](Ground::ULitVec &lits, bool primary, bool) {
+- if (primary) { lits.emplace_back(gringo_make_unique<Ground::BodyAggregateLiteral>(completeRef, naf)); }
++ return CreateBody([&completeRef, this](Ground::ULitVec &lits, bool primary, bool auxiliary) {
++ if (primary) { lits.emplace_back(gringo_make_unique<Ground::BodyAggregateLiteral>(completeRef, naf, auxiliary)); }
+ }, std::move(split));
+ }
+ else {
+@@ -362,8 +362,8 @@ CreateBody TupleBodyAggregate::toGround(ToGroundArg &x, Ground::UStmVec &stms) c
+ return std::move(ret);
+ });
+ }
+- return CreateBody([&completeRef, this](Ground::ULitVec &lits, bool primary, bool) {
+- if (primary) { lits.emplace_back(gringo_make_unique<Ground::AssignmentAggregateLiteral>(completeRef)); }
++ return CreateBody([&completeRef, this](Ground::ULitVec &lits, bool primary, bool auxiliary) {
++ if (primary) { lits.emplace_back(gringo_make_unique<Ground::AssignmentAggregateLiteral>(completeRef, auxiliary)); }
+ }, std::move(split));
+ }
+ }
+@@ -752,8 +752,8 @@ CreateBody Conjunction::toGround(ToGroundArg &x, Ground::UStmVec &stms) const {
+ return std::move(ret);
+ });
+
+- return CreateBody([&completeRef](Ground::ULitVec &lits, bool primary, bool) {
+- if (primary) { lits.emplace_back(gringo_make_unique<Ground::ConjunctionLiteral>(completeRef)); }
++ return CreateBody([&completeRef](Ground::ULitVec &lits, bool primary, bool auxiliary) {
++ if (primary) { lits.emplace_back(gringo_make_unique<Ground::ConjunctionLiteral>(completeRef, auxiliary)); }
+ }, std::move(split));
+ }
+
+@@ -1751,8 +1751,8 @@ CreateBody DisjointAggregate::toGround(ToGroundArg &x, Ground::UStmVec &stms) co
+ return std::move(ret);
+ });
+ }
+- return CreateBody([&completeRef, this](Ground::ULitVec &lits, bool primary, bool) {
+- if (primary) { lits.emplace_back(gringo_make_unique<Ground::DisjointLiteral>(completeRef, naf)); }
++ return CreateBody([&completeRef, this](Ground::ULitVec &lits, bool primary, bool auxiliary) {
++ if (primary) { lits.emplace_back(gringo_make_unique<Ground::DisjointLiteral>(completeRef, naf, auxiliary)); }
+ }, std::move(split));
+ }
+
+diff --git a/libgringo/tests/ground/instantiation.cc b/libgringo/tests/ground/instantiation.cc
+index 22817af..7bc9d87 100644
+--- a/libgringo/tests/ground/instantiation.cc
++++ b/libgringo/tests/ground/instantiation.cc
+@@ -1108,6 +1108,14 @@ TEST_CASE("ground-instantiation", "[ground]") {
+ "-q(X):-not not -q(X), p(X).\n"
+ " q(X):-not not q(X), p(X).\n"));
+ }
++ SECTION("two aggregates") {
++ REQUIRE(
++ "p:-#count{0,a:a}=0.\n"
++ "p:-#count{0,a:a}=1,1<=#count{0,b:b}.\n"
++ "{a;b}.\n" == ground(
++ "{a;b}.\n"
++ "p :- X = { a }, X { b }.\n"));
++ }
+
+ SECTION("tuple") {
+ REQUIRE("p(((),())).\n" == ground("p(((),())).\n"));
+--
+2.11.0
+
diff --git a/debian/patches/series b/debian/patches/series
index 8b5f395..0f28dd1 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,2 +1,3 @@
gringo-manpages.patch
reproducible-build.patch
+gringo-fix-body-literals-as-auxiliary.patch
--
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/debian-science/packages/gringo.git
More information about the debian-science-commits
mailing list