21 using System.Diagnostics.Contracts;
28 [ContractVerification(
true)]
38 Contract.Ensures(Contract.Result<
string>() != null);
51 Contract.Requires(value != null);
53 Context.CheckContextMatch(value);
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
182 return assertions.
Size;
193 Contract.Ensures(Contract.Result<
BoolExpr[]>() != null);
211 if (assumptions == null || assumptions.Length == 0)
219 default:
return Status.UNKNOWN;
235 if (x == IntPtr.Zero)
254 if (x == IntPtr.Zero)
273 Contract.Ensures(Contract.Result<
Expr[]>() != null);
283 public string ReasonUnknown
287 Contract.Ensures(Contract.Result<
string>() != null);
300 Contract.Ensures(Contract.Result<
Statistics>() != null);
318 Contract.Requires(ctx != null);
323 public DecRefQueue() : base() { }
324 public DecRefQueue(uint move_limit) : base(move_limit) { }
325 internal override void IncRef(
Context ctx, IntPtr obj)
330 internal override void DecRef(
Context ctx, IntPtr obj)
336 internal override void IncRef(IntPtr o)
342 internal override void DecRef(IntPtr 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)
static void Z3_solver_inc_ref(Z3_context a0, Z3_solver a1)
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.
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)
BoolExpr[] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
static Z3_model Z3_solver_get_model(Z3_context a0, Z3_solver a1)
A Params objects represents a configuration in the form of Symbol/value pairs.
static void Z3_solver_dec_ref(Z3_context a0, Z3_solver a1)
A ParamDescrs describes a set of parameters.
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)