MetaSMT builder, solver and command-line options.

3 files changed, 1616 insertions, 0 deletions

diff --git a/lib/Solver/Makefile b/lib/Solver/Makefile
index 11d3d330..2be74c01 100755
--- a/lib/Solver/Makefile
+++ b/lib/Solver/Makefile
@@ -14,3 +14,12 @@ DONT_BUILD_RELINKED=1
 BUILD_ARCHIVE=1
 
 include $(LEVEL)/Makefile.common
+
+ifeq ($(ENABLE_METASMT),1)
+  include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
+  CXX.Flags += -DBOOST_HAS_GCC_TR1
+  CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags))
+  CXX.Flags := $(filter-out -fno-rtti,$(CXX.Flags))
+  CXX.Flags += $(metaSMT_CXXFLAGS)
+  CXX.Flags += $(metaSMT_INCLUDES)
+endif
\ No newline at end of file
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
new file mode 100644
index 00000000..0e508b46
--- /dev/null
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -0,0 +1,1167 @@
+ /*
+ * 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, bvneg(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_ */
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 3414cda2..4df691f2 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -12,6 +12,7 @@
 
 #include "SolverStats.h"
 #include "STPBuilder.h"
+#include "MetaSMTBuilder.h"
 
 #include "klee/Constraints.h"
 #include "klee/Expr.h"
@@ -20,6 +21,7 @@
 #include "klee/util/ExprPPrinter.h"
 #include "klee/util/ExprUtil.h"
 #include "klee/Internal/Support/Timer.h"
+#include "klee/CommandLine.h"
 
 #define vc_bvBoolExtract IAMTHESPAWNOFSATAN
 
