/*
 * MetaSMTBuilder.h
 *
 *  Created on: 8 Aug 2012
 *      Author: hpalikar
 */

#ifndef METASMTBUILDER_H_
#define METASMTBUILDER_H_

#include "klee/Config/config.h"
#include "klee/Expr.h"
#include "klee/util/ExprPPrinter.h"
#include "klee/util/ArrayExprHash.h"
#include "klee/util/ExprHashMap.h"
#include "ConstantDivision.h"

#ifdef SUPPORT_METASMT

#include "llvm/Support/CommandLine.h"

#include <metaSMT/frontend/Logic.hpp>
#include <metaSMT/frontend/QF_BV.hpp>
#include <metaSMT/frontend/Array.hpp>
#include <metaSMT/support/default_visitation_unrolling_limit.hpp>
#include <metaSMT/support/run_algorithm.hpp>

#define Expr VCExpr
#define STP STP_Backend
#include <metaSMT/backend/STP.hpp>
#undef Expr
#undef STP
 
#include <boost/mpl/vector.hpp>
#include <boost/format.hpp>

using namespace metaSMT;
using namespace metaSMT::logic::QF_BV;


#define DIRECT_CONTEXT

namespace {
  llvm::cl::opt<bool>
  UseConstructHashMetaSMT("use-construct-hash-metasmt", 
                   llvm::cl::desc("Use hash-consing during metaSMT query construction."),
                   llvm::cl::init(true));
}


namespace klee {

typedef metaSMT::logic::Predicate<proto::terminal<metaSMT::logic::tag::true_tag>::type  > const MetaSMTConstTrue;
typedef metaSMT::logic::Predicate<proto::terminal<metaSMT::logic::tag::false_tag>::type  > const MetaSMTConstFalse;
typedef metaSMT::logic::Array::array MetaSMTArray;

template<typename SolverContext>
class MetaSMTBuilder;

template<typename SolverContext>
class MetaSMTArrayExprHash : public ArrayExprHash< typename SolverContext::result_type > {
    
    friend class MetaSMTBuilder<SolverContext>;
    
public:
    MetaSMTArrayExprHash() {};
    virtual ~MetaSMTArrayExprHash() {};
};

static const bool mimic_stp = true;


template<typename SolverContext>
class MetaSMTBuilder {
public:

    MetaSMTBuilder(SolverContext& solver, bool optimizeDivides) : _solver(solver), _optimizeDivides(optimizeDivides) { };
    virtual ~MetaSMTBuilder() {};
    
    typename SolverContext::result_type construct(ref<Expr> e);
    
    typename SolverContext::result_type getInitialRead(const Array *root, unsigned index);
    
    typename SolverContext::result_type getTrue() {
        return(evaluate(_solver, metaSMT::logic::True));        
    }
    
    typename SolverContext::result_type getFalse() {        
        return(evaluate(_solver, metaSMT::logic::False));        
    }
    
    typename SolverContext::result_type bvOne(unsigned width) {
        return bvZExtConst(width, 1);
    }
    
    typename SolverContext::result_type bvZero(unsigned width) {
        return bvZExtConst(width, 0);
    }
    
    typename SolverContext::result_type bvMinusOne(unsigned width) {
        return bvSExtConst(width, (int64_t) -1);
    }
    
    typename SolverContext::result_type bvConst32(unsigned width, uint32_t value) {
        return(evaluate(_solver, bvuint(value, width)));
    }
    
    typename SolverContext::result_type bvConst64(unsigned width, uint64_t value) {
         return(evaluate(_solver, bvuint(value, width)));
    }
       
    typename SolverContext::result_type bvZExtConst(unsigned width, uint64_t value);    
    typename SolverContext::result_type bvSExtConst(unsigned width, uint64_t value);
    
    //logical left and right shift (not arithmetic)
    typename SolverContext::result_type bvLeftShift(typename SolverContext::result_type expr, unsigned width, unsigned shift, unsigned shiftBits);
    typename SolverContext::result_type bvRightShift(typename SolverContext::result_type expr, unsigned width, unsigned amount, unsigned shiftBits);
    typename SolverContext::result_type bvVarLeftShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width);
    typename SolverContext::result_type bvVarRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width);
    typename SolverContext::result_type bvVarArithRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width);
    
    
    typename SolverContext::result_type getArrayForUpdate(const Array *root, const UpdateNode *un);
    typename SolverContext::result_type getInitialArray(const Array *root);
    MetaSMTArray buildArray(unsigned elem_width, unsigned index_width);
        
