//
// 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 this file was 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
//

#include "stdafx.h"
#include "NotExp.h"

#include <boost/unordered_set.hpp>
#include <assert.h>

using namespace planning;

/// <summary>
/// Creates a new negative expression.
/// </summary>
/// <param name="exp">The expression to negate.</param>
NotExp::NotExp(const ILogicalExp* expression)
  : m_exp(expression)
{
  assert(m_exp != NULL);

  m_exp->acquire(this);
  INITIALIZE_HASH_CODE();
}

NotExp::~NotExp()
{
  m_exp->release(this);
}

/// <summary>
/// Evaluates this logical expression in the specified closed world.
/// </summary>
/// <param name="world">The evaluation world.</param>
/// <param name="bindings">A set of variable bindings.</param>
/// <returns>True, false, or undefined.</returns>
bool NotExp::evaluate(const IClosedWorld* world, const Bindings* bindings) const
{
  return !m_exp->evaluate(world, bindings);
}

/// <summary>
/// Enumerates all the worlds within which this logical expression evaluates to true.
/// This method is used to support the goal modality expressions.
/// The worlds satisfying a negative expression correspond to the complement of the set of 
/// worlds satisfying the negated expression.
/// </summary>
/// <returns>All worlds except the ones satisfying the negated expression.</returns>
void NotExp::enumerateSatisfyingWorlds(PartialWorldSet& worlds) const
{
  assert(worlds.size() == 0);

  PartialWorldSet badWorlds;
  m_exp->enumerateSatisfyingWorlds(badWorlds);
  PartialWorld currentWorld;

  if (badWorlds.size() == 0)
  {
    worlds.insert(new PartialWorld());
  }
  else
  {
    typedef boost::unordered_set<const AtomicFormulaApplication*> AtomicFormulaApplicationSet;

    AtomicFormulaApplicationSet allPredicates;
    for (PartialWorldSet::const_iterator it = badWorlds.begin();
         it != badWorlds.end();
         ++it)
    {
      allPredicates.insert((*it)->predicatesBegin(), (*it)->predicatesEnd());
    }
    for (AtomicFormulaApplicationSet::const_iterator it = allPredicates.begin();
         it != allPredicates.end();
         ++it)
    {
      currentWorld.set(*it);
    }

    bool hasNext;
    do
    {
      if (badWorlds.find(&currentWorld) == badWorlds.end())
      {
        std::pair<PartialWorldSet::iterator, bool> p = 
          worlds.insert(new PartialWorld(currentWorld));
        assert(p.second);
      }

      hasNext = false;
      for (AtomicFormulaApplicationSet::const_iterator it = allPredicates.begin();
         it != allPredicates.end();
         ++it)
      {
        bool value = currentWorld.isSet(*it);
        if (value)
        {
          currentWorld.unset(*it);
          hasNext = true;
        }
        else
        {
          currentWorld.set(*it);
        }
      }
    } while (hasNext);

    // Clean up
    for (PartialWorldSet::const_iterator it = badWorlds.begin();
         it != badWorlds.end();
         ++it)
    {
      delete *it;
    }
  }


  //  HashSet<PartialWorld> worlds = new HashSet<PartialWorld>();
  //  HashSet<PartialWorld> badWorlds = m_exp.EnumerateAllSatisfyingWorlds();
  //  PartialWorld currentWorld = new PartialWorld();

  //  if (badWorlds.Count == 0)
  //  {
  //    worlds.Add(currentWorld);
  //    return worlds;
  //  }

  //  HashSet<AtomicFormulaApplication> allPredicates = new HashSet<AtomicFormulaApplication>();
  //  foreach (PartialWorld badWorld in badWorlds)
  //  {
  //    allPredicates.UnionWith(badWorld.GetAllPredicates());
  //  }
  //  foreach (AtomicFormulaApplication predicate in allPredicates)
  //  {
  //    currentWorld.Set(predicate);
  //  }

  //  bool hasNext;
  //  do
  //  {
  //    if (!badWorlds.Contains(currentWorld))
  //      worlds.Add((PartialWorld)currentWorld.Clone());

  //    hasNext = false;
  //    foreach (AtomicFormulaApplication predicate in allPredicates)
  //    {
  //      bool value = currentWorld.IsSet(predicate).ToBool();
  //      if (value)
  //      {
  //        currentWorld.Unset(predicate);
  //        hasNext = true;
  //      }
  //      else
  //      {
  //        currentWorld.Set(predicate);
  //      }
  //    }
  //  } while (hasNext);

  //  return worlds;
}

void NotExp::_output(std::ostream& out) const
{
  out << "(not " << *m_exp << ")";
}

const IExp* NotExp::_internalApply(const Bindings* bindings) const
{
  return new NotExp(m_exp->apply(bindings));
}

int NotExp::_internalCompareTo(const IExp& other) const
{
  const NotExp& exp = dynamic_cast<const NotExp&>(other);

  COMPARE(m_exp, exp.m_exp);

  return 0;
}

