911 lines
24 KiB
C++
911 lines
24 KiB
C++
#include "solve.hpp"
|
|
|
|
#include <assert.h>
|
|
#include "src/kissat.h"
|
|
|
|
extern "C" {
|
|
#include "aiger.h"
|
|
}
|
|
|
|
#define ENABLE_INPUT_VAR_DIVIED 0
|
|
#define DIVEDED_VAR_NUM 48
|
|
|
|
#define ENABLE_MERGE_NODE 0
|
|
|
|
#if ENABLE_INPUT_VAR_DIVIED
|
|
std::map<int, int> init_inputs;
|
|
#endif
|
|
|
|
using std::vector;
|
|
|
|
bool match_equal(aiger* aiger, int var) {
|
|
if(graph.redge[var].size() != 2) return false;
|
|
int x = graph.redge[var][0].to;
|
|
int y = graph.redge[var][1].to;
|
|
|
|
if(!graph.redge[var][0].neg) return false;
|
|
if(!graph.redge[var][1].neg) return false;
|
|
|
|
if(graph.redge[x].size() != 2) return false;
|
|
if(graph.redge[y].size() != 2) return false;
|
|
|
|
Graph::Edge ex0 = graph.redge[x][0];
|
|
Graph::Edge ex1 = graph.redge[x][1];
|
|
if(ex0.to > ex1.to) std::swap(ex0, ex1);
|
|
|
|
Graph::Edge ey0 = graph.redge[y][0];
|
|
Graph::Edge ey1 = graph.redge[y][1];
|
|
if(ey0.to > ey1.to) std::swap(ey0, ey1);
|
|
|
|
if(ex0.to != ey0.to || ex1.to != ey1.to) return false;
|
|
|
|
if(ex0.neg + ex1.neg != 1) return false;
|
|
if(ey0.neg + ey1.neg != 1) return false;
|
|
if(ex0.neg + ey0.neg != 1) return false;
|
|
|
|
// for(auto& e : graph.edge[var]) {
|
|
// if(!e.neg) return false;
|
|
// }
|
|
|
|
return true;
|
|
}
|
|
|
|
bool match_xor(aiger* aiger, int var) {
|
|
if(graph.redge[var].size() != 2) return false;
|
|
int x = graph.redge[var][0].to;
|
|
int y = graph.redge[var][1].to;
|
|
|
|
if(!graph.redge[var][0].neg) return false;
|
|
if(!graph.redge[var][1].neg) return false;
|
|
|
|
if(graph.redge[x].size() != 2) return false;
|
|
if(graph.redge[y].size() != 2) return false;
|
|
|
|
Graph::Edge ex0 = graph.redge[x][0];
|
|
Graph::Edge ex1 = graph.redge[x][1];
|
|
if(ex0.to > ex1.to) std::swap(ex0, ex1);
|
|
|
|
Graph::Edge ey0 = graph.redge[y][0];
|
|
Graph::Edge ey1 = graph.redge[y][1];
|
|
if(ey0.to > ey1.to) std::swap(ey0, ey1);
|
|
|
|
if(ex0.to != ey0.to || ex1.to != ey1.to) return false;
|
|
|
|
if(ex0.neg != ex1.neg) return false;
|
|
if(ey0.neg != ey1.neg) return false;
|
|
if(ex0.neg == ey0.neg) return false;
|
|
|
|
return true;
|
|
}
|
|
|
|
void cal_topo_index(aiger *aiger) {
|
|
|
|
static int* used = new int[aiger->maxvar + 1];
|
|
memset(used, 0, (aiger->maxvar + 1) * sizeof(int));
|
|
|
|
std::queue<int> q;
|
|
for(int i=0; i<aiger->num_inputs; i++) {
|
|
int input = aiger_lit2var(aiger->inputs[i].lit);
|
|
topo_index[input] = 1;
|
|
q.push(input);
|
|
}
|
|
|
|
while(!q.empty()) {
|
|
int cur = q.front();
|
|
q.pop();
|
|
for(auto& edge : graph.edge[cur]) {
|
|
int v = edge.to;
|
|
if(!used[v]) {
|
|
used[v] = true;
|
|
q.push(v);
|
|
topo_index[v] = topo_index[cur] + 1;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
void simulate(aiger* aiger, int* input, int* result) {
|
|
|
|
std::queue<int> q;
|
|
|
|
for(int i=0; i<aiger->num_inputs; i++) {
|
|
int var = aiger_lit2var(aiger->inputs[i].lit);
|
|
result[var] = input[i];
|
|
q.push(var);
|
|
}
|
|
|
|
static int* topo_counter = new int[aiger->maxvar + 1];
|
|
memset(topo_counter, 0, (aiger->maxvar + 1) * sizeof(int));
|
|
|
|
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);
|
|
|
|
//cout << "redge: " << v << " " << graph.redge[v][0].to << " " << graph.redge[v][1].to << endl;
|
|
|
|
Graph::Edge rhs0_edge = graph.redge[v][0];
|
|
int rhs0 = rhs0_edge.neg ? !result[rhs0_edge.to] : result[rhs0_edge.to];
|
|
|
|
Graph::Edge rhs1_edge = graph.redge[v][1];
|
|
int rhs1 = rhs1_edge.neg ? !result[rhs1_edge.to] : result[rhs1_edge.to];
|
|
|
|
result[v] = rhs0 & rhs1;
|
|
|
|
//cout << "var: " << aiger_var2lit(v) << " = " << rhs0 + rhs0_edge.neg << " " << rhs1 + rhs1_edge.neg << " : " << result[aiger_var2lit(v)] << endl;
|
|
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
aiger* get_var_as_output_aiger(aiger* aiger, unsigned var) {
|
|
|
|
std::queue<int> q;
|
|
|
|
static int* used = new int[aiger->maxvar + 1];
|
|
memset(used, 0, (aiger->maxvar + 1) * sizeof(int));
|
|
|
|
q.push(var);
|
|
used[var] = true;
|
|
|
|
std::vector<std::pair<int, std::pair<int, int>>> ands;
|
|
std::vector<int> inputs;
|
|
|
|
|
|
while(!q.empty()) {
|
|
int u = q.front();
|
|
q.pop();
|
|
|
|
// if(graph.redge[u].size() == 0) {
|
|
// inputs.push_back(aiger_var2lit(u));
|
|
// continue;
|
|
// }
|
|
|
|
int a = graph.redge[u][0].to;
|
|
int b = graph.redge[u][1].to;
|
|
|
|
if(a <= aiger->num_inputs && b <= aiger->num_inputs) {
|
|
printf("AND-START: %d (%d %d)\n", u, a, b);
|
|
inputs.push_back(aiger_var2lit(u));
|
|
continue;
|
|
}
|
|
if(a <= aiger->num_inputs || b <= aiger->num_inputs) {
|
|
printf("FUCK!!!!!");
|
|
}
|
|
|
|
ands.push_back(std::make_pair(aiger_var2lit(u), std::make_pair(aiger_var2lit(a) + graph.redge[u][0].neg, aiger_var2lit(b) + graph.redge[u][1].neg)));
|
|
|
|
if(!used[a]) q.push(a), used[a] = true;
|
|
if(!used[b]) q.push(b), used[b] = true;
|
|
}
|
|
|
|
auto result_aiger = aiger_init();
|
|
for(int i=0; i<inputs.size(); i++) {
|
|
printf("add INPUTS: %d\n", inputs[i]);
|
|
aiger_add_input(result_aiger, inputs[i], std::to_string(inputs[i]).c_str());
|
|
}
|
|
for(auto &pr : ands) {
|
|
aiger_add_and(result_aiger, pr.first, pr.second.first, pr.second.second);
|
|
printf("add AND: %d %d %d\n", pr.first, pr.second.first, pr.second.second);
|
|
}
|
|
aiger_add_output(result_aiger, aiger_var2lit(var), "238901893");
|
|
|
|
return result_aiger;
|
|
}
|
|
|
|
void get_cone_of_points(aiger *aiger, std::vector<int> &points, std::vector<int> &result, int lmin) {
|
|
result.clear();
|
|
|
|
std::queue<int> q;
|
|
static int* used = new int[aiger->maxvar + 1];
|
|
memset(used, 0, (aiger->maxvar + 1) * sizeof(int));
|
|
|
|
for(auto& p : points) {
|
|
q.push(p);
|
|
used[p] = true;
|
|
}
|
|
|
|
while(!q.empty()) {
|
|
int u = q.front();
|
|
q.pop();
|
|
|
|
result.push_back(u);
|
|
|
|
if(topo_index[u] < lmin) continue;
|
|
if(graph.redge[u].size() == 0) 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;
|
|
|
|
a = abs(a), b = abs(b);
|
|
|
|
if(!used[a]) q.push(a), used[a] = true;
|
|
if(!used[b]) q.push(b), used[b] = true;
|
|
}
|
|
}
|
|
|
|
bool check_var_equal_with_input_set(aiger *aiger, int x, int y, std::set<int> &inputs) {
|
|
|
|
|
|
|
|
SATSolver solver;
|
|
solver.set_max_time(10);
|
|
solver.new_vars(aiger->maxvar + 1);
|
|
solver.log_to_file("cms.log");
|
|
|
|
std::queue<int> q;
|
|
static int* used = new int[aiger->maxvar + 1];
|
|
memset(used, 0, (aiger->maxvar + 1) * sizeof(int));
|
|
|
|
q.push(x);
|
|
q.push(y);
|
|
int can_del = 0;
|
|
used[x] = true;
|
|
used[y] = true;
|
|
|
|
// printf("[%d]inputs: ", inputs.size());
|
|
// for(auto& in : inputs) {
|
|
// printf("%d ", inputs);
|
|
// }
|
|
// printf("\n");
|
|
|
|
#if ENABLE_INPUT_VAR_DIVIED
|
|
for(auto& p : init_inputs) {
|
|
int var = aiger_lit2var(p.first);
|
|
if(!p.second) var = -var;
|
|
cms_add(solver, var);
|
|
cms_add(solver, 0);
|
|
}
|
|
#endif
|
|
|
|
while(!q.empty()) {
|
|
int u = q.front();
|
|
q.pop();
|
|
|
|
can_del++;
|
|
|
|
if(inputs.count(u)) continue;
|
|
|
|
if(match_xor(aiger, u) || match_equal(aiger, u)) {
|
|
//printf("FUCK %d\n", u);
|
|
std::vector<unsigned> vars;
|
|
int x = graph.redge[graph.redge[u][0].to][0].to;
|
|
int y = graph.redge[graph.redge[u][0].to][1].to;
|
|
vars.push_back(x);
|
|
vars.push_back(y);
|
|
vars.push_back(u);
|
|
solver.add_xor_clause(vars, match_equal(aiger, u));
|
|
//printf("x: %d %d %d (%d)\n", x, y, u, match_equal(aiger, u));
|
|
|
|
if(!used[x]) q.push(x), used[x] = true;
|
|
if(!used[y]) q.push(y), used[y] = true;
|
|
|
|
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;
|
|
|
|
cms_add(solver, -u), cms_add(solver, a), cms_add(solver, 0);
|
|
cms_add(solver, -u), cms_add(solver, b), cms_add(solver, 0);
|
|
cms_add(solver, -a), cms_add(solver, -b), cms_add(solver, u), cms_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;
|
|
}
|
|
|
|
cms_add(solver, -x), cms_add(solver, -y), cms_add(solver, 0);
|
|
cms_add(solver, x), cms_add(solver, y), cms_add(solver, 0);
|
|
|
|
for(auto& pair : eqs) {
|
|
int a = pair.first;
|
|
int b = pair.second;
|
|
cms_add(solver, -a), cms_add(solver, b), cms_add(solver, 0);
|
|
cms_add(solver, a), cms_add(solver, -b), cms_add(solver, 0);
|
|
}
|
|
|
|
// printf("2one %d\n", can_del);
|
|
|
|
// printf("##### %d\n", result);
|
|
|
|
// printf("FIND XOR: %d\n",);
|
|
|
|
auto result = solver.solve();
|
|
|
|
return result == l_False;
|
|
}
|
|
|
|
bool check_var_equal(aiger* aiger, int x, int y) {
|
|
std::vector<int> cone;
|
|
std::vector<int> points;
|
|
points.push_back(x);
|
|
points.push_back(y);
|
|
|
|
get_cone_of_points(aiger, points, cone, 0);
|
|
|
|
printf("cone %d\n", cone.size());
|
|
|
|
std::set<int> inputs;
|
|
for(auto& p : cone) {
|
|
// if(eqn.count(p) || graph.redge[p].size() == 0)
|
|
// inputs.insert(p);
|
|
if(graph.redge[p].size() == 0)
|
|
inputs.insert(p);
|
|
}
|
|
|
|
while(!check_var_equal_with_input_set(aiger, x, y, inputs)) {
|
|
std::vector<std::pair<int, int>> vec;
|
|
for(auto& p : inputs) {
|
|
vec.push_back(std::make_pair(topo_index[p], p));
|
|
}
|
|
std::sort(vec.begin(), vec.end());
|
|
|
|
int p = vec[vec.size()-1].second;
|
|
|
|
//printf("max-topo: %d\n", topo_index[p]);
|
|
|
|
if(topo_index[p] == 1) return false;
|
|
|
|
std::queue<int> q;
|
|
static int* used = new int[aiger->maxvar + 1];
|
|
memset(used, 0, (aiger->maxvar + 1) * sizeof(int));
|
|
|
|
q.push(p);
|
|
used[p] = true;
|
|
|
|
while(!q.empty()) {
|
|
int u = q.front();
|
|
q.pop();
|
|
|
|
if(graph.redge[u].size() == 0 || (eqn.count(u) && u != p)) {
|
|
inputs.insert(u);
|
|
continue;
|
|
}
|
|
|
|
int a = graph.redge[u][0].to;
|
|
int b = graph.redge[u][1].to;
|
|
|
|
if(!used[a]) q.push(a), used[a] = true;
|
|
if(!used[b]) q.push(b), used[b] = true;
|
|
}
|
|
|
|
inputs.erase(p);
|
|
}
|
|
|
|
return true;
|
|
}
|
|
|
|
void check_entire_problem(aiger* aiger) {
|
|
|
|
SATSolver solver;
|
|
solver.new_vars(aiger->maxvar + 1);
|
|
|
|
std::queue<int> q;
|
|
static int* used = new int[aiger->maxvar + 1];
|
|
memset(used, 0, (aiger->maxvar + 1) * sizeof(int));
|
|
|
|
int x = aiger_lit2var(aiger->outputs[0].lit);
|
|
|
|
q.push(x);
|
|
used[x] = true;
|
|
|
|
while(!q.empty()) {
|
|
int u = q.front();
|
|
q.pop();
|
|
|
|
/*
|
|
(u => a & b) <=> ~u | (a & b) <=> (~u | a) & (~u | b)
|
|
(u <= a & b) <=> ~(a & b) | u <=> ~a | ~b | u
|
|
*/
|
|
// if(eqn.count(u)) {
|
|
// cout << "back ends " << u << endl;
|
|
// continue;
|
|
// }
|
|
|
|
if(graph.redge[u].size() == 0) {
|
|
//cout << "oh FUCK" << endl;
|
|
continue;
|
|
}
|
|
|
|
if(match_xor(aiger, u) || match_equal(aiger, u)) {
|
|
//printf("FUCK %d\n", u);
|
|
std::vector<unsigned> vars;
|
|
int x = graph.redge[graph.redge[u][0].to][0].to;
|
|
int y = graph.redge[graph.redge[u][0].to][1].to;
|
|
vars.push_back(x);
|
|
vars.push_back(y);
|
|
vars.push_back(u);
|
|
solver.add_xor_clause(vars, match_equal(aiger, u));
|
|
//printf("x: %d %d %d (%d)\n", x, y, u, match_equal(aiger, u));
|
|
|
|
if(!used[x]) q.push(x), used[x] = true;
|
|
if(!used[y]) q.push(y), used[y] = true;
|
|
|
|
continue;
|
|
}
|
|
|
|
|
|
int a = graph.redge[u][0].to;
|
|
int b = graph.redge[u][1].to;
|
|
|
|
|
|
int ta = aiger_var2lit(a);// + graph.redge[u][0].neg;
|
|
int tb = aiger_var2lit(b);// + graph.redge[u][1].neg;
|
|
|
|
//if(eqp.find(make_pair(ta, tb)) != eqp.end() || eqp.find(make_pair(tb, ta)) != eqp.end()) {
|
|
// if(eqn.count(a) && eqn.count(b)) {
|
|
// cout << "SPCIAL-AND " << ta << " " << tb << endl;
|
|
// continue;
|
|
// }
|
|
|
|
|
|
// 下面找到所有的异或/等价电路
|
|
if(graph.redge[a].size() > 0 && graph.redge[b].size() > 0) {
|
|
|
|
//graph.redge[u][0].neg && graph.redge[u][1].neg &&
|
|
|
|
auto ea0 = graph.redge[a][0];
|
|
auto ea1 = graph.redge[a][1];
|
|
if(ea0.to > ea1.to) std::swap(ea0, ea1);
|
|
|
|
auto eb0 = graph.redge[b][0];
|
|
auto eb1 = graph.redge[b][1];
|
|
if(eb0.to > eb1.to) std::swap(eb0, eb1);
|
|
|
|
// 两个与门连接的都是相同的节点
|
|
if(ea0.to == eb0.to && ea1.to == eb1.to) {
|
|
|
|
// 二个节点等价
|
|
if(eqp.find(std::make_pair(aiger_var2lit(ea0.to), aiger_var2lit(ea1.to))) != eqp.end() || eqp.find(std::make_pair(aiger_var2lit(ea1.to), aiger_var2lit(ea0.to))) != eqp.end()) {
|
|
printf("c XOR %d %d\n", aiger_var2lit(ea0.to), aiger_var2lit(ea1.to));
|
|
}
|
|
}
|
|
}
|
|
|
|
//cout << "AND " << aiger_var2lit(u) << " " << (aiger_var2lit(a) + graph.redge[u][0].neg) << " " << (aiger_var2lit(b) + graph.redge[u][1].neg) << endl;
|
|
|
|
if(graph.redge[u][0].neg) a = -a;
|
|
if(graph.redge[u][1].neg) b = -b;
|
|
|
|
|
|
cms_add(solver, -u);
|
|
cms_add(solver, a);
|
|
cms_add(solver, 0);
|
|
|
|
cms_add(solver, -u);
|
|
cms_add(solver, b);
|
|
cms_add(solver, 0);
|
|
|
|
cms_add(solver, -a);
|
|
cms_add(solver, -b);
|
|
cms_add(solver, u);
|
|
cms_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;
|
|
|
|
cms_add(solver, -a);
|
|
cms_add(solver, b);
|
|
cms_add(solver, 0);
|
|
|
|
cms_add(solver, a);
|
|
cms_add(solver, -b);
|
|
cms_add(solver, 0);
|
|
}
|
|
|
|
if(aiger->outputs[0].lit & 1) {
|
|
cms_add(solver, -x);
|
|
cms_add(solver, 0);
|
|
} else {
|
|
cms_add(solver, x);
|
|
cms_add(solver, 0);
|
|
}
|
|
//ipasir_set_conflict_limit(solver, 100000);
|
|
|
|
printf("c final: %d\n", solver.solve());
|
|
|
|
return;
|
|
}
|
|
|
|
bool check_var_equal_new(aiger* aiger, int x, int y) {
|
|
auto aiger0 = get_var_as_output_aiger(aiger, x);
|
|
auto aiger1 = get_var_as_output_aiger(aiger, y);
|
|
|
|
system("rm -rf test0*");
|
|
system("rm -rf test1*");
|
|
|
|
FILE* f0 = fopen("test0.aiger", "w");
|
|
FILE* f1 = fopen("test1.aiger", "w");
|
|
|
|
aiger_write_to_file(aiger0, aiger_mode::aiger_binary_mode, f0);
|
|
aiger_write_to_file(aiger1, aiger_mode::aiger_binary_mode, f1);
|
|
|
|
fclose(f0);
|
|
fclose(f1);
|
|
|
|
aiger_reset(aiger0);
|
|
aiger_reset(aiger1);
|
|
|
|
system("./bash.sh");
|
|
|
|
std::string str;
|
|
FILE* result = fopen("abc_result", "r");
|
|
char c;
|
|
while((c = fgetc(result)) != EOF) str += c;
|
|
|
|
std::cout << str << std::endl;
|
|
|
|
static int cnt = 0;
|
|
char cmd[100];
|
|
sprintf(cmd, "cp test0.aiger hard1/test%d_0.aiger", cnt);
|
|
system(cmd);
|
|
sprintf(cmd, "cp test1.aiger hard1/test%d_1.aiger", cnt);
|
|
system(cmd);
|
|
cnt++;
|
|
|
|
return str.find("equivalent") != std::string::npos;
|
|
}
|
|
|
|
int cal_input_related_size(aiger* aiger, int input) {
|
|
|
|
static int* used = new int[aiger->maxvar + 1];
|
|
memset(used, 0, (aiger->maxvar + 1) * sizeof(int));
|
|
|
|
std::queue<int> q;
|
|
q.push(input);
|
|
used[input] = true;
|
|
|
|
int result = 1;
|
|
|
|
while(!q.empty()) {
|
|
int cur = q.front();
|
|
q.pop();
|
|
for(auto& edge : graph.edge[cur]) {
|
|
int v = edge.to;
|
|
if(!used[v]) {
|
|
used[v] = true;
|
|
q.push(v);
|
|
result++;
|
|
}
|
|
}
|
|
}
|
|
return result;
|
|
}
|
|
|
|
|
|
#if ENABLE_MERGE_NODE
|
|
std::map<int, int> fa;
|
|
int father(int x) {
|
|
if(fa[x] == x) return x;
|
|
return fa[x] = father(fa[x]);
|
|
}
|
|
void merge_node(aiger* aiger, int x, int y) {
|
|
if(father(x) == father(y)) return;
|
|
|
|
x = father(x);
|
|
y = father(y);
|
|
|
|
std::vector<int> cone_x;
|
|
std::vector<int> cone_y;
|
|
std::vector<int> points_x;
|
|
points_x.push_back(x);
|
|
std::vector<int> points_y;
|
|
points_y.push_back(y);
|
|
get_cone_of_points(aiger, points_x, cone_x, 0);
|
|
get_cone_of_points(aiger, points_y, cone_y, 0);
|
|
|
|
if(cone_y.size() < cone_x.size()) std::swap(x, y);
|
|
|
|
fa[y] = x;
|
|
|
|
std::cout << "merge " << y << " to " << x << std::endl;
|
|
|
|
for(auto& edge : graph.edge[y]) {
|
|
int v = edge.to;
|
|
//std::cout << "v:" << v << std::endl;
|
|
for(auto &e : graph.redge[v]) {
|
|
if(e.to == y) e.to = x;
|
|
else if(e.to == y) e.to = x;
|
|
}
|
|
}
|
|
graph.edge[y].clear();
|
|
}
|
|
#endif
|
|
|
|
int main(int argv, char* args[]) {
|
|
|
|
// SATSolver sat;
|
|
// sat.new_vars(10);
|
|
|
|
// vector<Lit> vec;
|
|
|
|
// vec.clear();
|
|
// vec.push_back(Lit(1, true));
|
|
// vec.push_back(Lit(2, false));
|
|
// sat.add_clause(vec);
|
|
|
|
// vec.clear();
|
|
// vec.push_back(Lit(2, true));
|
|
// vec.push_back(Lit(1, false));
|
|
// sat.add_clause(vec);
|
|
|
|
// vector<unsigned> xor_clause;
|
|
// xor_clause.push_back(1);
|
|
// //xor_clause.push_back(2);
|
|
// log
|
|
|
|
// vec.clear();
|
|
// vec.push_back(Lit(2, false));
|
|
// sat.add_clause(vec);
|
|
|
|
// printf("%d\n", sat.solve() == l_True);
|
|
|
|
// return 0;
|
|
|
|
|
|
printf("c =================================== input =================================\n");
|
|
aiger* aiger = aiger_init();
|
|
FILE* file = fopen(args[1], "r");
|
|
aiger_read_from_file(aiger, file);
|
|
|
|
for(int i=0; i<aiger->num_ands; i++) {
|
|
auto gate = aiger->ands[i];
|
|
//cout << gate.lhs << " " << gate.rhs0 << " " << gate.rhs1 << endl;
|
|
graph.add(aiger_lit2var(gate.rhs0), aiger_lit2var(gate.lhs), gate.rhs0 & 1);
|
|
graph.add(aiger_lit2var(gate.rhs1), aiger_lit2var(gate.lhs), gate.rhs1 & 1);
|
|
}
|
|
printf("c inputs: \nc ");
|
|
|
|
for(int i=0; i<aiger->num_inputs; i++) {
|
|
printf("%d ", aiger->inputs[i].lit);
|
|
}
|
|
|
|
printf("\nc outputs: \nc ");
|
|
|
|
for(int i=0; i<aiger->num_outputs; i++) {
|
|
printf("%d ", aiger->outputs[i].lit);
|
|
}
|
|
printf("\nc maxvar: \nc %d\n", aiger->maxvar);
|
|
|
|
cal_topo_index(aiger);
|
|
|
|
printf("c max-topo-level: %d\n", topo_index[aiger_lit2var(aiger->outputs[0].lit)]);
|
|
|
|
int xor_cnt = 0;
|
|
for(int i=1; i<=aiger->maxvar; i++) {
|
|
if(match_xor(aiger, i) || match_equal(aiger, i)) xor_cnt++;
|
|
}
|
|
|
|
printf("c find xor: %d\n", xor_cnt);
|
|
|
|
// FILE* file1 = fopen("new.aig", "w");
|
|
// auto * aig = get_var_as_output_aiger(aiger, 156);
|
|
// aiger_write_to_file(aig, aiger_mode::aiger_binary_mode, file1);
|
|
// return 0;
|
|
|
|
classes.push_back(std::vector<int>());
|
|
for(int i=1; i<=aiger->maxvar; i++) {
|
|
classes[0].push_back(i);
|
|
}
|
|
|
|
int* result = new int[aiger->maxvar + 1];
|
|
int* input_vector = new int[aiger->num_inputs];
|
|
|
|
#if ENABLE_INPUT_VAR_DIVIED
|
|
|
|
std::vector<std::pair<int, int>> input_size;
|
|
for(int i=0; i<aiger->num_inputs; i++) {
|
|
int lit = aiger->inputs[i].lit;
|
|
int size = cal_input_related_size(aiger, lit);
|
|
input_size.push_back(std::make_pair(size, lit));
|
|
}
|
|
std::sort(input_size.begin(), input_size.end(), std::greater<std::pair<int, int>>());
|
|
|
|
for(int i=0; i<std::min((int)input_size.size(), DIVEDED_VAR_NUM); i++) {
|
|
init_inputs[input_size[i].second] = rand() % 2;
|
|
}
|
|
|
|
#endif
|
|
|
|
#if ENABLE_MERGE_NODE
|
|
for(int i=1; i<=aiger->maxvar; i++) fa[i] = i;
|
|
#endif
|
|
|
|
int const_zero[aiger->maxvar + 1];
|
|
int const_one[aiger->maxvar + 1];
|
|
for(int i=1; i<=aiger->maxvar; i++) {
|
|
const_zero[i] = const_one[i] = 1;
|
|
}
|
|
|
|
printf("c =================================== detect =================================\n");
|
|
for(int i=0; i<atoi(args[2]); i++) {
|
|
|
|
if(i % 10000 == 0) printf("c simulate count: %d\n", i);
|
|
|
|
for(int i=0; i<aiger->num_inputs; i++) {
|
|
input_vector[i] = rand() % 2;
|
|
|
|
#if ENABLE_INPUT_VAR_DIVIED
|
|
if(init_inputs.count(aiger->inputs[i].lit))
|
|
input_vector[i] = init_inputs[aiger->inputs[i].lit];
|
|
#endif
|
|
}
|
|
|
|
memset(result, -1, (aiger->maxvar + 1) * sizeof(int));
|
|
|
|
simulate(aiger, input_vector, result);
|
|
|
|
|
|
for(int i=1; i<=aiger->maxvar; i++) {
|
|
if(result[i] == 0) {
|
|
const_one[i] = 0;
|
|
}
|
|
if(result[i] == 1) {
|
|
const_zero[i] = 0;
|
|
}
|
|
if(result[i] == -1) {
|
|
printf("wrong\n");
|
|
exit(0);
|
|
}
|
|
}
|
|
|
|
|
|
std::vector<std::vector<int>> tmp;
|
|
for(auto& clas : classes) {
|
|
std::vector<int> v0;
|
|
std::vector<int> v1;
|
|
for(auto &v : clas) {
|
|
if(result[v]) v1.push_back(v);
|
|
else v0.push_back(v);
|
|
}
|
|
if(v0.size() > 1) tmp.push_back(v0);
|
|
if(v1.size() > 1) tmp.push_back(v1);
|
|
}
|
|
|
|
classes = tmp;
|
|
}
|
|
|
|
printf("c Number of equivalent classes: %d\n", classes.size());
|
|
printf("classes: \n");
|
|
for(auto& clas : classes) {
|
|
printf("[ ");
|
|
for(auto &v : clas) {
|
|
printf("%d ", v);
|
|
eqn.insert(v);
|
|
}
|
|
printf("]\n");
|
|
}
|
|
|
|
for(int i=1; i<=aiger->maxvar; i++) {
|
|
if(const_zero[i]) printf("const-zero: %d\n", i);
|
|
if(const_one[i]) printf("const-one: %d\n", i);
|
|
}
|
|
return 0;
|
|
|
|
printf("c =================================== some test code =================================\n");
|
|
|
|
// test(aiger);
|
|
// return 0;
|
|
|
|
for(auto& clas : classes) {
|
|
//if(clas.size() != 2) continue;
|
|
std::vector<int> tmp;
|
|
if(clas.size() > 100) {
|
|
printf("classes too big!\n");
|
|
continue;
|
|
}
|
|
|
|
for(int i=0; i<clas.size(); i++) {
|
|
for(int j=i+1; j<clas.size(); j++) {
|
|
|
|
std::vector<int> cone;
|
|
std::vector<int> pionts;
|
|
pionts.push_back(clas[i]);
|
|
pionts.push_back(clas[j]);
|
|
get_cone_of_points(aiger, pionts, cone, 0);
|
|
|
|
int vara = aiger_lit2var(clas[i]);
|
|
int varb = aiger_lit2var(clas[j]);
|
|
|
|
pairs.push_back(std::make_pair(cone.size(), std::make_pair(clas[i], clas[j])));
|
|
}
|
|
}
|
|
}
|
|
|
|
sort(pairs.begin(), pairs.end());
|
|
|
|
printf("c =================================== check =================================\n");
|
|
|
|
|
|
int s = 0;
|
|
printf("c Number of pairs detected: %d\n", pairs.size());
|
|
|
|
int pair_cnt = 0;
|
|
|
|
|
|
auto &p = pairs[pairs.size()-1];
|
|
auto ta = get_var_as_output_aiger(aiger, p.second.first);
|
|
auto tb = get_var_as_output_aiger(aiger, p.second.second);
|
|
FILE* f0 = fopen("test0.aiger", "w");
|
|
FILE* f1 = fopen("test1.aiger", "w");
|
|
|
|
//aiger_write_to_file(ta aiger_mode::aiger_binary_mode, f0);
|
|
//aiger_write_to_file(ta, aiger_mode::aiger_binary_mode, f1);
|
|
|
|
for(auto& pr : pairs) {
|
|
int a = pr.second.first;
|
|
int b = pr.second.second;
|
|
|
|
printf("[%d/%d] check-eq %d %d (max-topo: %d)\n",++pair_cnt, pairs.size(), a, b, pr.first);//13148
|
|
|
|
// bool eq1 = check_var_equal(aiger, a, b);
|
|
// bool eq2 = check_var_equal_new(aiger, a, b);
|
|
|
|
// if(eq1 != eq2) {
|
|
// printf("TEST FAILED\n");
|
|
// exit(0);
|
|
// }
|
|
|
|
#if ENABLE_MERGE_NODE
|
|
|
|
if(father(a) != father(b) && check_var_equal(aiger, father(a), father(b))) {
|
|
printf("result is eq: %d %d\n", a, b);
|
|
merge_node(aiger, a, b);
|
|
|
|
++s;
|
|
eqn.insert(a);
|
|
eqn.insert(b);
|
|
eqs.push_back(std::make_pair(a, b));
|
|
}
|
|
|
|
#else
|
|
|
|
if(check_var_equal(aiger, a, b)) {
|
|
printf("result is eq: %d %d\n", a, b);
|
|
++s;
|
|
eqn.insert(a);
|
|
eqn.insert(b);
|
|
eqs.push_back(std::make_pair(a, b));
|
|
}
|
|
|
|
#endif
|
|
}
|
|
printf("c Number of equivalent pairs: %d\n", s);
|
|
printf("checking entire graph...\n");
|
|
|
|
check_entire_problem(aiger);
|
|
|
|
return 0;
|
|
} |