Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Data Structures | Public Member Functions | Properties
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.
void Add (params BoolExpr[] constraints)
 Alias for Assert.
void AssertAndTrack (BoolExpr[] constraints, BoolExpr[] ps)
 Assert multiple constraints into the solver, and track them (in the unsat) core using the Boolean constants in ps.
void AssertAndTrack (BoolExpr constraint, BoolExpr p)
 Assert a constraint into the solver, and track it (in the unsat) core using the Boolean constant p.
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.

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 Add ( params BoolExpr[]  constraints) [inline]

Alias for Assert.

Definition at line 123 of file Solver.cs.

        {
            Assert(constraints);
        }
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);
            }
        }
void AssertAndTrack ( BoolExpr[]  constraints,
BoolExpr[]  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 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(BoolExpr[],BoolExpr[]) and the Boolean literals provided using Check with assumptions.

Definition at line 139 of file Solver.cs.

        {
            Contract.Requires(constraints != null);
            Contract.Requires(Contract.ForAll(constraints, c => c != null));
            Contract.Requires(Contract.ForAll(ps, c => c != null));
            Context.CheckContextMatch(constraints);
            Context.CheckContextMatch(ps);
            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(Context.nCtx, NativeObject, constraints[i].NativeObject, ps[i].NativeObject);
        }
void AssertAndTrack ( BoolExpr  constraint,
BoolExpr  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 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(BoolExpr[],BoolExpr[]) and the Boolean literals provided using Check with assumptions.

Definition at line 164 of file Solver.cs.

        {
            Contract.Requires(constraint != null);
            Contract.Requires(p != null);
            Context.CheckContextMatch(constraint);
            Context.CheckContextMatch(p);
                        
            Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.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 212 of file Solver.cs.

        {
            Z3_lbool r;
            if (assumptions == null || assumptions.Length == 0)
                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 317 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 190 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 235 of file Solver.cs.

uint NumAssertions [get]

The number of assertions in the solver.

Definition at line 178 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.

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 254 of file Solver.cs.

string ReasonUnknown [get]

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

Definition at line 292 of file Solver.cs.

Solver statistics.

Definition at line 305 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 274 of file Solver.cs.

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines