Method getTrailLevels

src/api/java/Solver.java:402–408

Retrieve the decision levels for each literal in the solver's trail after a check call. The trail contains Boolean literals (decisions and propagations) in the order they were assigned. The returned array has one entry per trail literal, indicating at which decision level it was assigned. Us

()

     * @throws Z3Exception
     **/
    public int[] getTrailLevels()
    {
        ASTVector trailVector = new ASTVector(getContext(), Native.solverGetTrail(getContext().nCtx(), getNativeObject()));
        int[] levels = new int[trailVector.size()];
        Native.solverGetLevels(getContext().nCtx(), getNativeObject(), trailVector.getNativeObject(), trailVector.size(), levels);
        return levels;
    }

    /**
     * Return a sequence of cubes (conjunctions of literals) for partitioning the search space.