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

Inheritance diagram for NativeContext:

Public Member Functions
	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...

Static Public Member Functions
static void	EnableTrace (string tag)
	Enable trace to file More...

Properties
Z3_sort	IntSort `[get]`
	Integer Sort More...

Z3_sort	BoolSort `[get]`
	Returns the "singleton" BoolSort for this NativeContext More...

Z3_sort	RealSort `[get]`
	Returns the "singleton" RealSort for this NativeContext More...

Z3_ast_print_mode	PrintMode `[set]`
	Selects the format used for pretty-printing expressions. More...

Detailed Description

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.

Constructor & Destructor Documentation

◆ NativeContext()

NativeContext ( Dictionary< string, string > settings )

inline

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.

             : base()
         {
             Debug.Assert(settings != null);
  
             lock (creation_lock)
             {
                 IntPtr cfg = Native.Z3_mk_config();
                 foreach (KeyValuePair<string, string> kv in settings)
                     Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
                 m_ctx = Native.Z3_mk_context(cfg);
                 Native.Z3_del_config(cfg);
                 InitContext();
             }
         }

Member Function Documentation

◆ Dispose()

void Dispose ( )

inline

Disposes of the context.

Definition at line 1371 of file NativeContext.cs.

         {
             if (m_ctx != IntPtr.Zero)
             {
                 m_n_err_handler = null;
                 IntPtr ctx = m_ctx;
                 m_ctx = IntPtr.Zero;
                 Native.Z3_del_context(ctx);
             }
             else
                 GC.ReRegisterForFinalize(this);
         }

◆ EnableTrace()

static void EnableTrace ( string tag )

inlinestatic

Enable trace to file

Parameters

tag	Tag to trace

Definition at line 1358 of file NativeContext.cs.

         {
             Debug.Assert(!string.IsNullOrEmpty(tag));
             Native.Z3_enable_trace(tag);
         }

◆ GetAppArgs()

Z3_ast [] GetAppArgs ( Z3_app app )

inline

Get the arguments for app

Parameters

app

Returns

Definition at line 1145 of file NativeContext.cs.

         {
             var numArgs = GetNumArgs(app);
             var args = new Z3_ast[numArgs];
             for (uint i = 0; i < numArgs; i++)
             {
                 args[i] = GetAppArg(app, i);
             }
             return args;
         }

◆ GetAppDecl()

Z3_func_decl GetAppDecl ( Z3_ast ast )

inline

Get App Decl from IntPtr

Definition at line 1173 of file NativeContext.cs.

         {
             Debug.Assert(ast != IntPtr.Zero);
  
             return Native.Z3_get_app_decl(nCtx, ast);
         }

Referenced by NativeModel.TryGetArrayValue().

◆ GetArraySortDomain()

Z3_sort GetArraySortDomain ( Z3_ast array )

inline

Get the domain IntPtr for Sort

Definition at line 1206 of file NativeContext.cs.

         {
             Debug.Assert(array != IntPtr.Zero);
  
             return Native.Z3_get_array_sort_domain(nCtx, array);
         }

◆ GetArraySortRange()

Z3_sort GetArraySortRange ( Z3_ast array )

inline

Get the range IntPtr for Sort

Definition at line 1216 of file NativeContext.cs.

         {
             Debug.Assert(array != IntPtr.Zero);
  
             return Native.Z3_get_array_sort_range(nCtx, array);
         }

◆ GetAstKind()

Z3_ast_kind GetAstKind ( Z3_ast ast )

inline

Get the AST kind from IntPtr

Definition at line 1113 of file NativeContext.cs.

         {
             Debug.Assert(ast != IntPtr.Zero);
  
             return (Z3_ast_kind)Native.Z3_get_ast_kind(nCtx, ast);
         }

Referenced by NativeModel.TryGetArrayValue().

◆ GetBvSortSize()

uint GetBvSortSize ( Z3_sort bvSort )

inline

Get size of BitVector Sort

Definition at line 1196 of file NativeContext.cs.

         {
             Debug.Assert(bvSort != IntPtr.Zero);
  
             return Native.Z3_get_bv_sort_size(nCtx, bvSort);
         }

◆ GetDeclKind()

Z3_decl_kind GetDeclKind ( Z3_func_decl decl )

inline

Get the Decl kind from IntPtr

