dependency_graph.h

Go to the documentation of this file.

// 
// Copyright (c) 2010-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_DEPENDENCY_GRAPH_H_INCLUDED
#define CLASP_DEPENDENCY_GRAPH_H_INCLUDED

#ifdef _MSC_VER
#pragma once
#endif

#include <clasp/logic_program.h>
#include <clasp/solver_strategies.h>
#include <algorithm>
namespace Clasp {
class Solver;
class SharedContext;
class SharedDependencyGraph;
struct SolverStats;
struct SolveTestEvent : SolveEvent<SolveTestEvent> {
        SolveTestEvent(const Solver& s, uint32 scc, bool partial);
        int    result;     // -1: before test, 0: unstable, 1: stable
        uint32 scc     :31;// scc under test
        uint32 partial : 1;// partial test?
        uint64 confDelta;  // conflicts before test
        uint64 choiceDelta;// choices before test
        double time;       // time for test
        
        uint64 conflicts() const;
        uint64 choices()   const;
};


class SharedDependencyGraph {
public:
        SharedDependencyGraph(Configuration* nonHcfCfg = 0);
        ~SharedDependencyGraph();
        typedef uint32            NodeId;
        typedef Asp::PrgNode      PrgNode;
        typedef Asp::PrgBody      PrgBody;
        typedef Asp::PrgAtom      PrgAtom;
        typedef Asp::PrgDisj      PrgDisj;
        typedef Asp::LogicProgram LogicProgram;
        typedef Asp::NonHcfSet    NonHcfSet;
        typedef Asp::AtomList     AtomList;

        class NonHcfComponent {
        public:
                explicit NonHcfComponent(const SharedDependencyGraph& dep, SharedContext& generator, uint32 scc, const VarVec& atoms, const VarVec& bodies);
                ~NonHcfComponent();
                void assumptionsFromAssignment(const Solver& generator, LitVec& assume) const;
                bool test(uint32 scc, const Solver& generator, const LitVec& assumptions, VarVec& unfoundedOut)  const;
                const SharedContext& ctx() const { return *prg_; }
                void update(const SharedContext& generator);
        private:
                friend class SharedDependencyGraph;
                NonHcfComponent(const NonHcfComponent&);
                NonHcfComponent& operator=(const NonHcfComponent&);
                class ComponentMap;
                SharedContext* prg_;
                ComponentMap*  comp_;
        };
        typedef std::pair<uint32, NonHcfComponent*> ComponentPair;
        typedef const ComponentPair* NonHcfIter;
        struct Node {
                Node(Literal l = Literal(0, false), uint32 sc = PrgNode::noScc) 
                        : lit(l), scc(sc), data(0), adj_(0), sep_(0) {}
                Literal lit;       // literal of this node
                uint32  scc   : 28;// scc of this node
                uint32  data  :  4;// additional atom/body data 
                NodeId* adj_;      // list of adjacent nodes
                NodeId* sep_;      // separates successor/predecessor nodes
        };

        struct AtomNode : public Node {
                enum Property { property_in_choice = 1u, property_in_disj = 2u, property_in_ext = 4u, property_in_non_hcf = 8u};
                AtomNode() {}
                void  set(Property p)         { data |= (uint32)p; }
                void  setProperties(uint32 f) { assert(f < 8); data |= f; }
                bool          inChoice()     const { return (data & property_in_choice) != 0; }
                bool          inDisjunctive()const { return (data & property_in_disj) != 0; }
                bool          inExtended()   const { return (data& property_in_ext) != 0; }
                bool          inNonHcf()     const { return (data & property_in_non_hcf) != 0; }
                const NodeId* bodies_begin() const { return adj_; }
                const NodeId* bodies_end()   const { return sep_; }
                NodeId        body(uint32 i) const { return bodies_begin()[i]; }

                const NodeId* succs()        const { return sep_; }
                template <class P>
                void visitSuccessors(const P& p) const {
                        const NodeId* s = succs();
                        for (; *s != idMax; ++s) { p(*s); }
                        if (inExtended()) {
                                for (++s; *s != idMax; s += 2) { p(*s, *(s+1)); }
                        }
                }
        };
        enum { sentinel_atom = 0u };
        

        struct BodyNode : public Node {
                enum Type { type_normal    = 0u, type_count = 1u, type_sum = 3u };
                enum Flag { flag_has_delta = 4u, flag_seen  = 8u };
                explicit BodyNode(PrgBody* b, uint32 scc) : Node(b->literal(), scc) {
                        if (scc == PrgNode::noScc || b->type() == Asp::BodyInfo::NORMAL_BODY) {
                                data = type_normal;
                        }
                        else if (b->type() == Asp::BodyInfo::COUNT_BODY){ data = type_count; }
                        else if (b->type() == Asp::BodyInfo::SUM_BODY)  { data = type_sum;   }
                        else                                            { assert("UNKNOWN BODY TYPE!\n"); }
                }
                bool seen() const { return (data & flag_seen) != 0; }
                void seen(bool b) { if (b) data |= flag_seen; else data &= ~uint32(flag_seen); }
                