private:
    typedef ExprHashMap< std::pair<typename SolverContext::result_type, unsigned> >  MetaSMTExprHashMap;
    typedef typename MetaSMTExprHashMap::iterator MetaSMTExprHashMapIter;
    typedef typename MetaSMTExprHashMap::const_iterator MetaSMTExprHashMapConstIter;    

    SolverContext&  _solver;
    bool _optimizeDivides;
    MetaSMTArrayExprHash<SolverContext>  _arr_hash;
    MetaSMTExprHashMap                   _constructed;
    
    typename SolverContext::result_type constructActual(ref<Expr> e, int *width_out);
    typename SolverContext::result_type construct(ref<Expr> e, int *width_out);
    
    typename SolverContext::result_type bvBoolExtract(typename SolverContext::result_type expr, int bit);
    typename SolverContext::result_type bvExtract(typename SolverContext::result_type expr, unsigned top, unsigned bottom);
    typename SolverContext::result_type eqExpr(typename SolverContext::result_type a, typename SolverContext::result_type b);
    
    typename SolverContext::result_type constructAShrByConstant(typename SolverContext::result_type expr, unsigned width, unsigned shift, 
                                                                typename SolverContext::result_type isSigned, unsigned shiftBits);
    typename SolverContext::result_type constructMulByConstant(typename SolverContext::result_type expr, unsigned width, uint64_t x);
    typename SolverContext::result_type constructUDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d);
    typename SolverContext::result_type constructSDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d);
    
    unsigned getShiftBits(unsigned amount) {
        unsigned bits = 1;
        amount--;
        while (amount >>= 1) {
            bits++;
        }
        return(bits);
    }
};

template<typename SolverContext>
typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getArrayForUpdate(const Array *root, const UpdateNode *un) {
  
    if (!un) {
        return(getInitialArray(root));
    }
    else {
        typename SolverContext::result_type un_expr;
        bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr);

        if (!hashed) {
            un_expr = evaluate(_solver,
                               metaSMT::logic::Array::store(getArrayForUpdate(root, un->next),
                                                            construct(un->index, 0),
                                                            construct(un->value, 0)));
            _arr_hash.hashUpdateNodeExpr(un, un_expr);
        }
        return(un_expr);
    }
}

template<typename SolverContext>
typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getInitialArray(const Array *root)
{
    assert(root);
    typename SolverContext::result_type array_expr;
    bool hashed = _arr_hash.lookupArrayExpr(root, array_expr);

    if (!hashed) {

        array_expr = evaluate(_solver, buildArray(8, 32));	

        if (root->isConstantArray()) {    
            for (unsigned i = 0, e = root->size; i != e; ++i) {
                 typename SolverContext::result_type tmp =
                            evaluate(_solver, 
                                     metaSMT::logic::Array::store(array_expr,
                                                                  construct(ConstantExpr::alloc(i, root->getDomain()), 0),
                                                                  construct(root->constantValues[i], 0)));
                array_expr = tmp;
            }
        }
        _arr_hash.hashArrayExpr(root, array_expr);
    }

    return(array_expr);
}

template<typename SolverContext>
MetaSMTArray MetaSMTBuilder<SolverContext>::buildArray(unsigned elem_width, unsigned index_width) {
    return(metaSMT::logic::Array::new_array(elem_width, index_width));
}

template<typename SolverContext>
typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getInitialRead(const Array *root, unsigned index) {
    assert(root); 
    assert(false);
    typename SolverContext::result_type array_exp = getInitialArray(root);
    typename SolverContext::result_type res = evaluate(
                        _solver,
                        metaSMT::logic::Array::select(array_exp, bvuint(index, root->getDomain())));    
    return(res);
}


template<typename SolverContext>  
typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvZExtConst(unsigned width, uint64_t value) {

    typename SolverContext::result_type res;

    if (width <= 64) {
        res = bvConst64(width, value);
    }
    else {
        typename SolverContext::result_type expr = bvConst64(64, value);
        typename SolverContext::result_type zero = bvConst64(64, 0);

        for (width -= 64; width > 64; width -= 64) {
             expr = evaluate(_solver, concat(zero, expr));  
        }
        res = evaluate(_solver, concat(bvConst64(width, 0), expr));  
    }

    return(res); 
}

template<typename SolverContext>  
typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvSExtConst(unsigned width, uint64_t value) {
  
  typename SolverContext::result_type res;
  
  if (width <= 64) {
      res = bvConst64(width, value); 
  }
  else {            
      // ToDo Reconsider -- note differences in STP and metaSMT for sign_extend arguments
      res = evaluate(_solver, sign_extend(width - 64, bvConst64(64, value)));		     
  }
  return(res); 
}

template<typename SolverContext>
typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvBoolExtract(typename SolverContext::result_type expr, int bit) {
    return(evaluate(_solver,
                    metaSMT::logic::equal(extract(bit, bit, expr),
                                          bvOne(1))));
}

template<typename SolverContext>
typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvExtract(typename SolverContext::result_type expr, unsigned top, unsigned bottom) {    
    return(evaluate(_solver, extract(top, bottom, expr)));
}

template<typename SolverContext>
typename SolverContext::result_type MetaSMTBuilder<SolverContext>::eqExpr(typename SolverContext::result_type a, typename SolverContext::result_type b) {    
    return(evaluate(_solver, metaSMT::logic::equal(a, b)));
}

