include/dlvhex2/GenuineGuessAndCheckModelGenerator.h

Go to the documentation of this file.

/* dlvhex -- Answer-Set Programming with external interfaces.
 * Copyright (C) 2005-2007 Roman Schindlauer
 * Copyright (C) 2006-2015 Thomas Krennwallner
 * Copyright (C) 2009-2016 Peter Schüller
 * Copyright (C) 2011-2016 Christoph Redl
 * Copyright (C) 2015-2016 Tobias Kaminski
 * Copyright (C) 2015-2016 Antonius Weinzierl
 *
 * This file is part of dlvhex.
 *
 * dlvhex is free software; you can redistribute it and/or modify it
 * under the terms of the GNU Lesser General Public License as
 * published by the Free Software Foundation; either version 2.1 of
 * the License, or (at your option) any later version.
 *
 * dlvhex 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
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with dlvhex; if not, write to the Free Software
 * Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA
 * 02110-1301 USA.
 */

#ifndef GENUINEGUESSANDCHECK_MODEL_GENERATOR_HPP_INCLUDED__09122011
#define GENUINEGUESSANDCHECK_MODEL_GENERATOR_HPP_INCLUDED__09122011

#include "dlvhex2/PlatformDefinitions.h"
#include "dlvhex2/fwd.h"
#include "dlvhex2/ID.h"
#include "dlvhex2/FLPModelGeneratorBase.h"
#include "dlvhex2/ComponentGraph.h"
#include "dlvhex2/PredicateMask.h"
#include "dlvhex2/GenuineSolver.h"
#include "dlvhex2/InternalGroundDASPSolver.h"
#include "dlvhex2/UnfoundedSetChecker.h"
#include "dlvhex2/NogoodGrounder.h"
#include "dlvhex2/ExternalAtomVerificationTree.h"

#include <boost/unordered_map.hpp>
#include <boost/shared_ptr.hpp>

DLVHEX_NAMESPACE_BEGIN

class GenuineGuessAndCheckModelGeneratorFactory;

