ZLive (CZT ZLive 1.6-SNAPSHOT API)

java.lang.Object
- net.sourceforge.czt.animation.eval.ZLive

```
public class ZLive
extends Object
```
This is the main class of the ZLive animator. It can be used directly by other Java programs that want to evaluate Z terms. It is also used by TextUI, which provides a text-based user interface for ZLive, and it could also be used by a GUI class.

Author:

marku

Field Summary

Fields
Modifier and Type	Field and Description
`static int`	`INFER_PASSES` The maximum number of static inference passes done prior to mode checking and evaluation.
`protected FlatPredList`	`predlist_` Stores the code used in the most recent evaluation.
`protected net.sourceforge.czt.session.SectionManager`	`sectman_`

Constructor Summary

Constructors
Constructor and Description

ZLive()

Constructors
Constructor and Description
`ZLive()`

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`void`	`compile(ZLiveResult result)` Processes and compiles a term into internal FlatPred form.
`net.sourceforge.czt.z.ast.ZName`	`createNewName()` Generates a fresh temporary name.
`net.sourceforge.czt.z.ast.Expr`	`evalExpr(net.sourceforge.czt.z.ast.Expr expr)` Evaluate an Expr.
`net.sourceforge.czt.z.ast.Pred`	`evalPred(net.sourceforge.czt.z.ast.Pred pred)` Evaluate a Pred.
`net.sourceforge.czt.z.ast.Expr`	`evalSchema(String string, net.sourceforge.czt.z.ast.BindExpr expr)`
`ZLiveResult`	`evalTerm(boolean expr, net.sourceforge.czt.base.ast.Term term, Envir env0)` Evaluate an expression or predicate.
`void`	`evaluate(ZLiveResult result)` Evaluates a term that has already been preprocessed and compiled.
`static String`	`getBanner()` Returns the name and current version of ZLive.
`String`	`getCurrentSection()` Which section evaluations are being done in.
`net.sourceforge.czt.z.util.Factory`	`getFactory()` Returns the factory used for creating AST objects.
`Flatten`	`getFlatten()` Get a flatten visitor.
`int`	`getGivenSetSize()` The maximum size of each given set.
`net.sourceforge.czt.session.Markup`	`getMarkup()`
`Preprocess`	`getPreprocess()` Get the Preprocess object that is used to unfold terms before evaluation.
`double`	`getSearchSize()` Set the maximum acceptable cost for evaluating each FlatPredList.
`net.sourceforge.czt.session.SectionManager`	`getSectionManager()` Get the current section manager.
`static String`	`getVersion()` Returns the version number as a String, or "unknown" if an error occured when accessing the property containing the version information.
`static boolean`	`isNewName(net.sourceforge.czt.z.ast.ZName name)` Recognises the Names produced by createNewName.
`static void`	`main(String[] args)`
`void`	`printCode(FlatPredList code, PrintWriter writer)` Prints the given list of FlatPreds.
`void`	`printTerm(PrintStream out, net.sourceforge.czt.base.ast.Term term)` Print any term (evaluated or not), using the current markup.
`void`	`printTerm(PrintWriter writer, net.sourceforge.czt.base.ast.Term term)` Print any term (evaluated or not), using the current markup.
`void`	`printTerm(PrintWriter out, net.sourceforge.czt.base.ast.Term term0, net.sourceforge.czt.session.Markup markup)` Write an evaluated term.
`void`	`reset()` Reset the section manager that will be used during evaluation.
`void`	`resetNewNames()` This can be called to reset the new name counter to 0.
`net.sourceforge.czt.z.ast.Expr`	`schemaExpr(String schemaName)` Converts a schema name into an expression that can be evaluated.
`void`	`setCurrentSection(String sectName)` Sets the current section to the one whose name is sectName.
`void`	`setFactory(net.sourceforge.czt.z.util.Factory fact)` Sets the AST factory used for creating AST objects.
`void`	`setGivenSetSize(String value)` Set the maximum size of all given sets.
`void`	`setMarkup(net.sourceforge.czt.session.Markup markup)` Sets the markup that will be used to parse and print terms.
`void`	`setMarkup(String markup)`
`void`	`setSearchSize(double num)`
`void`	`setSearchSize(String str)`
`String`	`termToString(net.sourceforge.czt.base.ast.Term term)` Converts the given term to a String, using the current markup.
`String`	`termToString(net.sourceforge.czt.base.ast.Term term, net.sourceforge.czt.session.Markup markup)` Converts the given term to a String.
`void`	`typecheck(net.sourceforge.czt.base.ast.Term term)` Typechecks a term, to check its correctness and to reestablish the unique-ids invariant of bound variables.
`net.sourceforge.czt.z.ast.BindExpr`	`unprime(net.sourceforge.czt.z.ast.BindExpr expr)` Converts an output BindExpr to an input BindExpr.

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Field Detail
  - INFER_PASSES
