Method getUnits

src/api/java/Solver.java:349–353

Retrieve currently inferred units. Remarks: This retrieves the set of literals that the solver has inferred at the current decision level after a check call. @return An array of Boolean expressions representing the inferred units @throws Z3Exception

()

     * @throws Z3Exception
     **/
    public BoolExpr[] getUnits()
    {
        ASTVector units = new ASTVector(getContext(), Native.solverGetUnits(getContext().nCtx(), getNativeObject()));
        return units.ToBoolExprArray();
    }

    /**
     * Retrieve non-unit atomic formulas in the solver state.