mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Added Solver.AssertAndTrack

Browse source 
Convenience fixes.
Renamed Context.Const to Context.ConstProbe

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-01-17 19:30:00 +00:00
parent 50bf845b40
commit 3abf397560
2 changed files with 47 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/api/dotnet/Context.cs
View file

@ -236,7 +236,7 @@ namespace Microsoft.Z3
/// <summary>
/// Create a new enumeration sort.
/// </summary>
public EnumSort MkEnumSort(Symbol name, Symbol[] enumNames)
public EnumSort MkEnumSort(Symbol name, params Symbol[] enumNames)
{
Contract.Requires(name != null);
Contract.Requires(enumNames != null);
@ -252,7 +252,7 @@ namespace Microsoft.Z3
/// <summary>
/// Create a new enumeration sort.
/// </summary>
public EnumSort MkEnumSort(string name, string[] enumNames)
public EnumSort MkEnumSort(string name, params string[] enumNames)
{
Contract.Requires(enumNames != null);
Contract.Ensures(Contract.Result<EnumSort>() != null);
@ -3219,7 +3219,7 @@ namespace Microsoft.Z3
/// <summary>
/// Create a probe that always evaluates to <paramref name="val"/>.
/// </summary>
public Probe Const(double val)
public Probe ConstProbe(double val)
{
Contract.Ensures(Contract.Result<Probe>() != null);

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

@ -117,6 +117,50 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Assert multiple constraints into the solver, and track them (in the unsat) core
/// using the Boolean constants in ps.
/// </summary>
/// <remarks>
/// This API is an alternative to <see cref="Check"/> 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"/> and the Boolean literals
/// provided using <see cref="Check"/> with assumptions.
/// </remarks>
public void AssertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
{
Contract.Requires(constraints != null);
Contract.Requires(Contract.ForAll(constraints, c => c != null));
Contract.Requires(Contract.ForAll(ps, c => c != null));
Context.CheckContextMatch(constraints);
Context.CheckContextMatch(ps);
if (constraints.Length != ps.Length)
throw new Z3Exception("Argument size mismatch");
for (int i = 0 ; i < constraints.Length; i++)
Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraints[i].NativeObject, ps[i].NativeObject);
}
/// <summary>
/// Assert a constraint into the solver, and track it (in the unsat) core
/// using the Boolean constant p.
/// </summary>
/// <remarks>
/// This API is an alternative to <see cref="Check"/> 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"/> and the Boolean literals
/// provided using <see cref="Check"/> with assumptions.
/// </remarks>
public void AssertAndTrack(BoolExpr constraint, BoolExpr p)
{
Contract.Requires(constraint != null);
Contract.Requires(p != null);
Context.CheckContextMatch(constraint);
Context.CheckContextMatch(p);
Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject);
}
/// <summary>
/// The number of assertions in the solver.
/// </summary>