280 lines
6.6 KiB
C++
280 lines
6.6 KiB
C++
|
|
|
|
// void cal_topo_index(aiger *aiger) {
|
|
|
|
// static int* topo_counter = new int[aiger->maxvar + 1];
|
|
// memset(topo_counter, 0, (aiger->maxvar + 1) * sizeof(int));
|
|
|
|
// int cnt = 0;
|
|
|
|
// std::queue<int> q;
|
|
// for(int i=0; i<aiger->num_inputs; i++) {
|
|
// int input = aiger_lit2var(aiger->inputs[i].lit);
|
|
// topo_index[input] = ++cnt;
|
|
// q.push(input);
|
|
// }
|
|
|
|
// while(!q.empty()) {
|
|
// int cur = q.front();
|
|
// q.pop();
|
|
// for(auto& edge : graph.edge[cur]) {
|
|
// int v = edge.to;
|
|
// topo_counter[v]++;
|
|
// if(topo_counter[v] == 2) {
|
|
// q.push(v);
|
|
// topo_index[v] = ++cnt;
|
|
// }
|
|
// }
|
|
// }
|
|
// }
|
|
|
|
|
|
bool check_left_graph(aiger* aiger, std::map<int, int> &new_inputs, std::vector<std::vector<int>> &clauses) {
|
|
std::queue<int> q;
|
|
static int* used = new int[aiger->maxvar + 1];
|
|
memset(used, 0, (aiger->maxvar + 1) * sizeof(int));
|
|
|
|
solver = ipasir_init();
|
|
|
|
for(auto& pair : new_inputs) {
|
|
q.push(pair.first);
|
|
used[pair.first] = true;
|
|
}
|
|
|
|
while(!q.empty()) {
|
|
int u = q.front();
|
|
q.pop();
|
|
|
|
if(graph.redge[u].size() < 2) {
|
|
continue;
|
|
}
|
|
|
|
int a = graph.redge[u][0].to;
|
|
int b = graph.redge[u][1].to;
|
|
|
|
if(graph.redge[u][0].neg) a = -a;
|
|
if(graph.redge[u][1].neg) b = -b;
|
|
|
|
ipasir_add(solver, -u);
|
|
ipasir_add(solver, a);
|
|
ipasir_add(solver, 0);
|
|
|
|
ipasir_add(solver, -u);
|
|
ipasir_add(solver, b);
|
|
ipasir_add(solver, 0);
|
|
|
|
ipasir_add(solver, -a);
|
|
ipasir_add(solver, -b);
|
|
ipasir_add(solver, u);
|
|
ipasir_add(solver, 0);
|
|
|
|
a = abs(a);
|
|
b = abs(b);
|
|
|
|
if(!used[a]) {
|
|
q.push(a);
|
|
used[a] = true;
|
|
}
|
|
|
|
if(!used[b]) {
|
|
q.push(b);
|
|
used[b] = true;
|
|
}
|
|
}
|
|
|
|
for(auto& pair : eqs) {
|
|
int a = pair.first;
|
|
int b = pair.second;
|
|
|
|
ipasir_add(solver, -a);
|
|
ipasir_add(solver, b);
|
|
ipasir_add(solver, 0);
|
|
|
|
ipasir_add(solver, a);
|
|
ipasir_add(solver, -b);
|
|
ipasir_add(solver, 0);
|
|
}
|
|
|
|
for(auto& pair : new_inputs) {
|
|
ipasir_assume(solver, pair.second ? pair.first : -pair.first);
|
|
}
|
|
|
|
int res = ipasir_solve(solver);
|
|
|
|
std::vector<int> failed_list;
|
|
|
|
if(res == 20) {
|
|
for(auto& pair : new_inputs) {
|
|
int lit = pair.second ? pair.first : -pair.first;
|
|
if(ipasir_failed(solver, lit)) {
|
|
failed_list.push_back(-lit);
|
|
}
|
|
}
|
|
classes.push_back(failed_list);
|
|
|
|
// printf("failed list: ");
|
|
// for(auto &v : failed_list) {
|
|
// printf("%d ", v);
|
|
// }
|
|
// printf("\n");
|
|
}
|
|
|
|
ipasir_release(solver);
|
|
|
|
// printf("left result: %d\n", res);
|
|
|
|
return true;
|
|
}
|
|
|
|
bool check_right_graph(aiger* aiger, std::map<int, int> &new_inputs, std::vector<std::vector<int>> &clauses) {
|
|
std::queue<int> q;
|
|
static int* used = new int[aiger->maxvar + 1];
|
|
memset(used, 0, (aiger->maxvar + 1) * sizeof(int));
|
|
|
|
solver = ipasir_init();
|
|
|
|
for(auto&vec : classes) {
|
|
for(auto &v : vec) {
|
|
ipasir_add(solver, v);
|
|
}
|
|
ipasir_add(solver, 0);
|
|
}
|
|
|
|
int x = aiger_lit2var(aiger->outputs[0].lit);
|
|
|
|
q.push(x);
|
|
used[x] = true;
|
|
|
|
while(!q.empty()) {
|
|
int u = q.front();
|
|
q.pop();
|
|
|
|
if(new_inputs.count(u)) {
|
|
continue;
|
|
}
|
|
|
|
if(graph.redge[u].size() < 2) {
|
|
printf("ERROR point %d has fanin size %d\n", u << 1, graph.redge[u].size());
|
|
exit(-1);
|
|
}
|
|
|
|
int a = graph.redge[u][0].to;
|
|
int b = graph.redge[u][1].to;
|
|
|
|
if(graph.redge[u][0].neg) a = -a;
|
|
if(graph.redge[u][1].neg) b = -b;
|
|
|
|
ipasir_add(solver, -u);
|
|
ipasir_add(solver, a);
|
|
ipasir_add(solver, 0);
|
|
|
|
ipasir_add(solver, -u);
|
|
ipasir_add(solver, b);
|
|
ipasir_add(solver, 0);
|
|
|
|
ipasir_add(solver, -a);
|
|
ipasir_add(solver, -b);
|
|
ipasir_add(solver, u);
|
|
ipasir_add(solver, 0);
|
|
|
|
a = abs(a);
|
|
b = abs(b);
|
|
|
|
if(!used[a]) {
|
|
q.push(a);
|
|
used[a] = true;
|
|
}
|
|
|
|
if(!used[b]) {
|
|
q.push(b);
|
|
used[b] = true;
|
|
}
|
|
}
|
|
|
|
for(auto& pair : eqs) {
|
|
int a = pair.first;
|
|
int b = pair.second;
|
|
|
|
ipasir_add(solver, -a);
|
|
ipasir_add(solver, b);
|
|
ipasir_add(solver, 0);
|
|
|
|
ipasir_add(solver, a);
|
|
ipasir_add(solver, -b);
|
|
ipasir_add(solver, 0);
|
|
}
|
|
|
|
if(aiger->outputs[0].lit & 1) {
|
|
ipasir_add(solver, -x);
|
|
ipasir_add(solver, 0);
|
|
} else {
|
|
ipasir_add(solver, x);
|
|
ipasir_add(solver, 0);
|
|
}
|
|
|
|
int res = ipasir_solve(solver);
|
|
|
|
if(res == 20) {
|
|
ipasir_release(solver);
|
|
return true;
|
|
}
|
|
else if(res == 10) {
|
|
for(auto& input : new_inputs) {
|
|
new_inputs[input.first] = ipasir_val(solver, input.first) >= 0 ? 1 : 0;
|
|
//printf("input[%d]=%d\n", input.first, ipasir_val(solver, input.first));
|
|
}
|
|
ipasir_release(solver);
|
|
return false;
|
|
} else {
|
|
ipasir_release(solver);
|
|
printf("UNKOWN ERROR\n");
|
|
exit(-1);
|
|
}
|
|
}
|
|
|
|
void topo_cut(aiger* aiger, int cut_topo) {
|
|
printf("c trying cut by topo_index......\n");
|
|
std::map<int, int> new_inputs;
|
|
|
|
printf("c Number of pairs detected: %d\n", pairs.size());
|
|
|
|
int pair_cnt = 0;
|
|
for(auto& pr : pairs) {
|
|
int a = pr.second.first;
|
|
int b = pr.second.second;
|
|
|
|
if(pr.first > cut_topo + 2) break;
|
|
|
|
printf("[%d/%d] check-eq %d %d (max-topo: %d)\n",++pair_cnt, pairs.size(), a, b, pr.first);//13148
|
|
|
|
if(check_var_equal(aiger, a, b)) {
|
|
printf("result is eq: %d %d\n", a, b);
|
|
int x = a & 1 ? -aiger_lit2var(a) : aiger_lit2var(a);
|
|
int y = b & 1 ? -aiger_lit2var(b) : aiger_lit2var(b);
|
|
eqs.push_back(std::make_pair(x, y));
|
|
}
|
|
}
|
|
|
|
for(int i=1; i<=aiger->maxvar; i++) {
|
|
if(topo_index[i] == cut_topo - 2) {
|
|
new_inputs[i] = -1;
|
|
}
|
|
}
|
|
|
|
std::vector<std::vector<int>> clauses;
|
|
|
|
while(!check_right_graph(aiger, new_inputs, clauses)) {
|
|
for(auto& pair : new_inputs) {
|
|
printf("%d ", pair.second);
|
|
}
|
|
printf("\n");
|
|
|
|
check_left_graph(aiger, new_inputs, clauses);
|
|
}
|
|
|
|
printf("c cut points: %d\n", new_inputs.size());
|
|
|
|
//printf("c final: %d\n", check_right_graph(aiger, new_inputs));
|
|
|
|
return;
|
|
} |