#ifndef _msol_hpp_
#define _msol_hpp_

#include <ostream>
#include <iostream>
#include <exception>
#include <set>
#include <vector>
using namespace std;

struct exception_msol_t : public exception {
  string s;

  virtual ~exception_msol_t() throw() {}
  
  exception_msol_t(string &s_) throw() :s(s_) {
  }

  exception_msol_t(char *s_) throw() :s(s_) {
  }

  virtual const char* what() const throw() {
    return s.c_str();
  }
};


#define KMAX 4
#define ARMAX 2
#define RMAX (4+KMAX)

#define TEX 1

//0 devrait etre bon...
#define FREEVAR 10

// relation 0 = F
// relation 1 = T
// relation 2 = =
// relation 3 = E
// relation 4..4+k-1 = P


//struct voc_t {

int nr; // nbr rel
int nc; // nbr constante
int ar[RMAX]; // arité

void initvoc() {
  nr=RMAX;
  nc=0;
  ar[0]=0;
  ar[1]=0;
  ar[2]=2;
  ar[3]=2;
  for(int i=4;i<RMAX;i++) ar[i]=1;
}

bool isrelation(int r) { return r>=0 && r<=nr;}
int arrelation(int r) { 
  if(r>=0 && r<=nr) return ar[r];
  else throw exception_msol_t("arrelation");
}
bool isconstant(int r) { return r>=0 && r<=nc;}

//int freefirst();
//int freesecond();

//};


////////////////////////////

struct form_t {
  virtual ~form_t() {}
  virtual form_t *copy() const=0;
  virtual ostream &affiche(ostream &) const=0;

  form_t() {}
  form_t(const form_t &) { throw exception_msol_t("form_t()");}
  const form_t &operator=(const form_t &){ throw exception_msol_t("form_t =");}
  
  friend ostream &operator<<(ostream &o, const form_t &a) { 
    return a.affiche(o);
  }
};

struct boolatom_t : public form_t{
  int i;

  boolatom_t(int j=0):i(j) {}

  boolatom_t(const boolatom_t &) { throw exception_msol_t("boolatom_t()");}


  form_t *copy() const {
    boolatom_t *ba=new boolatom_t();
    ba->i=i;
    return ba;
  }

  ostream &affiche(ostream &o) const {
    o<<i;
    return o;
  }
};

struct atom_t : public form_t {
  int r; // la relation 
  int ar;
  // si r<0 : variable du second ordre, ar=1
  // sinon ar= voc.ar[r]; 
  int var[ARMAX];

  ~atom_t() {}

  atom_t(int rr=0,int v1=0,int v2=0):r(rr),ar(::ar[rr]) {
    if(isrelation(rr)) ar=arrelation(rr);
    else ar=1;
    if(ar>0) var[0]=v1;
    if(ar>1) var[1]=v2;
  }

  atom_t(const atom_t &) { throw exception_msol_t("atom_t()");}
  
  form_t *copy() const {
    atom_t *a=new atom_t();
    a->r=r;
    a->ar=ar;
    for(int i=0;i<ar;i++)
      a->var[i]=var[i];
    return a;
  }


  static string lalav(int i) {
    if(i==42) return "u";
    if(i==43) return "v";
    return "x_" + i;
  }

#if TEX
  ostream &affiche(ostream &o) const {
    if(isrelation(r)) {
      if(r==0) o<<"\\operatoname{False}";
      if(r==1) o<<"\\operatorname{True}";
      if(r==2) o<< lalav(var[0]) << "=" << lalav(var[1]);
      if(r==3) o<< "\\adju(" << lalav(var[0]) << "," << lalav(var[1]) << ")";
      if(r>=4) o<< "P_" << r-4 << "(" << lalav(var[0]) << ")";
      return o;
    }
    if(r==79)  
      o<<"X" << "(" << lalav(var[0]) << ")";
    else
      o<<"X_" << r << "(" << var[0] << ")";
    return o;
  }
#else
  ostream &affiche(ostream &o) const {
    if(isrelation(r)) {
      if(r==0) o<<"False";
      if(r==1) o<<"True";
      if(r==2) o<< (var[0]) << "=" << var[1];
      if(r==3) o<< "Adj(" << (var[0]) << "," << (var[1]) << ")";
      if(r>=4) o<< "P_" << r-4 << "(" << (var[0]) << ")";
      return o;
    }
    o<<"X_" << r << "(" << var[0] << ")";
    return o;
  }
#endif
};

struct boolform_t : public form_t {
  int type; // 0:neg 1:and 2:or
  form_t *e1,*e2;

  boolform_t():type(0),e1(NULL),e2(NULL) {}
  ~boolform_t() {
    //cout << "delete boolfrom " << *this << "\n";
    if(e1) delete e1; 
    if(e2) delete e2;
  }
  boolform_t(int t,form_t *e1_,form_t *e2_=NULL):type(t),e1(e1_),e2(e2_) {}
  
  boolform_t(const boolform_t &) { throw exception_msol_t("boolform_t()");}

  const boolform_t &operator=(const boolform_t &){ throw exception_msol_t("boolform_t =");}
 
