program_builder.h

Go to the documentation of this file.

// 
// Copyright (c) 2006, 2007, 2012, 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_PROGRAM_BUILDER_H_INCLUDED
#define CLASP_PROGRAM_BUILDER_H_INCLUDED

#ifdef _MSC_VER
#pragma once
#endif

#include <clasp/literal.h>
#include <clasp/claspfwd.h>
#include <clasp/util/misc_types.h>
#include <map>
#include <iosfwd>

namespace Clasp {


class ProgramBuilder {
public:
        typedef SharedMinimizeData SharedMinimize;
        typedef SingleOwnerPtr<SharedMinimize, ReleaseObject> MinPtr;
        ProgramBuilder();
        virtual ~ProgramBuilder();

        bool startProgram(SharedContext& ctx);
        bool parseProgram(StreamSource& prg);
        bool parseProgram(std::istream& prg);
        bool updateProgram();
        bool endProgram();

        void             getAssumptions(LitVec& out) const;

        SharedMinimize*  getMinimizeConstraint(SumVec* softBound = 0) const;
        void             disposeMinimizeConstraint();
        int              type()   const { return doType(); }
        bool             frozen() const { return frozen_; }
        virtual bool     ok()     const;
        SharedContext*   ctx()    const { return ctx_; }
protected:
        void addMinLit(WeightLiteral x);
        void addMinRule(const WeightLitVec& lits);
        void disposeMin();
        void setFrozen(bool frozen)  { frozen_ = frozen; }
        void setCtx(SharedContext* x){ ctx_    = x; }
private:
        typedef SingleOwnerPtr<MinimizeBuilder> MinBuildPtr;
        ProgramBuilder(const ProgramBuilder&);
        ProgramBuilder& operator=(ProgramBuilder&);
        virtual void getMinBound(SumVec& out)      const;
        virtual bool doStartProgram()                    = 0;
        virtual bool doUpdateProgram()                   = 0;
        virtual bool doEndProgram()                      = 0;
        virtual void doGetAssumptions(LitVec& out) const = 0;
        virtual int  doType() const                      = 0;
        virtual bool doParse(StreamSource& prg)          = 0;
        SharedContext*      ctx_;
        mutable MinBuildPtr min_;
        mutable MinPtr      minCon_;
        bool                frozen_;
};

class SatBuilder : public ProgramBuilder {
public:
        explicit SatBuilder(bool maxSat = false);
        // program definition
        

        void prepareProblem(uint32 numVars, wsum_t hardClauseWeight = 0, uint32 clauseHint = 100);
        Var numVars() const { return vars_; }

        bool addClause(LitVec& clause, wsum_t cw = 0);
private:
        typedef PodVector<uint8>::type VarState;
        bool doStartProgram();
        bool doParse(StreamSource& prg);
        int  doType() const                   { return Problem_t::SAT; }
        bool doUpdateProgram()                { return !frozen(); }
        void doGetAssumptions(LitVec&) const  { }
        bool doEndProgram();
        bool satisfied(LitVec& clause);
        bool markAssigned();
        void markLit(Literal x) { varState_[x.var()] |= 1 + x.sign(); }
        VarState varState_;
        LitVec   softClauses_;
        wsum_t   hardWeight_;
        Var      vars_;
        uint32   pos_;
        bool     maxSat_;
};

class PBBuilder : public ProgramBuilder {
public:
        PBBuilder();
        // program definition

        void    prepareProblem(uint32 numVars, uint32 maxProduct, uint32 maxSoft, uint32 constraintHint = 100);
        uint32  numVars() const { return nextVar_; }

        bool    addConstraint(WeightLitVec& lits, weight_t bound, bool eq = false, weight_t cw = 0);

        Literal addProduct(LitVec& lits);
        bool    addObjective(const WeightLitVec& min);
        bool    setSoftBound(wsum_t bound);
private:
        typedef std::map<LitVec, Literal> ProductIndex;
        bool doStartProgram();
        void getMinBound(SumVec& out) const;
        int  doType() const                   { return Problem_t::PB; }
        bool doUpdateProgram()                { return !frozen(); }
        void doGetAssumptions(LitVec&) const  { }
        bool doParse(StreamSource& prg);
        bool doEndProgram();
        bool productSubsumed(LitVec& lits, Literal& subLit);
        void addProductConstraints(Literal eqLit, LitVec& lits);
        Var  getNextVar();
        ProductIndex products_;
        uint32       nextVar_;
        uint32       maxVar_;
        wsum_t       soft_;
};
}
#endif