Decomposition.h

// Decomposition.h -- The interface to the super class of all the
// `decomposition' algorithms.

/*
 * Copyright (C) 1997-1998, 2003-2005 Tudor Hulubei <tudor@hulubei.net>.
 *
 * This library 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, or (at
 * your option) any later version.
 *
 * This library 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 this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA,
 * 02111-1307, USA.
 */

/*
 * NOTE: This is an interal header file.
 * You should not attempt to use it directly.
 */

// $Id: Decomposition_8h-source.html,v 1.1 2005/05/25 12:37:18 tudor Exp $

#ifndef _CSP_KERNEL_Decomposition_H
#define _CSP_KERNEL_Decomposition_H


CSP_NAMESPACE_BEGIN(csp);


class CSP_API Driver;


class CSP_API Decomposition
{
  public:
    static const timeval NoTimeLimit;

    static const ulonglong NoNodeLimit;

    static const bool KeepChanges = true;

    static const bool DiscardChanges = false;

    static const bool ReselectAllowed = true;

    static const bool ReselectProhibited = false;

    typedef bool (*SolutionCallback)(Decomposition&, bool&);

    typedef bool (*EvaluationCallback)(Decomposition&, bool&);

    typedef bool (*RefutationCallback)(Decomposition&, bool&);

    typedef hash_set<Variable*> ActiveVariablesSet;

    typedef hash_set<Constraint*> ActiveConstraintsSet;

    enum Statistics
    {
        NoStatistics = 0,

        AverageUninstantiatedVariables = 1,

        AverageModifiedVariables = 2,

        AverageDomainSize = 4,

        AverageActiveConstraints = 8,

        AverageVariableDegree = 16,

        AverageConstrainedness = 32,

        AverageConstraintDensity = 64,

        AverageConstraintTightness = 128,

        AverageLooseConstraints = 256,

        AverageLeafDepth = 512,

        Nodes = 1024,

        Leaves = 2048,

        ExtraPropagationStatistics = 4096,

        VariableSelectionCounters = 8192,

        LastPathSelections = 16384,

        Backdoor = 32768,

        BranchingAssignments = 65536,

        AllStatistics = UINT_MAX
    };

    enum Features
    {
        NoFeatures = 0,

        StaticOptimismBucketing = 1,

        DynamicOptimismBucketing = 2,

        GreedyVariableProcessing = 8,

        LooseConstraintsDeactivation = 16,

        FailFirstnessAnalysis = 32,

        AggregateScoreValueSelection = 64,

        AllFeatures = UINT_MAX
    };

    struct Refutation
    {
        Refutation() { init(); }

        void init()
        {
            m_ccks = ULONGLONG_MAX;
            m_nodes = ULONGLONG_MAX;
            m_assignments = ULONGLONG_MAX;
            m_lowerBound = 0;
            m_resources = true;
            m_depth = INT_MAX;
            m_isOptimal = false;
        }

        vector<vector<id_t> > m_variables;

        vector<vector<id_t> > m_values;

        ulonglong m_ccks;

        ulonglong m_nodes;

        ulonglong m_assignments;

        ulonglong m_lowerBound;

        Resources m_resources;

        int m_depth;

        bool m_isOptimal;
    };

    virtual ~Decomposition();

    const wstring name() const {
        return m_fullName + L" (" + m_shortName + L")"; }

    const wstring& fullName() const { return m_fullName; }

    const wstring& shortName() const { return m_shortName; }

    const Problem& problem() const { return m_problem; }

    Problem& problem() { return m_problem; }

    const Filter& filter() const { return m_filter; }

    Filter& filter() { return m_filter; }

    const Retraction& retraction() const { return m_retraction; }

    Retraction& retraction() { return m_retraction; }

    int depth() const { return m_depth; }

    void keepBestValues(double percentage);

    double percentageOfInstantiatedVariables() const;

    void getModifiedVariables(
        int depth,
        vector<Variable*>& modifiedVariables) const;

    ulonglong solutions() const { return m_solutions.back(); }

    bool registerHeuristic(VariableOH& heuristic, bool back = true);

