YicesSolver Class Reference

#include <YicesSolver.h>

Inheritance diagram for YicesSolver:

Inheritance graph
[legend]
Collaboration diagram for YicesSolver:

Collaboration graph
[legend]
List of all members.

Detailed Description

Interface to the Yices Satisfiability Modulo Theory (SMT) Solver.

ROSE should be configured with --with-yices in order for the satisfiable() virtual method to work (otherwise, the YicesSolver class is still available but will fail an assertion when instantiated).

Yices provides two interfaces: an executable named "yices", and a library. The choice of which linkage to use to answer satisfiability questions is made at runtime (see set_linkage()).


Public Types

 LM_NONE = 0x0000
 No available linkage.
 LM_LIBRARY = 0x0001
 The Yices runtime library is available.
 LM_EXECUTABLE = 0x0002
 The "yices" executable is available.
enum  LinkMode {
  LM_NONE = 0x0000,
  LM_LIBRARY = 0x0001,
  LM_EXECUTABLE = 0x0002
}
 Bit flags to indicate what style of calls are made to Yices. More...

Public Member Functions

 YicesSolver ()
 Constructor prefers to use the Yices executable interface.
virtual ~YicesSolver ()
virtual void generate_file (std::ostream &, const std::vector< const InsnSemanticsExpr::TreeNode * > &exprs, Definitions *)
virtual std::string get_command (const std::string &config_name)
 Given the name of a configuration file, return the command that is needed to run the solver.
unsigned available_linkage () const
 Returns a bit vector indicating what calling modes are available.
LinkMode get_linkage () const
 Returns the style of linkage currently enabled.
void set_linkage (LinkMode lm)
 Sets the linkage style.
virtual bool satisfiable (const std::vector< const InsnSemanticsExpr::TreeNode * > &exprs)
 Determines if the specified expression is satisfiable.
virtual bool satisfiable (const InsnSemanticsExpr::TreeNode *tn)
 Determines if the specified expression is satisfiable.
virtual InsnSemanticsExpr::TreeNode * get_definition (uint64_t varno)
 See SMTSolver::get_definition().
virtual InsnSemanticsExpr::TreeNode * get_definition (const InsnSemanticsExpr::LeafNode *var)
 See SMTSolver::get_definition().

Protected Member Functions

virtual void parse_evidence ()
 Parses evidence of satisfiability.

Protected Attributes

std::map< uint64_t, std::pair<
size_t, uint64_t > > 		evidence

Private Member Functions

void init ()
void out_define (std::ostream &, const InsnSemanticsExpr::TreeNode *, Definitions *)
 Traverse an expression and produce Yices "define" statements for variables.
void out_assert (std::ostream &, const InsnSemanticsExpr::TreeNode *)
 Generate a Yices "assert" statement for an expression.
void out_number (std::ostream &, const InsnSemanticsExpr::TreeNode *)
 Output a decimal number.
void out_expr (std::ostream &, const InsnSemanticsExpr::TreeNode *)
 Output for one expression.
void out_unary (std::ostream &, const char *opname, const InsnSemanticsExpr::InternalNode *)
 Output for unary operators.
void out_binary (std::ostream &, const char *opname, const InsnSemanticsExpr::InternalNode *)
 Output for binary operators.
void out_ite (std::ostream &, const InsnSemanticsExpr::InternalNode *)
void out_la (std::ostream &, const char *opname, const InsnSemanticsExpr::InternalNode *, bool identity_elmt)
void out_la (std::ostream &, const char *opname, const InsnSemanticsExpr::InternalNode *)
void out_extract (std::ostream &, const InsnSemanticsExpr::InternalNode *)
void out_sext (std::ostream &, const InsnSemanticsExpr::InternalNode *)
void out_uext (std::ostream &, const InsnSemanticsExpr::InternalNode *)
void out_shift (std::ostream &, const char *opname, const InsnSemanticsExpr::InternalNode *, bool newbits)
void out_asr (std::ostream &, const InsnSemanticsExpr::InternalNode *)
void out_zerop (std::ostream &, const InsnSemanticsExpr::InternalNode *)
 Output for if-then-else operator.
void out_mult (std::ostream &o, const InsnSemanticsExpr::InternalNode *in)
 Output for multiply.

Private Attributes

LinkMode linkage
void * context

Member Enumeration Documentation

enum YicesSolver::LinkMode

Bit flags to indicate what style of calls are made to Yices.

Enumerator:
LM_NONE  No available linkage.
LM_LIBRARY  The Yices runtime library is available.
LM_EXECUTABLE  The "yices" executable is available.

Constructor & Destructor Documentation

YicesSolver::YicesSolver (  )  [inline]

Constructor prefers to use the Yices executable interface.

See set_linkage().

YicesSolver::~YicesSolver (  )  [virtual]

Member Function Documentation

void YicesSolver::generate_file ( std::ostream &  ,
const std::vector< const InsnSemanticsExpr::TreeNode * > &  exprs,
Definitions *   
) [virtual]

std::string YicesSolver::get_command ( const std::string &  config_name  )  [virtual]

Given the name of a configuration file, return the command that is needed to run the solver.

