Analyze performance regressions with Z3 after update to version 4.12.1

[kfriedberger]

With the latest version 4.12.1 of Z3, there are two performance regressions in our JUnit tests.
As temporary solution, the tests were disabled with the commit c1ad8c0.
For long-term solution, we should at least analyze the problem one step deeper, summarize the result, and create an example query or minimal Java program which can be reported back to the Z3 developers.

@baierd Feel free to add more info about the bugs within this issue.

[baierd]

I've written a program in native Z3 API and could not reproduce the slowdown. (see below)
But i did use the current main branch of Z3 in my tests (because of API fixes that i needed) and i did not use any options.
I will test the main Z3 version next and see if that fixes the problem for us.
If it does not i will refine the example program.

import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.CharSort;
import com.microsoft.z3.Context;
import com.microsoft.z3.Expr;
import com.microsoft.z3.SeqSort;
import com.microsoft.z3.Solver;
import com.microsoft.z3.Sort;
import com.microsoft.z3.Status;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;
import java.util.function.Consumer;

public class Z3SlowdownExamples {

    public static void main(String[] args) throws Exception {
        loadLibrariesWithFallback(
                System::loadLibrary, new ArrayList<>(Arrays.asList("z3", "z3java")), new ArrayList<>(Arrays.asList("libz3", "libz3java")));
        Z3SlowdownExamples instance = new Z3SlowdownExamples();
        instance.z3String();
        instance.modelIssue();
    }

    public void z3String() throws Exception {
        Context ctx = new Context();

        SeqSort<CharSort> stringSort = ctx.mkStringSort();
        Expr<SeqSort<CharSort>> var1 = ctx.mkConst(ctx.mkSymbol("0"), stringSort);
        Expr<SeqSort<CharSort>> var2 = ctx.mkConst(ctx.mkSymbol("1"), stringSort);
        BoolExpr formula1 = ctx.mkAnd(ctx.MkStringLe(var1, var2), ctx.MkStringLe(var2, var1));
        BoolExpr expected = ctx.mkEq(var1, var2);
        BoolExpr impl = ctx.mkOr(ctx.mkNot(formula1), expected);

        Solver s = ctx.mkSolver();
        s.add(ctx.mkNot(impl));
        Status sat = s.check();
        if (sat == Status.SATISFIABLE) {
            // We expect this to be UNSAT
            throw new Exception("SAT. Wrong answer.");
        }

        BoolExpr implReversed = ctx.mkOr(ctx.mkNot(expected), formula1);

        s = ctx.mkSolver();
        s.add(ctx.mkNot(implReversed));
        sat = s.check();
        if (sat == Status.SATISFIABLE) {
            // We expect this to be UNSAT
            throw new Exception("SAT. Wrong answer.");
        }
        System.out.println("String example done");
    }


    public void modelIssue() throws Exception {
        Context ctx = new Context();
        BoolExpr a = ctx.mkAnd(ctx.parseSMTLIB2File("../SMT2_UF_and_Array.smt2", null, null, null, null));

        Solver s = ctx.mkSolver();
        s.add(a);
        Status sat = s.check();
        if (sat != Status.SATISFIABLE) {
            throw new Exception("UNSAT");
        } else {
            s.getModel();

        }
        System.out.println("Model example done");
    }

    protected static void loadLibrariesWithFallback(
            Consumer<String> loader,
            List<String> librariesForFirstTry,
            List<String> librariesForSecondTry)
            throws UnsatisfiedLinkError {
        try {
            librariesForFirstTry.forEach(loader);
        } catch (UnsatisfiedLinkError e1) {
            try {
                librariesForSecondTry.forEach(loader);
            } catch (UnsatisfiedLinkError e2) {
                e1.addSuppressed(e2);
                throw e1;
            }
        }
    }
}

[baierd]

Using the internal API of Z3, the String based task suddenly takes a very long time.