    bool unregisterHeuristic(VariableOH& heuristic);

    size_t variableOrderingHeuristics() const
    {
        return m_variableOH.size();
    }

    VariableOH& variableOrderingHeuristic(size_t n) const
    {
        return *m_variableOH[n];
    }

    bool registerHeuristic(ValueOH& heuristic, bool back = true);

    bool unregisterHeuristic(ValueOH& heuristic);

    size_t valueOrderingHeuristics() const
    {
        return m_valueOH.size();
    }

    ValueOH& valueOrderingHeuristic(size_t n) const
    {
        return *m_valueOH[n];
    }

    const vlist_type& uninstantiatedVariables() const
    {
        return m_uninstantiatedVariables;
    }

    void getInstantiatedVariables(hash_set<const Variable*>& c) const;

    const shash_type& solutionsLeft() const { return m_solutionsLeft; }

    void getKnownSolutions(
        const hash_set<const Variable*>& instantiatedVariables,
        const shash_type& solutionsLeft,
        shash_type& goodSolutions,
        shash_type& badSolutions) const;

    void getPerfectValues(
        const Variable& variable,
        hash_set<const Value*>& values,
        const shash_type& solutions) const;

    void setSolutionCallback(SolutionCallback solutionCallback)
    {
        m_solutionCallbacks[m_solutionCallbacks.size() - 1] =
            solutionCallback;
    }

    SolutionCallback solutionCallback() const
    {
        return m_solutionCallbacks[m_solutionCallbacks.size() - 1];
    }

    void setEvaluationCallback(EvaluationCallback evaluationCallback)
    {
        m_evaluationCallbacks[m_evaluationCallbacks.size() - 1] =
            evaluationCallback;
    }

    EvaluationCallback evaluationCallback() const
    {
        return m_evaluationCallbacks[m_evaluationCallbacks.size() - 1];
    }

    void setRefutationCallback(RefutationCallback refutationCallback)
    {
        m_refutationCallbacks[m_refutationCallbacks.size() - 1] =
            refutationCallback;
    }

    RefutationCallback refutationCallback() const
    {
        return m_refutationCallbacks[m_refutationCallbacks.size() - 1];
    }

    ulonglong search(
        const bool yield = false,
        const vlist_type& instantiables = s_all);

    void buildActiveSets(
        const vlist_type& variables,
        ActiveVariablesSet& avs,
        ActiveConstraintsSet& acs) const;

    int depthOfDeepestModifiedVariable(const hash_set<id_t>& wanted) const;

    size_t branching(
        Variable& variable,
        hash_map<const Value*, size_t>& costs,
        int level,
        bool minimum = true);

    void postPropagationDomainSizes(
        Variable& variable,
        hash_map<const Value*, size_t>& domainSizes,
        bool minimum = true);

    ulonglong totalNodes() const;

    double staticOptimismPercentage() const
    {
        return m_staticOptimismPercentage;
    }

    void setStaticOptimismPercentage(double percentage)
    {
        m_staticOptimismPercentage = percentage;
    }

    double dynamicOptimismPercentage() const
    {
        return m_dynamicOptimismPercentage;
    }

    void setDynamicOptimismPercentage(double percentage)
    {
        m_dynamicOptimismPercentage = percentage;
    }

    const BitFlags& statistics() const { return m_statistics; }

    bool setStatistics(const BitFlags::Flags flags);

    const BitFlags& features() const { return m_features; }

    bool setFeatures(const BitFlags::Flags flags);

    const PropagationStatistics& propagationStatistics() const
    {
        return m_propagationStatistics;
    }

    const Resources& resources() const { return m_resources; }

    Resources& resources() { return m_resources; }

    const vector<long double>& averageUninstantiatedVariables() const
    {
        return m_averageUninstantiatedVariables;
    }

    const vector<long double>& averageModifiedVariables() const
    {
        return m_averageModifiedVariables;
    }

    const vector<long double>& averageDomainSize() const
    {
        return m_averageDomainSize;
    }

    const vector<long double>& averageMinimumDomainSize() const
    {
        return m_averageMinimumDomainSize;
    }

