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

/**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 <stdlib.h>
#include <pthread.h>
#include <unistd.h>
#include <sys/sysinfo.h>
#include <sys/wait.h> 
#include<time.h>

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;i<size;i++){
        if(vs[i]){
          mdd_t* v1=bdd_var_with_index(mgr,i);
          mdd_t* p=mdd_and(v1,l,1,1);
          mdd_free(v1);

          mdd_t* v=bdd_var_with_index(nmgr,vars[i]);
          int sign=(mdd_equal(p,zero)) ? 0:1;
          mdd_t* tmp= clause;
          mdd_t* tmp1= V;
          clause=mdd_and(clause,v,1,sign);
          V=mdd_and(V,v,1,1);
          
          mdd_free(tmp1);
          mdd_free(tmp);
          mdd_free(p);
          mdd_free(v);
        }
      }
      (void)lsNewEnd(f->F,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;i<size;i++){
        if(vs[i]){
          mdd_t* v=bdd_var_with_index(nmgr,vars[i]);
          mdd_t* tmp=R;
          R=mdd_and(R,v,1,1);
          mdd_free(tmp);
          mdd_free(v);
        }
      }
      free(vs);
      free(vars);
      f->R=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<nbvar;++i){
    mdd_t* v=bdd_var_with_index(mgr,i);
    mdd_t* c=_k_clause(Form, k);
    if (!mdd_equal(c, zero) &&
        (s=_d(Form,v))> 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;i<nbvar;++i){
    if(vars[i]){
      mdd_t* v=bdd_var_with_index(mgr,i);
      if (_d(Form,v)==k){
        mdd_t* s=Get_support(mgr,clause);
        mdd_t* r=bdd_smooth_with_cube(s,v);
        mdd_free(v);
        mdd_free(s);
        return r;
      }
      mdd_free(v);
    }
  }
  return mdd_zero(mgr); 
}

mdd_t*
pick_2_clause_w(Formula_t Form, mdd_t* clause){
  int * vars=NULL;
  mdd_manager* mgr =Form->mgr;
  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<nbvar;++i){
    if (vars[i]){
      mdd_t* v  =bdd_var_with_index(mgr,i);
      mdd_t* nhb=get_neighbour(Form, v,&deg);
      if(deg> 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;i<nbvar;++i){
    if (vars[i]){
      mdd_t* v=bdd_var_with_index(mgr,i);
      if(_d(Form,v)== k) {
        mdd_t* nhb=get_neighbour(Form, v,&deg);
        r=get_max_degree_(Form, nhb);
        mdd_free(v);
        mdd_free(nhb);
        return r;
      }
    }  
  }  
  return mdd_zero(mgr);
}


mdd_t*
pick_clause_w(Formula_t Form){
  int * vars=NULL;
  mdd_manager* mgr =Form->mgr;
  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<nbvar;++i){
    if(vars[i]){
      mdd_t* v=bdd_var_with_index(mgr,i);
      mdd_t* t=get_neighbour(Form,v,&deg);
      if(deg > 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;i<nbvar && var_size;++i){
      if(vars[i] && t==1){ 
        v1=bdd_var_with_index(mgr,i);
        var_size --;
        if(var_size != 0)
          t=2;
        else{
          mdd_t* tmp1=res;
          res=mdd_and(res,v1,1,1);
          mdd_free(tmp1);
        }
      }

      if(vars[i] && t==2){ 
        var_size --;
        v2=bdd_var_with_index(mgr,i);
        res=convert_dnf_cnf(Form,v1,v2,res); 
        t=1;
      } 
   
    } 
    free(vars);
    mdd_free(tmp);
    tmp=res;
  }while(Cudd_SupportSize((DdManager *)mgr,res->node) > 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;
}