mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
Added new params.Add functions to the .NET and Java APIs.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
e8b04790cf
commit
0e4e72b1bc
|
@ -58,6 +58,16 @@ namespace Microsoft.Z3
|
|||
Native.Z3_params_set_double(Context.nCtx, NativeObject, name.NativeObject, value);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Adds a parameter setting.
|
||||
/// </summary>
|
||||
public void Add(Symbol name, string value)
|
||||
{
|
||||
Contract.Requires(value != null);
|
||||
|
||||
Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, Context.MkSymbol(value).NativeObject);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Adds a parameter setting.
|
||||
/// </summary>
|
||||
|
@ -103,6 +113,16 @@ namespace Microsoft.Z3
|
|||
Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value.NativeObject);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Adds a parameter setting.
|
||||
/// </summary>
|
||||
public void Add(string name, string value)
|
||||
{
|
||||
Contract.Requires(value != null);
|
||||
|
||||
Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, Context.MkSymbol(value).NativeObject);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// A string representation of the parameter set.
|
||||
/// </summary>
|
||||
|
|
|
@ -28,6 +28,17 @@ public class Params extends Z3Object
|
|||
Native.paramsSetDouble(getContext().nCtx(), getNativeObject(),
|
||||
name.getNativeObject(), value);
|
||||
}
|
||||
|
||||
/**
|
||||
* Adds a parameter setting.
|
||||
**/
|
||||
public void add(Symbol name, String value) throws Z3Exception
|
||||
{
|
||||
|
||||
Native.paramsSetSymbol(getContext().nCtx(), getNativeObject(),
|
||||
name.getNativeObject(),
|
||||
getContext().mkSymbol(value).getNativeObject());
|
||||
}
|
||||
|
||||
/**
|
||||
* Adds a parameter setting.
|
||||
|
@ -75,6 +86,17 @@ public class Params extends Z3Object
|
|||
.mkSymbol(name).getNativeObject(), value.getNativeObject());
|
||||
}
|
||||
|
||||
/**
|
||||
* Adds a parameter setting.
|
||||
**/
|
||||
public void add(String name, String value) throws Z3Exception
|
||||
{
|
||||
|
||||
Native.paramsSetSymbol(getContext().nCtx(), getNativeObject(),
|
||||
getContext().mkSymbol(name).getNativeObject(),
|
||||
getContext().mkSymbol(value).getNativeObject());
|
||||
}
|
||||
|
||||
/**
|
||||
* A string representation of the parameter set.
|
||||
**/
|
||||
|
|
Loading…
Reference in a new issue