source: vis_dev/vis-2.3/src/rob/SatCountAlgo.c @ 80

Last change on this file since 80 was 19, checked in by cecile, 13 years ago

add rob

File size: 30.3 KB
Line 
1
2/**CFile***********************************************************************
3
4  FileName    [SatCountAlgo.c]
5
6  PackageName [rob]
7
8  Synopsis    [Functions for Sat count Algo. ]
9
10  Author      [Souheib baarir]
11
12  Copyright   [Copyright (c) 2008-2009 The Regents of the Univ. of Paris VI.
13  All rights reserved.
14
15  Permission is hereby granted, without written agreement and without license
16  or royalty fees, to use, copy, modify, and distribute this software and its
17  documentation for any purpose, provided that the above copyright notice and
18  the following two paragraphs appear in all copies of this software.
19
20  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
21  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
22  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
23  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
24
25  THE UNIVERSITY OF PARIS VI SPECIFICALLY DISCLAIMS ANY WARRANTIES,
26  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
27  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
28  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
29  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
30
31*****************************************************************************/
32
33#include "SatCountAlgo.h"
34#include <stdlib.h>
35#include <pthread.h>
36#include <unistd.h>
37#include <sys/sysinfo.h>
38#include <sys/wait.h> 
39#include<time.h>
40
41int nVar=0, nCl=0;
42const int K=5;
43
44
45
46Formula_t
47createFormula(mdd_manager * mgr){
48  Formula_t formul = ALLOC(Formula,1);
49  formul->F=lsCreate();
50  formul->V=mdd_zero(mgr);
51  formul->R=mdd_zero(mgr);
52  formul->mgr=mgr;
53  return formul;
54}
55
56
57void free_formula(Formula_t F){
58  (void)lsDestroy(F->F,mdd_free);
59  mdd_free(F->V);
60  mdd_free(F->R);
61  free(F);
62}
63
64
65static mdd_t*
66mdd_restrict(mdd_manager* mgr,
67             mdd_t* l,mdd_t* d){
68
69  DdNode * tmp=bdd_bdd_restrict(mgr, l->node,d->node);
70
71  if (tmp== DD_ONE((DdManager *)mgr) ) {
72    return mdd_one(mgr);
73  }
74
75  if (tmp==Cudd_Not(DD_ONE((DdManager *)mgr))) {
76    return mdd_zero(mgr);
77  }
78   
79  cuddRef(tmp);
80  return bdd_construct_bdd_t(mgr,tmp);
81}
82
83mdd_t* 
84ComposeCubes(mdd_manager* mgr,
85             mdd_t* vars1,
86             mdd_t* vars2){
87 
88  bdd_node* v[2];
89  v[0]= vars1->node;
90  v[1]= vars2->node;
91  DdNode * b = bdd_bdd_vector_support(mgr,v,2);
92  cuddRef(b);
93  return bdd_construct_bdd_t(mgr,b);
94                             
95}
96
97mdd_t*
98Get_support(mdd_manager* mgr,mdd_t* l){
99
100  DdNode * v = bdd_bdd_support(mgr, l->node);
101  cuddRef(v);
102  return bdd_construct_bdd_t(mgr, v);
103                   
104}
105
106int
107Common_support(mdd_manager* mgr,
108               mdd_t* f,
109               mdd_t* c){
110
111  int v=1;
112
113  mdd_t* fs= Get_support(mgr,f);
114  mdd_t* cs= Get_support(mgr,c);
115  mdd_t* k = bdd_smooth_with_cube(fs,cs);
116
117  assert(k!=NULL);
118
119  if (mdd_equal(k,fs))
120    v=0;
121
122  mdd_free(k);
123  mdd_free(fs);
124  mdd_free(cs);
125  return v;
126
127}
128
129
130Formula_t
131clone_formula(Formula_t form){
132  mdd_manager* mgr = form->mgr;
133  lsGen gen =lsStart(form->F);
134 
135  lsGeneric data;
136  lsHandle  itemHandle;
137  int* vars=NULL;
138  int* vs=NULL;
139  int j=0,i=0;
140  int size=((DdManager *)mgr)->size;
141  mdd_manager* nmgr=bdd_start(size);
142  Formula_t f=NULL;
143
144  if(nmgr){
145    vars=Cudd_SupportIndex((DdManager *) mgr, form->V->node);
146 
147    for (i=0;i< size;i++)
148      if(vars[i]){
149        vars[i]=j;
150        j++; 
151      }
152 
153    mdd_t* zero=mdd_zero(mgr); 
154    mdd_t*    V=mdd_one(nmgr);
155    f=createFormula(nmgr);
156   
157    while(lsNext(gen, &data, &itemHandle) == LS_OK){
158      mdd_t* l =(mdd_t*)data;
159      vs       =Cudd_SupportIndex((DdManager *) mgr, l->node);
160      mdd_t* clause=mdd_one(nmgr);
161     
162      for(i=0;i<size;i++){
163        if(vs[i]){
164          mdd_t* v1=bdd_var_with_index(mgr,i);
165          mdd_t* p=mdd_and(v1,l,1,1);
166          mdd_free(v1);
167
168          mdd_t* v=bdd_var_with_index(nmgr,vars[i]);
169          int sign=(mdd_equal(p,zero)) ? 0:1;
170          mdd_t* tmp= clause;
171          mdd_t* tmp1= V;
172          clause=mdd_and(clause,v,1,sign);
173          V=mdd_and(V,v,1,1);
174         
175          mdd_free(tmp1);
176          mdd_free(tmp);
177          mdd_free(p);
178          mdd_free(v);
179        }
180      }
181      (void)lsNewEnd(f->F,clause,LS_NH);
182      free(vs); 
183    }
184   
185    lsFinish(gen);
186   
187    free(vars);
188    mdd_free(f->V);
189    f->V=V;
190 
191    if(!mdd_equal(form->R,zero)){
192     
193      vars=Cudd_SupportIndex((DdManager *) mgr, form->R->node);
194     
195      for (i=0;i< size;i++)
196        if(vars[i]){
197          vars[i]=j;
198          j++; 
199        }
200     
201      mdd_free(f->R);
202      mdd_t*    R=mdd_one(nmgr);
203      vs=Cudd_SupportIndex((DdManager *) mgr, form->R->node);
204      for(i=0;i<size;i++){
205        if(vs[i]){
206          mdd_t* v=bdd_var_with_index(nmgr,vars[i]);
207          mdd_t* tmp=R;
208          R=mdd_and(R,v,1,1);
209          mdd_free(tmp);
210          mdd_free(v);
211        }
212      }
213      free(vs);
214      free(vars);
215      f->R=R;
216    }
217
218    mdd_free(zero);
219  }
220  return f;
221}
222
223
224
225Formula_t
226_psi(Formula_t For,mdd_t* d){
227 
228  mdd_manager* mgr = For->mgr;
229  lsGen gen =lsStart(For->F);
230 
231  lsGeneric data;
232  lsHandle  itemHandle;
233
234  mdd_t* nd  =bdd_not(d);
235  mdd_t* one =mdd_one(mgr);
236  mdd_t* zero=mdd_zero(mgr);
237  mdd_t* v   =mdd_zero(mgr);
238
239  Formula_t F2=createFormula(mgr);
240  while(lsNext(gen, &data, &itemHandle) == LS_OK){
241    mdd_t* l=(mdd_t*)data; 
242
243    if(Common_support(mgr,l,d)){ 
244      mdd_t* res=mdd_restrict(mgr,l,d);
245      if(mdd_equal(res,zero)){
246        mdd_t* newl = mdd_restrict(mgr,l,nd);
247        (void)lsNewEnd(F2->F,newl,LS_NH);
248        mdd_t* tmp = v;
249        v=ComposeCubes(mgr,v,newl);
250        mdd_free(tmp);
251       
252        if(mdd_equal(newl,one)){
253          lsFinish(gen);       
254          mdd_free(res);         
255          mdd_free(one);
256          mdd_free(zero);
257          mdd_free(nd);
258          return F2; 
259        }
260     
261      }     
262      mdd_free(res);
263    }
264    else{
265      mdd_t* ll= mdd_dup(l);
266      (void)lsNewEnd(F2->F,ll,LS_NH);
267      mdd_t* tmp=v;
268      v=ComposeCubes(mgr,v,l);
269      mdd_free(tmp);
270    }
271  }
272
273  lsFinish(gen);
274  // New set of elemanated variables
275  mdd_t* v1=ComposeCubes(mgr,v,d);
276  mdd_t* newelem=bdd_smooth_with_cube(For->V,v1);
277  mdd_t* R;
278  mdd_t* V;
279
280  R=mdd_dup(For->R);
281  mdd_free(F2->R);
282  mdd_free(F2->V);
283 
284  if (!mdd_equal(newelem,one)){
285    F2->R=ComposeCubes(mgr,R,newelem);
286    mdd_free(R);
287  }
288  else{
289    F2->R=R;
290  }
291
292  // New set of variables
293  F2->V=v;
294
295  mdd_free(one);
296  mdd_free(zero);
297  mdd_free(v1);
298  mdd_free(nd);
299  mdd_free(newelem);
300
301  return F2;
302}
303
304mdd_t* 
305get_var_sup (Formula_t Form){
306  lsGeneric data;
307  lsHandle itemHandle;
308  mdd_manager* mgr =Form->mgr;
309  lsGen gen=lsStart(Form->F);
310  mdd_t* Current;
311  mdd_t* Before=mdd_zero(mgr);
312
313  (void)lsFirstItem(Form->F,&data,&itemHandle);
314  Current=Get_support(mgr,(mdd_t*)data);
315
316  assert(Current!=NULL);
317
318  do{ 
319
320    mdd_free(Before); 
321    Before = mdd_dup(Current);
322    while(lsNext(gen, &data, &itemHandle) == LS_OK){
323      mdd_t* l = mdd_dup((mdd_t*)data);
324      mdd_t* sup =Get_support (mgr,l);
325      if(Common_support(mgr,Current, l)){
326        mdd_t* tmp= Current;
327        Current=ComposeCubes(mgr,Current,sup);
328        mdd_free(tmp);
329      }
330      mdd_free(l);
331      mdd_free(sup); 
332    } 
333    lsFinish(gen);
334    gen=lsStart(Form->F);
335  } 
336  while(!mdd_equal(Before,Current));
337  lsFinish(gen);
338
339  mdd_free(Before);
340  return Current;
341}
342 
343
344int
345disjoint_formula(Formula_t Form,
346                 Formula_t* F1, 
347                 Formula_t* F2){
348
349  lsGeneric data;
350  lsHandle itemHandle;
351  lsGen gen=lsStart(Form->F);
352  mdd_manager* mgr =Form->mgr;
353  mdd_t* V1;
354  mdd_t* V2; 
355
356  V2=get_var_sup (Form);
357
358  if (!mdd_equal(V2,Form->V)){
359
360    (*F1)    = createFormula(mgr);
361    (*F2)    = createFormula(mgr);
362    mdd_free((*F2)->V);
363    mdd_free((*F1)->V);
364    (*F2)->V = V2;
365    (*F1)->V = bdd_smooth_with_cube(Form->V,V2);
366   
367    assert((*F1)->V!=NULL);
368
369    while(lsNext(gen, &data, &itemHandle) == LS_OK){
370      mdd_t* l = mdd_dup((mdd_t*)data);
371      if(Common_support(mgr,V2, l)){
372        (void)lsNewEnd((*F2)->F,mdd_dup(data),LS_NH);
373      }
374      else{
375        (void)lsNewEnd((*F1)->F,mdd_dup(data),LS_NH);
376      }
377      mdd_free(l);
378    }
379
380    lsFinish(gen);
381    return 1;
382  }
383  lsFinish(gen);
384  mdd_free(V2);
385  return 0;
386}
387
388
389
390
391int 
392_d(Formula_t Form, mdd_t* x){
393 
394  int cpt=0;
395  lsGeneric data;
396  lsHandle itemHandle;
397  lsGen gen=lsStart(Form->F);
398  mdd_manager* mgr =Form->mgr;
399 
400  while(lsNext(gen, &data, &itemHandle) == LS_OK){
401    mdd_t* l = mdd_dup((mdd_t*)data);
402
403    if(Common_support(mgr,l,x))
404      cpt ++;
405   
406    mdd_free(l);
407  }
408
409  lsFinish(gen);
410  return cpt;
411}
412
413
414
415mdd_t* 
416_k_clause(Formula_t Form, int k){
417  int cpt=0;
418  lsGeneric data;
419  lsHandle itemHandle;
420  lsGen gen=lsStart(Form->F);
421  mdd_manager* mgr =Form->mgr;
422 
423  while(lsNext(gen, &data, &itemHandle) == LS_OK){
424    mdd_t* l = (mdd_t*)data;
425    if (Cudd_SupportSize((DdManager *) mgr,
426                         l->node)==k){
427      lsFinish(gen);
428      return mdd_dup(l);
429    }
430  }
431
432  lsFinish(gen);
433  return mdd_zero(mgr);
434}
435
436
437int 
438greater_d(Formula_t Form,int k){
439  int* vars=NULL;
440  mdd_manager* mgr =Form->mgr;
441  int nbvar=((DdManager *)mgr)->size;
442  int d=0,i,g,s;
443  mdd_t* zero=mdd_zero(mgr);
444 
445  for(i=0;i<nbvar;++i){
446    mdd_t* v=bdd_var_with_index(mgr,i);
447    mdd_t* c=_k_clause(Form, k);
448    if (!mdd_equal(c, zero) &&
449        (s=_d(Form,v))> d){
450      d = s;
451      g = i;
452    }
453    mdd_free(v);
454    mdd_free(c);
455  }
456
457  mdd_free(zero);
458  return g;
459}
460
461
462mdd_t*
463get_w(Formula_t Form,
464      mdd_t* clause,
465      int * vars, int k){
466  int i,j,nbvar=((DdManager *)(Form->mgr))->size;
467  mdd_manager* mgr =Form->mgr;
468
469  for(i=0;i<nbvar;++i){
470    if(vars[i]){
471      mdd_t* v=bdd_var_with_index(mgr,i);
472      if (_d(Form,v)==k){
473        mdd_t* s=Get_support(mgr,clause);
474        mdd_t* r=bdd_smooth_with_cube(s,v);
475        mdd_free(v);
476        mdd_free(s);
477        return r;
478      }
479      mdd_free(v);
480    }
481  }
482  return mdd_zero(mgr); 
483}
484
485mdd_t*
486pick_2_clause_w(Formula_t Form, mdd_t* clause){
487  int * vars=NULL;
488  mdd_manager* mgr =Form->mgr;
489  int i,nbvar=((DdManager *)mgr)->size;
490  mdd_t* w;
491  mdd_t* zero=mdd_zero(mgr);
492 
493  vars=Cudd_SupportIndex((DdManager *) mgr, clause->node);
494
495  if (!mdd_equal((w=get_w(Form, clause, vars, 1)), 
496                 zero)){
497    free(vars);
498    mdd_free(zero);
499    return w;
500  }
501 
502  mdd_free(w);
503
504  if (!mdd_equal((w=get_w(Form, clause, vars, 2)), 
505                 zero)){
506    free(vars);
507    mdd_free(zero);
508    return w;
509  }   
510
511  mdd_free(w);
512  mdd_free(zero);
513  free(vars);
514  int ind = greater_d(Form,2);
515  return bdd_var_with_index(mgr,ind);
516}
517
518mdd_t*
519get_neighbour(Formula_t Form, mdd_t* x,int * deg){
520   
521  mdd_manager* mgr = Form->mgr;
522  lsGen gen=lsStart(Form->F);
523 
524  lsGeneric data;
525  lsHandle itemHandle;
526  mdd_t* res = mdd_zero(mgr);
527 
528  while(lsNext(gen, &data, &itemHandle) == LS_OK){
529    mdd_t* l = (mdd_t*)data;
530    if(Common_support(mgr,l, x)){
531      mdd_t* tmp=res;
532      mdd_t* cmp=bdd_smooth_with_cube(l,x);
533      res =ComposeCubes(mgr,res,cmp);
534      mdd_free(tmp);
535      mdd_free(cmp);
536    }
537  }
538
539  lsFinish(gen);
540 
541  (*deg)= Cudd_SupportSize((DdManager *) mgr,res->node);
542  return res;
543}
544
545mdd_t*
546get_max_degree_(Formula_t Form, mdd_t* clause){
547  int *vars=NULL;
548  int i,max=0,deg;
549  mdd_manager* mgr =Form->mgr;
550  int nbvar=((DdManager *)mgr)->size;
551  mdd_t* res=mdd_zero(mgr);
552  vars=Cudd_SupportIndex((DdManager *)mgr,clause->node);
553
554  for(i=0;i<nbvar;++i){
555    if (vars[i]){
556      mdd_t* v  =bdd_var_with_index(mgr,i);
557      mdd_t* nhb=get_neighbour(Form, v,&deg);
558      if(deg> max) {
559        max=deg;
560        mdd_free(res);
561        res=mdd_dup(v);
562      }
563      mdd_free(v);
564      mdd_free(nhb);
565   }
566  }
567 
568  free(vars);
569  return res;
570}
571
572mdd_t*
573get_max_nhb_degre(Formula_t Form, 
574                  int * vars,
575                  int k){
576
577  mdd_manager* mgr =Form->mgr;
578  int i,deg,nbvar=((DdManager *)mgr)->size;
579  mdd_t* r;
580 
581  for(i=0;i<nbvar;++i){
582    if (vars[i]){
583      mdd_t* v=bdd_var_with_index(mgr,i);
584      if(_d(Form,v)== k) {
585        mdd_t* nhb=get_neighbour(Form, v,&deg);
586        r=get_max_degree_(Form, nhb);
587        mdd_free(v);
588        mdd_free(nhb);
589        return r;
590      }
591    } 
592  } 
593  return mdd_zero(mgr);
594}
595
596
597mdd_t*
598pick_clause_w(Formula_t Form){
599  int * vars=NULL;
600  mdd_manager* mgr =Form->mgr;
601  int i,deg,max=0,nbvar=((DdManager *)mgr)->size;
602  mdd_t* w=mdd_zero(mgr);
603  mdd_t* zero=mdd_zero(mgr);
604 
605  vars=Cudd_SupportIndex((DdManager *) mgr, Form->V->node);
606
607  if(!mdd_equal((w=get_max_nhb_degre(Form, vars, 1)), 
608                zero)){
609    free(vars);
610    mdd_free(zero);
611    return w;
612  }
613
614  if(!mdd_equal((w=get_max_nhb_degre(Form, vars, 2)), 
615                zero)){
616    free(vars);
617    mdd_free(zero);
618    return w;
619  }
620 
621  for(i=0;i<nbvar;++i){
622    if(vars[i]){
623      mdd_t* v=bdd_var_with_index(mgr,i);
624      mdd_t* t=get_neighbour(Form,v,&deg);
625      if(deg > max ){
626        max=deg;
627        mdd_free(w);
628        w=mdd_dup(v);
629      }
630      mdd_free(t);
631      mdd_free(v);
632    }
633  }
634  mdd_free(zero);
635  free(vars);
636  return w;
637}
638
639int 
640is_empty_formula(Formula_t Form){
641  mdd_manager* mgr = Form->mgr;
642  lsGen gen=lsStart(Form->F);
643 
644  lsGeneric data;
645  lsHandle itemHandle;
646  mdd_t* one = mdd_one(mgr);
647 
648  while(lsNext(gen, &data, &itemHandle) == LS_OK){
649    mdd_t* l = (mdd_t*)data;
650    if(mdd_equal(l,one)){
651      lsFinish(gen);
652      return TRUE;
653    }
654  }
655  mdd_free(one);
656  lsFinish(gen);
657  return FALSE;
658}
659
660
661int
662D(Formula_t Form){
663  mdd_manager* mgr = Form->mgr;
664  Formula_t F1,F2;
665  mdd_t* R;
666  mdd_t* x;
667  mdd_t* w;
668  int card_R,d_f1,d_f2;
669  mdd_t* zero = mdd_zero(mgr);
670  unsigned long lswap;
671
672  if (is_empty_formula(Form)) {
673    mdd_free(zero);
674    return 0;
675  }
676 
677  if (lsLength(Form->F)==0) {
678    int r  =Cudd_SupportSize((DdManager *)mgr,
679                             (Form->R)->node);
680    card_R =(int)pow(2,r);
681    mdd_free(zero);
682    return card_R;
683  }
684 
685  if(disjoint_formula(Form,&F1,&F2)){
686    d_f1=0;d_f2=0;
687    int r  =Cudd_SupportSize((DdManager *)mgr,
688                             (Form->R)->node);
689    card_R =(int)pow(2,r);
690   
691    // if ((rand()%K) == 0){
692    if (K <= 12){
693      int fd1[2];
694      int fd2[2];
695
696      if (pipe(fd1) != 0)  {
697        fprintf(stderr,"Problemes dans l'ouverture de Pipe \n");
698        exit(1);
699      }
700 
701      if (pipe(fd2) != 0)  {
702        fprintf(stderr,"Problemes dans l'ouverture de Pipe \n");
703        exit(1);
704      } 
705      int pid1,pid2;
706
707      if((pid1=fork())==0){
708        char buf[30]="\0";
709        d_f1=D(F1);
710        close(fd1[0]); 
711        sprintf(buf,"%d",d_f1);
712        write(fd1[1], buf, strlen(buf)); 
713        close(fd1[1]); 
714        //free_formula(F1);
715        exit(EXIT_SUCCESS); 
716      }
717   
718      if((pid2=fork())==0){
719        char buf[30]="\0";
720        d_f2=D(F2);
721        close(fd2[0]); 
722        sprintf(buf,"%d",d_f2);
723        write(fd2[1],buf,strlen(buf)); 
724        close(fd2[1]); 
725        //free_formula(F2);
726        exit(EXIT_SUCCESS); 
727      }
728     
729      int i,s;
730      if(pid1 > 0){
731        free_formula(F1);
732        char buf[30]="\0";
733        i=waitpid(pid1, &s, WUNTRACED);
734        close(fd1[1]);
735        read(fd1[0],buf,30);
736        d_f1=atoi(buf);
737        close(fd1[0]);
738      }else{
739        d_f1=D(F1);
740        free_formula(F1);
741      }
742
743      if(pid2 > 0){
744        free_formula(F2); 
745        char buf[30]="\0";
746        i=waitpid(pid2, &s, WUNTRACED);
747        close(fd2[1]);
748        read(fd2[0],buf,30);
749        d_f2=atoi(buf);
750        close(fd2[0]);
751      }else{
752        d_f2=D(F2);
753        free_formula(F2); 
754      }
755    }
756    else{
757      d_f1=D(F1);free_formula(F1);
758      d_f2=D(F2);free_formula(F2); 
759    }
760    assert( card_R*d_f1*d_f2 >= 0);
761    return card_R*d_f1*d_f2; 
762  }
763 
764  if(!mdd_equal((x=_k_clause(Form,1)),zero)){
765
766    F1=Form;
767    int k;
768    do{ 
769      F2 = F1; F1 =_psi(F2,x); mdd_free(x);
770      k=mdd_equal((x=_k_clause(F1,1)),zero);
771      if( F2 != Form)
772        free_formula(F2);
773
774    } while(!k && !is_empty_formula(F1));
775
776    d_f1  =D(F1);
777    free_formula(F1);
778    mdd_free(x); 
779    mdd_free(zero);
780    return d_f1;
781  }
782
783  mdd_free(x);
784  if(!mdd_equal((x=_k_clause(Form,2)),zero)){
785    w=pick_2_clause_w(Form,x);   
786  }
787  else{
788    w=pick_clause_w(Form);
789  }
790 
791  mdd_t* nw=mdd_not(w);
792  // if ((rand()%K) == 0){
793  if (K <= 12){
794    int fd1[2];
795    int fd2[2];
796
797    if (pipe(fd1) != 0)  {
798      fprintf(stderr,"Problemes dans l'ouverture de Pipe \n");
799      exit(1);
800    }
801
802    if (pipe(fd2) != 0)  {
803      fprintf(stderr,"Problemes dans l'ouverture de Pipe \n");
804      exit(1);
805    } 
806    int pid1,pid2;
807    if((pid1=fork())==0){
808      char buf[30]="\0";
809      F1=_psi(Form,w);
810      d_f1=D(F1);
811      close(fd1[0]); 
812      sprintf(buf,"%d",d_f1);
813      write(fd1[1],buf,strlen(buf)); 
814      close(fd1[1]); 
815      exit(EXIT_SUCCESS); 
816    }
817   
818    if((pid2=fork())==0){
819      char buf[30]="\0";
820      F2=_psi(Form,nw);
821      d_f2=D(F2);
822      close(fd2[0]); 
823      sprintf(buf,"%d",d_f2);
824      write(fd2[1],buf,strlen(buf)); 
825      close(fd2[1]); 
826      exit(EXIT_SUCCESS); 
827    }
828   
829    int i,s;
830    if(pid1>0){
831      char buf[30]="\0";
832      i=waitpid(pid1,&s,WUNTRACED);
833      close(fd1[1]);
834      read(fd1[0],buf,30);
835      d_f1=atoi(buf);
836      close(fd1[0]);
837    }else{
838      F1=_psi(Form,w);
839      d_f1=D(F1);
840      free_formula(F1);
841    }
842
843    if(pid2>0){
844      char buf[30]="\0";
845      i=waitpid(pid2,&s, WUNTRACED);
846      close(fd2[1]);
847      read(fd2[0],buf, 30);
848      d_f2=atoi(buf);
849      close(fd2[0]);
850    }else{
851      F2=_psi(Form,nw);
852      d_f2=D(F2);
853      free_formula(F2); 
854    }
855  }
856  else{
857    F1=_psi(Form,w);
858    F2=_psi(Form,nw);
859    d_f1=D(F1);free_formula(F1);
860    d_f2=D(F2);free_formula(F2);
861  }
862
863  mdd_free(x);
864  mdd_free(w);
865  mdd_free(nw);
866  mdd_free(zero);
867  assert(d_f1+d_f2 >= 0);
868  return (d_f1+d_f2);
869}
870
871int exit_(Formula_t Form, mdd_t* n){
872  lsGen gen=lsStart(Form->F);
873 
874  lsGeneric data;
875  lsHandle itemHandle;
876
877  while(lsNext(gen, &data, &itemHandle) == LS_OK){ 
878    if(mdd_equal(data,n)){
879        lsFinish(gen);
880        return TRUE;
881    }
882  }
883  lsFinish(gen);
884  return FALSE;
885}
886/*
887int var_to_add(int size){
888  int k,r,nb=0;
889  k=size;
890 
891  do{
892    k=(int)k/2;
893    r=size % 2;
894    nb +=k;k +=r;
895  }while(k > 3);
896
897  return nb;
898}
899*/
900
901mdd_t* convert_dnf_cnf(Formula_t Form,
902                       mdd_t* v1,mdd_t* v2,
903                       mdd_t* res){
904  mdd_manager* mgr = Form->mgr;
905  int nbvar=((DdManager *)mgr)->size;
906  mdd_t* tmp;
907
908  mdd_t* ind  =bdd_var_with_index(mgr,nbvar);
909  tmp=mdd_and(res,ind,1,1);
910  mdd_t*data=mdd_and(v1,v2,1,1);
911  (void)lsNewEnd(Form->F,mdd_and(data,ind,1,0),LS_NH);
912  (void)lsNewEnd(Form->F,mdd_and(ind,v1,1,0),LS_NH);
913  (void)lsNewEnd(Form->F,mdd_and(ind,v2,1,0),LS_NH);
914  mdd_free(data);
915  mdd_free(res);
916  return tmp;
917}
918
919
920void 
921couvert_dnf_to_cnf3(Formula_t Form,
922                    mdd_t* clause){
923  mdd_manager* mgr = Form->mgr;
924  int  *vars=NULL;
925  mdd_t* res;
926  mdd_t* tmp=mdd_dup(clause);
927 
928  do{
929    int i,t = 1;
930    mdd_t* v1;
931    mdd_t* v2;
932    int nbvar=((DdManager *)mgr)->size;
933    vars=Cudd_SupportIndex((DdManager *)mgr,
934                           tmp->node);
935    int var_size=Cudd_SupportSize((DdManager *)mgr,
936                                  tmp->node);
937    res=mdd_one(mgr);
938    for(i=0;i<nbvar && var_size;++i){
939      if(vars[i] && t==1){ 
940        v1=bdd_var_with_index(mgr,i);
941        var_size --;
942        if(var_size != 0)
943          t=2;
944        else{
945          mdd_t* tmp1=res;
946          res=mdd_and(res,v1,1,1);
947          mdd_free(tmp1);
948        }
949      }
950
951      if(vars[i] && t==2){ 
952        var_size --;
953        v2=bdd_var_with_index(mgr,i);
954        res=convert_dnf_cnf(Form,v1,v2,res); 
955        t=1;
956      } 
957   
958    } 
959    free(vars);
960    mdd_free(tmp);
961    tmp=res;
962  }while(Cudd_SupportSize((DdManager *)mgr,res->node) > 3);
963
964  (void)lsNewEnd(Form->F,res,LS_NH);
965
966}
967
968/*
969void printf_form(Formula_t form){
970
971  char *filename="./test_cnf";
972  FILE *cnf_file;
973  lsGen gen=lsStart(form->F);
974  lsGeneric data;
975  lsHandle itemHandle;
976  int * vars=NULL;
977  mdd_manager* mgr =Form->mgr;
978  int i,nbvar=((DdManager *)mgr)->size;
979 
980 
981  if(!(cnf_file = fopen(filename, "w"))) {
982    fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n");
983    return(0);
984  }
985
986  while(lsNext(gen, &data, &itemHandle) == LS_OK){
987    mdd_t* l = (mdd_t*)data;
988    vars=Cudd_SupportIndex((DdManager *) mgr,l);
989   
990
991
992  }
993
994  lsFinish(gen);
995}
996
997*/
998Formula_t
999ReadCNF_For_Count(Ntk_Network_t   *network,
1000                  st_table        *nodeToMvfAigTable,
1001                  st_table        *coiTable,
1002                  char            *filename) {
1003  mdd_manager* mgr; 
1004  Formula_t    Form;
1005  mdd_t* var;
1006  FILE *fin;
1007  char line[16384], word[1024], *lp;
1008  int  nArg,V=0,index;
1009  int i, id, sign;
1010  long v;
1011  st_table*  hashTable = 
1012    st_init_table(st_ptrcmp, st_ptrhash);
1013  mdd_t* zero;
1014 
1015  if(!(fin = fopen(filename, "r"))) {
1016    fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n");
1017    return(0);
1018  }
1019
1020  while(fgets(line, 16384, fin)) {
1021
1022    lp = sat_RemoveSpace(line);
1023
1024    if(lp[0] == '\n')   continue;
1025    if(lp[0] == '#')    continue;
1026    if(lp[0] == 'c')    continue;
1027
1028    if(lp[0] == 'p') {
1029           
1030      nArg = sscanf(line, "p cnf %d %d", &nVar, &nCl);
1031     
1032      if(nArg < 2) {
1033        fprintf(vis_stdout,"ERROR : Unable to read the number of ");
1034        fprintf(vis_stdout,"variables and clauses from CNF file %s\n");
1035        fclose(fin);
1036        return(0);
1037      }
1038
1039      mgr=bdd_start(nVar); 
1040      Form=createFormula(mgr);
1041      var=mdd_one(mgr);
1042      zero=mdd_zero(mgr);
1043      continue;
1044    }
1045
1046    mdd_t* data =mdd_one(mgr);
1047
1048    while(1) { 
1049      lp = sat_RemoveSpace(lp);
1050      lp = sat_CopyWord(lp, word);
1051
1052      if(strlen(word)) {
1053        id = atoi(word);
1054        sign = 1;
1055
1056        if(id != 0) {
1057          if(id < 0) {
1058            id = -id;
1059            sign = 0;
1060          }
1061
1062          id <<=3;
1063         
1064          if(!st_lookup_int(hashTable, (char *)id, &index)) {
1065            st_insert(hashTable, (char*)id,(char*) V);
1066            index=V; V++; 
1067          }
1068         
1069          mdd_t* value= bdd_var_with_index(mgr,index);
1070          mdd_t* d =data;
1071          mdd_t* v =var;
1072       
1073          data=mdd_and(data,value,1,sign);
1074          var=mdd_and(var,value,1,1);
1075          mdd_free(value);
1076          mdd_free(v);
1077          mdd_free(d);
1078        }
1079        else {
1080         
1081          if(mdd_equal(data,zero) || 
1082             exit_(Form, data)) {
1083            mdd_free(data);
1084            break;
1085          }
1086
1087         
1088          if(Cudd_SupportSize((DdManager *)mgr,data->node) > 3)
1089            couvert_dnf_to_cnf3(Form,data);
1090          else
1091            (void)lsNewEnd(Form->F,data,LS_NH);
1092          break;
1093        }
1094      }
1095    } 
1096  }
1097  mdd_free(Form->V);
1098  // mdd_free(Form->R);
1099
1100  Form->V=var;
1101   
1102  st_free_table(hashTable);
1103  mdd_free(zero);
1104  fclose(fin);
1105  return(Form);
1106}
1107
1108void print_formula(Formula_t F){
1109 mdd_manager* mgr = F->mgr;
1110  lsGen gen =lsStart(F->F);
1111 
1112  lsGeneric data;
1113  lsHandle  itemHandle;
1114 
1115  printf ("F->F: \n");
1116  while(lsNext(gen, &data, &itemHandle) == LS_OK){
1117    mdd_t* l = (mdd_t*)data;
1118    bdd_print(l);
1119  }
1120  lsFinish(gen);
1121 
1122  printf ("F->R: \n");
1123  bdd_print(F->R);
1124 
1125  printf ("F->V: \n");
1126  bdd_print(F->V);
1127 
1128  getchar();
1129}
1130
1131
1132int 
1133main_Count_test(Ntk_Network_t   *network,
1134                st_table        *nodeToMvfAigTable,
1135                st_table        *coiTable,char *filename){
1136 
1137  Formula_t Form=ReadCNF_For_Count(network,nodeToMvfAigTable,
1138                                   coiTable,filename);
1139  srand(time(NULL));
1140  mdd_manager* mgr =Form->mgr;
1141  int k=D(Form);
1142  free_formula(Form);
1143  bdd_end(mgr);
1144 
1145  return k;
1146}
1147
1148
1149Formula_t
1150ReadCNF_For_Count_( char *filename) {
1151  mdd_manager* mgr; 
1152  Formula_t    Form;
1153  mdd_t* var;
1154  FILE *fin;
1155  char line[16384], word[1024], *lp;
1156  int nVar, nCl, nArg,V=0,index;
1157  int i, id, sign;
1158  long v;
1159  st_table*  hashTable = 
1160    st_init_table(st_ptrcmp, st_ptrhash);
1161  mdd_t* zero;
1162 
1163  if(!(fin = fopen(filename, "r"))) {
1164    fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n");
1165    return(0);
1166  }
1167
1168  while(fgets(line, 16384, fin)) {
1169
1170    lp = sat_RemoveSpace(line);
1171
1172    if(lp[0] == '\n')   continue;
1173    if(lp[0] == '#')    continue;
1174    if(lp[0] == 'c')    continue;
1175
1176    if(lp[0] == 'p') {
1177           
1178      nArg = sscanf(line, "p cnf %d %d", &nVar, &nCl);
1179     
1180      if(nArg < 2) {
1181        fprintf(vis_stdout,"ERROR : Unable to read the number of ");
1182        fprintf(vis_stdout,"variables and clauses from CNF file %s\n");
1183        fclose(fin);
1184        return(0);
1185      }
1186
1187      mgr=bdd_start(nVar); 
1188      Form=createFormula(mgr);
1189      var=mdd_one(mgr);
1190      zero=mdd_zero(mgr);
1191      continue;
1192    }
1193
1194    mdd_t* data =mdd_one(mgr);
1195
1196    while(1) { 
1197      lp = sat_RemoveSpace(lp);
1198      lp = sat_CopyWord(lp, word);
1199
1200      if(strlen(word)) {
1201        id = atoi(word);
1202        sign = 1;
1203
1204        if(id != 0) {
1205          if(id < 0) {
1206            id = -id;
1207            sign = 0;
1208          }
1209 
1210          if(!st_lookup_int(hashTable, (char *)id, &index)) {
1211            st_insert(hashTable, (char*)id,(char*) V);
1212            index=V; V++; 
1213          }
1214
1215          mdd_t* value= bdd_var_with_index(mgr,index);
1216          mdd_t* d =data;
1217          mdd_t* v =var;
1218         
1219          data=mdd_and(data,value,1,sign);
1220          var=mdd_and(var,value,1,1);
1221          mdd_free(value);
1222          mdd_free(v);
1223          mdd_free(d);
1224        }
1225        else{
1226
1227          if(mdd_equal(data,zero) || 
1228             exit_(Form, data)) {
1229            mdd_free(data);
1230            break;
1231          }
1232          (void)lsNewEnd(Form->F,data,LS_NH); break;
1233        }
1234      }
1235    } 
1236  }
1237  mdd_free(Form->V);
1238 
1239  Form->V=var;
1240   
1241  st_free_table(hashTable);
1242  mdd_free(zero);
1243  fclose(fin);
1244  return(Form);
1245}
1246
1247
1248
1249
1250
1251int 
1252main_Count_test_(Ntk_Network_t   *network,
1253                st_table        *nodeToMvfAigTable,
1254                st_table        *coiTable,char *filename){
1255 
1256  Formula_t Form=ReadCNF_For_Count(network,nodeToMvfAigTable,
1257                                   coiTable,filename);
1258  srand(time(NULL));
1259  mdd_manager* mgr =Form->mgr;
1260  int k=D(Form);
1261  free_formula(Form);
1262  bdd_end(mgr);
1263 
1264  return k;
1265  return 0;
1266
1267}
1268
1269
1270
1271char *
1272WriteCNF__rel_sat(char *filename) {
1273  mdd_manager* mgr; 
1274  Formula_t    Form;
1275  mdd_t* var;
1276  FILE *fin;
1277  char line[16384], word[1024], *lp;
1278  int  nArg,V=1,index;
1279  int i, id, sign;
1280  long v;
1281  st_table*  hashTable = 
1282    st_init_table(st_ptrcmp, st_ptrhash);
1283  mdd_t* zero;
1284  char* parseBuffer=(char*)calloc(1024,sizeof(char));
1285
1286  if(!(fin = fopen(filename, "r"))) {
1287    fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n");
1288    exit(0);
1289  }
1290
1291  strcpy(parseBuffer,filename);
1292  strcat(parseBuffer, "sat");
1293  char            *filenamecnf ="./tmp.vis.cl";
1294  FILE            *cnf_file; 
1295
1296  if(!(cnf_file = fopen(filenamecnf, "w"))) {
1297    fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n");
1298    exit(0);
1299  }
1300
1301  while(fgets(line, 16384, fin)) {
1302
1303    lp = sat_RemoveSpace(line);
1304
1305    if(lp[0] == '\n')   continue;
1306    if(lp[0] == '#')    continue;
1307    if(lp[0] == 'c')    continue;
1308
1309    if(lp[0] == 'p') {
1310           
1311      nArg = sscanf(line, "p cnf %d %d", &nVar, &nCl);
1312     
1313      if(nArg < 2) {
1314        fprintf(vis_stdout,"ERROR : Unable to read the number of ");
1315        fprintf(vis_stdout,"variables and clauses from CNF file %s\n");
1316        fclose(fin);
1317        exit(0);
1318      }
1319
1320       continue;
1321    }
1322
1323 
1324    while(1) { 
1325      lp = sat_RemoveSpace(lp);
1326      lp = sat_CopyWord(lp, word);
1327
1328      if(strlen(word)) {
1329        id = atoi(word);
1330        sign = 1;
1331
1332        if(id != 0) {
1333
1334          if(id < 0) {
1335            id = -id;
1336            sign = 0;
1337          }
1338
1339          id <<=3;
1340         
1341          if(!st_lookup_int(hashTable,(char *)id,&index)) {
1342            st_insert(hashTable, (char*)id,(char*) V);
1343            index=V; V++; 
1344          }
1345         
1346          if(!sign)
1347            fprintf(cnf_file, " %d ", -index); 
1348          else
1349            fprintf(cnf_file, " %d ", index); 
1350        }
1351        else {
1352          fprintf(cnf_file, "0\n"); break;
1353        }
1354      }
1355    } 
1356  }
1357 
1358  st_free_table(hashTable);
1359  fclose(fin);
1360  fclose(cnf_file);
1361
1362  char* Buffer=(char*)calloc(1024,sizeof(char));
1363  FILE* s=fopen("./tmp.vis.cnf", "w");
1364  fprintf (s, "p cnf %d %d \n", V-1, nCl);
1365  fclose(s);
1366
1367  strcpy(Buffer,"cat ./tmp.vis.cnf ./tmp.vis.cl > ");
1368  strcat(Buffer, parseBuffer);
1369  system(Buffer);
1370  system("rm -f ./tmp.vis.cnf ./tmp.vis.cl");
1371  return parseBuffer;
1372}
1373
1374
1375char*   
1376main_Count_test_sharp(char *filename, int cnt){
1377 
1378 char* cnf_file=WriteCNF__rel_sat(filename);
1379 
1380 FILE        *fp;
1381 static char parseBuffer[1024];
1382 static char resBuffer[1024];
1383 static char rmBuffer[1024];
1384 int         satStatus;
1385 char*        line=calloc(2048,sizeof(char));
1386 int         num;
1387 array_t     *result = NIL(array_t);
1388 char        *tmpStr, *tmpStr1, *tmpStr2;
1389 long        solverStart;
1390 int         satTimeOutPeriod = 0;
1391 char        *fileName = NIL(char);
1392
1393
1394if (cnt)  strcpy(parseBuffer,"sharpSAT ");
1395else strcpy(parseBuffer,"sharpSAT -nocount ");
1396
1397 strcpy(resBuffer,filename);
1398 strcat(resBuffer, "res");
1399 strcpy(rmBuffer,"rm -f ");
1400 strcat(rmBuffer,resBuffer);
1401 strcat(cnf_file, " > " );
1402 strcat(cnf_file, resBuffer);
1403
1404 system(rmBuffer);
1405 strcat(parseBuffer, cnf_file);
1406 
1407 //printf("\n command : %s",parseBuffer);
1408 
1409 satStatus = system(parseBuffer);
1410 
1411 if(!(fp = fopen(resBuffer, "r"))) {
1412   fprintf(vis_stdout, "%s ERROR : Can't open result file %s\n");
1413   exit(0);
1414 }
1415
1416 fgets(line, 16384, fp);
1417 free(cnf_file);
1418// WriteIDL__rel_sat(filename);
1419 return line;
1420 
1421}
1422
1423char*   
1424main_SatCount(char *filename){
1425 
1426 char* cnf_file=WriteCNF__rel_sat(filename);
1427 
1428 FILE        *fp;
1429 static char parseBuffer[1024];
1430 static char resBuffer[1024];
1431 static char rmBuffer[1024];
1432 int         satStatus;
1433 char*        line=calloc(2048,sizeof(char));
1434 int         num;
1435 array_t     *result = NIL(array_t);
1436 char        *tmpStr, *tmpStr1, *tmpStr2;
1437 long        solverStart;
1438 int         satTimeOutPeriod = 0;
1439 char        *fileName = NIL(char);
1440
1441
1442strcpy(parseBuffer,"SatCount ");
1443
1444
1445 strcpy(resBuffer,filename);
1446 strcat(resBuffer, "res");
1447 strcpy(rmBuffer,"rm -f ");
1448 strcat(rmBuffer,resBuffer);
1449 strcat(cnf_file, " 40 > " );
1450 strcat(cnf_file, resBuffer);
1451
1452 system(rmBuffer);
1453 strcat(parseBuffer, cnf_file);
1454 
1455 //printf("\n command : %s",parseBuffer);
1456 
1457 satStatus = system(parseBuffer);
1458 
1459 if(!(fp = fopen(resBuffer, "r"))) {
1460   fprintf(vis_stdout, "%s ERROR : Can't open result file %s\n");
1461   exit(0);
1462 }
1463
1464 fgets(line, 16384, fp);
1465 free(cnf_file);
1466// WriteIDL__rel_sat(filename);
1467 return line;
1468 
1469}
1470
1471//char *
1472void
1473WriteIDL__rel_sat(char *filename) {
1474  mdd_manager* mgr; 
1475  Formula_t    Form;
1476  mdd_t* var;
1477  FILE *fin;
1478  char line[16384], word[1024], *lp;
1479  int  nArg,V=1,index;
1480  int i, id, sign;
1481  long v;
1482  st_table*  hashTable = 
1483    st_init_table(st_ptrcmp, st_ptrhash);
1484  mdd_t* zero;
1485  char* parseBuffer=(char*)calloc(1024,sizeof(char));
1486
1487  if(!(fin = fopen(filename, "r"))) {
1488    fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n");
1489    exit(0);
1490  }
1491
1492  strcpy(parseBuffer,filename);
1493  strcat(parseBuffer, "sat");
1494  char            *filenamecnf ="./tmp.vis.idl";
1495  FILE            *cnf_file; 
1496
1497  if(!(cnf_file = fopen(filenamecnf, "w"))) {
1498    fprintf(vis_stdout, "%s ERROR : Can't open CNF file %s\n");
1499    exit(0);
1500  }
1501
1502  while(fgets(line, 16384, fin)) {
1503
1504    lp = sat_RemoveSpace(line);
1505
1506    if(lp[0] == '\n')   continue;
1507    if(lp[0] == '#')    continue;
1508    if(lp[0] == 'c')    continue;
1509
1510    if(lp[0] == 'p') {
1511           
1512      nArg = sscanf(line, "p cnf %d %d", &nVar, &nCl);
1513     
1514      if(nArg < 2) {
1515        fprintf(vis_stdout,"ERROR : Unable to read the number of ");
1516        fprintf(vis_stdout,"variables and clauses from CNF file %s\n");
1517        fclose(fin);
1518        exit(0);
1519      }
1520
1521       continue;
1522    }
1523
1524    int k=0;
1525    while(1) { 
1526      lp = sat_RemoveSpace(lp);
1527      lp = sat_CopyWord(lp, word);
1528     
1529      if(strlen(word)) {
1530        id = atoi(word);
1531        sign = 1;
1532
1533        if(id != 0) {
1534
1535          if(id < 0) {
1536            id = -id;
1537            sign = 0;
1538          }
1539
1540          id <<=3;
1541         
1542          if(!st_lookup_int(hashTable,(char *)id,&index)) {
1543            st_insert(hashTable, (char*)id,(char*) V);
1544            index=V; V++; 
1545          }
1546         
1547          if(!sign){
1548            if(!k)
1549              fprintf(cnf_file, "-1*x%d ", index); 
1550            else 
1551              fprintf(cnf_file, " -1*x%d ", index); 
1552          }
1553          else{
1554             if(!k)
1555              fprintf(cnf_file, "+1*x%d ", index); 
1556            else 
1557              fprintf(cnf_file, " +1*x%d ", index); 
1558             
1559          }
1560        }
1561        else {
1562          fprintf(cnf_file, ">= +1;\n"); break;
1563        }
1564      }
1565      k++;
1566    } 
1567  }
1568 
1569  st_free_table(hashTable);
1570  fclose(fin);
1571  fclose(cnf_file);
1572
1573  // char* Buffer=(char*)calloc(1024,sizeof(char));
1574 
1575  //strcpy(Buffer,"cp ./tmp.vis.idl ");
1576  // strcat(Buffer, parseBuffer);
1577  // system(Buffer);
1578  //  system("rm -f ./tmp.vis.cl");
1579  // return parseBuffer;
1580}
Note: See TracBrowser for help on using the repository browser.