Java - Windows Intellij: Configure Microsoft z3

When I start configuring Microsoft Z3 solver for Java and for Intellij, I have a lot of difficulties. Here is some important points you must take care of to make it work.

• Download Microsoft Z3 and save it to your folder. e.g: C:\z3-4.8.8-x64-win. Remember the fitness of Z3 must be the same as Java virtual machine. I used the 64-bit version.
• Copy com.microsoft.z3.jar to your libs folder inside the project and add it as a library.
• I get the sample from this link: https://github.com/Z3Prover/z3/blob/master/examples/java/JavaExample.java

package solver;

import com.microsoft.z3.*;

public class z3solver {
    public z3solver() {

    }

    public static void main(String[] args) throws Exception {

//        System.loadLibrary("E:\\Vie" +"t" + "Data\\Th" + "ay Hung\\DSE\\libs\\z3-4.8.8-x64-win\\bin\\lib" + "z3java.dll");
        z3solver solver = new z3solver();
        solver.quantifierExample1();
    }

    public void simpleExample() {
        System.out.println("SimpleExample");
        Log.append("SimpleExample");

        {
            Context ctx = new Context();
            /* do something with the context */

            /* be kind to dispose manually and not wait for the GC. */
            ctx.close();
        }
    }

    void quantifierExample1() {
        try
        {
            Context ctx = new Context();

            System.out.println("QuantifierExample");
//            Log.append("QuantifierExample");

            Sort[] types = new Sort[3];
            IntExpr[] xs = new IntExpr[3];
            Symbol[] names = new Symbol[3];
            IntExpr[] vars = new IntExpr[3];

            for (int j = 0; j < 3; j++) {
                types[j] = ctx.getIntSort();
                names[j] = ctx.mkSymbol("x_" + Integer.toString(j));
                xs[j] = (IntExpr) ctx.mkConst(names[j], types[j]);
                vars[j] = (IntExpr) ctx.mkBound(2 - j, types[j]); // <-- vars
                // reversed!
            }

            Expr body_vars = ctx.mkAnd(
                    ctx.mkEq(ctx.mkAdd(vars[0], ctx.mkInt(1)), ctx.mkInt(2)),
                    ctx.mkEq(ctx.mkAdd(vars[1], ctx.mkInt(2)),
                            ctx.mkAdd(vars[2], ctx.mkInt(3))));

            Expr body_const = ctx.mkAnd(
                    ctx.mkEq(ctx.mkAdd(xs[0], ctx.mkInt(1)), ctx.mkInt(2)),
                    ctx.mkEq(ctx.mkAdd(xs[1], ctx.mkInt(2)),
                            ctx.mkAdd(xs[2], ctx.mkInt(3))));

            Expr x = ctx.mkForall(types, names, body_vars, 1, null, null,
                    ctx.mkSymbol("Q1"), ctx.mkSymbol("skid1"));
            System.out.println("Quantifier X: " + x.toString());

            Expr y = ctx.mkForall(xs, body_const, 1, null, null,
                    ctx.mkSymbol("Q2"), ctx.mkSymbol("skid2"));
            System.out.println("Quantifier Y: " + y.toString());

        }
        catch (Exception ex)
        {

        }
    }

    Model check(Context ctx, BoolExpr f, Status sat) throws Exception {
        Solver s = ctx.mkSolver();
        s.add(f);
        if (s.check() != sat)
            throw new Exception();
        if (sat == Status.SATISFIABLE)
            return s.getModel();
        else
            return null;
    }
}

• Build the project successfully, but then I get the error.

Connected to the target VM, address: '127.0.0.1:54691', transport: 'socket'

Exception in thread "main" java.lang.UnsatisfiedLinkError: no libz3java in java.library.path

at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1860)

at java.lang.Runtime.loadLibrary0(Runtime.java:870)

at java.lang.System.loadLibrary(System.java:1122)

at com.microsoft.z3.Native.<clinit>(Native.java:14)

at com.microsoft.z3.Context.<init>(Context.java:41)

at solver.z3solver.quantifierExample1(z3solver.java:33)

at solver.z3solver.main(z3solver.java:14)

Disconnected from the target VM, address: '127.0.0.1:54691', transport: 'socket'

• You must understand that Java takes care of the build so using the import com.microsoft.z3.*; command is enough, but when running, you must provide java.library.path to the library of Z3 so it knows where the library is. You can do this by go to Run --> Edit Configurations --> VM options: Add this command: -Djava.library.path="C:\z3-4.8.8-x64-win\bin\". If your path have the last "\", VM still complains as follows:

