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_context.html below:

Z3: NativeContext Class Reference

The main interaction with Z3 happens via the Context. NativeContext allows for efficient wrapper-reduced interaction with Z3 expressions. More...

NativeContext (Dictionary< string, string > settings) Constructor. More...
Z3_ast MkAdd (params Z3_ast[] t) Create an expression representing t[0] + t[1] + .... More...
Z3_ast MkMul (params Z3_ast[] t) Create an expression representing t[0] * t[1] * .... More...
Z3_ast MkSub (params Z3_ast[] t) Create an expression representing t[0] - t[1] - .... More...
Z3_ast MkDiv (Z3_ast t1, Z3_ast t2) Create an expression representing t1 / t2. More...
Z3_ast MkLe (Z3_ast t1, Z3_ast t2) Create an expression representing t1 <= t2 More...
Z3_ast MkLt (Z3_ast t1, Z3_ast t2) Create an expression representing t1 < t2 More...
Z3_ast MkGe (Z3_ast t1, Z3_ast t2) Create an expression representing t1 >= t2 More...
Z3_ast MkGt (Z3_ast t1, Z3_ast t2) Create an expression representing t1 > t2 More...
Z3_ast MkBvUlt (Z3_ast t1, Z3_ast t2) Unsigned less-than More...
Z3_ast MkBvUle (Z3_ast t1, Z3_ast t2) Unsigned less-than-equal More...
Z3_ast MkEq (Z3_ast x, Z3_ast y) Creates the equality x = y . More...
Z3_ast MkNot (Z3_ast a) Mk an expression representing not(a). More...
Z3_ast MkAnd (params Z3_ast[] t) Create an expression representing t[0] and t[1] and .... More...
Z3_ast MkOr (params Z3_ast[] t) Create an expression representing t[0] or t[1] or .... More...
Z3_ast MkReal (string v) Create a real numeral. More...
Z3_ast MkNumeral (int v, Z3_sort sort) Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. More...
Z3_ast MkNumeral (uint v, Z3_sort sort) Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. More...
Z3_ast MkNumeral (long v, Z3_sort sort) Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. More...
Z3_ast MkIte (Z3_ast t1, Z3_ast t2, Z3_ast t3) Create an expression representing an if-then-else: ite(t1, t2, t3). More...
Z3_ast MkImplies (Z3_ast t1, Z3_ast t2) Create an expression representing t1 -> t2. More...
Z3_sort MkBvSort (uint size) Returns the BvSort for size in this NativeContext More...
Z3_sort MkListSort (string name, Z3_sort elemSort, out Z3_func_decl inil, out Z3_func_decl iisnil, out Z3_func_decl icons, out Z3_func_decl iiscons, out Z3_func_decl ihead, out Z3_func_decl itail) returns ListSort More...
Z3_sort MkArraySort (Z3_sort domain, Z3_sort range) Create a new array sort. More...
Z3_sort MkTupleSort (Z3_symbol name, Z3_symbol[] fieldNames, Z3_sort[] fieldSorts, out Z3_func_decl constructor, Z3_func_decl[] projections) Create a new tuple sort. More...
Z3_ast MkTrue () The true Term. More...
Z3_ast MkFalse () The false Term. More...
Z3_ast MkBool (bool value) Creates a Boolean value. More...
Z3_ast MkIff (Z3_ast t1, Z3_ast t2) Create an expression representing t1 iff t2. More...
Z3_ast MkConst (string name, Z3_sort range) Creates a new Constant of sort range and named name . More...
Z3_symbol MkStringSymbol (string name) Return a ptr to symbol for string More...
Z3_ast MkApp (Z3_func_decl f, params Z3_ast[] args) Create a new function application. More...
Z3_ast MkBound (uint index, Z3_sort sort) Creates a new bound variable. More...
Z3_ast_vector MkBvAnd (Z3_ast_vector t1, Z3_ast_vector t2) Bitwise conjunction. More...
Z3_ast_vector MkBvNot (Z3_ast_vector t) Bitwise negation. More...
Z3_ast_vector MkBvNeg (Z3_ast_vector t) Standard two's complement unary minus. More...
Z3_ast_vector MkBVNeg (Z3_ast_vector t) Standard two's complement unary minus. More...
Z3_ast_vector MkBvAdd (Z3_ast_vector t1, Z3_ast_vector t2) Two's complement addition. More...
Z3_ast_vector MkBvExtract (uint high, uint low, Z3_ast_vector t) Bit-vector extraction. More...
Z3_ast_vector MkBvSignExt (uint i, Z3_ast_vector t) Bit-vector sign extension. More...
Z3_ast_vector MkBvZeroExt (uint i, Z3_ast_vector t) Bit-vector zero extension. More...
Z3_ast_vector MkBvShl (Z3_ast_vector t1, Z3_ast_vector t2) Shift left. More...
Z3_ast_vector MkBvLshr (Z3_ast_vector t1, Z3_ast_vector t2) Logical shift right More...
Z3_ast_vector MkBvAshr (Z3_ast_vector t1, Z3_ast_vector t2) Arithmetic shift right More...
Z3_ast MkBvSlt (Z3_ast_vector t1, Z3_ast_vector t2) Two's complement signed less-than More...
Z3_ast_vector MkBvMul (Z3_ast_vector t1, Z3_ast_vector t2) Two's complement multiplication. More...
Z3_ast_vector MkBvUdiv (Z3_ast_vector t1, Z3_ast_vector t2) Unsigned division. More...
Z3_ast_vector MkBvSdiv (Z3_ast_vector t1, Z3_ast_vector t2) Signed division. More...
Z3_ast_vector MkBvUrem (Z3_ast_vector t1, Z3_ast_vector t2) Unsigned remainder. More...
Z3_ast_vector MkBvSrem (Z3_ast_vector t1, Z3_ast_vector t2) Signed remainder. More...
Z3_ast_vector MkBvSub (Z3_ast_vector t1, Z3_ast_vector t2) Two's complement subtraction. More...
Z3_ast_vector MkBvOr (Z3_ast_vector t1, Z3_ast_vector t2) Bitwise disjunction. More...
Z3_ast_vector MkBvXor (Z3_ast_vector t1, Z3_ast_vector t2) Bitwise XOR. More...
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. More...
Z3_ast MkExists (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) Same as MkForAll but defaults to "forall" = false Create an existential Quantifier. More...
Z3_ast MkConstArray (Z3_sort domain, Z3_ast v) Create a constant array. More...
Z3_ast MkStore (Z3_ast a, Z3_ast i, Z3_ast v) Array update. More...
Z3_ast MkSelect (Z3_ast array, Z3_ast index) Array read. More...
Z3_ast MkDefault (Z3_ast a) Access the array default value. More...
Z3_func_decl MkFuncDecl (string name, Z3_sort[] domain, Z3_sort range) Creates a new function declaration. More...
Z3_func_decl MkFuncDecl (string name, Z3_sort domain, Z3_sort range) Creates a new function declaration. More...
Z3_func_decl MkFreshFuncDecl (string prefix, Z3_sort[] domain, Z3_sort range) Creates a fresh function declaration with a name prefixed with prefix . More...
Z3_func_decl MkConstDecl (string name, Z3_sort range) Creates a new constant function declaration. More...
Z3_sort[] GetDomain (Z3_func_decl fdecl) Get domain for a funcdecl More...
Z3_sort GetRange (Z3_func_decl fdecl) Get range for a funcdecl More...
Z3_pattern MkPattern (params Z3_ast[] terms) Create a quantifier pattern. More...
NativeSolver MkSimpleSolver () Creates a new (incremental) solver. More...
Z3_sort_kind GetSortKind (Z3_sort sort) Get the sort kind from IntPtr More...
Z3_ast_kind GetAstKind (Z3_ast ast) Get the AST kind from IntPtr More...
Z3_decl_kind GetDeclKind (Z3_func_decl decl) Get the Decl kind from IntPtr More...
Z3_sort GetSort (Z3_ast ast) Get Sort for AST More...
Z3_ast[] GetAppArgs (Z3_app app) Get the arguments for app More...
uint GetNumArgs (Z3_app app) Return number of arguments for app More...
Z3_func_decl GetAppDecl (Z3_ast ast) Get App Decl from IntPtr More...
string GetDeclName (Z3_func_decl decl) Get string name for Decl More...
uint GetBvSortSize (Z3_sort bvSort) Get size of BitVector Sort More...
Z3_sort GetArraySortDomain (Z3_ast array) Get the domain IntPtr for Sort More...
Z3_sort GetArraySortRange (Z3_ast array) Get the range IntPtr for Sort More...
bool TryGetNumeralInt (Z3_ast v, out int i) Try to get integer from AST More...
bool TryGetNumeralUInt (Z3_ast v, out uint u) Try to get uint from AST More...
bool TryGetNumeralInt64 (Z3_ast v, out long i) Try to get long from AST More...
bool TryGetNumeralUInt64 (Z3_ast v, out ulong u) Try get ulong from AST More...
string GetNumeralString (Z3_ast v) Get string for numeral ast More...
string ToString (Z3_ast ast) Get printable string representing Z3_ast More...
void ToggleWarningMessages (bool turnOn) Enable or disable warning messages More...
void Dispose () Disposes of the context. More...
Z3_ast[] ToArray (Z3_ast_vector vec) Utility to convert a vector object of ast to a .Net array More...
Statistics.Entry[] GetStatistics (Z3_stats stats) Retrieve statistics as an array of entries More...

