PathPredicate.h

#ifndef ROSE_BinaryAnalysis_ModelChecker_PathPredicate_H
#define ROSE_BinaryAnalysis_ModelChecker_PathPredicate_H
#include <featureTests.h>
#ifdef ROSE_ENABLE_MODEL_CHECKER

#include <Rose/BinaryAnalysis/ModelChecker/Types.h>

namespace Rose {
namespace BinaryAnalysis {
namespace ModelChecker {

// Base class

class PathPredicate {
public:
    using Ptr = PathPredicatePtr;

protected:
    PathPredicate();
public:
    virtual ~PathPredicate();

public:
    virtual std::pair<bool, const char*> operator()(const SettingsPtr&, const PathPtr&) = 0;
    virtual std::pair<bool, const char*> test(const SettingsPtr&, const PathPtr&) final; // virtual only so we can say final
    virtual void reset() {}
};

// Predicate that's always true.

class AlwaysTrue: public PathPredicate {
public:
    using Ptr = AlwaysTruePtr;

public:
    static Ptr instance();

    virtual std::pair<bool, const char*> operator()(const SettingsPtr&, const PathPtr&) override;
};

// Default predicate guarding the work queue.

class WorkPredicate: public PathPredicate {
public:
    using Ptr = WorkPredicatePtr;

private:
    mutable SAWYER_THREAD_TRAITS::Mutex mutex_;         // protects the following data members
    size_t kLimitReached_ = 0;                          // number of times the K limit was hit
    size_t timeLimitReached_ = 0;                       // number of times the time limit was hit

public:
    static Ptr instance();

    size_t kLimitReached() const;

    size_t timeLimitReached() const;

public: // overrides
    virtual std::pair<bool, const char*> operator()(const SettingsPtr&, const PathPtr&) override;
    virtual void reset() override;
};

// Default predicate guarding the "interesting" queue.

class HasFinalTags: public PathPredicate {
public:
    using Ptr = HasFinalTagsPtr;

public:
    static Ptr instance();

    virtual std::pair<bool, const char*> operator()(const SettingsPtr&, const PathPtr&) override;
};

} // namespace
} // namespace
} // namespace

#endif
#endif