logic_program.h

Go to the documentation of this file.

// 
// Copyright (c) 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_LOGIC_PROGRAM_H_INCLUDED
#define CLASP_LOGIC_PROGRAM_H_INCLUDED

#ifdef _MSC_VER
#pragma once
#endif

#include <clasp/logic_program_types.h>
#include <clasp/program_builder.h>
#include <clasp/util/misc_types.h>
#include <map>

namespace Clasp { namespace Asp {
class LpStats {
public:
        typedef std::pair<uint32, uint32> RPair;
        LpStats() { reset(); }
        void   reset();
        uint32 eqs()             const { return eqs(Var_t::atom_var) + eqs(Var_t::body_var) + eqs(Var_t::atom_body_var); }
        uint32 eqs(VarType t)    const { return eqs_[t-1]; }
        uint32 rules()           const;
        RPair  rules(RuleType t) const { return rules_[ruleIndex(t)]; }
        RPair& rules(RuleType t)       { return rules_[ruleIndex(t)]; }
        bool   tr()              const { return rules_[0].first != rules_[0].second; }
        void   incEqs(VarType t)       { ++eqs_[t-1]; }
        void   upRule(RuleType t,  int32 i) { RPair& x = rules_[ruleIndex(t)]; x.first += i; x.second += i; }
        void   trRule(RuleType t, uint32 i) { --rules_[ruleIndex(t)].second; rules_[0].first -= i; }
        void   accu(const LpStats& o);
        double operator[](const char* key) const;
        static const char* keys(const char* path); 
        uint32 bodies;          
        uint32 atoms;           
        uint32 auxAtoms;        
        uint32 sccs;            
        uint32 nonHcfs;         
        uint32 gammas;          
        uint32 ufsNodes;        
private:
        uint32 eqs_[3];         
        RPair  rules_[NUM_RULE_TYPES]; 
};
class RedefinitionError : public std::logic_error {
public:
        explicit RedefinitionError(unsigned atomId, const char* atomName = "");
        unsigned atom() const { return atomId_; }
private:
        unsigned atomId_;
};


class LogicProgram : public ProgramBuilder {
public:
        LogicProgram();
        ~LogicProgram();
        enum ExtendedRuleMode {
                mode_native           = 0, 
                mode_transform        = 1, 
                mode_transform_choice = 2, 
                mode_transform_card   = 3, 
                mode_transform_weight = 4, 
                mode_transform_scc    = 5, 
                mode_transform_nhcf   = 6, 
                mode_transform_integ  = 7, 
                mode_transform_dynamic= 8  
        };

        struct AspOptions {
                static const uint32 MAX_EQ_ITERS = static_cast<uint32>( (1u<<26)-1 );
                AspOptions() : erMode(mode_native), iters(5), noSCC(0), dfOrder(0), backprop(0), normalize(0), suppMod(0), noGamma(0) {}
                AspOptions& iterations(uint32 it)   { iters   = it;return *this;}
                AspOptions& depthFirst()            { dfOrder = 1; return *this;}
                AspOptions& backpropagate()         { backprop= 1; return *this;}
                AspOptions& noScc()                 { noSCC   = 1; return *this;}
                AspOptions& noEq()                  { iters   = 0; return *this;}
                AspOptions& disableGamma()          { noGamma = 1; return *this;}
                AspOptions& ext(ExtendedRuleMode m) { erMode = m;  return *this;}
                AspOptions& supportedModels()       { suppMod = 1; noEq(); return noScc(); }
                ExtendedRuleMode erMode;       
                uint32           iters    : 26;
                uint32           noSCC    :  1;
                uint32           dfOrder  :  1;
                uint32           backprop :  1;
                uint32           normalize:  1;
                uint32           suppMod  :  1;
                uint32           noGamma  :  1;
        };
        
        LogicProgram& start(SharedContext& ctx, const AspOptions& opts = AspOptions()) {
                startProgram(ctx);
                setOptions(opts);
                return *this;
        }
        void setExtendedRuleMode(ExtendedRuleMode m) { opts_.ext(m); }
        void setOptions(const AspOptions& opts);
        void setNonHcfConfiguration(Configuration* c){ nonHcfCfg_ = c; }
        

        bool update() { return updateProgram(); }


        bool end() { return endProgram(); }

        void write(std::ostream& os);
        

        void dispose(bool forceFullDispose);

        /*
         * \pre The program is currently frozen.
         */
        bool clone(SharedContext& ctx, bool shareSymbols = false);




        Var newAtom();


        LogicProgram& setAtomName(Var atomId, const char* name);


        LogicProgram& setCompute(Var atomId, bool value);


        LogicProgram& freeze(Var atomId, ValueRep value = value_false);