The main interaction with Z3 happens via the Context. NativeContext allows for efficient wrapper-reduced interaction with Z3 expressions.

Definition at line 42 of file NativeContext.cs.

◆ NativeContext()

Constructor.

The following parameters can be set:

proof (Boolean) Enable proof generation
debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting
trace (Boolean) Tracing support for VCC
trace_file_name (String) Trace out file for VCC traces
timeout (unsigned) default timeout (in milliseconds) used for solvers
well_sorted_check type checker
auto_config use heuristics to automatically select solver and configure it
model model generation for solvers, this parameter can be overwritten when creating a solver
model_validate validate models produced by solvers
unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver Note that in previous versions of Z3, this constructor was also used to set global and module parameters. For this purpose we should now use Global.SetParameter

Definition at line 62 of file NativeContext.cs.

65

Debug.Assert(settings !=

null

);

69

IntPtr cfg = Native.Z3_mk_config();

70 foreach

(KeyValuePair<string, string> kv

in

settings)

71

Native.Z3_set_param_value(cfg, kv.Key, kv.Value);

72

m_ctx = Native.Z3_mk_context(cfg);

73

Native.Z3_del_config(cfg);

◆ Dispose()

Disposes of the context.

Definition at line 1371 of file NativeContext.cs.

1373 if

