smtlib v1.0.0

Node.js API for SMT-LIB 2.0

SMT-LIB 2.0 is an interoperability format to communicate with different SMT solvers, such as CVC4 or Z3.

The syntax of SMT-LIB is similar to Lisp:

(set-logic QF_ALL_SUPPORTED)
(declare-fun x () Bool)
(declare-fun y () Bool)
(assert (and (or x y) (not x) (not y))
(check-sat)

This package provides an high-level API to construct SMT-Lib expressions, taking care of escaping:

const smt = require('smtlib');
let solver = new smt.LocalCVC4Solver('QF_ALL_SUPPORTED');
solver.add(smt.DeclareFun('x', [], 'Bool'))
solver.add(smt.DeclareFun('y', [], 'Bool'))
solver.assert(smt.And(smt.Or('x', 'y'), smt.Not('x'), smt.Not('y')));
solver.checkSat().then(([sat, assignment]) => ...).catch((e) => ...);

The library also includes code to interact with a locally installed CVC4, as an external process.