    const vector<long double>& averageMaximumDomainSize() const
    {
        return m_averageMaximumDomainSize;
    }

    const vector<long double>& averageActiveConstraints() const
    {
        return m_averageActiveConstraints;
    }

    const vector<long double>& averageVariableDegree() const
    {
        return m_averageVariableDegree;
    }

    const vector<long double>& averageConstrainedness() const
    {
        return m_averageConstrainedness;
    }

    const vector<long double>& averageConstraintDensity() const
    {
        return m_averageConstraintDensity;
    }

    const vector<long double>& averageConstraintTightness() const
    {
        return m_averageConstraintTightness;
    }

    const vector<long double>& averageLooseConstraints() const
    {
        return m_averageLooseConstraints;
    }

    const vector<hash_map<Variable*, ulonglong> >&
    variableSelectionCounters() const
    {
        return m_variableSelectionCounters;
    }

    const vector<vector<pair<Variable*, Domain*> > >& lastPathSelections() const
    {
        return m_lastPathSelections;
    }

    const vector<pair <Variable*, Domain*> >& backdoor() const
    {
        return m_backdoor;
    }

    const vector<vector<pair <Variable*, Domain*> > >&
    branchingAssignments() const
    {
        return m_branchingAssignments;
    }

    inline Driver* driver() { return m_driver; }

    inline const Driver* driver() const { return m_driver; }

    inline const timeval& timeLimit() const { return m_timeLimit; }

    bool timeLimitEnabled() const;

    timeval setTimeLimit(const timeval& timeLimit);

    bool timeLimitExceeded();

    inline const ulonglong nodeLimit() const { return m_nodeLimit; }

    bool nodeLimitEnabled() const { return m_nodeLimit != NoNodeLimit; }

    ulonglong setNodeLimit(const ulonglong nodeLimit);

    bool nodeLimitExceeded();

    ulonglong setRefutationsLimit(ulonglong refutationsLimit);

    void setRefutationNodesUpperBound(ulonglong nodes)
    {
        m_ffaRefutationNodesUpperBound = nodes;
    }

    void recordRefutationParameters(
        const ulonglong ccks,
        const ulonglong nodes,
        const Resources& resources,
        const int depth);

    void currentRefutation(
        vector<vector<id_t> >& variables,
        vector<vector<id_t> >& values);

    bool shortestRefutation(Refutation& refutation) const;

    ulonglong shortestRefutationNodes() const
    {
        return m_ffaShortestRefutation.m_nodes;
    }

    void setRefutationDepthUpperBound(int depthUpperBound);

    void setIterativeDeepening(bool iterativeDeepening)
    {
        m_ffaIterativeDeepening = iterativeDeepening;
    }

    void setLookAheadLevel(int lookAheadLevel)
    {
        m_ffaLookAheadLevel = lookAheadLevel;
    }

    void setOptimalRefutationCaching(bool caching)
    {
        m_ffaOptimalRefutationCaching = caching;
    }

    void setConsistencyBeforeSearch(bool consistencyBeforeSearch);

    size_t ffaDynamicUpperBoundThreshold() const
    {
        return m_ffaDynamicUpperBoundThreshold;
    }

    void setFFADynamicUpperBoundThreshold(size_t nVariables)
    {
        m_ffaDynamicUpperBoundThreshold = nVariables;
    }

    int ffaProgressReportingDepthLimit() const
    {
        return m_ffaProgressReportingDepthLimit;
    }

    void setFFAProgressReportingDepthLimit(int limit)
    {
        m_ffaProgressReportingDepthLimit = limit;
    }

    size_t ffaLowerBoundLookAheadLevel() const
    {
        return m_ffaLowerBoundLookAheadLevel;
    }

    void setFFALowerBoundLookAheadLevel(size_t level)
    {
        m_ffaLowerBoundLookAheadLevel = level;
    }

    double setFFAOptimismPercentage() const
    {
        return m_ffaOptimismPercentage;
    }

    void setFFAOptimismPercentage(double percentage)
    {
        m_ffaOptimismPercentage = percentage;
    }

    int maximumSearchDepth() const;