        LogicProgram& unfreeze(Var atomId);


        LogicProgram& addRule(const Rule& r);
        



        LogicProgram& startRule(RuleType t = BASICRULE, weight_t bound = -1) {
                rule_.clear();
                rule_.setType(t);
                if ((t == CONSTRAINTRULE || t == WEIGHTRULE) && bound > 0) {
                        rule_.setBound(bound);
                }
                return *this;
        }


        LogicProgram& setBound(weight_t bound) { // only valid for CONSTRAINT and WEIGHTRULES
                rule_.setBound(bound);
                return *this;
        }

        LogicProgram& addHead(Var atomId) {
                assert(atomId > 0);
                rule_.addHead(atomId);
                return *this;
        }
        

        LogicProgram& addToBody(Var atomId, bool pos, weight_t weight = 1) {
                rule_.addToBody(atomId, pos, weight);
                return *this;
        }
        

        LogicProgram& endRule() {
                return addRule(rule_);
        }
        


        bool   hasMinimize()     const { return minimize_ != 0; }
        uint32 numAtoms()        const { return (uint32)atoms_.size()-1; }
        uint32 numBodies()       const { return (uint32)bodies_.size(); }
        uint32 numDisjunctions() const { return (uint32)disjunctions_.size(); }
        Var    startAtom()       const { return incData_?incData_->startAtom:1; }

        Literal getLiteral(Var atomId) const;
        LpStats  stats;
        LpStats* accu;

