From: Roland Kaminski Date: Wed, 16 Nov 2016 11:12:52 +0000 (+0100) Subject: bugfix: correctly mark body literals as auxiliary in all cases X-Git-Tag: archive/raspbian/5.3.0-13+rpi1~1^2^2~3 X-Git-Url: https://dgit.raspbian.org/?a=commitdiff_plain;h=0ddf1cf6fc240cec55042212698deaa7b4963294;p=gringo.git 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/ Gbp-Pq: Name gringo-fix-body-literals-as-auxiliary.patch --- 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 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 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 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 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 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(completeRef, naf)); } + return CreateBody([&completeRef, this](Ground::ULitVec &lits, bool primary, bool auxiliary) { + if (primary) { lits.emplace_back(gringo_make_unique(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(completeRef)); } + return CreateBody([&completeRef, this](Ground::ULitVec &lits, bool primary, bool auxiliary) { + if (primary) { lits.emplace_back(gringo_make_unique(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(completeRef)); } + return CreateBody([&completeRef](Ground::ULitVec &lits, bool primary, bool auxiliary) { + if (primary) { lits.emplace_back(gringo_make_unique(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(completeRef, naf)); } + return CreateBody([&completeRef, this](Ground::ULitVec &lits, bool primary, bool auxiliary) { + if (primary) { lits.emplace_back(gringo_make_unique(completeRef, naf, auxiliary)); } }, std::move(split)); } diff --git a/libgringo/tests/ground/instantiation.cc b/libgringo/tests/ground/instantiation.cc index aa71c76..0e4bb6a 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"));