Merge branch 'master' of https://github.com/Z3Prover/z3

examples/interp/iz3.cpp

@@ -1,458 +0,0 @@
-
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
---*/
-
-#include <stdio.h>
-#include <stdlib.h>
-#include <iostream>
-#include <string>
-#include <vector>
-#include "z3.h"
-
-
-
-int usage(const char **argv){
-  std::cerr << "usage: " << argv[0] << " [options] file.smt" << std::endl;
-  std::cerr << std::endl;
-  std::cerr << "options:" << std::endl;
-  std::cerr << "  -t,--tree        tree interpolation" << std::endl;
-  std::cerr << "  -c,--check       check result" << std::endl;
-  std::cerr << "  -p,--profile     profile execution" << std::endl;
-  std::cerr << "  -w,--weak        weak interpolants" << std::endl;
-  std::cerr << "  -f,--flat        ouput flat formulas" << std::endl;
-  std::cerr << "  -o <file>        ouput to SMT-LIB file" << std::endl;
-  std::cerr << "  -a,--anon        anonymize" << std::endl;
-  std::cerr << "  -s,--simple      simple proof mode" << std::endl;
-  std::cerr << std::endl;
-  return 1;
-}
-
-int main(int argc, const char **argv) {
-    
-  bool tree_mode = false;
-  bool check_mode = false;
-  bool profile_mode = false;
-  bool incremental_mode = false;
-  std::string output_file;
-  bool flat_mode = false;
-  bool anonymize = false;
-  bool write = false;
-
-  Z3_config cfg = Z3_mk_config();
-  // Z3_interpolation_options options = Z3_mk_interpolation_options();
-  // Z3_params options = 0;
-
-  /* Parse the command line */
-  int argn = 1;
-  while(argn < argc-1){
-    std::string flag = argv[argn];
-    if(flag[0] == '-'){
-      if(flag == "-t" || flag == "--tree")
-	tree_mode = true;
-      else if(flag == "-c" || flag == "--check")
-	check_mode = true;
-      else if(flag == "-p" || flag == "--profile")
-	profile_mode = true;
-#if 0
-      else if(flag == "-w" || flag == "--weak")
-        Z3_set_interpolation_option(options,"weak","1");
-      else if(flag == "--secondary")
-        Z3_set_interpolation_option(options,"secondary","1");
-#endif
-      else if(flag == "-i" || flag == "--incremental")
-        incremental_mode = true;
-      else if(flag == "-o"){
-        argn++;
-        if(argn >= argc) return usage(argv);
-        output_file = argv[argn];
-      }
-      else if(flag == "-f" || flag == "--flat")
-        flat_mode = true;
-      else if(flag == "-a" || flag == "--anon")
-        anonymize = true;
-      else if(flag == "-w" || flag == "--write")
-        write = true;
-      else if(flag == "-s" || flag == "--simple")
-        Z3_set_param_value(cfg,"PREPROCESS","false");
-      else
-        return usage(argv);
-    }
-    argn++;
-  }
-  if(argn != argc-1)
-    return usage(argv);
-  const char *filename = argv[argn];
-
-
-  /* Create a Z3 context to contain formulas */
-  Z3_context ctx = Z3_mk_interpolation_context(cfg);
-
-  if(write || anonymize)
-    Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB2_COMPLIANT);
-  else if(!flat_mode)
-    Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB_COMPLIANT);
-  
-  /* Read an interpolation problem */
-
-  unsigned num;
-  Z3_ast *constraints;
-  unsigned *parents = 0;
-  const char *error;
-  bool ok;
-  unsigned num_theory;
-  Z3_ast *theory;
-
-  ok = Z3_read_interpolation_problem(ctx, &num, &constraints, tree_mode ? &parents : 0, filename, &error, &num_theory, &theory) != 0;
-
-  /* If parse failed, print the error message */
-
-  if(!ok){
-    std::cerr << error << "\n";
-    return 1;
-  }
-
-  /* if we get only one formula, and it is a conjunction, split it into conjuncts. */
-  if(!tree_mode && num == 1){
-    Z3_app app = Z3_to_app(ctx,constraints[0]);
-    Z3_func_decl func = Z3_get_app_decl(ctx,app);
-    Z3_decl_kind dk = Z3_get_decl_kind(ctx,func);
-    if(dk == Z3_OP_AND){
-      int nconjs = Z3_get_app_num_args(ctx,app);
-      if(nconjs > 1){
-	std::cout << "Splitting formula into " << nconjs << " conjuncts...\n";
-	num = nconjs;
-	constraints = new Z3_ast[num];
-	for(unsigned k = 0; k < num; k++)
-	  constraints[k] = Z3_get_app_arg(ctx,app,k);
-      }
-    }
-  }
-
-  /* Write out anonymized version. */
-
-  if(write || anonymize){
-#if 0
-    Z3_anonymize_ast_vector(ctx,num,constraints);
-#endif
-    std::string ofn = output_file.empty() ? "iz3out.smt2" : output_file;
-    Z3_write_interpolation_problem(ctx, num, constraints, parents, ofn.c_str(), num_theory,  theory);
-    std::cout << "anonymized problem written to " << ofn << "\n";
-    exit(0);
-  }
-
-  /* Compute an interpolant, or get a model. */
-
-  Z3_ast *interpolants = (Z3_ast *)malloc((num-1) * sizeof(Z3_ast));
-  Z3_model model = 0;
-  Z3_lbool result;
-
-  if(!incremental_mode){
-    /* In non-incremental mode, we just pass the constraints. */
-      result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, constraints, parents,  options, interpolants, &model, 0, false, num_theory, theory);
-  }
-  else {
-
-    /* This is a somewhat useless demonstration of incremental mode.
-      Here, we assert the constraints in the context, then pass them to
-      iZ3 in an array, so iZ3 knows the sequence. Note it's safe to pass
-      "true", even though we haven't techically asserted if. */
-
-    Z3_push(ctx);
-    std::vector<Z3_ast> asserted(num);
-
-    /* We start with nothing asserted. */
-    for(unsigned i = 0; i < num; i++)
-      asserted[i] = Z3_mk_true(ctx);
-
-    /* Now we assert the constrints one at a time until UNSAT. */
-
-    for(unsigned i = 0; i < num; i++){
-      asserted[i] = constraints[i];
-      Z3_assert_cnstr(ctx,constraints[i]);  // assert one constraint
-      result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, &asserted[0], parents,  options, interpolants, &model, 0, true, 0, 0);
-      if(result == Z3_L_FALSE){
-	for(unsigned j = 0; j < num-1; j++)
-          /* Since we want the interpolant formulas to survive a "pop", we
-            "persist" them here. */
-          Z3_persist_ast(ctx,interpolants[j],1);
-        break;
-      }
-    }
-    Z3_pop(ctx,1);
-  }
-  
-  switch (result) {
-  
-    /* If UNSAT, print the interpolants */
-  case Z3_L_FALSE:
-    printf("unsat\n");
-    if(output_file.empty()){
-      printf("interpolant:\n");
-      for(unsigned i = 0; i < num-1; i++)
-        printf("%s\n", Z3_ast_to_string(ctx, interpolants[i]));
-    }
-    else {
-#if 0
-      Z3_write_interpolation_problem(ctx,num-1,interpolants,0,output_file.c_str());
-      printf("interpolant written to %s\n",output_file.c_str());
-#endif
-    }
-#if 1
-    if(check_mode){
-      std::cout << "Checking interpolant...\n";
-      bool chk;
-      chk = Z3_check_interpolant(ctx,num,constraints,parents,interpolants,&error,num_theory,theory) != 0;
-      if(chk)
-	std::cout << "Interpolant is correct\n";
-      else {
-        std::cout << "Interpolant is incorrect\n";
-        std::cout << error;
-        return 1;
-      }
-    }
-#endif
-    break;
-  case Z3_L_UNDEF:
-    printf("fail\n");
-    break;
-  case Z3_L_TRUE:
-    printf("sat\n");
-    printf("model:\n%s\n", Z3_model_to_string(ctx, model));
-    break;
-  }
-
-  if(profile_mode)
-    std::cout << Z3_interpolation_profile(ctx);
-
-  /* Delete the model if there is one */
-  
-  if (model)
-    Z3_del_model(ctx, model);
-  
-  /* Delete logical context. */
-
-  Z3_del_context(ctx);
-  free(interpolants);
-
-  return 0;
-}
-
-
-#if 0
-
-
-
-int test(){
-  int i;
-
-  /* Create a Z3 context to contain formulas */
-
-  Z3_config cfg = Z3_mk_config();
-  Z3_context ctx = iz3_mk_context(cfg);
-    
-  int num = 2;
-
-  Z3_ast *constraints = (Z3_ast *)malloc(num * sizeof(Z3_ast));
-
-#if 1
-  Z3_sort arr = Z3_mk_array_sort(ctx,Z3_mk_int_sort(ctx),Z3_mk_bool_sort(ctx)); 
-  Z3_symbol  as  = Z3_mk_string_symbol(ctx, "a");
-  Z3_symbol  bs  = Z3_mk_string_symbol(ctx, "b");
-  Z3_symbol  xs  = Z3_mk_string_symbol(ctx, "x");
-
-  Z3_ast a = Z3_mk_const(ctx,as,arr);
-  Z3_ast b = Z3_mk_const(ctx,bs,arr);
-  Z3_ast x = Z3_mk_const(ctx,xs,Z3_mk_int_sort(ctx));
-  
-  Z3_ast c1 = Z3_mk_eq(ctx,a,Z3_mk_store(ctx,b,x,Z3_mk_true(ctx)));
-  Z3_ast c2 = Z3_mk_not(ctx,Z3_mk_select(ctx,a,x));
-#else
-  Z3_symbol  xs  = Z3_mk_string_symbol(ctx, "x");
-  Z3_ast x = Z3_mk_const(ctx,xs,Z3_mk_bool_sort(ctx));
-  Z3_ast c1 = Z3_mk_eq(ctx,x,Z3_mk_true(ctx));
-  Z3_ast c2 = Z3_mk_eq(ctx,x,Z3_mk_false(ctx));
-
-#endif
-
-  constraints[0] = c1;
-  constraints[1] = c2;
-  
-  /* print out the result for grins. */
-
-  // Z3_string smtout = Z3_benchmark_to_smtlib_string (ctx, "foo", "QFLIA", "sat", "", num, constraints, Z3_mk_true(ctx));
-
-  // Z3_string smtout = Z3_ast_to_string(ctx,constraints[0]);
-  // Z3_string smtout = Z3_context_to_string(ctx);
-  // puts(smtout);
-
-  iz3_print(ctx,num,constraints,"iZ3temp.smt");
-
-  /* Make room for interpolants. */
-
-  Z3_ast *interpolants = (Z3_ast *)malloc((num-1) * sizeof(Z3_ast));
-
-  /* Make room for the model. */
-
-  Z3_model model = 0;
-
-  /* Call the prover */
-
-  Z3_lbool result = iz3_interpolate(ctx, num, constraints, interpolants, &model);
-
-  switch (result) {
-  
-    /* If UNSAT, print the interpolants */
-  case Z3_L_FALSE:
-    printf("unsat, interpolants:\n");
-    for(i = 0; i < num-1; i++)
-      printf("%s\n", Z3_ast_to_string(ctx, interpolants[i]));
-    break;
-  case Z3_L_UNDEF:
-    printf("fail\n");
-    break;
-  case Z3_L_TRUE:
-    printf("sat\n");
-    printf("model:\n%s\n", Z3_model_to_string(ctx, model));
-    break;
-  }
-
-  /* Delete the model if there is one */
-  
-  if (model)
-    Z3_del_model(ctx, model);
-  
-  /* Delete logical context (note, we call iz3_del_context, not
-     Z3_del_context */
-
-  iz3_del_context(ctx);
-
-  return 1;
-}
-
-struct z3_error {
-  Z3_error_code c;
-  z3_error(Z3_error_code _c) : c(_c) {}
-};
-
-extern "C" {
-  static void throw_z3_error(Z3_error_code c){
-    throw z3_error(c);
-  }
-}
-
-int main(int argc, const char **argv) {
-
-  /* Create a Z3 context to contain formulas */
-
-  Z3_config cfg = Z3_mk_config();
-  Z3_context ctx = iz3_mk_context(cfg);
-  Z3_set_error_handler(ctx, throw_z3_error);
-    
-  /* Make some constraints, by parsing an smtlib formatted file given as arg 1 */
-
-  try {
-    Z3_parse_smtlib_file(ctx, argv[1], 0, 0, 0, 0, 0, 0);
-  }
-  catch(const z3_error &err){
-    std::cerr << "Z3 error: " << Z3_get_error_msg(err.c) << "\n";
-    std::cerr << Z3_get_smtlib_error(ctx) << "\n";
-    return(1);
-  } 
-
-  /* Get the constraints from the parser. */
-
-  int num = Z3_get_smtlib_num_formulas(ctx);
-
-  if(num == 0){
-    std::cerr << "iZ3 error: File contains no formulas.\n";
-    return 1;
-  }
-
-
-  Z3_ast *constraints = (Z3_ast *)malloc(num * sizeof(Z3_ast));
-
-  int i;
-  for (i = 0; i < num; i++)
-    constraints[i] = Z3_get_smtlib_formula(ctx, i);
-
-  /* if we get only one formula, and it is a conjunction, split it into conjuncts. */
-  if(num == 1){
-    Z3_app app = Z3_to_app(ctx,constraints[0]);
-    Z3_func_decl func = Z3_get_app_decl(ctx,app);
-    Z3_decl_kind dk = Z3_get_decl_kind(ctx,func);
-    if(dk == Z3_OP_AND){
-      int nconjs = Z3_get_app_num_args(ctx,app);
-      if(nconjs > 1){
-	std::cout << "Splitting formula into " << nconjs << " conjuncts...\n";
-	num = nconjs;
-	constraints = new Z3_ast[num];
-	for(int k = 0; k < num; k++)
-	  constraints[k] = Z3_get_app_arg(ctx,app,k);
-      }
-    }
-  }
-
-
-  /* print out the result for grins. */
-
-  // Z3_string smtout = Z3_benchmark_to_smtlib_string (ctx, "foo", "QFLIA", "sat", "", num, constraints, Z3_mk_true(ctx));
-
-  // Z3_string smtout = Z3_ast_to_string(ctx,constraints[0]);
-  // Z3_string smtout = Z3_context_to_string(ctx);
-  // puts(smtout);
-
-  // iz3_print(ctx,num,constraints,"iZ3temp.smt");
-
-  /* Make room for interpolants. */
-
-  Z3_ast *interpolants = (Z3_ast *)malloc((num-1) * sizeof(Z3_ast));
-
-  /* Make room for the model. */
-
-  Z3_model model = 0;
-
-  /* Call the prover */
-
-  Z3_lbool result = iz3_interpolate(ctx, num, constraints, interpolants, &model);
-
-  switch (result) {
-  
-    /* If UNSAT, print the interpolants */
-  case Z3_L_FALSE:
-    printf("unsat, interpolants:\n");
-    for(i = 0; i < num-1; i++)
-      printf("%s\n", Z3_ast_to_string(ctx, interpolants[i]));
-    std::cout << "Checking interpolants...\n";
-    const char *error;
-    if(iZ3_check_interpolant(ctx, num, constraints, 0, interpolants, &error))
-      std::cout << "Interpolant is correct\n";
-    else {
-      std::cout << "Interpolant is incorrect\n";
-      std::cout << error << "\n";
-    }
-    break;
-  case Z3_L_UNDEF:
-    printf("fail\n");
-    break;
-  case Z3_L_TRUE:
-    printf("sat\n");
-    printf("model:\n%s\n", Z3_model_to_string(ctx, model));
-    break;
-  }
-
-  /* Delete the model if there is one */
-  
-  if (model)
-    Z3_del_model(ctx, model);
-  
-  /* Delete logical context (note, we call iz3_del_context, not
-     Z3_del_context */
-
-  iz3_del_context(ctx);
-
-  return 0;
-}
-
-#endif

scripts/mk_project.py

@@ -94,7 +94,6 @@ def init_project_def():
     set_z3py_dir('api/python')
     # Examples
     add_cpp_example('cpp_example', 'c++') 
-    add_cpp_example('iz3', 'interp') 
     add_cpp_example('z3_tptp', 'tptp') 
     add_c_example('c_example', 'c')
     add_c_example('maxsat')

scripts/mk_util.py

@@ -90,7 +90,13 @@ FPMATH="Default"
 FPMATH_FLAGS="-mfpmath=sse -msse -msse2"
 
 def check_output(cmd):
-    return (subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]).decode("utf-8").rstrip('\r\n')
+    out = subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]
+    if out != None:
+        enc = sys.stdout.encoding
+        if enc != None: return out.decode(enc).rstrip('\r\n')
+        else: return out.rstrip('\r\n')
+    else:
+        return ""
 
 def git_hash():
     try:
@@ -2586,7 +2592,7 @@ def mk_z3consts_py(api_files):
     if Z3PY_SRC_DIR is None:
         raise MKException("You must invoke set_z3py_dir(path):")
 
-    blank_pat      = re.compile("^ *$")
+    blank_pat      = re.compile("^ *\r?$")
     comment_pat    = re.compile("^ *//.*$")
     typedef_pat    = re.compile("typedef enum *")
     typedef2_pat   = re.compile("typedef enum { *")
@@ -2647,6 +2653,8 @@ def mk_z3consts_py(api_files):
                         z3consts.write('%s = %s\n' % (k, i))
                     z3consts.write('\n')
                     mode = SEARCHING
+                elif len(words) <= 2:
+                    assert False, "Invalid %s, line: %s" % (api_file, linenum)
                 else:
                     if words[2] != '':
                         if len(words[2]) > 1 and words[2][1] == 'x':
@@ -2664,7 +2672,7 @@ def mk_z3consts_py(api_files):
 
 # Extract enumeration types from z3_api.h, and add .Net definitions
 def mk_z3consts_dotnet(api_files):
-    blank_pat      = re.compile("^ *$")
+    blank_pat      = re.compile("^ *\r?$")
     comment_pat    = re.compile("^ *//.*$")
     typedef_pat    = re.compile("typedef enum *")
     typedef2_pat   = re.compile("typedef enum { *")
@@ -2734,6 +2742,8 @@ def mk_z3consts_dotnet(api_files):
                             z3consts.write('  %s = %s,\n' % (k, i))
                         z3consts.write('  }\n\n')
                     mode = SEARCHING
+                elif len(words) <= 2:
+                    assert False, "Invalid %s, line: %s" % (api_file, linenum)
                 else:
                     if words[2] != '':
                         if len(words[2]) > 1 and words[2][1] == 'x':

scripts/update_api.py

@@ -96,7 +96,12 @@ if sys.version < '3':
      return s
 else:
   def _to_pystr(s):
-     return s.decode('utf-8')
+     if s != None:
+        enc = sys.stdout.encoding
+        if enc != None: return s.decode(enc)
+        else: return s.decode('ascii')
+     else:
+        return ""
 
 def init(PATH):
   global _lib

src/api/api_array.cpp

