solver.h

#ifndef IR_SOLVER_H_
#define IR_SOLVER_H_
 
#include <optional>
#include <vector>
 
#include <boost/container/flat_map.hpp>
#include <boost/container/flat_set.hpp>
 
#include "ir/ir.h"
#include "lib/castable.h"
#include "lib/cstring.h"
 
// TODO: This should implement AbstractRepCheckedNode<Constraint>.
using Constraint = IR::Expression;
 
struct SymbolicVarComp {
    bool operator()(const IR::SymbolicVariable *s1, const IR::SymbolicVariable *s2) const {
        return s1->operator<(*s2);
    }
};
 
using SymbolicMapping = boost::container::flat_map<const IR::SymbolicVariable *,
                                                   const IR::Expression *, SymbolicVarComp>;
 
using SymbolicSet = boost::container::flat_set<const IR::SymbolicVariable *, SymbolicVarComp>;
 
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);
};
 
#endif /* IR_SOLVER_H_ */