Exception in thread "main" java.lang.UnsatisfiedLinkError: no libz3java in java.library.path

at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1860)

at java.lang.Runtime.loadLibrary0(Runtime.java:870)

at java.lang.System.loadLibrary(System.java:1122)

at com.microsoft.z3.Native.<clinit>(Native.java:14)

at com.microsoft.z3.Context.<init>(Context.java:41)

at solver.z3solver.quantifierExample1(z3solver.java:33)

at solver.z3solver.main(z3solver.java:14)

Disconnected from the target VM, address: '127.0.0.1:53632', transport: 'socket'

• You must remove the last "\" from the path, VM will understand it. So the last and successful will be: -Djava.library.path="C:\z3-4.8.8-x64-win\bin". However, now you will have the following error.

Exception in thread "main" java.lang.UnsatisfiedLinkError: C:\z3-4.8.8-x64-win\bin\libz3java.dll: Can't find dependent libraries

at java.lang.ClassLoader$NativeLibrary.load(Native Method)

at java.lang.ClassLoader.loadLibrary0(ClassLoader.java:1934)

at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1850)

at java.lang.Runtime.loadLibrary0(Runtime.java:870)

at java.lang.System.loadLibrary(System.java:1122)

at com.microsoft.z3.Native.<clinit>(Native.java:14)

at com.microsoft.z3.Context.<init>(Context.java:41)

at solver.z3solver.quantifierExample1(z3solver.java:33)

at solver.z3solver.main(z3solver.java:14)

Disconnected from the target VM, address: '127.0.0.1:56441', transport: 'socket'

• Now I copy all the folder of Z3 to my libs folder. remove the previous com.microsoft.z3.jar from the libs folder. Add the new one com.microsoft.z3.jar as a library. Now I must edit the Run configurations. so it is: -Djava.library.path="My path\libs\z3-4.8.8-x64-win\bin"

• Now you can run the sample code without problem.

Connected to the target VM, address: '127.0.0.1:58074', transport: 'socket'

QuantifierExample

Quantifier X: (forall ((x_0 Int) (x_1 Int) (x_2 Int))

  (! (and (= (+ x_0 1) 2) (= (+ x_1 2) (+ x_2 3))) :skolemid skid1 :qid Q1))

Quantifier Y: (forall ((x_0 Int) (x_1 Int) (x_2 Int))

  (! (and (= (+ x_0 1) 2) (= (+ x_1 2) (+ x_2 3))) :skolemid skid1 :qid Q1))

C# - Prevent Windows Form from flickering during Maximizing or Restoring

My problem today is that my windows form application has one second or more of black before displaying full screen. That make it not smooth when restoring the windows or change from minimize state to maximize. Even when the application contains only some control on the screen only.

I have tried to disable / comment out all of the source code that related to the resize related events of windows. But that doesn't resolve the issue.

After all, I thought that the solution must be that we can catch the event when user begin to maximize the windows and temporary suspend the layout redraw, then when the application comes to maximized state, we will allow it to resume the layout. Therefore, the last source code of the application will be somehow like the following.

 using System;  
 using System.Collections.Generic;  
 using System.ComponentModel;  
 using System.Data;  
 using System.Drawing;  
 using System.Linq;  
 using System.Text;  
 using System.Threading.Tasks;  
 using System.Windows.Forms;  
 namespace TestMaximizeWindows  
 {  
   public partial class Form1 : Form  
   {  
     public Form1()  
     {  
       InitializeComponent();  
     }  
     private void Form1_Load(object sender, EventArgs e)  
     {  
     }  
     protected override void WndProc(ref Message m)  
     {  
       var msg = '\x112';  
       const int minimize = '\xf020';  
       const int maximize = '\xf030';  
       const int restore = '\xf120';  
       if (m.Msg == msg)  
       {  
         Console.WriteLine(m.ToString());  
         var param = m.WParam.ToInt32();  
         switch (param)  
         {  
           case minimize:  
             // handle minimize              
             break;  
           case maximize:  
             // handle maximize     
             this.SuspendLayout();           
             break;  
           case restore:  
             // handle restore    
             this.SuspendLayout();            
             break;  
         }  
       }  
       base.WndProc(ref m);  
     }  
     private void Form1_SizeChanged(object sender, EventArgs e)  
     {  
       this.ResumeLayout();  
     }  
   }  
 }  

