Home • Docs • Download • FM Tools
Yices

Yices 1 is no longer maintained. You can still download it and use it, but we do not provide support for Yices 1.

Our more recent Yices 2 solver is here

Yices 1 C API Lite


Typedefs

typedef void * yicesl_context

Functions

const  char * yicesl_version ()
 Return the yices version number.
void yicesl_set_verbosity (int l)
 Set the verbosity level.
void yicesl_enable_type_checker (int flag)
 Force Yices to type check expressions when they are asserted (default = false).
int yicesl_enable_log_file (const 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.
int yicesl_set_output_file (const 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.
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, const 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.
const  char * yicesl_get_last_error_message ()
 Return the last error message produced by the logical context.

Typedef Documentation

typedef void* yicesl_context
 

Pointer to a Yices logical context.

Function Documentation

const char* yicesl_version (   ) 
 

Return the yices version number.

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.

void yicesl_enable_type_checker (  int  flag  ) 
 

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

int yicesl_enable_log_file (  const  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.

Returns:
one of the following codes
  • 1 if the operation succeeded
  • 0 if there's already a log file
  • -1 if there was an error while trying to open the file
int yicesl_set_output_file (  const  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.

If the file can be opened then it replaces the current ouput file. The latter, if different from stdout, is closed first.

If the file can't be opened then the current output file is kept.

Returns:
a non-zero value if the file can be opened and used for output, or 0 if the file can't be opened.
yicesl_context yicesl_mk_context (   ) 
 

Create a logical context.

void yicesl_del_context (  yicesl_context  ctx  ) 
 

Delete the given logical context.

See also:
yicesl_mk_context
int yicesl_read (  yicesl_context  ctx,
const  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 or 0 if the command failed. Function yicesl_get_last_error_message can be used to retrieve the error message.
int yicesl_inconsistent (  yicesl_context  ctx  ) 
 

Return true if the given logical context is known to be inconsistent.

If the function returns true (i.e., a non-zero value) then the context is known to be inconsistent.

If it returns false (i.e., 0) then the context status is not known. In such a case, one must use command (check) to determine whether the context is satisfiable,

const  char* yicesl_get_last_error_message (   ) 
 

Return the last error message produced by the logical context.

Home • Docs • Download • FM Tools