[SAL-HELP] RE: [SAL] asking for help with SAL

[Dulce María Hernández Rojas]

Thank you very much. Your help is being useful to me. I have another
question:
What is the meaning of these lines:

map: pc1_ at _0!1 -> x_0
map: pc1_ at _0!2 -> x_1

And what does the ! operator mean?

Thank you again for your answer. :)



-----Mensaje original-----
De: Bruno Dutertre [mailto:bruno at csl.sri.com] 
Enviado el: Lunes, 26 de Marzo de 2007 11:26 a.m.
Para: Dulce María Hernández Rojas
CC: sal-help at csl.sri.com
Asunto: Re: [SAL] asking for help with SAL

Dulce María Hernández Rojas wrote:
> I have a Dimac boolean formulation. I need the relation of the Bounded
Model
> Checking generated variables with the Dimacs ones.
> Is there a file containing these relationships?
> 

That's not easy to do with sal-bmc. If you're willing to use sal-inf-bmc,
then the option --show-var-mapping will print the mapping between SAL
and Yices variables (or other decision procedure).

The mapping is shown as follows

map: pc1_ at _0 -> x_0
...
map: pc1_ at _9 --> x_102

This means variable pc1 in state 0 is mapped to x_0 and
pc1 is state 9 is mapped to x_102. There may be extra variables
introduced during the translation that will not correspond to any
state variables in the SAL module. If you don't want that,
use options --disable-cse and --disable-traceability, but there may
be a performance cost with --disable-cse.

Bruno

-- 
No virus found in this incoming message.
Checked by AVG Free Edition.
Version: 7.5.446 / Virus Database: 268.18.18/733 - Release Date: 25/03/2007
11:07 a.m.
 

-- 
No virus found in this outgoing message.
Checked by AVG Free Edition.
Version: 7.5.446 / Virus Database: 268.18.18/734 - Release Date: 26/03/2007
02:31 p.m.