Did you know ... Search Documentation:
Packs (add-ons) for SWI-Prolog

Package "smtlib"

Title:SMT-LIB parser for SWI-Prolog
Rating:Not rated. Create the first rating!
Latest version:0.0.5
SHA1 sum:6c39f900a1039569a7ab5530b1cc4c3e2fa847a5
Author:Jose Antonio Riaza Valverde <riaza.valverde@gmail.com>
Maintainer:Jose Antonio Riaza Valverde <riaza.valverde@gmail.com>
Packager:Jose Antonio Riaza Valverde <riaza.valverde@gmail.com>
Home page:https://github.com/jariazavalverde/prolog-smtlib
Download URL:https://github.com/jariazavalverde/prolog-smtlib

Reviews

No reviews. Create the first review!.

Details by download location

VersionSHA1#DownloadsURL
0.0.1dff16a3f0729ee3348742a1e8956720be32146231http://jariaza.es/swipl/smtlib-0.0.1.tgz
http://jariaza.es/swipl/smtlib/smtlib-0.0.1.tgz
0.0.299a5a4cc61b3e7659498ec7106eef1f9dfa149951http://jariaza.es/swipl/smtlib/smtlib-0.0.2.tgz
0.0.321aefb126281d0073e65ba386ed96f066329fe991http://jariaza.es/swipl/smtlib/smtlib-0.0.3.tgz
0.0.43f42104f5bc9853b032d037a7ef115fa5747d4cb1http://jariaza.es/swipl/smtlib/smtlib-0.0.4.tgz
0.0.56c39f900a1039569a7ab5530b1cc4c3e2fa847a52http://jariaza.es/swipl/smtlib/smtlib-0.0.5.tgz

SMT-LIB to Prolog

An SMT-LIB parser in Prolog

SMT-LIB is an international initiative aimed at facilitating research and development in SMT. Specifically, Version 2.0 defines:

  • a language for writing terms and formulas in a sorted (i.e., typed) version of first-order logic;
  • a language for specifying background theories and fixing a standard vocabulary of sort, function, and predicate symbols for them;
  • a language for specifying logics, suitably restricted classes of formulas to be checked for satisfiability with respect to a specific background theory;
  • a command language for interacting with SMT solvers via a textual interface that allows asserting and retracting formulas, querying about their satisfiability, examining their models or their unsatisfiability proofs, and so on.

Installation (SWI-Prolog)

?- pack_install(smtlib).

Usage

:- use_module(library(smtlib)).

Examples

Reading SMT-LIB scripts

?- smtlib_read_script('../sample/script/figure-3.4.smt', X).
X = list([
  [reserved('set-logic'),symbol('QF_LIA')],
  [reserved('declare-fun'),symbol(w),[],symbol('Int')],
  [reserved('declare-fun'),symbol(x),[],symbol('Int')],
  [reserved('declare-fun'),symbol(y),[],symbol('Int')],
  [reserved('declare-fun'),symbol(z),[],symbol('Int')],
  [reserved(assert),[symbol(>),symbol(x),symbol(y)]],
  [reserved(assert),[symbol(>),symbol(y),symbol(z)]],
  [reserved('set-option'),[keyword('print-success'),symbol(false)]],
  [reserved(push),numeral(1)],
  [reserved(assert),[symbol(>),symbol(z),symbol(x)]],
  [reserved('check-sat')],
  [reserved('get-info'),keyword('all-statistics')],
  [reserved(pop),numeral(1)],
  [reserved(push),numeral(1)],
  [reserved('check-sat')],
  [reserved(exit)]
]).

Reading SMT-LIB theory declarations

?- smtlib_read_theory('../sample/theory/core.smt', X).
X = list([
  symbol(theory),
  symbol('Core'),
  [keyword('smt-lib-version'),decimal(2.6)],
  [keyword('smt-lib-release'),string('2017-11-24')],
  [keyword('written-by'),string(...)],
  [keyword(date),string(...)],
  [keyword('last-updated'),string(...)],
  [keyword('update-history'),string(...)],
  [keyword(sorts),[
    [symbol('Bool'),numeral(0),[]]
  ]],
  [keyword(funs),[
    [symbol(true),symbol('Bool')],
    [symbol(false),symbol('Bool')],
    [symbol(not),symbol('Bool'),symbol('Bool')],
    [symbol(=>),symbol('Bool'),symbol('Bool'),symbol('Bool'),keyword('right-assoc')],
    [symbol(and),symbol('Bool'),symbol('Bool'),symbol('Bool'),keyword('left-assoc')],
    [symbol(or),symbol('Bool'),symbol('Bool'),symbol('Bool'),keyword('left-assoc')],
    [symbol(xor),symbol('Bool'),symbol('Bool'),symbol('Bool'),keyword('left-assoc')],
    [reserved(par),[symbol('A')],[symbol(=),symbol('A'),symbol('A'),symbol('Bool'),keyword(chainable)]],
    [reserved(par),[symbol('A')],[symbol(distinct),symbol('A'),symbol('A'),symbol('Bool'),keyword(pairwise)]],
    [reserved(par),[symbol('A')],[symbol(ite),symbol('Bool'),symbol('A'),symbol('A'),symbol('A')]]
  ]],
  [keyword(definition),string(...)],
  [keyword(values),string(...)]
]).

Reading SMT-LIB logic declarations

?- smtlib_read_logic('../sample/logic/LIA.smt', X).
X = list([
  symbol(logic),
  symbol('LIA'),
  [keyword('smt-lib-version'),decimal(2.6)],
  [keyword('smt-lib-release'),string('2017-11-24')],
  [keyword('written-by'),string(...)],
  [keyword(date),string(...)],
  [keyword('update-history'),string(...)],
  [keyword(theories),[symbol('Ints')]],
  [keyword(language),string(...)],
  [keyword(extensions),string(...)]
]).

License

Source code is released under the terms of the BSD 3-Clause License.

References

  1. Barrett, C., Fontaine, P. & Tinelli, C. The SMT-LIB Standard: Version 2.6. Department of Computer Science, The University of Iowa (2017). View online

Contents of pack "smtlib"

Pack contains 4 files holding a total of 29.2K bytes.