solver.h

#ifndef IR_SOLVER_H_
#define IR_SOLVER_H_
 
#include <optional>
#include <vector>
 
#include "absl/container/btree_map.h"
#include "ir/compare.h"
#include "ir/ir.h"
#include "lib/castable.h"
#include "lib/cstring.h"
 
// TODO: This should implement AbstractRepCheckedNode<Constraint>.
using Constraint = IR::Expression;
 
using SymbolicMapping =
    absl::btree_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);
};
 
#endif /* IR_SOLVER_H_ */