enumerator.h

Go to the documentation of this file.

// 
// Copyright (c) 2006-2013, 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_ENUMERATOR_H_INCLUDED
#define CLASP_ENUMERATOR_H_INCLUDED

#ifdef _MSC_VER
#pragma once
#endif
#include <clasp/literal.h>
#include <clasp/constraint.h>
#include <clasp/minimize_constraint.h>
#include <clasp/util/misc_types.h>

namespace Clasp { 
class Solver;
class SharedContext;
class Enumerator;
class EnumerationConstraint;

struct Model {
        enum Type { model_sat = 0, model_cons = 1, max_value = 1 };
        bool     consequences()    const { return (type & model_cons) != 0; }
        ValueRep value(Var v)      const { assert(values && v < values->size()); return (*values)[v]; }
        bool     isTrue(Literal p) const { return (value(p.var()) & trueValue(p)) != 0; }
        uint64                    num;    // running number of this model
        const ValueVec*           values; // variable assignment or consequences
        const SharedMinimizeData* costs;  // associated costs (or 0)
        uint32                    sId :16;// id of solver that found the model
        uint32                    type:14;// type of model
        uint32                    opt : 1;// whether the model is optimal w.r.t costs (0: unknown)
        uint32                    sym : 1;// whether symmetric models are possible
};


struct EnumOptions {  
        typedef MinimizeMode OptMode;
        enum EnumType { enum_auto = 0, enum_bt  = 1, enum_record  = 2, enum_consequences = 4, enum_brave = 5, enum_cautious = 6 };
        EnumOptions() : numModels(-1), type(enum_auto), opt(MinimizeMode_t::optimize), project(0), maxSat(false) {}
        static Enumerator* createModelEnumerator(const EnumOptions& opts);
        static Enumerator* createConsEnumerator(const EnumOptions& opts);
        static Enumerator* nullEnumerator();
        
        Enumerator* createEnumerator() const;
        bool        consequences()     const { return (type & enum_consequences) != 0; }
        bool        optimize()         const { return ((opt  & MinimizeMode_t::optimize) != 0); }
        int      numModels; 
        EnumType type;      
        OptMode  opt;       
        uint32   project;   
        SumVec   bound;     
        bool     maxSat;    
};



class Enumerator {
public:
        typedef EnumerationConstraint*       ConPtr;
        typedef const EnumerationConstraint* ConPtrConst;
        typedef const SharedMinimizeData*    Minimizer;
        typedef EnumOptions::OptMode         OptMode;
        explicit Enumerator();
        virtual ~Enumerator();

        void   reset();


        int    init(SharedContext& problem, SharedMinimizeData* min = 0, int limit = 0);
        

        bool   start(Solver& s, const LitVec& path = LitVec(), bool disjointPath = false)  const;
        

        bool   update(Solver& s)  const;
        

        bool   commitModel(Solver& s);
        bool   commitSymmetric(Solver& s);

        bool   commitUnsat(Solver& s);

        bool   commitComplete();

        uint8  commit(Solver& s);
        void   end(Solver& s) const;
        uint64 enumerated()   const { return model_.num; }

        const Model& lastModel()        const { return model_; }
        bool         optimize()         const { return mini_ && mini_->mode() != MinimizeMode_t::enumerate && model_.opt == 0; }
        bool         tentative()        const { return mini_ && mini_->mode() == MinimizeMode_t::enumOpt && model_.opt == 0; }
        virtual int  modelType()        const { return Model::model_sat; }
        virtual bool supportsRestarts() const { return true; }
        virtual bool supportsParallel() const { return true; }
        virtual bool exhaustive()       const { return mini_ && mini_->mode() != MinimizeMode_t::enumerate; }
        void         setDisjoint(Solver& s, bool b) const;
        void         setIgnoreSymmetric(bool b);
        Minimizer    minimizer()                    const { return mini_; }
protected:

        virtual ConPtr doInit(SharedContext& ctx, MinimizeConstraint* m, int numModels) = 0;
        virtual void   doReset();
        ConPtr         constraint(const Solver& s) const;
private:
        Enumerator(const Enumerator&);
        Enumerator& operator=(const Enumerator&);
        SharedMinimizeData* mini_;
        Model               model_;
};


class EnumerationConstraint : public Constraint {
public:
        typedef EnumerationConstraint* ConPtr;
        typedef MinimizeConstraint*    MinPtr;
        bool     disjointPath()const { return (flags_ & flag_path_disjoint) != 0u; }
        ValueRep state()       const { return static_cast<ValueRep>(flags_ & 3u); }
        bool     optimize()    const;
        MinPtr   minimizer()   const { return mini_; }
        
        // Methods used by enumerator
        bool start(Solver& s, const LitVec& path, bool disjoint);
        void end(Solver& s);
        bool update(Solver& s);
        void setDisjoint(bool x);
        bool integrateBound(Solver& s) const;
        bool commitModel(Enumerator& ctx, Solver& s);
        bool commitUnsat(Enumerator& ctx, Solver& s);
        void setMinimizer(MinPtr min) { mini_ = min; }
protected:
        EnumerationConstraint(Solver& s, MinimizeConstraint* min);
        virtual ~EnumerationConstraint();
        // base interface
        virtual void        destroy(Solver* s, bool detach);
        virtual PropResult  propagate(Solver&, Literal, uint32&) { return PropResult(true, true); }
        virtual void        reason(Solver&, Literal, LitVec&)    {}
        virtual bool        simplify(Solver& s, bool reinit);
        virtual bool        valid(Solver& s);
        // own interface
        virtual bool        doUpdate(Solver& s) = 0;
        virtual void        doCommitModel(Enumerator&, Solver&) {}
        MinimizeConstraint* cloneMinimizer(Solver& s) const;
private:
        enum Flag { flag_path_disjoint = 4u };
        enum { clear_state_mask = ~uint32(value_true|value_false) };
        MinimizeConstraint* mini_;
        LitVec              next_;
        uint32              flags_ : 4;
        uint32              root_  : 28;
};
}

#endif