(m_ctx != IntPtr.Zero)

1375

m_n_err_handler =

null

;

1377

m_ctx = IntPtr.Zero;

1378

Native.Z3_del_context(ctx);

1381

GC.ReRegisterForFinalize(

this

);

◆ EnableTrace() static void EnableTrace ( string tag ) inlinestatic

Enable trace to file

Parameters

Definition at line 1358 of file NativeContext.cs.

1360

Debug.Assert(!

string

.IsNullOrEmpty(tag));

1361

Native.Z3_enable_trace(tag);

◆ GetAppArgs()

Get the arguments for app

Parameters

Returns

Definition at line 1145 of file NativeContext.cs.

1148

var args =

new Z3_ast

[numArgs];

1149 for

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

1151

args[i] = GetAppArg(app, i);

uint GetNumArgs(Z3_app app)

Return number of arguments for app

◆ GetAppDecl() ◆ GetArraySortDomain()

Get the domain IntPtr for Sort

Definition at line 1206 of file NativeContext.cs.

1208

Debug.Assert(array != IntPtr.Zero);

1210 return

Native.Z3_get_array_sort_domain(nCtx, array);

◆ GetArraySortRange()

Get the range IntPtr for Sort

Definition at line 1216 of file NativeContext.cs.

1218

Debug.Assert(array != IntPtr.Zero);

1220 return

Native.Z3_get_array_sort_range(nCtx, array);

◆ GetAstKind()

Get the AST kind from IntPtr

Definition at line 1113 of file NativeContext.cs.

1115

Debug.Assert(ast != IntPtr.Zero);

1117 return

(

Z3_ast_kind

)Native.Z3_get_ast_kind(nCtx, ast);

Z3_ast_kind

The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.

Referenced by NativeModel.TryGetArrayValue().

◆ GetBvSortSize() uint GetBvSortSize ( Z3_sort bvSort ) inline

Get size of BitVector Sort

Definition at line 1196 of file NativeContext.cs.

1198

Debug.Assert(bvSort != IntPtr.Zero);

1200 return

Native.Z3_get_bv_sort_size(nCtx, bvSort);

◆ GetDeclKind() ◆ GetDeclName()

Get string name for Decl

Parameters

Returns

Definition at line 1185 of file NativeContext.cs.

1187

Debug.Assert(decl != IntPtr.Zero);

1189

var namePtr = Native.Z3_get_decl_name(nCtx, decl);

1190 return

Marshal.PtrToStringAnsi(namePtr);

◆ GetDomain()

Get domain for a funcdecl

Parameters

Returns

Definition at line 1045 of file NativeContext.cs.

1047

Debug.Assert(fdecl != IntPtr.Zero);

1049

var sz = Native.Z3_get_domain_size(nCtx, fdecl);

1050

var domain =

new Z3_sort

[sz];

1051 for

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

1053

domain[i] = Native.Z3_get_domain(nCtx, fdecl, i);

◆ GetNumArgs() uint GetNumArgs ( Z3_app app ) inline ◆ GetNumeralString() string GetNumeralString ( Z3_ast v ) inline

Get string for numeral ast

Parameters

Returns

Definition at line 1304 of file NativeContext.cs.

1306

Debug.Assert(v != IntPtr.Zero);

1307 return

Native.Z3_get_numeral_string(nCtx, v);

◆ GetRange()

Get range for a funcdecl

Parameters

Returns

Definition at line 1063 of file NativeContext.cs.

1065

Debug.Assert(fdecl != IntPtr.Zero);

1067 return

Native.Z3_get_range(nCtx, fdecl);

◆ GetSort()

Get Sort for AST

Definition at line 1133 of file NativeContext.cs.

1135

Debug.Assert(ast != IntPtr.Zero);

1137 return

Native.Z3_get_sort(nCtx, ast);

◆ GetSortKind()

Get the sort kind from IntPtr

Definition at line 1103 of file NativeContext.cs.

1105

Debug.Assert(sort != IntPtr.Zero);

1107 return

(

Z3_sort_kind

)Native.Z3_get_sort_kind(nCtx, sort);

Z3_sort_kind

The different kinds of Z3 types (See Z3_get_sort_kind).

◆ GetStatistics()

Retrieve statistics as an array of entries

Parameters

Returns

Definition at line 1407 of file NativeContext.cs.

1409

Native.Z3_stats_inc_ref(nCtx, stats);

1410

var result = Statistics.NativeEntries(nCtx, stats);

1411

Native.Z3_stats_dec_ref(nCtx, stats);

◆ MkAdd()

Create an expression representing t[0] + t[1] + ....

Definition at line 83 of file NativeContext.cs.

85

Debug.Assert(t !=

null

);

86

Debug.Assert(t.All(a => a != IntPtr.Zero));

