API tools faq
paste
Advertisement
fabriceleal

Untitled

fabriceleal
Oct 26th, 2015
73
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
C# 24.65 KB | None | 0 0
raw download clone embed print report
  1. using ClassLibrary1;
  2. using ClassLibrary3;
  3. using Microsoft.Z3;
  4. using System;
  5. using System.Collections.Generic;
  6. using System.Linq;
  7. using System.Text;
  8. using System.Threading.Tasks;
  9.  
  10. namespace WindowsFormsApplication11.Csp
  11. {
  12.     public class PuzzleComposer
  13.     {
  14.     [Flags()]
  15.     public enum SquareScalar : ulong
  16.     {
  17.         A1 = 0x1, B1 = 0x2, C1 = 0x4, D1 = 0x8,
  18.         E1 = 0x10, F1 = 0x20, G1 = 0x40, H1 = 0x80,
  19.  
  20.         A2 = 0x100, B2 = 0x200, C2 = 0x400, D2 = 0x800,
  21.         E2 = 0x1000, F2 = 0x2000, G2 = 0x4000, H2 = 0x8000,
  22.  
  23.         A3 = 0x10000, B3 = 0x20000, C3 = 0x40000, D3 = 0x80000,
  24.         E3 = 0x100000, F3 = 0x200000, G3 = 0x400000, H3 = 0x800000,
  25.  
  26.         A4 = 0x1000000, B4 = 0x2000000, C4 = 0x4000000, D4 = 0x8000000,
  27.         E4 = 0x10000000, F4 = 0x20000000, G4 = 0x40000000, H4 = 0x80000000,
  28.  
  29.         A5 = 0x100000000, B5 = 0x200000000, C5 = 0x400000000, D5 = 0x800000000,
  30.         E5 = 0x1000000000, F5 = 0x2000000000, G5 = 0x4000000000, H5 = 0x8000000000,
  31.  
  32.         A6 = 0x10000000000, B6 = 0x20000000000, C6 = 0x40000000000, D6 = 0x80000000000,
  33.         E6 = 0x100000000000, F6 = 0x200000000000, G6 = 0x400000000000, H6 = 0x800000000000,
  34.  
  35.         A7 = 0x1000000000000, B7 = 0x2000000000000, C7 = 0x4000000000000, D7 = 0x8000000000000,
  36.         E7 = 0x10000000000000, F7 = 0x20000000000000, G7 = 0x40000000000000, H7 = 0x80000000000000,
  37.  
  38.         A8 = 0x100000000000000, B8 = 0x200000000000000, C8 = 0x400000000000000, D8 = 0x800000000000000,
  39.         E8 = 0x1000000000000000, F8 = 0x2000000000000000, G8 = 0x4000000000000000, H8 = 0x8000000000000000
  40.     }
  41.        
  42.         public void Test()
  43.         {
  44.             using(var x = new Microsoft.Z3.Context())
  45.             {
  46.                 uint bitboardQueenAttacks = 0x0;
  47.                
  48.                 var bitboardSort = x.MkBitVecSort(64);
  49.  
  50.                 var piece = x.MkDatatypeSort("Piece", new[]{
  51.                     x.MkConstructor("Queen", ""),
  52.                     x.MkConstructor("Rook", ""),                    
  53.                     x.MkConstructor("Bishop", ""),
  54.                     x.MkConstructor("Knight", "")
  55.                 });
  56.  
  57.                 var pieceQueen = piece.Constructors[0];
  58.                 var pieceRook = piece.Constructors[1];                
  59.                 var pieceBishop = piece.Constructors[2];
  60.                 var pieceKnight = piece.Constructors[3];
  61.  
  62.                 var bitboard_to_piece = x.MkFuncDecl("type_of", bitboardSort, piece);
  63.  
  64.                 var f = x.MkFuncDecl("piece_bitboard_to_attacked", new Microsoft.Z3.Sort[] {
  65.                     piece,
  66.                     bitboardSort
  67.                 }, bitboardSort);
  68.  
  69.                 //x.ParseSMTLIB2String("");
  70.                 var solver = x.MkSimpleSolver(); // Solver();
  71.  
  72.                 //solver.Assert(x.MkEq());
  73.                 foreach (SquareScalar value in Enum.GetValues(typeof(SquareScalar)))
  74.                 {
  75.                     UInt64 bitboard = (UInt64)value;
  76.  
  77.  
  78.                     UInt64 queens = PositionWrapper.AttackedSquares(ClassLibrary3.PieceSpec.Queen, bitboard, bitboard);
  79.                     UInt64 orthogonal = PositionWrapper.AttackedSquares(ClassLibrary3.PieceSpec.Rook, bitboard, bitboard);
  80.                     UInt64 diagonals = PositionWrapper.AttackedSquares(ClassLibrary3.PieceSpec.Bishop, bitboard, bitboard);
  81.                     UInt64 knights = PositionWrapper.AttackedSquares(ClassLibrary3.PieceSpec.Knight, bitboard, bitboard);
  82.  
  83.  
  84.                     var bvPiecePos = x.MkBV(bitboard, 64);
  85.                    
  86.                     // rooks
  87.                     solver.Assert(x.MkEq(
  88.                         x.MkApp(f, pieceRook.Apply(), bvPiecePos),
  89.                         x.MkBV(orthogonal, 64)));
  90.  
  91.                     // queens
  92.                     solver.Assert(x.MkEq(
  93.                         x.MkApp(f, pieceQueen.Apply(), bvPiecePos),
  94.                         x.MkBV(queens, 64)));
  95.  
  96.                     // bishops
  97.                     solver.Assert(x.MkEq(
  98.                         x.MkApp(f, pieceBishop.Apply(), bvPiecePos),
  99.                         x.MkBV(diagonals, 64)));
  100.  
  101.                     // knights
  102.                     solver.Assert(x.MkEq(
  103.                         x.MkApp(f, pieceKnight.Apply(), bvPiecePos),
  104.                         x.MkBV(knights, 64)));
  105.  
  106.                 }
  107.  
  108.                 //EightQueensProblem(bitboardSort, x, solver, f, pieceRook, pieceQueen, pieceBishop);
  109.                 var status = SquaresProblem(bitboardSort, x, ref solver, f, pieceRook, pieceQueen, pieceBishop, pieceKnight);
  110.                              
  111.  
  112.                 if (status != Status.SATISFIABLE) return;
  113.  
  114.                 // var status = solver.Check();
  115.                 var model = solver.Model;
  116.  
  117.                 ulong piece0 = 0, piece1 = 0, piece2 = 0, piece3 = 0;
  118.  
  119.                 ulong test = 0;
  120.                 foreach(var d in model.Decls)
  121.                 {
  122.                     if (d.Arity != 0) continue;
  123.                     var interpr = model.ConstInterp(d);
  124.  
  125.                     System.Diagnostics.Debug.WriteLine(d.Name + " = " + interpr + " (" + string.Format("{0:X}", ulong.Parse(interpr.ToString())) + ")");
  126.  
  127.                     if (d.Name + "" == "piece0")
  128.                     {
  129.                         piece0 = ulong.Parse(interpr.ToString());
  130.                     }
  131.                     else if (d.Name + "" == "piece1")
  132.                     {
  133.                         piece1 = ulong.Parse(interpr.ToString());
  134.                     }
  135.                     else if (d.Name + "" == "piece2")
  136.                     {
  137.                         piece2 = ulong.Parse(interpr.ToString());
  138.                     }
  139.                     else if (d.Name + "" == "piece3")
  140.                     {
  141.                         piece3 = ulong.Parse(interpr.ToString());
  142.                     }
  143.  
  144.                    
  145.                 }
  146.  
  147.                 test = piece0 | piece1 | piece2 | piece3;
  148.                 System.Diagnostics.Debug.WriteLine(string.Format("{0:X}", test));
  149.  
  150.                 int file, rank;
  151.                 //GameState gm = GameState.Clean;
  152.                 var gm = new MutableGameState();
  153.  
  154.                 ClassLibrary1.PieceSquareSpec.BreakSquare((SquareScalar)piece0, out file, out rank);
  155.                 gm.AddPieceAt(file, rank, (int)kind.queen + (int)color.white);
  156.  
  157.                 ClassLibrary1.PieceSquareSpec.BreakSquare((SquareScalar)piece1, out file, out rank);
  158.                 gm.AddPieceAt(file, rank, (int)kind.rook + (int)color.white);
  159.  
  160.                 ClassLibrary1.PieceSquareSpec.BreakSquare((SquareScalar)piece2, out file, out rank);
  161.                 gm.AddPieceAt(file, rank, (int)kind.bishop + (int)color.white);
  162.  
  163.                 ClassLibrary1.PieceSquareSpec.BreakSquare((SquareScalar)piece3, out file, out rank);
  164.                 gm.AddPieceAt(file, rank, (int)kind.knight + (int)color.white);
  165.  
  166.                 var gmState = GameState.FromIGameState(gm);
  167.  
  168.                 //var y = new NewGame(gmState);
  169.                 //Main.OpenForm(y);
  170.  
  171.                 var frm = new FormBoardEditor(gmState);              
  172.                 frm.ShowDialog();
  173.             }
  174.         }
  175.  
  176.         private Status SquaresProblem(Sort bitboardSort, Context x, ref Solver solver, FuncDecl f, FuncDecl pieceRook, FuncDecl pieceQueen, FuncDecl pieceBishop, FuncDecl pieceKnight)
  177.         {
  178.             BitVecExpr p0 = (BitVecExpr)x.MkConst("piece0", bitboardSort);
  179.             BitVecExpr p1 = (BitVecExpr)x.MkConst("piece1", bitboardSort);
  180.             BitVecExpr p2 = (BitVecExpr)x.MkConst("piece2", bitboardSort);
  181.             BitVecExpr p3 = (BitVecExpr)x.MkConst("piece3", bitboardSort);
  182.  
  183.             // pieces cant overlap
  184.             solver.Assert(x.MkDistinct(p0, p1, p2, p3));
  185.  
  186.             BitVecExpr p0Attacked = (BitVecExpr)x.MkApp(f, pieceQueen.Apply(), p0);
  187.             BitVecExpr p1Attacked = (BitVecExpr)x.MkApp(f, pieceRook.Apply(), p1);
  188.             BitVecExpr p2Attacked = (BitVecExpr)x.MkApp(f, pieceBishop.Apply(), p2);
  189.             BitVecExpr p3Attacked = (BitVecExpr)x.MkApp(f, pieceKnight.Apply(), p3);
  190.  
  191.             // pieces must not be 0
  192.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p0)));
  193.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p1)));
  194.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p2)));
  195.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p3)));
  196.  
  197.             // the set of attacked squares by an arbitrary piece must not equal 0
  198.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p0Attacked)));
  199.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p1Attacked)));
  200.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p2Attacked)));
  201.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p3Attacked)));
  202.  
  203.             // the piece bitboard must have one and only one bit set
  204.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND(p0, x.MkBVSub(p0, x.MkBV(1, 64)))));
  205.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND(p1, x.MkBVSub(p1, x.MkBV(1, 64)))));
  206.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND(p2, x.MkBVSub(p2, x.MkBV(1, 64)))));
  207.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND(p3, x.MkBVSub(p3, x.MkBV(1, 64)))));
  208.  
  209.             // pieces and squares cant overlap
  210.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND(
  211.                     x.MkBV((ulong)(SquareScalar.E1 | SquareScalar.E5 | SquareScalar.H2), 64),
  212.                     x.MkBVOR(x.MkBVOR(x.MkBVOR(p0, p1), p2), p3)
  213.                 )));
  214.  
  215.             // place a rook queen and bishop in such a way that
  216.             // the square a1 is attacked 3 times
  217.             // the square h1 is attacked 2 times
  218.             // the square f4 is attacked 1 time
  219.  
  220.             //foreach(var square in squaresSpec)
  221.             //{
  222.  
  223.             //}
  224.  
  225.             var checkA1_0 = x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.E1, 64), x.MkBVAND(p0Attacked, x.MkBV((ulong)SquareScalar.E1, 64))), x.MkInt(1), x.MkInt(0));
  226.             var checkA1_1 = x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.E1, 64), x.MkBVAND(p1Attacked, x.MkBV((ulong)SquareScalar.E1, 64))), x.MkInt(1), x.MkInt(0));
  227.             var checkA1_2 = x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.E1, 64), x.MkBVAND(p2Attacked, x.MkBV((ulong)SquareScalar.E1, 64))), x.MkInt(1), x.MkInt(0));
  228.             var checkA1_3 = x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.E1, 64), x.MkBVAND(p3Attacked, x.MkBV((ulong)SquareScalar.E1, 64))), x.MkInt(1), x.MkInt(0));
  229.  
  230.             var checkH1_0 = x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.E5, 64), x.MkBVAND(p0Attacked, x.MkBV((ulong)SquareScalar.E5, 64))), x.MkInt(1), x.MkInt(0));
  231.             var checkH1_1 = x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.E5, 64), x.MkBVAND(p1Attacked, x.MkBV((ulong)SquareScalar.E5, 64))), x.MkInt(1), x.MkInt(0));
  232.             var checkH1_2 = x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.E5, 64), x.MkBVAND(p2Attacked, x.MkBV((ulong)SquareScalar.E5, 64))), x.MkInt(1), x.MkInt(0));
  233.             var checkH1_3 = x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.E5, 64), x.MkBVAND(p3Attacked, x.MkBV((ulong)SquareScalar.E5, 64))), x.MkInt(1), x.MkInt(0));
  234.  
  235.             var checkF4_0 = x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.H2, 64), x.MkBVAND(p0Attacked, x.MkBV((ulong)SquareScalar.H2, 64))), x.MkInt(1), x.MkInt(0));
  236.             var checkF4_1 = x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.H2, 64), x.MkBVAND(p1Attacked, x.MkBV((ulong)SquareScalar.H2, 64))), x.MkInt(1), x.MkInt(0));
  237.             var checkF4_2 = x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.H2, 64), x.MkBVAND(p2Attacked, x.MkBV((ulong)SquareScalar.H2, 64))), x.MkInt(1), x.MkInt(0));
  238.             var checkF4_3 = x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.H2, 64), x.MkBVAND(p3Attacked, x.MkBV((ulong)SquareScalar.H2, 64))), x.MkInt(1), x.MkInt(0));
  239.  
  240.             solver.Assert(x.MkEq(x.MkInt(3), x.MkAdd((ArithExpr)checkA1_0, (ArithExpr)checkA1_1, (ArithExpr)checkA1_2, (ArithExpr)checkA1_3)));
  241.             solver.Assert(x.MkEq(x.MkInt(2), x.MkAdd((ArithExpr)checkH1_0, (ArithExpr)checkH1_1, (ArithExpr)checkH1_2, (ArithExpr)checkH1_3)));
  242.             solver.Assert(x.MkEq(x.MkInt(1), x.MkAdd((ArithExpr)checkF4_0, (ArithExpr)checkF4_1, (ArithExpr)checkF4_2, (ArithExpr)checkF4_3)));
  243.  
  244.             while (true)
  245.             {
  246.                 // get next pseudo solution
  247.                 var status = solver.Check();
  248.  
  249.                 // None???
  250.                 if (status != Status.SATISFIABLE)
  251.                 {
  252.                     return status;
  253.                 }
  254.  
  255.                 UInt64 queen = 0;
  256.                 UInt64 rook = 0;
  257.                 UInt64 bishop = 0;
  258.                 UInt64 knight = 0;
  259.  
  260.                 foreach (var d in solver.Model.Decls)
  261.                 {
  262.                     if (d.Arity != 0) continue;
  263.                     var interpr = solver.Model.ConstInterp(d);
  264.  
  265.                     if (d.Name + "" == "piece0")
  266.                     {
  267.                         queen = ulong.Parse(interpr.ToString());
  268.                     }
  269.                     else if (d.Name + "" == "piece1")
  270.                     {
  271.                         rook = ulong.Parse(interpr.ToString());
  272.                     }
  273.                     else if (d.Name + "" == "piece2")
  274.                     {
  275.                         bishop = ulong.Parse(interpr.ToString());
  276.                     }
  277.                     else if (d.Name + "" == "piece3")
  278.                     {
  279.                         knight = ulong.Parse(interpr.ToString());
  280.                     }
  281.                 }
  282.  
  283.                 // get position of queen / rook / bishop
  284.  
  285.                 // get occupancy board
  286.                 var occ = queen | rook | bishop | knight;
  287.  
  288.                 // get new attacking bitboards
  289.                 var queenRealAttacked = PositionWrapper.AttackedSquares(ClassLibrary3.PieceSpec.Queen, queen, occ);
  290.                 var rookRealAttacked = PositionWrapper.AttackedSquares(ClassLibrary3.PieceSpec.Rook, rook, occ);
  291.                 var bishopRealAttacked = PositionWrapper.AttackedSquares(ClassLibrary3.PieceSpec.Bishop, bishop, occ);
  292.                 var knightRealAttacked = PositionWrapper.AttackedSquares(ClassLibrary3.PieceSpec.Knight, knight, occ);
  293.  
  294.                 // push new context for our tiny test
  295.                 solver.Push();
  296.                
  297.                 //{
  298.                     BitVecExpr p0AttackedReal = (BitVecExpr)x.MkConst("p0AttackedReal", bitboardSort);
  299.                     BitVecExpr p1AttackedReal = (BitVecExpr)x.MkConst("p1AttackedReal", bitboardSort);
  300.                     BitVecExpr p2AttackedReal = (BitVecExpr)x.MkConst("p2AttackedReal", bitboardSort);
  301.                     BitVecExpr p3AttackedReal = (BitVecExpr)x.MkConst("p3AttackedReal", bitboardSort);
  302.  
  303.                     solver.Assert(x.MkEq(p0AttackedReal, x.MkBV(queenRealAttacked, 64)));
  304.                     solver.Assert(x.MkEq(p1AttackedReal, x.MkBV(rookRealAttacked, 64)));
  305.                     solver.Assert(x.MkEq(p2AttackedReal, x.MkBV(bishopRealAttacked, 64)));
  306.                     solver.Assert(x.MkEq(p3AttackedReal, x.MkBV(knightRealAttacked, 64)));
  307.  
  308.                     ArithExpr checkA1_0_2 = (ArithExpr)x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.E1, 64), x.MkBVAND(p0AttackedReal, x.MkBV((ulong)SquareScalar.E1, 64))), x.MkInt(1), x.MkInt(0));
  309.                     ArithExpr checkA1_1_2 = (ArithExpr)x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.E1, 64), x.MkBVAND(p1AttackedReal, x.MkBV((ulong)SquareScalar.E1, 64))), x.MkInt(1), x.MkInt(0));
  310.                     ArithExpr checkA1_2_2 = (ArithExpr)x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.E1, 64), x.MkBVAND(p2AttackedReal, x.MkBV((ulong)SquareScalar.E1, 64))), x.MkInt(1), x.MkInt(0));
  311.                     ArithExpr checkA1_3_2 = (ArithExpr)x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.E1, 64), x.MkBVAND(p3AttackedReal, x.MkBV((ulong)SquareScalar.E1, 64))), x.MkInt(1), x.MkInt(0));
  312.  
  313.                     ArithExpr checkH1_0_2 = (ArithExpr)x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.E5, 64), x.MkBVAND(p0AttackedReal, x.MkBV((ulong)SquareScalar.E5, 64))), x.MkInt(1), x.MkInt(0));
  314.                     ArithExpr checkH1_1_2 = (ArithExpr)x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.E5, 64), x.MkBVAND(p1AttackedReal, x.MkBV((ulong)SquareScalar.E5, 64))), x.MkInt(1), x.MkInt(0));
  315.                     ArithExpr checkH1_2_2 = (ArithExpr)x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.E5, 64), x.MkBVAND(p2AttackedReal, x.MkBV((ulong)SquareScalar.E5, 64))), x.MkInt(1), x.MkInt(0));
  316.                     ArithExpr checkH1_3_2 = (ArithExpr)x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.E5, 64), x.MkBVAND(p3AttackedReal, x.MkBV((ulong)SquareScalar.E5, 64))), x.MkInt(1), x.MkInt(0));
  317.  
  318.                     ArithExpr checkF4_0_2 = (ArithExpr)x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.H2, 64), x.MkBVAND(p0AttackedReal, x.MkBV((ulong)SquareScalar.H2, 64))), x.MkInt(1), x.MkInt(0));
  319.                     ArithExpr checkF4_1_2 = (ArithExpr)x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.H2, 64), x.MkBVAND(p1AttackedReal, x.MkBV((ulong)SquareScalar.H2, 64))), x.MkInt(1), x.MkInt(0));
  320.                     ArithExpr checkF4_2_2 = (ArithExpr)x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.H2, 64), x.MkBVAND(p2AttackedReal, x.MkBV((ulong)SquareScalar.H2, 64))), x.MkInt(1), x.MkInt(0));
  321.                     ArithExpr checkF4_3_2 = (ArithExpr)x.MkITE(x.MkEq(x.MkBV((ulong)SquareScalar.H2, 64), x.MkBVAND(p3AttackedReal, x.MkBV((ulong)SquareScalar.H2, 64))), x.MkInt(1), x.MkInt(0));
  322.  
  323.                     solver.Assert(x.MkEq(x.MkInt(3), x.MkAdd(checkA1_0_2, checkA1_1_2, checkA1_2_2, checkA1_3_2)));
  324.                     solver.Assert(x.MkEq(x.MkInt(2), x.MkAdd(checkH1_0_2, checkH1_1_2, checkH1_2_2, checkH1_3_2)));
  325.                     solver.Assert(x.MkEq(x.MkInt(1), x.MkAdd(checkF4_0_2, checkF4_1_2, checkF4_2_2, checkF4_3_2)));
  326.  
  327.                     // Every piece must be working!
  328.                     solver.Assert(x.MkGe(x.MkAdd(checkA1_0_2, checkH1_0_2, checkF4_0_2), x.MkInt(1)));
  329.                     solver.Assert(x.MkGe(x.MkAdd(checkA1_1_2, checkH1_1_2, checkF4_1_2), x.MkInt(1)));
  330.                     solver.Assert(x.MkGe(x.MkAdd(checkA1_2_2, checkH1_2_2, checkF4_2_2), x.MkInt(1)));
  331.                     solver.Assert(x.MkGe(x.MkAdd(checkA1_3_2, checkH1_3_2, checkF4_3_2), x.MkInt(1)));
  332.  
  333.  
  334.                 //}
  335.                
  336.                 // check if they comply
  337.  
  338.                 status = solver.Check();
  339.                
  340.  
  341.                 if (status == Status.SATISFIABLE)
  342.                 {
  343.                    
  344.                     // if it complies, return
  345.                     return status;
  346.                 }
  347.  
  348.                 // if they do not, push invalid condition, and continue
  349.  
  350.                 // pop out the tiny test
  351.                 solver.Pop();
  352.                
  353.                 solver.Assert(x.MkAnd(
  354.                     x.MkNot(x.MkEq(p0, x.MkBV(queen, 64))),
  355.                     x.MkNot(x.MkEq(p1, x.MkBV(rook, 64))),
  356.                     x.MkNot(x.MkEq(p2, x.MkBV(bishop, 64))),
  357.                     x.MkNot(x.MkEq(p3, x.MkBV(knight, 64)))));
  358.  
  359.             }
  360.  
  361.             return Status.UNKNOWN;
  362.         }
  363.  
  364.         private void EightQueensProblem(Sort bitboardSort, Context x, Solver solver, FuncDecl f, FuncDecl pieceRook, FuncDecl pieceQueen, FuncDecl pieceBishop)
  365.         {
  366.  
  367.             var p0 = x.MkConst("piece0", bitboardSort);
  368.             var p1 = x.MkConst("piece1", bitboardSort);
  369.             var p2 = x.MkConst("piece2", bitboardSort);
  370.             var p3 = x.MkConst("piece3", bitboardSort);
  371.             var p4 = x.MkConst("piece4", bitboardSort);
  372.             var p5 = x.MkConst("piece5", bitboardSort);
  373.             var p6 = x.MkConst("piece6", bitboardSort);
  374.             var p7 = x.MkConst("piece7", bitboardSort);
  375.  
  376.             // pieces cant overlap
  377.             solver.Assert(x.MkDistinct(p0, p1, p2, p3, p4, p5, p6, p7));
  378.  
  379.             // pieces must not be 0
  380.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p0)));
  381.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p1)));
  382.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p2)));
  383.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p3)));
  384.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p4)));
  385.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p5)));
  386.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p6)));
  387.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), p7)));
  388.  
  389.             // the set of attacked squares by an arbitrary piece must not equal 0
  390.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), x.MkApp(f, pieceQueen.Apply(), p0))));
  391.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), x.MkApp(f, pieceQueen.Apply(), p1))));
  392.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), x.MkApp(f, pieceQueen.Apply(), p2))));
  393.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), x.MkApp(f, pieceQueen.Apply(), p3))));
  394.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), x.MkApp(f, pieceQueen.Apply(), p4))));
  395.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), x.MkApp(f, pieceQueen.Apply(), p5))));
  396.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), x.MkApp(f, pieceQueen.Apply(), p6))));
  397.             solver.Assert(x.MkNot(x.MkEq(x.MkBV(0, 64), x.MkApp(f, pieceQueen.Apply(), p7))));
  398.  
  399.             // the piece bitboard must have one and only one bit set
  400.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)p0, x.MkBVSub((Microsoft.Z3.BitVecExpr)p0, x.MkBV(1, 64)))));
  401.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)p1, x.MkBVSub((Microsoft.Z3.BitVecExpr)p1, x.MkBV(1, 64)))));
  402.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)p2, x.MkBVSub((Microsoft.Z3.BitVecExpr)p2, x.MkBV(1, 64)))));
  403.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)p3, x.MkBVSub((Microsoft.Z3.BitVecExpr)p3, x.MkBV(1, 64)))));
  404.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)p4, x.MkBVSub((Microsoft.Z3.BitVecExpr)p4, x.MkBV(1, 64)))));
  405.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)p5, x.MkBVSub((Microsoft.Z3.BitVecExpr)p5, x.MkBV(1, 64)))));
  406.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)p6, x.MkBVSub((Microsoft.Z3.BitVecExpr)p6, x.MkBV(1, 64)))));
  407.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)p7, x.MkBVSub((Microsoft.Z3.BitVecExpr)p7, x.MkBV(1, 64)))));
  408.  
  409.             Microsoft.Z3.Expr expr;
  410.             Microsoft.Z3.Expr expr1;
  411.             {
  412.                 expr = x.MkBVOR(
  413.                         (Microsoft.Z3.BitVecExpr)p0,
  414.                         (Microsoft.Z3.BitVecExpr)p1);
  415.  
  416.                 expr = x.MkBVOR(
  417.                     (Microsoft.Z3.BitVecExpr)expr,
  418.                     (Microsoft.Z3.BitVecExpr)p2);
  419.  
  420.                 expr = x.MkBVOR(
  421.                     (Microsoft.Z3.BitVecExpr)expr,
  422.                     (Microsoft.Z3.BitVecExpr)p3);
  423.  
  424.                 expr = x.MkBVOR(
  425.                     (Microsoft.Z3.BitVecExpr)expr,
  426.                     (Microsoft.Z3.BitVecExpr)p4);
  427.  
  428.                 expr = x.MkBVOR(
  429.                     (Microsoft.Z3.BitVecExpr)expr,
  430.                     (Microsoft.Z3.BitVecExpr)p5);
  431.  
  432.                 expr = x.MkBVOR(
  433.                     (Microsoft.Z3.BitVecExpr)expr,
  434.                     (Microsoft.Z3.BitVecExpr)p6);
  435.  
  436.                 expr = x.MkBVOR(
  437.                     (Microsoft.Z3.BitVecExpr)expr,
  438.                     (Microsoft.Z3.BitVecExpr)p7);
  439.             }
  440.             {
  441.                 expr1 = x.MkBVOR(
  442.                     (Microsoft.Z3.BitVecExpr)x.MkApp(f, pieceQueen.Apply(), p0),
  443.                     (Microsoft.Z3.BitVecExpr)x.MkApp(f, pieceQueen.Apply(), p1));
  444.  
  445.                 expr1 = x.MkBVOR(
  446.                     (Microsoft.Z3.BitVecExpr)expr1,
  447.                     (Microsoft.Z3.BitVecExpr)x.MkApp(f, pieceQueen.Apply(), p2));
  448.  
  449.                 expr1 = x.MkBVOR(
  450.                     (Microsoft.Z3.BitVecExpr)expr1,
  451.                     (Microsoft.Z3.BitVecExpr)x.MkApp(f, pieceQueen.Apply(), p3));
  452.  
  453.                 expr1 = x.MkBVOR(
  454.                     (Microsoft.Z3.BitVecExpr)expr1,
  455.                     (Microsoft.Z3.BitVecExpr)x.MkApp(f, pieceQueen.Apply(), p4));
  456.  
  457.                 expr1 = x.MkBVOR(
  458.                     (Microsoft.Z3.BitVecExpr)expr1,
  459.                     (Microsoft.Z3.BitVecExpr)x.MkApp(f, pieceQueen.Apply(), p5));
  460.  
  461.                 expr1 = x.MkBVOR(
  462.                     (Microsoft.Z3.BitVecExpr)expr1,
  463.                     (Microsoft.Z3.BitVecExpr)x.MkApp(f, pieceQueen.Apply(), p6));
  464.  
  465.                 expr1 = x.MkBVOR(
  466.                     (Microsoft.Z3.BitVecExpr)expr1,
  467.                     (Microsoft.Z3.BitVecExpr)x.MkApp(f, pieceQueen.Apply(), p7));
  468.  
  469.  
  470.             }
  471.  
  472.             // pieces dont attack one another
  473.             solver.Assert(x.MkEq(x.MkBV(0, 64), x.MkBVAND((Microsoft.Z3.BitVecExpr)expr, (Microsoft.Z3.BitVecExpr)expr1)));
  474.  
  475.         }
  476.  
  477.     }
  478. }
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!