fix #169

This commit makes sure that theory data is passed only once to the
backend(s).

examples/clingo/dl/dl.lp

@@ -10,8 +10,8 @@ import clingo, difference_logic as dl
 
 def print_assignment(p, m):
     a = p.get_assignment(m.thread_id)
-    print "Valid assignment for constraints found:"
-    print " ".join(["{}={}".format(n, v) for n, v in a])
+    print ("Valid assignment for constraints found:")
+    print (" ".join(["{}={}".format(n, v) for n, v in a]))
 
 def main(prg):
     p = dl.Propagator()

examples/clingo/dl/dlO.lp

@@ -25,12 +25,12 @@ def main(prg):
                     if n == "bound":
                         bound = v
                         break
-                print "Valid assignment for constraints found:"
-                print " ".join(["{}={}".format(n, v) for n, v in a])
+                print ("Valid assignment for constraints found:")
+                print (" ".join(["{}={}".format(n, v) for n, v in a]))
                 break
             else:
-                print "Optimum found"
+                print ("Optimum found")
                 break
-        print "Found new bound: {}".format(bound)
+        print ("Found new bound: {}".format(bound))
         prg.ground([("bound", [bound-1])])
 #end.

libclingo/tests/clingo.cc

@@ -603,6 +603,35 @@ TEST_CASE("solving", "[clingo]") {
             REQUIRE(models == ModelVec({}));
             REQUIRE(trail == std::vector<std::string>({"IP: incremental", "BS", "R: 1:-~1", "ES"}));
         }