Definition at line 1123 of file NativeContext.cs.

         {
             Debug.Assert(decl != IntPtr.Zero);
  
             return (Z3_decl_kind)Native.Z3_get_decl_kind(nCtx, decl);
         }

Referenced by NativeModel.TryGetArrayValue().

◆ GetDeclName()

string GetDeclName ( Z3_func_decl decl )

inline

Get string name for Decl

Parameters

decl

Returns

Definition at line 1185 of file NativeContext.cs.

         {
             Debug.Assert(decl != IntPtr.Zero);
  
             var namePtr = Native.Z3_get_decl_name(nCtx, decl);
             return Marshal.PtrToStringAnsi(namePtr);
         }

◆ GetDomain()

Z3_sort [] GetDomain ( Z3_func_decl fdecl )

inline

Get domain for a funcdecl

Parameters

fdecl

Returns

Definition at line 1045 of file NativeContext.cs.

         {
             Debug.Assert(fdecl != IntPtr.Zero);
  
             var sz = Native.Z3_get_domain_size(nCtx, fdecl);
             var domain = new Z3_sort[sz];
             for (uint i = 0; i < sz; i++)
             {
                 domain[i] = Native.Z3_get_domain(nCtx, fdecl, i);
             }
             return domain;
         }

◆ GetNumArgs()

uint GetNumArgs ( Z3_app app )

inline

Return number of arguments for app

Parameters

app

Returns

Definition at line 1161 of file NativeContext.cs.

         {
             Debug.Assert(app != IntPtr.Zero);
  
             return Native.Z3_get_app_num_args(nCtx, app);
         }

Referenced by NativeContext.GetAppArgs(), and NativeModel.TryGetArrayValue().

◆ GetNumeralString()

string GetNumeralString ( Z3_ast v )

inline

Get string for numeral ast

Parameters

v

Returns

Definition at line 1304 of file NativeContext.cs.

         {
             Debug.Assert(v != IntPtr.Zero);
             return Native.Z3_get_numeral_string(nCtx, v);
         }

◆ GetRange()

Z3_sort GetRange ( Z3_func_decl fdecl )

inline

Get range for a funcdecl

Parameters

fdecl

Returns

Definition at line 1063 of file NativeContext.cs.

         {
             Debug.Assert(fdecl != IntPtr.Zero);
  
             return Native.Z3_get_range(nCtx, fdecl);
         }

◆ GetSort()

Z3_sort GetSort ( Z3_ast ast )

inline

Get Sort for AST

Definition at line 1133 of file NativeContext.cs.

         {
             Debug.Assert(ast != IntPtr.Zero);
  
             return Native.Z3_get_sort(nCtx, ast);
         }

◆ GetSortKind()

Z3_sort_kind GetSortKind ( Z3_sort sort )

inline

Get the sort kind from IntPtr

Definition at line 1103 of file NativeContext.cs.

         {
             Debug.Assert(sort != IntPtr.Zero);
  
             return (Z3_sort_kind)Native.Z3_get_sort_kind(nCtx, sort);
         }

◆ GetStatistics()

Statistics.Entry [] GetStatistics ( Z3_stats stats )

inline

Retrieve statistics as an array of entries

Parameters

stats

Returns

Definition at line 1407 of file NativeContext.cs.

         {
             Native.Z3_stats_inc_ref(nCtx, stats);
             var result = Statistics.NativeEntries(nCtx, stats);
             Native.Z3_stats_dec_ref(nCtx, stats);
             return result;
         }

◆ MkAdd()

Z3_ast MkAdd ( params Z3_ast[] t )

inline

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

Definition at line 83 of file NativeContext.cs.

         {
             Debug.Assert(t != null);
             Debug.Assert(t.All(a => a != IntPtr.Zero));
  
             return Native.Z3_mk_add(nCtx, (uint)(t?.Length ?? 0), t);
         }

◆ MkAnd()

Z3_ast MkAnd ( params Z3_ast[] t )

inline

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

Definition at line 221 of file NativeContext.cs.

         {
             Debug.Assert(t != null);
             Debug.Assert(t.All(a => a != IntPtr.Zero));
  
             return Native.Z3_mk_and(nCtx, (uint)(t?.Length ?? 0), t);
         }

◆ MkApp()

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

inline

Create a new function application.

Definition at line 466 of file NativeContext.cs.

         {
             Debug.Assert(f != IntPtr.Zero);
             Debug.Assert(args == null || args.All(a => a != IntPtr.Zero));
  
             return Native.Z3_mk_app(nCtx, f, (uint)(args?.Length ?? 0), args);
         }

