点击这里查看代码
 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!
……

标准式的化简步骤
　　如果一个合适公式的所有量词均非否定的出现在公式的前部，而且所有的量词的
　　约束范围均是整个公式，则称这样的合适公式为前束范式。任何一个合适公式，
　　都可以等价地转化为一个前束范式。消去前束范式中所有的存在量词后得到的
　　合适公式，称为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]*