好不容易從校內某個ftp上下載到《2012》，木有字幕……強迫自己看下去，考一考自己的聽力。發現除了罵人的語句，其他基本上一知半解，尤其是人物在討論文學／哲學／書籍等等文化相關的話題時。看來光看美劇，不看書籍了解一下西方文化還是不行啊……

 只好乖乖去找字幕。Google和百度的第一頁都是垃圾網站，現在的SEO越來越淫蕩了……
 好不容易下了個字幕。字幕質量不錯，時間間隔還可以接受。不過有一個缺陷，他是單獨一個字幕，而我的DVD版《2012》是分成兩個鏡像的——也就是第二部分無法使用這個字幕了。Orz

 我用的是ＱＱ影音，試了試調整字幕的延遲，發現那個調整對話框超搞——有一個輸入框，但是里面的數字不是延遲／提前的時間，而是基數，每按一次左／右方向鍵就增加這個數量的時間，而這個倍數卻是設定之后就看不到的。 最終使得我下決心動手山寨一個時間軸修改器，是因為QQ影音沒有為我保存字幕的延遲設定。

跑題太遠了。打開字幕文件，是純文本，Nice，省了Google的時間了。略過文件頭，有價值的地方是一行行這樣的東東：

Dialogue: 0,1:01:56.28,1:01:58.40,en,,0000,0000,0000,,We're safe!
Dialogue: 0,1:01:58.64,1:02:00.24,en,,0000,0000,0000,,We're fine!
Dialogue: 0,1:02:04.16,1:02:07.92,en,,0000,0000,0000,,Now that you have your\nmap, where we go?
Dialogue: 0,1:02:18.00,1:02:21.16,en,,0000,0000,0000,,We need a larger aircraft.
……

其中各個段由逗號隔開，各段的意義文件里也有寫：

Format: Layer, Start, End, Style, Name, MarginL, MarginR, MarginV, Effect, Text

一目了然啦。OK，其他不管，關注Start、End即可。Start和End也不用多猜，用分號隔開的時分秒是也。接下來的工作就輕松了，直接貼代碼吧。。。

點擊這里查看代碼
 1// by lingol 2009.12.05
 2
 3#include <iostream>
 4#include <string>
 5using namespace std;
 6
 7// convert "1:01:56.28" into micro-seconds
 8size_t convert(const string& str_time);
 9
10// convert micro-seconds into "1:01:56.28" like string
11string convert(size_t time);
12
13int main()
14{
15    string str;
16    while(1) {
17        getline(cin, str);
18        if (str.find("Dialogue") == 0)
19            break;
20        cout << str << endl;
21    };
22
23    size_t pos = str.find(',') + 1;
24    const size_t base_time = convert(str.substr(pos, 10));
25
26    do {
27        pos = str.find(',') + 1;
28        string tmp = str.substr(pos, 10);
29        size_t time = convert(tmp) - base_time;
30        tmp = convert(time);
31        str.replace(pos, 10, tmp);
32
33        pos = str.find(',', pos) + 1;
34        tmp = str.substr(pos, 10);
35        time = convert(tmp) - base_time;
36        tmp = convert(time);
37        str.replace(pos, 10, tmp);
38
39        cout << str << endl;
40    } while(getline(cin, str));
41    return 0;
42}
43
44// convert "1:01:56.28" into micro-seconds
45size_t convert(const string& str_time)
46{
47    size_t time = 0;
48    time += 3600 * (str_time[0] - '0');
49    time += 60 * (10*(str_time[2] - '0') + (str_time[3] - '0'));
50    time += 10*(str_time[5] - '0') + (str_time[6] - '0');
51    time *= 100;
52    time += 10*(str_time[8] - '0') + (str_time[9] - '0');
53    return time;
54}
55
56// convert micro-seconds into "1:01:56.28" like string
57string convert(size_t time)
58{
59    string str = "0:00:00.00";
60    str[9] = '0' + (time % 10);
61    time /= 10;
62    str[8] = '0' + (time % 10);
63    time /= 10;
64
65    size_t t = time % 60;
66    time /= 60;
67    str[6] = '0' + (t % 10);
68    t /= 10;
69    str[5] = '0' + (t % 10);
70
71    t = time % 60;
72    str[3] = '0' + (t % 10);
73    t /= 10;
74    str[2] = '0' + (t % 10);
75
76    str[0] = '0' + time / 60;
77
78    return str;
79}

 上面的代碼是把所有字幕的開始結束時間減去第一個字幕的開始時間，也就是把時間軸提前到0啦。把原來那個文件的文件頭拷過來，第二部的字幕也拷過來，一坨新鮮熱辣的字幕就出來咯。用硬編碼的c++做這個還真是秒殺啊~。有同學問了，第二部開始到人物說話有十幾秒延遲啊，如果我不想提前到0，而是提前到例如說12秒，怎么辦捏？有個比較hack的辦法，在第一條字幕之前增加一個無用字幕，把他的時間設置得前一點，再在生成的字幕去掉它，嘿嘿，嘿嘿