Referenced by NativeSolver.AssertInjective().

◆ MkArraySort()

Z3_sort MkArraySort	(	Z3_sort	domain,
		Z3_sort	range
	)

inline

Create a new array sort.

Definition at line 381 of file NativeContext.cs.

         {
             Debug.Assert(domain != IntPtr.Zero);
             Debug.Assert(range != IntPtr.Zero);
  
             return Native.Z3_mk_array_sort(nCtx, domain, range);
         }

◆ MkBool()

Z3_ast MkBool ( bool value )

Creates a Boolean value.

◆ MkBound()

Z3_ast MkBound	(	uint	index,
		Z3_sort	sort
	)

inline

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.

         {
             Debug.Assert(sort != IntPtr.Zero);
  
             return Native.Z3_mk_bound(nCtx, index, sort);
         }

Referenced by NativeSolver.AssertInjective().

◆ MkBvAdd()

Z3_ast_vector MkBvAdd	(	Z3_ast_vector	t1,
		Z3_ast_vector	t2
	)

inline

Two's complement addition.

The arguments must have the same bit-vector sort.

Definition at line 540 of file NativeContext.cs.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_bvadd(nCtx, t1, t2);
         }

◆ MkBvAnd()

Z3_ast_vector MkBvAnd	(	Z3_ast_vector	t1,
		Z3_ast_vector	t2
	)

inline

Bitwise conjunction.

The arguments must have a bit-vector sort.

Definition at line 495 of file NativeContext.cs.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_bvand(nCtx, t1, t2);
         }

◆ MkBvAshr()

Z3_ast_vector MkBvAshr	(	Z3_ast_vector	t1,
		Z3_ast_vector	t2
	)

inline

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.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_bvashr(nCtx, t1, t2);
         }

◆ MkBvExtract()

Z3_ast_vector MkBvExtract	(	uint	high,
		uint	low,
		Z3_ast_vector	t
	)

inline

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.

         {
             Debug.Assert(t != IntPtr.Zero);
  
             return Native.Z3_mk_extract(nCtx, high, low, t);
         }

◆ MkBvLshr()

Z3_ast_vector MkBvLshr	(	Z3_ast_vector	t1,
		Z3_ast_vector	t2
	)

inline

Logical shift right

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

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 627 of file NativeContext.cs.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_bvlshr(nCtx, t1, t2);
         }

◆ MkBvMul()

Z3_ast_vector MkBvMul	(	Z3_ast_vector	t1,
		Z3_ast_vector	t2
	)

inline

Two's complement multiplication.

The arguments must have the same bit-vector sort.

Definition at line 675 of file NativeContext.cs.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_bvmul(nCtx, t1, t2);
         }

◆ MkBvNeg()

Z3_ast_vector MkBvNeg ( Z3_ast_vector t )

inline

Standard two's complement unary minus.

The arguments must have a bit-vector sort.

Definition at line 518 of file NativeContext.cs.

         {
             Debug.Assert(t != IntPtr.Zero);
  
             return Native.Z3_mk_bvneg(nCtx, t);
         }

◆ MkBVNeg()

Z3_ast_vector MkBVNeg ( Z3_ast_vector t )

inline

Standard two's complement unary minus.

The arguments must have a bit-vector sort.

Definition at line 529 of file NativeContext.cs.

         {
             Debug.Assert(t != IntPtr.Zero);
  
             return Native.Z3_mk_bvneg(nCtx, t);
         }

◆ MkBvNot()

Z3_ast_vector MkBvNot ( Z3_ast_vector t )

inline

Bitwise negation.

The argument must have a bit-vector sort.

Definition at line 507 of file NativeContext.cs.

         {
             Debug.Assert(t != IntPtr.Zero);
  
             return Native.Z3_mk_bvnot(nCtx, t);
         }

◆ MkBvOr()

Z3_ast_vector MkBvOr	(	Z3_ast_vector	t1,
		Z3_ast_vector	t2
	)

inline

Bitwise disjunction.

The arguments must have a bit-vector sort.

Definition at line 771 of file NativeContext.cs.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_bvor(nCtx, t1, t2);
         }

◆ MkBvSdiv()

Z3_ast_vector MkBvSdiv	(	Z3_ast_vector	t1,
		Z3_ast_vector	t2
	)

