From f0a30ded7db8aa1e93cf91840ae2469e51c5deb5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 1 Jan 2018 19:25:09 -0800
Subject: [PATCH] add shorthand for translating models #1407

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_model.cpp   | 12 ++++++++++++
 src/api/c++/z3++.h      |  2 ++
 src/api/python/z3/z3.py | 31 +++++++++++++++++++++++++------
 src/api/z3_api.h        |  7 +++++++
 src/smt/theory_seq.cpp  |  3 ++-
 5 files changed, 48 insertions(+), 7 deletions(-)

diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index bda33f186..d9936ff66 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -212,6 +212,18 @@ extern "C" {
         RETURN_Z3(of_ast_vector(v));
         Z3_CATCH_RETURN(0);
     }
+
+    Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context target) {
+        Z3_TRY;
+        LOG_Z3_model_translate(c, m, target);
+        RESET_ERROR_CODE();
+        Z3_model_ref* dst = alloc(Z3_model_ref, *mk_c(target));
+        ast_translation tr(mk_c(c)->m(), mk_c(target)->m());
+        dst->m_model = to_model_ref(m)->translate(tr);
+        mk_c(target)->save_object(dst);
+        RETURN_Z3(of_model(dst));
+        Z3_CATCH_RETURN(0);
+    }
     
     Z3_bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a) {
         Z3_TRY;
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 8ff2be239..b1e667e9f 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -1809,9 +1809,11 @@ namespace z3 {
             Z3_model_inc_ref(ctx(), m);
         }
     public:
+        struct translate {};
         model(context & c):object(c) { init(Z3_mk_model(c)); }
         model(context & c, Z3_model m):object(c) { init(m); }
         model(model const & s):object(s) { init(s.m_model); }
+        model(model& src, context& dst, translate) : object(dst) { init(Z3_model_translate(src.ctx(), src, dst)); } 
         ~model() { Z3_model_dec_ref(ctx(), m_model); }
         operator Z3_model() const { return m_model; }
         model & operator=(model const & s) {
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 20c521df6..465e9aab8 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -5585,6 +5585,17 @@ class FuncInterp(Z3PPObject):
             raise IndexError
         return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx)
 
+    def translate(self, other_ctx):
+        """Copy model 'self' to context 'other_ctx'.
+        """
+        return ModelRef(Z3_model_translate(self.ctx.ref(), self.model, other_ctx.ref()), other_ctx)
+
+    def __copy__(self):
+        return self.translate(self.ctx)
+
+    def __deepcopy__(self):
+        return self.translate(self.ctx)
+
     def as_list(self):
         """Return the function interpretation as a Python list.
         >>> f = Function('f', IntSort(), IntSort())
@@ -5614,9 +5625,6 @@ class ModelRef(Z3PPObject):
         self.ctx   = ctx
         Z3_model_inc_ref(self.ctx.ref(), self.model)
 
-    def __deepcopy__(self, memo={}):
-        return ModelRef(self.m, self.ctx)
-
     def __del__(self):
         if self.ctx.ref() is not None:
            Z3_model_dec_ref(self.ctx.ref(), self.model)
@@ -5870,6 +5878,20 @@ class ModelRef(Z3PPObject):
             r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx))
         return r
 
+    def translate(self, target):
+        """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
+        """
+        if __debug__:
+            _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
+        model = Z3_model_translate(self.ctx.ref(), self.model, target.ref())
+        return Model(model, target)
+
+    def __copy__(self):
+        return self.translate(self.ctx)
+
+    def __deepcopy__(self):
+        return self.translate(self.ctx)
+
 def is_as_array(n):
     """Return true if n is a Z3 expression of the form (_ as-array f)."""
     return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())
@@ -6072,9 +6094,6 @@ class Solver(Z3PPObject):
             self.solver = solver
         Z3_solver_inc_ref(self.ctx.ref(), self.solver)
 
-    def __deepcopy__(self, memo={}):
-        return Solver(self.solver, self.ctx)
-
     def __del__(self):
         if self.solver is not None and self.ctx.ref() is not None:
             Z3_solver_dec_ref(self.ctx.ref(), self.solver)
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 007bc3ab6..0ba49a5e5 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -4896,6 +4896,13 @@ extern "C" {
     */
     Z3_ast_vector Z3_API Z3_model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s);
 
+    /**
+       \brief translate model from context c to context \c dst.
+
+       def_API('Z3_model_translate', MODEL, (_in(CONTEXT), _in(MODEL), _in(CONTEXT)))
+    */
+    Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst);
+
     /**
        \brief The \ccode{(_ as-array f)} AST node is a construct for assigning interpretations for arrays in Z3.
        It is the array such that forall indices \c i we have that \ccode{(select (_ as-array f) i)} is equal to \ccode{(f i)}.
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 597348589..27ed95155 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3218,9 +3218,10 @@ void theory_seq::add_indexof_axiom(expr* i) {
     literal t_eq_empty = mk_eq_empty(t);
 
     // |t| = 0 => |s| = 0 or indexof(t,s,offset) = -1
-    // ~contains(t,s) => indexof(t,s,offset) = -1
+    // ~contains(t,s) <=> indexof(t,s,offset) = -1
 
     add_axiom(cnt,  i_eq_m1);
+    add_axiom(~cnt,  ~i_eq_m1);
     add_axiom(~t_eq_empty, s_eq_empty, i_eq_m1);
 
     if (!offset || (m_autil.is_numeral(offset, r) && r.is_zero())) {