Different duration for a different push/pop queries order?

[sy6sy2]

Hi,

I just notice that I obtain a different computation time of Boolector if I send it a list of queries in a different order, is it normal and how to optimize this?

To reproduce this issue download the files formula.smt2, mem_analysis.smt2 and reg_analysis.smt2.

• formula.smt2 only contain variables definitions without any check-sat or get-value.
• mem_analysis.smt2 and reg_analysis.smt2 contain a list of queries in the form of push - check-sat - get-value - assert - check-sat - pop.

If I swap mem_analysis.smt2 and reg_analysis.smt2 I obtain different durations:

$ cat formula.smt2 reg_analysis.smt2 mem_analysis.smt2 | time boolector --smt2 -i -d -m
boolector --smt2 -i -d -m  21,24s user 0,08s system 99% cpu 21,441 total

$ cat formula.smt2 mem_analysis.smt2 reg_analysis.smt2 | time boolector --smt2 -i -d -m
boolector --smt2 -i -d -m  39,16s user 0,17s system 98% cpu 39,880 total

Time is multiplied by 2!

Thank you for your help and/or explanation

Edit: It seems that I obtain a better time if I restart Boolector and re send the formula for each query instead of playing with the push - pop commands :-/

smtlib files.zip

[mpreiner]

Didn't have time to look at the files yet, since I'm currently very busy. I'll have a look and let you know soon.

[mpreiner]

@SylvainCecchetto A few questions:

1. How did you generate these files?
2. Are the values that you assert in each context the values returned by get-value?
3. What is the time if you always restart Boolector?

If 2. is yes:
In the first run you always exclude the current model value of the variable queried via get-value.
In the second run you exclude some value, but not the model value queried via get-value.

[sy6sy2]

Hi @mpreiner and thank you for taking a look at that.

1. Those files are generated with a tool that I currently code during my PhD. This tool need to makes some symbolic execution of a binary code. First we have to "translate" x86 instructions to an equivalent semantic (here SMTLIB), then from the SMTLIB formula I ask some queries to the solver in order to get informations about the system state (CPU registers values and memory cells values).

2. Yes this exactly what I do (maybe there is a smarter method to do that ?) What I want is to know if a variable can only get specifics values while the formula is SAT. This what I achieve:

   • Me: "Boolector, give me a SAT value of ESP_exit" ((get-value ESP_exit))
   • Boolector: "ESP_exit can take the value 0x12345678 while maintaining the formula SAT
   • Me: "Ok, is ESP_exit can take another value" ((assert ESP_exit != 0x12345678) and (get-value ESP_exit))
   • Boolector: "ESP_exit can take the value 0x87654321 while maintaining the formula SAT"
   • Me: "Ok, is ESP_exit can take another value" ((assert ESP_exit != 0x87654321) and (get-value ESP_exit))
   • Boolector: "UNSAT"

So I can conclude that ESP_exit can only take the values 0x12345678 and 0x87654321

Do you think that I can ask the same "question" to Boolector in only one query with the "maximum number of values to compute" paramter?

3. I do not have the exact execution time now for this experience but this actually what I do now: For each variable that I want the value(s) I kill Boolector, restart-it, and resend the complete formula. This is why I made this feature request (Add support for the (reset) SMTLIB command #32) in order to avoid the kill / restart steps of the processus.

Sorry but I don't really understand the last part of your comment :-/

[mpreiner]

@SylvainCecchetto Sorry for the delay. I totally forgot about this issue...

Do you see this behavior in more examples? I need to further look into this issue since it seems that the solving time does not really increase, but Boolector reports more time spent on generating the model.

[sy6sy2]

Sorry but I do not have more examples ATM.
I do not use the push/pop commands anymore, instead I reopen an instance of Boolector for each query and the total execution time is better.

[mpreiner]

Interesting. If you have benchmarks that exhibit this behaviour (push/pop slower than recreating solver instance) can you please share?