Performance Regression from 4.11.2 to 4.12.1

[baierd]

Hi,
we over at JavaSMT noticed a performance regression for some tasks.
Those were quite fast in 4.11.2 etc. but now either don't terminate or take a very long time (10min+).
We use the internal Java API.
The following example program first executes a example using the public Java API, which results in the correct solution in 1-2s. Then the same query is run using the internal API, which takes 10min+.
Either something changed in the handling of the internal API in that we need to change something, or there is some regression going on.
Help would be appreciated.

(We can provide at least 1 more example if needed, the second example is not String based.)

Example (Java):

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.z3StringInternalAPI();
    }

    // Works fine
    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 public API done");
    }


    // 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));
        }
    }

    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;
            }
        }
    }
}

[kfriedberger]

The difference in the programs is the random seed. It looks like the value "42" is a bad choice.

[NikolajBjorner]

You can create SMT2 files to make repros easier for others.
Setting up a Java repro takes some time.

[baierd]

Sorry, SMT2 as follows:

(declare-fun |1| () String)
(declare-fun |0| () String)
(assert (let ((a!1 (or (not (and (str.<= |0| |1|) (str.<= |1| |0|))) (= |0| |1|))))
  (not a!1)))
(check-sat)

[NikolajBjorner]

I added trichotomy which solves this.
I considered str.<= as a somewhat exotic predicate.
There is limited inference support for it.
Do you have a use case for it or is it just unit testing every possible predicate?

[kfriedberger]

We encountered the regression through an existing unit test in JavaSMT.
The JavaSMT API provides the operations for String theory, because users requested it in general.
However, String theory is quite new and we do not know which user applies which theory or operation.