    long double constrainedness(
        const ActiveVariablesSet& avs,
        const ActiveConstraintsSet& acs) const;

    ulonglong nodes(int depth) const;

    ulonglong leaves(int depth) const;

    const vector<vector<ulonglong> >& mistakePointNodes(int depth) const
    {
        assert(depth < (int)m_nodes.size());
        return m_nodes[depth];
    }

    const vector<vector<ulonglong> >& mistakePointLeaves(int depth) const
    {
        assert(depth < (int)m_leaves.size());
        return m_leaves[depth];
    }

    ulonglong backtracks(int depth) const;

    int solutionDepth() const
    {
        assert(m_solutionDepth == (int)m_solutionHeuristicMistakes.size() - 1);
        return m_solutionDepth;
    }

    const vector<ulonglong>& solutionHeuristicMistakes() const
    {
        return m_solutionHeuristicMistakes;
    }

    const vector<ulonglong>& globalHeuristicMistakes() const
    {
        return m_globalHeuristicMistakes;
    }

    ulonglong refutationSizeLowerBound(int lookAheadLevel);

    ulonglong initialRefutationSizeLowerBound() const {
        return m_ffaInitialRefutationSizeLowerBound; }

    void generateProblemGraph(wostream& wos) const;

    void generateProblemGraph(const wstring& stem) const;

    bool scheduleProblemGraphGeneration(const wstring& stem, int depth);

    bool scheduleSearchTreeGeneration(const wstring& stem, int depth);

  protected:
    virtual bool init();

    virtual void done();

    void eureka();

    bool hideBadValues(Variable& variable) const;

    ulonglong totalValues(vlist_type& variables) const;

    virtual void decompose() = 0;

    bool propagate(
        const bool keepChanges = KeepChanges,
        const vlist_type& instantiables = s_all);

    bool propagateAndSearch(const vlist_type& instantiable = s_all);

    bool canYield() const;

    Variable* selectVariable(
        const bool reselectOk = ReselectAllowed,
        const vlist_type& undesirables = s_empty);

    Variable& selectVariable(Variable& variable);

    size_t selectAllVariables(vlist_type* selection = 0);

    void unselectVariable(Variable& variable);

    Value* selectValue(Variable& variable, Domain& domain);

    void unselectValue(Domain& domain, Value* value)
    {
        insert(domain, value);
    }

    void saveState()
    {
        csp::Filter::saveState(m_uninstantiatedVariables);
        csp::Filter::saveState(m_instantiatedVariables[m_depth]);
    }

    void restoreState()
    {
        csp::Filter::restoreState(m_instantiatedVariables[m_depth]);
        csp::Filter::restoreState(m_uninstantiatedVariables);
    }

    bool moreWork();

    bool moreSolutionsNeeded() const { return m_moreSolutionsNeeded.back(); }

    bool discardableSubtree();

    bool atJumpDepth() const { return m_depth == m_jumpDepth; }

    void restrict(const vlist_type& variables);

    void unrestrict();

    void printStack();

    Decomposition(
        const wstring& fullName,
        const wstring& shortName,
        Problem& problem,
        Filter& filter,
        Retraction& retraction,
        Randomizer& randomizer,
        bool consistencyBeforeSearch = true);

    Problem& m_problem;

    vector<SolutionCallback> m_solutionCallbacks;

    vector<EvaluationCallback> m_evaluationCallbacks;

    vector<RefutationCallback> m_refutationCallbacks;

    bool m_consistencyBeforeSearch;

  private:
    friend class Driver;

    Decomposition(const Decomposition&);

    Decomposition& operator=(const Decomposition&);

    static const bool UnselectableVariables = true;
    static const bool SelectedVariables = false;

    static const bool WillingToYield = true;
    static const bool UnwillingToYield = false;

    bool selectVariables();

    void unselectVariables();

    void goModifiedOrUnmodified2OneValue(
        Variable& variable,
        const bool instantiable,
        vlist_type& modifiedVariables,
        vlist_type& instantiatedVariables);

    void goModifiedOrUnmodified2Modified(
        Variable& variable,
        vlist_type& modifiedVariables);

