Extend PropagateInit interface.

app/clingo/tests/lua/add-clause-lua.lp

@@ -19,24 +19,39 @@ function Propagator:init(init)
     if self.step == 0 then
         l = init:add_literal()
         init:add_clause({-b, l})
+        init:propagate()
         init:add_clause({-l, b})
+        init:propagate()
         init:add_clause({-c, l})
+        init:propagate()
         init:add_clause({-l, c})
+        init:propagate()
         init:add_clause({-a, -b})
+        init:propagate()
         init:add_clause({-a,  b})
+        init:propagate()
         init:add_clause({-a, -a, -b})
+        init:propagate()
         init:add_clause({-a, a})
+        init:propagate()
     end
     if self.step == 1 then
         init:add_clause({b})
+        init:propagate()
         init:add_clause({b})
+        init:propagate()
     end
     if self.step == 2 then
         init:add_clause({})
+        init:propagate()
         init:add_clause({a})
+        init:propagate()
         init:add_clause({b})
+        init:propagate()
         init:add_clause({-a})
+        init:propagate()
         init:add_clause({-b})
+        init:propagate()
     end
     self.step = self.step + 1
 end

app/clingo/tests/lua/add_minimize.cmd

@@ -0,0 +1 @@
+--opt-mode=optN -q1,1

app/clingo/tests/lua/add_minimize.lp

@@ -0,0 +1,34 @@
+#script (lua)
+
+require("clingo")
+
+local Propagator = { }
+Propagator.__index = Propagator
+
+function Propagator.new()
+    local self = setmetatable({ }, Propagator)
+    return self
+end
+
+function Propagator:init(init)
+    a = init:solver_literal(init.symbolic_atoms:lookup(clingo.Function("a")).literal)
+    b = init:solver_literal(init.symbolic_atoms:lookup(clingo.Function("b")).literal)
+    c = init:solver_literal(init.symbolic_atoms:lookup(clingo.Function("c")).literal)
+    d = init:solver_literal(init.symbolic_atoms:lookup(clingo.Function("d")).literal)
+    init:add_minimize(a, 1)
+    init:add_minimize(b, 1)
+    init:add_minimize(c, 1)
+    init:add_minimize(d, 1)
+end
+
+function main(prg)
+    prg:ground({ {"base", {}} })
+    prg:register_propagator(Propagator.new())
+    prg:solve()
+end
+
+#end.
+
+2 { a; b; c }.
+2 { b; c; d }.
+

app/clingo/tests/lua/add_minimize.sol

@@ -0,0 +1,3 @@
+Step: 1
+b c
+OPTIMUM FOUND

app/clingo/tests/lua/add_weight.lp

@@ -0,0 +1,31 @@
+#script (lua)
+
+require("clingo")
+
+local Propagator = { }
+Propagator.__index = Propagator
+
+function Propagator.new()
+    local self = setmetatable({ }, Propagator)
+    return self
+end
+
+function Propagator:init(init)
+    a = init:solver_literal(init.symbolic_atoms:lookup(clingo.Function("a")).literal)
+    b = init:solver_literal(init.symbolic_atoms:lookup(clingo.Function("b")).literal)
+    c = init:solver_literal(init.symbolic_atoms:lookup(clingo.Function("c")).literal)
+    l = init:add_literal()
+    init:add_weight_constraint( l, {{a, 1}, {b, 1}}, 2)
+    init:add_weight_constraint(-l, {{b, 1}, {c, 1}}, 2)
+end
+
+function main(prg)
+    prg:ground({ {"base", {}} })
+    prg:register_propagator(Propagator.new())
+    prg:solve()
+end
+
+#end.
+
+{ a; b; c }.
+

app/clingo/tests/lua/add_weight.sol

@@ -0,0 +1,4 @@
+Step: 1
+a b
+b c
+SAT

app/clingo/tests/python/add-clause-py.lp

@@ -13,22 +13,37 @@ class Propagator:
         if self.step == 0:
             l = init.add_literal()
             init.add_clause([-b, l])
+            init.propagate()
             init.add_clause([-l, b])
+            init.propagate()
             init.add_clause([-c, l])
+            init.propagate()
             init.add_clause([-l, c])
+            init.propagate()
             init.add_clause([-a, -b])
+            init.propagate()
             init.add_clause([-a,  b])
+            init.propagate()
             init.add_clause([-a, -a, -b])
+            init.propagate()
             init.add_clause([-a, a])
