From 96a292613cdd5ebcc023842086cdfaab2149bf03 Mon Sep 17 00:00:00 2001 From: Roland Kaminski Date: Wed, 29 Jul 2020 11:17:29 +0200 Subject: [PATCH] add an option to freeze literals This commit adds an option to freeze a literal added during propagator initialization. This is important to prevent the literal from being eliminated from preprocessing. Not freezing the literal will lead to crashes if clauses over this literal are added later during propagation. --- libclingo/clingo.h | 6 +++++- libclingo/clingo.hh | 6 +++--- libclingo/clingo/control.hh | 2 +- libclingo/src/clingocontrol.cc | 9 +++++++-- libclingo/src/control.cc | 4 ++-- libluaclingo/luaclingo.cc | 3 ++- libpyclingo/pyclingo.cc | 18 +++++++++++++++--- 7 files changed, 35 insertions(+), 13 deletions(-) diff --git a/libclingo/clingo.h b/libclingo/clingo.h index 0eb6d51ce..63616da3f 100644 --- a/libclingo/clingo.h +++ b/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. diff --git a/libclingo/clingo.hh b/libclingo/clingo.hh index d5e67cbd2..d8e9e88b2 100644 --- a/libclingo/clingo.hh +++ b/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; } diff --git a/libclingo/clingo/control.hh b/libclingo/clingo/control.hh index dd5a967d6..62d42600c 100644 --- a/libclingo/clingo/control.hh +++ b/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; diff --git a/libclingo/src/clingocontrol.cc b/libclingo/src/clingocontrol.cc index 8cc64dc72..4acfb0e90 100644 --- a/libclingo/src/clingocontrol.cc +++ b/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(c_.claspFacade())->ctx; diff --git a/libclingo/src/control.cc b/libclingo/src/control.cc index 5e7b9759b..98b7dc3b5 100644 --- a/libclingo/src/control.cc +++ b/libclingo/src/control.cc @@ -688,8 +688,8 @@ extern "C" clingo_assignment_t const *clingo_propagate_init_assignment(clingo_pr return static_cast(&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; } diff --git a/libluaclingo/luaclingo.cc b/libluaclingo/luaclingo.cc index f13088a76..3239a0603 100644 --- a/libluaclingo/luaclingo.cc +++ b/libluaclingo/luaclingo.cc @@ -2561,7 +2561,8 @@ struct PropagateInit : Object { 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; } diff --git a/libpyclingo/pyclingo.cc b/libpyclingo/pyclingo.cc index 408b0ac3d..83c97b1f2 100644 --- a/libpyclingo/pyclingo.cc +++ b/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(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