3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

add shorthand for translating models #1407

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-01-01 19:25:09 -08:00
parent 8dadd30db5
commit f0a30ded7d
5 changed files with 48 additions and 7 deletions

View file

@ -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;

View file

@ -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) {

View file

@ -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)

View file

@ -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)}.

View file

@ -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())) {