@@ -45,6 +47,24 @@ IgnoreSolverFailures("ignore-solver-failures",
 
 using namespace klee;
 
+
+#ifdef SUPPORT_METASMT
+
+#include <metaSMT/DirectSolver_Context.hpp>
+#include <metaSMT/backend/Z3_Backend.hpp>
+#include <metaSMT/backend/Boolector.hpp>
+#include <metaSMT/backend/MiniSAT.hpp>
+#include <metaSMT/support/run_algorithm.hpp>
+#include <metaSMT/API/Stack.hpp>
+#include <metaSMT/API/Group.hpp>
+
+using namespace metaSMT;
+using namespace metaSMT::solver;
+
+#endif /* SUPPORT_METASMT */
+
+
+
 /***/
 
 SolverImpl::~SolverImpl() {
@@ -809,3 +829,423 @@ STPSolverImpl::computeInitialValues(const Query &query,
 SolverImpl::SolverRunStatus STPSolverImpl::getOperationStatusCode() {
    return runStatusCode;
 }
+
+#ifdef SUPPORT_METASMT
+
+// ------------------------------------- MetaSMTSolverImpl class declaration ------------------------------
+
+template<typename SolverContext>
+class MetaSMTSolverImpl : public SolverImpl {
+private:
+
+  SolverContext _meta_solver;
+  MetaSMTSolver<SolverContext>  *_solver;  
+  MetaSMTBuilder<SolverContext> *_builder;
+  double _timeout;
+  bool   _useForked;
+  SolverRunStatus _runStatusCode;
+
+public:
+  MetaSMTSolverImpl(MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides);  
+  virtual ~MetaSMTSolverImpl();
+  
+  char *getConstraintLog(const Query&);
+  void setCoreSolverTimeout(double timeout) { _timeout = timeout; }
+
+  bool computeTruth(const Query&, bool &isValid);
+  bool computeValue(const Query&, ref<Expr> &result);
+    
+  bool computeInitialValues(const Query &query,
+                            const std::vector<const Array*> &objects,
+                            std::vector< std::vector<unsigned char> > &values,
+                            bool &hasSolution);
+    
+  SolverImpl::SolverRunStatus runAndGetCex(ref<Expr> query_expr,
+                                           const std::vector<const Array*> &objects,
+                                           std::vector< std::vector<unsigned char> > &values,
+                                           bool &hasSolution);
+  
+  SolverImpl::SolverRunStatus runAndGetCexForked(const Query &query,
+                                                 const std::vector<const Array*> &objects,
+                                                 std::vector< std::vector<unsigned char> > &values,
+                                                 bool &hasSolution,
+                                                 double timeout);
+  
+  SolverRunStatus getOperationStatusCode();
+  
+  SolverContext& get_meta_solver() { return(_meta_solver); };
+  
+};
+
+
+// ------------------------------------- MetaSMTSolver methods --------------------------------------------
+
+
+template<typename SolverContext>
+MetaSMTSolver<SolverContext>::MetaSMTSolver(bool useForked, bool optimizeDivides) 
+  : Solver(new MetaSMTSolverImpl<SolverContext>(this, useForked, optimizeDivides))
+{
+   
+}
+
+template<typename SolverContext>
+MetaSMTSolver<SolverContext>::~MetaSMTSolver()
+{
+  
+}
+
+template<typename SolverContext>
+char *MetaSMTSolver<SolverContext>::getConstraintLog(const Query& query) {
+  return(impl->getConstraintLog(query));
+}
+
+template<typename SolverContext>
+void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) {
+  impl->setCoreSolverTimeout(timeout);
+}
+
+
+// ------------------------------------- MetaSMTSolverImpl methods ----------------------------------------
+
+
+
+template<typename SolverContext>
+MetaSMTSolverImpl<SolverContext>::MetaSMTSolverImpl(MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides)
+  : _solver(solver),    
+    _builder(new MetaSMTBuilder<SolverContext>(_meta_solver, optimizeDivides)),
+    _timeout(0.0),
+    _useForked(useForked)
+{  
+  assert(_solver && "unable to create MetaSMTSolver");
+  assert(_builder && "unable to create MetaSMTBuilder");
+  
+  if (_useForked) {
+      shared_memory_id = shmget(IPC_PRIVATE, shared_memory_size, IPC_CREAT | 0700);
+      assert(shared_memory_id >= 0 && "shmget failed");
+      shared_memory_ptr = (unsigned char*) shmat(shared_memory_id, NULL, 0);
+      assert(shared_memory_ptr != (void*) -1 && "shmat failed");
+      shmctl(shared_memory_id, IPC_RMID, NULL);
+  }
+}
+
+template<typename SolverContext>
+MetaSMTSolverImpl<SolverContext>::~MetaSMTSolverImpl() {
+
+}
+
+template<typename SolverContext>
+char *MetaSMTSolverImpl<SolverContext>::getConstraintLog(const Query&) {
+  // ToDo
+}
+
+template<typename SolverContext>
+bool MetaSMTSolverImpl<SolverContext>::computeTruth(const Query& query, bool &isValid) {  
+
+  bool success = false;
+  std::vector<const Array*> objects;
+  std::vector< std::vector<unsigned char> > values;
+  bool hasSolution;
+
+  if (computeInitialValues(query, objects, values, hasSolution)) {
+      // query.expr is valid iff !query.expr is not satisfiable
+      isValid = !hasSolution;
+      success = true;
+  }
+
+  return(success);
+}
+
+template<typename SolverContext>
+bool MetaSMTSolverImpl<SolverContext>::computeValue(const Query& query, ref<Expr> &result) {
+  
+  bool success = false;
+  std::vector<const Array*> objects;
+  std::vector< std::vector<unsigned char> > values;
+  bool hasSolution;
+
+  // Find the object used in the expression, and compute an assignment for them.
+  findSymbolicObjects(query.expr, objects);  
+  if (computeInitialValues(query.withFalse(), objects, values, hasSolution)) {  
+      assert(hasSolution && "state has invalid constraint set");
+      // Evaluate the expression with the computed assignment.
+      Assignment a(objects, values);
+      result = a.evaluate(query.expr);
+      success = true;
+  }
+
+  return(success);
+}
+
+
+template<typename SolverContext>
+bool MetaSMTSolverImpl<SolverContext>::computeInitialValues(const Query &query,
+                                             const std::vector<const Array*> &objects,
+                                             std::vector< std::vector<unsigned char> > &values,
+                                             bool &hasSolution) {  
+
+  _runStatusCode =  SOLVER_RUN_STATUS_FAILURE;
+
+  TimerStatIncrementer t(stats::queryTime);
+  assert(_builder);
+
+  /*
+   * FIXME push() and pop() work for Z3 but not for Boolector.
+   * If using Z3, use push() and pop() and assert constraints.
+   * If using Boolector, assume constrainsts instead of asserting them.
+   */
+  //push(_meta_solver);
+
+  if (!_useForked) {
+      for (ConstraintManager::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) {
+          //assertion(_meta_solver, _builder->construct(*it));
+          assumption(_meta_solver, _builder->construct(*it));  
+      }  
+  }  
+    
+  ++stats::queries;
+  ++stats::queryCounterexamples;  
+ 
+  bool success = true;
+  if (_useForked) {
+      _runStatusCode = runAndGetCexForked(query, objects, values, hasSolution, _timeout);
+      success = ((SOLVER_RUN_STATUS_SUCCESS_SOLVABLE == _runStatusCode) || (SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE == _runStatusCode));
+  }
+  else {
+      _runStatusCode = runAndGetCex(query.expr, objects, values, hasSolution);
+      success = true;
+  } 
+    
+  if (success) {
+      if (hasSolution) {
+          ++stats::queriesInvalid;
+      }
+      else {
+          ++stats::queriesValid;
+      }
+  }  
+   
+  //pop(_meta_solver); 
+  
+  return(success);
+}
+
+template<typename SolverContext>
+SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCex(ref<Expr> query_expr,
+                                             const std::vector<const Array*> &objects,
+                                             std::vector< std::vector<unsigned char> > &values,
+                                             bool &hasSolution)
+{
+
+  // assume the negation of the query  
+  assumption(_meta_solver, _builder->construct(Expr::createIsZero(query_expr)));  
+  hasSolution = solve(_meta_solver);  
+  
+  if (hasSolution) {
+      values.reserve(objects.size());
+      for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) {
+        
+          const Array *array = *it;
+          assert(array);
+          typename SolverContext::result_type array_exp = _builder->getInitialArray(array);
+           
+          std::vector<unsigned char> data;      
+          data.reserve(array->size);       
+           
+          for (unsigned offset = 0; offset < array->size; offset++) {
+              typename SolverContext::result_type elem_exp = evaluate(
+                       _meta_solver,
+                       metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain())));
+              unsigned char elem_value = metaSMT::read_value(_meta_solver, elem_exp);
+              data.push_back(elem_value);
+          }
+                   
+          values.push_back(data);
+      }
+  }
+  
+  if (true == hasSolution) {
+      return(SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE);
+  }
+  else {
+      return(SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE);  
+  }
+}
+
+static void metaSMTTimeoutHandler(int x) {
+  _exit(52);
+}
+
+template<typename SolverContext>
+SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(const Query &query,
+                                                          const std::vector<const Array*> &objects,
+                                                          std::vector< std::vector<unsigned char> > &values,
+                                                          bool &hasSolution,
+                                                          double timeout)
+{
+  unsigned char *pos = shared_memory_ptr;
+  unsigned sum = 0;
+  for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) {
+      sum += (*it)->size;    
+  }
+  // sum += sizeof(uint64_t);
+  sum += sizeof(stats::queryConstructs);
+  assert(sum < shared_memory_size && "not enough shared memory for counterexample");
+
+  fflush(stdout);
+  fflush(stderr);
+  int pid = fork();
+  if (pid == -1) {
+      fprintf(stderr, "error: fork failed (for metaSMT)");
+      return(SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED);
+  }
+  
+  if (pid == 0) {
+      if (timeout) {
+          ::alarm(0); /* Turn off alarm so we can safely set signal handler */
+          ::signal(SIGALRM, metaSMTTimeoutHandler);
+          ::alarm(std::max(1, (int) timeout));
+      }     
+      
+      for (ConstraintManager::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) {      
+          assertion(_meta_solver, _builder->construct(*it));
+          //assumption(_meta_solver, _builder->construct(*it));  
+      } 
+      
+      
+      std::vector< std::vector<typename SolverContext::result_type> > aux_arr_exprs;
+      if (UseMetaSMT == METASMT_BACKEND_BOOLECTOR) {
+          for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) {
+            
+              std::vector<typename SolverContext::result_type> aux_arr;          
+              const Array *array = *it;
+              assert(array);
+              typename SolverContext::result_type array_exp = _builder->getInitialArray(array);
+              
+              for (unsigned offset = 0; offset < array->size; offset++) {
+                  typename SolverContext::result_type elem_exp = evaluate(
+                      _meta_solver,
+                      metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain())));
+                  aux_arr.push_back(elem_exp);
+              }
+              aux_arr_exprs.push_back(aux_arr);
+          }
+          assert(aux_arr_exprs.size() == objects.size());
+      }
+      
+           
+      // assume the negation of the query
+      // can be also asserted instead of assumed as we are in a child process
+      assumption(_meta_solver, _builder->construct(Expr::createIsZero(query.expr)));        
+      unsigned res = solve(_meta_solver);
+
+      if (res) {
+
+          if (UseMetaSMT != METASMT_BACKEND_BOOLECTOR) {
+
+              for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) {
+
+                  const Array *array = *it;
+                  assert(array);
+                  typename SolverContext::result_type array_exp = _builder->getInitialArray(array);      
+
+                  for (unsigned offset = 0; offset < array->size; offset++) {
+
+                      typename SolverContext::result_type elem_exp = evaluate(
+                          _meta_solver,
+                          metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain())));
+                      unsigned char elem_value = metaSMT::read_value(_meta_solver, elem_exp);
+                      *pos++ = elem_value;
+                  }
+              }
+          }
+          else {
+              typename std::vector< std::vector<typename SolverContext::result_type> >::const_iterator eit = aux_arr_exprs.begin(), eie = aux_arr_exprs.end();
+              for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie, eit != eie; ++it, ++eit) {
+                  const Array *array = *it;
+                  const std::vector<typename SolverContext::result_type>& arr_exp = *eit;
+                  assert(array);
+                  assert(array->size == arr_exp.size());
+
+                  for (unsigned offset = 0; offset < array->size; offset++) {
+                      unsigned char elem_value = metaSMT::read_value(_meta_solver, arr_exp[offset]);
+                       *pos++ = elem_value;
+                  }
+              }
+          }
+      }
+      assert((uint64_t*) pos);
+      *((uint64_t*) pos) = stats::queryConstructs;      
+      
+      _exit(!res);
+  }
+  else {
+      int status;
+      pid_t res;
+
+      do {
+          res = waitpid(pid, &status, 0);
+      } 
+      while (res < 0 && errno == EINTR);
+    
+      if (res < 0) {
+          fprintf(stderr, "error: waitpid() for metaSMT failed");
+          return(SolverImpl::SOLVER_RUN_STATUS_WAITPID_FAILED);
+      }
+      
+      // From timed_run.py: It appears that linux at least will on
+      // "occasion" return a status when the process was terminated by a
+      // signal, so test signal first.
+      if (WIFSIGNALED(status) || !WIFEXITED(status)) {
+           fprintf(stderr, "error: metaSMT did not return successfully (status = %d) \n", WTERMSIG(status));
+           return(SolverImpl::SOLVER_RUN_STATUS_INTERRUPTED);
+      }
+
+      int exitcode = WEXITSTATUS(status);
+      if (exitcode == 0) {
+          hasSolution = true;
+      } 
+      else if (exitcode == 1) {
+          hasSolution = false;
+      }
+      else if (exitcode == 52) {
+          fprintf(stderr, "error: metaSMT timed out");
+          return(SolverImpl::SOLVER_RUN_STATUS_TIMEOUT);
+      }
+      else {
+          fprintf(stderr, "error: metaSMT did not return a recognized code");
+          return(SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE);
+      }
+      
+      if (hasSolution) {
+          values = std::vector< std::vector<unsigned char> >(objects.size());
+          unsigned i = 0;
+          for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) {
+              const Array *array = *it;
+              assert(array);
+              std::vector<unsigned char> &data = values[i++];
+              data.insert(data.begin(), pos, pos + array->size);
+              pos += array->size;
+          }
+      }
+      stats::queryConstructs += (*((uint64_t*) pos) - stats::queryConstructs);      
+
+      if (true == hasSolution) {
+          return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE;
+      }
+      else {
+          return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE;
+      }
+  }
+}
+
+template<typename SolverContext>
+SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::getOperationStatusCode() {
+   return _runStatusCode;
+}
+
+template class MetaSMTSolver< DirectSolver_Context < Boolector> >;
+template class MetaSMTSolver< DirectSolver_Context < Z3_Backend> >;
+template class MetaSMTSolver< DirectSolver_Context < STP_Backend> >;
+
+#endif /* SUPPORT_METASMT */
+