mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
.NET/Java: API doc update for Context constructor.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
ef2a9994a9
commit
5d1339beec
|
@ -44,6 +44,21 @@ namespace Microsoft.Z3
|
|||
/// <summary>
|
||||
/// Constructor.
|
||||
/// </summary>
|
||||
/// <remarks>
|
||||
/// 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
|
||||
/// Note that in previous versions of Z3, this constructor was also used to set global and module parameters.
|
||||
/// For this purpose we should now use <see cref="Global.SetParameter"/>
|
||||
/// </remarks>
|
||||
public Context(Dictionary<string, string> settings)
|
||||
: base()
|
||||
{
|
||||
|
|
|
@ -27,6 +27,21 @@ public class Context extends IDisposable
|
|||
|
||||
/**
|
||||
* Constructor.
|
||||
* <remarks>
|
||||
* 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
|
||||
* Note that in previous versions of Z3, this constructor was also used to set global and
|
||||
* module parameters. For this purpose we should now use <see cref="Global.setParameter"/>
|
||||
* </remarks>
|
||||
**/
|
||||
public Context(Map<String, String> settings) throws Z3Exception
|
||||
{
|
||||
|
|
Loading…
Reference in a new issue