88 return

Native.Z3_mk_add(nCtx, (uint)(t?.

Length

?? 0), t);

◆ MkAnd()

Create an expression representing t[0] and t[1] and ....

Definition at line 221 of file NativeContext.cs.

223

Debug.Assert(t !=

null

);

224

Debug.Assert(t.All(a => a != IntPtr.Zero));

226 return

Native.Z3_mk_and(nCtx, (uint)(t?.

Length

?? 0), t);

◆ MkApp()

Create a new function application.

Definition at line 466 of file NativeContext.cs.

468

Debug.Assert(f != IntPtr.Zero);

469

Debug.Assert(args ==

null

|| args.All(a => a != IntPtr.Zero));

471 return

Native.Z3_mk_app(nCtx, f, (uint)(args?.

Length

?? 0), args);

Referenced by NativeSolver.AssertInjective().

◆ MkArraySort()

Create a new array sort.

Definition at line 381 of file NativeContext.cs.

383

Debug.Assert(domain != IntPtr.Zero);

384

Debug.Assert(

range

!= IntPtr.Zero);

386 return

Native.Z3_mk_array_sort(nCtx, domain,

range

);

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

◆ MkBool() ◆ MkBound()

Creates a new bound variable.

Parameters: index The de-Bruijn index of the variable sort The sort of the variable

Definition at line 482 of file NativeContext.cs.

484

Debug.Assert(sort != IntPtr.Zero);

486 return

Native.Z3_mk_bound(nCtx, index, sort);

Referenced by NativeSolver.AssertInjective().

◆ MkBvAdd()

Two's complement addition.

The arguments must have the same bit-vector sort.

Definition at line 540 of file NativeContext.cs.

542

Debug.Assert(t1 != IntPtr.Zero);

543

Debug.Assert(t2 != IntPtr.Zero);

545 return

Native.Z3_mk_bvadd(nCtx, t1, t2);

◆ MkBvAnd()

Bitwise conjunction.

The arguments must have a bit-vector sort.

Definition at line 495 of file NativeContext.cs.

497

Debug.Assert(t1 != IntPtr.Zero);

498

Debug.Assert(t2 != IntPtr.Zero);

500 return

Native.Z3_mk_bvand(nCtx, t1, t2);

◆ MkBvAshr()

Arithmetic shift right

It is like logical shift right except that the most significant bits of the result always copy the most significant bit of the second argument.

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

The arguments must have a bit-vector sort.

Definition at line 649 of file NativeContext.cs.

651

Debug.Assert(t1 != IntPtr.Zero);

652

Debug.Assert(t2 != IntPtr.Zero);

654 return

Native.Z3_mk_bvashr(nCtx, t1, t2);

◆ MkBvExtract()

Bit-vector extraction.

Extract the bits high down to low from a bitvector of size m to yield a new bitvector of size n, where n = high - low + 1. The argument t must have a bit-vector sort.

Definition at line 557 of file NativeContext.cs.

559

Debug.Assert(t != IntPtr.Zero);

561 return

Native.Z3_mk_extract(nCtx, high, low, t);

◆ MkBvLshr()

Logical shift right

It is equivalent to unsigned division by 2^x where x is the value of t2 .

The arguments must have a bit-vector sort.

Definition at line 627 of file NativeContext.cs.

629

Debug.Assert(t1 != IntPtr.Zero);

630

Debug.Assert(t2 != IntPtr.Zero);

632 return

Native.Z3_mk_bvlshr(nCtx, t1, t2);

◆ MkBvMul()

Two's complement multiplication.

The arguments must have the same bit-vector sort.

Definition at line 675 of file NativeContext.cs.

677

Debug.Assert(t1 != IntPtr.Zero);

678

Debug.Assert(t2 != IntPtr.Zero);

680 return

Native.Z3_mk_bvmul(nCtx, t1, t2);

◆ MkBvNeg()

Standard two's complement unary minus.

The arguments must have a bit-vector sort.

Definition at line 518 of file NativeContext.cs.

520

Debug.Assert(t != IntPtr.Zero);

522 return

Native.Z3_mk_bvneg(nCtx, t);

◆ MkBVNeg()

Standard two's complement unary minus.

The arguments must have a bit-vector sort.

Definition at line 529 of file NativeContext.cs.

531

Debug.Assert(t != IntPtr.Zero);

533 return

Native.Z3_mk_bvneg(nCtx, t);

◆ MkBvNot()

Bitwise negation.

The argument must have a bit-vector sort.

Definition at line 507 of file NativeContext.cs.

509

Debug.Assert(t != IntPtr.Zero);

511 return

Native.Z3_mk_bvnot(nCtx, t);

◆ MkBvOr()

Bitwise disjunction.

The arguments must have a bit-vector sort.

Definition at line 771 of file NativeContext.cs.

773

Debug.Assert(t1 != IntPtr.Zero);

774

Debug.Assert(t2 != IntPtr.Zero);

776 return

Native.Z3_mk_bvor(nCtx, t1, t2);

◆ MkBvSdiv()

Signed division.

It is defined in the following way:

The floor of t1/t2 if t2 is different from zero, and t1*t2 >= 0.
The ceiling of t1/t2 if t2 is different from zero, and t1*t2 < 0.

