Method getConsequences

src/api/java/Solver.java:274–284

Retrieve fixed assignments to the set of variables in the form of consequences. Each consequence is an implication of the form relevant-assumptions Implies variable = value where the relevant assumptions is a subset of the assumptions that are passed in and the equality on the right side of

(Expr<BoolSort>[] assumptions, Expr<?>[] variables, List<Expr<BoolSort>> consequences)

     *
     */
    public Status getConsequences(Expr<BoolSort>[] assumptions, Expr<?>[] variables, List<Expr<BoolSort>> consequences)
    {
	ASTVector result = new ASTVector(getContext());
	ASTVector asms = new ASTVector(getContext());
	ASTVector vars = new ASTVector(getContext());
	for (Expr<BoolSort> asm : assumptions) asms.push(asm);
	for (Expr<?> v : variables) vars.push(v);
	int r = Native.solverGetConsequences(getContext().nCtx(), getNativeObject(), asms.getNativeObject(), vars.getNativeObject(), result.getNativeObject());
        for (int i = 0; i < result.size(); ++i) consequences.add((BoolExpr) Expr.create(getContext(), result.get(i).getNativeObject()));
	return lboolToStatus(Z3_lbool.fromInt(r));
    }


    /**