/**
 *  Licensed to the Apache Software Foundation (ASF) under one
 *  or more contributor license agreements.  See the NOTICE file
 *  distributed with this work for additional information
 *  regarding copyright ownership.  The ASF licenses this file
 *  to you under the Apache License, Version 2.0 (the
 *  "License"); you may not use this file except in compliance
 *  with the License.  You may obtain a copy of the License at
 * 
 *   http://www.apache.org/licenses/LICENSE-2.0
 * 
 *  Unless required by applicable law or agreed to in writing,
 *  software distributed under the License is distributed on an
 *  "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
 *  KIND, either express or implied.  See the License for the
 *  specific language governing permissions and limitations
 *  under the License.
 */
package org.apache.maven.mercury.metadata.sat;

import java.math.BigInteger;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collections;
import java.util.Comparator;
import java.util.LinkedHashMap;
import java.util.List;
import java.util.Map;

import org.apache.maven.mercury.artifact.ArtifactMetadata;
import org.apache.maven.mercury.artifact.MetadataTreeNode;
import org.apache.maven.mercury.event.EventManager;
import org.apache.maven.mercury.event.EventTypeEnum;
import org.apache.maven.mercury.event.GenericEvent;
import org.apache.maven.mercury.event.MercuryEventListener;
import org.apache.maven.mercury.logging.IMercuryLogger;
import org.apache.maven.mercury.logging.MercuryLoggerManager;
import org.apache.maven.mercury.metadata.MetadataTreeNodeGAComparator;
import org.apache.maven.mercury.metadata.MetadataTreeNodeGAVComparator;
import org.codehaus.plexus.lang.DefaultLanguage;
import org.codehaus.plexus.lang.Language;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.ObjectiveFunction;
import org.sat4j.pb.SolverFactory;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.TimeoutException;

/**
 * Default SAT4J implementation.
 * 
 * @author Oleg Gusakov
 * @version $Id$
 */
