z3_solver.h

/*
 * SPDX-FileCopyrightText: 2022 The P4 Language Consortium
 *
 * SPDX-License-Identifier: Apache-2.0
 */
 
#ifndef BACKENDS_P4TOOLS_COMMON_CORE_Z3_SOLVER_H_
#define BACKENDS_P4TOOLS_COMMON_CORE_Z3_SOLVER_H_
 
#include <z3++.h>
#include <z3.h>
 
#include <cstddef>
#include <iosfwd>
#include <optional>
#include <string>
#include <vector>
 
#include "ir/ir.h"
#include "ir/json_generator.h"
#include "ir/solver.h"
#include "lib/cstring.h"
#include "lib/ordered_map.h"
#include "lib/rtti.h"
#include "lib/safe_vector.h"
 
namespace P4::P4Tools {

using Z3DeclaredVariablesMap = std::vector<ordered_map<unsigned, const IR::SymbolicVariable *>>;

class Z3Solver : public AbstractSolver {
    friend class Z3Translator;
    friend class Z3JSON;
    friend class Z3SolverAccessor;
 
 public:
    ~Z3Solver() override = default;
 
    explicit Z3Solver(bool isIncremental = true,
                      std::optional<std::istream *> inOpt = std::nullopt);
 
    void comment(cstring comment) override;
 
    void seed(unsigned seed) override;
 
    void timeout(unsigned tm) override;
 
    std::optional<bool> checkSat(const std::vector<const Constraint *> &asserts) override;

    std::optional<bool> checkSat(const z3::expr_vector &asserts);

    std::optional<bool> checkSat();
 
    [[nodiscard]] const SymbolicMapping &getSymbolicMapping() const override;
 
    void toJSON(JSONGenerator & /*json*/) const override;
 
    [[nodiscard]] bool isInIncrementalMode() const override;

    [[nodiscard]] const z3::solver &getZ3Solver() const;

    [[nodiscard]] const z3::context &getZ3Ctx() const;

    [[nodiscard]] safe_vector<const Constraint *> getAssertions() const;

    void reset();

    void push();

    void pop();

    void clearMemory();

    void asrt(const z3::expr &assert);

    void asrt(const Constraint *assertion);
 
 private:
    z3::sort toSort(const IR::Type *type);

    [[nodiscard]] z3::context &ctx() const;

    z3::expr declareVar(const IR::SymbolicVariable &var);

    [[nodiscard]] static std::string generateName(const IR::SymbolicVariable &var);

    static const IR::Literal *toLiteral(const z3::expr &e, const IR::Type *type);

    //             that is greater than or equal to @asrtIndex.
    void addZ3Pushes(size_t &chkIndex, size_t asrtIndex);

    static std::optional<bool> interpretSolverResult(z3::check_result result);

    z3::solver z3solver;

    Z3DeclaredVariablesMap declaredVarsById;

    safe_vector<const Constraint *> p4Assertions;

    bool isIncremental;

    std::vector<size_t> checkpoints;

    z3::expr_vector z3Assertions;

    std::optional<unsigned> seed_;

    std::optional<unsigned> timeout_;
 
    DECLARE_TYPEINFO(Z3Solver, AbstractSolver);
};

class Z3Translator : public virtual Inspector {
 public:
    explicit Z3Translator(Z3Solver &solver);

    bool preorder(const IR::Node *node) override;

    bool preorder(const IR::Cast *cast) override;

    bool preorder(const IR::Constant *constant) override;
    bool preorder(const IR::BoolLiteral *boolLiteral) override;
    bool preorder(const IR::StringLiteral *stringLiteral) override;

    bool preorder(const IR::SymbolicVariable *var) override;
 
    // Translations for unary operations.
    bool preorder(const IR::Neg *op) override;
    bool preorder(const IR::Cmpl *op) override;
    bool preorder(const IR::LNot *op) override;
 
    // Translations for binary operations.
    bool preorder(const IR::Equ *op) override;
    bool preorder(const IR::Neq *op) override;
    bool preorder(const IR::Lss *op) override;
    bool preorder(const IR::Leq *op) override;
    bool preorder(const IR::Grt *op) override;
    bool preorder(const IR::Geq *op) override;
    bool preorder(const IR::Mod *op) override;
    bool preorder(const IR::Add *op) override;
    bool preorder(const IR::Sub *op) override;
    bool preorder(const IR::Mul *op) override;
    bool preorder(const IR::Div *op) override;
    bool preorder(const IR::Shl *op) override;
    bool preorder(const IR::Shr *op) override;
    bool preorder(const IR::BAnd *op) override;
    bool preorder(const IR::BOr *op) override;
    bool preorder(const IR::BXor *op) override;
    bool preorder(const IR::LAnd *op) override;
    bool preorder(const IR::LOr *op) override;
    bool preorder(const IR::Concat *op) override;
 
    // Translations for ternary operations.
    bool preorder(const IR::Mux *op) override;
    bool preorder(const IR::Slice *op) override;

    z3::expr getResult();

    z3::expr translate(const IR::Expression *expression);
 
 private:
    using Z3UnaryOp = z3::expr (*)(const z3::expr &);

    using Z3BinaryOp = z3::expr (*)(const z3::expr &, const z3::expr &);

    using Z3TernaryOp = z3::expr (*)(const z3::expr &, const z3::expr &, const z3::expr &);

    bool recurseUnary(const IR::Operation_Unary *unary, Z3UnaryOp f);

    bool recurseBinary(const IR::Operation_Binary *binary, Z3BinaryOp f);

    bool recurseTernary(const IR::Operation_Ternary *ternary, Z3TernaryOp f);

    template <class ShiftType>
    const ShiftType *rewriteShift(const ShiftType *shift) const;

    z3::expr result;

    std::reference_wrapper<Z3Solver> solver;
};
 
}  // namespace P4::P4Tools
 
#endif /* BACKENDS_P4TOOLS_COMMON_CORE_Z3_SOLVER_H_ */