ic3: property numbers

[kroening]

The 'short_name' idea seems to be that properties end on a dot followed by a unique number. This is not the case.

Instead of --prop, please use --property, to be consistent with the rest of ebmc.

[eigold]

I just made a simple assumption to keep going when I was working on incorporating ic3. Matthias fixed the problem in one of PRs. Eugene

…

On Sun, May 21, 2017 at 11:13 AM, Daniel Kroening ***@***.***> wrote: The 'short_name' idea seems to be that properties end on a dot followed by a unique number. This is not the case. Instead of --prop, please use --property, to be consistent with the rest of ebmc. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#9>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AS5pClFBqDOx2tTzLZP9SXT4TjjoscG8ks5r8FSlgaJpZM4NhoNu> .

[eigold]

I will replace --prop to --property. Eugene

…

On Sun, May 21, 2017 at 11:13 AM, Daniel Kroening ***@***.***> wrote: Assigned #9 <#9> to @eigold <https://github.com/eigold>. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#9 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AS5pClFBqDOx2tTzLZP9SXT4TjjoscG8ks5r8FSlgaJpZM4NhoNu> .

[eigold]

Okay, now I see what Daniel's comment is about. Option --property of ebmc actually assumes
that a property is specified by name. So Matthias' fix does not work. Then a new regression test that Matthias put in directory 'non_inductive1' should be probably removed or rewritten.

[eigold]

Daniel,
I have made changes to use ebmc' --property option. However, this does not look too user-friendly.

1. Suppose I use a circuit root.sv with multiple properties. When I print out how properties are
   named in list 'properties' of ebmc_baset I get root.property.1, root.property.2, root.property.3 and so on.
   So ebmc seems to form the name of a property P by concatenation of 'root.property' with the string specifying the order number of P in 'root.sv'. The name of P used in 'root.sv' is IGNORED. So my original assumption seems to have been correct.

2. To verify the 25-th property listed in 'root.sv' using option --property I have to type in
   ebmc root.sv --ic3 --property root.property.25

So instead of just giving the order number of a property, one has to use the
lengthy prefix 'root.property'.

Eugene

[eigold]

I took a closer look and found out that the first part of the prefix specifies a module name rather
than a file name. (In my example, the file contained only one module that shared the file's name.) Indicating, the module name in a property name makes sense. Besides, if assertions have labels (as in Matthias' example), a property is specified by its label rather than the order number. So my original assumption is wrong in this case.

Still, the word 'property' in a property name seems to be redundant :-)
Eugene