Dialogue: 0,1:01:44.28,1:01:58.40,en,,0000,0000,0000,,We're safe!
Dialogue: 0,1:01:56.28,1:01:58.40,en,,0000,0000,0000,,We're safe!
Dialogue: 0,1:01:58.64,1:02:00.24,en,,0000,0000,0000,,We're fine!
……

參考自http://www.ycrc.com.cn/qinghua/18/text/chapter4/section1/1.htm

標準式的化簡步驟
　　如果一個合適公式的所有量詞均非否定的出現在公式的前部，而且所有的量詞的
　　約束范圍均是整個公式，則稱這樣的合適公式為前束范式。任何一個合適公式，
　　都可以等價地轉化為一個前束范式。消去前束范式中所有的存在量詞后得到的
　　合適公式，稱為S范式，這一過程稱作skolem化。S范式與它的原式不一定等價，
　　但在不可滿足性方面，二者是等價的。也就是說，如果原式是不可滿足的，
　　則其對應的S范式也一定是不可滿足的。反之亦成立。

（1）消蘊涵符

（2）移動否定符
如果公式中的否定符"～"不只是作用于原子公式，則要利用摩根定律對公式進行變換，
使得否定符只作用于原子公式。

如果否定作用于量詞的話，可以用量詞轉換律將量詞提到否定的作用域之外。

（3）變量換名

（4）量詞左移
將所有的量詞移到公式的左邊，但不改變原來各量詞的排列順序。
這也是為什么在第三步要進行變量改名的原因，否則就不能進行這種移動。

（5）消去存在量詞（skolem化）
按照這樣的原則將公式中的存在量詞消去：設E是前束范式中的一個存在量詞，
如果在它的前面沒有出現全稱量詞，則所約束的變量x，全部用一個新的常量
（未在公式中出現過）代替；如果E前面有全稱量詞，則所約束的變量x，
全部用一個新的（未在公式出現過的）函數（稱為skolem函數）代替，該函數的
變量是哪些在前面的全稱量詞所約束的變量。然后將存在量詞E消去。

（6）化為合取范式
利用結合律、分配律等，可以把S范式的母式轉化為合取范式。
A(x)∨(B(x)∧C(x)) ≡ (A(x)∨B(x))∧(A(x)∨C(x))

（7）隱去全稱量詞
經過前6步變換以后，所有的變量都是受全稱量詞約束，所以可以將全稱量詞隱去，
默認所有的變量是受全稱量詞約束的。

（8）表示為子句集
在隱去全稱量詞以后，用"，"號代替公式中的"∧"，并用"{"和"}"括起來，就得到了
原合適公式的子句集。

（9）變量換名
對子句集中的變量再次進行換名替換，使得不同的子句中的變量使用不同的名字。
最簡單的方法是采用加下標的方法。注意：在有些書中并不要求對子句集中的變量
進行換名替換，如果是這樣的話，你必須很清楚，不同子句中的變量，即便是同名的，
也可以代表不同的變量。在后邊將要介紹的歸結法中，你會發現，如果不進行換名，
很容易出現錯誤。因此建議大家對變量進行換名。由于每一個子句都對應一個不同的
合取元，變量都由全稱量詞量化，因而實質上兩個子句的變量之間不存在任何關系，
這里的變量換名不影響公式的真值。

---------------------------------------------------
Skolem化并不影響原合適公式的永假特性
---------------------------------------------------

Formula -> Formula → Formula | Formula « Formula

               | Formula ∧ Formula | Formula ∨ Formula | ~Formula

               | "Variable(Formula) | $Variable(Formula)

               | Relation

Relation -> RelationSym(TermList)

RelationSym -> Constant

TermList -> Term(,Term)*

Term -> Function

          | Variable

          | Constant

Function -> FunctionSym(TermList)

FunctionSym -> [a-b]+

Variable -> [a-b]+

Constant -> [A-Z][a-zA-Z]*