Merge pull request #527 from potassco/issue-525

Add API for removing minimize constraints and updating projection atoms

libclingo/clingo.h

@@ -1710,7 +1710,7 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_backend_theory_element(clingo_backend_t *b
 //! @param[in] backend the target backend
 //! @param[in] atom an undefined value, program atom, or zero for theory directives
 //! @param[in] term_id the term id of the term associated with the theory atom
-//! @param[in] elements an array of element ids for the theory atoms's elements
+//! @param[in] elements an array of element ids for the theory atom's elements
 //! @param[in] size the number of elements
 //! @param[out] atom_id the final program atom of the theory atom
 //! @return whether the call was successful; might set one of the following error codes:
@@ -1723,7 +1723,7 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_backend_theory_atom(clingo_backend_t *back
 //! @param[in] backend the target backend
 //! @param[in] atom an undefined value, program atom, or zero for theory directives
 //! @param[in] term_id the term id of the term associated with the theory atom
-//! @param[in] elements an array of element ids for the theory atoms's elements
+//! @param[in] elements an array of element ids for the theory atom's elements
 //! @param[in] size the number of elements
 //! @param[in] operator_name the string representation of a theory operator
 //! @param[in] right_hand_side_id the term id of the right hand side term
@@ -2903,14 +2903,35 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_control_assign_external(clingo_control_t *
 //! If a negative literal is passed, the corresponding atom is released.
 //!
 //! After this call, an external atom is no longer external and subject to
-//! program simplifications.  If the atom does not exist or is not external,
+//! program simplifications. If the atom does not exist or is not external,
 //! this is a noop.
 //!
 //! @param[in] control the target
 //! @param[in] literal literal to release
 //! @return whether the call was successful; might set one of the following error codes:
 //! - ::clingo_error_bad_alloc
 CLINGO_VISIBILITY_DEFAULT bool clingo_control_release_external(clingo_control_t *control, clingo_literal_t literal);
+//! Remove minimize constraints from the program.
+//!
+//! After this call, the program no longer contains any minimize constraints.
+//!
+//! @param[in] control the target
+//! @return whether the call was successful; might set one of the following error codes:
+//! - ::clingo_error_bad_alloc
+CLINGO_VISIBILITY_DEFAULT bool clingo_control_remove_minimize(clingo_control_t *control);
+//! Add to or replace the set of projection variables.
+//!
+//! If `append` is true, the function adds the given atoms to the set of projection variables. Otherwise, it discards
+//! any previously added projection variables and sets the given atoms as the new set of projection variables.
+//!
+//! @param[in] control the target
+//! @param[in] atoms the projection atoms to add/set
+//! @param[in] size the number of atoms
+//! @param[in] append whether to append to (true) or replace (false) any previously added projection variables
+//! @return whether the call was successful; might set one of the following error codes:
+//! - ::clingo_error_bad_alloc
+CLINGO_VISIBILITY_DEFAULT bool clingo_control_update_project(clingo_control_t *control, clingo_atom_t const* atoms, size_t size, bool append);
+
 //! Register a custom propagator with the control object.
 //!
 //! If the sequential flag is set to true, the propagator is called
@@ -2967,7 +2988,7 @@ CLINGO_VISIBILITY_DEFAULT void clingo_control_interrupt(clingo_control_t *contro
 //! This function is intended for experimental use only and not part of the stable API.
 //!
 //! This function may return a <code>nullptr</code>.
-//! Otherwise, the returned pointer can be casted to a ClaspFacade pointer.
+//! Otherwise, the returned pointer can be cast to a ClaspFacade pointer.
 //!
 //! @param[in] control the target
 //! @param[out] clasp pointer to the ClaspFacade object (may be <code>nullptr</code>)
@@ -3385,7 +3406,7 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_ast_build(clingo_ast_type_t type, clingo_a
 
 //! @}
 
-//! @name Functions to manage life time of ASTs
+//! @name Functions to manage lifetime of ASTs
 //! @{
 
 //! Increment the reference count of an AST node.

libclingo/clingo/clingocontrol.hh

@@ -206,6 +206,7 @@ public:
     bool onUnsat(Potassco::Span<int64_t> optimization);
     void onFinish(Clasp::ClaspFacade::Result ret);
     bool update();
+    Clasp::Asp::LogicProgram* claspProgram() const;
 
     virtual void postGround(Clasp::ProgramBuilder& prg) {
         if (pgf_ && !pgf_(prg)) {
@@ -261,6 +262,8 @@ public:
             assignExternal(res.first->uid(), val);
         }
     }
+    void updateProject(Potassco::AtomSpan project, bool append) override;
+    void removeMinimize() override;
     Symbol getConst(std::string const &name) const override;
     bool isConflicting() const noexcept override;
     Potassco::AbstractStatistics const *statistics() const override;

libclingo/clingo/control.hh

@@ -250,6 +250,8 @@ struct clingo_control {
     virtual bool blocked() = 0;
     virtual void assignExternal(Potassco::Atom_t ext, Potassco::Value_t val) = 0;
     virtual void assignExternal(Gringo::Symbol ext, Potassco::Value_t val) = 0;
+    virtual void updateProject(Potassco::AtomSpan project, bool append) = 0;
+    virtual void removeMinimize() = 0;
     virtual bool isConflicting() const noexcept = 0;
     virtual Potassco::AbstractStatistics const *statistics() const = 0;
     virtual void useEnumAssumption(bool enable) = 0;

libclingo/src/clingocontrol.cc

@@ -126,7 +126,7 @@ void ClaspAPIBackend::theoryAtom(Potassco::Id_t, Potassco::Id_t, const Potassco:
 void ClaspAPIBackend::theoryAtom(Potassco::Id_t, Potassco::Id_t, const Potassco::IdSpan&, Potassco::Id_t, Potassco::Id_t){ }
 
 Clasp::Asp::LogicProgram *ClaspAPIBackend::prg() {
-    return ctl_.update() ? static_cast<Clasp::Asp::LogicProgram*>(ctl_.clasp_->program()) : nullptr;
+    return ctl_.update() ? ctl_.claspProgram() : nullptr;
 }
 
 ClaspAPIBackend::~ClaspAPIBackend() noexcept = default;
@@ -525,7 +525,7 @@ void ClingoControl::prepare(Assumptions ass) {
             //     For now, we explicitly restore the state here. Alternatively, we could adjust Atomtab::output() so
             //     that it always passes the atom id to the backend, or we could just maintain the set of "shown" atoms
             //     in ClingoControl.
-            auto &prg = static_cast<Clasp::Asp::LogicProgram&>(*clasp_->program());
+            auto &prg = *claspProgram();
             (void) out_->atoms(clingo_show_type_shown, [&](unsigned uid) {
                 if (prg.isFact(uid) && !prg.isShown(uid)) {
                     prg.addOutputState(uid, Clasp::Asp::LogicProgram::OutputState::out_shown);
@@ -542,6 +542,10 @@ void *ClingoControl::claspFacade() {
     return clasp_;
 }
 
+Clasp::Asp::LogicProgram *ClingoControl::claspProgram() const {
+    return static_cast<Clasp::Asp::LogicProgram*>(clasp_->program());
+}
+
 const char* TheoryOutput::first(const Clasp::Model&) {
     index_ = 0;
     return next();
@@ -569,7 +573,7 @@ Potassco::Lit_t ClingoControl::decide(Id_t solverId, Potassco::AbstractAssignmen
 void ClingoControl::registerPropagator(UProp p, bool sequential) {
     propagators_.emplace_back(gringo_make_unique<Clasp::ClingoPropagatorInit>(*p, propLock_.add(sequential)));
     claspConfig_.addConfigurator(propagators_.back().get(), Clasp::Ownership_t::Retain);
-    static_cast<Clasp::Asp::LogicProgram*>(clasp_->program())->enableDistinctTrue();
+    claspProgram()->enableDistinctTrue();
     props_.emplace_back(std::move(p));
     if (props_.back()->hasHeuristic()) {
         if (heus_.empty()) {
@@ -584,7 +588,7 @@ void ClingoControl::cleanup() {
         return;
     }
     canClean_ = false;
-    Clasp::Asp::LogicProgram &prg = static_cast<Clasp::Asp::LogicProgram&>(*clasp_->program());
+    Clasp::Asp::LogicProgram &prg = *claspProgram();
     Clasp::Solver &solver = *clasp_->ctx.master();
     auto assignment = [&prg, &solver](unsigned uid) {
         Potassco::Value_t truth{Potassco::Value_t::Free};
@@ -615,6 +619,26 @@ void ClingoControl::assignExternal(Potassco::Atom_t ext, Potassco::Value_t val)
     }
 }
 
+void ClingoControl::updateProject(Potassco::AtomSpan project, bool append) {
+    auto *backend = update() ? out_->backend() : nullptr;
+    if (backend != nullptr) {
+        if (!append && clingoMode_) {
+            claspProgram()->removeProject();
+        }
+        backend->project(project);
+    }
+}
+
+void ClingoControl::removeMinimize() {
+    if (clingoMode_) {
+        out_->removeMinimize();
+        claspProgram()->removeMinimize();
+    }
+    else {
+        throw std::runtime_error("removing minimize constraints is not supported");
+    }
+}
+
 bool ClingoControl::isConflicting() const noexcept {
     return !clasp_->ok();
 }
@@ -724,7 +748,7 @@ bool ClingoControl::fact(SymbolicAtomIter it) const {
 
 bool ClingoControl::external(SymbolicAtomIter it) const {
     auto &elem = domainElem(out_->predDoms(), it);
-    return elem.hasUid() && elem.isExternal() && (!clingoMode_ || static_cast<Clasp::Asp::LogicProgram*>(clasp_->program())->isExternal(elem.uid()));
+    return elem.hasUid() && elem.isExternal() && (!clingoMode_ || claspProgram()->isExternal(elem.uid()));
 }
 
 SymbolicAtomIter ClingoControl::next(SymbolicAtomIter it) const {

libclingo/src/control.cc

@@ -1971,6 +1971,16 @@ extern "C" bool clingo_control_release_external(clingo_control_t *ctl, clingo_li
     GRINGO_CLINGO_CATCH;
 }
 
+extern "C" bool clingo_control_remove_minimize(clingo_control_t *ctl) {
+    GRINGO_CLINGO_TRY { ctl->removeMinimize(); }
+    GRINGO_CLINGO_CATCH;
+}
+
+extern "C" bool clingo_control_update_project(clingo_control_t *ctl, clingo_atom_t const* atoms, size_t size, bool append) {
+    GRINGO_CLINGO_TRY { ctl->updateProject({atoms, size}, append); }
+    GRINGO_CLINGO_CATCH;
+}
+
 extern "C" bool clingo_program_builder_init(clingo_control_t *ctl, clingo_program_builder_t **ret) {
     GRINGO_CLINGO_TRY { *ret = static_cast<clingo_program_builder_t*>(ctl); }
     GRINGO_CLINGO_CATCH;

libclingo/src/gringo_app.cc

@@ -88,7 +88,7 @@ struct IncrementalControl : Control, private Output::ASPIFOutBackend {
     }
     void update() {
         // This function starts a new step and has to be called at least once
-        // before anything that causes output at the beginning of excecution or
+        // before anything that causes output at the beginning of execution or
         // after a solve step.
         if (!grounded) {
             if (!initialized_) {
@@ -200,6 +200,18 @@ struct IncrementalControl : Control, private Output::ASPIFOutBackend {
             assignExternal(res.first->uid(), val);
         }
     }
+    void updateProject(Potassco::AtomSpan project, bool append) override {
+        if (append) {
+            update();
+            if (auto *b = out.backend()) {
+                b->project(project);
+            }
+        }
+        else {
+            throw std::runtime_error("replacing projection atoms is not supported");
+        }
+    }
+    void removeMinimize() override { throw std::runtime_error("removing minimize constraints is not supported"); }
     SymbolicAtoms const &getDomain() const override { throw std::runtime_error("domain introspection not supported"); }
     ConfigProxy &getConf() override { throw std::runtime_error("configuration not supported"); }
     void registerPropagator(UProp, bool) override { throw std::runtime_error("theory propagators not supported"); }

libgringo/gringo/output/output.hh

@@ -156,6 +156,7 @@ public:
         }
         return atm.uid();
     }
+    void removeMinimize();
 private:
     static UAbstractOutput fromFormat(std::ostream &out, OutputFormat format, OutputOptions opts);
     static UAbstractOutput fromBackend(UBackend out, OutputOptions opts);

libgringo/gringo/output/statements.hh

@@ -231,6 +231,7 @@ public:
     Translator(UAbstractOutput out, bool preserveFacts);
 
     void addMinimize(TupleId tuple, LiteralId cond);
+    void removeMinimize();
     void atoms(DomainData &data, unsigned atomset, IsTrueLookup const &isTrue, SymVec &atoms, OutputPredicates const &outPreds);
     void translate(DomainData &data, OutputPredicates const &outPreds, Logger &log);
     void output(DomainData &data, Statement &x);
@@ -239,7 +240,7 @@ public:
     LiteralId removeNotNot(DomainData &data, LiteralId lit);
     unsigned nodeUid(Symbol v);
     // These are used to cache literals of translated formulas.
-    // The clauses and formuals are tied to clauses and formulas in DomainData.
+    // The clauses and formulas are tied to clauses and formulas in DomainData.
     // Hence, they have to be deleted after each step.
     LiteralId clause(ClauseId id, bool conjunctive, bool equivalence);
     void clause(LiteralId lit, ClauseId id, bool conjunctive, bool equivalence);

libgringo/src/output/output.cc

@@ -618,6 +618,9 @@ Backend *OutputBase::backend() {
     backendLambda(data, *out_, [&backend](DomainData &, UBackend &out) { backend = out.get(); });
     return backend;
 }
+void OutputBase::removeMinimize() {
+    translateLambda(data, *out_, [](DomainData &, Translator &x) { x.removeMinimize(); });
+}
 
 namespace {
 
@@ -736,7 +739,7 @@ void ASPIFOutBackend::theoryAtom(Id_t atomOrZero, Id_t termId, IdSpan const &ele
 }
 
 void ASPIFOutBackend::endStep() {
-    // transfer stored theory atoms to the ouputs theory class
+    // transfer stored theory atoms to the outputs theory class
     theory_.accept(*this);
     for (auto it = sym_tab_.begin(), ie = sym_tab_.end(); it != ie; ++it) {
         auto const &sym = it.key();
@@ -849,7 +852,7 @@ void ASPIFOutBackend::visit(const Potassco::TheoryData &data, Id_t elemId, const
         for (auto const &x : e) {
             tuple.emplace_back(terms_[x]);
         }
-        // one could alse remap to named literals but would have to store the mapping
+        // one could also remap to named literals but would have to store the mapping
         elements_[elemId].first = theory.addElem(make_span(tuple), make_span(elements_[elemId].second));
     }
 }

libgringo/src/output/statements.cc

@@ -437,6 +437,10 @@ Translator::Translator(UAbstractOutput out, bool preserveFacts)
 void Translator::addMinimize(TupleId tuple, LiteralId cond) {
     minimize_.emplace_back(tuple, cond);
 }
+void Translator::removeMinimize() {
+    minimize_.clear();
+    tuples_.clear();
+}
 
 void Translator::translate(DomainData &data, OutputPredicates const &outPreds, Logger &log) {
     translateMinimize(data);