Solver Class Reference

Solvers. More...

Inheritance diagram for Solver:

Data Structures
class	DecRefQueue

Public Member Functions
void	Push ()
	Creates a backtracking point.
void	Pop (uint n=1)
	Backtracks n backtracking points.
void	Reset ()
	Resets the Solver.
void	Assert (params BoolExpr[] constraints)
	Assert a constraint (or multiple) into the solver.
Status	Check (params Expr[] assumptions)
	Checks whether the assertions in the solver are consistent or not.
override string	ToString ()
	A string representation of the solver.
Public Member Functions inherited from Z3Object
void	Dispose ()
	Disposes of the underlying native Z3 object.

Properties
string	Help [get]
	A string that describes all available solver parameters.
Params	Parameters [set]
	Sets the solver parameters.
ParamDescrs	ParameterDescriptions [get]
	Retrieves parameter descriptions for solver.
uint	NumScopes [get]
	The current number of backtracking points (scopes).
uint	NumAssertions [get]
	The number of assertions in the solver.
BoolExpr[]	Assertions [get]
	The set of asserted formulas.
Model	Model [get]
	The model of the last Check.
Expr	Proof [get]
	The proof of the last Check.
Expr[]	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	Statistics [get]
	Solver statistics.

Detailed Description

Solvers.

Definition at line 29 of file Solver.cs.

Member Function Documentation

void Assert ( params BoolExpr[]  constraints )

inline

Assert a constraint (or multiple) into the solver.

Definition at line 108 of file Solver.cs.

        {
            Contract.Requires(constraints != null);
            Contract.Requires(Contract.ForAll(constraints, c => c != null));

            Context.CheckContextMatch(constraints);
            foreach (BoolExpr a in constraints)
            {
                Native.Z3_solver_assert(Context.nCtx, NativeObject, a.NativeObject);
            }
        }

Status Check ( params Expr[]  assumptions )

inline

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

See Also

Model, UnsatCore, Proof

Definition at line 158 of file Solver.cs.

        {
            Z3_lbool r;
            if (assumptions == null)
                r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject);
            else
                r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));
            switch (r)
            {
                case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
                case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
                default: return Status.UNKNOWN;
            }
        }

void Pop ( uint  n = 1 )

inline

Backtracks n backtracking points.

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

See Also

Push

Definition at line 91 of file Solver.cs.

        {
            Native.Z3_solver_pop(Context.nCtx, NativeObject, n);
        }

void Push ( )

inline

Creates a backtracking point.

See Also

Pop

Definition at line 81 of file Solver.cs.

        {
            Native.Z3_solver_push(Context.nCtx, NativeObject);
        }

void Reset ( )

inline

Resets the Solver.

This removes all assertions from the solver.

Definition at line 100 of file Solver.cs.

        {
            Native.Z3_solver_reset(Context.nCtx, NativeObject);
        }

override string ToString ( )

inline

A string representation of the solver.

Definition at line 263 of file Solver.cs.

        {
            return Native.Z3_solver_to_string(Context.nCtx, NativeObject);
        }

Property Documentation

BoolExpr [] Assertions

get

The set of asserted formulas.

Definition at line 136 of file Solver.cs.

string Help

get

A string that describes all available solver parameters.

Definition at line 35 of file Solver.cs.

Model Model

get

The model of the last Check.

The result is null if Check was not invoked before, if its results was not SATISFIABLE, or if model production is not enabled.

Definition at line 181 of file Solver.cs.

uint NumAssertions

get

The number of assertions in the solver.

Definition at line 124 of file Solver.cs.

uint NumScopes

get

The current number of backtracking points (scopes).

See Also

Pop, Push

Definition at line 73 of file Solver.cs.

ParamDescrs ParameterDescriptions

get

Retrieves parameter descriptions for solver.

Definition at line 62 of file Solver.cs.

Params Parameters

set

Sets the solver parameters.

Definition at line 48 of file Solver.cs.

Expr Proof

get

The proof of the last Check.

The result is null if Check was not invoked before, if its results was not UNSATISFIABLE, or if proof production is disabled.

Definition at line 200 of file Solver.cs.

string ReasonUnknown

get

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

Definition at line 238 of file Solver.cs.

Statistics Statistics

get

Solver statistics.

Definition at line 251 of file Solver.cs.

Expr [] 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 220 of file Solver.cs.