Symbolic Simulator Operations¶

grackle_fresh¶

uint8_t grackle_fresh_uint8( const char* name )
uint16_t grackle_fresh_uint16( const char* name )
uint32_t grackle_fresh_uint32( const char* name )
uint64_t grackle_fresh_uint64( const char* name )
float grackle_fresh_float( const char* name )
double grackle_fresh_double( const char* name )

This family of functions provides access to fresh symbolic values. When executed in Grackle, these functions generate a fresh uninterpreted constant of the appropriate type, which is returned.

A name may be supplied, which can later be used to refer to the symbolic constant. The name argument must either be a null pointer (in which case no name is assigned), or a nonnull concrete string.

Although these functions only return unsigned integer types, they may be freely cast to signed integers if desired.

grackle_fresh_array¶

uint8_t*  grackle_fresh_uint8_array ( const char* name, uint32_t num )
uint16_t* grackle_fresh_uint16_array( const char* name, uint32_t num )
uint32_t* grackle_fresh_uint32_array( const char* name, uint32_t num )
uint64_t* grackle_fresh_uint64_array( const char* name, uint32_t num )
float*    grackle_fresh_float_array ( const char* name, uint32_t num )
double*   grackle_fresh_double_array( const char* name, uint32_t num )

This family of functions produce arrays of fresh symbolic values. These functions allocate a fresh array on the heap filled with symbolic values of the appropriate type. The number of elements in the array is determined by the second argument, num.

A name may be supplied, which can later be used to refer to the symbolic array. The name argument must either be a null pointer (in which case no name is assigned), or a nonnull concrete string.

Although these functions only return unsigned integer types, they may be freely cast to signed integers if desired.

If desired, the arrays returned by these functions may safely be passed to free. However, the simulator will retain internal resources related to the fresh constants even if the heap memory in which they were stored is released.

grackle_print_symbolic¶

void grackle_print_symbolic_uint8( uint8_t sym )
void grackle_print_symbolic_uint16( uint16_t sym )
void grackle_print_symbolic_uint32( uint32_t sym )
void grackle_print_symbolic_uint64( uint64_t sym )
void grackle_print_symbolic_float( float sym )
void grackle_print_symbolic_double( double sym )
void grackle_print_symbolic_pointer( void* sym )

This family of functions prints the symbolic representation of the given symbolic value onto the standard output stream.

grackle_check_sat¶

struct grackle_model* grackle_check_sat( uint32_t pred )

This function is the primary interface to Grackle’s constraint solving capabilities. Given an integer value to interpret as a boolean (0 for false, nonzero for true), ask the currently-configured solver to check the satisfiability of the given predicate.

If the predicate is unsatisfiable, a null pointer will be returned. Otherwise a nonnull pointer of the opaque type struct grackle_model will be returned. This pointer can be used to access the satisfying assignment calculated by the underlying constraint solver using the grackle_model_get family of functions.

struct grackle_model pointers are opaque handles and should only be passed into further Grackle API functions. Trying to load or store through such pointers will fail. The returned pointer may be passed to free, which will release the simulator resources associated with the model.

grackle_check_sat_raw¶

struct grackle_model* grackle_check_sat_raw( uint32_t pred )

This function behaves exactly the same as grackle_check_sat, except that the given predicate is passed into the underlying solver totally unmodified. In particular, the current path-conditions are not added to the query.

This is the correct variant of check sat to use if one is manually proving proof obligations retrieved from the grackle_proof_obligations. Otherwise, previously-asserted predicates will be automatically assumed, and the proof obligations will follow vacuously.

grackle_model_get¶

uint8_t grackle_model_get_uint8( struct grackle_model*, const char* name )
uint16_t grackle_model_get_uint16( struct grackle_model*, const char* name )
uint32_t grackle_model_get_uint32( struct grackle_model*, const char* name )
uint64_t grackle_model_get_uint64( struct grackle_model*, const char* name )
float grackle_model_get_float( struct grackle_model*, const char* name )
double grackle_model_get_double( struct grackle_model*, const char* name )

