maven-commits mailing list archives

Site index · List index
Message view « Date » · « Thread »
Top « Date » · « Thread »
From jvan...@apache.org
Subject svn commit: r663678 - in /maven/sandbox/trunk/mercury/src: main/java/org/apache/maven/mercury/metadata/ main/java/org/apache/maven/mercury/metadata/sat/ test/java/org/apache/maven/mercury/metadata/sat/
Date Thu, 05 Jun 2008 17:56:36 GMT
Author: jvanzyl
Date: Thu Jun  5 10:56:35 2008
New Revision: 663678

URL: http://svn.apache.org/viewvc?rev=663678&view=rev
Log:
MARTIFACT-20: constrain, and preserve relationships along a given branch to make sure that
we don't grab a set of dependencies from separate partitions of the tree which is not correct.
sometimes we need to backtrack to find the correct version in the correct branch.
Submitted by: Oleg Gusakov 

Modified:
    maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/ArtifactMetadata.java
    maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/DefaultSatSolver.java
    maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatClause.java
    maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatConstraint.java
    maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatContext.java
    maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatHelper.java
    maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatVar.java
    maven/sandbox/trunk/mercury/src/test/java/org/apache/maven/mercury/metadata/sat/DefaultSatSolverTest.java
    maven/sandbox/trunk/mercury/src/test/java/org/apache/maven/mercury/metadata/sat/SatFeedTest.java

Modified: maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/ArtifactMetadata.java
URL: http://svn.apache.org/viewvc/maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/ArtifactMetadata.java?rev=663678&r1=663677&r2=663678&view=diff
==============================================================================
--- maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/ArtifactMetadata.java
(original)
+++ maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/ArtifactMetadata.java
Thu Jun  5 10:56:35 2008
@@ -135,6 +135,32 @@
     public ArtifactMetadata( Artifact af )
     {
     }
+    
+    //---------------------------------------------------------------------
+    public boolean sameGAV( ArtifactMetadata md )
+    {
+      if( md == null )
+        return false;
+      
+      return 
+          sameGA( md )
+          && version != null
+          && version.equals( md.getVersion() )
+      ;
+    }
+    //---------------------------------------------------------------------
+    public boolean sameGA( ArtifactMetadata md )
+    {
+      if( md == null )
+        return false;
+      
+      return
+          groupId != null
+          && artifactId != null
+          && groupId.equals( md.getGroupId() )
+          && artifactId.equals( md.getArtifactId() )
+      ;
+    }
 
     @Override
     public String toString()

Modified: maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/DefaultSatSolver.java
URL: http://svn.apache.org/viewvc/maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/DefaultSatSolver.java?rev=663678&r1=663677&r2=663678&view=diff
==============================================================================
--- maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/DefaultSatSolver.java
(original)
+++ maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/DefaultSatSolver.java
Thu Jun  5 10:56:35 2008
@@ -6,8 +6,6 @@
 
 import org.apache.maven.mercury.metadata.ArtifactMetadata;
 import org.apache.maven.mercury.metadata.MetadataTreeNode;
-import org.sat4j.core.Vec;
-import org.sat4j.core.VecInt;
 import org.sat4j.pb.IPBSolver;
 import org.sat4j.pb.SolverFactory;
 import org.sat4j.specs.ContradictionException;
@@ -41,7 +39,8 @@
     
     int nNodes = tree.countNodes();
     context = new SatContext( nNodes );
-    setVars( tree );
+    setPivots( tree );
+    setOthers( tree );
     
     solver.newVar( context.varCount );
   }
@@ -60,18 +59,93 @@
     solver.newVar( nVars );
   }
   //-----------------------------------------------------------------------
-  private final void setVars( MetadataTreeNode tree )
+  private final void setPivots( MetadataTreeNode tree )
   throws SatException
   {
     if( tree == null )
       return;
+
+// TODO implement    
+if(true) throw new SatException("Not implemented yet");
     
-    context.find( tree.getMd() );
+    context.addWeak( tree.getMd() );
     if( tree.getChildren() != null )
       for( MetadataTreeNode child : tree.getChildren() )
       {
-        setVars( child );
+        setPivots( child );
+      }
+  }
+  //-----------------------------------------------------------------------
+  private final void setOthers( MetadataTreeNode tree )
+  throws SatException
+  {
+    if( tree == null )
+      return;
+    
+    context.addStrong( tree.getMd() );
+    if( tree.getChildren() != null )
+      for( MetadataTreeNode child : tree.getChildren() )
+      {
+        setOthers( child );
+      }
+  }
+  //-----------------------------------------------------------------------
+  private List<ArtifactMetadata> groupCommonHear( List<List<ArtifactMetadata>>
orGroup )
+  throws SatException
+  {
+    if( orGroup == null || orGroup.size() < 1 )
+      throw new SatException("cannot scan empty group for common head");
+    
+    int groupSize = orGroup.size();
+    List<ArtifactMetadata> res = new ArrayList<ArtifactMetadata>( orGroup.get(0)
);
+    
+    // one member? - done
+    if( groupSize == 1 )
+      return res;
+    
+    int index = 0;
+
+    for( List<ArtifactMetadata> branch : orGroup )
+    {
+      if( index++ == 0 )
+        continue;
+
+      for( ArtifactMetadata md : branch )
+      {
+        int len = res.size();
+        
+        for( int i=0; i<len; i++ )
+        {
+          ArtifactMetadata hmd = res.get(i);
+
+          if( hmd.sameGAV(md) )
+            continue;
+
+          // remove the rest
+          for( int j=i; j<len; j++ )
+            res.remove(i);
+          
+          break;
+        }
       }
+    }
+    
+    return res;
+  }
+  //-----------------------------------------------------------------------
+  private int calcWeekness( List<ArtifactMetadata> branch, int currentMin )
+  {
+    int res = 0;
+    
+    for( ArtifactMetadata md : branch )
+    {
+      SatVar v = context.find(md);
+      
+      if( v.isWeak() )
+        ++res;
+    }
+    
+    return res < currentMin ? res : currentMin;
   }
   //-----------------------------------------------------------------------
   public SatConstraint addOrGroup( List<List<ArtifactMetadata>> orGroup )