The first line of stdout emitted by the solver should be the word "sat" or "unsat".

Implements SMTSolver.

unsigned YicesSolver::available_linkage (  )  const

Returns a bit vector indicating what calling modes are available.

The bits are defined by the LinkMode enum.

LinkMode YicesSolver::get_linkage (  )  const [inline]

Returns the style of linkage currently enabled.

void YicesSolver::set_linkage ( LinkMode  lm  )  [inline]

Sets the linkage style.

bool YicesSolver::satisfiable ( const std::vector< const InsnSemanticsExpr::TreeNode * > &  exprs  )  [virtual]

Determines if the specified expression is satisfiable.

Most solvers use the implementation in the base class, which creates a text file (usually in SMT-LIB format) and then invokes an executable with that input, looking for a line of output containing "sat" or "unsat". However, Yices provides a library that can optionally be linked into ROSE, and uses this library if the link mode is LM_LIBRARY.

Reimplemented from SMTSolver.

virtual bool YicesSolver::satisfiable ( const InsnSemanticsExpr::TreeNode *  tn  )  [inline, virtual]

Determines if the specified expression is satisfiable.

Most solvers use the implementation in the base class, which creates a text file (usually in SMT-LIB format) and then invokes an executable with that input, looking for a line of output containing "sat" or "unsat". However, Yices provides a library that can optionally be linked into ROSE, and uses this library if the link mode is LM_LIBRARY.

Reimplemented from SMTSolver.

InsnSemanticsExpr::TreeNode * YicesSolver::get_definition ( uint64_t  varno  )  [virtual]

See SMTSolver::get_definition().

Reimplemented from SMTSolver.

virtual InsnSemanticsExpr::TreeNode* YicesSolver::get_definition ( const InsnSemanticsExpr::LeafNode *  var  )  [inline, virtual]

See SMTSolver::get_definition().

Reimplemented from SMTSolver.

void YicesSolver::parse_evidence (  )  [protected, virtual]

Parses evidence of satisfiability.

Some solvers can emit information about what variable bindings satisfy the expression. This information is parsed by this function and added to a mapping of variable to value.

Reimplemented from SMTSolver.

void YicesSolver::init (  )  [private]

void YicesSolver::out_define ( std::ostream &  ,
const InsnSemanticsExpr::TreeNode *  ,
Definitions *   
) [private]

Traverse an expression and produce Yices "define" statements for variables.

void YicesSolver::out_assert ( std::ostream &  ,
const InsnSemanticsExpr::TreeNode *   
) [private]

Generate a Yices "assert" statement for an expression.

void YicesSolver::out_number ( std::ostream &  ,
const InsnSemanticsExpr::TreeNode *   
) [private]

Output a decimal number.

void YicesSolver::out_expr ( std::ostream &  ,
const InsnSemanticsExpr::TreeNode *   
) [private]

Output for one expression.

void YicesSolver::out_unary ( std::ostream &  ,
const char *  opname,
const InsnSemanticsExpr::InternalNode *   
) [private]

Output for unary operators.

void YicesSolver::out_binary ( std::ostream &  ,
const char *  opname,
const InsnSemanticsExpr::InternalNode *   
) [private]

Output for binary operators.

void YicesSolver::out_ite ( std::ostream &  ,
const InsnSemanticsExpr::InternalNode *   
) [private]

void YicesSolver::out_la ( std::ostream &  ,
const char *  opname,
const InsnSemanticsExpr::InternalNode *  ,
bool  identity_elmt 
) [private]

void YicesSolver::out_la ( std::ostream &  ,
const char *  opname,
const InsnSemanticsExpr::InternalNode *   
) [private]

void YicesSolver::out_extract ( std::ostream &  ,
const InsnSemanticsExpr::InternalNode *   
) [private]

void YicesSolver::out_sext ( std::ostream &  ,
const InsnSemanticsExpr::InternalNode *   
) [private]

void YicesSolver::out_uext ( std::ostream &  ,
const InsnSemanticsExpr::InternalNode *   
) [private]

void YicesSolver::out_shift ( std::ostream &  ,
const char *  opname,
const InsnSemanticsExpr::InternalNode *  ,
bool  newbits 
) [private]

void YicesSolver::out_asr ( std::ostream &  ,
const InsnSemanticsExpr::InternalNode *   
) [private]

void YicesSolver::out_zerop ( std::ostream &  o,
const InsnSemanticsExpr::InternalNode *  in 
) [private]

Output for if-then-else operator.

The condition must be cast from a 1-bit vector to a number, therefore, the input 

      (OP_ITE COND S1 S2)

will be rewritten as 

      (ite (= COND 0b1) S1 S2)
  \code
 */
void
YicesSolver::out_ite(std::ostream &o, const InsnSemanticsExpr::InternalNode *in)
{
    assert(in && 3==in->size());
    assert(in->child(0)->get_nbits()==1);
    o <<"(ite (=";
    out_expr(o, in->child(0));
    o <<" 0b1)";
    for (size_t i=1; i<3; i++) {
        o <<" ";
        out_expr(o, in->child(i));
    }
    o <<")";
}