There are two other events that you can use in this WinProc method

private const Int32 WM_SIZE = 0x0005;
private const Int32 WM_SIZING = 0x0214;

C# - Draw line, rectangle on a Windows Form

The following code snippet show you how to draw a line and rectangle in C#.

 using System;  
 using System.Collections.Generic;  
 using System.ComponentModel;  
 using System.Data;  
 using System.Drawing;  
 using System.Linq;  
 using System.Text;  
 using System.Threading.Tasks;  
 using System.Windows.Forms;  
 namespace DrawOnWinForm  
 {  
   public partial class Form1 : Form  
   {  
     public Form1()  
     {  
       InitializeComponent();  
     }  
     System.Drawing.Pen bounderyPen;  
     System.Drawing.Pen OxOyPen;  
     System.Drawing.Pen ABPen;  
     System.Drawing.Pen CPen;  
     System.Drawing.Brush ACMBrush = Brushes.LightGray;  
     System.Drawing.Brush BCMpBrush = Brushes.LightCyan;  
     System.Drawing.Brush TextBrush = Brushes.Black;  
     Font textFont = new Font("Arial", 10);  
     Point TOPLEFT = new Point(0, 0);  
     Point BASEO = new Point(400, 400);  
     Rectangle Boundery = new Rectangle();  
     double xO = 0, yO = 0;  
     private void Form1_Load(object sender, EventArgs e)  
     {  
     }  
     int zoomX = 50;  
     int margin = 10;  
     int zoomY = 50;  
     System.Drawing.Brush brush = Brushes.White;  
     private void Form1_Paint(object sender, PaintEventArgs e)  
     {  
       Clear();  
       System.Drawing.Graphics formGraphics = this.CreateGraphics();  
       Boundery.X = margin;  
       Boundery.Y = margin;  
       Boundery.Width = this.Width - 4 * margin;  
       Boundery.Height = this.Height - Boundery.Y - margin * 5;  
       bounderyPen = new System.Drawing.Pen(System.Drawing.Color.Brown);  
       bounderyPen.Width = 2;  
       formGraphics.DrawRectangle(bounderyPen, Boundery);  
       BASEO.X = (int)(this.Width / 2);  
       BASEO.Y = this.Height - margin * 5 - 100;  
       OxOyPen = new System.Drawing.Pen(System.Drawing.Color.Blue);  
       OxOyPen.Width = 2;  
       formGraphics.DrawLine(OxOyPen, margin, BASEO.Y, Boundery.X + Boundery.Width - margin * 0, BASEO.Y);  
       formGraphics.DrawLine(OxOyPen, Boundery.X + Boundery.Width - 10 - margin * 0, BASEO.Y - 5, Boundery.X + Boundery.Width - margin * 0, BASEO.Y);  
       formGraphics.DrawLine(OxOyPen, Boundery.X + Boundery.Width - 10 - margin * 0, BASEO.Y + 5, Boundery.X + Boundery.Width - margin * 0, BASEO.Y);  
       string textTrucX = "x";  
       formGraphics.DrawString(textTrucX, textFont, TextBrush, new PointF(Boundery.X + Boundery.Width - 10 - margin * 0, BASEO.Y + 2));  
       formGraphics.DrawLine(OxOyPen, BASEO.X, this.Height - margin * 5, BASEO.X, this.Height - margin * 5 - Boundery.Height);  
       formGraphics.DrawLine(OxOyPen, BASEO.X - 5, this.Height - margin * 5 - Boundery.Height + 10, BASEO.X, this.Height - margin * 5 - Boundery.Height);  
       formGraphics.DrawLine(OxOyPen, BASEO.X + 5, this.Height - margin * 5 - Boundery.Height + 10, BASEO.X, this.Height - margin * 5 - Boundery.Height);  
       string textTrucY = "y";  
       formGraphics.DrawString(textTrucY, textFont, TextBrush, new PointF(BASEO.X - 15, this.Height - margin * 5 - Boundery.Height));  
       string textO = "O(" + xO + "," + yO + ")";  
       formGraphics.DrawString(textO, textFont, TextBrush, new PointF(ToaDoFormXZoomY(xO), ToaDoFormYZoomY(yO)));  
     }  
     private void Clear()  
     {  
       System.Drawing.Graphics formGraphics = this.CreateGraphics();  
       #region Ve Boundery  
       Rectangle screen = new Rectangle();  
       screen.X = 0;  
       screen.Y = 0;  
       screen.Width = this.Width - 1;  
       screen.Height = this.Height;  
       formGraphics.FillRectangle(brush, screen);  
       #endregion  
       formGraphics.Dispose();  
     }  
     private int ToaDoFormXZoomY(double x)  
     {  
       return (int)(BASEO.X + x * zoomY);  
     }  
     private int ToaDoFormYZoomY(double y)  
     {  
       return (int)(BASEO.Y - y * zoomY);  
     }  
     private int ToaDoFormXZoomX(double x)  
     {  
       return (int)(BASEO.X + x * zoomX);  
     }  
     private int ToaDoFormYZoomX(double y)  
     {  
       return (int)(BASEO.X - y * zoomX);  
     }  
   }  
 }  