    void goModifiedOrUnmodified2Unmodified(Variable& variable);

    void prePropagation(const vlist_type& instantiables = s_all);

    void postPropagation(bool endSearch);

    void activateConstraints(clist_type& cl);

    void deactivateConstraints();

    void makeChangesPermanent();

    void saveTemporalFlags();

    void shiftTemporalFlags();

    void restoreTemporalFlags(const bool type = SelectedVariables);

    void discardTemporalFlags(const bool type = SelectedVariables);

    bool autoSelectVariables();

    bool temporaryPropagate();

    void deinstantiateVariableList(const vlist_type& vl);

    template <class Iterator>
    void accumulateConstraints(
        const Iterator vb,
        const Iterator ve,
        ActiveConstraintsSet& acs) const
    {
        for (Iterator vi = vb; vi != ve; ++vi)
        {
            const Variable& variable = **vi;
            Variable::constraint_iterator ci = variable.beginConstraints();
            Variable::constraint_iterator cie = variable.endConstraints();
            for (; ci != cie; ++ci)
            {
                Constraint& constraint = **ci;
                if (acs.find(&constraint) == acs.end())
                    acs.insert(&constraint);
            }
        }
    }

    void getNonHiddenVariables(
        vhash_type& nonHiddenVariables) const;

    void getNonHiddenConstraints(
        const vhash_type& nonHiddenVariables,
        chash_type& nonHiddenConstraints) const;

    bool isSolution(bool debugging = false) const;

    void saveVariables(
        vector<Variable*>& variables,
        vector<Domain*>& domains,
        vector<vector<Constraint*>*>& constraints);

    void compareVariables(
        const vector<Variable*>& variables,
        const vector<Domain*>& domains,
        vector<vector<Constraint*>*>& constraints);

    bool validBackdoorReassignment(
        Variable& variable,
        Value& value,
        const vector<Constraint*>& constraints) const;

    void updateStatistics();

    void onFringe(bool isSolution);

    void updateNodeCount();

    void updateLeafCount();

    void updateAverageUninstantiatedVariables();

    void updateAverageModifiedVariables();

    void updateAverageDomainSize();

    void updateAverageActiveConstraints(
        const ActiveConstraintsSet& acs);

    void updateAverageVariableDegree(
        const ActiveVariablesSet& avs);

    void updateAverageConstrainedness(
        const ActiveVariablesSet& avs,
        const ActiveConstraintsSet& acs);

    void updateAverageConstraintDensity(
        const ActiveVariablesSet& avs,
        const ActiveConstraintsSet& acs);

    void updateAverageConstraintTightness(
        const ActiveConstraintsSet& acs);

    void updateAverageLooseConstraints(
        const ActiveConstraintsSet& acs);

    void incrementSelectionCounter(Variable& variable);

    void updateHeuristicMistakeStatistics();

    void updateSolutions();

    void computeBackdoor();

    void computeBackdoorKey();

    void computeBranchingAssignments();

    void callBackdoorHooks() const;

    void callBackdoorKeyHooks() const;

    void callBranchingHooks() const;

    void updateLastPathSelections(Variable* variable);

    void trimLastPathSelections(int depth);

    void sortDomains(const vlist_type& variables);

    void decomposeWrapper();

    void generateSearchTree(const wstring& stem) const;

    wstring searchTreeNodeLabel();

    void addSearchTreeNode(bool isLeaf, bool isSolution);

    void addSearchTreeArc();

    void assertDomainsAreSorted() const;

    typedef vector<size_t> marks_type;

    ulonglong dynamicNodesUpperBound();

    void decomposeForOptimalRefutation();

    void kwayDecompose();

    ulonglong uncertainAssignments(const marks_type& marks) const;

    ulonglong refutationAssignments() const;

    void computeMinimumValueCosts(
        Variable& variable,
        Domain& copy,
        hash_map<const Value*, size_t>& costs,
        int level,
        bool minimum = true);

    size_t minimumVariableCost(
        Domain& domain,
        hash_map<const Value*, size_t>& costs,
        int lookAheadLevel) const;

