Path.h

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

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

#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/BasicTypes.h>
#include <Rose/BinaryAnalysis/SmtSolver.h>
#include <Rose/BinaryAnalysis/SymbolicExpression.h>
#include <Combinatorics.h>

namespace Rose {
namespace BinaryAnalysis {
namespace ModelChecker {

class Path {
public:
    using Ptr = PathPtr;

private:
    PathNodePtr end_;

protected:
    Path() = delete;
    explicit Path(const PathNodePtr &end);
public:
    ~Path();

public:
    static Ptr instance(const ExecutionUnitPtr&);

    static Ptr instance(const PathPtr &prefix, const ExecutionUnitPtr&, const SymbolicExpression::Ptr &assertion,
                        const SmtSolver::Evidence&, const InstructionSemantics::BaseSemantics::StatePtr &parentOutgoingState);

    bool isEmpty() const;

    size_t nNodes() const;

    size_t nSteps() const;

    double processingTime() const;

    uint64_t hash() const;
    void hash(Combinatorics::Hasher&) const;
    bool executionFailed() const;

    std::vector<SymbolicExpression::Ptr> assertions() const;

    PathNodePtr lastNode() const;

    std::vector<PathNodePtr> nodes() const;

    std::string printableName() const;

    void print(const SettingsPtr&, std::ostream&, const std::string &prefix, size_t maxSteps) const;

    void toYaml(const SettingsPtr&, std::ostream&, const std::string &prefix, size_t maxSteps) const;


};

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

#endif
#endif