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(, , , ).
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)]).
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).
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,[],[]).
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, _).
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)).
forall(Var,Goal) and success if Var
success in all its domain for the goal Goal. It calls solve/4
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 ; !,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
285 append(ModelMid, ModelList, Model) 286 )
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).
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]).
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].
396solve_goal_builtin(is(X, Exp), Model) :-
397 exec_goal(is(X, Exp)),
398 Model = [is(X, Exp)]. 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]
428 ; fail
429 )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
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.
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 ).
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 ).
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) :- !.
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).
629proved_in_stack(Goal, Proved) :-
630 proved_relatives(Goal, Proved, Relatives),
631 member(Relative, Relatives),
632 ( Goal == Relative
633 ; Goal == chs(Relative)
634 ),
635 !.even if we have an even
loop through negation or a simple positive match.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)).
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).
The code is based on the old proved_in_stack/2. Effectively this extracts the other half than stack_parents/2, so possibly we should sync the code with that.
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 ).
c_forall(Vars,Goal) and succeeds if the
goal Goal succeeds covering the domain of all the vars in the list
of vars `Vars. It calls solve/4
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 ).
Note that the constraints on the forall variables are maintained explicitly.
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),
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)])),
894 ProvedOut2 = ProvedIn, 895 StackOut2 = StackIn, 896 Model3 = [] 897 )
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)
902. 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).
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)]).
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).
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 *******************************/
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.
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)
The sCASP solver
*/