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

[Bruno Dutertre]

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