//---------------------------------------------------------------------------
#include <string.h>
#include <stdlib.h>
#ifdef BC
  #include <algorithm.h>
#endif
#include <math.h> // powl
//---------------------------------------------------------------------------
#include "main.h"
#include "conf.h"
#include "boom.h"
#include "tboolfnct.h"
#include "tpfnct.h"
#include "algs.h"
#include "cover.h"
#include "simulate.h"
#include "checks.h"
#include "bufferstruct.h"
//---------------------------------------------------------------------------
int CheckConsist( TBoolFnct * fn, TGauge gauge ) // 0=nonconsistent, 1=OK, 2=overlapping
{
  TPfnct * ff, * ff1;
  int i, brk, j;
  int flg1, flg2;
  int ovt;

  gauge.NewGauge( "Checkling PLA for consistence", fn->terms, 1 );
  ff = fn->fnct;
  ovt = 0;
  j = 0;
  while ( ff != 0 )
  {
    ff1 = ff->next;
    flg1 = 0;
    flg2 = 0;
    while ( ff1 != 0 )
    {
      brk = 0;
      for ( i = 0; i < fn->inpvars; i++ )
      {
        if ( ff->iv[i] != ff1->iv[i] && ff->iv[i] != '-' && ff1->iv[i] != '-' )
        {
          brk = 1;
          break;
        }
        if ( ff->iv[i] != ff1->iv[i] && ff->iv[i] == '-' ) flg1 = 1;
        if ( ff->iv[i] != ff1->iv[i] && ff1->iv[i] == '-' ) flg2 = 1;
      }
      if ( brk == 0 )
        for ( i = 0; i < fn->outvars; i++ )
        {
          if ( ff->ov[i] != ff1->ov[i] && ff->ov[i] != '~' && ff1->ov[i] != '~' )
          {
            gauge.CloseGauge();
            return 0;
          }
          if ( flg1 + flg2 == 2 && ff->ov[i] == '1' ) ovt = 1;
        }
      ff1 = ff1->next;
    }
    ff = ff->next;
    gauge.GaugeStep( j++, 0 );
  }
  gauge.CloseGauge();
  return ovt + 1;
}

//---------------------------------------------------------------------------

void MakeCovField( TBoolFnct * fn, TPfnct * ff )
{
  TCovs * c;
  int d;

  delete[] ff->covfield;
  ff->covfield = new int[ff->covlen];
  c = ff->cov;
  d = 0;
  while ( c != 0 )
  {
    ff->covfield[d++] = c->index + fn->parent->maxonterms * c->var;
    c = c->next;
  }
  QuickSort( ff->covfield, d );
}

