Closed sy6sy2 closed 4 years ago
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.
@SylvainCecchetto A few questions:
get-value
?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
.
Hi @mpreiner and thank you for taking a look at that.
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).
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:
(get-value ESP_exit)
)(assert ESP_exit != 0x12345678)
and (get-value ESP_exit)
)(assert ESP_exit != 0x87654321)
and (get-value ESP_exit)
)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?
Sorry but I don't really understand the last part of your comment :-/
@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.
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.
Interesting. If you have benchmarks that exhibit this behaviour (push/pop slower than recreating solver instance) can you please share?
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
andreg_analysis.smt2
.formula.smt2
only contain variables definitions without anycheck-sat
orget-value
.mem_analysis.smt2
andreg_analysis.smt2
contain a list of queries in the form ofpush - check-sat - get-value - assert - check-sat - pop
.If I swap
mem_analysis.smt2
andreg_analysis.smt2
I obtain different durations: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