baierd
commented
1 year ago 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;
}
}
}
}
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 c1ad8c01e76ee8073ea53db5636f129b6ef867b6. 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.