@@ -187,6 +187,7 @@ extern "C" {
     MK_BINARY(Z3_mk_set_difference, mk_c(c)->get_array_fid(), OP_SET_DIFFERENCE, SKIP);
     MK_UNARY(Z3_mk_set_complement, mk_c(c)->get_array_fid(), OP_SET_COMPLEMENT, SKIP);
     MK_BINARY(Z3_mk_set_subset, mk_c(c)->get_array_fid(), OP_SET_SUBSET, SKIP);
+    MK_BINARY(Z3_mk_array_ext, mk_c(c)->get_array_fid(), OP_ARRAY_EXT, SKIP);
 
     Z3_ast Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set) {
         return Z3_mk_select(c, set, elem);

src/api/api_ast.cpp

@@ -1012,6 +1012,7 @@ extern "C" {
             case OP_SET_COMPLEMENT: return Z3_OP_SET_COMPLEMENT;
             case OP_SET_SUBSET: return Z3_OP_SET_SUBSET;
             case OP_AS_ARRAY: return Z3_OP_AS_ARRAY;
+            case OP_ARRAY_EXT: return Z3_OP_ARRAY_EXT;
             default:
                 UNREACHABLE();
                 return Z3_OP_UNINTERPRETED;

src/api/api_context.cpp

@@ -104,8 +104,6 @@ namespace api {
         m_smtlib_parser           = 0;
         m_smtlib_parser_has_decls = false;
                 
-        z3_bound_num_procs();
-        
         m_error_handler = &default_error_handler;
 
         m_basic_fid = m().get_basic_family_id();

src/api/api_solver.cpp

@@ -97,6 +97,20 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_solver Z3_API Z3_solver_translate(Z3_context c, Z3_solver s, Z3_context target) {
+        Z3_TRY;
+        LOG_Z3_solver_translate(c, s, target);
+        RESET_ERROR_CODE();
+        params_ref const& p = to_solver(s)->m_params; 
+        Z3_solver_ref * sr = alloc(Z3_solver_ref, 0);
+        init_solver(c, s);
+        sr->m_solver = to_solver(s)->m_solver->translate(mk_c(target)->m(), p);
+        mk_c(target)->save_object(sr);
+        Z3_solver r = of_solver(sr);
+        RETURN_Z3(r);
+        Z3_CATCH_RETURN(0);
+    }
+
     Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s) {
         Z3_TRY;
         LOG_Z3_solver_get_help(c, s);

src/api/api_solver_old.cpp

@@ -23,6 +23,8 @@ Revision History:
 #include"api_context.h"
 #include"api_model.h"
 #include"cancel_eh.h"
+#include"scoped_timer.h"
+#include"rlimit.h"
 
 extern "C" {
 
@@ -75,8 +77,13 @@ extern "C" {
         cancel_eh<smt::kernel> eh(mk_c(c)->get_smt_kernel());
         api::context::set_interruptable si(*(mk_c(c)), eh);
         flet<bool> _model(mk_c(c)->fparams().m_model, true);
+        unsigned timeout = mk_c(c)->params().m_timeout;
+        unsigned rlimit = mk_c(c)->params().m_rlimit;
         lbool result;
         try {
+            scoped_timer timer(timeout, &eh);
+            scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
+
             model_ref _m;
             result = mk_c(c)->check(_m);
             if (m) {

src/api/c++/z3++.h

@@ -1359,9 +1359,13 @@ namespace z3 {
             Z3_solver_inc_ref(ctx(), s);
         }
     public:
+        struct simple {};
+        struct translate {};
         solver(context & c):object(c) { init(Z3_mk_solver(c)); }
+        solver(context & c, simple):object(c) { init(Z3_mk_simple_solver(c)); }
         solver(context & c, Z3_solver s):object(c) { init(s); }
         solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }
+        solver(context & c, solver const& src, translate): object(c) { init(Z3_solver_translate(src.ctx(), src, c)); }
         solver(solver const & s):object(s) { init(s.m_solver); }
         ~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
         operator Z3_solver() const { return m_solver; }

src/api/dotnet/Context.cs

@@ -2122,6 +2122,21 @@ namespace Microsoft.Z3
             CheckContextMatch(array);
             return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
         }
+
+        /// <summary>
+        /// Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt.
+        /// </summary>
+        public Expr MkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
+        {
+            Contract.Requires(arg1 != null);
+            Contract.Requires(arg2 != null);
+            Contract.Ensures(Contract.Result<Expr>() != null);
+
+            CheckContextMatch(arg1);
+            CheckContextMatch(arg2);
+            return Expr.Create(this, Native.Z3_mk_array_ext(nCtx, arg1.NativeObject, arg2.NativeObject));
+        }
+
         #endregion
 
         #region Sets
@@ -2268,6 +2283,7 @@ namespace Microsoft.Z3
             CheckContextMatch(arg2);
             return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
         }
+
         #endregion
 
         #region Pseudo-Boolean constraints
@@ -2597,8 +2613,13 @@ namespace Microsoft.Z3
         /// <paramref name="patterns"/> is an array of patterns, <paramref name="sorts"/> is an array
         /// with the sorts of the bound variables, <paramref name="names"/> is an array with the
         /// 'names' of the bound variables, and <paramref name="body"/> is the body of the
-        /// quantifier. Quantifiers are associated with weights indicating
+        /// quantifier. Quantifiers are associated with weights indicating the importance of 
-        /// the importance of using the quantifier during instantiation.
+        /// using the quantifier during instantiation.
+        /// Note that the bound variables are de-Bruijn indices created using <see cref="MkBound"/>. 
+        /// Z3 applies the convention that the last element in <paramref name="names"/> and 
+        /// <paramref name="sorts"/> refers to the variable with index 0, the second to last element 
+        /// of <paramref name="names"/> and <paramref name="sorts"/> refers to the variable 
+        /// with index 1, etc. 
         /// </remarks>
         /// <param name="sorts">the sorts of the bound variables.</param>
         /// <param name="names">names of the bound variables</param>
@@ -2628,6 +2649,11 @@ namespace Microsoft.Z3
         /// <summary>
         /// Create a universal Quantifier.
         /// </summary>
+        /// <remarks>
+        /// Creates a universal quantifier using a list of constants that will 
+        /// form the set of bound variables. 
+        /// <seealso cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
+        /// </remarks>
         public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
         {
             Contract.Requires(body != null);
@@ -2643,7 +2669,10 @@ namespace Microsoft.Z3
         /// <summary>
         /// Create an existential Quantifier.
         /// </summary>
-        /// <seealso cref="MkForall(Sort[],Symbol[],Expr,uint,Pattern[],Expr[],Symbol,Symbol)"/>
+        /// <remarks>
+        /// Creates an existential quantifier using de-Brujin indexed variables. 
+        /// (<see cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>).
+        /// </remarks>
         public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
         {
             Contract.Requires(sorts != null);
@@ -2662,6 +2691,11 @@ namespace Microsoft.Z3
         /// <summary>
         /// Create an existential Quantifier.
         /// </summary>
+        /// <remarks>
+        /// Creates an existential quantifier using a list of constants that will 
+        /// form the set of bound variables. 
+        /// <seealso cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
+        /// </remarks>
         public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
         {
             Contract.Requires(body != null);
@@ -2677,6 +2711,7 @@ namespace Microsoft.Z3
         /// <summary>
         /// Create a Quantifier.
         /// </summary>
+        /// <see cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
         public Quantifier MkQuantifier(bool universal, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
         {
             Contract.Requires(body != null);
@@ -2700,6 +2735,7 @@ namespace Microsoft.Z3
         /// <summary>
         /// Create a Quantifier.
         /// </summary>
+        /// <see cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
         public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
         {
             Contract.Requires(body != null);

src/api/dotnet/Solver.cs

@@ -290,6 +290,17 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// Create a clone of the current solver with respect to <c>ctx</c>.
+        /// </summary>
+        public Solver Translate(Context ctx) 
+        {
+	     Contract.Requires(ctx != null);
+             Contract.Ensures(Contract.Result<Solver>() != null);
+             return new Solver(ctx, Native.Z3_solver_translate(Context.nCtx, NativeObject, ctx.nCtx));
+        }
+
+
         /// <summary>
         /// Solver statistics.
         /// </summary>

src/api/java/Context.java

@@ -433,8 +433,8 @@ public class Context extends IDisposable
     /**
      * Creates a fresh function declaration with a name prefixed with
      * {@code prefix}. 
-     * @see mkFuncDecl(String,Sort,Sort)
+     * @see #mkFuncDecl(String,Sort,Sort)
-     * @see mkFuncDecl(String,Sort[],Sort)
+     * @see #mkFuncDecl(String,Sort[],Sort)
      **/
     public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
            
@@ -1717,6 +1717,17 @@ public class Context extends IDisposable
                 Native.mkArrayDefault(nCtx(), array.getNativeObject()));
     }
 
+    /**
+     * Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt.
+     **/
+    public Expr mkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
+    {
+    checkContextMatch(arg1);
+    checkContextMatch(arg2);
+    return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
+    }
+
+
     /**
      * Create a set type.
      **/
@@ -2014,6 +2025,7 @@ public class Context extends IDisposable
 
     /**
      * Create a universal Quantifier.
+     *
      * @param sorts the sorts of the bound variables. 
      * @param names names of the bound variables 
      * @param body the body of the quantifier. 
@@ -2023,17 +2035,22 @@ public class Context extends IDisposable
      * @param quantifierID optional symbol to track quantifier. 
      * @param skolemID optional symbol to track skolem constants.
      * 
-     * Remarks:  Creates a forall formula, where
+     * @return Creates a forall formula, where
-     * {@code weight"/> is the weight, <paramref name="patterns} is
+     * {@code weight} is the weight, {@code patterns} is
      * an array of patterns, {@code sorts} is an array with the sorts
      * of the bound variables, {@code names} is an array with the
      * 'names' of the bound variables, and {@code body} is the body
      * of the quantifier. Quantifiers are associated with weights indicating the
      * importance of using the quantifier during instantiation.
+     * Note that the bound variables are de-Bruijn indices created using {@link mkBound}.
+     * Z3 applies the convention that the last element in {@code names} and 
+     * {@code sorts} refers to the variable with index 0, the second to last element 
+     * of {@code names} and {@code sorts} refers to the variable 
+     * with index 1, etc. 
      **/
     public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body,
-            int weight, Pattern[] patterns, Expr[] noPatterns,
+                               int weight, Pattern[] patterns, Expr[] noPatterns,
-            Symbol quantifierID, Symbol skolemID)
+                               Symbol quantifierID, Symbol skolemID)
     {
 
         return new Quantifier(this, true, sorts, names, body, weight, patterns,
@@ -2041,11 +2058,12 @@ public class Context extends IDisposable
     }
 
     /**
-     * Create a universal Quantifier.
+     * Creates a universal quantifier using a list of constants that will form the set of bound variables. 
+     * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
     public Quantifier mkForall(Expr[] boundConstants, Expr body, int weight,
-            Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
+                               Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
-            Symbol skolemID)
+                               Symbol skolemID)
     {
 
         return new Quantifier(this, true, boundConstants, body, weight,
@@ -2053,12 +2071,12 @@ public class Context extends IDisposable
     }
 
     /**
-     * Create an existential Quantifier. 
+     * Creates an existential quantifier using de-Brujin indexed variables. 
      * @see mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
     public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body,
-            int weight, Pattern[] patterns, Expr[] noPatterns,
+                               int weight, Pattern[] patterns, Expr[] noPatterns,
-            Symbol quantifierID, Symbol skolemID)
+                               Symbol quantifierID, Symbol skolemID)
     {
 
         return new Quantifier(this, false, sorts, names, body, weight,
@@ -2066,11 +2084,12 @@ public class Context extends IDisposable
     }
 
     /**
-     * Create an existential Quantifier.
+     * Creates an existential quantifier using a list of constants that will form the set of bound variables. 
+     * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
     public Quantifier mkExists(Expr[] boundConstants, Expr body, int weight,
-            Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
+                               Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
-            Symbol skolemID)
+                               Symbol skolemID)
     {
 
         return new Quantifier(this, false, boundConstants, body, weight,
@@ -2079,10 +2098,11 @@ public class Context extends IDisposable
 
     /**
      * Create a Quantifier.
+     * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
     public Quantifier mkQuantifier(boolean universal, Sort[] sorts,
-            Symbol[] names, Expr body, int weight, Pattern[] patterns,
+                                   Symbol[] names, Expr body, int weight, Pattern[] patterns,
-            Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
+                                   Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
         
     {
 
@@ -2095,11 +2115,12 @@ public class Context extends IDisposable
     }
 
     /**
-     * Create a Quantifier.
+     * Create a Quantifier
+     * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
     public Quantifier mkQuantifier(boolean universal, Expr[] boundConstants,
-            Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
+                                   Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
-            Symbol quantifierID, Symbol skolemID)
+                                   Symbol quantifierID, Symbol skolemID)
     {
 
         if (universal)

src/api/java/Solver.java

@@ -293,6 +293,14 @@ public class Solver extends Z3Object
                 getNativeObject());
     }
 
+    /**
+     * Create a clone of the current solver with respect to <c>ctx</c>.
+     */
+    public Solver translate(Context ctx) 
+    {
+	return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
+    }
+
     /**
      * Solver statistics.
      * 

src/api/ml/z3.ml

@@ -1217,6 +1217,9 @@ struct
 
   let mk_term_array  ( ctx : context ) ( arg : expr ) =
     expr_of_ptr ctx (Z3native.mk_array_default (context_gno ctx) (Expr.gno arg))
+
+  let mk_array_ext ( ctx : context) ( arg1 : expr ) ( arg2 : expr ) =
+	expr_of_ptr ctx (Z3native.mk_array_ext (context_gno ctx) (Expr.gno arg1) (Expr.gno arg2))
 end
 
 
@@ -2740,10 +2743,13 @@ struct
     mk_solver ctx (Some (Symbol.mk_string ctx logic))
 
   let mk_simple_solver ( ctx : context ) =
-    (create ctx (Z3native.mk_simple_solver (context_gno ctx)))
+    create ctx (Z3native.mk_simple_solver (context_gno ctx))
 
   let mk_solver_t ( ctx : context ) ( t : Tactic.tactic ) = 
-    (create ctx (Z3native.mk_solver_from_tactic (context_gno ctx) (z3obj_gno t)))
+    create ctx (Z3native.mk_solver_from_tactic (context_gno ctx) (z3obj_gno t))
+
+  let translate  ( x : solver ) ( to_ctx : context ) =
+	create to_ctx (Z3native.solver_translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx))
 
   let to_string ( x : solver ) = Z3native.solver_to_string (z3obj_gnc x) (z3obj_gno x)
 end

src/api/ml/z3.mli

@@ -864,8 +864,15 @@ sig
   (** Access the array default value.
       
       Produces the default range value, for arrays that can be represented as 
-      finite maps with a default range value.     *)
+      finite maps with a default range value. *)
   val mk_term_array : context -> Expr.expr -> Expr.expr
+
+  (** Create array extensionality index given two arrays with the same sort. 
+
+      The meaning is given by the axiom:
+          (=> (= (select A (array-ext A B)) (select B (array-ext A B))) (= A B)) *)
+  val mk_array_ext : context -> Expr.expr -> Expr.expr -> Expr.expr
+
 end
 
 (** Functions to manipulate Set expressions *)
@@ -1185,36 +1192,36 @@ sig
     val mk_const_s : context -> string -> Expr.expr
 
     (** Create an expression representing [t1 mod t2].
-		The arguments must have int type. *)
+        The arguments must have int type. *)
     val mk_mod : context -> Expr.expr -> Expr.expr -> Expr.expr
 
     (** Create an expression representing [t1 rem t2].
-		The arguments must have int type. *)
+        The arguments must have int type. *)
     val mk_rem : context -> Expr.expr -> Expr.expr -> Expr.expr
 
     (** Create an integer numeral. *)
     val mk_numeral_s : context -> string -> Expr.expr
 
     (** Create an integer numeral.
-		@return A Term with the given value and sort Integer *)
+        @return A Term with the given value and sort Integer *)
     val mk_numeral_i : context -> int -> Expr.expr
 
     (** Coerce an integer to a real.    
         
-		There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard.
+        There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard.
         
-		You can take the floor of a real by creating an auxiliary integer Term [k] and
+        You can take the floor of a real by creating an auxiliary integer Term [k] and
-		and asserting [MakeInt2Real(k) <= t1 < MkInt2Real(k)+1].
+        and asserting [MakeInt2Real(k) <= t1 < MkInt2Real(k)+1].
-		The argument must be of integer sort. *)
+        The argument must be of integer sort. *)
     val mk_int2real : context -> Expr.expr -> Expr.expr
 
     (**   Create an n-bit bit-vector from an integer argument.  
           
-		  NB. This function is essentially treated as uninterpreted. 
+          NB. This function is essentially treated as uninterpreted. 
-		  So you cannot expect Z3 to precisely reflect the semantics of this function
+          So you cannot expect Z3 to precisely reflect the semantics of this function
-		  when solving constraints with this function.
+          when solving constraints with this function.
           
-		  The argument must be of integer sort. *)
+          The argument must be of integer sort. *)
     val mk_int2bv : context -> int -> Expr.expr -> Expr.expr
   end
 
@@ -1234,7 +1241,7 @@ sig
     val get_ratio : Expr.expr -> Ratio.ratio
 
     (** Returns a string representation in decimal notation. 
-		The result has at most as many decimal places as indicated by the int argument.*)
+        The result has at most as many decimal places as indicated by the int argument.*)
     val to_decimal_string : Expr.expr-> int -> string
 
     (** Returns a string representation of a numeral. *)
@@ -1247,16 +1254,16 @@ sig
     val mk_const_s : context -> string -> Expr.expr
 
     (** Create a real numeral from a fraction.       
-		@return A Term with rational value and sort Real
+        @return A Term with rational value and sort Real
-		{!mk_numeral_s} *)
+        {!mk_numeral_s} *)
     val mk_numeral_nd : context -> int -> int -> Expr.expr
 
     (** Create a real numeral.
-		@return A Term with the given value and sort Real *)
+        @return A Term with the given value and sort Real *)
     val mk_numeral_s : context -> string -> Expr.expr
 
     (** Create a real numeral.
-		@return A Term with the given value and sort Real *)
+        @return A Term with the given value and sort Real *)
     val mk_numeral_i : context -> int -> Expr.expr
 
     (** Creates an expression that checks whether a real number is an integer. *)
@@ -1264,27 +1271,27 @@ sig
 
     (** Coerce a real to an integer.
 
-		The semantics of this function follows the SMT-LIB standard for the function to_int.
+        The semantics of this function follows the SMT-LIB standard for the function to_int.
-		The argument must be of real sort. *)
+        The argument must be of real sort. *)
     val mk_real2int : context -> Expr.expr -> Expr.expr
       
     (** Algebraic Numbers *)
     module AlgebraicNumber :
     sig
       (** Return a upper bound for a given real algebraic number. 
-		  The interval isolating the number is smaller than 1/10^precision.
+          The interval isolating the number is smaller than 1/10^precision.
-		  {!is_algebraic_number}   
+          {!is_algebraic_number}   
-		  @return A numeral Expr of sort Real *)
+          @return A numeral Expr of sort Real *)
       val to_upper : Expr.expr -> int -> Expr.expr
         
       (** Return a lower bound for the given real algebraic number. 
-		  The interval isolating the number is smaller than 1/10^precision.
+          The interval isolating the number is smaller than 1/10^precision.
-		  {!is_algebraic_number}
+          {!is_algebraic_number}
-		  @return A numeral Expr of sort Real *)
+          @return A numeral Expr of sort Real *)
       val to_lower : Expr.expr -> int -> Expr.expr
         
       (** Returns a string representation in decimal notation. 
-		  The result has at most as many decimal places as the int argument provided.*)
+          The result has at most as many decimal places as the int argument provided.*)
       val to_decimal_string : Expr.expr -> int -> string
         
       (** Returns a string representation of a numeral. *)
@@ -1849,40 +1856,40 @@ sig
   (** Rounding Modes *)    
   module RoundingMode :
   sig
-	(** Create the RoundingMode sort. *)
+    (** Create the RoundingMode sort. *)
     val mk_sort : context -> Sort.sort
 
-	(** Indicates whether the terms is of floating-point rounding mode sort. *)
+    (** Indicates whether the terms is of floating-point rounding mode sort. *)
     val is_fprm : Expr.expr -> bool
 
-	(** Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. *)
+    (** Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. *)
     val mk_round_nearest_ties_to_even : context -> Expr.expr
       
-	(** Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. *)
+    (** Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. *)
     val mk_rne : context -> Expr.expr
 
-	(** Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. *)
+    (** Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. *)
     val mk_round_nearest_ties_to_away : context -> Expr.expr
       
-	(** Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. *)
+    (** Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. *)
     val mk_rna : context -> Expr.expr
       
-	(** Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. *)
+    (** Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. *)
     val mk_round_toward_positive : context -> Expr.expr
       
-	(** Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. *)
+    (** Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. *)
-	val mk_rtp : context -> Expr.expr
+    val mk_rtp : context -> Expr.expr
       
-	(** Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. *)
+    (** Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. *)
     val mk_round_toward_negative : context -> Expr.expr
       
-	(** Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. *)
+    (** Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. *)
     val mk_rtn : context -> Expr.expr
       
-	(** Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. *)
+    (** Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. *)
     val mk_round_toward_zero : context -> Expr.expr
       
-	(** Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. *)
+    (** Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. *)
     val mk_rtz : context -> Expr.expr
   end
 
@@ -1924,7 +1931,7 @@ sig
 
   (** Create an expression of FloatingPoint sort from three bit-vector expressions. 
 
-	  This is the operator named `fp' in the SMT FP theory definition.
+      This is the operator named `fp' in the SMT FP theory definition.
       Note that \c sign is required to be a bit-vector of size 1. Significand and exponent 
       are required to be greater than 1 and 2 respectively. The FloatingPoint sort 
       of the resulting expression is automatically determined from the bit-vector sizes
@@ -2079,8 +2086,8 @@ sig
     
   (** Floating-point roundToIntegral. 
 
-	  Rounds a floating-point number to the closest integer, 
+      Rounds a floating-point number to the closest integer, 
-	  again represented as a floating-point number. *)
+      again represented as a floating-point number. *)
   val mk_round_to_integral : context -> Expr.expr -> Expr.expr -> Expr.expr
 
   (** Minimum of floating-point numbers. *)
@@ -2162,7 +2169,7 @@ sig
   val get_numeral_significand_string : context -> Expr.expr -> string
 
   (** Return the significand value of a floating-point numeral as a uint64. 
-	  Remark: This function extracts the significand bits, without the 
+      Remark: This function extracts the significand bits, without the 
       hidden bit or normalization. Throws an exception if the
       significand does not fit into a uint64. *)
   val get_numeral_significand_uint : context -> Expr.expr -> bool * int
@@ -2675,7 +2682,7 @@ sig
       
     (** Function interpretations entries 
 
-		An Entry object represents an element in the finite map used to a function interpretation. *)  
+        An Entry object represents an element in the finite map used to a function interpretation. *)  
     module FuncEntry :
     sig
       type func_entry 
@@ -2865,8 +2872,8 @@ sig
     val get_subgoal : apply_result -> int -> Goal.goal
 
     (** Convert a model for a subgoal into a model for the original 
-		goal [g], that the ApplyResult was obtained from. 
+        goal [g], that the ApplyResult was obtained from. 
-		#return A model for [g] *)
+        #return A model for [g] *)
     val convert_model : apply_result -> int -> Model.model -> Model.model
 
     (** A string representation of the ApplyResult. *)
@@ -2959,7 +2966,7 @@ sig
   type statistics 
     
   (** Statistical data is organized into pairs of \[Key, Entry\], where every
-	  Entry is either a floating point or integer value. *)
+      Entry is either a floating point or integer value. *)
   module Entry :
   sig
     type statistics_entry
@@ -3123,6 +3130,9 @@ sig
       will always solve each check from scratch. *)
   val mk_solver_t : context -> Tactic.tactic -> solver
         
+  (** Create a clone of the current solver with respect to a context. *)
+  val translate : solver -> context -> solver
+
   (** A string representation of the solver. *)
   val to_string : solver -> string
 end

src/api/python/z3.py

@@ -1,3 +1,4 @@
+
 ############################################
 # Copyright (c) 2012 Microsoft Corporation
 # 
@@ -4143,6 +4144,13 @@ def K(dom, v):
         v = _py2expr(v, ctx)
     return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx)
 
+def Ext(a, b):
+    """Return extensionality index for arrays.
+    """
+    if __debug__:
+        _z3_assert(is_array(a) and is_array(b))
+    return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()));
+
 def is_select(a):
     """Return `True` if `a` is a Z3 array select application.
     
@@ -4854,7 +4862,7 @@ class Goal(Z3PPObject):
         elif sz == 1:
             return self.get(0)
         else:
-            return And([ self.get(i) for i in range(len(self)) ])
+            return And([ self.get(i) for i in range(len(self)) ], self.ctx)
 
 #########################################
 #
@@ -6084,6 +6092,19 @@ class Solver(Z3PPObject):
         """Return a formatted string with all added constraints."""
         return obj_to_string(self)
 
+    def translate(self, target):
+        """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`. 
+        
+        >>> c1 = Context()
+        >>> c2 = Context()
+        >>> s1 = Solver(ctx=c1)
+        >>> s2 = s1.translate(c2)
+        """
+        if __debug__:
+            _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
+        solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
+        return Solver(solver, target)
+    
     def sexpr(self):
         """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
         

src/api/python/z3printer.py

@@ -31,7 +31,7 @@ _z3_op_to_str = {
     Z3_OP_BASHR : '>>', Z3_OP_BSHL : '<<', Z3_OP_BLSHR : 'LShR', 
     Z3_OP_CONCAT : 'Concat', Z3_OP_EXTRACT : 'Extract', Z3_OP_BV2INT : 'BV2Int',
     Z3_OP_ARRAY_MAP : 'Map', Z3_OP_SELECT : 'Select', Z3_OP_STORE : 'Store', 
-    Z3_OP_CONST_ARRAY : 'K',
+    Z3_OP_CONST_ARRAY : 'K', Z3_OP_ARRAY_EXT : 'Ext', 
     Z3_OP_PB_AT_MOST : 'AtMost', Z3_OP_PB_LE : 'PbLe', Z3_OP_PB_GE : 'PbGe'
     }
 
@@ -1157,7 +1157,13 @@ def set_pp_option(k, v):
 def obj_to_string(a):
     out = io.StringIO()
     _PP(out, _Formatter(a))
-    return out.getvalue()
+    r = out.getvalue()
+    if sys.version < '3':
+        return r
+    else:
+        enc = sys.stdout.encoding
+        if enc != None: return r.decode(enc)
+        return r
 
 _html_out = None
 

src/api/z3_api.h

@@ -322,6 +322,9 @@ typedef enum
    - Z3_OP_AS_ARRAY An array value that behaves as the function graph of the
                     function passed as parameter.
 
+   - Z3_OP_ARRAY_EXT Array extensionality function. It takes two arrays as arguments and produces an index, such that the arrays
+                    are different if they are different on the index.
+
    - Z3_OP_BNUM Bit-vector numeral.
 
    - Z3_OP_BIT1 One bit bit-vector.
@@ -1033,6 +1036,7 @@ typedef enum {
     Z3_OP_SET_COMPLEMENT,
     Z3_OP_SET_SUBSET,
     Z3_OP_AS_ARRAY,
+    Z3_OP_ARRAY_EXT,
 
     // Bit-vectors
     Z3_OP_BNUM = 0x400,
@@ -3260,6 +3264,17 @@ END_MLAPI_EXCLUDE
     Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2);
     /*@}*/
 
+    /**
+       \brief Create array extensionality index given two arrays with the same sort. 
+              The meaning is given by the axiom:
+              (=> (= (select A (array-ext A B)) (select B (array-ext A B))) (= A B))
+
+       def_API('Z3_mk_array_ext', AST, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+
+    Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2);
+    /*@}*/
+
     /**
        @name Numerals
     */
@@ -7062,6 +7077,14 @@ END_MLAPI_EXCLUDE
     */
     Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t);
 
+    /**
+       \brief Copy a solver \c s from the context \c source to a the context \c target.
+
+       def_API('Z3_solver_translate', SOLVER, (_in(CONTEXT), _in(SOLVER), _in(CONTEXT)))
+    */
+    Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target);
+    
+
     /**
        \brief Return a string describing all solver available parameters.
 

src/ast/array_decl_plugin.cpp

@@ -293,7 +293,7 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) {
                                    func_decl_info(m_family_id, OP_STORE));
 }
 
-func_decl * array_decl_plugin::mk_array_ext_skolem(unsigned arity, sort * const * domain, unsigned i) {
+func_decl * array_decl_plugin::mk_array_ext(unsigned arity, sort * const * domain, unsigned i) {
     if (arity != 2 || domain[0] != domain[1]) {
         UNREACHABLE();
         return 0;
@@ -306,7 +306,7 @@ func_decl * array_decl_plugin::mk_array_ext_skolem(unsigned arity, sort * const
     }
     sort * r = to_sort(s->get_parameter(i).get_ast());
     parameter param(s);
-    return m_manager->mk_func_decl(m_array_ext_sym, arity, domain, r, func_decl_info(m_family_id, OP_ARRAY_EXT_SKOLEM, 1, &param));
+    return m_manager->mk_func_decl(m_array_ext_sym, arity, domain, r, func_decl_info(m_family_id, OP_ARRAY_EXT, 1, &param));
 }
 
 
@@ -463,12 +463,15 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
         func_decl * f = to_func_decl(parameters[0].get_ast());
         return mk_map(f, arity, domain);        
     }
-    case OP_ARRAY_EXT_SKOLEM:
+    case OP_ARRAY_EXT:
+        if (num_parameters == 0) {
+            return mk_array_ext(arity, domain, 0);
+        }
         if (num_parameters != 1 || !parameters[0].is_int()) {
             UNREACHABLE();
             return 0;
         }
-        return mk_array_ext_skolem(arity, domain, parameters[0].get_int());
+        return mk_array_ext(arity, domain, parameters[0].get_int());
     case OP_ARRAY_DEFAULT:
         return mk_default(arity, domain);
     case OP_SET_UNION:
@@ -519,6 +522,7 @@ void array_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
         op_names.push_back(builtin_name("complement",OP_SET_COMPLEMENT));
         op_names.push_back(builtin_name("subset",OP_SET_SUBSET));
         op_names.push_back(builtin_name("as-array", OP_AS_ARRAY));
+        op_names.push_back(builtin_name("array-ext", OP_ARRAY_EXT));
     }
 }
 

src/ast/array_decl_plugin.h

@@ -42,7 +42,7 @@ enum array_op_kind {
     OP_STORE,
     OP_SELECT,
     OP_CONST_ARRAY,
-    OP_ARRAY_EXT_SKOLEM,
+    OP_ARRAY_EXT,
     OP_ARRAY_DEFAULT,
     OP_ARRAY_MAP,
     OP_SET_UNION,
@@ -80,7 +80,7 @@ class array_decl_plugin : public decl_plugin {
 
     func_decl * mk_store(unsigned arity, sort * const * domain);
 
-    func_decl * mk_array_ext_skolem(unsigned arity, sort * const * domain, unsigned i);
+    func_decl * mk_array_ext(unsigned arity, sort * const * domain, unsigned i);
 
     func_decl * mk_set_union(unsigned arity, sort * const * domain);
 
@@ -184,6 +184,11 @@ public:
     sort * mk_array_sort(sort* dom, sort* range) { return mk_array_sort(1, &dom, range); }
 
     sort * mk_array_sort(unsigned arity, sort* const* domain, sort* range);
+
+    app * mk_as_array(sort * s, func_decl * f) {
+        parameter param(f);
+        return m_manager.mk_app(m_fid, OP_AS_ARRAY, 1, &param, 0, 0, s);
+    }
 };
 
 

src/ast/ast_translation.cpp

@@ -184,6 +184,7 @@ void ast_translation::mk_func_decl(func_decl * f, frame & fr) {
 }
 
 ast * ast_translation::process(ast const * _n) {
+    if (!_n) return 0;
     SASSERT(m_result_stack.empty());
     SASSERT(m_frame_stack.empty());
     SASSERT(m_extra_children_stack.empty());

src/ast/ast_translation.h

@@ -58,9 +58,9 @@ public:
 
     template<typename T>
     T * operator()(T const * n) { 
-        SASSERT(from().contains(const_cast<T*>(n)));
+        SASSERT(!n || from().contains(const_cast<T*>(n)));
         ast * r = process(n);
-        SASSERT(to().contains(const_cast<ast*>(r)));
+        SASSERT((!n && !r) || to().contains(const_cast<ast*>(r)));
         return static_cast<T*>(r);
     }
 

src/ast/ast_util.cpp

@@ -166,6 +166,11 @@ expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args) {
         return m.mk_and(num_args, args);
 }
 
+app* mk_and(ast_manager & m, unsigned num_args, app * const * args) {
+    return to_app(mk_and(m, num_args, (expr* const*) args));
+}
+
+
 expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args) {
     if (num_args == 0)
         return m.mk_false();
@@ -175,6 +180,10 @@ expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args) {
         return m.mk_or(num_args, args);
 }
 
+app* mk_or(ast_manager & m, unsigned num_args, app * const * args) {
+    return to_app(mk_or(m, num_args, (expr* const*) args));
+}
+
 expr * mk_not(ast_manager & m, expr * arg) {
     expr * atom;
     if (m.is_not(arg, atom))

src/ast/ast_util.h

@@ -107,6 +107,9 @@ expr * get_clause_literal(ast_manager & m, expr * cls, unsigned idx);
    Return true                               if num_args == 0
  */
 expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args);
+app  * mk_and(ast_manager & m, unsigned num_args, app * const * args);
+inline app_ref mk_and(app_ref_vector const& args) { return app_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
+inline expr_ref mk_and(expr_ref_vector const& args) { return expr_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
 
 /**
    Return (or args[0] ... args[num_args-1]) if num_args >= 2
@@ -114,6 +117,10 @@ expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args);
    Return false                             if num_args == 0
  */
 expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args);
+app  * mk_or(ast_manager & m, unsigned num_args, app * const * args);
+inline app_ref mk_or(app_ref_vector const& args) { return app_ref(mk_or(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
+inline expr_ref mk_or(expr_ref_vector const& args) { return expr_ref(mk_or(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
+
 
 /**
    Return a          if arg = (not a)

src/ast/fpa/fpa2bv_converter.cpp

@@ -2648,9 +2648,8 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
 
     SASSERT(num == 2);
     SASSERT(m_util.is_float(f->get_range()));
-    SASSERT(m_bv_util.is_bv(args[0]));
-    SASSERT(m_bv_util.is_bv(args[1]));
     SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
+    SASSERT(m_bv_util.is_bv(args[1]));
 
     expr_ref bv_rm(m), x(m);
     bv_rm = to_app(args[0])->get_arg(0);

src/ast/rewriter/bool_rewriter.cpp

@@ -708,6 +708,19 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
             result = m().mk_eq(lhs, rhs);
             return BR_DONE;
         }
+
+        expr *la, *lb, *ra, *rb;
+        // fold (iff (iff a b) (iff (not a) b)) to false
+        if (m().is_iff(lhs, la, lb) && m().is_iff(rhs, ra, rb)) {
+            expr *n;
+            if ((la == ra && ((m().is_not(rb, n) && n == lb) ||
+                (m().is_not(lb, n) && n == rb))) ||
+                (lb == rb && ((m().is_not(ra, n) && n == la) ||
+                    (m().is_not(la, n) && n == ra)))) {
+                result = m().mk_false();
+                return BR_DONE;
+            }
+        }
     }
     return BR_FAILED;
 }

src/ast/rewriter/var_subst.cpp

@@ -27,7 +27,7 @@ void var_subst::operator()(expr * n, unsigned num_args, expr * const * args, exp
     SASSERT(is_well_sorted(result.m(), n));
     m_reducer.reset();
     if (m_std_order)
-	m_reducer.set_inv_bindings(num_args, args);
+        m_reducer.set_inv_bindings(num_args, args);
     else
         m_reducer.set_bindings(num_args, args);
     m_reducer(n, result);

src/cmd_context/cmd_context.cpp

@@ -1401,9 +1401,10 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
     unsigned rlimit  = m_params.m_rlimit;
     scoped_watch sw(*this);
     lbool r;
+    bool was_pareto = false, was_opt = false;
 
     if (m_opt && !m_opt->empty()) {
-        bool was_pareto = false;
+        was_opt = true;
         m_check_sat_result = get_opt();
         cancel_eh<opt_wrapper> eh(*get_opt());
         scoped_ctrl_c ctrlc(eh);
@@ -1436,9 +1437,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
             r = l_true;
         }
         get_opt()->set_status(r);
-        if (r != l_false && !was_pareto) {
-            get_opt()->display_assignment(regular_stream());
-        }
     }
     else if (m_solver) {
         m_check_sat_result = m_solver.get(); // solver itself stores the result.
@@ -1465,6 +1463,10 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
     }
     display_sat_result(r);
     validate_check_sat_result(r);
+    if (was_opt && r != l_false && !was_pareto) {
+        get_opt()->display_assignment(regular_stream());
+    }
+
     if (r == l_true) {
         validate_model();
         if (m_params.m_dump_models) {

src/cmd_context/context_params.cpp

@@ -48,7 +48,26 @@ void context_params::set_bool(bool & opt, char const * param, char const * value
     }
     else {
         std::stringstream strm;
-        strm << "invalid value '" << value << "' for Boolean parameter '" << param;
+        strm << "invalid value '" << value << "' for Boolean parameter '" << param << "'";
+        throw default_exception(strm.str());
+    }
+}
+
+void context_params::set_uint(unsigned & opt, char const * param, char const * value) {
+    bool is_uint = true;
+    size_t sz = strlen(value);
+    for (unsigned i = 0; i < sz; i++) {
+        if (!(value[i] >= '0' && value[i] <= '9'))
+            is_uint = false;
+    }
+
+    if (is_uint) {
+        long val = strtol(value, 0, 10);
+        opt = static_cast<unsigned>(val);
+    }
+    else {
+        std::stringstream strm;
+        strm << "invalid value '" << value << "' for unsigned int parameter '" << param << "'";
         throw default_exception(strm.str());
     }
 }
@@ -63,12 +82,10 @@ void context_params::set(char const * param, char const * value) {
             p[i] = '_';
     }
     if (p == "timeout") {
-        long val = strtol(value, 0, 10);
+        set_uint(m_timeout, param, value);
-        m_timeout = static_cast<unsigned>(val);
     }
     else if (p == "rlimit") {
-        long val = strtol(value, 0, 10);
+        set_uint(m_rlimit, param, value);
-        m_rlimit = static_cast<unsigned>(val);
     }
     else if (p == "type_check" || p == "well_sorted_check") {
         set_bool(m_well_sorted_check, param, value);

src/cmd_context/context_params.h

@@ -25,6 +25,7 @@ class ast_manager;
 
 class context_params {
     void set_bool(bool & opt, char const * param, char const * value);
+    void set_uint(unsigned & opt, char const * param, char const * value);
 
 public:
     bool        m_auto_config;

src/muz/dataflow/dataflow.h

@@ -87,6 +87,7 @@ namespace datalog {
             for (func_decl_set::iterator I = output_preds.begin(),
                 E = output_preds.end(); I != E; ++I) {
                 func_decl* sym = *I;
+                TRACE("dl", tout << sym->get_name() << "\n";);
                 const rule_vector& output_rules = m_rules.get_predicate_rules(sym);
                 for (unsigned i = 0; i < output_rules.size(); ++i) {
                     m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value.init_down(m_context, output_rules[i]);

src/muz/pdr/pdr_context.cpp

@@ -50,6 +50,7 @@ Notes:
 #include "blast_term_ite_tactic.h"
 #include "model_implicant.h"
 #include "expr_safe_replace.h"
+#include "ast_util.h"
 
 namespace pdr {
 
@@ -448,6 +449,7 @@ namespace pdr {
         else if (is_sat == l_false) {
             uses_level = m_solver.assumes_level();
         }
+        m_solver.set_model(0);
         return is_sat;
     }
 
@@ -481,6 +483,7 @@ namespace pdr {
         prop_solver::scoped_level _sl(m_solver, level);
         m_solver.set_core(&core);
         m_solver.set_subset_based_core(true);
+        m_solver.set_model(0);
         lbool res = m_solver.check_assumptions_and_formula(lits, fml);
         if (res == l_false) {
             lits.reset();
@@ -738,6 +741,7 @@ namespace pdr {
     // model_node
 
     void model_node::set_closed() {
+        TRACE("pdr", tout << state() << "\n";);
         pt().close(state());
         m_closed = true; 
     }
@@ -774,6 +778,13 @@ namespace pdr {
         }
         // only initial states are not set by the PDR search.
         SASSERT(m_model.get());
+        if (!m_model.get()) {
+            std::stringstream msg;
+            msg << "no model for node " << state();
+            IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);
+            throw default_exception(msg.str());
+        }
+
         datalog::rule const& rl1 = pt().find_rule(*m_model);
         if (is_ini(rl1)) {
             set_rule(&rl1);
@@ -792,15 +803,23 @@ namespace pdr {
             }
         }
         SASSERT(!tags.empty());
-        ini_tags = m.mk_or(tags.size(), tags.c_ptr());
+        ini_tags = ::mk_or(tags);
         ini_state = m.mk_and(ini_tags, pt().initial_state(), state());
         model_ref mdl;
         pt().get_solver().set_model(&mdl);
-        TRACE("pdr", tout << mk_pp(ini_state, m) << "\n";);
+        TRACE("pdr", tout << ini_state << "\n";);
-        VERIFY(l_true == pt().get_solver().check_conjunction_as_assumptions(ini_state));
+        if (l_true != pt().get_solver().check_conjunction_as_assumptions(ini_state)) {
+            std::stringstream msg;
+            msg << "Unsatisfiable initial state: " << ini_state << "\n";
+            display(msg, 2);
+            IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);
+            throw default_exception(msg.str());
+        }
+        SASSERT(mdl.get());
         datalog::rule const& rl2 = pt().find_rule(*mdl);
         SASSERT(is_ini(rl2));
         set_rule(&rl2);
+        pt().get_solver().set_model(0);
         return const_cast<datalog::rule*>(m_rule);                        
     }
 
@@ -829,7 +848,7 @@ namespace pdr {
         }
         r0 = get_rule();
         app_ref_vector& inst = pt().get_inst(r0);
-        TRACE("pdr", tout << mk_pp(state(), m) << " instance: " << inst.size() << "\n";);
+        TRACE("pdr", tout << state() << " instance: " << inst.size() << "\n";);
         for (unsigned i = 0; i < inst.size(); ++i) {
             expr* v;
             if (model.find(inst[i].get(), v)) {
@@ -851,7 +870,7 @@ namespace pdr {
         for (unsigned i = 0; i < indent; ++i) out << " ";
         out << m_level << " " << m_pt.head()->get_name() << " " << (m_closed?"closed":"open") << "\n";
         for (unsigned i = 0; i < indent; ++i) out << " ";
-        out << "  " << mk_pp(m_state, m_state.get_manager(), indent) << "\n";
+        out << "  " << mk_pp(m_state, m_state.get_manager(), indent) << " " << m_state->get_id() << "\n";
         for (unsigned i = 0; i < children().size(); ++i) {
             children()[i]->display(out, indent + 1);
         }
@@ -924,17 +943,6 @@ namespace pdr {
         }
     }
 
-    bool model_search::is_repeated(model_node& n) const {
-        model_node* p = n.parent();
-        while (p) {
-            if (p->state() == n.state()) {
-                TRACE("pdr", tout << "repeated\n";);
-                return true;
-            }
-            p = p->parent();
-        }
-        return false;
-    }
 
     void model_search::add_leaf(model_node& n) {
         SASSERT(n.children().empty());
@@ -1011,13 +1019,18 @@ namespace pdr {
         nodes.erase(&n);
         bool is_goal = n.is_goal();
         remove_goal(n);
-        if (!nodes.empty() && is_goal && backtrack) {
+        // TBD: siblings would also fail if n is not a goal.
+        if (!nodes.empty() && backtrack && nodes[0]->children().empty() && nodes[0]->is_closed()) {
             TRACE("pdr_verbose", for (unsigned i = 0; i < nodes.size(); ++i) n.display(tout << &n << "\n", 2););
             model_node* n1 = nodes[0];
             n1->set_open();            
-            SASSERT(n1->children().empty());
             enqueue_leaf(n1);
         }
+
+        if (!nodes.empty() && n.get_model_ptr() && backtrack) {
+            model_ref mr(n.get_model_ptr());
+            nodes[0]->set_model(mr);
+        }
         if (nodes.empty()) {            
             cache(n).remove(n.state());
         }
@@ -1149,17 +1162,21 @@ namespace pdr {
             ast_manager& m = n->pt().get_manager();
             if (!n->get_model_ptr()) {
                 if (models.find(n->state(), md)) {
-                    TRACE("pdr", tout << mk_pp(n->state(), m) << "\n";);
+                    TRACE("pdr", tout << n->state() << "\n";);
                     model_ref mr(md);
                     n->set_model(mr);
                     datalog::rule const* rule = rules.find(n->state());
                     n->set_rule(rule);
                 }
                 else {
+                    TRACE("pdr", tout << "no model for " << n->state() << "\n";);
                     IF_VERBOSE(1, n->display(verbose_stream() << "no model:\n", 0);
-                               verbose_stream() << mk_pp(n->state(), m) << "\n";);
+                               verbose_stream() << n->state() << "\n";);
                 }
             }
+            else {
+                TRACE("pdr", tout << n->state() << "\n";);
+            }
             todo.pop_back();
             todo.append(n->children().size(), n->children().c_ptr());
         }        
@@ -1692,7 +1709,15 @@ namespace pdr {
 
     void context::validate_search() {
         expr_ref tr = m_search.get_trace(*this);
-        // TBD: tr << "\n";
+        smt::kernel solver(m, get_fparams());
+        solver.assert_expr(tr);
+        lbool res = solver.check();
+        if (res != l_true) {
+            std::stringstream msg;
+            msg << "rule validation failed when checking: " << tr;
+            IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);
+            throw default_exception(msg.str());
+        }                                
     }
 
     void context::validate_model() {
@@ -1928,11 +1953,11 @@ namespace pdr {
         proof_ref proof(m);
         SASSERT(m_last_result == l_true);
         proof = m_search.get_proof_trace(*this);
-        TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
+        TRACE("pdr", tout << "PDR trace: " << proof << "\n";);
         apply(m, m_pc.get(), proof);
-        TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
+        TRACE("pdr", tout << "PDR trace: " << proof << "\n";);
         // proof_utils::push_instantiations_up(proof);
-        // TRACE("pdr", tout << "PDR up: " << mk_pp(proof, m) << "\n";);
+        // TRACE("pdr", tout << "PDR up: " << proof << "\n";);
         return proof;
     }
 
@@ -2027,11 +2052,11 @@ namespace pdr {
             switch (expand_state(n, cube, uses_level)) {
             case l_true:
                 if (n.level() == 0) {
-                    TRACE("pdr", tout << "reachable at level 0\n";);
+                    TRACE("pdr", n.display(tout << "reachable at level 0\n", 0););
                     close_node(n);
                 }
                 else {
-                    TRACE("pdr", tout << "node: " << &n << "\n";); 
+                    TRACE("pdr", n.display(tout, 0);); 
                     create_children(n);
                 }
                 break;

src/muz/pdr/pdr_context.h

@@ -240,7 +240,7 @@ namespace pdr {
         void check_pre_closed();
         void set_closed();     
         void set_open();
-        void set_pre_closed() { m_closed = true; }
+        void set_pre_closed() { TRACE("pdr", tout << state() << "\n";); m_closed = true; }
         void reset() { m_children.reset(); }
 
         void set_rule(datalog::rule const* r) { m_rule = r; }
@@ -268,7 +268,6 @@ namespace pdr {
         void enqueue_leaf(model_node* n); // add leaf to priority queue.
         void update_models();
         void set_leaf(model_node& n); // Set node as leaf, remove children.
-        bool is_repeated(model_node& n) const;
         unsigned num_goals() const; 
 
     public:

src/muz/transforms/dl_mk_coi_filter.cpp

@@ -41,6 +41,9 @@ namespace datalog {
             bool new_tail = false;
             bool contained = true;
             for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) {
+                if (m_context.has_facts(r->get_decl(i))) {
+                    return 0;
+                }
                 if (r->is_neg_tail(i)) {
                     if (!engine.get_fact(r->get_decl(i)).is_reachable()) {
                         if (!new_tail) {

src/opt/maxsmt.cpp

@@ -154,7 +154,7 @@ namespace opt {
         m_soft_constraints(m), m_answer(m) {}
 
     lbool maxsmt::operator()() {
-        lbool is_sat;
+        lbool is_sat = l_undef;
         m_msolver = 0;
         symbol const& maxsat_engine = m_c.maxsat_engine();
         IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
@@ -191,7 +191,7 @@ namespace opt {
             m_msolver->set_adjust_value(m_adjust_value);
             is_sat = (*m_msolver)();
             if (is_sat != l_false) {
-                m_msolver->get_model(m_model);
+                m_msolver->get_model(m_model, m_labels);
             }
         }
 
@@ -247,8 +247,9 @@ namespace opt {
         m_upper = r;
     }    
 
-    void maxsmt::get_model(model_ref& mdl) {
+    void maxsmt::get_model(model_ref& mdl, svector<symbol>& labels) {
         mdl = m_model.get();
+        labels = m_labels;
     }
 
     void maxsmt::commit_assignment() {

src/opt/maxsmt.h

@@ -46,7 +46,7 @@ namespace opt {
         virtual bool get_assignment(unsigned index) const = 0;
         virtual void set_cancel(bool f) = 0;
         virtual void collect_statistics(statistics& st) const = 0;
-        virtual void get_model(model_ref& mdl) = 0;
+        virtual void get_model(model_ref& mdl, svector<symbol>& labels) = 0;
         virtual void updt_params(params_ref& p) = 0;
         void set_adjust_value(adjust_value& adj) { m_adjust_value = adj; }
 
@@ -67,6 +67,7 @@ namespace opt {
         rational         m_lower;
         rational         m_upper;
         model_ref        m_model;
+        svector<symbol>  m_labels;
         svector<bool>    m_assignment;       // truth assignment to soft constraints
         params_ref       m_params;           // config
 
@@ -79,9 +80,9 @@ namespace opt {
         virtual bool get_assignment(unsigned index) const { return m_assignment[index]; }
         virtual void set_cancel(bool f) { m_cancel = f; if (f) s().cancel(); else s().reset_cancel(); }
         virtual void collect_statistics(statistics& st) const { }
-        virtual void get_model(model_ref& mdl) { mdl = m_model.get(); }
+        virtual void get_model(model_ref& mdl, svector<symbol>& labels) { mdl = m_model.get(); labels = m_labels;}
         virtual void commit_assignment();
-        void set_model() { s().get_model(m_model); }
+        void set_model() { s().get_model(m_model); s().get_labels(m_labels); }
         virtual void updt_params(params_ref& p);
         solver& s();
         void init();
@@ -122,6 +123,7 @@ namespace opt {
         rational         m_upper;
         adjust_value     m_adjust_value;
         model_ref        m_model;
+        svector<symbol>  m_labels;
         params_ref       m_params;
     public:
         maxsmt(maxsat_context& c);
@@ -139,7 +141,7 @@ namespace opt {
         rational get_upper() const;        
         void update_lower(rational const& r);
         void update_upper(rational const& r);
-        void get_model(model_ref& mdl);
+        void get_model(model_ref& mdl, svector<symbol>& labels);
         bool get_assignment(unsigned index) const;
         void display_answer(std::ostream& out) const;        
         void collect_statistics(statistics& st) const;

src/opt/opt_context.cpp

@@ -167,6 +167,10 @@ namespace opt {
         m_hard_constraints.reset();
     }
 
+    void context::get_labels(svector<symbol> & r) {
+        r.append(m_labels);
+    }
+
     void context::set_hard_constraints(ptr_vector<expr>& fmls) {
         if (m_scoped_state.set(fmls)) {
             clear_state();
@@ -228,6 +232,7 @@ namespace opt {
         TRACE("opt", tout << "initial search result: " << is_sat << "\n";);
         if (is_sat != l_false) {
             s.get_model(m_model);
+            s.get_labels(m_labels);
         }
         if (is_sat != l_true) {
             return is_sat;
@@ -276,11 +281,6 @@ namespace opt {
         }
     }
 
-    void context::set_model(model_ref& mdl) {
-        m_model = mdl;
-        fix_model(mdl);
-    }
-
     void context::get_model(model_ref& mdl) {
         mdl = m_model;
         fix_model(mdl);
@@ -289,7 +289,7 @@ namespace opt {
     lbool context::execute_min_max(unsigned index, bool committed, bool scoped, bool is_max) {
         if (scoped) get_solver().push();            
         lbool result = m_optsmt.lex(index, is_max);
-        if (result == l_true) m_optsmt.get_model(m_model);
+        if (result == l_true) m_optsmt.get_model(m_model, m_labels);
         if (scoped) get_solver().pop(1);        
         if (result == l_true && committed) m_optsmt.commit_assignment(index);
         return result;
@@ -300,7 +300,7 @@ namespace opt {
         maxsmt& ms = *m_maxsmts.find(id);
         if (scoped) get_solver().push();            
         lbool result = ms();
-        if (result != l_false && (ms.get_model(tmp), tmp.get())) ms.get_model(m_model);
+        if (result != l_false && (ms.get_model(tmp, m_labels), tmp.get())) ms.get_model(m_model, m_labels);
         if (scoped) get_solver().pop(1);
         if (result == l_true && committed) ms.commit_assignment();
         return result;
@@ -453,7 +453,7 @@ namespace opt {
     }
 
     void context::yield() {
-        m_pareto->get_model(m_model);
+        m_pareto->get_model(m_model, m_labels);
         update_bound(true);
         update_bound(false);
     }
@@ -770,7 +770,7 @@ namespace opt {
                   tout << "offset: " << offset << "\n";
                   );
             std::ostringstream out;
-            out << mk_pp(orig_term, m);
+            out << mk_pp(orig_term, m) << ":" << index;
             id = symbol(out.str().c_str());
             return true;
         }
@@ -793,7 +793,7 @@ namespace opt {
             }
             neg = true;
             std::ostringstream out;
-            out << mk_pp(orig_term, m);
+            out << mk_pp(orig_term, m) << ":" << index;
             id = symbol(out.str().c_str());
             return true;
         }
@@ -812,7 +812,7 @@ namespace opt {
             }
             neg = is_max;
             std::ostringstream out;
-            out << mk_pp(orig_term, m);
+            out << mk_pp(orig_term, m) << ":" << index;
             id = symbol(out.str().c_str());
             return true;            
         }
@@ -902,6 +902,21 @@ namespace opt {
                 m_hard_constraints.push_back(fml);
             }
         }
+        // fix types of objectives:
+        for (unsigned i = 0; i < m_objectives.size(); ++i) {
+            objective & obj = m_objectives[i];
+            expr* t = obj.m_term;
+            switch(obj.m_type) {
+            case O_MINIMIZE:
+            case O_MAXIMIZE:
+                if (!m_arith.is_int(t) && !m_arith.is_real(t)) {
+                    obj.m_term = m_arith.mk_numeral(rational(0), true);
+                }
+                break;
+            default:
+                break;
+            }
+        }
     }
 
     void context::purify(app_ref& term) {
@@ -1000,7 +1015,10 @@ namespace opt {
             switch(obj.m_type) {
             case O_MINIMIZE: {
                 app_ref tmp(m);
-                tmp = m_arith.mk_uminus(obj.m_term);
+                tmp = obj.m_term;
+                if (m_arith.is_int(tmp) || m_arith.is_real(tmp)) {
+                    tmp = m_arith.mk_uminus(obj.m_term);
+                }
                 obj.m_index = m_optsmt.add(tmp);
                 break;
             }
@@ -1103,16 +1121,20 @@ namespace opt {
     }
 
     void context::display_assignment(std::ostream& out) {
+        out << "(objectives\n";
         for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) {
             objective const& obj = m_scoped_state.m_objectives[i];
+            out << " (";
             display_objective(out, obj);
             if (get_lower_as_num(i) != get_upper_as_num(i)) {
-                out << " |-> [" << get_lower(i) << ":" << get_upper(i) << "]\n";
+                out << "  (" << get_lower(i) << " " << get_upper(i) << ")";
             }
             else {
-                out << " |-> " << get_lower(i) << "\n";
+                out << " " << get_lower(i);
             }
+            out << ")\n";
         }
+        out << ")\n";
     }
 
     void context::display_objective(std::ostream& out, objective const& obj) const {

src/opt/opt_context.h

@@ -162,6 +162,7 @@ namespace opt {
         bool                         m_pp_neat;
         symbol                       m_maxsat_engine;
         symbol                       m_logic;
+        svector<symbol>              m_labels;
     public:
         context(ast_manager& m);
         virtual ~context();
@@ -180,11 +181,10 @@ namespace opt {
         virtual lbool optimize();
         virtual bool print_model() const;
         virtual void get_model(model_ref& _m);
-        virtual void set_model(model_ref& _m);
         virtual void fix_model(model_ref& _m);
         virtual void collect_statistics(statistics& stats) const;
         virtual proof* get_proof() { return 0; }
-        virtual void get_labels(svector<symbol> & r) {}
+        virtual void get_labels(svector<symbol> & r);
         virtual void get_unsat_core(ptr_vector<expr> & r) {}
         virtual std::string reason_unknown() const;
 

src/opt/opt_pareto.cpp

@@ -38,6 +38,7 @@ namespace opt {
                         return l_undef;
                     }
                     m_solver->get_model(m_model);
+                    m_solver->get_labels(m_labels);
                     IF_VERBOSE(1,
                                model_ref mdl(m_model);
                                cb.fix_model(mdl); 
@@ -96,6 +97,7 @@ namespace opt {
         }
         if (is_sat == l_true) {
             m_solver->get_model(m_model);
+            m_solver->get_labels(m_labels);
             mk_not_dominated_by();
         }
         return is_sat;

src/opt/opt_pareto.h

@@ -31,7 +31,6 @@ namespace opt {
         virtual expr_ref mk_gt(unsigned i, model_ref& model) = 0;
         virtual expr_ref mk_ge(unsigned i, model_ref& model) = 0;
         virtual expr_ref mk_le(unsigned i, model_ref& model) = 0;
-        virtual void set_model(model_ref& m) = 0;
         virtual void fix_model(model_ref& m) = 0;
     };
     class pareto_base {
@@ -42,6 +41,7 @@ namespace opt {
         ref<solver>      m_solver;
         params_ref       m_params;
         model_ref        m_model;
+        svector<symbol>  m_labels;
     public:
         pareto_base(
             ast_manager & m, 
@@ -77,8 +77,9 @@ namespace opt {
         }
         virtual lbool operator()() = 0;
 
-        virtual void get_model(model_ref& mdl) {
+        virtual void get_model(model_ref& mdl, svector<symbol>& labels) {
             mdl = m_model;
+            labels = m_labels;
         }
 
     protected:

src/opt/opt_solver.cpp

@@ -63,6 +63,11 @@ namespace opt {
         m_context.updt_params(_p);
     }
 
+    solver* opt_solver::translate(ast_manager& m, params_ref const& p) {
+        UNREACHABLE();
+        return 0;
+    }
+
     void opt_solver::collect_param_descrs(param_descrs & r) {
         m_context.collect_param_descrs(r);
     }
@@ -277,6 +282,7 @@ namespace opt {
     }
     
     void opt_solver::get_labels(svector<symbol> & r) {
+        r.reset();
         buffer<symbol> tmp;
         m_context.get_relevant_labels(0, tmp);
         r.append(tmp.size(), tmp.c_ptr());

src/opt/opt_solver.h

@@ -86,6 +86,7 @@ namespace opt {
         opt_solver(ast_manager & m, params_ref const & p, filter_model_converter& fm);
         virtual ~opt_solver();
 
+        virtual solver* translate(ast_manager& m, params_ref const& p);
         virtual void updt_params(params_ref & p);
         virtual void collect_param_descrs(param_descrs & r);
         virtual void collect_statistics(statistics & st) const;

src/opt/optsmt.cpp

@@ -51,6 +51,7 @@ namespace opt {
             if (src[i] >= dst[i]) {
                 dst[i] = src[i];
                 m_models.set(i, m_s->get_model(i));
+                m_s->get_labels(m_labels);
                 m_lower_fmls[i] = fmls[i].get();
                 if (dst[i].is_pos() && !dst[i].is_finite()) { // review: likely done already.
                     m_lower_fmls[i] = m.mk_false();
@@ -157,6 +158,7 @@ namespace opt {
                     disj.reset();
                     m_s->maximize_objectives(disj);
                     m_s->get_model(m_model);       
+                    m_s->get_labels(m_labels);            
                     for (unsigned i = 0; i < ors.size(); ++i) {
                         expr_ref tmp(m);
                         m_model->eval(ors[i].get(), tmp);
@@ -203,6 +205,7 @@ namespace opt {
     expr_ref optsmt::update_lower() {
         expr_ref_vector disj(m);
         m_s->get_model(m_model);
+        m_s->get_labels(m_labels);
         m_s->maximize_objectives(disj);
         set_max(m_lower, m_s->get_objective_values(), disj);
         TRACE("opt",
@@ -331,6 +334,7 @@ namespace opt {
             
             m_s->maximize_objective(obj_index, block);
             m_s->get_model(m_model);
+            m_s->get_labels(m_labels);
             inf_eps obj = m_s->saved_objective_value(obj_index);
             if (obj > m_lower[obj_index]) {
                 m_lower[obj_index] = obj;                
@@ -405,8 +409,9 @@ namespace opt {
         return m_upper[i];
     }
 
-    void optsmt::get_model(model_ref& mdl) {
+    void optsmt::get_model(model_ref& mdl, svector<symbol> & labels) {
         mdl = m_model.get();
+        labels = m_labels;
     }
 
     // force lower_bound(i) <= objective_value(i)    

src/opt/optsmt.h

@@ -38,6 +38,7 @@ namespace opt {
         svector<smt::theory_var> m_vars;
         symbol           m_optsmt_engine;
         model_ref        m_model;
+        svector<symbol>  m_labels;
         sref_vector<model> m_models;
     public:
         optsmt(ast_manager& m): 
@@ -60,7 +61,7 @@ namespace opt {
         inf_eps get_lower(unsigned index) const;
         inf_eps get_upper(unsigned index) const;
         bool objective_is_model_valid(unsigned index) const;
-        void    get_model(model_ref& mdl);
+        void    get_model(model_ref& mdl, svector<symbol>& labels);
         model*  get_model(unsigned index) const { return m_models[index]; }
 
         void update_lower(unsigned idx, inf_eps const& r);

src/parsers/util/pattern_validation.cpp

@@ -88,7 +88,7 @@ bool pattern_validator::process(uint_set & found_vars, unsigned num_bindings, un
     if (!f.m_result)
         return false;
     if (!f.m_found_a_var) {
-        warning_msg("pattern does contain any variable.");
+        warning_msg("pattern does not contain any variable.");
         return false;
     }
     return true;

src/sat/sat_solver/inc_sat_solver.cpp

@@ -32,6 +32,7 @@ Notes:
 #include "model_smt2_pp.h"
 #include "filter_model_converter.h"
 #include "bit_blaster_model_converter.h"
+#include "ast_translation.h"
 
 // incremental SAT solver.
 class inc_sat_solver : public solver {
@@ -94,6 +95,24 @@ public:
     
     virtual ~inc_sat_solver() {}
    
+    virtual solver* translate(ast_manager& dst_m, params_ref const& p) {
+        ast_translation tr(m, dst_m);
+        if (m_num_scopes > 0) {
+            throw default_exception("Cannot translate sat solver at non-base level");
+        }
+        inc_sat_solver* result = alloc(inc_sat_solver, dst_m, p);
+        expr_ref fml(dst_m);
+        for (unsigned i = 0; i < m_fmls.size(); ++i) {
+            fml = tr(m_fmls[i].get());
+            result->m_fmls.push_back(fml);
+        }
+        for (unsigned i = 0; i < m_asmsf.size(); ++i) {
+            fml = tr(m_asmsf[i].get());
+            result->m_asmsf.push_back(fml);
+        }
+        return result;
+    }
+
     virtual void set_progress_callback(progress_callback * callback) {}
 
     virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) { 
@@ -231,7 +250,6 @@ public:
         return "no reason given";
     }
     virtual void get_labels(svector<symbol> & r) {
-        UNREACHABLE();
     }
     virtual unsigned get_num_assertions() const {
         return m_fmls.size();

src/smt/mam.cpp

@@ -3646,6 +3646,9 @@ namespace smt {
                 approx_set::iterator it1  = plbls1.begin();
                 approx_set::iterator end1 = plbls1.end();
                 for (; it1 != end1; ++it1) {
+                    if (m_context.get_cancel_flag()) {
+                        break;
+                    }
                     unsigned plbl1 = *it1;
                     SASSERT(plbls1.may_contain(plbl1));
                     approx_set::iterator it2  = plbls2.begin();
@@ -3687,6 +3690,9 @@ namespace smt {
                 approx_set::iterator it1  = plbls.begin();
                 approx_set::iterator end1 = plbls.end();
                 for (; it1 != end1; ++it1) {
+                    if (m_context.get_cancel_flag()) {
+                        break;
+                    }
                     unsigned plbl1 = *it1;
                     SASSERT(plbls.may_contain(plbl1));
                     approx_set::iterator it2  = clbls.begin();
@@ -3706,6 +3712,9 @@ namespace smt {
             svector<qp_pair>::iterator it1  = m_new_patterns.begin();
             svector<qp_pair>::iterator end1 = m_new_patterns.end();
             for (; it1 != end1; ++it1) {
+                if (m_context.get_cancel_flag()) {
+                    break;
+                }
                 quantifier * qa    = it1->first;
                 app *        mp    = it1->second;
                 SASSERT(m_ast_manager.is_pattern(mp));

src/smt/params/smt_params_helper.pyg

@@ -33,7 +33,7 @@ def_module_params(module_name='smt',
                           ('qi.cost', STRING, '(+ weight generation)', 'expression specifying what is the cost of a given quantifier instantiation'),
                           ('qi.max_multi_patterns', UINT, 0, 'specify the number of extra multi patterns'),
                           ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
-                          ('bv.enable_int2bv', BOOL, False, 'enable support for int2bv and bv2int operators'),
+                          ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
                           ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
                           ('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination'),
                           ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation'),

src/smt/params/theory_bv_params.h

@@ -39,7 +39,7 @@ struct theory_bv_params {
         m_bv_lazy_le(false),
         m_bv_cc(false),
         m_bv_blast_max_size(INT_MAX),
-        m_bv_enable_int2bv2int(false) {
+        m_bv_enable_int2bv2int(true) {
         updt_params(p);
     }
     

src/smt/smt_context.cpp

@@ -36,6 +36,7 @@ Revision History:
 #include"smt_model_finder.h"
 #include"model_pp.h"
 #include"ast_smt2_pp.h"
+#include"ast_translation.h"
 
 namespace smt {
 
@@ -98,38 +99,159 @@ namespace smt {
         m_model_generator->set_context(this);
     }
 
+    literal context::translate_literal(
+        literal lit, context& src_ctx, context& dst_ctx,
+        vector<bool_var> b2v, ast_translation& tr) {
+        ast_manager& dst_m = dst_ctx.get_manager();
+        ast_manager& src_m = src_ctx.get_manager();
+        expr_ref dst_f(dst_m);
+
+        SASSERT(lit != false_literal && lit != true_literal);    
+        bool_var v = b2v.get(lit.var(), null_bool_var);           
+        if (v == null_bool_var) {                                  
+            expr* e = src_ctx.m_bool_var2expr.get(lit.var(), 0);  
+            SASSERT(e);                                            
+            dst_f = tr(e);                                         
+            v = dst_ctx.get_bool_var_of_id_option(dst_f->get_id());
+            if (v != null_bool_var) {                              
+            }                                                      
+            else if (src_m.is_not(e) || src_m.is_and(e) || src_m.is_or(e) ||
+                     src_m.is_iff(e) || src_m.is_ite(e)) {         
+                v = dst_ctx.mk_bool_var(dst_f);                    
+            }                                                      
+            else {                                                 
+                dst_ctx.internalize_formula(dst_f, false);         
+                v = dst_ctx.get_bool_var(dst_f);                   
+            }                                                      
+            b2v.setx(lit.var(), v, null_bool_var);                
+        }                                                          
+        return literal(v, lit.sign());                                   
+    }
+
+
+    void context::copy(context& src_ctx, context& dst_ctx) {
+        ast_manager& dst_m = dst_ctx.get_manager();
+        ast_manager& src_m = src_ctx.get_manager();
+        src_ctx.pop_to_base_lvl();
+        
+        if (src_ctx.m_base_lvl > 0) {
+            throw default_exception("Cloning contexts within a user-scope is not allowed");
+        }
+        SASSERT(src_ctx.m_base_lvl == 0);
+        
+        ast_translation tr(src_m, dst_m, false);
+
+        dst_ctx.set_logic(src_ctx.m_setup.get_logic());
+        dst_ctx.copy_plugins(src_ctx, dst_ctx);
+
+        asserted_formulas& src_af = src_ctx.m_asserted_formulas;
+        asserted_formulas& dst_af = dst_ctx.m_asserted_formulas;
+
+        // Copy asserted formulas.        
+        for (unsigned i = 0; i < src_af.get_num_formulas(); ++i) {
+            expr_ref fml(dst_m);
+            proof_ref pr(dst_m);
+            proof* pr_src = src_af.get_formula_proof(i);
+            fml = tr(src_af.get_formula(i));
+            if (pr_src) {
+                pr = tr(pr_src);
+            }
+            dst_af.assert_expr(fml, pr);            
+        }
+
+        if (!src_ctx.m_setup.already_configured()) {
+            return;
+        }
+        dst_ctx.setup_context(dst_ctx.m_fparams.m_auto_config);
+        dst_ctx.internalize_assertions();
+
+        vector<bool_var> b2v;
+
+#define TRANSLATE(_lit) translate_literal(_lit, src_ctx, dst_ctx, b2v, tr)
+
+        for (unsigned i = 0; i < src_ctx.m_assigned_literals.size(); ++i) {
+            literal lit;
+            lit = TRANSLATE(src_ctx.m_assigned_literals[i]);
+            dst_ctx.mk_clause(1, &lit, 0, CLS_AUX, 0);
+        }
+#if 0
+        literal_vector lits;
+        expr_ref_vector cls(src_m);
+        for (unsigned i = 0; i < src_ctx.m_lemmas.size(); ++i) {
+            lits.reset();
+            cls.reset();
+            clause& src_cls = *src_ctx.m_lemmas[i];
+            unsigned sz = src_cls.get_num_literals();
+            for (unsigned j = 0; j < sz; ++j) {
+                literal lit = TRANSLATE(src_cls.get_literal(j));
+                lits.push_back(lit);
+            }
+            dst_ctx.mk_clause(lits.size(), lits.c_ptr(), 0, src_cls.get_kind(), 0);
+        }        
+        vector<watch_list>::const_iterator it  = src_ctx.m_watches.begin();
+        vector<watch_list>::const_iterator end = src_ctx.m_watches.end();
+        literal ls[2];
+        for (unsigned l_idx = 0; it != end; ++it, ++l_idx) {
+            literal l1 = to_literal(l_idx);
+            literal neg_l1 = ~l1;
+            watch_list const & wl = *it;
+            literal const * it2  = wl.begin_literals();
+            literal const * end2 = wl.end_literals();
+            for (; it2 != end2; ++it2) {
+                literal l2 = *it2;
+                if (l1.index() < l2.index()) {
+                    ls[0] = TRANSLATE(neg_l1);
+                    ls[1] = TRANSLATE(l2);
+                    dst_ctx.mk_clause(2, ls, 0, CLS_AUX, 0);
+                }                
+            }
+        }
+#endif
+        
+        TRACE("smt_context", 
+              src_ctx.display(tout);
+              dst_ctx.display(tout););
+    }
+
+
     context::~context() {
         flush();
     }
 
+    void context::copy_plugins(context& src, context& dst) {
+
+        // copy missing simplifier_plugins
+        // remark: some simplifier_plugins are automatically created by the asserted_formulas class.
+        simplifier & src_s = src.get_simplifier();
+        simplifier & dst_s = dst.get_simplifier(); 
+        ptr_vector<simplifier_plugin>::const_iterator it1  = src_s.begin_plugins();
+        ptr_vector<simplifier_plugin>::const_iterator end1 = src_s.end_plugins();
+        for (; it1 != end1; ++it1) {
+            simplifier_plugin * p = *it1;
+            if (dst_s.get_plugin(p->get_family_id()) == 0) {
+                dst.register_plugin(p->mk_fresh());
+            }
+            SASSERT(dst_s.get_plugin(p->get_family_id()) != 0);
+        }
+
+        // copy theory plugins
+        ptr_vector<theory>::iterator it2  = src.m_theory_set.begin();
+        ptr_vector<theory>::iterator end2 = src.m_theory_set.end();
+        for (; it2 != end2; ++it2) {
+            theory * new_th = (*it2)->mk_fresh(&dst);
+            dst.register_plugin(new_th);
+        }
+    }
+
     context * context::mk_fresh(symbol const * l, smt_params * p) {
         context * new_ctx = alloc(context, m_manager, p == 0 ? m_fparams : *p);
         new_ctx->set_logic(l == 0 ? m_setup.get_logic() : *l);
-        // copy missing simplifier_plugins
+        copy_plugins(*this, *new_ctx);        
-        // remark: some simplifier_plugins are automatically created by the asserted_formulas class.
-        simplifier & s     = get_simplifier();
-        simplifier & new_s = new_ctx->get_simplifier(); 
-        ptr_vector<simplifier_plugin>::const_iterator it1  = s.begin_plugins();
-        ptr_vector<simplifier_plugin>::const_iterator end1 = s.end_plugins();
-        for (; it1 != end1; ++it1) {
-            simplifier_plugin * p = *it1;
-            if (new_s.get_plugin(p->get_family_id()) == 0) {
-                new_ctx->register_plugin(p->mk_fresh());
-            }
-            SASSERT(new_s.get_plugin(p->get_family_id()) != 0);
-        }
-
-        // copy theory plugins
-        ptr_vector<theory>::iterator it2  = m_theory_set.begin();
-        ptr_vector<theory>::iterator end2 = m_theory_set.end();
-        for (; it2 != end2; ++it2) {
-            theory * new_th = (*it2)->mk_fresh(new_ctx);
-            new_ctx->register_plugin(new_th);
-        }
-        new_ctx->m_setup.mark_already_configured();
         return new_ctx;
     }
 
+       
+
     void context::init() {
         app * t       = m_manager.mk_true();
         mk_bool_var(t);

src/smt/smt_context.h

@@ -1326,9 +1326,18 @@ namespace smt {
         // -----------------------------------
         void assert_expr_core(expr * e, proof * pr);
 
+        // copy plugins into a fresh context.
+        void copy_plugins(context& src, context& dst);
+
+        static literal translate_literal(
+            literal lit, context& src_ctx, context& dst_ctx,
+            vector<bool_var> b2v, ast_translation& tr);
+
+
     public:
         context(ast_manager & m, smt_params & fp, params_ref const & p = params_ref());
 
+
         virtual ~context();
 
         /**
@@ -1340,6 +1349,12 @@ namespace smt {
         */
         context * mk_fresh(symbol const * l = 0,  smt_params * p = 0);
 
+        static void copy(context& src, context& dst);
+
+        /**
+           \brief Translate context to use new manager m.
+         */
+
         app * mk_eq_atom(expr * lhs, expr * rhs);
 
         bool set_logic(symbol logic) { return m_setup.set_logic(logic); }

src/smt/smt_kernel.cpp

@@ -32,6 +32,10 @@ namespace smt {
             m_params(p) {
         }
 
+        static void copy(imp& src, imp& dst) {
+            context::copy(src.m_kernel, dst.m_kernel);
+        }
+
         smt_params & fparams() {
             return m_kernel.get_fparams();
         }
@@ -193,6 +197,11 @@ namespace smt {
         return m_imp->m();
     }
 
+    void  kernel::copy(kernel& src, kernel& dst) {
+        imp::copy(*src.m_imp, *dst.m_imp);
+    }
+
+
     bool kernel::set_logic(symbol logic) {
         return m_imp->set_logic(logic);
     }

src/smt/smt_kernel.h

@@ -50,6 +50,8 @@ namespace smt {
 
         ~kernel();
 
+        static void copy(kernel& src, kernel& dst);
+
         ast_manager & m() const;
         
         /**

src/smt/smt_setup.cpp

@@ -721,8 +721,8 @@ namespace smt {
         IF_VERBOSE(100, verbose_stream() << "(smt.collecting-features)\n";);
         st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas());
         IF_VERBOSE(1000, st.display_primitive(verbose_stream()););
-        bool fixnum = st.arith_k_sum_is_small();
+        bool fixnum = st.arith_k_sum_is_small() && m_params.m_arith_fixnum;
-        bool int_only = !st.m_has_rational && !st.m_has_real;
+        bool int_only = !st.m_has_rational && !st.m_has_real && m_params.m_arith_int_only;
         switch(m_params.m_arith_mode) {
         case AS_NO_ARITH:
             m_context.register_plugin(alloc(smt::theory_dummy, m_manager.mk_family_id("arith"), "no arithmetic"));

src/smt/smt_solver.cpp

@@ -38,6 +38,12 @@ namespace smt {
                 m_context.set_logic(m_logic);
         }
 
+        virtual solver* translate(ast_manager& m, params_ref const& p) {            
+            solver* result = alloc(solver, m, p, m_logic);
+            smt::kernel::copy(m_context, result->m_context);
+            return result;
+        }
+        
         virtual ~solver() {
         }
 

src/smt/theory_arith.h

@@ -1029,7 +1029,7 @@ namespace smt {
         theory_arith(ast_manager & m, theory_arith_params & params);
         virtual ~theory_arith();
         
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_arith, get_manager(), m_params); }
+        virtual theory * mk_fresh(context * new_ctx);
 
         virtual void setup();
 

src/smt/theory_arith_core.h

@@ -1538,6 +1538,11 @@ namespace smt {
     theory_arith<Ext>::~theory_arith() {
     }
 
+    template<typename Ext>
+    theory* theory_arith<Ext>::mk_fresh(context* new_ctx) { 
+        return alloc(theory_arith<Ext>, new_ctx->get_manager(), m_params); 
+    }
+
     template<typename Ext>
     void theory_arith<Ext>::setup() {
         m_random.set_seed(m_params.m_arith_random_seed);

src/smt/theory_arith_int.h

@@ -210,7 +210,7 @@ namespace smt {
         TRACE("arith_int", tout << mk_bounded_pp(bound, get_manager()) << "\n";);
         context & ctx = get_context();
         ctx.internalize(bound, true);
-        ctx.mark_as_relevant(bound);
+        ctx.mark_as_relevant(bound.get());
     }
 
     

src/smt/theory_array.h

@@ -98,7 +98,7 @@ namespace smt {
         theory_array(ast_manager & m, theory_array_params & params);
         virtual ~theory_array();
 
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_array, get_manager(), m_params); }
+        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_array, new_ctx->get_manager(), m_params); }
 
         virtual char const * get_name() const { return "array"; }
 

src/smt/theory_array_base.cpp

@@ -220,7 +220,7 @@ namespace smt {
             for (unsigned i = 0; i < dimension; ++i) {
                 sort * ext_sk_domain[2] = { s_array, s_array };
                 parameter p(i);
-                func_decl * ext_sk_decl = m.mk_func_decl(get_id(), OP_ARRAY_EXT_SKOLEM, 1, &p, 2, ext_sk_domain);
+                func_decl * ext_sk_decl = m.mk_func_decl(get_id(), OP_ARRAY_EXT, 1, &p, 2, ext_sk_domain);
                 ext_skolems->push_back(ext_sk_decl);
             }
             m_sort2skolem.insert(s_array, ext_skolems);
@@ -310,10 +310,7 @@ namespace smt {
         func_decl_ref_vector * funcs = 0;
         sort *                     s = m.get_sort(e1);
 
-        if (!m_sort2skolem.find(s, funcs)) {
+        VERIFY(m_sort2skolem.find(s, funcs));
-            UNREACHABLE();
-            return;
-        }
 
         unsigned dimension = funcs->size();
 

src/smt/theory_array_base.h

@@ -36,7 +36,7 @@ namespace smt {
         bool is_select(app const* n) const { return n->is_app_of(get_id(), OP_SELECT); }
         bool is_default(app const* n) const { return n->is_app_of(get_id(), OP_ARRAY_DEFAULT); }
         bool is_const(app const* n) const { return n->is_app_of(get_id(), OP_CONST_ARRAY); }
-        bool is_array_ext(app const * n) const { return n->is_app_of(get_id(), OP_ARRAY_EXT_SKOLEM); }
+        bool is_array_ext(app const * n) const { return n->is_app_of(get_id(), OP_ARRAY_EXT); }
         bool is_as_array(app const * n) const { return n->is_app_of(get_id(), OP_AS_ARRAY); }
         bool is_array_sort(sort const* s) const { return s->is_sort_of(get_id(), ARRAY_SORT); }
         bool is_array_sort(app const* n) const { return is_array_sort(get_manager().get_sort(n)); }

src/smt/theory_array_full.cpp

@@ -35,6 +35,10 @@ namespace smt {
         m_var_data_full.reset();
     }
 
+    theory* theory_array_full::mk_fresh(context* new_ctx) { 
+        return alloc(theory_array_full, new_ctx->get_manager(), m_params); 
+    }
+
     void theory_array_full::add_map(theory_var v, enode* s) {
         if (m_params.m_array_cg && !s->is_cgr()) {
             return;
@@ -269,7 +273,7 @@ namespace smt {
         }
         context & ctx = get_context();
 
-        if (is_map(n)) {
+        if (is_map(n) || is_array_ext(n)) {
             for (unsigned i = 0; i < n->get_num_args(); ++i) {
                 enode* arg = ctx.get_enode(n->get_arg(i));
                 if (!is_attached_to_var(arg)) {
@@ -316,6 +320,10 @@ namespace smt {
             found_unsupported_op(n);
             instantiate_default_as_array_axiom(node);
         }
+        else if (is_array_ext(n)) {
+            SASSERT(n->get_num_args() == 2);
+            instantiate_extensionality(ctx.get_enode(n->get_arg(0)), ctx.get_enode(n->get_arg(1)));
+        }
         return true;
     }
 

src/smt/theory_array_full.h

@@ -91,7 +91,7 @@ namespace smt {
         theory_array_full(ast_manager & m, theory_array_params & params);
         virtual ~theory_array_full();
 
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_array_full, get_manager(), m_params); }
+        virtual theory * mk_fresh(context * new_ctx);
 
         virtual void merge_eh(theory_var v1, theory_var v2, theory_var, theory_var);
         virtual void display_var(std::ostream & out, theory_var v) const;

src/smt/theory_bv.cpp

@@ -1313,6 +1313,11 @@ namespace smt {
     theory_bv::~theory_bv() {
     }
 
+    theory* theory_bv::mk_fresh(context* new_ctx) {
+        return alloc(theory_bv, new_ctx->get_manager(), m_params, m_bb.get_params()); 
+    }
+
+    
     void theory_bv::merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {
         TRACE("bv", tout << "merging: #" << get_enode(v1)->get_owner_id() << " #" << get_enode(v2)->get_owner_id() << "\n";);
         TRACE("bv_bit_prop", tout << "merging: #" << get_enode(v1)->get_owner_id() << " #" << get_enode(v2)->get_owner_id() << "\n";);

src/smt/theory_bv.h

@@ -253,7 +253,7 @@ namespace smt {
         theory_bv(ast_manager & m, theory_bv_params const & params, bit_blaster_params const & bb_params);
         virtual ~theory_bv();
         
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_bv, get_manager(), m_params, m_bb.get_params()); }
+        virtual theory * mk_fresh(context * new_ctx);
 
         virtual char const * get_name() const { return "bit-vector"; }
 

src/smt/theory_datatype.cpp

@@ -36,6 +36,11 @@ namespace smt {
         virtual theory_id get_from_theory() const { return null_theory_id; } 
     };
 
+
+    theory* theory_datatype::mk_fresh(context* new_ctx) { 
+        return alloc(theory_datatype, new_ctx->get_manager(), m_params); 
+    }
+
     /**
        \brief Assert the axiom (antecedent => lhs = rhs)
        antecedent may be null_literal

src/smt/theory_datatype.h

@@ -101,7 +101,7 @@ namespace smt {
     public:
         theory_datatype(ast_manager & m, theory_datatype_params & p);
         virtual ~theory_datatype();
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_datatype, get_manager(), m_params); }
+        virtual theory * mk_fresh(context * new_ctx);
         virtual void display(std::ostream & out) const;
         virtual void collect_statistics(::statistics & st) const;        
         virtual void init_model(model_generator & m);

src/smt/theory_dense_diff_logic.h

@@ -282,7 +282,7 @@ namespace smt {
         theory_dense_diff_logic(ast_manager & m, theory_arith_params & p);
         virtual ~theory_dense_diff_logic() { reset_eh(); }
         
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_dense_diff_logic, get_manager(), m_params); }
+        virtual theory * mk_fresh(context * new_ctx);
 
         virtual char const * get_name() const { return "difference-logic"; }
 

src/smt/theory_dense_diff_logic_def.h

@@ -39,6 +39,11 @@ namespace smt {
         m_edges.push_back(edge());
     }
 
+    template<typename Ext>
+    theory* theory_dense_diff_logic<Ext>::mk_fresh(context * new_ctx) { 
+        return alloc(theory_dense_diff_logic<Ext>, new_ctx->get_manager(), m_params); 
+    }
+
     template<typename Ext>
     inline app * theory_dense_diff_logic<Ext>::mk_zero_for(expr * n) {
         return m_autil.mk_numeral(rational(0), get_manager().get_sort(n));

src/smt/theory_diff_logic.h

@@ -243,7 +243,7 @@ namespace smt {
             reset_eh();
         }
 
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_diff_logic, get_manager(), m_params); }
+        virtual theory * mk_fresh(context * new_ctx);
 
         virtual char const * get_name() const { return "difference-logic"; }
 

src/smt/theory_diff_logic_def.h

@@ -1384,5 +1384,11 @@ bool theory_diff_logic<Ext>::internalize_objective(expr * n, rational const& m,
     return true;
 }
 
+template<typename Ext>
+theory* theory_diff_logic<Ext>::mk_fresh(context* new_ctx) {
+    return alloc(theory_diff_logic<Ext>, new_ctx->get_manager(), m_params); 
+}
+
+
 #endif /* THEORY_DIFF_LOGIC_DEF_H_ */
 

src/smt/theory_dl.cpp

@@ -155,7 +155,7 @@ namespace smt {
         }
 
         virtual theory * mk_fresh(context * new_ctx) {
-            return alloc(theory_dl, get_manager());
+            return alloc(theory_dl, new_ctx->get_manager());
         }
 
         virtual void init_model(smt::model_generator & m) {

src/smt/theory_fpa.cpp

@@ -142,7 +142,8 @@ namespace smt {
         m_trail_stack(*this),
         m_fpa_util(m_converter.fu()),
         m_bv_util(m_converter.bu()),
-        m_arith_util(m_converter.au())
+        m_arith_util(m_converter.au()),
+        m_is_initialized(false)
     {
         params_ref p;
         p.set_bool("arith_lhs", true);
@@ -151,10 +152,24 @@ namespace smt {
 
     theory_fpa::~theory_fpa()
     {
-        ast_manager & m = get_manager();
+        if (m_is_initialized) {
-        dec_ref_map_values(m, m_conversions);
+            ast_manager & m = get_manager();
-        dec_ref_map_values(m, m_wraps);
+            dec_ref_map_values(m, m_conversions);
-        dec_ref_map_values(m, m_unwraps);
+            dec_ref_map_values(m, m_wraps);
+            dec_ref_map_values(m, m_unwraps);
+        }
+        else {
+            SASSERT(m_conversions.empty());
+            SASSERT(m_wraps.empty());
+            SASSERT(m_unwraps.empty());
+        }
+
+        m_is_initialized = false;
+    }
+
+    void theory_fpa::init(context * ctx) {
+        smt::theory::init(ctx);
+        m_is_initialized = true;
     }
 
     app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
@@ -716,6 +731,10 @@ namespace smt {
         return;
     }
 
+    theory* theory_fpa::mk_fresh(context* new_ctx) {
+        return alloc(theory_fpa, new_ctx->get_manager());
+    }
+
     void theory_fpa::push_scope_eh() {
         theory::push_scope_eh();
         m_trail_stack.push_scope();
@@ -859,6 +878,16 @@ namespace smt {
                   mk_ismt2_pp(a2, m) << " eq. cls. #" << get_enode(a2)->get_root()->get_owner()->get_id() << std::endl;);
             res = vp;
         }
+        else if (is_app_of(owner, get_family_id(), OP_FPA_INTERNAL_RM)) {
+            SASSERT(to_app(owner)->get_num_args() == 1);
+            app_ref a0(m);
+            a0 = to_app(owner->get_arg(0));
+            fpa_rm_value_proc * vp = alloc(fpa_rm_value_proc, this);
+            vp->add_dependency(ctx.get_enode(a0));
+            TRACE("t_fpa_detail", tout << "Depends on: " <<
+                mk_ismt2_pp(a0, m) << " eq. cls. #" << get_enode(a0)->get_root()->get_owner()->get_id() << std::endl;);
+            res = vp;
+        }
         else if (ctx.e_internalized(wrapped)) {
             if (m_fpa_util.is_rm(owner)) {
                 fpa_rm_value_proc * vp = alloc(fpa_rm_value_proc, this);

src/smt/theory_fpa.h

@@ -148,6 +148,7 @@ namespace smt {
         obj_map<sort, func_decl*> m_wraps;
         obj_map<sort, func_decl*> m_unwraps;
         obj_map<expr, expr*>      m_conversions;
+        bool                      m_is_initialized;
 
         virtual final_check_status final_check_eh();
         virtual bool internalize_atom(app * atom, bool gate_ctx);
@@ -158,7 +159,7 @@ namespace smt {
         virtual void push_scope_eh();
         virtual void pop_scope_eh(unsigned num_scopes);
         virtual void reset_eh();
-        virtual theory* mk_fresh(context*) { return alloc(theory_fpa, get_manager()); }
+        virtual theory* mk_fresh(context* new_ctx);
         virtual char const * get_name() const { return "fpa"; }
 
         virtual model_value_proc * mk_value(enode * n, model_generator & mg);
@@ -169,9 +170,11 @@ namespace smt {
         virtual void finalize_model(model_generator & mg);
 
     public:
-        theory_fpa(ast_manager& m);
+        theory_fpa(ast_manager & m);
         virtual ~theory_fpa();
 
+        virtual void init(context * ctx);
+
         virtual void display(std::ostream & out) const;
 
     protected:

src/smt/theory_seq_empty.h

@@ -29,7 +29,7 @@ namespace smt {
         virtual bool internalize_term(app*) { return internalize_atom(0,false);  }
         virtual void new_eq_eh(theory_var, theory_var) { }
         virtual void new_diseq_eh(theory_var, theory_var) {}
-        virtual theory* mk_fresh(context*) { return alloc(theory_seq_empty, get_manager()); }
+        virtual theory* mk_fresh(context* new_ctx) { return alloc(theory_seq_empty, new_ctx->get_manager()); }
         virtual char const * get_name() const { return "seq-empty"; }
     public:
         theory_seq_empty(ast_manager& m):theory(m.mk_family_id("seq")), m_used(false) {}

src/smt/theory_utvpi.h

@@ -183,7 +183,7 @@ namespace smt {
 
         virtual ~theory_utvpi();
 
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_utvpi, get_manager()); }
+        virtual theory * mk_fresh(context * new_ctx);
 
         virtual char const * get_name() const { return "utvpi-logic"; }
 

src/smt/theory_utvpi_def.h

@@ -942,6 +942,10 @@ namespace smt {
         }
     }
 
+    template<typename Ext>
+    theory* theory_utvpi<Ext>::mk_fresh(context* new_ctx) { 
+        return alloc(theory_utvpi<Ext>, new_ctx->get_manager()); 
+    }
 
 
 };

src/solver/combined_solver.cpp

@@ -127,6 +127,17 @@ public:
         m_use_solver1_results = true;
     }
 
+    solver* translate(ast_manager& m, params_ref const& p) {
+        solver* s1 = m_solver1->translate(m, p);
+        solver* s2 = m_solver2->translate(m, p);
+        combined_solver* r = alloc(combined_solver, s1, s2, p);
+        r->m_solver2_initialized = m_solver2_initialized;
+        r->m_inc_mode = m_inc_mode;
+        r->m_check_sat_executed = m_check_sat_executed;
+        r->m_use_solver1_results = m_use_solver1_results;
+        return r;
+    }
+
     virtual void updt_params(params_ref const & p) {
         m_solver1->updt_params(p);
         m_solver2->updt_params(p);

src/solver/solver.h

@@ -46,6 +46,12 @@ public:
 class solver : public check_sat_result {
 public:
     virtual ~solver() {}
+
+    /**
+    \brief Creates a clone of the solver.
+    */
+    virtual solver* translate(ast_manager& m, params_ref const& p) = 0;
+
     /**
        \brief Update the solver internal settings. 
     */
@@ -135,6 +141,8 @@ public:
     */
     virtual expr * get_assumption(unsigned idx) const = 0;
 
+
+
     /**
        \brief Display the content of this solver.
     */

src/solver/tactic2solver.cpp

@@ -22,6 +22,7 @@ Notes:
 #include"solver_na2as.h"
 #include"tactic.h"
 #include"ast_pp_util.h"
+#include"ast_translation.h"
 
 /**
    \brief Simulates the incremental solver interface using a tactic.
@@ -45,6 +46,8 @@ public:
     tactic2solver(ast_manager & m, tactic * t, params_ref const & p, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic);
     virtual ~tactic2solver();
 
+    virtual solver* translate(ast_manager& m, params_ref const& p);
+
     virtual void updt_params(params_ref const & p);
     virtual void collect_param_descrs(param_descrs & r);
 
@@ -183,6 +186,22 @@ void tactic2solver::set_cancel(bool f) {
     }
 }
 
+solver* tactic2solver::translate(ast_manager& m, params_ref const& p) {
+    tactic* t = m_tactic->translate(m);
+    tactic2solver* r = alloc(tactic2solver, m, t, p, m_produce_proofs, m_produce_models, m_produce_unsat_cores, m_logic);
+    r->m_result = 0;
+    if (!m_scopes.empty()) {
+        throw default_exception("translation of contexts is only supported at base level");
+    }
+    ast_translation tr(m_assertions.get_manager(), m, false);
+    
+    for (unsigned i = 0; i < get_num_assertions(); ++i) {
+        r->m_assertions.push_back(tr(get_assertion(i)));
+    }
+    return r;
+}
+
+
 void tactic2solver::collect_statistics(statistics & st) const {    
     st.copy(m_stats);
     //SASSERT(m_stats.size() > 0);

src/tactic/arith/eq2bv_tactic.cpp

@@ -305,14 +305,16 @@ public:
             m_nonfd.mark(f, true);
             expr* e1, *e2;
             if (m.is_eq(f, e1, e2)) {
-                if (is_fd(e1, e2)) {
+				if (is_fd(e1, e2) || is_fd(e2, e1)) {
-                    continue;
-                }
-                if (is_fd(e2, e1)) {
                     continue;
                 }            
             }
-            m_todo.append(to_app(f)->get_num_args(), to_app(f)->get_args());
+			if (is_app(f)) {
+				m_todo.append(to_app(f)->get_num_args(), to_app(f)->get_args());
+			}
+			else if (is_quantifier(f)) {
+				m_todo.push_back(to_quantifier(f)->get_expr());
+			}
         }
     }
 

src/tactic/bv/bvarray2uf_rewriter.cpp

@@ -0,0 +1,377 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    bvarray2uf_rewriter.cpp
+
+Abstract:
+
+    Rewriter that rewrites bit-vector arrays into bit-vector
+    (uninterpreted) functions.
+
+Author:
+
+    Christoph (cwinter) 2015-11-04
+
+Notes:
+
+--*/
+
+#include"cooperate.h"
+#include"bv_decl_plugin.h"
+#include"array_decl_plugin.h"
+#include"params.h"
+#include"ast_pp.h"
+#include"bvarray2uf_rewriter.h"
+
+// [1] C. M. Wintersteiger, Y. Hamadi, and L. de Moura: Efficiently Solving
+//     Quantified Bit-Vector Formulas, in Formal Methods in System Design,
+//     vol. 42, no. 1, pp. 3-23, Springer, 2013.
+
+bvarray2uf_rewriter_cfg::bvarray2uf_rewriter_cfg(ast_manager & m, params_ref const & p) :
+    m_manager(m),
+    m_out(m),
+    m_bindings(m),
+    m_bv_util(m),
+    m_array_util(m),
+    m_emc(0),
+    m_fmc(0),
+    extra_assertions(m) {
+    updt_params(p);
+    // We need to make sure that the mananger has the BV and array plugins loaded.
+    symbol s_bv("bv");
+    if (!m_manager.has_plugin(s_bv))
+        m_manager.register_plugin(s_bv, alloc(bv_decl_plugin));
+    symbol s_array("array");
+    if (!m_manager.has_plugin(s_array))
+        m_manager.register_plugin(s_array, alloc(array_decl_plugin));
+}
+
+bvarray2uf_rewriter_cfg::~bvarray2uf_rewriter_cfg() {
+    for (obj_map<expr, func_decl*>::iterator it = m_arrays_fs.begin();
+    it != m_arrays_fs.end();
+        it++)
+        m_manager.dec_ref(it->m_value);
+}
+
+void bvarray2uf_rewriter_cfg::reset() {}
+
+sort * bvarray2uf_rewriter_cfg::get_index_sort(expr * e) {
+    return get_index_sort(m_manager.get_sort(e));
+}
+
+sort * bvarray2uf_rewriter_cfg::get_index_sort(sort * s) {
+    SASSERT(s->get_num_parameters() >= 2);
+    unsigned total_width = 0;
+    for (unsigned i = 0; i < s->get_num_parameters() - 1; i++) {
+        parameter const & p = s->get_parameter(i);
+        SASSERT(p.is_ast() && is_sort(to_sort(p.get_ast())));
+        SASSERT(m_bv_util.is_bv_sort(to_sort(p.get_ast())));
+        total_width += m_bv_util.get_bv_size(to_sort(p.get_ast()));
+    }
+    return m_bv_util.mk_sort(total_width);
+}
+
+sort * bvarray2uf_rewriter_cfg::get_value_sort(expr * e) {
+    return get_value_sort(m_manager.get_sort(e));
+}
+
+sort * bvarray2uf_rewriter_cfg::get_value_sort(sort * s) {
+    SASSERT(s->get_num_parameters() >= 2);
+    parameter const & p = s->get_parameter(s->get_num_parameters() - 1);
+    SASSERT(p.is_ast() && is_sort(to_sort(p.get_ast())));
+    return to_sort(p.get_ast());
+}
+
+bool bvarray2uf_rewriter_cfg::is_bv_array(expr * e) {
+    return is_bv_array(m_manager.get_sort(e));
+}
+
+bool bvarray2uf_rewriter_cfg::is_bv_array(sort * s) {
+    if (!m_array_util.is_array(s))
+        return false;
+
+    SASSERT(s->get_num_parameters() >= 2);
+    for (unsigned i = 0; i < s->get_num_parameters(); i++) {
+        parameter const & p = s->get_parameter(i);
+        if (!p.is_ast() || !is_sort(to_sort(p.get_ast())) ||
+            !m_bv_util.is_bv_sort(to_sort(p.get_ast())))
+            return false;
+    }
+
+    return true;
+}
+
+func_decl_ref bvarray2uf_rewriter_cfg::mk_uf_for_array(expr * e) {
+    SASSERT(is_bv_array(e));
+
+    if (m_array_util.is_as_array(e))
+        return func_decl_ref(static_cast<func_decl*>(to_app(e)->get_decl()->get_parameter(0).get_ast()), m_manager);
+    else {
+        app * a = to_app(e);
+        func_decl * bv_f = 0;
+        if (!m_arrays_fs.find(e, bv_f)) {
+            sort * domain = get_index_sort(a);
+            sort * range = get_value_sort(a);
+            bv_f = m_manager.mk_fresh_func_decl("f_t", "", 1, &domain, range);
+            if (is_uninterp_const(e)) {
+                if (m_emc)
+                    m_emc->insert(to_app(e)->get_decl(),
+                                  m_array_util.mk_as_array(m_manager.get_sort(e), bv_f));
+            }
+            else if (m_fmc)
+                m_fmc->insert(bv_f);
+            m_arrays_fs.insert(e, bv_f);
+            m_manager.inc_ref(bv_f);
+        }
+
+        return func_decl_ref(bv_f, m_manager);
+    }
+}
+
+br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
+    br_status res = BR_FAILED;
+
+    if (m_manager.is_eq(f) && is_bv_array(f->get_domain()[0])) {
+        SASSERT(num == 2);
+        // From [1]: Finally, we replace equations of the form t = s,
+        // where t and s are arrays, with \forall x . f_t(x) = f_s(x).
+        func_decl_ref f_t(mk_uf_for_array(args[0]), m_manager);
+        func_decl_ref f_s(mk_uf_for_array(args[1]), m_manager);
+
+        sort * sorts[1] = { get_index_sort(m_manager.get_sort(args[0])) };
+        symbol names[1] = { symbol("x") };
+        var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
+
+        expr_ref body(m_manager);
+        body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), m_manager.mk_app(f_s, x.get()));
+
+        result = m_manager.mk_forall(1, sorts, names, body);
+        res = BR_DONE;
+    }
+    else if (m_manager.is_distinct(f) && is_bv_array(f->get_domain()[0])) {
+        result = m_manager.mk_distinct_expanded(num, args);
+        res = BR_REWRITE1;
+    }
+    else if (f->get_family_id() == null_family_id) {
+        TRACE("bvarray2uf_rw", tout << "UF APP: " << f->get_name() << std::endl; );
+
+        bool has_bv_arrays = false;
+        func_decl_ref f_t(m_manager);
+        for (unsigned i = 0; i < num; i++) {
+            if (is_bv_array(args[i])) {
+                SASSERT(m_array_util.is_as_array(args[i]));
+                has_bv_arrays = true;
+            }
+        }
+
+        expr_ref t(m_manager);
+        t = m_manager.mk_app(f, num, args);
+
+        if (is_bv_array(t)) {
+            // From [1]: For every array term t we create a fresh uninterpreted function f_t.
+            f_t = mk_uf_for_array(t);
+            result = m_array_util.mk_as_array(m_manager.get_sort(t), f_t);
+            res = BR_DONE;
+        }
+        else if (has_bv_arrays) {
+            result = t;
+            res = BR_DONE;
+        }
+        else
+            res = BR_FAILED;
+    }
+    else if (m_array_util.get_family_id() == f->get_family_id()) {
+        TRACE("bvarray2uf_rw", tout << "APP: " << f->get_name() << std::endl; );
+
+        if (m_array_util.is_select(f)) {
+            SASSERT(num == 2);
+            expr * t = args[0];
+            expr * i = args[1];
+            TRACE("bvarray2uf_rw", tout <<
+                "select; array: " << mk_ismt2_pp(t, m()) <<
+                " index: " << mk_ismt2_pp(i, m()) << std::endl;);
+
+            if (!is_bv_array(t))
+                res = BR_FAILED;
+            else {
+                // From [1]: Then, we replace terms of the form select(t, i) with f_t(i).
+                func_decl_ref f_t(mk_uf_for_array(t), m_manager);
+                result = m_manager.mk_app(f_t, i);
+                res = BR_DONE;
+            }
+        }
+        else {
+            if (!is_bv_array(f->get_range()))
+                res = BR_FAILED;
+            else {
+                if (m_array_util.is_const(f)) {
+                    SASSERT(num == 1);
+                    expr_ref t(m_manager.mk_app(f, num, args), m_manager);
+                    expr * v = args[0];
+                    func_decl_ref f_t(mk_uf_for_array(t), m_manager);
+
+                    result = m_array_util.mk_as_array(f->get_range(), f_t);
+                    res = BR_DONE;
+
+                    // Add \forall x . f_t(x) = v
+                    sort * sorts[1] = { get_index_sort(f->get_range()) };
+                    symbol names[1] = { symbol("x") };
+                    var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
+
+                    expr_ref body(m_manager);
+                    body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), v);
+
+                    expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager);
+                    extra_assertions.push_back(frllx);
+                }
+                else if (m_array_util.is_as_array(f)) {
+                    res = BR_FAILED;
+                }
+                else if (m_array_util.is_map(f)) {
+                    SASSERT(f->get_num_parameters() == 1);
+                    SASSERT(f->get_parameter(0).is_ast());
+                    expr_ref t(m_manager.mk_app(f, num, args), m_manager);
+                    func_decl_ref f_t(mk_uf_for_array(t), m_manager);
+                    func_decl_ref map_f(to_func_decl(f->get_parameter(0).get_ast()), m_manager);
+
+                    func_decl_ref_vector ss(m_manager);
+                    for (unsigned i = 0; i < num; i++) {
+                        SASSERT(m_array_util.is_array(args[i]));
+                        func_decl_ref fd(mk_uf_for_array(args[i]), m_manager);
+                        ss.push_back(fd);
+                    }
+
+                    // Add \forall x . f_t(x) = map_f(a[x], b[x], ...)
+                    sort * sorts[1] = { get_index_sort(f->get_range()) };
+                    symbol names[1] = { symbol("x") };
+                    var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
+
+                    expr_ref_vector new_args(m_manager);
+                    for (unsigned i = 0; i < num; i++)
+                        new_args.push_back(m_manager.mk_app(ss[i].get(), x.get()));
+
+                    expr_ref body(m_manager);
+                    body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()),
+                                           m_manager.mk_app(map_f, num, new_args.c_ptr()));
+
+                    expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager);
+                    extra_assertions.push_back(frllx);
+
+                    result = m_array_util.mk_as_array(f->get_range(), f_t);
+                    res = BR_DONE;
+                }
+                else if (m_array_util.is_store(f)) {
+                    SASSERT(num == 3);
+                    expr * s = args[0];
+                    expr * i = args[1];
+                    expr * v = args[2];
+                    TRACE("bvarray2uf_rw", tout <<
+                        "store; array: " << mk_ismt2_pp(s, m()) <<
+                        " index: " << mk_ismt2_pp(i, m()) <<
+                        " value: " << mk_ismt2_pp(v, m()) << std::endl;);
+                    if (!is_bv_array(s))
+                        res = BR_FAILED;
+                    else {
+                        expr_ref t(m_manager.mk_app(f, num, args), m_manager);
+                        // From [1]: For every term t of the form store(s, i, v), we add the universal
+                        // formula \forall x . x = i \vee f_t(x) = f_s(x), and the ground atom f_t(i) = v.
+                        func_decl_ref f_s(mk_uf_for_array(s), m_manager);
+                        func_decl_ref f_t(mk_uf_for_array(t), m_manager);
+
+                        result = m_array_util.mk_as_array(f->get_range(), f_t);
+                        res = BR_DONE;
+
+                        sort * sorts[1] = { get_index_sort(f->get_range()) };
+                        symbol names[1] = { symbol("x") };
+                        var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
+
+                        expr_ref body(m_manager);
+                        body = m_manager.mk_or(m_manager.mk_eq(x, i),
+                                               m_manager.mk_eq(m_manager.mk_app(f_t, x.get()),
+                                                               m_manager.mk_app(f_s, x.get())));
+
+                        expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager);
+                        extra_assertions.push_back(frllx);
+
+                        expr_ref ground_atom(m_manager);
+                        ground_atom = m_manager.mk_eq(m_manager.mk_app(f_t, i), v);
+                        extra_assertions.push_back(ground_atom);
+                        TRACE("bvarray2uf_rw", tout << "ground atom: " << mk_ismt2_pp(ground_atom, m()) << std::endl; );
+                    }
+                }
+                else {
+                    NOT_IMPLEMENTED_YET();
+                    res = BR_FAILED;
+                }
+            }
+        }
+    }
+
+    CTRACE("bvarray2uf_rw", res==BR_DONE, tout << "result: " << mk_ismt2_pp(result, m()) << std::endl; );
+    return res;
+}
+
+bool bvarray2uf_rewriter_cfg::pre_visit(expr * t)
+{
+    TRACE("bvarray2uf_rw_q", tout << "pre_visit: " << mk_ismt2_pp(t, m()) << std::endl;);
+
+    if (is_quantifier(t)) {
+        quantifier * q = to_quantifier(t);
+        TRACE("bvarray2uf_rw_q", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m()) << std::endl;);
+        sort_ref_vector new_bindings(m_manager);
+        for (unsigned i = 0; i < q->get_num_decls(); i++)
+            new_bindings.push_back(q->get_decl_sort(i));
+        SASSERT(new_bindings.size() == q->get_num_decls());
+        m_bindings.append(new_bindings);
+    }
+    return true;
+}
+
+bool bvarray2uf_rewriter_cfg::reduce_quantifier(quantifier * old_q,
+    expr * new_body,
+    expr * const * new_patterns,
+    expr * const * new_no_patterns,
+    expr_ref & result,
+    proof_ref & result_pr) {
+    unsigned curr_sz = m_bindings.size();
+    SASSERT(old_q->get_num_decls() <= curr_sz);
+    unsigned num_decls = old_q->get_num_decls();
+    unsigned old_sz = curr_sz - num_decls;
+    string_buffer<> name_buffer;
+    ptr_buffer<sort> new_decl_sorts;
+    sbuffer<symbol>  new_decl_names;
+    for (unsigned i = 0; i < num_decls; i++) {
+        symbol const & n = old_q->get_decl_name(i);
+        sort * s = old_q->get_decl_sort(i);
+
+        NOT_IMPLEMENTED_YET();
+
+    }
+    result = m().mk_quantifier(old_q->is_forall(), new_decl_sorts.size(), new_decl_sorts.c_ptr(), new_decl_names.c_ptr(),
+        new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(),
+        old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns);
+    result_pr = 0;
+    m_bindings.shrink(old_sz);
+    TRACE("bvarray2uf_rw_q", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " <<
+        mk_ismt2_pp(old_q->get_expr(), m()) << std::endl <<
+        " new body: " << mk_ismt2_pp(new_body, m()) << std::endl;
+    tout << "result = " << mk_ismt2_pp(result, m()) << std::endl;);
+    return true;
+}
+
+bool bvarray2uf_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & result_pr) {
+    if (t->get_idx() >= m_bindings.size())
+        return false;
+
+    expr_ref new_exp(m());
+    sort * s = t->get_sort();
+
+    NOT_IMPLEMENTED_YET();
+
+    result = new_exp;
+    result_pr = 0;
+    TRACE("bvarray2uf_rw_q", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;);
+    return true;
+}

src/tactic/bv/bvarray2uf_rewriter.h

@@ -0,0 +1,87 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    bvarray2uf_rewriter.h
+
+Abstract:
+
+    Rewriter that rewrites bit-vector arrays into bit-vector
+    (uninterpreted) functions.
+
+Author:
+
+    Christoph (cwinter) 2015-11-04
+
+Notes:
+
+--*/
+#ifndef BVARRAY2UF_REWRITER_H_
+#define BVARRAY2UF_REWRITER_H_
+
+#include"rewriter_def.h"
+#include"extension_model_converter.h"
+#include"filter_model_converter.h"
+
+class bvarray2uf_rewriter_cfg : public default_rewriter_cfg {
+    ast_manager       & m_manager;
+    expr_ref_vector     m_out;
+    sort_ref_vector     m_bindings;
+    bv_util             m_bv_util;
+    array_util          m_array_util;
+    extension_model_converter * m_emc;
+    filter_model_converter * m_fmc;
+
+    obj_map<expr, func_decl*> m_arrays_fs;
+
+public:
+    bvarray2uf_rewriter_cfg(ast_manager & m, params_ref const & p);
+    ~bvarray2uf_rewriter_cfg();
+
+    ast_manager & m() const { return m_manager; }
+    void updt_params(params_ref const & p) {}
+
+    void reset();
+
+    bool pre_visit(expr * t);
+
+    br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr);
+
+    bool reduce_quantifier(quantifier * old_q,
+                           expr * new_body,
+                           expr * const * new_patterns,
+                           expr * const * new_no_patterns,
+                           expr_ref & result,
+                           proof_ref & result_pr);
+
+    bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr);
+
+    expr_ref_vector extra_assertions;
+
+    void set_mcs(extension_model_converter * emc, filter_model_converter * fmc) { m_emc = emc; m_fmc = fmc; }
+
+protected:
+    sort * get_index_sort(expr * e);
+    sort * get_index_sort(sort * s);
+    sort * get_value_sort(expr * e);
+    sort * get_value_sort(sort * s);
+    bool is_bv_array(expr * e);
+    bool is_bv_array(sort * e);
+    func_decl_ref mk_uf_for_array(expr * e);
+};
+
+template class rewriter_tpl<bvarray2uf_rewriter_cfg>;
+
+struct bvarray2uf_rewriter : public rewriter_tpl<bvarray2uf_rewriter_cfg> {
+    bvarray2uf_rewriter_cfg m_cfg;
+    bvarray2uf_rewriter(ast_manager & m, params_ref const & p) :
+        rewriter_tpl<bvarray2uf_rewriter_cfg>(m, m.proofs_enabled(), m_cfg),
+        m_cfg(m, p) {
+    }
+
+    void set_mcs(extension_model_converter * emc, filter_model_converter * fmc) { m_cfg.set_mcs(emc, fmc); }
+};
+
+#endif
+

src/tactic/bv/bvarray2uf_tactic.cpp

@@ -0,0 +1,168 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    bvarray2uf_tactic.cpp
+
+Abstract:
+
+    Tactic that rewrites bit-vector arrays into bit-vector
+    (uninterpreted) functions.
+
+Author:
+
+    Christoph (cwinter) 2015-11-04
+
+Notes:
+
+--*/
+#include"tactical.h"
+#include"bv_decl_plugin.h"
+#include"expr_replacer.h"
+#include"extension_model_converter.h"
+#include"filter_model_converter.h"
+#include"ast_smt2_pp.h"
+
+#include"bvarray2uf_tactic.h"
+#include"bvarray2uf_rewriter.h"
+
+class bvarray2uf_tactic : public tactic {
+
+    struct imp {
+        ast_manager &       m_manager;
+        bool                m_produce_models;
+        bool                m_produce_proofs;
+        bool                m_produce_cores;
+        volatile bool       m_cancel;
+        bvarray2uf_rewriter m_rw;
+
+        ast_manager & m() { return m_manager; }
+
+        imp(ast_manager & m, params_ref const & p) :
+            m_manager(m),
+            m_produce_models(false),
+            m_cancel(false),
+            m_produce_proofs(false),
+            m_produce_cores(false),
+            m_rw(m, p) {
+            updt_params(p);
+        }
+
+        void set_cancel(bool f) {
+            m_cancel = f;
+        }
+
+        void checkpoint() {
+            if (m_cancel)
+                throw tactic_exception(TACTIC_CANCELED_MSG);
+        }
+
+        void operator()(goal_ref const & g,
+                        goal_ref_buffer & result,
+                        model_converter_ref & mc,
+                        proof_converter_ref & pc,
+                        expr_dependency_ref & core)
+        {
+            SASSERT(g->is_well_sorted());
+            tactic_report report("bvarray2uf", *g);
+            mc = 0; pc = 0; core = 0; result.reset();
+            fail_if_proof_generation("bvarray2uf", g);
+            fail_if_unsat_core_generation("bvarray2uf", g);
+
+            TRACE("bvarray2uf", tout << "Before: " << std::endl; g->display(tout); );
+            m_produce_models = g->models_enabled();
+
+            if (m_produce_models) {
+                extension_model_converter * emc = alloc(extension_model_converter, m_manager);
+                filter_model_converter * fmc = alloc(filter_model_converter, m_manager);
+                mc = concat(emc, fmc);
+                m_rw.set_mcs(emc, fmc);
+
+            }
+
+
+            m_rw.reset();
+            expr_ref   new_curr(m_manager);
+            proof_ref  new_pr(m_manager);
+            unsigned size = g->size();
+            for (unsigned idx = 0; idx < size; idx++) {
+                if (g->inconsistent())
+                    break;
+                expr * curr = g->form(idx);
+                m_rw(curr, new_curr, new_pr);
+                //if (m_produce_proofs) {
+                //    proof * pr = g->pr(idx);
+                //    new_pr = m.mk_modus_ponens(pr, new_pr);
+                //}
+                g->update(idx, new_curr, new_pr, g->dep(idx));
+            }
+
+            for (unsigned i = 0; i < m_rw.m_cfg.extra_assertions.size(); i++)
+                g->assert_expr(m_rw.m_cfg.extra_assertions[i].get());
+
+            g->inc_depth();
+            result.push_back(g.get());
+            TRACE("bvarray2uf", tout << "After: " << std::endl; g->display(tout););
+            SASSERT(g->is_well_sorted());
+        }
+
+        void updt_params(params_ref const & p) {
+        }
+    };
+
+    imp *      m_imp;
+    params_ref m_params;
+
+public:
+    bvarray2uf_tactic(ast_manager & m, params_ref const & p) :
+        m_params(p) {
+        m_imp = alloc(imp, m, p);
+    }
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(bvarray2uf_tactic, m, m_params);
+    }
+
+    virtual ~bvarray2uf_tactic() {
+        dealloc(m_imp);
+    }
+
+    virtual void updt_params(params_ref const & p) {
+        m_params = p;
+        m_imp->updt_params(p);
+    }
+
+    virtual void collect_param_descrs(param_descrs & r) {
+        insert_produce_models(r);
+    }
+
+    virtual void operator()(goal_ref const & in,
+                            goal_ref_buffer & result,
+                            model_converter_ref & mc,
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        (*m_imp)(in, result, mc, pc, core);
+    }
+
+    virtual void cleanup() {
+        ast_manager & m = m_imp->m();
+        imp * d = alloc(imp, m, m_params);
+    #pragma omp critical (tactic_cancel)
+        {
+            std::swap(d, m_imp);
+        }
+        dealloc(d);
+    }
+
+    virtual void set_cancel(bool f) {
+        if (m_imp)
+            m_imp->set_cancel(f);
+    }
+
+};
+
+
+tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(bvarray2uf_tactic, m, p));
+}

src/tactic/bv/bvarray2uf_tactic.h

@@ -0,0 +1,33 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    bvarray2ufbvarray2uf_tactic.h
+
+Abstract:
+
+    Tactic that rewrites bit-vector arrays into bit-vector
+    (uninterpreted) functions.
+
+Author:
+
+    Christoph (cwinter) 2015-11-04
+
+Notes:
+
+--*/
+#ifndef BV_ARRAY2UF_TACTIC_H_
+#define BV_ARRAY2UF_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p = params_ref());
+/*
+    ADD_TACTIC("bvarray2uf", "Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.", "mk_bvarray2uf_tactic(m, p)")
+*/
+
+
+#endif

src/tactic/bv/elim_small_bv_tactic.cpp

@@ -0,0 +1,332 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    elim_small_bv.h
+
+Abstract:
+
+    Tactic that eliminates small, quantified bit-vectors.
+
+Author:
+
+    Christoph (cwinter) 2015-11-09
+
+Revision History:
+
+--*/
+#include"tactical.h"
+#include"rewriter_def.h"
+#include"filter_model_converter.h"
+#include"cooperate.h"
+#include"bv_decl_plugin.h"
+#include"used_vars.h"
+#include"well_sorted.h"
+#include"var_subst.h"
+#include"simplifier.h"
+#include"basic_simplifier_plugin.h"
+#include"bv_simplifier_plugin.h"
+
+#include"elim_small_bv_tactic.h"
+
+class elim_small_bv_tactic : public tactic {
+
+    struct rw_cfg : public default_rewriter_cfg {
+        ast_manager               & m;
+        bv_util                     m_util;
+        simplifier                  m_simp;
+        ref<filter_model_converter> m_mc;
+        goal *                      m_goal;
+        unsigned                    m_max_bits;
+        unsigned long long          m_max_steps;
+        unsigned long long          m_max_memory; // in bytes
+        bool                        m_produce_models;
+        sort_ref_vector             m_bindings;
+        unsigned long               m_num_eliminated;
+
+        rw_cfg(ast_manager & _m, params_ref const & p) :
+            m(_m),
+            m_util(_m),
+            m_simp(_m),
+            m_bindings(_m),
+            m_num_eliminated(0) {
+            updt_params(p);
+            m_goal = 0;
+            m_max_steps = UINT_MAX;
+
+            basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m);
+            // bsimp->set_eliminate_and(true);
+            m_simp.register_plugin(bsimp);
+
+            bv_simplifier_params bv_params;
+            bv_simplifier_plugin * bvsimp = alloc(bv_simplifier_plugin, m, *bsimp, bv_params);
+            m_simp.register_plugin(bvsimp);
+        }
+
+        bool max_steps_exceeded(unsigned long long num_steps) const {
+            cooperate("elim-small-bv");
+            if (num_steps > m_max_steps)
+                return true;
+            if (memory::get_allocation_size() > m_max_memory)
+                throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
+            return false;
+        }
+
+        bool is_small_bv(sort * s) {
+            return m_util.is_bv_sort(s) && m_util.get_bv_size(s) <= m_max_bits;
+        }
+
+        expr_ref replace_var(used_vars & uv,
+            unsigned num_decls, unsigned max_var_idx_p1,
+            unsigned idx, sort * s, expr * e, expr * replacement) {
+            TRACE("elim_small_bv", tout << "replace idx " << idx << " with " << mk_ismt2_pp(replacement, m) <<
+                " in " << mk_ismt2_pp(e, m) << std::endl;);
+            expr_ref res(m);
+            expr_ref_vector substitution(m);
+
+            substitution.resize(num_decls, 0);
+            substitution[num_decls - idx - 1] = replacement;
+
+            // (VAR 0) is in the first position of substitution; (VAR num_decls-1) is in the last position.
+
+            for (unsigned i = 0; i < max_var_idx_p1; i++) {
+                sort * s = uv.get(i);
+                substitution.push_back(0);
+            }
+
+            // (VAR num_decls) ... (VAR num_decls+sz-1); are in positions num_decls .. num_decls+sz-1
+
+            std::reverse(substitution.c_ptr(), substitution.c_ptr() + substitution.size());
+
+            // (VAR 0) should be in the last position of substitution.
+
+            TRACE("elim_small_bv", tout << "substitution: " << std::endl;
+                                    for (unsigned k = 0; k < substitution.size(); k++) {
+                                        expr * se = substitution[k].get();
+                                        tout << k << " = ";
+                                        if (se == 0) tout << "0";
+                                        else tout << mk_ismt2_pp(se, m);
+                                        tout << std::endl;
+                                    });
+
+            var_subst vsbst(m);
+            vsbst(e, substitution.size(), substitution.c_ptr(), res);
+            SASSERT(is_well_sorted(m, res));
+
+            proof_ref pr(m);
+            m_simp(res, res, pr);
+            TRACE("elim_small_bv", tout << "replace done: " << mk_ismt2_pp(res, m) << std::endl;);
+
+            return res;
+        }
+
+        br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
+            result = m.mk_app(f, num, args);
+            TRACE("elim_small_bv_app", tout << "reduce " << mk_ismt2_pp(result, m) << std::endl; );
+            return BR_FAILED;
+        }
+
+        bool reduce_quantifier(
+            quantifier * q,
+            expr * old_body,
+            expr * const * new_patterns,
+            expr * const * new_no_patterns,
+            expr_ref & result,
+            proof_ref & result_pr) {
+            TRACE("elim_small_bv", tout << "reduce_quantifier " << mk_ismt2_pp(q, m) << std::endl; );
+            unsigned long long num_steps = 0;
+            unsigned curr_sz = m_bindings.size();
+            SASSERT(q->get_num_decls() <= curr_sz);
+            unsigned num_decls = q->get_num_decls();
+            unsigned old_sz = curr_sz - num_decls;
+
+            used_vars uv;
+            uv(q);
+            SASSERT(is_well_sorted(m, q));
+            unsigned max_var_idx_p1 = uv.get_max_found_var_idx_plus_1();
+
+            expr_ref body(old_body, m);
+            for (unsigned i = num_decls-1; i != ((unsigned)-1) && !max_steps_exceeded(num_steps); i--) {
+                sort * s = q->get_decl_sort(i);
+                symbol const & name = q->get_decl_name(i);
+                unsigned bv_sz = m_util.get_bv_size(s);
+
+                if (is_small_bv(s) && !max_steps_exceeded(num_steps)) {
+                    TRACE("elim_small_bv", tout << "eliminating " << name <<
+                        "; sort = " << mk_ismt2_pp(s, m) <<
+                        "; body = " << mk_ismt2_pp(body, m) << std::endl;);
+
+                    expr_ref_vector new_bodies(m);
+                    for (unsigned j = 0; j < bv_sz && !max_steps_exceeded(num_steps); j ++) {
+                        expr_ref n(m_util.mk_numeral(j, bv_sz), m);
+                        expr_ref nb(m);
+                        nb = replace_var(uv, num_decls, max_var_idx_p1, i, s, body, n);
+                        new_bodies.push_back(nb);
+                        num_steps++;
+                    }
+
+                    TRACE("elim_small_bv", tout << "new bodies: " << std::endl;
+                                           for (unsigned k = 0; k < new_bodies.size(); k++)
+                                               tout << mk_ismt2_pp(new_bodies[k].get(), m) << std::endl; );
+
+                    body = q->is_forall() ? m.mk_and(new_bodies.size(), new_bodies.c_ptr()) :
+                                            m.mk_or(new_bodies.size(), new_bodies.c_ptr());
+                    SASSERT(is_well_sorted(m, body));
+
+                    proof_ref pr(m);
+                    m_simp(body, body, pr);
+                    m_num_eliminated++;
+                }
+            }
+
+            quantifier_ref new_q(m);
+            new_q = m.update_quantifier(q, body);
+            unused_vars_eliminator el(m);
+            el(new_q, result);
+
+            TRACE("elim_small_bv", tout << "elimination result: " << mk_ismt2_pp(result, m) << std::endl; );
+
+            result_pr = 0; // proofs NIY
+            m_bindings.shrink(old_sz);
+            return true;
+        }
+
+        bool pre_visit(expr * t) {
+            TRACE("elim_small_bv_pre", tout << "pre_visit: " << mk_ismt2_pp(t, m) << std::endl;);
+            if (is_quantifier(t)) {
+                quantifier * q = to_quantifier(t);
+                TRACE("elim_small_bv", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m) << std::endl;);
+                sort_ref_vector new_bindings(m);
+                for (unsigned i = 0; i < q->get_num_decls(); i++)
+                    new_bindings.push_back(q->get_decl_sort(i));
+                SASSERT(new_bindings.size() == q->get_num_decls());
+                m_bindings.append(new_bindings);
+            }
+            return true;
+        }
+
+        void updt_params(params_ref const & p) {
+            m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
+            m_max_steps = p.get_uint("max_steps", UINT_MAX);
+            m_max_bits = p.get_uint("max_bits", 4);
+        }
+    };
+
+    struct rw : public rewriter_tpl<rw_cfg> {
+        rw_cfg m_cfg;
+
+        rw(ast_manager & m, params_ref const & p) :
+            rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg),
+            m_cfg(m, p) {
+        }
+    };
+
+    struct imp {
+        ast_manager & m;
+        rw            m_rw;
+
+        imp(ast_manager & _m, params_ref const & p) :
+            m(_m),
+            m_rw(m, p) {
+        }
+
+        void set_cancel(bool f) {
+            m_rw.set_cancel(f);
+        }
+
+        void updt_params(params_ref const & p) {
+            m_rw.cfg().updt_params(p);
+        }
+
+        void operator()(goal_ref const & g,
+            goal_ref_buffer & result,
+            model_converter_ref & mc,
+            proof_converter_ref & pc,
+            expr_dependency_ref & core) {
+            SASSERT(g->is_well_sorted());
+            mc = 0; pc = 0; core = 0;
+            tactic_report report("elim-small-bv", *g);
+            bool produce_proofs = g->proofs_enabled();
+            fail_if_proof_generation("elim-small-bv", g);
+            fail_if_unsat_core_generation("elim-small-bv", g);
+            m_rw.cfg().m_produce_models = g->models_enabled();
+
+            m_rw.m_cfg.m_goal = g.get();
+            expr_ref   new_curr(m);
+            proof_ref  new_pr(m);
+            unsigned   size = g->size();
+            for (unsigned idx = 0; idx < size; idx++) {
+                expr * curr = g->form(idx);
+                m_rw(curr, new_curr, new_pr);
+                if (produce_proofs) {
+                    proof * pr = g->pr(idx);
+                    new_pr = m.mk_modus_ponens(pr, new_pr);
+                }
+                g->update(idx, new_curr, new_pr, g->dep(idx));
+            }
+            mc = m_rw.m_cfg.m_mc.get();
+
+            report_tactic_progress(":elim-small-bv-num-eliminated", m_rw.m_cfg.m_num_eliminated);
+            g->inc_depth();
+            result.push_back(g.get());
+            TRACE("elim-small-bv", g->display(tout););
+            SASSERT(g->is_well_sorted());
+        }
+    };
+
+    imp *      m_imp;
+    params_ref m_params;
+public:
+    elim_small_bv_tactic(ast_manager & m, params_ref const & p) :
+        m_params(p) {
+        m_imp = alloc(imp, m, p);
+    }
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(elim_small_bv_tactic, m, m_params);
+    }
+
+    virtual ~elim_small_bv_tactic() {
+        dealloc(m_imp);
+    }
+
+    virtual void updt_params(params_ref const & p) {
+        m_params = p;
+        m_imp->m_rw.cfg().updt_params(p);
+    }
+
+    virtual void collect_param_descrs(param_descrs & r) {
+        insert_max_memory(r);
+        insert_max_steps(r);
+        r.insert("max_bits", CPK_UINT, "(default: 4) maximum bit-vector size of quantified bit-vectors to be eliminated.");
+    }
+
+    virtual void operator()(goal_ref const & in,
+        goal_ref_buffer & result,
+        model_converter_ref & mc,
+        proof_converter_ref & pc,
+        expr_dependency_ref & core) {
+        (*m_imp)(in, result, mc, pc, core);
+    }
+
+    virtual void cleanup() {
+        ast_manager & m = m_imp->m;
+        imp * d = alloc(imp, m, m_params);
+#pragma omp critical (tactic_cancel)
+        {
+            std::swap(d, m_imp);
+        }
+        dealloc(d);
+    }
+
+    virtual void set_cancel(bool f) {
+        if (m_imp)
+            m_imp->set_cancel(f);
+    }
+};
+
+tactic * mk_elim_small_bv_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(elim_small_bv_tactic, m, p));
+}
+

