GitPlanet

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details
All Projects → zv → z3-mode

zv / z3-mode

Licence: other
An interactive development environment for SMT-LIB files and Z3

Programming Languages

emacs lisp
2029 projects

Labels

satsolversmtlibsmtlibv2z3

Projects that are alternatives of or similar to z3-mode

vim-smt2
A VIM plugin that adds support for the SMT-LIB2 format (including Z3's extensions)
Stars: ✭ 35 (+75%)
Mutual labels:  smtlib, z3
pigosat
Go (golang) bindings for Picosat, the satisfiability solver
Stars: ✭ 15 (-25%)
Mutual labels:  satsolver
libsmt.rs
Rust Bindings to interact with SMTLIB2 compliant solvers
Stars: ✭ 14 (-30%)
Mutual labels:  smtlib
stevia
A simple (unfinished) SMT solver for QF_ABV.
Stars: ✭ 30 (+50%)
Mutual labels:  smtlibv2
Manticore
Symbolic execution tool
Stars: ✭ 2,599 (+12895%)
Mutual labels:  z3
gauntlet
Finding bugs in P4 compilers using translation validation.
Stars: ✭ 23 (+15%)
Mutual labels:  z3
Casper
A compiler for automatically re-targeting sequential Java code to Apache Spark.
Stars: ✭ 45 (+125%)
Mutual labels:  z3
grilops
a GRId LOgic Puzzle Solver library
Stars: ✭ 29 (+45%)
Mutual labels:  z3
intrepid
Intrepyd Model Checker
Stars: ✭ 14 (-30%)
Mutual labels:  z3
z3 tutorial
Jupyter notebooks for tutorial on the Z3 SMT solver
Stars: ✭ 117 (+485%)
Mutual labels:  z3
mbeddr.formal
FASTEN: FormAl SpecificaTion ENvironment - a set of DSLs to experiment with rigorous systems and safety engineering.
Stars: ✭ 16 (-20%)
Mutual labels:  z3
haskell-z3
Haskell bindings to Microsoft's Z3 API (unofficial).
Stars: ✭ 48 (+140%)
Mutual labels:  z3
TSNsched
Automated Schedule Generation for Time-Sensitive Networks (TSN).
Stars: ✭ 46 (+130%)
Mutual labels:  z3
z3-wasm
Scripts and Javascript Glue code to use Z3 in the browser using WASM
Stars: ✭ 11 (-45%)
Mutual labels:  z3
easy z3
Using z3's never been easier (maybe)
Stars: ✭ 94 (+370%)
Mutual labels:  z3

Configuration

Introduction

z3-mode provides an interactive development environment for checking the satisfiability of logical formula written in SMTLIBv2 with backends such as Z3.

Manual Installation

To install manually, check out this repository and add the following to your .emacs

(add-to-list 'load-path "/path/to/z3-mode/")
(autoload 'z3-mode "z3-mode" nil t)
(add-to-list 'auto-mode-alist '("\\.rs\\'" . z3-mode))

package.el installation via MELPA

It can be more convenient to use Emacs’s package manager to handle installation for you if you use many elisp libraries. If you have package.el but haven’t added MELPA, the community package source, yet, add this to ~/.emacs.d/init.el:

(require 'package)
(add-to-list 'package-archives
             '("melpa" . "https://melpa.org/packages/") t)
(package-initialize)

Then do this to load the package listing:

M-x eval-buffer

M-x package-refresh-contents

If you use a version of Emacs prior to 24 that doesn’t include package.el, you can get it from here.

If you have an older ELPA package.el installed from tromey.com, you should upgrade in order to support installation from multiple sources. The ELPA archive is deprecated and no longer accepting new packages, so the version there (1.7.1) is very outdated.

Install z3-mode

One you have package.el, you can install z3-mode or any other modes by choosing them from a list:

M-x package-list-packages Now, to install packages, move your cursor to them and press i. This will mark the packages for installation. When you’re done with marking, press x, and ELPA will install the packages for you (under ~/.emacs.d/elpa/ ).

or using M-x package-install z3-mode

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].