extend PropagateInit to add weight constraints

libclingo/clingo.h

@@ -125,6 +125,12 @@ typedef uint32_t clingo_atom_t;
 typedef uint32_t clingo_id_t;
 //! Signed integer type for weights in sum aggregates and minimize constraints.
 typedef int32_t clingo_weight_t;
+//! A Literal with an associated weight.
+typedef struct clingo_weighted_literal {
+    clingo_literal_t literal;
+    clingo_weight_t weight;
+} clingo_weighted_literal_t;
+
 
 //! Enumeration of error codes.
 //!
@@ -1107,6 +1113,22 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_add_literal(clingo_propagat
 //! @return whether the call was successful; might set one of the following error codes:
 //! - ::clingo_error_bad_alloc
 CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_add_clause(clingo_propagate_init_t *init, clingo_literal_t const *clause, size_t size, bool *result);
+//! Add the given weight constraint to the solver.
+//!
+//! This function add a constraint of form `literal == { lit=weight | (lit, weight) in literals } <= bound` to the solver.
+//!
+//! @attention No further calls on the init object or functions on the assignment should be called when the result of this method is false.
+//!
+//! @param[in] init the target
+//! @param[in] literal the literal of the constraint
+//! @param[in] literals the weighted literals
+//! @param[in] size the number of weighted literals
+//! @param[in] bound the bound of the constraint
+//! @param[in] compare_equal if true compare equal instead of less than equal
+//! @param[out] result result indicating whether whether the problem became unsatisfiable
+//! @return whether the call was successful; might set one of the following error codes:
+//! - ::clingo_error_bad_alloc
+CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_add_weight_constraint(clingo_propagate_init_t *init, clingo_literal_t literal, clingo_weighted_literal_t const *literals, size_t size, clingo_weight_t bound, bool compare_equal, bool *result);
 //! Propagates consequences of the underlying problem excluding registered propagators.
 //!
 //! @note The function has no effect if SAT-preprocessing is enabled.
@@ -1379,13 +1401,6 @@ enum clingo_external_type {
 //! @ingroup ProgramInspection
 typedef int clingo_external_type_t;
 
-//! A Literal with an associated weight.
-//! @ingroup ProgramInspection
-typedef struct clingo_weighted_literal {
-    clingo_literal_t literal;
-    clingo_weight_t weight;
-} clingo_weighted_literal_t;
-
 //! Handle to the backend to add directives in aspif format.
 typedef struct clingo_backend clingo_backend_t;
 

libclingo/clingo.hh

@@ -43,29 +43,6 @@
 
 namespace Clingo {
 
-// {{{1 basic types
-
-// consider using upper case
-using literal_t = clingo_literal_t;
-using id_t = clingo_id_t;
-using weight_t = clingo_weight_t;
-using atom_t = clingo_atom_t;
-
-enum class TruthValue {
-    Free  = clingo_truth_value_free,
-    True  = clingo_truth_value_true,
-    False = clingo_truth_value_false
-};
-
-inline std::ostream &operator<<(std::ostream &out, TruthValue tv) {
-    switch (tv) {
-        case TruthValue::Free:  { out << "Free"; break; }
-        case TruthValue::True:  { out << "True"; break; }
-        case TruthValue::False: { out << "False"; break; }
-    }
-    return out;
-}
-
 // {{{1 variant
 
 namespace Detail {
@@ -435,6 +412,44 @@ std::ostream &operator<<(std::ostream &out, Span<T, I> span) {
     return out;
 }
 
+// {{{1 basic types
+
+// consider using upper case
+using literal_t = clingo_literal_t;
+using id_t = clingo_id_t;
+using weight_t = clingo_weight_t;
+using atom_t = clingo_atom_t;
+
+class WeightedLiteral {
+public:
+    WeightedLiteral(clingo_literal_t lit, clingo_weight_t weight)
+    : wlit_{lit, weight} { }
+    explicit WeightedLiteral(clingo_weighted_literal_t wlit)
+    : wlit_(wlit) { }
+    literal_t literal() const { return wlit_.literal; }
+    weight_t weight() const { return wlit_.weight; }
+    clingo_weighted_literal_t const &to_c() const { return wlit_; }
+    clingo_weighted_literal_t &to_c() { return wlit_; }
+private:
+    clingo_weighted_literal_t wlit_;
+};
+using WeightedLiteralSpan = Span<WeightedLiteral>;
+
+enum class TruthValue {
+    Free  = clingo_truth_value_free,
+    True  = clingo_truth_value_true,
+    False = clingo_truth_value_false
+};
+
+inline std::ostream &operator<<(std::ostream &out, TruthValue tv) {
+    switch (tv) {
+        case TruthValue::Free:  { out << "Free"; break; }
+        case TruthValue::True:  { out << "True"; break; }
+        case TruthValue::False: { out << "False"; break; }
+    }
+    return out;
+}
+
 // {{{1 signature
 
 class Signature {
@@ -836,6 +851,7 @@ public:
     void set_check_mode(PropagatorCheckMode mode);
     literal_t add_literal();
     bool add_clause(LiteralSpan clause);
+    bool add_weight_constraint(literal_t literal, WeightedLiteralSpan literals, weight_t bound, bool compare_equal = false);
     bool propagate();
     clingo_propagate_init_t *to_c() const { return init_; }
 private:
@@ -900,21 +916,6 @@ public:
 using IdSpan = Span<id_t>;
 using AtomSpan = Span<atom_t>;
 
-class WeightedLiteral {
-public:
-    WeightedLiteral(clingo_literal_t lit, clingo_weight_t weight)
-    : wlit_{lit, weight} { }
-    explicit WeightedLiteral(clingo_weighted_literal_t wlit)
-    : wlit_(wlit) { }
-    literal_t literal() const { return wlit_.literal; }
-    weight_t weight() const { return wlit_.weight; }
-    clingo_weighted_literal_t const &to_c() const { return wlit_; }
-    clingo_weighted_literal_t &to_c() { return wlit_; }
-private:
-    clingo_weighted_literal_t wlit_;
-};
-using WeightedLiteralSpan = Span<WeightedLiteral>;
-
 enum class HeuristicType : clingo_heuristic_type_t {
     Level  = clingo_heuristic_type_level,
     Sign   = clingo_heuristic_type_sign,
@@ -2763,6 +2764,12 @@ inline bool PropagateInit::add_clause(LiteralSpan clause) {
     return ret;
 }
 
+inline bool PropagateInit::add_weight_constraint(literal_t literal, WeightedLiteralSpan literals, weight_t bound, bool compare_equal) {
+    bool ret;
+    Detail::handle_error(clingo_propagate_init_add_weight_constraint(init_, literal, reinterpret_cast<clingo_weighted_literal_t const *>(literals.begin()), literals.size(), bound, compare_equal, &ret));
+    return ret;
+}
+
 inline bool PropagateInit::propagate() {
     bool ret;
     Detail::handle_error(clingo_propagate_init_propagate(init_, &ret));

libclingo/clingo/control.hh

@@ -182,6 +182,7 @@ using PropagateInit = clingo_propagate_init;
 struct clingo_propagate_init {
     virtual Potassco::Lit_t addLiteral() = 0;
     virtual bool addClause(Potassco::LitSpan lits) = 0;
+    virtual bool addWeightConstraint(Potassco::Lit_t lit, Potassco::WeightLitSpan lits, Potassco::Weight_t bound, bool eq) = 0;
     virtual bool propagate() = 0;
     virtual Gringo::Output::DomainData const &theory() const = 0;
     virtual Gringo::SymbolicAtoms const &getDomain() const = 0;

libclingo/src/clingocontrol.cc

@@ -28,6 +28,7 @@
 #include <potassco/program_opts/typed_value.h>
 #include <potassco/basic_types.h>
 #include <clasp/clause.h>
+#include <clasp/weight_constraint.h>
 #include "clingo.h"
 #include <signal.h>
 #include <clingo/script.h>
@@ -404,6 +405,23 @@ class ClingoPropagateInit : public PropagateInit {
         }
         return cc.end(Clasp::ClauseCreator::clause_force_simplify).ok();
     }
+    bool addWeightConstraint(Potassco::Lit_t lit, Potassco::WeightLitSpan lits, Potassco::Weight_t bound, bool eq) override {
+        auto &ctx = static_cast<Clasp::ClaspFacade*>(c_.claspFacade())->ctx;
+        auto &master = *ctx.master();
+        if (master.hasConflict()) { return false; }
+        Clasp::WeightLitVec claspLits;
+        claspLits.reserve(lits.size);
+        Clasp::Var m = 0;
+        for (auto &x : lits) {
+            auto y = Clasp::decodeLit(x.lit);
+            m = std::max(m, y.var());
+            claspLits.push_back({y, x.weight});
+        }
+        if (m > 0 && !master.validVar(m)) {
+            master.acquireProblemVars();
+        }
+        return Clasp::WeightConstraint::create(*ctx.master(), Clasp::decodeLit(lit), claspLits, bound, eq ? Clasp::WeightConstraint::create_eq_bound : 0).ok();
+    }
     bool propagate() override {
         auto &ctx = static_cast<Clasp::ClaspFacade*>(c_.claspFacade())->ctx;
         if (ctx.master()->hasConflict()) { return false; }

libclingo/src/control.cc

@@ -672,6 +672,11 @@ extern "C" bool clingo_propagate_init_add_clause(clingo_propagate_init_t *init,
     GRINGO_CLINGO_CATCH;
 }
 
+extern "C" bool clingo_propagate_init_add_weight_constraint(clingo_propagate_init_t *init, clingo_literal_t literal, clingo_weighted_literal_t const *literals, size_t size, clingo_weight_t bound, bool compare_equal, bool *ret) {
+    GRINGO_CLINGO_TRY { *ret = init->addWeightConstraint(literal, Potassco::WeightLitSpan{reinterpret_cast<Potassco::WeightLit_t const *>(literals), size}, bound, compare_equal); }
+    GRINGO_CLINGO_CATCH;
+}
+
 extern "C" bool clingo_propagate_init_propagate(clingo_propagate_init_t *init, bool *ret) {
     GRINGO_CLINGO_TRY { *ret = init->propagate(); }
     GRINGO_CLINGO_CATCH;

libclingo/tests/propagator.cc

@@ -754,6 +754,23 @@ TEST_CASE("propagator", "[clingo][propagator]") {
             REQUIRE(models.size() == 0);
         }
     }
+    SECTION("add_weight_constraint") {
+        ctl.add("base", {}, "{a; b}.");
+        ctl.ground({{"base", {}}}, nullptr);
+        SECTION("wc") {
+            auto p{make_init([](Clingo::PropagateInit &init){
+                auto t = init.add_literal();
+                auto a = get_literal(init, "a");
+                auto b = get_literal(init, "b");
+                REQUIRE(init.add_clause({t}));
+                auto l = init.add_literal();
+                REQUIRE(init.add_weight_constraint(t, {{a,1}, {b,1}, {l,1}}, 2, true));
+            })};
+            ctl.register_propagator(p, false);
+            test_solve(ctl.solve(), models);
+            REQUIRE(models.size() == 3);
+        }
+    }
 }
 
 TEST_CASE("propgator-sequence-mining", "[clingo][propagator]") {