1:- module(scasp_main,
    2          [ main/1,                         % +Argv
    3
    4            op(700, xfx, [#= , #<>, #< , #> , #=<, #>= ]),
    5            op(900, fy, not),
    6            op(700, xfx, '\u2209')          % not element of
    7          ]).    8:- set_prolog_flag(optimise, true).    9
   10:- use_module(compile).   11:- use_module(ops).   12:- use_module(options).   13:- use_module(solve).   14:- use_module(stack).   15:- use_module(human).   16:- use_module(output).   17:- use_module(model).   18:- use_module(listing).   19:- use_module(html).   20:- use_module(html_text).   21:- use_module(json).   22:- use_module(messages).   23:- use_module(library(http/html_write)).   24:- use_module(library(http/js_write)).   25:- use_module(library(http/json)).   26:- use_module(library(dcg/high_order)).   27
   28:- meta_predicate
   29    print_query(:, +, +).

   37:- initialization(main, main).

 main(+Argv)

Used when calling from command line by passing the command line options and the input files.

   44main(Argv) :-
   45    require_prolog_version('8.5.0-71',
   46                           [ warning(rational)
   47                           ]),
   48    catch_with_backtrace(
   49        ( scasp_parse_args(Argv, Sources, Options),
   50          scasp_set_options(Options),
   51          main(Sources, Options)
   52        ),
   53        Error,
   54        error(Error)).
   55
   56main(Sources, Options) :-
   57    set_prolog_flag(rational_syntax, natural),
   58    set_prolog_flag(prefer_rationals, true),
   59
   60    load_sources(Sources, Options),
   61    (   option(write_program(_), Options)
   62    ->  scasp_portray_program(Options),
   63        halt
   64    ;   option(interactive(true), Options)
   65    ->  '$toplevel':setup_readline,
   66        main_loop(Options)
   67    ;   query(Q, Bindings, Options)
   68    ->  ignore(main_solve(Q, [ variable_names(Bindings),
   69                               inputs(Sources)
   70                             | Options
   71                             ]))
   72    ).
   73
   74load_sources([], _) :-
   75    !,
   76    print_message(error, scasp(no_input_files)),
   77    scasp_help,
   78    halt(1).
   79load_sources(Sources, Options) :-
   80    scasp_load(Sources, Options).

 error(Error)

Report expected errors concisely and unexpected ones with a full backtrace.

   87error(error(scasp_undefined(PIs), _)) :-
   88    !,
   89    maplist(report_undef, PIs),
   90    halt(1).
   91error(error(existence_error(source_sink, Source),_)) :-
   92    print_message(error, scasp(source_not_found(Source))),
   93    halt(1).
   94error(error(existence_error(scasp_query,scasp_main), _)) :-
   95    print_message(error, scasp(no_query)),
   96    halt(1).
   97error(PrologError) :-
   98    print_message(error, PrologError),
   99    halt(1).
  100
  101report_undef(PI) :-
  102    print_message(error,
  103                  error(existence_error(scasp_predicate, PI), _)).
  104
  105
  106query(Query, Bindings, Options) :-
  107    option(query(Term-Bindings), Options),
  108    !,
  109    scasp_compile_query(Term, Query, Options).
  110query(Query, Bindings, Options) :-
  111    scasp_query(Query, Bindings, Options).

 main_loop(+Options)

Run an interactive toplevel loop. Invoked by `scasp -i ...`

  117main_loop(Options) :-
  118    read_term_with_history(R,
  119                           [ prompt('casp ~! ?- '),
  120                             variable_names(Bindings)
  121                           ]),
  122    (   atom(R),
  123        end_of_input(R)
  124    ->  format('~N'),
  125        halt
  126    ;   scasp_compile_query(R, Q, Options)
  127    ->  (   main_solve(Q, [variable_names(Bindings)|Options])
  128        ->  nl, main_loop(Options)
  129        ;   main_loop(Options)
  130        )
  131    ;   main_loop(Options)
  132    ).
  133
  134end_of_input(end_of_file).
  135end_of_input(exit).
  136end_of_input(quit).
  137end_of_input(halt).

 main_solve(+Query, +Options) is semidet

Solve a toplevel query. Query is a callable term where variables are represented as $Name.

To be done

- : If minimal_model(true) is given we must select the minimal model using printable_model/2 and simply print all answers.

  147main_solve(Query, Options) :-
  148    option(html(_File), Options),
  149    !,
  150    option(answers(MaxAnswers), Options, 0),
  151    option(variable_names(Bindings), Options, []),
  152
  153    copy_term(Query-Bindings, QueryVar-QBindings),
  154    ovar_set_bindings(QBindings),
  155    inline_constraints(QueryVar, []),
  156
  157    statistics(cputime, T0),
  158    (   MaxAnswers == 0
  159    ->  findall(Result,
  160                solve_results(Query, Bindings, Result, Options),
  161                Results)
  162    ;   findnsols(MaxAnswers, Result,
  163                  solve_results(Query, Bindings, Result, Options),
  164                  Results)
  165    ->  true
  166    ),
  167    statistics(cputime, T1),
  168    Time is T1-T0,
  169
  170    html_print_results(scasp{ query:QueryVar,
  171                              cpu:Time,
  172                              answers:Results
  173                            },
  174                       Options).
  175main_solve(Query, Options) :-
  176    option(json(Name), Options),
  177    !,
  178    option(answers(MaxAnswers), Options, 0),
  179    option(variable_names(Bindings), Options, []),
  180    option(inputs(Inputs), Options, []),
  181
  182    copy_term(Query-Bindings, QueryVar-QBindings),
  183    ovar_set_bindings(QBindings),
  184    inline_constraints(QueryVar, []),
  185    ROptions = [inline_constraints(false)|Options],
  186
  187    statistics(cputime, T0),
  188    (   MaxAnswers == 0
  189    ->  findall(Result,
  190                solve_results(Query, Bindings, Result, ROptions),
  191                Results)
  192    ;   findnsols(MaxAnswers, Result,
  193                  solve_results(Query, Bindings, Result, ROptions),
  194                  Results)
  195    ->  true
  196    ),
  197    statistics(cputime, T1),
  198    Time is T1-T0,
  199
  200    scasp_results_json(scasp{ query:QueryVar,
  201                              cpu:Time,
  202                              answers:Results,
  203                              inputs:Inputs
  204                            },
  205                       Dict),
  206    (   Name == '-'
  207    ->  json_write_dict(current_output, Dict, Options),
  208        format(current_output, '~N', [])
  209    ;   ensure_extension(Name, json, File),
  210        setup_call_cleanup(
  211            open(File, write, Out, [encoding(utf8)]),
  212            ( json_write_dict(Out, Dict, Options),
  213              format(current_output, '~N', [])
  214            ),
  215            close(Out))
  216    ).
  217main_solve(Query, Options) :-
  218    option(answers(MaxAnswers), Options, -1),
  219    option(variable_names(Bindings), Options, []),
  220
  221    print_query(Query, Bindings, Options),
  222    statistics(cputime, T0),
  223    (   solve_results(Query, Bindings, Result, Options)
  224    *-> true
  225    ;   statistics(cputime, T1),
  226        T is T1-T0,
  227        print_message(warning, scasp(no_models(T))),
  228        fail
  229    ),
  230
  231    print_answer(Result.answer, Result.time, Options),
  232
  233    (   option(tree(_Detail), Options)
  234    ->  print_justification(Result.tree, Options)
  235    ;   true
  236    ),
  237    main_print_model(Result.model, Options),
  238    print_bindings(Bindings, [full_stop(false)|Options]),
  239
  240    (   MaxAnswers == -1
  241    ->  allways_ask_for_more_models, nl, nl
  242    ;   MaxAnswers == 0
  243    ->  nl, nl,
  244        fail
  245    ;   MaxAnswers > 0
  246    ->  nl, nl,
  247        Result.answer = MaxAnswers
  248    ),
  249    !.

 solve_results(+Query, +Bindings, -Result:dict) is nondet

  253solve_results(Query, Bindings,
  254              scasp{ query:Query,
  255                     answer:Counter,
  256                     bindings:Bindings,
  257                     model:Model,
  258                     tree:Tree,
  259                     time:Time
  260                   },
  261              Options) :-
  262    option(tree(true), Options),
  263    !,
  264    call_nth(call_time(solve(Query, [], StackOut, ModelOut), Time), Counter),
  265    justification_tree(StackOut, Tree, Options),
  266    canonical_model(ModelOut, Model),
  267    analyze_variables(t(Bindings, Model, StackOut), Bindings, Options).
  268solve_results(Query, Bindings,
  269              scasp{ query:Query,
  270                     answer:Counter,
  271                     bindings:Bindings,
  272                     model:Model,
  273                     time:Time
  274                   },
  275              Options) :-
  276    call_nth(call_time(solve(Query, [], _, ModelOut), Time), Counter),
  277    canonical_model(ModelOut, Model),
  278    analyze_variables(t(Bindings, Model), Bindings, Options).
  279
  280analyze_variables(Term, Bindings, Options) :-
  281    ovar_set_bindings(Bindings),
  282    (   option(inline_constraints(false), Options)
  283    ->  ovar_analyze_term(Term, [name_constraints(true)])
  284    ;   ovar_analyze_term(Term, []),
  285        inline_constraints(Term, [])
  286    ).
  287
  288:- if(\+current_predicate(tty_size/2)).  289tty_size(25,80).
  290:- endif.

 print_answer(+Nth, +Resources:dict, +Options)

  294print_answer(Nth, Resources, Options) :-
  295    (   option(width(Width), Options)
  296    ->  true
  297    ;   catch(tty_size(_, Width), _, Width = 80)
  298    ),
  299    LineWidth is Width-8,
  300    ansi_format(comment, '~N% ~`\u2015t~*|~n', [LineWidth]),
  301    ansi_format(comment, '~N%', []),
  302    ansi_format(bold,    '~t Answer ~D (~3f sec) ~t~*|~n',
  303                [Nth, Resources.cpu, LineWidth]),
  304    ansi_format(comment, '~N% ~`\u2015t~*|~n', [LineWidth]).

 main_print_model(+Model, +Options)

  309main_print_model(Model, Options) :-
  310    ansi_format(comment, '~N% Model~n', []),
  311    print_model(Model,
  312                [ as_comment(false)
  313                | Options
  314                ]).

 print_query(:Query, +Bindings, +Options)

  318:- det(print_query/3).  319print_query(M:Query, Bindings, Options) :-
  320    ansi_format(comment, '~N% Query~n', []),
  321    (   option(human(true), Options)
  322    ->  human_query(M:Query, [as_comment(false)|Options])
  323    ;   format('?- '),
  324        query_body(Query, PQ),
  325        portray_clause(current_output, PQ, [variable_names(Bindings)])
  326    ).
  327
  328query_body(Query, Body) :-
  329    append(Q1, [o_nmr_check], Query),
  330    !,
  331    comma_list(Body, Q1).
  332query_body(Query, Body) :-
  333    comma_list(Body, Query).

 print_justification(+Tree, +Options)

  337print_justification(Tree, Options) :-
  338    ansi_format(comment, '~N% Justification~n', []),
  339    print_justification_tree(Tree, [ depth(1),
  340                                     as_comment(false)
  341                                   | Options
  342                                   ]).
  343
  344print_bindings(Bindings, Options) :-
  345    exclude(empty_binding, Bindings, Bindings1),
  346    (   Bindings1 == []
  347    ->  ansi_format(comment, '~N% No bindings~n', []),
  348        (   option(full_stop(true), Options, true)
  349        ->  ansi_format(bold, 'true.', [])
  350        ;   ansi_format(bold, 'true', [])
  351        )
  352    ;   ansi_format(comment, '~N% Bindings~n', []),
  353        print_bindings1(Bindings1, Options)
  354    ).
  355
  356empty_binding(Name = Value) :-
  357    Value == '$VAR'(Name).
  358
  359print_bindings1([], _).
  360print_bindings1([H|T], Options) :-
  361    print_binding(H, Options),
  362    (   T == []
  363    ->  (   option(full_stop(true), Options, true)
  364        ->  format('.')
  365        ;   true
  366        )
  367    ;   format(',~n'),
  368        print_bindings1(T, Options)
  369    ).
  370
  371print_binding(Name = Value, Options) :-
  372    format('~w = ~W',
  373           [ Name,
  374             Value, [ numbervars(true),
  375                      quoted(true),
  376                      portray(true)
  377                    | Options
  378                    ]
  379           ]).
  380
  381% rational number handling
  382
  383:- multifile
  384    user:portray/1.  385
  386user:portray(Rat) :-
  387    rational(Rat),
  388    current_prolog_flag(scasp_real, Decimals),
  389    (   integer(Decimals)
  390    ->  format('~*f', [Decimals, Rat])
  391    ;   Decimals == float
  392    ->  Value is float(Rat),
  393        write(Value)
  394    ).

 html_print_results(+Results:dict, +Options)

Options processed:

human(Bool)

If true, open the HTML in human mode. Default is to use the formal notation.

collapse_below(Depth)

Collapse the justification tree below the given level (default: 2).

style(+Boolean)

When false (default true), do not include the HTML style sheets.

script(+Boolean)

When false (default true), do not include the JavaScript.

  413html_print_results(Results, Options) :-
  414    option(html(Name), Options),
  415    Name \== '-',               % stdout
  416    !,
  417    ensure_extension(Name, html, File),
  418    setup_call_cleanup(
  419        open(File, write, Out, [encoding(utf8)]),
  420        ( phrase(reply(Results, Options), Tokens),
  421          print_html(Out, Tokens)
  422        ),
  423        close(Out)).
  424html_print_results(Results, Options) :-
  425    phrase(reply(Results, Options), Tokens),
  426    print_html(Tokens).
  427
  428ensure_extension(Base, Ext, File) :-
  429    file_name_extension(_, Ext, Base),
  430    !,
  431    File = Base.
  432ensure_extension(Base, Ext, File) :-
  433    file_name_extension(Base, Ext, File).
  434
  435reply(Results, Options) -->
  436    { length(Results.answers, Count)
  437    },
  438    emit_as(\page([],
  439                  [ \styles(Options),
  440                    \html_query(Results.query, Options),
  441                    \sequence(answer(Options), Results.answers),
  442                    div(class('scasp-statistics'),
  443                        [ h4('Statistics'),
  444                          p('~D answers in ~3f seconds'-[Count, Results.cpu])
  445                        ]),
  446                    \scripts(Options)
  447                  ]), html).
  448
  449answer(Options, Answer) -->
  450    emit([ div(class('scasp-answer-header'),
  451               'Answer ~D (~3f seconds)'-[Answer.answer, Answer.time.cpu]),
  452           div(class('scasp-answer'),
  453               [ \html_bindings(Answer.bindings, Options),
  454                 \html_model(Answer.model, Options),
  455                 \html_justification_tree(Answer.tree, Options)
  456               ])
  457         ]).

 styles(+Options)

Include the style sheets unless --no-styles is given.

  463styles(Options) -->
  464    { option(style(false), Options) },
  465    !.
  466styles(_Options) -->
  467    { read_file(library('scasp/web/css/scasp.css'), SCASPCSS),
  468      read_file(library('http/web/css/plterm.css'), TermCSS)
  469    },
  470    html(style(SCASPCSS)),
  471    html(style(TermCSS)).
  472
  473scripts(Options) -->
  474    { option(script(false), Options) },
  475    !.
  476scripts(Options) -->
  477    { (   option(human(true), Options)
  478      ->  As = human
  479      ;   As = machine
  480      ),
  481      option(collapse_below(Depth), Options, 2)
  482    },
  483    html(script(
  484             [ src('https://code.jquery.com/jquery-1.11.2.min.js'),
  485               integrity('sha256-Ls0pXSlb7AYs7evhd+VLnWsZ/AqEHcXBeMZUycz/CcA='),
  486               crossorigin('anonymous')
  487             ], [])),
  488    { read_file(library('scasp/web/js/scasp.js'), String) },
  489    html(script(String)),
  490    js_script({|javascript(As,Depth)||
  491
  492$(function() {
  493  $("body").sCASP("swish_answer", {
  494    open_as:As,
  495    justification: {
  496      collapse_below: Depth,
  497      collapsed: false
  498    }
  499  });
  500});
  501              |}).
  502
  503read_file(Spec, String) :-
  504    absolute_file_name(Spec, Path, [access(read)]),
  505    read_file_to_string(Path, String, []).

 ask_for_more_models is semidet

Ask if the user want to generate more models (execution from console)". Fails if a next model is requested.

  512allways_ask_for_more_models :-
  513    (   format(' ? ', []),
  514        get_single_char(R),
  515        memberchk(R, `\s;`)
  516    ->  format(';\n'),
  517        fail
  518    ;   true
  519    )