inline

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.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_bvsdiv(nCtx, t1, t2);
         }

◆ MkBvShl()

Z3_ast_vector MkBvShl	(	Z3_ast_vector	t1,
		Z3_ast_vector	t2
	)

inline

Shift left.

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

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 607 of file NativeContext.cs.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_bvshl(nCtx, t1, t2);
         }

◆ MkBvSignExt()

Z3_ast_vector MkBvSignExt	(	uint	i,
		Z3_ast_vector	t
	)

inline

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.

         {
             Debug.Assert(t != IntPtr.Zero);
  
             return Native.Z3_mk_sign_ext(nCtx, i, t);
         }

◆ MkBvSlt()

Z3_ast MkBvSlt	(	Z3_ast_vector	t1,
		Z3_ast_vector	t2
	)

inline

Two's complement signed less-than

The arguments must have the same bit-vector sort.

Definition at line 663 of file NativeContext.cs.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_bvslt(nCtx, t1, t2);
         }

◆ MkBvSort()

Z3_sort MkBvSort ( uint size )

Returns the BvSort for size in this NativeContext

◆ MkBvSrem()

Z3_ast_vector MkBvSrem	(	Z3_ast_vector	t1,
		Z3_ast_vector	t2
	)

inline

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.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_bvsrem(nCtx, t1, t2);
         }

◆ MkBvSub()

Z3_ast_vector MkBvSub	(	Z3_ast_vector	t1,
		Z3_ast_vector	t2
	)

inline

Two's complement subtraction.

The arguments must have the same bit-vector sort.

Definition at line 759 of file NativeContext.cs.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_bvsub(nCtx, t1, t2);
         }

◆ MkBvUdiv()

Z3_ast_vector MkBvUdiv	(	Z3_ast_vector	t1,
		Z3_ast_vector	t2
	)

inline

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.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_bvudiv(nCtx, t1, t2);
         }

◆ MkBvUle()

Z3_ast MkBvUle	(	Z3_ast	t1,
		Z3_ast	t2
	)

inline

Unsigned less-than-equal

The arguments must have the same bit-vector sort.

Definition at line 189 of file NativeContext.cs.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_bvule(nCtx, t1, t2);
         }

◆ MkBvUlt()

Z3_ast MkBvUlt	(	Z3_ast	t1,
		Z3_ast	t2
	)

inline

Unsigned less-than

The arguments must have the same bit-vector sort.

Definition at line 175 of file NativeContext.cs.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_bvult(nCtx, t1, t2);
         }

◆ MkBvUrem()

Z3_ast_vector MkBvUrem	(	Z3_ast_vector	t1,
		Z3_ast_vector	t2
	)

inline

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.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_bvurem(nCtx, t1, t2);
         }

◆ MkBvXor()

Z3_ast_vector MkBvXor	(	Z3_ast_vector	t1,
		Z3_ast_vector	t2
	)

inline

Bitwise XOR.

The arguments must have a bit-vector sort.

Definition at line 783 of file NativeContext.cs.

         {
             Debug.Assert(t1 != null);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_bvxor(nCtx, t1, t2);
         }

◆ MkBvZeroExt()

Z3_ast_vector MkBvZeroExt	(	uint	i,
		Z3_ast_vector	t
	)

inline

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.

         {
             Debug.Assert(t != IntPtr.Zero);
  
             return Native.Z3_mk_zero_ext(nCtx, i, t);
         }

◆ MkConst()

Z3_ast MkConst	(	string	name,
		Z3_sort	range
	)

inline

Creates a new Constant of sort range and named name .

Definition at line 438 of file NativeContext.cs.

         {
             Debug.Assert(!string.IsNullOrEmpty(name));
             Debug.Assert(range != IntPtr.Zero);
  
             return Native.Z3_mk_const(nCtx, MkStringSymbol(name), range);
         }

◆ MkConstArray()

Z3_ast MkConstArray	(	Z3_sort	domain,
		Z3_ast	v
	)

inline

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.

         {
             Debug.Assert(domain != IntPtr.Zero);
             Debug.Assert(v != IntPtr.Zero);
  
             return Native.Z3_mk_const_array(nCtx, domain, v);
         }

◆ MkConstDecl()

Z3_func_decl MkConstDecl	(	string	name,
		Z3_sort	range
	)

inline

Creates a new constant function declaration.

