Inheritance diagram for NativeSolver:

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

Properties
string	Help `[get]`
	A string that describes all available solver parameters. More...

uint	NumScopes `[get]`
	The current number of backtracking points (scopes). More...

uint	NumAssertions `[get]`
	The number of assertions in the solver. More...

Z3_ast[]	Assertions `[get]`
	The set of asserted formulas. More...

Z3_ast[]	Units `[get]`
	Currently inferred units. More...

NativeModel?	Model `[get]`
	The model of the last `Check(params Expr[] assumptions)`. More...

Z3_ast	Proof `[get]`
	The proof of the last `Check(params Expr[] assumptions)`. More...

Z3_ast[]	UnsatCore `[get]`
	The unsat core of the last `Check`. More...

string	ReasonUnknown `[get]`
	A brief justification of why the last call to `Check` returned `UNKNOWN`. More...

Statistics.Entry[]	Statistics `[get]`
	Solver statistics. More...

Detailed Description

Solvers.

Definition at line 40 of file NativeSolver.cs.

Member Function Documentation

◆ Add() [1/2]

void Add ( IEnumerable< Z3_ast > constraints )

Alias for Assert.

◆ Add() [2/2]

void Add ( params Z3_ast[] constraints )

Alias for Assert.

◆ Assert()

void Assert ( params Z3_ast[] constraints )

inline

Assert a constraint (or multiple) into the solver.

Definition at line 153 of file NativeSolver.cs.

         {
             Debug.Assert(constraints != null);
             Debug.Assert(constraints.All(c => c != IntPtr.Zero));
  
             foreach (Z3_ast a in constraints)
             {
                 Native.Z3_solver_assert(nCtx, z3solver, a);
             }
         }

Referenced by NativeSolver.AssertInjective(), and NativeSolver.Translate().

◆ AssertAndTrack() [1/2]

void AssertAndTrack	(	Z3_ast	constraint,
		Z3_ast	p
	)

inline

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.

         {
             Debug.Assert(constraint != null);
             Debug.Assert(p != null);
  
             Native.Z3_solver_assert_and_track(nCtx, z3solver, constraint, p);
         }

◆ AssertAndTrack() [2/2]

void AssertAndTrack	(	Z3_ast[]	constraints,
		Z3_ast[]	ps
	)

inline

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

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 219 of file NativeSolver.cs.

         {
             Debug.Assert(constraints != null);
             Debug.Assert(constraints.All(c => c != IntPtr.Zero));
             Debug.Assert(ps.All(c => c != IntPtr.Zero));
             if (constraints.Length != ps.Length)
                 throw new Z3Exception("Argument size mismatch");
  
             for (int i = 0; i < constraints.Length; i++)
                 Native.Z3_solver_assert_and_track(nCtx, z3solver, constraints[i], ps[i]);
         }

◆ AssertInjective()

void AssertInjective ( Z3_func_decl f )

inline

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

f

Definition at line 183 of file NativeSolver.cs.

         {
             uint arity = Native.Z3_get_arity(nCtx, f);
             Z3_sort range = Native.Z3_get_range(nCtx, f);
             Z3_ast[] vars = new Z3_ast[arity];
             Z3_sort[] sorts = new Z3_sort[arity];
             Z3_symbol[] names = new Z3_symbol[arity];
             for (uint i = 0; i < arity; ++i)
             {
                 Z3_sort domain = Native.Z3_get_domain(nCtx, f, i);
                 vars[i] = ntvContext.MkBound(arity - i - 1, domain);
                 sorts[i] = domain;
                 names[i] = Native.Z3_mk_int_symbol(nCtx, (int)i);
             }
             Z3_ast app_f = IntPtr.Zero; // Context.MkApp(f, vars);
             for (uint i = 0; i < arity; ++i)
             {
                 Z3_sort domain = Native.Z3_get_domain(nCtx, f, i);
                 Z3_func_decl proj = ntvContext.MkFreshFuncDecl("inv", new Z3_sort[] { range }, domain);
                 Z3_ast body = ntvContext.MkEq(vars[i], ntvContext.MkApp(proj, app_f));
                 Z3_ast q = ntvContext.MkForall(names, sorts, body);
                 Assert(q);
             }
         }

◆ Check() [1/2]

Status Check ( IEnumerable< Z3_ast > assumptions )

inline

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

See also: Model, UnsatCore, Proof

