21 using System.Collections.Generic;
39 Contract.Ensures(Contract.Result<
string>() != null);
41 return Native.Z3_solver_get_help(
Context.nCtx, NativeObject);
52 Contract.Requires(value != null);
54 Context.CheckContextMatch(value);
55 Native.Z3_solver_set_params(
Context.nCtx, NativeObject, value.NativeObject);
75 get {
return Native.Z3_solver_get_num_scopes(
Context.nCtx, NativeObject); }
84 Native.Z3_solver_push(
Context.nCtx, NativeObject);
92 public void Pop(uint n = 1)
94 Native.Z3_solver_pop(
Context.nCtx, NativeObject, n);
103 Native.Z3_solver_reset(
Context.nCtx, NativeObject);
111 Contract.Requires(constraints != null);
112 Contract.Requires(Contract.ForAll(constraints, c => c != null));
117 Native.Z3_solver_assert(
Context.nCtx, NativeObject, a.NativeObject);
142 Contract.Requires(constraints != null);
143 Contract.Requires(Contract.ForAll(constraints, c => c != null));
144 Contract.Requires(Contract.ForAll(ps, c => c != null));
147 if (constraints.Length != ps.Length)
150 for (
int i = 0 ; i < constraints.Length; i++)
151 Native.Z3_solver_assert_and_track(
Context.nCtx, NativeObject, constraints[i].NativeObject, ps[i].NativeObject);
167 Contract.Requires(constraint != null);
168 Contract.Requires(p != null);
169 Context.CheckContextMatch(constraint);
172 Native.Z3_solver_assert_and_track(
Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject);
178 public uint NumAssertions
183 return assertions.
Size;
194 Contract.Ensures(Contract.Result<
BoolExpr[]>() != null);
212 if (assumptions == null || assumptions.Length == 0)
215 r = (
Z3_lbool)Native.Z3_solver_check_assumptions(
Context.nCtx, NativeObject, (uint)assumptions.Length,
AST.ArrayToNative(assumptions));
216 return lboolToStatus(r);
239 foreach (var
asm in assumptions) asms.Push(
asm);
240 foreach (var v
in variables) vars.Push(v);
241 Z3_lbool r = (
Z3_lbool)Native.Z3_solver_get_consequences(
Context.nCtx, NativeObject, asms.NativeObject, vars.NativeObject, result.NativeObject);
242 consequences = result.ToBoolExprArray();
243 return lboolToStatus(r);
257 IntPtr x = Native.Z3_solver_get_model(
Context.nCtx, NativeObject);
258 if (x == IntPtr.Zero)
276 IntPtr x = Native.Z3_solver_get_proof(
Context.nCtx, NativeObject);
277 if (x == IntPtr.Zero)
296 Contract.Ensures(Contract.Result<
Expr[]>() != null);
306 public string ReasonUnknown
310 Contract.Ensures(Contract.Result<
string>() != null);
312 return Native.Z3_solver_get_reason_unknown(
Context.nCtx, NativeObject);
321 Contract.Requires(ctx != null);
322 Contract.Ensures(Contract.Result<
Solver>() != null);
323 return new Solver(ctx, Native.Z3_solver_translate(
Context.nCtx, NativeObject, ctx.nCtx));
334 Contract.Ensures(Contract.Result<
Statistics>() != null);
345 return Native.Z3_solver_to_string(
Context.nCtx, NativeObject);
352 Contract.Requires(ctx != null);
357 public DecRefQueue() : base() { }
358 public DecRefQueue(uint move_limit) : base(move_limit) { }
359 internal override void IncRef(
Context ctx, IntPtr obj)
361 Native.Z3_solver_inc_ref(ctx.nCtx, obj);
364 internal override void DecRef(
Context ctx, IntPtr obj)
366 Native.Z3_solver_dec_ref(ctx.nCtx, obj);
370 internal override void IncRef(IntPtr o)
376 internal override void DecRef(IntPtr o)
388 default:
return Status.UNKNOWN;
void AssertAndTrack(BoolExpr constraint, BoolExpr p)
Assert a constraint into the solver, and track it (in the unsat) core using the Boolean constant p...
void AssertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
Assert multiple constraints into the solver, and track them (in the unsat) core using the Boolean con...
Status Consequences(IEnumerable< BoolExpr > assumptions, IEnumerable< Expr > variables, out BoolExpr[] consequences)
Retrieve fixed assignments to the set of variables in the form of consequences. Each consequence is a...
Status Check(params Expr[] assumptions)
Checks whether the assertions in the solver are consistent or not.
void Add(params BoolExpr[] constraints)
Alias for Assert.
Objects of this class track statistical information about solvers.
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the solver.
IDecRefQueue Solver_DRQ
Solver DRQ
uint Size
The size of the vector
Z3_lbool
Lifted Boolean type: false, undefined, true.
void Push()
Creates a backtracking point.
override string ToString()
A string representation of the solver.
void Reset()
Resets the Solver.
Solver Translate(Context ctx)
Create a clone of the current solver with respect to ctx.
BoolExpr [] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
A Params objects represents a configuration in the form of Symbol/value pairs.
A ParamDescrs describes a set of parameters.
A Model contains interpretations (assignments) of constants and functions.
The main interaction with Z3 happens via the Context.
The exception base class for error reporting from Z3
The abstract syntax tree (AST) class.
Internal base class for interfacing with native Z3 objects. Should not be used externally.
void Pop(uint n=1)
Backtracks n backtracking points.