  form_t *copy() const {
    boolform_t *a=new boolform_t();
    a->type=type;
    a->e1=e1->copy();
    if(type)
      a->e2=e2->copy();
    return a;
  }

#if TEX
  ostream &affiche(ostream &o) const {
    if(type==0) {
      o<<"\\neg (";e1->affiche(o); o<<")";
    } else if(type==1) {
      o<<"(";e1->affiche(o); o<<" \\and "; e2->affiche(o);o<<")";
    } else if(type==2) {
      o<<"(";e1->affiche(o); o<<" \\oor "; e2->affiche(o);o<<")";
    } else o<<"ERROR";

    return o;
  }
#else
  ostream &affiche(ostream &o) const {
    if(type==0) {
      o<<"!(";e1->affiche(o); o<<")";
    } else if(type==1) {
      o<<"(";e1->affiche(o); o<<"&"; e2->affiche(o);o<<")";
    } else if(type==2) {
      o<<"(";e1->affiche(o); o<<"|"; e2->affiche(o);o<<")";
    } else o<<"ERROR";

    return o;
  }
#endif

};

struct quant_t : public form_t {
  int forall;
  bool first;
  form_t *e1;
  int v;
  
  quant_t():e1(NULL) {}
  quant_t(bool fa,bool f, int x, form_t *e):forall(fa),first(f),e1(e),v(x) {}
  ~quant_t() {
    //cout << "delete quant " << *this << "\n";
    if(e1) delete e1;
  }
  quant_t(const quant_t &) { throw exception_msol_t("quantform_t()");}

  const quant_t &operator=(const quant_t &){ throw exception_msol_t("quant_t =");}
  
  form_t *copy() const {
    quant_t *a=new quant_t();
    a->e1=e1->copy();
    a->first=first;
    a->forall=forall;
    a->v=v;
    return a;
  }

#if TEX
  ostream &affiche(ostream &o) const {
    string str;
    if(first) {
      if(v==42) str= "u"; 
      else if(v==43) str= "v"; 
      else 
      str= " " + v;
    } else {
      if(v==79) str="X";
      else str= "X_" + v;
    }
    o<<"(" << (forall?"\\forall ":"\\exists ") << str << ",";e1->affiche(o);o<<")";
    return o;
  }
#else
  ostream &affiche(ostream &o) const {
    if(first) {
      o<<"(" << (forall?"F":"E") << " "<<v<<",";e1->affiche(o);o<<")";
    } else {
      o<<"(" << (forall?"F":"E") << " X_"<<v<<",";e1->affiche(o);o<<")";
    }
    return o;
  }
#endif
};

////////////////////////////

//rename

bool verify(form_t *f)
{
  atom_t *a=dynamic_cast<atom_t*>(f);
  if(a) {
    if(!(isrelation(a->r))) {
      if(a->ar!=1) return false;
      else return true;
    } else
      if(a->ar != arrelation(a->r))  return false;
    
    return true;
  }
  
  quant_t *q=dynamic_cast<quant_t*>(f);
  if(q) {
    if(q->first) {
      if(isconstant(q->v)) return false;
    } else {
      if(isrelation(q->v)) return false;
    }
    return true;
  }

  boolform_t *b=dynamic_cast<boolform_t*>(f);
  if(b) {
    if(!verify(b->e1)) return false;
    if( b->type && ! verify(b->e2)) return false;
    return true;
  }
  
  throw exception_msol_t("verify");
}

void libre(form_t *f,set<int> &first, set<int> &second)
{
  atom_t *a=dynamic_cast<atom_t*>(f);
  if(a) {
    first.clear();
    second.clear();
    if(!(isrelation(a->r))) second.insert(a->r);
    for(int i=0;i<a->ar;i++) {
      if(!isconstant(a->var[i])) first.insert(a->var[i]);
    }
    
    return;
  }
  
  quant_t *q=dynamic_cast<quant_t*>(f);
  if(q) {
    libre(q->e1,first,second);
    if(q->first) first.erase(q->v);
    else second.erase(q->v);
    return;
  }

  boolform_t *b=dynamic_cast<boolform_t*>(f);
  if(b) {
    libre(b->e1,first,second);
    if(b->type) {
      set<int> f,s;
      libre(b->e2,f,s);
      
      set<int>::iterator it;
      for(it=f.begin();it!=f.end();++it)
	first.insert(*it);
      for(it=s.begin();it!=s.end();++it)
	second.insert(*it);
    }
    return;
  }

  throw exception_msol_t("libre");
}

