RetroSearch Browse

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/class_microsoft_1_1_z3_1_1_native_solver.html below:

Z3: NativeSolver Class Reference

void Set (string name, bool value) Sets parameter on the solver More...
void Set (string name, uint value) Sets parameter on the solver More...
void Set (string name, double value) Sets parameter on the solver More...
void Set (string name, string value) Sets parameter on the solver More...
void Push () Creates a backtracking point. More...
void Pop (uint n=1) Backtracks n backtracking points. More...
void Reset () Resets the Solver. More...
void Assert (params Z3_ast[] constraints) Assert a constraint (or multiple) into the solver. More...
void Add (params Z3_ast[] constraints) Alias for Assert. More...
void Add (IEnumerable< Z3_ast > constraints) Alias for Assert. More...
void AssertInjective (Z3_func_decl f) Add constraints to ensure the function f can only be injective. Example: for function f : D1 x D2 -> R assert axioms forall (x1 : D1, x2 : D2) x1 = inv1(f(x1,x2)) forall (x1 : D1, x2 : D2) x2 = inv2(f(x1,x2)) More...
void AssertAndTrack (Z3_ast[] constraints, Z3_ast[] ps) Assert multiple constraints into the solver, and track them (in the unsat) core using the Boolean constants in ps. More...
void AssertAndTrack (Z3_ast constraint, Z3_ast p) Assert a constraint into the solver, and track it (in the unsat) core using the Boolean constant p. More...
void FromFile (string file) Load solver assertions from a file. More...
void FromString (string str) Load solver assertions from a string. More...
Status Check (params Z3_ast[] assumptions) Checks whether the assertions in the solver are consistent or not. More...
Status Check (IEnumerable< Z3_ast > assumptions) Checks whether the assertions in the solver are consistent or not. More...
NativeSolver Translate (NativeContext ctx) Create a clone of the current solver with respect to ctx. More...
void ImportModelConverter (NativeSolver src) Import model converter from other solver. More...
override string ToString () A string representation of the solver. More...
void Dispose () Disposes of the underlying native Z3 object. More...

Solvers.

Definition at line 40 of file NativeSolver.cs.

◆ Add() [1/2] void Add ( IEnumerable< Z3_ast > constraints ) ◆ Add() [2/2] void Add ( params Z3_ast[] constraints ) ◆ Assert() void Assert ( params Z3_ast[] constraints ) inline ◆ AssertAndTrack() [1/2]

Assert a constraint into the solver, and track it (in the unsat) core using the Boolean constant p.

This API is an alternative to Check(Z3_ast[]) 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 AssertAndTrack(Z3_ast[],Z3_ast[]) and the Boolean literals provided using Check(Z3_ast[]) with assumptions.

Definition at line 242 of file NativeSolver.cs.

244

Debug.Assert(constraint !=

null

);

245

Debug.Assert(p !=

null

);

247

Native.Z3_solver_assert_and_track(nCtx, z3solver, constraint, p);

◆ AssertAndTrack() [2/2]

Assert multiple constraints into the solver, and track them (in the unsat) core using the Boolean constants in ps.

Definition at line 219 of file NativeSolver.cs.

221

Debug.Assert(constraints !=

null

);

222

Debug.Assert(constraints.All(c => c != IntPtr.Zero));

223

Debug.Assert(ps.All(c => c != IntPtr.Zero));

224 if

(constraints.Length != ps.Length)

225 throw new

Z3Exception(

"Argument size mismatch"

);

227 for

(

int

i = 0; i < constraints.Length; i++)

228

Native.Z3_solver_assert_and_track(nCtx, z3solver, constraints[i], ps[i]);

◆ AssertInjective()

Add constraints to ensure the function f can only be injective. Example: for function f : D1 x D2 -> R assert axioms forall (x1 : D1, x2 : D2) x1 = inv1(f(x1,x2)) forall (x1 : D1, x2 : D2) x2 = inv2(f(x1,x2))

Parameters

Definition at line 183 of file NativeSolver.cs.

185

uint arity = Native.Z3_get_arity(nCtx, f);

190 for

(uint i = 0; i < arity; ++i)

192 Z3_sort

domain = Native.Z3_get_domain(nCtx, f, i);

193

vars[i] = ntvContext.

MkBound

(arity - i - 1, domain);

195

names[i] = Native.Z3_mk_int_symbol(nCtx, (

int

)i);

197 Z3_ast

app_f = IntPtr.Zero;

198 for

(uint i = 0; i < arity; ++i)

200 Z3_sort

domain = Native.Z3_get_domain(nCtx, f, i);

202 Z3_ast

body = ntvContext.

MkEq

(vars[i], ntvContext.

MkApp

(proj, app_f));

Z3_ast MkApp(Z3_func_decl f, params Z3_ast[] args)

Create a new function application.

Z3_ast MkEq(Z3_ast x, Z3_ast y)

Creates the equality x = y .

Z3_ast MkBound(uint index, Z3_sort sort)

Creates a new bound variable.

