commit 5b9f1cec9aa20c4be3af3eaf1fcde5681b0d0bc7
Author: Leszek Koltunski <leszek@koltunski.pl>
Date:   Tue Mar 28 12:58:47 2023 +0200

    Dino6 solver: pruning version done.

diff --git a/src/main/java/org/distorted/objectlib/tablebases/TBDino6.java b/src/main/java/org/distorted/objectlib/tablebases/TBDino6.java
index 9e9bd4f9..7f237b29 100644
--- a/src/main/java/org/distorted/objectlib/tablebases/TBDino6.java
+++ b/src/main/java/org/distorted/objectlib/tablebases/TBDino6.java
@@ -14,11 +14,14 @@ import static org.distorted.objectlib.main.TwistyObject.SQ3;
 import android.content.res.Resources;
 
 import org.distorted.library.type.Static3D;
+import org.distorted.objectlib.R;
 
 ///////////////////////////////////////////////////////////////////////////////////////////////////
 
-public class TBDino6 extends TablebasesAbstract
+public class TBDino6 extends TablebasesPruning
 {
+  private static final int INDEX_INVERTED = 13379863; // quats (0,10,0,10, 11,11,11,11, 0,10,0,10)
+
   private static final int[][] QUATS =
       {
           {0,2,10,8, 1,4,6,7,   11,5,9,3},
@@ -35,6 +38,8 @@ public class TBDino6 extends TablebasesAbstract
           {4,11,7,9, 8,3,2,5,   6,10,1,0}
       };
 
+  private int[][] mAngles;
+
 ///////////////////////////////////////////////////////////////////////////////////////////////////
 
   public TBDino6()
@@ -46,15 +51,20 @@ public class TBDino6 extends TablebasesAbstract
 
   public TBDino6(Resources res)
     {
-    super(res,org.distorted.objectlib.R.raw.dino_3_tablebase);
+    super(res,new int[] {R.raw.dino_3_pruning3,R.raw.dino_3_pruning4},new int[] {R.raw.dino_3_pruning10});
     }
 
 ///////////////////////////////////////////////////////////////////////////////////////////////////
 
   int[][] getBasicAngles()
     {
-    int[] tmp = {3,3,3};
-    return new int[][] { tmp,tmp,tmp,tmp };
+    if( mAngles==null )
+      {
+      int[] tmp = {3,3,3};
+      mAngles = new int[][] { tmp,tmp,tmp,tmp };
+      }
+
+    return mAngles;
     }
 
 ///////////////////////////////////////////////////////////////////////////////////////////////////
@@ -110,6 +120,42 @@ public class TBDino6 extends TablebasesAbstract
 
 ///////////////////////////////////////////////////////////////////////////////////////////////////
 // specifically for the tablebase
+///////////////////////////////////////////////////////////////////////////////////////////////////
+// two solved positions: original and mirrored (left face swapped with right)
+
+  @Override
+  int[] getSolvedIndices()
+    {
+    return new int[] {0,INDEX_INVERTED};
+    }
+
+///////////////////////////////////////////////////////////////////////////////////////////////////
+// ditto
+
+  @Override
+  boolean isSolved(int index)
+    {
+    return index==0 || index==INDEX_INVERTED;
+    }
+
+///////////////////////////////////////////////////////////////////////////////////////////////////
+// we can never really move the top-front edge, because if we do so, we would also rotate the
+// rotation axis themselves! (see getIndex() where the cubit quats are normalized so that quat[0]
+// - i.e. the front-top edge - is always 0).
+// That's why map the moves (0,2,X) to (0,0&1,-X) and (3,0,X) to (3,1&2,-X)
+
+  @Override
+  int[] newMove(int axis, int layer, int angle)
+    {
+    if( axis==0 && layer==2 ) return new int[] { axis, (1<<0)+(1<<1), angle==1 ? 1:-1};
+    if( axis==3 && layer==0 ) return new int[] { axis, (1<<1)+(1<<2), angle==1 ? 1:-1};
+
+    int maxAngle = mAngles[axis][layer];
+    angle = maxAngle-angle;
+    if( angle> 0.5f*maxAngle ) angle -= maxAngle;
+    return new int[] { axis, (1<<layer), angle };
+    }
+
 ///////////////////////////////////////////////////////////////////////////////////////////////////
 
   int getSize()
@@ -121,7 +167,35 @@ public class TBDino6 extends TablebasesAbstract
 
   int getMinScramble()
     {
-    return 9;
+    return 8;
+    }
+
+///////////////////////////////////////////////////////////////////////////////////////////////////
+
+  int[] getMidPruningLevels()
+    {
+    return new int[] {3,4};
+    }
+
+///////////////////////////////////////////////////////////////////////////////////////////////////
+
+  int[] getHighPruningLevels()
+    {
+    return new int[] {10};
+    }
+
+///////////////////////////////////////////////////////////////////////////////////////////////////
+
+  int getGodsNumber()
+    {
+    return 10;
+    }
+
+///////////////////////////////////////////////////////////////////////////////////////////////////
+
+  boolean moveCanProceed(int lastA, int lastR, int currA, int currR)
+    {
+    return (lastA!=currA) || (lastR!=currR);
     }
 
 ///////////////////////////////////////////////////////////////////////////////////////////////////
@@ -157,7 +231,7 @@ public class TBDino6 extends TablebasesAbstract
 ///////////////////////////////////////////////////////////////////////////////////////////////////
 // in-place!
 
-  private int[] getQuatsFromPerm(int[] perm)
+  public static int[] getQuatsFromPerm(int[] perm)
     {
     for(int i=0; i<12; i++)
       {
diff --git a/src/main/java/org/distorted/objectlib/tablebases/TablebasesAbstract.java b/src/main/java/org/distorted/objectlib/tablebases/TablebasesAbstract.java
index 8e783d53..eaa365e1 100644
--- a/src/main/java/org/distorted/objectlib/tablebases/TablebasesAbstract.java
+++ b/src/main/java/org/distorted/objectlib/tablebases/TablebasesAbstract.java
@@ -303,9 +303,11 @@ public abstract class TablebasesAbstract
   public void createTablebase(int maxLevel)
     {
     mTablebase = new Tablebase(mSize);
-    mTablebase.insertUnpacked(0,(byte)0);
+    int[] solved = getSolvedIndices();
+    int numSolved = solved.length;
+    for(int s : solved ) mTablebase.insertUnpacked(s,(byte)0);
 
-    int numInserted, totalInserted=1;
+    int numInserted, totalInserted=numSolved;
     byte insertingLevel = 0;
 
     android.util.Log.e("D", "creating tablebase of size "+mSize);
@@ -329,6 +331,20 @@ public abstract class TablebasesAbstract
     android.util.Log.e("D", "total Inserted: "+totalInserted);
     }
 
+///////////////////////////////////////////////////////////////////////////////////////////////////
+
+  int[] getSolvedIndices()
+    {
+    return new int[] {0};
+    }
+
+///////////////////////////////////////////////////////////////////////////////////////////////////
+
+  boolean isSolved(int index)
+    {
+    return index==0;
+    }
+
 ///////////////////////////////////////////////////////////////////////////////////////////////////
 
   public void pack()
@@ -359,29 +375,23 @@ public abstract class TablebasesAbstract
     {
     for(int[] move : moves )
       {
-      int axis = move[0];
-      int layer= move[1];
-      int angle= move[2];
-
-      int maxAngle = mAngles[axis][layer];
-      angle = maxAngle-angle;
-      if( angle> 0.5f*maxAngle ) angle -= maxAngle;
+      int[] newMove = newMove(move[0],move[1],move[2]);
 
-      move[1] = (1<<layer);
-      move[2] = angle;
+      move[0] = newMove[0];
+      move[1] = newMove[1];
+      move[2] = newMove[2];
       }
     }
 
 ///////////////////////////////////////////////////////////////////////////////////////////////////
 
-  private void addMove(ArrayList<int[]> moves, int axis, int layer, int angle)
+  int[] newMove(int axis, int layer, int angle)
     {
     int maxAngle = mAngles[axis][layer];
     angle = maxAngle-angle;
     if( angle> 0.5f*maxAngle ) angle -= maxAngle;
 
-    int[] move = new int[] { axis, (1<<layer), angle };
-    moves.add(move);
+    return new int[] { axis, (1<<layer), angle };
     }
 
 ///////////////////////////////////////////////////////////////////////////////////////////////////
@@ -439,7 +449,7 @@ public abstract class TablebasesAbstract
     int numQuats = quats.length;
     int[] tmpQuats = new int[numQuats];
 
-    while(index!=0)
+    while( !isSolved(index) )
       {
       boolean found = false;
 
@@ -477,7 +487,8 @@ public abstract class TablebasesAbstract
 
           if( ((newLevel-level+1)%3) == 0 )
             {
-            addMove(moves,ax,layer,angle);
+            int[] tmpMove = newMove(ax,layer,angle);
+            moves.add(tmpMove);
             index = childIndex;
             level = (level==0 ? 2 : (byte)(level-1));
             found = true;
@@ -534,6 +545,8 @@ public abstract class TablebasesAbstract
       }
     }
 
+///////////////////////////////////////////////////////////////////////////////////////////////////
+// TESTING
 ///////////////////////////////////////////////////////////////////////////////////////////////////
 
   public boolean test(int index)
@@ -588,59 +601,104 @@ public abstract class TablebasesAbstract
 
 ///////////////////////////////////////////////////////////////////////////////////////////////////
 
-    public void testPruning(int level)
+  public void testPruning(int level)
+    {
+    for( int supp : PruningTable.SUPPORTED )
       {
-      for( int supp : PruningTable.SUPPORTED )
-        {
-        PruningTable table = new PruningTable(mTablebase, level, supp);
-        int size = mTablebase.getSize();
+      PruningTable table = new PruningTable(mTablebase, level, supp);
+      int size = mTablebase.getSize();
 
-        StringBuilder sb = new StringBuilder();
-        int num = 0;
+      StringBuilder sb = new StringBuilder();
+      int num = 0;
 
-        for(int i=0; i<size; i++)
+      for(int i=0; i<size; i++)
+        {
+        if (table.contains(i))
           {
-          if (table.contains(i))
-            {
-            if ((num % 10) == 0) sb.append("\n");
-            num++;
-            sb.append(i);
-            sb.append(' ');
-            }
+          if ((num % 10) == 0) sb.append("\n");
+          num++;
+          sb.append(i);
+          sb.append(' ');
           }
-
-        android.util.Log.e("D", "numbers: " + sb);
         }
+
+      android.util.Log.e("D", "numbers: " + sb);
+      }
+    }
+
+///////////////////////////////////////////////////////////////////////////////////////////////////
+
+  private void printQuats(int[] quats)
+    {
+    StringBuilder sb = new StringBuilder();
+    for(int q : quats )
+      {
+      sb.append(' ');
+      sb.append(q);
       }
+    android.util.Log.e("D", "quats: "+sb);
+    }
+
+///////////////////////////////////////////////////////////////////////////////////////////////////
+
+  public void test()
+    {
+    int[] p0 = {0,5,6,10, 2,3,11,9, 1,4,7,8};
+    int[] q0 = TBDino6.getQuatsFromPerm(p0);
+    int index0 = getIndex(q0);
+    android.util.Log.e("D", "index0: "+index0);
+
+    int[] p1 = {0,3,11,6,  7,8,10,2,  1,4,9,5};
+    int[] q1 = TBDino6.getQuatsFromPerm(p1);
+    int index1 = getIndex(q1);
+    android.util.Log.e("D", "index1: "+index1);
+
+    int[] p2 = {0,3,2,1,  7,6,5,4,  8,11,10,9};
+    int[] q2 = TBDino6.getQuatsFromPerm(p2);
+    int index2 = getIndex(q2);
+    android.util.Log.e("D", "index2: "+index2);
+    }
 
 ///////////////////////////////////////////////////////////////////////////////////////////////////
 
-    private void printQuats(int[] quats)
+  private void printPerm(int index)
+    {
+    int[] perm11 = new int[11];
+    TablebaseHelpers.getEvenPermutationFromNum(perm11,index);
+    int[] perm = new int[12];
+    for(int i=1; i<12; i++) perm[i] = perm11[i-1]+1;
+
+    StringBuilder sb = new StringBuilder();
+    sb.append(index);
+    sb.append(" : ");
+
+    for(int i=0; i<12; i++)
       {
-      StringBuilder sb = new StringBuilder();
-      for(int q : quats )
-        {
-        sb.append(' ');
-        sb.append(q);
-        }
-      android.util.Log.e("D", "quats: "+sb);
+      sb.append(' ');
+      sb.append(perm[i]);
       }
+    android.util.Log.e("D", "PERM: "+sb);
+    }
 
 ///////////////////////////////////////////////////////////////////////////////////////////////////
 
-    public void test()
+  private void printQuat(int index)
+    {
+    int[] perm11 = new int[11];
+    TablebaseHelpers.getEvenPermutationFromNum(perm11,index);
+    int[] perm = new int[12];
+    for(int i=1; i<12; i++) perm[i] = perm11[i-1]+1;
+    int[] quats = TBDino6.getQuatsFromPerm(perm);
+
+    StringBuilder sb = new StringBuilder();
+    sb.append(index);
+    sb.append(" : ");
+
+    for(int i=0; i<12; i++)
       {
-      int[] q1 = {1,1,1,0,1,0,0,0, 1,0,1,0,1,0 };
-      int index1 = getIndex(q1);
-      android.util.Log.e("D", "index1: "+index1);
-
-      int[] q2 = getQuats(index1);
-      printQuats(q2);
-/*
-      int[] q2 = {0,0,3,0,4,0,0,0, 0,0,0,0,0,0 };
-      int index2 = getIndex(q2);
-      android.util.Log.e("D", "index2: "+index2);
-
- */
+      sb.append(' ');
+      sb.append(quats[i]);
       }
+    android.util.Log.e("D", "QUATS: "+sb);
+    }
 }
diff --git a/src/main/java/org/distorted/objectlib/tablebases/TablebasesPruning.java b/src/main/java/org/distorted/objectlib/tablebases/TablebasesPruning.java
index 4f682dfb..5fa99164 100644
--- a/src/main/java/org/distorted/objectlib/tablebases/TablebasesPruning.java
+++ b/src/main/java/org/distorted/objectlib/tablebases/TablebasesPruning.java
@@ -312,7 +312,7 @@ public abstract class TablebasesPruning extends TablebasesAbstract
 
         int childIndex = getIndex(tmp);
 
-        if( childIndex==0 )
+        if( isSolved(childIndex) )
           {
           solution[0][0] = childIndex;
           solution[0][1] = 0;
diff --git a/src/main/res/raw/dino_3_pruning10.db b/src/main/res/raw/dino_3_pruning10.db
new file mode 100644
index 00000000..60cb6b5c
Binary files /dev/null and b/src/main/res/raw/dino_3_pruning10.db differ
diff --git a/src/main/res/raw/dino_3_pruning3.db b/src/main/res/raw/dino_3_pruning3.db
new file mode 100644
index 00000000..1368c15b
Binary files /dev/null and b/src/main/res/raw/dino_3_pruning3.db differ
diff --git a/src/main/res/raw/dino_3_pruning4.db b/src/main/res/raw/dino_3_pruning4.db
new file mode 100644
index 00000000..ae66d535
Binary files /dev/null and b/src/main/res/raw/dino_3_pruning4.db differ
diff --git a/src/main/res/raw/dino_3_tablebase.db b/src/main/res/raw/dino_3_tablebase.db
deleted file mode 100644
index d49c7aec..00000000
Binary files a/src/main/res/raw/dino_3_tablebase.db and /dev/null differ