def ResetZ3 ():
    z3._main_ctx = None
    z3.main_ctx()
    z3.set_param('auto_config', False)
    z3.set_param('smt.mbqi', True)
    z3.set_param('model.compact', True)
    z3.set_param('smt.pull_nested_quantifiers', True)
    z3.set_param('smt.mbqi.max_iterations', 10000)
    z3.set_param('smt.random_seed', random.SystemRandom().randint(0, sys.maxint))

def is_sat(solver,f):
    solver.push()
    ctx = z3.main_ctx()
    z3.Z3_solver_assert(ctx.ref(), solver.solver, f.as_ast())
    #solver.add(f)
    res = solver.check() != z3.unsat
    solver.pop()
    return res

def string_regexdigit():
  ctx = z3.main_ctx()
  decl = z3strlib.z3str_regexdigit_decl()
  return z3.FuncDeclRef(decl, ctx)

def string_unroll():
  ctx = z3.main_ctx()
  decl = z3strlib.z3str_unroll_decl()
  return z3.FuncDeclRef(decl, ctx)

def string_replace():
  ctx = z3.main_ctx()
  decl = z3strlib.z3str_replace_decl()
  return z3.FuncDeclRef(decl, ctx)

z3strlib.z3str_regexunion_decl.argtypes = []
z3strlib.z3str_regexconcat_decl.restype = z3.FuncDecl
z3strlib.z3str_regexconcat_decl.argtypes = []
z3strlib.z3str_unroll_decl.restype = z3.FuncDecl
z3strlib.z3str_unroll_decl.argtypes = []
z3strlib.z3str_regexdigit_decl.restype = z3.FuncDecl
z3strlib.z3str_regexdigit_decl.argtypes = []
z3strlib.z3str_register_vars.restype = None
z3strlib.z3str_register_vars.argtypes = [z3.Ast]
z3strlib.setAlphabet.restype = None
z3strlib.setAlphabet.argtypes = []
z3strlib.setAlphabet7bit.restype = None
z3strlib.setAlphabet7bit.argtypes = []

## Set the default Z3py context to use z3str
ctx = z3.main_ctx()
ctx.ctx = z3strlib.z3str_context()
z3strlib.setAlphabet7bit()

## Wrappers around the various z3str_*() functions in libz3str2.so
def StringSort():
  ctx = z3.main_ctx()
  sort = z3strlib.z3str_mk_string_sort()
  return z3.SortRef(sort, ctx)

def RegexSort():
  ctx = z3.main_ctx()
  sort = z3strlib.z3str_mk_regex_sort()
  return z3.SortRef(sort, ctx)

def string_concat():

def my_eq(x, y):
    ctx = z3.main_ctx()
    #    print "my_eq: {} = {}".format(x,y)
    return z3.BoolRef(z3.Z3_mk_eq(ctx.ref(), x.as_ast(), y.as_ast()), ctx)

def string_substring():
  ctx = z3.main_ctx()
  decl = z3strlib.z3str_substring_decl()
  return z3.FuncDeclRef(decl, ctx)

def string_concat():
  ctx = z3.main_ctx()
  decl = z3strlib.z3str_concat_decl()
  return z3.FuncDeclRef(decl, ctx)

 def __init__(self, environment, logic=None):
     QuantifierEliminator.__init__(self)
     self.environment = environment
     self.logic = logic
     self.converter = Z3Converter(environment, z3.main_ctx())

def ResetZ3 ():
    z3._main_ctx = None
    z3.main_ctx()
    z3.set_param('smt.random_seed', random.SystemRandom().randint(0, sys.maxint))
    z3.set_param('smt.mbqi.max_iterations', 10000)
    z3.set_param('smt.mbqi.max_cexs', 100)

def ResetZ3 ():
    z3._main_ctx = None
    z3.main_ctx()
    z3.set_param('smt.random_seed', random.SystemRandom().randint(0, sys.maxint))

def my_eq(x,y):
    ctx = z3.main_ctx()
    return z3.BoolRef(z3.Z3_mk_eq(ctx.ref(), x.as_ast(), y.as_ast()), ctx)

def my_and(*args):
    ctx = z3.main_ctx()
    _args, sz = z3._to_ast_array(args)
    return z3.BoolRef(z3.Z3_mk_and(ctx.ref(), sz, _args), ctx)

def RegexSort():
  ctx = z3.main_ctx()
  sort = z3strlib.z3str_mk_regex_sort()
  return z3.SortRef(sort, ctx)

 def _context(self):
     try:
         return self._tls.context
     except AttributeError:
         self._tls.context = z3.Context() if threading.current_thread().name != 'MainThread' else z3.main_ctx()
         return self._tls.context

def string_length():
  ctx = z3.main_ctx()
  decl = z3strlib.z3str_length_decl()
  return z3.FuncDeclRef(decl, ctx)

def ResetZ3 (seed):
    z3._main_ctx = None
    z3.main_ctx()
    z3.set_param('smt.random_seed', seed)

def string_indexof():
  ctx = z3.main_ctx()
  decl = z3strlib.z3str_indexof_decl()
  return z3.FuncDeclRef(decl, ctx)

def ResetZ3 ():
    z3._main_ctx = None
    z3.main_ctx()