/**CFile*********************************************************************** FileName [SatCountAlgo.c] PackageName [rob] Synopsis [Functions for Sat count Algo. ] Author [Souheib baarir] Copyright [Copyright (c) 2008-2009 The Regents of the Univ. of Paris VI. All rights reserved. Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software. IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. THE UNIVERSITY OF PARIS VI SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.] *****************************************************************************/ #include "SatCountAlgo.h" #include #include #include #include #include #include int nVar=0, nCl=0; const int K=5; Formula_t createFormula(mdd_manager * mgr){ Formula_t formul = ALLOC(Formula,1); formul->F=lsCreate(); formul->V=mdd_zero(mgr); formul->R=mdd_zero(mgr); formul->mgr=mgr; return formul; } void free_formula(Formula_t F){ (void)lsDestroy(F->F,mdd_free); mdd_free(F->V); mdd_free(F->R); free(F); } static mdd_t* mdd_restrict(mdd_manager* mgr, mdd_t* l,mdd_t* d){ DdNode * tmp=bdd_bdd_restrict(mgr, l->node,d->node); if (tmp== DD_ONE((DdManager *)mgr) ) { return mdd_one(mgr); } if (tmp==Cudd_Not(DD_ONE((DdManager *)mgr))) { return mdd_zero(mgr); } cuddRef(tmp); return bdd_construct_bdd_t(mgr,tmp); } mdd_t* ComposeCubes(mdd_manager* mgr, mdd_t* vars1, mdd_t* vars2){ bdd_node* v[2]; v[0]= vars1->node; v[1]= vars2->node; DdNode * b = bdd_bdd_vector_support(mgr,v,2); cuddRef(b); return bdd_construct_bdd_t(mgr,b); } mdd_t* Get_support(mdd_manager* mgr,mdd_t* l){ DdNode * v = bdd_bdd_support(mgr, l->node); cuddRef(v); return bdd_construct_bdd_t(mgr, v); } int Common_support(mdd_manager* mgr, mdd_t* f, mdd_t* c){ int v=1; mdd_t* fs= Get_support(mgr,f); mdd_t* cs= Get_support(mgr,c); mdd_t* k = bdd_smooth_with_cube(fs,cs); assert(k!=NULL); if (mdd_equal(k,fs)) v=0; mdd_free(k); mdd_free(fs); mdd_free(cs); return v; } Formula_t clone_formula(Formula_t form){ mdd_manager* mgr = form->mgr; lsGen gen =lsStart(form->F); lsGeneric data; lsHandle itemHandle; int* vars=NULL; int* vs=NULL; int j=0,i=0; int size=((DdManager *)mgr)->size; mdd_manager* nmgr=bdd_start(size); Formula_t f=NULL; if(nmgr){ vars=Cudd_SupportIndex((DdManager *) mgr, form->V->node); for (i=0;i< size;i++) if(vars[i]){ vars[i]=j; j++; } mdd_t* zero=mdd_zero(mgr); mdd_t* V=mdd_one(nmgr); f=createFormula(nmgr); while(lsNext(gen, &data, &itemHandle) == LS_OK){ mdd_t* l =(mdd_t*)data; vs =Cudd_SupportIndex((DdManager *) mgr, l->node); mdd_t* clause=mdd_one(nmgr); for(i=0;iF,clause,LS_NH); free(vs); } lsFinish(gen); free(vars); mdd_free(f->V); f->V=V; if(!mdd_equal(form->R,zero)){ vars=Cudd_SupportIndex((DdManager *) mgr, form->R->node); for (i=0;i< size;i++) if(vars[i]){ vars[i]=j; j++; } mdd_free(f->R); mdd_t* R=mdd_one(nmgr); vs=Cudd_SupportIndex((DdManager *) mgr, form->R->node); for(i=0;iR=R; } mdd_free(zero); } return f; } Formula_t _psi(Formula_t For,mdd_t* d){ mdd_manager* mgr = For->mgr; lsGen gen =lsStart(For->F); lsGeneric data; lsHandle itemHandle; mdd_t* nd =bdd_not(d); mdd_t* one =mdd_one(mgr); mdd_t* zero=mdd_zero(mgr); mdd_t* v =mdd_zero(mgr); Formula_t F2=createFormula(mgr); while(lsNext(gen, &data, &itemHandle) == LS_OK){ mdd_t* l=(mdd_t*)data; if(Common_support(mgr,l,d)){ mdd_t* res=mdd_restrict(mgr,l,d); if(mdd_equal(res,zero)){ mdd_t* newl = mdd_restrict(mgr,l,nd); (void)lsNewEnd(F2->F,newl,LS_NH); mdd_t* tmp = v; v=ComposeCubes(mgr,v,newl); mdd_free(tmp); if(mdd_equal(newl,one)){ lsFinish(gen); mdd_free(res); mdd_free(one); mdd_free(zero); mdd_free(nd); return F2; } } mdd_free(res); } else{ mdd_t* ll= mdd_dup(l); (void)lsNewEnd(F2->F,ll,LS_NH); mdd_t* tmp=v; v=ComposeCubes(mgr,v,l); mdd_free(tmp); } } lsFinish(gen); // New set of elemanated variables mdd_t* v1=ComposeCubes(mgr,v,d); mdd_t* newelem=bdd_smooth_with_cube(For->V,v1); mdd_t* R; mdd_t* V; R=mdd_dup(For->R); mdd_free(F2->R); mdd_free(F2->V); if (!mdd_equal(newelem,one)){ F2->R=ComposeCubes(mgr,R,newelem); mdd_free(R); } else{ F2->R=R; } // New set of variables F2->V=v; mdd_free(one); mdd_free(zero); mdd_free(v1); mdd_free(nd); mdd_free(newelem); return F2; } mdd_t* get_var_sup (Formula_t Form){ lsGeneric data; lsHandle itemHandle; mdd_manager* mgr =Form->mgr; lsGen gen=lsStart(Form->F); mdd_t* Current; mdd_t* Before=mdd_zero(mgr); (void)lsFirstItem(Form->F,&data,&itemHandle); Current=Get_support(mgr,(mdd_t*)data); assert(Current!=NULL); do{ mdd_free(Before); Before = mdd_dup(Current); while(lsNext(gen, &data, &itemHandle) == LS_OK){ mdd_t* l = mdd_dup((mdd_t*)data); mdd_t* sup =Get_support (mgr,l); if(Common_support(mgr,Current, l)){ mdd_t* tmp= Current; Current=ComposeCubes(mgr,Current,sup); mdd_free(tmp); } mdd_free(l); mdd_free(sup); } lsFinish(gen); gen=lsStart(Form->F); } while(!mdd_equal(Before,Current)); lsFinish(gen); mdd_free(Before); return Current; } int disjoint_formula(Formula_t Form, Formula_t* F1, Formula_t* F2){ lsGeneric data; lsHandle itemHandle; lsGen gen=lsStart(Form->F); mdd_manager* mgr =Form->mgr; mdd_t* V1; mdd_t* V2; V2=get_var_sup (Form); if (!mdd_equal(V2,Form->V)){ (*F1) = createFormula(mgr); (*F2) = createFormula(mgr); mdd_free((*F2)->V); mdd_free((*F1)->V); (*F2)->V = V2; (*F1)->V = bdd_smooth_with_cube(Form->V,V2); assert((*F1)->V!=NULL); while(lsNext(gen, &data, &itemHandle) == LS_OK){ mdd_t* l = mdd_dup((mdd_t*)data); if(Common_support(mgr,V2, l)){ (void)lsNewEnd((*F2)->F,mdd_dup(data),LS_NH); } else{ (void)lsNewEnd((*F1)->F,mdd_dup(data),LS_NH); } mdd_free(l); } lsFinish(gen); return 1; } lsFinish(gen); mdd_free(V2); return 0; } int _d(Formula_t Form, mdd_t* x){ int cpt=0; lsGeneric data; lsHandle itemHandle; lsGen gen=lsStart(Form->F); mdd_manager* mgr =Form->mgr; while(lsNext(gen, &data, &itemHandle) == LS_OK){ mdd_t* l = mdd_dup((mdd_t*)data); if(Common_support(mgr,l,x)) cpt ++; mdd_free(l); } lsFinish(gen); return cpt; } mdd_t* _k_clause(Formula_t Form, int k){ int cpt=0; lsGeneric data; lsHandle itemHandle; lsGen gen=lsStart(Form->F); mdd_manager* mgr =Form->mgr; while(lsNext(gen, &data, &itemHandle) == LS_OK){ mdd_t* l = (mdd_t*)data; if (Cudd_SupportSize((DdManager *) mgr, l->node)==k){ lsFinish(gen); return mdd_dup(l); } } lsFinish(gen); return mdd_zero(mgr); } int greater_d(Formula_t Form,int k){ int* vars=NULL; mdd_manager* mgr =Form->mgr; int nbvar=((DdManager *)mgr)->size; int d=0,i,g,s; mdd_t* zero=mdd_zero(mgr); for(i=0;i d){ d = s; g = i; } mdd_free(v); mdd_free(c); } mdd_free(zero); return g; } mdd_t* get_w(Formula_t Form, mdd_t* clause, int * vars, int k){ int i,j,nbvar=((DdManager *)(Form->mgr))->size; mdd_manager* mgr =Form->mgr; for(i=0;imgr; int i,nbvar=((DdManager *)mgr)->size; mdd_t* w; mdd_t* zero=mdd_zero(mgr); vars=Cudd_SupportIndex((DdManager *) mgr, clause->node); if (!mdd_equal((w=get_w(Form, clause, vars, 1)), zero)){ free(vars); mdd_free(zero); return w; } mdd_free(w); if (!mdd_equal((w=get_w(Form, clause, vars, 2)), zero)){ free(vars); mdd_free(zero); return w; } mdd_free(w); mdd_free(zero); free(vars); int ind = greater_d(Form,2); return bdd_var_with_index(mgr,ind); } mdd_t* get_neighbour(Formula_t Form, mdd_t* x,int * deg){ mdd_manager* mgr = Form->mgr; lsGen gen=lsStart(Form->F); lsGeneric data; lsHandle itemHandle; mdd_t* res = mdd_zero(mgr); while(lsNext(gen, &data, &itemHandle) == LS_OK){ mdd_t* l = (mdd_t*)data; if(Common_support(mgr,l, x)){ mdd_t* tmp=res; mdd_t* cmp=bdd_smooth_with_cube(l,x); res =ComposeCubes(mgr,res,cmp); mdd_free(tmp); mdd_free(cmp); } } lsFinish(gen); (*deg)= Cudd_SupportSize((DdManager *) mgr,res->node); return res; } mdd_t* get_max_degree_(Formula_t Form, mdd_t* clause){ int *vars=NULL; int i,max=0,deg; mdd_manager* mgr =Form->mgr; int nbvar=((DdManager *)mgr)->size; mdd_t* res=mdd_zero(mgr); vars=Cudd_SupportIndex((DdManager *)mgr,clause->node); for(i=0;i max) { max=deg; mdd_free(res); res=mdd_dup(v); } mdd_free(v); mdd_free(nhb); } } free(vars); return res; } mdd_t* get_max_nhb_degre(Formula_t Form, int * vars, int k){ mdd_manager* mgr =Form->mgr; int i,deg,nbvar=((DdManager *)mgr)->size; mdd_t* r; for(i=0;imgr; int i,deg,max=0,nbvar=((DdManager *)mgr)->size; mdd_t* w=mdd_zero(mgr); mdd_t* zero=mdd_zero(mgr); vars=Cudd_SupportIndex((DdManager *) mgr, Form->V->node); if(!mdd_equal((w=get_max_nhb_degre(Form, vars, 1)), zero)){ free(vars); mdd_free(zero); return w; } if(!mdd_equal((w=get_max_nhb_degre(Form, vars, 2)), zero)){ free(vars); mdd_free(zero); return w; } for(i=0;i max ){ max=deg; mdd_free(w); w=mdd_dup(v); } mdd_free(t); mdd_free(v); } } mdd_free(zero); free(vars); return w; } int is_empty_formula(Formula_t Form){ mdd_manager* mgr = Form->mgr; lsGen gen=lsStart(Form->F); lsGeneric data; lsHandle itemHandle; mdd_t* one = mdd_one(mgr); while(lsNext(gen, &data, &itemHandle) == LS_OK){ mdd_t* l = (mdd_t*)data; if(mdd_equal(l,one)){ lsFinish(gen); return TRUE; } } mdd_free(one); lsFinish(gen); return FALSE; } int D(Formula_t Form){ mdd_manager* mgr = Form->mgr; Formula_t F1,F2; mdd_t* R; mdd_t* x; mdd_t* w; int card_R,d_f1,d_f2; mdd_t* zero = mdd_zero(mgr); unsigned long lswap; if (is_empty_formula(Form)) { mdd_free(zero); return 0; } if (lsLength(Form->F)==0) { int r =Cudd_SupportSize((DdManager *)mgr, (Form->R)->node); card_R =(int)pow(2,r); mdd_free(zero); return card_R; } if(disjoint_formula(Form,&F1,&F2)){ d_f1=0;d_f2=0; int r =Cudd_SupportSize((DdManager *)mgr, (Form->R)->node); card_R =(int)pow(2,r); // if ((rand()%K) == 0){ if (K <= 12){ int fd1[2]; int fd2[2]; if (pipe(fd1) != 0) { fprintf(stderr,"Problemes dans l'ouverture de Pipe \n"); exit(1); } if (pipe(fd2) != 0) { fprintf(stderr,"Problemes dans l'ouverture de Pipe \n"); exit(1); } int pid1,pid2; if((pid1=fork())==0){ char buf[30]="\0"; d_f1=D(F1); close(fd1[0]); sprintf(buf,"%d",d_f1); write(fd1[1], buf, strlen(buf)); close(fd1[1]); //free_formula(F1); exit(EXIT_SUCCESS); } if((pid2=fork())==0){ char buf[30]="\0"; d_f2=D(F2); close(fd2[0]); sprintf(buf,"%d",d_f2); write(fd2[1],buf,strlen(buf)); close(fd2[1]); //free_formula(F2); exit(EXIT_SUCCESS); } int i,s; if(pid1 > 0){ free_formula(F1); char buf[30]="\0"; i=waitpid(pid1, &s, WUNTRACED); close(fd1[1]); read(fd1[0],buf,30); d_f1=atoi(buf); close(fd1[0]); }else{ d_f1=D(F1); free_formula(F1); } if(pid2 > 0){ free_formula(F2); char buf[30]="\0"; i=waitpid(pid2, &s, WUNTRACED); close(fd2[1]); read(fd2[0],buf,30); d_f2=atoi(buf); close(fd2[0]); }else{ d_f2=D(F2); free_formula(F2); } } else{ d_f1=D(F1);free_formula(F1); d_f2=D(F2);free_formula(F2); } assert( card_R*d_f1*d_f2 >= 0); return card_R*d_f1*d_f2; } if(!mdd_equal((x=_k_clause(Form,1)),zero)){ F1=Form; int k; do{ F2 = F1; F1 =_psi(F2,x); mdd_free(x); k=mdd_equal((x=_k_clause(F1,1)),zero); if( F2 != Form) free_formula(F2); } while(!k && !is_empty_formula(F1)); d_f1 =D(F1); free_formula(F1); mdd_free(x); mdd_free(zero); return d_f1; } mdd_free(x); if(!mdd_equal((x=_k_clause(Form,2)),zero)){ w=pick_2_clause_w(Form,x); } else{ w=pick_clause_w(Form); } mdd_t* nw=mdd_not(w); // if ((rand()%K) == 0){ if (K <= 12){ int fd1[2]; int fd2[2]; if (pipe(fd1) != 0) { fprintf(stderr,"Problemes dans l'ouverture de Pipe \n"); exit(1); } if (pipe(fd2) != 0) { fprintf(stderr,"Problemes dans l'ouverture de Pipe \n"); exit(1); } int pid1,pid2; if((pid1=fork())==0){ char buf[30]="\0"; F1=_psi(Form,w); d_f1=D(F1); close(fd1[0]); sprintf(buf,"%d",d_f1); write(fd1[1],buf,strlen(buf)); close(fd1[1]); exit(EXIT_SUCCESS); } if((pid2=fork())==0){ char buf[30]="\0"; F2=_psi(Form,nw); d_f2=D(F2); close(fd2[0]); sprintf(buf,"%d",d_f2); write(fd2[1],buf,strlen(buf)); close(fd2[1]); exit(EXIT_SUCCESS); } int i,s; if(pid1>0){ char buf[30]="\0"; i=waitpid(pid1,&s,WUNTRACED); close(fd1[1]); read(fd1[0],buf,30); d_f1=atoi(buf); close(fd1[0]); }else{ F1=_psi(Form,w); d_f1=D(F1); free_formula(F1); } if(pid2>0){ char buf[30]="\0"; i=waitpid(pid2,&s, WUNTRACED); close(fd2[1]); read(fd2[0],buf, 30); d_f2=atoi(buf); close(fd2[0]); }else{ F2=_psi(Form,nw); d_f2=D(F2); free_formula(F2); } } else{ F1=_psi(Form,w); F2=_psi(Form,nw); d_f1=D(F1);free_formula(F1); d_f2=D(F2);free_formula(F2); } mdd_free(x); mdd_free(w); mdd_free(nw); mdd_free(zero); assert(d_f1+d_f2 >= 0); return (d_f1+d_f2); } int exit_(Formula_t Form, mdd_t* n){ lsGen gen=lsStart(Form->F); lsGeneric data; lsHandle itemHandle; while(lsNext(gen, &data, &itemHandle) == LS_OK){ if(mdd_equal(data,n)){ lsFinish(gen); return TRUE; } } lsFinish(gen); return FALSE; } /* int var_to_add(int size){ int k,r,nb=0; k=size; do{ k=(int)k/2; r=size % 2; nb +=k;k +=r; }while(k > 3); return nb; } */ mdd_t* convert_dnf_cnf(Formula_t Form, mdd_t* v1,mdd_t* v2, mdd_t* res){ mdd_manager* mgr = Form->mgr; int nbvar=((DdManager *)mgr)->size; mdd_t* tmp; mdd_t* ind =bdd_var_with_index(mgr,nbvar); tmp=mdd_and(res,ind,1,1); mdd_t*data=mdd_and(v1,v2,1,1); (void)lsNewEnd(Form->F,mdd_and(data,ind,1,0),LS_NH); (void)lsNewEnd(Form->F,mdd_and(ind,v1,1,0),LS_NH); (void)lsNewEnd(Form->F,mdd_and(ind,v2,1,0),LS_NH); mdd_free(data); mdd_free(res); return tmp; } void couvert_dnf_to_cnf3(Formula_t Form, mdd_t* clause){ mdd_manager* mgr = Form->mgr; int *vars=NULL; mdd_t* res; mdd_t* tmp=mdd_dup(clause); do{ int i,t = 1; mdd_t* v1; mdd_t* v2; int nbvar=((DdManager *)mgr)->size; vars=Cudd_SupportIndex((DdManager *)mgr, tmp->node); int var_size=Cudd_SupportSize((DdManager *)mgr, tmp->node); res=mdd_one(mgr); for(i=0;inode) > 3); (void)lsNewEnd(Form->F,res,LS_NH); } /* void printf_form(Formula_t form){ char *filename="./test_cnf"; FILE *cnf_file; lsGen gen=lsStart(form->F); lsGeneric data; lsHandle itemHandle; int * vars=NULL; mdd_manager* mgr =Form->mgr; int i,nbvar=((DdManager *)mgr)->size; if(!(cnf_file = fopen(filename, "w"))) { fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n"); return(0); } while(lsNext(gen, &data, &itemHandle) == LS_OK){ mdd_t* l = (mdd_t*)data; vars=Cudd_SupportIndex((DdManager *) mgr,l); } lsFinish(gen); } */ Formula_t ReadCNF_For_Count(Ntk_Network_t *network, st_table *nodeToMvfAigTable, st_table *coiTable, char *filename) { mdd_manager* mgr; Formula_t Form; mdd_t* var; FILE *fin; char line[16384], word[1024], *lp; int nArg,V=0,index; int i, id, sign; long v; st_table* hashTable = st_init_table(st_ptrcmp, st_ptrhash); mdd_t* zero; if(!(fin = fopen(filename, "r"))) { fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n"); return(0); } while(fgets(line, 16384, fin)) { lp = sat_RemoveSpace(line); if(lp[0] == '\n') continue; if(lp[0] == '#') continue; if(lp[0] == 'c') continue; if(lp[0] == 'p') { nArg = sscanf(line, "p cnf %d %d", &nVar, &nCl); if(nArg < 2) { fprintf(vis_stdout,"ERROR : Unable to read the number of "); fprintf(vis_stdout,"variables and clauses from CNF file %s\n"); fclose(fin); return(0); } mgr=bdd_start(nVar); Form=createFormula(mgr); var=mdd_one(mgr); zero=mdd_zero(mgr); continue; } mdd_t* data =mdd_one(mgr); while(1) { lp = sat_RemoveSpace(lp); lp = sat_CopyWord(lp, word); if(strlen(word)) { id = atoi(word); sign = 1; if(id != 0) { if(id < 0) { id = -id; sign = 0; } id <<=3; if(!st_lookup_int(hashTable, (char *)id, &index)) { st_insert(hashTable, (char*)id,(char*) V); index=V; V++; } mdd_t* value= bdd_var_with_index(mgr,index); mdd_t* d =data; mdd_t* v =var; data=mdd_and(data,value,1,sign); var=mdd_and(var,value,1,1); mdd_free(value); mdd_free(v); mdd_free(d); } else { if(mdd_equal(data,zero) || exit_(Form, data)) { mdd_free(data); break; } if(Cudd_SupportSize((DdManager *)mgr,data->node) > 3) couvert_dnf_to_cnf3(Form,data); else (void)lsNewEnd(Form->F,data,LS_NH); break; } } } } mdd_free(Form->V); // mdd_free(Form->R); Form->V=var; st_free_table(hashTable); mdd_free(zero); fclose(fin); return(Form); } void print_formula(Formula_t F){ mdd_manager* mgr = F->mgr; lsGen gen =lsStart(F->F); lsGeneric data; lsHandle itemHandle; printf ("F->F: \n"); while(lsNext(gen, &data, &itemHandle) == LS_OK){ mdd_t* l = (mdd_t*)data; bdd_print(l); } lsFinish(gen); printf ("F->R: \n"); bdd_print(F->R); printf ("F->V: \n"); bdd_print(F->V); getchar(); } int main_Count_test(Ntk_Network_t *network, st_table *nodeToMvfAigTable, st_table *coiTable,char *filename){ Formula_t Form=ReadCNF_For_Count(network,nodeToMvfAigTable, coiTable,filename); srand(time(NULL)); mdd_manager* mgr =Form->mgr; int k=D(Form); free_formula(Form); bdd_end(mgr); return k; } Formula_t ReadCNF_For_Count_( char *filename) { mdd_manager* mgr; Formula_t Form; mdd_t* var; FILE *fin; char line[16384], word[1024], *lp; int nVar, nCl, nArg,V=0,index; int i, id, sign; long v; st_table* hashTable = st_init_table(st_ptrcmp, st_ptrhash); mdd_t* zero; if(!(fin = fopen(filename, "r"))) { fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n"); return(0); } while(fgets(line, 16384, fin)) { lp = sat_RemoveSpace(line); if(lp[0] == '\n') continue; if(lp[0] == '#') continue; if(lp[0] == 'c') continue; if(lp[0] == 'p') { nArg = sscanf(line, "p cnf %d %d", &nVar, &nCl); if(nArg < 2) { fprintf(vis_stdout,"ERROR : Unable to read the number of "); fprintf(vis_stdout,"variables and clauses from CNF file %s\n"); fclose(fin); return(0); } mgr=bdd_start(nVar); Form=createFormula(mgr); var=mdd_one(mgr); zero=mdd_zero(mgr); continue; } mdd_t* data =mdd_one(mgr); while(1) { lp = sat_RemoveSpace(lp); lp = sat_CopyWord(lp, word); if(strlen(word)) { id = atoi(word); sign = 1; if(id != 0) { if(id < 0) { id = -id; sign = 0; } if(!st_lookup_int(hashTable, (char *)id, &index)) { st_insert(hashTable, (char*)id,(char*) V); index=V; V++; } mdd_t* value= bdd_var_with_index(mgr,index); mdd_t* d =data; mdd_t* v =var; data=mdd_and(data,value,1,sign); var=mdd_and(var,value,1,1); mdd_free(value); mdd_free(v); mdd_free(d); } else{ if(mdd_equal(data,zero) || exit_(Form, data)) { mdd_free(data); break; } (void)lsNewEnd(Form->F,data,LS_NH); break; } } } } mdd_free(Form->V); Form->V=var; st_free_table(hashTable); mdd_free(zero); fclose(fin); return(Form); } int main_Count_test_(Ntk_Network_t *network, st_table *nodeToMvfAigTable, st_table *coiTable,char *filename){ Formula_t Form=ReadCNF_For_Count(network,nodeToMvfAigTable, coiTable,filename); srand(time(NULL)); mdd_manager* mgr =Form->mgr; int k=D(Form); free_formula(Form); bdd_end(mgr); return k; return 0; } char * WriteCNF__rel_sat(char *filename) { mdd_manager* mgr; Formula_t Form; mdd_t* var; FILE *fin; char line[16384], word[1024], *lp; int nArg,V=1,index; int i, id, sign; long v; st_table* hashTable = st_init_table(st_ptrcmp, st_ptrhash); mdd_t* zero; char* parseBuffer=(char*)calloc(1024,sizeof(char)); if(!(fin = fopen(filename, "r"))) { fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n"); exit(0); } strcpy(parseBuffer,filename); strcat(parseBuffer, "sat"); char *filenamecnf ="./tmp.vis.cl"; FILE *cnf_file; if(!(cnf_file = fopen(filenamecnf, "w"))) { fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n"); exit(0); } while(fgets(line, 16384, fin)) { lp = sat_RemoveSpace(line); if(lp[0] == '\n') continue; if(lp[0] == '#') continue; if(lp[0] == 'c') continue; if(lp[0] == 'p') { nArg = sscanf(line, "p cnf %d %d", &nVar, &nCl); if(nArg < 2) { fprintf(vis_stdout,"ERROR : Unable to read the number of "); fprintf(vis_stdout,"variables and clauses from CNF file %s\n"); fclose(fin); exit(0); } continue; } while(1) { lp = sat_RemoveSpace(lp); lp = sat_CopyWord(lp, word); if(strlen(word)) { id = atoi(word); sign = 1; if(id != 0) { if(id < 0) { id = -id; sign = 0; } id <<=3; if(!st_lookup_int(hashTable,(char *)id,&index)) { st_insert(hashTable, (char*)id,(char*) V); index=V; V++; } if(!sign) fprintf(cnf_file, " %d ", -index); else fprintf(cnf_file, " %d ", index); } else { fprintf(cnf_file, "0\n"); break; } } } } st_free_table(hashTable); fclose(fin); fclose(cnf_file); char* Buffer=(char*)calloc(1024,sizeof(char)); FILE* s=fopen("./tmp.vis.cnf", "w"); fprintf (s, "p cnf %d %d \n", V-1, nCl); fclose(s); strcpy(Buffer,"cat ./tmp.vis.cnf ./tmp.vis.cl > "); strcat(Buffer, parseBuffer); system(Buffer); system("rm -f ./tmp.vis.cnf ./tmp.vis.cl"); return parseBuffer; } char* main_Count_test_sharp(char *filename, int cnt){ char* cnf_file=WriteCNF__rel_sat(filename); FILE *fp; static char parseBuffer[1024]; static char resBuffer[1024]; static char rmBuffer[1024]; int satStatus; char* line=calloc(2048,sizeof(char)); int num; array_t *result = NIL(array_t); char *tmpStr, *tmpStr1, *tmpStr2; long solverStart; int satTimeOutPeriod = 0; char *fileName = NIL(char); if (cnt) strcpy(parseBuffer,"sharpSAT "); else strcpy(parseBuffer,"sharpSAT -nocount "); strcpy(resBuffer,filename); strcat(resBuffer, "res"); strcpy(rmBuffer,"rm -f "); strcat(rmBuffer,resBuffer); strcat(cnf_file, " > " ); strcat(cnf_file, resBuffer); system(rmBuffer); strcat(parseBuffer, cnf_file); //printf("\n command : %s",parseBuffer); satStatus = system(parseBuffer); if(!(fp = fopen(resBuffer, "r"))) { fprintf(vis_stdout, "%s ERROR : Can't open result file %s\n"); exit(0); } fgets(line, 16384, fp); free(cnf_file); // WriteIDL__rel_sat(filename); return line; } char* main_SatCount(char *filename){ char* cnf_file=WriteCNF__rel_sat(filename); FILE *fp; static char parseBuffer[1024]; static char resBuffer[1024]; static char rmBuffer[1024]; int satStatus; char* line=calloc(2048,sizeof(char)); int num; array_t *result = NIL(array_t); char *tmpStr, *tmpStr1, *tmpStr2; long solverStart; int satTimeOutPeriod = 0; char *fileName = NIL(char); strcpy(parseBuffer,"SatCount "); strcpy(resBuffer,filename); strcat(resBuffer, "res"); strcpy(rmBuffer,"rm -f "); strcat(rmBuffer,resBuffer); strcat(cnf_file, " 40 > " ); strcat(cnf_file, resBuffer); system(rmBuffer); strcat(parseBuffer, cnf_file); //printf("\n command : %s",parseBuffer); satStatus = system(parseBuffer); if(!(fp = fopen(resBuffer, "r"))) { fprintf(vis_stdout, "%s ERROR : Can't open result file %s\n"); exit(0); } fgets(line, 16384, fp); free(cnf_file); // WriteIDL__rel_sat(filename); return line; } //char * void WriteIDL__rel_sat(char *filename) { mdd_manager* mgr; Formula_t Form; mdd_t* var; FILE *fin; char line[16384], word[1024], *lp; int nArg,V=1,index; int i, id, sign; long v; st_table* hashTable = st_init_table(st_ptrcmp, st_ptrhash); mdd_t* zero; char* parseBuffer=(char*)calloc(1024,sizeof(char)); if(!(fin = fopen(filename, "r"))) { fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n"); exit(0); } strcpy(parseBuffer,filename); strcat(parseBuffer, "sat"); char *filenamecnf ="./tmp.vis.idl"; FILE *cnf_file; if(!(cnf_file = fopen(filenamecnf, "w"))) { fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n"); exit(0); } while(fgets(line, 16384, fin)) { lp = sat_RemoveSpace(line); if(lp[0] == '\n') continue; if(lp[0] == '#') continue; if(lp[0] == 'c') continue; if(lp[0] == 'p') { nArg = sscanf(line, "p cnf %d %d", &nVar, &nCl); if(nArg < 2) { fprintf(vis_stdout,"ERROR : Unable to read the number of "); fprintf(vis_stdout,"variables and clauses from CNF file %s\n"); fclose(fin); exit(0); } continue; } int k=0; while(1) { lp = sat_RemoveSpace(lp); lp = sat_CopyWord(lp, word); if(strlen(word)) { id = atoi(word); sign = 1; if(id != 0) { if(id < 0) { id = -id; sign = 0; } id <<=3; if(!st_lookup_int(hashTable,(char *)id,&index)) { st_insert(hashTable, (char*)id,(char*) V); index=V; V++; } if(!sign){ if(!k) fprintf(cnf_file, "-1*x%d ", index); else fprintf(cnf_file, " -1*x%d ", index); } else{ if(!k) fprintf(cnf_file, "+1*x%d ", index); else fprintf(cnf_file, " +1*x%d ", index); } } else { fprintf(cnf_file, ">= +1;\n"); break; } } k++; } } st_free_table(hashTable); fclose(fin); fclose(cnf_file); // char* Buffer=(char*)calloc(1024,sizeof(char)); //strcpy(Buffer,"cp ./tmp.vis.idl "); // strcat(Buffer, parseBuffer); // system(Buffer); // system("rm -f ./tmp.vis.cl"); // return parseBuffer; }