Skip to content

MfesGA/Hsmtlib

master
Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
src
 
 
 
 
 
 

Hsmtl provides functions to interact with several smt solvers using SMT-LIB 2.

Current supported solvers and avaliable interaction modes in each other.

Solver Online Script
Cvc4 X X
Z3 X X
Alt-Ergo X
Yices* X X
MathSat X

(* using yices-smt2 available in: http://yices.csl.sri.com/download-yices2.shtml)

There exists two modes to interact with a solver:

  • Online:

    In online Mode a solver is creted and kept running. Commands are sent via pipe one by one and every time one is sent it also reads the answer of the solver.

  • Script:

    In script Mode a file is created in a desired file path, if Nothing is passed then its created in the current directory with the name temp.smt2. If a file already exists then it's overwriten.

    The functions in this mode behave in the following manner: If it's a funcion where something is declared, for example declareFun or assert then it's only writen to the file. In functions where some feedback is expected such as checkSat, this are writen to the file, a solver is created and the file is given to solver, and it waits for the result. The result is the result of the last function.

  • Batch executiton allows the solver to read an entire context and execute it

A few tutorials on how to use this library can be found in the [wiki] (https://github.com/MfesGA/Hsmtlib/wiki).

The documnetation is in Hackage.

About

Haskell library for easy interaction with SMT-LIB 2 compliant solvers.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published