#ifndef INCLUDE_TITANIUM_QUAL_SOLVER_H
#define INCLUDE_TITANIUM_QUAL_SOLVER_H

#include <cassert>
#include <AST.h>
#include <quals.h>
#include "QualMap.h"

class TreeNode;
class TypeNode;


class QualSolver
{
public:
  QualSolver();
  virtual ~QualSolver();
  
  void conservative( const TypeNode & );
  void identicalTo(  const TreeNode &, const TreeNode & );
  void subsumedBy(   const TreeNode &, const TreeNode & );

protected:
  virtual qual qconst( const TypeNode & ) const = 0;
  qual qvar( const TreeNode & );
  qual qvar( const TreeNode & ) const;
  
  QualMap variables;
};


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


inline QualSolver::QualSolver()
{
  init_quals();
}


inline QualSolver::~QualSolver()
{
  finish_quals();
  dispose_quals();
}


inline qual QualSolver::qvar( const TreeNode &node )
{
  qual &result = variables[ &node ];
  if (!result)
    result = make_fresh_qvar( &node );
  
  return result;
}


inline qual QualSolver::qvar( const TreeNode &node ) const
{
  QualMap::const_iterator found = variables.find( &node );
  return found == variables.end() ? 0 : found->second;
}


inline void QualSolver::conservative( const TypeNode &type )
{
  unify_qual( qvar( type ), qconst( type ) );
}


inline void QualSolver::identicalTo( const TreeNode &node1,
			      const TreeNode &node2 )
{
  if ( &node1 != &node2 )
    unify_qual( qvar( node1 ), qvar( node2 ) );
}


inline void QualSolver::subsumedBy( const TreeNode &lesser,
			     const TreeNode &greater )
{
  mkleq_qual( qvar( lesser ), qvar( greater ) );
}



#endif // !INCLUDE_TITANIUM_QUAL_SOLVER_H