Class Module

Method Details

• delete

  public void delete()

• getModuleType

  public Module.ModuleType getModuleType()

  Get the module type.
  
  This allows distinguishing modules from theories, and the
  functional, system and strategy variants within them.

• getSorts

  public SortVector getSorts()

  Get the sorts declared in the module.

• getSymbols

  public SymbolVector getSymbols()

  Get the symbols declared in the module.

• getKinds

  public KindVector getKinds()

  Get the kinds defined in the module.

• getMembershipAxioms

  public SubsortVector getMembershipAxioms()

  Get the membership axioms defined in the module.

• getEquations

  public EquationVector getEquations()

  Get the equations defined in the module.

• getRules

  public RuleVector getRules()

  Get the rules defined in the module.

• getStrategies

  public StratVector getStrategies()

  Get the strategies declared in the module.

• getStrategyDefinitions

  public StratDefVector getStrategyDefinitions()

  Get the strategy definitions defined in the module.

• getNrParameters

  public int getNrParameters()

  Number of parameters of the parameterized module.

• hasFreeParameters

  public boolean hasFreeParameters()

  Is this a parameterized module with free parameters?

• getNrImportedSorts

  public int getNrImportedSorts()

  Number of sorts imported from other modules or parameters.

• getNrImportedSymbols

  public int getNrImportedSymbols()

  Number of symbols imported from other modules or parameters.

• getNrImportedStrategies

  public int getNrImportedStrategies()

  Number of strategies imported from other modules or parameters.

• getNrOriginalEquations

  public int getNrOriginalEquations()

  Number of equations from this module.

• getNrOriginalRules

  public int getNrOriginalRules()

  Number of rules from this module.

• getNrOriginalStrategyDefinitions

  public int getNrOriginalStrategyDefinitions()

  Number of strategy definitions from this module.

• getParameterTheory

  public Module getParameterTheory(int index)

  Get the theory of the given parameter.

• getParameterName

  public String getParameterName(int index)

  Get the name of a module parameter.
  
  

  Parameters:

  index - Index of the parameter.

• findSort

  public Sort findSort(String name)

  Finds a sort by its name in the module.
  
  

  Parameters:

  name - The name of the sort.
  
  

  Returns:

  The sort or null if it does not exist.

• findSymbol

  public Symbol findSymbol(String name, KindVector domainKinds, Kind rangeKind)

  Find a symbol by its name and signature in the module.
  
  

  Parameters:

  name - The name of the sort.
  

  domainKinds - Kinds of the symbol domain.
  

  rangeKind - Range kind of the symbol.
  
  

  Returns:

  The symbol or null if it does not exist.

• parseTerm

  public Term parseTerm(TokenVector bubble, Kind kind)

  Parse a term.
  
  

  Parameters:

  bubble - Tokenized term.
  

  kind - Restrict parsing to terms of the given kind.

• parseTerm

  public Term parseTerm(TokenVector bubble)

  Parse a term.
  
  

  Parameters:

  bubble - Tokenized term.
  

• parseTerm

  public Term parseTerm(String term_str, Kind kind, TermVector vars)

  Parse a term.
  
  

  Parameters:

  term_str - A term represented as a string.
  

  kind - Restrict parsing to terms of the given kind.
  

  vars - Variables that may appear without explicit type
  annotation in the strategy.

• parseTerm

  public Term parseTerm(String term_str, Kind kind)

  Parse a term.
  
  

  Parameters:

  term_str - A term represented as a string.
  

  kind - Restrict parsing to terms of the given kind.
  

• parseTerm

  public Term parseTerm(String term_str)

  Parse a term.
  
  

  Parameters:

  term_str - A term represented as a string.
  
  

• parseStrategy

  public StrategyExpression parseStrategy(String strat_str, TermVector vars)

  Parse a strategy expression.
  
  
  

  Parameters:

  vars - Variables that may appear without explicit type
  annotation in the strategy.

• parseStrategy

  public StrategyExpression parseStrategy(String strat_str)

  Parse a strategy expression.
  
  
  

• downTerm

  public Term downTerm(Term term)

  Get a term in this module from its metarepresentation
  in (possibly) another module.
  
  

  Parameters:

  term - The metarepresentation of a term, that is,
  a valid element of the Term sort in META-TERM.
  This term must belong to a module where the META-LEVEL
  module is included. The term will be reduced.
  
  

  Returns:

  The term or null if the metarepresentation was
  not valid.

• downStrategy

  public StrategyExpression downStrategy(Term term)

  Get a strategy expression in this module from its
  metarepresentation in (possibly) another module.
  
  

  Parameters:

  term - The metarepresentation of a strategy, that is,
  a valid element of the Strategy sort in META-STRATEGY.
  This term must belong to a module where the META-LEVEL
  module is included. The term will be reduced.
  
  

  Returns:

  The strategy expression or null if the
  metarepresentation was not valid.

