luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
abc/src/base/abci/abcSaucy.c

3347 lines
90 KiB
C
Raw Blame History

/**CFile****************************************************************
FileName [abcSaucy.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Symmetry Detection Package.]
Synopsis [Finds symmetries under permutation (but not negation) of I/Os.]
Author [Hadi Katebi]
Affiliation [University of Michigan]
Date [Ver. 1.0. Started - April, 2012.]
Revision [No revisions so far]
Comments []
Debugging [There are some part of the code that are commented out. Those parts mostly print
the contents of the data structures to the standard output. Un-comment them if you
find them useful for debugging.]
***********************************************************************/
#include "base/abc/abc.h"
#include "opt/sim/sim.h"
ABC_NAMESPACE_IMPL_START
/* on/off switches */
#define REFINE_BY_SIM_1 0
#define REFINE_BY_SIM_2 0
#define BACKTRACK_BY_SAT 1
#define SELECT_DYNAMICALLY 0
/* number of iterations for sim1 and sim2 refinements */
int NUM_SIM1_ITERATION;
int NUM_SIM2_ITERATION;
/* conflict analysis */
#define CLAUSE_DECAY 0.9
#define MAX_LEARNTS 50
/*
* saucy.c
*
* by Paul T. Darga <pdarga@umich.edu>
* and Mark Liffiton <liffiton@umich.edu>
* and Hadi Katebi <hadik@eecs.umich.edu>
*
* Copyright (C) 2004, The Regents of the University of Michigan
* See the LICENSE file for details.
*/
struct saucy_stats {
double grpsize_base;
int grpsize_exp;
int levels;
int nodes;
int bads;
int gens;
int support;
};
struct saucy_graph {
int n;
int e;
int *adj;
int *edg;
};
struct coloring {
int *lab; /* Labelling of objects */
int *unlab; /* Inverse of lab */
int *cfront; /* Pointer to front of cells */
int *clen; /* Length of cells (defined for cfront's) */
};
struct sim_result {
int *inVec;
int *outVec;
int inVecSignature;
int outVecOnes;
double activity;
};
struct saucy {
/* Graph data */
int n; /* Size of domain */
int *adj; /* Neighbors of k: edg[adj[k]]..edg[adj[k+1]] */
int *edg; /* Actual neighbor data */
int *dadj; /* Fanin neighbor indices, for digraphs */
int *dedg; /* Fanin neighbor data, for digraphs */
/* Coloring data */
struct coloring left, right;
int *nextnon; /* Forward next-nonsingleton pointers */
int *prevnon; /* Backward next-nonsingleton pointers */
/* Refinement: inducers */
char *indmark; /* Induce marks */
int *ninduce; /* Nonsingletons that might induce refinement */
int *sinduce; /* Singletons that might induce refinement */
int nninduce; /* Size of ninduce stack */
int nsinduce; /* Size of sinduce stack */
/* Refinement: marked cells */
int *clist; /* List of cells marked for refining */
int csize; /* Number of cells in clist */
/* Refinement: workspace */
char *stuff; /* Bit vector, but one char per bit */
int *ccount; /* Number of connections to refining cell */
int *bucket; /* Workspace */
int *count; /* Num vertices with same adj count to ref cell */
int *junk; /* More workspace */
int *gamma; /* Working permutation */
int *conncnts; /* Connection counts for cell fronts */
/* Search data */
int lev; /* Current search tree level */
int anc; /* Level of greatest common ancestor with zeta */
int *anctar; /* Copy of target cell at anc */
int kanctar; /* Location within anctar to iterate from */
int *start; /* Location of target at each level */
int indmin; /* Used for group size computation */
int match; /* Have we not diverged from previous left? */
/* Search: orbit partition */
int *theta; /* Running approximation of orbit partition */
int *thsize; /* Size of cells in theta, defined for mcrs */
int *thnext; /* Next rep in list (circular list) */
int *thprev; /* Previous rep in list */
int *threp; /* First rep for a given cell front */
int *thfront; /* The cell front associated with this rep */
/* Search: split record */
int *splitvar; /* The actual value of the splits on the left-most branch */
int *splitwho; /* List of where splits occurred */
int *splitfrom; /* List of cells which were split */
int *splitlev; /* Where splitwho/from begins for each level */
int nsplits; /* Number of splits at this point */
/* Search: differences from leftmost */
char *diffmark; /* Marked for diff labels */
int *diffs; /* List of diff labels */
int *difflev; /* How many labels diffed at each level */
int ndiffs; /* Current number of diffs */
int *undifflev; /* How many diff labels fixed at each level */
int nundiffs; /* Current number of diffs in singletons (fixed) */
int *unsupp; /* Inverted diff array */
int *specmin; /* Speculated mappings */
int *pairs; /* Not-undiffed diffs that can make two-cycles */
int *unpairs; /* Indices into pairs */
int npairs; /* Number of such pairs */
int *diffnons; /* Diffs that haven't been undiffed */
int *undiffnons; /* Inverse of that */
int ndiffnons; /* Number of such diffs */
/* Polymorphic functions */
int (*split)(struct saucy *, struct coloring *, int, int);
int (*is_automorphism)(struct saucy *);
int (*ref_singleton)(struct saucy *, struct coloring *, int);
int (*ref_nonsingle)(struct saucy *, struct coloring *, int);
void (*select_decomposition)(struct saucy *, int *, int *, int *);
/* Statistics structure */
struct saucy_stats *stats;
/* New data structures for Boolean formulas */
Abc_Ntk_t * pNtk;
Abc_Ntk_t * pNtk_permuted;
int * depAdj;
int * depEdg;
Vec_Int_t ** iDep, ** oDep;
Vec_Int_t ** obs, ** ctrl;
Vec_Ptr_t ** topOrder;
Vec_Ptr_t * randomVectorArray_sim1;
int * randomVectorSplit_sim1;
Vec_Ptr_t * randomVectorArray_sim2;
int * randomVectorSplit_sim2;
char * marks;
int * pModel;
Vec_Ptr_t * satCounterExamples;
double activityInc;
int fBooleanMatching;
int fPrintTree;
int fLookForSwaps;
FILE * gFile;
int (*refineBySim1)(struct saucy *, struct coloring *);
int (*refineBySim2)(struct saucy *, struct coloring *);
int (*print_automorphism)(FILE *f, int n, const int *gamma, int nsupp, const int *support, char * marks, Abc_Ntk_t * pNtk);
};
static int *ints(int n) { return ABC_ALLOC(int, n); }
static int *zeros(int n) { return ABC_CALLOC(int, n); }
static char *bits(int n) { return ABC_CALLOC(char, n); }
static char * getVertexName(Abc_Ntk_t *pNtk, int v);
static int * generateProperInputVector(Abc_Ntk_t * pNtk, struct coloring *c, Vec_Int_t * randomVector);
static int ifInputVectorsAreConsistent(struct saucy * s, int * leftVec, int * rightVec);
static int ifOutputVectorsAreConsistent(struct saucy * s, int * leftVec, int * rightVec);
static Vec_Ptr_t ** findTopologicalOrder(Abc_Ntk_t * pNtk);
static void getDependencies(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** oDep);
static struct saucy_graph * buildDepGraph (Abc_Ntk_t *pNtk, Vec_Int_t ** iDep, Vec_Int_t ** oDep);
static struct saucy_graph * buildSim1Graph(Abc_Ntk_t * pNtk, struct coloring *c, Vec_Int_t * randVec, Vec_Int_t ** iDep, Vec_Int_t ** oDep);
static struct saucy_graph * buildSim2Graph(Abc_Ntk_t * pNtk, struct coloring *c, Vec_Int_t * randVec, Vec_Int_t ** iDep, Vec_Int_t ** oDep, Vec_Ptr_t ** topOrder, Vec_Int_t ** obs, Vec_Int_t ** ctrl);
static Vec_Int_t * assignRandomBitsToCells(Abc_Ntk_t * pNtk, struct coloring *c);
static int Abc_NtkCecSat_saucy(Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel);
static struct sim_result * analyzeConflict(Abc_Ntk_t * pNtk, int * pModel, int fVerbose);
static void bumpActivity (struct saucy * s, struct sim_result * cex);
static void reduceDB(struct saucy * s);
static int
print_automorphism_ntk(FILE *f, int n, const int *gamma, int nsupp, const int *support, char * marks, Abc_Ntk_t * pNtk)
{
int i, j, k;
/* We presume support is already sorted */
for (i = 0; i < nsupp; ++i) {
k = support[i];
/* Skip elements already seen */
if (marks[k]) continue;
/* Start an orbit */
marks[k] = 1;
fprintf(f, "(%s", getVertexName(pNtk, k));
/* Mark and notify elements in this orbit */
for (j = gamma[k]; j != k; j = gamma[j]) {
marks[j] = 1;
fprintf(f, " %s", getVertexName(pNtk, j));
}
/* Finish off the orbit */
fprintf(f, ")");
}
fprintf(f, "\n");
/* Clean up after ourselves */
for (i = 0; i < nsupp; ++i) {
marks[support[i]] = 0;
}
return 1;
}
static int
print_automorphism_ntk2(FILE *f, int n, const int *gamma, int nsupp, const int *support, char * marks, Abc_Ntk_t * pNtk)
{
int i, j, k;
/* We presume support is already sorted */
for (i = 0; i < nsupp; ++i) {
k = support[i];
/* Skip elements already seen */
if (marks[k]) continue;
/* Start an orbit */
marks[k] = 1;
fprintf(f, "%d", k-1);
/* Mark and notify elements in this orbit */
for (j = gamma[k]; j != k; j = gamma[j]) {
marks[j] = 1;
fprintf(f, " %d ", j-1);
}
/* Finish off the orbit */
}
fprintf(f, "-1\n");
/* Clean up after ourselves */
for (i = 0; i < nsupp; ++i) {
marks[support[i]] = 0;
}
return 1;
}
static int
print_automorphism_quiet(FILE *f, int n, const int *gamma, int nsupp, const int *support, char * marks, Abc_Ntk_t * pNtk)
{
return 1;
}
static int
array_find_min(const int *a, int n)
{
const int *start = a, *end = a + n, *min = a;
while (++a != end) {
if (*a < *min) min = a;
}
return min - start;
}
static void
swap(int *a, int x, int y)
{
int tmp = a[x];
a[x] = a[y];
a[y] = tmp;
}
static void
sift_up(int *a, int k)
{
int p;
do {
p = k / 2;
if (a[k] <= a[p]) {
return;
}
else {
swap(a, k, p);
k = p;
}
} while (k > 1);
}
static void
sift_down(int *a, int n)
{
int p = 1, k = 2;
while (k <= n) {
if (k < n && a[k] < a[k+1]) ++k;
if (a[p] < a[k]) {
swap(a, p, k);
p = k;
k = 2 * p;
}
else {
return;
}
}
}
static void
heap_sort(int *a, int n)
{
int i;
for (i = 1; i < n; ++i) {
sift_up(a-1, i+1);
}
--i;
while (i > 0) {
swap(a, 0, i);
sift_down(a-1, i--);
}
}
static void
insertion_sort(int *a, int n)
{
int i, j, k;
for (i = 1; i < n; ++i) {
k = a[i];
for (j = i; j > 0 && a[j-1] > k; --j) {
a[j] = a[j-1];
}
a[j] = k;
}
}
static int
partition(int *a, int n, int m)
{
int f = 0, b = n;
for (;;) {
while (a[f] <= m) ++f;
do --b; while (m <= a[b]);
if (f < b) {
swap(a, f, b);
++f;
}
else break;
}
return f;
}
static int
log_base2(int n)
{
int k = 0;
while (n > 1) {
++k;
n >>= 1;
}
return k;
}
static int
median(int a, int b, int c)
{
if (a <= b) {
if (b <= c) return b;
if (a <= c) return c;
return a;
}
else {
if (a <= c) return a;
if (b <= c) return c;
return b;
}
}
static void
introsort_loop(int *a, int n, int lim)
{
int p;
while (n > 16) {
if (lim == 0) {
heap_sort(a, n);
return;
}
--lim;
p = partition(a, n, median(a[0], a[n/2], a[n-1]));
introsort_loop(a + p, n - p, lim);
n = p;
}
}
static void
introsort(int *a, int n)
{
introsort_loop(a, n, 2 * log_base2(n));
insertion_sort(a, n);
}
static int
do_find_min(struct coloring *c, int t)
{
return array_find_min(c->lab + t, c->clen[t] + 1) + t;
}
static int
find_min(struct saucy *s, int t)
{
return do_find_min(&s->right, t);
}
static void
set_label(struct coloring *c, int index, int value)
{
c->lab[index] = value;
c->unlab[value] = index;
}
static void
swap_labels(struct coloring *c, int a, int b)
{
int tmp = c->lab[a];
set_label(c, a, c->lab[b]);
set_label(c, b, tmp);
}
static void
move_to_back(struct saucy *s, struct coloring *c, int k)
{
int cf = c->cfront[k];
int cb = cf + c->clen[cf];
int offset = s->conncnts[cf]++;
/* Move this connected label to the back of its cell */
swap_labels(c, cb - offset, c->unlab[k]);
/* Add it to the cell list if it's the first one swapped */
if (!offset) s->clist[s->csize++] = cf;
}
static void
data_mark(struct saucy *s, struct coloring *c, int k)
{
int cf = c->cfront[k];
/* Move connects to the back of nonsingletons */
if (c->clen[cf]) move_to_back(s, c, k);
}
static void
data_count(struct saucy *s, struct coloring *c, int k)
{
int cf = c->cfront[k];
/* Move to back and count the number of connections */
if (c->clen[cf] && !s->ccount[k]++) move_to_back(s, c, k);
}
static int
check_mapping(struct saucy *s, const int *adj, const int *edg, int k)
{
int i, gk, ret = 1;
/* Mark gamma of neighbors */
for (i = adj[k]; i != adj[k+1]; ++i) {
s->stuff[s->gamma[edg[i]]] = 1;
}
/* Check neighbors of gamma */
gk = s->gamma[k];
for (i = adj[gk]; ret && i != adj[gk+1]; ++i) {
ret = s->stuff[edg[i]];
}
/* Clear out bit vector before we leave */
for (i = adj[k]; i != adj[k+1]; ++i) {
s->stuff[s->gamma[edg[i]]] = 0;
}
return ret;
}
static int
add_conterexample(struct saucy *s, struct sim_result * cex)
{
int i;
int nins = Abc_NtkPiNum(s->pNtk);
struct sim_result * savedcex;
cex->inVecSignature = 0;
for (i = 0; i < nins; i++) {
if (cex->inVec[i]) {
cex->inVecSignature += (cex->inVec[i] * i * i);
cex->inVecSignature ^= 0xABCD;
}
}
for (i = 0; i < Vec_PtrSize(s->satCounterExamples); i++) {
savedcex = (struct sim_result *)Vec_PtrEntry(s->satCounterExamples, i);
if (savedcex->inVecSignature == cex->inVecSignature) {
//bumpActivity(s, savedcex);
return 0;
}
}
Vec_PtrPush(s->satCounterExamples, cex);
bumpActivity(s, cex);
return 1;
}
static int
is_undirected_automorphism(struct saucy *s)
{
int i, j, ret;
for (i = 0; i < s->ndiffs; ++i) {
j = s->unsupp[i];
if (!check_mapping(s, s->adj, s->edg, j)) return 0;
}
ret = Abc_NtkCecSat_saucy(s->pNtk, s->pNtk_permuted, s->pModel);
if( BACKTRACK_BY_SAT && !ret ) {
struct sim_result * cex;
cex = analyzeConflict( s->pNtk, s->pModel, s->fPrintTree );
add_conterexample(s, cex);
cex = analyzeConflict( s->pNtk_permuted, s->pModel, s->fPrintTree );
add_conterexample(s, cex);
s->activityInc *= (1 / CLAUSE_DECAY);
if (Vec_PtrSize(s->satCounterExamples) >= MAX_LEARNTS)
reduceDB(s);
}
return ret;
}
static int
is_directed_automorphism(struct saucy *s)
{
int i, j;
for (i = 0; i < s->ndiffs; ++i) {
j = s->unsupp[i];
if (!check_mapping(s, s->adj, s->edg, j)) return 0;
if (!check_mapping(s, s->dadj, s->dedg, j)) return 0;
}
return 1;
}
static void
add_induce(struct saucy *s, struct coloring *c, int who)
{
if (!c->clen[who]) {
s->sinduce[s->nsinduce++] = who;
}
else {
s->ninduce[s->nninduce++] = who;
}
s->indmark[who] = 1;
}
static void
fix_fronts(struct coloring *c, int cf, int ff)
{
int i, end = cf + c->clen[cf];
for (i = ff; i <= end; ++i) {
c->cfront[c->lab[i]] = cf;
}
}
static void
array_indirect_sort(int *a, const int *b, int n)
{
int h, i, j, k;
/* Shell sort, as implemented in nauty, (C) Brendan McKay */
j = n / 3;
h = 1;
do { h = 3 * h + 1; } while (h < j);
do {
for (i = h; i < n; ++i) {
k = a[i];
for (j = i; b[a[j-h]] > b[k]; ) {
a[j] = a[j-h];
if ((j -= h) < h) break;
}
a[j] = k;
}
h /= 3;
} while (h > 0);
}
static int
at_terminal(struct saucy *s)
{
return s->nsplits == s->n;
}
static void
add_diffnon(struct saucy *s, int k)
{
/* Only add if we're in a consistent state */
if (s->ndiffnons == -1) return;
s->undiffnons[k] = s->ndiffnons;
s->diffnons[s->ndiffnons++] = k;
}
static void
remove_diffnon(struct saucy *s, int k)
{
int j;
if (s->undiffnons[k] == -1) return;
j = s->diffnons[--s->ndiffnons];
s->diffnons[s->undiffnons[k]] = j;
s->undiffnons[j] = s->undiffnons[k];
s->undiffnons[k] = -1;
}
static void
add_diff(struct saucy *s, int k)
{
if (!s->diffmark[k]) {
s->diffmark[k] = 1;
s->diffs[s->ndiffs++] = k;
add_diffnon(s, k);
}
}
static int
is_a_pair(struct saucy *s, int k)
{
return s->unpairs[k] != -1;
}
static int
in_cell_range(struct coloring *c, int ff, int cf)
{
int cb = cf + c->clen[cf];
return cf <= ff && ff <= cb;
}
static void
add_pair(struct saucy *s, int k)
{
if (s->npairs != -1) {
s->unpairs[k] = s->npairs;
s->pairs[s->npairs++] = k;
}
}
static void
eat_pair(struct saucy *s, int k)
{
int j;
j = s->pairs[--s->npairs];
s->pairs[s->unpairs[k]] = j;
s->unpairs[j] = s->unpairs[k];
s->unpairs[k] = -1;
}
static void
pick_all_the_pairs(struct saucy *s)
{
int i;
for (i = 0; i < s->npairs; ++i) {
s->unpairs[s->pairs[i]] = -1;
}
s->npairs = 0;
}
static void
clear_undiffnons(struct saucy *s)
{
int i;
for (i = 0 ; i < s->ndiffnons ; ++i) {
s->undiffnons[s->diffnons[i]] = -1;
}
}
static void
fix_diff_singleton(struct saucy *s, int cf)
{
int r = s->right.lab[cf];
int l = s->left.lab[cf];
int rcfl;
if (!s->right.clen[cf] && r != l) {
/* Make sure diff is marked */
add_diff(s, r);
/* It is now undiffed since it is singleton */
++s->nundiffs;
remove_diffnon(s, r);
/* Mark the other if not singleton already */
rcfl = s->right.cfront[l];
if (s->right.clen[rcfl]) {
add_diff(s, l);
/* Check for pairs */
if (in_cell_range(&s->right, s->left.unlab[r], rcfl)) {
add_pair(s, l);
}
}
/* Otherwise we might be eating a pair */
else if (is_a_pair(s, r)) {
eat_pair(s, r);
}
}
}
static void
fix_diff_subtract(struct saucy *s, int cf, const int *a, const int *b)
{
int i, k;
int cb = cf + s->right.clen[cf];
/* Mark the contents of the first set */
for (i = cf; i <= cb; ++i) {
s->stuff[a[i]] = 1;
}
/* Add elements from second set not present in the first */
for (i = cf; i <= cb; ++i) {
k = b[i];
if (!s->stuff[k]) add_diff(s, k);
}
/* Clear the marks of the first set */
for (i = cf; i <= cb; ++i) {
s->stuff[a[i]] = 0;
}
}
static void
fix_diffs(struct saucy *s, int cf, int ff)
{
int min;
/* Check for singleton cases in both cells */
fix_diff_singleton(s, cf);
fix_diff_singleton(s, ff);
/* If they're both nonsingleton, do subtraction on smaller */
if (s->right.clen[cf] && s->right.clen[ff]) {
min = s->right.clen[cf] < s->right.clen[ff] ? cf : ff;
fix_diff_subtract(s, min, s->left.lab, s->right.lab);
fix_diff_subtract(s, min, s->right.lab, s->left.lab);
}
}
static void
split_color(struct coloring *c, int cf, int ff)
{
int cb, fb;
/* Fix lengths */
fb = ff - 1;
cb = cf + c->clen[cf];
c->clen[cf] = fb - cf;
c->clen[ff] = cb - ff;
/* Fix cell front pointers */
fix_fronts(c, ff, ff);
}
static void
split_common(struct saucy *s, struct coloring *c, int cf, int ff)
{
split_color(c, cf, ff);
/* Add to refinement */
if (s->indmark[cf] || c->clen[ff] < c->clen[cf]) {
add_induce(s, c, ff);
}
else {
add_induce(s, c, cf);
}
}
static int
split_left(struct saucy *s, struct coloring *c, int cf, int ff)
{
/* Record the split */
s->splitwho[s->nsplits] = ff;
s->splitfrom[s->nsplits] = cf;
++s->nsplits;
/* Do common splitting tasks */
split_common(s, c, cf, ff);
/* Always succeeds */
return 1;
}
static int
split_init(struct saucy *s, struct coloring *c, int cf, int ff)
{
split_left(s, c, cf, ff);
/* Maintain nonsingleton list for finding new targets */
if (c->clen[ff]) {
s->prevnon[s->nextnon[cf]] = ff;
s->nextnon[ff] = s->nextnon[cf];
s->prevnon[ff] = cf;
s->nextnon[cf] = ff;
}
if (!c->clen[cf]) {
s->nextnon[s->prevnon[cf]] = s->nextnon[cf];
s->prevnon[s->nextnon[cf]] = s->prevnon[cf];
}
/* Always succeeds */
return 1;
}
static int
split_other(struct saucy *s, struct coloring *c, int cf, int ff)
{
int k = s->nsplits;
/* Verify the split with init */
if (s->splitwho[k] != ff || s->splitfrom[k] != cf
|| k >= s->splitlev[s->lev]) {
return 0;
}
++s->nsplits;
/* Do common splitting tasks */
split_common(s, c, cf, ff);
/* Fix differences with init */
fix_diffs(s, cf, ff);
/* If we got this far we succeeded */
return 1;
}
static int
print_partition(struct coloring *left, struct coloring *right, int n, Abc_Ntk_t * pNtk, int fNames)
{
int i, j;
printf("top = |");
for(i = 0; i < n; i += (left->clen[i]+1)) {
for(j = 0; j < (left->clen[i]+1); j++) {
if (fNames) printf("%s ", getVertexName(pNtk, left->lab[i+j]));
else printf("%d ", left->lab[i+j]);
}
if((i+left->clen[i]+1) < n) printf("|");
}
printf("|\n");
/*printf("(cfront = {");
for (i = 0; i < n; i++)
printf("%d ", left->cfront[i]);
printf("})\n");*/
if (right == NULL) return 1;
printf("bot = |");
for(i = 0; i < n; i += (right->clen[i]+1)) {
for(j = 0; j < (right->clen[i]+1); j++) {
if (fNames) printf("%s ", getVertexName(pNtk, right->lab[i+j]));
else printf("%d ", right->lab[i+j]);
}
if((i+right->clen[i]+1) < n) printf("|");
}
printf("|\n");
/*printf("(cfront = {");
for (i = 0; i < n; i++)
printf("%d ", right->cfront[i]);
printf("})\n");*/
return 1;
}
static int
refine_cell(struct saucy *s, struct coloring *c,
int (*refine)(struct saucy *, struct coloring *, int))
{
int i, cf, ret = 1;
/*
* The connected list must be consistent. This is for
* detecting mappings across nodes at a given level. However,
* at the root of the tree, we never have to map with another
* node, so we lack this consistency constraint in that case.
*/
if (s->lev > 1) introsort(s->clist, s->csize);
/* Now iterate over the marked cells */
for (i = 0; ret && i < s->csize; ++i) {
cf = s->clist[i];
ret = refine(s, c, cf);
}
/* Clear the connected marks */
for (i = 0; i < s->csize; ++i) {
cf = s->clist[i];
s->conncnts[cf] = 0;
}
s->csize = 0;
return ret;
}
static int
maybe_split(struct saucy *s, struct coloring *c, int cf, int ff)
{
return cf == ff ? 1 : s->split(s, c, cf, ff);
}
static int
ref_single_cell(struct saucy *s, struct coloring *c, int cf)
{
int zcnt = c->clen[cf] + 1 - s->conncnts[cf];
return maybe_split(s, c, cf, cf + zcnt);
}
static int
ref_singleton(struct saucy *s, struct coloring *c,
const int *adj, const int *edg, int cf)
{
int i, k = c->lab[cf];
/* Find the cells we're connected to, and mark our neighbors */
for (i = adj[k]; i != adj[k+1]; ++i) {
data_mark(s, c, edg[i]);
}
/* Refine the cells we're connected to */
return refine_cell(s, c, ref_single_cell);
}
static int
ref_singleton_directed(struct saucy *s, struct coloring *c, int cf)
{
return ref_singleton(s, c, s->adj, s->edg, cf)
&& ref_singleton(s, c, s->dadj, s->dedg, cf);
}
static int
ref_singleton_undirected(struct saucy *s, struct coloring *c, int cf)
{
return ref_singleton(s, c, s->adj, s->edg, cf);
}
static int
ref_nonsingle_cell(struct saucy *s, struct coloring *c, int cf)
{
int cnt, i, cb, nzf, ff, fb, bmin, bmax;
/* Find the front and back */
cb = cf + c->clen[cf];
nzf = cb - s->conncnts[cf] + 1;
/* Prepare the buckets */
ff = nzf;
cnt = s->ccount[c->lab[ff]];
s->count[ff] = bmin = bmax = cnt;
s->bucket[cnt] = 1;
/* Iterate through the rest of the vertices */
while (++ff <= cb) {
cnt = s->ccount[c->lab[ff]];
/* Initialize intermediate buckets */
while (bmin > cnt) s->bucket[--bmin] = 0;
while (bmax < cnt) s->bucket[++bmax] = 0;
/* Mark this count */
++s->bucket[cnt];
s->count[ff] = cnt;
}
/* If they all had the same count, bail */
if (bmin == bmax && cf == nzf) return 1;
ff = fb = nzf;
/* Calculate bucket locations, sizes */
for (i = bmin; i <= bmax; ++i, ff = fb) {
if (!s->bucket[i]) continue;
fb = ff + s->bucket[i];
s->bucket[i] = fb;
}
/* Repair the partition nest */
for (i = nzf; i <= cb; ++i) {
s->junk[--s->bucket[s->count[i]]] = c->lab[i];
}
for (i = nzf; i <= cb; ++i) {
set_label(c, i, s->junk[i]);
}
/* Split; induce */
for (i = bmax; i > bmin; --i) {
ff = s->bucket[i];
if (ff && !s->split(s, c, cf, ff)) return 0;
}
/* If there was a zero area, then there's one more cell */
return maybe_split(s, c, cf, s->bucket[bmin]);
}
static int
ref_nonsingle(struct saucy *s, struct coloring *c,
const int *adj, const int *edg, int cf)
{
int i, j, k, ret;
const int cb = cf + c->clen[cf];
const int size = cb - cf + 1;
/* Double check for nonsingles which became singles later */
if (cf == cb) {
return ref_singleton(s, c, adj, edg, cf);
}
/* Establish connected list */
memcpy(s->junk, c->lab + cf, size * sizeof(int));
for (i = 0; i < size; ++i) {
k = s->junk[i];
for (j = adj[k]; j != adj[k+1]; ++j) {
data_count(s, c, edg[j]);
}
}
/* Refine the cells we're connected to */
ret = refine_cell(s, c, ref_nonsingle_cell);
/* Clear the counts; use lab because junk was overwritten */
for (i = cf; i <= cb; ++i) {
k = c->lab[i];
for (j = adj[k]; j != adj[k+1]; ++j) {
s->ccount[edg[j]] = 0;
}
}
return ret;
}
static int
ref_nonsingle_directed(struct saucy *s, struct coloring *c, int cf)
{
return ref_nonsingle(s, c, s->adj, s->edg, cf)
&& ref_nonsingle(s, c, s->dadj, s->dedg, cf);
}
static int
ref_nonsingle_undirected(struct saucy *s, struct coloring *c, int cf)
{
return ref_nonsingle(s, c, s->adj, s->edg, cf);
}
static void
clear_refine(struct saucy *s)
{
int i;
for (i = 0; i < s->nninduce; ++i) {
s->indmark[s->ninduce[i]] = 0;
}
for (i = 0; i < s->nsinduce; ++i) {
s->indmark[s->sinduce[i]] = 0;
}
s->nninduce = s->nsinduce = 0;
}
static int
refine(struct saucy *s, struct coloring *c)
{
int front;
/* Keep going until refinement stops */
while (1) {
/* If discrete, bail */
if (at_terminal(s)) {
clear_refine(s);
return 1;
};
/* Look for something else to refine on */
if (s->nsinduce) {
front = s->sinduce[--s->nsinduce];
s->indmark[front] = 0;
if (!s->ref_singleton(s, c, front)) break;
}
else if (s->nninduce) {
front = s->ninduce[--s->nninduce];
s->indmark[front] = 0;
if (!s->ref_nonsingle(s, c, front)) break;
}
else {
return 1;
};
}
clear_refine(s);
return 0;
}
static int
refineByDepGraph(struct saucy *s, struct coloring *c)
{
s->adj = s->depAdj;
s->edg = s->depEdg;
return refine(s, c);
}
static int
backtrackBysatCounterExamples(struct saucy *s, struct coloring *c)
{
int i, j, res;
struct sim_result * cex1, * cex2;
int * flag = zeros(Vec_PtrSize(s->satCounterExamples));
if (c == &s->left) return 1;
if (Vec_PtrSize(s->satCounterExamples) == 0) return 1;
for (i = 0; i < Vec_PtrSize(s->satCounterExamples); i++) {
cex1 = (struct sim_result *)Vec_PtrEntry(s->satCounterExamples, i);
for (j = 0; j < Vec_PtrSize(s->satCounterExamples); j++) {
if (flag[j]) continue;
cex2 = (struct sim_result *)Vec_PtrEntry(s->satCounterExamples, j);
res = ifInputVectorsAreConsistent(s, cex1->inVec, cex2->inVec);
if (res == -2) {
flag[j] = 1;
continue;
}
if (res == -1) break;
if (res == 0) continue;
if (cex1->outVecOnes != cex2->outVecOnes) {
bumpActivity(s, cex1);
bumpActivity(s, cex2);
ABC_FREE(flag);
return 0;
}
/* if two input vectors produce the same number of ones (look above), and
* pNtk's number of outputs is 1, then output vectors are definitely consistent. */
if (Abc_NtkPoNum(s->pNtk) == 1) continue;
if (!ifOutputVectorsAreConsistent(s, cex1->outVec, cex2->outVec)) {
bumpActivity(s, cex1);
bumpActivity(s, cex2);
ABC_FREE(flag);
return 0;
}
}
}
ABC_FREE(flag);
return 1;
}
static int
refineBySim1_init(struct saucy *s, struct coloring *c)
{
struct saucy_graph *g;
Vec_Int_t * randVec;
int i, j;
int allOutputsAreDistinguished;
int nsplits;
if (Abc_NtkPoNum(s->pNtk) == 1) return 1;
for (i = 0; i < NUM_SIM1_ITERATION; i++) {
/* if all outputs are distinguished, quit */
allOutputsAreDistinguished = 1;
for (j = 0; j < Abc_NtkPoNum(s->pNtk); j++) {
if (c->clen[j]) {
allOutputsAreDistinguished = 0;
break;
}
}
if (allOutputsAreDistinguished) break;
randVec = assignRandomBitsToCells(s->pNtk, c);
g = buildSim1Graph(s->pNtk, c, randVec, s->iDep, s->oDep);
assert(g != NULL);
s->adj = g->adj;
s->edg = g->edg;
nsplits = s->nsplits;
for (j = 0; j < s->n; j += c->clen[j]+1)
add_induce(s, c, j);
refine(s, c);
if (s->nsplits > nsplits) {
i = 0; /* reset i */
/* do more refinement by dependency graph */
for (j = 0; j < s->n; j += c->clen[j]+1)
add_induce(s, c, j);
refineByDepGraph(s, c);
}
Vec_IntFree(randVec);
ABC_FREE( g->adj );
ABC_FREE( g->edg );
ABC_FREE( g );
}
return 1;
}
static int
refineBySim1_left(struct saucy *s, struct coloring *c)
{
struct saucy_graph *g;
Vec_Int_t * randVec;
int i, j;
int allOutputsAreDistinguished;
int nsplits;
if (Abc_NtkPoNum(s->pNtk) == 1) return 1;
for (i = 0; i < NUM_SIM1_ITERATION; i++) {
/* if all outputs are distinguished, quit */
allOutputsAreDistinguished = 1;
for (j = 0; j < Abc_NtkPoNum(s->pNtk); j++) {
if (c->clen[j]) {
allOutputsAreDistinguished = 0;
break;
}
}
if (allOutputsAreDistinguished) break;
randVec = assignRandomBitsToCells(s->pNtk, c);
g = buildSim1Graph(s->pNtk, c, randVec, s->iDep, s->oDep);
assert(g != NULL);
s->adj = g->adj;
s->edg = g->edg;
nsplits = s->nsplits;
for (j = 0; j < s->n; j += c->clen[j]+1)
add_induce(s, c, j);
refine(s, c);
if (s->nsplits > nsplits) {
/* save the random vector */
Vec_PtrPush(s->randomVectorArray_sim1, randVec);
i = 0; /* reset i */
/* do more refinement by dependency graph */
for (j = 0; j < s->n; j += c->clen[j]+1)
add_induce(s, c, j);
refineByDepGraph(s, c);
}
else
Vec_IntFree(randVec);
ABC_FREE( g->adj );
ABC_FREE( g->edg );
ABC_FREE( g );
}
s->randomVectorSplit_sim1[s->lev] = Vec_PtrSize(s->randomVectorArray_sim1);
return 1;
}
static int
refineBySim1_other(struct saucy *s, struct coloring *c)
{
struct saucy_graph *g;
Vec_Int_t * randVec;
int i, j;
int ret, nsplits;
for (i = s->randomVectorSplit_sim1[s->lev-1]; i < s->randomVectorSplit_sim1[s->lev]; i++) {
randVec = (Vec_Int_t *)Vec_PtrEntry(s->randomVectorArray_sim1, i);
g = buildSim1Graph(s->pNtk, c, randVec, s->iDep, s->oDep);
if (g == NULL) {
assert(c == &s->right);
return 0;
}
s->adj = g->adj;
s->edg = g->edg;
nsplits = s->nsplits;
for (j = 0; j < s->n; j += c->clen[j]+1)
add_induce(s, c, j);
ret = refine(s, c);
if (s->nsplits == nsplits) {
assert(c == &s->right);
ret = 0;
}
if (ret) {
/* do more refinement now by dependency graph */
for (j = 0; j < s->n; j += c->clen[j]+1)
add_induce(s, c, j);
ret = refineByDepGraph(s, c);
}
ABC_FREE( g->adj );
ABC_FREE( g->edg );
ABC_FREE( g );
if (!ret) return 0;
}
return 1;
}
static int
refineBySim2_init(struct saucy *s, struct coloring *c)
{
struct saucy_graph *g;
Vec_Int_t * randVec;
int i, j;
int nsplits;
for (i = 0; i < NUM_SIM2_ITERATION; i++) {
randVec = assignRandomBitsToCells(s->pNtk, c);
g = buildSim2Graph(s->pNtk, c, randVec, s->iDep, s->oDep, s->topOrder, s->obs, s->ctrl);
assert(g != NULL);
s->adj = g->adj;
s->edg = g->edg;
nsplits = s->nsplits;
for (j = 0; j < s->n; j += c->clen[j]+1)
add_induce(s, c, j);
refine(s, c);
if (s->nsplits > nsplits) {
i = 0; /* reset i */
/* do more refinement by dependency graph */
for (j = 0; j < s->n; j += c->clen[j]+1)
add_induce(s, c, j);
refineByDepGraph(s, c);
}
Vec_IntFree(randVec);
ABC_FREE( g->adj );
ABC_FREE( g->edg );
ABC_FREE( g );
}
return 1;
}
static int
refineBySim2_left(struct saucy *s, struct coloring *c)
{
struct saucy_graph *g;
Vec_Int_t * randVec;
int i, j;
int nsplits;
for (i = 0; i < NUM_SIM2_ITERATION; i++) {
randVec = assignRandomBitsToCells(s->pNtk, c);
g = buildSim2Graph(s->pNtk, c, randVec, s->iDep, s->oDep, s->topOrder, s->obs, s->ctrl);
assert(g != NULL);
s->adj = g->adj;
s->edg = g->edg;
nsplits = s->nsplits;
for (j = 0; j < s->n; j += c->clen[j]+1)
add_induce(s, c, j);
refine(s, c);
if (s->nsplits > nsplits) {
/* save the random vector */
Vec_PtrPush(s->randomVectorArray_sim2, randVec);
i = 0; /* reset i */
/* do more refinement by dependency graph */
for (j = 0; j < s->n; j += c->clen[j]+1)
add_induce(s, c, j);
refineByDepGraph(s, c);
}
else
Vec_IntFree(randVec);
ABC_FREE( g->adj );
ABC_FREE( g->edg );
ABC_FREE( g );
}
s->randomVectorSplit_sim2[s->lev] = Vec_PtrSize(s->randomVectorArray_sim2);
return 1;
}
static int
refineBySim2_other(struct saucy *s, struct coloring *c)
{
struct saucy_graph *g;
Vec_Int_t * randVec;
int i, j;
int ret, nsplits;
for (i = s->randomVectorSplit_sim2[s->lev-1]; i < s->randomVectorSplit_sim2[s->lev]; i++) {
randVec = (Vec_Int_t *)Vec_PtrEntry(s->randomVectorArray_sim2, i);
g = buildSim2Graph(s->pNtk, c, randVec, s->iDep, s->oDep, s->topOrder, s->obs, s->ctrl);
if (g == NULL) {
assert(c == &s->right);
return 0;
}
s->adj = g->adj;
s->edg = g->edg;
nsplits = s->nsplits;
for (j = 0; j < s->n; j += c->clen[j]+1)
add_induce(s, c, j);
ret = refine(s, c);
if (s->nsplits == nsplits) {
assert(c == &s->right);
ret = 0;
}
if (ret) {
/* do more refinement by dependency graph */
for (j = 0; j < s->n; j += c->clen[j]+1)
add_induce(s, c, j);
ret = refineByDepGraph(s, c);
}
ABC_FREE( g->adj );
ABC_FREE( g->edg );
ABC_FREE( g );
if (!ret) {
assert(c == &s->right);
return 0;
}
}
return 1;
}
static int
check_OPP_only_has_swaps(struct saucy *s, struct coloring *c)
{
int j, cell;
Vec_Int_t * left_cfront, * right_cfront;
if (c == &s->left)
return 1;
left_cfront = Vec_IntAlloc (1);
right_cfront = Vec_IntAlloc (1);
for (cell = 0; cell < s->n; cell += (s->left.clen[cell]+1)) {
for (j = cell; j <= (cell+s->left.clen[cell]); j++) {
Vec_IntPush(left_cfront, s->left.cfront[s->right.lab[j]]);
Vec_IntPush(right_cfront, s->right.cfront[s->left.lab[j]]);
}
Vec_IntSortUnsigned(left_cfront);
Vec_IntSortUnsigned(right_cfront);
for (j = 0; j < Vec_IntSize(left_cfront); j++) {
if (Vec_IntEntry(left_cfront, j) != Vec_IntEntry(right_cfront, j)) {
Vec_IntFree(left_cfront);
Vec_IntFree(right_cfront);
return 0;
}
}
Vec_IntClear(left_cfront);
Vec_IntClear(right_cfront);
}
Vec_IntFree(left_cfront);
Vec_IntFree(right_cfront);
return 1;
}
static int
check_OPP_for_Boolean_matching(struct saucy *s, struct coloring *c)
{
int j, cell;
int countN1Left, countN2Left;
int countN1Right, countN2Right;
char *name;
if (c == &s->left)
return 1;
for (cell = 0; cell < s->n; cell += (s->right.clen[cell]+1)) {
countN1Left = countN2Left = countN1Right = countN2Right = 0;
for (j = cell; j <= (cell+s->right.clen[cell]); j++) {
name = getVertexName(s->pNtk, s->left.lab[j]);
assert(name[0] == 'N' && name[2] == ':');
if (name[1] == '1')
countN1Left++;
else {
assert(name[1] == '2');
countN2Left++;
}
name = getVertexName(s->pNtk, s->right.lab[j]);
assert(name[0] == 'N' && name[2] == ':');
if (name[1] == '1')
countN1Right++;
else {
assert(name[1] == '2');
countN2Right++;
}
}
if (countN1Left != countN2Right || countN2Left != countN1Right)
return 0;
}
return 1;
}
static int
double_check_OPP_isomorphism(struct saucy *s, struct coloring * c)
{
/* This is the new enhancement in saucy 3.0 */
int i, j, v, sum1, sum2, xor1, xor2;
if (c == &s->left)
return 1;
for (i = s->nsplits - 1; i > s->splitlev[s->lev-1]; --i) {
v = c->lab[s->splitwho[i]];
sum1 = xor1 = 0;
for (j = s->adj[v]; j < s->adj[v+1]; j++) {
sum1 += c->cfront[s->edg[j]];
xor1 ^= c->cfront[s->edg[j]];
}
v = s->left.lab[s->splitwho[i]];
sum2 = xor2 = 0;
for (j = s->adj[v]; j < s->adj[v+1]; j++) {
sum2 += s->left.cfront[s->edg[j]];
xor2 ^= s->left.cfront[s->edg[j]];
}
if ((sum1 != sum2) || (xor1 != xor2))
return 0;
v = c->lab[s->splitfrom[i]];
sum1 = xor1 = 0;
for (j = s->adj[v]; j < s->adj[v+1]; j++) {
sum1 += c->cfront[s->edg[j]];
xor1 ^= c->cfront[s->edg[j]];
}
v = s->left.lab[s->splitfrom[i]];
sum2 = xor2 = 0;
for (j = s->adj[v]; j < s->adj[v+1]; j++) {
sum2 += s->left.cfront[s->edg[j]];
xor2 ^= s->left.cfront[s->edg[j]];
}
if ((sum1 != sum2) || (xor1 != xor2))
return 0;
}
return 1;
}
static int
descend(struct saucy *s, struct coloring *c, int target, int min)
{
int back = target + c->clen[target];
/* Count this node */
++s->stats->nodes;
/* Move the minimum label to the back */
swap_labels(c, min, back);
/* Split the cell */
s->difflev[s->lev] = s->ndiffs;
s->undifflev[s->lev] = s->nundiffs;
++s->lev;
s->split(s, c, target, back);
/* Now go and do some work */
//print_partition(&s->left, NULL, s->n, s->pNtk, 1);
if (!refineByDepGraph(s, c)) return 0;
/* if we are looking for a Boolean matching, check the OPP and
* backtrack if the OPP maps part of one network to itself */
if (s->fBooleanMatching && !check_OPP_for_Boolean_matching(s, c)) return 0;
//print_partition(&s->left, NULL, s->n, s->pNtk, 1);
if (REFINE_BY_SIM_1 && !s->refineBySim1(s, c)) return 0;
//print_partition(&s->left, NULL, s->n, s->pNtk, 1);
if (REFINE_BY_SIM_2 && !s->refineBySim2(s, c)) return 0;
/* do the check once more, maybe the check fails, now that refinement is complete */
if (s->fBooleanMatching && !check_OPP_for_Boolean_matching(s, c)) return 0;
if (s->fLookForSwaps && !check_OPP_only_has_swaps(s, c)) return 0;
if (!double_check_OPP_isomorphism(s, c)) return 0;
return 1;
}
static int
select_smallest_max_connected_cell(struct saucy *s, int start, int end)
{
int smallest_cell = -1, cell;
int smallest_cell_size = s->n;
int max_connections = -1;
int * connection_list = zeros(s->n);
cell = start;
while( !s->left.clen[cell] ) cell++;
while( cell < end ) {
if (s->left.clen[cell] <= smallest_cell_size) {
int i, connections = 0;;
for (i = s->depAdj[s->left.lab[cell]]; i < s->depAdj[s->left.lab[cell]+1]; i++) {
if (!connection_list[s->depEdg[i]]) {
connections++;
connection_list[s->depEdg[i]] = 1;
}
}
if ((s->left.clen[cell] < smallest_cell_size) || (connections > max_connections)) {
smallest_cell_size = s->left.clen[cell];
max_connections = connections;
smallest_cell = cell;
}
for (i = s->depAdj[s->left.lab[cell]]; i < s->depAdj[s->left.lab[cell]+1]; i++)
connection_list[s->depEdg[i]] = 0;
}
cell = s->nextnon[cell];
}
ABC_FREE( connection_list );
return smallest_cell;
}
static int
descend_leftmost(struct saucy *s)
{
int target, min;
/* Keep going until we're discrete */
//print_partition(&s->left, NULL, s->n, s->pNtk, 1);
while (!at_terminal(s)) {
//target = min = s->nextnon[-1];
if (s->nextnon[-1] < Abc_NtkPoNum(s->pNtk))
target = min = select_smallest_max_connected_cell(s, s->nextnon[-1], Abc_NtkPoNum(s->pNtk));
else
target = min = select_smallest_max_connected_cell(s, Abc_NtkPoNum(s->pNtk), s->n);
if (s->fPrintTree)
printf("%s->%s\n", getVertexName(s->pNtk, s->left.lab[min]), getVertexName(s->pNtk, s->left.lab[min]));
s->splitvar[s->lev] = s->left.lab[min];
s->start[s->lev] = target;
s->splitlev[s->lev] = s->nsplits;
if (!descend(s, &s->left, target, min)) return 0;
}
s->splitlev[s->lev] = s->n;
return 1;
}
/*
* If the remaining nonsingletons in this partition match exactly
* those nonsingletons from the leftmost branch of the search tree,
* then there is no point in continuing descent.
*/
static int
zeta_fixed(struct saucy *s)
{
return s->ndiffs == s->nundiffs;
}
static void
select_dynamically(struct saucy *s, int *target, int *lmin, int *rmin)
{
/* Both clens are equal; this clarifies the code a bit */
const int *clen = s->left.clen;
int i, k;
//int cf;
/*
* If there's a pair, use it. pairs[0] should always work,
* but we use a checked loop instead because I'm not 100% sure
* I'm "unpairing" at every point I should be.
*/
for (i = 0; i < s->npairs; ++i) {
k = s->pairs[i];
*target = s->right.cfront[k];
*lmin = s->left.unlab[s->right.lab[s->left.unlab[k]]];
*rmin = s->right.unlab[k];
if (clen[*target]
&& in_cell_range(&s->left, *lmin, *target)
&& in_cell_range(&s->right, *rmin, *target))
return;
}
/* Diffnons is only consistent when there are no baddies */
/*if (s->ndiffnons != -1) {
*target = *lmin = *rmin = s->right.cfront[s->diffnons[0]];
return;
}*/
/* Pick any old target cell and element */
/*for (i = 0; i < s->ndiffs; ++i) {
cf = s->right.cfront[s->diffs[i]];
if (clen[cf]) {
*lmin = *rmin = *target = cf;
return;
}
}*/
for (i = 0; i < s->n; i += (clen[i]+1)) {
if (!clen[i]) continue;
*rmin = *lmin = *target = i;
if (s->right.cfront[s->left.lab[*lmin]] == *target)
*rmin = s->right.unlab[s->left.lab[*lmin]];
return;
}
/* we should never get here */
abort();
}
static void
select_statically(struct saucy *s, int *target, int *lmin, int *rmin)
{
int i;
*target = *rmin = s->left.cfront[s->splitvar[s->lev]];
*lmin = s->left.unlab[s->splitvar[s->lev]];
/* try to map identically! */
for (i = *rmin; i <= (*rmin + s->right.clen[*target]); i++)
if (s->right.lab[*rmin] == s->left.lab[*lmin]) {
*rmin = i;
break;
}
}
static int
descend_left(struct saucy *s)
{
int target, lmin, rmin;
/* Check that we ended at the right spot */
if (s->nsplits != s->splitlev[s->lev]) return 0;
/* Keep going until we're discrete */
while (!at_terminal(s) /*&& !zeta_fixed(s)*/) {
/* We can pick any old target cell and element */
s->select_decomposition(s, &target, &lmin, &rmin);
if (s->fPrintTree) {
//printf("in level %d: %d->%d\n", s->lev, s->left.lab[lmin], s->right.lab[rmin]);
printf("in level %d: %s->%s\n", s->lev, getVertexName(s->pNtk, s->left.lab[lmin]), getVertexName(s->pNtk, s->right.lab[rmin]));
}
/* Check if we need to refine on the left */
s->match = 0;
s->start[s->lev] = target;
s->split = split_left;
if (SELECT_DYNAMICALLY) {
s->refineBySim1 = refineBySim1_left;
s->refineBySim2 = refineBySim2_left;
}
descend(s, &s->left, target, lmin);
s->splitlev[s->lev] = s->nsplits;
s->split = split_other;
if (SELECT_DYNAMICALLY) {
s->refineBySim1 = refineBySim1_other;
s->refineBySim2 = refineBySim2_other;
}
--s->lev;
s->nsplits = s->splitlev[s->lev];
/* Now refine on the right and ensure matching */
s->specmin[s->lev] = s->right.lab[rmin];
if (!descend(s, &s->right, target, rmin)) return 0;
if (s->nsplits != s->splitlev[s->lev]) return 0;
}
return 1;
}
static int
find_representative(int k, int *theta)
{
int rep, tmp;
/* Find the minimum cell representative */
for (rep = k; rep != theta[rep]; rep = theta[rep]);
/* Update all intermediaries */
while (theta[k] != rep) {
tmp = theta[k]; theta[k] = rep; k = tmp;
}
return rep;
}
static void
update_theta(struct saucy *s)
{
int i, k, x, y, tmp;
for (i = 0; i < s->ndiffs; ++i) {
k = s->unsupp[i];
x = find_representative(k, s->theta);
y = find_representative(s->gamma[k], s->theta);
if (x != y) {
if (x > y) {
tmp = x;
x = y;
y = tmp;
}
s->theta[y] = x;
s->thsize[x] += s->thsize[y];
s->thnext[s->thprev[y]] = s->thnext[y];
s->thprev[s->thnext[y]] = s->thprev[y];
s->threp[s->thfront[y]] = s->thnext[y];
}
}
}
static int
theta_prune(struct saucy *s)
{
int start = s->start[s->lev];
int label, rep, irep;
irep = find_representative(s->indmin, s->theta);
while (s->kanctar) {
label = s->anctar[--s->kanctar];
rep = find_representative(label, s->theta);
if (rep == label && rep != irep) {
return s->right.unlab[label] - start;
}
}
return -1;
}
static int
orbit_prune(struct saucy *s)
{
int i, label, fixed, min = -1;
int k = s->start[s->lev];
int size = s->right.clen[k] + 1;
int *cell = s->right.lab + k;
/* The previously fixed value */
fixed = cell[size-1];
/* Look for the next minimum cell representative */
for (i = 0; i < size-1; ++i) {
label = cell[i];
/* Skip things we've already considered */
if (label <= fixed) continue;
/* Skip things that we'll consider later */
if (min != -1 && label > cell[min]) continue;
/* New candidate minimum */
min = i;
}
return min;
}
static void
note_anctar_reps(struct saucy *s)
{
int i, j, k, m, f, rep, tmp;
/*
* Undo the previous level's splits along leftmost so that we
* join the appropriate lists of theta reps.
*/
for (i = s->splitlev[s->anc+1]-1; i >= s->splitlev[s->anc]; --i) {
f = s->splitfrom[i];
j = s->threp[f];
k = s->threp[s->splitwho[i]];
s->thnext[s->thprev[j]] = k;
s->thnext[s->thprev[k]] = j;
tmp = s->thprev[j];
s->thprev[j] = s->thprev[k];
s->thprev[k] = tmp;
for (m = k; m != j; m = s->thnext[m]) {
s->thfront[m] = f;
}
}
/*
* Just copy over the target's reps and sort by cell size, in
* the hopes of trimming some otherwise redundant generators.
*/
s->kanctar = 0;
s->anctar[s->kanctar++] = rep = s->threp[s->start[s->lev]];
for (k = s->thnext[rep]; k != rep; k = s->thnext[k]) {
s->anctar[s->kanctar++] = k;
}
array_indirect_sort(s->anctar, s->thsize, s->kanctar);
}
static void
multiply_index(struct saucy *s, int k)
{
if ((s->stats->grpsize_base *= k) > 1e10) {
s->stats->grpsize_base /= 1e10;
s->stats->grpsize_exp += 10;
}
}
static int
backtrack_leftmost(struct saucy *s)
{
int rep = find_representative(s->indmin, s->theta);
int repsize = s->thsize[rep];
int min = -1;
pick_all_the_pairs(s);
clear_undiffnons(s);
s->ndiffs = s->nundiffs = s->npairs = s->ndiffnons = 0;
if (repsize != s->right.clen[s->start[s->lev]]+1) {
min = theta_prune(s);
}
if (min == -1) {
multiply_index(s, repsize);
}
return min;
}
static int
backtrack_other(struct saucy *s)
{
int cf = s->start[s->lev];
int cb = cf + s->right.clen[cf];
int spec = s->specmin[s->lev];
int min;
/* Avoid using pairs until we get back to leftmost. */
pick_all_the_pairs(s);
clear_undiffnons(s);
s->npairs = s->ndiffnons = -1;
if (s->right.lab[cb] == spec) {
min = find_min(s, cf);
if (min == cb) {
min = orbit_prune(s);
}
else {
min -= cf;
}
}
else {
min = orbit_prune(s);
if (min != -1 && s->right.lab[min + cf] == spec) {
swap_labels(&s->right, min + cf, cb);
min = orbit_prune(s);
}
}
return min;
}
static void
rewind_coloring(struct saucy *s, struct coloring *c, int lev)
{
int i, cf, ff, splits = s->splitlev[lev];
for (i = s->nsplits - 1; i >= splits; --i) {
cf = s->splitfrom[i];
ff = s->splitwho[i];
c->clen[cf] += c->clen[ff] + 1;
fix_fronts(c, cf, ff);
}
}
static void
rewind_simulation_vectors(struct saucy *s, int lev)
{
int i;
for (i = s->randomVectorSplit_sim1[lev]; i < Vec_PtrSize(s->randomVectorArray_sim1); i++)
Vec_IntFree((Vec_Int_t *)Vec_PtrEntry(s->randomVectorArray_sim1, i));
Vec_PtrShrink(s->randomVectorArray_sim1, s->randomVectorSplit_sim1[lev]);
for (i = s->randomVectorSplit_sim2[lev]; i < Vec_PtrSize(s->randomVectorArray_sim2); i++)
Vec_IntFree((Vec_Int_t *)Vec_PtrEntry(s->randomVectorArray_sim2, i));
Vec_PtrShrink(s->randomVectorArray_sim2, s->randomVectorSplit_sim2[lev]);
}
static int
do_backtrack(struct saucy *s)
{
int i, cf, cb;
/* Undo the splits up to this level */
rewind_coloring(s, &s->right, s->lev);
s->nsplits = s->splitlev[s->lev];
/* Rewind diff information */
for (i = s->ndiffs - 1; i >= s->difflev[s->lev]; --i) {
s->diffmark[s->diffs[i]] = 0;
}
s->ndiffs = s->difflev[s->lev];
s->nundiffs = s->undifflev[s->lev];
/* Point to the target cell */
cf = s->start[s->lev];
cb = cf + s->right.clen[cf];
/* Update ancestor with zeta if we've rewound more */
if (s->anc > s->lev) {
s->anc = s->lev;
s->indmin = s->left.lab[cb];
s->match = 1;
note_anctar_reps(s);
}
/* Perform backtracking appropriate to our location */
return s->lev == s->anc
? backtrack_leftmost(s)
: backtrack_other(s);
}
static int
backtrack_loop(struct saucy *s)
{
int min;
/* Backtrack as long as we're exhausting target cells */
for (--s->lev; s->lev; --s->lev) {
min = do_backtrack(s);
if (min != -1) return min + s->start[s->lev];
}
return -1;
}
static int
backtrack(struct saucy *s)
{
int min, old, tmp;
old = s->nsplits;
min = backtrack_loop(s);
tmp = s->nsplits;
s->nsplits = old;
rewind_coloring(s, &s->left, s->lev+1);
s->nsplits = tmp;
if (SELECT_DYNAMICALLY)
rewind_simulation_vectors(s, s->lev+1);
return min;
}
static int
backtrack_bad(struct saucy *s)
{
int min, old, tmp;
old = s->lev;
min = backtrack_loop(s);
if (BACKTRACK_BY_SAT) {
int oldLev = s->lev;
while (!backtrackBysatCounterExamples(s, &s->right)) {
min = backtrack_loop(s);
if (!s->lev) {
if (s->fPrintTree)
printf("Backtrack by SAT from level %d to %d\n", oldLev, 0);
return -1;
}
}
if (s->fPrintTree)
if (s->lev < oldLev)
printf("Backtrack by SAT from level %d to %d\n", oldLev, s->lev);
}
tmp = s->nsplits;
s->nsplits = s->splitlev[old];
rewind_coloring(s, &s->left, s->lev+1);
s->nsplits = tmp;
if (SELECT_DYNAMICALLY)
rewind_simulation_vectors(s, s->lev+1);
return min;
}
void
prepare_permutation_ntk(struct saucy *s)
{
int i;
Abc_Obj_t * pObj, * pObjPerm;
int numouts = Abc_NtkPoNum(s->pNtk);
Nm_ManFree( s->pNtk_permuted->pManName );
s->pNtk_permuted->pManName = Nm_ManCreate( Abc_NtkCiNum(s->pNtk) + Abc_NtkCoNum(s->pNtk) + Abc_NtkBoxNum(s->pNtk) );
for (i = 0; i < s->n; ++i) {
if (i < numouts) {
pObj = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk->vPos, i);
pObjPerm = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk_permuted->vPos, s->gamma[i]);
}
else {
pObj = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk->vPis, i - numouts);
pObjPerm = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk_permuted->vPis, s->gamma[i] - numouts);
}
Abc_ObjAssignName( pObjPerm, Abc_ObjName(pObj), NULL );
}
Abc_NtkOrderObjsByName( s->pNtk_permuted, 1 );
/* print the permutation */
/*for (i = 0; i < s->ndiffs; ++i)
printf(" %d->%d", s->unsupp[i], s->diffs[i]);
printf("\n");
Abc_NtkForEachCo( s->pNtk, pObj, i )
printf (" %d", Abc_ObjId(pObj)-1-Abc_NtkPiNum(s->pNtk));
Abc_NtkForEachCi( s->pNtk, pObj, i )
printf (" %d", Abc_ObjId(pObj)-1+Abc_NtkPoNum(s->pNtk));
printf("\n");
Abc_NtkForEachCo( s->pNtk_permuted, pObj, i )
printf (" %d", Abc_ObjId(pObj)-1-Abc_NtkPiNum(s->pNtk_permuted));
Abc_NtkForEachCi( s->pNtk_permuted, pObj, i )
printf (" %d", Abc_ObjId(pObj)-1+Abc_NtkPoNum(s->pNtk_permuted));
printf("\n");*/
}
static void
prepare_permutation(struct saucy *s)
{
int i, k;
for (i = 0; i < s->ndiffs; ++i) {
k = s->right.unlab[s->diffs[i]];
s->unsupp[i] = s->left.lab[k];
s->gamma[s->left.lab[k]] = s->right.lab[k];
}
prepare_permutation_ntk(s);
}
void
unprepare_permutation_ntk(struct saucy *s)
{
int i;
Abc_Obj_t * pObj, * pObjPerm;
int numouts = Abc_NtkPoNum(s->pNtk);
Nm_ManFree( s->pNtk_permuted->pManName );
s->pNtk_permuted->pManName = Nm_ManCreate( Abc_NtkCiNum(s->pNtk) + Abc_NtkCoNum(s->pNtk) + Abc_NtkBoxNum(s->pNtk) );
for (i = 0; i < s->n; ++i) {
if (i < numouts) {
pObj = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk->vPos, s->gamma[i]);
pObjPerm = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk_permuted->vPos, i);
}
else {
pObj = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk->vPis, s->gamma[i] - numouts);
pObjPerm = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk_permuted->vPis, i - numouts);
}
Abc_ObjAssignName( pObjPerm, Abc_ObjName(pObj), NULL );
}
Abc_NtkOrderObjsByName( s->pNtk_permuted, 1 );
}
static void
unprepare_permutation(struct saucy *s)
{
int i;
unprepare_permutation_ntk(s);
for (i = 0; i < s->ndiffs; ++i) {
s->gamma[s->unsupp[i]] = s->unsupp[i];
}
}
static int
do_search(struct saucy *s)
{
int min;
unprepare_permutation(s);
/* Backtrack to the ancestor with zeta */
if (s->lev > s->anc) s->lev = s->anc + 1;
/* Perform additional backtracking */
min = backtrack(s);
if (s->fBooleanMatching && (s->stats->grpsize_base > 1 || s->stats->grpsize_exp > 0))
return 0;
if (s->fPrintTree && s->lev > 0) {
//printf("in level %d: %d->%d\n", s->lev, s->left.lab[s->splitwho[s->nsplits]], s->right.lab[min]);
printf("in level %d: %s->%s\n", s->lev, getVertexName(s->pNtk, s->left.lab[s->splitwho[s->nsplits]]), getVertexName(s->pNtk, s->right.lab[min]));
}
/* Keep going while there are tree nodes to expand */
while (s->lev) {
/* Descend to a new leaf node */
if (descend(s, &s->right, s->start[s->lev], min)
&& descend_left(s)) {
/* Prepare permutation */
prepare_permutation(s);
/* If we found an automorphism, return it */
if (s->is_automorphism(s)) {
++s->stats->gens;
s->stats->support += s->ndiffs;
update_theta(s);
s->print_automorphism(s->gFile, s->n, s->gamma, s->ndiffs, s->unsupp, s->marks, s->pNtk);
unprepare_permutation(s);
return 1;
}
else {
unprepare_permutation(s);
}
}
/* If we get here, something went wrong; backtrack */
++s->stats->bads;
min = backtrack_bad(s);
if (s->fPrintTree) {
printf("BAD NODE\n");
if (s->lev > 0) {
//printf("in level %d: %d->%d\n", s->lev, s->left.lab[s->splitwho[s->nsplits]], s->right.lab[min]);
printf("in level %d: %s->%s\n", s->lev, getVertexName(s->pNtk, s->left.lab[s->splitwho[s->nsplits]]), getVertexName(s->pNtk, s->right.lab[min]));
}
}
}
/* Normalize group size */
while (s->stats->grpsize_base >= 10.0) {
s->stats->grpsize_base /= 10;
++s->stats->grpsize_exp;
}
return 0;
}
void
saucy_search(
Abc_Ntk_t * pNtk,
struct saucy *s,
int directed,
const int *colors,
struct saucy_stats *stats)
{
int i, j, max = 0;
struct saucy_graph *g;
extern Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk );
/* Save network information */
s->pNtk = pNtk;
s->pNtk_permuted = Abc_NtkDup( pNtk );
/* Builde dependency graph */
g = buildDepGraph(pNtk, s->iDep, s->oDep);
/* Save graph information */
s->n = g->n;
s->depAdj = g->adj;
s->depEdg = g->edg;
/*s->dadj = g->adj + g->n + 1;
s->dedg = g->edg + g->e;*/
/* Save client information */
s->stats = stats;
/* Polymorphism */
if (directed) {
s->is_automorphism = is_directed_automorphism;
s->ref_singleton = ref_singleton_directed;
s->ref_nonsingle = ref_nonsingle_directed;
}
else {
s->is_automorphism = is_undirected_automorphism;
s->ref_singleton = ref_singleton_undirected;
s->ref_nonsingle = ref_nonsingle_undirected;
}
/* Initialize scalars */
s->indmin = 0;
s->lev = s->anc = 1;
s->ndiffs = s->nundiffs = s->ndiffnons = 0;
s->activityInc = 1;
/* The initial orbit partition is discrete */
for (i = 0; i < s->n; ++i) {
s->theta[i] = i;
}
/* The initial permutation is the identity */
for (i = 0; i < s->n; ++i) {
s->gamma[i] = i;
}
/* Initially every cell of theta has one element */
for (i = 0; i < s->n; ++i) {
s->thsize[i] = 1;
}
/* Every theta rep list is singleton */
for (i = 0; i < s->n; ++i) {
s->thprev[i] = s->thnext[i] = i;
}
/* We have no pairs yet */
s->npairs = 0;
for (i = 0; i < s->n; ++i) {
s->unpairs[i] = -1;
}
/* Ensure no stray pointers in undiffnons, which is checked by removed_diffnon() */
for (i = 0; i < s->n; ++i) {
s->undiffnons[i] = -1;
}
/* Initialize stats */
s->stats->grpsize_base = 1.0;
s->stats->grpsize_exp = 0;
s->stats->nodes = 1;
s->stats->bads = s->stats->gens = s->stats->support = 0;
/* Prepare for refinement */
s->nninduce = s->nsinduce = 0;
s->csize = 0;
/* Count cell sizes */
for (i = 0; i < s->n; ++i) {
s->ccount[colors[i]]++;
if (max < colors[i]) max = colors[i];
}
s->nsplits = max + 1;
/* Build cell lengths */
s->left.clen[0] = s->ccount[0] - 1;
for (i = 0; i < max; ++i) {
s->left.clen[s->ccount[i]] = s->ccount[i+1] - 1;
s->ccount[i+1] += s->ccount[i];
}
/* Build the label array */
for (i = 0; i < s->n; ++i) {
set_label(&s->left, --s->ccount[colors[i]], i);
}
/* Clear out ccount */
for (i = 0; i <= max; ++i) {
s->ccount[i] = 0;
}
/* Update refinement stuff based on initial partition */
for (i = 0; i < s->n; i += s->left.clen[i]+1) {
add_induce(s, &s->left, i);
fix_fronts(&s->left, i, i);
}
/* Prepare lists based on cell lengths */
for (i = 0, j = -1; i < s->n; i += s->left.clen[i] + 1) {
if (!s->left.clen[i]) continue;
s->prevnon[i] = j;
s->nextnon[j] = i;
j = i;
}
/* Fix the end */
s->prevnon[s->n] = j;
s->nextnon[j] = s->n;
/* Preprocessing after initial coloring */
s->split = split_init;
s->refineBySim1 = refineBySim1_init;
s->refineBySim2 = refineBySim2_init;
//print_partition(&s->left, NULL, s->n, s->pNtk, 1);
printf("Initial Refine by Dependency graph ... ");
refineByDepGraph(s, &s->left);
//print_partition(&s->left, NULL, s->n, s->pNtk, 1);
printf("done!\n");
printf("Initial Refine by Simulation ... ");
if (REFINE_BY_SIM_1) s->refineBySim1(s, &s->left);
//print_partition(&s->left, NULL, s->n, s->pNtk, 1);
if (REFINE_BY_SIM_2) s->refineBySim2(s, &s->left);
//print_partition(&s->left, NULL, s->n, s->pNtk, 1);
printf("done!\n\t--------------------\n");
/* Descend along the leftmost branch and compute zeta */
s->refineBySim1 = refineBySim1_left;
s->refineBySim2 = refineBySim2_left;
descend_leftmost(s);
s->split = split_other;
s->refineBySim1 = refineBySim1_other;
s->refineBySim2 = refineBySim2_other;
/* Our common ancestor with zeta is the current level */
s->stats->levels = s->anc = s->lev;
/* Copy over this data to our non-leftmost coloring */
memcpy(s->right.lab, s->left.lab, s->n * sizeof(int));
memcpy(s->right.unlab, s->left.unlab, s->n * sizeof(int));
memcpy(s->right.clen, s->left.clen, s->n * sizeof(int));
memcpy(s->right.cfront, s->left.cfront, s->n * sizeof(int));
/* The reps are just the labels at this point */
memcpy(s->threp, s->left.lab, s->n * sizeof(int));
memcpy(s->thfront, s->left.unlab, s->n * sizeof(int));
/* choose cell selection method */
if (SELECT_DYNAMICALLY) s->select_decomposition = select_dynamically;
else s->select_decomposition = select_statically;
/* Keep running till we're out of automorphisms */
while (do_search(s));
}
void
saucy_free(struct saucy *s)
{
int i;
ABC_FREE(s->undiffnons);
ABC_FREE(s->diffnons);
ABC_FREE(s->unpairs);
ABC_FREE(s->pairs);
ABC_FREE(s->thfront);
ABC_FREE(s->threp);
ABC_FREE(s->thnext);
ABC_FREE(s->thprev);
ABC_FREE(s->specmin);
ABC_FREE(s->anctar);
ABC_FREE(s->thsize);
ABC_FREE(s->undifflev);
ABC_FREE(s->difflev);
ABC_FREE(s->diffs);
ABC_FREE(s->diffmark);
ABC_FREE(s->conncnts);
ABC_FREE(s->unsupp);
ABC_FREE(s->splitlev);
ABC_FREE(s->splitfrom);
ABC_FREE(s->splitwho);
ABC_FREE(s->splitvar);
ABC_FREE(s->right.unlab);
ABC_FREE(s->right.lab);
ABC_FREE(s->left.unlab);
ABC_FREE(s->left.lab);
ABC_FREE(s->theta);
ABC_FREE(s->junk);
ABC_FREE(s->gamma);
ABC_FREE(s->start);
ABC_FREE(s->prevnon);
free(s->nextnon-1);
ABC_FREE(s->clist);
ABC_FREE(s->ccount);
ABC_FREE(s->count);
ABC_FREE(s->bucket);
ABC_FREE(s->stuff);
ABC_FREE(s->right.clen);
ABC_FREE(s->right.cfront);
ABC_FREE(s->left.clen);
ABC_FREE(s->left.cfront);
ABC_FREE(s->indmark);
ABC_FREE(s->sinduce);
ABC_FREE(s->ninduce);
ABC_FREE(s->depAdj);
ABC_FREE(s->depEdg);
ABC_FREE(s->marks);
for (i = 0; i < Abc_NtkPiNum(s->pNtk); i++) {
Vec_IntFree( s->iDep[i] );
Vec_IntFree( s->obs[i] );
Vec_PtrFree( s->topOrder[i] );
}
for (i = 0; i < Abc_NtkPoNum(s->pNtk); i++) {
Vec_IntFree( s->oDep[i] );
Vec_IntFree( s->ctrl[i] );
}
for (i = 0; i < Vec_PtrSize(s->randomVectorArray_sim1); i++)
Vec_IntFree((Vec_Int_t *)Vec_PtrEntry(s->randomVectorArray_sim1, i));
for (i = 0; i < Vec_PtrSize(s->randomVectorArray_sim2); i++)
Vec_IntFree((Vec_Int_t *)Vec_PtrEntry(s->randomVectorArray_sim2, i));
Vec_PtrFree( s->randomVectorArray_sim1 );
Vec_PtrFree( s->randomVectorArray_sim2 );
ABC_FREE(s->randomVectorSplit_sim1);
ABC_FREE(s->randomVectorSplit_sim2);
Abc_NtkDelete( s->pNtk_permuted );
for (i = 0; i < Vec_PtrSize(s->satCounterExamples); i++) {
struct sim_result * cex = (struct sim_result *)Vec_PtrEntry(s->satCounterExamples, i);
ABC_FREE( cex->inVec );
ABC_FREE( cex->outVec );
ABC_FREE( cex );
}
Vec_PtrFree(s->satCounterExamples);
ABC_FREE( s->pModel );
ABC_FREE( s->iDep );
ABC_FREE( s->oDep );
ABC_FREE( s->obs );
ABC_FREE( s->ctrl );
ABC_FREE( s->topOrder );
ABC_FREE(s);
}
struct saucy *
saucy_alloc(Abc_Ntk_t * pNtk)
{
int i;
int numouts = Abc_NtkPoNum(pNtk);
int numins = Abc_NtkPiNum(pNtk);
int n = numins + numouts;
struct saucy *s = ABC_ALLOC(struct saucy, 1);
if (s == NULL) return NULL;
s->ninduce = ints(n);
s->sinduce = ints(n);
s->indmark = bits(n);
s->left.cfront = zeros(n);
s->left.clen = ints(n);
s->right.cfront = zeros(n);
s->right.clen = ints(n);
s->stuff = bits(n+1);
s->bucket = ints(n+2);
s->count = ints(n+1);
s->ccount = zeros(n);
s->clist = ints(n);
s->nextnon = ints(n+1) + 1;
s->prevnon = ints(n+1);
s->anctar = ints(n);
s->start = ints(n);
s->gamma = ints(n);
s->junk = ints(n);
s->theta = ints(n);
s->thsize = ints(n);
s->left.lab = ints(n);
s->left.unlab = ints(n);
s->right.lab = ints(n);
s->right.unlab = ints(n);
s->splitvar = ints(n);
s->splitwho = ints(n);
s->splitfrom = ints(n);
s->splitlev = ints(n+1);
s->unsupp = ints(n);
s->conncnts = zeros(n);
s->diffmark = bits(n);
s->diffs = ints(n);
s->difflev = ints(n);
s->undifflev = ints(n);
s->specmin = ints(n);
s->thnext = ints(n);
s->thprev = ints(n);
s->threp = ints(n);
s->thfront = ints(n);
s->pairs = ints(n);
s->unpairs = ints(n);
s->diffnons = ints(n);
s->undiffnons = ints(n);
s->marks = bits(n);
s->iDep = ABC_ALLOC( Vec_Int_t*, numins );
s->oDep = ABC_ALLOC( Vec_Int_t*, numouts );
s->obs = ABC_ALLOC( Vec_Int_t*, numins );
s->ctrl = ABC_ALLOC( Vec_Int_t*, numouts );
for(i = 0; i < numins; i++) {
s->iDep[i] = Vec_IntAlloc( 1 );
s->obs[i] = Vec_IntAlloc( 1 );
}
for(i = 0; i < numouts; i++) {
s->oDep[i] = Vec_IntAlloc( 1 );
s->ctrl[i] = Vec_IntAlloc( 1 );
}
s->randomVectorArray_sim1 = Vec_PtrAlloc( n );
s->randomVectorSplit_sim1 = zeros( n );
s->randomVectorArray_sim2 = Vec_PtrAlloc( n );
s->randomVectorSplit_sim2= zeros( n );
s->satCounterExamples = Vec_PtrAlloc( 1 );
s->pModel = ints( numins );
if (s->ninduce && s->sinduce && s->left.cfront && s->left.clen
&& s->right.cfront && s->right.clen
&& s->stuff && s->bucket && s->count && s->ccount
&& s->clist && s->nextnon-1 && s->prevnon
&& s->start && s->gamma && s->theta && s->left.unlab
&& s->right.lab && s->right.unlab
&& s->left.lab && s->splitvar && s->splitwho && s->junk
&& s->splitfrom && s->splitlev && s->thsize
&& s->unsupp && s->conncnts && s->anctar
&& s->diffmark && s->diffs && s->indmark
&& s->thnext && s->thprev && s->threp && s->thfront
&& s->pairs && s->unpairs && s->diffnons && s->undiffnons
&& s->difflev && s->undifflev && s->specmin)
{
return s;
}
else {
saucy_free(s);
return NULL;
}
}
static void
print_stats(FILE *f, struct saucy_stats stats )
{
fprintf(f, "group size = %fe%d\n",
stats.grpsize_base, stats.grpsize_exp);
fprintf(f, "levels = %d\n", stats.levels);
fprintf(f, "nodes = %d\n", stats.nodes);
fprintf(f, "generators = %d\n", stats.gens);
fprintf(f, "total support = %d\n", stats.support);
fprintf(f, "average support = %.2f\n",(double)(stats.support)/(double)(stats.gens));
fprintf(f, "nodes per generator = %.2f\n",(double)(stats.nodes)/(double)(stats.gens));
fprintf(f, "bad nodes = %d\n", stats.bads);
}
/* From this point up are SAUCY functions*/
/////////////////////////////////////////////////////////////////////////////////////////////////////////
/* From this point down are new functions */
static char *
getVertexName(Abc_Ntk_t *pNtk, int v)
{
Abc_Obj_t * pObj;
int numouts = Abc_NtkPoNum(pNtk);
if (v < numouts)
pObj = (Abc_Obj_t *)Vec_PtrEntry(pNtk->vPos, v);
else
pObj = (Abc_Obj_t *)Vec_PtrEntry(pNtk->vPis, v - numouts);
return Abc_ObjName(pObj);
}
static Vec_Ptr_t **
findTopologicalOrder( Abc_Ntk_t * pNtk )
{
Vec_Ptr_t ** vNodes;
Abc_Obj_t * pObj, * pFanout;
int i, k;
extern void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
/* start the array of nodes */
vNodes = ABC_ALLOC(Vec_Ptr_t *, Abc_NtkPiNum(pNtk));
for(i = 0; i < Abc_NtkPiNum(pNtk); i++)
vNodes[i] = Vec_PtrAlloc(50);
Abc_NtkForEachCi( pNtk, pObj, i )
{
/* set the traversal ID */
Abc_NtkIncrementTravId( pNtk );
Abc_NodeSetTravIdCurrent( pObj );
pObj = Abc_ObjFanout0Ntk(pObj);
Abc_ObjForEachFanout( pObj, pFanout, k )
Abc_NtkDfsReverse_rec( pFanout, vNodes[i] );
}
return vNodes;
}
static void
getDependencies(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** oDep)
{
Vec_Ptr_t * vSuppFun;
int i, j;
vSuppFun = Sim_ComputeFunSupp(pNtk, 0);
for(i = 0; i < Abc_NtkPoNum(pNtk); i++) {
char * seg = (char *)vSuppFun->pArray[i];
for(j = 0; j < Abc_NtkPiNum(pNtk); j+=8) {
if(((*seg) & 0x01) == 0x01)
Vec_IntPushOrder(oDep[i], j);
if(((*seg) & 0x02) == 0x02)
Vec_IntPushOrder(oDep[i], j+1);
if(((*seg) & 0x04) == 0x04)
Vec_IntPushOrder(oDep[i], j+2);
if(((*seg) & 0x08) == 0x08)
Vec_IntPushOrder(oDep[i], j+3);
if(((*seg) & 0x10) == 0x10)
Vec_IntPushOrder(oDep[i], j+4);
if(((*seg) & 0x20) == 0x20)
Vec_IntPushOrder(oDep[i], j+5);
if(((*seg) & 0x40) == 0x40)
Vec_IntPushOrder(oDep[i], j+6);
if(((*seg) & 0x80) == 0x80)
Vec_IntPushOrder(oDep[i], j+7);
seg++;
}
}
for(i = 0; i < Abc_NtkPoNum(pNtk); i++)
for(j = 0; j < Vec_IntSize(oDep[i]); j++)
Vec_IntPush(iDep[Vec_IntEntry(oDep[i], j)], i);
/*for(i = 0; i < Abc_NtkPoNum(pNtk); i++)
{
printf("Output %d: ", i);
for(j = 0; j < Vec_IntSize(oDep[i]); j++)
printf("%d ", Vec_IntEntry(oDep[i], j));
printf("\n");
}
printf("\n");
for(i = 0; i < Abc_NtkPiNum(pNtk); i++)
{
printf("Input %d: ", i);
for(j = 0; j < Vec_IntSize(iDep[i]); j++)
printf("%d ", Vec_IntEntry(iDep[i], j));
printf("\n");
}
printf("\n"); */
}
static void
getDependenciesDummy(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** oDep)
{
int i, j;
/* let's assume that every output is dependent on every input */
for(i = 0; i < Abc_NtkPoNum(pNtk); i++)
for(j = 0; j < Abc_NtkPiNum(pNtk); j++)
Vec_IntPush(oDep[i], j);
for(i = 0; i < Abc_NtkPiNum(pNtk); i++)
for(j = 0; j < Abc_NtkPoNum(pNtk); j++)
Vec_IntPush(iDep[i], j);
}
static struct saucy_graph *
buildDepGraph(Abc_Ntk_t *pNtk, Vec_Int_t ** iDep, Vec_Int_t ** oDep)
{
int i, j, k;
struct saucy_graph *g = NULL;
int n, e, *adj, *edg;
n = Abc_NtkPoNum(pNtk) + Abc_NtkPiNum(pNtk);
for (e = 0, i = 0; i < Abc_NtkPoNum(pNtk); i++)
e += Vec_IntSize(oDep[i]);
g = ABC_ALLOC(struct saucy_graph, 1);
adj = zeros(n+1);
edg = ints(2*e);
g->n = n;
g->e = e;
g->adj = adj;
g->edg = edg;
adj[0] = 0;
for (i = 0; i < n; i++) {
/* first add outputs and then inputs */
if ( i < Abc_NtkPoNum(pNtk)) {
adj[i+1] = adj[i] + Vec_IntSize(oDep[i]);
for (k = 0, j = adj[i]; j < adj[i+1]; j++, k++)
edg[j] = Vec_IntEntry(oDep[i], k) + Abc_NtkPoNum(pNtk);
}
else {
adj[i+1] = adj[i] + Vec_IntSize(iDep[i-Abc_NtkPoNum(pNtk)]);
for (k = 0, j = adj[i]; j < adj[i+1]; j++, k++)
edg[j] = Vec_IntEntry(iDep[i-Abc_NtkPoNum(pNtk)], k);
}
}
/* print graph for testing */
/*for (i = 0; i < n; i++) {
printf("%d: ", i);
for (j = adj[i]; j < adj[i+1]; j++)
printf("%d ", edg[j]);
printf("\n");
}*/
return g;
}
static Vec_Int_t *
assignRandomBitsToCells(Abc_Ntk_t * pNtk, struct coloring *c)
{
Vec_Int_t * randVec = Vec_IntAlloc( 1 );
int i, bit;
for (i = 0; i < Abc_NtkPiNum(pNtk); i += (c->clen[i+Abc_NtkPoNum(pNtk)]+1)) {
bit = (int)(SIM_RANDOM_UNSIGNED % 2);
Vec_IntPush(randVec, bit);
}
return randVec;
}
static int *
generateProperInputVector( Abc_Ntk_t * pNtk, struct coloring *c, Vec_Int_t * randomVector )
{
int * vPiValues;
int i, j, k, bit, input;
int numouts = Abc_NtkPoNum(pNtk);
int numins = Abc_NtkPiNum(pNtk);
int n = numouts + numins;
vPiValues = ABC_ALLOC( int, numins);
for (i = numouts, k = 0; i < n; i += (c->clen[i]+1), k++) {
if (k == Vec_IntSize(randomVector)) break;
bit = Vec_IntEntry(randomVector, k);
for (j = i; j <= (i + c->clen[i]); j++) {
input = c->lab[j] - numouts;
vPiValues[input] = bit;
}
}
//if (k != Vec_IntSize(randomVector)) {
if (i < n) {
ABC_FREE( vPiValues );
return NULL;
}
return vPiValues;
}
static int
ifInputVectorsAreConsistent( struct saucy * s, int * leftVec, int * rightVec )
{
/* This function assumes that left and right partitions are isomorphic */
int i, j;
int lab;
int left_bit, right_bit;
int numouts = Abc_NtkPoNum(s->pNtk);
int n = numouts + Abc_NtkPiNum(s->pNtk);
for (i = numouts; i < n; i += (s->right.clen[i]+1)) {
lab = s->left.lab[i] - numouts;
left_bit = leftVec[lab];
for (j = i+1; j <= (i + s->right.clen[i]); j++) {
lab = s->left.lab[j] - numouts;
if (left_bit != leftVec[lab]) return -1;
}
lab = s->right.lab[i] - numouts;
right_bit = rightVec[lab];
for (j = i+1; j <= (i + s->right.clen[i]); j++) {
lab = s->right.lab[j] - numouts;
if (right_bit != rightVec[lab]) return 0;
}
if (left_bit != right_bit)
return 0;
}
return 1;
}
static int
ifOutputVectorsAreConsistent( struct saucy * s, int * leftVec, int * rightVec )
{
/* This function assumes that left and right partitions are isomorphic */
int i, j;
int count1, count2;
for (i = 0; i < Abc_NtkPoNum(s->pNtk); i += (s->right.clen[i]+1)) {
count1 = count2 = 0;
for (j = i; j <= (i + s->right.clen[i]); j++) {
if (leftVec[s->left.lab[j]]) count1++;
if (rightVec[s->right.lab[j]]) count2++;
}
if (count1 != count2) return 0;
}
return 1;
}
static struct saucy_graph *
buildSim1Graph( Abc_Ntk_t * pNtk, struct coloring *c, Vec_Int_t * randVec, Vec_Int_t ** iDep, Vec_Int_t ** oDep )
{
int i, j, k;
struct saucy_graph *g;
int n, e, *adj, *edg;
int * vPiValues, * output;
int numOneOutputs = 0;
int numouts = Abc_NtkPoNum(pNtk);
int numins = Abc_NtkPiNum(pNtk);
vPiValues = generateProperInputVector(pNtk, c, randVec);
if (vPiValues == NULL)
return NULL;
output = Abc_NtkVerifySimulatePattern(pNtk, vPiValues);
for (i = 0; i < numouts; i++) {
if (output[i])
numOneOutputs++;
}
g = ABC_ALLOC(struct saucy_graph, 1);
n = numouts + numins;
e = numins * numOneOutputs;
adj = ints(n+1);
edg = ints(2*e);
g->n = n;
g->e = e;
g->adj = adj;
g->edg = edg;
adj[0] = 0;
for (i = 0; i < numouts; i++) {
if (output[i]) {
adj[i+1] = adj[i] + Vec_IntSize(oDep[i]);
for (j = adj[i], k = 0; j < adj[i+1]; j++, k++)
edg[j] = Vec_IntEntry(oDep[i], k) + numouts;
} else {
adj[i+1] = adj[i];
}
}
for (i = 0; i < numins; i++) {
adj[i+numouts+1] = adj[i+numouts];
for (k = 0, j = adj[i+numouts]; k < Vec_IntSize(iDep[i]); k++) {
if (output[Vec_IntEntry(iDep[i], k)]) {
edg[j++] = Vec_IntEntry(iDep[i], k);
adj[i+numouts+1]++;
}
}
}
/* print graph */
/*for (i = 0; i < n; i++) {
printf("%d: ", i);
for (j = adj[i]; j < adj[i+1]; j++)
printf("%d ", edg[j]);
printf("\n");
}*/
ABC_FREE( vPiValues );
ABC_FREE( output );
return g;
}
static struct saucy_graph *
buildSim2Graph( Abc_Ntk_t * pNtk, struct coloring *c, Vec_Int_t * randVec, Vec_Int_t ** iDep, Vec_Int_t ** oDep, Vec_Ptr_t ** topOrder, Vec_Int_t ** obs, Vec_Int_t ** ctrl )
{
int i, j, k;
struct saucy_graph *g = NULL;
int n, e = 0, *adj, *edg;
int * vPiValues;
int * output, * output2;
int numouts = Abc_NtkPoNum(pNtk);
int numins = Abc_NtkPiNum(pNtk);
extern int * Abc_NtkSimulateOneNode( Abc_Ntk_t * , int * , int , Vec_Ptr_t ** );
vPiValues = generateProperInputVector(pNtk, c, randVec);
if (vPiValues == NULL)
return NULL;
output = Abc_NtkVerifySimulatePattern( pNtk, vPiValues );
for (i = 0; i < numins; i++) {
if (!c->clen[c->cfront[i+numouts]]) continue;
if (vPiValues[i] == 0) vPiValues[i] = 1;
else vPiValues[i] = 0;
output2 = Abc_NtkSimulateOneNode( pNtk, vPiValues, i, topOrder );
for (j = 0; j < Vec_IntSize(iDep[i]); j++) {
if (output[Vec_IntEntry(iDep[i], j)] != output2[Vec_IntEntry(iDep[i], j)]) {
Vec_IntPush(obs[i], Vec_IntEntry(iDep[i], j));
Vec_IntPush(ctrl[Vec_IntEntry(iDep[i], j)], i);
e++;
}
}
if (vPiValues[i] == 0) vPiValues[i] = 1;
else vPiValues[i] = 0;
ABC_FREE( output2 );
}
/* build the graph */
g = ABC_ALLOC(struct saucy_graph, 1);
n = numouts + numins;
adj = ints(n+1);
edg = ints(2*e);
g->n = n;
g->e = e;
g->adj = adj;
g->edg = edg;
adj[0] = 0;
for (i = 0; i < numouts; i++) {
adj[i+1] = adj[i] + Vec_IntSize(ctrl[i]);
for (k = 0, j = adj[i]; j < adj[i+1]; j++, k++)
edg[j] = Vec_IntEntry(ctrl[i], k) + numouts;
}
for (i = 0; i < numins; i++) {
adj[i+numouts+1] = adj[i+numouts] + Vec_IntSize(obs[i]);
for (k = 0, j = adj[i+numouts]; j < adj[i+numouts+1]; j++, k++)
edg[j] = Vec_IntEntry(obs[i], k);
}
/* print graph */
/*for (i = 0; i < n; i++) {
printf("%d: ", i);
for (j = adj[i]; j < adj[i+1]; j++)
printf("%d ", edg[j]);
printf("\n");
}*/
ABC_FREE( output );
ABC_FREE( vPiValues );
for (j = 0; j < numins; j++)
Vec_IntClear(obs[j]);
for (j = 0; j < numouts; j++)
Vec_IntClear(ctrl[j]);
return g;
}
static void
bumpActivity( struct saucy * s, struct sim_result * cex )
{
int i;
struct sim_result * cex2;
if ( (cex->activity += s->activityInc) > 1e20 ) {
/* Rescale: */
for (i = 0; i < Vec_PtrSize(s->satCounterExamples); i++) {
cex2 = (struct sim_result *)Vec_PtrEntry(s->satCounterExamples, i);
cex2->activity *= 1e-20;
}
s->activityInc *= 1e-20;
}
}
static void
reduceDB( struct saucy * s )
{
int i, j;
double extra_lim = s->activityInc / Vec_PtrSize(s->satCounterExamples); /* Remove any clause below this activity */
struct sim_result * cex;
while (Vec_PtrSize(s->satCounterExamples) > (0.7 * MAX_LEARNTS)) {
for (i = j = 0; i < Vec_PtrSize(s->satCounterExamples); i++) {
cex = (struct sim_result *)Vec_PtrEntry(s->satCounterExamples, i);
if (cex->activity < extra_lim) {
ABC_FREE(cex->inVec);
ABC_FREE(cex->outVec);
ABC_FREE(cex);
}
else if (j < i) {
Vec_PtrWriteEntry(s->satCounterExamples, j, cex);
j++;
}
}
//printf("Database size reduced from %d to %d\n", Vec_PtrSize(s->satCounterExamples), j);
Vec_PtrShrink(s->satCounterExamples, j);
extra_lim *= 2;
}
assert(Vec_PtrSize(s->satCounterExamples) <= (0.7 * MAX_LEARNTS));
}
static struct sim_result *
analyzeConflict( Abc_Ntk_t * pNtk, int * pModel, int fVerbose )
{
Abc_Obj_t * pNode;
int i, count = 0;
int * pValues;
struct sim_result * cex;
int numouts = Abc_NtkPoNum(pNtk);
int numins = Abc_NtkPiNum(pNtk);
cex = ABC_ALLOC(struct sim_result, 1);
cex->inVec = ints( numins );
cex->outVec = ints( numouts );
/* get the CO values under this model */
pValues = Abc_NtkVerifySimulatePattern( pNtk, pModel );
Abc_NtkForEachCi( pNtk, pNode, i )
cex->inVec[Abc_ObjId(pNode)-1] = pModel[i];
Abc_NtkForEachCo( pNtk, pNode, i ) {
cex->outVec[Abc_ObjId(pNode)-numins-1] = pValues[i];
if (pValues[i]) count++;
}
cex->outVecOnes = count;
cex->activity = 0;
if (fVerbose) {
Abc_NtkForEachCi( pNtk, pNode, i )
printf(" %s=%d", Abc_ObjName(pNode), pModel[i]);
printf("\n");
}
ABC_FREE( pValues );
return cex;
}
static int
Abc_NtkCecSat_saucy( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel )
{
extern Abc_Ntk_t * Abc_NtkMulti( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
Abc_Ntk_t * pMiter;
Abc_Ntk_t * pCnf;
int RetValue;
int nConfLimit;
int nInsLimit;
int i;
nConfLimit = 10000;
nInsLimit = 0;
/* get the miter of the two networks */
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0, 0, 0 );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );
exit(1);
}
RetValue = Abc_NtkMiterIsConstant( pMiter );
if ( RetValue == 0 )
{
//printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
/* report the error */
pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
for (i = 0; i < Abc_NtkPiNum(pNtk1); i++)
pModel[i] = pMiter->pModel[i];
ABC_FREE( pMiter->pModel );
Abc_NtkDelete( pMiter );
return 0;
}
if ( RetValue == 1 )
{
Abc_NtkDelete( pMiter );
//printf( "Networks are equivalent after structural hashing.\n" );
return 1;
}
/* convert the miter into a CNF */
pCnf = Abc_NtkMulti( pMiter, 0, 100, 1, 0, 0, 0 );
Abc_NtkDelete( pMiter );
if ( pCnf == NULL )
{
printf( "Renoding for CNF has failed.\n" );
exit(1);
}
/* solve the CNF using the SAT solver */
RetValue = Abc_NtkMiterSat( pCnf, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, 0, NULL, NULL );
if ( RetValue == -1 ) {
printf( "Networks are undecided (SAT solver timed out).\n" );
exit(1);
}
/*else if ( RetValue == 0 )
printf( "Networks are NOT EQUIVALENT after SAT.\n" );
else
printf( "Networks are equivalent after SAT.\n" );*/
if ( pCnf->pModel ) {
for (i = 0; i < Abc_NtkPiNum(pNtk1); i++)
pModel[i] = pCnf->pModel[i];
}
ABC_FREE( pCnf->pModel );
Abc_NtkDelete( pCnf );
return RetValue;
}
void saucyGateWay( Abc_Ntk_t * pNtkOrig, Abc_Obj_t * pNodePo, FILE * gFile, int fBooleanMatching,
int fLookForSwaps, int fFixOutputs, int fFixInputs, int fQuiet, int fPrintTree )
{
Abc_Ntk_t * pNtk;
struct saucy *s;
struct saucy_stats stats;
int *colors;
int i, clk = clock();
if (pNodePo == NULL)
pNtk = Abc_NtkDup( pNtkOrig );
else
pNtk = Abc_NtkCreateCone( pNtkOrig, Abc_ObjFanin0(pNodePo), Abc_ObjName(pNodePo), 0 );
if (Abc_NtkPiNum(pNtk) == 0) {
Abc_Print( 0, "This output is not dependent on any input\n" );
Abc_NtkDelete( pNtk );
return;
}
s = saucy_alloc( pNtk );
/******* Getting Dependencies *******/
printf("Build functional dependency graph (dependency stats are below) ... ");
getDependencies( pNtk, s->iDep, s->oDep );
printf("\t--------------------\n");
/************************************/
/* Finding toplogical orde */
s->topOrder = findTopologicalOrder( pNtk );
/* Setting graph colors: outputs = 0 and inputs = 1 */
colors = ints(Abc_NtkPoNum(pNtk) + Abc_NtkPiNum(pNtk));
if (fFixOutputs) {
for (i = 0; i < Abc_NtkPoNum(pNtk); i++)
colors[i] = i;
} else {
for (i = 0; i < Abc_NtkPoNum(pNtk); i++)
colors[i] = 0;
}
if (fFixInputs) {
int c = (fFixOutputs) ? Abc_NtkPoNum(pNtk) : 1;
for (i = 0; i < Abc_NtkPiNum(pNtk); i++)
colors[i+Abc_NtkPoNum(pNtk)] = c+i;
} else {
int c = (fFixOutputs) ? Abc_NtkPoNum(pNtk) : 1;
for (i = 0; i < Abc_NtkPiNum(pNtk); i++)
colors[i+Abc_NtkPoNum(pNtk)] = c;
}
/* Are we looking for Boolean matching? */
s->fBooleanMatching = fBooleanMatching;
if (fBooleanMatching) {
NUM_SIM1_ITERATION = 50;
NUM_SIM2_ITERATION = 50;
} else {
NUM_SIM1_ITERATION = 200;
NUM_SIM2_ITERATION = 200;
}
/* Set the print automorphism routine */
if (!fQuiet)
s->print_automorphism = print_automorphism_ntk;
else
s->print_automorphism = print_automorphism_quiet;
/* Set the output file for generators */
if (gFile == NULL)
s->gFile = stdout;
else
s->gFile = gFile;
/* Set print tree option */
s->fPrintTree = fPrintTree;
/* Set input permutations option */
s->fLookForSwaps = fLookForSwaps;
saucy_search(pNtk, s, 0, colors, &stats);
print_stats(stdout, stats);
if (fBooleanMatching) {
if (stats.grpsize_base > 1 || stats.grpsize_exp > 0)
printf("*** Networks are equivalent ***\n");
else
printf("*** Networks are NOT equivalent ***\n");
}
saucy_free(s);
Abc_NtkDelete(pNtk);
if (1) {
FILE * hadi = fopen("hadi.txt", "a");
fprintf(hadi, "group size = %fe%d\n",
stats.grpsize_base, stats.grpsize_exp);
fclose(hadi);
}
ABC_PRT( "Runtime", clock() - clk );
}ABC_NAMESPACE_IMPL_END
Reference in New Issue View Git Blame Copy Permalink