```
public static final int INFER_PASSES
```
    The maximum number of static inference passes done prior to mode checking and evaluation.
    
    See Also:
    
    FlatPredList.inferBoundsFixPoint(Bounds,int), Constant Field Values
  - sectman_
```
protected net.sourceforge.czt.session.SectionManager sectman_
```
  - predlist_
```
protected FlatPredList predlist_
```
    Stores the code used in the most recent evaluation.
- Constructor Detail
  - ZLive
```
public ZLive()
```
- Method Detail
  - resetNewNames
```
public void resetNewNames()
```
    This can be called to reset the new name counter to 0. This should be done only before starting an evaluation that does not rely on the results of any previous evaluation (otherwise the same name might be generated twice).
  - createNewName
```
public net.sourceforge.czt.z.ast.ZName createNewName()
```
    Generates a fresh temporary name.
  - isNewName
```
public static boolean isNewName(net.sourceforge.czt.z.ast.ZName name)
```
    Recognises the Names produced by createNewName.
  - getFactory
```
public net.sourceforge.czt.z.util.Factory getFactory()
```
    Returns the factory used for creating AST objects.
  - setFactory
```
public void setFactory(net.sourceforge.czt.z.util.Factory fact)
```
    Sets the AST factory used for creating AST objects.
  - getPreprocess
```
public Preprocess getPreprocess()
```
    Get the Preprocess object that is used to unfold terms before evaluation.
  - getSectionManager
```
public net.sourceforge.czt.session.SectionManager getSectionManager()
```
    Get the current section manager.
  - reset
```
public void reset()
```
    Reset the section manager that will be used during evaluation. This clears all the specifications that have been loaded.
  - getFlatten
```
public Flatten getFlatten()
```
    Get a flatten visitor.
  - getMarkup
```
public net.sourceforge.czt.session.Markup getMarkup()
```
  - setMarkup
```
public void setMarkup(net.sourceforge.czt.session.Markup markup)
```
    Sets the markup that will be used to parse and print terms.
  - setMarkup
```
public void setMarkup(String markup)
```
    Throws:
    
    IllegalArgumentException - if the given markup is not supported.
  - getGivenSetSize
```
public int getGivenSetSize()
```
    The maximum size of each given set. This is effectively infinite (actually Integer.MAX_VALUE) by default.
  - setGivenSetSize
```
public void setGivenSetSize(String value)
```
    Set the maximum size of all given sets. Note that this setting restricts on the semantics of the specification, so small values are likely to change the results of evaluations.
    
    Throws:
    
    NumberFormatException - if the argument string is not a positive integer.
  - getSearchSize
```
public double getSearchSize()
```
    Set the maximum acceptable cost for evaluating each FlatPredList. If the chosen mode has more solutions this, then an exception will be thrown before evaluation starts.
  - setSearchSize
```
public void setSearchSize(double num)
```
  - setSearchSize
```
public void setSearchSize(String str)
```
  - getCurrentSection
```
public String getCurrentSection()
```
    Which section evaluations are being done in.
  - setCurrentSection
```
public void setCurrentSection(String sectName)
                       throws net.sourceforge.czt.session.CommandException
```
    Sets the current section to the one whose name is sectName. It parses and typechecks the section first. If sectName is null or empty, a reset is done instead.
    
    Throws:
    
    net.sourceforge.czt.session.CommandException
  - evalPred
```
public net.sourceforge.czt.z.ast.Pred evalPred(net.sourceforge.czt.z.ast.Pred pred)
                                        throws EvalException
```
    Evaluate a Pred. This throws some kind of EvalException if pred is too difficult to evaluate or contains an undefined expression. The input predicate must have been type checked.
    
    Parameters:
    
    pred - A net.sourceforge.czt.z.ast.Pred object.
    
    Returns:
    
    Usually an instance of TruePred or FalsePred.
    
    Throws:
    
    EvalException
  - evalExpr
```
public net.sourceforge.czt.z.ast.Expr evalExpr(net.sourceforge.czt.z.ast.Expr expr)
                                        throws EvalException
```
    Evaluate an Expr. This throws some kind of EvalException if expr is too difficult to evaluate or contains an undefined expression. The input expression must be type checked.
    
    Parameters:
    
    expr - A net.sourceforge.czt.z.ast.Expr object.
    
    Returns:
    
    Usually an instance of EvalSet, or some other expr.
    
    Throws:
    
    EvalException
  - evalTerm
```
public ZLiveResult evalTerm(boolean expr,
                            net.sourceforge.czt.base.ast.Term term,
                            Envir env0)
```
    Evaluate an expression or predicate.
  - compile