// Takes a very long time
    public void z3StringInternalAPI() throws Exception {
        final Map<String, Long> symbolsToDeclarations = new LinkedHashMap<>();

        long cfg = Native.mkConfig();
        Native.globalParamSet("smt.random_seed", String.valueOf("42"));
        Native.globalParamSet("model.compact", "false");
        Map<String, Object> pSolverOptions = new HashMap<>();
        pSolverOptions.put(":random-seed", 42);
        pSolverOptions.put(":model", true);
        pSolverOptions.put(":unsat_core", false);

        final long ctx = Native.mkContextRc(cfg);
        Native.delConfig(cfg);

        long stringSort = Native.mkStringSort(ctx);
        Native.incRef(ctx, Native.sortToAst(ctx, stringSort));

        long symbol1 = Native.mkStringSymbol(ctx, "00");
        long var1 = Native.mkConst(ctx, symbol1, stringSort);
        Native.incRef(ctx, Native.sortToAst(ctx, var1));
        long symbol2 = Native.mkStringSymbol(ctx, "11");
        long var2 = Native.mkConst(ctx, symbol2, stringSort);
        Native.incRef(ctx, Native.sortToAst(ctx, var2));
        long le = Native.mkStrLe(ctx, var1, var2);
        Native.incRef(ctx, le);
        long ge = Native.mkStrLe(ctx, var2, var1);
        Native.incRef(ctx, ge);
        long[] array = new long[]{le, ge};
        long formula1 = Native.mkAnd(ctx, 2, array);
        Native.incRef(ctx, formula1);
        long not = Native.mkNot(ctx, formula1);
        Native.incRef(ctx, not);
        long expected = Native.mkEq(ctx, var1, var2);
        Native.incRef(ctx, expected);

        long impl = Native.mkOr(ctx, 2, new long[] {not, expected});
        Native.incRef(ctx, impl);
        long negFormula = Native.mkNot(ctx, impl);
        Native.incRef(ctx, negFormula);

        System.out.println("z3StringInternalAPI formulas created");
        long s = Native.mkSolver(ctx);
        System.out.println("z3StringInternalAPI solver created w/o options");
        // missing: interrupt
        Native.solverIncRef(ctx, s);

        long z3params = Native.mkParams(ctx);
        Native.paramsIncRef(ctx, z3params);
        for (Map.Entry<String, Object> entry : pSolverOptions.entrySet()) {
            addParameter(z3params, entry.getKey(), entry.getValue(), ctx);
        }
        System.out.println("z3StringInternalAPI option params added");
        Native.solverSetParams(ctx, s, z3params);
        Native.paramsDecRef(ctx, z3params);
        System.out.println("z3StringInternalAPI solver created fully");

        Native.solverPush(ctx, s);
        System.out.println("z3StringInternalAPI pushed solver");
        addConstraint0(negFormula, ctx, s);
        System.out.println("z3StringInternalAPI constraint added, begin solving");
        int result = Native.solverCheck(ctx, s);
        if (result != Z3_lbool.Z3_L_FALSE.toInt()) {
            // We expect this to be UNSAT
            throw new Exception("SAT. Wrong answer.");
        }
        System.out.println("z3StringInternalAPI first SAT check successfull UNSAT");

        long not2 = Native.mkNot(ctx, expected);
        Native.incRef(ctx, not2);
        long implReversed = Native.mkOr(ctx, 2, new long[] {not2, formula1});
        Native.incRef(ctx, implReversed);
        long neg2Formula = Native.mkNot(ctx, implReversed);
        Native.incRef(ctx, neg2Formula);
        addConstraint0(neg2Formula, ctx, s);
        result = Native.solverCheck(ctx, s);
        if (result == Z3_lbool.Z3_L_FALSE.toInt()) {
            // We expect this to be UNSAT
            throw new Exception("SAT. Wrong answer.");
        }
        System.out.println("String internal API example done");
    }

    void addParameter(long z3params, String key, Object value, long z3context) {
        long keySymbol = Native.mkStringSymbol(z3context, key);
        if (value instanceof Boolean) {
            Native.paramsSetBool(z3context, z3params, keySymbol, (Boolean) value);
        } else if (value instanceof Integer) {
            Native.paramsSetUint(z3context, z3params, keySymbol, (Integer) value);
        } else if (value instanceof Double) {
            Native.paramsSetDouble(z3context, z3params, keySymbol, (Double) value);
        } else if (value instanceof String) {
            long valueSymbol = Native.mkStringSymbol(z3context, (String) value);
            Native.paramsSetSymbol(z3context, z3params, keySymbol, valueSymbol);
        } else {
            throw new IllegalArgumentException(
                    String.format(
                            "unexpected type '%s' with value '%s' for parameter '%s'",
                            value.getClass(), value, key));
        }
    }

[kfriedberger]

@baierd could you file an issue for Z3 with your information? Maybe @NikolajBjorner can help with the regression.

[baierd]

Done:
Z3Prover/z3#6586

[baierd]

I've just tested the change in random seed for the parsed model (array) problem and it does not seem to change the issue present there. I've tried no random seed, as well as seeds 1, 2, 22, 43, 745638.

I'll translate the model problem to internal API and update the Z3 issue.

[baierd]

I've tested the current main branch after the update of our Z3 String issue, and the regression is gone!

[baierd]

I found the time to finish the model/parsing issue program and opened a issue.

[baierd]

Fixed in the newest main branch. Therefore both regressions should be gone by the next release of Z3.