This family of functions retrieves the concrete assignment made by underlying solver in a previous call to grackle_check_sat for scalar variables (those declared using the grackle_fresh family of functions).

These functions will fail if grackle_model is the null pointer; if name does not refer to some previously generated symbolic value; or if the type of the value referred to by name does not match the type expected by the accessor function.

The model and name arguments to these functions must be concrete.

grackle_model_get_array¶

uint8_t*  grackle_model_get_uint8_array ( struct grackle_model* mdl, const char* name, uint32_t* num )
uint16_t* grackle_model_get_uint16_array( struct grackle_model* mdl, const char* name, uint32_t* num )
uint32_t* grackle_model_get_uint32_array( struct grackle_model* mdl, const char* name, uint32_t* num )
uint64_t* grackle_model_get_uint64_array( struct grackle_model* mdl, const char* name, uint32_t* num )
float*    grackle_model_get_float_array ( struct grackle_model* mdl, const char* name, uint32_t* num )
double*   grackle_model_get_double_array( struct grackle_model* mdl, const char* name, uint32_t* num )

This family of functions allocate fresh arrays on the heap, into which are copied the concrete values chosen by the underlying solver in a previous call to grackle_check_sat for array variables (those declared using the grackle_fresh_array family of functions). The returned array will have the same size as the original array generated by grackle_fresh_array. If num is a nonnull pointer, the number of elements in the array will be stored into the given pointer.

These functions will fail if grackle_model is the null pointer; if name does not refer to some previously generated symbolic value; or if the type of the value referred to by name does not match the type expected by the accessor function.

The model and name arguments to these functions must be concrete.

The arrays returned by these functions may be safely passed to free.

grackle_print_model¶

void grackle_print_model( struct grackle_model* )

Print the given model on the standard output stream, using a default formatting scheme.

The model argument to this function must be concrete.

grackle_proof_obligations¶

uint32_t* grackle_proof_obligations( uint32_t* num )

Construct an array containing the currently-outstanding proof obligations. The number of elements of this array will be written into the memory location pointed to by num.

The returned proof obligations are given in negated-goal form, so that the proof is completed if UNSAT is returned on a check sat query.

NOTE: one should use the grackle_check_sat_raw variant to discharge proof obligations. Otherwise, the current path assumptions may cause the proof to succeed vacuously.

grackle_prove_obligations¶

uint32_t grackle_prove_obligations( void )

grackle_prove_obligations passes each of the currently outstanding proof obligations to the default solver. Any obligations which are proved are removed from the list. Any obligations which are disproved are printed together with their counterexamples.

Afterward, a short summary message is printed which indicates: how many total proofs were attempted; how many were succesfully proved; how many were falsified with a counterexample; and how many were inconclusive.

The return value indicates the number of proof obligations that remain after all proof attempts are complete. This count includes both proof obligations that were falsified and those which were inconclusive. In particular, if the return value is 0, all proof attempts were successful.

Calls to grackle_assert and the use of partial operations generate proof obligatons.

grackle_write_smtlib2¶

void grackle_write_smtlib2( uint32_t pred, const char *filename )

Given an integer pred to interpret as a boolean (in the same way as check_sat), write a SMTLib2-formatted description of the problem into filename.

The filename argument to this function must be concrete. This function will fail if it cannot write the file for some reason.

grackle_write_yices¶

void grackle_write_yices( uint32_t pred, const char *filename )

Given an integer pred to interpret as a boolean (in the same way as check_sat), write a description of the problem into filename, formatted using the Yices native input language.

The filename argument to this function must be concrete. This function will fail if it cannot write the file for some reason.

grackle_assume¶

void grackle_assume( uint32_t pred )

Given an integer pred to interpret as a boolean, assume the given predicate. This adds the predicate to the current path condition and does not generate any verification obligations. If pred evaluates to the concrete false value, a warning will be generated.

grackle_assert¶

void grackle_assert( uint32_t pred )

Given an integer pred to interpret as a boolean, assert the given predicate. This adds the predicate to the current path condition and generates a delayed proof obligation. If pred evaluates to the concrete false value, an error will be generated listing the location of the assertion and the expression that was asserted.