Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Package Functions
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());
    }

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();
        }
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines