Package "smtlib"

Title:	SMT-LIB parser for SWI-Prolog
Rating:	Not rated. Create the first rating!
Latest version:	0.0.6
SHA1 sum:	76fe142cdea350a88a300e4f192f1af4026ec505
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

Version	SHA1	#Downloads	URL
0.0.1	dff16a3f0729ee3348742a1e8956720be3214623	1	http://jariaza.es/swipl/smtlib-0.0.1.tgz
			http://jariaza.es/swipl/smtlib/smtlib-0.0.1.tgz
0.0.2	99a5a4cc61b3e7659498ec7106eef1f9dfa14995	1	http://jariaza.es/swipl/smtlib/smtlib-0.0.2.tgz
0.0.3	21aefb126281d0073e65ba386ed96f066329fe99	1	http://jariaza.es/swipl/smtlib/smtlib-0.0.3.tgz
0.0.4	3f42104f5bc9853b032d037a7ef115fa5747d4cb	1	http://jariaza.es/swipl/smtlib/smtlib-0.0.4.tgz
0.0.5	6c39f900a1039569a7ab5530b1cc4c3e2fa847a5	3	http://jariaza.es/swipl/smtlib/smtlib-0.0.5.tgz
0.0.6	76fe142cdea350a88a300e4f192f1af4026ec505	25	http://jariaza.es/swipl/smtlib/smtlib-0.0.6.tgz
			https://jariaza.es/swipl/smtlib/smtlib-0.0.6.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)).

• smtlib_read_script/2 - parses SMT-LIB script from file.
• smtlib_read_theory/2 - parses SMT-LIB theory declaration from file.
• smtlib_read_logic/2 - parses SMT-LIB logic declaration from file.
• smtlib_read_expression/2 - parses SMT-LIB expression from file.
• smtlib_read_expressions/2 - parses SMT-LIB expressions from file.
• smtlib_parse_script/2 - parses SMT-LIB script from chars.
• smtlib_parse_theory/2 - parses SMT-LIB theory declaration from chars.
• smtlib_parse_logic/2 - parses SMT-LIB logic declaration from chars.
• smtlib_parse_expression/2 - parses SMT-LIB expression from chars.
• smtlib_parse_expressions/2 - parses SMT-LIB expressions from chars.
• smtlib_write_to_stream/2 - writes SMT-LIB expression into stream.
• smtlib_write_to_file/2 - writes SMT-LIB expression into file.

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 30.2K bytes.