Solver Class Reference

Inheritance diagram for Solver:

Public Member Functions
String	getHelp () throws Z3Exception
void	setParameters (Params value) throws Z3Exception
ParamDescrs	getParameterDescriptions () throws Z3Exception
int	getNumScopes () throws Z3Exception
void	push () throws Z3Exception
void	pop () throws Z3Exception
void	pop (int n) throws Z3Exception
void	reset () throws Z3Exception
void	add (BoolExpr...constraints) throws Z3Exception
void	assertAndTrack (BoolExpr[] constraints, BoolExpr[] ps) throws Z3Exception
void	assertAndTrack (BoolExpr constraint, BoolExpr p) throws Z3Exception
int	getNumAssertions () throws Z3Exception
BoolExpr[]	getAssertions () throws Z3Exception
Status	check (Expr...assumptions) throws Z3Exception
Status	check () throws Z3Exception
Model	getModel () throws Z3Exception
Expr	getProof () throws Z3Exception
Expr[]	getUnsatCore () throws Z3Exception
String	getReasonUnknown () throws Z3Exception
Statistics	getStatistics () throws Z3Exception
String	toString ()
Package Functions
	Solver (Context ctx, long obj) throws Z3Exception
void	incRef (long o) throws Z3Exception
void	decRef (long o) throws Z3Exception

---

Detailed Description

Solvers.

Definition at line 25 of file Solver.java.

---

Constructor & Destructor Documentation

Solver	(	Context	ctx,
		long	obj
	)		throws Z3Exception [inline, package]

Definition at line 320 of file Solver.java.

    {
        super(ctx, obj);
    }

---

Member Function Documentation

void add

(

BoolExpr...

constraints

)

throws Z3Exception [inline]

Assert a multiple constraints into the solver.

Exceptions:

Z3Exception

Definition at line 108 of file Solver.java.

    {
        getContext().checkContextMatch(constraints);
        for (BoolExpr a : constraints)
        {
            Native.solverAssert(getContext().nCtx(), getNativeObject(),
                    a.getNativeObject());
        }
    }

void assertAndTrack	(	BoolExpr[]	constraints,
		BoolExpr[]	ps
	)		throws Z3Exception [inline]

Definition at line 132 of file Solver.java.

    {
        getContext().checkContextMatch(constraints);
        getContext().checkContextMatch(ps);
        if (constraints.length != ps.length)
            throw new Z3Exception("Argument size mismatch");

        for (int i = 0; i < constraints.length; i++)
            Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
                    constraints[i].getNativeObject(), ps[i].getNativeObject());
    }

void assertAndTrack	(	BoolExpr	constraint,
		BoolExpr	p
	)		throws Z3Exception [inline]

Definition at line 157 of file Solver.java.

    {
        getContext().checkContextMatch(constraint);
        getContext().checkContextMatch(p);

        Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
                constraint.getNativeObject(), p.getNativeObject());
    }

Status check

(

Expr...

assumptions

)

throws Z3Exception [inline]

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

See also:

Model, UnsatCore, Proof

Definition at line 199 of file Solver.java.

    {
        Z3_lbool r;
        if (assumptions == null)
            r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
                    getNativeObject()));
        else
            r = Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext()
                    .nCtx(), getNativeObject(), (int) assumptions.length, AST
                    .arrayToNative(assumptions)));
        switch (r)
        {
        case Z3_L_TRUE:
            return Status.SATISFIABLE;
        case Z3_L_FALSE:
            return Status.UNSATISFIABLE;
        default:
            return Status.UNKNOWN;
        }
    }

Status check

(

)

throws Z3Exception [inline]

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

See also:

Model, UnsatCore, Proof

Definition at line 225 of file Solver.java.

    {
        return check((Expr[]) null);
    }

void decRef

(

long

o

)

throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 331 of file Solver.java.

    {
        getContext().solver_DRQ().add(o);
        super.decRef(o);
    }

BoolExpr [] getAssertions

(

)

throws Z3Exception [inline]

The set of asserted formulas.

Exceptions:

Z3Exception

Definition at line 183 of file Solver.java.

    {
        ASTVector ass = new ASTVector(getContext(), Native.solverGetAssertions(
                getContext().nCtx(), getNativeObject()));
        int n = ass.size();
        BoolExpr[] res = new BoolExpr[n];
        for (int i = 0; i < n; i++)
            res[i] = new BoolExpr(getContext(), ass.get(i).getNativeObject());
        return res;
    }

