Discrepancy between Java/SMTlib interface

[GerhardSchellhorn]

Attached is a zip file with one file in SMTlib syntax and another file with java code. Both should have the same 3 axioms and same goal, and the same settings. Only the second axiom (named "Pot-pos") is relevant for the proof. Calling Z3 on command line with the SMTlib-file a proof is found, while running the Java program does not find one. After removing the "assertandTrack"-line for the first or third (irrelevant) axiom in the Java code the goal is proved. Changing the settings to auto=true does not change the result. I'm working under Ubuntu 18.04 with a checkout of Z3 several months old, but also just tested with a checkout from this morning (30.10.19). configure was standard with --java and --prefix. The output printed by the Java program shows no difference between the axioms and the goal compared to what's in the SMTlib file (except that some let's are pretty-printed). So my question is: What is different?

smtlib_vs_java.zip

[NikolajBjorner]

It is taking bandwidth to set up appropriate Java environment and remember how to operate Java. Could you use the logging mechanism? It produces text files that can be directly replayed without recompiling anything. You add a single line in your Log.open("z3.log"); as follows:

    System.out.println("smt: loading " + library);
    System.load(library);

    Log.open("z3.log");

    Map<String,String> config = new HashMap<String,String>();

Then upload z3.log

Another thing to play with, when quantifiers are involved is the random seed. Sometimes behavior changes according to order of declarations and the random seed (smt.random_seed=NN) can shed some light on this case

[GerhardSchellhorn]

Since I now found out, that the problem of the message "cannot process" when trying to attach the log-files was on my side, I thought it makes sense to upload the log-files here too (after sending them by mail last week with info how to run the java program). Changing the seed value to X=10,20,....100 with params.add("smt.random_seed", );

in Java and (set-option :smt.random_seed )

in the SMT-file did not make any difference. So here are three log-files: one with all three axioms (no proof found), two others with just axiom1+2 and axiom2+3 (both successful)

z3-allthreeaxioms.log z3-axiomsoneandtwo.log z3-axiomstwoandthree.log

[GerhardSchellhorn]

Always the same problem: github does not like using less/greater The lines were params.add("smt.random_seed", X) and (set-option :smt.random_seed X) etc.

[NikolajBjorner]

This helps a lot. It times out on the first file z3-allthreeaxioms.log, but finishes quickly on the other two. The first file enters an instantiation loop. It can be throttled using options smt.qi... For example smt.qi.max_instances=200 limits the instantiations and makes it complete. Generally, there is a axiom profiler tool from ETHZ that can be used to expose deficiencies in quantifier instantiation.

There are some built-in throttles to avoid instantiation loops, but it could be that these happen in a special case where assumptions are used. So something to investigate.

[GerhardSchellhorn]

I can understand if the pattern used in the second axiom causes an infinite loop, but it is really hard for me to analyze results (when deleting axioms , adding lemmas changing patterns etc) when I get a different result with the Java/standalone interface. Are the settings currently used in the smt file in any way different? It did not seem so, as I got the same difference with auto-config = true

[NikolajBjorner]

it is pretty subtle: the quantifiers created over the API have weight 0, the default weight from the parsed files is 1. This makes a difference in how it schedules quantifier instantiation. I will try to make this easier out of the box even though some workarounds are available, such as setting the weights to 1. A quantifier with weight 0 is assumed super cheap to instantiate. This isn't the case with the quantifier that defines embed.

I will push an update to Z3 later that ensures that even on 0 weight quantifier, the instance generation tracking is increased. In this way it will automatically throttle quantifier instantiation for this case.

[GerhardSchellhorn]

Ah, I understand now. The default I used in java for the weight of mkForall was indeed 0. I just ran the code for the example with weight 1, a proof is found then. I assume the default for existential quantifiers when parsing an SMT file then is 1 too, and this should remove the discrepancy. Thanks for the help.

[NikolajBjorner]

I am going to close this as I pushed a change that ensures that even if you assign weight = 0, the quantifier instantiation will back off appropriately and avoid the loop that this bug exposes.