[SAL-HELP] Re: [SAL] asking for help with SAL
bruno at csl.sri.com
Mon Mar 26 10:25:48 PDT 2007
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.
More information about the SAL-HELP