String getHelp

(

)

throws Z3Exception [inline]

A string that describes all available solver parameters.

Definition at line 30 of file Solver.java.

    {
        return Native.solverGetHelp(getContext().nCtx(), getNativeObject());
    }

Model getModel

(

)

throws Z3Exception [inline]

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.

Exceptions:

Z3Exception

Definition at line 238 of file Solver.java.

    {
        long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
        if (x == 0)
            return null;
        else
            return new Model(getContext(), x);
    }

int getNumAssertions

(

)

throws Z3Exception [inline]

The number of assertions in the solver.

Exceptions:

Z3Exception

Definition at line 171 of file Solver.java.

    {
        ASTVector ass = new ASTVector(getContext(), Native.solverGetAssertions(
                getContext().nCtx(), getNativeObject()));
        return ass.size();
    }

int getNumScopes

(

)

throws Z3Exception [inline]

The current number of backtracking points (scopes).

See also:

Pop, Push

Definition at line 62 of file Solver.java.

    {
        return Native
                .solverGetNumScopes(getContext().nCtx(), getNativeObject());
    }

ParamDescrs getParameterDescriptions

(

)

throws Z3Exception [inline]

Retrieves parameter descriptions for solver.

Exceptions:

Z3Exception

Definition at line 52 of file Solver.java.

    {
        return new ParamDescrs(getContext(), Native.solverGetParamDescrs(
                getContext().nCtx(), getNativeObject()));
    }

Expr getProof

(

)

throws Z3Exception [inline]

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.

Exceptions:

Z3Exception

Definition at line 255 of file Solver.java.

    {
        long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
        if (x == 0)
            return null;
        else
            return Expr.create(getContext(), x);
    }

String getReasonUnknown

(

)

throws Z3Exception [inline]

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

Definition at line 288 of file Solver.java.

    {
        return Native.solverGetReasonUnknown(getContext().nCtx(),
                getNativeObject());
    }

Statistics getStatistics

(

)

throws Z3Exception [inline]

Solver statistics.

Exceptions:

Z3Exception

Definition at line 299 of file Solver.java.

    {
        return new Statistics(getContext(), Native.solverGetStatistics(
                getContext().nCtx(), getNativeObject()));
    }

Expr [] getUnsatCore

(

)

throws Z3Exception [inline]

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.

Exceptions:

Z3Exception

Definition at line 272 of file Solver.java.

    {

        ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(
                getContext().nCtx(), getNativeObject()));
        int n = core.size();
        Expr[] res = new Expr[n];
        for (int i = 0; i < n; i++)
            res[i] = Expr.create(getContext(), core.get(i).getNativeObject());
        return res;
    }

void incRef

(

long

o

)

throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 325 of file Solver.java.

    {
        getContext().solver_DRQ().incAndClear(getContext(), o);
        super.incRef(o);
    }

void pop

(

)

throws Z3Exception [inline]

Backtracks one backtracking point. .

Definition at line 79 of file Solver.java.

    {
        pop(1);
    }

void pop

(

int

n

)

throws Z3Exception [inline]

Backtracks n backtracking points. Note that an exception is thrown if n is not smaller than NumScopes

See also:

Push

Definition at line 89 of file Solver.java.

    {
        Native.solverPop(getContext().nCtx(), getNativeObject(), n);
    }

void push

(

)

throws Z3Exception [inline]

Creates a backtracking point.

See also:

Pop

Definition at line 71 of file Solver.java.

    {
        Native.solverPush(getContext().nCtx(), getNativeObject());
    }

void reset

(

)

throws Z3Exception [inline]

Resets the Solver. This removes all assertions from the solver.

Definition at line 98 of file Solver.java.

    {
        Native.solverReset(getContext().nCtx(), getNativeObject());
    }

void setParameters

(

Params

value

)

throws Z3Exception [inline]

Sets the solver parameters.

Exceptions:

Z3Exception

Definition at line 40 of file Solver.java.

    {
        getContext().checkContextMatch(value);
        Native.solverSetParams(getContext().nCtx(), getNativeObject(),
                value.getNativeObject());
    }

String toString

(

)

[inline]

A string representation of the solver.

Definition at line 308 of file Solver.java.

    {
        try
        {
            return Native
                    .solverToString(getContext().nCtx(), getNativeObject());
        } catch (Z3Exception e)
        {
            return "Z3Exception: " + e.getMessage();
        }
    }