Definition at line 1032 of file NativeContext.cs.

         {
             Debug.Assert(range != IntPtr.Zero);
  
             var symbol = Native.Z3_mk_string_symbol(nCtx, name);
             return Native.Z3_mk_func_decl(nCtx, symbol, 0, new IntPtr[0], range);
         }

◆ MkDefault()

Z3_ast MkDefault ( Z3_ast a )

inline

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.

         {
             Debug.Assert(a != null);
  
             return Native.Z3_mk_array_default(nCtx, a);
         }

◆ MkDiv()

Z3_ast MkDiv	(	Z3_ast	t1,
		Z3_ast	t2
	)

inline

Create an expression representing t1 / t2.

Definition at line 117 of file NativeContext.cs.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_div(nCtx, t1, t2);
         }

◆ MkEq()

Z3_ast MkEq	(	Z3_ast	x,
		Z3_ast	y
	)

inline

Creates the equality x = y .

Definition at line 200 of file NativeContext.cs.

         {
             Debug.Assert(x != IntPtr.Zero);
             Debug.Assert(y != IntPtr.Zero);
  
             return Native.Z3_mk_eq(nCtx, x, y);
         }

Referenced by NativeSolver.AssertInjective().

◆ MkExists()

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`
	)

inline

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.

         {
             return MkQuantifier(false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
         }

◆ MkFalse()

Z3_ast MkFalse ( )

The false Term.

◆ MkForall()

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`
	)

inline

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.

         {
             return MkQuantifier(true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
         }

Referenced by NativeSolver.AssertInjective().

◆ MkFreshFuncDecl()

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

inline

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

Definition at line 1020 of file NativeContext.cs.

         {
             Debug.Assert(domain != null);
             Debug.Assert(range != IntPtr.Zero);
             Debug.Assert(domain.All(d => d != IntPtr.Zero));
  
             return Native.Z3_mk_fresh_func_decl(nCtx, prefix, (uint)(domain?.Length ?? 0), domain, range);
         }

Referenced by NativeSolver.AssertInjective().

◆ MkFuncDecl() [1/2]

Z3_func_decl MkFuncDecl	(	string	name,
		Z3_sort	domain,
		Z3_sort	range
	)

inline

Creates a new function declaration.

Definition at line 1006 of file NativeContext.cs.

         {
             Debug.Assert(!string.IsNullOrEmpty(name));
             Debug.Assert(range != IntPtr.Zero);
             Debug.Assert(domain != IntPtr.Zero);
  
             var symbol = Native.Z3_mk_string_symbol(nCtx, name);
             var q = new Z3_sort[] { domain };
             return Native.Z3_mk_func_decl(nCtx, symbol, (uint)q.Length, q, range);
         }

◆ MkFuncDecl() [2/2]

Z3_func_decl MkFuncDecl	(	string	name,
		Z3_sort[]	domain,
		Z3_sort	range
	)

inline

Creates a new function declaration.

Definition at line 992 of file NativeContext.cs.

         {
             Debug.Assert(!string.IsNullOrEmpty(name));
             Debug.Assert(range != IntPtr.Zero);
             Debug.Assert(domain != null);
             Debug.Assert(domain.All(d => d != IntPtr.Zero));
  
             var symbol = Native.Z3_mk_string_symbol(nCtx, name);
             return Native.Z3_mk_func_decl(nCtx, symbol, (uint)(domain?.Length ?? 0), domain, range);
         }

◆ MkGe()

Z3_ast MkGe	(	Z3_ast	t1,
		Z3_ast	t2
	)

inline

Create an expression representing t1 >= t2

Definition at line 150 of file NativeContext.cs.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_ge(nCtx, t1, t2);
         }

◆ MkGt()

Z3_ast MkGt	(	Z3_ast	t1,
		Z3_ast	t2
	)

inline

Create an expression representing t1 > t2

Definition at line 161 of file NativeContext.cs.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_gt(nCtx, t1, t2);
         }

◆ MkIff()

Z3_ast MkIff	(	Z3_ast	t1,
		Z3_ast	t2
	)

inline

Create an expression representing t1 iff t2.

Definition at line 425 of file NativeContext.cs.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_iff(nCtx, t1, t2);
         }

◆ MkImplies()

Z3_ast MkImplies	(	Z3_ast	t1,
		Z3_ast	t2
	)

inline

Create an expression representing t1 -> t2.