    bool tooManyAssignments(
        const marks_type& marks,
        size_t extraAssignments) const;

    bool partialRefutationIsConsistent() const;

    void mark(marks_type& marks, vector<vector<id_t> >& data);

    void undo(const marks_type& marks, vector<vector<id_t> >& data);

    void saveBest(
        const marks_type& marks,
        vector<vector<id_t> >& data,
        vector<vector<id_t> >& best);

    void restoreBest(
        vector<vector<id_t> >& data,
        vector<vector<id_t> >& best);

    const wstring optimalRefutationCacheKey(int maxDepth) const;

    void clearOptimalRefutationsCache();

    void printOptimalRefutationsCacheStatistics();

    void updatePercentage(
        double completed,
        double total,
        csp::Resources& resources,
        bool print = true);

    const wstring m_fullName;

    const wstring m_shortName;

    Filter& m_filter;

    Retraction& m_retraction;

    Randomizer& m_randomizer;

    vlist_type m_uninstantiatedVariables;

    int m_depth;

    int m_jumpDepth;

    wstring m_problemGraphFileStem;

    int m_problemGraphGenerationDepth;

    wstring m_searchTreeFileStem;

    int m_searchTreeGenerationDepth;

    wostringstream m_searchTreeNodes;

    wostringstream m_searchTreeArcs;

    vector<size_t> m_searchTreeStack;

    size_t m_searchTreeNodeIndex;

    double m_staticOptimismPercentage;

    double m_dynamicOptimismPercentage;

    vector<vlist_type> m_modifiedVariables;

    vector<vlist_type> m_instantiatedVariables;

    size_t m_totalInstantiatedVariables;

    vector<vlist_type> m_unselectableVariables;

    vector<vlist_type> m_selectedVariables;

    vector<clist_type> m_inactiveConstraints;

    vector<clist_type> m_permanentlyInactiveConstraints;

    vector<list<size_t> > m_selectedVariablesDomainSizes;

    typedef struct flags_t
    {
        bool m_past; // `true' for past variables.
        bool m_current; // `true' for current variables.
        bool m_future; // `true' for future variables.
    };

    vector<vector<flags_t> > m_selectedVariablesTemporalFlags;

    vector<vector<flags_t> > m_unselectableVariablesTemporalFlags;

    Resources m_resources;

    bool m_timeLimitExceeded;

    timeval m_timeLimit;

    bool m_nodeLimitExceeded;

    ulonglong m_nodeLimit;

    vector<bool> m_moreSolutionsNeeded;

    vector<ulonglong> m_solutions;

    Driver* m_driver;

    size_t m_index;

    bool m_propagationIsRestorable;

    vector<vector<vector<ulonglong> > > m_nodes;

    vector<vector<vector<ulonglong> > > m_leaves;

    vector<ulonglong> m_currentHeuristicMistakes;

    vector<ulonglong> m_solutionHeuristicMistakes;

    vector<ulonglong> m_globalHeuristicMistakes;

    vector<long double> m_averageUninstantiatedVariables;

    vector<long double> m_averageModifiedVariables;

    hash_map<const Variable*, size_t> m_originalDomainSizes;

    vector<long double> m_averageDomainSize;

    vector<long double> m_averageMinimumDomainSize;

    vector<long double> m_averageMaximumDomainSize;

    vector<long double> m_averageActiveConstraints;

    vector<long double> m_averageVariableDegree;

    vector<long double> m_averageConstrainedness;

    vector<long double> m_averageConstraintDensity;

    vector<long double> m_averageConstraintTightness;

    vector<long double> m_averageLooseConstraints;

    vector<hash_map<Variable*, ulonglong> >
        m_variableSelectionCounters;

    vector<vector<pair<Variable*, Domain*> > > m_lastPathSelections;

    vector<pair<Variable*, Domain*> > m_backdoor;

    vector<vector<pair<Variable*, Domain*> > > m_branchingAssignments;

    vector<VariableOH*> m_variableOH;

    vector<ValueOH*> m_valueOH;

    vector<vlist_type> m_hiddenVariables;

    hash_map<Variable*, Domain*> m_unwantedValues;

