de.uka.ilkd.key.strategy.quantifierHeuristics

Class ReplacerOfQuanVariablesWithMetavariables

java.lang.Object

de.uka.ilkd.key.strategy.quantifierHeuristics.ReplacerOfQuanVariablesWithMetavariables

Deprecated.

@Deprecated
class ReplacerOfQuanVariablesWithMetavariables
extends java.lang.Object

This class is used to create metavariables for every universal variables in quantified formula allTerm and create constant functions for all existential variables. The variables with new created metavariables or constant functions are store to a map mapQM.

Field Summary

Fields

Modifier and Type	Field and Description
private static Name	ARBITRARY_NAME Deprecated.

Constructor Summary

Constructors

Modifier	Constructor and Description
private	ReplacerOfQuanVariablesWithMetavariables() Deprecated.

Method Summary

Modifier and Type	Method and Description
static Substitution	createSubstitutionForVars(Term allTerm, TermServices services) Deprecated.

Methods inherited from class java.lang.Object

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

Field Detail

ARBITRARY_NAME

private static final Name ARBITRARY_NAME

Deprecated.

Constructor Detail

ReplacerOfQuanVariablesWithMetavariables

private ReplacerOfQuanVariablesWithMetavariables()

Deprecated.

Method Detail

createSubstitutionForVars

public static Substitution createSubstitutionForVars(Term allTerm,
                                                     TermServices services)

Deprecated.