void rename(form_t *f, int si, int tab[][2], int si2, int tab2[][2])
{
  atom_t *a=dynamic_cast<atom_t*>(f);
  if(a) {
    int i,j;
    // relation
    for(j=0;j<si2;j++)
      if(a->r==tab2[j][0]) {a->r=tab2[j][1];break;}
    //variables
    for(i=0;i<a->ar;i++) {
      for(j=0;j<si;j++)
	if(a->var[i]==tab[j][0]) {a->var[i]=tab[j][1];break;}
    }
    return;
  }
  
  quant_t *q=dynamic_cast<quant_t*>(f);
  if(q) {
    if(q->first) {
      int v=q->v;
      int j;
      for(j=0;j<si;j++)
	if(tab[j][0]==v) break;
      if(j!=si) {
	tab[j][0]=-1;
	rename(f,si,tab,si2,tab2);
	tab[j][0]=v;
      }
      else rename(q->e1,si,tab,si2,tab2);
    } else { // second ordre
      int r=q->v;
      int j;
      for(j=0;j<si2;j++)
	if(tab2[j][0]==r) break;
      if(j!=si2) {
	tab2[j][0]=-1;
	rename(f,si,tab,si2,tab2);
	tab2[j][0]=r;
      }
      else rename(q->e1,si,tab,si2,tab2);
    } 
    return;
  }
  
  boolform_t *b=dynamic_cast<boolform_t*>(f);
  if(b) {
    rename(b->e1,si,tab,si2,tab2);
    if(b->type) {
      rename(b->e2,si,tab,si2,tab2);
    }
    return;
  }

  cout << typeid(*f).name() << endl;

  throw exception_msol_t("rename");
}

struct transduction_t {

  transduction_t() {for(int i=0;i<RMAX;i++) tab[i]=NULL;}
  ~transduction_t() {for(int i=0;i<RMAX;i++) if(tab[i]) delete tab[i];}
  
  form_t *tab[RMAX];// null si change pas
  int tr[RMAX][ARMAX]; // var libres des formules
};

// calcul la transduction t de f
form_t *transduct(form_t *f, transduction_t &t)
{
  atom_t *a=dynamic_cast<atom_t*>(f);
  if(a) {
    if(isrelation(a->r)) {
      if(t.tab[a->r]) {
	int tr2[1][2];
	int tr[a->ar][2];
	for(int j=0;j<a->ar;j++) {
	  tr[j][0]=t.tr[a->r][j];
	  tr[j][1]=a->var[j];
	}
	form_t *lala=t.tab[a->r]->copy();
	rename(lala,a->ar,tr,0,tr2);
	return lala;
      }
    } 
    return f->copy();
  }
  
  quant_t *q=dynamic_cast<quant_t*>(f);
  if(q) {
    quant_t *q_=new quant_t();
    q_->forall=q->forall;
    q_->v=q->v;
    q_->first=q->first;
    q_->e1=transduct(q->e1,t);
    
    return q_;
  }

  boolform_t *b=dynamic_cast<boolform_t*>(f);
  if(b) {
    boolform_t *b_=new boolform_t();
    b_->type=b->type;
    b_->e1=transduct(b->e1,t);
    if(b->type) {
      b_->e2=transduct(b->e2,t);
    }
    return b_;
  }
  
  throw exception_msol_t("trans");
}

form_t *extractbool(form_t *f,vector<form_t*> &tab)
{
  atom_t *a=dynamic_cast<atom_t*>(f);
  if(a) {
    int i=tab.size();
    tab.resize(i+1);
    tab[i]=a->copy();
    
    return new boolatom_t(i);;
  }
  
  quant_t *q=dynamic_cast<quant_t*>(f);
  if(q) {
    int i=tab.size();
    tab.resize(i+1);
    tab[i]=q->copy();
    
    return new boolatom_t(i);;
  }

  boolform_t *b=dynamic_cast<boolform_t*>(f);
  if(b) {
    boolform_t *f;
    form_t *e1=extractbool(b->e1,tab),*e2=NULL;
    if(b->type) e2=extractbool(b->e2,tab);
    if(b->type)
      f=new boolform_t(b->type,e1,e2);
    else
      f=new boolform_t(0,e1);
    return f;
  }
  
  throw exception_msol_t("extractbool");
}

void renamebool(form_t *f, int t[])
{
  
  /*
  boolatom2_t *a=dynamic_cast<boolatom2_t*>(f);
  if(a) {
    a->i=t[a->i];
    return;
  }
  */

  atom_t *a_=dynamic_cast<atom_t*>(f);
  if(a_) {
    //suppose true ou false
    return;
  }

  boolatom_t *a=dynamic_cast<boolatom_t*>(f);
  if(a) {
    a->i=t[a->i];
    return;
  }


  boolform_t *b=dynamic_cast<boolform_t*>(f);
  if(b) {
    renamebool(b->e1,t);
    if(b->type) renamebool(b->e2,t);
    return;
  }
  
  cout << typeid(*f).name() << endl;
  throw exception_msol_t("renamebool");
}

bool evalbool(form_t *f,bool t[])
{
  boolatom_t *a=dynamic_cast<boolatom_t*>(f);
  if(a) {
    return t[a->i];
  }

  /*
  boolatom2_t *a2=dynamic_cast<boolatom2_t*>(f);
  if(a2) {
    return t[a2->i];
  }
  */

  boolform_t *b=dynamic_cast<boolform_t*>(f);
  if(b) {
    bool r1=evalbool(b->e1,t);
    if(b->type==0) return !r1;
    if(b->type==1) if(r1) return evalbool(b->e2,t); else return false;
    if(b->type==2) if(!r1) return evalbool(b->e2,t); else return true;
  }
  
  throw exception_msol_t("evalbool");
}

bool inctab(bool t[], int nv)
{
  int i=0;
  do {
    if(t[i]==false) {t[i]=true;return true;}
    else {t[i]=false; i++;}
  } while(i<nv);
  return false;
}