template<typename SolverContext>
typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructAShrByConstant(typename SolverContext::result_type expr, unsigned width, unsigned amount,
                                                                                           typename SolverContext::result_type isSigned, unsigned shiftBits) {
    unsigned shift = amount & ((1 << shiftBits) - 1);
    typename SolverContext::result_type res;
    
    if (shift == 0) {
        res = expr;
    }
    else if (shift >= width - 1) {
        res = evaluate(_solver, metaSMT::logic::Ite(isSigned, bvMinusOne(width), bvZero(width)));
    }
    else {
        res = evaluate(_solver, metaSMT::logic::Ite(isSigned,
                                                    concat(bvMinusOne(shift), bvExtract(expr, width - 1, shift)),
                                                    bvRightShift(expr, width, shift, shiftBits)));
    }
    
    return(res);
}

// width is the width of expr; x -- number of bits to shift with
template<typename SolverContext>
typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructMulByConstant(typename SolverContext::result_type expr, unsigned width, uint64_t x) {
    
    unsigned shiftBits = getShiftBits(width);
    uint64_t add, sub;
    typename SolverContext::result_type res;
    bool first = true;

    // expr*x == expr*(add-sub) == expr*add - expr*sub
    ComputeMultConstants64(x, add, sub);

    // legal, these would overflow completely
    add = bits64::truncateToNBits(add, width);
    sub = bits64::truncateToNBits(sub, width);
    
    for (int j = 63; j >= 0; j--) {
        uint64_t bit = 1LL << j;

        if ((add & bit) || (sub & bit)) {
            assert(!((add & bit) && (sub & bit)) && "invalid mult constants");

            typename SolverContext::result_type op = bvLeftShift(expr, width, j, shiftBits);

            if (add & bit) {
                if (!first) {
                    res = evaluate(_solver, bvadd(res, op));
                } else {
                    res = op;
                    first = false;
                }
            } else {
                if (!first) {
                    res = evaluate(_solver, bvsub(res, op));                    
                } else {
                     // To reconsider: vc_bvUMinusExpr in STP
                    res = evaluate(_solver, bvsub(bvZero(width), op));
                    first = false;
                }
            }
        }
    }
  
    if (first) { 
        res = bvZero(width);
    }

    return(res);
}


/* 
 * Compute the 32-bit unsigned integer division of n by a divisor d based on 
 * the constants derived from the constant divisor d.
 *
 * Returns n/d without doing explicit division.  The cost is 2 adds, 3 shifts, 
 * and a (64-bit) multiply.
 *
 * @param expr_n numerator (dividend) n as an expression
 * @param width  number of bits used to represent the value
 * @param d      the divisor
 *
 * @return n/d without doing explicit division
 */
template<typename SolverContext>
typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructUDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d) {
    
    assert(width == 32 && "can only compute udiv constants for 32-bit division");
    
    // Compute the constants needed to compute n/d for constant d without division by d.
    uint32_t mprime, sh1, sh2;
    ComputeUDivConstants32(d, mprime, sh1, sh2);
    typename SolverContext::result_type expr_sh1 = bvConst32(32, sh1);
    typename SolverContext::result_type expr_sh2 = bvConst32(32, sh2);
    
    // t1  = MULUH(mprime, n) = ( (uint64_t)mprime * (uint64_t)n ) >> 32
    typename SolverContext::result_type expr_n_64 = evaluate(_solver, concat(bvZero(32), expr_n)); //extend to 64 bits
    typename SolverContext::result_type t1_64bits = constructMulByConstant(expr_n_64, 64, (uint64_t)mprime);
    typename SolverContext::result_type t1        = bvExtract(t1_64bits, 63, 32); //upper 32 bits
    
    // n/d = (((n - t1) >> sh1) + t1) >> sh2;
    typename SolverContext::result_type n_minus_t1 = evaluate(_solver, bvsub(expr_n, t1));   
    typename SolverContext::result_type shift_sh1  = bvVarRightShift(n_minus_t1, expr_sh1, 32);
    typename SolverContext::result_type plus_t1    = evaluate(_solver, bvadd(shift_sh1, t1));    
    typename SolverContext::result_type res        = bvVarRightShift(plus_t1, expr_sh2, 32);
    
    return(res);
}

/* 
 * Compute the 32-bitnsigned integer division of n by a divisor d based on 
 * the constants derived from the constant divisor d.
 *
 * Returns n/d without doing explicit division.  The cost is 3 adds, 3 shifts, 
 * a (64-bit) multiply, and an XOR.
 *
 * @param n      numerator (dividend) as an expression
 * @param width  number of bits used to represent the value
 * @param d      the divisor
 *
 * @return n/d without doing explicit division
 */
