NativeSolver Class Reference

Solvers. More...

Inheritance diagram for NativeSolver:

Public Member Functions
void	Set (string name, bool value)
	Sets parameter on the solver.
void	Set (string name, uint value)
	Sets parameter on the solver.
void	Set (string name, double value)
	Sets parameter on the solver.
void	Set (string name, string value)
	Sets parameter on the solver.
void	Push ()
	Creates a backtracking point.
void	Pop (uint n=1)
	Backtracks n backtracking points.
void	Reset ()
	Resets the Solver.
void	Assert (params Z3_ast[] constraints)
	Assert a constraint (or multiple) into the solver.
void	Add (params Z3_ast[] constraints)
	Alias for Assert.
void	Add (IEnumerable< Z3_ast > constraints)
	Alias for Assert.
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))
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.
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.
void	FromFile (string file)
	Load solver assertions from a file.
void	FromString (string str)
	Load solver assertions from a string.
Z3_ast	CongruenceRoot (Z3_ast t)
	Retrieve congruence closure root of the term t relative to the current search state. The function primarily works for SimpleSolver. Terms and variables that are eliminated during pre-processing are not visible to the congruence closure.
Z3_ast	CongruenceNext (Z3_ast t)
	Retrieve congruence closure sibling of the term t relative to the current search state. The function primarily works for SimpleSolver. Terms and variables that are eliminated during pre-processing are not visible to the congruence closure.
Z3_ast	CongruenceExplain (Z3_ast a, Z3_ast b)
	Explain congruence of a and b relative to the current search state.
Status	Check (params Z3_ast[] assumptions)
	Checks whether the assertions in the solver are consistent or not.
Status	Check (IEnumerable< Z3_ast > assumptions)
	Checks whether the assertions in the solver are consistent or not.
NativeSolver	Translate (NativeContext ctx)
	Create a clone of the current solver with respect to ctx.
void	ImportModelConverter (NativeSolver src)
	Import model converter from other solver.
override string	ToString ()
	A string representation of the solver.
void	Dispose ()
	Disposes of the underlying native Z3 object.

Properties
string	Help [get]
	A string that describes all available solver parameters.
uint	NumScopes [get]
	The current number of backtracking points (scopes).
uint	NumAssertions [get]
	The number of assertions in the solver.
Z3_ast[]	Assertions [get]
	The set of asserted formulas.
Z3_ast[]	Units [get]
	Currently inferred units.
Z3_ast[]	NonUnits [get]
	Non-unit literals in the solver state.
Z3_ast[]	Trail [get]
	Trail of the solver state after a check() call.
NativeModel	Model [get]
	The model of the last Check(params Expr[] assumptions).
Z3_ast	Proof [get]
	The proof of the last Check(params Expr[] assumptions).
Z3_ast[]	UnsatCore [get]
	The unsat core of the last Check.
string	ReasonUnknown [get]
	A brief justification of why the last call to Check returned UNKNOWN.
Statistics.Entry[]	Statistics [get]
	Solver statistics.

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 350 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 332 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);
        }

CongruenceExplain()

Z3_ast CongruenceExplain ( Z3_ast  a, Z3_ast  b  )

inline

Explain congruence of a and b relative to the current search state.

Definition at line 317 of file NativeSolver.cs.

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

CongruenceNext()

Z3_ast CongruenceNext ( Z3_ast  t )

inline

Retrieve congruence closure sibling of the term t relative to the current search state. The function primarily works for SimpleSolver. Terms and variables that are eliminated during pre-processing are not visible to the congruence closure.

Definition at line 308 of file NativeSolver.cs.

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

CongruenceRoot()

Z3_ast CongruenceRoot ( Z3_ast  t )

inline

Retrieve congruence closure root of the term t relative to the current search state. The function primarily works for SimpleSolver. Terms and variables that are eliminated during pre-processing are not visible to the congruence closure.

Definition at line 297 of file NativeSolver.cs.

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

Dispose()

void Dispose ( )

inline

Disposes of the underlying native Z3 object.

Definition at line 472 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 418 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 440 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 409 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 368 of file NativeSolver.cs.

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

NonUnits

Z3_ast [] NonUnits

get

Non-unit literals in the solver state.

Definition at line 283 of file NativeSolver.cs.

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

ReasonUnknown

string ReasonUnknown

get

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

Definition at line 403 of file NativeSolver.cs.

Statistics

Statistics.Entry [] Statistics

get

Solver statistics.

Definition at line 428 of file NativeSolver.cs.

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

Trail

Z3_ast [] Trail

get

Trail of the solver state after a check() call.

Definition at line 289 of file NativeSolver.cs.

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