bool equivbool(form_t *f1,form_t *f2,int nv)
{
  //a faire !!! quoi a faire ?
  bool t[nv];
  int i;
  for(i=0;i<nv;i++)
    t[i]=false;

  do {
    if(evalbool(f1,t) != evalbool(f2,t)) return false;
    //printf("lala\n");
  } while(inctab(t,nv));
  return true;
}

form_t *newtrue() { return new atom_t(1);}
form_t *newfalse() { return new atom_t(0);}

bool istrue(form_t *f) {
  atom_t *a=dynamic_cast<atom_t*>(f);
  if(a && a->r==1) return true;
  return false;
}

bool isfalse(form_t *f) {
  atom_t *a=dynamic_cast<atom_t*>(f);
  if(a && a->r==0) return true;
  return false;
}

/*
form_t *deltruefalse_(form_t *f);
form_t *deltruefalse(form_t *f)
{
  cout << ">>> delTF " << *f << endl;
  form_t *r=deltruefalse_(f);
  cout << "<<< delTF " << *f << " " <<*r << endl;
  return r;
}
*/

form_t *deltruefalse(form_t *f)
{

  atom_t *a=dynamic_cast<atom_t*>(f);
  if(a) {
    return a->copy();
  }

  boolatom_t *a_=dynamic_cast<boolatom_t*>(f);
  if(a_) {
    return a_->copy();
  }

  quant_t *q=dynamic_cast<quant_t*>(f);
  if(q) {
    form_t *e1=deltruefalse(q->e1);
    if(istrue(e1)) {delete e1; return newtrue();}
    if(isfalse(e1)) {delete e1; return newfalse();}
    return new quant_t(q->forall,q->first,q->v,e1);
  }

  boolform_t *b=dynamic_cast<boolform_t*>(f);
  if(b) {
    form_t *e1=deltruefalse(b->e1),*e2=NULL;
    if(b->type) e2=deltruefalse(b->e2);
    if(b->type==0) {
      if(istrue(e1)) {delete e1; return newfalse();}
      if(isfalse(e1)) {delete e1; return newtrue();}
      return new boolform_t(0,e1);
    }
    if(b->type==1) {
      if(istrue(e1)) {delete e1; return e2;}
      if(istrue(e2)) {delete e2; return e1;}
      if(isfalse(e1)) {delete e1; delete e2; return newfalse();}
      if(isfalse(e2)) {delete e1; delete e2; return newfalse();}
      return new boolform_t(b->type,e1,e2);
    }
    if(b->type==2) {
      if(isfalse(e1)) {delete e1; return e2;}
      if(isfalse(e2)) {delete e2; return e1;}
      if(istrue(e1)) {delete e1; delete e2; return newtrue();}
      if(istrue(e2)) {delete e1; delete e2; return newtrue();}
      return new boolform_t(b->type,e1,e2);
    }
  }

  cout << typeid(*f).name() << endl;  
  throw exception_msol_t("deltruefalse");
}

//renvoie  vrai si elles sont equivalentes par \approx
bool equiv_(form_t *f1, form_t *f2) {
  {
    quant_t *q1=dynamic_cast<quant_t*>(f1);
    quant_t *q2=dynamic_cast<quant_t*>(f2);

    atom_t *a1=dynamic_cast<atom_t*>(f1);
    atom_t *a2=dynamic_cast<atom_t*>(f2);

    if(q1 && q2) {
      if(q1->first && !q2->first) return false;
      if(q2->first && !q1->first) return false;
      if(q1->forall && ! q2->forall) return false;
      if(q2->forall && ! q1->forall) return false;

      // faut faire rename (c'est fait ????)
      form_t *lala=q2->e1->copy();
      int tr[1][2];
      int tr2[1][2];
      tr[0][0]=q2->v;
      tr[0][1]=q1->v;
      if(q1->first) {
	rename(lala,1,tr,0,tr2);
      } else {
	rename(lala,0,tr2,1,tr);
      }

      bool res=equiv_(q1->e1,lala);

      delete lala;
      return res;
    }
    
    if(a1 && a2) {
      if(a1->r!=a2->r) return false;
      if(a1->ar==0) return true;
      if(a1->ar==1) return a1->var[0]==a2->var[0];
      if(a1->ar==2) return 
		      (a1->var[0]==a2->var[0] && a1->var[1]==a2->var[1] ) ||
		      (a1->var[0]==a2->var[1] && a1->var[1]==a2->var[0] );
      
    }

    if(a1 && q2) return false;
    if(a2 && q1) return false;
  }

  vector<form_t*> tab;
  form_t *bf1=extractbool(f1, tab);
  form_t *bf2=extractbool(f2, tab);

  int tabe[tab.size()];
  unsigned int i,j;
  for(i=0;i<tab.size();i++)
    tabe[i]=-1;
  
  for(i=0;i<tab.size();i++) {
    if(!tab[i]) throw exception_msol_t("equiv: tab[i]==NULL");
    for(j=0;j<i;j++) {
      if(tab[j])
	if(equiv_(tab[i],tab[j])) {
	  delete tab[i];tab[i]=NULL;
	  tabe[i]=j;
	  goto skipequiv;
	}
    }
  skipequiv:;
  }

  j=0;
  for(i=0;i<tab.size();i++)
    if(tabe[i]==-1) tabe[i]=j++;
    else tabe[i]=tabe[tabe[i]];
  
  renamebool(bf1,tabe);
  renamebool(bf2,tabe);

  for(i=0;i<tab.size();i++)
    if(tab[i]) delete tab[i];

  bool r=equivbool(bf1,bf2,j);

  delete bf1;
  delete bf2;

  return r;
}

