yices
Class YicesLite

java.lang.Object
  extended by yices.YicesLite

public class YicesLite
extends java.lang.Object

This is the YicesLite Java API built on top of the existing C API

Author:
Sokharith Sok

Constructor Summary
YicesLite()
           
 
Method Summary
 void yicesl_del_context(int ctx)
          Delete an existing context ctx
 void yicesl_enable_log_file(java.lang.String filename)
          Log all the yices command executed into filename.
 void yicesl_enable_type_checker(short flag)
          Enable the type checker
 java.lang.String yicesl_get_last_error_message()
          Get the last error message
 int yicesl_inconsistent(int ctx)
          Check the inconsistency of the current logical context ctx
 int yicesl_mk_context()
          Create new context
 int yicesl_read(int ctx, java.lang.String cmd)
          Run the yices command
 void yicesl_set_output_file(java.lang.String filename)
          Log the output to a file, filename
 void yicesl_set_verbosity(short l)
          This method use to set the verbosity level
 java.lang.String yicesl_version()
          Get the version of the yices engine
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

YicesLite

public YicesLite()
Method Detail

yicesl_set_verbosity

public void yicesl_set_verbosity(short l)
This method use to set the verbosity level

Parameters:
l - the verbosity level

yicesl_version

public java.lang.String yicesl_version()
Get the version of the yices engine

Returns:
the String version of yices

yicesl_enable_type_checker

public void yicesl_enable_type_checker(short flag)
Enable the type checker

Parameters:
flag - to enable the type checker Note: flag: 0 means disable and not 0 is enable

yicesl_enable_log_file

public void yicesl_enable_log_file(java.lang.String filename)
Log all the yices command executed into filename.

Parameters:
filename -

yicesl_mk_context

public int yicesl_mk_context()
Create new context

Returns:
the logical context reference number

yicesl_del_context

public void yicesl_del_context(int ctx)
Delete an existing context ctx

Parameters:
ctx - delete the logical context reference number ctx

yicesl_read

public int yicesl_read(int ctx,
                       java.lang.String cmd)
Run the yices command

Parameters:
ctx - the logical context reference number
cmd - the commnad in the yices input language format
Returns:
zero if fail.

yicesl_inconsistent

public int yicesl_inconsistent(int ctx)
Check the inconsistency of the current logical context ctx

Parameters:
ctx - check inconsistency in the logical context
Returns:
zero if there is abnormalie, otherwise non-zero integer

yicesl_get_last_error_message

public java.lang.String yicesl_get_last_error_message()
Get the last error message

Returns:
get the last message error produced

yicesl_set_output_file

public void yicesl_set_output_file(java.lang.String filename)
Log the output to a file, filename

Parameters:
filename - write output to the file, filename, instead of standard ouput of the system