mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

add useful shorthands to Solver interface

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-13 00:00:06 -08:00
parent 0f4afc4536
commit 38e4fb307c
2 changed files with 89 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/api/dotnet/Params.cs
View file

@ -31,98 +31,108 @@ namespace Microsoft.Z3
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(Symbol name, bool value)
public Params Add(Symbol name, bool value)
{
Contract.Requires(name != null);
Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (value) ? 1 : 0);
return this;
}
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(Symbol name, uint value)
public Params Add(Symbol name, uint value)
{
Contract.Requires(name != null);
Native.Z3_params_set_uint(Context.nCtx, NativeObject, name.NativeObject, value);
return this;
}
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(Symbol name, double value)
public Params Add(Symbol name, double value)
{
Contract.Requires(name != null);
Native.Z3_params_set_double(Context.nCtx, NativeObject, name.NativeObject, value);
return this;
}
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(Symbol name, string value)
public Params Add(Symbol name, string value)
{
Contract.Requires(value != null);
Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, Context.MkSymbol(value).NativeObject);
return this;
}
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(Symbol name, Symbol value)
public Params Add(Symbol name, Symbol value)
{
Contract.Requires(name != null);
Contract.Requires(value != null);
Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, value.NativeObject);
return this;
}
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(string name, bool value)
public Params Add(string name, bool value)
{
Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value) ? 1 : 0);
return this;
}
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(string name, uint value)
public Params Add(string name, uint value)
{
Native.Z3_params_set_uint(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value);
return this;
}
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(string name, double value)
public Params Add(string name, double value)
{
Native.Z3_params_set_double(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value);
return this;
}
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(string name, Symbol value)
public Params Add(string name, Symbol value)
{
Contract.Requires(value != null);
Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value.NativeObject);
return this;
}
/// <summary>
/// Adds a parameter setting.
/// </summary>
public void Add(string name, string value)
public Params Add(string name, string value)
{
Contract.Requires(name != null);
Contract.Requires(value != null);
Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, Context.MkSymbol(value).NativeObject);
return this;
}
/// <summary>

77
src/api/dotnet/Solver.cs
View file

@ -57,6 +57,48 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(string name, bool value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(string name, uint value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(string name, double value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(string name, string value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(string name, Symbol value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(Symbol name, bool value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(Symbol name, uint value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(Symbol name, double value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(Symbol name, string value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary>
/// Sets parameter on the solver
/// </summary>
public void Set(Symbol name, Symbol value) { Parameters = Context.MkParams().Add(name, value); }
/// <summary>
/// Retrieves parameter descriptions for solver.
/// </summary>
@ -140,11 +182,11 @@ namespace Microsoft.Z3
/// using the Boolean constants in ps.
/// </summary>
/// <remarks>
/// This API is an alternative to <see cref="Check"/> with assumptions for extracting unsat cores.
/// This API is an alternative to <see cref="Check(Expr[])"/> with assumptions for extracting unsat cores.
/// Both APIs can be used in the same solver. The unsat core will contain a combination
/// of the Boolean variables provided using <see cref="AssertAndTrack(BoolExpr[],BoolExpr[])"/>
/// and the Boolean literals
/// provided using <see cref="Check"/> with assumptions.
/// provided using <see cref="Check(Expr[])"/> with assumptions.
/// </remarks>
public void AssertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
{
@ -165,11 +207,11 @@ namespace Microsoft.Z3
/// using the Boolean constant p.
/// </summary>
/// <remarks>
/// This API is an alternative to <see cref="Check"/> with assumptions for extracting unsat cores.
/// This API is an alternative to <see cref="Check(Expr[])"/> with assumptions for extracting unsat cores.
/// Both APIs can be used in the same solver. The unsat core will contain a combination
/// of the Boolean variables provided using <see cref="AssertAndTrack(BoolExpr[],BoolExpr[])"/>
/// and the Boolean literals
/// provided using <see cref="Check"/> with assumptions.
/// provided using <see cref="Check(Expr[])"/> with assumptions.
/// </remarks>
public void AssertAndTrack(BoolExpr constraint, BoolExpr p)
{
@ -256,6 +298,25 @@ namespace Microsoft.Z3
return lboolToStatus(r);
}
/// <summary>
/// Checks whether the assertions in the solver are consistent or not.
/// </summary>
/// <remarks>
/// <seealso cref="Model"/>
/// <seealso cref="UnsatCore"/>
/// <seealso cref="Proof"/>
/// </remarks>
public Status Check(IEnumerable<BoolExpr> assumptions)
{
Z3_lbool r;
BoolExpr[] asms = assumptions.ToArray();
if (asms.Length == 0)
r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject);
else
r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)asms.Length, AST.ArrayToNative(asms));
return lboolToStatus(r);
}
/// <summary>
/// Retrieve fixed assignments to the set of variables in the form of consequences.
/// Each consequence is an implication of the form
@ -284,10 +345,10 @@ namespace Microsoft.Z3
}
/// <summary>
/// The model of the last <c>Check</c>.
/// The model of the last <c>Check(params Expr[] assumptions)</c>.
/// </summary>
/// <remarks>
/// The result is <c>null</c> if <c>Check</c> was not invoked before,
/// The result is <c>null</c> if <c>Check(params Expr[] assumptions)</c> was not invoked before,
/// if its results was not <c>SATISFIABLE</c>, or if model production is not enabled.
/// </remarks>
public Model Model
@ -303,10 +364,10 @@ namespace Microsoft.Z3
}
/// <summary>
/// The proof of the last <c>Check</c>.
/// The proof of the last <c>Check(params Expr[] assumptions)</c>.
/// </summary>
/// <remarks>
/// The result is <c>null</c> if <c>Check</c> was not invoked before,
/// The result is <c>null</c> if <c>Check(params Expr[] assumptions)</c> was not invoked before,
/// if its results was not <c>UNSATISFIABLE</c>, or if proof production is disabled.
/// </remarks>
public Expr Proof