//
// Copyright (c) 2009 Froduald Kabanza and the Université de Sherbrooke.
// Use of this software is permitted for non-commercial research purposes, and
// it may be copied or applied only for that use. All copies must include this
// copyright message.
// 
// This is a research prototype that has not gone through intensive tests and
// is delivered as is. It may still contain bugs. Froduald Kabanza and the
// Université de Sherbrooke disclaim any responsibility for damage that may be
// caused by using it.
//
// Please note that some files were inspired in part by the PDDL4J library:
// http://www.math-info.univ-paris5.fr/~pellier/software/software.php 
//
// Implementation: Simon Chamberland
// Project Manager: Froduald Kabanza
//

#ifndef _ROOT_FORMULA_H
#define _ROOT_FORMULA_H

#include "../ITerm.h"
#include "../Term/Object.h"
#include "../Term/ObjectParameterVariable.h"
#include "../../Utils/Utils.h"
#include "../../../Utils/ReferenceCounted.h"

#include <string>
#include <list>
#include <vector>
#include <map>

#undef min
#undef max

namespace planning
{
  class FormulaApplication;

  /// <summary>
  /// This abstract class is the base class for root formula, i.e. formulas "template"
  /// defined in a PDDL domain.
  /// </summary>
  class RootFormula : public ReferenceCounted
  {
  public:
    /// <summary>
    /// Creates a new root formula with a specified name and arguments.
    /// </summary>
    /// <param name="name">The name of the new root formula.</param>
    /// <param name="arguments">The arguments (variables) of the new root formula.</param>
    template <class Iterator>
    RootFormula(const std::string& name, Iterator argumentsBegin, Iterator argumentsEnd)
      : m_name(name), m_arguments(argumentsBegin, argumentsEnd), m_offset(std::numeric_limits<size_t>::max()),
        m_hashCode(s_stringHasher(name))
    {
      memory::acquire(this, m_arguments.begin(), m_arguments.end());

      m_objectBuffer = new const Object*[m_arguments.size()];
      m_termBuffer = new const ITerm*[m_arguments.size()];
      assert(!sequenceContainsNullValues(m_arguments.begin(), m_arguments.end()));
    }

    virtual ~RootFormula();

    const std::string& getName() const;

    size_t getOffset() const;

    /// <summary>
    /// Returns the arity (number of arguments) of this root formula.
    /// </summary>
    /// <returns>The arity of this root formula.</returns>
    size_t getArity() const;

    const std::vector<ObjectParameterVariable*>& getArguments() const;

    /// <summary>
    /// Updates this root formula according to another root formula.
    /// </summary>
    /// <param name="source">The other root formula used to update this one.</param>
    //virtual void copyFrom(const RootFormula *source);

    size_t getDomainCardinality() const;

    void preprocess(size_t offset);

    virtual void releaseMembers();

    template <class Iterator>
    const FormulaApplication* evaluateArguments(Iterator argumentsBegin,
                                                Iterator argumentsEnd,
                                                const IClosedWorld* world, 
                                                const Bindings* bindings) const
    {
      const Object** objectPos = m_objectBuffer;
      for (; argumentsBegin != argumentsEnd; ++argumentsBegin)
      {
        *objectPos++ = (*argumentsBegin)->evaluate(world, bindings);
      }
      return getGroundFormulaApplication(m_objectBuffer, m_objectBuffer + getArity());
    }

    template <class Iterator>
    FormulaApplication* getFormulaApplication(Iterator argumentsBegin,
                                              Iterator argumentsEnd) const
    {
      // Can't use ground formulas since IDs might not be calculated yet
      bool allObjectArgs = true;
      const Object** objectPos = m_objectBuffer;
      const ITerm** termPos = m_termBuffer;
      for (; argumentsBegin != argumentsEnd; ++argumentsBegin)
      {
        *termPos++ = *argumentsBegin;

        const Object* object;
        if (allObjectArgs && (object = dynamic_cast<const Object*>(*argumentsBegin)) != NULL)
          *objectPos++ = object;
        else
          allObjectArgs = false;
      }

      if (allObjectArgs)
      {
        return getGroundFormulaApplication(m_objectBuffer, m_objectBuffer + getArity());
      }
      else
      {
        return instantiate(m_termBuffer, m_termBuffer + getArity());
      }
    }

