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.