public class DefaultSatSolver
implements SatSolver
{
  private static final IMercuryLogger LOG = MercuryLoggerManager.getLogger( DefaultSatSolver.class ); 
  private static final Language LANG = new DefaultLanguage( DefaultSatSolver.class );
  
  protected SatContext _context;
  protected IPBSolver _solver = SolverFactory.newEclipseP2();
  protected MetadataTreeNode _root;
  
  protected EventManager _eventManager;

  public static final BigInteger TWO = new BigInteger("2");
  
  protected static final Comparator<MetadataTreeNode> gaComparator = new MetadataTreeNodeGAComparator();
  //-----------------------------------------------------------------------
  public static SatSolver create( MetadataTreeNode tree )
  throws SatException
  {
    return new DefaultSatSolver( tree );
  }
  //-----------------------------------------------------------------------
  public static SatSolver create( MetadataTreeNode tree, EventManager eventManager )
  throws SatException
  {
    return new DefaultSatSolver( tree, eventManager );
  }
  //-----------------------------------------------------------------------
  public DefaultSatSolver( MetadataTreeNode tree, EventManager eventManager )
  throws SatException
  {
    this._eventManager = eventManager;
    GenericEvent event = null;
    
    if( tree == null)
      throw new SatException( LANG.getMessage( "null.tree.arg" ) );
    
    try
    {
      if( _eventManager != null )
        event = new GenericEvent( EventTypeEnum.satSolver, EVENT_CREATE_SOLVER, tree.toString() );
        
      if( tree.getId() == 0 )
        MetadataTreeNode.reNumber( tree, 1 );
      
      int nNodes = tree.countDistinctNodes();
  
      LOG.debug( "SatContext: # of variables: "+nNodes );
  
      _context = new SatContext( nNodes );
      _solver.newVar( tree.countNodes() );
      _root = tree;
      
      try
      {
        addNode( tree );
      }
      catch (ContradictionException e)
      {
        throw new SatException(e);
      }
    }
    finally
    {
      if( _eventManager != null )
      {
        event.stop();
        _eventManager.fireEvent( event );
      }
    }
  }
  //-----------------------------------------------------------------------
  public DefaultSatSolver( MetadataTreeNode tree )
  throws SatException
  {
    this( tree, null );
  }
  //-----------------------------------------------------------------------
  public final void applyPolicies( List<Comparator<MetadataTreeNode>> comparators )
  throws SatException
  {
    if( comparators == null || comparators.size() < 1 )
      return;
    
    if( _root == null )
      throw new SatException( "cannot apply policies to a null tree" );
    
    // TODO og: assumption - around 128 GA's per tree. If more - map reallocates - slow down.
    // TODO og: MERCURY-40
    Map<String, List<MetadataTreeNode>> buckets = new LinkedHashMap<String, List<MetadataTreeNode>>(128);
    fillBuckets( buckets, _root );
    sortBuckets( buckets, comparators );
    useBuckets( buckets );
  }
  //-----------------------------------------------------------------------
  private void useBuckets( Map<String, List<MetadataTreeNode>> buckets )
  throws SatException
  {
    if( buckets == null || buckets.size() < 1 )
      return;
    
    IVecInt vars            = new VecInt( 128 );
    IVec<BigInteger> coeffs = new Vec<BigInteger>( 128 );
    
    int count = 0;
    
    for( String key : buckets.keySet() )
    {
      List<MetadataTreeNode> bucket = buckets.get( key );
  
// oleg: ? this is needed if optimization is "maximize"       
//      Collections.reverse(  bucket );
      
      int bucketSize = bucket.size(); 
      
      boolean bigBucket = bucketSize > 1;

if( LOG.isDebugEnabled() )
    LOG.debug( "\n\nBucket "+key );

      IVecInt bucketVars = new VecInt( bucketSize );
      
      for( int i=0; i<bucketSize; i++ )
      {
        MetadataTreeNode n  = bucket.get(i);

if( LOG.isDebugEnabled() )
    LOG.debug( n.toString() );

        SatVar var = _context.findOrAdd(n);
        int varLiteral = var.getLiteral(); 
        
        bucketVars.push( varLiteral );
        
        if( bigBucket )
        {
          vars.push( varLiteral );
          
          BigInteger cf = TWO.pow( count++ );
          
          coeffs.push( cf );

if( LOG.isDebugEnabled() )
    LOG.debug( "    "+cf+" x"+var.getLiteral() );
        }

      }

      try
      {
        if( bucketVars != null && !bucketVars.isEmpty() )
        {
          _solver.addAtMost( bucketVars, 1 );
          _solver.addAtLeast( bucketVars, 1 );
        }
      }
      catch( ContradictionException e )
      {
        throw new SatException(e);
      }
      
if( LOG.isDebugEnabled() )
  LOG.debug( "\n" );
    }

    if( vars.isEmpty() )
      return;
    
    _solver.setObjectiveFunction( new ObjectiveFunction( vars, coeffs ) );
  }
  //-----------------------------------------------------------------------
  protected static final void sortBuckets(
        Map<String, List<MetadataTreeNode>> buckets
      , List<Comparator<MetadataTreeNode>> comparators
                                          )
  {
    Comparator<MetadataTreeNode> lastComparator;
    for( List<MetadataTreeNode> bucket : buckets.values() )
    {
      lastComparator = gaComparator;
      for( Comparator<MetadataTreeNode> comparator : comparators )
      {
        sortBucket( bucket, comparator, lastComparator );
        lastComparator = comparator;
      }
      // due to the nature of Comparator need to reverse the result
      // as the best fit is now last
      Collections.reverse( bucket );

      // the best fit now first, and we don't need duplicate GAVs
      removeDuplicateGAVs( bucket );

    }
  }
  //-----------------------------------------------------------------------
  // remove duplicates, preserving the order. The first one is the most fit,
  // so need to delete from tail
  protected static final void removeDuplicateGAVs( List<MetadataTreeNode> bucket )
  {
    if( bucket == null || bucket.size() < 2 )
      return;

    Comparator<MetadataTreeNode> gav = new MetadataTreeNodeGAVComparator();
    
    int len = bucket.size();
    int [] dups = new int[ len-1 ];
    int cnt = 0;
    
    for( int i=1; i<len; i++ )
    {
      MetadataTreeNode ti = bucket.get(i);
      
      for( int j=0; j<i; j++ )
        if( gav.compare( ti, bucket.get(j) ) == 0 )
        {
          dups[cnt++] = i;
          break;
        }
    }
    
    if( cnt > 0 )
      for( int i=0; i<cnt; i++ )
        bucket.remove( dups[cnt-i-1] );
  }
  //-----------------------------------------------------------------------
  /**
   * reorders the bucket's lastComparator equal subsets with comparator.
   */
  protected static final void sortBucket(
               List<MetadataTreeNode> bucket
               , Comparator<MetadataTreeNode> comparator
               , Comparator<MetadataTreeNode> lastComparator
               )
  {
    if( bucket == null || bucket.size() < 2 )
      return;
    
    int bLen = bucket.size();
    MetadataTreeNode [] temp = bucket.toArray( new MetadataTreeNode[ bLen ] );
    
    int wStart = -1;
    int wLen = 0;
    MetadataTreeNode [] work = new MetadataTreeNode[ bLen ];
    
    MetadataTreeNode lastNode = null;
    for( int i=0; i<bLen; i++ )
    {
      MetadataTreeNode n = temp[i];
      
      if( lastNode == null )
      {
        lastNode = n;
        continue;
      }
      
      if( lastComparator.compare(lastNode, n) == 0 )
      {
        if( wLen == 0 )
        {
          work[ wLen++ ] = lastNode;
          wStart = i-1;
        }
        
        work[ wLen++ ] = n;

        lastNode = n;

        if( i < (bLen-1) )
          continue;
      }
      
      if( wLen > 0 ) // eq list formed
      {
        reorder( work, wLen, comparator );
        for( int j=0; j<wLen; j++ )
          temp[ wStart+j ] = work[ j ];
        wLen = 0;
        wStart = -1;
      }
      
      lastNode = n;
    }
    
    bucket.clear();
    for( int i=0; i<bLen; i++ )
      bucket.add( temp[ i ] );
  }
  //-----------------------------------------------------------------------
  private static final void reorder(
                          MetadataTreeNode[] work
                          , int wLen
                          , Comparator<MetadataTreeNode> comparator
                                   )
  {
    MetadataTreeNode[] temp = new MetadataTreeNode[ wLen ];
    
    for( int i=0; i< wLen; i++ )
      temp[i] = work[i];
    
    Arrays.sort( temp, comparator );
    
    for( int i=0; i<wLen; i++ )
      work[i] = temp[i];
    
  }
  //-----------------------------------------------------------------------
  protected static final void fillBuckets(
        Map<String, List<MetadataTreeNode>> buckets
      , MetadataTreeNode node
                          )
  {
    String ga = node.getMd().getGA();
    List<MetadataTreeNode> bucket = buckets.get(ga);
    if( bucket == null )
    {
      // TODO og: assumption - around 32 GAVs per GA
      bucket = new ArrayList<MetadataTreeNode>( 32 );
      buckets.put( ga, bucket );
    }
    
    bucket.add( node );
    
    if( ! node.hasChildren() )
      return;
    
    for( MetadataTreeNode kid : node.getChildren() )
    {
      fillBuckets( buckets, kid );
    }
  }
  //-----------------------------------------------------------------------
  private final void addPB( IVecInt lits, IVec<BigInteger> coeff, boolean ge, BigInteger cardinality )
  throws ContradictionException
  {
    _solver.addPseudoBoolean( lits, coeff, ge, cardinality );
    
if( LOG.isDebugEnabled() )
  LOG.debug("PB: ");
    
    for( int i=0; i<lits.size(); i++ )
    {
      int co = Integer.parseInt( ""+coeff.get(i) );
      String sign = co < 0 ? "-" : "+";
      int    val = Math.abs(co);
      String space = val == 1 ? "" : " ";
      
if( LOG.isDebugEnabled() )
  LOG.debug( " " + sign + (val==1?"":val) + space  + "x"+lits.get(i) );
    }
if( LOG.isDebugEnabled() )
  LOG.debug(( ge ? " >= " : " < ")+" "+cardinality );
  }
  //-----------------------------------------------------------------------
  private final Map<ArtifactMetadata, List<MetadataTreeNode>> processChildren(
                                                        List<ArtifactMetadata> queries
                                                        , List<MetadataTreeNode> children
                                                                              )
  throws SatException
  {
    if( queries == null || queries.size() < 1 )
      return null;
    
    if( children == null || children.size() < 1 )
      throw new SatException("there are queries, but not results. Queries: "+queries);
    
    // TODO og: MERCURY-40
    Map<ArtifactMetadata, List<MetadataTreeNode>> res = new LinkedHashMap<ArtifactMetadata, List<MetadataTreeNode>>( queries.size() );

    for( ArtifactMetadata q : queries )
    {
      List<MetadataTreeNode> bucket = new ArrayList<MetadataTreeNode>(4);
      String queryGA = q.getGA();
      
      for( MetadataTreeNode tn : children )
      {
        if( tn.getMd() == null )
          throw new SatException("resulting tree node without metadata for query "+q );
        
        if( queryGA.equals( tn.getMd().getGA()) )
        {
          bucket.add(tn);
        }
      }
      
      if( bucket.size() < 1 )
        throw new SatException("No children for query "+queryGA );
      
      res.put( q, bucket );
    }

    return res;
  } 
  //-----------------------------------------------------------------------
  private final void addNode( MetadataTreeNode node )
  throws ContradictionException, SatException
  {
    if( node == null )
      return;
    
    if( node.getMd() == null )
      throw new SatException("found a node without metadata");
    
    SatVar nodeLit = _context.findOrAdd( node );

    // this one is a must :)
    if( node.getParent() == null )
      addPB( SatHelper.getSmallOnes( nodeLit.getLiteral() ), SatHelper.getBigOnes(1,false), true, BigInteger.ONE );
    
    if( ! node.hasChildren() )
      return;
    
    Map<ArtifactMetadata,List<MetadataTreeNode>> kids = processChildren( node.getQueries(), node.getChildren() );
    
    // leaf node in this scope
    if( kids == null )
      return;
    
    for( Map.Entry<ArtifactMetadata,List<MetadataTreeNode>> kid : kids.entrySet() )
    {
      ArtifactMetadata query = kid.getKey();
      
      List<MetadataTreeNode> range = kid.getValue();

      if( range.size() > 1 )
      {
        addRange( nodeLit.getLiteral(), range, query.isOptional() );
        for( MetadataTreeNode tn : range )
        {
          addNode( tn );
        }
      }
      else
      {
        MetadataTreeNode child = range.get(0);
        SatVar kidLit = _context.findOrAdd( child );
        
        addPB( SatHelper.getSmallOnes( new int [] { nodeLit.getLiteral(), kidLit.getLiteral() } )
            , SatHelper.getBigOnes( 1, -1 )
            , true, BigInteger.ZERO
            );
//        addRange( nodeLit.getLiteral(), range, query.isOptional() );
        addNode( child );
      }

    }
  }
  //-----------------------------------------------------------------------
  private final int [] addRange( int parentLiteral, List<MetadataTreeNode> range, boolean optional )
  throws ContradictionException, SatException
  {
    SatVar literal;
    
    int [] literals = new int[ range.size() ];
    
    int count = 0;
    
    for( MetadataTreeNode tn : range )
    {
      literal = _context.findOrAdd( tn );
      literals[count++] = literal.getLiteral();

      // implication to parent
      addPB( SatHelper.getSmallOnes( new int [] { parentLiteral, literal.getLiteral() } )
          , SatHelper.getBigOnes( 1, -1 )
          , true, BigInteger.ZERO
          );
    }
    
    IVecInt rangeVector = SatHelper.getSmallOnes( literals );
    
    if( optional ) // Sxi >= 0
    {
if( LOG.isDebugEnabled() )
  LOG.debug( "optional range: atMost 1: "+ SatHelper.vectorToString( rangeVector) );
    
      _solver.addAtMost( rangeVector, 1 );
    }
    else // Sxi = 1
    {
if( LOG.isDebugEnabled() )
  LOG.debug( "range: " + SatHelper.vectorToString( rangeVector) );

    IConstr atLeast = _solver.addAtLeast( rangeVector, 1 );
    if( LOG.isDebugEnabled() )
      LOG.debug( "atLeast: " + SatHelper.vectorToString( atLeast) );

    IConstr atMost  = _solver.addAtMost( rangeVector, 1 );
    if( LOG.isDebugEnabled() )
      LOG.debug( "atMost: " + SatHelper.vectorToString( atMost) );

    }
    
    return literals;
  }
  //-----------------------------------------------------------------------
  public final List<ArtifactMetadata> solve()
  throws SatException
  {
    List<ArtifactMetadata> res = null;
    GenericEvent event = null;
    
    try
    {
      if( _eventManager != null )
        event = new GenericEvent( EventTypeEnum.satSolver, EVENT_SOLVE, _root.toString() );
      
      if( _solver.isSatisfiable() )
      {
        res = new ArrayList<ArtifactMetadata>( _root.countNodes() );
        
        int [] model = _solver.model();

if( LOG.isDebugEnabled() )
  if( model != null )
  {
    StringBuilder sb = new StringBuilder();
    String comma = "";
    for( int m : model )
    {
      sb.append( comma+m );
      comma = ", ";
    }
    LOG.debug( '['+sb.toString()+']' );
  }
  else 
    LOG.debug( "model is null" );

        for( int i : model )
          if( i > 0 )
            res.add( _context.getMd( i ) );
      }
    }
    catch (TimeoutException e)
    {
      throw new SatException( e );
    }
    finally
    {
      if( _eventManager != null )
      {
        event.stop();
        _eventManager.fireEvent( event );
      }
    }
    return res;
  }
  //-----------------------------------------------------------------------
  public final MetadataTreeNode solveAsTree()
  throws SatException
  {
    try
    {
      if( _solver.isSatisfiable() )
      {
        int [] model = _solver.model();

if( LOG.isDebugEnabled() )
  if( model != null )
  {
    StringBuilder sb = new StringBuilder();
    String comma = "";
    for( int m : model )
    {
      sb.append( comma+m );
      comma = ", ";
    }
    LOG.debug( '['+sb.toString()+']' );
  }
  else 
    LOG.debug( "model is null" );

        return _context.getSolutionSubtree( _root, model );
      }
      return null;
    }
    catch (TimeoutException e)
    {
      throw new SatException( e );
    }
    
  }
  //-----------------------------------------------------------------------
  public void register( MercuryEventListener listener )
  {
    if( _eventManager == null )
      _eventManager = new EventManager();

    _eventManager.register( listener );
  }

  public void setEventManager( EventManager eventManager )
  {
    _eventManager = eventManager;
  }

  public void unRegister( MercuryEventListener listener )
  {
    if( _eventManager != null )
      _eventManager.unRegister( listener );
  }
  //-----------------------------------------------------------------------
}