Did you know ... | Search Documentation: |
Pack smtlib -- README.md |
SMT-LIB is an international initiative aimed at facilitating research and development in SMT. Specifically, Version 2.0 defines:
?- pack_install(smtlib).
:- use_module(library(smtlib)).
?- 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)] ]).
?- 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(...)] ]).
?- 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(...)] ]).
Source code is released under the terms of the BSD 3-Clause License.