solver_import_model_converter method

void solver_import_model_converter(
  1. Z3_context ctx,
  2. Z3_solver src,
  3. Z3_solver dst
)

\brief Ad-hoc method for importing model conversion from solver.

This method is used for scenarios where \c src has been used to solve a set of formulas and was interrupted. The \c dst solver may be a strengthening of \c src obtained from cubing (assigning a subset of literals or adding constraints over the assertions available in \c src). If \c dst ends up being satisfiable, the model for \c dst may not correspond to a model of the original formula due to inprocessing in \c src. This method is used to take the side-effect of inprocessing into account when returning a model for \c dst.

def_API('Z3_solver_import_model_converter', VOID, (_in(CONTEXT), _in(SOLVER), _in(SOLVER)))

Implementation

void solver_import_model_converter(
  Z3_context ctx,
  Z3_solver src,
  Z3_solver dst,
) {
  return _solver_import_model_converter(
    ctx,
    src,
    dst,
  );
}