Home • Intro • Docs • Wiki • FAQ • Download - Mail • Awards • Status • FM Tools
Yices

C API Lite


Typedefs

typedef void * yicesl_context

Functions

void yicesl_set_verbosity (int l)
 Set the verbosity level.
char * yicesl_version ()
 Return the yices version number.
void yicesl_enable_type_checker (int flag)
 Force Yices to type check expressions when they are asserted (default = false).
void yicesl_enable_log_file (char *file_name)
 Enable a log file that will store the assertions, checks, decls, etc. If the log file is already open, then nothing happens.
yicesl_context yicesl_mk_context ()
 Create a logical context.
void yicesl_del_context (yicesl_context ctx)
 Delete the given logical context.
int yicesl_read (yicesl_context ctx, char *cmd)
 Process the given command in the given logical context. The command must use Yices input language.
int yicesl_inconsistent (yicesl_context ctx)
 Return true if the given logical context is inconsistent.
char * yicesl_get_last_error_message ()
 Return the last error message produced by the logical context.
void yicesl_set_output_file (char *file_name)
 Set the file that will store the output produced by yices (e.g., models). The default behavior is to send the output to standard output.

Typedef Documentation

typedef void* yicesl_context
 

Pointer to a Yices logical context.

Function Documentation

int yicesl_read (  yicesl_context  ctx,
char *  cmd
) 
 

Process the given command in the given logical context. The command must use Yices input language.

Returns:
a non-zero value if the command succeeds, and 0 if the command failed. Function yicesl_get_last_error_message can be used to retrieve the error message.

void yicesl_del_context (  yicesl_context  ctx  ) 
 

Delete the given logical context.

See also:
yicesl_mk_context

void yicesl_enable_log_file (  char *  file_name  ) 
 

Opens a log file that will store the assertions, checks, declarations, etc. If the log file is already open, then nothing happens.

void yicesl_enable_type_checker (  int  flag  ) 
 

Force Yices to type check expressions when they are asserted (default = false).

char* yicesl_get_last_error_message (   ) 
 

Return the last error message produced by the logical context.

int yicesl_inconsistent (  yicesl_context  ctx  ) 
 

Return true if the given logical context is inconsistent.

yicesl_context yicesl_mk_context (   ) 
 

Create a logical context.

void yicesl_set_output_file (  char *  file_name  ) 
 

Set the file that will store the output produced by yices (e.g., models). The default behavior is to send the output to standard output.

void yicesl_set_verbosity (  int  l  ) 
 

Set the verbosity level. The default level is 0.

At verbosity level 0, Yices does not print anything during processing. Increasing the level causes Yices to print some (or a lot of) information.

char* yicesl_version (   ) 
 

Return the yices version number.

Home • Intro • Docs • Wiki • FAQ • Download - Mail • Awards • Status • FM Tools

Last modified: Mon 18 Sep 2006 10:59 PDT