final_state.h

#ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_FINAL_STATE_H_
#define BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_FINAL_STATE_H_
 
#include <functional>
#include <optional>
#include <vector>
 
#include "backends/p4tools/common/lib/model.h"
#include "backends/p4tools/common/lib/trace_event.h"
#include "ir/solver.h"
#include "midend/coverage.h"
 
#include "backends/p4tools/modules/testgen/lib/concolic.h"
#include "backends/p4tools/modules/testgen/lib/execution_state.h"
 
namespace P4Tools::P4Testgen {
 
class FinalState {
 private:
    std::reference_wrapper<AbstractSolver> solver;
 
    std::reference_wrapper<const ExecutionState> state;
 
    std::reference_wrapper<const Model> finalModel;
 
    std::vector<std::reference_wrapper<const TraceEvent>> trace;
 
    static void calculatePayload(const ExecutionState &executionState, Model &evaluatedModel);
 
    static Model &processModel(const ExecutionState &finalState, Model &model,
                               bool postProcess = true);
 
 public:
    FinalState(AbstractSolver &solver, const ExecutionState &finalState);
 
    FinalState(AbstractSolver &solver, const ExecutionState &finalState, const Model &finalModel);
 
    [[nodiscard]] std::optional<std::reference_wrapper<const FinalState>> computeConcolicState(
        const ConcolicVariableMap &resolvedConcolicVariables) const;
 
    [[nodiscard]] const Model &getFinalModel() const;
 
    [[nodiscard]] AbstractSolver &getSolver() const;
 
    [[nodiscard]] const ExecutionState *getExecutionState() const;
 
    [[nodiscard]] const std::vector<std::reference_wrapper<const TraceEvent>> *getTraces() const;
 
    [[nodiscard]] const P4::Coverage::CoverageSet &getVisited() const;
};
 
}  // namespace P4Tools::P4Testgen
 
#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_FINAL_STATE_H_ */