    int compareTo(const RootFormula& other) const;

    size_t getHashCode() const;

    typedef int TypeId;

  protected:
    virtual void _output(std::ostream& out) const;

    //const FormulaApplication* getFormulaApplication(int formulaId) const;

    static boost::hash<std::string> s_stringHasher;

    FormulaApplication* getGroundFormulaApplication(const Object** begin, const Object** end) const;

    template <class Iterator>
    size_t getArgumentsId(Iterator argumentsBegin, Iterator argumentsEnd) const
    {
      size_t id = 0, cur = 1;

      std::vector<ObjectParameterVariable*>::const_iterator it = m_arguments.begin();
      for (; argumentsBegin != argumentsEnd; ++argumentsBegin)
      {
        ObjectParameterVariable* var = *it++;
        const Type* type = var->getType();
        const Object* object = *argumentsBegin;
        id += (cur * object->getObjectId(type));
        cur *= type->getDomainCardinality();
      }
      return id;
    }

    template <class TermIterator>
    FormulaApplication* instantiate(TermIterator begin, TermIterator end) const
    {
      const ITerm** arguments = new const ITerm*[getArity()];
      for (const ITerm** current = arguments; begin != end; ++current, ++begin)
      {
        *current = *begin;
      }
      return instantiate(arguments);
    }

    /// <summary>
    /// Instantiates a formula application associated with this root formula.
    /// </summary>
    /// <param name="arguments">Arguments of the formula application to instantiate.</param>
    /// <returns>A new formula application associated with this root formula.</returns>
    virtual FormulaApplication* instantiate(const ITerm** arguments) const = 0;

    typedef std::vector<ObjectParameterVariable*>::iterator iterator;
    typedef std::vector<ObjectParameterVariable*>::const_iterator const_iterator;

    /// <summary>
    /// The parameter variables of this root formula.
    /// </summary>
    std::vector<ObjectParameterVariable*> m_arguments;

  private:
    bool isPreprocessed() const;

    THREAD_UNSAFE const Object** m_objectBuffer;

    THREAD_UNSAFE const ITerm** m_termBuffer;

    /// <summary>
    /// The offset (in a lookup table) at which the values of the formula applications
    /// of this type can be found.
    /// This value is set in the preprocessing phase by the preprocess() call.
    /// </summary>
    size_t m_offset;

    /// <summary>
    /// The name of this root formula.
    /// </summary>
    const std::string m_name;

    size_t m_hashCode;

    mutable std::vector<FormulaApplication*> m_applications;

    typedef std::map<std::vector<const Object*>, FormulaApplication*> MapIncompleteApplications;
    mutable MapIncompleteApplications m_incompleteGroundApplications;

    /// <summary>
    /// Returns the unique formula application associated with the given ID.
    /// </summary>
    /// <param name="argumentsID">The unique ID of the formula application to create.</param>
    /// <returns>The unique formula application associated with the given ID.</returns>
    //FormulaApplication* instantiateFromId(int argumentsID)
    //{
    //  std::vector<ITerm*> constants;
    //  foreach (ObjectParameterVariable var in this.m_parameters)
    //  {
    //    TypeSet typeSet = var.GetTypeSet();
    //    int typeSetCardinality = typeSet.Domain.Count;
    //    Constant constant = typeSet.GetConstant(argumentsID % typeSetCardinality);
    //    argumentsID /= typeSetCardinality;
    //    constants.Add(constant);
    //  }
    //  return Instantiate(constants);
    //}

