21 using System.Diagnostics.Contracts;
28 [ContractVerification(
true)]
38 Contract.Ensures(Contract.Result<
string>() != null);
51 Contract.Requires(value != null);
53 Context.CheckContextMatch(value);
61 public ParamDescrs ParameterDescriptions
91 public void Pop(uint n = 1)
110 Contract.Requires(constraints != null);
111 Contract.Requires(Contract.ForAll(constraints, c => c != null));
113 Context.CheckContextMatch(constraints);
141 Contract.Requires(constraints != null);
142 Contract.Requires(Contract.ForAll(constraints, c => c != null));
143 Contract.Requires(Contract.ForAll(ps, c => c != null));
144 Context.CheckContextMatch(constraints);
146 if (constraints.Length != ps.Length)
149 for (
int i = 0 ; i < constraints.Length; i++)
166 Contract.Requires(constraint != null);
167 Contract.Requires(p != null);
168 Context.CheckContextMatch(constraint);
177 public uint NumAssertions
193 Contract.Ensures(Contract.Result<
BoolExpr[]>() != null);
198 for (uint i = 0; i < n; i++)
215 if (assumptions == null || assumptions.Length == 0)
223 default:
return Status.UNKNOWN;
239 if (x == IntPtr.Zero)
258 if (x == IntPtr.Zero)
273 public Expr[] UnsatCore
277 Contract.Ensures(Contract.Result<
Expr[]>() != null);
282 for (uint i = 0; i < n; i++)
283 res[i] =
Expr.Create(
Context, core[i].NativeObject);
291 public string ReasonUnknown
295 Contract.Ensures(Contract.Result<
string>() != null);
308 Contract.Ensures(Contract.Result<
Statistics>() != null);
326 Contract.Requires(ctx != null);
331 public override void IncRef(Context ctx, IntPtr obj)
333 Native.Z3_solver_inc_ref(ctx.nCtx, obj);
336 public override void DecRef(Context ctx, IntPtr obj)
338 Native.Z3_solver_dec_ref(ctx.nCtx, obj);
342 internal override void IncRef(IntPtr o)
344 Context.Solver_DRQ.IncAndClear(Context, o);
348 internal override void DecRef(IntPtr o)
350 Context.Solver_DRQ.Add(o);
static int Z3_solver_check_assumptions(Z3_context a0, Z3_solver a1, uint a2, [In] Z3_ast[] a3)
static void Z3_solver_pop(Z3_context a0, Z3_solver a1, uint a2)
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...
static Z3_ast_vector Z3_solver_get_assertions(Z3_context a0, Z3_solver a1)
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.
static Z3_stats Z3_solver_get_statistics(Z3_context a0, Z3_solver a1)
static string Z3_solver_to_string(Z3_context a0, Z3_solver a1)
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the solver.
static void Z3_solver_reset(Z3_context a0, Z3_solver a1)
static Z3_param_descrs Z3_solver_get_param_descrs(Z3_context a0, Z3_solver a1)
Z3_lbool
Lifted Boolean type: false, undefined, true.
void Push()
Creates a backtracking point.
static void Z3_solver_assert_and_track(Z3_context a0, Z3_solver a1, Z3_ast a2, Z3_ast a3)
override string ToString()
A string representation of the solver.
void Reset()
Resets the Solver.
static int Z3_solver_check(Z3_context a0, Z3_solver a1)
static Z3_model Z3_solver_get_model(Z3_context a0, Z3_solver a1)
A ParameterSet represents a configuration in the form of Symbol/value pairs.
static string Z3_solver_get_reason_unknown(Z3_context a0, Z3_solver a1)
A Model contains interpretations (assignments) of constants and functions.
static Z3_ast Z3_solver_get_proof(Z3_context a0, Z3_solver a1)
static void Z3_solver_set_params(Z3_context a0, Z3_solver a1, Z3_params a2)
The main interaction with Z3 happens via the Context.
The exception base class for error reporting from Z3
The abstract syntax tree (AST) class.
static string Z3_solver_get_help(Z3_context a0, Z3_solver a1)
static void Z3_solver_push(Z3_context a0, Z3_solver a1)
Internal base class for interfacing with native Z3 objects. Should not be used externally.
static void Z3_solver_assert(Z3_context a0, Z3_solver a1, Z3_ast a2)
void Pop(uint n=1)
Backtracks n backtracking points.
static Z3_ast_vector Z3_solver_get_unsat_core(Z3_context a0, Z3_solver a1)
static uint Z3_solver_get_num_scopes(Z3_context a0, Z3_solver a1)