solver.h

/*
 * SPDX-FileCopyrightText: 2023 The P4 Language Consortium
 *
 * SPDX-License-Identifier: Apache-2.0
 */
 
#ifndef IR_SOLVER_H_
#define IR_SOLVER_H_
 
#include <optional>
#include <vector>
 
#include "ir/compare.h"
#include "ir/ir.h"
#include "lib/castable.h"
#include "lib/cstring.h"
#include "lib/flat_map.h"
 
namespace P4 {

// TODO: This should implement AbstractRepCheckedNode<Constraint>.
using Constraint = IR::Expression;

using SymbolicMapping =
    P4::flat_map<const IR::SymbolicVariable *, const IR::Expression *, IR::SymbolicVariableLess>;

class AbstractSolver : public ICastable {
 public:
    virtual void comment(cstring comment) = 0;

    virtual void seed(unsigned seed) = 0;

    virtual void timeout(unsigned tm) = 0;

    virtual std::optional<bool> checkSat(const std::vector<const Constraint *> &asserts) = 0;

    [[nodiscard]] virtual const SymbolicMapping &getSymbolicMapping() const = 0;

    virtual void toJSON(JSONGenerator &) const = 0;

    [[nodiscard]] virtual bool isInIncrementalMode() const = 0;
 
    DECLARE_TYPEINFO(AbstractSolver);
};
 
}  // namespace P4
 
#endif /* IR_SOLVER_H_ */