    /// <summary>
    /// Verifies whether this root formula matches with a specified formula application.
    /// The two formulas match if they have the same name, the same arity, and all the
    /// arguments of the formula application can be assigned to their respective variable
    /// counterpart of the root formula.
    /// </summary>
    /// <param name="formula">The formula application to be matched with this one.</param>
    /// <returns>True if the two formulas match.</returns>
    //bool match(FormulaApplication* formula) const
    //{
    //  bool match = this.Name.Equals(formula.Name)
    //            && this.m_parameters.Count == formula.GetArguments().Count;
    //  for (int i = 0; i < this.m_parameters.Count && match; ++i)
    //  {
    //    match = this.m_parameters[i].CanBeAssignedFrom(formula.GetArguments()[i]);
    //  }
    //  return match;
    //}

    /// <summary>
    /// Returns the cardinality of this root formula's domain.
    /// The root formula's domain corresponds to all possible bindings of constants (objects)
    /// it may be evaluated with.
    /// </summary>
    /// <returns>The domain cardinality of this root formula.</returns>
    //int GetDomainCardinality() const
    //{
    //  int cardinality = 1;
    //  foreach (ObjectParameterVariable var in this.m_parameters)
    //  {
    //    List<Constant> constants = var.GetTypeSet().Domain;
    //    cardinality *= constants.Count;
    //  }
    //  return cardinality;
    //}

    /// <summary>
    /// Creates a set of parameter bindings from a specified set of constant parameters.
    /// </summary>
    /// <param name="parameters">A set of constant parameters.</param>
    /// <returns>A set of parameter bindings.</returns>
    //protected IParameterBindings GetParameterBindings(IEnumerable<Constant> parameters)
    //{
    //  ParameterBindings parameterBindings = new ParameterBindings();
    //  IEnumerator<Constant> enumCst = parameters.GetEnumerator();

    //  foreach (ObjectParameterVariable var in this.m_parameters)
    //  {
    //    enumCst.MoveNext();
    //    parameterBindings.Bind(var, enumCst.Current);
    //  }
    //  return parameterBindings;
    //}

    /// <summary>
    /// Returns true if this root formula is equal to a specified object.
    /// Two root formulas are equal if they are reference-equal.
    /// </summary>
    /// <param name="obj">Object to test for equality.</param>
    /// <returns>True if this formula is equal to the specified objet.</returns>
    //public override bool Equals(object obj)
    //{
    //  if (obj == this)
    //  {
    //    return true;
    //  }
    //  else
    //  {
    //    return false;
    //  }
    //}

    /// <summary>
    /// Returns the hash code of this root formula.
    /// </summary>
    /// <returns>The hash code of this root formula.</returns>
    //public override int GetHashCode()
    //{
    //  return this.m_hashCode;
    //}

    /// <summary>
    /// Returns a string representation of this formula.
    /// </summary>
    /// <returns>A string representation of this formula.</returns>
    //virtual std::string toString() const
    //{
    //  StringBuilder str = new StringBuilder();
    //  str.Append("(");
    //  str.Append(this.Name);
    //  foreach (ObjectParameterVariable t in this.m_parameters)
    //  {
    //    str.Append(" ");
    //    str.Append(t.ToString());
    //  }
    //  str.Append(")");
    //  return str.ToString();
    //}

    /// <summary>
    /// Returns a typed string representation of this formula.
    /// </summary>
    /// <returns>A typed string representation of this formula.</returns>
    //virtual std::string toTypedString() const
    //{
    //  StringBuilder str = new StringBuilder();
    //  str.Append("(");
    //  str.Append(this.Name);
    //  foreach (ObjectParameterVariable t in this.m_parameters)
    //  {
    //    str.Append(" ");
    //    str.Append(t.ToTypedString());
    //  }
    //  str.Append(")");
    //  return str.ToString();
    //}

    /// <summary>
    /// Compares this root formula with another root formula.
    /// </summary>
    /// <param name="other">The other expression to compare this expression to.</param>
    /// <returns>An integer representing the total order relation between the two expressions.
    /// </returns>
    //public int CompareTo(RootFormula other)
    //{
    //  return this.m_name.CompareTo(other.m_name);
    //}

  private:
    //const member prevent the use of the assigment operator
    RootFormula& operator=(const RootFormula&);
  };
}

#include "FormulaApplication.h"

#endif