Keyword: attribute

An attribute declares some practical aspect of the way an object is treated by the various Ivy commands. Typically these relate to code extraction.

Attributes may name a dot-separated object name prefix, in which case they apply only to the named object. If there is no prefix provided, they apply the object enclosing their declaration.

The following attributes are currently supported:

• weight: provides (as a double-quoted string) a floating-point weight between "0" and "1" that biases the execution of actions in an extracted randomized tester (as generated by ivy_to_cpp command)
• test: provides the name of an object to generate tests for, in an extracted randomized tester.
• method: specifies the preferred method of verifying an isolate. Equivalent to passing the method option on the command-line to ivy_check.
• separate: controls theory separation in model checking when using method=mc
• iterable: instructs code extraction to iterate over values of an uninterpreted type t in generated code by calling functions t.iter.create(int), t.iter.is_end(int), and t.iter.next(int).
• cardinality: instructs code extraction to calculate the cardinality of an uninterpreted type t in generated code by consulting variable t.cardinality, which should be an integer.
• radix: controls the output formatting of trace messages in extracted code. The only legal non-default value is 16, which causes printing in hexadecimal.
• override: specifies a sort to interpret an uninterpreted type as during code extraction.
• cppstd: specifies the C++ standard used in code extraction, the only legal non-default action is the symbol cpp11
• libspec: specifies a comma-separated list of libraries to link with the system linker when linking extracted code
• macro_finder: equivalent to passing the macro_finder option to ivy_check

Example:

object t = {
    attribute cardinality = 5
    attribute method = mc
}

attribute t.weight = "0.1"