Class Term

Method Details

• delete

  public void delete()

• symbol

  public Symbol symbol()

  Get the top symbol of this term.

• ground

  public boolean ground()

  Is this term ground?

• equal

  public boolean equal(Term other)

  Compare two terms for equality.
  
  

  Parameters:

  other - The second term to be compared.

• leq

  public boolean leq(Sort sort)

  Check whether the sort of this term is a subtype of the given sort.
  
  

  Parameters:

  sort - The pretended supertype.

• getSort

  public Sort getSort()

  Get the sort of this term.

• normalize

  public void normalize(boolean full)

  Normalize this term modulo axioms.
  
  

  Parameters:

  full - Whether to normalize in depth.

• normalize

  public void normalize()

  Normalize this term modulo axioms.
  
  

• reduce

  public int reduce()

  Reduce this term.
  
  

  Returns:

  The total number of rewrites.

• rewrite

  public int rewrite(int bound)

  Rewrite a term following the semantics of the rewrite command.
  
  

  Parameters:

  bound - An upper bound on the number of rule rewrites.
  
  

  Returns:

  The total number of rewrites.

• rewrite

  public int rewrite()

  Rewrite a term following the semantics of the rewrite command.
  
  
  
  

  Returns:

  The total number of rewrites.

• frewrite

  public int frewrite(int bound, int gas)

  Rewrite a term following the semantics of the frewrite command.
  
  

  Parameters:

  bound - An upper bound on the number of rule rewrites.
  

  gas - An upper bound on the number of rule rewrites per position.
  
  

  Returns:

  The total number of rewrites.

• frewrite

  public int frewrite(int bound)

  Rewrite a term following the semantics of the frewrite command.
  
  

  Parameters:

  bound - An upper bound on the number of rule rewrites.
  
  
  

  Returns:

  The total number of rewrites.

• frewrite

  public int frewrite()

  Rewrite a term following the semantics of the frewrite command.
  
  
  
  
  

  Returns:

  The total number of rewrites.

• erewrite

  public TermIntPair erewrite(int bound, int gas)

  Rewrite a term following the semantics of the erewrite command.
  
  

  Parameters:

  bound - An upper bound on the number of rule rewrites.
  

  gas - An upper bound on the number of rule rewrites by position.
  
  

  Returns:

  The result and the total number of rewrites (the original
  term is not modified).

• erewrite

  public TermIntPair erewrite(int bound)

  Rewrite a term following the semantics of the erewrite command.
  
  

  Parameters:

  bound - An upper bound on the number of rule rewrites.
  
  
  

  Returns:

  The result and the total number of rewrites (the original
  term is not modified).

• erewrite

  public TermIntPair erewrite()

  Rewrite a term following the semantics of the erewrite command.
  
  
  
  
  

  Returns:

  The result and the total number of rewrites (the original
  term is not modified).

• match

  public MatchSearchState match(Term pattern, Condition condition, boolean withExtension, int minDepth, int maxDepth)

  Match this term into a given pattern.
  
  

  Parameters:

  pattern - Pattern term.
  

  condition - Equational condition that solutions must satisfy.
  

  withExtension - Whether the matching should be done with extension modulo axioms
  (deprecated, use maxDepth=0 instead).
  

  minDepth - Minimum matching depth.
  

  maxDepth - Maximum matching depth (-1 to match on top without extension, 0
  to match on top with extension, UNBOUNDED to match anywhere, or any intermediate value).
  
  

  Returns:

  An object to iterate through matches.

• match

  public MatchSearchState match(Term pattern, Condition condition, boolean withExtension, int minDepth)

  Match this term into a given pattern.
  
  

  Parameters:

  pattern - Pattern term.
  

  condition - Equational condition that solutions must satisfy.
  

  withExtension - Whether the matching should be done with extension modulo axioms
  (deprecated, use maxDepth=0 instead).
  

  minDepth - Minimum matching depth.
  
  
  

  Returns:

  An object to iterate through matches.

