solve.pl

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