13:- module(smtlib, [
   14    % read from file
   15    smtlib_read_expression/2,
   16    smtlib_read_expressions/2,
   17    smtlib_read_theory/2,
   18    smtlib_read_logic/2,
   19    smtlib_read_script/2,
   20    % read from chars
   21    smtlib_parse_expression/2,
   22    smtlib_parse_expressions/2,
   23    smtlib_parse_theory/2,
   24    smtlib_parse_logic/2,
   25    smtlib_parse_script/2,
   26    % write
   27    smtlib_write_to_stream/2,
   28    smtlib_write_to_file/2
   29]).

   46% EXPORTED PREDICATES
   47
   48% smtlib_read_expression/2
   49% smtlib_read_expression(+Path, ?Expression)
   50%
   51% This predicate succeeds when file +Path exists and ?Expression
   52% is the expression resulting from parsing the file as an
   53% S-Expression of SMT-LIB.
   54smtlib_read_expression(Path, Expression) :-
   55    open(Path, read, Stream),
   56    stream_to_list(Stream, Chars),
   57    close(Stream),
   58    smtlib_parse_expression(Chars, Expression).
   59
   60% smtlib_read_expressions/2
   61% smtlib_read_expressions(+Path, ?Expression)
   62%
   63% This predicate succeeds when file +Path exists and ?Expression
   64% is the expression resulting from parsing the file as a list of
   65% S-Expressions of SMT-LIB.
   66smtlib_read_expressions(Path, Expression) :-
   67    open(Path, read, Stream),
   68    stream_to_list(Stream, Chars),
   69    close(Stream),
   70    smtlib_parse_expressions(Chars, Expression).
   71
   72% smtlib_read_theory/2
   73% smtlib_read_theory(+Path, ?Theory)
   74%
   75% This predicate succeeds when file +Path exists and ?Theory
   76% is the expression resulting from parsing the file as an
   77% SMT-LIB theory declaration.
   78smtlib_read_theory(Path, Theory) :-
   79    open(Path, read, Stream),
   80    stream_to_list(Stream, Chars),
   81    close(Stream),
   82    smtlib_parse_theory(Chars, Theory).
   83
   84% smtlib_read_logic/2
   85% smtlib_read_logic(+Path, ?Logic)
   86%
   87% This predicate succeeds when file +Path exists and ?Theory
   88% is the expression resulting from parsing the file as an
   89% SMT-LIB logic declaration.
   90smtlib_read_logic(Path, Logic) :-
   91    open(Path, read, Stream),
   92    stream_to_list(Stream, Chars),
   93    close(Stream),
   94    smtlib_parse_logic(Chars, Logic).
   95
   96% smtlib_read_script/2
   97% smtlib_read_script(+Chars, ?Script)
   98%
   99% This predicate succeeds when file +Path exists and ?Script is
  100% the script resulting from parsing +Chars as an SMT-LIB script.
  101smtlib_read_script(Path, Script) :-
  102    open(Path, read, Stream),
  103    stream_to_list(Stream, Chars),
  104    close(Stream),
  105    smtlib_parse_script(Chars, Script).
  106
  107% smtlib_parse_expression/2
  108% smtlib_parse_expression(+Chars, ?Expression)
  109%
  110% This predicate succeeds when +Chars is a list of characters and
  111% ?Expression is the expression resulting from parsing +Chars as an
  112% S-Expression of SMT-LIB.
  113smtlib_parse_expression(Chars, Expression) :- s_expr(Expression, Chars, []).
  114
  115% smtlib_parse_expressions/2
  116% smtlib_parse_expressions(+Chars, ?Expression)
  117%
  118% This predicate succeeds when +Chars is a list of characters and
  119% ?Expression is the expression resulting from parsing +Chars as a
  120% list of S-Expressions of SMT-LIB.
  121smtlib_parse_expressions(Chars, Expression) :- s_exprs(Expression, Chars, []).
  122
  123% smtlib_parse_theory/2
  124% smtlib_parse_theory(+Chars, ?Theory)
  125%
  126% This predicate succeeds when +Chars is a list of characters and
  127% ?Theory is the expression resulting from parsing +Chars as an
  128% SMT-LIB theory declaration.
  129smtlib_parse_theory(Chars, Theory) :- theory_decl(Theory, Chars, []).
  130
  131% smtlib_parse_logic/2
  132% smtlib_parse_logic(+Chars, ?Logic)
  133%
  134% This predicate succeeds when +Chars is a list of characters and
  135% ?Logic is the expression resulting from parsing +Chars as an
  136% SMT-LIB logic declaration.
  137smtlib_parse_logic(Chars, Logic) :- logic(Logic, Chars, []).
  138
  139% smtlib_parse_script/2
  140% smtlib_parse_script(+Chars, ?Script)
  141%
  142% This predicate succeeds when +Chars is a list of characters and
  143% ?Script is the script resulting from parsing +Chars as an SMT-LIB script.
  144smtlib_parse_script(Chars, Script) :- script(Script, Chars, []).
  145
  146% smtlib_write_to_stream/2
  147% smtlib_write_to_stream(+Stream, +SMTLIB)
  148%
  149% This predicate succeeds when +SMTLIB is a valid SMT-LIB
  150% expression and can be written in the stream +Stream.
  151smtlib_write_to_stream(Stream, numeral(N)) :- !, write(Stream, N), write(Stream, ' ').
  152smtlib_write_to_stream(Stream, decimal(D)) :- !, write(Stream, D), write(Stream, ' ').
  153smtlib_write_to_stream(Stream, hexadecimal(H)) :- !, write(Stream, H), write(Stream, ' ').
  154smtlib_write_to_stream(Stream, binary(B)) :- !, write(Stream, B), write(Stream, ' ').
  155smtlib_write_to_stream(Stream, symbol(S)) :- !, write(Stream, S), write(Stream, ' ').
  156smtlib_write_to_stream(Stream, reserved(R)) :- !, write(Stream, R), write(Stream, ' ').
  157smtlib_write_to_stream(Stream, keyword(K)) :- !, write(Stream, ':'), write(Stream, K), write(Stream, ' ').
  158smtlib_write_to_stream(Stream, string(S)) :- !,
  159    write(Stream, '"'),
  160    write(Stream, S),
  161    write(Stream, '"'),
  162    write(Stream, ' ').
  163smtlib_write_to_stream(Stream, list(Expr)) :- !,
  164    maplist(smtlib_write_to_stream(Stream), Expr).
  165smtlib_write_to_stream(Stream, Expr) :-
  166    is_list(Expr), !,
  167    write(Stream, '('),
  168    maplist(smtlib_write_to_stream(Stream), Expr),
  169    writeln(Stream, ')').
  170
  171% smtlib_write_to_file/2
  172% smtlib_write_to_file(+Path, +SMTLIB)
  173%
  174% This predicate succeeds when +SMTLIB is a valid SMT-LIB
  175% expression and can be written in the file +Path.
  176smtlib_write_to_file(Path, SMTLIB) :- 
  177    open(Path, write, Stream),
  178    smtlib_write_to_stream(Stream, SMTLIB),
  179    close(Stream).
  180
  181
  182
  183% UTILS
  184
  185% stream_to_list/2
  186% stream_to_list(+Stream, ?List)
  187%
  188% This predicate succeeds when ?List is the lists
  189% of characters reads from the stream +Stream.
  190stream_to_list(Stream, []) :-
  191    at_end_of_stream(Stream), !.
  192stream_to_list(Stream, [Char|Input]) :-
  193    get_code(Stream, Code),
  194    char_code(Char, Code),
  195stream_to_list(Stream, Input).
  196
  197
  198
  199% LEXICON
  200% SMT-LIB source files consist of ASCII characters.
  201
  202% A comment is any character sequence not contained within a string literal
  203% or a quoted symbol that begins with the semicolon character ; and ends 
  204% with the first subsequent line-breaking character.
  205comment --> [X], {X \= '\n'}, !, comment.
  206comment --> [].
  207
  208% Comments together with the space, tab and line-breaking characters are all
  209% considered whitespace.
  210whitespace --> [' '].
  211whitespace --> ['\t'].
  212whitespace --> ['\n'].
  213whitespace --> ['\r'].
  214whitespace --> [';'], comment, ['\n'], !.
  215whitespace([';'|Xs],[]) :- comment(Xs,[]).
  216
  217whitespaces --> whitespace, !, whitespaces.
  218whitespaces --> [].
  219
  220lpar --> ['('], whitespaces.
  221rpar --> [')'], whitespaces.
  222
  223% A <numeral> is the digit 0 or a non-empty sequence of digits not starting with 0.
  224numeral(numeral(Y)) --> digits([X|Xs]), {(Xs = [] ; X \= '0'), number_chars(Y, [X|Xs])}, whitespaces.
  225
  226numerals([X|Xs]) --> numeral(X), !, numerals(Xs).
  227numerals([]) --> [].
  228
  229digits([X|Xs]) --> [X], {char_code(X, C), C >= 48, C =< 57}, !, digits(Xs).
  230digits([]) --> [].
  231
  232% A <decimal> is a token of the form <numeral>.0*<numeral>.
  233decimal(decimal(D)) -->
  234    digits([X|Xs]),
  235    {(Xs = [] ; X \= '0')},
  236    ['.'], digits(Y),
  237    {append([X|Xs], ['.'|Y], Z),
  238    number_chars(D, Z)},
  239    whitespaces.
  240
  241% A <hexadecimal> is a non-empty case-insensitive sequence of digits and letters
  242% from A to F preceded by the (case sensitive) characters #x.
  243hexadecimal(hexadecimal(Y)) --> ['#','x'], hexadecimal_digits(X), {X \= [], atom_chars(Y, X)}, whitespaces.
  244
  245hexadecimal_digits([X|Xs]) --> [X],
  246    {member(X, ['0','1','2','3','4','5','6','7','8','9',a,b,c,d,e,f,'A','B','C','D','E','F'])}, !,
  247    hexadecimal_digits(Xs).
  248hexadecimal_digits([]) --> [].
  249
  250% A <binary> is a non-empty sequence of the characters 0 and 1 preceded by the characters #b.
  251binary(binary(Y)) --> ['#','b'], binary_digits(X), {X \= [], atom_chars(Y, X)}, whitespaces.
  252
  253binary_digits([X|Xs]) --> [X], {member(X, ['0','1'])}, !, binary_digits(Xs).
  254binary_digits([]) --> [].
  255
  256% A <string> is any sequence of printable ASCII characters delimited by double quotes
  257% (") and possibly containing the C-style escape sequences \" and \\, both of which are
  258% treated as a single character—respectively " and \.  The first escape sequence allows
  259% as usual the double quote character to appear within a string literal, the second allows
  260% the backslash character to end a string literal.
  261string(string(Y)) --> ['"'], quoted(X), ['"'], {atom_chars(Y, X)}, whitespaces.
  262
  263quoted([X|Xs]) --> printable_character(X), {X \= '"'}, !, quoted(Xs).
  264quoted([X|Xs]) --> [X], {member(X, [' ','\n','\r','\t'])}, !, quoted(Xs).
  265quoted(['"'|Xs]) --> ['"','"'], !, quoted(Xs).
  266quoted([]) --> [].
  267
  268printable_character(X) --> [X], {char_code(X, C), (C >= 32, C =< 126 ; C >= 128)}.
  269
  270% The language uses a number of reserved words, sequences of (non-whitespace) characters
  271% that are to be treated as individual tokens. Additionally, each command name in the
  272% scripting language is also a reserved word.
  273reserved_word(X) :- member(X, [
  274    par, 'BINARY', 'HEXADECIMAL', 'NUMERAL', 'DECIMAL', 'STRING', '_', '!', as,
  275    let, forall, exists, match, 'set-logic', 'set-option', 'set-info', 'declare-sort',
  276    'define-sort', 'declare-fun', push, pop, assert, 'check-sat', 'get-assertions',
  277    'get-proof', 'get-unsat-core', 'get-value', 'get-assignment', 'get-info', exit,
  278    'check-sat-assuming', 'declare-const', 'declare-datatype', 'declare-datatypes',
  279    'define-fun', 'define-fun-rec', 'define-funs-rec', echo, 'get-model', 'get-option',
  280    'get-unsat-assumptions', reset, 'reset-assertions', 'set-option'
  281]).
  282
  283reserved_word(reserved(Y)) -->
  284    symbol_chars([X|Xs]),
  285    {atom_chars(Y, [X|Xs]),
  286    reserved_word(Y)},
  287    whitespaces.
  288
  289% A <symbol> is either a simple symbol or a quoted symbol. The former is any non-empty
  290% sequence of letters, digits and the characters ~ ! @ $ % ^ & * _ - + = < > . ? / that
  291% does not start with a digit and is not a reserved word. The latter is any sequence of
  292% printable ASCII characters (including space, tab, and line-breaking characters) except
  293% for the backslash character \, that starts and ends with | and does not otherwise contain |.
  294symbol(X) --> simple_symbol(X).
  295symbol(X) --> quoted_symbol(X).
  296
  297symbols([X|Xs]) --> symbol(X), !, symbols(Xs).
  298symbols([]) --> [].
  299
  300simple_symbol(symbol(Y)) -->
  301    symbol_chars([X|Xs]),
  302    {\+member(X, ['0','1','2','3','4','5','6','7','8','9']),
  303    atom_chars(Y, [X|Xs]),
  304    \+reserved_word(Y)},
  305    whitespaces.
  306
  307symbol_chars([X|Xs]) --> [X],
  308    {member(X, ['~','!','@','$','%','^','&','*','_','-','+','=','<','>','.','?','/']) ;
  309    (char_code(X, C), C >= 48, C =< 57) ; 
  310    (char_code(X, C), C >= 97, C =< 122) ; 
  311    (char_code(X, C), C >= 65, C =< 90)}, !,
  312    symbol_chars(Xs).
  313symbol_chars([]) --> [].
  314
  315quoted_symbol(symbol(Y)) --> ['|'], quoted_symbol_chars(X), ['|'], {atom_chars(Y, X)}, whitespaces.
  316
  317quoted_symbol_chars([X|Xs]) --> printable_character(X), {X \= '|', X \= '\\'}, !, quoted_symbol_chars(Xs).
  318quoted_symbol_chars([X|Xs]) --> [X], {member(X, [' ','\n','\r','\t'])}, !, quoted_symbol_chars(Xs).
  319quoted_symbol_chars([]) --> [].
  320
  321% A <keyword> is a non-empty sequence of letters, digits, and the characters
  322% ~ ! @ $ % ^ & * _ - + = < > . ? / preceded by the character :.
  323keyword(keyword(Y)) --> [':'], symbol_chars(X), {X \= [], atom_chars(Y, X)}, whitespaces.
  324
  325
  326
  327% S-EXPRESSIONS
  328
  329% An S-expression is either a non-parenthesis token or a (possibly  empty) sequence of
  330% S-expressions enclosed in parentheses. Every syntactic category of the SMT-LIB language
  331% is a specialization of the category <s-expr> defined by the production rules below.
  332spec_constant(X) --> decimal(X), !.
  333spec_constant(X) --> numeral(X), !.
  334spec_constant(X) --> hexadecimal(X), !.
  335spec_constant(X) --> binary(X), !.
  336spec_constant(X) --> string(X), !.
  337
  338s_expr(X) --> whitespaces, s_expr2(X).
  339s_expr2(X) --> spec_constant(X), !.
  340s_expr2(X) --> symbol(X), !.
  341s_expr2(X) --> reserved_word(X), !.
  342s_expr2(X) --> keyword(X), !.
  343s_expr2(X) --> lpar, s_exprs(X), whitespaces, rpar.
  344
  345s_exprs([X|Xs]) --> s_expr(X), !, s_exprs(Xs).
  346s_exprs([]) --> [].
  347
  348
  349
  350% IDENTIFIERS
  351
  352% Indexed identifiers are defined more systematically as the application of the reserved
  353% word _ to a symbol and one or more indices. Indices can be numerals or symbols.
  354identifier([reserved('_'),X|Xs]) --> lpar, ['_'], whitespaces, symbol(X), indices(Xs), {Xs \= []}, rpar.
  355identifier(X) --> symbol(X).
  356
  357index(X) --> numeral(X).
  358index(X) --> symbol(X).
  359
  360indices([X|Xs]) --> index(X), !, indices(Xs).
  361indices([]) --> [].
  362
  363
  364% ATTRIBUTES
  365
  366% These are generally pairs consisting of an attribute name and an associated value,
  367% although attributes with no value are also allowed.
  368attribute_value(X) --> spec_constant(X), !.
  369attribute_value(X) --> symbol(X), !.
  370attribute_value(Xs) --> lpar, s_exprs(Xs), rpar.
  371
  372attribute([X,Xs]) --> keyword(X), attribute_value(Xs), !.
  373attribute(X) --> keyword(X).
  374
  375attributes([X|Xs]) --> attribute(X), !, attributes(Xs).
  376attributes([]) --> [].
  377
  378
  379% SORTS
  380
  381% A sort symbol can be either the distinguished symbol Bool or any <identifier>. A sort
  382% parameter can be any <symbol> (which in turn, is an <identifier>).
  383sort([X|Xs]) --> lpar, identifier(X), sorts(Xs), {Xs \= []}, rpar.
  384sort(X) --> identifier(X).
  385
  386sorts([X|Xs]) --> sort(X), sorts(Xs).
  387sorts([]) --> [].
  388
  389
  390
  391% TERMS AND FORMULAS
  392
  393% Well-sorted terms are a subset of the set of all terms. The latter are constructed out of
  394% constant symbols in the <spec-constant> category (numerals, rationals, strings, etc.),
  395% variables, function symbols, three kinds of binders--the reserved words let, forall, match
  396% and exists--and an annotation operator--the reserved word !.
  397qual_identifier(X) --> identifier(X).
  398qual_identifier([reserved(as),X,Y]) --> lpar, [a,s], whitespaces, identifier(X), sort(Y), rpar.
  399
  400var_binding([X,Y]) --> lpar, symbol(X), term(Y), rpar.
  401var_bindings([X|Xs]) --> var_binding(X), !, var_bindings(Xs).
  402var_bindings([]) --> [].
  403
  404sorted_var([X,Y]) --> lpar, symbol(X), sort(Y), rpar.
  405sorted_vars([X|Xs]) --> sorted_var(X), !, sorted_vars(Xs).
  406sorted_vars([]) --> [].
  407
  408pattern([X|Xs]) --> lpar, !, symbol(X), symbols(Xs), {Xs \= []}, rpar.
  409pattern(X) --> symbol(X).
  410
  411match_case([X,Y]) --> lpar, pattern(X), term(Y), rpar.
  412match_cases([X|Xs]) --> match_case(X), !, match_cases(Xs).
  413match_cases([]) --> [].
  414
  415term(X) --> spec_constant(X).
  416term(X) --> qual_identifier(X).
  417term([X|Xs]) --> lpar, qual_identifier(X), terms(Xs), {Xs \= []}, rpar.
  418term([reserved(let), Xs, X]) --> lpar, reserved_word(reserved(let)), lpar, var_bindings(Xs), {Xs \= []}, rpar, term(X), rpar.
  419term([reserved(Y), Xs, X]) --> lpar, reserved_word(reserved(Y)), {member(Y, [forall, exists])}, lpar, sorted_vars(Xs), {Xs \= []}, rpar, term(X), rpar.
  420term([reserved(match), Xs]) --> lpar, reserved_word(reserved(match)), lpar, match_cases(Xs), {Xs \= []}, rpar, rpar.
  421term([reserved('!'),X|Xs]) --> lpar, reserved_word(reserved('!')), term(X), attributes(Xs), {Xs \= []}, rpar.
  422
  423terms([X|Xs]) --> term(X), !, terms(Xs).
  424terms([]) --> [].
  425
  426
  427
  428% THEORY DECLARATIONS
  429
  430% The syntax of theory declarations follows an attribute-value-based format. A theory
  431% declaration consists of a theory name and a list of <attribute> elements. Theory attributes
  432% with the following predefined keywords have a prescribed usage and semantics: :definition,
  433% :funs, :funs-description, :notes, :sorts, :sorts-description, and :values. Additionally, a
  434% theory declaration can contain any number of user-defined attributes.
  435sort_symbol_decl([X,Y|Z]) --> lpar, identifier(X), numeral(Y), attributes(Z), rpar.
  436sort_symbol_decls([X|Xs]) --> sort_symbol_decl(X), !, sort_symbol_decls(Xs).
  437sort_symbol_decls([]) --> [].
  438
  439meta_spec_constant(reserved(X)) --> reserved_word(reserved(X)), {member(X, ['NUMERAL','DECIMAL','STRING'])}.
  440
  441fun_symbol_decl([X,Y|Z]) --> lpar, spec_constant(X), sort(Y), attributes(Z), rpar.
  442fun_symbol_decl([X,Y|Z]) --> lpar, meta_spec_constant(X), sort(Y), attributes(Z), rpar.
  443fun_symbol_decl([X|YZ]) --> lpar, identifier(X), sorts(Y), {Y \= []}, attributes(Z), rpar, {append(Y, Z, YZ)}.
  444
  445par_fun_symbol_decl(X) --> fun_symbol_decl(X).
  446par_fun_symbol_decl([reserved(par), X, [Y|ZW]]) -->
  447    lpar, reserved_word(reserved(par)),
  448    lpar, symbols(X), {X \= []}, rpar,
  449    lpar, identifier(Y), sorts(Z), {Z \= []},
  450    attributes(W), rpar,
  451    rpar, {append(Z, W, ZW)}.
  452
  453par_fun_symbol_decls([X|Xs]) --> par_fun_symbol_decl(X), !, par_fun_symbol_decls(Xs).
  454par_fun_symbol_decls([]) --> [].
  455
  456theory_attribute([keyword(sorts),Xs]) -->  keyword(keyword(sorts)), lpar, sort_symbol_decls(Xs), {Xs \= []}, rpar, !.
  457theory_attribute([keyword(funs),Xs]) -->  keyword(keyword(funs)), lpar, par_fun_symbol_decls(Xs), {Xs \= []}, rpar, !.
  458theory_attribute([keyword(X),Y]) -->  keyword(keyword(X)), {member(X,['sorts-description','funs-description',definition,values,notes])}, string(Y), !.
  459theory_attribute(X) -->  attribute(X), !.
  460
  461theory_attributes([X|Xs]) --> theory_attribute(X), !, theory_attributes(Xs).
  462theory_attributes([]) --> [].
  463
  464theory_decl(list([symbol(theory),X|Y])) --> whitespaces, lpar, symbol(symbol(theory)), symbol(X), theory_attributes(Y), {Y \= []}, rpar.
  465
  466
  467
  468% LOGIC DECLARATIONS
  469
  470% Attributes with the following predefined keywords have a prescribed usage and semantics
  471% in logic declarations: :theories, :language, :extensions, :notes, and :values. Additionally,
  472% as with theories, a logic declaration can contain any number of user-defined  attributes.
  473logic_attribute([keyword(theories),Xs]) --> keyword(keyword(theories)), lpar, symbols(Xs), {Xs \= []}, rpar, !.
  474logic_attribute([keyword(X),Y]) --> keyword(keyword(X)), {member(X,[language,extensions,values,notes])}, string(Y), !.
  475logic_attribute(X) --> attribute(X).
  476
  477logic_attributes([X|Xs]) --> logic_attribute(X), !, logic_attributes(Xs).
  478logic_attributes([]) --> [].
  479
  480logic(list([symbol(logic),X|Xs])) --> whitespaces, lpar, symbol(symbol(logic)), symbol(X), logic_attributes(Xs), {Xs \= []}, rpar.
  481
  482
  483
  484% SCRIPTS
  485
  486% Scripts are sequences of commands. In line with the LISP-like syntax, all commands look
  487% like LISP-function applications, with a command name applied to zero or more arguments.
  488
  489sort_dec([X,Y]) --> lpar, symbol(X), numeral(Y), rpar.
  490sort_decs([X|Xs]) --> sort_dec(X), !, sort_decs(Xs).
  491sort_decs([]) --> [].
  492
  493selector_dec([X,Y]) --> lpar, symbol(X), sort(Y), rpar.
  494selector_decs([X|Xs]) --> selector_dec(X), !, selector_decs(Xs).
  495selector_decs([]) --> [].
  496
  497constructor_dec([X|Xs]) --> lpar, symbol(X), selector_decs(Xs), rpar.
  498constructor_decs([X|Xs]) --> constructor_dec(X), !, constructor_decs(Xs).
  499constructor_decs([]) --> [].
  500
  501datatype_dec(Xs) --> lpar, constructor_decs(Xs), {Xs \= []}, rpar.
  502datatype_dec([reserved(par),X,Y]) --> lpar, reserved_word(reserved(par)),
  503    lpar, symbols(X), {X \= []}, rpar,
  504    lpar, constructor_decs(Y), {Y \= []}, rpar, rpar.
  505datatype_decs([X|Xs]) --> datatype_dec(X), !, datatype_decs(Xs).
  506datatype_decs([]) --> [].
  507
  508function_dec([X,Y,Z]) --> lpar, symbol(X), lpar, sorted_vars(Y), rpar, sort(Z), rpar.
  509function_decs([X|Xs]) --> function_dec(X), !, function_decs(Xs).
  510function_decs([]) --> [].
  511
  512function_def([X,Y,Z,W]) --> symbol(X), lpar, sorted_vars(Y), rpar, sort(Z), term(W).
  513
  514prop_literal([symbol(not),X]) --> lpar, symbol(symbol(not)), symbol(X), rpar.
  515prop_literal(X) --> symbol(X).
  516prop_literals([X|Xs]) --> prop_literal(X), !, prop_literals(Xs).
  517prop_literals([]) --> [].
  518
  519command([reserved('check-sat-assuming'),X]) --> lpar, reserved_word(reserved('check-sat-assuming')), lpar, prop_literals(X), rpar, rpar.
  520command([reserved('declare-const'),X,Y]) --> lpar, reserved_word(reserved('declare-const')), symbol(X), sort(Y), rpar.
  521command([reserved('declare-datatype'),X,Y]) --> lpar, reserved_word(reserved('declare-datatype')), symbol(X), datatype_dec(Y), rpar.
  522command([reserved('declare-datatypes'),X,Y]) --> lpar, reserved_word(reserved('declare-datatypes')),
  523    lpar, sort_decs(X), rpar, lpar, datatype_decs(Y), {length(X,Length), length(Y,Length), Length > 0}, rpar, rpar.
  524command([reserved('set-logic'),X]) --> lpar, reserved_word(reserved('set-logic')), symbol(X), rpar.
  525command([reserved('set-option')|X]) --> lpar, reserved_word(reserved('set-option')), option(X), rpar.
  526command([reserved('set-info'),X]) --> lpar, reserved_word(reserved('set-info')), attribute(X), rpar.
  527command([reserved('declare-sort'),X,Y]) --> lpar, reserved_word(reserved('declare-sort')), symbol(X), numeral(Y), rpar.
  528command([reserved('define-sort'),X,Y,Z]) --> lpar, reserved_word(reserved('define-sort')), symbol(X), lpar, symbols(Y), rpar, sort(Z), rpar.
  529command([reserved('declare-fun'),X,Y,Z]) --> lpar, reserved_word(reserved('declare-fun')), symbol(X), lpar, sorts(Y), rpar, sort(Z), rpar.
  530command([reserved('define-fun'),X,Y,Z,W]) --> lpar, reserved_word(reserved('define-fun')), function_def([X,Y,Z,W]), rpar.
  531command([reserved('define-fun-rec'),X,Y,Z,W]) --> lpar, reserved_word(reserved('define-fun-rec')), function_def([X,Y,Z,W]), rpar.
  532command([reserved('define-funs-rec'),X,Y]) --> lpar, reserved_word(reserved('define-funs-rec')),
  533    lpar, function_decs(X), rpar, lpar, terms(Y), {length(X,Length), length(Y,Length), Length > 0}, rpar, rpar.
  534command([reserved(push),X]) --> lpar, reserved_word(reserved(push)), numeral(X), rpar.
  535command([reserved(pop),X]) --> lpar, reserved_word(reserved(pop)), numeral(X), rpar.
  536command([reserved(assert),X]) --> lpar, reserved_word(reserved(assert)), term(X), rpar.
  537command([reserved(X)]) --> lpar, reserved_word(reserved(X)), {member(X,['check-sat','get-model','get-assertions','get-proof','get-unsat-core','get-assignment','get-unsat-assumptions',exit,reset,'reset-assertions'])}, rpar.
  538command([reserved('get-value'),Xs]) --> lpar, reserved_word(reserved('get-value')), lpar, terms(Xs), {Xs \= []}, rpar, rpar.
  539command([reserved('get-option'),X]) --> lpar, reserved_word(reserved('get-option')), keyword(X), rpar.
  540command([reserved('get-info'),X]) --> lpar, reserved_word(reserved('get-info')), info_flag(X), rpar.
  541command([reserved(echo),X]) --> lpar, reserved_word(reserved(echo)), string(X), rpar.
  542
  543script(list(X)) --> whitespaces, script2(X).
  544script2([X|Xs]) --> command(X), !, script2(Xs).
  545script2([]) --> [].
  546
  547% The command set-option takes as argument expressions of the syntactic category <option>
  548% which have the same form as attributes with values. Options with the predefined keywords
  549% below have a prescribed usage and semantics.
  550b_value(symbol(X)) --> symbol(symbol(X)), {member(X, [true,false])}.
  551
  552option([keyword(X),Y]) --> keyword(keyword(X)), {member(X,['global-declarations','print-success','interactive-mode','produce-proofs','produce-unsat-cores','produce-models','produce-assignments','produce-assertions','produce-unsat-assumptions'])}, b_value(Y).
  553option([keyword('diagnostic-output-channel'),X]) --> keyword(keyword('diagnostic-output-channel')), string(X).
  554option([keyword('random-seed'),X]) --> keyword(keyword('random-seed')), numeral(X).
  555option([keyword('verbosity'),X]) --> keyword(keyword('verbosity')), numeral(X).
  556option([keyword('reproducible-resource-limit'),X]) --> keyword(keyword('reproducible-resource-limit')), numeral(X).
  557option([keyword('regular-output-channel'),X]) --> keyword(keyword('regular-output-channel')), string(X).
  558option([X]) --> attribute(X).
  559
  560% The command get-info takes as argument expressions of the syntactic category <info_flag>
  561% which are flags with the same form as keywords. The predefined flags below have a prescribed
  562% usage and semantics.
  563info_flag(keyword(X)) --> keyword(keyword(X)), {member(X,['error-behavior',name,authors,version,'reason-unknown','all-statistics','assertion-stack-lavels'])}, !.
  564info_flag(X) --> keyword(X)