Method query

src/api/java/Fixedpoint.java:123–136

Query the fixedpoint solver. A query is a conjunction of constraints. The constraints may include the recursively defined relations. The query is satisfiable if there is an instance of the query variables and a derivation for it. The query is unsatisfiable if there are no derivations satisfying the

(Expr<BoolSort> query)

     * @throws Z3Exception
     **/
    public Status query(Expr<BoolSort> query) {
        getContext().checkContextMatch(query);
        Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQuery(getContext().nCtx(),
                getNativeObject(), query.getNativeObject()));
        switch (r)
        {
        case Z3_L_TRUE:
            return Status.SATISFIABLE;
        case Z3_L_FALSE:
            return Status.UNSATISFIABLE;
        default:
            return Status.UNKNOWN;
        }
    }

    /**
     * Query the fixedpoint solver. A query is an array of relations. The query