class GenuineGuessAndCheckModelGenerator:
public FLPModelGeneratorBase,
public ostream_printable<GenuineGuessAndCheckModelGenerator>,
public PropagatorCallback
{
    // types
    public:
        typedef GenuineGuessAndCheckModelGeneratorFactory Factory;

        // storage
    protected:
        // we store the factory again, because the base class stores it with the base type only!
        Factory& factory;
        RegistryPtr reg;

        // information about verification/falsification of current external atom guesses
        std::vector<ID> activeInnerEatoms;
        boost::unordered_map<IDAddress, std::vector<int> > verifyWatchList;
        boost::unordered_map<IDAddress, std::vector<int> > unverifyWatchList;
        std::vector<bool> eaEvaluated;
        std::vector<bool> eaVerified;
        InterpretationPtr verifiedAuxes;
        std::vector<InterpretationPtr> changedAtomsPerExternalAtom;

        // heuristics
        ExternalAtomEvaluationHeuristicsPtr defaultExternalAtomEvalHeuristics;
        std::vector<ExternalAtomEvaluationHeuristicsPtr> eaEvalHeuristics;
        /* \brief Heuristics to be used for unfounded set checking over partial assignments. */
        UnfoundedSetCheckHeuristicsPtr ufsCheckHeuristics;

        InterpretationConstPtr postprocessedInput;
        InterpretationPtr mask;

        // internal solver
        NogoodGrounderPtr nogoodGrounder;
        SimpleNogoodContainerPtr learnedEANogoods;
        ExternalAtomVerificationTree eavTree;
        int learnedEANogoodsTransferredIndex;
        GenuineGrounderPtr grounder;
        GenuineGroundSolverPtr solver;
        int cmModelCount;
        InterpretationPtr explAtoms;
        InternalGroundDASPSolverPtr analysissolver;
        bool haveInconsistencyCause;
        Nogood inconsistencyCause;
        UnfoundedSetCheckerManagerPtr ufscm;
        InterpretationPtr programMask;

        // members

        void inlineExternalAtoms(OrdinaryASPProgram& program, GenuineGrounderPtr& grounder, AnnotatedGroundProgram& annotatedGroundProgram, std::vector<ID>& activeInnerEatoms);

        ID replacePredForInlinedEAs(ID atomID, InterpretationConstPtr eliminatedExtAuxes);

        void initializeExplanationAtoms(OrdinaryASPProgram& program);

        void initializeInconsistencyAnalysis();

        void initializeHeuristics();

        void initializeVerificationWatchLists();

        void generalizeNogood(Nogood ng);

        void learnSupportSets();

        void updateEANogoods(InterpretationConstPtr compatibleSet, InterpretationConstPtr assigned = InterpretationConstPtr(), InterpretationConstPtr changed = InterpretationConstPtr());

        bool finalCompatibilityCheck(InterpretationConstPtr modelCandidate);

        bool isModel(InterpretationConstPtr compatibleSet);

        bool unfoundedSetCheck(InterpretationConstPtr partialInterpretation, InterpretationConstPtr assigned = InterpretationConstPtr(), InterpretationConstPtr changed = InterpretationConstPtr(), bool partial = false);

        IDAddress getWatchedLiteral(int eaIndex, InterpretationConstPtr search, bool truthValue);

        void unverifyExternalAtoms(InterpretationConstPtr changed);

        bool verifyExternalAtoms(InterpretationConstPtr partialInterpretation, InterpretationConstPtr assigned, InterpretationConstPtr changed);

        bool verifyExternalAtom(int eaIndex, InterpretationConstPtr partialInterpretation,
            InterpretationConstPtr assigned = InterpretationConstPtr(),
            InterpretationConstPtr changed = InterpretationConstPtr(),
            bool* answeredFromCacheOrSupportSets = 0);
        bool verifyExternalAtomByEvaluation(int eaIndex, InterpretationConstPtr partialInterpretation,
            InterpretationConstPtr assigned = InterpretationConstPtr(),
            InterpretationConstPtr changed = InterpretationConstPtr(),
            bool* answeredFromCache = 0);

        bool verifyExternalAtomBySupportSets(int eaIndex, InterpretationConstPtr partialInterpretation,
            InterpretationConstPtr assigned = InterpretationConstPtr(),
            InterpretationConstPtr changed = InterpretationConstPtr());

        const OrdinaryASPProgram& getGroundProgram();

        void propagate(InterpretationConstPtr partialInterpretation, InterpretationConstPtr assigned, InterpretationConstPtr changed);

    public:
        GenuineGuessAndCheckModelGenerator(Factory& factory, InterpretationConstPtr input);

        virtual ~GenuineGuessAndCheckModelGenerator();

        // generate and return next model, return null after last model
        virtual InterpretationPtr generateNextModel();

        void identifyInconsistencyCause();

        // handling inconsistencies propagated over multiple units
        virtual const Nogood* getInconsistencyCause();
        virtual void addNogood(const Nogood* cause);
};

class GenuineGuessAndCheckModelGeneratorFactory:
public FLPModelGeneratorFactoryBase,
public ostream_printable<GenuineGuessAndCheckModelGeneratorFactory>
{
    // types
    public:
        friend class GenuineGuessAndCheckModelGenerator;
        typedef ComponentGraph::ComponentInfo ComponentInfo;

        // storage
    protected:
        ASPSolverManager::SoftwareConfigurationPtr externalEvalConfig;
        ProgramCtx& ctx;
        ComponentInfo ci;        // should be a reference, but there is currently a bug in the copy constructor of ComponentGraph: it seems that the component info is shared between different copies of a component graph, hence it is deallocated when one of the copies dies.
        WARNING("TODO see comment above about ComponentInfo copy construction bug")

        
        std::vector<ID> outerEatoms;

        std::vector<std::pair<Nogood, int> > succNogoods;
    public:
        GenuineGuessAndCheckModelGeneratorFactory(
            ProgramCtx& ctx, const ComponentInfo& ci,
            ASPSolverManager::SoftwareConfigurationPtr externalEvalConfig);

        virtual ~GenuineGuessAndCheckModelGeneratorFactory() { }

        // add inconsistency explanation nogoods from successor components
        virtual void addInconsistencyCauseFromSuccessor(const Nogood* cause);

        virtual ModelGeneratorPtr createModelGenerator(InterpretationConstPtr input);

        virtual std::ostream& print(std::ostream& o) const;
        virtual std::ostream& print(std::ostream& o, bool verbose) const;
};

DLVHEX_NAMESPACE_END
#endif                           // GUESSANDCHECK_MODEL_GENERATOR_HPP_INCLUDED__09112010

// vim:expandtab:ts=4:sw=4:
// mode: C++
// End: