accessor.h

/*
 * SPDX-FileCopyrightText: 2022 The P4 Language Consortium
 *
 * SPDX-License-Identifier: Apache-2.0
 */
 
#ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_TEST_Z3_SOLVER_ACCESSOR_H_
#define BACKENDS_P4TOOLS_MODULES_TESTGEN_TEST_Z3_SOLVER_ACCESSOR_H_
 
#include <vector>
 
#include "backends/p4tools/common/core/z3_solver.h"
 
namespace P4::P4Tools {
 
// The main class for access to a private members
class Z3SolverAccessor {
 public:
    explicit Z3SolverAccessor(Z3Solver &solver) : solver(solver) {}

    z3::expr_vector getAssertions(std::optional<bool> assertionType = std::nullopt) {
        if (!assertionType) {
            return solver.isIncremental ? solver.z3solver.assertions() : solver.z3Assertions;
        }
        if (assertionType.value()) {
            return solver.z3solver.assertions();
        }
        return solver.z3Assertions;
    }

    safe_vector<const Constraint *> getP4Assertions() { return solver.p4Assertions; }

    const z3::context &getContext() { return solver.getZ3Ctx(); }

    std::vector<size_t> &getCheckpoints() { return solver.checkpoints; }
 
 private:
    Z3Solver &solver;
};
 
}  // namespace P4::P4Tools
 
#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_TEST_Z3_SOLVER_ACCESSOR_H_ */