Предположим, у нас есть две замены, каждая из которых представляет собой список пар, как мы можем эффективно объединить их? Размер пары в одном списке обычно большой (большинство около 100, некоторые 5000 или больше).
Более формальное определение:
- Подстановка :: = Список [Пара [Срок]]
- Срок :: = Переменная | Constant
- Переменная :: = Int формата: 0xXXXXXXXXXXXX11 // например: v1 = 7,
v2 = 11, v3 = 15, ....
- Константа :: = Int формата: 0xXXXXXXXXXXXX10 // например: c1 = 6, c2 = 10, c3 = 14, ....
Состояние:
Одна пара отображает переменную только на константу или переменную на другую переменную. Он не может сопоставить константу с другой константой или переменной.
Примечание:
- Возможно, что две замены не могут объединиться: например. объединить Список ((7, 6), (11, 10) и Список (7, 11) / * {v1-> c1, v2-> c2} и {v1-> v2} * /
- Подстановки ввода всегда действительны, что означает, что условие выполняется в начале. Там нет идентичной пары.
- Для простоты переменные, которые появляются в левой части любой пары, не могут появляться в правой части любой пары. Для любых двух пар левые части всегда разные.
Вопрос:
- Что такое эффективное кодирование для термина.
- Что такое эффективная кодировка для подстановки.
- Каков наилучший способ объединения двух подстановок.
Спасибо!
ОБНОВЛЕНО Описание алгоритма (объединить одну новую пару p = (s, t) в список (L))
- Если в новой паре p s - это константа, а t - переменная, то измените на (v, c);
- Если новая пара идентична s = t, то удалить и DONE;
- Если новая пара отображает константу на другую константу (c1 <> c2), то происходит сбой и DONE;
- Если t существует в левой части одной пары в подстановке L, заменить ее правой частью этой пары;
- Если s существует в левой части одной пары, сохраните правую часть пары как t2 и перейдите к 7; если такой пары нет, переходите к 6;
6 Если правая часть пары в подстановке равна s, то заменить ее на t; Добавляет (s, t) в список L; и СОВЕРШЕНО;
- Если (s, t) уже есть в списке L, вернуть L и DONE;
- Если t и t2 являются константами, то произойдет сбой и DONE;
- Если t является константой, то goto 10 else goto 11;
- Если правая часть пары в подстановке равна t2, то заменить ее на t; Добавляет (t2, t) в список L; и СОВЕРШЕНО;
- Если правая часть пары в подстановке равна t, то заменить ее на t2; Добавляет (t, t2) в список L; и СОВЕРШЕНО;
Базовое определение термина: Термин может использовать некоторую другую структуру данных.
object Terms {
type Term = Int
@inline final def isV( t : Term ) = ((t & 3) == 0x3)
@inline final def isC(t : Term) = ((t & 3) == 0x2)
}
object MERGEException extends Exception
Основной код Scala:
final case class Subst( _data : List[ Tuple2[Int, Int] ] ) {
type Term = Int
type PairType = Tuple2[Term, Term]
type ListType = List[PairType]
// Find a pair in the list, which the first element matches the query t
// Returns the second element if found; t if no match
private final def find(t : Term, list : ListType) : Term =
list match {
case List() => t
case h :: list2 =>
val cmp = h._1 - t
if(cmp < 0) find(t, list2)
else if(cmp == 0) h._2
else t
}
// Replace s for t in the substitution (right part)
private final def replace_helper(s : Term, t : Term, list : ListType) : ListType =
list.map( h => if(h._2 equals s) (h._1, t) else h).distinct
// Assume: s in not in the list
private final def add(s : Term, t : Term, list : ListType) : ListType = {
var wlist = list
var rlist : ListType = List.empty
while(wlist != List.empty) {
val h = wlist.head
if(h._1 < s) {
rlist = rlist ::: List(h)
wlist = wlist.tail
} else
return rlist ::: ( (s, t) :: wlist )
}
return rlist ::: List( (s, t) )
}
private final def merge_helper(e : PairType, list : ListType) : ListType = {
// Orient the pair of SubTerms
def orient(s : Term, t : Term) : PairType =
if( Terms.isC(s) && !Terms.isC(t) ) (t, s)
else (s, t)
// Orientation
var (s, t) = orient(e._1, e._2)
// Remove identical pair
if(s equals t) return list
// Constant
if(Terms.isC(s) && Terms.isC(t)) throw MERGEException
if(list == List.empty) return List((s, t))
// If t exists in the left part of one pair, replace it by the right part of the pair
t = find(t, list)
if(s equals t) list
// now t is not in the left part of any pair
val t2 = find(s, list)
if(t2 equals s) {
// s doesn't appear in the left part of existed elements
add( s, t, replace_helper(s, t, list) )
} else {
// s appears in the left part of existed elements
if( t2 equals t ) list
else {
// s appear in the left part of existed elements
// then s doesn't appear in the right part of existed elements
// and isDirected = false
//merge_helper( (t, t2), list, isDirected )
if(Terms.isC(t) && Terms.isC(t2)) throw MERGEException
else if(Terms.isC(t)) {
add( t2, t, replace_helper(t2, t, list) )
}
else add( t, t2, replace_helper(t, t2, list) )
}
}
}
// Merge a pair into the substitution
final def merge( e : PairType ) : Option[Subst] = {
try {
val ret = merge_helper(e, _data)
return Some( Subst(ret) )
} catch {
case MERGEException => return None
}
}
// Union a new substitution together
final def union(s : Subst) : Option[Subst] = {
try {
if(_data.isEmpty) return Some(s)
else if(s.isEmpty) return Some(this)
else {
var ret = _data
var Subst(slist) = s
slist.foreach( e =>
ret = merge_helper(e, ret) )
return Some( Subst(ret) )
}
} catch {
case e => return None
}
}
final def isEmpty = _data.isEmpty
}
Код тестирования:
// Test case 1
val s1 = Subst( List( (7, 6), (11, 10) ) ) // {v1->c1, v2->c2}
val s2 = Subst( List( (7, 11) ) ) // {v1->v2}
val s3 = s1.union(s2) // none
// Test case 2
val s12 = Subst( List( (7, 6), (11, 6), (23, 19), (27, 15), (31, 35) ) ) // {v1->c1, v2->c1, v5->v4, v6->v3, v7->v8}
val s22 = Subst( List( (11, 7), (15, 7), (19, 10) ) ) // {v2->v1, v3->v1, v4->c2}
val s32 = s12.union(s22) // Some( Subst( List( (7, 6), (11, 6), (15, 6), (19, 10), (23, 10), (27, 6), (31, 35) ) ) )