SMTSolver.h

Go to the documentation of this file.

#ifndef Rose_SMTSolver_H
#define Rose_SMTSolver_H

#include "InsnSemanticsExpr.h"

class SMTSolver {
public:
    struct Exception {
        Exception(const std::string &mesg): mesg(mesg) {}
        friend std::ostream& operator<<(std::ostream&, const SMTSolver::Exception&);
        std::string mesg;
    };
    
    typedef std::set<uint64_t> Definitions;     
    SMTSolver(): debug(NULL) {}

    virtual ~SMTSolver() {}

    virtual bool satisfiable(const InsnSemanticsExpr::TreeNodePtr &expr);

    virtual bool satisfiable(const std::vector<InsnSemanticsExpr::TreeNodePtr> &exprs);

    virtual InsnSemanticsExpr::TreeNodePtr get_definition(uint64_t varno) {
        return InsnSemanticsExpr::TreeNodePtr();
    }
    virtual InsnSemanticsExpr::TreeNodePtr get_definition(const InsnSemanticsExpr::LeafNodePtr &var) {
        assert(var!=NULL && !var->is_known());
        return get_definition(var->get_name());
    }
    void set_debug(FILE *f) { debug = f; }

    FILE *get_debug() const { return debug; }

    static size_t get_ncalls() { return total_calls; }

protected:
    virtual void generate_file(std::ostream&, const std::vector<InsnSemanticsExpr::TreeNodePtr> &exprs,
                               Definitions*) = 0;

    virtual std::string get_command(const std::string &config_name) = 0;

    virtual void parse_evidence() {};

    std::vector<std::string> output_text;
    
    static size_t total_calls;

private:
    FILE *debug;
};

#endif

---