1:- module(scasp_solve,
    2          [ solve/4                   % :Goals, +StackIn, -StackOut, -Model
    3          ]).    4:- use_module(clp/call_stack).    5:- use_module(predicates).    6:- use_module(clp/disequality).    7:- use_module(clp/clpq).    8:- use_module(verbose).    9
   10:- autoload(library(apply), [maplist/2, include/3]).   11:- autoload(library(assoc),
   12            [get_assoc/3, empty_assoc/1, get_assoc/5, put_assoc/4]).   13:- autoload(library(lists), [append/3, member/2]).   14:- autoload(library(terms), [variant/2, mapsubterms/3]).   15
   16:- meta_predicate
   17    solve(:, +, -, -).   18
   19/** <module> The sCASP solver
   20*/
   21
   22% Note:  The  Ciao  original  controls   forall  algorithm  using  three
   23% current_option/2 facts, `prev_forall`, `sasp_forall` and `all_forall`:
   24%
   25%   <no option>:    no current_option/2
   26%   --prev_forall:  prev_forall=on, sasp_forall=off
   27%   --all_c_forall: all_forall=on
   28%   --sasp_forall:  prev_forall=on sasp_forall=on
   29
   30:- create_prolog_flag(scasp_no_fail_loop, false, [keep(true)]).   31:- create_prolog_flag(scasp_assume,       false, [keep(true)]).   32:- create_prolog_flag(scasp_forall,       all,   [keep(true)]).   33:- create_prolog_flag(scasp_dcc,	  false, [keep(true)]).   34:- create_prolog_flag(scasp_trace_dcc,	  false, [keep(true)]).   35
   36%!  solve(:Goals, +StackIn, -StackOut, -Model)
   37%
   38%   Solve the list of sub-goals `Goal`  where   StackIn  is  the list of
   39%   goals already visited and returns  in   StackOut  the  list of goals
   40%   visited to prove the sub-goals and in  Model the model that supports
   41%   the sub-goals.
   42
   43solve(M:Goals, StackIn, StackOut, Model) :-
   44    stack_parents(StackIn, Parents),
   45    stack_proved(StackIn, ProvedIn),
   46    solve(Goals, M, Parents, ProvedIn, _ProvedOut, StackIn, StackOut, Model).
   47
   48solve([], _, _, Proved, Proved, StackIn, [[]|StackIn], []).
   49solve([Goal|Goals], M, Parents, ProvedIn, ProvedOut, StackIn, StackOut, Model) :-
   50    verbose(print_check_calls_calling(Goal, StackIn)),
   51    check_goal(Goal, M, Parents, ProvedIn, ProvedMid, StackIn, StackMid, Modelx),
   52    Modelx = [AddGoal|JGoal],
   53    verbose(format('Success ~@\n', [print_goal(Goal)])),
   54    solve(Goals, M, Parents, ProvedMid, ProvedOut, StackMid, StackOut, Modelxs),
   55    Modelxs = JGoals,
   56    (   shown_predicate(M:Goal)
   57    ->  Model = [AddGoal, JGoal|JGoals]
   58    ;   Model = [JGoal|JGoals]
   59    ).
   60
   61
   62proved_relatives(not(Goal), Proved, Relatives) =>
   63    proved_relatives(Goal, Proved, Relatives).
   64proved_relatives(Goal, Proved, Relatives) =>
   65    functor(Goal, Name, Arity),
   66    get_assoc(Name/Arity, Proved, Relatives).
   67
   68%!  check_goal(+Goal, +Module, +Parents, +ProvedIn, -ProvedOut,
   69%!              +StackIn, -StackOut, -Model)
   70%
   71%   Call  check_CHS/3 to  check the  sub-goal Goal  against the  list of
   72%   goals already visited StackIn to  determine if  it is  a coinductive
   73%   success, a coinductive failure, an already proved sub-goal, or if it
   74%   has to be evaluated.
   75%
   76%   @arg StackOut is updated by prepending one or more elements to
   77%   StackIn.
   78%
   79%	  - [], chs(Goal)		Proved by co-induction
   80%	  - [], proved(Goal)		Proved in a completed subtree
   81%	  - From solve_goal/5		Continued execution
   82
   83check_goal(Goal, M, Parents, ProvedIn, ProvedOut, StackIn, StackOut, Model) :-
   84    check_CHS(Goal, M, Parents, ProvedIn, StackIn, Check),
   85    check_goal_(Check, Goal, M,
   86                Parents, ProvedIn, ProvedOut, StackIn, StackOut,
   87                Model),
   88    (   current_prolog_flag(scasp_dcc, true),
   89        (   Check == co_success
   90        ;   Check == cont
   91        )
   92    ->  dynamic_consistency_check(Goal, M, StackIn)
   93    ;   true
   94    ).
   95
   96% coinduction success <- cycles containing even loops may succeed
   97check_goal_(co_success, Goal, _M,
   98            _Parents, ProvedIn, ProvedOut, StackIn, StackOut,
   99            [AddGoal]) :-
  100    AddGoal = chs(Goal),
  101    add_proved(AddGoal, ProvedIn, ProvedOut),
  102    (   current_prolog_flag(scasp_assume, true)
  103    ->  mark_prev_goal(Goal, StackIn, StackMark),
  104        StackOut = [[],AddGoal|StackMark]
  105    ;   StackOut = [[],AddGoal|StackIn]
  106    ).
  107% already proved in the stack
  108check_goal_(proved, Goal, _M,
  109            _Parents, ProvedIn, ProvedOut, StackIn, StackOut,
  110            [AddGoal]) :-
  111    AddGoal = proved(Goal),
  112    add_proved(AddGoal, ProvedIn, ProvedOut),
  113    StackOut = [[], proved(Goal)|StackIn].
  114% coinduction does neither success nor fails <- the execution continues inductively
  115check_goal_(cont, Goal, M,
  116            Parents, ProvedIn, ProvedOut, StackIn, StackOut,
  117            Model) :-
  118    solve_goal(Goal, M,
  119               [Goal|Parents], ProvedIn, ProvedOut, StackIn, StackOut,
  120               Model).
  121% coinduction fails <- the negation of a call unifies with a call in the call stack
  122check_goal_(co_failure, _Goal, _M,
  123            _Parents, _ProvedIn, _ProvedOut, _StackIn, _StackOut,
  124            _Model) :-
  125    fail.
  126
  127mark_prev_goal(Goal, [I|In], [assume(Goal)|In]) :-  Goal == I, !.
  128mark_prev_goal(Goal, [I|In], [I|Mk]) :- mark_prev_goal(Goal,In,Mk).
  129mark_prev_goal(_Goal,[],[]).
  130
  131%!  dynamic_consistency_check(+Goal, +Module, +StackIn) is semidet.
  132%
  133%   Check that the resulting literal is consistent with the nmr.
  134
  135dynamic_consistency_check(Goal, M, StackIn) :-
  136    user_predicate(M:Goal),
  137    ground(Goal),
  138    M:pr_dcc_predicate(dcc(Goal), Body),
  139%   scasp_trace(scasp_trace_dcc, dcc_call(Goal, StackIn)),
  140    dynamic_consistency_eval(Body, M, StackIn),
  141    !,
  142    scasp_trace(scasp_trace_dcc, dcc_discard(Goal, Body)),
  143    fail.
  144dynamic_consistency_check(_, _, _).
  145
  146
  147dynamic_consistency_eval([], _, _).
  148dynamic_consistency_eval([SubGoal|Bs], M, StackIn) :-
  149    dynamic_consistency_eval_(SubGoal, M, StackIn),
  150    dynamic_consistency_eval(Bs, M, StackIn).
  151
  152dynamic_consistency_eval_(not(SubGoal), M, StackIn) :-
  153    user_predicate(M:SubGoal), !,
  154    member_stack(not(SubGoal), StackIn).
  155dynamic_consistency_eval_(SubGoal, M, StackIn) :-
  156    user_predicate(M:SubGoal), !,
  157    member_stack(SubGoal, StackIn).
  158dynamic_consistency_eval_(SubGoal, _, _) :-
  159    solve_goal_builtin(SubGoal, _).
  160
  161
  162%!  solve_goal(+Goal, +Module,
  163%!             +Parents, +ProvedIn, -ProvedOut, +StackIn, -StackOut,
  164%!             -Model)
  165%
  166%   Solve a  simple sub-goal  Goal where  StackIn is  the list  of goals
  167%   already visited and returns in StackOut the list of goals visited to
  168%   prove  the  sub-goals  and  in  `Model` the  model with  support the
  169%   sub-goals
  170
  171solve_goal(Goal, M, Parents, ProvedIn, ProvedOut, StackIn, StackOut, GoalModel) :-
  172    Goal = forall(_, _),
  173    !,
  174    (   current_prolog_flag(scasp_forall, Algo),
  175        ( Algo == prev -> true ; Algo == sasp )
  176        % Ciao version --prev_forall or --sasp_forall
  177    ->  solve_goal_forall(Goal, M,
  178                          Parents, ProvedIn, ProvedOut, [Goal|StackIn], StackOut,
  179                          Model)
  180    ;   solve_c_forall(Goal, M,
  181                       Parents, ProvedIn, ProvedOut, [Goal|StackIn], StackOut,
  182                       Model)
  183    ),
  184    GoalModel = [Goal|Model].
  185solve_goal(Goal, _M,
  186           _Parents, ProvedIn, ProvedOut, StackIn, [[], Goal|StackIn],
  187           GoalModel) :-
  188    Goal = not(is(V, Expresion)),
  189    add_proved(Goal, ProvedIn, ProvedOut),
  190    !,
  191    NV is Expresion,
  192    V .\=. NV,
  193    GoalModel = [Goal].
  194solve_goal(Goal, _, _, _, _, _, _, _) :-
  195    Goal = not(true),
  196    !,
  197    fail.
  198solve_goal(Goal, M, Parents, ProvedIn, ProvedOut, StackIn, StackOut, Model) :-
  199    table_predicate(M:Goal),
  200    !,
  201    verbose(format('Solve the tabled goal ~p\n', [Goal])),
  202    AttStackIn <~ stack([Goal|StackIn]),
  203    solve_goal_table_predicate(Goal, M, Parents, ProvedIn, ProvedOut,
  204                               AttStackIn, AttStackOut, AttModel),
  205    AttStackOut ~> stack(StackOut),
  206    AttModel ~> model(Model).
  207solve_goal(call(Goal), M, Parents, ProvedIn, ProvedOut, StackIn, StackOut,
  208           [call(Goal)|Model]) :-
  209    !,
  210    solve_goal(Goal, M, Parents, ProvedIn, ProvedOut, StackIn, StackOut, Model).
  211solve_goal(not(call(Goal)), M, Parents, ProvedIn, ProvedOut, StackIn, StackOut,
  212           [not(call(Goal))|Model]) :-
  213    !,
  214    solve_goal(not(Goal), M, Parents, ProvedIn, ProvedOut, StackIn, StackOut,
  215               Model).
  216solve_goal(Goal, M, Parents, ProvedIn, ProvedOut, StackIn, StackOut,
  217           [Goal|Model]) :-
  218    Goal = findall(_, _, _),
  219    !,
  220    exec_findall(Goal, M, Parents, ProvedIn, ProvedOut, StackIn, StackOut, Model).
  221solve_goal(not(Goal), M, Parents, ProvedIn, ProvedIn, StackIn, StackIn,
  222           [not(Goal)]) :-
  223    Goal = findall(_, _, _),
  224    !,
  225    exec_neg_findall(Goal, M, Parents, ProvedIn, StackIn).
  226solve_goal(Goal, M, Parents, ProvedIn, ProvedOut, StackIn, StackOut, Model) :-
  227    user_predicate(M:Goal),
  228    !,
  229    (   solve_goal_predicate(Goal, M, Parents, ProvedIn, ProvedOut,
  230                             StackIn, StackOut, Model)
  231    *-> true
  232    ;   verbose(format(' FAIL~n')),
  233        shown_predicate(M:Goal),
  234        scasp_trace(scasp_trace_failures,
  235                    trace_failure(Goal, [Goal|StackIn])),
  236        fail
  237    ).
  238solve_goal(Goal, _M, _Parents, ProvedIn, ProvedIn, StackIn, [[], Goal|StackIn],
  239           Model) :-
  240    solve_goal_builtin(Goal, Model).
  241
  242
  243mkgoal(Goal, generated(_), Goal                     ) :- !.
  244mkgoal(Goal, Origin      , goal_origin(Goal, Origin)).
  245
  246%!  solve_goal_forall(+Forall, +Module,
  247%!                    +Parents, +ProvedIn, -ProvedOut, +StackIn, -StackOut,
  248%!                    -Model)
  249%
  250%   Solve a sub-goal of the form `forall(Var,Goal)`  and success  if Var
  251%   success in all its domain for the goal Goal. It calls solve/4
  252%
  253%   @arg Forall is a term forall(?Var, ?Goal)
  254
  255solve_goal_forall(forall(Var, Goal), M,
  256                  Parents, ProvedIn, ProvedOut, StackIn, [[]|StackOut],
  257                  Model) :-
  258    my_copy_term(Var, Goal, NewVar, NewGoal),
  259    my_copy_term(Var, Goal, NewVar2, NewGoal2),
  260    solve([NewGoal], M, Parents, ProvedIn, ProvedMid, StackIn, [[]|StackMid],
  261          ModelMid),
  262    verbose(format('\tSuccess solve ~@\n\t\t for the ~@\n',
  263                   [print_goal(NewGoal), print_goal(forall(Var, Goal))])),
  264    check_unbound(NewVar, List),
  265    (   List == ground
  266    ->  verbose(format('The var ~p is grounded so try with other clause\n',
  267                       [NewVar])),
  268        fail
  269    ;   List == []
  270    ->  ProvedOut = ProvedMid,
  271        StackOut = StackMid,
  272        Model = ModelMid
  273    ;   List = clpq(NewVar3, Constraints)
  274    ->  findall(dual(NewVar3, ConDual),
  275                dual_clpq(Constraints, ConDual),
  276                DualList),
  277        verbose(format('Executing ~@ with clpq ConstraintList = ~p\n',
  278                       [print_goal(Goal), DualList])),
  279        exec_with_clpq_constraints(NewVar2, NewGoal2, M,
  280                                   entry(NewVar3, []),
  281                                   DualList,
  282                                   Parents, ProvedMid, ProvedOut,
  283                                   StackMid, StackOut, ModelList),
  284        !,
  285        append(ModelMid, ModelList, Model)
  286    ;   verbose(format('Executing ~@ with clp_disequality list = ~p\n',
  287                       [print_goal(Goal), List])),
  288        (   current_prolog_flag(scasp_forall, prev)
  289        ->  !  % Ciao --prev_forall: remove answers in max.lp
  290        ;   true
  291        ),
  292        exec_with_neg_list(NewVar2, NewGoal2, M,
  293                           List, Parents, ProvedMid, ProvedOut,
  294                           StackMid, StackOut, ModelList),
  295        (   current_prolog_flag(scasp_forall, sasp)
  296        ->  !  % Ciao --sasp_forall: remove answers in hamcycle_two.lp
  297               % Without cuts the evaluation may loop - e.g. queens.lp
  298        ;   true
  299        ),
  300        append(ModelMid, ModelList, Model)
  301    ).
  302
  303check_unbound(Var, ground) :-
  304    ground(Var), !.
  305check_unbound(Var, List) :-
  306    get_neg_var(Var, List), !.
  307check_unbound(Var, 'clpq'(NewVar, Constraints)) :-
  308    dump_clpq_var([Var], [NewVar], Constraints),
  309    Constraints \== [], !.
  310check_unbound(Var, []) :-
  311    var(Var), !.
  312
  313exec_with_clpq_constraints(_Var, _Goal, _M, _, [],
  314                           _Parents, ProvedIn, ProvedIn, StackIn, StackIn, []).
  315exec_with_clpq_constraints(Var, Goal, M, entry(ConVar, ConEntry),
  316                           [dual(ConVar, ConDual)|Duals],
  317                           Parents, ProvedIn, ProvedOut, StackIn, StackOut,
  318                           Model) :-
  319    my_copy_term(Var,   [Goal,   Parents,   StackIn,   ProvedIn],
  320                 Var01, [Goal01, Parents01, StackIn01, ProvedIn01]),
  321    append(ConEntry, ConDual, Con),
  322    my_copy_term(ConVar, Con, ConVar01, Con01),
  323    my_copy_term(Var, Goal, Var02, Goal02),
  324    my_copy_term(ConVar, ConEntry, ConVar02, ConEntry02),
  325    Var01 = ConVar,
  326    (   apply_clpq_constraints(Con)
  327    ->  verbose(format('Executing ~p with clpq_constrains ~p\n',
  328                       [Goal01, Con])),
  329        solve([Goal01], M, Parents01, ProvedIn01, ProvedOut01, StackIn01, [[]|StackOut01], Model01),
  330        verbose(format('Success executing ~p with constrains ~p\n',
  331                       [Goal01, Con])),
  332        verbose(format('Check entails Var = ~p with const ~p and ~p\n',
  333                       [Var01, ConVar01, Con01])),
  334        (   entails([Var01], ([ConVar01], Con01))
  335        ->  verbose(format('\tOK\n', [])),
  336            StackOut02 = StackOut01,
  337            Model03 = Model01
  338        ;   verbose(format('\tFail\n', [])),
  339            dump_clpq_var([Var01], [ConVar01], ExitCon),
  340            findall(dual(ConVar01, ConDual01),
  341                    dual_clpq(ExitCon, ConDual01),
  342                    DualList),
  343            verbose(format('Executing ~p with clpq ConstraintList = ~p\n',
  344                           [Goal, DualList])),
  345            exec_with_clpq_constraints(Var, Goal, M, entry(ConVar01, Con01),
  346                                       DualList,
  347                                       Parents01, ProvedOut01, ProvedOut02,
  348                                       StackOut01, StackOut02, Model02),
  349            append(Model01, Model02, Model03)
  350        )
  351    ;   verbose(format('Skip execution of an already checked \c
  352                        constraint ~p (it is inconsitent with ~p)\n',
  353                       [ConDual, ConEntry])),
  354        StackOut02 = StackIn01,
  355        Model03 = []
  356    ),
  357    verbose(format('Executing ~p with clpq ConstraintList = ~p\n',
  358                   [Goal, Duals])),
  359    exec_with_clpq_constraints(Var02, Goal02, M,
  360                               entry(ConVar02, ConEntry02),
  361                               Duals, Parents, ProvedOut02, ProvedOut,
  362                               StackOut02, StackOut, Model04),
  363    append(Model03, Model04, Model).
  364
  365exec_with_neg_list(_, _, _, [], _, ProvedIn, ProvedIn, StackIn, StackIn, []).
  366exec_with_neg_list(Var, Goal, M, [Value|Vs],
  367                   Parents, ProvedIn, ProvedOut, StackIn, StackOut,
  368                   Model) :-
  369    my_copy_term(Var, [Goal, StackIn], NewVar, [NewGoal, NewStackIn]),
  370    NewVar = Value,
  371    verbose(format('Executing ~p with value ~p\n', [NewGoal, Value])),
  372    solve([NewGoal], M, Parents,
  373          ProvedIn, ProvedMid, NewStackIn, [[]|NewStackMid], ModelMid),
  374    verbose(format('Success executing ~p with value ~p\n',
  375                   [NewGoal, Value])),
  376    exec_with_neg_list(Var, Goal, M, Vs, Parents,
  377                       ProvedMid, ProvedOut, NewStackMid, StackOut, Models),
  378    append(ModelMid, Models, Model).
  379
  380%!  solve_goal_table_predicate(+Goal, +Module, +Parents, +ProvedIn, -ProvedOut,
  381%!                             +AttStackIn, -AttStackOut, -AttModel)
  382%
  383%   Used to evaluate predicates under tabling. This predicates should be
  384%   defined in the program using the directive _#table pred/n._
  385
  386solve_goal_table_predicate(Goal, M, Parents, ProvedIn, ProvedOut, AttStackIn, AttStackOut, AttModel) :-
  387    M:pr_rule(Goal, Body, _Origin),
  388    AttStackIn ~> stack(StackIn),
  389    solve(Body, M, Parents, ProvedIn, ProvedOut, StackIn, StackOut, Model),
  390    AttStackOut <~ stack(StackOut),
  391    AttModel <~ model([Goal|Model]).
  392
  393%!  solve_goal_predicate(+Goal, +Module,
  394%!                       +Parents, +ProvedIn, -ProvedOut, +StackIn, -StackOut,
  395%!                       -Model)
  396%
  397%   Used to evaluate a user predicate
  398
  399solve_goal_predicate(Goal, M, Parents, ProvedIn, ProvedOut, StackIn, StackOut,
  400                     GoalModel) :-
  401    M:pr_rule(Goal, Body, Origin),
  402    mkgoal(Goal, Origin, StackGoal),
  403    solve(Body, M, Parents, ProvedIn, ProvedMid, [StackGoal|StackIn], StackOut, BodyModel),
  404    add_proved(Goal, ProvedMid, ProvedOut),
  405    GoalModel = [Goal|BodyModel].
  406
  407%!  solve_goal_builtin(+Goal, -Model)
  408%
  409%   Used to evaluate builtin predicates predicate
  410
  411solve_goal_builtin(is(X, Exp), Model) :-
  412    exec_goal(is(X, Exp)),
  413    Model = [is(X, Exp)]. %% the Model should 'Start' with the Goal
  414solve_goal_builtin(builtin(Goal), Model) :- !,
  415    exec_goal(Goal),
  416    Model = [builtin(Goal)].
  417solve_goal_builtin(Goal, Model) :-
  418    clp_builtin(Goal), !,
  419    exec_goal(apply_clpq_constraints(Goal)),
  420    Model = [Goal].
  421solve_goal_builtin(Goal, Model) :-
  422    clp_interval(Goal), !,
  423    exec_goal(Goal),
  424    Model = [Goal].
  425solve_goal_builtin(not(Goal), _Model) :-
  426    clp_interval(Goal), !,
  427    scasp_warning(scasp(failure_calling_negation(Goal))),
  428    fail.
  429solve_goal_builtin(Goal, Model) :-
  430    clp_builtin(Goal),
  431    !,
  432    exec_goal(apply_clpq_constraints(Goal)),
  433    Model = [Goal].
  434solve_goal_builtin(Goal, Model) :-
  435    prolog_builtin(Goal), !,
  436    exec_goal(Goal),
  437    Model = [Goal].
  438% The predicate is not defined as user_predicates neither builtin
  439solve_goal_builtin(Goal, Model) :-
  440    verbose(format('The predicate ~p is not user_defined / builtin\n', [Goal])),
  441    (   Goal = not(_)
  442    ->  Model = [Goal] %% the negation of a not defined predicate success.
  443    ;   fail %% a not defined predicate allways fails.
  444    ).
  445
  446exec_goal(A \= B) :- !,
  447    verbose(format('exec ~@\n', [print_goal(A \= B)])),
  448    A .\=. B,
  449    verbose(format('ok   ~@\n', [print_goal(A \= B)])).
  450exec_goal(Goal) :-
  451    (   current_prolog_flag(scasp_verbose, true)
  452    ->  E = error(_,_),
  453        verbose(format('exec goal ~@ \n', [print_goal(Goal)])),
  454        catch(call(Goal), E, (print_message(warning, E), fail)),
  455        verbose(format('ok   goal ~@ \n', [print_goal(Goal)]))
  456    ;   catch(call(Goal), error(_,_), fail)
  457    ).
  458
  459% TODO: Pending StackOut to carry the literal involved in the findall
  460% (if needed)
  461% TODO: Handling of ProvedIn/ProvedOut
  462
  463%!  exec_findall(+Findall, +Module,
  464%!		 +ProvedIn, -ProvedOut, +StackIn, -StackOut, -Model)
  465
  466exec_findall(findall(Var, Call, List), M,
  467             Parents, ProvedIn, ProvedOut, StackIn, StackOut, Model) :-
  468    verbose(format('execution of findall(~p, ~p, _) \n', [Var, Call])),
  469    findall(t(Var, S, Mdl), (
  470            solve([Call], M, Parents, ProvedIn, _ProvedOut, StackIn, S0, Mdl),
  471            append(S, StackIn, S0)
  472        ), VSMList),
  473    process_vsmlist(VSMList, List, SOut, Model),
  474    append(SOut, [findall(Var, Call, List)|StackIn], StackOut),
  475    stack_proved(StackOut, ProvedOut),
  476    verbose(format('Result execution = ~p \n', [List])).
  477
  478process_vsmlist(VSMList, List, [[]|StackOut], Model) :-
  479    process_vsmlist_(VSMList, List, StackOut, Model).
  480
  481process_vsmlist_([], [], [], []).
  482process_vsmlist_([t(V, [[]|S], M)|Rs], [V|Vs], S1, M1) :-
  483    process_vsmlist_(Rs, Vs, S0, M0),
  484    append(S0, S, S1),
  485    append(M, M0, M1).
  486
  487% TODO: What to do with the negation of findall/3 (if required)
  488exec_neg_findall(Goal, _, _, _, _) :-
  489    verbose(format('PENDING: execution of not ~p \n', [Goal])),
  490    fail.
  491
  492
  493%!  check_CHS(+Goal, +Module, +Parents, +ProvedIn, +StackIn, -Result) is det.
  494%
  495%   Checks the StackIn and returns  in  Result   if  the  goal Goal is a
  496%   coinductive success, a coinductive  failure   or  an  already proved
  497%   goal. Otherwise it is constraint against  its negation atoms already
  498%   visited.
  499
  500:- det(check_CHS/6).  501
  502check_CHS(Goal, M, Parents, Proved, I, Result) :-
  503    (   user_predicate(M:Goal)
  504    ->  check_CHS_(Goal, M, Parents, Proved, I, Result)
  505    ;   Result = cont
  506    ).
  507
  508% inmediate success if the goal has already been proved.
  509check_CHS_(Goal, _M, _Parents, Proved, _Stack, proved) :-
  510    ground(Goal),
  511    proved_in_stack(Goal, Proved),
  512    !.
  513% coinduction success <- cycles containing even loops may succeed
  514check_CHS_(Goal, _M, Parents, _Proved, _I, co_success) :-
  515    check_parents(Goal, Parents, even),
  516    !.
  517% coinduction fails <- the goal is entailed by its negation in the
  518% call stack
  519check_CHS_(Goal, _M, Parents, Proved, _Stack, co_failure) :-
  520    neg_in_stack(Goal, Parents, Proved), !,
  521    verbose(format('Negation of the goal in the stack, failling (Goal = ~w)\n', [Goal])).
  522% coinduction fails <- cycles containing positive loops can be solved
  523% using tabling
  524check_CHS_(Goal, M, Parents, _Proved, _Stask, co_failure) :-
  525    \+ table_predicate(M:Goal),
  526    \+ current_prolog_flag(scasp_no_fail_loop, true),
  527    \+ \+ (
  528        check_parents(Goal, Parents, fail_pos(S)),
  529        verbose(format('Positive loop, failing (Goal == ~w)\n', [Goal])),
  530        scasp_warning(scasp_warn_pos_loops, pos_loop(fail, Goal, S))
  531    ), !.
  532check_CHS_(Goal, M, Parents, _Proved, _Stack, _Cont) :-
  533    \+ table_predicate(M:Goal),
  534    \+ \+ (
  535        check_parents(Goal, Parents, pos(S)),
  536        verbose(format('Positive loop, continuing (Goal = ~w)\n', [Goal])),
  537        scasp_info(scasp_warn_pos_loops, pos_loop(continue, Goal, S))
  538    ), fail.
  539% coinduction does not succeed or fail <- the execution continues inductively
  540check_CHS_(Goal, _M, Parents, Proved, _Stack, cont) :-
  541    (   ground(Goal)
  542    ->  constrained_neg_in_stack(Goal, Parents, Proved)
  543    ;   ground_neg_in_stack(Goal, Parents, Proved)
  544    ).
  545
  546%!  neg_in_stack(+Goal, +Parents, +Proved) is semidet.
  547%
  548%   True when the nagation of  Goal  is  in   Stack.  If  so  we  have a
  549%   coinductive failure. Check on variants   which  requires tabling for
  550%   proper results.
  551
  552neg_in_stack(Goal, _Parents, Proved) :-
  553    proved_relatives(Goal, Proved, Relatives),
  554    member(Relative, Relatives),
  555    is_negated_goal(Goal, Relative),
  556    !.
  557neg_in_stack(Goal, Parents, _) :-
  558    member(Relative, Parents),
  559    is_negated_goal(Goal, Relative),
  560    !.
  561
  562is_negated_goal(Goal, Head) :-
  563    (   Goal = not(G)
  564    ->  (   G == Head
  565        ->  true
  566        ;   G =@= Head
  567        ->  scasp_warning(co_failing_in_negated_loop(G, Head))
  568        )
  569    ;   Head = not(NegGoal)
  570    ->  (   Goal == NegGoal
  571        ->  true
  572        ;   Goal =@= NegGoal
  573        ->  scasp_warning(co_failing_in_negated_loop(Goal, NegGoal))
  574        )
  575    ).
  576
  577%!  ground_neg_in_stack(++Goal, +Parents, +Proved) is det.
  578%
  579%   Propagate disequality constraints of Goal  through matching goals on
  580%   the stack.
  581
  582:- det(ground_neg_in_stack/3).  583
  584ground_neg_in_stack(Goal, Parents, Proved) :-
  585    verbose(format('Enter ground_neg_in_stack for ~@\n', [print_goal(Goal)])),
  586    (   proved_relatives(Goal, Proved, Relatives)
  587    ->  maplist(ground_neg_in_stack_(Flag, Goal), Relatives)
  588    ;   true
  589    ),
  590    maplist(ground_neg_in_stack_(Flag, Goal), Parents),
  591    (   Flag == found
  592    ->  verbose(format('\tThere exit the negation of ~@\n\n', [print_goal(Goal)]))
  593    ;   true
  594    ).
  595
  596ground_neg_in_stack_(found, TGoal, SGoal) :-
  597    gn_match(TGoal, SGoal, Goal, NegGoal),
  598    \+ Goal \= NegGoal,
  599    verbose(format('\t\tCheck disequality of ~@ and ~@\n',
  600                   [print_goal(TGoal), print_goal(SGoal)])),
  601    loop_term(Goal, NegGoal),
  602    !.
  603ground_neg_in_stack_(_, _, _).
  604
  605gn_match(Goal, chs(not(NegGoal)), Goal, NegGoal) :- !.
  606gn_match(not(Goal), chs(NegGoal), Goal, NegGoal) :- !.
  607gn_match(not(Goal), NegGoal,      Goal, NegGoal) :- !.
  608
  609
  610%!  constrained_neg_in_stack(+Goal, +Parents, +Proved) is det.
  611%
  612%   Propagate the fact that we accept Goal into all other accepted goals
  613%   in the stack.
  614
  615:- det(constrained_neg_in_stack/3).  616
  617constrained_neg_in_stack(Goal, Parents, Proved) :-
  618    (   proved_relatives(Goal, Proved, Relatives)
  619    ->  maplist(contrained_neg(Goal), Relatives)
  620    ;   true
  621    ),
  622    maplist(contrained_neg(Goal), Parents).
  623
  624contrained_neg(not(Goal), NegGoal) :-
  625    is_same_functor(Goal, NegGoal),
  626    verbose(format('\t\tCheck if not(~@) is consistent with ~@\n',
  627                   [print_goal(Goal), print_goal(NegGoal)])), !,
  628    loop_term(Goal, NegGoal),
  629    !,
  630    verbose(format('\t\tOK\n', [])).
  631contrained_neg(Goal, not(NegGoal)) :-
  632    is_same_functor(Goal, NegGoal),
  633    verbose(format('\t\tCheck if not(~@) is consistent with ~@\n',
  634                   [print_goal(Goal), print_goal(NegGoal)])), !,
  635    loop_term(Goal, NegGoal),
  636    !,
  637    verbose(format('\t\tOK\n', [])).
  638contrained_neg(_,_).
  639
  640is_same_functor(Term1, Term2) :-
  641    functor(Term1, Name, Arity, Type),
  642    functor(Term2, Name, Arity, Type).
  643
  644%!  proved_in_stack(+Goal, +Proved) is semidet.
  645%
  646%   True when Goal appears in one of  the finished branches of the proof
  647%   tree, i.e., it appears in Stack, but not as direct parent.
  648
  649proved_in_stack(Goal, Proved) :-
  650    proved_relatives(Goal, Proved, Relatives),
  651    member(Relative, Relatives),
  652    (   Goal == Relative
  653    ;   Goal == chs(Relative)
  654    ),
  655    !.
  656
  657%!  check_parents(+Goal, +Parents, -Type) is semidet.
  658%
  659%   Type is the coinductive result. This is   `even`  if we have an even
  660%   loop through negation or a simple positive match.
  661
  662check_parents(not(Goal), Parents, Type) :-
  663    !,
  664    check_parents(not(Goal), 1, Parents, Type).
  665check_parents(Goal, Parents, Type) :-
  666    check_parents(Goal, 0, Parents, Type).
  667
  668check_parents(Goal, 0, [Parent|_Parents], Type) :-
  669    (   \+ \+ type_loop_fail_pos(Goal, Parent)
  670    ->  Type = fail_pos(Parent)
  671    ;   \+ Goal \= Parent
  672    ->  Type = pos(Parent)
  673    ),
  674    !.
  675check_parents(Goal, N, [Parent|Parents], Type) :-
  676    (   even_loop(Goal, Parent, N)
  677    ->  Type = even
  678    ;   Goal \== Parent
  679    ->  (  Parent = not(_)
  680        ->  NewN is N + 1,
  681            check_parents(Goal, NewN, Parents, Type)
  682        ;   check_parents(Goal, N, Parents, Type)
  683        )
  684    ).
  685
  686even_loop(not(Goal), not(Parent), _) :-
  687    Goal =@= Parent,
  688    !,
  689    Goal = Parent.
  690even_loop(Goal, Parent, N) :-
  691    Goal \= not(_),
  692    Goal == Parent,
  693    N > 0,
  694    0 =:= mod(N, 2).
  695
  696type_loop_fail_pos(Goal, S) :-
  697    Goal == S, !.
  698type_loop_fail_pos(Goal, S) :-
  699    variant(Goal, S), !,
  700    scasp_warning(variant_loop(Goal, S)).
  701type_loop_fail_pos(Goal, S) :-
  702    entail_terms(Goal, S),
  703    scasp_warning(subsumed_loop(Goal, S)).
  704
  705%!  stack_parents(+Stack, -Parents) is det.
  706%
  707%   Get the direct callers from  Stack.   Stack  contains  both previous
  708%   proved stacks as well as the current list of parents.
  709
  710:- det(stack_parents/2).  711stack_parents(Stack, Parents) :-
  712    stack_parents(Stack, 0, Parents).
  713
  714stack_parents([], _, []).
  715stack_parents([[]|T], N, Parents) :-
  716    !,
  717    N1 is N-1,
  718    stack_parents(T, N1, Parents).
  719stack_parents([_|T], N, Parents) :-
  720    N < 0,
  721    !,
  722    N1 is N+1,
  723    stack_parents(T, N1, Parents).
  724stack_parents([goal_origin(H, _)|T], N, [H|TP]) :-
  725    !,
  726    stack_parents(T, N, TP).
  727stack_parents([H|T], N, [H|TP]) :-
  728    stack_parents(T, N, TP).
  729
  730%!  stack_proved(Stack, Proved:assoc) is det.
  731%
  732%   True when Proved is an assoc  holding   all  goals that have already
  733%   been proved in Stack. This excludes  the   direct  parents of in the
  734%   stack, i.e. only adds goals from already completed branches.
  735%
  736%   The code is based on  the   old  proved_in_stack/2. Effectively this
  737%   extracts the other half than stack_parents/2,  so possibly we should
  738%   sync the code with that.
  739
  740:- det(stack_proved/2).  741
  742stack_proved(Stack, Proved) :-
  743    empty_assoc(Proved0),
  744    stack_proved(Stack, 0, -1, Proved0, Proved).
  745
  746stack_proved([], _, _, Proved, Proved).
  747stack_proved([Top|Ss], Intervening, MaxInter, Proved0, Proved) :-
  748    (   Top == []
  749    ->  NewInter is Intervening - 1,
  750        stack_proved(Ss, NewInter, MaxInter, Proved0, Proved)
  751    ;   Intervening > MaxInter
  752    ->  NewMaxInter is max(MaxInter, Intervening),
  753        NewInter is Intervening + 1,
  754        stack_proved(Ss, NewInter, NewMaxInter, Proved0, Proved)
  755    ;   add_proved(Top, Proved0, Proved1),
  756        stack_proved(Ss, Intervening, MaxInter, Proved1, Proved)
  757    ).
  758
  759add_proved(goal_origin(Goal, _), Assoc0, Assoc) =>
  760    add_proved(Goal, Goal, Assoc0, Assoc).
  761add_proved(Goal, Assoc0, Assoc) =>
  762    add_proved(Goal, Goal, Assoc0, Assoc).
  763
  764add_proved(not(Term), Goal, Assoc0, Assoc) =>
  765    add_proved(Term, Goal, Assoc0, Assoc).
  766add_proved(chs(Term), Goal, Assoc0, Assoc) =>
  767    add_proved(Term, Goal, Assoc0, Assoc).
  768add_proved(forall(_,_), _Goal, Assoc0, Assoc) =>
  769    Assoc = Assoc0.
  770add_proved(Term, Goal, Assoc0, Assoc) =>
  771    functor(Term, Name, Arity),
  772    (   get_assoc(Name/Arity, Assoc0, List, Assoc, [Goal|List])
  773    ->  true
  774    ;   put_assoc(Name/Arity, Assoc0, [Goal], Assoc)
  775    ).
  776
  777%!  solve_c_forall(+Forall, +Module,
  778%!                 +Parents, +ProvedIn, -ProvedOut, +StackIn, -StackOut,
  779%!                 -Model)
  780%
  781%   Solve a sub-goal of the form c_forall(Vars,Goal) and succeeds if the
  782%   goal `Goal` succeeds covering the domain of all the vars in the list
  783%   of vars `Vars. It calls solve/4
  784%
  785%   @arg Forall is a term forall(Var, Goal).
  786%   @tbd Improve the efficiency by removing redundant justifications w.o.
  787%   losing solutions.
  788
  789solve_c_forall(Forall, M, Parents, ProvedIn, ProvedOut, StackIn, [[]|StackOut],
  790               Model) :-
  791    collect_vars(Forall, c_forall(Vars0, Goal0)),    % c_forall([F,G], not q_1(F,G))
  792
  793    verbose(format('\nc_forall(~p,\t~@)\n\n',[Vars0, print_goal(Goal0)])),
  794
  795    my_copy_vars(Vars0, Goal0, Vars1, Goal1),        % Vars should remain free
  796    my_diff_term(Goal1, Vars1, OtherVars),
  797    Initial_Const = [],                              % Constraint store = top
  798    (   current_prolog_flag(scasp_forall, all_c)     % Ciao --all_c_forall
  799    ->  solve_var_forall_(Goal1, M, Parents, ProvedIn, ProvedOut,
  800                          entry(Vars1, Initial_Const),
  801                          dual(Vars1, [Initial_Const]),
  802                          OtherVars, StackIn, StackOut, Model)
  803    ;   solve_other_forall(Goal1, M, Parents, ProvedIn, ProvedOut,
  804                           entry(Vars1, Initial_Const),
  805                           dual(Vars1, [Initial_Const]),
  806                           OtherVars, StackIn, StackOut, Model)
  807    ).
  808
  809solve_other_forall(Goal, M, Parents, ProvedIn, ProvedOutExit,
  810                   entry(Vars, Initial_Const),
  811                   dual(Vars, [Initial_Const]),
  812                   OtherVars, StackIn, StackOutExit, ModelExit) :-
  813    append(Vars,OtherVars,AllVars),
  814    my_copy_vars(AllVars,   [Goal,  Parents,  ProvedIn,  StackIn,  OtherVars,  Vars],
  815                 _AllVars1, [Goal1, Parents1, ProvedIn1, StackIn1, OtherVars1, Vars1]),
  816    my_copy_vars(AllVars,   [Goal,  Parents,  ProvedIn,  StackIn,  OtherVars,  Vars],
  817                 _AllVars2, [Goal2, Parents2, ProvedIn2, StackIn2, OtherVars2, Vars2]),
  818
  819    verbose(format("solve other forall:\n\c
  820                           \t Goal \t~p\n\c
  821                           \t Vars1       \t~p\n\c
  822                           \t OtherVars   \t~p\n\c
  823                           \t StackIn     \t~p\n\n",
  824                          ['G'(Goal),'G'(Vars1),
  825                           'G'(OtherVars),'G'(StackIn)])),
  826
  827    % disequality and clp for numbers
  828    dump_constraint(OtherVars, OtherVars1, Dump, []-[], Pending-Pending1), !,
  829    clpqr_dump_constraints(Pending, Pending1, CLP),
  830    append(CLP, Dump, Constraints1),
  831    my_copy_vars(OtherVars1, Constraints1, OtherVars2, Constraints2),
  832
  833    verbose(format("solve other forall:\n\c
  834                          \t OtherVars1   \t~p\n\c
  835                          \t OtherVars2   \t~p\n\c
  836                          \t Constraints1 \t~p\n\c
  837                          \t Constraints2 \t~p\n\n",
  838                          ['G'(OtherVars1), 'G'(OtherVars2),
  839                           'G'(Constraints1), 'G'(Constraints2)])),
  840
  841    apply_const_store(Constraints1),
  842    !,
  843
  844    solve_var_forall_(Goal1, M, Parents1, ProvedIn1, ProvedOut,
  845                      entry(Vars1, Initial_Const),
  846                      dual(Vars1, [Initial_Const]), OtherVars1,
  847                      StackIn1, StackOut, Model),
  848    !,
  849    (   OtherVars = OtherVars1,
  850        StackOutExit = StackOut,
  851        ModelExit = Model,
  852        ProvedOutExit = ProvedOut
  853    ;   \+ ground(OtherVars),
  854        apply_const_store(Constraints2),
  855        % disequality and clp for numbers
  856        dump_constraint(OtherVars1, OtherVars2, Dump1, []-[], Pend-Pend1), !,
  857        clpqr_dump_constraints(Pend, Pend1, CLP1),
  858        append(CLP1, Dump1, AnsConstraints2),
  859        make_duals(AnsConstraints2, Duals),
  860        member(Dual, Duals),
  861        apply_const_store(Dual),
  862        solve_other_forall(Goal2, M, Parents2, ProvedIn2, ProvedOutExit,
  863                           entry(Vars2, Initial_Const),
  864                           dual(Vars2, [Initial_Const]),
  865                           OtherVars2, StackIn2, StackOutExit, ModelExit), !,
  866        OtherVars = OtherVars2
  867    ).
  868
  869%!  solve_var_forall_(+Goal, +Module, +Parents, +ProvedIn, -ProvedOut,
  870%!                    +Entry, +Duals, +OtherVars,
  871%!                    +StackIn, -StackOut, -Model) is nondet.
  872%
  873%   Implements the _forall_ algorithm as described   in section 2.3 from
  874%   "Constraint Answer Set Programming  without   Grounding"  by Joaquin
  875%   Arias et all. It works different though.
  876%
  877%     - For each step  we  copy  the   Goal,  solve  it  and compute the
  878%       instantiations created by Goal. From these instantiations we
  879%       compute the _duals_.
  880%     - Continue until all duals are proved.
  881%
  882%   Note that the constraints on the   _forall variables_ are maintained
  883%   explicitly.
  884
  885solve_var_forall_(_Goal, _M, _Parents, Proved, Proved, _, dual(_, []),
  886                  _OtherVars, StackIn, StackIn, []) :- !.
  887solve_var_forall_(Goal, M, Parents, ProvedIn, ProvedOut,
  888                  entry(C_Vars, Prev_Store),
  889                  dual(C_Vars, [C_St|C_Stores]),
  890                  OtherVars, StackIn, StackOut, Model) :-
  891    verbose(format("solve forall:\n\c
  892                          \tPrev_Store \t~p\n\c
  893                          \tC_St       \t~p\n\c
  894                          \tC_Stores   \t~p\n\c
  895                          \tStackIn    \t~p\n\n",
  896                          ['G'(Prev_Store),'G'(C_St),
  897                           'G'(C_Stores),'G'(StackIn)])),
  898
  899    my_copy_vars(C_Vars,  [Goal,Prev_Store,C_St],
  900                 C_Vars1, [Goal1,Prev_Store1,C_St1]),
  901    my_copy_vars(C_Vars,  [Goal,Prev_Store,C_Stores],
  902                 C_Vars2, [Goal2,Prev_Store2,C_Stores2]),
  903
  904    apply_const_store(Prev_Store),
  905    (   %verbose(format('apply_const_store ~@\n',[print_goal(C_St)])),
  906        apply_const_store(C_St) % apply a Dual
  907    ->  solve([Goal], M, Parents, ProvedIn, ProvedOut1, StackIn, [[]|StackOut1], Model1),
  908        find_duals(C_Vars, C_Vars1, OtherVars, Duals),       %% New Duals
  909        verbose(format('Duals = \t ~p\n',[Duals])),
  910        append_set(Prev_Store1, C_St1, Current_Store1),
  911        solve_var_forall_(Goal1, M, Parents, ProvedOut1, ProvedOut2,
  912                          entry(C_Vars1, Current_Store1),
  913                          dual(C_Vars1, Duals),
  914                          OtherVars, StackOut1, StackOut2, Model2),
  915        append(Model1,Model2,Model3)
  916    ;   verbose(format('Entail: Fail  applying \t ~p\n', ['G'(C_St)])),
  917        %% The dual C_St is not consistent with Prev_Store -> already checked (entails)
  918        ProvedOut2 = ProvedIn,
  919        StackOut2 = StackIn,
  920        Model3 = []
  921    ),
  922    solve_var_forall_(Goal2, M, Parents, ProvedOut2, ProvedOut,
  923                      entry(C_Vars2, Prev_Store2),
  924                      dual(C_Vars2, C_Stores2),
  925                      OtherVars, StackOut2, StackOut, Model4),
  926    append(Model3, Model4, Model).
  927
  928append_set([],X,X):- !.
  929append_set([A|As],Bs,Cs) :-
  930    \+ \+ memberchk_oc(A, Bs),
  931    !,
  932    append_set(As,Bs,Cs).
  933append_set([A|As],Bs,[A|Cs]) :-
  934    append_set(As,Bs,Cs).
  935
  936memberchk_oc(Term, [H|T]) :-
  937    (   unify_with_occurs_check(Term, H)
  938    ->  true
  939    ;   memberchk_oc(Term, T)
  940    ).
  941
  942apply_const_store([]) :- !.
  943apply_const_store([C|Cs]) :-
  944    apply_constraint(C),
  945    apply_const_store(Cs).
  946
  947apply_constraint(A \= B) =>
  948    A .\=. B.
  949apply_constraint(A = B) =>
  950    A = B.
  951apply_constraint(CLPConstraint) =>
  952    apply_clpq_constraints(CLPConstraint).
  953
  954%!  find_duals(+C_Vars, +C_Vars1, +OtherVars, -Duals)
  955%
  956%   C_Vars is the list of forall variables   after solve/4. C_Vars1 is a
  957%   copy of this list before calling solve/4.   Our  task is to create a
  958%   _dual_ model from the instantiation. If   subsequently  we can prove
  959%   the dual model to be true then  we   proved  the forall is true. For
  960%   example, if solve  succeeded  with  [X]   -->  [q],  it  created the
  961%   instantiation X=q. It we now can prove X\=q, we proved solve is true
  962%   for all X.
  963%
  964%   @see Section 2.3 from  "Constraint   Answer  Set Programming without
  965%   Grounding" by Joaquin Arias et all.
  966%   @tbd JW: it is not clear to me why OtherVars is needed and why it is
  967%   not copied.
  968
  969find_duals(C_Vars, C_Vars1, OtherVars, Duals) :-
  970    % disequality and clp for numbers
  971    dump_constraint(C_Vars, C_Vars1, Dump, []-[], Pending-Pending1), !,
  972    clp_vars_in(OtherVars, OtherCLPVars),		% clp(Q) vars
  973    append(Pending, OtherCLPVars, CLPVars),
  974    append(Pending1, OtherCLPVars, CLPVars1),
  975    clpqr_dump_constraints(CLPVars, CLPVars1, CLP),
  976    append(CLP, Dump, Constraints),
  977    make_duals(Constraints,Duals), !.
  978
  979make_duals(Ls,Ds) :-
  980    make_duals_([],Ls,[],Ds).
  981
  982make_duals_(_,[],Ds,Ds).
  983make_duals_(Prev,[A|As],D0,Ds) :-
  984    append(Prev,[A],Prev1),
  985    make_duals_(Prev1,As,D0,D1),
  986    dual(A,Duals_A),
  987    combine(Duals_A,Prev,As,Ls),
  988    append(Ls,D1,Ds).
  989
  990combine([A],Prev,Post,[Rs]) :-
  991    append(Prev,[A|Post],Rs).
  992combine([A,B|As],Prev,Post,[RA|RAs]) :-
  993    append(Prev,[A|Post],RA),
  994    combine([B|As],Prev,Post,RAs).
  995
  996:- det(dual/2).  997
  998dual(#=(A,B), [#<(A,B), #>(A,B)]).
  999dual(#<(A,B), [#>=(A,B)]).
 1000dual(#>(A,B), [#=<(A,B)]).
 1001dual(#=<(A,B), [#>(A,B)]).
 1002dual(#>=(A,B), [#<(A,B)]).
 1003
 1004dual(=(A,B), [\=(A,B)]).
 1005dual(\=(A,B), [=(A,B)]).
 1006
 1007
 1008%!  dump_constraint(+C_Vars, +C_Vars1, -Dump, +Pending0, -Pending) is det
 1009%
 1010%   @arg Dump is a list of V1=B and V1\=B, where V1 is a variable from
 1011%   C_Vars1.
 1012%   @arg Pending is a pair of lists with variables from C_Vars and
 1013%   C_Vars1 that are not processed (in reverse order, why?)
 1014
 1015:- det(dump_constraint/5). 1016dump_constraint([], [], [], Pending, Pending).
 1017dump_constraint([V|Vs], [V1|V1s], [V1 = V | Vs_Dump], P0, P1) :-
 1018    ground(V), !,
 1019    dump_constraint(Vs, V1s, Vs_Dump, P0, P1).
 1020dump_constraint([V|Vs], [V1|V1s], Rs_Dump, P0, P1) :-
 1021    get_neg_var(V, List),
 1022    List \== [], !,
 1023    dump_neg_list(V1, List, V_Dump),
 1024    dump_constraint(Vs, V1s, Vs_Dump, P0, P1),
 1025    append(V_Dump, Vs_Dump, Rs_Dump).
 1026dump_constraint([V|Vs], [V1|V1s], Vs_Dump, PV-PV1, P1) :-
 1027    dump_constraint(Vs, V1s, Vs_Dump, [V|PV]-[V1|PV1], P1).
 1028
 1029dump_neg_list(_,[],[]) :- !.
 1030dump_neg_list(V,[L|Ls],[V \= L|Rs]) :- dump_neg_list(V,Ls,Rs).
 1031
 1032clp_vars_in(Vars, ClpVars) :-
 1033    include(is_clpq_var, Vars, ClpVars).
 1034
 1035%!  collect_vars(?Forall, ?CollectForall)
 1036%
 1037%   Forall Vars in a list
 1038
 1039collect_vars(Forall, c_forall(Vars, Goal)) :-
 1040    collect_vars_(Forall, [], Vars, Goal).
 1041
 1042collect_vars_(forall(Var, Goal), Vars, [Var|Vars], Goal) :-
 1043    Goal \= forall(_, _), !.
 1044collect_vars_(forall(Var, Forall), V0, V1, Goal) :-
 1045    collect_vars_(Forall, [Var|V0], V1, Goal).
 1046
 1047
 1048		 /*******************************
 1049		 *     AUXILIAR PREDICATES      *
 1050		 *******************************/
 1051
 1052%!  my_copy_term(+Var, +Term, -NewVar, -NewTerm) is det.
 1053%
 1054%   Its behaviour is similar to  copy_term/2.   It  returns in NewTerm a
 1055%   copy of the term Term but  it   only  replaces with a fresh variable
 1056%   NewVar the occurrences of Var
 1057
 1058:- if(current_predicate(copy_term_nat/4)). 1059
 1060my_copy_term(Var0, Term0, Var, Term) :-
 1061    copy_term_nat(Var0, Term0, Var, Term).
 1062
 1063my_copy_vars(Vars0, Term0, Vars, Term) :-
 1064    copy_term_nat(Vars0, Term0, Vars, Term).
 1065
 1066:- else. 1067
 1068my_copy_term(Var0, Term0, Var, Term) :-
 1069    term_variables(Term0, AllVars),
 1070    delete_var(AllVars, Var0, Share0),
 1071    copy_term_nat(t(Var0,Share0,Term0), t(Var,Share,Term)),
 1072    Share = Share0.
 1073
 1074delete_var([], _, []).
 1075delete_var([H|T0], V, List) :-
 1076    (   H == V
 1077    ->  List = T0
 1078    ;   List = [H|T],
 1079        delete_var(T0, V, T)
 1080    ).
 1081
 1082my_copy_vars(Vars0, Term0, Vars, Term) :-
 1083    term_variables(Term0, AllVars),
 1084    sort(AllVars, AllVarsSorted),
 1085    sort(Vars0, Vars0Sorted),
 1086    ord_subtract(AllVarsSorted, Vars0Sorted, Share0),
 1087    copy_term_nat(t(Vars0,Share0,Term0), t(Vars,Share,Term)),
 1088    Share = Share0.
 1089
 1090:- endif. 1091
 1092%!  my_diff_term(+Term, +Vars, -Others) is det.
 1093%
 1094%   Others are variables in Term that do not appear in Vars.
 1095
 1096my_diff_term(Term, Vars, Others) :-
 1097    term_variables(Term, Set),
 1098    diff_vars(Set, Vars, Others).
 1099
 1100diff_vars([], _, []).
 1101diff_vars([H|T0], Vars, List) :-
 1102    (   member_var(Vars, H)
 1103    ->  diff_vars(T0, Vars, List)
 1104    ;   List = [H|T],
 1105        diff_vars(T0, Vars, T)
 1106    ).
 1107
 1108member_var(Vars, Var) :-
 1109    member(V, Vars),
 1110    Var == V,
 1111    !.
 1112
 1113member_stack(Goal, Stack) :- member(goal_origin(Goal, _), Stack).
 1114member_stack(Goal, Stack) :- member(Goal, Stack)