    shash_type m_solutionsLeft;

    BitFlags m_features;

    BitFlags m_statistics;

    BitFlags m_previousFeatures;

    BitFlags m_previousStatistics;

    PropagationStatistics m_propagationStatistics;

    bool m_searching;

    int m_maximumSearchDepth;

    int m_solutionDepth;

    int* m_previousIndentationLevelPlaceholder;

    static const vlist_type s_empty;

    static const vlist_type s_all;

    int m_ffaDepthUpperBound;

    bool m_ffaKWayDecomposition;

    int m_ffaDepthLimit;

    bool m_ffaIterativeDeepening;

    int m_ffaLookAheadLevel;

    bool m_ffaDepthLimitReached;

    size_t m_ffaLowerBoundLookAheadLevel;

    size_t m_ffaDynamicUpperBoundThreshold;

    ulonglong m_ffaInitialRefutationSizeLowerBound;

    ulonglong m_ffaRefutationExtraCostLowerBound;

    bool m_ffaTooManyAssignments;

    int m_ffaRefutationDepth;

    ulonglong m_ffaRefutationsFound;

    ulonglong m_ffaRefutationsLimit;

    vector<vector<id_t> > m_ffaRefutationVariables;

    vector<vector<id_t> > m_ffaRefutationValues;

    vector<ulonglong> m_ffaRefutationMinimumAssignments;

    Refutation m_ffaShortestRefutation;

    ulonglong m_ffaRefutationNodesUpperBound;

    bool m_ffaOptimalRefutationCaching;

    struct OptimalRefutation
    {
        OptimalRefutation(
            vector<vector<id_t> >* variables,
            vector<vector<id_t> >* values,
            ulonglong assignments,
            int depthLimit,
            size_t nVariables) :
            m_variables(variables),
            m_values(values),
            m_assignments(assignments),
            m_depthLimit(depthLimit),
            m_nVariables(nVariables),
            m_hits(0),
            m_quasiHits(0) {}

        vector<vector<id_t> >* m_variables;
        vector<vector<id_t> >* m_values;
        ulonglong m_assignments;
        int m_depthLimit;
        size_t m_nVariables;
        ulonglong m_hits;
        ulonglong m_quasiHits;
    };

    struct OptimalRefutationLessThan
    {
        bool operator()(
            const OptimalRefutation* or1,
            const OptimalRefutation* or2) const
        {
            return or1->m_assignments > or2->m_assignments;
        }
    };

#if defined(__GNUG__)

    struct StringEqual
    {
        bool operator()(const char* s1, const char* s2) const
        {
            return strcmp(s1, s2) == 0;
        }
    };

    typedef hash_map<
            const char*,
            OptimalRefutation*,
            hash<const char*>,
            StringEqual> OptimalRefutationsCache;
#elif defined(_MSC_VER)
    // Comparison object for character pointers.
    struct StringCompare
    {
        enum
        {
            bucket_size = 32, // 0 < bucket_size
            min_buckets = 32
        };

        size_t operator()(const char* s) const
        {
            size_t hashval = 0;
            const unsigned char* p = reinterpret_cast<const unsigned char*>(s);
            while (*p != '\0')
                hashval += *p++;
            return hashval;
        }

        bool operator()(const char* s1, const char* s2) const
        {
            return strcmp(s1, s2) < 0;
        }
    };

    typedef hash_map<
            const char*,
            OptimalRefutation*,
            StringCompare> OptimalRefutationsCache;
#endif

    OptimalRefutationsCache m_ffaOptimalRefutationsCache;

    ulonglong m_ffaOptimalRefutationsCacheLookups;

    ulonglong m_ffaOptimalRefutationsCacheHits;

    ulonglong m_ffaOptimalRefutationsCacheQuasiHits;

    vector<pair<pair<double, double>, Resources*> > m_ffaAlternativesLeft;

    int m_ffaProgressReportingDepthLimit;

    double m_ffaOptimismPercentage;
};


CSP_NAMESPACE_END(csp);


#endif // _CSP_KERNEL_Decomposition_H

// Local Variables:
// mode: C++
// End:

---