[JAVA] Comment utiliser la bibliothèque Z3 dans Scala avec Eclipse

Introduction In this post, I will show how to use the z3 Java library with Scala in Eclipse to solve a SAT formula. I made this post because even if it is quite short, I did lot of investigations on it to succeed to use z3 Java library with Scala in Eclipse IDE.

Requirements

Getting Z3 jar file

  1. Clone the Z3 git repository or download it
  2. Go in the z3 folder and run the command python scripts/mk_make.py --java
  3. Inside the z3 folder, go into the folder build and then make examples
    1. Note: If you encounter an error during the make due to an invalid argument -std=c++11, edit the file config.mk and remove the argument -std=c++11 from the CXXFLAGS flag
  4. The jar file is now created in the folder yourf3folder/build and some Java examples

Note: For a full installation of z3 repository please follow these instructions.

Eclipse configuration In Eclipse, right-click on your Scala project, click on Build Path and Configure Build Path: Screen Shot 2017-08-14 at 15.32.23.png

It should open a window, once it's open go into the Libraries tab, click on Add External JARs... and select the z3 Jar file from the gitfolder/build (the file name would be com.microsoft.z3.jar): tmp.png

Once you did that, you have to specify one last thing to Eclipse to make it works with z3. On the same window as the previous configuration, go on the Source tab click on your project to open the menu context, choose Native library location, click on the button Edit... on the right and choose the gitfolder/build folder : q.png

You need to do that because the library uses two file into the gitfolder/build to work. (libz3.dylib and libz3java.dylib in Mac Os, libz3.dll and libz3java.dll in Windows)

Now you just have to import the library into your project file to use it. Because Scala is made with Java, you can also use this part of the tutorial to use the z3 library into a Java project in Eclipse. The below part of the tutorial was made for Scala but if you want to know how to do it in Java you can follow this link for Java examples.

How to use Z3 in Scala

There are two ways to use Z3 in Scala:

  1. using a file SMT2 formatted with the formula you want to solve,
  2. programming directly in code the formula.

In the following, I explain both ways by solving the propositional formula ((a | b) & c), as an example.

To solve a formula in z3 library, you need two things, the formula you want to solve in BoolExpr format and the variables from the formula you want to know the result format.

  1. Using external SMT2-formatted files

Consider the following SMT2 formatted text file, named sample.smt2, which express the above propositional formula, i.e., (a|b) & c):

sample.smt2


(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)
(assert (and (or a b) c))

A Scala program code which read this smt2 file, and compute the formula is as follows:


import com.microsoft.z3._

object z3test
{
  def main(args: Array[String])
  {
    val ctx: Context = new Context(new java.util.HashMap[String, String])  
    val formula: BoolExpr = ctx.parseSMTLIB2File("sample.smt2", null, null, null, null)
    val args: Array[Expr] = formula.getArgs // Here I will get 2 args
    val arg1: Expr = args(0)
    val arg2: Expr = args(1)

    val a: Expr = formula.getArgs()(0).getArgs()(0)
    val b: Expr = formula.getArgs()(0).getArgs()(1)
    val c: Expr = formula.getArgs()(1)



    /* Evaluation part */
    val solver: com.microsoft.z3.Solver = ctx.mkSolver()   // Get a solver from the Context object
    solver.add(formula)                                    // Add the formula to the solver (BoolExpr)
    
    if(solver.check == Status.SATISFIABLE)                 // Check if the formula is satisfiable or not
    {
      val model: Model = solver.getModel                   // Get a model from the solver
      val resultVa: Expr = model.eval(a,false)             // Get the result for each variables
      val resultVb: Expr = model.eval(b,false)
      val resultVc: Expr = model.eval(c,false)
      
      println(resultVa)   // Result is true
      println(resultVb)   // Result is false
      println(resultVc)   // Result is true
    }
  }
}

The program code first initializes a Context object with a HashMap[String, String] :

val ctx: Context = new Context(new java.util.HashMap[String, String])

So you can parse the file by calling this method on the Context object previously created :

val formula: BoolExpr = ctx.parseSMTLIB2File("smt2file.txt", null, null, null, null)

After you did that you get my BoolExpr variable which contains the formula, you can access to the formula by this way :

val args: Array[Expr] = formula.getArgs // Here I will get 2 args
val arg1: Expr = args(0)
val arg2: Expr = args(1)

println(arg1)
println(arg2)

// Result
(or a b)
c

With my formula, I will use this code to get my variables :

val a: Expr = formula.getArgs()(0).getArgs()(0)
val b: Expr = formula.getArgs()(0).getArgs()(1)
val c: Expr = formula.getArgs()(1)

There is a better way to achieve that : The formula is divide part by part and you can access it by using the method getArgs(). This method will return you an Array[Expr]. You can call it again on the Expr you got from the array. Until there is a single element in the Expr the size of the array return by getArgs() will be greater than 0. I.E. : if you want to get all the variables of the formula, you can achieve this using a method like that :

  def getAllVariable(a: Array[Expr]): List[Expr] =
  {
      if (a == null || a.size == 0)
        Nil
      else if (a.head.getNumArgs == 0)
        a.head :: getAllVariable(a.tail)
      else
        getAllVariable(a.head.getArgs) ::: getAllVariable(a.tail)  
  }
  1. Programming the formula

