701 lines
16 KiB
C++
701 lines
16 KiB
C++
|
|
#include <string.h>
|
|
#include <stdarg.h>
|
|
#include <limits.h>
|
|
|
|
#include <quack.hpp>
|
|
#include <heap.hpp>
|
|
#include <set.hpp>
|
|
#include <print.hpp>
|
|
#include <automata.hpp>
|
|
#include <tuple.hpp>
|
|
#include <dict.hpp>
|
|
|
|
struct automata* automata::new_variable(
|
|
int depth,
|
|
bool verbose,
|
|
unsigned variable_index,
|
|
bool value,
|
|
unsigned number_of_variables)
|
|
{
|
|
assert(variable_index < number_of_variables);
|
|
|
|
if (verbose)
|
|
{
|
|
printf("%*s" "variable(index = %u, value = %s):\n",
|
|
depth++, "", variable_index, value ? "true" : "false");
|
|
}
|
|
|
|
size_t total_number_of_states = 0;
|
|
|
|
struct automata* start = new automata();
|
|
struct automata* moving = start;
|
|
|
|
total_number_of_states++;
|
|
|
|
for (unsigned i = 0; i < number_of_variables; i++)
|
|
{
|
|
struct automata* newmoving = new automata();
|
|
|
|
total_number_of_states++;
|
|
|
|
if (i == variable_index)
|
|
{
|
|
moving->on[value] = newmoving;
|
|
}
|
|
else
|
|
{
|
|
moving->on[0] = newmoving;
|
|
moving->on[1] = newmoving;
|
|
}
|
|
|
|
moving = newmoving;
|
|
}
|
|
|
|
moving->is_accepting = true;
|
|
|
|
if (verbose)
|
|
{
|
|
printf("%*s" "returned automata with %'lu states.\n",
|
|
depth, "", total_number_of_states);
|
|
}
|
|
|
|
return start;
|
|
}
|
|
|
|
void automata::dump(struct automata* start, const char* fmt, ...)
|
|
{
|
|
char path[PATH_MAX];
|
|
|
|
static size_t dump_id = 0;
|
|
|
|
snprintf(path, PATH_MAX, "/tmp/%05lu.dot", dump_id++);
|
|
|
|
FILE* stream = fopen(path, "w");
|
|
|
|
fprintf(stream, ""
|
|
"digraph {" "\n"
|
|
"\t" "rankdir = LR;" "\n"
|
|
"\t"
|
|
"\t" "node [" "\n"
|
|
"\t" "\t" "shape = circle" "\n"
|
|
"\t" "\t" "label = \"\"" "\n"
|
|
"\t" "];" "\n"
|
|
"\t" "\n"
|
|
"");
|
|
|
|
va_list va;
|
|
va_start(va, fmt);
|
|
|
|
vfprintf(stream, fmt, va);
|
|
|
|
va_end(va);
|
|
|
|
quack<automata*> todo;
|
|
|
|
set<automata*> queued;
|
|
|
|
if (start && queued.add(start))
|
|
{
|
|
todo.append(start);
|
|
}
|
|
|
|
while (todo.n)
|
|
{
|
|
automata* state = todo.pop();
|
|
|
|
if (state->is_accepting)
|
|
{
|
|
fprintf(stream, "\"%p\" [ shape = doublecircle ];\n", state);
|
|
}
|
|
|
|
for (int on = 0; on < 2; on++)
|
|
{
|
|
automata* to = state->on[on];
|
|
|
|
if (to)
|
|
{
|
|
fprintf(stream, "\"%p\" -> \"%p\" [label = \"%i\"];\n", state, to, on);
|
|
|
|
if (queued.add(to))
|
|
{
|
|
todo.append(to);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
fprintf(stream, ""
|
|
"}" "\n"
|
|
"");
|
|
|
|
fclose(stream);
|
|
}
|
|
|
|
struct automata* automata::complement(
|
|
const struct automata* original_start)
|
|
{
|
|
dict<const automata*, automata*> mapping;
|
|
|
|
struct automata* start = new automata();
|
|
|
|
struct automata* phi = NULL;
|
|
|
|
quack<decltype(mapping)::keyvalue_pair*> todo;
|
|
|
|
todo.append(mapping.add(original_start, start));
|
|
|
|
while (todo.n)
|
|
{
|
|
auto [original, state] = *todo.pop();
|
|
|
|
state->is_accepting = !original->is_accepting;
|
|
|
|
for (int value = 0; value < 2; value++)
|
|
{
|
|
if (const automata* to = original->on[value])
|
|
{
|
|
if (mapping.has(to))
|
|
{
|
|
state->on[value] = mapping[to];
|
|
}
|
|
else
|
|
{
|
|
automata* state_to = new automata();
|
|
|
|
state->on[value] = state_to;
|
|
|
|
todo.append(mapping.add(to, state_to));
|
|
}
|
|
}
|
|
else
|
|
{
|
|
if (!phi)
|
|
{
|
|
phi = new automata();
|
|
|
|
phi->is_accepting = true;
|
|
|
|
phi->on[0] = phi;
|
|
phi->on[1] = phi;
|
|
}
|
|
|
|
state->on[value] = phi;
|
|
}
|
|
}
|
|
}
|
|
|
|
return start;
|
|
}
|
|
|
|
struct automata* automata::union_(
|
|
int depth,
|
|
bool verbose,
|
|
const struct automata* left_start,
|
|
const struct automata* right_start)
|
|
{
|
|
if (verbose)
|
|
{
|
|
printf("%*s" "union():\n", depth++, "");
|
|
}
|
|
|
|
dict<tuple<const automata*, const automata*>, automata*> mapping;
|
|
|
|
size_t total_number_of_states = 0;
|
|
|
|
struct automata* start = new automata();
|
|
|
|
total_number_of_states++;
|
|
|
|
quack<decltype(mapping)::keyvalue_pair*> todo;
|
|
|
|
// initial state:
|
|
todo.append(mapping.add(tuple(left_start, right_start), start));
|
|
|
|
while (todo.n)
|
|
{
|
|
auto keyvalue = todo.pop();
|
|
|
|
auto [left, right] = keyvalue->key;
|
|
|
|
automata* state = keyvalue->value;
|
|
|
|
state->is_accepting = false
|
|
|| (left && left->is_accepting)
|
|
|| (right && right->is_accepting);
|
|
|
|
for (int value = 0; value < 2; value++)
|
|
{
|
|
const automata* left_to = left ? left->on[value] : NULL;
|
|
const automata* right_to = right ? right->on[value] : NULL;
|
|
|
|
if (left_to || right_to)
|
|
{
|
|
if (mapping.has(tuple(left_to, right_to)))
|
|
{
|
|
state->on[value] = mapping[tuple(left_to, right_to)];
|
|
}
|
|
else
|
|
{
|
|
automata* state_to = new automata();
|
|
|
|
total_number_of_states++;
|
|
|
|
state->on[value] = state_to;
|
|
|
|
todo.append(mapping.add(tuple(left_to, right_to), state_to));
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
if (verbose)
|
|
{
|
|
printf("%*s" "returned automata with %'lu states" "\n",
|
|
depth, "", total_number_of_states);
|
|
}
|
|
|
|
return start;
|
|
}
|
|
|
|
struct automata* automata::intersect(
|
|
int depth,
|
|
bool verbose,
|
|
const struct automata* left_start,
|
|
const struct automata* right_start)
|
|
{
|
|
if (verbose)
|
|
{
|
|
printf("%*s" "intersect():\n", depth++, "");
|
|
}
|
|
|
|
dict<tuple<const automata*, const automata*>, automata*> mapping;
|
|
|
|
size_t total_number_of_states = 0;
|
|
|
|
struct automata* start = new automata();
|
|
|
|
total_number_of_states++;
|
|
|
|
quack<decltype(mapping)::keyvalue_pair*> todo;
|
|
|
|
// initial state:
|
|
todo.append(mapping.add(tuple(left_start, right_start), start));
|
|
|
|
while (todo.n)
|
|
{
|
|
auto keyvalue = todo.pop();
|
|
|
|
auto [left, right] = keyvalue->key;
|
|
|
|
automata* state = keyvalue->value;
|
|
|
|
state->is_accepting = left->is_accepting && right->is_accepting;
|
|
|
|
for (int value = 0; value < 2; value++)
|
|
{
|
|
const automata* left_to = left->on[value];
|
|
const automata* right_to = right->on[value];
|
|
|
|
if (left_to && right_to)
|
|
{
|
|
if (mapping.has(tuple(left_to, right_to)))
|
|
{
|
|
state->on[value] = mapping[tuple(left_to, right_to)];
|
|
}
|
|
else
|
|
{
|
|
automata* state_to = new automata();
|
|
|
|
total_number_of_states++;
|
|
|
|
state->on[value] = state_to;
|
|
|
|
todo.append(mapping.add(tuple(left_to, right_to), state_to));
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
if (verbose)
|
|
{
|
|
printf("%*s" "returned automata with %'lu states" "\n",
|
|
depth, "", total_number_of_states);
|
|
}
|
|
|
|
return start;
|
|
}
|
|
|
|
struct automata* automata::eliminate_dead_code(
|
|
int depth,
|
|
bool verbose,
|
|
const struct automata* original_start)
|
|
{
|
|
if (verbose)
|
|
{
|
|
printf("%*s" "eliminate_dead_code():\n", depth++, "");
|
|
}
|
|
|
|
set<const automata*> can_reach;
|
|
{
|
|
set<const automata*> queued;
|
|
|
|
dict<const automata*, set<const automata*>> dep_on;
|
|
|
|
quack<const automata*> explore_todo;
|
|
|
|
quack<const automata*> percolate_todo;
|
|
|
|
queued.add(original_start);
|
|
|
|
explore_todo.append(original_start);
|
|
|
|
if (verbose)
|
|
{
|
|
printf("%*s" "exploring ...\n", depth, "");
|
|
}
|
|
|
|
while (explore_todo.n)
|
|
{
|
|
auto state = explore_todo.pop();
|
|
|
|
if (state->is_accepting)
|
|
{
|
|
can_reach.add(state);
|
|
|
|
percolate_todo.append(state);
|
|
}
|
|
else for (int val = 0; val < 2; val++)
|
|
{
|
|
if (auto to = state->on[val])
|
|
{
|
|
if (!dep_on.has(to))
|
|
{
|
|
dep_on.add(to, set<const automata*>());
|
|
}
|
|
|
|
dep_on[to].add(state);
|
|
|
|
if (queued.add(to))
|
|
{
|
|
explore_todo.append(to);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
if (verbose)
|
|
{
|
|
printf("%*s" "percolating ...\n", depth, "");
|
|
}
|
|
|
|
while (percolate_todo.n)
|
|
{
|
|
auto state = percolate_todo.pop();
|
|
|
|
if (dep_on.has(state))
|
|
{
|
|
for (auto substate: dep_on[state])
|
|
{
|
|
if (can_reach.add(substate))
|
|
{
|
|
percolate_todo.append(substate);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
if (verbose)
|
|
{
|
|
printf("%*s" "cloning ...\n", depth, "");
|
|
}
|
|
|
|
size_t total_number_of_states = 0;
|
|
|
|
struct automata* new_start = NULL;
|
|
{
|
|
dict<const automata*, automata*> mapping;
|
|
|
|
quack<decltype(mapping)::keyvalue_pair*> todo;
|
|
|
|
// initial state:
|
|
if (can_reach.has(original_start))
|
|
{
|
|
new_start = new automata();
|
|
|
|
total_number_of_states++;
|
|
|
|
todo.append(mapping.add(original_start, new_start));
|
|
}
|
|
|
|
while (todo.n)
|
|
{
|
|
auto [old, state] = *todo.pop();
|
|
|
|
state->is_accepting = old->is_accepting;
|
|
|
|
for (int val = 0; val < 2; val++)
|
|
{
|
|
const automata* to = old->on[val];
|
|
|
|
if (to && can_reach.has(to))
|
|
{
|
|
if (mapping.has(to))
|
|
{
|
|
state->on[val] = mapping[to];
|
|
}
|
|
else
|
|
{
|
|
automata* substate = new automata();
|
|
|
|
total_number_of_states++;
|
|
|
|
state->on[val] = substate;
|
|
|
|
todo.append(mapping.add(to, substate));
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
if (verbose)
|
|
{
|
|
printf("%*s" "returned automata with %'lu states" "\n",
|
|
depth, "", total_number_of_states);
|
|
}
|
|
|
|
return new_start;
|
|
}
|
|
|
|
struct automata* automata::simplify(
|
|
int depth,
|
|
bool verbose,
|
|
const struct automata* original_start)
|
|
{
|
|
if (verbose)
|
|
{
|
|
printf("%*s" "simplify():\n", depth++, "");
|
|
}
|
|
|
|
set<const automata*> universe;
|
|
{
|
|
quack<const automata*> todo;
|
|
|
|
universe.add(original_start);
|
|
|
|
todo.append(original_start);
|
|
|
|
while (todo.n)
|
|
{
|
|
const automata* state = todo.pop();
|
|
|
|
for (int val = 0; val < 2; val++)
|
|
{
|
|
auto to = state->on[val];
|
|
|
|
if (to && universe.add(to))
|
|
{
|
|
todo.append(to);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
typedef tuple<const automata*, const automata*> pair_t;
|
|
|
|
dict<pair_t, set<pair_t>> dependent_of;
|
|
|
|
heap<tuple<unsigned /* hopcount */, pair_t>> todo;
|
|
|
|
for (const automata* a: universe)
|
|
{
|
|
for (const automata* b: universe)
|
|
{
|
|
if (a < b)
|
|
{
|
|
bool are_different = false;
|
|
|
|
if (a->is_accepting != b->is_accepting)
|
|
{
|
|
are_different = true;
|
|
}
|
|
else for (int val = 0; !are_different && val < 2; val++)
|
|
{
|
|
const automata* a_to = a->on[val];
|
|
const automata* b_to = b->on[val];
|
|
|
|
if (!a_to != !b_to)
|
|
{
|
|
are_different = true;
|
|
}
|
|
else if (a_to && b_to)
|
|
{
|
|
if (a_to > b_to)
|
|
{
|
|
const automata* swap = b_to;
|
|
b_to = a_to, a_to = swap;
|
|
}
|
|
|
|
if (!dependent_of.has(tuple(a_to, b_to)))
|
|
{
|
|
dependent_of.add(tuple(a_to, b_to), set<pair_t>());
|
|
}
|
|
|
|
dependent_of[tuple(a_to, b_to)].add(tuple(a, b));
|
|
}
|
|
}
|
|
|
|
if (are_different)
|
|
{
|
|
todo.push(tuple(0U, tuple(a, b)));
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
dict<const automata*, set<const automata*>> same_as;
|
|
|
|
for (const automata* state: universe)
|
|
{
|
|
same_as.add(state, set<const automata*>(universe));
|
|
}
|
|
|
|
while (todo.n)
|
|
{
|
|
auto [hopcount, pair] = todo.pop();
|
|
|
|
auto [a, b] = pair;
|
|
|
|
if (same_as[a].discard(b) && same_as[b].discard(a))
|
|
{
|
|
if (dependent_of.has(pair))
|
|
{
|
|
for (pair_t dep_on: dependent_of[pair])
|
|
{
|
|
todo.push(tuple(hopcount + 1, dep_on));
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
size_t total_number_of_states = 1;
|
|
|
|
struct automata* new_start = new automata();
|
|
{
|
|
dict<const automata*, automata*> mapping;
|
|
|
|
quack<decltype(mapping)::keyvalue_pair*> todo;
|
|
|
|
// initial state:
|
|
{
|
|
const automata* cloneme = same_as[original_start].min();
|
|
|
|
todo.append(mapping.add(cloneme, new_start));
|
|
}
|
|
|
|
while (todo.n)
|
|
{
|
|
auto [old, state] = *todo.pop();
|
|
|
|
state->is_accepting = old->is_accepting;
|
|
|
|
for (int val = 0; val < 2; val++)
|
|
{
|
|
if (const automata* to = old->on[val])
|
|
{
|
|
const automata* cloneme = same_as[to].min();
|
|
|
|
if (mapping.has(cloneme))
|
|
{
|
|
state->on[val] = mapping[cloneme];
|
|
}
|
|
else
|
|
{
|
|
automata* substate = new automata();
|
|
|
|
total_number_of_states++;
|
|
|
|
state->on[val] = substate;
|
|
|
|
todo.append(mapping.add(cloneme, substate));
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
if (verbose)
|
|
{
|
|
printf("%*s" "returned automata with %'lu states" "\n",
|
|
depth, "", total_number_of_states);
|
|
}
|
|
|
|
return new_start;
|
|
}
|
|
|
|
void automata::free(struct automata* start)
|
|
{
|
|
set<automata*> queued;
|
|
|
|
quack<automata*> todo;
|
|
|
|
if (start)
|
|
{
|
|
queued.add(start);
|
|
|
|
todo.append(start);
|
|
}
|
|
|
|
while (todo.n)
|
|
{
|
|
struct automata* state = todo.pop();
|
|
|
|
for (int val = 0; val < 2; val++)
|
|
{
|
|
if (struct automata* to = state->on[val])
|
|
{
|
|
if (queued.add(to))
|
|
{
|
|
todo.append(to);
|
|
}
|
|
}
|
|
}
|
|
|
|
delete state;
|
|
}
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|