If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.

Definition at line 713 of file NativeContext.cs.

715

Debug.Assert(t1 != IntPtr.Zero);

716

Debug.Assert(t2 != IntPtr.Zero);

718 return

Native.Z3_mk_bvsdiv(nCtx, t1, t2);

◆ MkBvShl()

Shift left.

It is equivalent to multiplication by 2^x where x is the value of t2 .

The arguments must have a bit-vector sort.

Definition at line 607 of file NativeContext.cs.

609

Debug.Assert(t1 != IntPtr.Zero);

610

Debug.Assert(t2 != IntPtr.Zero);

612 return

Native.Z3_mk_bvshl(nCtx, t1, t2);

◆ MkBvSignExt()

Bit-vector sign extension.

Sign-extends the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector. The argument t must have a bit-vector sort.

Definition at line 572 of file NativeContext.cs.

574

Debug.Assert(t != IntPtr.Zero);

576 return

Native.Z3_mk_sign_ext(nCtx, i, t);

◆ MkBvSlt()

Two's complement signed less-than

The arguments must have the same bit-vector sort.

Definition at line 663 of file NativeContext.cs.

665

Debug.Assert(t1 != IntPtr.Zero);

666

Debug.Assert(t2 != IntPtr.Zero);

668 return

Native.Z3_mk_bvslt(nCtx, t1, t2);

◆ MkBvSort() ◆ MkBvSrem()

Signed remainder.

It is defined as t1 - (t1 /s t2) * t2, where /s represents signed division. The most significant bit (sign) of the result is equal to the most significant bit of t1.

If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.

Definition at line 747 of file NativeContext.cs.

749

Debug.Assert(t1 != IntPtr.Zero);

750

Debug.Assert(t2 != IntPtr.Zero);

752 return

Native.Z3_mk_bvsrem(nCtx, t1, t2);

◆ MkBvSub()

Two's complement subtraction.

The arguments must have the same bit-vector sort.

Definition at line 759 of file NativeContext.cs.

761

Debug.Assert(t1 != IntPtr.Zero);

762

Debug.Assert(t2 != IntPtr.Zero);

764 return

Native.Z3_mk_bvsub(nCtx, t1, t2);

◆ MkBvUdiv()

Unsigned division.

It is defined as the floor of t1/t2 if t2 is different from zero. If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.

Definition at line 692 of file NativeContext.cs.

694

Debug.Assert(t1 != IntPtr.Zero);

695

Debug.Assert(t2 != IntPtr.Zero);

697 return

Native.Z3_mk_bvudiv(nCtx, t1, t2);

◆ MkBvUle()

Unsigned less-than-equal

The arguments must have the same bit-vector sort.

Definition at line 189 of file NativeContext.cs.

191

Debug.Assert(t1 != IntPtr.Zero);

192

Debug.Assert(t2 != IntPtr.Zero);

194 return

Native.Z3_mk_bvule(nCtx, t1, t2);

◆ MkBvUlt()

Unsigned less-than

The arguments must have the same bit-vector sort.

Definition at line 175 of file NativeContext.cs.

177

Debug.Assert(t1 != IntPtr.Zero);

178

Debug.Assert(t2 != IntPtr.Zero);

180 return

Native.Z3_mk_bvult(nCtx, t1, t2);

◆ MkBvUrem()

Unsigned remainder.

It is defined as t1 - (t1 /u t2) * t2, where /u represents unsigned division. If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.

Definition at line 729 of file NativeContext.cs.

731

Debug.Assert(t1 != IntPtr.Zero);

732

Debug.Assert(t2 != IntPtr.Zero);

734 return

Native.Z3_mk_bvurem(nCtx, t1, t2);

◆ MkBvXor()

Bitwise XOR.

The arguments must have a bit-vector sort.

Definition at line 783 of file NativeContext.cs.

785

Debug.Assert(t1 !=

null

);

786

Debug.Assert(t2 != IntPtr.Zero);

788 return

Native.Z3_mk_bvxor(nCtx, t1, t2);

◆ MkBvZeroExt()

Bit-vector zero extension.

Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector. The argument t must have a bit-vector sort.

Definition at line 588 of file NativeContext.cs.

590

Debug.Assert(t != IntPtr.Zero);

592 return

Native.Z3_mk_zero_ext(nCtx, i, t);

◆ MkConst()

Creates a new Constant of sort range and named name .

Definition at line 438 of file NativeContext.cs.

440

Debug.Assert(!

string

.IsNullOrEmpty(name));

441

Debug.Assert(

range

!= IntPtr.Zero);

Z3_symbol MkStringSymbol(string name)

Return a ptr to symbol for string

◆ MkConstArray()

Create a constant array.

The resulting term is an array, such that a selecton an arbitrary index produces the value v.

Definition at line 920 of file NativeContext.cs.

922

Debug.Assert(domain != IntPtr.Zero);

923

Debug.Assert(v != IntPtr.Zero);

925 return

Native.Z3_mk_const_array(nCtx, domain, v);

◆ MkConstDecl()

Creates a new constant function declaration.

Definition at line 1032 of file NativeContext.cs.

1034