template<typename SolverContext>
typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructSDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d) {
    
    assert(width == 32 && "can only compute udiv constants for 32-bit division");

    // Compute the constants needed to compute n/d for constant d w/o division by d.
    int32_t mprime, dsign, shpost;
    ComputeSDivConstants32(d, mprime, dsign, shpost);
    typename SolverContext::result_type expr_dsign  = bvConst32(32, dsign);
    typename SolverContext::result_type expr_shpost = bvConst32(32, shpost);
    
    // q0 = n + MULSH( mprime, n ) = n + (( (int64_t)mprime * (int64_t)n ) >> 32)
    int64_t mprime_64     = (int64_t)mprime;
    
    // ToDo Reconsider -- note differences in STP and metaSMT for sign_extend arguments
    typename SolverContext::result_type expr_n_64    = evaluate(_solver, sign_extend(64 - width, expr_n));    
    typename SolverContext::result_type mult_64      = constructMulByConstant(expr_n_64, 64, mprime_64);
    typename SolverContext::result_type mulsh        = bvExtract(mult_64, 63, 32); //upper 32-bits    
    typename SolverContext::result_type n_plus_mulsh = evaluate(_solver, bvadd(expr_n, mulsh));
    
    // Improved variable arithmetic right shift: sign extend, shift, extract.
    typename SolverContext::result_type extend_npm   = evaluate(_solver, sign_extend(64 - width, n_plus_mulsh));    
    typename SolverContext::result_type shift_npm    = bvVarRightShift(extend_npm, expr_shpost, 64);
    typename SolverContext::result_type shift_shpost = bvExtract(shift_npm, 31, 0); //lower 32-bits
    
    /////////////
    
    // XSIGN(n) is -1 if n is negative, positive one otherwise
    typename SolverContext::result_type is_signed    = bvBoolExtract(expr_n, 31);
    typename SolverContext::result_type neg_one      = bvMinusOne(32);
    typename SolverContext::result_type xsign_of_n   = evaluate(_solver, metaSMT::logic::Ite(is_signed, neg_one, bvZero(32)));    

    // q0 = (n_plus_mulsh >> shpost) - XSIGN(n)
    typename SolverContext::result_type q0           = evaluate(_solver, bvsub(shift_shpost, xsign_of_n));    
  
    // n/d = (q0 ^ dsign) - dsign
    typename SolverContext::result_type q0_xor_dsign = evaluate(_solver, bvxor(q0, expr_dsign));    
    typename SolverContext::result_type res          = evaluate(_solver, bvsub(q0_xor_dsign, expr_dsign));    
    
    return(res);
}

template<typename SolverContext>
typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvLeftShift(typename SolverContext::result_type expr, unsigned width, unsigned amount, unsigned shiftBits) {
    
    typename SolverContext::result_type res;    
    unsigned shift = amount & ((1 << shiftBits) - 1);

    if (shift == 0) {
        res = expr;
    }
    else if (shift >= width) {
        res = bvZero(width);
    }
    else {
        // stp shift does "expr @ [0 x s]" which we then have to extract,
        // rolling our own gives slightly smaller exprs
        res = evaluate(_solver, concat(extract(width - shift - 1, 0, expr),
                                       bvZero(shift)));
    }

    return(res);
}

template<typename SolverContext>
typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvRightShift(typename SolverContext::result_type expr, unsigned width, unsigned amount, unsigned shiftBits) {
  
    typename SolverContext::result_type res;    
    unsigned shift = amount & ((1 << shiftBits) - 1);

    if (shift == 0) {
        res = expr;
    } 
    else if (shift >= width) {
        res = bvZero(width);
    }
    else {
        res = evaluate(_solver, concat(bvZero(shift),
                                       extract(width - 1, shift, expr)));        
    }

    return(res);
}

// left shift by a variable amount on an expression of the specified width
template<typename SolverContext>
typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarLeftShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width) {
    
    typename SolverContext::result_type res =  bvZero(width);
    
    int shiftBits = getShiftBits(width);

    //get the shift amount (looking only at the bits appropriate for the given width)
    typename SolverContext::result_type shift = evaluate(_solver, extract(shiftBits - 1, 0, amount));    

    //construct a big if-then-elif-elif-... with one case per possible shift amount
    for(int i = width - 1; i >= 0; i--) {
        res = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(shiftBits, i)),
                                                    bvLeftShift(expr, width, i, shiftBits),
                                                    res));
    }

    return(res);
}

// logical right shift by a variable amount on an expression of the specified width
template<typename SolverContext>
typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width) {
    
    typename SolverContext::result_type res = bvZero(width);
    
    int shiftBits = getShiftBits(width);
    
    //get the shift amount (looking only at the bits appropriate for the given width)
    typename SolverContext::result_type shift = bvExtract(amount, shiftBits - 1, 0);
    
    //construct a big if-then-elif-elif-... with one case per possible shift amount
    for (int i = width - 1; i >= 0; i--) {
        res = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(shiftBits, i)),
                                                    bvRightShift(expr, width, i, shiftBits),
                                                    res));
         // ToDo Reconsider widht to provide to bvRightShift
    }

    return(res);
}

