API tools faq
paste
Advertisement
fabriceleal

Untitled

fabriceleal
Oct 12th, 2015
82
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
C# 14.88 KB | None | 0 0
raw download clone embed print report
  1. using ClassLibrary1;
  2. using Microsoft.Z3;
  3. using System;
  4. using System.Collections.Generic;
  5. using System.Linq;
  6. using System.Text;
  7. using System.Threading.Tasks;
  8.  
  9. namespace WindowsFormsApplication11.Csp
  10. {
  11.     public class PuzzleComposer
  12.     {
  13.  
  14.  
  15.     [Flags()]
  16.     public enum SquareScalar : ulong
  17.     {
  18.         A1 = 0x1, B1 = 0x2, C1 = 0x4, D1 = 0x8,
  19.         E1 = 0x10, F1 = 0x20, G1 = 0x40, H1 = 0x80,
  20.  
  21.         A2 = 0x100, B2 = 0x200, C2 = 0x400, D2 = 0x800,
  22.         E2 = 0x1000, F2 = 0x2000, G2 = 0x4000, H2 = 0x8000,
  23.  
  24.         A3 = 0x10000, B3 = 0x20000, C3 = 0x40000, D3 = 0x80000,
  25.         E3 = 0x100000, F3 = 0x200000, G3 = 0x400000, H3 = 0x800000,
  26.  
  27.         A4 = 0x1000000, B4 = 0x2000000, C4 = 0x4000000, D4 = 0x8000000,
  28.         E4 = 0x10000000, F4 = 0x20000000, G4 = 0x40000000, H4 = 0x80000000,
  29.  
  30.         A5 = 0x100000000, B5 = 0x200000000, C5 = 0x400000000, D5 = 0x800000000,
  31.         E5 = 0x1000000000, F5 = 0x2000000000, G5 = 0x4000000000, H5 = 0x8000000000,
  32.  
  33.         A6 = 0x10000000000, B6 = 0x20000000000, C6 = 0x40000000000, D6 = 0x80000000000,
  34.         E6 = 0x100000000000, F6 = 0x200000000000, G6 = 0x400000000000, H6 = 0x800000000000,
  35.  
  36.         A7 = 0x1000000000000, B7 = 0x2000000000000, C7 = 0x4000000000000, D7 = 0x8000000000000,
  37.         E7 = 0x10000000000000, F7 = 0x20000000000000, G7 = 0x40000000000000, H7 = 0x80000000000000,
  38.  
  39.         A8 = 0x100000000000000, B8 = 0x200000000000000, C8 = 0x400000000000000, D8 = 0x800000000000000,
  40.     E8 = 0x1000000000000000, F8 = 0x2000000000000000, G8 = 0x4000000000000000, H8 = 0x8000000000000000
  41.     }
  42.  
  43.         // TODO Split in north, south attack
  44.        
  45.         public UInt64 AttackVertical(UInt64 startingSquare)
  46.         {
  47.             int file, rank;
  48.             PieceSquareSpec.BreakSquare((SquareScalar)startingSquare, out file, out rank);
  49.             var spec = (ulong)PieceSquareSpec.Files[file];
  50.             return spec & ~(startingSquare);
  51.         }
  52.  
  53.         // TODO Split in west, east attack
  54.  
  55.         public UInt64 AttackHorizontal(UInt64 startingSquare)
  56.         {
  57.             int file, rank;
  58.             PieceSquareSpec.BreakSquare((SquareScalar)startingSquare, out file, out rank);
  59.             var spec = (ulong)PieceSquareSpec.Ranks[rank];
  60.             return spec & ~(startingSquare);
  61.         }
  62.  
  63.         // TODO Split in north-west, north-east, south-west, south-east attack
  64.  
  65.         public UInt64 AttackDiagonals(UInt64 startingSquare)
  66.         {
  67.             UInt64 r = 0;
  68.             int centerFile, centerRank;
  69.             PieceSquareSpec.BreakSquare((SquareScalar)startingSquare, out centerFile, out centerRank);
  70.  
  71.             for (int off = 1; off < 8; ++off)
  72.             {
  73.                 var x_min = centerFile - off;
  74.                 var x_max = centerFile + off;
  75.                 var y_min = centerRank - off;
  76.                 var y_max = centerFile + off;
  77.  
  78.                 // x_min, y_min
  79.                 if (x_min >= 0 && x_min < 8 && y_min >= 0 && y_min < 8)
  80.                 {
  81.                     r |= PieceSquareSpec.MakeSquare(x_min, y_min);
  82.                 }
  83.                 // x_min, y_max
  84.                 if (x_min >= 0 && x_min < 8 && y_max >= 0 && y_max < 8)
  85.                 {
  86.                     r |= PieceSquareSpec.MakeSquare(x_min, y_max);
  87.                 }
  88.                 // x_max, y_min
  89.                 if (x_max >= 0 && x_max < 8 && y_min >= 0 && y_min < 8)
  90.                 {
  91.                     r |= PieceSquareSpec.MakeSquare(x_max, y_min);
  92.                 }
  93.                 // x_max, y_max
  94.                 if (x_max >= 0 && x_max < 8 && y_max >= 0 && y_max < 8)
  95.                 {
  96.                     r |= PieceSquareSpec.MakeSquare(x_max, y_max);
  97.                 }
  98.             }
  99.  
  100.             return r;
  101.         }
  102.  
  103.         public void Test()
  104.         {
  105.             using(var x = new Microsoft.Z3.Context())
  106.             {
  107.                 uint bitboardQueenAttacks = 0x0;
  108.                
  109.                 var bitboardSort = x.MkBitVecSort(64);
  110.  
  111.                 var piece = x.MkDatatypeSort("Piece", new[]{
  112.                     x.MkConstructor("Rook", ""),
  113.                     x.MkConstructor("Queen", ""),
  114.                     x.MkConstructor("Bishop", "")
  115.                 });
  116.                      
  117.                 var pieceRook = piece.Constructors[0];
  118.                 var pieceQueen = piece.Constructors[1];
  119.                 var pieceBishop = piece.Constructors[2];
  120.  
  121.                 var bitboard_to_piece = x.MkFuncDecl("type_of", bitboardSort, piece);
  122.  
  123.                 var f = x.MkFuncDecl("piece_bitboard_to_attacked", new Microsoft.Z3.Sort[] {
  124.                     piece,
  125.                     bitboardSort
  126.                 }, bitboardSort);
  127.  
  128.                 //x.ParseSMTLIB2String("");
  129.                 var solver = x.MkSolver();
  130.  
  131.                 //solver.Assert(x.MkEq());
  132.                 foreach (SquareScalar value in Enum.GetValues(typeof(SquareScalar)))
  133.                 {
  134.                     UInt64 bitboard = (UInt64)value;
  135.  
  136.  
  137.                     UInt64 orthogonal = AttackVertical(bitboard) | AttackHorizontal(bitboard);
  138.                     UInt64 diagonals = AttackDiagonals(bitboard);
  139.  
  140.                     // rooks
  141.  
  142.                     solver.Assert(x.MkEq(
  143.                         x.MkApp(f, pieceRook.Apply(), x.MkBV(bitboard, 64)),
  144.                         x.MkBV(orthogonal, 64)));
  145.  
  146.                     // queens
  147.  
  148.                     solver.Assert(x.MkEq(
  149.                         x.MkApp(f, pieceQueen.Apply(), x.MkBV(bitboard, 64)),
  150.                         x.MkBV(orthogonal | diagonals, 64)));
  151.  
  152.                     // bishops
  153.  
  154.                     solver.Assert(x.MkEq(
  155.                         x.MkApp(f, pieceBishop.Apply(), x.MkBV(bitboard, 64)),
  156.                         x.MkBV(diagonals, 64)));
  157.  
  158.                 }
  159.  
  160.                 //EightQueensProblem(bitboardSort, x, solver, f, pieceRook, pieceQueen, pieceBishop);
  161.                 SquaresProblem(bitboardSort, x, solver, f, pieceRook, pieceQueen, pieceBishop);
  162.  
  163.                 var status = solver.Check();
  164.                 var model = solver.Model;
  165.  
  166.                 ulong test = 0;
  167.                 foreach(var d in model.Decls)
  168.                 {
  169.                     if (d.Arity != 0) continue;
  170.                     var interpr = model.ConstInterp(d);
  171.                     System.Diagnostics.Debug.WriteLine(f.Name + " = " + interpr + " (" + string.Format("{0:X}", ulong.Parse(interpr.ToString())) + ")");
  172.  
  173.                     test |= ulong.Parse(interpr.ToString());
  174.                 }
  175.  
  176.                 System.Diagnostics.Debug.WriteLine(string.Format("{0:X}", test));
  177.  
  178.             }
  179.         }
  180.  
  181.         private void SquaresProblem(Sort bitboardSort, Context x, Solver solver, FuncDecl f, FuncDecl pieceRook, FuncDecl pieceQueen, FuncDecl pieceBishop)
  182.         {
  183.             var p0 = x.MkConst("piece0", bitboardSort);
  184.             var p1 = x.MkConst("piece1", bitboardSort);
  185.             var p2 = x.MkConst("piece2", bitboardSort);
  186.  
  187.             // pieces cant overlap
  188.             solver.Assert(x.MkDistinct(p0, p1, p2));
  189.  
  190.             var p0Attacked = x.MkApp(f, pieceQueen.Apply(), p0);
  191.             var p1Attacked = x.MkApp(f, pieceRook.Apply(), p1);
  192.             var p2Attacked = x.MkApp(f, pieceBishop.Apply(), p2);
  193.  
  194.             // pieces must not be 0
  195.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p0)));
  196.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p1)));
  197.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p2)));
  198.  
  199.             // the set of attacked squares by an arbitrary piece must not equal 0
  200.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p0Attacked)));
  201.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p1Attacked)));
  202.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p2Attacked)));
  203.  
  204.             // the piece bitboard must have one and only one bit set
  205.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)p0, x.MkBVSub((Microsoft.Z3.BitVecExpr)p0, x.MkBV(1, 64)))));
  206.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)p1, x.MkBVSub((Microsoft.Z3.BitVecExpr)p1, x.MkBV(1, 64)))));
  207.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)p2, x.MkBVSub((Microsoft.Z3.BitVecExpr)p2, x.MkBV(1, 64)))));
  208.  
  209.  
  210.             // place a rook queen and bishop in such a way that
  211.             // the square a1 is attacked 3 times
  212.             // the square h1 is attacked 2 times
  213.             // the square f4 is attacked 1 time
  214.  
  215.             var checkA1_0 = x.MkITE(x.MkEq(x.MkBV(1, 64), x.MkBVAND((BitVecExpr)p0Attacked, x.MkBV((ulong)SquareScalar.A1, 64))), x.MkInt(1), x.MkInt(0));
  216.             var checkA1_1 = x.MkITE(x.MkEq(x.MkBV(1, 64), x.MkBVAND((BitVecExpr)p1Attacked, x.MkBV((ulong)SquareScalar.A1, 64))), x.MkInt(1), x.MkInt(0));
  217.             var checkA1_2 = x.MkITE(x.MkEq(x.MkBV(1, 64), x.MkBVAND((BitVecExpr)p2Attacked, x.MkBV((ulong)SquareScalar.A1, 64))), x.MkInt(1), x.MkInt(0));
  218.  
  219.             solver.Assert(x.MkEq(x.MkInt(3), x.MkAdd((ArithExpr)checkA1_0, (ArithExpr)checkA1_1, (ArithExpr)checkA1_2)));
  220.  
  221.             // TODO pieces cant be in each others way!!!
  222.            
  223.  
  224.         }
  225.  
  226.         private void EightQueensProblem(Sort bitboardSort, Context x, Solver solver, FuncDecl f, FuncDecl pieceRook, FuncDecl pieceQueen, FuncDecl pieceBishop)
  227.         {
  228.  
  229.             var p0 = x.MkConst("piece0", bitboardSort);
  230.             var p1 = x.MkConst("piece1", bitboardSort);
  231.             var p2 = x.MkConst("piece2", bitboardSort);
  232.             var p3 = x.MkConst("piece3", bitboardSort);
  233.             var p4 = x.MkConst("piece4", bitboardSort);
  234.             var p5 = x.MkConst("piece5", bitboardSort);
  235.             var p6 = x.MkConst("piece6", bitboardSort);
  236.             var p7 = x.MkConst("piece7", bitboardSort);
  237.  
  238.             // pieces cant overlap
  239.             solver.Assert(x.MkDistinct(p0, p1, p2, p3, p4, p5, p6, p7));
  240.  
  241.             // pieces must not be 0
  242.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p0)));
  243.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p1)));
  244.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p2)));
  245.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p3)));
  246.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p4)));
  247.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p5)));
  248.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p6)));
  249.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p7)));
  250.  
  251.             // the set of attacked squares by an arbitrary piece must not equal 0
  252.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), x.MkApp(f, pieceQueen.Apply(), p0))));
  253.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), x.MkApp(f, pieceQueen.Apply(), p1))));
  254.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), x.MkApp(f, pieceQueen.Apply(), p2))));
  255.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), x.MkApp(f, pieceQueen.Apply(), p3))));
  256.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), x.MkApp(f, pieceQueen.Apply(), p4))));
  257.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), x.MkApp(f, pieceQueen.Apply(), p5))));
  258.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), x.MkApp(f, pieceQueen.Apply(), p6))));
  259.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), x.MkApp(f, pieceQueen.Apply(), p7))));
  260.  
  261.             // the piece bitboard must have one and only one bit set
  262.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)p0, x.MkBVSub((Microsoft.Z3.BitVecExpr)p0, x.MkBV(1, 64)))));
  263.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)p1, x.MkBVSub((Microsoft.Z3.BitVecExpr)p1, x.MkBV(1, 64)))));
  264.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)p2, x.MkBVSub((Microsoft.Z3.BitVecExpr)p2, x.MkBV(1, 64)))));
  265.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)p3, x.MkBVSub((Microsoft.Z3.BitVecExpr)p3, x.MkBV(1, 64)))));
  266.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)p4, x.MkBVSub((Microsoft.Z3.BitVecExpr)p4, x.MkBV(1, 64)))));
  267.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)p5, x.MkBVSub((Microsoft.Z3.BitVecExpr)p5, x.MkBV(1, 64)))));
  268.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)p6, x.MkBVSub((Microsoft.Z3.BitVecExpr)p6, x.MkBV(1, 64)))));
  269.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)p7, x.MkBVSub((Microsoft.Z3.BitVecExpr)p7, x.MkBV(1, 64)))));
  270.  
  271.             Microsoft.Z3.Expr expr;
  272.             Microsoft.Z3.Expr expr1;
  273.             {
  274.                 expr = x.MkBVOR(
  275.                         (Microsoft.Z3.BitVecExpr)p0,
  276.                         (Microsoft.Z3.BitVecExpr)p1);
  277.  
  278.                 expr = x.MkBVOR(
  279.                     (Microsoft.Z3.BitVecExpr)expr,
  280.                     (Microsoft.Z3.BitVecExpr)p2);
  281.  
  282.                 expr = x.MkBVOR(
  283.                     (Microsoft.Z3.BitVecExpr)expr,
  284.                     (Microsoft.Z3.BitVecExpr)p3);
  285.  
  286.                 expr = x.MkBVOR(
  287.                     (Microsoft.Z3.BitVecExpr)expr,
  288.                     (Microsoft.Z3.BitVecExpr)p4);
  289.  
  290.                 expr = x.MkBVOR(
  291.                     (Microsoft.Z3.BitVecExpr)expr,
  292.                     (Microsoft.Z3.BitVecExpr)p5);
  293.  
  294.                 expr = x.MkBVOR(
  295.                     (Microsoft.Z3.BitVecExpr)expr,
  296.                     (Microsoft.Z3.BitVecExpr)p6);
  297.  
  298.                 expr = x.MkBVOR(
  299.                     (Microsoft.Z3.BitVecExpr)expr,
  300.                     (Microsoft.Z3.BitVecExpr)p7);
  301.             }
  302.             {
  303.                 expr1 = x.MkBVOR(
  304.                     (Microsoft.Z3.BitVecExpr)x.MkApp(f, pieceQueen.Apply(), p0),
  305.                     (Microsoft.Z3.BitVecExpr)x.MkApp(f, pieceQueen.Apply(), p1));
  306.  
  307.                 expr1 = x.MkBVOR(
  308.                     (Microsoft.Z3.BitVecExpr)expr1,
  309.                     (Microsoft.Z3.BitVecExpr)x.MkApp(f, pieceQueen.Apply(), p2));
  310.  
  311.                 expr1 = x.MkBVOR(
  312.                     (Microsoft.Z3.BitVecExpr)expr1,
  313.                     (Microsoft.Z3.BitVecExpr)x.MkApp(f, pieceQueen.Apply(), p3));
  314.  
  315.                 expr1 = x.MkBVOR(
  316.                     (Microsoft.Z3.BitVecExpr)expr1,
  317.                     (Microsoft.Z3.BitVecExpr)x.MkApp(f, pieceQueen.Apply(), p4));
  318.  
  319.                 expr1 = x.MkBVOR(
  320.                     (Microsoft.Z3.BitVecExpr)expr1,
  321.                     (Microsoft.Z3.BitVecExpr)x.MkApp(f, pieceQueen.Apply(), p5));
  322.  
  323.                 expr1 = x.MkBVOR(
  324.                     (Microsoft.Z3.BitVecExpr)expr1,
  325.                     (Microsoft.Z3.BitVecExpr)x.MkApp(f, pieceQueen.Apply(), p6));
  326.  
  327.                 expr1 = x.MkBVOR(
  328.                     (Microsoft.Z3.BitVecExpr)expr1,
  329.                     (Microsoft.Z3.BitVecExpr)x.MkApp(f, pieceQueen.Apply(), p7));
  330.  
  331.  
  332.             }
  333.  
  334.             // pieces dont attack one another
  335.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)expr, (Microsoft.Z3.BitVecExpr)expr1)));
  336.  
  337.         }
  338.  
  339.     }
  340. }
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!