weight_constraint.h

Go to the documentation of this file.

// 
// Copyright (c) 2006-2011, Benjamin Kaufmann
// 
// This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/ 
// 
// Clasp is free software; you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
// 
// Clasp is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
// 
// You should have received a copy of the GNU General Public License
// along with Clasp; if not, write to the Free Software
// Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA
//
#ifndef CLASP_SMODELS_CONSTRAINTS_H_INCLUDED
#define CLASP_SMODELS_CONSTRAINTS_H_INCLUDED

#ifdef _MSC_VER
#pragma warning (disable : 4200) // nonstandard extension used : zero-sized array
#pragma once
#endif

#include <clasp/constraint.h>

namespace Clasp {

struct WeightLitsRep {

        static WeightLitsRep create(Solver& s, WeightLitVec& lits, weight_t bound);

        bool propagate(Solver& s, Literal W);
        bool sat()        const { return bound <= 0; }
        bool unsat()      const { return reach < bound; }
        bool open()       const { return bound > 0 && bound <= reach;}
        bool hasWeights() const { return size && lits[0].second > 1;  }
        WeightLiteral* lits;  
        uint32         size;  
        weight_t       bound; 
        weight_t       reach; 
};


class WeightConstraint : public Constraint {
public:
        enum CreationFlags {
                create_explicit  = 1u, 
                create_no_add    = 3u, 
                create_sat       = 4u, 
                create_no_freeze = 8u, 
                create_no_share  =16u, 
                create_eq_bound  =32u, 
        };
        class CPair {
        public:
                CPair() { con[0] = con[1] = 0; }
                bool              ok()    const { return con[0] != (WeightConstraint*)0x1 && con[1] != (WeightConstraint*)0x1; }
                WeightConstraint* first() const { return con[0]; }
                WeightConstraint* second()const { return con[1]; }
        private:
                friend class WeightConstraint;
                WeightConstraint* con[2];
        };

        static CPair create(Solver& s, Literal W, WeightLitVec& lits, weight_t bound, uint32 creationFlags = 0);
        static CPair create(Solver& s, Literal W, WeightLitsRep rep , uint32 creationFlags);
        // constraint interface
        Constraint* cloneAttach(Solver&);
        bool simplify(Solver& s, bool = false);
        void destroy(Solver*, bool);
        PropResult propagate(Solver& s, Literal p, uint32& data);
        void reason(Solver&, Literal p, LitVec& lits);
        bool minimize(Solver& s, Literal p, CCMinRecursive* r);
        void undoLevel(Solver& s);
        uint32 estimateComplexity(const Solver& s) const;
        enum ActiveConstraint {
                FFB_BTB   = 0, 
                FTB_BFB   = 1, 
        };
        Literal  lit(uint32 i, ActiveConstraint c) const { return Literal::fromIndex( lits_->lit(i).index() ^ c ); }
        weight_t weight(uint32 i)                  const { return lits_->weight(i); }
        uint32   size()                            const { return lits_->size();    }
        bool     isWeight()                        const { return lits_->weights(); }
        // Returns the index of next literal to look at during backward propagation.
        uint32   getBpIndex()                      const { return !isWeight() ? 1 : undo_[0].data>>1; }
private:
        static WeightConstraint* createImpl(Solver& s, Literal W, WeightLitsRep& rep, uint32 flags);
        bool                     integrateRoot(Solver& s);
        struct WL {
                WL(uint32 s, bool shared, bool w);
                bool     shareable()      const { return rc != 0; }
                bool     unique()         const { return rc == 0 || refCount() == 1; }
                bool     weights()        const { return w != 0; }
                uint32   size()           const { return sz; }
                Literal  lit(uint32 i)    const { return lits[(i<<w)]; }
                Var      var(uint32 i)    const { return lits[(i<<w)].var(); }
                weight_t weight(uint32 i) const { return !weights() ? weight_t(1) : (weight_t)lits[(i<<1)+1].asUint(); }
                uint32   refCount()       const;
                WL*      clone();
                void     release();
                uint8*   address();
                uint32  sz : 30; // number of literals
                uint32  rc : 1;  // ref counted?
                uint32  w  : 1;  // has weights?
                Literal lits[0]; // Literals of constraint: ~B [Bw], l1 [w1], ..., ln-1 [Wn-1]
        };
        WeightConstraint(Solver& s, SharedContext* ctx, Literal W, const WeightLitsRep& , WL* out);
        WeightConstraint(Solver& s, const WeightConstraint& other);
        ~WeightConstraint();
        
        static const uint32 NOT_ACTIVE = 3u;
        
        // Represents a literal on the undo stack.
        // idx()        returns the index of the literal.
        // constraint() returns the constraint that added the literal to the undo stack.
        // Note: Only 31-bits are used for undo info.
        // The remaining bit is used as a flag for marking processed literals.
        struct UndoInfo {
                explicit UndoInfo(uint32 d = 0) : data(d) {}
                uint32           idx()        const { return data >> 2; }
                ActiveConstraint constraint() const { return static_cast<ActiveConstraint>((data&2) != 0); }
                uint32 data; 
        };
        // Is literal idx contained as reason lit in the undo stack?
        bool litSeen(uint32 idx) const { return (undo_[idx].data & 1) != 0; }
        // Mark/unmark literal idx.
        void toggleLitSeen(uint32 idx) { undo_[idx].data ^= 1; }
        // Add watch for idx'th literal of c to the solver.
        void addWatch(Solver& s, uint32 idx, ActiveConstraint c);
        // Updates bound_[c] and adds an undo watch to the solver if necessary.
        // Then adds the literal at position idx to the reason set (and the undo stack).
        void updateConstraint(Solver& s, uint32 idx, ActiveConstraint c);
        // Returns the starting index of the undo stack.
        uint32   undoStart()       const { return isWeight(); }
        UndoInfo undoTop()         const { assert(up_ != undoStart()); return undo_[up_-1]; }
        // Returns the decision level of the last assigned literal
        // or 0 if no literal was assigned yet.
        uint32   highestUndoLevel(Solver&) const;
        void     setBpIndex(uint32 n);
        WL*      lits_;        // literals of constraint
        uint32   up_     : 29; // undo position; [undoStart(), up_] is the undo stack
        uint32   ownsLit_:  1; // owns lits_?
        uint32   active_ :  2; // which of the two sub-constraints is currently unit?
        weight_t bound_[2];    // FFB_BTB: (sumW-bound)+1 / FTB_BFB: bound
        UndoInfo undo_[0];     // undo stack + seen flag for each literal
};
}

#endif