A B C D E F G H I J L M N O P R S T U V X

A

AbstractOracle - Class in net.sourceforge.czt.rules.oracles

AbstractOracle() - Constructor for class net.sourceforge.czt.rules.oracles.AbstractOracle

accept(Visitor<R>) - Method in class net.sourceforge.czt.rules.ast.EmptyDeclListImpl

addRulePara(RulePara) - Method in class net.sourceforge.czt.rules.RuleTable

addRuleParas(RuleTable) - Method in class net.sourceforge.czt.rules.RuleTable

addRuleParas(List<RulePara>) - Method in class net.sourceforge.czt.rules.RuleTable

AddRuleVisitor(RewriteVisitor.RewriteRule) - Constructor for class net.sourceforge.czt.rules.rewriter.RewriteVisitor.AddRuleVisitor

apply(Term) - Static method in class net.sourceforge.czt.rules.ast.TermToString

apply(RulePara, Sequent) - Static method in class net.sourceforge.czt.rules.prover.SimpleProver

apply(Rule, Sequent) - Static method in class net.sourceforge.czt.rules.prover.SimpleProver

Tries to apply a given Rule to a given Sequent.

apply(Oracle, Sequent) - Static method in class net.sourceforge.czt.rules.prover.SimpleProver

Tries to apply a given Oracle to a given Sequent.

apply(Term) - Method in class net.sourceforge.czt.rules.rewriter.RewriteVisitor.RewriteRule

apply2(RulePara, Sequent) - Static method in class net.sourceforge.czt.rules.prover.SimpleProver

apply2(Rule, Sequent) - Static method in class net.sourceforge.czt.rules.prover.SimpleProver

apply2(Oracle, Sequent) - Static method in class net.sourceforge.czt.rules.prover.SimpleProver

AstToPrintTreeVisitor - Class in net.sourceforge.czt.rules.print

AstToPrintTreeVisitor(SectionInfo) - Constructor for class net.sourceforge.czt.rules.print.AstToPrintTreeVisitor

B

bind(Term) - Method in class net.sourceforge.czt.rules.ast.ProverJokerDeclList

bind(Term) - Method in class net.sourceforge.czt.rules.ast.ProverJokerExpr

bind(Term) - Method in class net.sourceforge.czt.rules.ast.ProverJokerExprList

bind(Term) - Method in class net.sourceforge.czt.rules.ast.ProverJokerName

bind(Term) - Method in class net.sourceforge.czt.rules.ast.ProverJokerNameList

bind(Term) - Method in class net.sourceforge.czt.rules.ast.ProverJokerPred

bind(Term) - Method in class net.sourceforge.czt.rules.ast.ProverJokerRenameList

bind(Term) - Method in class net.sourceforge.czt.rules.ast.ProverJokerStroke

bind(Term) - Method in interface net.sourceforge.czt.rules.Joker

boundTo() - Method in class net.sourceforge.czt.rules.ast.ProverJokerDeclList

boundTo() - Method in class net.sourceforge.czt.rules.ast.ProverJokerExpr

boundTo() - Method in class net.sourceforge.czt.rules.ast.ProverJokerExprList

boundTo() - Method in class net.sourceforge.czt.rules.ast.ProverJokerName

boundTo() - Method in class net.sourceforge.czt.rules.ast.ProverJokerNameList

boundTo() - Method in class net.sourceforge.czt.rules.ast.ProverJokerPred

boundTo() - Method in class net.sourceforge.czt.rules.ast.ProverJokerRenameList

boundTo() - Method in class net.sourceforge.czt.rules.ast.ProverJokerStroke

boundTo() - Method in interface net.sourceforge.czt.rules.Joker

C

check(List<? extends Term>, SectionManager, String) - Method in class net.sourceforge.czt.rules.oracles.AbstractOracle

Returns null if the check fails, the set of bindings if it succeeds.

check(List<? extends Term>, SectionManager, String) - Method in class net.sourceforge.czt.rules.oracles.DecorateOracle

check(List<? extends Term>, SectionManager, String) - Method in class net.sourceforge.czt.rules.oracles.HideOracle

check(List<? extends Term>, SectionManager, String) - Method in class net.sourceforge.czt.rules.oracles.LookupOracle

check(List<? extends Term>, SectionManager, String) - Method in class net.sourceforge.czt.rules.oracles.RenameOracle

check(List<? extends Term>, SectionManager, String) - Method in class net.sourceforge.czt.rules.oracles.SchemaMinusOracle

Implements the [D1|true] schemaminus [D2|true] oracle.

check(List<? extends Term>, SectionManager, String) - Method in class net.sourceforge.czt.rules.oracles.SplitNamesOracle

check(List<? extends Term>, SectionManager, String) - Method in class net.sourceforge.czt.rules.oracles.ThetaOracle

check(List<? extends Term>, SectionManager, String) - Method in class net.sourceforge.czt.rules.oracles.TypecheckOracle

check(List<? extends Term>, SectionManager, String) - Method in class net.sourceforge.czt.rules.oracles.UnprefixOracle

check(List<? extends Term>, SectionManager, String) - Method in class net.sourceforge.czt.rules.oracles.XiOracle

ChildExtractor - Class in net.sourceforge.czt.rules.unification

A visitor that extracts the children of a given term suitable for unification.

ChildExtractor() - Constructor for class net.sourceforge.czt.rules.unification.ChildExtractor

collectBindings(Sequent, List<Binding>) - Static method in class net.sourceforge.czt.rules.prover.ProverUtils

collectConjectures(Term) - Static method in class net.sourceforge.czt.rules.prover.ProverUtils

