• Stars
    star
    117
  • Rank 290,746 (Top 6 %)
  • Language
    Scala
  • License
    Apache License 2.0
  • Created about 13 years ago
  • Updated 11 months ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

DSL in Scala for Constraint Solving with Z3 SMT Solver

ScalaZ3 Build status

This is ScalaZ3 for Z3 4.8.14 and Scala 3.2.0.

Compiling ScalaZ3

You should have Java and SBT 1.7.x installed.

Mac & Unix

Run

sbt +package

to compile Z3 4.8.14 for Scala 3.2.0.

The JAR files will be in target/scala-3.2.0/scalaz3_3-4.8.14.jar and will contain the shared library dependencies.

For testing, run

sbt +test

Windows

Prerequisites

Install Visual Studio Community edition 2015 Make sure to have the following:

  • Programming Languages
    • Visual C++
      • Common tools for Visual C++ 2015 (CHECK)

Install JDK 1.8 (or higher)

  • There is a folder include in C:\Program Files\Java\jdk1.8.0_121. Create a copy of this include folder directly in C:\Program Files\Java\

Install a 64-bit version of GCC. To chec that, run gcc -v, it should display 64. If it shows mingw32 you need to install a new version.

We were able to successfully package and test ScalaZ3 with the MinGW 64bit compiler suite with the following options.

Version: 6.3.0
Architecture: x86_64
Threads: wind32
Esception: seh
Build revision: 2

Packaging instructions

Open the native x64 command prompt (available in the start menu under the Visual Studio folder)

Now navigate to the scalaz3 folder and type:

sbt +package

The JAR files will be in target/scala-3.2.0/scalaz3_3-4.8.14.jar and will contain the shared library dependencies.

Test your package.

Run

sbt test

If this does not work, check that lib-bin/scalaz3.dll is a correctly set up 64 bit dll:

dumpbin /headers lib-bin/scalaz3.dll | findstr machine

The output should be (x64). If you encounter any other issue, please let us know.

Using ScalaZ3

On a single operating system / architecture

Create a folder named unmanaged at the same level as your build.sbt file, and copy the JAR file in target/scala-3.2.0/scalaz3_3-4.8.14.jar into it.

Then add, the following lines to your build.sbt file:

Compile / unmanagedJars += {
  baseDirectory.value / "unmanaged" / s"scalaz3_3-4.8.14.jar"
}

On multiple operating systems / architectures

If you want to use ScalaZ3 in a project which must support various operating systems and architectures, you will have to compile ScalaZ3 on each of those systems/architectures, following the instructions above.

Make sure to name the resulting JAR files as scalaz3-[osName]-[osArch]-3.jar, where:

  • [osName] is one of: mac, win, unix.
  • [osArch] corresponds to System.getProperty("sun.arch.data.model"), ie. x64, fds, etc.

Create a folder named unmanaged at the same level as your build.sbt file, and copy the aforementioned JAR files into it.

Add the following lines to your build.sbt file:

val osInf = Option(System.getProperty("os.name")).getOrElse("")
val osArch = System.getProperty("sun.arch.data.model")

val isUnix    = osInf.indexOf("nix") >= 0 || osInf.indexOf("nux") >= 0
val isWindows = osInf.indexOf("Win") >= 0
val isMac     = osInf.indexOf("Mac") >= 0

val osName = if (isWindows) "win" else if (isMac) "mac" else "unix"

Compile / unmanagedJars += {
  baseDirectory.value / "unmanaged" / s"scalaz3-$osName-$osArch-3.jar"
}

More Repositories

1

stainless

Verification framework and tool for higher-order Scala programs
HTML
347
star
2

leon

The Leon system for verification, synthesis, repair
Scala
162
star
3

inox

Solver for higher-order functional programs
Scala
87
star
4

scallion

LL(1) parser combinators in Scala
Scala
54
star
5

smart

Verification and Generation of Smart Contracts using Stainless and Scala
HTML
35
star
6

treenet

Recursive Neural Networks for PyTorch
Python
31
star
7

lisa

Proof assistant based on first-order logic and set theory
Scala
29
star
8

bolts

Bolts: Stainless Verified Scala Examples
Scala
15
star
9

nugget

Neural-Network Guided Expression Transformation
Python
13
star
10

jahob

Jahob Verification System
C
11
star
11

comfusy

Implementation of the "Complete Functional Synthesis" approach described in the eponymous PLDI 2010 paper.
Scala
11
star
12

silex

Lexing library for Scala
Scala
10
star
13

welder

Interactive Theorem Proving based on Inox
Scala
10
star
14

SystemFR

System FR: Formalized Foundations for Stainless
Coq
9
star
15

scallion-proofs

Proofs of correctness for Scallion (https://github.com/epfl-lara/scallion)
Coq
9
star
16

rust-stainless

An experimental Rust frontend for Stainless
Rust
6
star
17

StainlessFit

Stainless directly built on System FR, with standalone front-end
Scala
5
star
18

verified-2048

A 2048 clone verified by Stainless
Scala
4
star
19

stainless-actors

Actor System library for Stainless which runs on Akka
Scala
4
star
20

asplos2022tutorial

ASPLOS 2022 Tutorial on Stainless
C
4
star
21

OCBSL

A minimal algorithm to decide the word problem in Orthocomplemented Bisemilattices, in Scala.
Scala
4
star
22

fit-code

TypeScript
3
star
23

verifythis2020

VerifyThis2020 Challenge in Stainless
Scala
2
star
24

silex-proofs

Proofs on lexing with derivatives and zippers
Coq
2
star
25

cs550

Scala
2
star
26

lattices-algorithms

This repository contains two algorithms for the word problem and normalization problem of Ortholattices and Orthocomplemented Bisemilattices
Scala
2
star
27

muscat

A unit testing framework for concurrent Scala programs
Scala
2
star
28

grammar-web

An online tutoring system for context-free grammars
Scala
2
star
29

compiler2024-labs-public

Scala
2
star
30

leon-web

Web-interface for Leon
Scala
2
star
31

stainless-project.g8

Giter8 template for Stainless-enabled projects
Scala
2
star
32

GrammarComparison

A System for Analyzing and Comparing Context-Free Grammars
Scala
2
star
33

scala-native-stainless-sample

Scala
1
star
34

Deep_Learning_On_Code_With_A_Graph_Vocabulary

Code to reproduce the experiments in the paper Deep Learning On Code With A Graph Vocabulary
Python
1
star
35

funprog-lambda

Scala
1
star
36

STIX-showcase

Scala
1
star
37

verified-lambda

A verified lambda interpreter
Scala
1
star