bool equiv(form_t *f1,form_t *f2) 
{
  form_t *f1_,*f2_;
  f1_=deltruefalse(f1);
  f2_=deltruefalse(f2);
  return equiv_(f1_,f2_);
}

#if 1

//#define ORN(a,b) if((a)==NULL) (a)=(b)->copy(); else (a)=new boolform_t(2,(a),(b)->copy());
void ORN(form_t *&a,form_t *b,bool pos=true) 
{
  if(pos)
    if(a==NULL)
      a=b->copy(); 
    else {
      form_t *aa=new boolform_t(2,a,b->copy());
      a=aa;
    }
  else
    if(a==NULL)
      a=new boolform_t(0,b->copy()); 
    else {
      form_t *aa=new boolform_t(2,a,new boolform_t(0,b->copy()));
      a=aa;
    }
}

void ANDN(form_t *&a,form_t *b,bool pos=true) 
{
  if(pos)
    if(a==NULL)
      a=b->copy(); 
    else {
      form_t *aa=new boolform_t(1,a,b->copy());
    a=aa;
    }
  else
    if(a==NULL)
      a=new boolform_t(0,b->copy()); 
    else {
      form_t *aa=new boolform_t(1,a,new boolform_t(0,b->copy()));
    a=aa;
    }
}

struct boolatom2_t : public boolatom_t {
  boolatom2_t(int ii,int jj):boolatom_t(ii),j(jj) {}
  //int i;
  int j;

  form_t *copy() const {
    boolatom2_t *ba=new boolatom2_t(i,j);
    return ba;
  }

  ostream &affiche(ostream &o) const {
    o<< i << "_" << j;
    return o;
  }

};

struct lit_t{
  int i;
  bool pos;
  int j;
};

typedef vector<lit_t> clause_t;

/*
struct clause_t {
  vector<lit_t> v;
};
*/

void negnf(vector<clause_t> &nf)
{
  for(unsigned int i=0;i<nf.size();i++)
    for(unsigned int j=0;j<nf[i].size();j++)
      nf[i][j].pos=!nf[i][j].pos;
}

const ostream &nfaff(vector<clause_t> &nf, ostream &o) 
{
  unsigned int i,j;
  for(i=0;i<nf.size();i++) {
    o << "(";
    for(j=0;j<nf[i].size();j++) {
      if(j) o << ",";
      if(nf[i][j].pos==false) o<< "!";
      o << nf[i][j].i << "_" << nf[i][j].j;
    }
    o << ") ";
  }
  o << endl;
  return o;
}


#if 0

void trouvej(form_t *f, vector<int> &t)
{
  boolatom2_t *a=dynamic_cast<boolatom2_t*>(f);
  if(a) {
    t[a->i]=a->j;
    return;
  }

  boolform_t *b=dynamic_cast<boolform_t*>(f);
  if(b) {
    trouvej(b->e1,t);
    if(b->type)
      trouvej(b->e2,t); 
    return;
  }

  throw exception_msol_t("trouvej");
}

// tres mauvais !!!!! : temps et espace en 2^nv
// utiliser karnaugh ?
void DNF(form_t *f,vector<clause_t> &dnf,int nv)
{
  bool t[nv];
  int i;

  if(dnf.size())
    throw exception_msol_t("DNF dnf.size!=0");  

  std::cout << "DNF: nv="<<nv << " f="  << *f << endl;

  vector<int> tj;
  tj.resize(nv);
  for(i=0;i<nv;i++) tj[i]=-1;

  trouvej(f,tj);

  for(i=0;i<nv;i++)
    t[i]=false;

  do {
    if(evalbool(f,t)==true) {
      clause_t cl;
      cl.resize(nv);

      for(i=0;i<nv;i++) {
	cl[i].i=i;
	cl[i].j=tj[i];
	if(tj[i]==-1) { 
	  //cout << *f << endl;
	  cout << i << endl;
	  throw exception_msol_t("DNF trouvej ");  
	}
	cl[i].pos=t[i];
      }

      dnf.resize(dnf.size()+1);
      dnf[dnf.size()-1]=cl;
      //cout << dnf.size()-1 << endl;
    }
  } while(inctab(t,nv));

  std::cout << "DNF END" << endl;
  
  return;
}


void CNF(form_t *f,vector<clause_t> &cnf,int nv)
{
  form_t *ff=new boolform_t(0,f->copy());

  DNF(ff,cnf,nv);
  negnf(cnf);
  
  delete ff;
}

#endif

