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