Lines Matching defs:Model

211   Z3_model Model;
214   Z3Model(Z3Context &C, Z3_model ZM) : Context(C), Model(ZM) {
215     Z3_model_inc_ref(Context.Context, Model);
224     if (Model)
225       Z3_model_dec_ref(Context.Context, Model);
229     OS << Z3_model_to_string(Context.Context, Model);
858     Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
861     if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)
866                Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
872     Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
875     if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)
880                Z3_model_get_const_interp(Context.Context, Model.Model, Func)));