void
YicesSolver::out_la(std::ostream &o, const char *opname, const InsnSemanticsExpr::InternalNode *in, bool identity_element)
{
    assert(opname && *opname);
    assert(in && in->size()>=1);

    for (size_t i=1; i<std::max((size_t)2, in->size()); i++)
        o <<"(" <<opname <<" ";
    out_expr(o, in->child(0));

    if (in->size()>1) {
        for (size_t i=1; i<in->size(); i++) {
            o <<" ";
            out_expr(o, in->child(i));
            o <<")";
        }
    } else {
        InsnSemanticsExpr::LeafNode *ident = InsnSemanticsExpr::LeafNode::create_integer(in->child(0)->get_nbits(),
                                                                                         identity_element ? (uint64_t)(-1) : 0);
        out_expr(o, ident);
        o <<")";
    }
}

void
YicesSolver::out_la(std::ostream &o, const char *opname, const InsnSemanticsExpr::InternalNode *in)
{
    if (in->size()==1) {
        out_unary(o, opname, in);
    } else {
        out_la(o, opname, in, false);
    }
}

void
YicesSolver::out_extract(std::ostream &o, const InsnSemanticsExpr::InternalNode *in)
{
    assert(in && 3==in->size());
    assert(in->child(0)->is_known());
    assert(in->child(1)->is_known());
    assert(in->child(0)->get_value() < in->child(1)->get_value());
    size_t lo = in->child(0)->get_value();
    size_t hi = in->child(1)->get_value() - 1;          /*inclusive*/
    o <<"(bv-extract " <<hi <<" " <<lo <<" ";
    out_expr(o, in->child(2));
    o <<")";
}

void
YicesSolver::out_sext(std::ostream &o, const InsnSemanticsExpr::InternalNode *in)
{
    assert(in && 2==in->size());
    assert(in->child(0)->is_known()); /*Yices bv-sign-extend needs a number for the second operand*/
    assert(in->child(0)->get_value() > in->child(1)->get_nbits());
    size_t extend_by = in->child(0)->get_value() - in->child(1)->get_nbits();
    o <<"(bv-sign-extend  ";
    out_expr(o, in->child(1)); /*vector*/
    o <<" " <<extend_by <<")";
}

void
YicesSolver::out_uext(std::ostream &o, const InsnSemanticsExpr::InternalNode *in)
{
    using namespace InsnSemanticsExpr;
    assert(in && 2==in->size());
    assert(in->child(0)->is_known()); /*Yices mk-bv needs a number for the size operand*/
    assert(in->child(0)->get_value() > in->child(1)->get_nbits());
    size_t extend_by = in->child(0)->get_value() - in->child(1)->get_nbits();

    o <<"(bv-concat (mk-bv " <<extend_by <<" 0) ";
    out_expr(o, in->child(1));
    o <<")";
}

void
YicesSolver::out_shift(std::ostream &o, const char *opname, const InsnSemanticsExpr::InternalNode *in, bool newbits)
{
    assert(opname && *opname);
    assert(in && 2==in->size());
    assert(in->child(0)->is_known()); /*Yices' bv-shift-* operators need a constant for the shift amount*/

    o <<"(" <<opname <<(newbits?"1":"0") <<" ";
    out_expr(o, in->child(1));
    o <<" " <<in->child(0)->get_value() <<")";
}

void
YicesSolver::out_asr(std::ostream &o, const InsnSemanticsExpr::InternalNode *in)
{
    assert(in && 2==in->size());
    const InsnSemanticsExpr::TreeNode *vector = in->child(1);
    uint64_t vector_size = vector->get_nbits();
    assert(in->child(0)->is_known());
    uint64_t shift_amount = in->child(0)->get_value();

    o <<"(ite (= (mk-bv 1 1) (bv-extract " <<(vector_size-1) <<" " <<(vector_size-1) <<" ";
    out_expr(o, vector);
    o <<")) (bv-shift-right1 ";
    out_expr(o, vector);
    o <<" " <<shift_amount <<") (bv-shift-right0 ";
    out_expr(o, vector);
    o <<" " <<shift_amount <<"))";
}

becomes 

      (ite (= (mk-bv [sizeof(X)] 0) [X]) 0b1 0b0)

void YicesSolver::out_mult ( std::ostream &  o,
const InsnSemanticsExpr::InternalNode *  in 
) [private]

Output for multiply.

The OP_SMUL and OP_UMUL nodes of InsnSemanticsExpr define the result width to be the sum of the input widths. Yices' bv-mul operator requires that both operands are the same size and the result is the size of each operand. Therefore, we rewrite (OP_SMUL A B) to become, in Yices: 

    (bv-mul (bv-sign-extend A [|B|-1]) (bv-sign-extend B [|A|-1]))

Member Data Documentation

std::map<uint64_t, std::pair<size_t, uint64_t> > YicesSolver::evidence [protected]

LinkMode YicesSolver::linkage [private]

void* YicesSolver::context [private]

The documentation for this class was generated from the following files:
Generated on Tue Jan 31 05:45:05 2012 for ROSE by  doxygen 1.4.7