net.sourceforge.czt.zeves

Class ZEvesApi

java.lang.Object

net.sourceforge.czt.zeves.ZEvesApi

public class ZEvesApi
extends Object

This class is provides calls to Z/EVES XML-based API, where communication is done via sockets. It allows one to connect to the Z/EVES server (e.g. running on localhost:6789 by default) and perform specific commands or run proof scripts. Z/EVES responses are translated into Java objects, which are returned to the caller. This class provides synchronization on writing/reading to the socket, so can be used in a parallel execution. Use available class methods to perform commands or send the preformatted XML commands via send(String).

Author:

Andrius Velykis

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	ZEvesApi.ZEvesTheoremType

Constructor Summary

Constructors

Constructor and Description
ZEvesApi(String zEvesServerAddress, int port)

Method Summary

Modifier and Type	Method and Description
void	back()
void	back(int numberOfSteps)
void	close()
void	connect()
boolean	connectRetry(int retries)
void	disconnect()
String	getCurrentGoalName()
int	getGoalProofLength(String goalName)
ZEvesOutput	getGoalProofStep(String goalName, int stepNumber)
boolean	getGoalProvedState(String goalName)
Object	getHistoryElement(int paragraphNumber)
int	getHistoryLength()
int	getNameSource(String name) Queries Z/EVES for the source paragraph (submitted by the user) introducing the given name.
int	getPort()
List<String>	getRulesMatchingExpression(String goalName, int stepNumber, String expr)
List<String>	getRulesMatchingPredicate(String goalName, int stepNumber, String predicate)
String	getServerAddress()
ZEvesTheorem	getTheorem(String theoremName) Queries Z/EVES for theorem contents.
Map<String,ZEvesApi.ZEvesTheoremType>	getTheoremNames(int paragraphNumber)
int	getTheoremOrigin(String theoremName)
boolean	isConnected()
void	reset()
void	retry()
ZEvesOutput	send(String command) Sends a command to the server, formatted as specified in Z/EVES XML API requirements.
void	sendAbort() Sends an abort command to stop executing current command.
ZEvesOutput	sendCommand(String cmdName, String... args) Sends the indicated command to the server, passing arguments as command contents.
ZEvesOutput	sendProofCommand(String command)
void	setCurrentGoalName(String goalName)
boolean	tryConnecting(int retries)
void	undoBackThrough(int paragraphNumber)
void	undoBackTo(int paragraphNumber)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

ZEvesApi

public ZEvesApi(String zEvesServerAddress,
                int port)

Method Detail

getServerAddress

public String getServerAddress()

getPort

public int getPort()

connect

public void connect()
             throws ConnectException,
                    IOException

Throws:

ConnectException

IOException

disconnect

public void disconnect()
                throws IOException

Throws:

IOException

connectRetry

public boolean connectRetry(int retries)
                     throws IOException

Throws:

IOException

tryConnecting

public boolean tryConnecting(int retries)
                      throws IOException

Throws:

IOException

close

public void close()
           throws IOException

Throws:

IOException

isConnected

public boolean isConnected()

send

public ZEvesOutput send(String command)
                 throws ZEvesException

Sends a command to the server, formatted as specified in Z/EVES XML API requirements.

Parameters:

command - formatted Z/EVES XML command

Returns:

result as Java object

Throws:

ZEvesException - if command produced an error (zerror) or communication failed

sendAbort

public void sendAbort()

Sends an abort command to stop executing current command. This can be done asynchronously, while waiting for reply from Z/EVES. The executing command still produces an output, even if it was aborted.

sendCommand

public ZEvesOutput sendCommand(String cmdName,
                               String... args)
                        throws ZEvesException

Sends the indicated command to the server, passing arguments as command contents.

Parameters:

cmdName - Z/EVES XML command name

args - arguments to be passed as command contents. They will be separated by white-space.

Returns:

result as Java object

Throws:

ZEvesException - if command produced an error (zerror) or communication failed

getHistoryLength

public int getHistoryLength()
                     throws ZEvesException

Throws:

ZEvesException

getHistoryElement

public Object getHistoryElement(int paragraphNumber)
                         throws ZEvesException

Throws:

ZEvesException

getTheoremNames

public Map<String,ZEvesApi.ZEvesTheoremType> getTheoremNames(int paragraphNumber)
                                                      throws ZEvesException

Throws:

ZEvesException

getTheorem

public ZEvesTheorem getTheorem(String theoremName)
                        throws ZEvesException

Queries Z/EVES for theorem contents.

Parameters:

theoremName - name of theorem

Returns:

Theorem definition as represented in Z/EVES, or null if the theorem does not exist in Z/EVES

Throws:

ZEvesException - if there are communications errors or Z/EVES errors

getNameSource

public int getNameSource(String name)
                  throws ZEvesException

Queries Z/EVES for the source paragraph (submitted by the user) introducing the given name.

Parameters:

name - name of Z/EVES construct

Returns:

source paragraph, as counted in Z/EVES, that introduces the given name, or -1 if the name is unknown (or the name was introduced in the mathematical toolkit)

Throws:

ZEvesException - if there are communications errors or Z/EVES errors

getTheoremOrigin

public int getTheoremOrigin(String theoremName)
                     throws ZEvesException

Throws:

ZEvesException

getRulesMatchingPredicate

public List<String> getRulesMatchingPredicate(String goalName,
                                              int stepNumber,
                                              String predicate)
                                       throws ZEvesException

Throws:

ZEvesException

getRulesMatchingExpression

public List<String> getRulesMatchingExpression(String goalName,
                                               int stepNumber,
                                               String expr)
                                        throws ZEvesException

Throws:

ZEvesException

getCurrentGoalName

public String getCurrentGoalName()
                          throws ZEvesException

Throws:

ZEvesException

getGoalProvedState

public boolean getGoalProvedState(String goalName)
                           throws ZEvesException

Throws:

ZEvesException

getGoalProofLength

public int getGoalProofLength(String goalName)
                       throws ZEvesException

Throws:

ZEvesException

getGoalProofStep

public ZEvesOutput getGoalProofStep(String goalName,
                                    int stepNumber)
                             throws ZEvesException

Throws:

ZEvesException

reset

public void reset()
           throws ZEvesException

Throws:

ZEvesException

undoBackTo

public void undoBackTo(int paragraphNumber)
                throws ZEvesException

Throws:

ZEvesException

undoBackThrough

public void undoBackThrough(int paragraphNumber)
                     throws ZEvesException

Throws:

ZEvesException

setCurrentGoalName

public void setCurrentGoalName(String goalName)
                        throws ZEvesException

Throws:

ZEvesException

sendProofCommand

public ZEvesOutput sendProofCommand(String command)
                             throws ZEvesException

Throws:

ZEvesException

back

public void back()
          throws ZEvesException

Throws:

ZEvesException

back

public void back(int numberOfSteps)
          throws ZEvesException

Throws:

ZEvesException

retry

public void retry()
           throws ZEvesException

Throws:

ZEvesException