solve_algorithms.h

Go to the documentation of this file.

// 
// Copyright (c) 2006-2012, 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_SOLVE_ALGORITHMS_H_INCLUDED
#define CLASP_SOLVE_ALGORITHMS_H_INCLUDED

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

#include <clasp/solver_strategies.h>
namespace Clasp {

struct SolveLimits {
        explicit SolveLimits(uint64 conf = UINT64_MAX, uint64 r = UINT64_MAX) 
                : conflicts(conf)
                , restarts(r) {
        }
        bool   reached() const { return conflicts == 0 || restarts == 0; }
        uint64 conflicts; 
        uint64 restarts;  
};

// Basic solving
class BasicSolve {
public:

        BasicSolve(Solver& s, const SolveParams& p, SolveLimits* lim = 0);
        BasicSolve(Solver& s, SolveLimits* lim = 0);
        ~BasicSolve();
        

        bool     assume(const LitVec& assumptions);


        ValueRep solve();

        bool     satisfiable(const LitVec& assumptions, bool init);

        void     reset(bool reinit = false);
        void     reset(Solver& s, const SolveParams& p, SolveLimits* lim = 0);
        Solver&  solver() { return *solver_; }
private:
        BasicSolve(const BasicSolve&);
        BasicSolve& operator=(const BasicSolve&);
        typedef const SolveParams Params;
        typedef SolveLimits       Limits;
        struct State;
        Solver* solver_; // active solver
        Params* params_; // active solving options
        Limits* limits_; // active solving limits
        State*  state_;  // internal solving state
};

struct BasicSolveEvent : SolveEvent<BasicSolveEvent> {
        enum EventOp { event_none = 0, event_deletion = 'D', event_exit = 'E', event_grow = 'G', event_restart = 'R' };
        BasicSolveEvent(const Solver& s, EventOp a_op, uint64 cLim, uint32 lLim) : SolveEvent<BasicSolveEvent>(s, verbosity_max), cLimit(cLim), lLimit(lLim) {
                op = a_op;
        }
        uint64 cLimit; // next conflict limit
        uint32 lLimit; // next learnt limit
};
// General solve
class Enumerator;

class SolveAlgorithm {
public:
        explicit SolveAlgorithm(Enumerator* enumerator = 0, const SolveLimits& limit = SolveLimits());
        virtual ~SolveAlgorithm();
        
        const Enumerator*   enumerator() const { return enum_; }
        const SolveLimits&  limits()     const { return limits_; }
        virtual bool        interrupted()const = 0;

        void setEnumerator(Enumerator& e)      { enum_     = &e; }
        void setEnumLimit(uint64 m)            { enumLimit_= m;  }
        void setLimits(const SolveLimits& x)   { limits_   = x;  }


        bool solve(SharedContext& ctx, const LitVec& assume = LitVec(), EventHandler* modelHandler = 0);
        

        virtual void resetSolve()        = 0;
        
        virtual void enableInterrupts()  = 0;
        

        bool         interrupt();
protected:
        SolveAlgorithm(const SolveAlgorithm&);
        SolveAlgorithm& operator=(const SolveAlgorithm&);
        virtual bool  doSolve(SharedContext& ctx, const LitVec& assume) = 0;
        virtual bool  doInterrupt()                                     = 0;
        bool          reportModel(Solver& s) const;
        Enumerator&   enumerator() { return *enum_;  }
private:
        SolveLimits   limits_;
        Enumerator*   enum_;
        EventHandler* onModel_;
        uint64        enumLimit_;
};

class SequentialSolve : public SolveAlgorithm {
public:
        explicit SequentialSolve(Enumerator* enumerator = 0, const SolveLimits& limit = SolveLimits());
        ~SequentialSolve();
        virtual bool interrupted() const;
        virtual void resetSolve();
        virtual void enableInterrupts();
protected:
        virtual bool doSolve(SharedContext& ctx, const LitVec& assume);
        virtual bool doInterrupt();
private:
        struct InterruptHandler;
        InterruptHandler* term_;
};

struct BasicSolveOptions {
        SolveLimits     limit;  
        SolveAlgorithm* createSolveObject() const { return new SequentialSolve(0, limit); }
        static uint32   supportedSolvers()        { return 1; }
        static uint32   recommendedSolvers()      { return 1; }
        uint32          numSolver() const         { return 1; }
        bool            defaultPortfolio() const  { return false; }
};

}
#endif