Here is the Scala code of the second approach:

import com.microsoft.z3._

object z3test
{
  def main(args: Array[String])
  {
    val ctx: Context = new Context(new java.util.HashMap[String, String])  
    
    val a: BoolExpr = ctx.mkBoolConst("a")
    val b: BoolExpr = ctx.mkBoolConst("b")
    val c: BoolExpr = ctx.mkBoolConst("c")
    
    val formula: BoolExpr = ctx.mkAnd(ctx.mkOr(a,b),c)



    /* Evaluation part */
    val solver: com.microsoft.z3.Solver = ctx.mkSolver()   // Get a solver from the Context object
    solver.add(formula)                                    // Add the formula to the solver (BoolExpr)
    
    if(solver.check == Status.SATISFIABLE)                 // Check if the formula is satisfiable or not
    {
      val model: Model = solver.getModel                   // Get a model from the solver
      val resultVa: Expr = model.eval(a,false)             // Get the result for each variables
      val resultVb: Expr = model.eval(b,false)
      val resultVc: Expr = model.eval(c,false)
      
      println(resultVa)   // Result is true
      println(resultVb)   // Result is false
      println(resultVc)   // Result is true
    }
  }
}

As you can see the code, the programming-the-formula ways share many things in common with the first approach, however, there are some differences. In the previous part, you get the formula first, in this part it will be the contrary: you get the variables first and the formula second.

The program code first initializes a Context object with a HashMap[String, String] :

val ctx: Context = new Context(new java.util.HashMap[String, String])

To create variables, you have to call the method mkBoolConst() on the Context object, like that :

val a: BoolExpr = ctx.mkBoolConst("a")
val b: BoolExpr = ctx.mkBoolConst("b")
val c: BoolExpr = ctx.mkBoolConst("c")

To program the formula, you need to use the variables and the boolean methods provide by the Context object:

val formula: BoolExpr = ctx.mkAnd(ctx.mkOr(a,b),c)

Notice that there is a lot of boolean methods provides by the Context object like ctx.mkImplies() or ctx.mkNot().

Sources Z3 Github Eclipse for Scala, Scala IDE

Recommended Posts

Comment utiliser la bibliothèque Z3 dans Scala avec Eclipse
Comment utiliser la bibliothèque JDD dans Scala avec Eclipse
Comment utiliser Eclipse Debug_Shell
Comment basculer Tomcat context.xml avec Eclipse WTP
Comment utiliser Lombok au printemps
Comment utiliser mssql-tools avec Alpine
Comment utiliser InjectorHolder dans OpenAM
Comment utiliser les classes en Java?
Comment définir Lombok dans Eclipse
Un mémorandum sur l'utilisation d'Eclipse
Prise en charge multilingue de Java Comment utiliser les paramètres régionaux
Comment utiliser Apache Derby sur Eclipse
Comment utiliser le volume nommé dans docker-compose.yml
Comment utiliser BootStrap avec Play Framework
Comment inclure Spring Tool dans Eclipse 4.6.3?
Je souhaite utiliser DBViewer avec Eclipse 2018-12! !!
Comment utiliser Docker dans VSCode DevContainer
Comment utiliser MySQL dans le didacticiel Rails
Comment utiliser les variables d'environnement dans RubyOnRails
Comment publier une bibliothèque dans jCenter
Comprendre en 5 minutes !! Comment utiliser Docker
Comment utiliser credentials.yml.enc introduit à partir de Rails 5.2
[Pour les débutants] Comment déboguer avec Eclipse
Comment utiliser ExpandableListView dans Android Studio
[Java FX] Comment écrire des autorisations Eclipse dans build.gradle
Comment colorer la sortie de la console de code dans Eclipse
Comment utiliser MyBatis2 (iBatis) avec Spring Boot 1.4 (Spring 4)
[Rails] Comment utiliser les boîtes de sélection dans Ransack
Comment utiliser h2db intégré avec Spring Boot
Comment utiliser le framework Java avec AWS Lambda! ??
Comment utiliser l'API Java avec des expressions lambda
Comment démarrer avec Eclipse Micro Profile
Comment utiliser JQuery dans Rails 6 js.erb
Comment utiliser le protocole NFS version 2 avec Ubuntu 18.04
[Rails] Comment utiliser PostgreSQL dans l'environnement Vagrant
Comment générer automatiquement un constructeur dans Eclipse
Comment utiliser Map
Comment utiliser rbenv
Comment utiliser with_option
Comment utiliser fields_for
Comment utiliser java.util.logging
Comment utiliser la carte
Comment utiliser collection_select
Pour déboguer avec Eclipse
Comment utiliser Twitter4J
Comment utiliser active_hash! !!
Comment utiliser MapStruct
Comment utiliser TreeSet
[Comment utiliser l'étiquette]
Comment utiliser l'identité
Comment utiliser le hachage
Utiliser PostgreSQL dans Scala
Comment utiliser Dozer.mapper