Optimize Class Reference

Inheritance diagram for Optimize:

Data Structures
class	Handle

Public Member Functions
String	getHelp ()
void	setParameters (Params value)
ParamDescrs	getParameterDescriptions ()
void	Assert (Expr< BoolSort >... constraints)
void	Add (Expr< BoolSort >... constraints)
void	AssertAndTrack (Expr< BoolSort > constraint, Expr< BoolSort > p)
Handle<?>	AssertSoft (Expr< BoolSort > constraint, int weight, String group)
Handle<?>	AssertSoft (Expr< BoolSort > constraint, String weight, String group)
Status	Check (Expr< BoolSort >... assumptions)
void	Push ()
void	Pop ()
Model	getModel ()
BoolExpr[]	getUnsatCore ()
String	getReasonUnknown ()
String	toString ()
void	fromFile (String file)
void	fromString (String s)
BoolExpr[]	getAssertions ()
Expr<?>[]	getObjectives ()
void	setInitialValue (Expr<?> var, Expr<?> value)
Statistics	getStatistics ()

Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[]	arrayToNative (Z3Object[] a)
static int	arrayLength (Z3Object[] a)

Detailed Description

Object for managing optimization context

Definition at line 30 of file Optimize.java.

Member Function Documentation

Add()

void Add ( Expr< BoolSort >...  constraints )

inline

Alias for Assert.

Definition at line 73 of file Optimize.java.

    {
        Assert(constraints);
    }

Assert()

void Assert ( Expr< BoolSort >...  constraints )

inline

Assert a constraint (or multiple) into the optimize solver.

Definition at line 61 of file Optimize.java.

    {
        getContext().checkContextMatch(constraints);
        for (Expr<BoolSort> a : constraints)
        {
            Native.optimizeAssert(getContext().nCtx(), getNativeObject(), a.getNativeObject());
        }
    }

AssertAndTrack()

void AssertAndTrack ( Expr< BoolSort >  constraint, Expr< BoolSort >  p  )

inline

Assert a constraint into the optimizer, and track it (in the unsat) core using the Boolean constant p.

Remarks: 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 and the Boolean literals provided using Check with assumptions.

See also

Optimize::Check

Optimize::AssertAndTrack

Definition at line 93 of file Optimize.java.

    {
        getContext().checkContextMatch(constraint);
        getContext().checkContextMatch(p);
 
        Native.optimizeAssertAndTrack(getContext().nCtx(), getNativeObject(),
                constraint.getNativeObject(), p.getNativeObject());
    }

AssertSoft() [1/2]

Handle<?> AssertSoft ( Expr< BoolSort >  constraint, int  weight, String  group  )

inline

Assert soft constraint

Return an objective which associates with the group of constraints.

Definition at line 179 of file Optimize.java.

    {
        return AssertSoft(constraint, Integer.toString(weight), group);
    }

AssertSoft() [2/2]

Handle<?> AssertSoft ( Expr< BoolSort >  constraint, String  weight, String  group  )

inline

Assert soft constraint

Return an objective which associates with the group of constraints.

Definition at line 190 of file Optimize.java.

    {
        getContext().checkContextMatch(constraint);
        Symbol s = getContext().mkSymbol(group);
        return new Handle<>(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), weight, s.getNativeObject()));
    }

Check()

Status Check ( Expr< BoolSort >...  assumptions )

inline

Check satisfiability of asserted constraints. Produce a model that (when the objectives are bounded and don't use strict inequalities) is optimal.

Definition at line 202 of file Optimize.java.

    {
        Z3_lbool r;
        if (assumptions == null) {
          r = Z3_lbool.fromInt(
              Native.optimizeCheck(
                  getContext().nCtx(), 
                  getNativeObject(), 0, null));
        }
        else {
          r = Z3_lbool.fromInt(
              Native.optimizeCheck(
                  getContext().nCtx(), 
                  getNativeObject(), 
                  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;
        }
    }

fromFile()

void fromFile ( String  file )

inline

Parse an SMT-LIB2 file with optimization objectives and constraints. The parsed constraints and objectives are added to the optimization context.

Definition at line 371 of file Optimize.java.

    {
        Native.optimizeFromFile(getContext().nCtx(), getNativeObject(), file);
    }

fromString()

void fromString ( String  s )

inline

Similar to FromFile. Instead it takes as argument a string.

Definition at line 379 of file Optimize.java.

    {
        Native.optimizeFromString(getContext().nCtx(), getNativeObject(), s);
    }

getAssertions()

BoolExpr[] getAssertions ( )

inline

The set of asserted formulas.

Definition at line 387 of file Optimize.java.

    {
        ASTVector assertions = new ASTVector(getContext(), Native.optimizeGetAssertions(getContext().nCtx(), getNativeObject()));
        return assertions.ToBoolExprArray();
    }

getHelp()

String getHelp ( )

inline

A string that describes all available optimize solver parameters.

Definition at line 35 of file Optimize.java.

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

getModel()

Model getModel ( )

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.

Definition at line 254 of file Optimize.java.

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

getObjectives()

Expr<?>[] getObjectives ( )

inline

The set of asserted formulas.

Definition at line 396 of file Optimize.java.

    {
        ASTVector objectives = new ASTVector(getContext(), Native.optimizeGetObjectives(getContext().nCtx(), getNativeObject()));
        return objectives.ToExprArray();
    }

getParameterDescriptions()

ParamDescrs getParameterDescriptions ( )

inline

Retrieves parameter descriptions for Optimize solver.

Definition at line 53 of file Optimize.java.

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

getReasonUnknown()

String getReasonUnknown ( )

inline

Return a string the describes why the last to check returned unknown

Definition at line 353 of file Optimize.java.

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

getStatistics()

Statistics getStatistics ( )

inline

Optimize statistics.

Definition at line 421 of file Optimize.java.

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

getUnsatCore()

BoolExpr[] getUnsatCore ( )

inline

The unsat core of the last Check. Remarks: The unsat core is a subset of Assumptions 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 273 of file Optimize.java.

    {
        ASTVector core = new ASTVector(getContext(), Native.optimizeGetUnsatCore(getContext().nCtx(), getNativeObject()));        
        return core.ToBoolExprArray();
    }

Pop()

void Pop ( )

inline

Backtrack one backtracking point.

Note that an exception is thrown if Pop is called without a corresponding Push.

Definition at line 242 of file Optimize.java.

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

Push()

void Push ( )

inline

Creates a backtracking point.

Definition at line 232 of file Optimize.java.

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

setInitialValue()

void setInitialValue ( Expr<?>  var, Expr<?>  value  )

inline

Set an initial value for a variable to guide the optimizer's search heuristics. This can improve performance when a good initial value is known for the variable.

Parameters

var	The variable to set an initial value for
value	The initial value for the variable

Exceptions

Z3Exception

Definition at line 410 of file Optimize.java.

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

setParameters()

void setParameters ( Params  value )

inline

Sets the optimize solver parameters.

Exceptions

Z3Exception

Definition at line 45 of file Optimize.java.

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

toString()

String toString ( )

inline

Print the context to a String (SMT-LIB parseable benchmark).

Definition at line 362 of file Optimize.java.

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