weight_constraint.h
Go to the documentation of this file.
00001 // 
00002 // Copyright (c) 2006-2011, Benjamin Kaufmann
00003 // 
00004 // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/ 
00005 // 
00006 // Clasp is free software; you can redistribute it and/or modify
00007 // it under the terms of the GNU General Public License as published by
00008 // the Free Software Foundation; either version 2 of the License, or
00009 // (at your option) any later version.
00010 // 
00011 // Clasp is distributed in the hope that it will be useful,
00012 // but WITHOUT ANY WARRANTY; without even the implied warranty of
00013 // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
00014 // GNU General Public License for more details.
00015 // 
00016 // You should have received a copy of the GNU General Public License
00017 // along with Clasp; if not, write to the Free Software
00018 // Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA
00019 //
00020 #ifndef CLASP_SMODELS_CONSTRAINTS_H_INCLUDED
00021 #define CLASP_SMODELS_CONSTRAINTS_H_INCLUDED
00022 
00023 #ifdef _MSC_VER
00024 #pragma warning (disable : 4200) // nonstandard extension used : zero-sized array
00025 #pragma once
00026 #endif
00027 
00028 #include <clasp/constraint.h>
00029 
00030 namespace Clasp {
00031 
00033 struct WeightLitsRep {
00035 
00041         static WeightLitsRep create(Solver& s, WeightLitVec& lits, weight_t bound);
00043 
00048         bool propagate(Solver& s, Literal W);
00049         bool sat()        const { return bound <= 0; }
00050         bool unsat()      const { return reach < bound; }
00051         bool open()       const { return bound > 0 && bound <= reach;}
00052         bool hasWeights() const { return size && lits[0].second > 1;  }
00053         WeightLiteral* lits;  
00054         uint32         size;  
00055         weight_t       bound; 
00056         weight_t       reach; 
00057 };
00058 
00060 
00078 class WeightConstraint : public Constraint {
00079 public:
00080         enum CreationFlags {
00081                 create_explicit  = 1u, 
00082                 create_no_add    = 3u, 
00083                 create_sat       = 4u, 
00084                 create_no_freeze = 8u, 
00085                 create_no_share  =16u, 
00086                 create_eq_bound  =32u, 
00087         };
00088         class CPair {
00089         public:
00090                 CPair() { con[0] = con[1] = 0; }
00091                 bool              ok()    const { return con[0] != (WeightConstraint*)0x1 && con[1] != (WeightConstraint*)0x1; }
00092                 WeightConstraint* first() const { return con[0]; }
00093                 WeightConstraint* second()const { return con[1]; }
00094         private:
00095                 friend class WeightConstraint;
00096                 WeightConstraint* con[2];
00097         };
00099 
00112         static CPair create(Solver& s, Literal W, WeightLitVec& lits, weight_t bound, uint32 creationFlags = 0);
00113         static CPair create(Solver& s, Literal W, WeightLitsRep rep , uint32 creationFlags);
00114         // constraint interface
00115         Constraint* cloneAttach(Solver&);
00116         bool simplify(Solver& s, bool = false);
00117         void destroy(Solver*, bool);
00118         PropResult propagate(Solver& s, Literal p, uint32& data);
00119         void reason(Solver&, Literal p, LitVec& lits);
00120         bool minimize(Solver& s, Literal p, CCMinRecursive* r);
00121         void undoLevel(Solver& s);
00122         uint32 estimateComplexity(const Solver& s) const;
00129         enum ActiveConstraint {
00130                 FFB_BTB   = 0, 
00131                 FTB_BFB   = 1, 
00132         };
00138         Literal  lit(uint32 i, ActiveConstraint c) const { return Literal::fromIndex( lits_->lit(i).index() ^ c ); }
00140         weight_t weight(uint32 i)                  const { return lits_->weight(i); }
00142         uint32   size()                            const { return lits_->size();    }
00144         bool     isWeight()                        const { return lits_->weights(); }
00145         // Returns the index of next literal to look at during backward propagation.
00146         uint32   getBpIndex()                      const { return !isWeight() ? 1 : undo_[0].data>>1; }
00147 private:
00148         static WeightConstraint* createImpl(Solver& s, Literal W, WeightLitsRep& rep, uint32 flags);
00149         bool                     integrateRoot(Solver& s);
00150         struct WL {
00151                 WL(uint32 s, bool shared, bool w);
00152                 bool     shareable()      const { return rc != 0; }
00153                 bool     unique()         const { return rc == 0 || refCount() == 1; }
00154                 bool     weights()        const { return w != 0; }
00155                 uint32   size()           const { return sz; }
00156                 Literal  lit(uint32 i)    const { return lits[(i<<w)]; }
00157                 Var      var(uint32 i)    const { return lits[(i<<w)].var(); }
00158                 weight_t weight(uint32 i) const { return !weights() ? weight_t(1) : (weight_t)lits[(i<<1)+1].asUint(); }
00159                 uint32   refCount()       const;
00160                 WL*      clone();
00161                 void     release();
00162                 uint8*   address();
00163                 uint32  sz : 30; // number of literals
00164                 uint32  rc : 1;  // ref counted?
00165                 uint32  w  : 1;  // has weights?
00166                 Literal lits[0]; // Literals of constraint: ~B [Bw], l1 [w1], ..., ln-1 [Wn-1]
00167         };
00168         WeightConstraint(Solver& s, SharedContext* ctx, Literal W, const WeightLitsRep& , WL* out);
00169         WeightConstraint(Solver& s, const WeightConstraint& other);
00170         ~WeightConstraint();
00171         
00172         static const uint32 NOT_ACTIVE = 3u;
00173         
00174         // Represents a literal on the undo stack.
00175         // idx()        returns the index of the literal.
00176         // constraint() returns the constraint that added the literal to the undo stack.
00177         // Note: Only 31-bits are used for undo info.
00178         // The remaining bit is used as a flag for marking processed literals.
00179         struct UndoInfo {
00180                 explicit UndoInfo(uint32 d = 0) : data(d) {}
00181                 uint32           idx()        const { return data >> 2; }
00182                 ActiveConstraint constraint() const { return static_cast<ActiveConstraint>((data&2) != 0); }
00183                 uint32 data; 
00184         };
00185         // Is literal idx contained as reason lit in the undo stack?
00186         bool litSeen(uint32 idx) const { return (undo_[idx].data & 1) != 0; }
00187         // Mark/unmark literal idx.
00188         void toggleLitSeen(uint32 idx) { undo_[idx].data ^= 1; }
00189         // Add watch for idx'th literal of c to the solver.
00190         void addWatch(Solver& s, uint32 idx, ActiveConstraint c);
00191         // Updates bound_[c] and adds an undo watch to the solver if necessary.
00192         // Then adds the literal at position idx to the reason set (and the undo stack).
00193         void updateConstraint(Solver& s, uint32 idx, ActiveConstraint c);
00194         // Returns the starting index of the undo stack.
00195         uint32   undoStart()       const { return isWeight(); }
00196         UndoInfo undoTop()         const { assert(up_ != undoStart()); return undo_[up_-1]; }
00197         // Returns the decision level of the last assigned literal
00198         // or 0 if no literal was assigned yet.
00199         uint32   highestUndoLevel(Solver&) const;
00200         void     setBpIndex(uint32 n);
00201         WL*      lits_;        // literals of constraint
00202         uint32   up_     : 29; // undo position; [undoStart(), up_] is the undo stack
00203         uint32   ownsLit_:  1; // owns lits_?
00204         uint32   active_ :  2; // which of the two sub-constraints is currently unit?
00205         weight_t bound_[2];    // FFB_BTB: (sumW-bound)+1 / FTB_BFB: bound
00206         UndoInfo undo_[0];     // undo stack + seen flag for each literal
00207 };
00208 }
00209 
00210 #endif


clasp
Author(s): Benjamin Kaufmann
autogenerated on Thu Aug 27 2015 12:41:40