void NF(boolatom2_t *f, vector<clause_t> &nf)
{
  nf.resize(1);
  nf[0].resize(1);
  nf[0][0].i=f->i;
  nf[0][0].j=f->j;
  nf[0][0].pos=true;
}

void clconcat(const clause_t &a, const clause_t &b, clause_t &c)
{
  c.resize(a.size()+b.size());
  unsigned int i,s=a.size();
  for(i=0;i<a.size();i++)
    c[i]=a[i];
  for(i=0;i<b.size();i++)
    c[i+s]=b[i];
}

void CNF_2(form_t *f, vector<clause_t> &nf,int =0);

void DNF_2(form_t *f, vector<clause_t> &nf,int =0)
{
  nf.resize(0); // normalement inutile;

  if(isfalse(f)) {nf.resize(0);return;}
  if(istrue(f)) {nf.resize(1);nf[0].resize(0);return;}

  boolatom2_t *a=dynamic_cast<boolatom2_t*>(f);
  if(a) {
    NF(a,nf);
    return;
  }
  
  boolform_t *b=dynamic_cast<boolform_t*>(f);
  if(b) {
    if(b->type==2) { // ou: cas facile
      vector<clause_t> t1;
      DNF_2(b->e1,nf);
      DNF_2(b->e2,t1);
      for(unsigned int i=0;i<t1.size();i++) 
	nf.push_back(t1[i]);
      return;
    }

    if(b->type==1) { // et
      unsigned int i,j;
      vector<clause_t> t1,t2;
      DNF_2(b->e1,t1);
      DNF_2(b->e2,t2);
      
      nf.resize(t1.size()*t2.size());
      for(i=0;i<t1.size();i++) 
	for(j=0;j<t2.size();j++) 
	  clconcat(t1[i],t2[j],nf[j*t1.size()+i]);
      return;
    }

    if(b->type==0) {
      CNF_2(b->e1,nf);
      negnf(nf);
      return;
    }

  }  

  throw exception_msol_t("DNF2");
}

void CNF_2(form_t *f, vector<clause_t> &nf,int)
{
  nf.resize(0); // normalement inutile;

  if(istrue(f)) {nf.resize(0);return;}
  if(isfalse(f)) {nf.resize(1);nf[0].resize(0);return;}

  boolatom2_t *a=dynamic_cast<boolatom2_t*>(f);
  if(a) {
    NF(a,nf);
    return;
  }
  
  boolform_t *b=dynamic_cast<boolform_t*>(f);
  if(b) {
    if(b->type==1) { // et: cas facile
      vector<clause_t> t1;
      CNF_2(b->e1,nf);
      CNF_2(b->e2,t1);
      for(unsigned int i=0;i<t1.size();i++) 
	nf.push_back(t1[i]);
      return;
    }

    if(b->type==2) { // ou
      unsigned int i,j;
      vector<clause_t> t1,t2;
      CNF_2(b->e1,t1);
      CNF_2(b->e2,t2);
      
      nf.resize(t1.size()*t2.size());
      for(i=0;i<t1.size();i++) 
	for(j=0;j<t2.size();j++) 
	  clconcat(t1[i],t2[j],nf[j*t1.size()+i]);
      return;
    }

    if(b->type==0) {
      DNF_2(b->e1,nf);
      negnf(nf);
      return;
    }

  }  

  cout << typeid(*f).name() << endl;
  throw exception_msol_t("CNF2");
}

///////////

void decale(form_t *f,int d)
{
  boolatom2_t *a=dynamic_cast<boolatom2_t*>(f);
  if(a) {
    a->i+=d;
    return;
  }

  boolform_t *b=dynamic_cast<boolform_t*>(f);
  if(b) {
    decale(b->e1,d);
    if(b->type) decale(b->e2,d);
    return;
  }

  cout << typeid(*f).name() << endl;
  throw exception_msol_t("decale");
}

/*
bool in(const set<int> &s,const int &i)
{
  set<int>::const_iterator it;
  it=s.find(i);
  return it!=s.end();
}
*/

form_t *fovout(form_t *f, int v)
{
  atom_t *a=dynamic_cast<atom_t*>(f);
  if(a) {
    int i;
    for(i=0;i<a->ar;i++)
      if(a->var[i]==v) return newfalse();
    
    return a->copy();
  }

  boolform_t *b=dynamic_cast<boolform_t*>(f);
  if(b) {
    int type=b->type;

    form_t *f1=fovout(b->e1,v),*f2=NULL;
    if(type) {
      f2=fovout(b->e2,v);
    }
    return new boolform_t(type,f1,f2);
  }
  
  quant_t *q=dynamic_cast<quant_t*>(f);
  if(q) {
    if(q->first==true && v==q->v) {
      //v est masqué
      return q->copy();
    }

    form_t *f1=fovout(q->e1,v);
    
    return new quant_t(q->forall,q->first,q->v,f1);
  }

  throw exception_msol_t("fovout");
}

form_t *newconj2(int i)
{
  return new boolform_t(1,new boolatom2_t(i*2,0),new boolatom2_t(i*2+1,1));
}

form_t *newdisj2(int i)
{
  return new boolform_t(2,new boolatom2_t(i*2,0),new boolatom2_t(i*2+1,1));
}

