add an option to freeze literals

libclingo/clingo.h

@@ -1160,14 +1160,18 @@ 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.
 //!
+//! To be able to use the variable in clauses during propagation or add watches to it, it has to be frozen.
+//! Otherwise, it might be removed during preprocessing.
+//!
 //! @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[in] freeze whether to freeze the literal
 //! @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);
+CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_add_literal(clingo_propagate_init_t *init, bool freeze, clingo_literal_t *result);
 //! Add the given clause 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.

libclingo/clingo.hh

@@ -928,7 +928,7 @@ public:
     TheoryAtoms theory_atoms() const;
     PropagatorCheckMode get_check_mode() const;
     void set_check_mode(PropagatorCheckMode mode);
-    literal_t add_literal();
+    literal_t add_literal(bool freeze = true);
     bool add_clause(LiteralSpan clause);
     bool add_weight_constraint(literal_t literal, WeightedLiteralSpan literals, weight_t bound, WeightConstraintType type, bool compare_equal = false);
     void add_minimize(literal_t literal, weight_t weight, weight_t priority = 0);
@@ -2900,9 +2900,9 @@ inline void PropagateInit::set_check_mode(PropagatorCheckMode mode) {
     clingo_propagate_init_set_check_mode(init_, mode);
 }
 
-inline literal_t PropagateInit::add_literal() {
+inline literal_t PropagateInit::add_literal(bool freeze) {
     literal_t ret;
-    Detail::handle_error(clingo_propagate_init_add_literal(init_, &ret));
+    Detail::handle_error(clingo_propagate_init_add_literal(init_, freeze, &ret));
     return ret;
 }
 

libclingo/clingo/control.hh

@@ -184,7 +184,7 @@ using PropagateInit = clingo_propagate_init;
 } // namespace Gringo
 
 struct clingo_propagate_init {
-    virtual Potassco::Lit_t addLiteral() = 0;
+    virtual Potassco::Lit_t addLiteral(bool freeze) = 0;
     virtual bool addClause(Potassco::LitSpan lits) = 0;
     virtual bool addWeightConstraint(Potassco::Lit_t lit, Potassco::WeightLitSpan lits, Potassco::Weight_t bound, int type, bool eq) = 0;
     virtual void addMinimize(Potassco::Lit_t literal, Potassco::Weight_t weight, Potassco::Weight_t priority) = 0;

libclingo/src/clingocontrol.cc

@@ -396,8 +396,13 @@ class ClingoPropagateInit : public PropagateInit {
     void addWatch(Lit_t lit) override { p_.addWatch(Clasp::decodeLit(lit)); }
     void addWatch(uint32_t solverId, Lit_t lit) override { p_.addWatch(solverId, Clasp::decodeLit(lit)); }
     void enableHistory(bool b) override { p_.enableHistory(b); };
-    Potassco::Lit_t addLiteral() override {
-        return Clasp::encodeLit(Clasp::Literal(facade_().ctx.addVar(Clasp::Var_t::Atom), false));
+    Potassco::Lit_t addLiteral(bool freeze) override {
+        auto &ctx = facade_().ctx;
+        auto var = ctx.addVar(Clasp::Var_t::Atom);
+        if (freeze) {
+            ctx.setFrozen(var, true);
+        }
+        return Clasp::encodeLit(Clasp::Literal(var, false));
     }
     bool addClause(Potassco::LitSpan lits) override {
         auto &ctx = static_cast<Clasp::ClaspFacade*>(c_.claspFacade())->ctx;

libclingo/src/control.cc

@@ -688,8 +688,8 @@ extern "C" clingo_assignment_t const *clingo_propagate_init_assignment(clingo_pr
     return static_cast<clingo_assignment_t const *>(&init->assignment());
 }
 
-extern "C" bool clingo_propagate_init_add_literal(clingo_propagate_init_t *init, clingo_literal_t *ret) {
-    GRINGO_CLINGO_TRY { *ret = init->addLiteral(); }
+extern "C" bool clingo_propagate_init_add_literal(clingo_propagate_init_t *init, bool freeze, clingo_literal_t *ret) {
+    GRINGO_CLINGO_TRY { *ret = init->addLiteral(freeze); }
     GRINGO_CLINGO_CATCH;
 }
 

libluaclingo/luaclingo.cc

@@ -2561,7 +2561,8 @@ struct PropagateInit : Object<PropagateInit> {
 
     static int addLiteral(lua_State *L) {
         auto &self = get_self(L);
-        lua_pushinteger(L, call_c(L, clingo_propagate_init_add_literal, self.init));
+        bool freeze = lua_isnoneornil(L, 1) || lua_toboolean(L, 1);
+        lua_pushinteger(L, call_c(L, clingo_propagate_init_add_literal, self.init, freeze));
         return 1;
     }
 

libpyclingo/pyclingo.cc

@@ -3876,9 +3876,13 @@ Control.register_propagator
         Py_RETURN_NONE;
     }
 
-    Object addLiteral() {
+    Object addLiteral(Reference pyargs, Reference pykwds) {
+        static char const *kwlist[] = {"freeze", nullptr};
+        Reference pyFreeze = Py_True;
+        ParseTupleAndKeywords(pyargs, pykwds, "|O", kwlist, pyFreeze);
+
         clingo_literal_t ret;
-        handle_c_error(clingo_propagate_init_add_literal(init, &ret));
+        handle_c_error(clingo_propagate_init_add_literal(init, pyToCpp<bool>(pyFreeze), &ret));
         return cppToPy(ret);
     }
 
@@ -3969,10 +3973,18 @@ Returns
 int
     A solver literal.
 )"},
-    {"add_literal", to_function<&PropagateInit::addLiteral>(), METH_NOARGS, R"(add_literal(self) -> int
+    {"add_literal", to_function<&PropagateInit::addLiteral>(), METH_KEYWORDS | METH_VARARGS, R"(add_literal(self, freeze: bool=True) -> int
 
 Statically adds a literal to the solver.
 
+To be able to use the variable in clauses during propagation or add watches to
+it, it has to be frozen. Otherwise, it might be removed during preprocessing.
+
+Parameters
+----------
+freeze : bool=True
+    Whether to freeze the variable.
+
 Returns
 -------
 int