Debug.Assert(

range

!= IntPtr.Zero);

1036

var symbol = Native.Z3_mk_string_symbol(nCtx, name);

1037 return

Native.Z3_mk_func_decl(nCtx, symbol, 0,

new

IntPtr[0],

range

);

◆ MkDefault()

Access the array default value.

Produces the default range value, for arrays that can be represented as finite maps with a default range value.

Definition at line 978 of file NativeContext.cs.

980

Debug.Assert(a !=

null

);

982 return

Native.Z3_mk_array_default(nCtx, a);

◆ MkDiv()

Create an expression representing t1 / t2.

Definition at line 117 of file NativeContext.cs.

119

Debug.Assert(t1 != IntPtr.Zero);

120

Debug.Assert(t2 != IntPtr.Zero);

122 return

Native.Z3_mk_div(nCtx, t1, t2);

◆ MkEq() ◆ MkExists()

Same as MkForAll but defaults to "forall" = false Create an existential Quantifier.

Parameters: sorts names body weight patterns noPatterns quantifierID skolemID

Returns

Definition at line 835 of file NativeContext.cs.

837 return

MkQuantifier(

false

, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);

◆ MkFalse() ◆ MkForall()

Create a universal Quantifier.

Creates a forall formula, where weight is the weight, patterns is an array of patterns, sorts is an array with the sorts of the bound variables, names is an array with the 'names' of the bound variables, and body is the body of the quantifier. Quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. Note that the bound variables are de-Bruijn indices created using MkBound. Z3 applies the convention that the last element in names and sorts refers to the variable with index 0, the second to last element of names and sorts refers to the variable with index 1, etc.

Parameters: sorts the sorts of the bound variables. names names of the bound variables body the body of the quantifier. weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0. patterns array containing the patterns created using MkPattern. noPatterns array containing the anti-patterns created using MkPattern. quantifierID optional symbol to track quantifier. skolemID optional symbol to track skolem constants.

Definition at line 817 of file NativeContext.cs.

819 return

MkQuantifier(

true

, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);

Referenced by NativeSolver.AssertInjective().

◆ MkFreshFuncDecl()

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

Definition at line 1020 of file NativeContext.cs.

1022

Debug.Assert(domain !=

null

);

1023

Debug.Assert(

range

!= IntPtr.Zero);

1024

Debug.Assert(domain.All(d => d != IntPtr.Zero));

1026 return

Native.Z3_mk_fresh_func_decl(nCtx, prefix, (uint)(domain?.

Length

?? 0), domain,

range

);

Referenced by NativeSolver.AssertInjective().

◆ MkFuncDecl() [1/2]

Creates a new function declaration.

Definition at line 1006 of file NativeContext.cs.

1008

Debug.Assert(!

string

.IsNullOrEmpty(name));

1009

Debug.Assert(

range

!= IntPtr.Zero);

1010

Debug.Assert(domain != IntPtr.Zero);

1012

var symbol = Native.Z3_mk_string_symbol(nCtx, name);

1013

var q =

new Z3_sort

[] { domain };

1014 return

Native.Z3_mk_func_decl(nCtx, symbol, (uint)q.Length, q,

range

);

◆ MkFuncDecl() [2/2]

Creates a new function declaration.

Definition at line 992 of file NativeContext.cs.

994

Debug.Assert(!

string

.IsNullOrEmpty(name));

995

Debug.Assert(

range

!= IntPtr.Zero);

996

Debug.Assert(domain !=

null

);

997

Debug.Assert(domain.All(d => d != IntPtr.Zero));

999

var symbol = Native.Z3_mk_string_symbol(nCtx, name);

1000 return

Native.Z3_mk_func_decl(nCtx, symbol, (uint)(domain?.

Length

?? 0), domain,

range

);

◆ MkGe()

Create an expression representing t1 >= t2

Definition at line 150 of file NativeContext.cs.

152

Debug.Assert(t1 != IntPtr.Zero);

153

Debug.Assert(t2 != IntPtr.Zero);

155 return

Native.Z3_mk_ge(nCtx, t1, t2);

◆ MkGt()

Create an expression representing t1 > t2

Definition at line 161 of file NativeContext.cs.

163

Debug.Assert(t1 != IntPtr.Zero);

164

Debug.Assert(t2 != IntPtr.Zero);

166 return

Native.Z3_mk_gt(nCtx, t1, t2);

◆ MkIff()

Create an expression representing t1 iff t2.

Definition at line 425 of file NativeContext.cs.

427

Debug.Assert(t1 != IntPtr.Zero);

428

Debug.Assert(t2 != IntPtr.Zero);

430 return

Native.Z3_mk_iff(nCtx, t1, t2);

◆ MkImplies()

Create an expression representing t1 -> t2.

Definition at line 306 of file NativeContext.cs.

308

Debug.Assert(t1 != IntPtr.Zero);

309

Debug.Assert(t2 != IntPtr.Zero);

311 return

Native.Z3_mk_implies(nCtx, t1, t2);

◆ MkIte()

Create an expression representing an if-then-else: ite(t1, t2, t3).

Parameters: t1 An expression with Boolean sort t2 An expression t3 An expression with the same sort as t2

Definition at line 294 of file NativeContext.cs.