form_t *newdisjonctionconj2(int i)
{
  form_t *f=NULL;
  for(int j=0;j<i;j++) {
    form_t *ff=newconj2(j);
    ORN(f,ff);
    delete ff;
  }

  if(f==NULL) return newfalse();
  return f;
}

form_t *newconjonctiondisj2(int i)
{
  form_t *f=NULL;
  for(int j=0;j<i;j++) {
    form_t *ff=newdisj2(j);
    ANDN(f,ff);
    delete ff;
  }

  if(f==NULL) return newtrue();
  return f;
}

form_t *replacebool(form_t *f, int i, form_t *r)
{
  atom_t *a_=dynamic_cast<atom_t*>(f);
  if(a_) {
    // suppose que c'est true ou false
    return a_->copy();
  }

  boolatom2_t *a=dynamic_cast<boolatom2_t*>(f);
  if(a) {
    if(a->i==i) return r->copy();
    else return a->copy();
  }

  boolform_t *b=dynamic_cast<boolform_t*>(f);
  if(b) {
    if(b->type==0) return new boolform_t(0,replacebool(b->e1,i,r));
    else  return new boolform_t(b->type,replacebool(b->e1,i,r),replacebool(b->e2,i,r));
  }

  cout << typeid(*f).name() << endl;
  throw exception_msol_t("replacebool");
}

void used(form_t *f, int tab[])
{
  atom_t *a_=dynamic_cast<atom_t*>(f);
  if(a_) {
    // suppose que c'est true ou false
    return;
  }

  boolatom2_t *a=dynamic_cast<boolatom2_t*>(f);
  if(a) {
    tab[a->i]=1;
    return;
  }

  boolform_t *b=dynamic_cast<boolform_t*>(f);
  if(b) {
    used(b->e1,tab);
    if(b->type) used(b->e2,tab);
    return;
  }
  
  cout << typeid(*f).name() << endl;
  throw exception_msol_t("used");
}

void FVaff(form_t *&B, vector<form_t*> &tab)
{
  cout << *B << endl;

  for(unsigned int i=0;i<tab.size();i++) 
    cout << "tab[" << i << "] = " << *tab[i] << endl;  
}

void FVsimpl(form_t *&B, vector<form_t*> &tab, int pass=1)
{
  unsigned int i;

  //cout << "' ";FVaff(B,tab);

  for(i=0;i<tab.size();i++) {
    form_t *f=deltruefalse(tab[i]);
    delete tab[i];
    tab[i]=f;
  }

  //cout << "- ";  FVaff(B,tab);

  if(!pass) return;

  int tabe[tab.size()];
  unsigned int j;
  for(i=0;i<tab.size();i++)
    tabe[i]=-1;
  
  for(i=0;i<tab.size();i++) {
    if(!tab[i]) throw exception_msol_t("FVsimpl: tab[i]==NULL");
    for(j=0;j<i;j++) {
      if(tab[j])
	if(equiv_(tab[i],tab[j])) {
	  delete tab[i];tab[i]=NULL;
	  tabe[i]=j;
	  goto skipequiv_;
	}
    }
  skipequiv_:;
  }

  j=0;
  for(i=0;i<tab.size();i++) {
    if(tabe[i]==-1) {
      tab[j]=tab[i];
      tabe[i]=j++;
    }
    else tabe[i]=tabe[tabe[i]];
  }

  tab.resize(j);
  
  renamebool(B,tabe);

  //cout << "_ ";  FVaff(B,tab);

  for(i=0;i<tab.size();i++) {
    if(istrue(tab[i])) {
      form_t *tr=newtrue();
      form_t *B_=replacebool(B,i,tr);
      delete tr;
      delete B;
      B=B_;
    }

    if(isfalse(tab[i])) {
      form_t *tr=newfalse();
      form_t *B_=replacebool(B,i,tr);
      delete tr;
      delete B;
      B=B_;
    }
  }

  //cout << "_- "; FVaff(B,tab);


  {
    form_t *B_=deltruefalse(B);
    delete B;
    B=B_;
  }


  //cout << "__ ";  FVaff(B,tab);

  for(i=0;i<tab.size();i++)
    tabe[i]=0;

  used(B,tabe);

  j=0;
  for(i=0;i<tab.size();i++)
    if(tabe[i]==0) {
      delete tab[i];
      tab[i]=NULL;
    }
    else {
      tab[j]=tab[i];
      tabe[i]=j;
      j++;
    }

  tab.resize(j);
  
  renamebool(B,tabe);  

  //cout << "___ ";FVaff(B,tab);
}

void FV_(form_t *f, form_t *&B, vector<form_t*> &tab);

void FV(form_t *f, form_t *&B, vector<form_t*> &tab)
{
  //cout << "FV " << *f << endl;

  FV_(f,B,tab);
  FVsimpl(B,tab);

  //FVaff(B,tab);

  //cout <<"! FV " << *f << endl;
}