• upTerm

  public Term upTerm(Term term)

  Get the metarepresentation in this module of a term
  in (possibly) another module. This module must contain
  META-LEVEL.
  
  

  Parameters:

  term - Any term.
  
  

  Returns:

  The metarepresentation term or null.

• upStrategy

  public Term upStrategy(StrategyExpression expr)

  Get the metarepresentation in this module of a strategy
  expression in (possibly) another module. This module must
  contain META-LEVEL.
  
  

  Parameters:

  expr - Any strategy expression.
  
  

  Returns:

  The metarepresented strategy or null.

• unify

  public UnificationProblem unify(TermPairVector problem, boolean irredundant)

  Solves the given unification problem.
  
  

  Parameters:

  problem - A list of pairs of terms to be unified.
  

  irredundant - Whether to compute a minimal set of unifiers.
  
  

  Returns:

  An object to iterate through unifiers.

• unify

  public UnificationProblem unify(TermPairVector problem)

  Solves the given unification problem.
  
  

  Parameters:

  problem - A list of pairs of terms to be unified.
  
  
  

  Returns:

  An object to iterate through unifiers.

• variant_unify

  public VariantUnifierSearch variant_unify(TermPairVector problem, TermVector irreducible, boolean filtered)

  Solves the given unification problem using variants.
  
  

  Parameters:

  problem - A list of pairs of terms to be unified.
  

  irreducible - Irreducible terms.
  

  filtered - Whether to compute a minimal set of unifiers.
  
  

  Returns:

  An object to iterate through unifiers.

• variant_unify

  public VariantUnifierSearch variant_unify(TermPairVector problem, TermVector irreducible)

  Solves the given unification problem using variants.
  
  

  Parameters:

  problem - A list of pairs of terms to be unified.
  

  irreducible - Irreducible terms.
  
  
  

  Returns:

  An object to iterate through unifiers.

• variant_unify

  public VariantUnifierSearch variant_unify(TermPairVector problem)

  Solves the given unification problem using variants.
  
  

  Parameters:

  problem - A list of pairs of terms to be unified.
  
  
  
  

  Returns:

  An object to iterate through unifiers.

• variant_match

  public VariantUnifierSearch variant_match(TermPairVector problem, TermVector irreducible)

  Computes a complete set of order-sorted matches modulo the equations
  declared with the variant attribute (which must satisfy the finite
  variant property) plus the (supported) equational axioms in the
  given module.
  
  

  Parameters:

  problem - A list of pairs of terms to be matched.
  

  irreducible - Irreducible terms.
  
  

  Returns:

  An object to iterate through unifiers.

• variant_match

  public VariantUnifierSearch variant_match(TermPairVector problem)

  Computes a complete set of order-sorted matches modulo the equations
  declared with the variant attribute (which must satisfy the finite
  variant property) plus the (supported) equational axioms in the
  given module.
  
  

  Parameters:

  problem - A list of pairs of terms to be matched.
  
  
  

  Returns:

  An object to iterate through unifiers.

• vu_narrow

  public NarrowingSequenceSearch vu_narrow(TermVector subject, SearchType type, Term target, int depth, int flags)

  Narrowing-based search of terms that unify with the given target
  with multiple initial states.
  
  

  Parameters:

  subject - Subject terms where to start the search.
  

  type - Type of the search (number of steps).
  

  target - Term that found states must unify with.
  

  depth - Depth bound (-1 for unbounded)
  

  flags - Narrowing search flags (fold, vfold, path, delay, or filter flag).

• vu_narrow

  public NarrowingSequenceSearch vu_narrow(TermVector subject, SearchType type, Term target, int depth)

  Narrowing-based search of terms that unify with the given target
  with multiple initial states.
  
  

  Parameters:

  subject - Subject terms where to start the search.
  

  type - Type of the search (number of steps).
  

  target - Term that found states must unify with.
  

  depth - Depth bound (-1 for unbounded)
  

• vu_narrow

  public NarrowingSequenceSearch vu_narrow(TermVector subject, SearchType type, Term target)

  Narrowing-based search of terms that unify with the given target
  with multiple initial states.
  
  

  Parameters:

  subject - Subject terms where to start the search.
  

  type - Type of the search (number of steps).
  

  target - Term that found states must unify with.
  
  

• toLatex

  public String toLatex(boolean all)

  Obtain the LaTeX representation of this module.
  
  

  Parameters:

  all - Whether to show all statements by transitivity.

• toLatex

  public String toLatex()

  Obtain the LaTeX representation of this module.
  
  

• toString

  public String toString()

  Overrides:

  toString in class Object