296

Debug.Assert(t1 != IntPtr.Zero);

297

Debug.Assert(t2 != IntPtr.Zero);

298

Debug.Assert(t3 != IntPtr.Zero);

300 return

Native.Z3_mk_ite(nCtx, t1, t2, t3);

◆ MkLe()

Create an expression representing t1 <= t2

Definition at line 128 of file NativeContext.cs.

130

Debug.Assert(t1 != IntPtr.Zero);

131

Debug.Assert(t2 != IntPtr.Zero);

133 return

Native.Z3_mk_le(nCtx, t1, t2);

◆ MkListSort()

returns ListSort

Parameters: name elemSort inil iisnil icons iiscons ihead itail

Returns: The list algebraic datatype

Definition at line 352 of file NativeContext.cs.

357

Debug.Assert(!

string

.IsNullOrEmpty(name));

358

Debug.Assert(elemSort != IntPtr.Zero);

360

IntPtr nil = IntPtr.Zero, isnil = IntPtr.Zero,

361

cons = IntPtr.Zero, iscons = IntPtr.Zero,

362

head = IntPtr.Zero, tail = IntPtr.Zero;

364

var symbol = Native.Z3_mk_string_symbol(nCtx, name);

365

var sort = Native.Z3_mk_list_sort(nCtx, symbol, elemSort,

366

ref nil, ref isnil, ref cons, ref iscons, ref head, ref tail);

◆ MkLt()

Create an expression representing t1 < t2

Definition at line 139 of file NativeContext.cs.

141

Debug.Assert(t1 != IntPtr.Zero);

142

Debug.Assert(t2 != IntPtr.Zero);

144 return

Native.Z3_mk_lt(nCtx, t1, t2);

◆ MkMul()

Create an expression representing t[0] * t[1] * ....

Definition at line 94 of file NativeContext.cs.

96

Debug.Assert(t !=

null

);

97

Debug.Assert(t.All(a => a != IntPtr.Zero));

100 return

Native.Z3_mk_mul(nCtx, (uint)(ts?.

Length

?? 0), ts);

◆ MkNot()

Mk an expression representing not(a).

Definition at line 211 of file NativeContext.cs.

213

Debug.Assert(a != IntPtr.Zero);

215 return

Native.Z3_mk_not(nCtx, a);

◆ MkNumeral() [1/3]

Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer.

Parameters: v Value of the numeral sort Sort of the numeral

Definition at line 257 of file NativeContext.cs.

259

Debug.Assert(sort != IntPtr.Zero);

261 return

Native.Z3_mk_int(nCtx, v, sort);

◆ MkNumeral() [2/3]

Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer.

Parameters: v Value of the numeral sort Sort of the numeral

Definition at line 281 of file NativeContext.cs.

283

Debug.Assert(sort !=

null

);

285 return

Native.Z3_mk_int64(nCtx, v, sort);

◆ MkNumeral() [3/3]

Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer.

Parameters: v Value of the numeral sort Sort of the numeral

Definition at line 269 of file NativeContext.cs.

271

Debug.Assert(sort !=

null

);

273 return

Native.Z3_mk_unsigned_int(nCtx, v, sort);

◆ MkOr()

Create an expression representing t[0] or t[1] or ....

Definition at line 232 of file NativeContext.cs.

234

Debug.Assert(t !=

null

);

235

Debug.Assert(t.All(a => a != IntPtr.Zero));

237 return

Native.Z3_mk_or(nCtx, (uint)(t?.

Length

?? 0), t);

◆ MkPattern()

Create a quantifier pattern.

Definition at line 1076 of file NativeContext.cs.

1078

Debug.Assert(terms !=

null

);

1079 if

(terms ==

null

|| terms.Length == 0)

1080 throw new

Z3Exception(

"Cannot create a pattern from zero terms"

);

1082 return

Native.Z3_mk_pattern(nCtx, (uint)terms.Length, terms);

◆ MkReal()

Create a real numeral.

Parameters: v A string representing the Term value in decimal notation.

Returns: A Term with value v and sort Real

Definition at line 246 of file NativeContext.cs.

248

Debug.Assert(!

string

.IsNullOrEmpty(v));

249 return

Native.Z3_mk_numeral(nCtx, v,

RealSort

);

Z3_sort RealSort

Returns the "singleton" RealSort for this NativeContext

◆ MkSelect()

Array read.

The argument array is the array and index is the index of the array that gets read.

The node array must have an array sort [domain -> range], and index must have the sort domain. The sort of the result is range.

Definition at line 963 of file NativeContext.cs.

965

Debug.Assert(array != IntPtr.Zero);

966

Debug.Assert(index != IntPtr.Zero);

968 return

Native.Z3_mk_select(nCtx, array, index);

◆ MkSimpleSolver()

Creates a new (incremental) solver.

Definition at line 1091 of file NativeContext.cs.

1093 Z3_solver

nSolver = Native.Z3_mk_simple_solver(nCtx);

1094 return new

NativeSolver(

this

, nSolver);

◆ MkStore()

Array update.