Z3_ast MkForall(Z3_sort[] sorts, Z3_symbol[] names, Z3_ast body, uint weight=1, Z3_ast[] patterns=null, Z3_ast[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)

Create a universal Quantifier.

Z3_func_decl MkFreshFuncDecl(string prefix, Z3_sort[] domain, Z3_sort range)

Creates a fresh function declaration with a name prefixed with prefix .

void Assert(params Z3_ast[] constraints)

Assert a constraint (or multiple) into the solver.

System.IntPtr Z3_func_decl

expr range(expr const &lo, expr const &hi)

◆ Check() [1/2]

Checks whether the assertions in the solver are consistent or not.

See also: Model, UnsatCore, Proof

Definition at line 306 of file NativeSolver.cs.

309 Z3_ast

[] asms = assumptions.ToArray();

310 if

(asms.Length == 0)

311

r = (

Z3_lbool

)Native.Z3_solver_check(nCtx, z3solver);

313

r = (

Z3_lbool

)Native.Z3_solver_check_assumptions(nCtx, z3solver, (uint)asms.Length, asms);

314 return

lboolToStatus(r);

Z3_lbool

Lifted Boolean type: false, undefined, true.

◆ Check() [2/2]

Checks whether the assertions in the solver are consistent or not.

See also: Model, UnsatCore, Proof

Definition at line 288 of file NativeSolver.cs.

291 if

(assumptions ==

null

|| assumptions.Length == 0)

292

r = (

Z3_lbool

)Native.Z3_solver_check(nCtx, z3solver);

294

r = (

Z3_lbool

)Native.Z3_solver_check_assumptions(nCtx, z3solver, (uint)assumptions.Length, assumptions);

295 return

lboolToStatus(r);

◆ Dispose()

Disposes of the underlying native Z3 object.

Definition at line 428 of file NativeSolver.cs.

430 if

(z3solver != IntPtr.Zero)

432

Native.Z3_solver_dec_ref(nCtx, z3solver);

433

z3solver = IntPtr.Zero;

435

GC.SuppressFinalize(

this

);

◆ FromFile() void FromFile ( string file )

Load solver assertions from a file.

◆ FromString() void FromString ( string str )

Load solver assertions from a string.

◆ ImportModelConverter()

Import model converter from other solver.

Definition at line 374 of file NativeSolver.cs.

376

Debug.Assert(src !=

null

);

378

Native.Z3_solver_import_model_converter(nCtx, src.z3solver, z3solver);

◆ Pop()

Backtracks n backtracking points.

Note that an exception is thrown if n is not smaller than NumScopes

See also: Push

◆ Push()

Creates a backtracking point.

See also: Pop

◆ Reset()

Resets the Solver.

This removes all assertions from the solver.

◆ Set() [1/4] void Set ( string name, bool value ) inline

Sets parameter on the solver

Definition at line 59 of file NativeSolver.cs.

61

SetParam((

Z3_params

p) => Native.Z3_params_set_bool(nCtx, p, Native.Z3_mk_string_symbol(nCtx, name), (

byte

)(value ? 1 : 0)));

◆ Set() [2/4] void Set ( string name, double value ) inline

Sets parameter on the solver

Definition at line 75 of file NativeSolver.cs.

77

SetParam((

Z3_params

p) => Native.Z3_params_set_double(nCtx, p, Native.Z3_mk_string_symbol(nCtx, name), value));

◆ Set() [3/4] void Set ( string name, string value ) inline

Sets parameter on the solver

Definition at line 83 of file NativeSolver.cs.

85

var value_sym = Native.Z3_mk_string_symbol(nCtx, value);

86

SetParam((

Z3_params

p) => Native.Z3_params_set_symbol(nCtx, p, Native.Z3_mk_string_symbol(nCtx, name), value_sym));

◆ Set() [4/4] void Set ( string name, uint value ) inline

Sets parameter on the solver

Definition at line 67 of file NativeSolver.cs.

69

SetParam((

Z3_params

p) => Native.Z3_params_set_uint(nCtx, p, Native.Z3_mk_string_symbol(nCtx, name), value));

◆ ToString() override string ToString ( ) inline

A string representation of the solver.

Definition at line 396 of file NativeSolver.cs.

398 return

Native.Z3_solver_to_string(nCtx, z3solver);

◆ Translate()

Create a clone of the current solver with respect to ctx.

Definition at line 365 of file NativeSolver.cs.

367

Debug.Assert(ctx !=

null

);

368 return new

NativeSolver(ctx, Native.Z3_solver_translate(nCtx, z3solver, ctx.nCtx));

◆ Assertions ◆ Help

A string that describes all available solver parameters.

Definition at line 45 of file NativeSolver.cs.

◆ Model

The model of the last Check(params Expr[] assumptions).

The result is null if Check(params Expr[] assumptions) was not invoked before, if its results was not SATISFIABLE, or if model production is not enabled.

Definition at line 324 of file NativeSolver.cs.

328

IntPtr x = Native.Z3_solver_get_model(nCtx, z3solver);

329 return

x == IntPtr.Zero

331

new

NativeModel(ntvContext, x);

◆ NumAssertions ◆ NumScopes ◆ Proof

The proof of the last Check(params Expr[] assumptions).

The result is null if Check(params Expr[] assumptions) was not invoked before, if its results was not UNSATISFIABLE, or if proof production is disabled.

Definition at line 342 of file NativeSolver.cs.

◆ ReasonUnknown

A brief justification of why the last call to Check returned UNKNOWN.

Definition at line 359 of file NativeSolver.cs.

◆ Statistics

Solver statistics.

Definition at line 384 of file NativeSolver.cs.

388

var stats = Native.Z3_solver_get_statistics(nCtx, z3solver);

Statistics.Entry[] GetStatistics(Z3_stats stats)

Retrieve statistics as an array of entries

◆ Units ◆ UnsatCore

The unsat core of the last Check.

The unsat core is a subset of Assertions The result is empty if Check was not invoked before, if its results was not UNSATISFIABLE, or if core production is disabled.

Definition at line 353 of file NativeSolver.cs.

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4