Definition at line 306 of file NativeSolver.cs.

         {
             Z3_lbool r;
             Z3_ast[] asms = assumptions.ToArray();
             if (asms.Length == 0)
                 r = (Z3_lbool)Native.Z3_solver_check(nCtx, z3solver);
             else
                 r = (Z3_lbool)Native.Z3_solver_check_assumptions(nCtx, z3solver, (uint)asms.Length, asms);
             return lboolToStatus(r);
         }

◆ Check() [2/2]

Status Check ( params Z3_ast[] assumptions )

inline

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

See also: Model, UnsatCore, Proof

Definition at line 288 of file NativeSolver.cs.

         {
             Z3_lbool r;
             if (assumptions == null || assumptions.Length == 0)
                 r = (Z3_lbool)Native.Z3_solver_check(nCtx, z3solver);
             else
                 r = (Z3_lbool)Native.Z3_solver_check_assumptions(nCtx, z3solver, (uint)assumptions.Length, assumptions);
             return lboolToStatus(r);
         }

◆ Dispose()

void Dispose ( )

inline

Disposes of the underlying native Z3 object.

Definition at line 428 of file NativeSolver.cs.

         {
             if (z3solver != IntPtr.Zero)
             {
                 Native.Z3_solver_dec_ref(nCtx, z3solver);
                 z3solver = IntPtr.Zero;
             }
             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()

void ImportModelConverter ( NativeSolver src )

inline

Import model converter from other solver.

Definition at line 374 of file NativeSolver.cs.

         {
             Debug.Assert(src != null);
  
             Native.Z3_solver_import_model_converter(nCtx, src.z3solver, z3solver);
         }

◆ Pop()

void Pop ( uint n = 1 )

Backtracks n backtracking points.

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

See also: Push

◆ Push()

void Push ( )

Creates a backtracking point.

See also: Pop

◆ Reset()

void 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.

         {
             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.

         {
             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.

         {
             var value_sym = Native.Z3_mk_string_symbol(nCtx, value);
             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.

         {
             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.

         {
             return Native.Z3_solver_to_string(nCtx, z3solver);
         }

◆ Translate()

NativeSolver Translate ( NativeContext ctx )

inline

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

Definition at line 365 of file NativeSolver.cs.

         {
             Debug.Assert(ctx != null);
             return new NativeSolver(ctx, Native.Z3_solver_translate(nCtx, z3solver, ctx.nCtx));
         }

Property Documentation

◆ Assertions

Z3_ast [] Assertions

get

The set of asserted formulas.

Definition at line 271 of file NativeSolver.cs.

◆ Help

string Help

get

A string that describes all available solver parameters.

Definition at line 45 of file NativeSolver.cs.

◆ Model

NativeModel? Model

get

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.

         {
             get
             {
                 IntPtr x = Native.Z3_solver_get_model(nCtx, z3solver);
                 return x == IntPtr.Zero
                     ? null
                     : new NativeModel(ntvContext, x);
             }
         }

◆ NumAssertions

uint NumAssertions

get

The number of assertions in the solver.

Definition at line 265 of file NativeSolver.cs.

◆ NumScopes

uint NumScopes

get

The current number of backtracking points (scopes).

See also: Pop, Push

Definition at line 129 of file NativeSolver.cs.

◆ Proof

Z3_ast Proof

get

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

string ReasonUnknown

get

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

Definition at line 359 of file NativeSolver.cs.

◆ Statistics

Statistics.Entry [] Statistics

get

Solver statistics.

Definition at line 384 of file NativeSolver.cs.

         {
             get
             {
                 var stats = Native.Z3_solver_get_statistics(nCtx, z3solver);
                 return ntvContext.GetStatistics(stats);
             }
         }

◆ Units

Z3_ast [] Units

get

Currently inferred units.

Definition at line 277 of file NativeSolver.cs.

◆ UnsatCore

Z3_ast [] UnsatCore

get

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.

Public Member Functions

Properties

Detailed Description

Member Function Documentation

◆ Add() [1/2]

◆ Add() [2/2]

◆ Assert()

◆ AssertAndTrack() [1/2]

◆ AssertAndTrack() [2/2]

◆ AssertInjective()

◆ Check() [1/2]

◆ Check() [2/2]

◆ Dispose()

◆ FromFile()

◆ FromString()

◆ ImportModelConverter()

◆ Pop()

◆ Push()

◆ Reset()

◆ Set() [1/4]

◆ Set() [2/4]

◆ Set() [3/4]

◆ Set() [4/4]

◆ ToString()

◆ Translate()

Property Documentation

◆ Assertions

◆ Help

◆ Model

◆ NumAssertions

◆ NumScopes

◆ Proof

◆ ReasonUnknown

◆ Statistics

◆ Units

◆ UnsatCore