+        SECTION("theory data bug") {
+            struct Observer : Clingo::GroundProgramObserver {
+                Observer(std::vector<id_t> &atoms) : atoms_{atoms} { }
+                void theory_atom(id_t atom_id_or_zero, id_t , IdSpan ) override {
+                    atoms_.emplace_back(atom_id_or_zero);
+                }
+                std::vector<id_t> &atoms_;
+            };
+
+            std::vector<id_t> atoms;
+            Observer o{atoms};
+            ctl.register_observer(o);
+            ctl.add("base",{}, R"(#theory csp {
+                                   dom_term {};
+                                   &dom/0 : dom_term, any}.)");
+            ctl.add("base",{}, "&dom {0}. &dom {1}.");
+            ctl.add("acid",{}, "&dom {1}. &dom {2}.");
+            REQUIRE(atoms == std::vector<id_t>({}));
+            ctl.ground({{"base", {}}});
+            REQUIRE(atoms == std::vector<id_t>({1, 2}));
+            ctl.ground({{"acid", {}}});
+            REQUIRE(atoms == std::vector<id_t>({1, 2, 3}));
+            ctl.cleanup();
+            REQUIRE(atoms == std::vector<id_t>({1, 2, 3}));
+            { ctl.backend(); }
+            REQUIRE(atoms == std::vector<id_t>({1, 2, 3}));
+            { ctl.backend(); }
+            REQUIRE(atoms == std::vector<id_t>({1, 2, 3}));
+        }
         SECTION("events") {
             ctl.add("base", {}, "{a}.");
             ctl.ground({{"base", {}}});

libgringo/CMakeLists.txt

@@ -73,7 +73,6 @@ bison_target_or_gen("src/input/nongroundgrammar.yy")
 re2c_target_or_gen("/src/input/nongroundlexer.xch")
 set(ide_source_group "Source Files")
 set(source-group
-    "${CMAKE_CURRENT_SOURCE_DIR}/src/backend.cc"
     "${CMAKE_CURRENT_SOURCE_DIR}/src/primes.cc"
     "${CMAKE_CURRENT_SOURCE_DIR}/src/symbol.cc"
     "${CMAKE_CURRENT_SOURCE_DIR}/src/term.cc"

libgringo/gringo/backend.hh

@@ -79,8 +79,6 @@ public:
 };
 using UBackend = std::unique_ptr<Backend>;
 
-void output(Potassco::TheoryData const &data, Backend &out, GetTheoryAtomCondition cond);
-
 inline void outputRule(Backend &out, bool choice, Potassco::AtomSpan head, Potassco::LitSpan body) {
     out.rule(choice ? Potassco::Head_t::Choice : Potassco::Head_t::Disjunctive, head, body);
 }

libgringo/gringo/output/theory.hh

@@ -41,7 +41,22 @@ using Gringo::GetName;
 
 // {{{1 declaration of TheoryData
 
-class TheoryData {
+class TheoryOutput {
+public:
+    using Id_t = Potassco::Id_t;
+    using IdSpan = Potassco::IdSpan;
+
+    virtual void theoryTerm(Id_t termId, int number) = 0;
+    virtual void theoryTerm(Id_t termId, const StringSpan& name) = 0;
+    virtual void theoryTerm(Id_t termId, int cId, const IdSpan& args) = 0;
+    virtual void theoryElement(Id_t elementId, IdSpan const & terms, LitVec const &cond) = 0;
+    virtual void theoryAtom(Id_t atomOrZero, Id_t termId, const IdSpan& elements) = 0;
+    virtual void theoryAtom(Id_t atomOrZero, Id_t termId, const IdSpan& elements, Id_t op, Id_t rhs) = 0;
+
+    virtual ~TheoryOutput() = default;
+};
+
+class TheoryData : private Potassco::TheoryData::Visitor {
     using TIdSet = HashSet<Potassco::Id_t>;
     using AtomSet = HashSet<uintptr_t>;
     using ConditionVec = std::vector<LitVec>;
@@ -66,7 +81,15 @@ public:
     void setCondition(Potassco::Id_t elementId, Potassco::Id_t newCond);
     bool hasConditions() const;
     void reset(bool resetData);
+    void output(TheoryOutput &tout);
     Potassco::TheoryAtom const &getAtom(Id_t offset) const { return **(data_.begin() + offset); }
+private:
+    void print(Potassco::Id_t termId, const Potassco::TheoryTerm& term);
+    void print(const Potassco::TheoryAtom& a);
+    void visit(Potassco::TheoryData const &data, Potassco::Id_t termId, Potassco::TheoryTerm const &t) override;
+    void visit(Potassco::TheoryData const &data, Potassco::Id_t elemId, Potassco::TheoryElement const &e) override;
+    void visit(Potassco::TheoryData const &data, Potassco::TheoryAtom const &a) override;
+    bool addSeen(std::vector<bool>& vec, Potassco::Id_t id) const;
 
 private:
     template <typename ...Args>
@@ -79,6 +102,10 @@ private:
     AtomSet atoms_;
     Potassco::TheoryData &data_;
     ConditionVec conditions_;
+    std::vector<bool> tSeen_;
+    std::vector<bool> eSeen_;
+    TheoryOutput *out_;
+    uint32_t aSeen_;
 };
 
 // {{{1 declaration of TheoryTerm

libgringo/src/output/output.cc

@@ -278,20 +278,54 @@ void OutputBase::beginStep() {
     backendLambda(data, *out_, [](DomainData &, UBackend &out) { out->beginStep(); });
 }
 
+namespace {
+
+class BackendTheoryOutput : public TheoryOutput {
+public:
+    BackendTheoryOutput(DomainData &data, AbstractOutput &out)
+    : data_{data}
+    , out_{out} {
+    }
+private:
+    void theoryTerm(Id_t termId, int number) override {
+        backendLambda(data_, out_, [&](DomainData &, UBackend &out) { out->theoryTerm(termId, number); });
+    }
+    void theoryTerm(Id_t termId, const StringSpan& name) override {
+        backendLambda(data_, out_, [&](DomainData &, UBackend &out) { out->theoryTerm(termId, name); });
+    }
+    void theoryTerm(Id_t termId, int cId, const IdSpan& args) override {
+        backendLambda(data_, out_, [&](DomainData &, UBackend &out) { out->theoryTerm(termId, cId, args); });
+    }
+    void theoryElement(Id_t elementId, IdSpan const & terms, LitVec const &cond) override {
+        backendLambda(data_, out_, [&](DomainData &, UBackend &out) {
+            BackendLitVec bc;
+            bc.reserve(cond.size());
+            for (auto &lit : cond) {
+                bc.emplace_back(call(data_, lit, &Literal::uid));
+            }
+            out->theoryElement(elementId, terms, Potassco::toSpan(bc));
+        });
+    }
+    void theoryAtom(Id_t atomOrZero, Id_t termId, const IdSpan& elements) override {
+        backendLambda(data_, out_, [&](DomainData &, UBackend &out) { out->theoryAtom(atomOrZero, termId, elements); });
+    }
+    void theoryAtom(Id_t atomOrZero, Id_t termId, const IdSpan& elements, Id_t op, Id_t rhs) override {
+        backendLambda(data_, out_, [&](DomainData &, UBackend &out) { out->theoryAtom(atomOrZero, termId, elements, op, rhs); });
+    }
+private:
+    DomainData &data_;
+    AbstractOutput &out_;
+};
+
+} // namespace
+
 void OutputBase::endGround(Logger &log) {
     for (auto &lit : delayed_) { DelayedStatement(lit).passTo(data, *out_); }
     delayed_.clear();
-    backendLambda(data, *out_, [](DomainData &data, UBackend &out) {
-        auto getCond = [&data](Id_t elem) {
-            TheoryData &td = data.theory();
-            BackendLitVec bc;
-            for (auto &lit : td.getCondition(elem)) {
-                bc.emplace_back(call(data, lit, &Literal::uid));
-            }
-            return bc;
-        };
-        Gringo::output(data.theory().data(), *out, getCond);
-    });
+
+    BackendTheoryOutput bto{data, *out_};
+    data.theory().output(bto);
+
     if (!outPreds.empty()) {
         std::move(outPredsForce.begin(), outPredsForce.end(), std::back_inserter(outPreds));
         outPredsForce.clear();

libgringo/src/output/theory.cc

@@ -24,6 +24,7 @@
 
 #include "gringo/output/theory.hh"
 #include "gringo/output/literal.hh"
+#include "gringo/backend.hh"
 #include "gringo/logger.hh"
 #include <cstring>
 
@@ -543,10 +544,56 @@ UTheoryTerm TermTheoryTerm::initTheory(TheoryParser &, Logger &) {
 
 TheoryData::TheoryData(Potassco::TheoryData &data)
 : data_(data)
+, aSeen_{0}
 { }
 
 TheoryData::~TheoryData() noexcept = default;
 
+void TheoryData::print(Potassco::Id_t termId, const Potassco::TheoryTerm& term) {
+    switch (term.type()) {
+        case Potassco::Theory_t::Number  : out_->theoryTerm(termId, term.number()); break;
+        case Potassco::Theory_t::Symbol  : out_->theoryTerm(termId, Potassco::toSpan(term.symbol())); break;
+        case Potassco::Theory_t::Compound: out_->theoryTerm(termId, term.compound(), term.terms()); break;
+    }
+}
+void TheoryData::print(const Potassco::TheoryAtom& a) {
+    if (a.guard()) { out_->theoryAtom(a.atom(), a.term(), a.elements(), *a.guard(), *a.rhs()); }
+    else           { out_->theoryAtom(a.atom(), a.term(), a.elements()); }
+}
+void TheoryData::visit(Potassco::TheoryData const &data, Potassco::Id_t termId, Potassco::TheoryTerm const &t) {
+    if (addSeen(tSeen_, termId)) { // only visit once
+        // visit any subterms then print
+        data.accept(t, *this);
+        print(termId, t);
+    }
+}
+void TheoryData::visit(Potassco::TheoryData const &data, Potassco::Id_t elemId, Potassco::TheoryElement const &e) {
+    if (addSeen(eSeen_, elemId)) { // only visit once
+        // visit terms then print element
+        data.accept(e, *this);
+        out_->theoryElement(elemId, e.terms(), getCondition(elemId));
+    }
+}
+void TheoryData::visit(Potassco::TheoryData const &data, Potassco::TheoryAtom const &a) {
+    // visit elements then print atom
+    data.accept(a, *this);
+    print(a);
+}
+
+bool TheoryData::addSeen(std::vector<bool>& vec, Potassco::Id_t id) const {
+    if (vec.size() <= id) { vec.resize(id + 1, false); }
+    bool seen = vec[id];
+    if (!seen) { vec[id] = true; }
+    return !seen;
+}
+
+void TheoryData::output(TheoryOutput &out) {
+    // NOTE: a friend class would probably have been nicer
+    out_ = &out;
+    for (auto it = data_.begin() + aSeen_; it != data_.end(); ++it) { visit(data_, **it); }
+    aSeen_ = data_.numAtoms();
+}
+
 template <typename ...Args>
 Potassco::Id_t TheoryData::addTerm_(Args ...args) {
     auto size = terms_.size();
@@ -744,6 +791,9 @@ void TheoryData::setCondition(Potassco::Id_t elementId, Potassco::Id_t newCond)
 }
 
 void TheoryData::reset(bool resetData) {
+    aSeen_ = 0;
+    tSeen_.clear();
+    eSeen_.clear();
     TIdSet().swap(terms_);
     TIdSet().swap(elems_);
     AtomSet().swap(atoms_);