Packages

c

edu.cmu.cs.ls.keymaerax.infrastruct

UniformMatching

abstract class UniformMatching extends BaseMatcher

Uniform Matching algorithm for tactics by sweeping. Their unify(shape, input) function matches second argument input against the pattern shape of the first argument, but not vice versa. Uniform matching leaves input alone and only substitutes into shape. Fast single-pass matcher that is defined by sweeping uniform matching.

Sweeping Uniform Matching is provably sound and is fast but not necessarily complete.

Note

Central recursive unification implementation.

,

a more comprehensive unification matcher would be found when jointly abstracting replacements at join conflicts if those have a joint lattice sup/inf.

See also

SchematicUnificationMatch

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

Instance Constructors

  1. new UniformMatching()

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

Abstract Value Members

  1. abstract def unify(shape: Sequent, input: 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
    BaseMatcher
    Exceptions thrown

    UnificationException if input cannot be matched against the pattern shape.

Concrete 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
    UniformMatching → 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 = 1): 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

    Example:

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

  15. def curried: (Expression) ⇒ (Expression) ⇒ RenUSubst
    Definition Classes
    Function2
    Annotations
    @unspecialized()
  16. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  17. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  18. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  19. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  20. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  21. val id: List[SubstRepl]

    Identity substitution {} that does not change anything.

    Identity substitution {} that does not change anything.

    Attributes
    protected
    Definition Classes
    Matcher
  22. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  23. 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
  24. lazy val logger: Logger
    Attributes
    protected
    Definition Classes
    LazyLogging → LoggerHolder
  25. final val loggerName: String
    Attributes
    protected
    Definition Classes
    LoggerHolder
  26. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  27. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  28. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  29. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  30. def toString(): String
    Definition Classes
    Function2 → AnyRef → Any
  31. def tupled: ((Expression, Expression)) ⇒ RenUSubst
    Definition Classes
    Function2
    Annotations
    @unspecialized()
  32. 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
  33. 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
  34. 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
  35. 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
  36. 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
  37. def unifies2(s1: Program, s2: Program, t1: Program, t2: Program): List[SubstRepl]
    Attributes
    protected
  38. def unifies2(s1: Formula, s2: Formula, t1: Formula, t2: Formula): List[SubstRepl]
    Attributes
    protected
  39. def unifies2(s1: Term, s2: Term, t1: Term, t2: Term): List[SubstRepl]
    Attributes
    protected
  40. 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 sweeping uniform matching.

    unifies2(s1,s2, t1,t2) unifies the two expressions of shape (s2,s2) against the two inputs (t1,t2) by sweeping uniform matching.

    s1 = t1 | u1     s2 = t2 | u2
-------------------------------- provided u1 and u2 compatible
(s1,s2) = (t1,t2)  | u1 join u2
    Attributes
    protected
  41. def unifiesODE2(s1: DifferentialProgram, s2: DifferentialProgram, t1: DifferentialProgram, t2: DifferentialProgram): List[SubstRepl]
    Attributes
    protected
  42. def unify(e1: Program, e2: Program): List[SubstRepl]

    Algorithm for sweeping uniform matching.

    Algorithm for sweeping uniform 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
    UniformMatching → BaseMatcher
  43. def unify(e1: Formula, e2: Formula): List[SubstRepl]

    Algorithm for sweeping uniform matching.

    Algorithm for sweeping uniform 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
    UniformMatching → BaseMatcher
  44. def unify(e1: Term, e2: Term): List[SubstRepl]

    Algorithm for sweeping uniform matching.

    Algorithm for sweeping uniform 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
    UniformMatching → BaseMatcher
  45. def unify(shape: Expression, input: Expression): List[SubstRepl]
    Attributes
    protected
    Definition Classes
    BaseMatcher
  46. 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
    Example:

    1. given t = (a, b), e2 = a2*b 1) unify((•_1, •_2), (a, b)) yields ua = •_1 ~> a, •_2 ~> b 2) the inverse is ua-1 = a ~> •_1, b ~> •_2, therefore ua-1(e2) = •_12*•_2, resulting in f(•_1, •_2) ~> (•_1^2*•_2) 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(•_1, •_2, •_3) ~> •_3; not f(•_1, •_2, •_3) ~> •_1 + •_2

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

    Algorithm for sweeping uniform matching.

    Algorithm for sweeping uniform 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
    UniformMatching → BaseMatcher
  48. 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
    Exceptions thrown

    UnificationException if e2 is not a differential variable

  49. 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
    Exceptions thrown

    UnificationException if e2 is not a variable

  50. 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.

  51. 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.

  52. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  53. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  54. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

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