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(:, +, -, -).
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)]).
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).
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,[],[]).
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, _).
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)).
forall(Var,Goal) and success if Var
success in all its domain for the goal Goal. It calls solve/4
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).
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]).
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].
411solve_goal_builtin(is(X, Exp), Model) :-
412 exec_goal(is(X, Exp)),
413 Model = [is(X, Exp)]. 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]
443 ; fail
444 )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
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.
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 ).
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 ).
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) :- !.
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).
649proved_in_stack(Goal, Proved) :-
650 proved_relatives(Goal, Proved, Relatives),
651 member(Relative, Relatives),
652 ( Goal == Relative
653 ; Goal == chs(Relative)
654 ),
655 !.even if we have an even
loop through negation or a simple positive match.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)).
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).
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.
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 ).
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
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 ).
Note that the constraints on the forall variables are maintained explicitly.
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),
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)])),
918 ProvedOut2 = ProvedIn, 919 StackOut2 = StackIn, 920 Model3 = [] 921 )
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)
926. 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).
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)]).
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).
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 *******************************/
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.
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)
The sCASP solver
*/