// arithmetic right shift by a variable amount on an expression of the specified width
template<typename SolverContext>
typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarArithRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width) {
  
    int shiftBits = getShiftBits(width);

    //get the shift amount (looking only at the bits appropriate for the given width)
    typename SolverContext::result_type shift = bvExtract(amount, shiftBits - 1, 0);
    
    //get the sign bit to fill with
    typename SolverContext::result_type signedBool = bvBoolExtract(expr, width - 1);

    //start with the result if shifting by width-1
    typename SolverContext::result_type res =  constructAShrByConstant(expr, width, width - 1, signedBool, shiftBits);

    // construct a big if-then-elif-elif-... with one case per possible shift amount
    // XXX more efficient to move the ite on the sign outside all exprs?
    // XXX more efficient to sign extend, right shift, then extract lower bits?
    for (int i = width - 2; i >= 0; i--) {
        res = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(shiftBits,i)),
                                                    constructAShrByConstant(expr, width, i, signedBool, shiftBits),
                                                    res));
    }

    return(res);
}

template<typename SolverContext>
typename SolverContext::result_type MetaSMTBuilder<SolverContext>::construct(ref<Expr> e) {
    typename SolverContext::result_type res = construct(e, 0);
    _constructed.clear();
    return res;
}


/** if *width_out!=1 then result is a bitvector,
    otherwise it is a bool */
template<typename SolverContext>
typename SolverContext::result_type MetaSMTBuilder<SolverContext>::construct(ref<Expr> e, int *width_out) {
  
    if (!UseConstructHashMetaSMT || isa<ConstantExpr>(e)) {
        return(constructActual(e, width_out));
    } else {
        MetaSMTExprHashMapIter it = _constructed.find(e);
        if (it != _constructed.end()) {
            if (width_out) {
                *width_out = it->second.second;
            }
            return it->second.first;
        } else {
            int width = 0;
            if (!width_out) {
                 width_out = &width;
            }
            typename SolverContext::result_type res = constructActual(e, width_out);
            _constructed.insert(std::make_pair(e, std::make_pair(res, *width_out)));
            return res;
        }
    }
}