src/tactic/bv/elim_small_bv_tactic.h

@@ -0,0 +1,32 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    elim_small_bv.h
+
+Abstract:
+
+    Tactic that eliminates small, quantified bit-vectors.
+
+Author:
+
+    Christoph (cwinter) 2015-11-09
+
+Revision History:
+
+--*/
+#ifndef ELIM_SMALL_BV_H_
+#define ELIM_SMALL_BV_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_elim_small_bv_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+/*
+    ADD_TACTIC("elim-small-bv", "eliminate small, quantified bit-vectors by expansion.", "mk_elim_small_bv_tactic(m, p)")
+*/
+
+#endif

src/tactic/fpa/fpa2bv_model_converter.cpp

@@ -177,7 +177,6 @@ expr_ref fpa2bv_model_converter::convert_bv2rm(expr * eval_v) const {
     rational bv_val(0);
     unsigned sz = 0;
 
-
     if (bu.is_numeral(eval_v, bv_val, sz)) {
         SASSERT(bv_val.is_uint64());
         switch (bv_val.get_uint64()) {
@@ -309,9 +308,9 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
         expr * bvval = to_app(val)->get_arg(0);
         expr_ref fv(m);
         fv = convert_bv2rm(bv_mdl, var, bvval);
-        TRACE("fpa2bv_mc", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << std::endl;);
+        TRACE("fpa2bv_mc", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << ")" << std::endl;);
         float_mdl->register_decl(var, fv);
-        seen.insert(to_app(val)->get_decl());
+        seen.insert(to_app(bvval)->get_decl());
     }
 
     for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();

src/tactic/smtlogics/qfufbv_tactic.cpp

@@ -25,6 +25,7 @@ Notes:
 #include"max_bv_sharing_tactic.h"
 #include"bv_size_reduction_tactic.h"
 #include"reduce_args_tactic.h"
+#include"qfbv_tactic.h"
 
 tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) {
     params_ref main_p;
@@ -41,13 +42,11 @@ tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) {
                                     );
 
     tactic * st = using_params(and_then(preamble_st,
-                                        mk_smt_tactic()),
+                                        cond(mk_is_qfbv_probe(),
+                                            mk_qfbv_tactic(m),
+                                            mk_smt_tactic())),
                                main_p);
 
-    //cond(is_qfbv(), 
-    // and_then(mk_bit_blaster(m),
-    //          mk_sat_solver(m)),
-    //  mk_smt_solver())
     st->updt_params(p);
     return st;
 }

src/util/util.cpp

@@ -151,24 +151,3 @@ void escaped::display(std::ostream & out) const {
     }
 }
 
-#ifdef _WINDOWS
-#ifdef ARRAYSIZE
-#undef ARRAYSIZE
-#endif
-#include <windows.h>
-#endif
-
-void z3_bound_num_procs() {
-
-#ifdef _Z3_COMMERCIAL
-#define Z3_COMMERCIAL_MAX_CORES 4
-#ifdef _WINDOWS
-    DWORD_PTR numProcs = (1 << Z3_COMMERCIAL_MAX_CORES) - 1;
-    SetProcessAffinityMask(GetCurrentProcess(), numProcs);
-#endif
-#else
-    // Not bounded: Research evaluations are 
-    // not reasonable if run with artificial 
-    // or hidden throttles.
-#endif
-}

src/util/util.h

@@ -400,7 +400,6 @@ inline size_t megabytes_to_bytes(unsigned mb) {
     return r;
 }
 
-void z3_bound_num_procs();
 
 #endif /* UTIL_H_ */