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 (file)
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 (file)
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 5b26c650e79bcd6314ce08ac0d0a495507b1e4af..f1804e7c7d9f6b2c089668db03d599f3683e363f 100644 (file)
--- 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 17bbf6e5ec67a35f7e8f10e9b4dc790332fbca31..38a45627915616e44b88cd4aa16154b96859c572 100644 (file)
--- 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 a77d5d938e7a0d5fb2a7a0beeef7073fb3e01e05..98469a89eacda1f6aa98eafba2acb5b0e97f23a5 100644 (file)
--- 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 aa71c760e87c5fc76a13b96d6658a74524f13111..0e4bb6a1a3db95d3cba71dc8bd15a9f40597a16a 100644 (file)
--- 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"));