void FV_(form_t *f, form_t *&B, vector<form_t*> &tab)
{
  // normalement inutile
  tab.clear();

  // si F atomique
  atom_t *a=dynamic_cast<atom_t*>(f);
  if(a) {
    tab.resize(2);
    tab[0]=a->copy(); //new atom_t(a->r,a->var[0],a->var[1]);
    tab[1]=a->copy(); //new atom_t(a->r,a->var[0],a->var[1]);
    B=new boolform_t(2,new boolatom2_t(0,0),new boolatom2_t(1,1));
    return;
  }

  // si F op bool
  boolform_t *b=dynamic_cast<boolform_t*>(f);
  if(b) {
    int type=b->type;

    form_t *B1,*B2;

    FV(b->e1,B1,tab);
    if(type) {
      vector<form_t*> t2;
      FV(b->e2,B2,t2);
      
      int s=tab.size();
      tab.resize(s+t2.size());
           
      for(unsigned int i=0;i<t2.size();i++) {
	tab[i+s]=t2[i];
      }
      
      decale(B2,s);

      //cout << "decale " << s << "  " << t2.size() << endl;
      //for(unsigned int i=0;i<tab.size();i++)
      //	cout << " - " << *(tab[i]->copy()) << endl;
    }
    
    if(type)
      B=new boolform_t(type,B1,B2);
    else
      B=new boolform_t(0,B1);
    
    return;
  }
  
  // si F quant
  quant_t *q=dynamic_cast<quant_t*>(f);
  if(q) {
    unsigned int i,j;
    int v=q->v;
    if(q->first==true && q->forall==false) {
      form_t *B1;
      vector<clause_t> dnf;
      vector<form_t*> t1,tabt;

      FV(q->e1,B1,t1);

      DNF_2(B1,dnf,t1.size());

      //cout << *B1 << endl;
      //nfaff(dnf,cout);

      //for(i=0;i<t1.size();i++)
      //cout << " = " << *(t1[i]->copy()) << endl;

      delete B1;
      
      tabt.resize(dnf.size()*2);
      tab.resize(dnf.size()*4);

      for(i=0;i<dnf.size();i++) {

	form_t *ft=NULL;
	for(j=0;j<dnf[i].size();j++) {
	  if(dnf[i][j].j==0) {
	    if(dnf[i][j].pos)
	      ANDN(ft,t1[dnf[i][j].i]);
	    else
	      ANDN(ft,t1[dnf[i][j].i],false);
	  }
	}
	
	if(ft==NULL) ft=newtrue();
	tabt[i*2]=ft;

	ft=NULL;
	for(j=0;j<dnf[i].size();j++) {
	  if(dnf[i][j].j==1)
	    if(dnf[i][j].pos)
	      ANDN(ft,t1[dnf[i][j].i]);
	    else
	      ANDN(ft,t1[dnf[i][j].i],false);
	}
	if(ft==NULL) ft=newtrue();
	tabt[i*2+1]=ft;

	tab[i*4]=new quant_t(false,true,v,tabt[i*2]->copy());
	tab[i*4+1]=fovout(tabt[i*2+1],v);
	tab[i*4+2]=fovout(tabt[i*2],v);
	tab[i*4+3]=new quant_t(false,true,v,tabt[i*2+1]->copy());

	delete tabt[i*2];
	delete tabt[i*2+1];

      }

      B=newdisjonctionconj2(dnf.size()*2);

      //cout << *B << endl;

      // delete t1 
      for(i=0;i<t1.size();i++) delete t1[i];
      
      return;
    }

    if(q->first==true && q->forall==true) {
      form_t *B1;
      vector<clause_t> dnf;
      vector<form_t*> t1,tabt;

      FV(q->e1,B1,t1);
      
      CNF_2(B1,dnf,t1.size());

      //cout << *B1 << endl;
      //nfaff(dnf,cout);

      delete B1;
      
      tabt.resize(dnf.size()*2);
      tab.resize(dnf.size()*4);

      for(i=0;i<dnf.size();i++) {

	form_t *ft=NULL;
	for(j=0;j<dnf[i].size();j++) {
	  if(dnf[i][j].j==0) {
	    if(dnf[i][j].pos)
	      ORN(ft,t1[dnf[i][j].i]);
	    else
	      ORN(ft,t1[dnf[i][j].i],false);
	  }
	}
	
	if(ft==NULL) ft=newfalse();
	tabt[i*2]=ft;

	ft=NULL;
	for(j=0;j<dnf[i].size();j++) {
	  if(dnf[i][j].j==1)
	    if(dnf[i][j].pos)
	      ORN(ft,t1[dnf[i][j].i]);
	    else
	      ORN(ft,t1[dnf[i][j].i],false);
	}
	if(ft==NULL) ft=newfalse();
	tabt[i*2+1]=ft;

	tab[i*4]=new quant_t(true,true,v,tabt[i*2]->copy());
	tab[i*4+1]=fovout(tabt[i*2+1],v);
	tab[i*4+2]=fovout(tabt[i*2],v);
	tab[i*4+3]=new quant_t(true,true,v,tabt[i*2+1]->copy());

	delete tabt[i*2];
	delete tabt[i*2+1];

      }

      B=newconjonctiondisj2(dnf.size()*2);

      // delete t1 
      for(i=0;i<t1.size();i++) delete t1[i];
      
      return;
    }
    throw exception_msol_t("FV todo");
  }


  throw exception_msol_t("FV");
}


#endif

#endif