Package com.microsoft.z3

Class Optimize

  • public class Optimize
extends Z3Object
    Object for managing optimization context

    • Method Detail

      • getHelp

        public java.lang.String getHelp()
        A string that describes all available optimize solver parameters.

      • setParameters

        public void setParameters​(Params value)
        Sets the optimize solver parameters.
        Throws:
        Z3Exception

      • getParameterDescriptions

        public ParamDescrs getParameterDescriptions()
        Retrieves parameter descriptions for Optimize solver.

      • Assert

        public void Assert​(Expr<BoolSort>... constraints)
        Assert a constraint (or multiple) into the optimize solver.

      • Add

        public void Add​(Expr<BoolSort>... constraints)
        Alias for Assert.

      • AssertAndTrack

        public void AssertAndTrack​(Expr<BoolSort> constraint,
                           Expr<BoolSort> p)
        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.

      • AssertSoft

        public Optimize.Handle<?> AssertSoft​(Expr<BoolSort> constraint,
                                     int weight,
                                     java.lang.String group)
        Assert soft constraint Return an objective which associates with the group of constraints.

      • AssertSoft

        public Optimize.Handle<?> AssertSoft​(Expr<BoolSort> constraint,
                                     java.lang.String weight,
                                     java.lang.String group)
        Assert soft constraint Return an objective which associates with the group of constraints.

      • Check

        public Status Check​(Expr<BoolSort>... assumptions)
        Check satisfiability of asserted constraints. Produce a model that (when the objectives are bounded and don't use strict inequalities) meets the objectives.

      • Push

        public void Push()
        Creates a backtracking point.

      • Pop

        public void Pop()
        Backtrack one backtracking point. Note that an exception is thrown if Pop is called without a corresponding Push.

      • getModel

        public Model getModel()
        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.

      • getUnsatCore

        public BoolExpr[] getUnsatCore()
        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.
        Throws:
        Z3Exception

      • MkMaximize

        public <R extends Sort> Optimize.Handle<R> MkMaximize​(Expr<R> e)
        Declare an arithmetical maximization objective. Return a handle to the objective. The handle is used as to retrieve the values of objectives after calling Check.

      • MkMinimize

        public <R extends Sort> Optimize.Handle<R> MkMinimize​(Expr<R> e)
        Declare an arithmetical minimization objective. Similar to MkMaximize.

      • getReasonUnknown

        public java.lang.String getReasonUnknown()
        Return a string the describes why the last to check returned unknown

      • toString

        public java.lang.String toString()
        Print the context to a String (SMT-LIB parseable benchmark).
        Overrides:
        toString in class java.lang.Object

      • fromFile

        public void fromFile​(java.lang.String file)
        Parse an SMT-LIB2 file with optimization objectives and constraints. The parsed constraints and objectives are added to the optimization context.

      • fromString

        public void fromString​(java.lang.String s)
        Similar to FromFile. Instead it takes as argument a string.

      • getAssertions

        public BoolExpr[] getAssertions()
        The set of asserted formulas.

      • getObjectives

        public Expr<?>[] getObjectives()
        The set of asserted formulas.

      • getStatistics

        public Statistics getStatistics()
        Optimize statistics.