template<typename SolverContext>
typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActual(ref<Expr> e, int *width_out)  {

    typename SolverContext::result_type res;
    
    int width = 0;
    if (!width_out) { 
        // assert(false);
        width_out = &width;
    }
    
    ++stats::queryConstructs;
    
//     std::cerr << "Constructing expression ";
//     ExprPPrinter::printSingleExpr(std::cerr, e);
//     std::cerr << "\n";

    switch (e->getKind()) {    

        case Expr::Constant:
        {
            ConstantExpr *coe = cast<ConstantExpr>(e);
            assert(coe);
            unsigned coe_width = coe->getWidth();
            *width_out = coe_width;

            // Coerce to bool if necessary.
            if (coe_width == 1) {
                res = (coe->isTrue()) ? getTrue() : getFalse();      
            }
            else if (coe_width <= 32) {
                 res = bvConst32(coe_width, coe->getZExtValue(32));
            }
            else if (coe_width <= 64) {
                 res = bvConst64(coe_width, coe->getZExtValue());
            }
            else {
                 ref<ConstantExpr> tmp = coe;
                 res = bvConst64(64, tmp->Extract(0, 64)->getZExtValue());                 
                 while (tmp->getWidth() > 64) {
                     tmp = tmp->Extract(64, tmp->getWidth() -  64);
                     unsigned min_width = std::min(64U, tmp->getWidth());
                     res = evaluate(_solver,
                                    concat(bvConst64(min_width, tmp->Extract(0, min_width)->getZExtValue()),
                                           res));
                 }
            }
            break;
        }

        case Expr::NotOptimized:
        { 
            NotOptimizedExpr *noe = cast<NotOptimizedExpr>(e);
            assert(noe);
            res = construct(noe->src, width_out);
            break;
        }
	
        case Expr::Select: 
        {
            SelectExpr *se = cast<SelectExpr>(e);
            assert(se);
            res = evaluate(_solver, 
                           metaSMT::logic::Ite(construct(se->cond, 0), 
                                               construct(se->trueExpr, width_out),
                                               construct(se->falseExpr, width_out)));
            break;
        }

        case Expr::Read:
        {
            ReadExpr *re = cast<ReadExpr>(e);
            assert(re);
            // FixMe call method of Array
            *width_out = 8;
            res = evaluate(_solver, 
                           metaSMT::logic::Array::select(
                                  getArrayForUpdate(re->updates.root, re->updates.head),
                                  construct(re->index, 0)));
            break;
        }

        case Expr::Concat:
        {
            ConcatExpr *ce = cast<ConcatExpr>(e);
            assert(ce);
            *width_out = ce->getWidth();
            unsigned numKids = ce->getNumKids();

            if (numKids > 0) {
                res = evaluate(_solver, construct(ce->getKid(numKids-1), 0));
                for (int i = numKids - 2; i >= 0; i--) {
                    res = evaluate(_solver, concat(construct(ce->getKid(i), 0), res));
                }
            }
            break;
        }

        case Expr::Extract:
        {
            ExtractExpr *ee = cast<ExtractExpr>(e);
            assert(ee);
            // ToDo spare evaluate?
            typename SolverContext::result_type child = evaluate(_solver, construct(ee->expr, width_out));

            unsigned ee_width = ee->getWidth();
            *width_out = ee_width;

            if (ee_width == 1) {
                res = bvBoolExtract(child, ee->offset);
            }
            else {
                res = evaluate(_solver,
                               extract(ee->offset + ee_width - 1, ee->offset, child));
            }
            break;
        }

        case Expr::ZExt:
        {
            CastExpr *ce = cast<CastExpr>(e);
            assert(ce);

            int child_width = 0;
            typename SolverContext::result_type child = evaluate(_solver, construct(ce->src, &child_width));

            unsigned ce_width = ce->getWidth();
            *width_out = ce_width;

            if (child_width == 1) {
                res = evaluate(_solver, 
                               metaSMT::logic::Ite(child, bvOne(ce_width), bvZero(ce_width)));			                       
            }
            else {
                res = evaluate(_solver, zero_extend(ce_width - child_width, child));
            }

            // ToDo calculate how many zeros to add
            // Note: STP and metaSMT differ in the prototype arguments;
            // STP requires the width of the resulting bv;
            // whereas metaSMT (and Z3) require the width of the zero vector that is to be appended
            // res = evaluate(_solver, zero_extend(ce_width, construct(ce->src)));
    
            break;	  
        }
  
        case Expr::SExt:
        {
            CastExpr *ce = cast<CastExpr>(e);
            assert(ce);
    
            int child_width = 0;
            typename SolverContext::result_type child = evaluate(_solver, construct(ce->src, &child_width));
            
            unsigned ce_width = ce->getWidth();
            *width_out = ce_width;
    
            if (child_width == 1) {
                res = evaluate(_solver, 
                               metaSMT::logic::Ite(child, bvMinusOne(ce_width), bvZero(ce_width)));
            }
            else {
                // ToDo ce_width - child_width? It is only ce_width in STPBuilder
                res = evaluate(_solver, sign_extend(ce_width - child_width, child));
            }

            break;
        }
  
        case Expr::Add:
        {
            AddExpr *ae = cast<AddExpr>(e);
            assert(ae);	    
            res = evaluate(_solver, bvadd(construct(ae->left, width_out), construct(ae->right, width_out)));
            assert(*width_out != 1 && "uncanonicalized add");
            break;	  
        }  
  
        case Expr::Sub:  
        {
            SubExpr *se = cast<SubExpr>(e);
            assert(se);	    
            res = evaluate(_solver, bvsub(construct(se->left, width_out), construct(se->right, width_out))); 
            assert(*width_out != 1 && "uncanonicalized sub");
            break;	  
        }  
   
        case Expr::Mul:
        { 
            MulExpr *me = cast<MulExpr>(e);
            assert(me);
    
            typename SolverContext::result_type right_expr = evaluate(_solver, construct(me->right, width_out));
            assert(*width_out != 1 && "uncanonicalized mul");
    
            ConstantExpr *CE = dyn_cast<ConstantExpr>(me->left);
            if (CE && (CE->getWidth() <= 64)) {	        		
                res = constructMulByConstant(right_expr, *width_out, CE->getZExtValue());		
            }
            else {
                res = evaluate(_solver, bvmul(construct(me->left, width_out), right_expr));	     
            }
            break;
        }

        case Expr::UDiv:
        {
            UDivExpr *de = cast<UDivExpr>(e);
            assert(de);

            typename SolverContext::result_type left_expr = construct(de->left, width_out);
            assert(*width_out != 1 && "uncanonicalized udiv");
            bool construct_both = true;

            ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right);
            if (CE && (CE->getWidth() <= 64)) {
                uint64_t divisor = CE->getZExtValue();
                if (bits64::isPowerOfTwo(divisor)) {
                    res = bvRightShift(left_expr, *width_out, bits64::indexOfSingleBit(divisor), getShiftBits(*width_out));
                    construct_both = false;
                }
                else if (_optimizeDivides) {
                    if (*width_out == 32) { //only works for 32-bit division
                        res = constructUDivByConstant(left_expr, *width_out, (uint32_t) divisor);
                        construct_both = false;
                    }
                }
            }

            if (construct_both) {	    
                res = evaluate(_solver, bvudiv(left_expr, construct(de->right, width_out))); 
            }
            break;
        }

        case Expr::SDiv:
        {
            SDivExpr *de = cast<SDivExpr>(e);
            assert(de);

            typename SolverContext::result_type left_expr = construct(de->left, width_out);
            assert(*width_out != 1 && "uncanonicalized sdiv");

            ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right);
            if (CE && _optimizeDivides && (*width_out == 32)) {
                res = constructSDivByConstant(left_expr, *width_out, CE->getZExtValue(32));
            }
            else {
                res = evaluate(_solver, bvsdiv(left_expr, construct(de->right, width_out))); 
            }
            break;
        }

        case Expr::URem:
        {
            URemExpr *de = cast<URemExpr>(e);
            assert(de);

            typename SolverContext::result_type left_expr = construct(de->left, width_out);
            assert(*width_out != 1 && "uncanonicalized urem");
    
            bool construct_both = true;
            ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right);
            if (CE && (CE->getWidth() <= 64)) {
      
                uint64_t divisor = CE->getZExtValue();

                if (bits64::isPowerOfTwo(divisor)) {
  
                    unsigned bits = bits64::indexOfSingleBit(divisor);		  
                    // special case for modding by 1 or else we bvExtract -1:0
                    if (bits == 0) {
                        res = bvZero(*width_out);
                        construct_both = false;
                    }
                    else {
                        res = evaluate(_solver, concat(bvZero(*width_out - bits), 
                                                       bvExtract(left_expr, bits - 1, 0)));
                        construct_both = false;
                    }
                }

                // Use fast division to compute modulo without explicit division for constant divisor.
       
                if (_optimizeDivides && *width_out == 32) { //only works for 32-bit division
                    typename SolverContext::result_type quotient = constructUDivByConstant(left_expr, *width_out, (uint32_t) divisor);
                    typename SolverContext::result_type quot_times_divisor = constructMulByConstant(quotient, *width_out, divisor);
                    res = evaluate(_solver, bvsub(left_expr, quot_times_divisor));                    
                    construct_both = false;
                }
            }
    
            if (construct_both) {
                res = evaluate(_solver, bvurem(left_expr, construct(de->right, width_out)));	      
            }
            break;  
        }

        case Expr::SRem:
        {
            SRemExpr *de = cast<SRemExpr>(e);
            assert(de);
    
            typename SolverContext::result_type left_expr = evaluate(_solver, construct(de->left, width_out));
            typename SolverContext::result_type right_expr = evaluate(_solver, construct(de->right, width_out));
            assert(*width_out != 1 && "uncanonicalized srem");
    
            bool construct_both = true;
    
#if 0 //not faster per first benchmark
            
            if (_optimizeDivides) {
                if (ConstantExpr *cre = de->right->asConstant()) {
                    uint64_t divisor = cre->asUInt64;
    
                    //use fast division to compute modulo without explicit division for constant divisor
                    if( *width_out == 32 ) { //only works for 32-bit division
                       	typename SolverContext::result_type quotient = constructSDivByConstant(left, *width_out, divisor);
                        typename SolverContext::result_type quot_times_divisor = constructMulByConstant(quotient, *width_out, divisor);
                        res = vc_bvMinusExpr( vc, *width_out, left, quot_times_divisor );
                        construct_both = false;
                    }
                }
            }
    
#endif

            if (construct_both) {     
                res = evaluate(_solver, bvsrem(left_expr, right_expr));
            }
            break;
        }

        case Expr::Not:
        {
            NotExpr *ne = cast<NotExpr>(e);
            assert(ne);
    
            typename SolverContext::result_type child = evaluate(_solver, construct(ne->expr, width_out));
            if (*width_out == 1) {
                res = evaluate(_solver, metaSMT::logic::Not(child));
            }
            else {                
                res = evaluate(_solver, bvnot(child));
            }    
            break;	  
        }
  
        case Expr::And:
        {
            AndExpr *ae = cast<AndExpr>(e);
	    assert(ae);
	    
	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(ae->left, width_out));
	    typename SolverContext::result_type right_expr = evaluate(_solver, construct(ae->right, width_out));
	    
	    if (*width_out == 1) {
	        res = evaluate(_solver, metaSMT::logic::And(left_expr, right_expr));
	    }
	    else {
	        res = evaluate(_solver, bvand(left_expr, right_expr));
	    }
	    
	    break;	  
	}
	  
	case Expr::Or:
	{
	    OrExpr *oe = cast<OrExpr>(e);
	    assert(oe);
	    
	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(oe->left, width_out));
	    typename SolverContext::result_type right_expr = evaluate(_solver, construct(oe->right, width_out));
	    
	    if (*width_out == 1) {
	        res = evaluate(_solver, metaSMT::logic::Or(left_expr, right_expr));
	    }
	    else {
	        res = evaluate(_solver, bvor(left_expr, right_expr));
	    }
	    
	    break;	  
	}
	  
	case Expr::Xor:
	{
	    XorExpr *xe = cast<XorExpr>(e);
	    assert(xe);
	    
	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(xe->left, width_out));
	    typename SolverContext::result_type right_expr = evaluate(_solver, construct(xe->right, width_out));
	    
	    if (*width_out == 1) {
	        res = evaluate(_solver, metaSMT::logic::Xor(left_expr, right_expr));
	    }
	    else {
	        res = evaluate(_solver, bvxor(left_expr, right_expr));
	    }
	    
	    break;	  
	}
	  
	case Expr::Shl:  
	{	    
	    ShlExpr *se = cast<ShlExpr>(e);
	    assert(se);
	    
	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(se->left, width_out));
	    assert(*width_out != 1 && "uncanonicalized shl");
	    
	    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(se->right)) {
	        res =  bvLeftShift(left_expr, *width_out, (unsigned) CE->getLimitedValue(), getShiftBits(*width_out));
            }
            else {
                int shiftWidth = 0;
		typename SolverContext::result_type right_expr = evaluate(_solver, construct(se->right, &shiftWidth));
		res = mimic_stp ? bvVarLeftShift(left_expr, right_expr, *width_out) : 
		                  evaluate(_solver, bvshl(left_expr, right_expr));	      
	    }    
	    
	    break;	  
	}
	
	case Expr::LShr:
	{
	    LShrExpr *lse = cast<LShrExpr>(e);
	    assert(lse);
	    
	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(lse->left, width_out));	    
	    assert(*width_out != 1 && "uncanonicalized lshr");
	    
	    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(lse->right)) {
	        res =  bvRightShift(left_expr, *width_out, (unsigned) CE->getLimitedValue(), getShiftBits(*width_out));
	    }
	    else {
                int shiftWidth = 0;
		typename SolverContext::result_type right_expr = evaluate(_solver, construct(lse->right, &shiftWidth));
		res = mimic_stp ? bvVarRightShift(left_expr, right_expr, *width_out) :
				  evaluate(_solver, bvshr(left_expr, right_expr));
	    }
	    
	    break;	  
	}
	  
	case Expr::AShr:  
	{
	    AShrExpr *ase = cast<AShrExpr>(e);
	    assert(ase);
	    
	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(ase->left, width_out));	    
	    assert(*width_out != 1 && "uncanonicalized ashr");
	    
	    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) {
	        unsigned shift = (unsigned) CE->getLimitedValue();
                typename SolverContext::result_type signedBool = bvBoolExtract(left_expr, *width_out - 1);
		res = constructAShrByConstant(left_expr, *width_out, shift, signedBool, getShiftBits(*width_out));	      
	    }
	    else {
                int shiftWidth = 0;
		typename SolverContext::result_type right_expr = evaluate(_solver, construct(ase->right, &shiftWidth));
		res = mimic_stp ? bvVarArithRightShift(left_expr, right_expr, *width_out) :
		                  evaluate(_solver, bvashr(left_expr, right_expr)); 
	    }    
	    
	    break;	  
	}
	  
	case Expr::Eq: 
	{
	     EqExpr *ee = cast<EqExpr>(e);
	     assert(ee);
	     
    	     typename SolverContext::result_type left_expr = evaluate(_solver, construct(ee->left, width_out));
	     typename SolverContext::result_type right_expr = evaluate(_solver, construct(ee->right, width_out));

	     if (*width_out==1) {
	         if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ee->left)) {
		     if (CE->isTrue()) {
		         res = right_expr;  
		     }
		     else {
		         res = evaluate(_solver, metaSMT::logic::Not(right_expr));
		     }
		 }
		 else {
		     res = evaluate(_solver, metaSMT::logic::equal(left_expr, right_expr));
		 }
	     } // end of *width_out == 1
	     else {
	         *width_out = 1;
	         res = evaluate(_solver, metaSMT::logic::equal(left_expr, right_expr));
	     }
	     
	     break;
	}
	
	case Expr::Ult:
	{
	    UltExpr *ue = cast<UltExpr>(e);
	    assert(ue);
	    
	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(ue->left, width_out));
	    typename SolverContext::result_type right_expr = evaluate(_solver, construct(ue->right, width_out));	    
	    
	    assert(*width_out != 1 && "uncanonicalized ult");
	    *width_out = 1;    
	    
	    res = evaluate(_solver, bvult(left_expr, right_expr));
	    break;	  
	}
	  
	case Expr::Ule:
	{
	    UleExpr *ue = cast<UleExpr>(e);
	    assert(ue);
	    
	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(ue->left, width_out));
	    typename SolverContext::result_type right_expr = evaluate(_solver, construct(ue->right, width_out));	
	    
	    assert(*width_out != 1 && "uncanonicalized ule");
	    *width_out = 1;    
	    
	    res = evaluate(_solver, bvule(left_expr, right_expr));
	    break;	  
	}
	  
	case Expr::Slt:
	{
	    SltExpr *se = cast<SltExpr>(e);
	    assert(se);
	    
	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(se->left, width_out));
	    typename SolverContext::result_type right_expr = evaluate(_solver, construct(se->right, width_out));	
	    
	    assert(*width_out != 1 && "uncanonicalized slt");
	    *width_out = 1;
	    
	    res = evaluate(_solver, bvslt(left_expr, right_expr));
	    break;	  
	}
	  
        case Expr::Sle:
        {
            SleExpr *se = cast<SleExpr>(e);
            assert(se);
    
            typename SolverContext::result_type left_expr = evaluate(_solver, construct(se->left, width_out));
            typename SolverContext::result_type right_expr = evaluate(_solver, construct(se->right, width_out));	
    
            assert(*width_out != 1 && "uncanonicalized sle");
            *width_out = 1;    
    
            res = evaluate(_solver, bvsle(left_expr, right_expr));
            break;	  
        }
  
        // unused due to canonicalization
#if 0
        case Expr::Ne:
        case Expr::Ugt:
        case Expr::Uge:
        case Expr::Sgt:
        case Expr::Sge:
#endif  
     
        default:
             assert(false);
             break;      
      
    };
    return res;
}


}  /* end of namespace klee */

#endif /* SUPPORT_METASMT */

#endif /* METASMTBUILDER_H_ */