• match

  public MatchSearchState match(Term pattern, Condition condition, boolean withExtension)

  Match this term into a given pattern.
  
  

  Parameters:

  pattern - Pattern term.
  

  condition - Equational condition that solutions must satisfy.
  

  withExtension - Whether the matching should be done with extension modulo axioms
  (deprecated, use maxDepth=0 instead).
  
  
  
  

  Returns:

  An object to iterate through matches.

• match

  public MatchSearchState match(Term pattern, Condition condition)

  Match this term into a given pattern.
  
  

  Parameters:

  pattern - Pattern term.
  

  condition - Equational condition that solutions must satisfy.
  
  
  
  
  

  Returns:

  An object to iterate through matches.

• match

  public MatchSearchState match(Term pattern)

  Match this term into a given pattern.
  
  

  Parameters:

  pattern - Pattern term.
  
  
  
  
  
  

  Returns:

  An object to iterate through matches.

• srewrite

  public StrategicSearch srewrite(StrategyExpression expr, boolean depth)

  Rewrite a term following a strategy.
  
  

  Parameters:

  expr - A strategy expression.
  

  depth - Whether to perform a depth-first search. By default, a fair search is used.
  
  

  Returns:

  An object to iterate through strategy solutions.

• srewrite

  public StrategicSearch srewrite(StrategyExpression expr)

  Rewrite a term following a strategy.
  
  

  Parameters:

  expr - A strategy expression.
  
  
  

  Returns:

  An object to iterate through strategy solutions.

• search

  public RewriteSequenceSearch search(SearchType type, Term target, Condition condition, int depth)

  Search states that match into a given pattern and satisfy a given
  condition by rewriting from this term.
  
  

  Parameters:

  type - Type of search (number of steps).
  

  target - Patterm term.
  

  condition - Condition that solutions must satisfy.
  

  depth - Depth bound.
  
  

  Returns:

  An object to iterate through matches.

• search

  public RewriteSequenceSearch search(SearchType type, Term target, Condition condition)

  Search states that match into a given pattern and satisfy a given
  condition by rewriting from this term.
  
  

  Parameters:

  type - Type of search (number of steps).
  

  target - Patterm term.
  

  condition - Condition that solutions must satisfy.
  
  
  

  Returns:

  An object to iterate through matches.

• search

  public RewriteSequenceSearch search(SearchType type, Term target)

  Search states that match into a given pattern and satisfy a given
  condition by rewriting from this term.
  
  

  Parameters:

  type - Type of search (number of steps).
  

  target - Patterm term.
  
  
  
  

  Returns:

  An object to iterate through matches.

• search

  public StrategySequenceSearch search(SearchType type, Term target, StrategyExpression strategy, Condition condition, int depth)

  Search states that match into a given pattern and satisfy a given
  condition by rewriting from this term using a strategy.
  
  

  Parameters:

  type - Type of search (number of steps).
  

  target - Patterm term.
  

  strategy - Strategy to control the search.
  

  condition - Condition that solutions must satisfy.
  

  depth - Depth bound.
  
  

  Returns:

  An object to iterate through matches.

• search

  public StrategySequenceSearch search(SearchType type, Term target, StrategyExpression strategy, Condition condition)

  Search states that match into a given pattern and satisfy a given
  condition by rewriting from this term using a strategy.
  
  

  Parameters:

  type - Type of search (number of steps).
  

  target - Patterm term.
  

  strategy - Strategy to control the search.
  

  condition - Condition that solutions must satisfy.
  
  
  

  Returns:

  An object to iterate through matches.

• search

  public StrategySequenceSearch search(SearchType type, Term target, StrategyExpression strategy)

  Search states that match into a given pattern and satisfy a given
  condition by rewriting from this term using a strategy.
  
  

  Parameters:

  type - Type of search (number of steps).
  

  target - Patterm term.
  

  strategy - Strategy to control the search.
  
  
  
  

  Returns:

  An object to iterate through matches.

• get_variants

  public VariantSearch get_variants(boolean irredundant, TermVector irreducible)

  Compute the most general variants of this term.
  
  

  Parameters:

  irredundant - Whether to obtain irredundant variants
  (for theories with the finite variant property).
  

  irreducible - Irreducible terms constraint.
  
  

  Returns:

  An object to iterate through variants.

