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, 
        create_only_btb  =64u, 
        create_only_bfb  =128u,
    };
    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, uint32 act = 3u);
    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_     : 27; // 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?
    uint32   watched_:  2; // which constraint is watched (3 both, 2 ignore, FTB_BFB, FFB_BTB)
    weight_t bound_[2];    // FFB_BTB: (sumW-bound)+1 / FTB_BFB: bound
    UndoInfo undo_[0];     // undo stack + seen flag for each literal
};
}

#endif