Definition at line 306 of file NativeContext.cs.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_implies(nCtx, t1, t2);
         }

◆ MkIte()

Z3_ast MkIte	(	Z3_ast	t1,
		Z3_ast	t2,
		Z3_ast	t3
	)

inline

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.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
             Debug.Assert(t3 != IntPtr.Zero);
  
             return Native.Z3_mk_ite(nCtx, t1, t2, t3);
         }

◆ MkLe()

Z3_ast MkLe	(	Z3_ast	t1,
		Z3_ast	t2
	)

inline

Create an expression representing t1 <= t2

Definition at line 128 of file NativeContext.cs.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_le(nCtx, t1, t2);
         }

◆ MkListSort()

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
	)

inline

returns ListSort

Parameters

name
elemSort
inil
iisnil
icons
iiscons
ihead
itail

Returns: The list algebraic datatype

Definition at line 352 of file NativeContext.cs.

         {
             Debug.Assert(!string.IsNullOrEmpty(name));
             Debug.Assert(elemSort != IntPtr.Zero);
  
             IntPtr nil = IntPtr.Zero, isnil = IntPtr.Zero,
                    cons = IntPtr.Zero, iscons = IntPtr.Zero,
                    head = IntPtr.Zero, tail = IntPtr.Zero;
  
             var symbol = Native.Z3_mk_string_symbol(nCtx, name);
             var sort = Native.Z3_mk_list_sort(nCtx, symbol, elemSort,
                                   ref nil, ref isnil, ref cons, ref iscons, ref head, ref tail);
  
             inil = nil;
             iisnil = isnil;
             icons = cons;
             iiscons = iscons;
             ihead = head;
             itail = tail;
  
             return sort;
         }

◆ MkLt()

Z3_ast MkLt	(	Z3_ast	t1,
		Z3_ast	t2
	)

inline

Create an expression representing t1 < t2

Definition at line 139 of file NativeContext.cs.

         {
             Debug.Assert(t1 != IntPtr.Zero);
             Debug.Assert(t2 != IntPtr.Zero);
  
             return Native.Z3_mk_lt(nCtx, t1, t2);
         }

◆ MkMul()

Z3_ast MkMul ( params Z3_ast[] t )

inline

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

Definition at line 94 of file NativeContext.cs.

         {
             Debug.Assert(t != null);
             Debug.Assert(t.All(a => a != IntPtr.Zero));
  
             var ts = t.ToArray();
             return Native.Z3_mk_mul(nCtx, (uint)(ts?.Length ?? 0), ts);
         }

◆ MkNot()

Z3_ast MkNot ( Z3_ast a )

inline

Mk an expression representing not(a).

Definition at line 211 of file NativeContext.cs.

         {
             Debug.Assert(a != IntPtr.Zero);
  
             return Native.Z3_mk_not(nCtx, a);
         }

◆ MkNumeral() [1/3]

Z3_ast MkNumeral	(	int	v,
		Z3_sort	sort
	)

inline

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.

         {
             Debug.Assert(sort != IntPtr.Zero);
  
             return Native.Z3_mk_int(nCtx, v, sort);
         }

◆ MkNumeral() [2/3]

Z3_ast MkNumeral	(	long	v,
		Z3_sort	sort
	)

inline

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.

         {
             Debug.Assert(sort != null);
  
             return Native.Z3_mk_int64(nCtx, v, sort);
         }

◆ MkNumeral() [3/3]

Z3_ast MkNumeral	(	uint	v,
		Z3_sort	sort
	)

inline

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.

         {
             Debug.Assert(sort != null);
  
             return Native.Z3_mk_unsigned_int(nCtx, v, sort);
         }

◆ MkOr()

Z3_ast MkOr ( params Z3_ast[] t )

inline

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

Definition at line 232 of file NativeContext.cs.

         {
             Debug.Assert(t != null);
             Debug.Assert(t.All(a => a != IntPtr.Zero));
  
             return Native.Z3_mk_or(nCtx, (uint)(t?.Length ?? 0), t);
         }

◆ MkPattern()

Z3_pattern MkPattern ( params Z3_ast[] terms )

inline

Create a quantifier pattern.

Definition at line 1076 of file NativeContext.cs.

         {
             Debug.Assert(terms != null);
             if (terms == null || terms.Length == 0)
                 throw new Z3Exception("Cannot create a pattern from zero terms");
  
             return Native.Z3_mk_pattern(nCtx, (uint)terms.Length, terms);
         }