Here is the output of the project.

C# - Change the size of text, apps, and other items to 125%, 150% by using AutoScaleMode

When user changes his Windows display settings of the size of text, apps, and other items to 125%, 150%, etc, how can a Windows Application can automatically response to the changes without breaking its structure and texts.

The solution is that we should let the .NET Framework to work on it automatically by using the following line of code.

       this.AutoScaleMode = AutoScaleMode.Dpi;  

Additionally, you may need to set the Application property of the main project's Properties to "Create application without a manifest".

Don't forget to set the Autosize property of the form to true.

Happy coding...

C# - Hide "Not Responding" message on Windows Form application

Sometimes, in a Windows Form application, we have a situation that make the application "Not Responding". This is not good from user's perspective. If any improvement cannot make any changes, you can choose a solution to hide the message from the application. The following application show you a case of "Not Responding" and a version that can hide the message.

This function will make the application "Not Responding".

     private void button1_Click(object sender, EventArgs e)  
     {  
       for (int i = 0;i < 100000000; i++)  
       {  
         label1.Text = "i = " + i.ToString();  
       }  
     }  

However, adding the following code, you can see no "Not Responding" on your application.

     [DllImport("user32.dll")]  
     public static extern void DisableProcessWindowsGhosting();  
     private void Form1_Load(object sender, EventArgs e)  
     {  
       DisableProcessWindowsGhosting();  
     }  

C# - Try / catch and application performance

The following test shows you how much the try / catch block cost your application performance. Therefore, please consider carefully every cases you use try / catch.

 using System;  
 using System.Collections.Generic;  
 using System.ComponentModel;  
 using System.Data;  
 using System.Drawing;  
 using System.Linq;  
 using System.Text;  
 using System.Threading.Tasks;  
 using System.Windows.Forms;  
 using System.Diagnostics;  
 namespace TryCatchTest  
 {  
   public partial class Form1 : Form  
   {  
     public Form1()  
     {  
       InitializeComponent();  
     }  
     private void Form1_Load(object sender, EventArgs e)  
     {  
       Stopwatch sw = new Stopwatch();  
       sw.Start();  
       try  
       {  
         int count = 0;  
         for (int i = 0; i < 10000; i++)  
         {  
           count += 1;  
           label1.Text = count.ToString();  
         }  
       }  
       catch(Exception ex)  
       {  
         Console.WriteLine(ex.ToString());  
       }  
       sw.Stop();  
       Console.WriteLine("With try / catch, the elapsed time is: " + sw.ElapsedMilliseconds + " miliseconds");  
       Stopwatch sw2 = new Stopwatch();  
       sw2.Start();  
       int count2 = 0;  
       for (int i = 0; i < 10000; i++)  
       {  
         count2 += 1;  
         label1.Text = count2.ToString();  
       }  
       sw2.Stop();  
       Console.WriteLine("Without try / catch, the elapsed time is: " + sw2.ElapsedMilliseconds + " miliseconds");  
     }  
   }  
 }  

The output in the Console window is as follows:

With try / catch, the elapsed time is: 1364 miliseconds

Without try / catch, the elapsed time is: 1152 miliseconds

C# - Prevent "Not Responding" error in Win form by using Task.Run

This function will make your application "Not Responding".

     private void button1_Click(object sender, EventArgs e)  
     {  
       for (int i = 0;i < 100000000; i++)  
       {  
         label1.Text = "i = " + i.ToString();  
       }  
     }  

Modify it a little bit, we can prevent "Not Responding" error happen by using Task.Run method like this:

     private async void button2_Click(object sender, EventArgs e)  
     {  
       await Task.Run(() =>  
       {  
         for (int i = 0; i < 100000000; i++)  
         {  
           label1.Text = "i = " + i.ToString();  
         }  
       });  
     }