```
public void compile(ZLiveResult result)
```
    Processes and compiles a term into internal FlatPred form. This fills in the unfoldterm, code and mode parts of result.
    
    Parameters:
    
    result - resultgetOriginalTerm() is the term to be compiled.
  - evaluate
```
public void evaluate(ZLiveResult result)
```
    Evaluates a term that has already been preprocessed and compiled. This fills in the getResult() part of result.
    
    Parameters:
    
    result - the code and mode must be already set.
  - schemaExpr
```
public net.sourceforge.czt.z.ast.Expr schemaExpr(String schemaName)
                                          throws EvalException,
                                                 net.sourceforge.czt.session.CommandException
```
    Converts a schema name into an expression that can be evaluated. The schema name is looked up in the definition table of the current section.
    
    Parameters:
    
    schemaName - The undecorated name of a schema.
    
    Returns:
    
    The expression that defines the schema.
    
    Throws:
    
    net.sourceforge.czt.util.CztException - if schemaName is not defined.
    
    EvalException
    
    net.sourceforge.czt.session.CommandException
  - typecheck
```
public void typecheck(net.sourceforge.czt.base.ast.Term term)
               throws EvalException,
                      net.sourceforge.czt.typecheck.z.util.TypeErrorException
```
    Typechecks a term, to check its correctness and to reestablish the unique-ids invariant of bound variables. (bound vars with the same name and scope must have the same id.)
    
    Throws:
    
    EvalException
    
    net.sourceforge.czt.typecheck.z.util.TypeErrorException
  - printCode
```
public void printCode(FlatPredList code,
                      PrintWriter writer)
```
    Prints the given list of FlatPreds.
  - printTerm
```
public void printTerm(PrintStream out,
                      net.sourceforge.czt.base.ast.Term term)
```
    Print any term (evaluated or not), using the current markup.
  - printTerm
```
public void printTerm(PrintWriter writer,
                      net.sourceforge.czt.base.ast.Term term)
```
    Print any term (evaluated or not), using the current markup.
  - printTerm
```
public void printTerm(PrintWriter out,
                      net.sourceforge.czt.base.ast.Term term0,
                      net.sourceforge.czt.session.Markup markup)
```
    Write an evaluated term. The output will be in LaTeX or Unicode format, according to the current markup setting (see getMarkup()). Internal ZLive evaluation results, such as EvalSets (which may contain infinite sets), are converted into standard Z constructs before they are printed. For example, each EvalSet enumerates a maximum number of elements (see the setEvalSetSize methods in the ResultTreeToZVisitor class) and then prints "..." if there are more elements remaining.
  - termToString
```
public String termToString(net.sourceforge.czt.base.ast.Term term,
                           net.sourceforge.czt.session.Markup markup)
```
    Converts the given term to a String.
  - termToString
```
public String termToString(net.sourceforge.czt.base.ast.Term term)
```
    Converts the given term to a String, using the current markup.
  - getBanner
```
public static String getBanner()
```
    Returns the name and current version of ZLive.
  - getVersion
```
public static String getVersion()
```
    Returns the version number as a String, or "unknown" if an error occured when accessing the property containing the version information.
  - main
```
public static void main(String[] args)
```
  - unprime
```
public net.sourceforge.czt.z.ast.BindExpr unprime(net.sourceforge.czt.z.ast.BindExpr expr)
```
    Converts an output BindExpr to an input BindExpr. That is, it throws away all entries whose names do not end with a prime, and removes one prime from the entries that do end with a prime.
    
    Parameters:
    
    expr - Eg. <| x==1, x'==2, y''==3, i?==4, o!==5 |>
    
    Returns:
    
    Eg. <| x==2, y'==3 |>
  - evalSchema
```
public net.sourceforge.czt.z.ast.Expr evalSchema(String string,
                                                 net.sourceforge.czt.z.ast.BindExpr expr)
                                          throws net.sourceforge.czt.session.CommandException
```
    Throws:
    
    net.sourceforge.czt.session.CommandException

Class ZLive

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

INFER_PASSES

sectman_

predlist_

Constructor Detail

ZLive

Method Detail

resetNewNames

createNewName

isNewName

getFactory

setFactory

getPreprocess

getSectionManager

reset

getFlatten

getMarkup

setMarkup

setMarkup

getGivenSetSize

setGivenSetSize

getSearchSize

setSearchSize

setSearchSize

getCurrentSection

setCurrentSection

evalPred

evalExpr

evalTerm

compile

evaluate

schemaExpr

typecheck

printCode

printTerm

printTerm

printTerm

termToString

termToString

getBanner

getVersion

main

unprime

evalSchema