+            init.propagate()
         if self.step == 1:
             init.add_clause([b])
+            init.propagate()
             init.add_clause([b])
+            init.propagate()
         if self.step == 2:
             init.add_clause([])
+            init.propagate()
             init.add_clause([a])
+            init.propagate()
             init.add_clause([b])
+            init.propagate()
             init.add_clause([-a])
+            init.propagate()
             init.add_clause([-b])
+            init.propagate()
         self.step += 1
 
 def main(prg):

app/clingo/tests/python/add_minimize.cmd

@@ -0,0 +1 @@
+--opt-mode=optN -q1,1

app/clingo/tests/python/add_minimize.lp

@@ -0,0 +1,25 @@
+#script (python)
+
+import clingo
+
+class Propagator:
+    def init(self, init):
+        a = init.solver_literal(init.symbolic_atoms[clingo.Function("a")].literal)
+        b = init.solver_literal(init.symbolic_atoms[clingo.Function("b")].literal)
+        c = init.solver_literal(init.symbolic_atoms[clingo.Function("c")].literal)
+        d = init.solver_literal(init.symbolic_atoms[clingo.Function("d")].literal)
+        init.add_minimize(a, 1)
+        init.add_minimize(b, 1)
+        init.add_minimize(c, 1)
+        init.add_minimize(d, 1)
+
+def main(prg):
+    prg.register_propagator(Propagator())
+    prg.ground([("base", [])])
+    prg.solve()
+
+#end.
+
+2 { a; b; c }.
+2 { b; c; d }.
+

app/clingo/tests/python/add_minimize.sol

@@ -0,0 +1,3 @@
+Step: 1
+b c
+OPTIMUM FOUND

app/clingo/tests/python/add_weight.lp

@@ -0,0 +1,22 @@
+#script (python)
+
+import clingo
+
+class Propagator:
+    def init(self, init):
+        a = init.solver_literal(init.symbolic_atoms[clingo.Function("a")].literal)
+        b = init.solver_literal(init.symbolic_atoms[clingo.Function("b")].literal)
+        c = init.solver_literal(init.symbolic_atoms[clingo.Function("c")].literal)
+        l = init.add_literal()
+        init.add_weight_constraint( l, ((a, 1), (b, 1)), 2)
+        init.add_weight_constraint(-l, ((b, 1), (c, 1)), 2)
+
+def main(prg):
+    prg.register_propagator(Propagator())
+    prg.ground([("base", [])])
+    prg.solve()
+
+#end.
+
+{ a; b; c }.
+

app/clingo/tests/python/add_weight.sol

@@ -0,0 +1,4 @@
+Step: 1
+a b
+b c
+SAT

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.
 //!
@@ -1088,23 +1094,62 @@ CLINGO_VISIBILITY_DEFAULT clingo_propagator_check_mode_t clingo_propagate_init_g
 CLINGO_VISIBILITY_DEFAULT clingo_assignment_t const *clingo_propagate_init_assignment(clingo_propagate_init_t const *init);
 //! Add a literal to the solver.
 //!
+//! @attention If varibales were added, subsequent calls to functions adding constraints or ::clingo_propagate_init_propagate() are expensive.
+//! It is best to add varables in batches.
+//!
 //! @param[in] init the target
 //! @param[out] result the added literal
 //! @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_literal(clingo_propagate_init_t *init, clingo_literal_t *result);
 //! Add the given clause to the solver.
 //!
-//! @note The result is always set to true and might be removed in a future version of the API.
-//!
+//! @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] clause the clause to add
 //! @param[in] size the size of the clause
-//! @param[out] result always true
+//! @param[out] result result indicating 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_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 adds 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 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);
+//! Add the given literal to minimize to the solver.
+//!
+//! This corresponds to a weak constraint of form `:~ literal. [weight@priority]`.
+//!
+//! @param[in] init the target
+//! @param[in] literal the literal to minimize
+//! @param[in] weight the weight of the literal
+//! @param[in] priority the priority of the literal
+//! @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_minimize(clingo_propagate_init_t *init, clingo_literal_t literal, clingo_weight_t weight, clingo_weight_t priority);
+//! Propagates consequences of the underlying problem excluding registered propagators.
+//!
+//! @note The function has no effect if SAT-preprocessing is enabled.
+//! @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[out] result result indicating 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_propagate(clingo_propagate_init_t *init, bool *result);
 
 //! @}
 
@@ -1367,13 +1412,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;