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/BasicTypes.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