Packages

c

edu.cmu.cs.ls.keymaerax.infrastruct

UnificationMatchBase

class UnificationMatchBase extends SchematicComposedUnificationMatch

Generic base for unification/matching algorithm for tactics. Unify(shape, input) matches second argument input against the pattern shape of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape. Reasonably fast single-pass matcher.

Linear Supertypes
SchematicComposedUnificationMatch, SchematicUnificationMatch, BaseMatcher, Logging, LazyLogging, LoggerHolder, Matcher, (Expression, Expression) ⇒ RenUSubst, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. UnificationMatchBase
  2. SchematicComposedUnificationMatch
  3. SchematicUnificationMatch
  4. BaseMatcher
  5. Logging
  6. LazyLogging
  7. LoggerHolder
  8. Matcher
  9. Function2
  10. AnyRef
  11. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new UnificationMatchBase()

Type Members

  1. type Subst = RenUSubst

    The (generalized) substitutions used for unification purposes

    The (generalized) substitutions used for unification purposes

    Definition Classes
    Matcher
    See also

    RenUSubst

  2. type SubstRepl = (Expression, Expression)

    A (generalized) substitution pair, which is either like a SubstitutionPair for uniform substitution or a pair of Variable for uniform renaming.

    A (generalized) substitution pair, which is either like a SubstitutionPair for uniform substitution or a pair of Variable for uniform renaming.

    Definition Classes
    Matcher
    See also

    SubstitutionPair

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. def Subst(subs: List[SubstRepl]): Subst

    Create a (generalized) substitution from the given representation subs.

    Create a (generalized) substitution from the given representation subs.

    Attributes
    protected
    Definition Classes
    Matcher
  5. def SubstRepl(what: Expression, repl: Expression): SubstRepl

    Create a (generalized) substitution pair.

    Create a (generalized) substitution pair.

    Attributes
    protected
    Definition Classes
    Matcher
    See also

    SubstitutionPair

  6. def apply(e1: Sequent, e2: Sequent): Subst

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Definition Classes
    BaseMatcher → Matcher
    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

  7. def apply(e1: DifferentialProgram, e2: DifferentialProgram): Subst

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Definition Classes
    BaseMatcher → Matcher
    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

  8. def apply(e1: Program, e2: Program): Subst

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Definition Classes
    BaseMatcher → Matcher
    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

  9. def apply(e1: Formula, e2: Formula): Subst

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Definition Classes
    BaseMatcher → Matcher
    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

  10. def apply(e1: Term, e2: Term): Subst

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Definition Classes
    BaseMatcher → Matcher
    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

  11. def apply(e1: Expression, e2: Expression): Subst

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    apply(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Definition Classes
    BaseMatcher → Matcher → Function2
  12. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  13. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  14. def coloredDotsTerm(s: Sort, color: Int = 0): Term

    DotTerms of different "colors" for components of a Tuple, uncolored DotTerm for non-Tuples

    DotTerms of different "colors" for components of a Tuple, uncolored DotTerm for non-Tuples

    Definition Classes
    SchematicUnificationMatch
    Example:

    1. coloredDotsTerm(Real) = • coloredDotsTerm(Real*Real) = (•_0, •_1) coloredDotsTerm(Real*Real*Real) = (•_0, •_1, •_2)

  15. def compose(after: List[SubstRepl], before: List[SubstRepl]): List[SubstRepl]

    Composition of renaming substitution representations: compose(after, before) gives the representation of after performed after before.

    Composition of renaming substitution representations: compose(after, before) gives the representation of after performed after before.

    s after t = {p(.)~>s(F) | (p(.)~>F) \in t}  ++  {(p(.)~>F) \in s | (p(.)~>G) \notin t for all G}
    returns

    a substitution that has the same effect as applying substitution after after applying substitution before.

    Attributes
    protected
    Definition Classes
    UnificationMatchBase → SchematicUnificationMatch
  16. def curried: (Expression) ⇒ (Expression) ⇒ RenUSubst
    Definition Classes
    Function2
    Annotations
    @unspecialized()
  17. def distinctIfNeedBe(repl: List[SubstRepl]): List[SubstRepl]

    Make repl distinct (if this algorithm does not preserve distinctness).

    Make repl distinct (if this algorithm does not preserve distinctness).

    returns

    repl.distinct

    Attributes
    protected
    Definition Classes
    SchematicComposedUnificationMatch
  18. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  19. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  20. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  21. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  22. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  23. val id: List[SubstRepl]

    Identity substitution {} that does not change anything.

    Identity substitution {} that does not change anything.

    Attributes
    protected
    Definition Classes
    Matcher
  24. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  25. def join(s: List[SubstRepl], t: List[SubstRepl]): List[SubstRepl]

    Union of renaming substitution representations: join(s, t) gives the representation of s performed together with t, if compatible.

    Union of renaming substitution representations: join(s, t) gives the representation of s performed together with t, if compatible.

    s \cup t = {p(.)~>F | (p(.)~>F) \in s}  ++  {(p(.)~>F) | (p(.)~>F) \in t}
if s and t are compatible, so do not map the same p(.) or f(.) or a to different replacements
    returns

    a substitution that has the same effect as applying both substitutions s and t simultaneously. Similar to returning s++t but skipping duplicates and checking compatibility in passing.

    Attributes
    protected
    Definition Classes
    BaseMatcher
  26. lazy val logger: Logger
    Attributes
    protected
    Definition Classes
    LazyLogging → LoggerHolder
  27. final val loggerName: String
    Attributes
    protected
    Definition Classes
    LoggerHolder
  28. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  29. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  30. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  31. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  32. def toString(): String
    Definition Classes
    Function2 → AnyRef → Any
  33. def tupled: ((Expression, Expression)) ⇒ RenUSubst
    Definition Classes
    Function2
    Annotations
    @unspecialized()
  34. def unifiable(shape: Sequent, input: Sequent): Option[Subst]

    unifiable(shape, input) Compute some unifier matching input against the pattern shape if unifiable else None

    unifiable(shape, input) Compute some unifier matching input against the pattern shape if unifiable else None

    Definition Classes
    BaseMatcher → Matcher
  35. def unifiable(shape: Expression, input: Expression): Option[Subst]

    unifiable(shape, input) Compute some unifier matching input against the pattern shape if unifiable else None

    unifiable(shape, input) Compute some unifier matching input against the pattern shape if unifiable else None

    Definition Classes
    BaseMatcher → Matcher
  36. def unifier(e1: Sequent, e2: Sequent, us: List[SubstRepl]): Subst

    Create the unifier us (which was formed for e1 and e2, just for the record).

    Create the unifier us (which was formed for e1 and e2, just for the record).

    Attributes
    protected
    Definition Classes
    BaseMatcher
  37. def unifier(e1: Expression, e2: Expression, us: List[SubstRepl]): Subst

    Create the unifier us (which was formed for e1 and e2, just for the record).

    Create the unifier us (which was formed for e1 and e2, just for the record).

    Attributes
    protected
    Definition Classes
    BaseMatcher
  38. def unifier(shape: Expression, input: Expression): List[SubstRepl]

    Construct the base unifier that forces shape and input to unify unless equal already

    Construct the base unifier that forces shape and input to unify unless equal already

    returns

    {shape~>input} unless shape=input in which case it's {}.

    Attributes
    protected
    Definition Classes
    BaseMatcher
  39. def unifies2(s1: Program, s2: Program, t1: Program, t2: Program): List[SubstRepl]
    Attributes
    protected
    Definition Classes
    SchematicComposedUnificationMatch → SchematicUnificationMatch
  40. def unifies2(s1: Formula, s2: Formula, t1: Formula, t2: Formula): List[SubstRepl]
    Attributes
    protected
    Definition Classes
    SchematicComposedUnificationMatch → SchematicUnificationMatch
  41. def unifies2(s1: Term, s2: Term, t1: Term, t2: Term): List[SubstRepl]
    Attributes
    protected
    Definition Classes
    SchematicComposedUnificationMatch → SchematicUnificationMatch
  42. def unifies2(s1: Expression, s2: Expression, t1: Expression, t2: Expression): List[SubstRepl]

    unifies2(s1,s2, t1,t2) unifies the two expressions of shape (s2,s2) against the two inputs (t1,t2) by single-sided matching.

    unifies2(s1,s2, t1,t2) unifies the two expressions of shape (s2,s2) against the two inputs (t1,t2) by single-sided matching.

    s1 = t1 | u1     u1(s2) = t2 | u2
----------------------------------
(s1,s2) = (t1,t2)  | u2 after u1

    Implemented by unifying from left to right, but will fall back to converse direction if exception.

    Attributes
    protected
    Definition Classes
    SchematicComposedUnificationMatch → SchematicUnificationMatch
  43. def unifiesODE2(s1: DifferentialProgram, s2: DifferentialProgram, t1: DifferentialProgram, t2: DifferentialProgram): List[SubstRepl]
    Attributes
    protected
    Definition Classes
    SchematicComposedUnificationMatch → SchematicUnificationMatch
  44. def unify(s1: Sequent, s2: Sequent): List[SubstRepl]

    unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Attributes
    protected
    Definition Classes
    SchematicComposedUnificationMatch → BaseMatcher
    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

  45. def unify(e1: Program, e2: Program): List[SubstRepl]

    A simple recursive unification algorithm for single-sided matching.

    A simple recursive unification algorithm for single-sided matching. unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Attributes
    protected
    Definition Classes
    SchematicUnificationMatch → BaseMatcher
  46. def unify(e1: Formula, e2: Formula): List[SubstRepl]

    A simple recursive unification algorithm for single-sided matching.

    A simple recursive unification algorithm for single-sided matching. unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Attributes
    protected
    Definition Classes
    SchematicUnificationMatch → BaseMatcher
  47. def unify(e1: Term, e2: Term): List[SubstRepl]

    A simple recursive unification algorithm for single-sided matching.

    A simple recursive unification algorithm for single-sided matching. unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Attributes
    protected
    Definition Classes
    SchematicUnificationMatch → BaseMatcher
  48. def unify(shape: Expression, input: Expression): List[SubstRepl]
    Attributes
    protected
    Definition Classes
    BaseMatcher
  49. def unifyApplicationOf(F: (Function, Term) ⇒ Expression, f: Function, t: Term, e2: Expression): List[SubstRepl]

    Unify f(t) with e2 where F is the operator (FuncOf or PredOf) that forms the ApplicationOf f(t).

    Unify f(t) with e2 where F is the operator (FuncOf or PredOf) that forms the ApplicationOf f(t).

    1) unify the argument t with a DotTerm abstraction • (t may be a tuple, then • is a tuple: coloredDotsTerm) ua = unify(•, t) 2) unifier = substitute with the inverse of the argument unifier e2 f(•) ~> ua^-1(e2)

    Attributes
    protected
    Definition Classes
    SchematicUnificationMatch
    Example:

    1. given t = (a, b), e2 = a2*b 1) unify((•_0, •_1), (a, b)) yields ua = •_0 ~> a, •_1 ~> b 2) the inverse is ua-1 = a ~> •_0, b ~> •_1, therefore ua-1(e2) = •_02*•_1, resulting in f(•_0, •_1) ~> (•_0^2*•_1) the inverse substitution is applied top-down, i.e., larger abstractions get precedence when components of t overlap: t = (x, y, x + y) and e2 = x + y yields f(•_0, •_1, •_2) ~> •_2; not f(•_0, •_1, •_2) ~> •_0 + •_1

  50. def unifyODE(e1: DifferentialProgram, e2: DifferentialProgram): List[SubstRepl]

    A simple recursive unification algorithm for single-sided matching.

    A simple recursive unification algorithm for single-sided matching. unify(shape, input) matches input against the pattern shape to find a uniform substitution \result such that \result(shape)==input.

    Attributes
    protected
    Definition Classes
    SchematicUnificationMatch → BaseMatcher
  51. def unifyVar(xp1: DifferentialSymbol, e2: Expression): List[SubstRepl]

    unifyVar(x1',e2) gives a unifier making x1' equal to e2 unless it already is.

    unifyVar(x1',e2) gives a unifier making x1' equal to e2 unless it already is.

    returns

    unifyVar(x1',x2')={x1~>x2} if x2' is a differential variable other than x1' unifyVar(x1',x1')={}

    Attributes
    protected
    Definition Classes
    SchematicUnificationMatch
    Exceptions thrown

    UnificationException if e2 is not a differential variable

  52. def unifyVar(x1: Variable, e2: Expression): List[SubstRepl]

    unifyVar(x1,e2) gives a unifier making x1 equal to e2 unless it already is.

    unifyVar(x1,e2) gives a unifier making x1 equal to e2 unless it already is.

    returns

    unifyVar(x1,x2)={x1~>x2} if x2 is a variable other than x1. unifyVar(x1,x1)={}

    Attributes
    protected
    Definition Classes
    SchematicUnificationMatch
    Exceptions thrown

    UnificationException if e2 is not a variable

  53. def ununifiable(shape: Sequent, input: Sequent): Nothing

    Indicates that input cannot be matched against the pattern shape by raising a UnificationException.

    Indicates that input cannot be matched against the pattern shape by raising a UnificationException.

    Attributes
    protected
    Definition Classes
    BaseMatcher
    Exceptions thrown

    UnificationException always.

  54. def ununifiable(shape: Expression, input: Expression): Nothing

    Indicates that input cannot be matched against the pattern shape by raising a UnificationException.

    Indicates that input cannot be matched against the pattern shape by raising a UnificationException.

    Attributes
    protected
    Definition Classes
    BaseMatcher
    Exceptions thrown

    UnificationException always.

  55. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  56. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  57. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from SchematicComposedUnificationMatch

Inherited from SchematicUnificationMatch

Inherited from BaseMatcher

Inherited from Logging

Inherited from LazyLogging

Inherited from LoggerHolder

Inherited from Matcher

Inherited from (Expression, Expression) ⇒ RenUSubst

Inherited from AnyRef

Inherited from Any

Ungrouped