1 // 2 // Copyright (c) 2010-2017 Benjamin Kaufmann 3 // 4 // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/ 5 // 6 // Permission is hereby granted, free of charge, to any person obtaining a copy 7 // of this software and associated documentation files (the "Software"), to 8 // deal in the Software without restriction, including without limitation the 9 // rights to use, copy, modify, merge, publish, distribute, sublicense, and/or 10 // sell copies of the Software, and to permit persons to whom the Software is 11 // furnished to do so, subject to the following conditions: 12 // 13 // The above copyright notice and this permission notice shall be included in 14 // all copies or substantial portions of the Software. 15 // 16 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR 17 // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, 18 // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE 19 // AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER 20 // LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING 21 // FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS 22 // IN THE SOFTWARE. 23 // 24 #ifndef CLASP_SHARED_CONTEXT_H_INCLUDED 25 #define CLASP_SHARED_CONTEXT_H_INCLUDED 26 #ifdef _MSC_VER 27 #pragma once 28 #endif 29 #include <clasp/claspfwd.h> 30 #include <clasp/literal.h> 31 #include <clasp/constraint.h> 32 #include <clasp/util/left_right_sequence.h> 33 #include <clasp/solver_strategies.h> 34 /*! 35 * \file 36 * \brief Contains common types shared between different solvers. 37 */ 38 namespace Clasp { 39 class Assignment; 40 class SharedLiterals; 41 struct SolverStats; 42 class StatisticObject; 43 typedef Asp::PrgDepGraph PrgDepGraph; 44 //! An immutable string with efficient copying. 45 /*! 46 * \ingroup misc 47 */ 48 class ConstString { 49 public: 50 //! Creates a string from str. 51 /*! 52 * \note If o is Ownership_t::Acquire (the default), str is copied. 53 * Otherwise, no copy is made and the lifetime of str shall extend 54 * past that of the constructed object. 55 */ 56 ConstString(const char* str = "", Ownership_t::Type o = Ownership_t::Acquire); 57 //! Creates a copy of str. 58 ConstString(const StrView& str); 59 ConstString(const ConstString& other); 60 ~ConstString(); fromLiteral(const char * str)61 static ConstString fromLiteral(const char* str) { return ConstString(str, Ownership_t::Retain); } 62 ConstString& operator=(const ConstString& rhs); 63 const char* c_str() const; 64 operator const char* () const { return c_str(); } 65 void swap(ConstString& o); 66 private: 67 typedef uint64 RefType; 68 RefType ref_; 69 }; 70 /** 71 * \defgroup shared SharedContext 72 * \brief %SharedContext and related types. 73 */ 74 75 //! Base class for event handlers. 76 /*! 77 * \ingroup shared 78 */ 79 class EventHandler : public ModelHandler { 80 public: 81 //! Creates a handler for events with given verbosity or lower. 82 explicit EventHandler(Event::Verbosity verbosity = Event::verbosity_quiet); 83 virtual ~EventHandler(); 84 //! Sets the verbosity for the given event source. 85 /*! 86 * Events with higher verbosity are not dispatched to this handler. 87 */ 88 void setVerbosity(Event::Subsystem sys, Event::Verbosity verb); 89 //! Sets the active event source to sys if sys is not yet active. 90 bool setActive(Event::Subsystem sys); 91 Event::Subsystem active() const; verbosity(Event::Subsystem sys)92 uint32 verbosity(Event::Subsystem sys) const { return (uint32(verb_) >> (uint32(sys)<<VERB_SHIFT)) & uint32(VERB_MAX); } 93 //! Calls onEvent(ev) if ev has acceptable verbosity. dispatch(const Event & ev)94 void dispatch(const Event& ev) { if (ev.verb <= verbosity(static_cast<Event::Subsystem>(ev.system))) { onEvent(ev); } } onEvent(const Event &)95 virtual void onEvent(const Event& /* ev */) {} onModel(const Solver &,const Model &)96 virtual bool onModel(const Solver&, const Model&) { return true; } 97 private: 98 enum { VERB_SHIFT = 2u, VERB_MAX = 15u }; 99 EventHandler(const EventHandler&); 100 EventHandler& operator=(const EventHandler&); 101 uint16 verb_; 102 uint16 sys_; 103 }; 104 105 //! Event type for log or warning messages. 106 /*! 107 * \ingroup enumerator 108 */ 109 struct LogEvent : Event_t<LogEvent> { 110 enum Type { Message = 'M', Warning = 'W' }; LogEventLogEvent111 LogEvent(Subsystem sys, Verbosity verb, Type t, const Solver* s, const char* what) : Event_t<LogEvent>(sys, verb), solver(s), msg(what) { 112 op = static_cast<uint32>(t); 113 } isWarningLogEvent114 bool isWarning() const { return op == static_cast<uint32>(Warning); } 115 const Solver* solver; 116 const char* msg; 117 }; 118 119 //! Base class for preprocessors working on clauses only. 120 /*! 121 * \ingroup shared 122 */ 123 class SatPreprocessor { 124 public: 125 //! A clause class optimized for preprocessing. 126 class Clause { 127 public: 128 static Clause* newClause(const Literal* lits, uint32 size); abstractLit(Literal p)129 static uint64 abstractLit(Literal p) { return uint64(1) << ((p.var()-1) & 63); } size()130 uint32 size() const { return size_; } 131 const Literal& operator[](uint32 x) const { return lits_[x]; } inQ()132 bool inQ() const { return inQ_ != 0; } abstraction()133 uint64 abstraction() const { return data_.abstr; } next()134 Clause* next() const { return data_.next; } marked()135 bool marked() const { return marked_ != 0;} 136 Literal& operator[](uint32 x) { return lits_[x]; } setInQ(bool b)137 void setInQ(bool b) { inQ_ = (uint32)b;} setMarked(bool b)138 void setMarked(bool b) { marked_ = (uint32)b;} abstraction()139 uint64& abstraction() { return data_.abstr; } linkRemoved(Clause * next)140 Clause* linkRemoved(Clause* next) { data_.next = next; return this; } 141 void strengthen(Literal p); 142 void simplify(Solver& s); 143 void destroy(); 144 private: 145 Clause(const Literal* lits, uint32 size); 146 union { 147 uint64 abstr; // abstraction of literals 148 Clause* next; // next removed clause 149 } data_; 150 uint32 size_ : 30; // size of the clause 151 uint32 inQ_ : 1; // in todo-queue? 152 uint32 marked_ : 1; // a marker flag 153 Literal lits_[1]; // literals of the clause: [lits_[0], lits_[size_]) 154 }; 155 156 SatPreprocessor(); 157 virtual ~SatPreprocessor(); 158 159 //! Creates a clone of this preprocessor. 160 /*! 161 * \note The function does not clone any clauses already added to *this. 162 */ 163 virtual SatPreprocessor* clone() = 0; 164 numClauses()165 uint32 numClauses() const { return (uint32)clauses_.size(); } 166 //! Adds a clause to the preprocessor. 167 /*! 168 * \pre clause is not a tautology (i.e. does not contain both l and ~l) 169 * \pre clause is a set (i.e. does not contain l more than once) 170 * \return true if clause was added. False if adding the clause makes the problem UNSAT 171 */ addClause(const LitVec & cl)172 bool addClause(const LitVec& cl) { return addClause(!cl.empty() ? &cl[0] : 0, sizeVec(cl)); } 173 bool addClause(const Literal* clause, uint32 size); 174 //! Runs the preprocessor on all clauses that were previously added. 175 /*! 176 * \pre A ctx.startAddConstraint() was called and has variables for all added clauses. 177 */ 178 bool preprocess(SharedContext& ctx, SatPreParams& opts); 179 bool preprocess(SharedContext& ctx); 180 181 //! Force removal of state & clauses. 182 void cleanUp(bool discardEliminated = false); 183 184 //! Extends the model in m with values for any eliminated variables. 185 void extendModel(ValueVec& m, LitVec& open); 186 struct Stats { StatsStats187 Stats() : clRemoved(0), clAdded(0), litsRemoved(0) {} 188 uint32 clRemoved; 189 uint32 clAdded; 190 uint32 litsRemoved; 191 } stats; 192 typedef SatPreParams Options; 193 protected: 194 typedef PodVector<Clause*>::type ClauseList; 195 virtual bool initPreprocess(SatPreParams& opts) = 0; 196 virtual bool doPreprocess() = 0; 197 virtual void doExtendModel(ValueVec& m, LitVec& open) = 0; 198 virtual void doCleanUp() = 0; clause(uint32 clId)199 Clause* clause(uint32 clId) { return clauses_[clId]; } clause(uint32 clId)200 const Clause* clause(uint32 clId) const { return clauses_[clId]; } 201 void freezeSeen(); 202 void discardClauses(bool discardEliminated); setClause(uint32 clId,const LitVec & cl)203 void setClause(uint32 clId, const LitVec& cl) { 204 clauses_[clId] = Clause::newClause(&cl[0], (uint32)cl.size()); 205 } destroyClause(uint32 clId)206 void destroyClause(uint32 clId){ 207 clauses_[clId]->destroy(); 208 clauses_[clId] = 0; 209 ++stats.clRemoved; 210 } eliminateClause(uint32 id)211 void eliminateClause(uint32 id){ 212 elimTop_ = clauses_[id]->linkRemoved(elimTop_); 213 clauses_[id] = 0; 214 ++stats.clRemoved; 215 } 216 SharedContext* ctx_; // current context 217 const Options* opts_; // active options 218 Clause* elimTop_; // stack of blocked/eliminated clauses 219 private: 220 SatPreprocessor(const SatPreprocessor&); 221 SatPreprocessor& operator=(const SatPreprocessor&); 222 ClauseList clauses_; // initial non-unit clauses 223 LitVec units_; // initial unit clauses 224 Range32 seen_; // vars seen in previous step 225 }; 226 227 /////////////////////////////////////////////////////////////////////////////// 228 // Problem statistics 229 /////////////////////////////////////////////////////////////////////////////// 230 /*! 231 * \addtogroup shared 232 * @{ 233 */ 234 //! A struct for aggregating basic problem statistics. 235 struct ProblemStats { ProblemStatsProblemStats236 ProblemStats() { reset(); } 237 struct { uint32 num, eliminated, frozen; } vars; 238 struct { uint32 other, binary, ternary; } constraints; 239 uint32 acycEdges; 240 uint32 complexity; resetProblemStats241 void reset() { std::memset(this, 0, sizeof(*this)); } numConstraintsProblemStats242 uint32 numConstraints() const { return constraints.other + constraints.binary + constraints.ternary; } diffProblemStats243 void diff(const ProblemStats& o) { 244 vars.num = std::max(vars.num, o.vars.num)-std::min(vars.num, o.vars.num); 245 vars.eliminated = std::max(vars.eliminated, o.vars.eliminated)-std::min(vars.eliminated, o.vars.eliminated); 246 vars.frozen = std::max(vars.frozen, o.vars.frozen)-std::min(vars.frozen, o.vars.frozen); 247 constraints.other = std::max(constraints.other, o.constraints.other) - std::min(constraints.other, o.constraints.other); 248 constraints.binary = std::max(constraints.binary, o.constraints.binary) - std::min(constraints.binary, o.constraints.binary); 249 constraints.ternary= std::max(constraints.ternary, o.constraints.ternary) - std::min(constraints.ternary, o.constraints.ternary); 250 acycEdges = std::max(acycEdges, o.acycEdges) - std::min(acycEdges, o.acycEdges); 251 } accuProblemStats252 void accu(const ProblemStats& o) { 253 vars.num += o.vars.num; 254 vars.eliminated += o.vars.eliminated; 255 vars.frozen += o.vars.frozen; 256 constraints.other += o.constraints.other; 257 constraints.binary += o.constraints.binary; 258 constraints.ternary += o.constraints.ternary; 259 acycEdges += o.acycEdges; 260 } 261 // StatisticObject 262 static uint32 size(); 263 static const char* key(uint32 i); 264 StatisticObject at(const char* k) const; 265 }; 266 267 //! Stores static information about a variable. 268 struct VarInfo { 269 //! Possible flags. 270 enum Flag { 271 Mark_p = 0x1u, //!< Mark for positive literal. 272 Mark_n = 0x2u, //!< Mark for negative literal. 273 Input = 0x4u, //!< Is this var an input variable? 274 Body = 0x8u, //!< Is this var representing a body? 275 Eq = 0x10u, //!< Is this var representing both a body and an atom? 276 Nant = 0x20u, //!< Is this var in NAnt(P)? 277 Frozen = 0x40u, //!< Is the variable frozen? 278 Output = 0x80u //!< Is the variable an output variable? 279 }; flagsVarInfo280 static uint8 flags(VarType t) { 281 if (t == Var_t::Body) { return VarInfo::Body; } 282 if (t == Var_t::Hybrid){ return VarInfo::Eq; } 283 return 0; 284 } repVarInfo285 explicit VarInfo(uint8 r = 0) : rep(r) { } 286 //! Returns the type of the variable (or Var_t::Hybrid if variable was created with parameter eq=true). typeVarInfo287 VarType type() const { return has(VarInfo::Eq) ? Var_t::Hybrid : VarType(Var_t::Atom + has(VarInfo::Body)); } 288 //! Returns whether var is part of negative antecedents (occurs negatively or in the head of a choice rule). nantVarInfo289 bool nant() const { return has(VarInfo::Nant); } 290 //! Returns true if var is excluded from variable elimination. frozenVarInfo291 bool frozen() const { return has(VarInfo::Frozen); } 292 //! Returns true if var is an input variable. inputVarInfo293 bool input() const { return has(VarInfo::Input); } 294 //! Returns true if var is marked as output variable. outputVarInfo295 bool output() const { return has(VarInfo::Output); } 296 //! Returns the preferred sign of this variable w.r.t its type. 297 /*! 298 * \return false (i.e no sign) if var originated from body, otherwise true. 299 */ preferredSignVarInfo300 bool preferredSign() const { return !has(VarInfo::Body); } 301 hasVarInfo302 bool has(Flag f) const { return (rep & flag(f)) != 0; } hasVarInfo303 bool has(uint32 f) const { return (rep & f) != 0; } hasAllVarInfo304 bool hasAll(uint32 f)const { return (rep & f) == f; } setVarInfo305 void set(Flag f) { rep |= flag(f); } toggleVarInfo306 void toggle(Flag f) { rep ^= flag(f); } flagVarInfo307 static uint8 flag(Flag x) { return uint8(x); } 308 uint8 rep; 309 }; 310 311 //! A class for efficiently storing and propagating binary and ternary clauses. 312 /*! 313 * \ingroup shared_con 314 */ 315 class ShortImplicationsGraph { 316 public: 317 ShortImplicationsGraph(); 318 ~ShortImplicationsGraph(); 319 enum ImpType { binary_imp = 2, ternary_imp = 3 }; 320 321 //! Makes room for nodes number of nodes. 322 void resize(uint32 nodes); 323 //! Mark the instance as shared/unshared. 324 /*! 325 * A shared instance adds learnt binary/ternary clauses 326 * to specialized shared blocks of memory. 327 */ markShared(bool b)328 void markShared(bool b) { shared_ = b; } 329 //! Adds the given constraint to the implication graph. 330 /*! 331 * \return true iff a new implication was added. 332 */ 333 bool add(ImpType t, bool learnt, const Literal* lits); 334 335 //! Removes p and its implications. 336 /*! 337 * \pre s.isTrue(p) 338 */ 339 void removeTrue(const Solver& s, Literal p); 340 341 //! Propagates consequences of p following from binary and ternary clauses. 342 /*! 343 * \pre s.isTrue(p) 344 */ 345 bool propagate(Solver& s, Literal p) const; 346 //! Propagates immediate consequences of p following from binary clauses only. 347 bool propagateBin(Assignment& out, Literal p, uint32 dl) const; 348 //! Checks whether there is a reverse arc implying p and if so returns it in out. 349 bool reverseArc(const Solver& s, Literal p, uint32 maxLev, Antecedent& out) const; 350 numBinary()351 uint32 numBinary() const { return bin_[0]; } numTernary()352 uint32 numTernary()const { return tern_[0]; } numLearnt()353 uint32 numLearnt() const { return bin_[1] + tern_[1]; } 354 uint32 numEdges(Literal p) const; size()355 uint32 size() const { return sizeVec(graph_); } 356 //! Applies op on all unary- and binary implications following from p. 357 /*! 358 * OP must provide two functions: 359 * - bool unary(Literal, Literal) 360 * - bool binary(Literal, Literal, Literal) 361 * The first argument will be p, the second (resp. third) the unary 362 * (resp. binary) clause implied by p. 363 * \note For learnt imps, at least one literal has its watch-flag set. 364 */ 365 template <class OP> forEach(Literal p,const OP & op)366 bool forEach(Literal p, const OP& op) const { 367 const ImplicationList& x = graph_[p.id()]; 368 if (x.empty()) return true; 369 ImplicationList::const_right_iterator rEnd = x.right_end(); // prefetch 370 for (ImplicationList::const_left_iterator it = x.left_begin(), end = x.left_end(); it != end; ++it) { 371 if (!op.unary(p, *it)) { return false; } 372 } 373 for (ImplicationList::const_right_iterator it = x.right_begin(); it != rEnd; ++it) { 374 if (!op.binary(p, it->first, it->second)) { return false; } 375 } 376 #if CLASP_HAS_THREADS 377 for (Block* b = (x).learnt; b ; b = b->next) { 378 p.flag(); bool r = true; 379 for (Block::const_iterator imp = b->begin(), endOf = b->end(); imp != endOf; ) { 380 if (!imp->flagged()) { r = op.binary(p, imp[0], imp[1]); imp += 2; } 381 else { r = op.unary(p, imp[0]); imp += 1; } 382 if (!r) { return false; } 383 } 384 } 385 #endif 386 return true; 387 } 388 private: 389 ShortImplicationsGraph(const ShortImplicationsGraph&); 390 ShortImplicationsGraph& operator=(ShortImplicationsGraph&); 391 struct Propagate; 392 struct ReverseArc; 393 #if CLASP_HAS_THREADS 394 struct Block { 395 typedef Clasp::mt::atomic<uint32> atomic_size; 396 typedef Clasp::mt::atomic<Block*> atomic_ptr; 397 typedef const Literal* const_iterator; 398 typedef Literal* iterator; 399 enum { block_cap = (64 - (sizeof(atomic_size)+sizeof(atomic_ptr)))/sizeof(Literal) }; 400 explicit Block(); beginBlock401 const_iterator begin() const { return data; } endBlock402 const_iterator end() const { return data+size(); } endBlock403 iterator end() { return data+size(); } sizeBlock404 uint32 size() const { return size_lock >> 1; } 405 bool tryLock(uint32& lockedSize); 406 void addUnlock(uint32 lockedSize, const Literal* x, uint32 xs); 407 atomic_ptr next; 408 atomic_size size_lock; 409 Literal data[block_cap]; 410 }; 411 typedef Block::atomic_ptr SharedBlockPtr; 412 typedef bk_lib::left_right_sequence<Literal, std::pair<Literal,Literal>, 64-sizeof(SharedBlockPtr)> ImpListBase; 413 struct ImplicationList : public ImpListBase { ImplicationListImplicationList414 ImplicationList() : ImpListBase() { learnt = 0; } ImplicationListImplicationList415 ImplicationList(const ImplicationList& other) : ImpListBase(other), learnt() { 416 learnt = static_cast<Block*>(other.learnt); 417 } 418 ImplicationList& operator=(const ImplicationList& other) { 419 ImpListBase::operator=(other); 420 learnt = static_cast<Block*>(other.learnt); 421 return *this; 422 } 423 ~ImplicationList(); 424 bool hasLearnt(Literal q, Literal r = lit_false()) const; 425 void addLearnt(Literal q, Literal r = lit_false()); 426 void simplifyLearnt(const Solver& s); emptyImplicationList427 bool empty() const { return ImpListBase::empty() && learnt == static_cast<Block*>(0); } 428 void move(ImplicationList& other); 429 void clear(bool b); 430 SharedBlockPtr learnt; 431 }; 432 #else 433 typedef bk_lib::left_right_sequence<Literal, std::pair<Literal,Literal>, 64> ImplicationList; 434 #endif getList(Literal p)435 ImplicationList& getList(Literal p) { return graph_[p.id()]; } 436 void remove_bin(ImplicationList& w, Literal p); 437 void remove_tern(ImplicationList& w, Literal p); 438 typedef PodVector<ImplicationList>::type ImpLists; 439 ImpLists graph_; // one implication list for each literal 440 uint32 bin_[2]; // number of binary constraints (0: problem / 1: learnt) 441 uint32 tern_[2]; // number of ternary constraints(0: problem / 1: learnt) 442 bool shared_; 443 }; 444 445 //! Base class for distributing learnt knowledge between solvers. 446 class Distributor { 447 public: 448 struct Policy { 449 enum Types { 450 no = 0, 451 conflict = Constraint_t::Conflict, 452 loop = Constraint_t::Loop, 453 all = conflict | loop, 454 implicit = all + 1 455 }; sizePolicy456 Policy(uint32 a_sz = 0, uint32 a_lbd = 0, uint32 a_type = 0) : size(a_sz), lbd(a_lbd), types(a_type) {} 457 uint32 size : 22; /*!< Allow distribution up to this size only. */ 458 uint32 lbd : 7; /*!< Allow distribution up to this lbd only. */ 459 uint32 types : 3; /*!< Restrict distribution to these types. */ 460 }; mask(uint32 i)461 static uint64 mask(uint32 i) { return uint64(1) << i; } initSet(uint32 sz)462 static uint32 initSet(uint32 sz) { return (uint64(1) << sz) - 1; } inSet(uint64 s,uint32 id)463 static bool inSet(uint64 s, uint32 id) { return (s & mask(id)) != 0; } 464 explicit Distributor(const Policy& p); 465 virtual ~Distributor(); isCandidate(uint32 size,uint32 lbd,uint32 type)466 bool isCandidate(uint32 size, uint32 lbd, uint32 type) const { 467 return size <= policy_.size && lbd <= policy_.lbd && ((type & policy_.types) != 0); 468 } 469 virtual void publish(const Solver& source, SharedLiterals* lits) = 0; 470 virtual uint32 receive(const Solver& in, SharedLiterals** out, uint32 maxOut) = 0; 471 private: 472 Distributor(const Distributor&); 473 Distributor& operator=(const Distributor&); 474 Policy policy_; 475 }; 476 477 //! Output table that contains predicates to be output on model. 478 class OutputTable { 479 public: 480 typedef ConstString NameType; 481 typedef Range32 RangeType; 482 struct PredType { 483 NameType name; 484 Literal cond; 485 uint32 user; 486 }; 487 typedef PodVector<NameType>::type FactVec; 488 typedef PodVector<PredType>::type PredVec; 489 typedef FactVec::const_iterator fact_iterator; 490 typedef PredVec::const_iterator pred_iterator; 491 typedef num_iterator<uint32> range_iterator; 492 typedef LitVec::const_iterator lit_iterator; 493 494 OutputTable(); 495 ~OutputTable(); 496 //! Ignore predicates starting with c. 497 void setFilter(char c); 498 //! Adds a fact. 499 bool add(const NameType& fact); 500 //! Adds an output predicate, i.e. n is output if c is true. 501 bool add(const NameType& n, Literal c, uint32 u = 0); 502 //! Sets a range of output variables. 503 void setVarRange(const RangeType& r); 504 void setProjectMode(ProjectMode m); 505 506 //! Returns whether n would be filtered out. 507 bool filter(const NameType& n) const; 508 fact_begin()509 fact_iterator fact_begin() const { return facts_.begin(); } fact_end()510 fact_iterator fact_end() const { return facts_.end(); } pred_begin()511 pred_iterator pred_begin() const { return preds_.begin(); } pred_end()512 pred_iterator pred_end() const { return preds_.end(); } vars_begin()513 range_iterator vars_begin() const { return range_iterator(vars_.lo); } vars_end()514 range_iterator vars_end() const { return range_iterator(vars_.hi); } vars_range()515 RangeType vars_range() const { return vars_; } 516 projectMode()517 ProjectMode projectMode()const { return projMode_ ? static_cast<ProjectMode>(projMode_) : hasProject() ? ProjectMode_t::Explicit : ProjectMode_t::Output; } hasProject()518 bool hasProject() const { return !proj_.empty(); } proj_begin()519 lit_iterator proj_begin() const { return proj_.begin(); } proj_end()520 lit_iterator proj_end() const { return proj_.end(); } 521 void addProject(Literal x); 522 523 //! Returns the number of output elements, counting each element in a var range. 524 uint32 size() const; numFacts()525 uint32 numFacts() const { return static_cast<uint32>(facts_.size()); } numPreds()526 uint32 numPreds() const { return static_cast<uint32>(preds_.size()); } numVars()527 uint32 numVars() const { return static_cast<uint32>(vars_.hi - vars_.lo); } 528 529 //! An optional callback for getting additional theory output. 530 class Theory { 531 public: 532 virtual ~Theory(); 533 //! Called once on new model m. Shall return 0 to indicate no output. 534 virtual const char* first(const Model& m) = 0; 535 //! Shall return 0 to indicate no output. 536 virtual const char* next() = 0; 537 }* theory; 538 private: 539 FactVec facts_; 540 PredVec preds_; 541 LitVec proj_; 542 Range32 vars_; 543 int projMode_; 544 char hide_; 545 }; 546 //! A type for storing information to be used in clasp's domain heuristic. 547 class DomainTable { 548 public: 549 DomainTable(); 550 //! A type storing a single domain modification for a variable. 551 class ValueType { 552 public: 553 ValueType(Var v, DomModType t, int16 bias, uint16 prio, Literal cond); hasCondition()554 bool hasCondition() const { return cond_ != 0; } cond()555 Literal cond() const { return Literal::fromId(cond_); } var()556 Var var() const { return var_; } 557 DomModType type() const; bias()558 int16 bias() const { return bias_; } prio()559 uint16 prio() const { return prio_; } comp()560 bool comp() const { return comp_ != 0; } 561 private: 562 uint32 cond_ : 31; 563 uint32 comp_ : 1; 564 uint32 var_ : 30; 565 uint32 type_ : 2; 566 int16 bias_; 567 uint16 prio_; 568 }; 569 typedef PodVector<ValueType>::type DomVec; 570 typedef DomVec::const_iterator iterator; 571 572 void add(Var v, DomModType t, int16 bias, uint16 prio, Literal cond); 573 uint32 simplify(); 574 void reset(); 575 bool empty() const; 576 uint32 size() const; 577 iterator begin() const; 578 iterator end() const; 579 LitVec* assume; 580 581 class DefaultAction { 582 public: 583 virtual ~DefaultAction(); 584 virtual void atom(Literal p, HeuParams::DomPref, uint32 strat) = 0; 585 }; 586 static void applyDefault(const SharedContext& ctx, DefaultAction& action, uint32 prefSet = 0); 587 private: cmp(const ValueType & lhs,const ValueType & rhs)588 static bool cmp(const ValueType& lhs, const ValueType& rhs) { 589 return lhs.cond() < rhs.cond() || (lhs.cond() == rhs.cond() && lhs.var() < rhs.var()); 590 } 591 DomVec entries_; 592 uint32 seen_; // size of domain table after last simplify 593 }; 594 595 //! Aggregates information to be shared between solver objects. 596 /*! 597 * Among other things, SharedContext objects store 598 * static information on variables, an output table, as well as the 599 * binary and ternary implication graph of the input problem. 600 * 601 * Furthermore, a SharedContext object always stores a distinguished 602 * master solver that is used to store and simplify problem constraints. 603 * Additional solvers can be added via SharedContext::pushSolver(). 604 * Once initialization is completed, any additional solvers must be attached 605 * to this object by calling SharedContext::attach(). 606 */ 607 class SharedContext { 608 public: 609 typedef PodVector<Solver*>::type SolverVec; 610 typedef SingleOwnerPtr<PrgDepGraph> SccGraph; 611 typedef SingleOwnerPtr<ExtDepGraph> ExtGraph; 612 typedef Configuration* ConfigPtr; 613 typedef SingleOwnerPtr<Distributor> DistrPtr; 614 typedef const ProblemStats& StatsCRef; 615 typedef DomainTable DomTab; 616 typedef OutputTable Output; 617 typedef LitVec::size_type size_type; 618 typedef ShortImplicationsGraph ImpGraph; 619 typedef const ImpGraph& ImpGraphRef; 620 typedef EventHandler* LogPtr; 621 typedef SingleOwnerPtr<SatPreprocessor>SatPrePtr; 622 typedef SharedMinimizeData* MinPtr; 623 enum ResizeMode { resize_reserve = 0u, resize_push = 1u, resize_pop = 2u, resize_resize = 3u}; 624 enum PreproMode { prepro_preserve_models = 1u, prepro_preserve_shown = 2u }; 625 enum ReportMode { report_default = 0u, report_conflict = 1u }; 626 enum SolveMode { solve_once = 0u, solve_multi = 1u }; 627 /*! 628 * \name Configuration 629 * \brief Functions for creating and configuring a shared context. 630 * @{ */ 631 //! Creates a new object for sharing variables and the binary and ternary implication graph. 632 explicit SharedContext(); 633 ~SharedContext(); 634 //! Resets this object to the state after default construction. 635 void reset(); 636 //! Enables event reporting via the given event handler. 637 void setEventHandler(LogPtr r, ReportMode m = report_default) { progress_ = r; share_.report = uint32(m); } 638 //! Sets solve mode, which can be used by other objects to query whether multi-shot solving is active. 639 void setSolveMode(SolveMode m); 640 //! Sets how to handle physical sharing of constraints. 641 void setShareMode(ContextParams::ShareMode m); 642 //! Sets whether the short implication graph should be used for storing short learnt constraints. 643 void setShortMode(ContextParams::ShortMode m); 644 //! Sets maximal number of solvers sharing this object. 645 void setConcurrency(uint32 numSolver, ResizeMode m = resize_reserve); 646 //! If b is true, sets preprocessing mode to model-preserving operations only. 647 void setPreserveModels(bool b = true) { setPreproMode(prepro_preserve_models, b); } 648 //! If b is true, excludes all shown variables from variable elimination. 649 void setPreserveShown(bool b = true) { setPreproMode(prepro_preserve_shown, b); } 650 651 //! Adds an additional solver to this object and returns it. 652 Solver& pushSolver(); 653 //! Configures the statistic object of attached solvers. 654 /*! 655 * The level determines the amount of extra statistics. 656 * \see ExtendedStats 657 * \see JumpStats 658 */ 659 void enableStats(uint32 level); 660 //! Sets the configuration for this object and its attached solvers. 661 /*! 662 * \note If ownership is Ownership_t::Acquire, ownership of c is transferred. 663 */ 664 void setConfiguration(Configuration* c, Ownership_t::Type ownership); 665 SatPrePtr satPrepro; /*!< Preprocessor for simplifying the problem. */ 666 SccGraph sccGraph; /*!< Program dependency graph - only used for ASP-problems. */ 667 ExtGraph extGraph; /*!< External dependency graph - given by user. */ 668 669 //! Returns the current configuration used in this object. configuration()670 ConfigPtr configuration() const { return config_.get(); } 671 //! Returns the active event handler or 0 if none was set. eventHandler()672 LogPtr eventHandler() const { return progress_; } 673 //! Returns whether this object seeds the RNG of new solvers. seedSolvers()674 bool seedSolvers() const { return share_.seed != 0; } 675 //! Returns the number of solvers that can share this object. concurrency()676 uint32 concurrency() const { return share_.count; } preserveModels()677 bool preserveModels() const { return (share_.satPreM & prepro_preserve_models) != 0; } preserveShown()678 bool preserveShown() const { return (share_.satPreM & prepro_preserve_shown) != 0; } 679 //! Returns whether physical sharing is enabled for constraints of type t. physicalShare(ConstraintType t)680 bool physicalShare(ConstraintType t) const { return (share_.shareM & (1 + (t != Constraint_t::Static))) != 0; } 681 //! Returns whether physical sharing of problem constraints is enabled. physicalShareProblem()682 bool physicalShareProblem() const { return (share_.shareM & ContextParams::share_problem) != 0; } 683 //! Returns whether short constraints of type t can be stored in the short implication graph. allowImplicit(ConstraintType t)684 bool allowImplicit(ConstraintType t) const { return t != Constraint_t::Static ? share_.shortM != ContextParams::short_explicit : !isShared(); } 685 //! Returns the configured solve mode. solveMode()686 SolveMode solveMode() const { return static_cast<SolveMode>(share_.solveM); } 687 //@} 688 689 /*! 690 * \name Problem introspection 691 * \brief Functions for querying information about the problem. 692 */ 693 //@{ 694 //! Returns true unless the master has an unresolvable top-level conflict. 695 bool ok() const; 696 //! Returns whether the problem is currently frozen and therefore ready for being solved. frozen()697 bool frozen() const { return share_.frozen;} 698 //! Returns whether more than one solver is actively working on the problem. isShared()699 bool isShared() const { return frozen() && concurrency() > 1; } 700 //! Returns whether the problem is more than a simple CNF. isExtended()701 bool isExtended() const { return stats_.vars.frozen != 0; } 702 //! Returns whether this object has a solver associcated with the given id. hasSolver(uint32 id)703 bool hasSolver(uint32 id) const { return id < solvers_.size(); } 704 //! Returns the master solver associated with this object. master()705 Solver* master() const { return solver(0); } 706 //! Returns the solver with the given id. solver(uint32 id)707 Solver* solver(uint32 id) const { return solvers_[id]; } 708 709 //! Returns the number of problem variables. 710 /*! 711 * \note The special sentinel-var 0 is not counted, i.e. numVars() returns 712 * the number of problem-variables. 713 * To iterate over all problem variables use a loop like: 714 * \code 715 * for (Var i = 1; i <= numVars(); ++i) {...} 716 * \endcode 717 */ numVars()718 uint32 numVars() const { return static_cast<uint32>(varInfo_.size() - 1); } 719 //! Returns the number of eliminated vars. numEliminatedVars()720 uint32 numEliminatedVars() const { return stats_.vars.eliminated; } 721 //! Returns true if var represents a valid variable in this problem. 722 /*! 723 * \note The range of valid variables is [1..numVars()]. The variable 0 724 * is a special sentinel variable. 725 */ validVar(Var var)726 bool validVar(Var var) const { return var < static_cast<uint32>(varInfo_.size()); } 727 //! Returns information about the given variable. varInfo(Var v)728 VarInfo varInfo(Var v) const { assert(validVar(v)); return varInfo_[v]; } 729 //! Returns true if v is currently eliminated, i.e. no longer part of the problem. 730 bool eliminated(Var v) const; marked(Literal p)731 bool marked(Literal p) const { return varInfo(p.var()).has(VarInfo::Mark_p + p.sign()); } 732 //! Returns the number of problem constraints. 733 uint32 numConstraints() const; 734 //! Returns the number of binary constraints. numBinary()735 uint32 numBinary() const { return btig_.numBinary(); } 736 //! Returns the number of ternary constraints. numTernary()737 uint32 numTernary() const { return btig_.numTernary(); } 738 //! Returns the number of unary constraints. numUnary()739 uint32 numUnary() const { return lastTopLevel_; } 740 //! Returns an estimate of the problem complexity based on the number and type of constraints. 741 uint32 problemComplexity() const; 742 //! Returns whether the problem contains minimize (i.e. weak) constraints. 743 bool hasMinimize() const; stats()744 StatsCRef stats() const { return stats_; } 745 //@} 746 747 /*! 748 * \name Problem setup 749 * \brief Functions for specifying the problem. 750 * 751 * Problem specification is a four-stage process: 752 * -# Add variables to the SharedContext object. 753 * -# Call startAddConstraints(). 754 * -# Add problem constraints. 755 * -# Call endInit() to finish the initialization process. 756 * . 757 * \note After endInit() was called, other solvers can be attached to this object. 758 * \note In incremental setting, the process must be repeated for each incremental step. 759 * 760 * \note Problem specification is *not* thread-safe, i.e. during initialization no other thread shall 761 * access the context. 762 * 763 * \note !frozen() is a precondition for all functions in this group! 764 * @{ */ 765 //! Unfreezes a frozen program and prepares it for updates. 766 /*! 767 * The function also triggers forgetting of volatile knowledge and removes 768 * any auxiliary variables. 769 * \see requestStepVar() 770 * \see Solver::popAuxVar() 771 */ 772 bool unfreeze(); 773 774 //! Adds a new variable and returns its numerical id. 775 /*! 776 * \param type Type of variable. 777 * \param flags Additional information associated with the new variable. 778 * \note Problem variables are numbered from 1 onwards! 779 */ 780 Var addVar(VarType type, uint8 flags = VarInfo::Nant | VarInfo::Input) { return addVars(1, type, flags); } 781 Var addVars(uint32 nVars, VarType type, uint8 flags = VarInfo::Nant | VarInfo::Input); 782 //! Removes the n most recently added problem variables. 783 /*! 784 * \pre The variables have either not yet been committed by a call to startAddConstraints() 785 * or they do not occur in any constraint. 786 */ 787 void popVars(uint32 n = 1); 788 //! Freezes/defreezes a variable (a frozen var is exempt from Sat-preprocessing). 789 void setFrozen(Var v, bool b); 790 //! Marks/unmarks v as input variable. setInput(Var v,bool b)791 void setInput(Var v, bool b) { set(v, VarInfo::Input, b); } 792 //! Marks/unmarks v as output variable. setOutput(Var v,bool b)793 void setOutput(Var v, bool b) { set(v, VarInfo::Output, b); } 794 //! Marks/unmarks v as part of negative antecedents. setNant(Var v,bool b)795 void setNant(Var v, bool b) { set(v, VarInfo::Nant, b); } setVarEq(Var v,bool b)796 void setVarEq(Var v, bool b) { set(v, VarInfo::Eq, b); } set(Var v,VarInfo::Flag f,bool b)797 void set(Var v, VarInfo::Flag f, bool b) { if (b != varInfo(v).has(f)) varInfo_[v].toggle(f); } mark(Literal p)798 void mark(Literal p) { assert(validVar(p.var())); varInfo_[p.var()].rep |= (VarInfo::Mark_p + p.sign()); } unmark(Var v)799 void unmark(Var v) { assert(validVar(v)); varInfo_[v].rep &= ~(VarInfo::Mark_p|VarInfo::Mark_n); } 800 //! Eliminates the variable v from the problem. 801 /*! 802 * \pre v must not occur in any constraint and frozen(v) == false and value(v) == value_free 803 */ 804 void eliminate(Var v); 805 806 //! Prepares the master solver so that constraints can be added. 807 /*! 808 * Must be called to publish previously added variables to master solver 809 * and before constraints over these variables can be added. 810 * \return The master solver associated with this object. 811 */ 812 Solver& startAddConstraints(uint32 constraintGuess = 100); 813 814 //! A convenience method for adding facts to the master. 815 bool addUnary(Literal x); 816 //! A convenience method for adding binary clauses. 817 bool addBinary(Literal x, Literal y); 818 //! A convenience method for adding ternary clauses. 819 bool addTernary(Literal x, Literal y, Literal z); 820 //! A convenience method for adding constraints to the master. 821 void add(Constraint* c); 822 //! Add weak constraint :~ x.first \[x.second\@p\]. 823 void addMinimize(WeightLiteral x, weight_t p); 824 //! Returns a pointer to an optimized representation of all minimize constraints in this problem. 825 MinPtr minimize(); 826 //! List of output predicates and/or variables. 827 Output output; 828 //! Set of heuristic modifications. 829 DomTab heuristic; 830 //! Requests a special variable for tagging volatile knowledge in multi-shot solving. 831 /*! 832 * The step variable is created on the next call to endInit() and removed on the next 833 * call to unfreeze(). 834 * Once the step variable S is set, learnt constraints containing ~S are 835 * considered to be "volatile" and removed on the next call to unfreeze(). 836 * For this to work correctly, S shall be a root assumption during search. 837 */ 838 void requestStepVar(); 839 //! Finishes initialization of the master solver. 840 /*! 841 * The function must be called once before search is started. After endInit() 842 * was called, previously added solvers can be attached to the 843 * shared context and learnt constraints may be added to solver. 844 * \param attachAll If true, also calls attach() for all solvers that were added to this object. 845 * \return If the constraints are initially conflicting, false. Otherwise, true. 846 * \note 847 * The master solver can't recover from top-level conflicts, i.e. if endInit() 848 * returned false, the solver is in an unusable state. 849 * \post frozen() 850 */ 851 bool endInit(bool attachAll = false); 852 //@} 853 854 /*! 855 * \name (Parallel) solving 856 * Functions to be called during (parallel) solving. 857 * 858 * \note If not otherwise noted, the functions in this group can be safely called 859 * from multiple threads. 860 * @{ */ 861 //! Returns the active step literal (see requestStepVar()). stepLiteral()862 Literal stepLiteral() const { return step_; } 863 //! Attaches the solver with the given id to this object. 864 /*! 865 * \note It is safe to attach multiple solvers concurrently 866 * but the master solver shall not change during the whole operation. 867 * 868 * \pre hasSolver(id) 869 */ attach(uint32 id)870 bool attach(uint32 id) { return attach(*solver(id)); } 871 bool attach(Solver& s); 872 873 //! Detaches the solver with the given id from this object. 874 /*! 875 * The function removes any tentative constraints from s. 876 * Shall be called once after search has stopped. 877 * \note The function is concurrency-safe w.r.t to different solver objects, 878 * i.e. in a parallel search different solvers may call detach() 879 * concurrently. 880 */ 881 void detach(uint32 id, bool reset = false) { return detach(*solver(id), reset); } 882 void detach(Solver& s, bool reset = false); 883 884 DistrPtr distributor;/*!< Distributor object to use for distribution of learnt constraints.*/ 885 winner()886 uint32 winner() const { return share_.winner; } setWinner(uint32 sId)887 void setWinner(uint32 sId) { share_.winner = std::min(sId, concurrency()); } 888 889 //! Simplifies the problem constraints w.r.t the master's assignment. 890 void simplify(LitVec::size_type trailStart, bool shuffle); 891 //! Removes the constraint with the given idx from the master's db. 892 void removeConstraint(uint32 idx, bool detach); 893 //! Removes all minimize constraints from this object. 894 void removeMinimize(); 895 896 //! Adds the given short implication to the short implication graph if possible. 897 /*! 898 * \return 899 * - > 0 if implication was added. 900 * - < 0 if implication can't be added because allowImplicit() is false for ct. 901 * - = 0 if implication is subsumed by some constraint in the short implication graph. 902 */ 903 int addImp(ImpGraph::ImpType t, const Literal* lits, ConstraintType ct); 904 //! Returns the number of learnt short implications. numLearntShort()905 uint32 numLearntShort() const { return btig_.numLearnt(); } shortImplications()906 ImpGraphRef shortImplications() const { return btig_; } report(const Event & ev)907 void report(const Event& ev) const { if (progress_) progress_->dispatch(ev); } report(const Solver & s,const Model & m)908 bool report(const Solver& s, const Model& m) const { return !progress_ || progress_->onModel(s, m); } 909 void report(const char* what, const Solver* s = 0) const; 910 void report(Event::Subsystem sys) const; 911 void warn(const char* what) const; reportMode()912 ReportMode reportMode() const { return static_cast<ReportMode>(share_.report); } 913 void initStats(Solver& s) const; 914 SolverStats& solverStats(uint32 sId) const; // stats of solver i 915 const SolverStats& accuStats(SolverStats& out) const; // accumulates all solver stats in out 916 MinPtr minimizeNoCreate() const; 917 //@} 918 private: 919 SharedContext(const SharedContext&); 920 SharedContext& operator=(const SharedContext&); 921 bool unfreezeStep(); 922 Literal addStepLit(); 923 typedef SingleOwnerPtr<Configuration> Config; 924 typedef PodVector<VarInfo>::type VarVec; 925 void setPreproMode(uint32 m, bool b); 926 struct Minimize; 927 ProblemStats stats_; // problem statistics 928 VarVec varInfo_; // varInfo[v] stores info about variable v 929 ImpGraph btig_; // binary-/ternary implication graph 930 Config config_; // active configuration 931 SolverVec solvers_; // solvers associated with this context 932 Minimize* mini_; // pointer to set of weak constraints 933 LogPtr progress_; // event handler or 0 if not used 934 Literal step_; // literal for tagging enumeration/step constraints 935 uint32 lastTopLevel_; // size of master's top-level after last init 936 struct Share { // Additional data 937 uint32 count :10; // max number of objects sharing this object 938 uint32 winner :10; // id of solver that terminated the search 939 uint32 shareM : 3; // physical sharing mode 940 uint32 shortM : 1; // short clause mode 941 uint32 solveM : 1; // solve mode 942 uint32 frozen : 1; // is adding of problem constraints allowed? 943 uint32 seed : 1; // set seed of new solvers 944 uint32 satPreM : 2; // preprocessing mode 945 uint32 report : 2; // report mode 946 uint32 reserved: 1; ShareShare947 Share() : count(1), winner(0), shareM((uint32)ContextParams::share_auto), shortM(0), solveM(0), frozen(0), seed(0), satPreM(0), report(0) {} 948 } share_; 949 }; 950 //@} 951 } 952 #endif 953