        typedef VarVec::const_iterator                VarIter;
        typedef PrgHead*const*                        HeadIter;
        typedef std::pair<EdgeIterator, EdgeIterator> EdgeRange;
        typedef std::pair<HeadIter, HeadIter>         HeadRange;
        const AspOptions& options()    const { return opts_; }
        bool       hasConflict()       const { return getFalseAtom()->literal() == posLit(0); }
        bool       ok()                const { return !hasConflict() && ProgramBuilder::ok(); }
        PrgAtom*   getAtom(Var atomId) const { return atoms_[atomId]; }
        PrgHead*   getHead(PrgEdge it) const { return it.isAtom() ? (PrgHead*)getAtom(it.node()) : (PrgHead*)getDisj(it.node()); }
        PrgNode*   getSupp(PrgEdge it) const { return it.isBody() ? (PrgNode*)getBody(it.node()) : (PrgNode*)getDisj(it.node()); }
        Var        getEqAtom(Var a)    const { return getEqNode(atoms_, a); }
        PrgBody*   getBody(Var bodyId) const { return bodies_[bodyId]; }
        Var        getEqBody(Var b)    const { return getEqNode(bodies_, b); }
        PrgDisj*   getDisj(Var disjId) const { return disjunctions_[disjId]; }
        bool       isFact(PrgAtom* a)  const { return a->value() == value_true && opts_.noSCC == false; }
        HeadIter   disj_begin()        const { return disjunctions_.empty() ? 0 : reinterpret_cast<HeadIter>(&disjunctions_[0]); }
        HeadIter   disj_end()          const { return disj_begin() + numDisjunctions(); }
        HeadIter   atom_begin()        const { return reinterpret_cast<HeadIter>(&atoms_[0]); }
        HeadIter   atom_end()          const { return atom_begin() + (numAtoms()+1); }
        VarIter    unfreeze_begin()    const { return incData_?incData_->update.begin() : activeHead_.end(); }
        VarIter    unfreeze_end()      const { return incData_?incData_->update.end()   : activeHead_.end(); }
        const char*getAtomName(Var id) const;
        RuleType   simplifyRule(const Rule& r, VarVec& head, BodyInfo& info);
        VarVec&    getSupportedBodies(bool sorted);
        uint32     update(PrgBody* b, uint32 oldHash, uint32 newHash);
        bool       assignValue(PrgAtom* a, ValueRep v);
        bool       assignValue(PrgHead* h, ValueRep v);
        bool       propagate(bool backprop);
        PrgAtom*   mergeEqAtoms(PrgAtom* a, Var rootAtom);
        PrgBody*   mergeEqBodies(PrgBody* b, Var rootBody, bool hashEq, bool atomsAssigned);
        bool       propagate()               { return propagate(options().backprop); }
        void       setConflict()             { getFalseAtom()->setLiteral(posLit(0)); }
        RuleState& ruleState()               { return ruleState_; }
        void       addMinimize();
        // ------------------------------------------------------------------------
        // Statistics
        void      upRules(RuleType r, int i) { stats.upRule(r, i);  }
        void      incTr(RuleType r, uint32 n){ stats.trRule(r, n);  }
        void      incTrAux(uint32 n)         { stats.auxAtoms += n; }
        void      incEqs(VarType t)          { stats.incEqs(t);     }
        // ------------------------------------------------------------------------
private:
        LogicProgram(const LogicProgram&);
        LogicProgram& operator=(const LogicProgram&);   
        typedef PodVector<Rule*>::type RuleList;
        typedef std::multimap<uint32, uint32>   IndexMap; // hash -> vec[offset]
        typedef IndexMap::iterator              IndexIter;
        typedef std::pair<IndexIter, IndexIter> IndexRange;
        typedef PodVector<uint8>::type          SccMap;
        struct MinimizeRule;
        // ------------------------------------------------------------------------
        // virtual overrides
        bool doStartProgram();
        bool doUpdateProgram();
        bool doEndProgram();
        void doGetAssumptions(LitVec& out) const;
        bool doParse(StreamSource& prg);
        int  doType() const { return Problem_t::ASP; }
        // ------------------------------------------------------------------------
        // Program definition
        PrgAtom* resize(Var atomId);
        void     addRuleImpl(RuleType t,    const VarVec& head, BodyInfo& body);
        bool     handleNatively(RuleType t, const BodyInfo& i) const;
        bool     transformNoAux(RuleType t, const BodyInfo& i) const;
        void     transformExtended();
        void     transformIntegrity(uint32 maxAux);
        PrgBody* getBodyFor(BodyInfo& body, bool addDeps = true);
        PrgDisj* getDisjFor(const VarVec& heads, uint32 headHash);
        PrgBody* assignBodyFor(BodyInfo& body, EdgeType x, bool strongSimp);
        uint32   findEqBody(PrgBody* b, uint32 hash);
        uint32   equalBody(const IndexRange& range, BodyInfo& info) const;
        RuleType simplifyBody(const Rule& r, BodyInfo& info);
        uint32   removeBody(PrgBody* b, uint32 oldHash);
        Literal  getEqAtomLit(Literal lit, const BodyList& supports, Preprocessor& p, const SccMap& x);
        bool     positiveLoopSafe(PrgBody* b, PrgBody* root) const;
        void     updateFrozenAtoms();
        void     normalize();
        template <class C>
        Var getEqNode(C& vec, Var id)  const {
                if (!vec[id]->eq()) return id;
                typedef typename C::value_type NodeType;
                NodeType n = vec[id];
                NodeType r;
                Var root   = n->id();
                for (r = vec[root]; r->eq(); r = vec[root]) {
                        // if n == r and r == r' -> n == r'
                        n->setEq(root = r->id());
                }
                return root;
        }
        // ------------------------------------------------------------------------
        // Nogood creation
        void prepareProgram(bool checkSccs);
        void finalizeDisjunctions(Preprocessor& p, uint32 numSccs);
        void prepareComponents();
        void simplifyMinimize();
        bool addConstraints();
        // ------------------------------------------------------------------------
        void writeBody(const BodyInfo& body, std::ostream&) const;
        bool transform(const PrgBody& body, BodyInfo& out)  const;
        void transform(const MinimizeRule&, BodyInfo& out)  const;
        Var      getFalseId()      const { return 0; }
        PrgAtom* getFalseAtom()    const { return atoms_[0]; }
        Var      findLpFalseAtom() const;
        Rule           rule_;        // active rule
        BodyInfo       activeBody_;  // simplified body of active rule
        VarVec         activeHead_;  // simplified head of active rule
        RuleState      ruleState_;   // which atoms appear in the active rule?
        RuleList       extended_;    // extended rules to be translated
        IndexMap       bodyIndex_;   // hash -> body
        IndexMap       disjIndex_;   // hash -> disjunction
        BodyList       bodies_;      // all bodies
        AtomList       atoms_;       // all atoms
        AtomList       sccAtoms_;    // atoms that are strongly connected
        DisjList       disjunctions_;// all (head) disjunctions
        VarVec         initialSupp_; // bodies that are (initially) supported
        VarVec         propQ_;       // assigned atoms
        NonHcfSet      nonHcfs_;     // set of non-hcf sccs
        Configuration* nonHcfCfg_;   // optional configuration second level solvers
        struct MinimizeRule {
                WeightLitVec lits_;
                MinimizeRule* next_;
        }*             minimize_;    // list of minimize-rules
        struct Incremental  {
                Incremental();
                uint32  startAtom;// first atom of current iteration
                uint32  startAux; // first aux atom of current iteration
                uint32  startScc; // first valid scc number in this iteration
                VarVec  frozen;   // list of frozen atoms
                VarVec  update;   // list of atoms to be updated (freeze/unfreeze) in this step
        }*             incData_;// additional state to handle incrementally defined programs 
        AspOptions     opts_;   // preprocessing 
};
} } // end namespace Asp
#endif