◆ MkReal()

Z3_ast MkReal ( string v )

inline

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.

         {
             Debug.Assert(!string.IsNullOrEmpty(v));
             return Native.Z3_mk_numeral(nCtx, v, RealSort);
         }

◆ MkSelect()

Z3_ast MkSelect	(	Z3_ast	array,
		Z3_ast	index
	)

inline

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.

         {
             Debug.Assert(array != IntPtr.Zero);
             Debug.Assert(index != IntPtr.Zero);
  
             return Native.Z3_mk_select(nCtx, array, index);
         }

◆ MkSimpleSolver()

NativeSolver MkSimpleSolver ( )

inline

Creates a new (incremental) solver.

Definition at line 1091 of file NativeContext.cs.

         {
             Z3_solver nSolver = Native.Z3_mk_simple_solver(nCtx);
             return new NativeSolver(this, nSolver);
         }

◆ MkStore()

Z3_ast MkStore	(	Z3_ast	a,
		Z3_ast	i,
		Z3_ast	v
	)

inline

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.

         {
             Debug.Assert(a != IntPtr.Zero);
             Debug.Assert(i != IntPtr.Zero);
             Debug.Assert(v != IntPtr.Zero);
  
             return Native.Z3_mk_store(nCtx, a, i, v);
         }

◆ MkStringSymbol()

Z3_symbol MkStringSymbol ( string name )

inline

Return a ptr to symbol for string

Parameters

name

Returns

Definition at line 454 of file NativeContext.cs.

         {
             Debug.Assert(!string.IsNullOrEmpty(name));
  
             return Native.Z3_mk_string_symbol(nCtx, name);
         }

Referenced by NativeContext.MkConst().

◆ MkSub()

Z3_ast MkSub ( params Z3_ast[] t )

inline

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

Definition at line 106 of file NativeContext.cs.

         {
             Debug.Assert(t != null);
             Debug.Assert(t.All(a => a != IntPtr.Zero));
             var ts = t.ToArray();
             return Native.Z3_mk_sub(nCtx, (uint)(ts?.Length ?? 0), ts);
         }

◆ MkTrue()

Z3_ast MkTrue ( )

The true Term.

◆ MkTupleSort()

Z3_sort MkTupleSort	(	Z3_symbol	name,
		Z3_symbol[]	fieldNames,
		Z3_sort[]	fieldSorts,
		out Z3_func_decl	constructor,
		Z3_func_decl[]	projections
	)

inline

Create a new tuple sort.

Definition at line 392 of file NativeContext.cs.

         {
             Debug.Assert(name != IntPtr.Zero);
             Debug.Assert(fieldNames != null);
             Debug.Assert(fieldNames.All(fn => fn != IntPtr.Zero));
             Debug.Assert(fieldSorts == null || fieldSorts.All(fs => fs != IntPtr.Zero));
  
             var numFields = (uint)(fieldNames?.Length ?? 0);
             constructor = IntPtr.Zero;
             return Native.Z3_mk_tuple_sort(nCtx, name, numFields, fieldNames, fieldSorts, ref constructor, projections);
         }

◆ ToArray()

Z3_ast [] ToArray ( Z3_ast_vector vec )

inline

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

Parameters

vec

Returns

Definition at line 1391 of file NativeContext.cs.

         {
             Native.Z3_ast_vector_inc_ref(nCtx, vec);
             var sz = Native.Z3_ast_vector_size(nCtx, vec);
             var result = new Z3_ast[sz];
             for (uint i = 0; i < sz; ++i)
                 result[i] = Native.Z3_ast_vector_get(nCtx, vec, i);
             Native.Z3_ast_vector_dec_ref(nCtx, vec);
             return result;
         }

◆ ToggleWarningMessages()

void ToggleWarningMessages ( bool turnOn )

Enable or disable warning messages

Parameters

turnOn

◆ ToString()

string ToString ( Z3_ast ast )

inline

Get printable string representing Z3_ast

Parameters

ast

Returns