                const NodeId* heads_begin() const { return adj_; }
                const NodeId* heads_end()   const { return sep_ - extended(); }
                bool          delta()       const { return (data & flag_has_delta) != 0; }

                const NodeId* preds()       const { assert(scc != PrgNode::noScc); return sep_; }
                uint32        get_pred_idx(NodeId atomId) const { 
                        const uint32 inc = pred_inc();
                              uint32 idx = 0;
                        for (const NodeId* x = preds(); *x != idMax; x += inc, ++idx) {
                                if (*x == atomId) return idx;
                        }
                        return idMax;
                }
                NodeId        get_pred(uint32 idx) const { return *(preds() + (idx*pred_inc())); }
                uint32        pred_inc()           const { return 1 + sum(); }

                uint32        pred_weight(uint32 i, bool ext) const { 
                        return !sum()
                                ? 1 
                                : *(preds() + (i*pred_inc()) + (1+ext));
                }
                uint32        num_preds() const {
                        if (scc == PrgNode::noScc) return 0;
                        uint32 p        = 0;
                        const NodeId* x = preds();
                        const uint32 inc= pred_inc();
                        for (; *x != idMax; x += inc) { ++p; }
                        x += extended();
                        for (; *x != idMax; x += inc) { ++p; }
                        return p;
                }
                bool          extended()const { return (data & type_count) != 0; }
                bool          sum()     const { return (data & type_sum) == type_sum; }
                weight_t      ext_bound() const { return sep_[-1]; }
        };

        void addSccs(LogicProgram& prg, const AtomList& sccAtoms, const NonHcfSet& nonHcfs);

        uint32 numAtoms() const { return (uint32)atoms_.size();  }
        uint32 numBodies()const { return (uint32)bodies_.size(); }
        uint32 nodes()    const { return numAtoms()+numBodies(); }

        const AtomNode& getAtom(NodeId atomId) const {
                assert(atomId < atoms_.size());
                return atoms_[atomId];
        }
        NodeId id(const AtomNode& n) const { return static_cast<uint32>(&n - &atoms_[0]); }
        const BodyNode& getBody(NodeId bodyId) const {
                assert(bodyId < bodies_.size());
                return bodies_[bodyId];
        }
        template <class P>
        void visitBodyLiterals(const BodyNode& n, const P& p) {
                const NodeId* x  = n.preds();
                const uint32 inc = n.pred_inc();
                uint32       i   = 0;
                for (; *x != idMax; x += inc, ++i) { p(getAtom(*x).lit, i, false); }
                x += n.extended();
                for (; *x != idMax; x += inc, ++i) { p(Literal::fromRep(*x),i, true); }
        }
        NonHcfIter     nonHcfBegin() const { return components_.empty() ? NonHcfIter(0) : &components_[0]; }
        NonHcfIter     nonHcfEnd()   const { return nonHcfBegin() + components_.size(); }
        uint32         numNonHcfs()  const { return (uint32)components_.size(); }
        Configuration* nonHcfConfig()const { return config_; }
        void           accuStats()   const;
private:
        typedef PodVector<AtomNode>::type      AtomVec;
        typedef PodVector<BodyNode>::type      BodyVec;
        typedef PodVector<ComponentPair>::type ComponentMap;
        SharedDependencyGraph(const SharedDependencyGraph&);
        SharedDependencyGraph& operator=(const SharedDependencyGraph&);
        inline bool      relevantPrgAtom(const Solver& s, PrgAtom* a) const;
        inline bool      relevantPrgBody(const Solver& s, PrgBody* b) const;
        NodeId           createBody(PrgBody* b, uint32 bScc);
        NodeId           createAtom(Literal lit, uint32 aScc);
        NodeId           addBody(const LogicProgram& prg, PrgBody*);
        NodeId           addDisj(const LogicProgram& prg, PrgDisj*);
        uint32           addHeads(const LogicProgram& prg, PrgBody*, VarVec& atoms) const;
        uint32           getAtoms(const LogicProgram& prg, PrgDisj*, VarVec& atoms) const;
        void             addPreds(const LogicProgram& prg, PrgBody*, uint32 bScc, VarVec& preds) const;
        void             initBody(uint32 id, const VarVec& preds, const VarVec& atHeads);
        void             initAtom(uint32 id, uint32 prop, const VarVec& adj, uint32 preds);
        void             addNonHcf(SharedContext& ctx, uint32 scc);
        AtomVec        atoms_;
        BodyVec        bodies_;
        ComponentMap   components_;
        Configuration* config_;
};

}
#endif