• get_variants

  public VariantSearch get_variants(boolean irredundant)

  Compute the most general variants of this term.
  
  

  Parameters:

  irredundant - Whether to obtain irredundant variants
  (for theories with the finite variant property).
  
  
  

  Returns:

  An object to iterate through variants.

• get_variants

  public VariantSearch get_variants()

  Compute the most general variants of this term.
  
  
  
  
  

  Returns:

  An object to iterate through variants.

• vu_narrow

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

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

  Parameters:

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

  target - The pattern that has to be reached.
  

  depth - Depth bound (-1 for unbounded).
  

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

  Returns:

  An object to iterate through solutions.

• vu_narrow

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

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

  Parameters:

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

  target - The pattern that has to be reached.
  

  depth - Depth bound (-1 for unbounded).
  
  
  

  Returns:

  An object to iterate through solutions.

• vu_narrow

  public NarrowingSequenceSearch vu_narrow(SearchType type, Term target)

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

  Parameters:

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

  target - The pattern that has to be reached.
  
  
  
  

  Returns:

  An object to iterate through solutions.

• apply

  public RewriteSearchState apply(String label, Substitution substitution, int minDepth, int maxDepth)

  Apply any rule with the given label.
  
  

  Parameters:

  label - Rule label (or null for any executable rule).
  

  substitution - Initial substitution that will be applied on the rule before matching.
  

  minDepth - Minimum matching depth.
  

  maxDepth - Maximum matching depth.
  
  

  Returns:

  An object to iterate through the rewritten terms.

• apply

  public RewriteSearchState apply(String label, Substitution substitution, int minDepth)

  Apply any rule with the given label.
  
  

  Parameters:

  label - Rule label (or null for any executable rule).
  

  substitution - Initial substitution that will be applied on the rule before matching.
  

  minDepth - Minimum matching depth.
  
  
  

  Returns:

  An object to iterate through the rewritten terms.

• apply

  public RewriteSearchState apply(String label, Substitution substitution)

  Apply any rule with the given label.
  
  

  Parameters:

  label - Rule label (or null for any executable rule).
  

  substitution - Initial substitution that will be applied on the rule before matching.
  
  
  
  

  Returns:

  An object to iterate through the rewritten terms.

• apply

  public RewriteSearchState apply(String label)

  Apply any rule with the given label.
  
  

  Parameters:

  label - Rule label (or null for any executable rule).
  
  
  
  
  

  Returns:

  An object to iterate through the rewritten terms.

• check

  public String check()

  Check an SMT formula.
  
  

  Returns:

  A string, either sat, unsat or undecided.

• arguments

  public ArgumentIterator arguments(boolean normalize)

  Iterate over the arguments of this term.
  
  

  Parameters:

  normalize - Whether to normalize before iterating over its arguments.

• arguments

  public ArgumentIterator arguments()

  Iterate over the arguments of this term.
  
  

• toFloat

  public double toFloat()

  Get the floating-point number represented by the given term or
  zero otherwise.

• toInt

  public int toInt()

  Get the integer number represented by the given term or
  zero otherwise.

• isVariable

  public boolean isVariable()

  Get whether the term is a variable.

• getVarName

  public String getVarName()

  Get the name of the variable if the current term is a variable or
  a null value otherwise.

• getIterExponent

  public long getIterExponent()

  Get the exponent of an iterable symbol or zero otherwise.

• hash

  public long hash()

  Get the hash value of the term.

• copy

  public Term copy()

  Get a copy of this term.

• getNO_CONDITION

  public static Condition getNO_CONDITION()

  An empty condition to be used as a placeholder.

• prettyPrint

  public String prettyPrint(PrintFlags flags)

  Pretty prints this term.
  
  

  Parameters:

  flags - Flags that affect the term output.

• toLatex

  public String toLatex()

  Obtain the LaTeX representation of this term.

• toString

  public String toString()

  Overrides:

  toString in class Object