好不容易从校内某个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]*