mk_config method

Z3_config mk_config()

\brief Create a configuration object for the Z3 context object.

Configurations are created in order to assign parameters prior to creating contexts for Z3 interaction. For example, if the users wishes to use proof generation, then call:

\ccode{Z3_set_param_value(cfg, "proof", "true")}

\remark In previous versions of Z3, the \c Z3_config was used to store global and module configurations. Now, we should use \c Z3_global_param_set.

The following parameters can be set:

  • proof (Boolean) Enable proof generation
  • debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting
  • trace (Boolean) Tracing support for VCC
  • trace_file_name (String) Trace out file for VCC traces
  • timeout (unsigned) default timeout (in milliseconds) used for solvers
  • well_sorted_check type checker
  • auto_config use heuristics to automatically select solver and configure it
  • model model generation for solvers, this parameter can be overwritten when creating a solver
  • model_validate validate models produced by solvers
  • unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver
  • encoding the string encoding used internally (must be either "unicode" - 18 bit, "bmp" - 16 bit or "ascii" - 8 bit)

\sa Z3_set_param_value \sa Z3_del_config

def_API('Z3_mk_config', CONFIG, ())

Implementation

Z3_config mk_config() {
  return _mk_config();
}