collectJokers(Term) - Static method in class net.sourceforge.czt.rules.prover.ProverUtils

CollectStateVariablesVisitor - Class in net.sourceforge.czt.rules.oracles

A visitor for collecting all ZNames in some schema text.

CollectStateVariablesVisitor() - Constructor for class net.sourceforge.czt.rules.oracles.CollectStateVariablesVisitor

compute(String, SectionManager) - Method in class net.sourceforge.czt.rules.RuleTableCommand

contains(Term, Joker) - Method in class net.sourceforge.czt.rules.unification.OccursCheckVisitor

True iff term contains joker.

copy(Term, Factory) - Static method in class net.sourceforge.czt.rules.prover.SimpleProver

CopyVisitor - Class in net.sourceforge.czt.rules

A visitor that copies a term using the given factory.

CopyVisitor() - Constructor for class net.sourceforge.czt.rules.CopyVisitor

CopyVisitor(Factory) - Constructor for class net.sourceforge.czt.rules.CopyVisitor

create(Object[]) - Method in class net.sourceforge.czt.rules.ast.EmptyDeclListImpl

create(Object[]) - Method in class net.sourceforge.czt.rules.ast.ProverJokerDeclList

create(Object[]) - Method in class net.sourceforge.czt.rules.ast.ProverJokerDeclListBinding

create(Object[]) - Method in class net.sourceforge.czt.rules.ast.ProverJokerExpr

create(Object[]) - Method in class net.sourceforge.czt.rules.ast.ProverJokerExprBinding

create(Object[]) - Method in class net.sourceforge.czt.rules.ast.ProverJokerExprList

create(Object[]) - Method in class net.sourceforge.czt.rules.ast.ProverJokerExprListBinding

create(Object[]) - Method in class net.sourceforge.czt.rules.ast.ProverJokerName

create(Object[]) - Method in class net.sourceforge.czt.rules.ast.ProverJokerNameBinding

create(Object[]) - Method in class net.sourceforge.czt.rules.ast.ProverJokerNameList

create(Object[]) - Method in class net.sourceforge.czt.rules.ast.ProverJokerNameListBinding

create(Object[]) - Method in class net.sourceforge.czt.rules.ast.ProverJokerPred

create(Object[]) - Method in class net.sourceforge.czt.rules.ast.ProverJokerPredBinding

create(Object[]) - Method in class net.sourceforge.czt.rules.ast.ProverJokerRenameList

create(Object[]) - Method in class net.sourceforge.czt.rules.ast.ProverJokerRenameListBinding

create(Object[]) - Method in class net.sourceforge.czt.rules.ast.ProverJokerStroke

create(Object[]) - Method in class net.sourceforge.czt.rules.ast.ProverJokerStrokeBinding

createAndShowGUI(Sequent, RuleTable, SectionManager, String) - Static method in class net.sourceforge.czt.rules.prover.ProofTree

createJokerDeclList() - Method in class net.sourceforge.czt.rules.ast.ProverFactory

Throws an UnsupportedOperationException.

createJokerDeclList(String, String) - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerDeclListBinding() - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerDeclListBinding(JokerDeclList) - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerExpr() - Method in class net.sourceforge.czt.rules.ast.ProverFactory

Throws an UnsupportedOperationException.

createJokerExpr(String, String) - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerExprBinding() - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerExprBinding(JokerExpr) - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerExprList() - Method in class net.sourceforge.czt.rules.ast.ProverFactory

Throws an UnsupportedOperationException.

createJokerExprList(String, String) - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerExprListBinding() - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerExprListBinding(JokerExprList) - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerName() - Method in class net.sourceforge.czt.rules.ast.ProverFactory

Throws an UnsupportedOperationException.

createJokerName(String, String) - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerNameBinding() - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerNameBinding(JokerName) - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerNameList() - Method in class net.sourceforge.czt.rules.ast.ProverFactory

Throws an UnsupportedOperationException.

createJokerNameList(String, String) - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerNameListBinding() - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerNameListBinding(JokerNameList) - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerPred() - Method in class net.sourceforge.czt.rules.ast.ProverFactory

Throws an UnsupportedOperationException.

createJokerPred(String, String) - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerPredBinding() - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerPredBinding(JokerPred) - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerRenameList() - Method in class net.sourceforge.czt.rules.ast.ProverFactory

Throws an UnsupportedOperationException.

createJokerRenameList(String, String) - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerRenameListBinding() - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerRenameListBinding(JokerRenameList) - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerStroke() - Method in class net.sourceforge.czt.rules.ast.ProverFactory

Throws an UnsupportedOperationException.

createJokerStroke(String, String) - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerStrokeBinding() - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createJokerStrokeBinding(JokerStroke) - Method in class net.sourceforge.czt.rules.ast.ProverFactory

createNormalizeAppl(Expr) - Static method in class net.sourceforge.czt.rules.rewriter.RewriteUtils

createOracleMap() - Static method in class net.sourceforge.czt.rules.prover.ProverUtils

createRewriteSequent(Expr, boolean) - Static method in class net.sourceforge.czt.rules.prover.ProverUtils

createRewriteSequent(Pred, boolean) - Static method in class net.sourceforge.czt.rules.prover.ProverUtils

createRewriteSequent(SchText, boolean) - Static method in class net.sourceforge.czt.rules.prover.ProverUtils

createSequent(Pred, boolean) - Static method in class net.sourceforge.czt.rules.prover.ProverUtils

Copies the given predicate using the CopyVisitor (which makes sure that unification works) and creates a Sequent with that predicate.

