[YICES-HELP] Questions on a few performance issues

[Marco Murciano]

Dear Yices community members,
I am a developer which has started using the Yices command line and API 
interface
since their very first releases. I would like to ask some simple 
questions, concerning a few
performance issues that I'm experiencing with the usage of the API. They 
arise from the
comparison with the command line version, which is unfair, in the sense 
that it is faster than
the API, while, in my honest opinion, it should not be like this.

1. Am I missing something about the command line version optimizations 
or am I using the API
in the wrong way?
2. Are there significant performance differences between the Yices 
binary and the API interface?

Here I attach a couple of examples. They both generate the same problem, 
a simple bubble
sorted array of integers (the input variables), which is internally 
constrained in such a way that
the last set of Yices expressions reflects the bsort ordering of the 
input array.
I used < >= and ITE operators, only.

Ex: having a 3 element { v_0, v_1, v_2 } input array, I impose that the 
final set of expressions
{ e_0, e_1, e_2 } is ordered in such a way that e_0 <= e_1 and e_1 <= e_2.
The main and sole assertion checks whether there exist a set of values 
which satisfies the clause

e_0 > e_1 || e_1 > e_2

which is obviously unsatisfiable.

---

- The example "yices_main_5.c" is based on the API.
Executing the command

./yices_main_5 0 20

the executable creates the set of clauses for a 20 element array, using 
the LIA logic.

- The example "bubblesort.c" generates an SMTLIB compatible instance, 
for the same problem.
The command:

./bubblesort 3 0 2>/dev/null

produces the human readable SMTLIB compatible benchmark for a three 
element array. The second
command line argument switches from a human readable SMTLIB compatible 
format (0, as in this case)
to optimized single line SMTLIB compatible format (1).
The stderr stream is redirected to /dev/null because it produces some 
debug info (the array element state
change across different iterations of the algorithm).
- The file "games.h" is an header needed to compile bubblesort.c, which 
contains some macros.

Some tech questions:

1. Is void yices_set_arith_only 
<http://yices.csl.sri.com/capi.shtml#ga13> (int flag) supposed to be 
used for BV or for LIA instances only?
2. How strongly do retractable assertions affect the solver reasoning speed?
3. Is there any issue related to the usage of APIs in the 
"yices_main_5.c" example? I just need
some feedback, as it is not easy to find examples on the web, but simple 
ones you provided.

Thank you very much.

Regards,

Marco Murciano

-- 
--------------------------------------------------------------------------------
!    Bocciato il lodo Alfano. Ad Hammamet stanno già dando aria alle stanze    !
--------------------------------------------------------------------------------
!                http://www.voglioscendere.ilcannocchiale.it/                  !
--------------------------------------------------------------------------------

-------------- next part --------------
A non-text attachment was scrubbed...
Name: yices_main_5.c
Type: text/x-csrc
Size: 5564 bytes
Desc: not available
Url : http://lists.csl.sri.com/pipermail/yices-help/attachments/20100207/b6ee5e42/yices_main_5.bin
-------------- next part --------------
A non-text attachment was scrubbed...
Name: bubblesort.c
Type: text/x-csrc
Size: 3164 bytes
Desc: not available
Url : http://lists.csl.sri.com/pipermail/yices-help/attachments/20100207/b6ee5e42/bubblesort.bin
-------------- next part --------------
A non-text attachment was scrubbed...
Name: games.h
Type: text/x-chdr
Size: 846 bytes
Desc: not available
Url : http://lists.csl.sri.com/pipermail/yices-help/attachments/20100207/b6ee5e42/games.bin