The node a must have an array sort [domain -> range], i must have sort domain, v must have sort range. The sort of the result is [domain -> range]. The semantics of this function is given by the theory of arrays described in the SMT-LIB standard. See http://smtlib.org for more details. The result of this function is an array that is equal to a (with respect to select) on all indices except for i, where it maps to v (and the select of a with respect to i may be a different value).

Definition at line 943 of file NativeContext.cs.

945

Debug.Assert(a != IntPtr.Zero);

946

Debug.Assert(i != IntPtr.Zero);

947

Debug.Assert(v != IntPtr.Zero);

949 return

Native.Z3_mk_store(nCtx, a, i, v);

◆ MkStringSymbol()

Return a ptr to symbol for string

Parameters

Returns

Definition at line 454 of file NativeContext.cs.

456

Debug.Assert(!

string

.IsNullOrEmpty(name));

458 return

Native.Z3_mk_string_symbol(nCtx, name);

Referenced by NativeContext.MkConst().

◆ MkSub()

Create an expression representing t[0] - t[1] - ....

Definition at line 106 of file NativeContext.cs.

108

Debug.Assert(t !=

null

);

109

Debug.Assert(t.All(a => a != IntPtr.Zero));

110

var ts = t.ToArray();

111 return

Native.Z3_mk_sub(nCtx, (uint)(ts?.

Length

?? 0), ts);

◆ MkTrue() ◆ MkTupleSort()

Create a new tuple sort.

Definition at line 392 of file NativeContext.cs.

394

Debug.Assert(name != IntPtr.Zero);

395

Debug.Assert(fieldNames !=

null

);

396

Debug.Assert(fieldNames.All(fn => fn != IntPtr.Zero));

397

Debug.Assert(fieldSorts ==

null

|| fieldSorts.All(fs => fs != IntPtr.Zero));

399

var numFields = (uint)(fieldNames?.

Length

?? 0);

400

constructor = IntPtr.Zero;

401 return

Native.Z3_mk_tuple_sort(nCtx, name, numFields, fieldNames, fieldSorts, ref constructor, projections);

◆ ToArray()

Utility to convert a vector object of ast to a .Net array

Parameters

Returns

Definition at line 1391 of file NativeContext.cs.

1393

Native.Z3_ast_vector_inc_ref(nCtx, vec);

1394

var sz = Native.Z3_ast_vector_size(nCtx, vec);

1395

var result =

new Z3_ast

[sz];

1396 for

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

1397

result[i] = Native.Z3_ast_vector_get(nCtx, vec, i);

1398

Native.Z3_ast_vector_dec_ref(nCtx, vec);

◆ ToggleWarningMessages() void ToggleWarningMessages ( bool turnOn )

Enable or disable warning messages

Parameters

◆ ToString() string ToString ( Z3_ast ast ) inline

Get printable string representing Z3_ast

Parameters

Returns

Definition at line 1315 of file NativeContext.cs.

1317

Debug.Assert(ast != IntPtr.Zero);

1319 return

Native.Z3_ast_to_string(nCtx, ast);

◆ TryGetNumeralInt() bool TryGetNumeralInt ( Z3_ast v, out int i ) inline

Try to get integer from AST

Parameters

Returns

Definition at line 1229 of file NativeContext.cs.

1231

Debug.Assert(v != IntPtr.Zero);

1234 if

(Native.Z3_get_numeral_int(nCtx, v, ref result) == 0)

◆ TryGetNumeralInt64() bool TryGetNumeralInt64 ( Z3_ast v, out long i ) inline

Try to get long from AST

Parameters

Returns

Definition at line 1267 of file NativeContext.cs.

1269

Debug.Assert(v != IntPtr.Zero);

1271 long

result = i = 0;

1272 if

(Native.Z3_get_numeral_int64(nCtx, v, ref result) == 0)

◆ TryGetNumeralUInt() bool TryGetNumeralUInt ( Z3_ast v, out uint u ) inline

Try to get uint from AST

Parameters

Returns

Definition at line 1248 of file NativeContext.cs.

1250

Debug.Assert(v != IntPtr.Zero);

1252

uint result = u = 0;

1253 if

(Native.Z3_get_numeral_uint(nCtx, v, ref result) == 0)

◆ TryGetNumeralUInt64() bool TryGetNumeralUInt64 ( Z3_ast v, out ulong u ) inline

Try get ulong from AST

Parameters

Returns

Definition at line 1286 of file NativeContext.cs.

1288

Debug.Assert(v != IntPtr.Zero);

1290

ulong result = u = 0;

1291 if

(Native.Z3_get_numeral_uint64(nCtx, v, ref result) == 0)

◆ BoolSort ◆ IntSort ◆ PrintMode

Selects the format used for pretty-printing expressions.

The default mode for pretty printing expressions is to produce SMT-LIB style output where common subexpressions are printed at each occurrence. The mode is called Z3_PRINT_SMTLIB_FULL. To print shared common subexpressions only once, use the Z3_PRINT_LOW_LEVEL mode. To print in way that conforms to SMT-LIB standards and uses let expressions to share common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT.

See also: AST.ToString(), Pattern.ToString(), FuncDecl.ToString(), Sort.ToString()

Definition at line 903 of file NativeContext.cs.

905 set

{ Native.Z3_set_ast_print_mode(nCtx, (uint)value); }

◆ RealSort

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