createSequent(Expr, boolean) - Static method in class net.sourceforge.czt.rules.prover.ProverUtils

D

DecorateNamesVisitor(Set<Name>, Stroke) - Constructor for class net.sourceforge.czt.rules.oracles.DecorateOracle.DecorateNamesVisitor

DecorateOracle - Class in net.sourceforge.czt.rules.oracles

Implements the 'decorated expression' oracle.

DecorateOracle() - Constructor for class net.sourceforge.czt.rules.oracles.DecorateOracle

DecorateOracle.DecorateNamesVisitor - Class in net.sourceforge.czt.rules.oracles

Assumes that the term is properly typechecked (i.e.

E

EmptyDeclList - Interface in net.sourceforge.czt.rules.ast

A decl cons pair.

EmptyDeclListImpl - Class in net.sourceforge.czt.rules.ast

An empty decl list

EmptyDeclListImpl() - Constructor for class net.sourceforge.czt.rules.ast.EmptyDeclListImpl

EmptyDeclListVisitor<R> - Interface in net.sourceforge.czt.rules.ast

F

FACTORY - Static variable in class net.sourceforge.czt.rules.prover.ProverUtils

firstRule(Spec) - Static method in class net.sourceforge.czt.rules.unification.UnificationUtils

Finds the first zedrule in the specification.

freshJokerExpr(String) - Method in class net.sourceforge.czt.rules.CopyVisitor

This allows clients to use this copy visitor's factory to create fresh jokers.

G

get(String) - Method in class net.sourceforge.czt.rules.RuleTable

Convenience method for getRule.

getBinding() - Method in class net.sourceforge.czt.rules.ast.ProverJokerDeclList

getBinding() - Method in class net.sourceforge.czt.rules.ast.ProverJokerExpr

getBinding() - Method in class net.sourceforge.czt.rules.ast.ProverJokerExprList

getBinding() - Method in class net.sourceforge.czt.rules.ast.ProverJokerName

getBinding() - Method in class net.sourceforge.czt.rules.ast.ProverJokerNameList

getBinding() - Method in class net.sourceforge.czt.rules.ast.ProverJokerPred

getBinding() - Method in class net.sourceforge.czt.rules.ast.ProverJokerRenameList

getBinding() - Method in class net.sourceforge.czt.rules.ast.ProverJokerStroke

getBindings() - Method in class net.sourceforge.czt.rules.unification.Unifier

getCause() - Method in class net.sourceforge.czt.rules.unification.Unifier

getChildren() - Method in class net.sourceforge.czt.rules.ast.EmptyDeclListImpl

getGeneralize() - Method in class net.sourceforge.czt.rules.CopyVisitor

getMessage() - Method in exception net.sourceforge.czt.rules.RuleApplicationException

getMessage() - Method in exception net.sourceforge.czt.rules.unification.UnificationException

getModel() - Method in class net.sourceforge.czt.rules.prover.ProofTree

getName() - Method in interface net.sourceforge.czt.rules.Joker

getName() - Method in class net.sourceforge.czt.rules.rewriter.RewriteVisitor.RewriteRule

GetNameWordVisitor - Class in net.sourceforge.czt.rules.ast

GetNameWordVisitor() - Constructor for class net.sourceforge.czt.rules.ast.GetNameWordVisitor

getResult() - Method in class net.sourceforge.czt.rules.JokerCollector

getRule() - Method in exception net.sourceforge.czt.rules.RuleApplicationException

getRulePara(String) - Method in class net.sourceforge.czt.rules.RuleTable

getRuleParas() - Method in class net.sourceforge.czt.rules.RuleTable

Deprecated.

getRuleTable(Term, SectionManager) - Static method in class net.sourceforge.czt.rules.RuleTableCommand

getRuleTable() - Method in class net.sourceforge.czt.rules.RuleTableCommand.RuleTableVisitor

getSection() - Method in class net.sourceforge.czt.rules.prover.SimpleProver

getSequent() - Method in exception net.sourceforge.czt.rules.RuleApplicationException

getUnfoldRules() - Static method in class net.sourceforge.czt.rules.RuleUtils

getVariables() - Method in class net.sourceforge.czt.rules.oracles.CollectStateVariablesVisitor

GetZSectNameVisitor() - Constructor for class net.sourceforge.czt.rules.prover.ProverUtils.GetZSectNameVisitor

H

HideOracle - Class in net.sourceforge.czt.rules.oracles

HideOracle() - Constructor for class net.sourceforge.czt.rules.oracles.HideOracle

I

innermost(Term, RuleTable, SectionManager, String) - Static method in class net.sourceforge.czt.rules.rewriter.Strategies

This is a convenience method.

innermost(Term, Rewriter) - Static method in class net.sourceforge.czt.rules.rewriter.Strategies

Performs a leftmost innermost rewriting of the given term.

innermost(Term, Rewriter, Set<Term>) - Static method in class net.sourceforge.czt.rules.rewriter.Strategies

iterator() - Method in class net.sourceforge.czt.rules.RuleTable

J

Joker - Interface in net.sourceforge.czt.rules

Joker can be bound to a term of the correct type.

JokerCollector - Class in net.sourceforge.czt.rules

JokerCollector() - Constructor for class net.sourceforge.czt.rules.JokerCollector

jokerizeNames(ZNameList, List<Expr>, Map<ZName, Expr>, CopyVisitor) - Method in class net.sourceforge.czt.rules.oracles.LookupOracle

Transforms formal type parameters into expression jokers.

jokers_ - Variable in class net.sourceforge.czt.rules.JokerCollector

L

LookupOracle - Class in net.sourceforge.czt.rules.oracles

LookupOracle() - Constructor for class net.sourceforge.czt.rules.oracles.LookupOracle

M

maxDepth_ - Static variable in class net.sourceforge.czt.rules.unification.Unifier

Unifications deeper than this fail! This is a convenient way of detecting infinite loops in the unification algorithms.

N

net.sourceforge.czt.rules - package net.sourceforge.czt.rules

net.sourceforge.czt.rules.ast - package net.sourceforge.czt.rules.ast

net.sourceforge.czt.rules.oldrewriter - package net.sourceforge.czt.rules.oldrewriter

net.sourceforge.czt.rules.oracles - package net.sourceforge.czt.rules.oracles

net.sourceforge.czt.rules.print - package net.sourceforge.czt.rules.print

net.sourceforge.czt.rules.prover - package net.sourceforge.czt.rules.prover

net.sourceforge.czt.rules.rewriter - package net.sourceforge.czt.rules.rewriter

net.sourceforge.czt.rules.unification - package net.sourceforge.czt.rules.unification

O

OccursCheckVisitor - Class in net.sourceforge.czt.rules.unification

Implements a simple occurs check, to avoid creating cyclic terms.

OccursCheckVisitor() - Constructor for class net.sourceforge.czt.rules.unification.OccursCheckVisitor

ORACLES - Static variable in class net.sourceforge.czt.rules.prover.ProverUtils

P

Packer - Class in net.sourceforge.czt.rules.unification

A visitor that returns the necessary wrapper classes for terms.

Packer() - Constructor for class net.sourceforge.czt.rules.unification.Packer

parseExpr(String, String, SectionManager) - Static method in class net.sourceforge.czt.rules.unification.UnificationUtils

Similar to parsePred, but for ZPattern expressions.

parsePred(String, String, SectionManager) - Static method in class net.sourceforge.czt.rules.unification.UnificationUtils

Parse a Source string/file as a ZPattern Predicate.

printDepth_ - Static variable in class net.sourceforge.czt.rules.unification.Unifier

Unifications deeper than this are printed.

printJokers(Term) - Static method in class net.sourceforge.czt.rules.prover.ProverUtils

printUnicode(Term, Writer, SectionManager, String) - Static method in class net.sourceforge.czt.rules.print.PrintUtils

Prints a given term (usually an Expr or Pred) as unicode to the given writer.

PrintUtils - Class in net.sourceforge.czt.rules.print

Utilities for printing Z specifications given as an AST.

ProofTree - Class in net.sourceforge.czt.rules.prover

ProofTree(JFrame, Sequent, RuleTable, SectionManager, String) - Constructor for class net.sourceforge.czt.rules.prover.ProofTree

prove(Sequent) - Method in interface net.sourceforge.czt.rules.prover.Prover

Proves a given sequent.

prove(Pred) - Method in class net.sourceforge.czt.rules.prover.SimpleProver

Tries to prove the given pred.

prove(Sequent) - Method in class net.sourceforge.czt.rules.prover.SimpleProver

Tries all known rules to prove the sequent.

prove(Deduction) - Method in class net.sourceforge.czt.rules.prover.SimpleProver

Tries to prove a deduction by proving all its children.

prove(OracleAppl) - Method in class net.sourceforge.czt.rules.prover.SimpleProver

prove(SequentList) - Method in class net.sourceforge.czt.rules.prover.SimpleProver

Tries to prove an array of sequents.

Prover - Interface in net.sourceforge.czt.rules.prover

A prover can be used to find proofs.

ProverFactory - Class in net.sourceforge.czt.rules.ast

Makes sure that Joker are only created once.

ProverFactory() - Constructor for class net.sourceforge.czt.rules.ast.ProverFactory

ProverJokerDeclList - Class in net.sourceforge.czt.rules.ast

An implementation of the JokerDeclList and Joker interface.

ProverJokerDeclList(String, String) - Constructor for class net.sourceforge.czt.rules.ast.ProverJokerDeclList

ProverJokerDeclListBinding - Class in net.sourceforge.czt.rules.ast

An implementation of the interface JokerDeclListBinding.

ProverJokerDeclListBinding(JokerDeclList) - Constructor for class net.sourceforge.czt.rules.ast.ProverJokerDeclListBinding

ProverJokerExpr - Class in net.sourceforge.czt.rules.ast

An implementation of the JokerExpr and Joker interface.

ProverJokerExpr(String, String) - Constructor for class net.sourceforge.czt.rules.ast.ProverJokerExpr

ProverJokerExprBinding - Class in net.sourceforge.czt.rules.ast

An implementation of the interface JokerExprBinding.

ProverJokerExprBinding(JokerExpr) - Constructor for class net.sourceforge.czt.rules.ast.ProverJokerExprBinding

ProverJokerExprList - Class in net.sourceforge.czt.rules.ast

An implementation of the JokerExprList and Joker interface.

ProverJokerExprList(String, String) - Constructor for class net.sourceforge.czt.rules.ast.ProverJokerExprList

ProverJokerExprListBinding - Class in net.sourceforge.czt.rules.ast

An implementation of the interface JokerExprListBinding.

ProverJokerExprListBinding(JokerExprList) - Constructor for class net.sourceforge.czt.rules.ast.ProverJokerExprListBinding

ProverJokerName - Class in net.sourceforge.czt.rules.ast

An implementation of the JokerName and Joker interface.

ProverJokerName(String, String) - Constructor for class net.sourceforge.czt.rules.ast.ProverJokerName

ProverJokerNameBinding - Class in net.sourceforge.czt.rules.ast

An implementation of the interface JokerNameBinding.

ProverJokerNameBinding(JokerName) - Constructor for class net.sourceforge.czt.rules.ast.ProverJokerNameBinding

ProverJokerNameList - Class in net.sourceforge.czt.rules.ast

An implementation of the JokerNameList and Joker interface.

ProverJokerNameList(String, String) - Constructor for class net.sourceforge.czt.rules.ast.ProverJokerNameList

ProverJokerNameListBinding - Class in net.sourceforge.czt.rules.ast

An implementation of the interface JokerNameListBinding.

ProverJokerNameListBinding(JokerNameList) - Constructor for class net.sourceforge.czt.rules.ast.ProverJokerNameListBinding

ProverJokerPred - Class in net.sourceforge.czt.rules.ast

An implementation of the JokerPred and Joker interface.

ProverJokerPred(String, String) - Constructor for class net.sourceforge.czt.rules.ast.ProverJokerPred

ProverJokerPredBinding - Class in net.sourceforge.czt.rules.ast

An implementation of the interface JokerPredBinding.

ProverJokerPredBinding(JokerPred) - Constructor for class net.sourceforge.czt.rules.ast.ProverJokerPredBinding

ProverJokerRenameList - Class in net.sourceforge.czt.rules.ast

An implementation of the JokerRenameList and Joker interface.

ProverJokerRenameList(String, String) - Constructor for class net.sourceforge.czt.rules.ast.ProverJokerRenameList

ProverJokerRenameListBinding - Class in net.sourceforge.czt.rules.ast

An implementation of the interface JokerRenameListBinding.

ProverJokerRenameListBinding(JokerRenameList) - Constructor for class net.sourceforge.czt.rules.ast.ProverJokerRenameListBinding

ProverJokerStroke - Class in net.sourceforge.czt.rules.ast

An implementation of the JokerStroke and Joker interface.

ProverJokerStroke(String, String) - Constructor for class net.sourceforge.czt.rules.ast.ProverJokerStroke

ProverJokerStrokeBinding - Class in net.sourceforge.czt.rules.ast

An implementation of the interface JokerStrokeBinding.

ProverJokerStrokeBinding(JokerStroke) - Constructor for class net.sourceforge.czt.rules.ast.ProverJokerStrokeBinding

ProverUtils - Class in net.sourceforge.czt.rules.prover

Utility methods for proving and rewriting.

ProverUtils() - Constructor for class net.sourceforge.czt.rules.prover.ProverUtils

ProverUtils.GetZSectNameVisitor - Class in net.sourceforge.czt.rules.prover

ProverUtils.UnboundJokerRuntimeException - Exception in net.sourceforge.czt.rules.prover

provideCause(boolean) - Method in class net.sourceforge.czt.rules.unification.Unifier

R

removeJoker(Term) - Static method in class net.sourceforge.czt.rules.prover.ProverUtils

RenameOracle - Class in net.sourceforge.czt.rules.oracles

Implements the rename oracle.

RenameOracle() - Constructor for class net.sourceforge.czt.rules.oracles.RenameOracle

RenameOracle.RenameVisitor - Class in net.sourceforge.czt.rules.oracles

Assumes that the term is properly typechecked (i.e.

RenameVisitor(Set<Name>, ZRenameList) - Constructor for class net.sourceforge.czt.rules.oracles.RenameOracle.RenameVisitor

reset(Collection<Binding>) - Static method in class net.sourceforge.czt.rules.prover.ProverUtils

Resets all the bindings in the collection.

Rewrite - Class in net.sourceforge.czt.rules.oldrewriter

A rewrite engine for Z terms.

Rewrite(SectionManager, RuleTable) - Constructor for class net.sourceforge.czt.rules.oldrewriter.Rewrite

Rewrite(SectionManager, RuleTable, String) - Constructor for class net.sourceforge.czt.rules.oldrewriter.Rewrite

rewrite(Expr) - Method in class net.sourceforge.czt.rules.oldrewriter.Rewrite

rewrite(Pred) - Method in class net.sourceforge.czt.rules.oldrewriter.Rewrite

rewrite(SchText) - Method in class net.sourceforge.czt.rules.oldrewriter.Rewrite

rewrite(SectionManager, Term, RuleTable) - Static method in class net.sourceforge.czt.rules.oldrewriter.Rewrite

Recurses into a Spec or ZSect and rewrites predicates and expressions using the given rules.

rewrite(SectionManager, String, Term, RuleTable) - Static method in class net.sourceforge.czt.rules.oldrewriter.Rewrite

Recurses into a term and rewrites predicates and expressions using the given rules.

rewrite(Term) - Method in class net.sourceforge.czt.rules.oldrewriter.RewriteOnceVisitor

rewrite(Term) - Method in interface net.sourceforge.czt.rules.rewriter.Rewriter

Returns the term itself if no rewriting could be performed.

rewrite(Term, SectionManager, String) - Static method in class net.sourceforge.czt.rules.rewriter.RewriteUtils

Runs the rewriter (strategy innermost) for the given term.

rewrite(Term) - Method in class net.sourceforge.czt.rules.rewriter.RewriteVisitor

rewrite(Term, Map<ConcreteSyntaxSymbol, List<RewriteVisitor.RewriteRule>>) - Method in class net.sourceforge.czt.rules.rewriter.RewriteVisitor

rewrite(Term, List<RewriteVisitor.RewriteRule>) - Method in class net.sourceforge.czt.rules.rewriter.RewriteVisitor

RewriteOnceVisitor - Class in net.sourceforge.czt.rules.oldrewriter

Returns a rewritten version of the given term.

RewriteOnceVisitor(Prover) - Constructor for class net.sourceforge.czt.rules.oldrewriter.RewriteOnceVisitor

Rewriter - Interface in net.sourceforge.czt.rules.rewriter

RewriteRule(String, Term, Term, SequentList) - Constructor for class net.sourceforge.czt.rules.rewriter.RewriteVisitor.RewriteRule

RewriteUtils - Class in net.sourceforge.czt.rules.rewriter

All section managers mentioned here must support Z Pattern.

RewriteVisitor - Class in net.sourceforge.czt.rules.rewriter

Returns a rewritten version of the given term.

RewriteVisitor(RuleTable, SectionManager, String) - Constructor for class net.sourceforge.czt.rules.rewriter.RewriteVisitor

RewriteVisitor.AddRuleVisitor - Class in net.sourceforge.czt.rules.rewriter

RewriteVisitor.RewriteRule - Class in net.sourceforge.czt.rules.rewriter

RuleApplicationException - Exception in net.sourceforge.czt.rules

Thrown when the application of a rule to a sequent has failed.

RuleApplicationException(RulePara, Sequent, UnificationException) - Constructor for exception net.sourceforge.czt.rules.RuleApplicationException

RuleTable - Class in net.sourceforge.czt.rules

RuleTable() - Constructor for class net.sourceforge.czt.rules.RuleTable

RuleTable.RuleTableException - Exception in net.sourceforge.czt.rules

RuleTableCommand - Class in net.sourceforge.czt.rules

RuleTableCommand() - Constructor for class net.sourceforge.czt.rules.RuleTableCommand

RuleTableCommand.RuleTableVisitor - Class in net.sourceforge.czt.rules

RuleTableCommand.VisitorException - Exception in net.sourceforge.czt.rules

RuleTableException(String) - Constructor for exception net.sourceforge.czt.rules.RuleTable.RuleTableException

RuleTableVisitor(SectionManager) - Constructor for class net.sourceforge.czt.rules.RuleTableCommand.RuleTableVisitor

RuleUtils - Class in net.sourceforge.czt.rules

Provides access methods to the rule sets.

S

SchemaMinusOracle - Class in net.sourceforge.czt.rules.oracles

SchemaMinusOracle() - Constructor for class net.sourceforge.czt.rules.oracles.SchemaMinusOracle

setBottomUp(boolean) - Method in class net.sourceforge.czt.rules.oldrewriter.Rewrite

setGeneralize(String, Map<ZName, Expr>) - Method in class net.sourceforge.czt.rules.CopyVisitor

Set the names that should be generalized into expressions (usually joker expressions) during the copy.

setJokerDeclList(JokerDeclList) - Method in class net.sourceforge.czt.rules.ast.ProverJokerDeclListBinding

setJokerExpr(JokerExpr) - Method in class net.sourceforge.czt.rules.ast.ProverJokerExprBinding

setJokerExprList(JokerExprList) - Method in class net.sourceforge.czt.rules.ast.ProverJokerExprListBinding

setJokerName(JokerName) - Method in class net.sourceforge.czt.rules.ast.ProverJokerNameBinding

setJokerNameList(JokerNameList) - Method in class net.sourceforge.czt.rules.ast.ProverJokerNameListBinding

setJokerPred(JokerPred) - Method in class net.sourceforge.czt.rules.ast.ProverJokerPredBinding

setJokerRenameList(JokerRenameList) - Method in class net.sourceforge.czt.rules.ast.ProverJokerRenameListBinding

setJokerStroke(JokerStroke) - Method in class net.sourceforge.czt.rules.ast.ProverJokerStrokeBinding

setName(String) - Method in class net.sourceforge.czt.rules.ast.ProverJokerDeclList

setName(String) - Method in class net.sourceforge.czt.rules.ast.ProverJokerExpr

setName(String) - Method in class net.sourceforge.czt.rules.ast.ProverJokerExprList

setName(String) - Method in class net.sourceforge.czt.rules.ast.ProverJokerName

setName(String) - Method in class net.sourceforge.czt.rules.ast.ProverJokerNameList

setName(String) - Method in class net.sourceforge.czt.rules.ast.ProverJokerPred

setName(String) - Method in class net.sourceforge.czt.rules.ast.ProverJokerRenameList

setName(String) - Method in class net.sourceforge.czt.rules.ast.ProverJokerStroke

SimpleProver - Class in net.sourceforge.czt.rules.prover

A simple implementation of the Prover interface.

SimpleProver(Session) - Constructor for class net.sourceforge.czt.rules.prover.SimpleProver

SimpleProver(RuleTable, SectionManager, String) - Constructor for class net.sourceforge.czt.rules.prover.SimpleProver

SplitNamesOracle - Class in net.sourceforge.czt.rules.oracles

SplitNamesOracle() - Constructor for class net.sourceforge.czt.rules.oracles.SplitNamesOracle

Strategies - Class in net.sourceforge.czt.rules.rewriter

Strategies for term rewriting.

Strategies() - Constructor for class net.sourceforge.czt.rules.rewriter.Strategies

T

TermToString - Class in net.sourceforge.czt.rules.ast

TermToString() - Constructor for class net.sourceforge.czt.rules.ast.TermToString

ThetaOracle - Class in net.sourceforge.czt.rules.oracles

ThetaOracle(boolean) - Constructor for class net.sourceforge.czt.rules.oracles.ThetaOracle

toString() - Method in class net.sourceforge.czt.rules.RuleTable

TypecheckOracle - Class in net.sourceforge.czt.rules.oracles

TypecheckOracle() - Constructor for class net.sourceforge.czt.rules.oracles.TypecheckOracle

U

UnboundJokerException - Exception in net.sourceforge.czt.rules

UnboundJokerException() - Constructor for exception net.sourceforge.czt.rules.UnboundJokerException

UnboundJokerException(String) - Constructor for exception net.sourceforge.czt.rules.UnboundJokerException

UnboundJokerRuntimeException() - Constructor for exception net.sourceforge.czt.rules.prover.ProverUtils.UnboundJokerRuntimeException

UnboundJokerRuntimeException(String) - Constructor for exception net.sourceforge.czt.rules.prover.ProverUtils.UnboundJokerRuntimeException

undo(Sequent) - Method in class net.sourceforge.czt.rules.prover.SimpleProver

Undos the bindings of the duduction and sets deduction to null.

UnificationException - Exception in net.sourceforge.czt.rules.unification

Thrown when unification has failed.

UnificationException(Object, Object, String) - Constructor for exception net.sourceforge.czt.rules.unification.UnificationException

UnificationException(Object, Object, String, Throwable) - Constructor for exception net.sourceforge.czt.rules.unification.UnificationException

UnificationUtils - Class in net.sourceforge.czt.rules.unification

Unifier - Class in net.sourceforge.czt.rules.unification

Unification of ASTs.

Unifier() - Constructor for class net.sourceforge.czt.rules.unification.Unifier

unify(Object, Object) - Static method in class net.sourceforge.czt.rules.unification.UnificationUtils

Returns null if unification failed.

unify(Object, Object) - Method in class net.sourceforge.czt.rules.unification.Unifier

unify(Term, Term) - Method in class net.sourceforge.czt.rules.unification.Unifier

Unifies two terms (with occurs check).

unify2(Object, Object) - Static method in class net.sourceforge.czt.rules.unification.UnificationUtils

Throws and exception if unification failed.

UnprefixOracle - Class in net.sourceforge.czt.rules.oracles

UnprefixOracle() - Constructor for class net.sourceforge.czt.rules.oracles.UnprefixOracle

V

visitApplExpr(ApplExpr) - Method in class net.sourceforge.czt.rules.unification.ChildExtractor

Doesn't return the Mixfix child.

visitAxPara(AxPara) - Method in class net.sourceforge.czt.rules.unification.ChildExtractor

Doesn't return the Box child.

visitChildren(Expr) - Method in class net.sourceforge.czt.rules.oldrewriter.Rewrite

visitChildren(Pred) - Method in class net.sourceforge.czt.rules.oldrewriter.Rewrite

visitChildren(SchText) - Method in class net.sourceforge.czt.rules.oldrewriter.Rewrite

visitConstDecl(ConstDecl) - Method in class net.sourceforge.czt.rules.oracles.CollectStateVariablesVisitor

visitEmptyDeclList(EmptyDeclList) - Method in interface net.sourceforge.czt.rules.ast.EmptyDeclListVisitor

visitExpr(Expr) - Method in class net.sourceforge.czt.rules.oldrewriter.Rewrite

visitExpr(Expr) - Method in class net.sourceforge.czt.rules.oldrewriter.RewriteOnceVisitor

Returns a rewritten version of the given expression by trying to prove expr = JokerExpr using the prover.

visitExpr(Expr) - Method in class net.sourceforge.czt.rules.rewriter.RewriteVisitor.AddRuleVisitor

visitExpr(Expr) - Method in class net.sourceforge.czt.rules.rewriter.RewriteVisitor

visitHeadDeclList(HeadDeclList) - Method in class net.sourceforge.czt.rules.oracles.CollectStateVariablesVisitor

visitHeadDeclList(HeadDeclList) - Method in class net.sourceforge.czt.rules.print.AstToPrintTreeVisitor

visitHeadDeclList(HeadDeclList) - Method in class net.sourceforge.czt.rules.unification.ChildExtractor

visitHeadDeclList(HeadDeclList) - Method in class net.sourceforge.czt.rules.unification.Packer

visitInclDecl(InclDecl) - Method in class net.sourceforge.czt.rules.oracles.CollectStateVariablesVisitor

visitInclDecl(InclDecl) - Method in class net.sourceforge.czt.rules.oracles.RenameOracle.RenameVisitor

visitJokerDeclList(JokerDeclList) - Method in class net.sourceforge.czt.rules.ast.TermToString

visitJokerDeclList(JokerDeclList) - Method in class net.sourceforge.czt.rules.CopyVisitor

visitJokerDeclList(JokerDeclList) - Method in class net.sourceforge.czt.rules.oracles.CollectStateVariablesVisitor

visitJokerExpr(JokerExpr) - Method in class net.sourceforge.czt.rules.CopyVisitor

visitJokerExprList(JokerExprList) - Method in class net.sourceforge.czt.rules.CopyVisitor

visitJokerName(JokerName) - Method in class net.sourceforge.czt.rules.ast.GetNameWordVisitor

visitJokerName(JokerName) - Method in class net.sourceforge.czt.rules.CopyVisitor

visitJokerNameList(JokerNameList) - Method in class net.sourceforge.czt.rules.CopyVisitor

visitJokerPred(JokerPred) - Method in class net.sourceforge.czt.rules.CopyVisitor

visitJokerRenameList(JokerRenameList) - Method in class net.sourceforge.czt.rules.CopyVisitor

visitJokerStroke(JokerStroke) - Method in class net.sourceforge.czt.rules.CopyVisitor

visitLetExpr(LetExpr) - Method in class net.sourceforge.czt.rules.oldrewriter.Rewrite

For LET expressions, we rewrite only the expressions, rather than the whole schema text because let expressions can only contain constant declarations and a general rewrite rule might transform a constant into a variable declaration.

visitMemPred(MemPred) - Method in class net.sourceforge.czt.rules.unification.ChildExtractor

Doesn't return the Mixfix child.

visitName(Name) - Method in class net.sourceforge.czt.rules.ast.GetNameWordVisitor

VisitorException(Exception) - Constructor for exception net.sourceforge.czt.rules.RuleTableCommand.VisitorException

visitPred(Pred) - Method in class net.sourceforge.czt.rules.oldrewriter.Rewrite

visitPred(Pred) - Method in class net.sourceforge.czt.rules.oldrewriter.RewriteOnceVisitor

Returns a rewritten version of the given predicate by trying to prove pred \iff JokerPred using the given prover.

visitPred(Pred) - Method in class net.sourceforge.czt.rules.rewriter.RewriteVisitor.AddRuleVisitor

visitPred(Pred) - Method in class net.sourceforge.czt.rules.rewriter.RewriteVisitor

visitRefExpr(RefExpr) - Method in class net.sourceforge.czt.rules.CopyVisitor

visitRefExpr(RefExpr) - Method in class net.sourceforge.czt.rules.unification.ChildExtractor

Returns the name and type parameters of refExpr.

visitRulePara(RulePara) - Method in class net.sourceforge.czt.rules.RuleTableCommand.RuleTableVisitor

visitSchText(SchText) - Method in class net.sourceforge.czt.rules.oldrewriter.Rewrite

This rewrites schema text, using rules with conclusions of the form [D1|P1] \schemaEquals [D2|P2].

visitSchText(SchText) - Method in class net.sourceforge.czt.rules.oldrewriter.RewriteOnceVisitor

Returns a rewritten version of the given schema text by trying to prove schText schemaEquals result using the given prover.

visitSpec(Spec) - Method in class net.sourceforge.czt.rules.prover.ProverUtils.GetZSectNameVisitor

visitSpec(Spec) - Method in class net.sourceforge.czt.rules.RuleTableCommand.RuleTableVisitor

visitTerm(Term) - Method in class net.sourceforge.czt.rules.CopyVisitor

visitTerm(Term) - Method in class net.sourceforge.czt.rules.JokerCollector

visitTerm(Term) - Method in class net.sourceforge.czt.rules.oldrewriter.Rewrite

visitTerm(Term) - Method in class net.sourceforge.czt.rules.oldrewriter.RewriteOnceVisitor

visitTerm(Term) - Method in class net.sourceforge.czt.rules.oracles.DecorateOracle.DecorateNamesVisitor

visitTerm(Term) - Method in class net.sourceforge.czt.rules.oracles.RenameOracle.RenameVisitor

visitTerm(Term) - Method in class net.sourceforge.czt.rules.print.AstToPrintTreeVisitor

visitTerm(Term) - Method in class net.sourceforge.czt.rules.rewriter.RewriteVisitor

visitTerm(Term) - Method in class net.sourceforge.czt.rules.RuleTableCommand.RuleTableVisitor

visitTerm(Term) - Method in class net.sourceforge.czt.rules.unification.ChildExtractor

visitTerm(Term) - Method in class net.sourceforge.czt.rules.unification.OccursCheckVisitor

visitTerm(Term) - Method in class net.sourceforge.czt.rules.unification.Packer

visitVarDecl(VarDecl) - Method in class net.sourceforge.czt.rules.CopyVisitor

Expands a,b,c,...:T into a:T; b:T; c:T; ...

visitVarDecl(VarDecl) - Method in class net.sourceforge.czt.rules.oracles.CollectStateVariablesVisitor

visitZDeclList(ZDeclList) - Method in class net.sourceforge.czt.rules.CopyVisitor

visitZDeclList(ZDeclList) - Method in class net.sourceforge.czt.rules.oracles.CollectStateVariablesVisitor

visitZDeclList(ZDeclList) - Method in class net.sourceforge.czt.rules.unification.ChildExtractor

visitZDeclList(ZDeclList) - Method in class net.sourceforge.czt.rules.unification.Packer

visitZName(ZName) - Method in class net.sourceforge.czt.rules.ast.GetNameWordVisitor

visitZName(ZName) - Method in class net.sourceforge.czt.rules.oracles.DecorateOracle.DecorateNamesVisitor

visitZName(ZName) - Method in class net.sourceforge.czt.rules.oracles.RenameOracle.RenameVisitor

visitZName(ZName) - Method in class net.sourceforge.czt.rules.unification.ChildExtractor

Doesn't return the Decl child.

visitZParaList(ZParaList) - Method in class net.sourceforge.czt.rules.RuleTableCommand.RuleTableVisitor

visitZSchText(ZSchText) - Method in class net.sourceforge.czt.rules.CopyVisitor

visitZSect(ZSect) - Method in class net.sourceforge.czt.rules.oldrewriter.Rewrite

visitZSect(ZSect) - Method in class net.sourceforge.czt.rules.prover.ProverUtils.GetZSectNameVisitor

visitZSect(ZSect) - Method in class net.sourceforge.czt.rules.RuleTableCommand.RuleTableVisitor

X

XiOracle - Class in net.sourceforge.czt.rules.oracles

XiOracle() - Constructor for class net.sourceforge.czt.rules.oracles.XiOracle

A B C D E F G H I J L M N O P R S T U V X