//---------------------------------------------------------------------------
void DominChk( TBoolFnct * fn, TBoolFnct * rfn, TGauge gauge ) /* Checks whether some rfn terms dominates dome fn terms.
Dominated terms from fn are deleted. Needs pre-computed cover (fn->cov).
For each fn term creates covfield structure, if not present */
{
  TPfnct * ff1, * ff2;
  TCovs * c;
  int i, j;
  int d1;

  gauge.NewGauge( "Cheching for dominance", fn->terms, 1 );

  ff1 = fn->fnct;
  while ( ff1 != 0 )
  {
    ff1->valid = 1;
    MakeCovField( fn, ff1 );
    ff2 = rfn->fnct;
    while ( ff2 != 0 && ff1->valid == 1 )
    {
      d1 = ff1->covlen;
      c = ff2->cov;
      while ( c != 0 && d1 > 0 )
      {
        if ( QFind( ff1->covfield, ff1->covlen, c->index + fn->parent->maxonterms * c->var ) ) d1--;
        c = c->next;
      }
      if ( d1 == 0 && ff1->dim <= ff2->dim )
      {
        ff1->valid = 0;
        if ( ff1->dim == ff2->dim ) ff2->origin |= ff1->origin;
      }
      ff2 = ff2->next;
    }
    ff1 = ff1->next;
    gauge.GaugeStep( j++, 0 );
  }
  fn->DeleteInvalidTerms();
  gauge.CloseGauge();
}
//---------------------------------------------------------------------------
void SelfDominChk( TBoolFnct * fn, TGauge gauge )
{
  TPfnct * ff1, * ff2;
  TCovs * c;
  char * coverd;
  int i, j;
  int d, d1;
  int ovd;

  gauge.NewGauge( "Cheching for dominance", fn->terms, 1 );
  coverd = new char[fn->parent->maxonterms * fn->outvars];
  ff1 = fn->fnct;
  while ( ff1 != 0 )
  {
    ff1->valid = 1;
    ff1 = ff1->next;
  }
  ff1 = fn->fnct;
  j = 0;
  while ( ff1 != 0 )
  {
    if ( ff1->valid == 1 )
    {
      for ( i = 0; i < fn->parent->maxonterms * fn->outvars; i++ ) coverd[i] = '0';
      c = ff1->cov;
      d = 0;
      while ( c != 0 )
      {
        coverd[c->index + fn->parent->maxonterms * c->var] = '1';
        d++;
        c = c->next;
      }
      ff2 = ff1->next;
      while ( ff2 != 0 && ff1->valid == 1 )
      {
        if ( ff2->valid == 1 )
        {
          ovd = 0;
          d1 = d;
          c = ff2->cov;
          while ( c != 0 && d1 > 0 )
          {
            if ( coverd[c->index + fn->parent->maxonterms * c->var] == '1' ) d1--;
            else
              ovd = 1;
            c = c->next;
          }
          if ( d1 <= 0 ) ff1->valid = 0;
          else if ( ovd == 0 ) ff2->valid = 0;
        }
        ff2 = ff2->next;
      }
    }
    ff1 = ff1->next;
    gauge.GaugeStep( j++, 0 );
  }
  fn->DeleteInvalidTerms();
  delete[] coverd;
  gauge.CloseGauge();
}
//---------------------------------------------------------------------------
void DuplChk( TBoolFnct * fn, TGauge gauge )
{
  TPfnct * ff1, * ff2;
  int i;

  gauge.NewGauge( "Removing duplicities", fn->terms, 1 );
  ff1 = fn->fnct;
  i = 0;
  while ( ff1 != 0 )
  {
    ff2 = ff1->next;
    while ( ff2 != 0 )
    {
      if ( strcmp( ff1->iv, ff2->iv ) == 0 ) ff2->valid = 0;
      ff2 = ff2->next;
    }
    ff1 = ff1->next;
    gauge.GaugeStep( i++, 0 );
  }
  fn->DeleteInvalidTerms();
  gauge.CloseGauge();
}
//---------------------------------------------------------------------------
int NoIntersections2( TBoolFnct * fn ) /* Reduces terms so that there are no intersecting terms
returns 0 if nonconsistent function is encountered Basic algorithm. Deprecated. */
{
  TPfnct * ff, * ff1, * ff2, * ff3, * pff, * pff1;
  int i, j, brk;
  int d;
  char * s;
  int uvs;
  int br2;
  unsigned int dff, dff1;

  uvs = 0;
  s = new char[fn->inpvars + 1];
  pff = 0;
  ff = fn->fnct;
  while ( ff != 0 )
  {
    pff1 = ff;
    ff1 = ff->next;
    while ( ff1 != 0 )
    { // check for intersection
      br2 = 0;
      brk = 0;
      dff = 0; dff1 = 0;
      for ( i = 0; i < fn->inpvars; i++ )
      {
        if ( ff->iv[i] != ff1->iv[i] && ff->iv[i] != '-' && ff1->iv[i] != '-' )
        {
          brk = 1;
          break;
        }
        if ( ff->iv[i] == '-' && ff1->iv[i] != '-' ) dff++;
        if ( ff1->iv[i] == '-' && ff->iv[i] != '-' ) dff1++;
      }
      if ( brk == 0 )
      {
        for ( i = 0; i < fn->outvars; i++ ) // check for inconsistency
               if ( abs( ff->ov[i] - ff1->ov[i] ) == 1 )
               {
                 delete[] s;
                 return 0;
               }
             if ( dff != 0 && dff1 != 0 )
             {
               memcpy( s, ff->iv, fn->inpvars + 1 ); // compute intersection
               d = ff->dim;
               for ( i = 0; i < fn->inpvars; i++ )
                 if ( ff->iv[i] != ff1->iv[i] )
                 {
                   if ( ff->iv[i] == '-' )
                   {
                     s[i] = ff1->iv[i];
                     d--;
                   }
                 }
               ff2 = fn->AddTermToEnd( s, ff->ov, d );
               ff3 = ff1;
        }
        if ( dff == 0 )
        {
          ff2 = ff;
          ff3 = ff1;
        }
        else if ( dff1 == 0 )
        {
          ff2 = ff1;
          ff3 = ff;
        }
        for ( i = 0; i < fn->outvars; i++ )
          if ( ff3->ov[i] != '~' ) ff2->ov[i] = ff3->ov[i];

        // compute ff - intersection
        if ( dff != 0 )
        {
          for ( i = 0; i < fn->inpvars; i++ )
            if ( ff->iv[i] == '-' && ff2->iv[i] != '-' )
            {
              if ( ff2->iv[i] == '1' ) ff->iv[i] = '0';
              else
                ff->iv[i] = '1';
              ff->dim--;
              memcpy( s, ff->iv, fn->inpvars + 1 );
              s[i] = ff2->iv[i];
              d = ff->dim;
              break;
            }
          j = i + 1;
          for ( i = j; i < fn->inpvars; i++ )
            if ( ff->iv[i] == '-' && ff2->iv[i] != '-' )
            {
              d--;
              ff3 = fn->AddTermToEnd( s, ff->ov, d );
              if ( ff2->iv[i] == '1' ) ff3->iv[i] = '0';
              else
                ff3->iv[i] = '1';
              s[i] = ff2->iv[i];
            }
        }
        // compute ff1 - intersection
        if ( dff1 != 0 )
        {
          for ( i = 0; i < fn->inpvars; i++ )
            if ( ff1->iv[i] == '-' && ff2->iv[i] != '-' )
            {
              if ( ff2->iv[i] == '1' ) ff1->iv[i] = '0';
              else
                ff1->iv[i] = '1';
              ff1->dim--;
              memcpy( s, ff1->iv, fn->inpvars + 1 );
              s[i] = ff2->iv[i];
              d = ff1->dim;
              break;
            }
          j = i + 1;
          for ( i = j; i < fn->inpvars; i++ )
            if ( ff1->iv[i] == '-' && ff2->iv[i] != '-' )
            {
              d--;
              ff3 = fn->AddTermToEnd( s, ff1->ov, d );
              if ( ff2->iv[i] == '1' ) ff3->iv[i] = '0';
              else
                ff3->iv[i] = '1';
              s[i] = ff2->iv[i];
            }
        }
        if ( dff == 0 && dff1 == 0 )
        {
          fn->DeleteTerm( ff1, pff1 );
          ff1 = pff1;
          br2 = 2;
        }
      }
      if ( br2 > 1 )
      {
        ff1 = pff1->next;
      }
      else
      {
        pff1 = ff1;
        ff1 = ff1->next;
      }
    }
    if ( br2 & 1 )
    {
      ff = fn->fnct;
      pff = 0;
    }
    else
    {
      pff = ff;
      ff = ff->next;
    }
  }
  delete[] s;
  return 1;
}
//---------------------------------------------------------------------------
int NoIntersections( TBoolFnct * fn, TGauge gauge ) /* Reduces terms so that there are no intersecting terms
returns 0 if nonconsistent function is encountered returns 3 when interrupted Uses tree buffer for speedup */
{
  TPfnct * ff, * ff1, * ff2, * ff3, * pff, * pff1, * ff4;
  int i, j, k, brk;
  int d;
  char * s, * s1;
  int uvs;
  int br2;
  unsigned int dff, dff1;
  TermTree * th;
  int tos;
  char * ov;

  ov = new char[fn->outvars + 1];
  s = new char[fn->inpvars + 1];
  s1 = new char[fn->inpvars + 1];
  gauge.NewGauge( "Splitting intersecting terms...", 0, 2 );
  th = new TermTree( fn ); // add terms to buffer & check for duplicities
  pff = 0;
  ff = fn->fnct;
  while ( ff != 0 )
  {
    ff1 = th->AddTermToTreeHistory( ff );
    if ( ff1 != 0 )
    {
      for ( i = 0; i < fn->outvars; i++ ) // check for inconsistency
             if ( abs( ff->ov[i] - ff1->ov[i] ) == 1 )
             {
               delete[] s;
               delete[] s1;
               delete[] ov;
               delete th;
               gauge.CloseGauge();
               return 0;
             }
           for ( i = 0; i < fn->outvars; i++ )
             if ( ff->ov[i] != '~' ) ff1->ov[i] = ff->ov[i];
      fn->DeleteTerm( ff, pff );
      ff = pff;
    }
    pff = ff;
    ff = ff->next;
  }

  tos = 0;
  uvs = 0;
  pff = 0;
  ff = fn->fnct;
  while ( ff != 0 )
  {
    pff1 = ff;
    ff1 = ff->next;
    while ( ff1 != 0 )
    { // check for intersection
      br2 = 0;
      brk = 0;
      dff = 0; dff1 = 0;
      for ( i = 0; i < fn->inpvars; i++ )
      {
        if ( ff->iv[i] != ff1->iv[i] && ff->iv[i] != '-' && ff1->iv[i] != '-' )
        {
          brk = 1;
          break;
        }
        if ( ff->iv[i] == '-' && ff1->iv[i] != '-' ) dff++;
        if ( ff1->iv[i] == '-' && ff->iv[i] != '-' ) dff1++;
      }
      if ( brk == 0 )
      {
        tos++;
        for ( i = 0; i < fn->outvars; i++ ) // check for inconsistency
               if ( abs( ff->ov[i] - ff1->ov[i] ) == 1 )
               {
                 delete[] s;
                 delete[] s1;
                 delete[] ov;
                 delete th;
                 gauge.CloseGauge();
                 return 0;
               }
             if ( dff != 0 && dff1 != 0 )
             {
               memcpy( s, ff->iv, fn->inpvars + 1 ); // compute intersection
               d = ff->dim;
               for ( i = 0; i < fn->inpvars; i++ )
                 if ( ff->iv[i] != ff1->iv[i] )
                 {
                   if ( ff->iv[i] == '-' )
                   {
                     s[i] = ff1->iv[i];
                     d--;
                   }
                 }
               ff4 = th->IsTermInTreeHistory2( s );
               if ( ff4 == 0 )
               {
                 ff2 = fn->AddTermToEnd( s, ff->ov, d );
                 ff3 = ff1;
                 th->AddTermToTreeHistory( ff2 );
               }
               else
               {
                 for ( i = 0; i < fn->outvars; i++ )
                   if ( ff->ov[i] != '~' ) ff4->ov[i] = ff->ov[i];
                 ff2 = ff4;
                 ff3 = ff1;
               }
        }
        if ( dff == 0 )
        {
          ff2 = ff;
          ff3 = ff1;
        }
        else if ( dff1 == 0 )
        {
          ff2 = ff1;
          ff3 = ff;
        }
        for ( i = 0; i < fn->outvars; i++ )
          if ( ff3->ov[i] != '~' ) ff2->ov[i] = ff3->ov[i];

        // compute ff - intersection
        if ( dff != 0 )
        {
          for ( i = 0; i < fn->inpvars; i++ )
            if ( ff->iv[i] == '-' && ff2->iv[i] != '-' )
            {
              if ( th->IsTermInTreeHistory2( ff->iv ) ) th->DeleteTermFromTreeHistory( ff->iv );
              if ( ff2->iv[i] == '1' ) ff->iv[i] = '0';
              else
                ff->iv[i] = '1';
              ff->dim--;

              memcpy( ov, ff->ov, fn->outvars + 1 );
              ff4 = th->IsTermInTreeHistory2( ff->iv );

              if ( ff4 != 0 )
              {
                for ( k = 0; k < fn->outvars; k++ )
                  if ( ff->ov[k] != '~' ) ff4->ov[k] = ff->ov[k];
                if ( pff1 == ff ) pff1 = pff;
                fn->DeleteTerm( ff, pff );
                ff = ff4;
                br2 = 3;
              }
              else
                th->AddTermToTreeHistory( ff );

              memcpy( s, ff->iv, fn->inpvars + 1 );
              s[i] = ff2->iv[i];
              d = ff->dim;
              break;
            }
          j = i + 1;
          for ( i = j; i < fn->inpvars; i++ )
          {
            memcpy( s1, s, fn->inpvars + 1 );
            if ( ff->iv[i] == '-' && ff2->iv[i] != '-' )
            {
              if ( ff2->iv[i] == '1' ) s1[i] = '0';
              else
                s1[i] = '1';
              s[i] = ff2->iv[i];
              d--;
              ff4 = th->IsTermInTreeHistory2( s1 );

              if ( ff4 == 0 )
              {
                ff3 = fn->AddTermToEnd( s1, ov, d );
                th->AddTermToTreeHistory( ff3 );
              }
              else
              {
                for ( k = 0; k < fn->outvars; k++ )
                  if ( ov[k] != '~' ) ff4->ov[k] = ov[k];
              }
            }
          }
        }
        // compute ff1 - intersection
        if ( dff1 != 0 )
        {
          for ( i = 0; i < fn->inpvars; i++ )
            if ( ff1->iv[i] == '-' && ff2->iv[i] != '-' )
            {
              if ( th->IsTermInTreeHistory2( ff1->iv ) ) th->DeleteTermFromTreeHistory( ff1->iv );
              if ( ff2->iv[i] == '1' ) ff1->iv[i] = '0';
              else
                ff1->iv[i] = '1';
              ff1->dim--;

              memcpy( ov, ff1->ov, fn->outvars + 1 );
              ff4 = th->IsTermInTreeHistory2( ff1->iv );

              if ( ff4 != 0 )
              {
                for ( k = 0; k < fn->outvars; k++ )
                  if ( ff1->ov[k] != '~' ) ff4->ov[k] = ff1->ov[k];
                fn->DeleteTerm( ff1, pff1 );
                ff1 = ff4;
                br2 = max( br2, 2 );
              }
              else
                th->AddTermToTreeHistory( ff1 );
              memcpy( s, ff1->iv, fn->inpvars + 1 );
              s[i] = ff2->iv[i];
              d = ff1->dim;
              break;
            }
          j = i + 1;
          for ( i = j; i < fn->inpvars; i++ )
          {
            memcpy( s1, s, fn->inpvars + 1 );
            if ( ff1->iv[i] == '-' && ff2->iv[i] != '-' )
            {
              if ( ff2->iv[i] == '1' ) s1[i] = '0';
              else
                s1[i] = '1';
              s[i] = ff2->iv[i];
              d--;
              ff4 = th->IsTermInTreeHistory2( s1 );

              if ( ff4 == 0 )
              {
                ff3 = fn->AddTermToEnd( s1, ov, d );
                th->AddTermToTreeHistory( ff3 );
              }
              else
              {
                for ( k = 0; k < fn->outvars; k++ )
                  if ( ov[k] != '~' ) ff4->ov[k] = ov[k];
              }
            }
          }
        }
        if ( dff == 0 && dff1 == 0 )
        {
          gauge.CloseGauge();
          return 2;
          // if it is OK, removing duplicities is not necessary, since they cannot occur
          /* ff4 = IsTermInTreeHistory2(th, ff1->iv); if (ff4 != ff1) { i = 0; } if (ff4 != 0)
          DeleteTermFromTreeHistory(th, ff1->iv); for (k = 0; k < fn->outvars; k++) if (ff1->ov[k] != '~' && ff->ov[k] == '~')
          ff->ov[k] = ff1->ov[k]; DeleteTerm(fn, ff1, pff1); ff1 = pff1; br2 = 2;    */
        }
      }
      if ( gauge.GaugeStep( fn->terms, 2 ) != 0 )
      {
        delete[] s;
        delete[] s1;
        delete[] ov;
        delete th;
        gauge.CloseGauge();
        return 3;
      }
      if ( br2 > 1 )
      {
        ff1 = pff1->next;
        if ( br2 == 3 ) break;
      }
      else
      {
        pff1 = ff1;
        ff1 = ff1->next;
      }
    }
    if ( br2 == 3 )
    {
      if ( pff == 0 ) ff = fn->fnct;
      else
        ff = pff->next;
    }
    else
    {
      pff = ff;
      ff = ff->next;
    }
  }
  delete[] s;
  delete[] s1;
  delete[] ov;
  delete th;
  gauge.CloseGauge();
  return 1;
}
//---------------------------------------------------------------------------
TBoolFnct * SplitToMinterms( TBoolFnct * fn, TGauge gauge ) /* Splits function into minterms, the outputs are simulated.
For both the fd and fr functions. Returns 0 when inconsistent function encountered. */
{
  TPfnct * ff;
  int i, j;
  TBoolFnct * ofn;
  long t, v;
  char * iv, * ov;

  ofn = fn->CreateChildFnct();
  iv = new char[fn->inpvars + 1];
  ov = new char[fn->outvars + 1];

  gauge.NewGauge( "Splitting into minterms...", pow( 2.0, (double)fn->inpvars ), 1 );
  for ( t = 0; t < pow( 2.0,(double)fn->inpvars ); t++ )
  {
    v = t; // fill iv with binary value
    i = fn->inpvars - 1;
    while ( v != 0 )
    {
      iv[i] = div((long)v, (long)2 ).rem + '0';
      v = div((long)v, (long)2 ).quot;
      i--;
    }
    while ( i >= 0 )
    {
      iv[i] = '0';
      i--;
    }

    if ( !Simulate( fn, iv, ov ) )
    {
      delete[] iv;
      delete[] ov;
      delete ofn;
      gauge.CloseGauge();
      return 0;
    }
    ofn->AddTermToEnd( iv, ov, 0 );
    gauge.GaugeStep( t, 1 );
  }
  delete[] iv;
  delete[] ov;
  gauge.CloseGauge();
  return ofn;
}
//---------------------------------------------------------------------------