@@ -80,46 +154,91 @@
     if( orGroup == null || orGroup.size() < 1 )
       throw new SatException("cannot process empty OR group");
     
-    SatConstraint constraint = null;
-    int minLen = orGroup.get(0).size();
- 
-    for( List<ArtifactMetadata> branch : orGroup )
+    try
     {
-      if( constraint == null )
-        constraint = new SatConstraint( branch, context );
-      else
-        constraint.addOrGroupMember( branch, context );
-      if( branch.size() < minLen )
-        minLen = branch.size();
-    }
-    
-    if( constraint != null )
-    {
-      constraint.cardinality = minLen;
-      System.out.println("Contraint is "+constraint.toString() );
-      SatClause clause = constraint.getClause();
-      try
-      {
-        solver.addPseudoBoolean( 
-                      new VecInt( clause._vars )
-                    , new Vec<BigInteger>( clause._coeff )
-                    , true
-                    , new BigInteger(""+constraint.cardinality) 
-                                );
+      SatConstraint constraint = null;
+      int groupSize = orGroup.size();
+      int maxLen = 0;
+      int minWeekness = Integer.MAX_VALUE;
+   
+      for( List<ArtifactMetadata> branch : orGroup )
+      {
+        if( constraint == null )
+          constraint = new SatConstraint( branch, context, SatContext.STRONG_VAR );
+        else
+          constraint.addOrGroupMember( branch, context );
+  
+        if( maxLen < branch.size() )
+          maxLen = branch.size();
+        
+        minWeekness = calcWeekness(branch, minWeekness );
       }
-      catch (ContradictionException e)
+  
+      // second pass - adjust each branch with strong variable up to the max length
+      for( List<ArtifactMetadata> branch : orGroup )
+      {
+        constraint.adjust( branch, maxLen, minWeekness, context );
+      }
+      
+      // 3rd pass - generate branch structure implications
+      for( List<ArtifactMetadata> branch : orGroup )
+      {
+        int blen = branch.size();
+        if( blen == 1 )
+          break;
+        
+        SatVar currLit = context.find( branch.get(0) );
+        SatVar nextLit = null;
+        
+        for( int i=1; i < blen; i++ )
+        {
+          nextLit = context.find( branch.get(i) );
+System.out.println(nextLit._md+" -> "+currLit._md + " : -x"+ nextLit._no+" +x"+currLit._no+"
>= -1");
+          // generate implication nextLit -> currLit
+          solver.addPseudoBoolean( 
+              SatHelper.getSmallOnes( nextLit._no, currLit._no )
+            , SatHelper.getBigOnes( -1, 1 )
+            , true
+            , new BigInteger("0") 
+                        );
+          solver.addPseudoBoolean( 
+              SatHelper.getSmallOnes( nextLit._no, currLit._no )
+            , SatHelper.getBigOnes( -1, 1 )
+            , false
+            , new BigInteger("1") 
+                      );
+          currLit = nextLit;
+        }
+      }
+      
+      constraint.finalAdjust( orGroup.get(0), groupSize, minWeekness, context );
+  
+      if( constraint != null )
       {
-        throw new SatException( e );
+        constraint.cardinality = groupSize * maxLen;
+System.out.println("Contraint is "+constraint.toString() );
+        SatClause clause = constraint.getClause();
+          solver.addPseudoBoolean( 
+                        SatHelper.getSmallOnes( clause._vars )
+                      , SatHelper.getBigOnes( clause._coeff )
+                      , true
+                      , new BigInteger(""+constraint.cardinality) 
+                                  );
       }
+      
+      return constraint;
+    }
+    catch (ContradictionException e)
+    {
+      throw new SatException( e );
     }
-    
-    return constraint;
   }
   //-----------------------------------------------------------------------
   public SatConstraint addPivot( List<ArtifactMetadata> pivot )
   throws SatException
   {
-    SatConstraint constraint = new SatConstraint( pivot, context );
+System.out.println("Pivot: " + pivot );
+    SatConstraint constraint = new SatConstraint( pivot, context, SatContext.WEAK_VAR );
 
     try
     {

Modified: maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatClause.java
URL: http://svn.apache.org/viewvc/maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatClause.java?rev=663678&r1=663677&r2=663678&view=diff
==============================================================================
--- maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatClause.java
(original)
+++ maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatClause.java
Thu Jun  5 10:56:35 2008
@@ -8,14 +8,14 @@
 public class SatClause
 {
   int [] _vars;
-  BigInteger [] _coeff;
+  int [] _coeff;
   int _sz = 0;
   int _ptr = 0;
   //---------------------------------------------------------------------------
   public SatClause( int sz )
   {
     _vars = new int [ sz ];
-    _coeff = new BigInteger[ sz ];
+    _coeff = new int[ sz ];
     _sz = sz;
     _ptr = 0;
   }
@@ -24,9 +24,10 @@
   throws SatException
   {
     if( _ptr >= _sz )
-      throw new SatException("trying to add element "+_ptr+" outsize of initialized size:
"+_sz);
+      throw new SatException("trying to add element "+_ptr+" outsize of initialized size
"+_sz);
+    
     _vars[_ptr] = v.intValue();
-    _coeff[_ptr++] = new BigInteger( ""+c.intValue() ) ;
+    _coeff[_ptr++] = c.intValue();
   }
   //---------------------------------------------------------------------------
   //---------------------------------------------------------------------------

Modified: maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatConstraint.java
URL: http://svn.apache.org/viewvc/maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatConstraint.java?rev=663678&r1=663677&r2=663678&view=diff
==============================================================================
--- maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatConstraint.java
(original)
+++ maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatConstraint.java
Thu Jun  5 10:56:35 2008
@@ -14,8 +14,9 @@
   Map<Integer,Integer> variables;
   int cardinality = 0;
   boolean ge = true;
+  boolean pivot = false;
   //----------------------------------------------------------------------------
-  public SatConstraint( List<ArtifactMetadata> mdl, SatContext context )
+  public SatConstraint( List<ArtifactMetadata> mdl, SatContext context, boolean weak
)
   throws SatException
   {
     if( mdl == null || mdl.size() < 1 )
@@ -23,40 +24,58 @@
     
     variables = new HashMap<Integer,Integer>( mdl.size() );
     
-    // first member of the group => do not decrement cardinality
+    SatVar var;
     for( ArtifactMetadata md : mdl )
     {
-      SatVar var = context.find( md );
+      var = context.find(md);
+
+      if( var == null )
+      {
+        if( weak )
+          var = context.addWeak( md );
+        else
+          var = context.addStrong( md );
+      }
+
+      add( var );
+    }
+  }
+  //----------------------------------------------------------------------------
+  public void addOrGroupMember( List<ArtifactMetadata> branch, SatContext context )
+  throws SatException
+  {
+    for( ArtifactMetadata md : branch )
+    {
+      SatVar var = context.find(md);
+      
+      if( var == null )
+        var = context.addStrong(md);
+      
       add( var );
     }
   }
   //----------------------------------------------------------------------------
   /**
-   * @return true if a new literal was added to this constraint
+   * @return new coeff of a given literal
    */
-  private boolean add( SatVar var )
+  private int add( SatVar var )
   {
     Integer varNo = new Integer( var.getNo() );
 
-    // TODO ?? check if this does not break the solver
     if( variables.containsKey(varNo) )
-      return false;
-    
-    variables.put( varNo, new Integer(1) );
-    ++cardinality;
-    return true;
-  }
-  //----------------------------------------------------------------------------
-  public void addOrGroupMember(List<ArtifactMetadata> branch, SatContext context )
-  throws SatException
-  {
-    boolean newVars = false; 
-    for( ArtifactMetadata md : branch )
     {
-      SatVar var = context.find( md );
-      if( add( var ) )
-        newVars = true;
+// TODO looks like after all we don't have to increment them.
+      int res = variables.get( varNo ).intValue();
+
+      // only strong can survive
+      if( ! var.isWeak() )
+        variables.put( varNo, new Integer(++res) );
+      
+      return res;
     }
+
+    variables.put( varNo, new Integer(1) );
+    return 1;
   }
   //----------------------------------------------------------------------------
   public SatClause getClause()
@@ -120,7 +139,108 @@
     }
     return sb.toString()+" >= "+cardinality;
   }
-  
+  //----------------------------------------------------------------------------
+  /**
+   * @param literal no
+   * @return new coeff of a given literal
+   * @throws SatException if the literal was not found
+   * 
+   */
+  private int increment( SatVar var )
+  throws SatException
+  {
+    if( var == null )
+      throw new SatException("Cannot increment a null variable");
+
+    Integer varNo = new Integer( var.getNo() );
+
+    if( variables.containsKey(varNo) )
+    {
+      int res = variables.get( varNo ).intValue() + 1;
+      variables.put( varNo, new Integer(res) );
+      
+      return res;
+    }
+    
+    throw new SatException("Literal "+varNo+" not found");
+  }
+  //----------------------------------------------------------------------------
+  /**
+   * increment the given strong variable to adjust to the max length of a group
+   * 
+   * @param mdl branch - member of an OR group
+   * @param maxlen - length of every branch to adjust to
+   * @throws SatException - if first element is not strong. Should never happen
+   *  because of the tree nature of our problem 
+   */
+  public void adjust( List<ArtifactMetadata> branch, int maxLen, int minWeekness, SatContext
context )
+  throws SatException
+  {
+    if( branch == null || branch.size() < 1 )
+      throw new SatException( "Cannot adjust an empty branch: "+branch );
+    
+    if( maxLen < 1 )
+      throw new SatException( "Max length cannot be less than zero. It is: " + maxLen );
+    
+    if( branch.size() > maxLen )
+      throw new SatException( "Maximum branch length "+maxLen+" cannot be less than current
branch length "+branch.size() );
+    
+    ArtifactMetadata md = branch.get(0);
+    if( md == null )
+      throw new SatException( "Cannot start a branch with a null metadata: "+md );
+    
+    SatVar strong = context.find( md );
+    if( strong == null )
+      throw new SatException( "Cannot start a branch with a null variable: "+strong );
+    
+    if( strong.isWeak() )
+      throw new SatException( "Cannot start a branch with a weak variable: "+strong );
+    
+    int nWeak = 0;
+    
+    for( ArtifactMetadata amd : branch )
+    {
+      SatVar lit = context.find(amd);
+      if( lit.isWeak() )
+        ++nWeak;
+    }
+
+    // and now - why we are here :)
+    int adjustBy = (nWeak - minWeekness) + ( maxLen - branch.size() );
+
+System.out.println("Adjusting branch "+branch+" ("+md+") by "+adjustBy+", ctx: "+context.toString());
+
+    while( adjustBy-- > 0 )
+      increment(strong);
+  }
+  public void finalAdjust( List<ArtifactMetadata> branch, int groupSize, int minWeekness,
SatContext context )
+  throws SatException
+  {
+    if( groupSize == 1 )
+      return;
+    
+    if( branch == null || branch.size() < 1 )
+      throw new SatException( "Cannot adjust an empty branch: "+branch );
+    
+    ArtifactMetadata md = branch.get(0);
+    if( md == null )
+      throw new SatException( "Cannot start a branch with a null metadata: "+md );
+    
+    SatVar strong = context.find( md );
+    if( strong == null )
+      throw new SatException( "Cannot start a branch with a null variable: "+strong );
+    
+    if( strong.isWeak() )
+      throw new SatException( "Cannot start a branch with a weak variable: "+strong );
+    // and now - why we are here :)
+
+    int adjustBy = (groupSize-1)* minWeekness;
+
+System.out.println("Finally adjusting branch "+branch+" ("+md+") by "+adjustBy+", ctx: "+context.toString());
+
+    while( adjustBy-- > 0 )
+      increment(strong);
+  }
   //----------------------------------------------------------------------------
   //----------------------------------------------------------------------------
 }

Modified: maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatContext.java
URL: http://svn.apache.org/viewvc/maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatContext.java?rev=663678&r1=663677&r2=663678&view=diff
==============================================================================
--- maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatContext.java
(original)
+++ maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatContext.java
Thu Jun  5 10:56:35 2008
@@ -6,19 +6,80 @@
 import org.apache.maven.mercury.metadata.ArtifactMetadata;
 
  /**
- * @author <a href="oleg@codehaus.org">Oleg Gusakov</a>
- */
+  * This class hold all variables fed to the SAT solver. Because of the
+  * tree unwinding algorithm all pivots (optional nodes) should be supplied first 
+  * 
+  * @author <a href="oleg@codehaus.org">Oleg Gusakov</a>
+  */
 class SatContext
 {
+  public static final boolean STRONG_VAR = false;
+  public static final boolean WEAK_VAR = true;
+  
   List<SatVar> variables;
   int varCount = 0;
+  boolean pivotsFinished = false;
   //-----------------------------------------------------------------------
   public SatContext(int estimatedTreeSize )
   {
     variables = new ArrayList<SatVar>( estimatedTreeSize );
   }
   //-----------------------------------------------------------------------
-  public SatVar find( ArtifactMetadata md )
+  public SatVar addWeak( ArtifactMetadata md )
+  throws SatException
+  {
+    if( pivotsFinished )
+      throw new SatException( "cannot mix Pivots and OR Groups. Pivots are always first."
);
+
+    if( md == null )
+      throw new SatException( "cannot create a literal out of a null metadata: "+md );
+
+    for( SatVar var : variables )
+    {
+      {
+        if( ! var._optional )
+          throw new SatException( "Literal x"+var._no+" ia already marked as strong. Cannot
add it as weak." );
+
+        if( var._md.sameGAV(md) )
+          return var;
+      }
+    }
+    
+    SatVar var = new SatVar( md, ++varCount, WEAK_VAR );
+    variables.add( var );
+    
+    return var; 
+  }
+  //-----------------------------------------------------------------------
+  public SatVar addStrong( ArtifactMetadata md )
+  throws SatException
+  {
+
+    if( md == null )
+      throw new SatException( "cannot create a literal out of a null metadata: "+md );
+
+    // force-finish pivots on the first non-pivot
+    pivotsFinished = true;
+    
+    for( SatVar var : variables )
+    {
+      if( var.compareTo(md) == 0 )
+      {
+        if( var._optional )
+          throw new SatException( "Literal x"+var._no+" ia already marked as weak. Cannot
add it as strong." );
+
+        if( var._md.sameGAV(md) )
+          return var;
+      }
+    }
+    
+    SatVar var = new SatVar( md, ++varCount, STRONG_VAR );
+    variables.add( var );
+    
+    return var; 
+  }
+  //-----------------------------------------------------------------------
+  private SatVar findOrAdd( ArtifactMetadata md, boolean optional )
   throws SatException
   {
     for( SatVar var : variables )
@@ -27,12 +88,23 @@
         return var;
     }
     
-    SatVar var = new SatVar( md, ++varCount );
+    SatVar var = new SatVar( md, ++varCount, optional );
     variables.add( var );
     
     return var; 
   }
   //-----------------------------------------------------------------------
+  public SatVar find( ArtifactMetadata md )
+  {
+    for( SatVar var : variables )
+    {
+      if( var.compareTo(md) == 0 )
+        return var;
+    }
+    
+    return null;
+  }
+  //-----------------------------------------------------------------------
   @Override
   public String toString()
   {
@@ -43,7 +115,7 @@
     
     for( SatVar var : variables )
     {
-      sb.append(comma+" x"+var._no+" > "+var._md.toString() );
+      sb.append(comma+" "+(var.isWeak()?'w':'s')+var._no+"="+var._md.toString() );
       comma = ',';
     }
     return sb.toString()+']';

Modified: maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatHelper.java
URL: http://svn.apache.org/viewvc/maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatHelper.java?rev=663678&r1=663677&r2=663678&view=diff
==============================================================================
--- maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatHelper.java
(original)
+++ maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatHelper.java
Thu Jun  5 10:56:35 2008
@@ -5,6 +5,8 @@
 import java.util.List;
 
 import org.apache.maven.mercury.metadata.ArtifactMetadata;
+import org.sat4j.core.ReadOnlyVec;
+import org.sat4j.core.ReadOnlyVecInt;
 import org.sat4j.core.Vec;
 import org.sat4j.core.VecInt;
 import org.sat4j.specs.IVec;
@@ -23,54 +25,45 @@
     return aml;
   }
   //-----------------------------------------------------------------------
-  public static final IVecInt getSmallOnes( int... ones )
+  public static final IVecInt getSmallOnes( int... ints )
   {
-    VecInt res = new VecInt( ones.length );
-    
-    for( int i=0; i<ones.length; i++ )
-      res.push( ones[i] );
-    
-    return res;
+    VecInt res = new VecInt( ints );
+    return new ReadOnlyVecInt(res);
+  }
+  //-----------------------------------------------------------------------
+  private static final IVec<BigInteger> toVec( BigInteger... bis  )
+  {
+    return new ReadOnlyVec<BigInteger>( new Vec<BigInteger>( bis ) );
   }
   //-----------------------------------------------------------------------
   public static final IVec<BigInteger> getBigOnes( int... ones )
   {
-    IVec<BigInteger> res = new Vec<BigInteger>( ones.length );
+    BigInteger [] res = new BigInteger[ ones.length ];
     
     for( int i=0; i<ones.length; i++ )
-      res.push( new BigInteger(""+ones[i]) );
+      res[ i ] = new BigInteger(""+ones[i]);
     
-    return res;
+    return toVec( res );
   }
   //-----------------------------------------------------------------------
   public static final IVec<BigInteger> getBigOnes( int nOnes )
   {
-    return getBigOnes(nOnes, false);
+    return getBigOnes( nOnes, false );
   }
   //-----------------------------------------------------------------------
   public static final IVec<BigInteger> getBigOnes( int nOnes, boolean negate )
   {
-    Vec<BigInteger> res = new Vec<BigInteger>( nOnes );
+    BigInteger [] res = new BigInteger[ nOnes ];
     BigInteger bi = negate ? BigInteger.ONE.negate() : BigInteger.ONE;
     
     for( int i=0; i<nOnes; i++ )
-      res.push( bi );
+      res[i] = bi;
     
-    return res;
-  }
-  //-----------------------------------------------------------------------
-  public static final void showContext( int... ones )
-  {
-    VecInt res = new VecInt( ones.length );
-    
-    for( int i=0; i<ones.length; i++ )
-      System.out.print( " x"+ones[i] );
+    return toVec(res);
   }
   //-----------------------------------------------------------------------
   public static final void show( int... ones )
   {
-    VecInt res = new VecInt( ones.length );
-    
     for( int i=0; i<ones.length; i++ )
       System.out.print( " x"+ones[i] );
   }

Modified: maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatVar.java
URL: http://svn.apache.org/viewvc/maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatVar.java?rev=663678&r1=663677&r2=663678&view=diff
==============================================================================
--- maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatVar.java
(original)
+++ maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatVar.java
Thu Jun  5 10:56:35 2008
@@ -10,8 +10,9 @@
 {
   ArtifactMetadata _md;
   int _no;
+  boolean _optional;
   //---------------------------------------------------------------------
-  public SatVar( ArtifactMetadata md, int var )
+  public SatVar( ArtifactMetadata md, int var, boolean optional )
   throws SatException
   {
     if( md == null
@@ -23,28 +24,7 @@
 
     this._md = md;
     this._no = var;
-  }
-  //---------------------------------------------------------------------
-  public boolean sameGAV( ArtifactMetadata md )
-  {
-    if( md == null )
-      return false;
-    
-    return 
-        sameGA( md )
-        && this._md.getVersion().equals( md.getVersion() )
-    ;
-  }
-  //---------------------------------------------------------------------
-  public boolean sameGA( ArtifactMetadata md )
-  {
-    if( md == null )
-      return false;
-    
-    return 
-        this._md.getGroupId().equals( md.getGroupId() )
-        && this._md.getArtifactId().equals( md.getArtifactId() )
-    ;
+    this._optional = optional;
   }
   //---------------------------------------------------------------------
   public ArtifactMetadata getMd()
@@ -63,6 +43,11 @@
   {
     this._no = var;
   }
+
+  public boolean isWeak()
+  {
+    return this._optional;
+  }
   //---------------------------------------------------------------------
   public int compareTo(ArtifactMetadata md)
   {

Modified: maven/sandbox/trunk/mercury/src/test/java/org/apache/maven/mercury/metadata/sat/DefaultSatSolverTest.java
URL: http://svn.apache.org/viewvc/maven/sandbox/trunk/mercury/src/test/java/org/apache/maven/mercury/metadata/sat/DefaultSatSolverTest.java?rev=663678&r1=663677&r2=663678&view=diff
==============================================================================
--- maven/sandbox/trunk/mercury/src/test/java/org/apache/maven/mercury/metadata/sat/DefaultSatSolverTest.java
(original)
+++ maven/sandbox/trunk/mercury/src/test/java/org/apache/maven/mercury/metadata/sat/DefaultSatSolverTest.java
Thu Jun  5 10:56:35 2008
@@ -16,24 +16,34 @@
   DefaultSatSolver ss;
   String title;
   List< List<ArtifactMetadata> > or;
+  SatConstraint constraint; 
   
   //----------------------------------------------------------------------
   protected void setUp()
   throws Exception
   {
     super.setUp();
+    
+    or = new ArrayList< List<ArtifactMetadata> >(8);
+
   }
   //----------------------------------------------------------------------
   public void testContext()
   throws SatException
   {
     ss = (DefaultSatSolver) DefaultSatSolver.create(3);
+
+    ss.addPivot(SatHelper.createList("t:b:1","t:b:2" ));
+    
+    assert ss.context != null : "created solver has a null context";
+    assert ss.context.varCount == 2 : "expected 2 variables in the context, but found "+ss.context.varCount;
+
     or = new ArrayList< List<ArtifactMetadata> >(1);
+
     or.add( SatHelper.createList("t:a:1","t:b:1" ) );
     ss.addOrGroup(or);
     
-    assert ss.context != null : "created solver has a null context";
-    assert ss.context.varCount == 2 : "expected 2 variables in the context, but found "+ss.context.varCount;
+    assert ss.context.varCount == 3 : "expected 3 variables in the context, but found "+ss.context.varCount;
 
     or = new ArrayList< List<ArtifactMetadata> >(1);
     or.add( SatHelper.createList("t:a:1","t:b:2" ) );
@@ -42,65 +52,115 @@
     assert ss.context.varCount == 3 : "expected 3 variables in the context, but found "+ss.context.varCount;
   }
   //----------------------------------------------------------------------
-  public void testSimpleResolution()
+  public void testSimplestResolution()
   throws SatException
   {
-    title = "simple 3-node tree";
-    ss = (DefaultSatSolver) DefaultSatSolver.create(6);
+    title = "simplest 3-node tree";
+    System.out.println("\n"+title+"\n");
+
+    ss = (DefaultSatSolver) DefaultSatSolver.create(3);
+
+    constraint = ss.addPivot( SatHelper.createList("t:b:1","t:b:2") );
+    System.out.println("Pivot: "+constraint.toString() );
+
+    or.add( SatHelper.createList("t:a:1","t:b:1") );
+    or.add( SatHelper.createList("t:a:1","t:b:2") );
+    constraint = ss.addOrGroup(or);
+    System.out.println("Constraint: "+constraint.toString() );    
     
-    or = new ArrayList< List<ArtifactMetadata> >(3);
+    System.out.println("\nContext: "+ss.context.toString()+"\n" );
+
+    List<ArtifactMetadata> res = ss.solve();
+System.out.print("model: " );
+int m[] = ss.solver.model();
+for( int i=0; i<m.length; i++ )
+  System.out.print(" "+m[i]);
+System.out.println("");
+
+    assert res != null : "Failed to solve "+title;
     
-    ss.addPivot( SatHelper.createList("t:b:1","t:b:2","t:b:3") );
+    System.out.print("Result:");
+    for( ArtifactMetadata md : res )
+    {
+      System.out.print(" "+md);
+    }
+    System.out.println("");
+
+    assert res.size() == 2 : "result contains "+res.size()+" artifacts instead of 2";
+  }
+  //----------------------------------------------------------------------
+  public void testSimpleResolution()
+  throws SatException
+  {
+    title = "simple 4-node tree";
+    System.out.println("\n"+title+"\n");
+
+    ss = (DefaultSatSolver) DefaultSatSolver.create(4);
 
+    constraint = ss.addPivot( SatHelper.createList("t:b:1","t:b:2","t:b:3") );
+    System.out.println("Pivot: "+constraint.toString() );
+    
     or.add( SatHelper.createList("t:a:1","t:b:1") );
     or.add( SatHelper.createList("t:a:1","t:b:2") );
     or.add( SatHelper.createList("t:a:1","t:b:3") );
-    ss.addOrGroup(or);
+    constraint = ss.addOrGroup(or);
+    System.out.println("Constraint: "+constraint.toString() );    
+    
+    System.out.println("\nContext: "+ss.context.toString()+"\n" );
 
     List<ArtifactMetadata> res = ss.solve();
+System.out.print("model: " );
+int m[] = ss.solver.model();
+for( int i=0; i<m.length; i++ )
+  System.out.print(" "+m[i]);
+System.out.println("");
+
     
     assert res != null : "Failed to solve "+title;
-    assert res.size() == 2 : "result contains "+res.size()+" artifacts instead of 2";
     
-    if( res != null )
+    System.out.print("Result:");
+    for( ArtifactMetadata md : res )
     {
-      System.out.println("\nResult:");
-      for( ArtifactMetadata md : res )
-      {
-        System.out.print(" "+md);
-      }
+      System.out.print(" "+md);
     }
+    System.out.println("");
+
+    assert res.size() == 2 : "result contains "+res.size()+" artifacts instead of 2";
   }
   //----------------------------------------------------------------------
-  public void testResolution()
+  public void testClassicResolution()
   throws SatException
   {
-    title = "simple 2 ranges tree";
-    System.out.println("\n"+title);
+    title = "Classical ranges tree";
+    System.out.println("\n"+title+"\n");
     
     ss = (DefaultSatSolver) DefaultSatSolver.create(6);
+
+    constraint = ss.addPivot( SatHelper.createList("t:b:1","t:b:2","t:b:3") );
+    System.out.println("Pivot: "+constraint.toString() );
     
-    or = new ArrayList< List<ArtifactMetadata> >(3);
-    
-    ss.addPivot( SatHelper.createList("t:b:1","t:b:2","t:b:3") );
+    constraint = ss.addPivot( SatHelper.createList("t:c:1","t:c:2") );
+    System.out.println("Pivot: "+constraint.toString() );
 
     or.add( SatHelper.createList("t:a:1","t:b:1") );
     or.add( SatHelper.createList("t:a:1","t:b:2") );
     or.add( SatHelper.createList("t:a:1","t:b:3") );
-    ss.addOrGroup(or);
+    constraint = ss.addOrGroup(or);
+    System.out.println("Constraint: "+constraint.toString() );    
 
     or.clear();
 
-    ss.addPivot( SatHelper.createList("t:c:1","t:c:2") );
-
     or.add( SatHelper.createList("t:a:1","t:c:1","t:b:1") );
     or.add( SatHelper.createList("t:a:1","t:c:2","t:b:2") );
     or.add( SatHelper.createList("t:a:1","t:c:2","t:b:3") );
-    ss.addOrGroup(or);
-    
+    constraint = ss.addOrGroup(or);
+    System.out.println("Constraint: "+constraint.toString() );    
+
     System.out.println( "Context: "+ss.context.toString() );
 
     List<ArtifactMetadata> res = ss.solve();
+    if(res==null)
+      System.out.println("\n"+title+" unsatified");
     
     assert res != null : "Failed to solve "+title;
 //    assert res.size() == 2 : "result contains "+res.size()+" artifacts instead of 2";
@@ -112,5 +172,16 @@
     }
   }
   //----------------------------------------------------------------------
+  public void testT()
+  {
+   for( int i=0; i<2; i++)
+     for( int j=0; j<2; j++)
+       System.out.println(i+", "+j+" -> "+f(i,j));
+  }
+  private int f( int a, int b )
+  {
+    return -a + b;
+  }
+  //----------------------------------------------------------------------
   //----------------------------------------------------------------------
 }

Modified: maven/sandbox/trunk/mercury/src/test/java/org/apache/maven/mercury/metadata/sat/SatFeedTest.java
URL: http://svn.apache.org/viewvc/maven/sandbox/trunk/mercury/src/test/java/org/apache/maven/mercury/metadata/sat/SatFeedTest.java?rev=663678&r1=663677&r2=663678&view=diff
==============================================================================
--- maven/sandbox/trunk/mercury/src/test/java/org/apache/maven/mercury/metadata/sat/SatFeedTest.java
(original)
+++ maven/sandbox/trunk/mercury/src/test/java/org/apache/maven/mercury/metadata/sat/SatFeedTest.java
Thu Jun  5 10:56:35 2008
@@ -323,12 +323,12 @@
   throws ContradictionException, TimeoutException
   {
     //             x3
-    //        x2 <or
-    //        /    x4 
-    //       /      \
-    //      /        x5 - x6
-    //     /          \ or
-    //    /            +- x7
+    //         x2 <or
+    //         /    x4 
+    //        /      \
+    //       /        x5 - x6
+    //      /          \ or
+    //     /            +- x7
     // x1 <
     //     \ x8 - x7
     String title = "really real problem";
@@ -359,14 +359,15 @@
       );
 
     // x1 + x2 + x3 >= 3 OR x1 + x2 + x4 + x5 + x6 >= 5 OR x1 + x2 + x4 + x5 + x7 >=
5
-    //  x1 + x2 + x3 >= 3 OR x1 + x2 + x4 + x5 + x6 +x7 >= 5
-    //  x1 + x2 + x3 + x4 + x5 + x6 +x7 >= 5
+    //  3x1 + 3x2 + x3 >= 3 OR x1 + x2 + x4 + x5 + x6 +x7 >= 5
+    //  3x1 + 3x2 + x3 + 2x4 + 2x5 + x6 +x7 >= 11
     pbSolver.addPseudoBoolean(
         SatHelper.getSmallOnes( 1, 2, 3, 4, 5, 6, 7 )
-      , SatHelper.getBigOnes( 7 )
-      , true, new BigInteger("5")
+      , SatHelper.getBigOnes  ( 3, 3, 1, 2, 2, 1, 1 )
+      , true, new BigInteger("11")
       );
 
+    // second "must have" branch
     // x1 + x8 + x7 >= 3
     pbSolver.addPseudoBoolean(
         SatHelper.getSmallOnes( 1, 8, 7 )
@@ -377,6 +378,8 @@
     boolean satisfiable = pbSolver.isSatisfiable();
     assert satisfiable : "Cannot find a solution to "+title+" problem";
     
+    showRes( title );
+    
     assert pbSolver.model(1)
          && pbSolver.model(2)
          && pbSolver.model(4)
@@ -386,6 +389,54 @@
     : "x1 & x2 & x4 & x5 & x7 & x8 should be true";
      assert !pbSolver.model(3) : "x3 should be false";
      assert !pbSolver.model(6) : "x6 should be false";
+  }
+  //---------------------------------------------------------------
+  public void testBackToDrawingBoard()
+  throws ContradictionException, TimeoutException
+  {
+    //      x2
+    // x1 <or
+    //      \   x4
+    //      x3 <or
+    //          x5
+    //        \- x6
+    String title = "BackToDrawingBoard";
+    pbSolver.newVar(6);
+    
+    // x2 + x3 = 1
+    pbSolver.addPseudoBoolean(
+        SatHelper.getSmallOnes( 2, 3 )
+      , SatHelper.getBigOnes(2)
+      , true, new BigInteger("1") 
+      );
+    pbSolver.addPseudoBoolean(
+        SatHelper.getSmallOnes( 2, 3 )
+      , SatHelper.getBigOnes( 2, true )
+      , true, new BigInteger("-1")
+      );
+    
+    // x4 + x5 + x6 = 1
+    pbSolver.addPseudoBoolean(
+        SatHelper.getSmallOnes( 4, 5, 6 )
+      , SatHelper.getBigOnes(3)
+      , true, new BigInteger("1") 
+      );
+    pbSolver.addPseudoBoolean(
+        SatHelper.getSmallOnes( 4, 5, 6 )
+      , SatHelper.getBigOnes( 3, true )
+      , true, new BigInteger("-1")
+      );
+
+    // x1 + x2 >= 2 OR x1 + x3 + x4 >= 3 OR x1 + x3 + x5 >= 3 OR x1 + x3 + x6 >=
3
+    // 4x1 + x2 + 2x3 + x4 + x5 + x6 >= 7
+    pbSolver.addPseudoBoolean(
+        SatHelper.getSmallOnes( 1, 2, 3, 4, 5, 6)
+      , SatHelper.getBigOnes(   5, 1, 3, 1, 1, 1 )
+      , true, new BigInteger("9")
+      );
+    
+    boolean satisfiable = pbSolver.isSatisfiable();
+    assert satisfiable : "Cannot find a solution to "+title+" problem";
     
     showRes( title );
   }



Mime
View raw message