Definition at line 1315 of file NativeContext.cs.

         {
             Debug.Assert(ast != IntPtr.Zero);
  
             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

v
i

Returns

Definition at line 1229 of file NativeContext.cs.

         {
             Debug.Assert(v != IntPtr.Zero);
  
             int result = i = 0;
             if (Native.Z3_get_numeral_int(nCtx, v, ref result) == 0) 
             {
                 return false;
             }
             i = result;
             return true;
         }

◆ TryGetNumeralInt64()

bool TryGetNumeralInt64	(	Z3_ast	v,
		out long	i
	)

inline

Try to get long from AST

Parameters

v
i

Returns

Definition at line 1267 of file NativeContext.cs.

         {
             Debug.Assert(v != IntPtr.Zero);
  
             long result = i = 0;
             if (Native.Z3_get_numeral_int64(nCtx, v, ref result) == 0)
             {
                 return false;
             }
             i = result;
             return true;
         }

◆ TryGetNumeralUInt()

bool TryGetNumeralUInt	(	Z3_ast	v,
		out uint	u
	)

inline

Try to get uint from AST

Parameters

v
u

Returns

Definition at line 1248 of file NativeContext.cs.

         {
             Debug.Assert(v != IntPtr.Zero);
  
             uint result = u = 0;
             if (Native.Z3_get_numeral_uint(nCtx, v, ref result) == 0)
             {
                 return false;
             }
             u = result;
             return true;
         }

◆ TryGetNumeralUInt64()

bool TryGetNumeralUInt64	(	Z3_ast	v,
		out ulong	u
	)

inline

Try get ulong from AST

Parameters

v
u

Returns

Definition at line 1286 of file NativeContext.cs.

         {
             Debug.Assert(v != IntPtr.Zero);
  
             ulong result = u = 0;
             if (Native.Z3_get_numeral_uint64(nCtx, v, ref result) == 0)
             {
                 return false;
             }
             u = result;
             return true;
         }

Property Documentation

◆ BoolSort

Z3_sort BoolSort

get

Returns the "singleton" BoolSort for this NativeContext

Definition at line 326 of file NativeContext.cs.

◆ IntSort

Z3_sort IntSort

get

Integer Sort

Definition at line 321 of file NativeContext.cs.

◆ PrintMode

Z3_ast_print_mode PrintMode

set

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.

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

◆ RealSort

Z3_sort RealSort

get

Returns the "singleton" RealSort for this NativeContext

Definition at line 331 of file NativeContext.cs.

Public Member Functions

Static Public Member Functions

Properties

Detailed Description

Constructor & Destructor Documentation

◆ NativeContext()

Member Function Documentation

◆ Dispose()

◆ EnableTrace()

◆ GetAppArgs()

◆ GetAppDecl()

◆ GetArraySortDomain()

◆ GetArraySortRange()

◆ GetAstKind()

◆ GetBvSortSize()

◆ GetDeclKind()

◆ GetDeclName()

◆ GetDomain()

◆ GetNumArgs()

◆ GetNumeralString()

◆ GetRange()

◆ GetSort()

◆ GetSortKind()

◆ GetStatistics()

◆ MkAdd()

◆ MkAnd()

◆ MkApp()

◆ MkArraySort()

◆ MkBool()

◆ MkBound()

◆ MkBvAdd()

◆ MkBvAnd()

◆ MkBvAshr()

◆ MkBvExtract()

◆ MkBvLshr()

◆ MkBvMul()

◆ MkBvNeg()

◆ MkBVNeg()

◆ MkBvNot()

◆ MkBvOr()

◆ MkBvSdiv()

◆ MkBvShl()

◆ MkBvSignExt()

◆ MkBvSlt()

◆ MkBvSort()

◆ MkBvSrem()

◆ MkBvSub()

◆ MkBvUdiv()

◆ MkBvUle()

◆ MkBvUlt()

◆ MkBvUrem()

◆ MkBvXor()

◆ MkBvZeroExt()

◆ MkConst()

◆ MkConstArray()

◆ MkConstDecl()

◆ MkDefault()

◆ MkDiv()

◆ MkEq()

◆ MkExists()

◆ MkFalse()

◆ MkForall()

◆ MkFreshFuncDecl()

◆ MkFuncDecl() [1/2]

◆ MkFuncDecl() [2/2]

◆ MkGe()

◆ MkGt()

◆ MkIff()

◆ MkImplies()

◆ MkIte()

◆ MkLe()

◆ MkListSort()

◆ MkLt()

◆ MkMul()

◆ MkNot()

◆ MkNumeral() [1/3]

◆ MkNumeral() [2/3]

◆ MkNumeral() [3/3]

◆ MkOr()

◆ MkPattern()