YicesSolver.h

Go to the documentation of this file.

#ifndef Rose_YicesSolver_H
#define Rose_YicesSolver_H

#include "SMTSolver.h"

#ifdef HAVE_LIBYICES
#  include <yices_c.h>
#endif

class YicesSolver: public SMTSolver {
public:
    enum LinkMode 
        {
        LM_NONE=0x0000,                         
        LM_LIBRARY=0x0001,                      
        LM_EXECUTABLE=0x0002                    
    };

    YicesSolver(): linkage(LM_NONE), context(NULL) {
        init();
    }
    virtual ~YicesSolver();

    virtual void generate_file(std::ostream&, const std::vector<InsnSemanticsExpr::TreeNodePtr> &exprs, Definitions*);
    virtual std::string get_command(const std::string &config_name);

    unsigned available_linkage() const;

    LinkMode get_linkage() const {
        return linkage;
    }

    void set_linkage(LinkMode lm) {
        ROSE_ASSERT(lm & available_linkage());
        linkage = lm;
    }

    virtual bool satisfiable(const std::vector<InsnSemanticsExpr::TreeNodePtr> &exprs);
    virtual bool satisfiable(const InsnSemanticsExpr::TreeNodePtr &tn) {
        std::vector<InsnSemanticsExpr::TreeNodePtr> exprs;
        exprs.push_back(tn);
        return satisfiable(exprs);
    }
    virtual InsnSemanticsExpr::TreeNodePtr get_definition(uint64_t varno);

    virtual InsnSemanticsExpr::TreeNodePtr get_definition(const InsnSemanticsExpr::LeafNodePtr &var) {
        assert(var!=NULL && !var->is_known());
        return get_definition(var->get_name());
    }
protected:
    virtual void parse_evidence();
    std::map<uint64_t/*varnum*/, std::pair<size_t/*nbits*/, uint64_t/*value*/> > evidence;

private:
    LinkMode linkage;
    void init();

    /* These out_*() functions convert a InsnSemanticsExpr expression into text which is suitable as input to "yices"
     * executable. */
    void out_define(std::ostream&, const InsnSemanticsExpr::TreeNodePtr&, Definitions*);
    void out_assert(std::ostream&, const InsnSemanticsExpr::TreeNodePtr&);
    void out_number(std::ostream&, const InsnSemanticsExpr::TreeNodePtr&);
    void out_expr(std::ostream&, const InsnSemanticsExpr::TreeNodePtr&);
    void out_unary(std::ostream&, const char *opname, const InsnSemanticsExpr::InternalNodePtr&);
    void out_binary(std::ostream&, const char *opname, const InsnSemanticsExpr::InternalNodePtr&);
    void out_ite(std::ostream&, const InsnSemanticsExpr::InternalNodePtr&);
    void out_la(std::ostream&, const char *opname, const InsnSemanticsExpr::InternalNodePtr&, bool identity_elmt);
    void out_la(std::ostream&, const char *opname, const InsnSemanticsExpr::InternalNodePtr&);
    void out_extract(std::ostream&, const InsnSemanticsExpr::InternalNodePtr&);
    void out_sext(std::ostream&, const InsnSemanticsExpr::InternalNodePtr&);
    void out_uext(std::ostream&, const InsnSemanticsExpr::InternalNodePtr&);
    void out_shift(std::ostream&, const char *opname, const InsnSemanticsExpr::InternalNodePtr&, bool newbits);
    void out_asr(std::ostream&, const InsnSemanticsExpr::InternalNodePtr&);
    void out_zerop(std::ostream&, const InsnSemanticsExpr::InternalNodePtr&);
    void out_mult(std::ostream &o, const InsnSemanticsExpr::InternalNodePtr&);

#ifdef HAVE_LIBYICES
    /* These ctx_*() functions build a Yices context object if Yices is linked into this executable. */
    typedef yices_expr (*UnaryAPI)(yices_context, yices_expr operand);
    typedef yices_expr (*BinaryAPI)(yices_context, yices_expr operand1, yices_expr operand2);
    typedef yices_expr (*NaryAPI)(yices_context, yices_expr *operands, unsigned n_operands);
    typedef yices_expr (*ShiftAPI)(yices_context, yices_expr, unsigned amount);

    yices_context context;
    void ctx_define(const InsnSemanticsExpr::TreeNodePtr&, Definitions*);
    void ctx_assert(const InsnSemanticsExpr::TreeNodePtr&);
    yices_expr ctx_expr(const InsnSemanticsExpr::TreeNodePtr&);
    yices_expr ctx_unary(UnaryAPI, const InsnSemanticsExpr::InternalNodePtr&);
    yices_expr ctx_binary(BinaryAPI, const InsnSemanticsExpr::InternalNodePtr&);
    yices_expr ctx_ite(const InsnSemanticsExpr::InternalNodePtr&);
    yices_expr ctx_la(BinaryAPI, const InsnSemanticsExpr::InternalNodePtr&, bool identity_elmt);
    yices_expr ctx_la(NaryAPI, const InsnSemanticsExpr::InternalNodePtr&, bool identity_elmt);
    yices_expr ctx_la(BinaryAPI, const InsnSemanticsExpr::InternalNodePtr&);
    yices_expr ctx_extract(const InsnSemanticsExpr::InternalNodePtr&);
    yices_expr ctx_sext(const InsnSemanticsExpr::InternalNodePtr&);
    yices_expr ctx_uext(const InsnSemanticsExpr::InternalNodePtr&);
    yices_expr ctx_shift(ShiftAPI, const InsnSemanticsExpr::InternalNodePtr&);
    yices_expr ctx_asr(const InsnSemanticsExpr::InternalNodePtr&);
    yices_expr ctx_zerop(const InsnSemanticsExpr::InternalNodePtr&);
    yices_expr ctx_mult(const InsnSemanticsExpr::InternalNodePtr&);
#else
    void *context; /*unused for now*/
#endif

};

#endif

---