#include <algorithm>
#include <list>

#include <AST.h>
#include <quals.h>
#include "solution.h"
#include "solver.h"


SharingSolver::SharingSolver()
{
  begin_po_qual();

  shared = add_qual( "shared" );
  nonshared = add_qual( "nonshared" );
  polyshared = add_qual( "polyshared" );

  add_qual_lt( shared, polyshared );
  add_qual_lt( nonshared, polyshared );

  end_po_qual();
  end_define_pos();
}


void SharingSolver::eitherAssignable( const TreeNode &type1,
				      const TreeNode &type2 )
{
  const qual var1 = qvar( type1 );
  const qual var2 = qvar( type2 );

  cond_mkleq_qual( var1, nonshared, nonshared, var2 );
  cond_mkleq_qual( var2, nonshared, nonshared, var1 );
  cond_mkleq_qual( var1, shared, shared, var2 );
  cond_mkleq_qual( var2, shared, shared, var1 );
}


Sharing SharingSolver::lub( const qual_set bounds ) const
{
  Sharing result = Unconstrained;
  qual bound;
  qual_set_scanner scanner;

  scan_quals (bound, scanner, bounds)
    result = ::lub( result, sharing( bound ) );

  return result == Unconstrained
    ? Nonshared
    : result;
}


#if 0
void SharingSolver::solve( SharingSolution &solution )
{
  for (QualMap::const_iterator scan = variables.begin(); scan != variables.end(); ++scan)
    {
      const qual_set bounds = lbc_qual( scan->second );
      const Sharing sharing = lub( bounds );
      solution.discover( *scan->first, sharing );
      unify_qual( scan->second, qconst( sharing ) );
    }
}
#endif


void SharingSolver::solve( SharingSolution &solutions )
{
  set< qual > notPrivate;
  
  for (QualMap::const_iterator scan = variables.begin(); scan != variables.end(); ++scan)
    {
      qual lower;
      qual_set_scanner scanner;
      
      scan_quals (lower, scanner, lbc_qual( scan->second ))
	if (lower == shared || lower == polyshared)
	  notPrivate.insert( scan->second );
    }
  
  for (QualMap::const_iterator scan = variables.begin(); scan != variables.end(); ++scan)
    if (notPrivate.find( scan->second ) == notPrivate.end())
      mkleq_qual( scan->second, nonshared );

  for (QualMap::const_iterator scan = variables.begin(); scan != variables.end(); ++scan)
    {
      const Sharing solution = lub( lbc_qual( scan->second ) );
      assert( solution != Unconstrained );
      solutions.discover( *scan->first, solution );
    }
}


qual SharingSolver::qconst( Sharing sharing ) const
{
  switch (sharing)
    {
    case Shared:
      return shared;
    case Nonshared:
      return nonshared;
    case Polyshared:
      return polyshared;
    default:
      assert( 0 );
      return 0;
    }
}


Sharing SharingSolver::sharing( const qual bound ) const
{
  if (bound == shared)
    return Shared;
  else if (bound == nonshared)
    return Nonshared;
  else if (bound == polyshared)
    return Polyshared;
  else
    {
      assert( 0 );
      return Unconstrained;
    }
}