2581 lines
67 KiB
Plaintext
2581 lines
67 KiB
Plaintext
#include "solve.hpp"
|
|
|
|
#include "cryptominisat.h"
|
|
#include <assert.h>
|
|
|
|
extern "C" {
|
|
#include "aiger.h"
|
|
}
|
|
|
|
|
|
|
|
#define ENABLE_INPUT_VAR_DIVIED 0
|
|
#define DIVEDED_VAR_NUM 48
|
|
|
|
#define ENABLE_MERGE_NODE 1
|
|
|
|
#if ENABLE_INPUT_VAR_DIVIED
|
|
std::map<int, int> init_inputs;
|
|
#endif
|
|
|
|
using namespace CMSat;
|
|
using std::vector;
|
|
|
|
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;
|
|
|
|
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<aiger->num_inputs; i++) {
|
|
aiger_add_input(result_aiger, aiger->inputs[i].lit, std::to_string(aiger->inputs[i].lit).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");
|
|
|
|
//printf("aiger maxvar %d\n", result_aiger->maxvar);
|
|
|
|
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 = ipasir_init();
|
|
|
|
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;
|
|
ipasir_add(solver, var);
|
|
ipasir_add(solver, 0);
|
|
}
|
|
#endif
|
|
|
|
while(!q.empty()) {
|
|
int u = q.front();
|
|
q.pop();
|
|
|
|
can_del++;
|
|
|
|
if(inputs.count(u)) 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;
|
|
}
|
|
|
|
ipasir_add(solver, -x), ipasir_add(solver, -y), ipasir_add(solver, 0);
|
|
ipasir_add(solver, x), ipasir_add(solver, y), ipasir_add(solver, 0);
|
|
|
|
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);
|
|
}
|
|
|
|
//printf("2one %d\n", can_del);
|
|
|
|
int result = ipasir_solve(solver);
|
|
|
|
ipasir_release(solver);
|
|
|
|
//printf("##### %d\n", result);
|
|
|
|
return result == 20;
|
|
}
|
|
|
|
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) {
|
|
|
|
solver = ipasir_init();
|
|
|
|
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;
|
|
}
|
|
|
|
|
|
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;
|
|
|
|
|
|
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 result = ipasir_solve(solver);
|
|
|
|
//ipasir_set_conflict_limit(solver, 100000);
|
|
|
|
ipasir_release(solver);
|
|
|
|
printf("c final: %d\n", result);
|
|
|
|
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[]) {
|
|
|
|
|
|
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)]);
|
|
|
|
|
|
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
|
|
|
|
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] == -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");
|
|
}
|
|
|
|
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;
|
|
|
|
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;
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
========================
|
|
#include "solve.hpp"
|
|
|
|
extern "C" {
|
|
#include "aiger.h"
|
|
}
|
|
|
|
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 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;
|
|
// }
|
|
// }
|
|
// }
|
|
// }
|
|
|
|
void simulate(aiger* aiger, int* input, int* result) {
|
|
|
|
std::queue<int> q;
|
|
|
|
for(int i=0; i<aiger->num_inputs; i++) {
|
|
result[aiger->inputs[i].lit] = input[i];
|
|
result[aiger->inputs[i].lit+1] = !input[i];
|
|
q.push(aiger_lit2var(aiger->inputs[i].lit));
|
|
}
|
|
|
|
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 = aiger_var2lit(rhs0_edge.to);
|
|
|
|
Graph::Edge rhs1_edge = graph.redge[v][1];
|
|
int rhs1 = aiger_var2lit(rhs1_edge.to);
|
|
|
|
result[aiger_var2lit(v)] = result[rhs0 + rhs0_edge.neg] & result[rhs1 + rhs1_edge.neg];
|
|
result[aiger_var2lit(v)+1] = !result[aiger_var2lit(v)];
|
|
|
|
//cout << "var: " << aiger_var2lit(v) << " = " << rhs0 + rhs0_edge.neg << " " << rhs1 + rhs1_edge.neg << " : " << result[aiger_var2lit(v)] << endl;
|
|
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
|
|
aiger* get_lit_as_output_aiger(aiger* aiger, unsigned lit) {
|
|
|
|
std::queue<int> q;
|
|
|
|
static int* used = new int[aiger->maxvar + 1];
|
|
memset(used, 0, (aiger->maxvar + 1) * sizeof(int));
|
|
|
|
q.push(aiger_lit2var(lit));
|
|
used[aiger_lit2var(lit)] = 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;
|
|
|
|
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<aiger->num_inputs; i++) {
|
|
aiger_add_input(result_aiger, aiger->inputs[i].lit, std::to_string(aiger->inputs[i].lit).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, lit, "238901893");
|
|
|
|
//printf("aiger maxvar %d\n", result_aiger->maxvar);
|
|
|
|
return result_aiger;
|
|
}
|
|
|
|
bool check_var_equal(aiger* aiger, int x, int y) {
|
|
|
|
//return true;
|
|
|
|
|
|
solver = ipasir_init();
|
|
|
|
//ipasir_reserve(solver, aiger->maxvar);
|
|
|
|
|
|
// for(int i=0; i<150; i++) {
|
|
// int var = aiger_lit2var(aiger->inputs[i].lit);
|
|
// if(rand() % 2) var = -var;
|
|
// ipasir_add(solver, var);
|
|
// ipasir_add(solver, 0);
|
|
// }
|
|
|
|
std::queue<int> q;
|
|
static int* used = new int[aiger->maxvar + 1];
|
|
memset(used, 0, (aiger->maxvar + 1) * sizeof(int));
|
|
|
|
x = x & 1 ? -aiger_lit2var(x) : aiger_lit2var(x);
|
|
y = y & 1 ? -aiger_lit2var(y) : aiger_lit2var(y);
|
|
|
|
q.push(abs(x));
|
|
q.push(abs(y));
|
|
int can_del = 2;
|
|
used[abs(x)] = true;
|
|
used[abs(y)] = 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(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;
|
|
|
|
|
|
//cout << "AND " << aiger_var2lit(u) << " " << (aiger_var2lit(a) + graph.redge[u][0].neg) << " " << (aiger_var2lit(b) + graph.redge[u][1].neg) << endl;
|
|
|
|
//aiger_add_and(aiger, aiger_var2lit(u), aiger_var2lit(a) + graph.redge[u][0].neg, aiger_var2lit(b) + graph.redge[u][1].neg);
|
|
//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(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, can_del++;
|
|
|
|
if(!used[b])
|
|
q.push(b), used[b] = true, can_del++;
|
|
}
|
|
|
|
ipasir_add(solver, -x), ipasir_add(solver, -y), ipasir_add(solver, 0);
|
|
ipasir_add(solver, x), ipasir_add(solver, y), ipasir_add(solver, 0);
|
|
|
|
for(auto& pair : eqs) {
|
|
int a = pair.first;
|
|
int b = pair.second;
|
|
// if (used[abs(a)] && used[abs(b)]) {
|
|
ipasir_add(solver, -a), ipasir_add(solver, b), ipasir_add(solver, 0);
|
|
ipasir_add(solver, a), ipasir_add(solver, -b), ipasir_add(solver, 0);
|
|
// }
|
|
// else printf("no used\n");
|
|
}
|
|
|
|
//ipasir_set_option(solver, "--time", 1);
|
|
//ipasir_set_conflict_limit(solver, 10000);
|
|
|
|
int result = ipasir_solve(solver);
|
|
|
|
printf("result is %d\n", result);
|
|
|
|
ipasir_release(solver);
|
|
if (result == 20) printf("can delete %d vars\n", can_del);
|
|
// printf("==============\n");
|
|
return result == 20;
|
|
}
|
|
|
|
|
|
int fa[100000];
|
|
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;
|
|
|
|
std::cout << "merge " << father(x) << " " << father(y) << std::endl;
|
|
|
|
x = aiger_lit2var(father(x));
|
|
y = aiger_lit2var(father(y));
|
|
|
|
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;
|
|
}
|
|
}
|
|
|
|
fa[y] = x;
|
|
|
|
graph.edge[y].clear();
|
|
}
|
|
|
|
void check_entire_problem(aiger* aiger) {
|
|
|
|
solver = ipasir_init();
|
|
|
|
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;
|
|
}
|
|
|
|
|
|
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;
|
|
|
|
|
|
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 result = ipasir_solve(solver);
|
|
|
|
//ipasir_set_conflict_limit(solver, 100000);
|
|
|
|
ipasir_release(solver);
|
|
|
|
printf("c final: %d\n", result);
|
|
|
|
return;
|
|
}
|
|
|
|
bool check_var_equal_new(aiger* aiger, int x, int y) {
|
|
auto aiger0 = get_lit_as_output_aiger(aiger, x);
|
|
auto aiger1 = get_lit_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;
|
|
}
|
|
|
|
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;
|
|
}
|
|
|
|
|
|
int main(int argv, char* args[]) {
|
|
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)]);
|
|
|
|
|
|
classes.push_back(std::vector<int>());
|
|
for(int i=2; i<=aiger->maxvar*2+1; i+=2) {
|
|
classes[0].push_back(i);
|
|
}
|
|
|
|
int* result = new int[2 * aiger->maxvar + 1];
|
|
int* input_vector = new int[aiger->num_inputs];
|
|
|
|
int tinput = 0;
|
|
|
|
printf("c =================================== detect =================================\n");
|
|
for(int i=0; i<atoi(args[2]); i++) {
|
|
|
|
if(i % 10000 == 0) printf("c simulate count: %d\n", i);
|
|
|
|
// if(tinput == (1 << aiger->num_inputs)) {
|
|
// cout << "simulate end!" << endl;
|
|
// break;
|
|
// }
|
|
// if(tinput % 1000 == 0) {
|
|
// cout << "simulate " << tinput << endl;
|
|
// }
|
|
// int tt = tinput;
|
|
// for(int i=0; i<aiger->num_inputs; i++) {
|
|
// input_vector[i] = tt & 1;
|
|
// tt >>= 1;
|
|
// }
|
|
// tinput++;
|
|
for(int i=0; i<aiger->num_inputs; i++) {
|
|
input_vector[i] = rand() % 2;
|
|
}
|
|
memset(result, -1, (2 * aiger->maxvar + 2) * sizeof(int));
|
|
|
|
simulate(aiger, input_vector, result);
|
|
|
|
for(int i=2; i<(2 * aiger->maxvar + 2); i++) {
|
|
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;
|
|
|
|
// cout << "classes: " << endl;
|
|
// for(auto& clas : classes) {
|
|
// cout << "[ ";
|
|
// for(auto &v : clas) {
|
|
// cout << v << " ";
|
|
// }
|
|
// cout << "]" << endl;
|
|
// }
|
|
}
|
|
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");
|
|
}
|
|
|
|
printf("c =================================== some test code =================================\n");
|
|
|
|
// test(aiger);
|
|
// return 0;
|
|
|
|
for(auto& clas : classes) {
|
|
//if(clas.size() != 2) continue;
|
|
std::vector<int> tmp;
|
|
|
|
for(int i=0; i<clas.size(); i++) {
|
|
for(int j=i+1; j<clas.size(); j++) {
|
|
int vara = aiger_lit2var(clas[i]);
|
|
int varb = aiger_lit2var(clas[j]);
|
|
pairs.push_back(std::make_pair(std::max(topo_index[vara], topo_index[varb]), std::make_pair(clas[i], clas[j])));
|
|
}
|
|
}
|
|
}
|
|
|
|
sort(pairs.begin(), pairs.end());
|
|
|
|
// test(aiger);
|
|
// exit(0);
|
|
|
|
printf("c =================================== check =================================\n");
|
|
|
|
// for(auto& pr : pairs) {
|
|
// printf("%d ", pr.first);
|
|
// }
|
|
// puts("");
|
|
|
|
// topo_cut(aiger, topo_index[aiger_lit2var(aiger->outputs[0].lit)] / 2);
|
|
// return 0;
|
|
|
|
int s = 0;
|
|
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;
|
|
|
|
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(check_var_equal(aiger, a, b)) {
|
|
printf("result is eq: %d %d\n", a, b);
|
|
++s;
|
|
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));
|
|
}
|
|
}
|
|
printf("c Number of equivalent pairs: %d\n", s);
|
|
printf("checking entire graph...\n");
|
|
|
|
check_entire_problem(aiger);
|
|
|
|
return 0;
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
#include "solve.hpp"
|
|
|
|
extern "C" {
|
|
#include "aiger.h"
|
|
}
|
|
|
|
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 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;
|
|
// }
|
|
// }
|
|
// }
|
|
// }
|
|
|
|
void simulate(aiger* aiger, int* input, int* result) {
|
|
|
|
std::queue<int> q;
|
|
|
|
for(int i=0; i<aiger->num_inputs; i++) {
|
|
result[aiger->inputs[i].lit] = input[i];
|
|
result[aiger->inputs[i].lit+1] = !input[i];
|
|
q.push(aiger_lit2var(aiger->inputs[i].lit));
|
|
}
|
|
|
|
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 = aiger_var2lit(rhs0_edge.to);
|
|
|
|
Graph::Edge rhs1_edge = graph.redge[v][1];
|
|
int rhs1 = aiger_var2lit(rhs1_edge.to);
|
|
|
|
result[aiger_var2lit(v)] = result[rhs0 + rhs0_edge.neg] & result[rhs1 + rhs1_edge.neg];
|
|
result[aiger_var2lit(v)+1] = !result[aiger_var2lit(v)];
|
|
|
|
//cout << "var: " << aiger_var2lit(v) << " = " << rhs0 + rhs0_edge.neg << " " << rhs1 + rhs1_edge.neg << " : " << result[aiger_var2lit(v)] << endl;
|
|
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
|
|
aiger* get_lit_as_output_aiger(aiger* aiger, unsigned lit) {
|
|
|
|
std::queue<int> q;
|
|
|
|
static int* used = new int[aiger->maxvar + 1];
|
|
memset(used, 0, (aiger->maxvar + 1) * sizeof(int));
|
|
|
|
q.push(aiger_lit2var(lit));
|
|
used[aiger_lit2var(lit)] = 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;
|
|
|
|
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<aiger->num_inputs; i++) {
|
|
aiger_add_input(result_aiger, aiger->inputs[i].lit, std::to_string(aiger->inputs[i].lit).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, lit, "238901893");
|
|
|
|
//printf("aiger maxvar %d\n", result_aiger->maxvar);
|
|
|
|
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) {
|
|
int var = aiger_lit2var(p);
|
|
q.push(var);
|
|
used[var] = 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) {
|
|
solver = ipasir_init();
|
|
|
|
std::queue<int> q;
|
|
static int* used = new int[aiger->maxvar + 1];
|
|
memset(used, 0, (aiger->maxvar + 1) * sizeof(int));
|
|
|
|
x = x & 1 ? -aiger_lit2var(x) : aiger_lit2var(x);
|
|
y = y & 1 ? -aiger_lit2var(y) : aiger_lit2var(y);
|
|
|
|
q.push(abs(x));
|
|
q.push(abs(y));
|
|
int can_del = 0;
|
|
used[abs(x)] = true;
|
|
used[abs(y)] = true;
|
|
|
|
// printf("[%d]inputs: ", inputs.size());
|
|
// for(auto& in : inputs) {
|
|
// printf("%d ", inputs);
|
|
// }
|
|
// printf("\n");
|
|
|
|
while(!q.empty()) {
|
|
int u = q.front();
|
|
q.pop();
|
|
|
|
can_del++;
|
|
|
|
if(inputs.count(u)) continue;
|
|
// if(graph.redge[u].size() == 0) {
|
|
// //printf("eeeeeeee %d\n", u);
|
|
// 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;
|
|
}
|
|
|
|
ipasir_add(solver, -x), ipasir_add(solver, -y), ipasir_add(solver, 0);
|
|
ipasir_add(solver, x), ipasir_add(solver, y), ipasir_add(solver, 0);
|
|
|
|
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);
|
|
}
|
|
|
|
printf("2one %d\n", can_del);
|
|
|
|
int result = ipasir_solve(solver);
|
|
|
|
ipasir_release(solver);
|
|
|
|
printf("##### %d\n", result);
|
|
|
|
return result == 20;
|
|
}
|
|
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);
|
|
}
|
|
|
|
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);
|
|
printf("insert %d\n", 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;
|
|
}
|
|
|
|
|
|
int fa[100000];
|
|
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;
|
|
|
|
std::cout << "merge " << father(x) << " " << father(y) << std::endl;
|
|
|
|
x = aiger_lit2var(father(x));
|
|
y = aiger_lit2var(father(y));
|
|
|
|
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;
|
|
}
|
|
}
|
|
|
|
fa[y] = x;
|
|
|
|
graph.edge[y].clear();
|
|
}
|
|
|
|
void check_entire_problem(aiger* aiger) {
|
|
|
|
solver = ipasir_init();
|
|
|
|
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;
|
|
}
|
|
|
|
|
|
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;
|
|
|
|
|
|
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 result = ipasir_solve(solver);
|
|
|
|
//ipasir_set_conflict_limit(solver, 100000);
|
|
|
|
ipasir_release(solver);
|
|
|
|
printf("c final: %d\n", result);
|
|
|
|
return;
|
|
}
|
|
|
|
bool check_var_equal_new(aiger* aiger, int x, int y) {
|
|
auto aiger0 = get_lit_as_output_aiger(aiger, x);
|
|
auto aiger1 = get_lit_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;
|
|
}
|
|
|
|
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;
|
|
}
|
|
|
|
|
|
int main(int argv, char* args[]) {
|
|
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)]);
|
|
|
|
|
|
classes.push_back(std::vector<int>());
|
|
for(int i=2; i<=aiger->maxvar*2+1; i+=2) {
|
|
classes[0].push_back(i);
|
|
}
|
|
|
|
int* result = new int[2 * aiger->maxvar + 1];
|
|
int* input_vector = new int[aiger->num_inputs];
|
|
|
|
int tinput = 0;
|
|
|
|
printf("c =================================== detect =================================\n");
|
|
for(int i=0; i<atoi(args[2]); i++) {
|
|
|
|
if(i % 10000 == 0) printf("c simulate count: %d\n", i);
|
|
|
|
// if(tinput == (1 << aiger->num_inputs)) {
|
|
// cout << "simulate end!" << endl;
|
|
// break;
|
|
// }
|
|
// if(tinput % 1000 == 0) {
|
|
// cout << "simulate " << tinput << endl;
|
|
// }
|
|
// int tt = tinput;
|
|
// for(int i=0; i<aiger->num_inputs; i++) {
|
|
// input_vector[i] = tt & 1;
|
|
// tt >>= 1;
|
|
// }
|
|
// tinput++;
|
|
for(int i=0; i<aiger->num_inputs; i++) {
|
|
input_vector[i] = rand() % 2;
|
|
}
|
|
memset(result, -1, (2 * aiger->maxvar + 2) * sizeof(int));
|
|
|
|
simulate(aiger, input_vector, result);
|
|
|
|
for(int i=2; i<(2 * aiger->maxvar + 2); i++) {
|
|
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;
|
|
|
|
// cout << "classes: " << endl;
|
|
// for(auto& clas : classes) {
|
|
// cout << "[ ";
|
|
// for(auto &v : clas) {
|
|
// cout << v << " ";
|
|
// }
|
|
// cout << "]" << endl;
|
|
// }
|
|
}
|
|
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");
|
|
}
|
|
|
|
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) 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());
|
|
|
|
// test(aiger);
|
|
// exit(0);
|
|
|
|
printf("c =================================== check =================================\n");
|
|
|
|
// for(auto& pr : pairs) {
|
|
// printf("%d ", pr.first);
|
|
// }
|
|
// puts("");
|
|
|
|
// topo_cut(aiger, topo_index[aiger_lit2var(aiger->outputs[0].lit)] / 2);
|
|
// return 0;
|
|
|
|
int s = 0;
|
|
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;
|
|
|
|
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(check_var_equal(aiger, a, b)) {
|
|
printf("result is eq: %d %d\n", a, b);
|
|
++s;
|
|
int x = a & 1 ? -aiger_lit2var(a) : aiger_lit2var(a);
|
|
int y = b & 1 ? -aiger_lit2var(b) : aiger_lit2var(b);
|
|
eqn.insert(x);
|
|
eqn.insert(y);
|
|
eqs.push_back(std::make_pair(x, y));
|
|
}
|
|
}
|
|
printf("c Number of equivalent pairs: %d\n", s);
|
|
printf("checking entire graph...\n");
|
|
|
|
check_entire_problem(aiger);
|
|
|
|
return 0;
|
|
} |