7
27is_sicstus:- \+ current_prolog_flag(version_data,swi(_,_,_,_)).
28
30
31?- is_sicstus -> ensure_loaded('sicstus.pl') ; ensure_loaded('swi.pl') . 32
36
37:- dynamic((
38 macro1/2, macro/3, ccsorts/1, domain_schema/2, domain/2, var_sort/2,
39 (<=)/2, (<-)/2, rule_schema/1, rule_schema1/2, query_rule_schema/1,
40 query_problem/3, nmquery_problem/3 ,
41 atom_integer/3, atom_integer_extension/3, saved_atom_integer/3,
43 clause/1, clause0/1, clause1/1, query_clause/1,
44 rule_body/2, query_rule_body/2, show_spec/1,
45 test/1, attribute0/2, ab/1, ab_cwa_1/1, objs/2,
46 consts/2, rigids/2, boolean_constants/2,
47 value/2 )). 48
49
52
53:- ccalcops:compile('precedences.std'). 54:- compile('./cchelp.pl'). 55
56safe_tell(FileName) :- tell(FileName), told, tell(FileName).
57safe_see(FileName) :- see(FileName), seen, see(FileName).
58
59
64
65loadf(Files) :-
66 initialize,
67 include_file('macros.std',0),
68
69 common_statistics(_),
70
71 read_file(Files),
72 loadf_Files2, !.
73
74loadf_Files2:-
75 instantiate_sorts, 76 77 ( show_spec(S)
78 -> \+ \+ valid_spec(S)
79 ; true ),
80
81 enumerate_atoms, 82
83 common_statistics(T1),
84 T1S is T1/1000,
85
86 write('%'),
87 value(original_atom_count,OC), format(" ~w atoms",[OC]),
88 flush_output,
89
90 insert_inertia_rules,
91
92 process_rule_schemas, 93
94 common_statistics(T2),
95 T2S is T2/1000,
96 value(rule_count,RC), format(", ~w rules",[RC]),
97 flush_output,
98
99 generate_completion_clauses(domain), 100 101 102
103 value(clause_count,CC), format(", ~w clauses",[CC]),
104 value(aux_atom_count,AAC),
105 ( AAC > 0
106 -> format(" (~w new atoms)",[AAC]),
107 ( ( value(mode,transition), AAC > 0 )
108 -> flush_output,
109 renumber_atoms
110 ; true )
111 ; true ),
112 common_statistics(T3),
113 T3S is T3/1000,
114 nl,
115 ( value(timed,true)
116 -> T12S is T1S + T2S,
117 format("% Grounding time: ~2f seconds~n",[T12S]),
118 format("% Completion time: ~2f seconds~n",[T3S]),
119 ( value(verbose,true)
120 -> T is T1S + T2S + T3S,
121 format("% Total time: ~2f seconds~n",[T])
122 ; true )
123 ; true ).
124
125
136
137include_file(File,RuleSchema) :-
138 include_file(File,_,RuleSchema).
139
140include_file([],_,_) :- !.
141
142include_file([File|Files],IncludeDir,RuleSchema) :-
143 !,
144 include_file(File,IncludeDir,RuleSchema),
145 include_file(Files,IncludeDir,RuleSchema).
146
148
150include_file(File,IncludeDir,RuleSchema) :-
151 \+ list(File), 152 !,
153 seeing(OldInput),
154 ( determine_full_filename(File,IncludeDir,AbsFile)
155 -> true
156 ; fatal_error("File \'~w\' not found.",[File]) ),
157 ( (RuleSchema==1 ;
158 member(File,['static0.std']))
159 -> true
160 ; write('% loading file '),
161 write(AbsFile), nl ),
162 flush_output,
163 safe_see(AbsFile),
164 read_pass(RuleSchema),
165 seen,
166 see(OldInput).
167
168
181
182determine_full_filename(File,FullName) :-
183 determine_full_filename(File,_,FullName).
184
185determine_full_filename(File,IncludeDir,FullName) :-
186 ( nonvar(IncludeDir),
187 format_to_atom(FullName,"~w~w",[IncludeDir,File])
188 ; expand_filename(File,FullName)
189 ; environ('PWD',PWD),
190 format_to_atom(FullName,"~w/~w",[PWD,File])
191 ; value(dir,Dir),
192 format_to_atom(File0,"~w~w",[Dir,File]),
193 expand_filename(File0,FullName)
194 ; value(ccalc_dir,CCalcPath),
195 format_to_atom(FullName,"~w~w",[CCalcPath,File])
196 ; fatal_error("File \'~w\' not found.",[File]) ),
197 common_file_exists(FullName),
198 !.
199
200
204
205determine_path(Filename,Path) :-
206 format_to_chars("~w",[Filename],FilenameStr),
207 determine_path_recur(FilenameStr,PathStr),
208 ( ground(PathStr)
209 -> format_to_atom(Path,"~s",[PathStr])
210 ; Path = '' ).
211
212determine_path_recur([],[]).
213
214determine_path_recur([47|Cs],Path) :- 215 !,
216 determine_path_recur(Cs,Path2),
217 Path = [47|Path2].
218
219determine_path_recur([C|Cs],Path) :-
220 determine_path_recur(Cs,Path2),
221 ( Path2 = []
222 -> Path = []
223 ; Path = [C|Path2] ).
224
225
240
241read_file(Files) :-
242 include_file('static0.std',0),
243 iset(dynamic_detected,false), 244 include_file(Files,0), 245 246 247 ( (value(dynamic_detected,true), \+ value(mode,history))
248 -> iset(mode,transition),
249 filter_static1_dynamic(Files) 250 ; true ),
251
252 ( value(additive_detected,true) 253 -> process_additive
254 ; true ),
255
256 value(mode,Mode),
257 write('%'),
258 format(" in ~w mode...~n",[Mode]),
259 iset(dynamic_detected,false).
260
261
262%-----------------------------------------------------------------------------%
263% filter_static1_dynamic(+Files) : Used in transition mode
264% read the rules only in Files and store them in
265% rule_schema1/1 for shifting
266%-----------------------------------------------------------------------------%
267
268filter_static1_dynamic(Files) :-
269 V_EA = var(exogenousActionAtomicFormula,-1),
270 Term = (0: V_EA <= 0: V_EA),
271 insert_rule_schema(Term,1),
272
273 V_AA = var(attributeAtomicFormula,-1),
274 Term1 = (0: V_AA <= 0: V_AA),
275 insert_rule_schema(Term1,1),
276
277 include_file(Files,1).
278
279
283
284is_op(B) :-
285 functor(B,F,_),
286 member_check(F, [include, macros, sorts, variables, objects, constants, of,
287 tests, maxstep, compile, show, query, nmquery, op]).
288
289read_pass(RuleSchema) :-
290 read_fail_loop(RuleSchema).
291read_pass(_RuleSchema).
292
293
294read_fail_loop(RuleSchema) :-
295 repeat,
296 read_and_expand(Term0,Term),
297
298 ( (Term == end_of_file)
299 -> !, fail
300
301 ; (Term = (:- maxstep :: N))
302 -> ( RuleSchema==0
303 -> process_maxstep(N) )
304
305 ; (Term = (:- maxAdditive :: N))
306 -> ( RuleSchema==0
307 -> iset(additive_detected,true),
308 process_macros((maxAdditive -> N)),
309 process_include('additive') )
310
311 ; (Term == dynamic; Term = ((dynamic) where C))
312 -> iset(dynamic_detected,true)
313
314 ; Term = (side_effect(SideEffect) where _Condition)
315 -> call(SideEffect)
316
317 ; Term = side_effect(SideEffect)
318 -> call(SideEffect)
319
320 ; ( (Term = (((B=>H) where C)); Term = (((H<-B) where C));
321 Term = (((H<=B) where C));
322 Term = (((<- B) where C)), H = false;
323 Term = (((<= B) where C)), H = false ) )
324 -> ( negative_nonboolean_atom(H) % rather check definiteness here
325 -> fatal_error("The rule is not definite: ~w",Term0)
326 ; true ),
327 ( \+ ( (RuleSchema ==1), rigid_atom(H))
328 -> insert_rule_schema(((H<=B) where C),RuleSchema ) )
329
330 ; ( (Term = (B=>H); Term = (H<-B); Term = (H<=B);
331 Term = (<- B), H = false; Term = (<= B), H = false) )
332 -> ( negative_nonboolean_atom(H)
333 -> fatal_error("The rule is not definite: ~w",Term0)
334 ; true ),
335 ( \+ ( (RuleSchema ==1), rigid_atom(H))
336 -> insert_rule_schema((H<=B),RuleSchema ) )
337
338 ; ( (Term = (H :- B); Term = (:- B), \+ is_op(B), H = false),
339 value(mode,basic) )
340 -> ( negative_nonboolean_atom(H)
341 -> fatal_error("The rule is not definite: ~w",Term0)
342 ; true ),
343 replace_comma_with_and(B,B1),
344 insert_rule_schema((H<=B1),RuleSchema)
345
346 ; (Term = (:- include(Arg))) % required for sicstus 3.8
347 -> process_include(Arg)
348
349 ; (Term = (:- Command))
350 -> ( RuleSchema==0
351 -> call(Command)) % other commands such as declarations of
352 % sorts, objects, etc
353
354 ; ( (Term = (F where C))
355 -> ( (RuleSchema==1, \+ rigid_atom(Term))
356 -> true
357 ; insert_rule_schema(((F <= true) where C),RuleSchema) ) )
358
359 ; ( ( (RuleSchema == 1), \+ rigid_atom(Term) )
360 -> true
361 ; insert_rule_schema((Term <= true), RuleSchema) ) ),
362 fail.
363
364
365%-----------------------------------------------------------------------------%
366% negative_nonboolean_atom(+Head):
367% Checks whether Head is a negation of nonboolean atoms, which makes
368% the rule nondefinite. -(a=1) (a \in {1,2,3}) for example.
369%-----------------------------------------------------------------------------%
370
371negative_nonboolean_atom(Head) :-
372 ( Head = -((_: C eq Val)) ; Head = -(C eq Val)),
373 \+ boolean_constants(C,_).
374
375
395
396
400
401macros(B) :- process_macros(B), !.
402sorts(B) :- process_sorts(B), declare_composite_sorts(B), !.
403variables(B) :- process_variables(B), !.
404objects(B) :- process_objects(B), !.
405constants(B) :- process_constants(B), !.
406include(B) :- process_include(B), !.
407show(B) :- process_show(B), !.
408tests(B) :- process_tests2(B), !.
409maxstep(B) :- process_maxstep(B), !.
410
411
412
413%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
414%% initialization
415%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
416
417initialize :-
418 garbage_collect,
419% close_all_streams,
420
421 retractall(macro(_,_,_)),
422 retractall(meta_macro(_,_,_)),
423 retractall(ccsorts(_)),
424 retractall(domain_schema(_,_)),
425 retractall(domain(_,_)),
426 retractall(var_sort(_,_)),
427
428 retractall((_ <= _)),
429 retractall((_ <- _)),
430 retractall(rule_schema(_)),
431 retractall(rule_schema1(_)),
432 retractall(query_rule_schema(_)),
433
434 retractall(query_problem(_,_,_)),
435 retractall(nmquery_problem(_,_,_)),
436
437 retractall(atom_integer(_,_)),
438 retractall(atom_integer_extension(_,_)),
439 retractall(saved_atom_integer(_,_)),
440
441 retractall(clause(_)),
442 retractall(clause0(_)),
443 retractall(clause1(_)),
444 retractall(query_clause(_)),
445 assertz((clause(C) :- clause0(C))),
446 assertz((clause(C) :- clause1(C))),
447
448 retractall(rule_body(_,_)),
449 retractall(query_rule_body(_,_)),
450
451 retractall(show_spec(_)),
452
453 retractall(test(_)),
454 retractall(attribute0(_,_)),
455 retractall(ab(_)),
456 retractall(ab_cwa_1(_)),
457
458 retractall(consts(_,_)),
459 retractall(rigids(_,_)),
460 retractall(boolean_constants(_,_)),
461 retractall(objs(_,_)),
462
463 assertz(ccsorts([node(atomicFormula,[])])),
464
465% process_sorts(((boolean*) >> boolean)),
466% assert_objects(true,boolean),
467% assert_objects(false,boolean),
468
469 assertz(test(true)),
470 assertz(test(false)),
471 assertz(test(next(_,_))),
472 assertz(test(_ = _)),
473 assertz(test(_ < _)),
474 assertz(test(_ > _)),
475 assertz(test(_ =< _)),
476 assertz(test(_ >= _)),
477
478 assertz(test(_ == _)),
479 assertz(test(_ @< _)),
480 assertz(test(_ @> _)),
481 assertz(test(_ @=< _)),
482 assertz(test(_ @>= _)),
483 assertz(test(_ is _)),
484 assertz(test(_ =:= _)),
485 assertz(test(_ =\= _)),
486
487 retractall(value(atom_count,_)),
488 retractall(value(rigid_count,_)),
489 retractall(value(atom_count_0,_)),
490 retractall(value(aux_atom_count_from_rules_0,_)),
491 retractall(value(aux_atom_count_from_rules,_)),
492 retractall(value(aux_atom_count_from_completion_0,_)),
493 retractall(value(aux_atom_count_from_completion,_)),
494 retractall(value(aux_atom_count,_)),
495 retractall(value(original_atom_count,_)),
496 retractall(value(extended_atom_count,_)),
497 retractall(value(fluent_count,_)),
498 retractall(value(action_count,_)),
499 retractall(value(rule_count,_)),
500 retractall(value(rule_count_0,_)),
501 retractall(value(query_rule_count,_)),
502 retractall(value(clause_count,_)),
503 retractall(value(clause_count_0,_)),
504 retractall(value(query_clause_count,_)),
505 retractall(value(extended_clause_count,_)),
506 retractall(value(compact_ans,_)),
507 retractall(value(dynamic_detected,_)),
508
509 iset(mode,basic),
510 iset(dynamic_detected,false),
511 iset(additive_detected,false),
512
513 db_init_external,
514 db_init_query_external.
515
516
520
524
525process_macros((A;B)) :-
526 !,
527 process_macros(A),
528 process_macros(B).
529
531process_macros(((maxstep) -> N)) :-
532 !,
533 fatal_error("In history mode, maxstep should now be specified by ~n
534 :- maxstep ~w. ~n",N).
535
536process_macros((Left -> Right)) :-
537 !,
538 subst_vars_for_macro_vars((Left->Right),(T1->T2),_Vs),
539 ( T1 == T2 540 -> true
541 ; assertz(macro(T1,true,T2)) ).
542
543process_macros((Left -> Right where Call)) :-
544 !,
545 subst_vars_for_macro_vars((Left->Right where Call),
546 (T1->T2 where C),_Vs),
547 ( T1 == T2
548 -> true
549 ; assertz(macro(T1,C,T2)) ).
550
551process_macros(Macro) :-
552 fatal_error("Invalid macro declaration (~w).",[Macro]).
553
554
559
560subst_vars_for_macro_vars(#(N),V,Vs) :-
561 member(=(N,V),Vs), !.
562subst_vars_for_macro_vars(C,D,Vs) :-
563 functor(C,F,N),
564 functor(D,F,N),
565 subst_vars_for_macro_vars_arg(C,0,N,D,Vs).
566
567subst_vars_for_macro_vars_arg(_C,N,N,_D,_Vs) :- !.
568subst_vars_for_macro_vars_arg(C,M,N,D,Vs) :-
569 M1 is M+1,
570 arg(M1,C,A),
571 subst_vars_for_macro_vars(A,B,Vs),
572 arg(M1,D,B),
573 subst_vars_for_macro_vars_arg(C,M1,N,D,Vs).
574
575
582
583subst_free(Term,Term,_Sub) :-
584 var(Term),
585 !.
586subst_free(Term,NewTerm,Sub) :-
587 atom(Term),
588 !,
589 ( member(=(Term,NewTerm),Sub)
590 -> true
591 ; NewTerm = Term ).
592subst_free([/\X|A],[/\X|A1],Sub) :-
593 !,
594 ( common_select(=(X,_),Sub,Sub1)
595 -> true
596 ; Sub1 = Sub ),
597 subst_free(A,A1,Sub1).
598subst_free([\/X|A],[\/X|A1],Sub) :-
599 !,
600 ( common_select(=(X,_),Sub,Sub1)
601 -> true
602 ; Sub1 = Sub ),
603 subst_free(A,A1,Sub1).
604subst_free(Term,NewTerm,Sub) :-
605 functor(Term,F,N),
606 functor(NewTerm,F,N),
607 subst_free_arg(Term,0,N,NewTerm,Sub).
608
609subst_free_arg(_Term,N,N,_NewTerm,_Sub) :-
610 !.
611subst_free_arg(Term,M,N,NewTerm,Sub) :-
612 M1 is M+1,
613 arg(M1,Term,A),
614 subst_free(A,B,Sub),
615 arg(M1,NewTerm,B),
616 subst_free_arg(Term,M1,N,NewTerm,Sub).
617
618
622
623subst_functor(F,G,T,NT) :-
624 functor(T,F,N), !,
625 functor(NT,G,N),
626 subst_functor_arg(F,G,T,0,N,NT).
627
628subst_functor(F,G,T,NT) :-
629 functor(T,F1,N), F1 \== F, !,
630 functor(NT,F1,N),
631 subst_functor_arg(F,G,T,0,N,NT).
632
633subst_functor_arg(_F,_G,_T,N,N,_NT) :- !.
634
635subst_functor_arg(F,G,T,M,N,NT) :-
636 M1 is M+1,
637 arg(M1,T,A),
638 subst_functor(F,G,A,B),
639 arg(M1,NT,B),
640 subst_functor_arg(F,G,T,M1,N,NT).
641
642
647
651
652complex_sort(S) :-
653 functor(S,_,1), !.
654
658
659composite_sort(simpleFluent(_)).
660composite_sort(inertialFluent(_)).
661composite_sort(additiveFluent(_)).
662
663composite_sort(sdFluent(_)).
664composite_sort(rigid(_)).
665
666composite_sort(action(_)).
667composite_sort(exogenousAction(_)).
668composite_sort(attribute(_)).
669composite_sort(additiveAction(_)).
670composite_sort(abAction(_)).
671
672
676
678is_constant(var(Sort,_)) :-
679 composite_sort(Sort), !.
680
682is_constant(C) :-
683 var_sort(C,Sort), composite_sort(Sort), !.
684
690is_constant(C) :-
691 !,
692 functor(C,F,N),
693 consts(F,N). 694
698
699object(O) :-
700 functor(O,F,N),
701 objs(F,N).
702
709
710expr(-(Expr)) :- expr(Expr), !.
711
712expr(Expr) :-
713 functor(Expr,F,2), 714 !,
715 member_check(F,['+','-','*','/','//','rem','mod','gcd','min','max','**',
716 '>','<','=<','>=','=']).
717
718expr(Expr) :-
719 functor(Expr,F,1), 720 !,
721 member_check(F,['abs']).
722
723
727
729rigid(var(rigid(_S),_)) :- !.
730
732rigid(R) :- 733 var_sort(R, rigid(_)), !.
734
736rigid(R) :-
737 !,
738 functor(R,F,N),
739 rigids(F,N).
740
741
747
748rigid_atom(R) :- 749 rigid(R), !.
750rigid_atom(-R) :- 751 rigid(R), !.
752rigid_atom(R eq _) :-
753 rigid(R), !.
754rigid_atom(R = _) :-
755 rigid(R), !.
756
757
761
762composite_var(V) :-
763 var_sort(V,Sort),
764 composite_sort(Sort), !.
765
766
770
771is_var(V) :-
772 var_sort(V,_), !.
773
774is_atom((_:V)) :-
775 is_var(V).
776is_atom(V) :-
777 is_var(V).
778is_atom(C=_) :-
779 is_constant(C).
780is_atom(C) :-
781 boolean_constant(C).
782is_atom(-C) :-
783 boolean_constant(C).
784is_atom(A=B) :-
785 ( evaluable_expr(A) ; evaluable_expr(B) ).
786
787
791
796
797simpleFluent_constant(var(simpleFluent(_),_)) :- !.
798simpleFluent_constant(var(inertialFluent(_),_)) :- !.
799
800simpleFluent_constant(C) :-
801 ( var_sort(C,simpleFluent(_));
802 var_sort(C,inertialFluent(_)) ), !.
803
804simpleFluent_constant(C) :-
805 functor(C,F,N),
806 ( domain_schema(simpleFluent(_),Ls);
807 domain_schema(inertialFluent(_),Ls) ),
808 member(L,Ls),
809 functor(L,F,N).
810
811
816
817sdFluent_constant(var(sdFluent(_),_)) :- !.
818sdFluent_constant(var(rigid(_),_)) :- !.
819
820sdFluent_constant(C) :-
821 ( var_sort(C,sdFluent(_));
822 var_sort(C,rigid(_)) ), !.
823
824sdFluent_constant(C) :-
825 functor(C,F,N),
826 ( domain_schema(sdFluent(_),Ls);
827 domain_schema(rigid(_),Ls) ),
828 member(L,Ls),
829 functor(L,F,N).
830
831
836
837fluent_constant(C) :-
838 ( simpleFluent_constant(C); sdFluent_constant(C) ).
839
840
844
845action_constant(var(action(_),_)) :- !.
846action_constant(var(abAction(_),_)) :- !.
847action_constant(var(exogenousAction(_),_)) :- !.
848action_constant(var(attribute(_),_)) :- !.
849action_constant(var(additiveAction(_),_)) :- !.
850
851action_constant(C) :-
852 ( var_sort(C,action(_));
853 var_sort(C,abAction(_));
854 var_sort(C,exogenousAction(_));
855 var_sort(C,attribute(_));
856 var_sort(C,additiveAction(_)) ), !.
857
858action_constant(C) :-
859 functor(C,F,N),
860 functor(L,F,N),
861 ( domain_schema(action(_),Ls);
862 domain_schema(abAction(_),Ls);
863 domain_schema(exogenousAction(_),Ls);
864 domain_schema(attribute(_),Ls);
865 domain_schema(additiveAction(_),Ls) ),
866 member(L,Ls).
867
868
872
873simpleFluent_atom(C=_) :-
874 simpleFluent_constant(C).
875simpleFluent_atom(C) :-
876 simpleFluent_constant(C).
877simpleFluent_atom(-C) :-
878 simpleFluent_constant(C).
879
880sdFluent_atom(C=_) :-
881 sdFluent_constant(C).
882sdFluent_atom(C) :-
883 sdFluent_constant(C).
884sdFluent_atom(-C) :-
885 sdFluent_constant(C).
886
887fluent_atom(C=_) :-
888 (simpleFluent_constant(C) ; sdFluent_constant(C)).
889fluent_atom(C) :-
890 (simpleFluent_constant(C) ; sdFluent_constant(C)).
891fluent_atom(-C) :-
892 (simpleFluent_constant(C) ; sdFluent_constant(C)).
893
894action_atom(C=_) :-
895 action_constant(C).
896action_atom(C) :-
897 action_constant(C).
898action_atom(-C) :-
899 action_constant(C).
900
901
905
909
910simpleFluent_formula(F) :-
911 simpleFluent_atom(F).
912simpleFluent_formula(F) :-
913 ( action_atom(F);
914 sdFluent_atom(F) ),
915 !, fail.
916simpleFluent_formula(F) :-
917 functor(F,_,N),
918 simpleFluent_formula_arg(F,1,N).
919simpleFluent_formula_arg(_F,M,N) :-
920 M > N,
921 !.
922simpleFluent_formula_arg(F,M,N) :-
923 M1 is M+1,
924 simpleFluent_formula_arg(F,M1,N).
925
926
930
931fluent_formula(F) :-
932 fluent_atom(F).
933fluent_formula(F) :-
934 action_atom(F),
935 !, fail.
936fluent_formula(F) :-
937 functor(F,_,N),
938 fluent_formula_arg(F,1,N).
939fluent_formula_arg(_F,M,N) :-
940 M > N,
941 !.
942fluent_formula_arg(F,M,N) :-
943 arg(M,F,A),
944 fluent_formula(A),
945 M1 is M+1,
946 fluent_formula_arg(F,M1,N).
947
948
952
953action_formula(F) :-
954 action_formula_1(F) , \+ fluent_formula(F).
955
956action_formula_1(F) :-
957 action_atom(F).
958action_formula_1(F) :-
959 fluent_atom(F),
960 !, fail.
961action_formula_1(F) :-
962 functor(F,_,N),
963 action_formula_1_arg(F,1,N).
964action_formula_1_arg(_F,M,N) :-
965 M > N,
966 !.
967action_formula_1_arg(F,M,N) :-
968 arg(M,F,A),
969 action_formula_1(A),
970 M1 is M+1,
971 action_formula_1_arg(F,M1,N).
972
973
977
978has_no_constants((_A@<_B)) :- !.
979has_no_constants((_A==_B)) :- !.
980has_no_constants(abby(_)) :- !.
981
982has_no_constants(Formula) :-
983 is_constant(Formula), !, fail.
984has_no_constants(Formula) :-
985 functor(Formula,_,N),
986 has_no_constants_arg(Formula,1,N).
987
988has_no_constants_arg(_Formula,M,N) :-
989 M > N,
990 !.
991has_no_constants_arg(Formula,M,N) :-
992 arg(M,Formula,A),
993 has_no_constants(A),
994 M1 is M+1,
995 has_no_constants_arg(Formula,M1,N).
996
997
1001
1002process_sorts((A;B)) :-
1003 !,
1004 process_sorts(A),
1005 process_sorts(B).
1006
1007process_sorts((S>>(S1>>S2))) :-
1008 !,
1009 process_sorts((S>>S1)),
1010 process_sorts((S1>>S2)).
1011
1012process_sorts((S>>(S1;S2))) :-
1013 !,
1014 process_sorts((S>>S1)),
1015 process_sorts((S>>S2)).
1016
1017process_sorts((S>>S1)) :-
1018 !,
1019 ( find_sort(S,_As)
1020 -> ( find_sort(S1,_Bs)
1021 -> ( true 1022 1023 1024 -> add_subsort(S,S1)
1025 ; fatal_error("Sorts ~q and ~q must have a common supersort.",
1026 [S,S1]) )
1027 ; add_subsort(S,S1) )
1028 ; process_sorts(S),
1029 process_sorts((S>>S1)) ).
1030
1031process_sorts(S) :- % skip if already declared
1032 ( atom(S) ; composite_sort(S) ; S = _* ),
1033 !,
1034 ( is_sort(S)
1035 -> true
1036 ; ( find_sort(S,As)
1037 -> ( As = []
1038 -> format("~nRedundant sort declaration: ~w.",[S])
1039 ; fatal_error("Invalid sort1 declaration (~w).",[S]) )
1040 ; get_ccsorts(Nodes),
1041 append(Nodes,[node(S,[])],NewNodes),
1042 put_ccsorts(NewNodes) ) ).
1043
1044process_sorts(Spec) :-
1045 fatal_error("Invalid sort declaration (~w).",[Spec]).
1046
1048compatible(As,Bs) :-
1049 append(_,[A],As), append(_,[A],Bs).
1050
1051get_ccsorts(Nodes) :- ccsorts(Nodes).
1052
1053put_ccsorts(Nodes) :-
1054 retractall(ccsorts(_)), assertz(ccsorts(Nodes)).
1055
1057
1058is_sort(Sort) :-
1059 ( Sort = atomicFormula
1060 -> true
1061 ; find_sort(Sort,_) ).
1062
1063
1067
1068find_sort(Sort,As) :-
1069 get_ccsorts(Nodes),
1070 find_sort(Nodes,Sort,[],As).
1071
1072find_sort([node(S,Subs)|Nodes],Sort,As1,As) :-
1073 ( S = Sort, As = As1
1074 ; find_sort(Subs,Sort,[S|As1],As) 1075 ; find_sort(Nodes,Sort,As1,As) ).
1076
1078
1079descendant_sort(Child,Ancestor) :-
1080 find_sort(Child,Ancestor_List), member_check(Ancestor, Ancestor_List).
1081
1082
1083
1087
1088add_subsort(Sort,Sub) :-
1089 get_ccsorts(Nodes),
1090 add_subsort(Nodes,Sort,Sub,[],NewNodes),
1091 put_ccsorts(NewNodes).
1092
1093
1099
1100add_subsort([],_Sort,_Sub,_Ancestors,[]).
1101add_subsort([node(S,Subs)|Nodes],Sort,Sub,Ancestors,NewNodes1) :-
1102 add_subsort(Subs,Sort,Sub,[S|Ancestors],NewSubs),
1103 add_subsort(Nodes,Sort,Sub,Ancestors,NewNodes),
1104 ( S == Sort 1105 -> ( member(Sub,[S|Ancestors])
1106 -> report_cycle([S|Ancestors],Sub)
1107 ; ( member(node(Sub,_),NewSubs) 1108 1109 -> NewSubs1 = NewSubs 1110 ; ( find_sort(Sub,_), find_nodes([Sub],SubNodes)
1111 -> append(NewSubs,SubNodes,NewSubs1)
1112 ; append(NewSubs,[node(Sub,[])],NewSubs1) ) ),
1113 1114 1115
1116 NewNodes1 = [node(S,NewSubs1)|NewNodes] ) 1117 1118 ; NewNodes1 = [node(S,NewSubs)|NewNodes] ).
1119
1120report_cycle(Ancestors,Sub) :-
1121 format("~nCycle in sorts: ",[]),
1122 reverse(Ancestors,As),
1123 ( member(A,As),
1124 format("~w >> ", [A]), fail;
1125 format("~w.~n",[Sub]) ),
1126 close_abort.
1127
1128
1133
1134declare_composite_sorts((A;B)) :-
1135 !,
1136 declare_composite_sorts(A),
1137 declare_composite_sorts(B).
1138
1139declare_composite_sorts((S>>(S1>>S2))) :-
1140 !,
1141 declare_composite_sorts((S>>S1)),
1142 declare_composite_sorts((S1>>S2)).
1143
1144declare_composite_sorts((S>>(S1;S2))) :-
1145 !,
1146 declare_composite_sorts((S>>S1)),
1147 declare_composite_sorts((S>>S2)).
1148
1149declare_composite_sorts((S>>S1)) :-
1150 !,
1151 declare_composite_sorts(S),
1152 declare_composite_sorts(S1).
1153
1154declare_composite_sorts(S) :-
1155 !,
1156 ( skip_declare_composite_sorts(S)
1157 -> true
1158 ;
1159 process_sorts(((S*) >> S)),
1160
1161 process_sorts((simpleFluent(S) >> inertialFluent(S))),
1162 process_sorts(sdFluent(S)),
1163 process_sorts((action(S) >> exogenousAction(S))),
1164 process_sorts(attribute(S)),
1165 process_sorts(abAction(S)),
1166 process_sorts(rigid(S)),
1167
1168 process_sorts((simpleFluent(S*) >> inertialFluent(S*))),
1169 process_sorts(sdFluent(S*)),
1170 process_sorts((action(S*) >> exogenousAction(S*))),
1171 process_sorts(attribute(S*)),
1172 process_sorts(rigid(S*)),
1173
1174 assert_objects((simpleFluent(S) eq S), simpleFluentAtomicFormula),
1175 assert_objects((sdFluent(S) eq S), sdFluentAtomicFormula),
1176
1177 assert_objects((action(S) eq S), actionAtomicFormula),
1178 assert_objects((exogenousAction(S) eq S), exogenousActionAtomicFormula),
1179 assert_objects((attribute(S) eq S*), attributeAtomicFormula),
1180 assert_objects((abAction(S) eq S), abActionAtomicFormula),
1181 assert_objects((rigid(S) eq S), rigidAtomicFormula),
1182
1183 assert_objects((simpleFluent(S*) eq S*), simpleFluentAtomicFormula),
1184 assert_objects((sdFluent(S*) eq S*), sdFluentAtomicFormula),
1185 assert_objects((action(S*) eq S*), actionAtomicFormula),
1186 assert_objects((exogenousAction(S*) eq S*), exogenousActionAtomicFormula),
1187 assert_objects((rigid(S*) eq S*), rigidAtomicFormula),
1188
1189%^ what if attribute(S*)? - no there is no such
1190 assert_objects(none,S*) ).
1191
1192
1193skip_declare_composite_sorts(S) :-
1194 ( composite_sort(S) ; S = _* ;
1195 member_check(S,[step, astep,
1196 simpleFluentAtomicFormula,inertialFluentAtomicFormula,
1197 sdFluentAtomicFormula,
1198 actionAtomicFormula,
1199 abActionAtomicFormula,
1200 exogenousActionAtomicFormula,
1201 attributeAtomicFormula,
1202 rigidAtomicFormula,
1203 atomicFormula]) ).
1204
1205
1209
1212assert_variables((A,B),S) :-
1213 !,
1214 assert_variables(A,S),
1215 assert_variables(B,S).
1216assert_variables(V,S) :-
1217 atom(V),
1218 ( S == computed
1219 -> true
1220 ; is_sort(S) ),
1221 !,
1222 ( var_sort(V,S1) 1223 -> ( S = S1
1224 -> true
1225 ; fatal_error("Variable (~w) has multiple declarations.",[V]) )
1226 ; assertz(var_sort(V,S)) ).
1227assert_variables(V,S) :-
1228 fatal_error("Invalid variable declaration (~w).",[(V::S)]).
1229
1230process_variables((A;B)) :-
1231 !,
1232 process_variables(A),
1233 process_variables(B).
1234
1235process_variables((Vs::M..N)) :-
1236 !,
1237 eval_expr(M,M1),
1238 eval_expr(N,N1),
1239 generate_range_sort(M1,N1,S1),
1240 assert_variables(Vs,S1).
1241
1242process_variables((Vs::(S+none))) :-
1243 is_sort(S),
1244 !,
1245 assert_variables(Vs,(S*)).
1246
1247process_variables((Vs::S)) :-
1248 is_sort(S),
1249 !,
1250 assert_variables(Vs,S).
1251
1252process_variables((Vs::S)) :-
1253 member(S,[simpleFluent,inertialFluent,sdFluent,action,exogenousAction,
1254 attribute,rigid]),
1255 !,
1256 S1 =.. [S, boolean],
1257 assert_variables(Vs,S1).
1258
1259process_variables(Spec) :-
1260 fatal_error("Invalid variable declaration (~w).",[Spec]).
1261
1262
1266
1267assert_objects((A,B),S) :-
1268 !,
1269 assert_objects(A,S),
1270 assert_objects(B,S).
1271
1272assert_objects(M..N,S) :- % a hack to allow convenient time specs
1273 !,
1274 expand_sequence(M,N,Ns),
1275 ( retract(domain_schema(S,Cs))
1276 -> append(Cs,Ns,NewCs),
1277 assertz(domain_schema(S,NewCs))
1278 ; assertz(domain_schema(S,Ns)) ).
1279
1280assert_objects(C,S) :-
1281 functor(C,F,N),
1282 ( objs(F,N)
1283 -> true
1284 ; assertz(objs(F,N)) ),
1285
1286 ( (domain_schema(S,Cs), member(C,Cs)) 1287 -> true 1288 ; ( retract(domain_schema(S,Cs)) 1289 -> append(Cs,[C],NewCs),
1290 assertz(domain_schema(S,NewCs))
1291 ; assertz(domain_schema(S,[C])))).
1292
1293process_objects((A;B)) :-
1294 !,
1295 process_objects(A),
1296 process_objects(B).
1297
1298process_objects((Cs::S)) :-
1299 is_sort(S), 1300 !,
1301 assert_objects(Cs,S).
1302
1303process_objects((Cs::(S+none))) :-
1304 atom(S),
1305 is_sort(S),
1306 !,
1307% introduce_star_sort(S),
1308 assert_objects(Cs,(S*)).
1309
1310process_objects(Spec) :-
1311 fatal_error("Invalid object declaration (~w).",[Spec]).
1312
1313introduce_star_sort(S) :-
1314 process_sorts((simpleFluent(S*) >> inertialFluent(S*))),
1315 process_sorts(sdFluent(S*)),
1316 process_sorts((action(S*) >> exogenousAction(S*))),
1317 process_sorts(rigid(S*)),
1318
1319 assert_objects((simpleFluent(S*) eq S*), simpleFluentAtomicFormula),
1320 assert_objects((sdFluent(S*) eq S*), sdFluentAtomicFormula),
1321 assert_objects((action(S*) eq S*), actionAtomicFormula),
1322 assert_objects((exogenousAction(S*) eq S*), exogenousActionAtomicFormula),
1323 assert_objects((rigid(S*) eq S*), rigidAtomicFormula).
1324
1326generate_range_sort(M,N,RangeSortM_N) :-
1327 expand_sequence(M,N,Ns),
1328 name(rangeSort,ListRangeSort),
1329 name(M,ListM),
1330 name(N,ListN),
1331 name('_',ListUL),
1332 append(ListRangeSort,ListM,ListRangeSortM),
1333 append(ListRangeSortM,ListUL,ListRangeSortM_),
1334 append(ListRangeSortM_,ListN,ListRangeSortM_N),
1335 atom_chars(RangeSortM_N,ListRangeSortM_N),
1336 sorts((integer >> RangeSortM_N)), 1337 list_to_tuple(Ns,T),
1338 process_objects((T :: RangeSortM_N)).
1339
1340check_domain_for_additive(S,M,N) :-
1341 ( (M =< 0, 0 =< N)
1342 -> true
1343 ; atom_chars(S,S1),
1344 ( prefix("rangeSort",S1)
1345 -> fatal_error("The domain of additiveFluent(~w..~w) should include the neutral element 0",[M,N])
1346 ; fatal_error("The domain of additiveFluent(~w) should include the neutral element 0",S) ) ).
1347
1348
1352
1354process_additive :-
1355 domain_schema(additiveFluent(S),_),
1356 domain_schema(S,[M|Ns]),
1357 common_last([M|Ns],N),
1358 check_domain_for_additive(S,M,N),
1359 insert_additiveFluent_rules(additiveFluent(S),M,N), 1360 fail.
1361process_additive :-
1362 domain_schema(additiveAction(S),_),
1363 domain_schema(S,[M|Ns]),
1364 common_last([M|Ns],N),
1365 check_domain_for_additive(S,M,N),
1366 insert_additiveAction_rules(additiveAction(S),M,N), 1367 fail.
1368process_additive.
1369
1370
1374
1375additive_fluent(AF) :-
1376 functor(AF,F,N),
1377 functor(AF1,F,N),
1378 domain_schema(additiveFluent(_),AFs),
1379 member_check(AF1,AFs).
1380
1381additive_action(AF) :-
1382 functor(AF,F,N),
1383 functor(AF1,F,N),
1384 domain_schema(additiveAction(_),AFs),
1385 member_check(AF1,AFs).
1386
1388
1389process_static_abLabel(Ab) :-
1390 Ab =.. [F|VArgs],
1391 vars_to_sorts(VArgs,SArgs),
1392 Ab2 =.. [F|SArgs],
1393 process_constants((Ab2 :: sdFluent)),
1394 register_ab(Ab).
1395
1396process_dynamic_abLabel(Ab) :-
1397 Ab =.. [F|VArgs],
1398 vars_to_sorts(VArgs,SArgs),
1399 Ab2 =.. [F|SArgs],
1400 process_constants((Ab2 :: abAction(boolean))),
1401 register_ab(Ab).
1402
1403register_ab(Ab) :-
1404 assertz(ab(Ab)).
1405
1406
1410
1415register_constants((A,B)) :-
1416 !,
1417 register_constants(A),
1418 register_constants(B).
1419
1420register_constants(C) :-
1421 functor(C,F,N),
1422 assertz(consts(F,N)).
1423
1428register_rigids((A,B)) :-
1429 !,
1430 register_rigids(A),
1431 register_rigids(B).
1432
1433register_rigids(C) :-
1434 functor(C,F,N),
1435 assertz(rigids(F,N)).
1436
1437
1442
1443register_boolean_constants((A,B)) :-
1444 !,
1445 register_boolean_constants(A),
1446 register_boolean_constants(B).
1447
1448register_boolean_constants(C) :-
1449 functor(C,F,N),
1450 assertz(boolean_constants(F,N)).
1451
1452
1456
1457process_constants((A;B)) :-
1458 !,
1459 process_constants(A),
1460 process_constants(B).
1461
1462process_constants((Cs::attribute(S*) of Action)) :-
1463 fatal_error("Invalid constant declaration: ~w. Use ~w instead of ~w.",[(Cs::attribute(S*) of Action), S, S*]).
1464
1465process_constants((Cs::attribute(S) of Action)) :-
1466% (S \= _*),
1467% introduce_star_sort(S),
1468 ( S = (M..N)
1469 -> eval_expr(M,M1),
1470 eval_expr(N,N1),
1471 generate_range_sort(M1,N1,S1)
1472 ; S1 = S ),
1473 is_sort(attribute(S1)),
1474 !,
1475 iset(dynamic_detected,true),
1476 ( S1 == boolean
1477 -> register_boolean_constants(Cs)
1478 ; true ),
1479 register_constants(Cs),
1480 assert_objects(Cs,attribute(S1)),
1481 insert_attribute_rules(Cs,Action).
1482
1483process_constants((Cs::additiveFluent(S))) :-
1484 !,
1485 iset(dynamic_detected,true),
1486 iset(additive_detected,true),
1487 ( S = (M..N)
1488 -> eval_expr(M,M1),
1489 eval_expr(N,N1),
1490 generate_range_sort(M1,N1,S1)
1491 ; S1 = S ),
1492 process_sorts((simpleFluent(S1) >> additiveFluent(S1))),
1493 register_constants(Cs),
1494 assert_objects(Cs,additiveFluent(S1)),
1495 process_constants(
1496 ( contribution(action(boolean),additiveFluent(S1)),
1497 accumulatedContribution(action(boolean),additiveFluent(S1))
1498 :: action(additiveInteger) ) ).
1499
1500process_constants((Cs::additiveAction(S))) :-
1501 !,
1502 iset(dynamic_detected,true),
1503 iset(additive_detected,true),
1504 ( S = (M..N)
1505 -> eval_expr(M,M1),
1506 eval_expr(N,N1),
1507 generate_range_sort(M1,N1,S1)
1508 ; S1 = S ),
1509 process_sorts((action(S1) >> additiveAction(S1))),
1510 register_constants(Cs),
1511 assert_objects(Cs,additiveAction(S1)),
1512 process_constants(
1513 ( contribution(action(boolean),additiveAction(S1)),
1514 accumulatedContribution(action(boolean),additiveAction(S1))
1515 :: action(additiveInteger) ) ).
1516
1517process_constants((Cs::M..N)) :-
1518 !,
1519 eval_expr(M,M1),
1520 eval_expr(N,N1),
1521 generate_range_sort(M1,N1,S1),
1522
1523 register_constants(Cs),
1524 register_rigids(Cs),
1525 assert_objects(Cs,rigid(S1)).
1526
1527process_constants((Cs::((M..N)+none))) :-
1528 !,
1529 eval_expr(M,M1),
1530 eval_expr(N,N1),
1531 generate_range_sort(M1,N1,S1),
1532
1533 register_constants(Cs),
1534 register_rigids(Cs),
1535 assert_objects(Cs,rigid(S1*)).
1536
1537process_constants((Cs::(S+none))) :-
1538 atom(S),
1539 is_sort(S),
1540 !,
1541 ( S == boolean
1542 -> register_boolean_constants(Cs)
1543 ; true),
1544 register_constants(Cs),
1545 register_rigids(Cs),
1546 assert_objects(Cs,rigid(S*)).
1547
1548process_constants((Cs::S)) :-
1549 atom(S),
1550 is_sort(S),
1551 !,
1552 ( S == boolean
1553 -> register_boolean_constants(Cs)
1554 ; true),
1555 register_constants(Cs),
1556 register_rigids(Cs),
1557 assert_objects(Cs,rigid(S)).
1558
1559% composite sort except rigid constants
1560process_constants((Cs::CompositeSort)) :-
1561 ( CompositeSort =.. [rigid,S0]
1562 -> fatal_error("Invalid constant declaration (~w): Use ~w instead of
1563~w",[(Cs::CompositeSort),S0,CompositeSort])
1564 ; true ),
1565 composite_sort(CompositeSort),
1566 !,
1567 iset(dynamic_detected,true),
1568 ( CompositeSort =.. [F,(M..N)]
1569 -> eval_expr(M,M1),
1570 eval_expr(N,N1),
1571 generate_range_sort(M1,N1,RangeSort),
1572 CompositeSort1 =.. [F,RangeSort]
1573 ; CompositeSort =.. [F,(S+none)]
1574 -> CompositeSort1 =.. [F,S*]
1575 ; CompositeSort1 = CompositeSort ),
1576 ( arg(1,CompositeSort,boolean)
1577 -> register_boolean_constants(Cs)
1578 ; true ),
1579 register_constants(Cs),
1580 assert_objects(Cs,CompositeSort1).
1581
1582process_constants((Cs::S)) :-
1583 (S = simpleFluent; S = inertialFluent),
1584 !,
1585 iset(dynamic_detected,true),
1586 S1 =.. [S, boolean],
1587 process_constants((Cs::S1)).
1588
1589process_constants((Cs::sdFluent)) :-
1590 !,
1591 iset(dynamic_detected,true),
1592 process_constants((Cs::sdFluent(boolean))).
1593
1594process_constants((Cs::action)) :-
1595 !,
1596 iset(dynamic_detected,true),
1597 process_constants((Cs::action(boolean))).
1598
1599process_constants((Cs::exogenousAction)) :-
1600 !,
1601 iset(dynamic_detected,true),
1602 process_constants((Cs::exogenousAction(boolean))).
1603
1604process_constants((Cs::attribute of Action)) :-
1605 process_constants((Cs::attribute(boolean) of Action)).
1606
1607process_constants(Spec) :-
1608 fatal_error("Invalid constant declaration (~w).",[Spec]).
1609
1610
1614
1620
1621sorts_to_vars(Sorts,Vars) :-
1622 length(Sorts,N),
1623 sorts_to_vars(Sorts,[],N,Vars).
1624
1625sorts_to_vars([Sort|Sorts],Acc,N,Vars) :-
1626 get_var(Sort,N,Var),
1627 N1 is N-1,
1628 append(Acc,[Var],Acc1),
1629 sorts_to_vars(Sorts,Acc1,N1,Vars).
1630
1631sorts_to_vars([],Vars,_,Vars).
1632
1633
1638
1639vars_to_sorts(Vars,Sorts) :-
1640 vars_to_sorts(Vars,[],Sorts).
1641
1642vars_to_sorts([Var|Vars],Acc,Sorts) :-
1643 var_sort(Var,Sort),
1644 append(Acc,[Sort],Acc1),
1645 vars_to_sorts(Vars,Acc1,Sorts).
1646
1647vars_to_sorts([],Sorts,Sorts).
1648
1649
1654
1655tuples_to_conjs(Tuples,Conjs) :-
1656 tuples_to_conjs(Tuples,[],Conjs).
1657
1658tuples_to_conjs([T|Ts],Acc,Conjs) :-
1659 conjoin_tuple(T,C),
1660 append(Acc,[C],Acc1),
1661 tuples_to_conjs(Ts,Acc1,Conjs).
1662
1663tuples_to_conjs([],Conjs,Conjs).
1664
1665
1670
1672
1673const_to_sort(C,S) :- domain(S,Cs), member(C,Cs).
1674
1676
1677consts_to_sorts([Const|Consts],[Sort|Sorts]) :-
1678 const_to_sort(Const,Sort),
1679 consts_to_sorts(Consts,Sorts).
1680consts_to_sorts([],[]).
1681
1682
1683/* Can't use tail recursion in find_all used in get_all_attributes
1684consts_to_sorts(Consts,Sorts) :-
1685 consts_to_sorts1(Consts,[],Sorts).
1686
1687consts_to_sorts1([C|Cs],Acc,Sorts) :-
1688 const_to_sort(C,S), !,
1689% domain(S,Ds), member(C,Ds), % inefficient?
1690 append(Acc,[S],Acc1),
1691 consts_to_sorts1(Cs,Acc1,Sorts).
1692
1693consts_to_sorts1([],Sorts,Sorts).
1694*/
1695
1696%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1697
1698%-----------------------------------------------------------------------------%
1699% expand_sequence(+M,+N,?Ns) :
1700% used for expanding a range of integers into a list of integers
1701% e.g. | ?- expand_sequence(1,5,Ns).
1702% Ns = [1,2,3,4,5] ? ;
1703%-----------------------------------------------------------------------------%
1704
1705expand_sequence(M0,N0,Ns) :-
1706 M is M0, N is N0,
1707 ( integer(M), integer(N)
1708 -> ( M =< N
1709 -> expand_sequence_aux(M,N,Ns)
1710 ; Ns = [] )
1711 ; fatal_error("Invalid sequence (~w)",[M..N]) ).
1712
1713
1714expand_sequence_aux(M,N,Ns) :-
1715 expand_sequence_aux(M,N,[],Ns).
1716
1717expand_sequence_aux(M,N,Acc,Ns) :-
1718 M<N,!,
1719 append(Acc,[M],Acc1),
1720 M1 is M+1,
1721 expand_sequence_aux(M1,N,Acc1,Ns).
1722expand_sequence_aux(N,N,Acc,Ns) :-
1723 append(Acc,[N],Ns).
1724
1725
1726
1730
1731process_include((A;B)) :-
1732 !,
1733 process_include(A),
1734 process_include(B).
1735
1753
1754process_include((A: Ls)) :-
1755 !,
1756 process_include1((A: Ls)),
1757 retract_macro1(Ls).
1758
1759process_include(A) :-
1760 !,
1761 process_include1(A).
1762
1763retract_macro1((L->R),Ls) :-
1764 retract(macro1(L,R)),
1765 retract_macro1(Ls).
1766
1767retract_macro1((L->R)) :-
1768 retract(macro1(L,R)).
1769
1770process_include1((A: (L, Ls))) :-
1771 !,
1772 process_include1((A: L)),
1773 process_include1((A: Ls)).
1774
1775process_include1((A: (Left->Right))) :-
1776 !,
1777 subst_vars_for_macro_vars((Left->Right),(T1->T2),_Vs),
1778 ( T1 == T2 1779 -> true
1780 ; assertz(macro1(T1,T2)) ),
1781 process_include1(A).
1782
1783process_include1(A) :-
1784 !,
1785 seeing_filename(CurrInput),
1786 determine_path(CurrInput,CurrPath),
1787 ( (value(mode,transition), value(dynamic_detected,true))
1788 -> include_file(A,CurrPath,1)
1789 ; include_file(A,CurrPath,0) ).
1790
1791
1795
1796show_all :-
1797 forall(valid_show_spec(B), process_show(B)).
1798
1799process_show(B) :-
1800 retractall(show_spec(_)),
1801 process_show_internal(B).
1802
1803process_show_internal((A;B)) :-
1804 !,
1805 process_show_internal(A),
1806 process_show_internal(B).
1807
1808process_show_internal((A;B)) :-
1809 !,
1810 process_show_internal(A),
1811 process_show_internal(B).
1812
1813process_show_internal(C0) :-
1814 decode_macro(C0,C),
1815 ( C = (T: F = V)
1816 -> C1 = (T: F eq V)
1817 ; C = (F = V)
1818 -> C1 = (F eq V)
1819 ; ( C = -((T: F = V)) ; C = (T: F \= V) ; C = (T: F <> V) )
1820 -> C1 = -((T: F eq V))
1821 ; ( C = -(F = V) ; C = (F \= V) ; C = (F <> V) )
1822 -> C1 = -(F eq V)
1823 ; C1 = C ),
1824
1825 ( domain(_,_)
1826 -> \+ \+ valid_spec([C1])
1827 ; valid_show_spec(C1)),
1828 !,
1829 ( retract(show_spec(Cs))
1830 -> append(Cs,[C1],NewCs),
1831 assertz(show_spec(NewCs))
1832 ; assertz(show_spec([C1])) ).
1833
1834process_show_internal(Spec) :-
1835 nonfatal_error("Invalid show spec (~w) ignored.",[Spec]).
1836
1840
1841valid_show_spec(positive).
1842valid_show_spec(negative).
1843valid_show_spec(all).
1844valid_show_spec(ab).
1845valid_show_spec(none).
1846valid_show_spec(Term) :- \+ callable(Term), !, fail.
1847valid_show_spec(Term) :-
1848 functor(Term,_F,_N).
1849valid_show_spec(-Term) :-
1850 functor(Term,_F,_N).
1851
1852(show) :- format("enter specs (then ctrl-d)",[]),
1853 nl,
1854 read_specs([],Specs),
1855 (Specs = []
1856 -> Specs0 = positive
1857 ; list_to_semituple(Specs, Specs0)),
1858 process_show(Specs0).
1859
1860
1861read_specs(SoFar, Specs) :-
1862 read(Spec),
1863 (Spec == end_of_file
1864 -> Specs = SoFar
1865 ; semituple_to_list(Spec,Spec0),
1866 \+ \+ valid_spec(Spec0),
1867 !,
1868 append(Spec0,SoFar,SoFar0),
1869 read_specs(SoFar0,Specs)).
1870
1871
1875
1876process_tests((A;B)) :-
1877 !,
1878 process_tests(A),
1879 process_tests(B).
1880process_tests(P/N) :-
1881 functor_test_spec(P/N),
1882 !,
1883 functor(Gen,P,N),
1884 assertz(test(Gen)).
1885process_tests(Spec) :-
1886 fatal_error("Invalid test declaration (~w).",[Spec]).
1887
1888process_tests2((A;B)) :-
1889 !,
1890 process_tests2(A),
1891 process_tests2(B).
1892process_tests2(((P/N,B):: File)) :-
1893 functor_test_spec(P/N),
1894 !,
1895 functor(Gen,P,N),
1896 assertz(test(Gen)),
1897 process_tests2((B :: File)).
1898process_tests2((P/N :: File)) :-
1899 functor_test_spec(P/N),
1900 !,
1901 functor(Gen,P,N),
1902 assertz(test(Gen)),
1903 ( determine_full_filename(File,AbsFile)
1904 -> true
1905 ; fatal_error("File \'~w\' not found.",[File]) ),
1906 compile(AbsFile).
1907process_tests2(Spec) :-
1908 fatal_error("Invalid test declaration (~w).",[Spec]).
1909
1910functor_test_spec(Spec) :-
1911 Spec = F/N, atom(F), integer(N), N >= 0.
1912
1913process_maxstep(MaxStep) :-
1914 !,
1915 iset(mode,history),
1916 retractall(macro(maxstep,_,_)),
1917 eval_expr(MaxStep,MaxStep1),
1918 assertz(macro(maxstep,true,MaxStep1)),
1919 include_file('history.std',0).
1920
1921
1922%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1923%% process_query
1924%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1925
1926process_query(Fields,QueryType) :-
1927 semituple_to_list(Fields,FieldList),
1928 ( member_check((label::Label),FieldList)
1929 -> ( atomic(Label)
1930 -> true
1931 ; fatal_error("Invalid label field (~w).",[Label]) )
1932 ; Label = 0 ),
1933
1934 ( member_check(((maxstep)::any),FieldList)
1935 -> process_unsolvable_query(Label,FieldList)
1936 ; true),
1937
1938 ( member_check(((maxstep)::MaxStep),FieldList)
1939 -> do_term_expansion(MaxStep,MaxStep1),
1940 eval_expr(MaxStep1,MaxStep2),
1941 ( value(mode,history)
1942 -> nonfatal_error("query ~w - maxstep is already declared in history mode.~n",[Label])
1943 ; ( ((integer(MaxStep2), MaxStep2 >=0) ; (MaxStep2 == 'any') ;
1944 (MaxStep2 = (T1..T2), check_bounds(T1,T2,Label)))
1945 -> true
1946 ; fatal_error("Invalid maxstep in Query ~w", [Label]) ))
1947 ; ( value(mode,history)
1948 -> macro((maxstep),_,MaxStep2)
1949 ; MaxStep2 = 0 ) ),
1950
1951 delete(FieldList, (label::Label), FieldList2),
1952 delete(FieldList2, ((maxstep)::MaxStep), Rules),
1953 ( QueryType == (nmquery)
1954 -> assertz(nmquery_problem(Label,MaxStep2,Rules))
1955 ; assertz(query_problem(Label,MaxStep2,Rules)) ).
1956
1957
1958check_bounds(T1,T2,Label) :-
1959 ( (integer(T1), T1>=0)
1960 -> true
1961 ; fatal_error("In query ~w, the lower bound for maxstep must be a nonnegative integer.~n",[Label]), fail),
1962
1963 ( (integer(T2)
1964 -> ( T1>T2
1965 -> fatal_error("In query ~w, the upper bound for maxstep must be at least large as the lower bound ",[Label])
1966 ; true)
1967 ; ( T2 \== 'infinity'
1968 -> fatal_error("In query ~w, the upper bound for maxstep must be a nonnegative integer or infinity.~n",[Label])
1969 ; true))).
1970
1971
1972process_unsolvable_query(Label,FieldList) :-
1973 member_check((invariant: Inv), FieldList),
1974 member_check(((maxstep): Goal), FieldList),
1975
1976 delete(FieldList, (label::Label), FieldList1),
1977 delete(FieldList1, ((maxstep):: any), FieldList2),
1978 delete(FieldList2, ((maxstep): Goal), FieldList3),
1979 delete(FieldList3, (invariant: Inv), Rules),
1980
1981 append_name(Label,'_init',InitLabel),
1982 append(Rules,[(0:Inv)],InitRules),
1983 assertz(query_problem(InitLabel,0,InitRules)),
1984
1985 append_name(Label,'_goal',GoalLabel),
1986 append([(0:Inv)],[(0:Goal)],GoalRules),
1987 assertz(query_problem(GoalLabel,0,GoalRules)),
1988
1989 append_name(Label,'_trans',TransLabel),
1990 append([(0:Inv)],[-(((1:Inv)))],TransRules),
1991 assertz(query_problem(TransLabel,1,TransRules)).
1992
1993
1994append_name(A,B,C) :-
1995 name(A,L),
1996 name(B,L1),
1997 append(L,L1,L2),
1998 name(C,L2).
1999
2000
2001
2005
2009
2010insert_rule_schema(Term,SchemaNo) :-
2011 do_term_expansion(Term,TermTree),
2012 leaf_element(TermTree,TermTree1),
2013 ( (SchemaNo == 0)
2014 -> asserta(rule_schema(TermTree1))
2015 ; asserta(rule_schema1(TermTree1)) ).
2016
2017
2021
2022insert_inertia_rules :-
2023 findall(L, (is_sort(inertialFluent(L)),
2024 domain(inertialFluent(L),D), D \== []), Ls),
2025 insert_inertia_rules(Ls).
2026
2027insert_inertia_rules([]).
2028
2029insert_inertia_rules([L|Ls]) :-
2030 insert_inertia_rules_aux(L),
2031 insert_inertia_rules(Ls).
2032
2033insert_inertia_rules_aux(L) :-
2034 Term = (inertial var(inertialFluent(L),-1)),
2035 do_term_expansion(Term,TermTree),
2036 leaf_element(TermTree,(H <= B)),
2037 ( value(mode,transition)
2038 -> assertz(rule_schema1((H <= B)))
2039 ; assertz(rule_schema((H <= B))) ).
2040
2041
2045
2046insert_attribute_rules((A,B),Action) :-
2047 !,
2048 insert_attribute_rules(A,Action),
2049 insert_attribute_rules(B,Action).
2050
2051insert_attribute_rules(Cs,Action) :-
2052 Cs =.. [F|Sorts],
2053 sorts_to_vars(Sorts,Vars),
2054 Cs1 =.. [F|Vars],
2055
2056 Action =.. [F1|Sorts1],
2057 sorts_to_vars(Sorts1,Vars1),
2058 Action1 =.. [F1|Vars1],
2059
2060 ( value(mode,history) % macro(maxstep,_,_) % history mode
2061 -> assertz(rule_schema((false <= ((var(astep,-1): Cs1 eq none)<->(var(astep,-1): Action1)))))
2062 ; assertz(rule_schema1((false <= ((0: Cs1 eq none)<->(0: Action1))))) ),
2063 assertz(attribute0(Action,Cs)).
2064
2065%-----------------------------------------------------------------------------%
2066% insert_additiveFluent_rules
2067%-----------------------------------------------------------------------------%
2068
2069insert_additiveFluent_rules(AF,M,N) :- % AF = additiveFluent(S)
2070 V_AF = var(AF,-1), % additive Fluent
2071 arg(1,AF,S), % integer sort
2072 V_VS = var(S,-1),
2073 V_A = var(action(boolean),-1),
2074 V_A1 = var(action(boolean),-2),
2075 V_I = var(additiveInteger,-100),
2076 V_I1 = var(additiveInteger,-101),
2077
2078 Term = (default contribution(V_A, V_AF) = 0 where \+ abby(V_A)),
2079 insert_rule_schema(Term,1),
2080
2081 Term1 = (caused accumulatedContribution(V_A,V_AF)=V_I
2082 if first(V_A) & contribution(V_A,V_AF) = V_I where \+ abby(V_A)),
2083 insert_rule_schema(Term1,1),
2084
2085 Term2 = (caused accumulatedContribution(V_A,V_AF)=V_I+V_I1
2086 if next(V_A1,V_A) & accumulatedContribution(V_A1,V_AF) = V_I1
2087 & contribution(V_A,V_AF) = V_I
2088 where \+ abby(V_A), \+abby(V_A1), V_I+V_I1 >= minAdditive, V_I + V_I1 =< maxAdditive ),
2089 insert_rule_schema(Term2,1),
2090
2091 Term3 = (caused V_AF=V_I+V_VS
2092 after last(V_A) & accumulatedContribution(V_A,V_AF)=V_I
2093 & V_AF=V_VS
2094 where \+ abby(V_A), V_I+V_VS >= M, V_I+V_VS =< N),
2095 insert_rule_schema(Term3,1).
2096
2097
2098%-----------------------------------------------------------------------------%
2099% insert_additiveAction_rules
2100%-----------------------------------------------------------------------------%
2101
2102insert_additiveAction_rules(AF,M,N) :- % AF = additiveFluent(S)
2103 V_AF = var(AF,-1), % additive Fluent
2104 V_A = var(action(boolean),-1),
2105 V_A1 = var(action(boolean),-2),
2106 V_I = var(additiveInteger,-100),
2107 V_I1 = var(additiveInteger,-101),
2108
2109 Term = (default contribution(V_A, V_AF) = 0 where \+ abby(V_A)),
2110 insert_rule_schema(Term,1),
2111
2112 Term1 = (caused accumulatedContribution(V_A,V_AF)=V_I
2113 if first(V_A) & contribution(V_A,V_AF) = V_I where \+ abby(V_A)),
2114 insert_rule_schema(Term1,1),
2115
2116 Term2 = (caused accumulatedContribution(V_A,V_AF)=V_I+V_I1
2117 if next(V_A1,V_A) & accumulatedContribution(V_A1,V_AF) = V_I1
2118 & contribution(V_A,V_AF) = V_I
2119 where \+ abby(V_A), \+ abby(V_A1), V_I+V_I1 >= minAdditive,
2120 V_I + V_I1 =< maxAdditive ),
2121 insert_rule_schema(Term2,1),
2122
2123 Term3 = (caused V_AF=V_I
2124 if last(V_A) & accumulatedContribution(V_A,V_AF) = V_I
2125 where \+ abby(V_A), V_I >= M, V_I =< N),
2126 insert_rule_schema(Term3,1).
2127
2128%-----------------------------------------------------------------------------%
2129% insert_query_rules.
2130%-----------------------------------------------------------------------------%
2131
2132insert_query_rules([R0|_Rs]) :-
2133 leaf_element(R0,R),
2134 ( (R = (((B=>H) where C)); R = (((H<-B) where C));
2135 R = (((H<=B) where C));
2136 R = (((<- B) where C)), H = false;
2137 R = (((<= B) where C)), H = false)
2138 -> assertz(query_rule_schema(((H<=B) where C)))
2139
2140 ; (R = (B=>H); R = (H<-B); R = (H<=B);
2141 R = (<- B), H = false; R = (<= B), H = false)
2142 -> assertz(query_rule_schema((H<=B)))
2143
2144 ; assertz(query_rule_schema(((R <= true)))) ),
2145 fail.
2146
2147insert_query_rules([_R|Rs]) :-
2148 insert_query_rules(Rs).
2149
2150insert_query_rules([]) :- !.
2151
2152
2156
2157instantiate_sorts :-
2158 get_ccsorts(Nodes),
2159 instantiate_sorts(Nodes,[]),
2160 !.
2161
2162instantiate_sorts([],_Ancestors).
2163instantiate_sorts([node(S,Subs)|Nodes],Ancestors) :-
2164 ( domain(S,_) 2165 -> instantiate_sorts(Nodes,Ancestors)
2166 ; member(S,Ancestors)
2167 -> fatal_error("Cyclic term. term/arg of sort ~w.",[S])
2168 ; instantiate_sorts(Subs,[S|Ancestors]), 2169 ( domain_schema(S,Cs)
2170 -> true
2171 ; Cs = [] ),
2172 instantiate_sorts_in_terms(Cs,Ancestors), 2173 instantiate_terms(Cs,Es1),
2174 subsorts_extension(Subs,Es2), 2175 2176 2177 append(Es1,Es2,Es3),
2178 remove_duplicates(Es3,Es),
2179
2180 ( domain(S,Es)
2181 -> true
2182 ; assertz(domain(S,Es))),
2183 instantiate_sorts(Nodes,Ancestors) ).
2184
2185
2189
2190instantiate_sorts_in_terms([],_Ancestors).
2191
2192instantiate_sorts_in_terms([C|Cs],Ancestors) :-
2193 C =.. [_|Sorts], 2194 find_nodes(Sorts,Nodes),
2195 instantiate_sorts(Nodes,Ancestors),
2196 instantiate_sorts_in_terms(Cs,Ancestors).
2197
2198instantiate_sorts_in_terms([C|Cs],[]) :-
2199 C =.. [_|Sorts],
2200 ( Sorts = []
2201 -> instantiate_sorts_in_terms(Cs,[])
2202 ; fail).
2203
2204
2210
2211find_nodes(Sorts,Nodes) :-
2212 get_ccsorts(Graph),
2213 find_nodes(Sorts,Graph,Nodes).
2214
2215find_nodes([],_Graph,[]).
2216
2217find_nodes([Sort|Sorts],Graph,[Node|Nodes]) :-
2218 ( find_node(Graph,Sort,Node)
2219 -> find_nodes(Sorts,Graph,Nodes)
2220 ; fatal_error("~w is not a known sort.",[Sort]) ).
2221
2228
2229find_node([node(S,Subs)|Nodes],Sort,Node) :-
2230 ( S = Sort
2231 -> Node = node(S,Subs)
2232 ; find_node(Subs,Sort,Node)
2233 -> true
2234 ; find_node(Nodes,Sort,Node) ).
2235
2236
2242
2243subsorts_extension([],[]).
2244
2245subsorts_extension([node(S,_)|Nodes],Es) :-
2246 domain(S,Es1),
2247 subsorts_extension(Nodes,Es2),
2248 append(Es1,Es2,Es).
2249
2257instantiate_terms([C|Cs],Ds) :-
2258 subst_vars_for_type_names(C,D,Vs),
2259 findall(D,bind_vars_to_terms(Vs),Ds,Es),
2260 instantiate_terms(Cs,Es).
2261instantiate_terms([],[]).
2262
2263
2264%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2265%% subst_vars_for_type_names(+C,-D,-Vs) :
2266%% C : object or constant whose argument are sort(type) names
2267%% D : object or constant whose argument are the corresponding variable
2268%% Vs: list of var=[ground instance of sort]
2269%% ex) subst_vars_for_type_names(arirang(aa),arirang(_61671),[_61671=[a,a1]])
2270%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2271
2272subst_vars_for_type_names(C,D,Vs) :-
2273 ( atom(C) ; composite_sort(C) ; C = _* ),
2274 !,
2275 ( domain(C,Cs) -> Vs = [=(D,Cs)] ; D = C, Vs = [] ).
2276subst_vars_for_type_names(C,D,Vs) :-
2277 functor(C,F,N),
2278 functor(D,F,N),
2279 subst_vars_for_type_names_arg(C,0,N,D,Vs).
2280
2281subst_vars_for_type_names_arg(_C,N,N,_D,[]) :-
2282 !.
2283subst_vars_for_type_names_arg(C,M,N,D,Vs) :-
2284 M1 is M+1,
2285 arg(M1,C,A),
2286 subst_vars_for_type_names(A,B,Xs),
2287 arg(M1,D,B),
2288 subst_vars_for_type_names_arg(C,M1,N,D,Ys),
2289 append(Xs,Ys,Vs).
2290
2291bind_vars_to_terms([=(V,Cs)|Vs]) :-
2292 member(V,Cs), bind_vars_to_terms(Vs).
2293bind_vars_to_terms([]).
2294
2295
2296
2329
2330enumerate_atoms :-
2331 iset(atom_count,0),
2332 ( value(mode,transition)
2333 -> Steps = [0,1]
2334 ; domain(step,Steps) ),
2335 enumerate_atoms([none|Steps]).
2336
2337enumerate_atoms([]) :-
2338 value(atom_count,AC),
2339 iset(original_atom_count,AC).
2340
2341enumerate_atoms([none|Ts]) :-
2342 domain(rigidAtomicFormula,Fs),
2343 enumerate_atoms(none,Fs),
2344 ( value(mode,transition) -> set_atom_count(rigid_count,_) ; true ),
2345 enumerate_atoms(Ts).
2346
2347enumerate_atoms([T|_Ts]) :-
2348 ( domain(simpleFluentAtomicFormula,Fs)
2349 ; domain(sdFluentAtomicFormula,Fs) ),
2350 enumerate_atoms(T,Fs),
2351 fail.
2352
2353enumerate_atoms([0|_Ts]) :-
2354 value(mode,transition),
2355 set_atom_count(atom_count_0,_),
2356 set_atom_count(fluent_count,rigid_count),
2357 fail.
2358
2359enumerate_atoms([T,_T2|_Ts]) :-
2360 ( domain(actionAtomicFormula,Fs)
2361 ; domain(abActionAtomicFormula,Fs)
2362 ; domain(attributeAtomicFormula,Fs) ),
2363 enumerate_atoms(T,Fs),
2364 fail.
2365
2366enumerate_atoms([0|_Ts]) :-
2367 value(mode,transition),
2368 set_atom_count(action_count,atom_count_0),
2369 fail.
2370
2371enumerate_atoms([_T|Ts]) :-
2372 enumerate_atoms(Ts).
2373
2374enumerate_atoms(T,Fs) :-
2375 member(F,Fs),
2376 \+ (F = (A2 eq false), boolean_constant(A2)),
2377 ( T == none
2378 -> A = F
2379 ; A = (T: F) ),
2380 \+ atom_integer(A,_),
2381 incr(atom_count,N),
2382 assertz(atom_integer(A,N)),
2383 fail.
2384
2385enumerate_atoms(_,_).
2386
2387set_atom_count(Count,Prev) :-
2388 ( nonvar(Prev), value(Prev,PrevVal) -> true ; PrevVal = 0 ),
2389 ( value(atom_count,AC) -> true ; AC = 0 ),
2390 AC2 is AC - PrevVal,
2391 iset(Count,AC2).
2392
2393
2397
2398renumber_atoms :-
2399
2400 2401 2402 2403 2404 2405 2406 2407 2408 2409 2410 2411 2412 2413 2414 2415 2416 2417 2418 2419 2420 2421 2422 2423 2424 2425 2426 2427 2428 2429 2430 2431 2432
2433 value(atom_count,C),
2434 value(rigid_count,RC),
2435 value(fluent_count,FC),
2436 value(action_count,AC),
2437 value(aux_atom_count_from_rules_0,NAR0),
2438 value(aux_atom_count_from_rules,NAR),
2439 value(aux_atom_count_from_completion_0,NAC0),
2440 value(aux_atom_count_from_completion,NAC),
2441
2442 2443 2444 2445 2446 2447 2448 2449 2450 2451 2452 2453 2454 2455 2456 2457 2458 2459 2460 2461 2462
2463 Level1 is RC,
2464 Level2 is Level1 + FC + AC,
2465 Level3 is Level2 + FC,
2466 Level4 is Level3 + NAR0,
2467 Level5 is Level3 + NAR, 2468 Level6 is Level5 + NAC0,
2469 Shift2 is NAR0 + NAC0,
2470 Shift3 is NAR + NAC,
2471 Shift4 is -(2*FC+AC),
2472 Shift5 is -FC + NAC0,
2473 Shift6 is -(2*FC+AC)-(NAR-NAR0),
2474 Shift7 is -FC,
2475 Shifts = [[Level1,0],[Level2,Shift2],[Level3,Shift3],[Level4,Shift4],
2476 [Level5,Shift5],[Level6,Shift6],[C,Shift7]],
2477
2478 save_atom_integer_mapping,
2479 findall(atom_integer(A,I),atom_integer(A,I),AIs),
2480 retractall(atom_integer(_,_)),
2481 renumber_atoms(AIs,Shifts),
2482
2483 findall(C0,clause0(C0),Cs0),
2484 retractall(clause0(_)),
2485 renumber_clauses(0,Cs0,Shifts),
2486 findall(C1,clause1(C1),Cs1),
2487 retractall(clause1(_)),
2488 renumber_clauses(1,Cs1,Shifts),
2489
2490 value(atom_count_0,AC0),
2491 NewAC0 is AC0 + NAR0 + NAC0,
2492 iset(atom_count_0,NewAC0).
2493
2494save_atom_integer_mapping :-
2495 atom_integer(A,I),
2496 assertz(saved_atom_integer(A,I)),
2497 fail.
2498save_atom_integer_mapping.
2499
2500
2501renumber_atoms([],_).
2502
2503renumber_atoms([atom_integer(A,I)|AIs],[[Bound,Shift]|Shifts]) :-
2504 ( I =< Bound
2505 -> NewI is I + Shift,
2506 assertz(atom_integer(A,NewI)),
2507 renumber_atoms(AIs,[[Bound,Shift]|Shifts])
2508 ; renumber_atoms([atom_integer(A,I)|AIs],Shifts) ).
2509
2510renumber_clauses(_,[],_).
2511
2512renumber_clauses(Phase,[C|Cs],Shifts) :-
2513 2514 2515 renumber_clause(C,Shifts,NewC),
2516 ( Phase == 0
2517 -> assertz(clause0(NewC))
2518 ; assertz(clause1(NewC)) ),
2519 renumber_clauses(Phase,Cs,Shifts).
2520
2521
2522renumber_clause([],_,[]).
2523
2524renumber_clause([L|Ls],Shifts,[N|Ns]) :-
2525 renumber_atom_index(L,Shifts,N),
2526 renumber_clause(Ls,Shifts,Ns).
2527
2528renumber_atom_index(I,[[Bound,Shift]|Shifts],N) :-
2529 ( I > 0
2530 -> ( I =< Bound
2531 -> N is I + Shift
2532 ; renumber_atom_index(I,Shifts,N) )
2533 ; AbsI is 0 - I,
2534 renumber_atom_index(AbsI,[[Bound,Shift]|Shifts],AbsN),
2535 N is 0 - AbsN ).
2536
2537
2538
2542
2547
2549get_var(Sort,Identifier,Var) :-
2550 name('V',[ListV]),
2551 name('_',[ListUS]),
2552 ( Sort =.. [F,A]
2553 -> name(F,ListF),
2554 ( A =.. [A1,R] 2555 -> name(A1,ListA1),
2556 name(R,ListR),
2557 append(ListA1,ListR,ListA)
2558 ; name(A,ListA) ),
2559 append(ListF,ListA,ListL)
2560 ; name(Sort,ListL) ),
2561
2562 ( Identifier =.. [FI,AI]
2563 -> name(FI,ListFI),
2564 name(AI,ListAI),
2565 append(ListFI, ListAI, ListNV0)
2566 ; name(Identifier,ListNV0)),
2567
2568 append([ListV,ListUS|ListL],ListNV0,ListNewVarLabel),
2569 name(Var,ListNewVarLabel),
2570 (var_sort(Var,Sort) -> true; assertz(var_sort(Var,Sort))).
2571
2572get_internal_var(Sort,Var) :-
2573 value(var_counter,VC),
2574 VC1 is VC-1,
2575 iset(var_counter,VC1),
2576 get_var(Sort,VC,Var).
2577
2579get_sort(Var,ValSort) :-
2580 atom(Var),
2581 var_sort(Var,CompositeSort),
2582 !, 2583 arg(1,CompositeSort,ValSort).
2584
2585get_sort(Constant,ValSort) :-
2586 functor(Constant,F,N),
2587 functor(B,F,N),
2588 domain_schema(Sort,Ds),
2589 member(B,Ds),
2590 arg(1,Sort,ValSort).
2591
2592get_sort2(Constant,Sort) :-
2593 functor(Constant,F,N),
2594 functor(B,F,N),
2595 domain_schema(Sort,Ds),
2596 member(B,Ds).
2597
2598
2599decode_macro(Schema,Schema) :-
2600 (var(Schema); atomic(Schema)),
2601 !.
2602decode_macro(Schema,DecodedSchema) :-
2603 functor(Schema,F,N),
2604 functor(Schema1,F,N),
2605 decode_macro_arg(Schema,1,N,Schema1),
2606 ( Schema1=sort(C)
2607 -> get_sort(C,Sort),
2608 DecodedSchema=Sort
2609 ; Schema1=sort2(C)
2610 -> get_sort2(C,Sort),
2611 DecodedSchema=Sort
2612 ; Schema1=var(Sort,Id)
2613 -> get_var(Sort,Id,Var),
2614 DecodedSchema=Var
2615 ; DecodedSchema=Schema1 ).
2616
2617decode_macro_arg(_Schema,M,N,_Schema1) :-
2618 M > N,
2619 !.
2620decode_macro_arg(Schema,M,N,Schema1) :-
2621 arg(M,Schema,A),
2622 decode_macro(A,B),
2623 arg(M,Schema1,B),
2624 M1 is M+1,
2625 decode_macro_arg(Schema,M1,N,Schema1).
2626
2627
2633boolean_constant(var(Sort,_)) :-
2634 member_check(Sort,
2635 [simpleFluent(boolean), inertialFluent(boolean),
2636 sdFluent(boolean), rigid(boolean),
2637 action(boolean), abAction(boolean), exogenousAction(boolean), attribute(boolean)]).
2638
2640boolean_constant(C) :-
2641 var_sort(C,Sort),
2642 member_check(Sort,
2643 [simpleFluent(boolean), inertialFluent(boolean),
2644 sdFluent(boolean), rigid(boolean),
2645 action(boolean), abAction(boolean), exogenousAction(boolean), attribute(boolean)]).
2646
2648boolean_constant(C) :-
2649 !,
2650 functor(C,F,N),
2651 boolean_constants(F,N).
2652
2653
2655expand_boolean(Schema,Schema) :- var(Schema), !.
2656expand_boolean(Schema,Schema) :-
2657 functor(Schema,F,_), member_check(F, [eq, /\, \/, @<, ==]), !.
2658expand_boolean(Schema,ExpandedSchema) :-
2659 ( (Schema = -((T: C)), boolean_constant(C))
2660 -> ExpandedSchema = (T: C eq false)
2661 ; (Schema = -(C), boolean_constant(C))
2662 -> ExpandedSchema = (C eq false)
2663 ; boolean_constant(Schema)
2664 -> ExpandedSchema = (Schema eq true)
2665 ; is_constant(Schema)
2666 -> ExpandedSchema = Schema
2667 ; functor(Schema,F,N),
2668 functor(ExpandedSchema,F,N),
2669 expand_boolean_arg(Schema,1,N,ExpandedSchema) ).
2670
2671expand_boolean_arg(_Schema,M,N,_Schema1) :- M > N, !.
2672expand_boolean_arg(Schema,M,N,Schema1) :-
2673 arg(M,Schema,A),
2674 expand_boolean(A,B),
2675 arg(M,Schema1,B),
2676 M1 is M+1,
2677 expand_boolean_arg(Schema,M1,N,Schema1).
2678
2679
2680%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2681%% remove_time_stamps(Schema,RemovedSchema)
2682%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2683% remove time stamps for rigid constant and test expression
2684
2685remove_time_stamps(Schema,RemovedSchema) :-
2686 ( ( (Schema = ((_ : C eq V)) ), rigid(C) )
2687 -> RemovedSchema = (C eq V)
2688 ; (Schema = ((_ : T)), test(T))
2689 -> RemovedSchema = T
2690 ; (Schema = ((_ : A)), rigid(A))
2691 -> RemovedSchema = A
2692 ; functor(Schema,F,N),
2693 functor(RemovedSchema,F,N),
2694 remove_time_stamps_arg(Schema,1,N,RemovedSchema) ).
2695
2696remove_time_stamps_arg(_Schema,M,N,_Schema1) :- M > N, !.
2697remove_time_stamps_arg(Schema,M,N,Schema1) :-
2698 arg(M,Schema,A),
2699 remove_time_stamps(A,B),
2700 arg(M,Schema1,B),
2701 M1 is M+1,
2702 remove_time_stamps_arg(Schema,M1,N,Schema1).
2703
2704
2705%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2706% postprocessing_before_binding = expand_boolean + remove_time_stamps_for_rigid
2707%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2708/*
2709postprocessing_before_binding(Schema,Schema1) :-
2710 expand_boolean(Schema,Schema2),
2711 remove_time_stamps(Schema2,Schema1).
2712*/
2713
2714postprocessing_before_binding(Schema,ExpandedSchema) :-
2715 ( (functor(Schema,F,_), member_check(F, [eq, /\, \/, @<, ==]))
2716 -> ExpandedSchema = Schema
2717 ; (Schema = ((_ : C eq V)), rigid(C))
2718 -> ExpandedSchema = (C eq V)
2719 ; (Schema = ((_ : T)), test(T))
2720 -> ExpandedSchema = T
2721 ; (Schema = ((_ : A)), rigid(A))
2722 -> ( boolean_constant(A)
2723 -> ExpandedSchema = (A eq true)
2724 ; ExpandedSchema = A )
2725 ; (Schema = -((T: C)), boolean_constant(C))
2726 -> ( rigid(C)
2727 -> ExpandedSchema = (C eq false)
2728 ; ExpandedSchema = (T: C eq false) )
2729 ; (Schema = -(C), boolean_constant(C))
2730 -> ExpandedSchema = (C eq false)
2731 ; boolean_constant(Schema)
2732 -> ExpandedSchema = (Schema eq true)
2733 ; ( is_constant(Schema) % don't expand boolean constants inside some
2734 % other constant
2735 -> ExpandedSchema = Schema
2736 ; functor(Schema,F,N),
2737 functor(ExpandedSchema,F,N),
2738 postprocessing_before_binding_arg(Schema,1,N,ExpandedSchema) ) ).
2739
2740postprocessing_before_binding_arg(_Schema,M,N,_Schema1) :-
2741 M > N,
2742 !.
2743postprocessing_before_binding_arg(Schema,M,N,Schema1) :-
2744 arg(M,Schema,A),
2745 postprocessing_before_binding(A,B),
2746 arg(M,Schema1,B),
2747 M1 is M+1,
2748 postprocessing_before_binding_arg(Schema,M1,N,Schema1).
2749
2750
2756postprocessing_after_binding(Schema,Schema) :-
2757 (var(Schema); atomic(Schema)),
2758 !.
2759postprocessing_after_binding(Schema0,EvaluatedSchema) :-
2760 ( ( Schema0 = (T: C eq false), boolean_constant(C))
2761 -> Schema = -((T: C eq true))
2762 ; ( Schema0 = (C eq false), boolean_constant(C))
2763 -> Schema = -(C eq true)
2764 ; Schema = Schema0 ),
2765
2766 ( evaluable_expr(Schema)
2767 -> ( test(Schema)
2768 -> ( Schema =.. [= | Args]
2769 -> Schema1 =.. [=:= | Args] % to call prolog to evaluate =
2770 ; Schema1 = Schema ), % in evaluable expression
2771 ( call(Schema1)
2772 -> EvaluatedSchema=true
2773 ; EvaluatedSchema=false )
2774 ; EvaluatedSchema is Schema) % otherwise error
2775 ; functor(Schema,F,N),
2776 functor(EvaluatedSchema,F,N),
2777 postprocessing_after_binding_arg(Schema,1,N,EvaluatedSchema) ).
2778
2779postprocessing_after_binding_arg(_Schema,M,N,_Schema1) :-
2780 M > N,
2781 !.
2782postprocessing_after_binding_arg(Schema,M,N,Schema1) :-
2783 arg(M,Schema,A),
2784 postprocessing_after_binding(A,B),
2785 arg(M,Schema1,B),
2786 M1 is M+1,
2787 postprocessing_after_binding_arg(Schema,M1,N,Schema1).
2788
2789
2795replace_false_with_negative_literal(Schema,Schema) :-
2796 (var(Schema); atomic(Schema)),
2797 !.
2798replace_false_with_negative_literal(Schema,ReplacedSchema) :-
2799 ( ( (Schema = (T: C eq false)), boolean_constant(C))
2800 -> ReplacedSchema = -((T: C eq true))
2801 ; ( (Schema = (C eq false)), boolean_constant(C))
2802 -> ReplacedSchema = -(C eq true)
2803 ; functor(Schema,F,N),
2804 functor(ReplacedSchema,F,N),
2805 replace_false_with_negative_literal_arg(Schema,1,N,ReplacedSchema) ).
2806
2807replace_false_with_negative_literal_arg(_Schema,M,N,_Schema1) :-
2808 M > N,
2809 !.
2810replace_false_with_negative_literal_arg(Schema,M,N,Schema1) :-
2811 arg(M,Schema,A),
2812 replace_false_with_negative_literal(A,B),
2813 arg(M,Schema1,B),
2814 M1 is M+1,
2815 replace_false_with_negative_literal_arg(Schema,M1,N,Schema1).
2816
2817
2819
2824
2829evaluable_expr(Expr) :- number(Expr), !.
2831 2832evaluable_expr(-(Expr)) :- evaluable_expr(Expr), !.
2833evaluable_expr(Expr) :-
2834 functor(Expr,F,2),
2835 !, 2836 ( member_check(F,['+','-','*','/','//','rem','mod','gcd','min',
2837 'max']) 2838 -> arg(1,Expr,FirstArg), evaluable_expr(FirstArg),
2839 arg(2,Expr,SecondArg), evaluable_expr(SecondArg) ).
2840
2841evaluable_expr(Expr) :- 2842 functor(Expr,F,1),
2843 !,
2844 ( member_check(F,['abs'])
2845 -> arg(1,Expr,FirstArg), evaluable_expr(FirstArg) ).
2846
2847
2853eval_expr(Schema,Schema) :-
2854 (var(Schema); atomic(Schema)),
2855 !.
2856
2857eval_expr(Schema,EvaluatedSchema) :-
2858 ( evaluable_expr(Schema)
2859 -> ( test(Schema)
2860 -> ( Schema =.. [= | Args]
2861 -> Schema1 =.. [=:= | Args] 2862 ; Schema1 = Schema ), 2863 ( call(Schema1)
2864 -> EvaluatedSchema=true
2865 ; EvaluatedSchema=false )
2866 ; EvaluatedSchema is Schema) 2867 ; functor(Schema,F,N),
2868 ( ( (F == '='),arg(1,Schema,C),is_constant(C) )
2869 2870 2871 2872 -> F1 = 'eq'
2873 ; F1 = F ),
2874 functor(EvaluatedSchema,F1,N),
2875 eval_expr_arg(Schema,1,N,EvaluatedSchema) ).
2876
2877eval_expr_arg(_Schema,M,N,_Schema1) :-
2878 M > N,
2879 !.
2880eval_expr_arg(Schema,M,N,Schema1) :-
2881 arg(M,Schema,A),
2882 eval_expr(A,B),
2883 arg(M,Schema1,B),
2884 M1 is M+1,
2885 eval_expr_arg(Schema,M1,N,Schema1).
2886
2887
2888
2890
2891
2892adjust_where(C,_) :-
2893 var(C), !.
2894adjust_where((-(A)),(\+ (A1))) :-
2895 \+ evaluable_expr(A),
2896 !,
2897 adjust_where(A,A1).
2898adjust_where(C,C1) :-
2899 functor(C,F,N),
2900 ( (F == '&&'; F == '&')
2901 -> functor(C1,',',N)
2902 ; (F == '++')
2903 -> functor(C1,';',N)
2904 ; (F == '=') 2905 2906 2907 -> functor(C1,'==',N) ),
2908 !,
2909 adjust_where_arg(C,1,N,C1).
2910adjust_where(C,C1) :-
2911 functor(C,F,N),
2912 functor(C1,F,N),
2913 adjust_where_arg(C,1,N,C1).
2914
2915adjust_where_arg(_C,M,N,_C1) :-
2916 M>N,
2917 !.
2918adjust_where_arg(C,M,N,C1) :-
2919 arg(M,C,A),
2920 adjust_where(A,B),
2921 arg(M,C1,B),
2922 M1 is M+1,
2923 adjust_where_arg(C,M1,N,C1).
2924
2925
2926%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2927%% process_rule_schemas
2928%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2929%
2930% Ground all of the rule schemas, by replacing every variable in each schema
2931% with each possible object of the appropriate type. During grounding,
2932% new atoms may be introduced to simplify complicated formulae
2933% (specifically those which contain a large conjunction of disjunctions or
2934% disjunction of conjunctions -- new atoms are introduced to avoid
2935% distributing one connective across the other). At the end of the procedure,
2936% the variable rule_count will store the total number of rules.
2937%
2938% In transition mode, some of the clauses generated will need to be shifted
2939% to later time units when a query is made. The rules are therefore grounded
2940% in such a way as to distinguish between the clauses which must be shifted
2941% and those which must not. First, all rule schemas stored with the predicate
2942% rule_schema/2 are grounded; these correspond to static laws at time 0.
2943% Next, the schemas in rule_schema1/2 are grounded; these correspond to static
2944% laws at time 1 and dynamic laws, which must be shifted. At the end of the
2945% procedure, the variable rule_count will still store the total number of
2946% rules as above. Additionally, rule_count_0 will contain the number
2947% of rules which will not be shifted; aux_atom_count_from_rules_0
2948% will store the number of new atoms generated during the grounding of
2949% static laws at time 0; and aux_atom_count_from_rules will store the total
2950% number of new atoms introduced during rule grounding.
2951
2952abby(A eq true) :- ab(A).
2953abby(A eq false) :- ab(A).
2954
2955process_rule_schemas :-
2956 iset(rule_count_0,0),
2957 iset(rule_count,0),
2958 iset(aux_atom_count,0),
2959
2960 % Start a loop -- select each rule schema and process it. After all rules
2961 % in rule_schema/2 have been processed, set the value of static0_rule_count
2962 % equal to the current rule_count, and then start processing rules in
2963 % rule_schema1/2.
2964
2965 ( value(mode,transition)
2966 -> ( % First, process static laws at time 0
2967 Phase=0,
2968 assertz(domain(step,[0])),
2969 assertz(domain(astep,[])),
2970 rule_schema(Schema)
2971 ; % Set variables related to static laws at time 0, then process
2972 % static laws at time 1 & dynamic laws
2973 Phase=1,
2974 value(atom_count,AC),
2975 value(original_atom_count,OAC),
2976 AACR0 is AC - OAC,
2977 iset(aux_atom_count_from_rules_0,AACR0),
2978 value(rule_count,RC),
2979 iset(rule_count_0,RC),
2980 retractall(domain(step,_)),
2981 retractall(domain(astep,_)),
2982 assertz(domain(step,[0,1])),
2983 assertz(domain(astep,[0])),
2984 rule_schema1(Schema) )
2985 ; rule_schema(Schema) ),
2986
2987 ( Schema = (Schema1 where Condition)
2988 -> adjust_where(Condition,Condition1)
2989 ; Schema = Schema1,
2990 Condition1 = true ),
2991
2992% postprocessing before binding
2993 decode_macro(Schema1,Schema2),
2994 decode_nested_constants_in_rule(Schema2,Schema3,CVs),
2995 postprocessing_before_binding(Schema3,Schema5),
2996 find_free_variables(Schema5,Vs1),
2997
2998/* to save time
2999% ( (Phase==1, \+ rule_has_time_stamps(Schema7))
3000% -> fail
3001% ; true ),
3002*/
3003 ( Condition1 \== true
3004 -> decode_macro(Condition1,Condition2),
3005 decode_nested_constants_for_condition(Condition2,Condition3,CVs),
3006 expand_boolean(Condition3,Condition4),
3007 remove_time_stamps(Condition4,Condition5),
3008 find_free_variables(Condition5,Vs2)
3009 ; Condition5 = true,
3010 Vs2 = [] ),
3011
3012 append(Vs1,Vs2,Vs3),
3013 remove_duplicates(Vs3,Vs),
3014 renaming_subst(Vs,Sub),
3015 subst_free(Schema5,Schema6,Sub),
3016 subst_free(Condition5,Condition6,Sub),
3017
3018 % at this point H0<=B0 is a rule schema whose variable is
3019 % in the form of prolog, and Sub is a pair like, ['B'=_297545,'L'=_297906]
3020 bind_vars(Sub), % loop starts here - until every free variable is
3021 % replaced with ground instances of corresponding sort
3022 ( (eval_expr(Condition6,Condition7), call(Condition7))
3023 % eval_expr? car1=:=car2 will not do; instead car1==car2
3024 -> true
3025 ; fail ),
3026
3027 postprocessing_after_binding(Schema6,(H<=B)),
3028
3029 negation_normal_form(B,B1),
3030 ( B1 = false -> fail ; true ),
3031 negation_normal_form(H,H1),
3032
3033 % remember the current value of atom_count
3034 value(atom_count,A),
3035
3036 % convert head to CNF and body to DNF, possibly introducing new auxiliary
3037 % atoms
3038 nnf_to_cnf(H1,Hss,Aux1),
3039 nnf_to_dnf(B1,Bss,Aux2),
3040 store_rule_schemas(Hss,Bss),
3041
3042 % if either head or body is empty, the rule wasn't stored, so the
3043 % clauses defining each new atom shouldn't be either. (Otherwise
3044 % these atoms are defined in the input file but are useless since they
3045 % don't appear in any "real" clause.) Reset atom_count to its previous
3046 % level to "delete" those new atoms.
3047 ( ( Hss == []; Bss == [] )
3048 -> iset(atom_count,A)
3049
3050 % otherwise, store the clauses defining new atoms used in the
3051 % main clause.
3052 ; store_aux_schemas(Aux1),
3053 store_aux_schemas(Aux2) ),
3054 fail.
3055
3056process_rule_schemas :-
3057 value(original_atom_count,OAC),
3058 value(atom_count,AC),
3059 AACFR is AC - OAC,
3060 iset(aux_atom_count_from_rules,AACFR).
3061
3062store_rule_schemas(Hss,Bss) :-
3063 member(Ms,Hss),
3064 member(Ns,Bss),
3065 incr(rule_count,I),
3066 db_open_external(I),
3067 db_store_rule(I,rule_body(I,Ns)),
3068 ( Ms = [] -> Ms1 = [0]; Ms1 = Ms ),
3069 ( Ms1 = [D]
3070 -> db_store_rule(I,(D<=I))
3071 ; fatal_error("One of the rules is not definite.",[])),
3072 fail. 3073
3074store_rule_schemas(_,_).
3075
3076
3077store_aux_schemas(Aux) :-
3078 member(C,Aux),
3079 negate_lits(C,NC),
3080 store_rule_schemas([[]],[NC]),
3081 fail.
3082
3083store_aux_schemas(_).
3084
3085
3086%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3087%% decode_nested_constants
3088%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3089
3090%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3091% decode_nested_constants_in_rule(+Rule,-Rule1,-CVs) :
3092% Rule: causal rule in which constants may contain other constants
3093% as arguments. For a theory to be definite, such nesting
3094% should not occur in the heads
3095% Rule1: the resulting rule of unfolding
3096% CVs: used in condition
3097%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3098decode_nested_constants_in_rule((H<=B),(H<=B2),CVs) :-
3099%^ should check nested constants are not used in the head of a rule
3100 ( (H = ((_: C = D)) ; (H = (C = D)))
3101 -> ( (evaluable_expr(C), evaluable_expr(D))
3102 -> true
3103 ; (evaluable_expr(C); evaluable_expr(D))
3104 -> subst_functor(eq,=,H,H2),
3105 fatal_error("Unrecognized identifiers in ~w",H2)
3106 ; subst_functor(eq,=,(H<=B),(H1<=B1)),
3107 fatal_error("The rule is not definite: ~w",(H1<=B1)) )
3108 ; true ),
3109
3110 decode_nested_constants(B,B1,CVs),
3111 list_to_conjuncts(CVs,Conjuncts),
3112 B2 = (B1 & Conjuncts).
3113
3120decode_nested_constants(Formula,Formula1,CVs) :-
3121 decode_nested_constants(Formula,Formula1,[],CVs,-1).
3122
3123decode_nested_constants(Formula,Formula1,Acc,CVs,Step) :-
3124 ( (is_constant(Formula); expr(Formula); test(Formula))
3125 3126 3127 3128 3129 -> unfold_nested_constants(Formula,Formula1,Acc,CVs,Step,_,-1,_)
3130 ; quantified_formula(Formula)
3131 -> unfold_quantified_formula(Formula,Formula1,Acc,CVs,[],Step)
3132 ; ( Formula = (T: _)
3133 -> Step1 = T
3134 ; Step1 = Step ),
3135 functor(Formula,F,N),
3136 functor(Formula1,F,N),
3137 decode_nested_constants_arg(Formula,1,N,Formula1,Acc,CVs,Step1) ).
3138
3139decode_nested_constants_arg(_Schema,M,N,_Schema1,Acc,Acc,_Step) :-
3140 M > N,
3141 !.
3142decode_nested_constants_arg(Schema,M,N,Schema1,Acc,CVs,Step) :-
3143 arg(M,Schema,A),
3144 decode_nested_constants(A,B,Acc,Acc1,Step),
3145 arg(M,Schema1,B),
3146 M1 is M+1,
3147 decode_nested_constants_arg(Schema,M1,N,Schema1,Acc1,CVs,Step).
3148
3149quantified_formula([\/ _Q | _F]).
3150quantified_formula([/\ _Q | _F]).
3151
3163
3166unfold_nested_constants((A@<B),(A@<B),Acc,Acc,_Step,_,_,_) :- !.
3167unfold_nested_constants((A==B),(A==B),Acc,Acc,_Step,_,_,_) :- !.
3168
3170unfold_nested_constants((T:C),D,Acc,CVs,Step,F0,N0,Arity0) :-
3173 !,
3174 functor(C,F,N),
3175 functor(C1,F,N),
3176 unfold_nested_constants_arg(C,C1,Acc,Acc1,Step,F,1,N),
3177 ( (\+ is_constant(C) ; skip_unfolding(F0,N0,Arity0))
3178 -> D=(T:C1),
3179 CVs=Acc1
3180 ; ( member_check((T: eq(C1,V1)),Acc1)
3181 3182 -> D=V1,
3183 CVs = Acc1
3184 ; D=V1,
3185 get_sort(C1,Sort),
3186 get_internal_var(Sort,V1),
3187 append(Acc1,[(T: eq(C1,V1))],CVs) ) ).
3188
3189unfold_nested_constants(C,D,Acc,CVs,Step,F0,N0,Arity0) :-
3191 !,
3192 functor(C,F,N),
3193 functor(C1,F,N),
3194 unfold_nested_constants_arg(C,C1,Acc,Acc1,Step,F,1,N),
3195 ( (\+ is_constant(C); skip_unfolding(F0,N0,Arity0))
3196 -> D=C1,
3197 CVs=Acc1
3198 ; ( member_check((Step: eq(C1,V1)),Acc1) 3199 3200 -> D=V1,
3201 CVs = Acc1
3202 ; D=V1,
3203 get_sort(C1,Sort),
3204 get_internal_var(Sort,V1),
3205 append(Acc1,[(Step: eq(C1,V1))],CVs) ) ).
3206
3207
3208unfold_nested_constants_arg(_C,_C2,Acc,Acc,_Step,_F,M,N) :-
3209 M > N,
3210 !.
3211unfold_nested_constants_arg(C,C2,Acc,CVs,Step,F,M,N) :-
3212 arg(M,C,A),
3213 unfold_nested_constants(A,A2,Acc,Acc1,Step,F,M,N),
3214 arg(M,C2,A2),
3215 M1 is M+1,
3216 unfold_nested_constants_arg(C,C2,Acc1,CVs,Step,F,M1,N),
3217 !.
3218
3226skip_unfolding(_,-1,_) :- !. 3227skip_unfolding(F,N,Arity) :- 3228 !,
3229 functor(P,F,Arity),
3230 domain_schema(_,L),
3231 member(P,L),
3232 arg(N,P,K),
3233 composite_sort(K).
3234
3235%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3236% unfold_quantified_formula(+QSubF,-F1,+Acc,-CVs,+AccQ,+Step)
3237% QSubF: quantified formula
3238% F : new formula whose nested constants are unfolded
3239% Acc : accumulation of CVs
3240% CVs : a list of (T: C eq V) where C is a nested constant
3241% V is universally quantified
3242% AccQ : accumulation of quantifiers
3243% Step : time stamp for elements in CVs
3244%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3245unfold_quantified_formula([\/Q|SubF],Formula1,Acc,CVs,AccQ,Step) :-
3246 append(AccQ,[Q],AccQ1),
3247 ( quantified_formula(SubF)
3248 -> unfold_quantified_formula(SubF,SubF1,Acc,CVs,AccQ1,Step),
3249 Formula1 = [\/Q | SubF1]
3250 ; decode_nested_constants(SubF,SubF1,[],CVs0,0),
3251 separate_cvpairs(CVs0,AccQ1,QCVs,UCVs),
3252 make_quantified_formula(SubF1,QCVs,SubF2),
3253 append(Acc,UCVs,CVs),
3254 Formula1 = [\/Q|SubF2] ).
3255
3256unfold_quantified_formula([/\Q|SubF],Formula1,Acc,CVs,AccQ,Step) :-
3257 append(AccQ,[Q],AccQ1),
3258 ( quantified_formula(SubF)
3259 -> unfold_quantified_formula(SubF,SubF1,Acc,CVs,AccQ1,Step),
3260 Formula1 = [/\Q | SubF1]
3261 ; decode_nested_constants(SubF,SubF1,[],CVs0,0),
3262 separate_cvpairs(CVs0,AccQ1,QCVs,UCVs),
3263 make_quantified_formula(SubF1,QCVs,SubF2),
3264 append(Acc,UCVs,CVs),
3265 Formula1 = [/\Q|SubF2] ).
3266
3276separate_cvpairs(CVs,AccQ,QCVs,UCVs) :-
3277 find_unquantified_cvpairs(CVs,AccQ,UCVs),
3278 subtract(CVs,UCVs,QCVs).
3279
3287find_unquantified_cvpairs(CVs,[Q|Qs],UCVs) :-
3288 find_cvpairs_containing_quantifier(Q,CVs,QCVs),
3289 subtract(CVs,QCVs,CVs1),
3290 find_unquantified_cvpairs(CVs1,Qs,UCVs).
3291find_unquantified_cvpairs(UCVs,[],UCVs).
3292
3299find_cvpairs_containing_quantifier(Q,CVs,QCVs) :-
3300 find_cvpairs_containing_quantifier(Q,CVs,[],QCVs).
3301
3302find_cvpairs_containing_quantifier(Q,[(T: C eq V)|CVs],Acc,QCVs) :-
3303 ( constant_has_quantified_variable(C,Q)
3304 -> append(Acc,[(T: C eq V)],Acc1)
3305 ; Acc1 = Acc ),
3306 find_cvpairs_containing_quantifier(Q,CVs,Acc1,QCVs).
3307
3308find_cvpairs_containing_quantifier(_Q,[],QCVs,QCVs).
3309
3310
3317constant_has_quantified_variable(C,Va) :-
3318 C =.. [_F | Args],
3319 member_check(Va,Args).
3320
3321
3322%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3323%% make_quantified_formula(+Formula,+QCVs,-Formula2)
3324%% Formula : input formula
3325%% QCVs : a list of (T: C eq V) where C contains a
3326%% quantified variable
3327%% Formula2 : variables V in (T: C eq V) is quantified
3328%% ex) With [\/N | c(d(N))]
3329%% Call: make_quantified_formula((0:c('V_boolean-20')),
3330%% [(0:d('N')eq 'V_boolean-20')],_18102) ? s
3331%% Exit: make_quantified_formula((0:c('V_boolean-20')),
3332%% [(0:d('N')eq 'V_boolean-20')],
3333%% [\/'V_boolean-20'|(0:c('V_boolean-20'))
3334%% &&(0:d('N')eq 'V_boolean-20')]) ?
3335%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3336
3337make_quantified_formula(Formula,[(T: C eq V)|CVs],Formula2) :-
3338 make_quantified_formula(Formula,CVs,Formula1),
3339 Formula2 = [\/ V | Formula1 && (T: C eq V)].
3340make_quantified_formula(Formula,[],Formula).
3341
3342
3347decode_by(A,Val,CVs,T) :- trace, decode_by_1(A,Val,CVs,T).
3348decode_by_1(A,Val,CVs,T) :-
3349 ( is_constant(A)
3350 -> unfold_nested_constants_inside(A,Val,[],CVList,T)
3351 ; (expr(A); is_constant(A) ; test(A))
3352 -> unfold_nested_constants(A,Val,[],CVList,T) ),
3353 replace_comma_with_and_1(CVList,CVs).
3354
3355
3369decode_nested_constants_in_fact(Formula,Formula1) :-
3370 decode_nested_constants(Formula,Formula2,CVs),
3372 make_exist_quantified_formula_from_cvpairs(Formula2,CVs,Formula1).
3373
3374make_univ_quantified_formula_from_cvpairs(Formula,CVs,Formula1) :-
3375 findall(V,member((_T: _C eq V),CVs),Vs),
3376 % collect variables to be universally quantified
3377 ( Vs == []
3378 -> Formula1 = Formula
3379 ; list_to_tuple(CVs,CVsTuple),
3380 Formula2 = (CVsTuple ->> Formula),
3381 wrap_univ_quantifiers(Vs,Formula2,Formula1) ).
3382
3383wrap_univ_quantifiers([Q|Qs],Formula,Formula1) :-
3384 Formula2 = [/\Q| Formula],
3385 wrap_univ_quantifiers(Qs,Formula2,Formula1).
3386wrap_univ_quantifiers([],Formula,Formula).
3387
3388make_exist_quantified_formula_from_cvpairs(Formula,CVs,Formula1) :-
3389 findall(V,member((_T: _C eq V),CVs),Vs),
3390 % collect variables to be universally quantified
3391 ( Vs == []
3392 -> Formula1 = Formula
3393 ; %list_to_tuple(CVs,CVsTuple),
3394 conjoin_list(CVs,CVsTuple),
3395 Formula2 = (CVsTuple & Formula),
3396 wrap_exist_quantifiers(Vs,Formula2,Formula1) ).
3397
3398wrap_exist_quantifiers([Q|Qs],Formula,Formula1) :-
3399 Formula2 = [\/Q| Formula],
3400 wrap_exist_quantifiers(Qs,Formula2,Formula1).
3401wrap_exist_quantifiers([],Formula,Formula).
3402
3403list_to_conjuncts([L|Ls],Cs) :-
3404 list_to_conjuncts(Ls,Cs1),
3405 Cs = (L && Cs1).
3406list_to_conjuncts([],true).
3407
3408decode_nested_constants_for_condition(Formula,Formula1,CVs) :-
3409 ( has_no_constants(Formula)
3410 -> true
3411 ; fatal_error("constants cannot be used in where clause: ~w", Formula) ),
3412 decode_nested_constants(Formula,Formula1,CVs,_,0).
3413
3414
3415%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3416
3417process_query_rule_schemas :-
3418 iset(query_rule_count,0),
3419 query_rule_schema(Schema),
3420
3421 ( Schema = (Schema1 where Condition)
3422 -> adjust_where(Condition,Condition1)
3423 ; Schema = Schema1,
3424 Condition1 = true ),
3425
3426 % postprocessing before binding
3427 decode_macro(Schema1,Schema2),
3428 decode_nested_constants_in_rule(Schema2,Schema3,CVs),
3429 expand_boolean(Schema3,Schema4),
3430 remove_time_stamps(Schema4,Schema5),
3431 find_free_variables(Schema5,Vs1),
3432
3433 ( Condition1 \== true
3434 -> decode_macro(Condition1,Condition2),
3435 decode_nested_constants_for_condition(Condition2,Condition3,CVs),
3436 expand_boolean(Condition3,Condition4),
3437 remove_time_stamps(Condition4,Condition5),
3438 find_free_variables(Condition5,Vs2)
3439 ; Condition5 = true,
3440 Vs2 = [] ),
3441
3442 append(Vs1,Vs2,Vs3),
3443 remove_duplicates(Vs3,Vs),
3444 renaming_subst(Vs,Sub),
3445 subst_free(Schema5,Schema6,Sub),
3446 subst_free(Condition5,Condition6,Sub),
3447
3448 % at this point H0<=B0 is a rule schema whose variable is
3449 % in the form of prolog, and Sub is a pair like, ['B'=_297545,'L'=_297906]
3450 bind_vars(Sub), % loop starts here - until every free variable is
3451 % replaced with ground instances of corresponding sort
3452 ( (eval_expr(Condition6,Condition7), call(Condition7))
3453 -> true
3454 ; fail ),
3455
3456 do_term_expansion(Schema6,Schema61), %^ for maxstep expansion
3457 %^ maxstep: true -> 3: true.
3458 postprocessing_after_binding(Schema61,(H<=B)),
3459
3460 negation_normal_form(B,B1),
3461 ( B1 = false -> fail ; true ),
3462 negation_normal_form(H,H1),
3463
3464 nnf_to_cnf(H1,Hss,Aux1),
3465 nnf_to_dnf(B1,Bss,Aux2),
3466 store_query_rule_schemas(Hss,Bss),
3467
3468 ( ( Hss == []; Bss == [] )
3469 -> true
3470 ; store_aux_query_schemas(Aux1),
3471 store_aux_query_schemas(Aux2) ),
3472 fail.
3473process_query_rule_schemas.
3474
3475
3476store_query_rule_schemas(Hss,Bss) :-
3477 member(Ms,Hss),
3478 member(Ns,Bss),
3479 incr(query_rule_count,I),
3480 db_open_query_external(I),
3481 db_store_query_rule(I,query_rule_body(I,Ns)),
3482 ( Ms = [] -> Ms1 = [0]; Ms1 = Ms ),
3483 ( Ms1 = [D]
3484 -> db_store_query_rule(I,(D<-I))
3485 ; fatal_error("One of the rules is not definite.",[])),
3486 fail.
3487store_query_rule_schemas(_,_).
3488
3489store_aux_query_schemas(Aux) :-
3490 member(NC,Aux),
3491 store_query_rule_schemas([[]],NC),
3492 fail.
3493store_aux_query_schemas(_).
3494
3496
3507
3509bind_vars([=(Name,Var)|Bs]) :-
3510 ( var_sort(Name,Sort)
3511 -> ( Sort == computed
3512 -> true
3513 ; domain(Sort,Es)
3514 -> member(Var,Es)
3515 ; fatal_error("Unknown sort (~w).",[Sort]) )
3516 ; fatal_error("Unknown variable (~w).",[Name]) ),
3517 bind_vars(Bs).
3518bind_vars([]).
3519
3520
3523
3524generate_completion_clauses(Stage) :-
3525 value(mode,Mode),
3526 generate_completion_clauses(Stage,Mode).
3527
3528generate_completion_clauses(Stage,Mode) :-
3529 % Generates all of the completion clauses for the theory. First, it
3530 % finds each rule of the form (false <= Body), and adds the negation of
3531 % Body as a clause. Then, for each atom A in the theory, it collects all
3532 % of the rules of the form (A <= Body), and adds clauses to set A
3533 % equivalent to the disjunction of every such Body. The same is then
3534 % done for -A.
3535
3536 % In transition mode, some of these clauses will need to be shifted during
3537 % query processing. Thus, completion must be performed in such a way as
3538 % to make clear which clauses should be shifted and which should not.
3539 % Completion for transition mode will therefore be performed in two steps.
3540 % First, in Phase 0, all of the rules corresponding to static laws at time 0
3541 % will be completed; then all of the rules corresponding to static laws at
3542 % time 1 and dynamic laws will be completed. (Clauses resulting from the
3543 % former will not be shifted to later time steps; clauses from the latter
3544 % will.) At the end of the procedure, the variable clause_count_0
3545 % will store the number of clauses which will not be shifted; clause_count
3546 % will store the total number of clauses;
3547 % aux_atom_count_from_completion_0 will store the number of new
3548 % atoms introduced for static laws at time 0 during completion; and
3549 % aux_atom_count_from_completion will store the total number of new
3550 % atoms introduced during completion.
3551
3552 ( Stage == domain
3553 -> iset(clause_count_0,0),
3554 iset(clause_count,0)
3555 ; iset(query_clause_count,0) ),
3556
3557 ( Stage == domain, Mode == transition
3558 -> value(atom_count_0,AC0),
3559 value(atom_count,AC1),
3560 value(rule_count_0,RC0),
3561 ( Phase = 0
3562 ; write_clauses_for_eq([0],Stage),
3563 value(clause_count,CC0),
3564 iset(clause_count_0,CC0),
3565 value(atom_count,AC2),
3566 AACC0 is AC2 - AC1,
3567 iset(aux_atom_count_from_completion_0,AACC0),
3568 Phase = 1 )
3569 ; % if maxstep is 0 when processing a transition mode query, generate
3570 % completion only for phase 0 atoms
3571 Mode == transition, macro(maxstep,true,0)
3572 -> value(atom_count_0,AC0),
3573 value(rule_count_0,RC0),
3574 Phase = 0
3575 ; true ),
3576
3577 % For each rule with false in the head, add its negated body as a clause
3578 ( ( Stage == domain
3579 -> db_fetch_rule((0<=L)),
3580 ( Phase == 0 -> L =< RC0
3581 ; Phase == 1 -> L > RC0
3582 ; true ),
3583 db_fetch_rule(rule_body(L,Ns))
3584 ; db_fetch_query_rule((0<-L)),
3585 ( Phase == 0 -> L =< RC0
3586 ; Phase == 1 -> L > RC0
3587 ; true ),
3588 db_fetch_query_rule(query_rule_body(L,Ns)) ),
3589 negate_lits(Ns,Cs),
3590 store_clause(Cs,Stage,Mode,Phase),
3591 fail
3592
3593 % Generate the completion of each atom. In Phase 0, do so only for rigid
3594 % constants and fluents at time 0 (those atoms with an index <=
3595 % static0_atom_count) and new atoms generated for static laws at
3596 % time 0 (those atoms with index > original_atom_count, but <= this plus
3597 % static0_new_atom_count_from_rules). In Phase 1, do so for the remaining
3598 % atoms. If not in transition mode (i.e. neither phase 0 nor 1), don't
3599 % worry about it and just do every atom.
3600
3601 ; (atom_integer((_Step: Constant eq V),N); atom_integer((Constant eq V),N)),
3602
3603 % *jc* need to do this more efficiently
3604 ( Phase == 0 -> N =< AC0
3605 ; Phase == 1 -> N > AC0
3606 ; true ),
3607 ( singleton_domain_constant(Constant)
3608 -> fail
3609 ; true),
3610 C is 0-N,
3611
3612 % store clauses corresponding to right-to-left implications
3613
3614 ( ( ( Stage == domain
3615 -> db_fetch_rule((N<=L)),
3616 db_fetch_rule(rule_body(L,Ms))
3617 ; db_fetch_query_rule((N<-L)),
3618 db_fetch_query_rule(query_rule_body(L,Ms)) ),
3619 negate_lits(Ms,Cs),
3620 store_clause([N|Cs],Stage,Mode,Phase),
3621 fail
3622
3623 % store clauses corresponding to left-to-right implications
3624
3625 ; % collect all the rule bodies with N as the head into a DNF formula
3626 ( Stage == domain
3627 -> rule_bodies_for_literal(N,Nss)
3628 ; query_rule_bodies_for_literal(N,Nss) ),
3629 % convert this to CNF, possibly introducing auxiliary atoms
3630 distribute_or_over_and(Nss,NewNss,Aux),
3631 ( member(Ns,NewNss),
3632 store_clause([C|Ns],Stage,Mode,Phase)
3633 ; member(Ns,Aux),
3634 store_clause(Ns,Stage,Mode,Phase) ),
3635 fail )
3636
3637 % if the current atom is a boolean fluent, generate completion clauses
3638 % for its negation too. (If it's nonboolean, this isn't necessary,
3639 % since there is a separate atom corresponding to each value of the
3640 % fluent.)
3641
3642 ; ( ( atom_integer((_Constant eq true),N) ;
3643 atom_integer((_Step: _Constant eq true),N) )
3644 -> ( ( Stage == domain
3645 -> db_fetch_rule((C<=L)),
3646 db_fetch_rule(rule_body(L,Ms))
3647 ; db_fetch_query_rule((C<-L)),
3648 db_fetch_query_rule(query_rule_body(L,Ms)) ),
3649 negate_lits(Ms,Cs),
3650 store_clause([C|Cs],Stage,Mode,Phase),
3651 fail
3652 ; ( Stage == domain
3653 -> rule_bodies_for_literal(C,Nss)
3654 ; query_rule_bodies_for_literal(C,Nss)),
3655 distribute_or_over_and(Nss,NewNss,Aux),
3656 ( member(Ns,NewNss),
3657 store_clause([N|Ns],Stage,Mode,Phase)
3658 ; member(Ns,Aux),
3659 store_clause(Ns,Stage,Mode,Phase) ),
3660 fail )
3661 ; fail ))).
3662
3663generate_completion_clauses(domain,Mode) :-
3664 ( Mode == transition
3665 -> write_clauses_for_eq([1],domain)
3666 ; write_clauses_for_eq(domain) ),
3667 value(atom_count,AC),
3668 iset(domain_atom_count,AC),
3669 value(original_atom_count,OAC),
3670 AAC is AC - OAC,
3671 iset(aux_atom_count,AAC),
3672 value(aux_atom_count_from_rules,AACFR),
3673 AACFC is AAC - AACFR,
3674 iset(aux_atom_count_from_completion,AACFC).
3675
3676generate_completion_clauses(query,_Mode).
3677
3678singleton_domain_constant(Constant) :-
3679 domain(D,Ds),
3680 member(Constant,Ds),
3681 arg(1,D,Sort),
3682 domain(Sort,Ss),
3683 length(Ss,1).
3684
3685
3687
3688number_of_clauses([Ns|Nss],Num) :-
3689 length(Ns,Num1),
3690 number_of_clauses(Nss,Num2),
3691 Num is Num1 * Num2.
3692
3693number_of_clauses([],1).
3694
3695
3696number_of_clauses(Nss,I,K) :-
3697 value(max_no_of_clauses_to_optimize,MaxNoOfClauses),
3698 I > MaxNoOfClauses,
3699 !,
3700 ( member([],Nss) -> K = 0 ; K = I ).
3701
3702number_of_clauses([],K,K).
3703
3704number_of_clauses([Ns|Nss],I,K) :-
3705 length(Ns,J),
3706 I1 is I * J,
3707 number_of_clauses(Nss,I1,K).
3708
3709
3710size_of_clauses([Ns|Nss],S) :-
3711 !,
3712 size_of_clauses(Ns,S1),
3713 size_of_clauses(Nss,S2),
3714 S is S1 + S2.
3715
3716size_of_clauses([],0) :- !.
3717
3718size_of_clauses(_A,1).
3719
3720
3726
3727store_clauses([Ns|Nss],Stage,Mode,Phase) :-
3728 store_clause(Ns,Stage,Mode,Phase),
3729 store_clauses(Nss,Stage,Mode,Phase).
3730
3731
3732store_clause(Ns,Stage,Mode,Phase) :-
3733 sort(Ns,Cs),
3734 ( tautology(Cs), value(eliminate_tautologies,true)
3735 -> true
3736 ; ( Stage == domain
3737 -> incr(clause_count,_),
3738 ( Mode == transition, Phase == 1
3739 -> assertz(clause1(Cs))
3740 ; assertz(clause0(Cs)) )
3741 ; incr(query_clause_count,_),
3742 assertz(query_clause(Cs)) )).
3743
3744
3745tautology([N|_Ns]) :-
3746 N>0, !, fail.
3747tautology([N|Ns]) :-
3748 M is (0-N),
3749 ( ord_member(M,Ns)
3750 -> true
3751 ; tautology(Ns) ).
3752
3753member_of_each([N|Rs],[Ns|Nss]) :-
3754 member(N,Ns), member_of_each(Rs,Nss).
3755member_of_each([],[]).
3756
3757
3758member_of_each_append(R,[Ns|Nss]) :-
3759 member(N,Ns),
3760 member_of_each_append(Rs,Nss),
3761 append(N,Rs,R).
3762member_of_each_append([],[]).
3763
3764
3765negate_lits([[N|Ns]|Nss],[[C|Cs]|Css]) :-
3766 C is -N,
3767 negate_lits(Ns,Cs),
3768 negate_lits(Nss,Css).
3769
3770negate_lits([N|Ns],[C|Cs]) :-
3771 C is -N,
3772 negate_lits(Ns,Cs).
3773
3774negate_lits([],[]).
3775
3779
3782
3792
3793write_clauses_for_eq(Stage) :-
3794 write_clauses_for_eq([],Stage).
3795
3796write_clauses_for_eq(Steps,Stage) :-
3797 findall(L, (is_sort(simpleFluent(L)), L \== boolean,
3798 domain(simpleFluent(L),D), D \== []), Ls),
3799 3800 3801 ( Ls \== []
3802 -> write_clauses_for_eq(simpleFluent,Ls,Steps,Stage)
3803 ; true),
3804
3805 findall(L1, (is_sort(sdFluent(L1)), L1 \== boolean,
3806 domain(sdFluent(L1),D1), D1 \== []), Ls1),
3807 ( Ls1 \== []
3808 -> write_clauses_for_eq(sdFluent,Ls1,Steps,Stage)
3809 ; true),
3810
3811 findall(L2, (is_sort(action(L2)), L2 \== boolean,
3812 domain(action(L2),D2), D2 \== []), Ls2),
3813 ( Ls2 \== []
3814 -> write_clauses_for_eq(action,Ls2,Steps,Stage)
3815 ; true),
3816
3817 findall(L3, (is_sort(attribute(L3)),
3818 domain(attribute(L3),D3), D3 \== []), Ls3),
3819 ( Ls3 \== []
3820 -> write_clauses_for_eq(attribute,Ls3,Steps,Stage)
3821 ; true),
3822 findall(L4, (is_sort(rigid(L4)), L4 \== boolean,
3823 domain(rigid(L4),D4), D4 \== []), Ls4),
3824 3825 ( (Ls4 \== [], (Steps=[] ; member(0,Steps)))
3826 -> write_clauses_for_eq(rigid,Ls4,[0],Stage)
3827 ; true).
3828
3829write_clauses_for_eq(_Composite,[],_Steps,_Stage).
3830
3831write_clauses_for_eq(Composite,[L|Ls],Steps,Stage) :-
3832 write_exist_clauses_for_eq(Composite,L,Steps,Stage),
3833 write_uniq_clauses_for_eq(Composite,L,Steps,Stage),
3834 write_clauses_for_eq(Composite,Ls,Steps,Stage).
3835
3836
3837% TermTree3 = col(0)eq 1++col(0)eq 2++col(0)eq 3
3838
3839write_exist_clauses_for_eq(Composite,L,Steps,Stage) :-
3840 CompositeSort =.. [Composite,L],
3841
3842 % if Steps has any values (it will be [0] or [1] for transition mode,
3843 % or the list of all steps in history mode), choose each step from the list
3844 % in succession and add clauses for that step. If Steps is [], just use
3845 % variables instead of specific steps. For fluents, all time steps will
3846 % be processed. For actions, all times but the last will be processed,
3847 % and the clauses for actions at time N are added at the same time as the
3848 % clauses for fluents at time N+1 (for shifting purposes). Rigid constants
3849 % are processed only at time 0 since they are never shifted.
3850
3851 ( (Composite = simpleFluent; Composite = sdFluent)
3852 -> ( Steps == []
3853 -> Step = var(step,-1)
3854 ; member(Phase,Steps),
3855 Step = Phase )
3856 ; (Composite = action; Composite = attribute)
3857 -> ( Steps == []
3858 -> Step = var(astep,-1)
3859 ; member(Phase,Steps),
3860 Phase > 0,
3861 Step is Phase - 1 )
3862 ; Composite = rigid
3863 -> Step = 0 ),
3864
3865 ( Composite = attribute
3866 -> L2 = (L*)
3867 ; L2 = L),
3868
3869 Term = ([\/var(L2,-1) |
3870 (Step: var(CompositeSort,-1) eq var(L2,-1))]),
3871
3872 decode_macro(Term,TermTree),
3873 do_term_expansion(TermTree,TermTree11),
3874 remove_time_stamps(TermTree11,TermTree1), %temp %remove_time_for_rigid
3875
3876 find_free_variables(TermTree1,Vs),
3877 renaming_subst(Vs,Sub),
3878 subst_free(TermTree1,TermTree2,Sub),
3879 bind_vars(Sub),
3880
3881 negation_normal_form(TermTree2,TermTree3),
3882 write_clause2(TermTree3,Phase,Stage),
3883 fail.
3884
3885write_exist_clauses_for_eq(_Composite,_L,_Steps,_Stage).
3886
3887write_uniq_clauses_for_eq(Composite,L,Steps,Stage) :-
3888 value(mode,Mode),
3889 CompositeSort =.. [Composite,L],
3890
3891 % if Steps has any values (it will be [0] or [1] for transition mode,
3892 % or the list of all steps in history mode), choose each step from the list
3893 % in succession and add clauses for that step. If Steps is [], just use
3894 % variables instead of specific steps. For fluents, all time steps will
3895 % be processed. For actions, all times but the last will be processed,
3896 % and the clauses for actions at time N are added at the same time as the
3897 % clauses for fluents at time N+1 (for shifting purposes). Rigid constants
3898 % are processed only at time 0 since they are never shifted.
3899
3900 ( (Composite = simpleFluent; Composite = sdFluent)
3901 -> ( Steps == []
3902 -> domain(step,StepDom)
3903 ; StepDom = Steps ),
3904 member(Step,StepDom),
3905 Phase = Step
3906 ; (Composite = action; Composite = attribute)
3907 -> ( Steps == []
3908 -> domain(astep,StepDom),
3909 member(Step,StepDom),
3910 Phase = Step
3911 ; member(Phase,Steps),
3912 Phase > 0,
3913 Step is Phase - 1 )
3914 ; Composite = rigid
3915 -> Step = 0 ),
3916
3917 ( Composite = attribute
3918 -> L2 = (L*)
3919 ; L2 = L ),
3920
3921 domain(CompositeSort,CDom),
3922 domain(L2,LDom),
3923 length(LDom,Len),
3924
3925 ( Len < 5
3926 -> % if the domain of the fluent has fewer than 5 elements, it's more
3927 % economical to add -P ++ -Q for each pair of elements P and Q
3928
3929 member(Const,CDom),
3930 suffix([Val1|Vals],LDom),
3931 ( Composite == rigid
3932 -> find_atom_integer((Const eq Val1),Int1)
3933 ; find_atom_integer((Step: Const eq Val1),Int1) ),
3934 Neg1 is -Int1,
3935 member(Val2,Vals),
3936 ( Composite == rigid
3937 -> find_atom_integer((Const eq Val2),Int2)
3938 ; find_atom_integer((Step: Const eq Val2),Int2) ),
3939 Neg2 is -Int2,
3940 store_clause([Neg1,Neg2],Stage,Mode,Phase)
3941
3942 ; % if the domain has 5 or more elements, it's more economical to include
3943 % uniqueness clauses equivalent to
3944 %
3945 % V_0 <-> A_0
3946 % A_i -> -V_(i-1) for i > 0
3947 % V_i <-> V_(i-1) ++ A_i for i > 0
3948 %
3949 % where the V_i are the elements of the domain, and the A_i are new
3950 % auxiliary atoms
3951
3952 member(Const,CDom),
3953 value(atom_count,FirstA),
3954
3955 LDom = [FirstVal|RestDom],
3956 ( Composite == rigid
3957 -> find_atom_integer((Const eq FirstVal),FirstConstA)
3958 ; find_atom_integer((Step: Const eq FirstVal),FirstConstA) ),
3959 FirstConstN is -FirstConstA,
3960
3961 member(Val,RestDom),
3962 ( Composite == rigid
3963 -> find_atom_integer((Const eq Val),ConstA)
3964 ; find_atom_integer((Step: Const eq Val),ConstA) ),
3965 ConstN is -ConstA,
3966
3967 value(atom_count,LastA),
3968 LastN is -LastA,
3969 incr(atom_count,NewA),
3970 NewN is -NewA,
3971
3972 ( LastA == FirstA
3973 -> ( Clause = [FirstConstN,ConstN]
3974 ; Clause = [NewN,FirstConstA,ConstA]
3975 ; Clause = [NewA,FirstConstN]
3976 ; Clause = [NewA,ConstN] ),
3977 store_clause(Clause,Stage,Mode,Phase)
3978 ; ( Clause = [NewN,LastA,ConstA]
3979 ; Clause = [NewA,LastN]
3980 ; Clause = [NewA,ConstN]
3981 ; Clause = [LastN,ConstN] ),
3982 store_clause(Clause,Stage,Mode,Phase) )),
3983
3984/* decode_macro(Term,TermTree),
3985 do_term_expansion(TermTree,TermTree11),
3986 remove_time_stamps(TermTree11,TermTree1), %temp
3987
3988 find_free_variables(TermTree1,Vs),
3989 renaming_subst(Vs,Sub),
3990 subst_free(TermTree1,TermTree2,Sub),
3991 bind_vars(Sub),
3992
3993 negation_normal_form(TermTree2,TermTree3),
3994
3995 ( TermTree3 = false
3996 -> true
3997 ; write_clause2(TermTree3,Phase,Stage) ),
3998*/
3999
4000 fail.
4001
4002write_uniq_clauses_for_eq(_Composite,_L,_Steps,_Stage).
4003
4005
4006write_clause2(Term,Phase,Stage) :-
4007 write_clause2_aux(Term,Clause),
4008 value(mode,Mode),
4009 store_clause(Clause,Stage,Mode,Phase).
4010
4011write_clause2_aux(A++B,[I|Is]) :-
4012 ( A = -C
4013 -> atom_integer(C,I1),
4014 I is -I1
4015 ; atom_integer(A,I)),
4016 write_clause2_aux(B,Is).
4017
4018write_clause2_aux(A,[I]) :-
4019 ( A = -C
4020 -> atom_integer(C,I1),
4021 I is -I1
4022 ; atom_integer(A,I)).
4023
4025
4027find_atom_integer(A,N) :-
4028 atom_integer(A,N),
4029 !.
4030
4031lowercase([],[]).
4032lowercase([C|Cs],[L|Ls]) :-
4033 ( C >= 65, C =< 90 ->
4034 L is C + 32
4035 ; L = C ),
4036 lowercase(Cs,Ls).
4037lowercase(C1-C2,L1-L2) :-
4038 4039 4040 lowercase(C1,L1),
4041 lowercase(C2,L2).
4042lowercase(C,L) :-
4043 name(C,CName),
4044 lowercase(CName,LName),
4045 name(L,LName),
4046 !.
4047lowercase(C,C).
4048
4049
4053
4054set(solver,Value) :-
4055 !,
4056 lowercase(Value,Value2),
4057 4058 4059 ( value(num,NOI)
4060 -> true
4061 ; NOI = 1 ),
4062 ( member(Value2,[relsat,grasp,mchaff])
4063 -> NumValue = NOI
4064 ; member(Value2,[sato,sato_old,walksat])
4065 -> ( NOI == all
4066 -> format("~nNote: The current value of num is 'all', but for ",[]),
4067 format("~w, num must be a~npositive integer. num ",[Value2]),
4068 format("will be set to 1.~n",[]),
4069 NumValue = 1
4070 ; NumValue = NOI )
4071 ; member(Value2,[relsat_old,satz,satz-rand,zchaff])
4072 -> ( NOI == 1
4073 -> true
4074 ; format("~nNote: The current value of num is \'~w\', but ",[NOI]),
4075 format("~w cannot return multiple~nsolutions. num will ",[Value2]),
4076 format("be set to 1.~n",[]) ),
4077 NumValue = 1
4078 ; format("~nError: ~w is not a valid solver choice.~n",[Value]),
4079 format("Please see 'help(solver)' for a list of valid choices.~n",[]),
4080 fail ),
4081 iset(solver,Value2),
4082 ( value(num,NOI)
4083 -> 4084 4085 set(num,NumValue)
4086 ; true ).
4087
4088set(num,Value) :-
4089 4090 4091 4092 4093 value(solver,Solver),
4094 !,
4095 ( member(Solver,[relsat,grasp,mchaff])
4096 -> ( Value == all
4097 -> SetValue = Value
4098 ; integer(Value), Value > 0
4099 -> SetValue = Value
4100 ; format("~nError: The value of num must be 'all' or a positive ",[]),
4101 format("integer for solver ~w.~nDefaulting to 1.~n",[Solver]),
4102 SetValue = 1 )
4103 ; member(Solver,[sato,sato_old,walksat])
4104 -> ( ( \+ integer(Value) ; Value =< 0 )
4105 -> format("~nError: The value of num must be a positive ",[]),
4106 format("integer for solver ~w.~nDefaulting to 1.~n",[Solver]),
4107 SetValue = 1
4108 ; SetValue = Value,
4109 ( value(solver,walksat)
4110 -> format("~nWarning: walksat is stochastic and may report ",[]),
4111 format("that a satisfiable problem is~nunsatisfiable, or ",[]),
4112 format("may return fewer solutions than the number ",[]),
4113 format("requested, even~nwhen that many exist.~n",[])
4114 ; Value > 1
4115 -> format("~nWarning: ~w may return fewer than the ",[Solver]),
4116 format("requested number of solutions, even~nwhen that ",[]),
4117 format("many exist, but will always find at least one ",[]),
4118 format("solution if the problem~nis satisfiable.~n",[])
4119 ; true ))
4120 ; Value == 1
4121 -> SetValue = Value
4122 ; integer(Value)
4123 -> format("~nError: Solver ~w cannot return multiple ",[Solver]),
4124 format("interpretations. num will be~nset to 1.~n",[]),
4125 SetValue = 1
4126 ; format("~nError: num must be a positive integer or 'all'.",[]),
4127 format("Defaulting to 1.~n",[]),
4128 SetValue = 1 ),
4129 iset(num,SetValue),
4130 ( value(eliminate_tautologies,false), SetValue \= 1
4131 -> format("~nWarning: when 'num' is set for multiple interpretations ",[]),
4132 format("and~neliminate_tautologies is set to false, it is possible",[]),
4133 format(" CCalc may generate~nmultiple copies of some ",[]),
4134 format("interpretations.~n",[])
4135 ; true ).
4136
4139set(num,Value) :-
4140 !,
4141 ( Value == 1
4142 -> true
4143 ; format("~nWarning: Not all solvers are capable of returning multiple",[]),
4144 format(" solutions.~n",[]) ),
4145 iset(num,Value).
4146
4147set(dir,Value) :-
4148 4149 format_to_chars("~w",[Value],V),
4150 common_last(V,C),
4151 ( C == 47 4152 -> iset(dir,Value)
4153 ; format_to_atom(V2,"~w/",[Value]),
4154 iset(dir,V2) ).
4155
4156set(eliminate_tautologies,Value) :-
4157 member(Value,[off,no,n,false]),
4158 value(num,NOI),
4159 ( NOI \= 1
4160 -> format("~nWarning: when 'num' is set for multiple interpretations ",[]),
4161 format("and~neliminate_tautologies is set to false, it is possible",[]),
4162 format(" CCalc may generate~nmultiple copies of some ",[]),
4163 format("interpretations.~n",[])
4164 ; true ),
4165 iset(eliminate_tautologies,false).
4166
4167set(sorted,_) :-
4168 format("~nNote: the 'sorted' option has been disabled.~n",[]),
4169 !.
4170
4171set(Term,Value) :-
4172 ( Term = solver_opts(_),
4173 Value1 = Value
4174 ; member(Term,[timed,verbose,compact,optimize,eliminate_tautologies,file_io,
4175 debug])
4176 -> ( member(Value,[on,yes,y,true,t])
4177 -> Value1 = true
4178 ; member(Value,[off,no,n,false,f,[],nil])
4179 -> Value1 = false
4180 ; format("Error: value must be 'true' or 'false' for option \'~w\'.~n",
4181 [Term]),
4182 fail )
4183 ; format("~s~w~s~s~n",["Error: ", Term, " is not a valid option. Please ",
4184 "see \'help(parameters)\'."]),
4185 fail ),
4186 iset(Term,Value1).
4187
4190iset(Term,Value) :-
4191 retractall(value(Term,_)),
4192 assertz(value(Term,Value)).
4193
4194
4195incr(Term,Value) :-
4196 ( retract(value(Term,N))
4197 -> Value is N+1,
4198 assertz(value(Term,Value))
4199 ; Value = 1,
4200 assertz(value(Term,Value)) ).
4201
4202decr(Term,Value) :-
4203 ( retract(value(Term,N))
4204 -> Value is N-1,
4205 assertz(value(Term,Value))
4206 ; Value = 1,
4207 assertz(value(Term,Value)) ).
4208
4209show_values :-
4210 value(Var,Val),
4211 format("~n ~w = ~w",[Var,Val]),
4212 fail.
4213show_values.
4214
4218
4242
4248
4249call_sat(Out1,Out2,VarTable,CompactTime) :-
4250 call_sat(no_notify,Out1,Out2,VarTable,CompactTime).
4251
4252call_sat(_,_,_,_,_) :-
4253 ( clause([]) ; query_clause([]) ),
4254 !,
4255 write('Theory is unsatisfiable -- it contains the empty clause.'), nl,
4256 fail.
4257
4258call_sat(Notify,Out1,Out2,VarTable,[CompactTime,Lockfile]) :-
4259 common_statistics(_),
4260 4261 4262 ( value(file_io,true)
4263 -> In = 'ccsat.in',
4264 open(In,write,InStrm),
4265 write_input(Notify,InStrm),
4266 close(InStrm)
4267 ; make_pipe(In) ),
4268
4269 value(solver,Solver),
4270
4271 4272 4273 ( value(compact,true)
4274 -> call_compact(Notify,In,CompactAns,SolvIn,VarTable0,CompactTime,
4275 Lockfile)
4276 ; SolvIn = In ),
4277
4278 4279 4280 4281 4282 4283 ( nonvar(CompactAns)
4284 -> Out1 = CompactAns,
4285 open(VarTable0,read,VarTable)
4286 ; 4287
4288 4289 4290 4291 call_solver(Notify,Solver,SolvIn,SolvOut1,SolvOut2),
4292
4293 4294 4295 ( value(file_io,false)
4296 -> open(In,write,InStrm),
4297 ( value(compact,true)
4298 -> open(VarTable0,read,VarTable)
4299 ; true ),
4300
4301 4302 4303 4304 ( value(solver,mchaff)
4305 -> open(SolvOut2,read,Out2)
4306 ; true ),
4307
4308 4309 write_input(Notify,InStrm),
4310 close(InStrm),
4311 rm_pipe(In),
4312
4313 4314 4315 4316 ( value(compact,true),
4317 read_compact_ans(Notify,VarTable,CompactAns),
4318 nonvar(CompactAns),
4319 Out1 = CompactAns,
4320 rm_pipe(SolvOut1),
4321 ( nonvar(SolvOut2) -> rm_pipe(SolvOut2) ; true ),
4322 ( CompactAns == "UNSAT" -> rm_pipe(VarTable) ; true )
4323 ; Out1 = SolvOut1 )
4324
4325 ; 4326 4327 4328 4329 4330 Out1 = SolvOut1,
4331 ( value(compact,true)
4332 -> open(VarTable0,read,VarTable)
4333 ; true ),
4334 ( value(solver,mchaff)
4335 -> open(SolvOut2,read,Out2)
4336 ; value(solver,satz)
4337 -> Out2 = SolvOut2
4338 ; true ) ) ).
4339
4340call_compact(Notify,In,Ans,Result,VarTable,Time,Lockfile) :-
4341 determine_os(OS),
4342 value(ccalc_dir,CCDir),
4343 ( value(mode,transition)
4344 -> value(extended_atom_count,AC)
4345 ; value(atom_count,AC) ),
4346 Vars is AC + 1,
4347
4348 4349 4350 4351
4352 ( value(file_io,false)
4353 -> make_pipe(Result),
4354 make_pipe(VarTable),
4355 format_to_atom(CompactCall,
4356 "~wsolvers/~s/compact -l -v~d -f~w < ~w > ~w 2>> ~w",
4357 [CCDir,OS,Vars,VarTable,In,Result,VarTable]),
4358 ( Notify == notify, value(verbose,true)
4359 -> format("% Starting compact in background.~n",[])
4360 ; true ),
4361 flush_output,
4362 time_system(CompactCall,background,Time,Lockfile)
4363 ; Result = 'ccsat.compacted',
4364 VarTable = 'ccsat.compact.vartable',
4365 Stderr = 'ccsat.compact.info',
4366 format_to_atom(CompactCall,
4367 "bash -c \"~wsolvers/~s/compact -l -v~d -f~w < ~w > ~w 2> ~w\"",
4368 [CCDir,OS,Vars,VarTable,In,Result,Stderr]),
4369 ( Notify == notify
4370 -> format("% Compacting...",[]),
4371 flush_output
4372 ; true ),
4373 time_system(CompactCall,TC),
4374 ( Notify == notify
4375 -> format(" done.",[]),
4376 ( value(timed,true)
4377 -> format(" (~2f seconds)~n",[TC])
4378 ; nl )
4379 ; true ),
4380 open(Stderr,read,StderrStrm),
4381 read_compact_ans(Notify,StderrStrm,Ans),
4382 close(StderrStrm) ).
4383
4384
4385read_compact_ans(Notify,VarTableStrm,Ans) :-
4386 ( Notify = notify, value(verbose,true)
4387 -> format("% Reading output file from compact...",[]),
4388 flush_output
4389 ; true ),
4390
4391 4392 current_input(CurIn),
4393
4394 4395 4396 4397 4398 4399 4400 4401 4402 4403 4404 4405 4406 4407
4408 set_input(VarTableStrm),
4409 repeat,
4410 read_line(Line),
4411 ( Line == end_of_file
4412 -> fatal_error("Invalid output from compact.~n",[])
4413 ; ( Line == "Contradiction after unit resolution."
4414 ; prefix(Line,_,"Contradiction after failed lit test.") )
4415 -> Ans = "UNSAT"
4416 ; Line == "Satisfying interpretation found"
4417 -> Ans = "SAT"
4418 ; Line == "No interpretation found"
4419 -> true
4420 ; fail ),
4421 !,
4422 ( Notify = notify, value(verbose,true)
4423 -> format(" done.~n",[])
4424 ; true ),
4425 set_input(CurIn).
4426
4427
4428call_solver(Notify,Solver,In,Out1Stream,Out2) :-
4429 value(ccalc_dir,CCDir),
4430 value(num,NOI),
4431 determine_os(OS),
4432 ( value(solver_opts(Solver),SOpts)
4433 -> true
4434 ; SOpts = '' ),
4435
4436 4437 format_to_atom(FullName,"~wsolvers/~s/~w",[CCDir,OS,Solver]),
4438 ( common_file_exists(FullName)
4439 -> true
4440 ; fatal_error("Executable ~w is missing.",[FullName]) ),
4441
4442 4443 ( value(solver,satz)
4444 -> common_file_delete('satx.sol'),
4445 ( value(file_io,false)
4446 -> Out1 = 'satx.sol',
4447 system('mkfifo satx.sol')
4448 ; Out1 = 'ccsat.out' )
4449 ; value(file_io,false)
4450 -> make_pipe(Out1)
4451 ; Out1 = 'ccsat.out' ),
4452
4453 4454 ( Solver == relsat
4455 -> Name = "relsat 2.0",
4456 ( NOI == all
4457 -> NOpt = a
4458 ; NOpt = NOI ),
4459 format_to_atom(Call,"~w -#~w ~w ~w >~w",
4460 [FullName,NOpt,SOpts,In,Out1])
4461 ; Solver == relsat_old
4462 -> Name = "relsat 1.1.2",
4463 format_to_atom(Call,"~w ~w ~w >~w",[FullName,SOpts,In,Out1])
4464 ; Solver == sato_old
4465 -> Name = "sato 3.1.2",
4466 format_to_atom(Call,"~w -f -m~w ~w ~w >~w",
4467 [FullName,NOI,SOpts,In,Out1])
4468 ; Solver == sato
4469 -> Name = "sato 3.2",
4470 ( value(sato_v,true)
4471 -> VOpt = "-v"
4472 ; VOpt = "" ),
4473 format_to_atom(Call,"~w -f -m~w ~s ~w ~w >~w",
4474 [FullName,NOI,VOpt,SOpts,In,Out1])
4475 ; Solver == satz
4476 -> Name = "satz 215",
4477 format_to_atom(Call,"~w ~w ~w >~w",[FullName,SOpts,In,Out1]),
4478 ( value(file_io,true)
4479 -> Out2 = 'ccsat.out2'
4480 ; true )
4481 ; Solver == satz-rand
4482 -> Name = "satz-rand 4.9",
4483 format_to_atom(Call,"~w -out - ~w ~w >~w",[FullName,SOpts,In,Out1])
4484 ; Solver == grasp
4485 -> Name = "GRASP",
4486 ( NOI == all
4487 -> NOpt = a
4488 ; NOpt = NOI ),
4489 format_to_atom(Call,"~w +O +s~w ~w ~w >~w",
4490 [FullName,NOpt,SOpts,In,Out1])
4491 ; Solver == walksat
4492 -> Name = "WalkSAT 37",
4493 format_to_atom(Call,"cat ~w | ~w -sol -numsol ~w ~w >~w 2> /dev/null",
4494 [In,FullName,NOI,SOpts,Out1])
4495 ; Solver == zchaff
4496 -> Name = "ZChaff",
4497 format_to_atom(Call,"~w ~w ~w >~w",[FullName,SOpts,In,Out1])
4498 ; Solver == mchaff
4499 -> Name = "mChaff spelt3",
4500 ( value(file_io,true)
4501 -> Out2 = 'ccsat.out2',
4502 Opts = 'mchaff-opts.smj'
4503 ; make_pipe(Out2),
4504 common_tmpname(Opts) ),
4505 write_mchaff_opts(Opts,Out2),
4506 format_to_atom(Call,"~w ~w /dev/null ~w >~w 2>/dev/null",
4507 [FullName,In,Opts,Out1])
4508 ; fatal_error("~w is not a valid SAT solver.",[Solver]) ),
4509
4510 4511 4512 4513 4514 4515 4516 ( value(file_io,true)
4517 -> ( Notify == notify
4518 -> format("% Calling ~s... ",[Name]),
4519 flush_output,
4520 system_value(Call),
4521 format("done.~n",[])
4522 ; system_value(Call) ),
4523 ( value(solver,satz)
4524 -> system('mv satx.sol ccsat.out2')
4525 ; true )
4526 ; ( var(Opts)
4527 -> OptsCall = ''
4528 ; format_to_atom(OptsCall,"; rm ~w",[Opts]) ),
4529 format_to_atom(BkgdCall,"(~w ~w) &",[Call,OptsCall]),
4530 ( Notify == notify, value(verbose,true)
4531 -> format("% Starting ~s in background.~n",[Name]),
4532 flush_output
4533 ; true ),
4534 system(BkgdCall) ),
4535 open(Out1,read,Out1Stream).
4536
4537
4543
4544write_mchaff_opts(OptsFile,Out2Pipe) :-
4545 common_tmpname(OptsFile0),
4546 tell(OptsFile0),
4547 format(" solutionsFile = ~w~n",[Out2Pipe]),
4548 value(num,NOI),
4549 ( NOI == all
4550 -> NArg = 0
4551 ; NArg = NOI ),
4552 format(" limitSolutionsToN = ~d~n",[NArg]),
4553 told,
4554 value(ccalc_dir,CCDir),
4555 format_to_atom(Call,
4556 "cat ~wsolvers/mchaff-opts.smj.1 ~w ~wsolvers/mchaff-opts.smj.2 > ~w",
4557 [CCDir,OptsFile0,CCDir,OptsFile]),
4558 system(Call),
4559 common_file_delete(OptsFile0).
4560
4561write_input(Notify,Dest) :-
4562 ( value(mode,transition)
4563 -> value(extended_atom_count,AC),
4564 value(extended_clause_count,CC)
4565 ; value(atom_count,AC),
4566 value(clause_count,CC) ),
4567 value(query_clause_count,QC),
4568 TC is QC + CC,
4569 ( Notify == notify, value(verbose,true)
4570 -> format("% Writing input clauses...",[])
4571 ; true ),
4572 common_statistics(_),
4573 current_output(CurOut),
4574
4575 4576 4577 ( TC == 0
4578 -> 4579 4580 set_output(Dest),
4581 ( \+ value(compact,true), \+ value(sorted,true)
4582 -> format("p cnf ~d 1~n",[AC])
4583 ; true ) ,
4584 write_clause([1,-1])
4585
4586 4587 ; set_output(Dest),
4588 ( \+ value(compact,true), \+ value(sorted,true)
4589 -> format("p cnf ~d ~d~n",[AC,TC])
4590 ; true ),
4591 ( ( clause(C) ; query_clause(C) ),
4592 write_clause(C),
4593 fail
4594 ; true )),
4595
4596 common_statistics(T),
4597 set_output(CurOut),
4598
4599 ( Notify == notify, value(verbose,true)
4600 -> format(" done.",[]),
4601 ( value(timed,true)
4602 -> TS is T/1000,
4603 format(" (~2f seconds)~n",[TS])
4604 ; nl ),
4605 ( TC == 0
4606 -> ( (value(solver,Solver), Solver \== relsat)
4607 -> format("~nWarning: Since the theory has no clauses for SAT solver input,~n",[]),
4608 format(" ~w may not return correct solutions.~n",[Solver]),
4609 format(" Trying relsat instead...~n~n",[]),
4610 set(solver,relsat)
4611 ; true)
4612 ; true )
4613 ; true ).
4614
4615
4616check_compact_ans(Ans) :-
4617 read_line(Line),
4618 ( Line == end_of_file ->
4619 seen,
4620 safe_see('ccsat.out4'),
4621 read_line(Line2),
4622 ( Line2 == end_of_file ->
4623 Ans = "SAT"
4624 ; true ),
4625 seen
4626 ; ( Line == "Contradiction after unit resolution." ;
4627 prefix(Line,_,"Contradiction after failed lit test.") ) ->
4628 Ans = "UNSAT"
4629 ; check_compact_ans(Ans) ).
4630
4631
4635
4636output :- extract_info("SAT",M,_,_,_DMIKLESTODO1,_DMIKLESTODO2,_DMIKLESTODO3), show_models(M,sat).
4637
4639sat :-
4640 common_statistics(_),
4641 ( value(mode,transition)
4642 -> format("% Displaying possible states: ~n",[]),
4643 flush_output,
4644 shift_atoms_and_clauses(0)
4645 ; true ),
4646 retractall(query_clause(_)),
4647 iset(query_clause_count,0),
4648 call_sat(notify,Out1,Out2,VarTable,CompactTime),
4649 extract_info(Out1,Out2,VarTable,Ans,Models,TimeMsg,Other),
4650 !,
4651 ( Ans == "UNSAT"
4652 -> report_time(CompactTime,TimeMsg), seen, fail
4653 ; Ans == "SAT"
4654 -> report_time(CompactTime,TimeMsg),
4655 ( value(mode,transition)
4656 -> assertz(domain(step,[0])),
4657 show_models(Models,sat),
4658 retract(domain(step,_))
4659 ; show_models(Models,sat) )
4660 ; format("~n~s",[Other]), seen, !, fail ).
4661
4662%%% query_/0 prompts the user for facts.
4663(query) :-
4664 common_statistics(_),
4665 read_rules(FieldList),
4666% semituple_to_list(Fields,FieldList),
4667 ( member_check((label::Label),FieldList)
4668 -> ( atomic(Label)
4669 -> true
4670 ; fatal_error("Invalid label field (~w).",[Label]) )
4671 ; Label = 0 ),
4672
4673 ( member_check(((maxstep)::MaxStep),FieldList)
4674 -> do_term_expansion(MaxStep,MaxStep1),
4675 eval_expr(MaxStep1,MaxStep2),
4676 ( value(mode,history)
4677 -> nonfatal_error("maxstep is already declared by macro. ",[])
4678 ; ( ( integer(MaxStep2) ; (MaxStep2 = (T1..T2), T2>=T1) )
4679 -> true %iset(dynamic_detected,true)
4680 ; fatal_error("Invalid time field (~w).",[MaxStep]) ) )
4681 ; ( value(mode,history)
4682 -> macro((maxstep),_,MaxStep2)
4683 ; MaxStep2 = 0 ) ),
4684
4685 delete(FieldList, (label::Label), FieldList2),
4686 delete(FieldList2, ((maxstep)::MaxStep), Rules),
4687
4688 ( Label == 0
4689 -> value(query_counter,M),
4690 Label1 = M,
4691 M1 is M-1,
4692 iset(query_counter,M1)
4693 ; Label1 = Label ),
4694
4695 assertz(query_problem(Label1,MaxStep2,Rules)),
4696 query(Label1).
4697
4698
4699(nmquery) :-
4700 common_statistics(_),
4701 read_rules(FieldList),
4702% semituple_to_list(Fields,FieldList),
4703 ( member_check((label::Label),FieldList)
4704 -> ( atomic(Label)
4705 -> true
4706 ; fatal_error("Invalid label field (~w).",[Label]) )
4707 ; Label = 0 ),
4708
4709 ( member_check(((maxstep)::MaxStep),FieldList)
4710 -> do_term_expansion(MaxStep,MaxStep1),
4711 eval_expr(MaxStep1,MaxStep2),
4712 ( value(mode,history)
4713 -> nonfatal_error("maxstep is already declared by macro. ",[])
4714 ; ( ( integer(MaxStep2) ; (MaxStep2 = (T1..T2), T2>=T1) )
4715 -> true %iset(dynamic_detected,true)
4716 ; fatal_error("Invalid time field (~w).",[MaxStep]) ) )
4717 ; ( value(mode,history)
4718 -> macro((maxstep),_,MaxStep2)
4719 ; MaxStep2 = 0 ) ),
4720
4721 delete(FieldList, (label::Label), FieldList2),
4722 delete(FieldList2, ((maxstep)::MaxStep), Rules),
4723
4724 ( Label == 0
4725 -> value(query_counter,M),
4726 Label1 = M,
4727 M1 is M-1,
4728 iset(query_counter,M1)
4729 ; Label1 = Label ),
4730
4731 assertz(nmquery_problem(Label1,MaxStep2,Rules)),
4732 nmquery(Label1).
4733
4736
4737
4745
4746
4750
4751assert_extended_steps_in_domain(MaxStep) :-
4752 retractall(domain(step,_)),
4753 retractall(domain(astep,_)),
4754 expand_sequence(0,MaxStep,Steps),
4755 AMaxStep is MaxStep-1,
4756 expand_sequence(0,AMaxStep,Asteps),
4757 assertz(domain(step,Steps)),
4758 assertz(domain(astep,Asteps)).
4759
4760verify_invariant(TransLabel,TransAns) :-
4761 query(TransLabel,TransAns).
4762
4763verify_init(InitLabel,InitAns) :-
4764 query(InitLabel,InitAns).
4765
4766verify_goal(GoalLabel,GoalAns) :-
4767 query(GoalLabel,GoalAns).
4768
4769
4770query(A) :-
4771 A =.. [maxstep | [Label,MaxStep]],
4772 !,
4773 query(Label,MaxStep,_).
4774
4775
4777query(Label) :-
4778 atomic(Label),
4779 ( query_problem(Label,MaxStep,_Rules)
4780 -> true
4781 ; fatal_error("Invalid query label (~q).",[Label]) ),
4782 MaxStep=='any',
4783 !,
4784
4785 format("~n% Verifying that the problem is not solvable...~n~n",[]),
4786
4787 append_name(Label,'_trans',TransLabel),
4788 append_name(Label,'_init',InitLabel),
4789 append_name(Label,'_goal',GoalLabel),
4790
4791 format("~n% Verifying the given invariant...~n~n", []),
4792 verify_invariant(TransLabel,TransAns),
4793 ( TransAns == "UNSAT"
4794 -> format("~n% Verified the invariant. ~n~n",[])
4795 ; fatal_error("Wrong invariant. The above is a counterexample.~n~n",[]) ),
4796
4797 format("~n% Verifying that initial state satisfies the invariant...~n~n", []),
4798 verify_init(InitLabel,InitAns),
4799 ( InitAns == "SAT"
4800 -> format("~n% Initial state satisfies the invariant. ~n~n",[])
4801 ; fatal_error("Initial state does not satisfy the invariant.~n~n",[])),
4802
4803 format("~n% Verifying that every goal state does not satisfy the invariant...~n~n", []),
4804 verify_goal(GoalLabel,GoalAns),
4805 ( GoalAns == "UNSAT"
4806 -> format("% Every goal state does not satisfy the invariant. ~n~n",[])
4807 ; fatal_error("% There exists a goal state that satisfies the invariant. ~The above is a counterexample.n~n",[]) ),
4808
4809 format("~n% Verified that the problem is not solvable for any number of steps.~n~n",[]).
4810
4811
4812query(Label) :-
4813 value(solver,Solver),
4814 query(Label,_),
4815 iset(solver,Solver).
4816
4817
4818query(Fields) :- process_query(Fields,query), !.
4819
4820query(Label,Ans) :-
4821 atomic(Label),
4822% (value(mode,transition) ; value(mode,history)),
4823 !,
4824 ( query_problem(Label,MaxStep,Rules)
4825 -> true
4826 ; fatal_error("Invalid query label (~q).",[Label]) ),
4827
4828 ( MaxStep == -1
4829 -> fatal_error("maxstep is not specified. ",[])
4830 ; true),
4831
4832 ( value(mode,history)
4833 -> macro(maxstep,true,MaxStep),
4834 assert_extended_steps_in_domain(MaxStep),
4835 query_aux(MaxStep,Rules,Ans)
4836 ; ( (value(mode,transition); value(mode,basic))
4837 -> ( MaxStep = (T1..T2) % transition mode
4838 -> iterative_query(T1,T2,Rules)
4839 ; retractall(macro(maxstep,true,_)),
4840 assertz(macro(maxstep,true,MaxStep)),
4841 assert_extended_steps_in_domain(MaxStep),
4842 query_aux(MaxStep,Rules,Ans) ) ) ).
4843
4844iterative_query(T1,T2,Rules) :-
4845 ( (number(T2), T1<T2) ; T2 == 'infinity' ),
4846 !,
4847 retractall(macro(maxstep,true,_)),
4848 assertz(macro(maxstep,true,T1)),
4849 assert_extended_steps_in_domain(T1),
4850 query_aux(T1,Rules,Ans),
4851 ( Ans == "UNSAT"
4852 -> NewT1 is T1+1,
4853 iterative_query(NewT1,T2,Rules)
4854 ; true).
4855
4856iterative_query(T1,T1,Rules) :-
4857 number(T1), !,
4858 retractall(macro(maxstep,true,_)),
4859 assertz(macro(maxstep,true,T1)),
4860 assert_extended_steps_in_domain(T1),
4861 query_aux(T1,Rules,_).
4862
4863
4864%^ temporary disable
4865query(Label,MaxStep1,Ans) :-
4866 atomic(Label),
4867 (value(mode,transition) ; value(mode,history)),
4868 !,
4869 ( query_problem(Label,_MaxStep0,Rules)
4870 -> true
4871 ; fatal_error("Invalid query label (~q).",[Label]) ),
4872
4873 eval_expr(MaxStep1,MaxStep),
4874
4875 ( value(mode,history)
4876 -> fatal_error("Can't pass maxstep along with query in history mode. ~n",[])
4877 ; ( value(mode,transition)
4878 -> ( MaxStep = (T1..T2) % transition mode
4879 -> iterative_query(T1,T2,Rules)
4880 ; retractall(macro(maxstep,true,_)),
4881 assertz(macro(maxstep,true,MaxStep)),
4882 assert_extended_steps_in_domain(MaxStep),
4883 query_aux(MaxStep,Rules,Ans) ) ) ).
4884
4885query_aux(MaxStep,Rules,Ans) :-
4886 ( value(mode,transition)
4887 -> ( value(verbose,true)
4888 -> format("% Shifting atoms and clauses... ",[])
4889 ; true ),
4890 flush_output,
4891 common_statistics(_),
4892 shift_atoms_and_clauses(MaxStep),
4893 ( value(verbose,true)
4894 -> format("done.",[]),
4895 ( value(timed,true)
4896 -> common_statistics(ST),
4897 STS is ST/1000,
4898 format(" (~2f seconds)~n",[STS])
4899 ; nl )
4900 ; true ),
4901 value(extended_atom_count,EAC),
4902 value(extended_clause_count,ECC),
4903 format("% After shifting: ~d atoms",[EAC]),
4904 ( value(aux_atom_count,AAC), AAC > 0
4905 -> format(" (including new atoms)",[])
4906 ; true ),
4907 format(", ~d clauses~n",[ECC]),
4908 flush_output
4909 ; true ),
4910
4911 4912 4913 value(domain_atom_count,DAC),
4914 iset(atom_count,DAC),
4915
4916 do_term_expansion(Rules,Rules1), 4917 4918 4919 4920 4921 replace_comma_with_and(Rules1,Rules11),
4922
4923 4924 4925 4926 4927 4928 4929 4930 4931 4932
4933 findall( R2,
4934 ( member(R,Rules11),
4935 ( decode_macro(R,Rules2),
4936 decode_nested_constants_in_fact(Rules2,Rules3),
4937 postprocessing_before_binding(Rules3,Rules4),
4938 postprocessing_after_binding(Rules4,Rules6),
4939 universal_closure(Rules6,Rules7),
4940 clausify_wff(Rules7,R2)
4941 -> true )),
4942 RCs0 ),
4943 findall( R, ( member(RC,RCs0), member(R,RC) ), RCs),
4944
4945 length(RCs,QCC),
4946 iset(query_clause_count,QCC),
4947 retractall(query_clause(_)),
4948 ( member(RC,RCs),
4949 assertz(query_clause(RC)),
4950 fail
4951 ; true ),
4952
4953 call_sat(notify,Out1,Out2,VarTable,CompactTime),
4954 extract_info(Out1,Out2,VarTable,Ans,Models,TimeMsg,Other),
4955 !,
4956 ( Ans == "UNSAT"
4957 -> report_time(CompactTime,TimeMsg),
4958 seen,
4959 ( value(mode,transition)
4960 -> macro(maxstep,true,MaxStep),
4961 format("No solution with maxstep ~w.~n~n",[MaxStep])
4962 ; ! ) 4963 ; Ans == "SAT"
4964 -> report_time(CompactTime,TimeMsg),
4965 show_models(Models,query)
4966 ; format("~n~s",[Other]), seen, !, fail ).
4967
4968
4972
4973nmquery(A) :-
4974 A =.. [maxstep | [Label,MaxStep]],
4975 !,
4976 value(solver,Solver),
4977 nmquery(Label,MaxStep),
4978 iset(solver,Solver).
4979
4980%^ here - iset(mode,basic) and don't shift clausex
4981nmquery(Label) :-
4982 atomic(Label),
4983 value(solver,Solver),
4984 value(mode,M),
4985 (M == transition ; M == basic),
4986 !,
4987 iset(mode,history), % nmquery in transition mode is temporarily set to
4988 % history mode
4989
4990 ( nmquery_problem(Label,MaxStep0,Rules)
4991 -> true
4992 ; iset(mode,M),
4993 fatal_error("Invalid nmquery label (~q).",[Label]) ),
4994
4995 do_term_expansion(Rules,Rules3),
4996 replace_comma_with_and(Rules3,Rules2),
4997
4998 retract(nmquery_problem(Label,MaxStep0,Rules)),
4999 assertz(nmquery_problem(Label,MaxStep0,Rules2)),
5000
5001 ( (MaxStep0) = (T1..T2)
5002 -> expand_sequence(T1,T2,MaxSteps),
5003 member(MaxStep,MaxSteps)
5004 ; MaxStep = MaxStep0 ),
5005
5006 % temp?
5007 retractall(macro(maxstep,true,_)),
5008 assertz(macro(maxstep,true,MaxStep)),
5009
5010 retractall(domain(_,_)),
5011 retractall(domain_schema(step,_)),
5012 retractall(domain_schema(astep,_)),
5013 expand_sequence(0,MaxStep,Ms),
5014 assertz(domain_schema(step,Ms)),
5015 M1 is MaxStep-1,
5016 expand_sequence(0,M1,Ms1),
5017 assertz(domain_schema(astep,Ms1)),
5018 instantiate_sorts, % cut
5019
5020 iset(mode,M), % get back to the original mode
5021 (M == transition
5022 ->
5023 ( value(verbose,true)
5024 -> format("% Shifting atoms and clauses... ",[])
5025 ; true ),
5026 flush_output,
5027 common_statistics(_),
5028 shift_atoms_and_clauses(MaxStep),
5029 ( value(verbose,true)
5030 -> format("done.",[]),
5031 ( value(timed,true)
5032 -> common_statistics(ST),
5033 STS is ST/1000,
5034 format(" (~2f seconds)~n",[STS])
5035 ; nl )
5036 ; true ),
5037 value(extended_atom_count,EAC),
5038 value(extended_clause_count,ECC),
5039 format("% After shifting: ~d atoms",[EAC]),
5040 ( value(aux_atom_count,AAC), AAC > 0
5041 -> format(" (including new atoms)",[])
5042 ; true ),
5043 format(", ~d clauses~n",[ECC]),
5044 flush_output
5045 ; true ),
5046
5047 nmquery_aux(Rules2),
5048 % temp?
5049 retractall(macro(maxstep,true,_)),
5050 iset(solver,Solver).
5051
5052nmquery(Label) :-
5053 atomic(Label),
5054 value(mode,history),
5055 !,
5056 value(solver,Solver),
5057 ( nmquery_problem(Label,_MaxStep,Rules)
5058 -> true
5059 ; fatal_error("Invalid nmquery label (~q).",[Label]) ),
5060 nmquery_aux(Rules),
5061 iset(solver,Solver).
5062
5067
5068nmquery(Fields) :- process_query(Fields,nmquery).
5069
5070nmquery(Label,MaxStep1) :-
5071 atomic(Label),
5072 value(mode,transition),
5073 !,
5074 value(solver,Solver),
5075 retractall(macro(maxstep,true,_)),
5076
5077 iset(mode,history), % nmquery in transition mode is temporarily set to
5078 % history mode
5079
5080 ( nmquery_problem(Label,MaxStep0,Rules)
5081 -> true
5082 ; iset(mode,transition),
5083 fatal_error("Invalid nmquery label (~q).",[Label]) ),
5084
5085 eval_expr(MaxStep1,MaxStep),
5086
5087 do_term_expansion(Rules,Rules2),
5088 retract(nmquery_problem(Label,MaxStep0,Rules)),
5089 assertz(nmquery_problem(Label,MaxStep,Rules2)), % overwrite MaxStep
5090
5091 ( MaxStep = (T1..T2)
5092 -> expand_sequence(T1,T2,Steps),
5093 member(CurMaxStep,Steps)
5094 ; CurMaxStep = MaxStep ),
5095
5096 % temp?
5097 retractall(macro(maxstep,true,_)),
5098 assertz(macro(maxstep,true,CurMaxStep)),
5099
5100 retractall(domain(_,_)),
5101 retractall(domain_schema(step,_)),
5102 retractall(domain_schema(astep,_)),
5103 expand_sequence(0,CurMaxStep,Ms),
5104 assertz(domain_schema(step,Ms)),
5105 M1 is CurMaxStep-1,
5106 expand_sequence(0,M1,Ms1),
5107 assertz(domain_schema(astep,Ms1)),
5108 instantiate_sorts, % cut
5109
5110 iset(mode,transition), % get back to transition mode
5111
5112 common_statistics(_),
5113 ( value(verbose,true)
5114 -> format("% Shifting atoms and clauses... ",[])
5115 ; true ),
5116 flush_output,
5117 common_statistics(_),
5118 shift_atoms_and_clauses(CurMaxStep),
5119 ( value(verbose,true)
5120 -> format("done.",[]),
5121 ( value(timed,true)
5122 -> common_statistics(ST),
5123 STS is ST/1000,
5124 format(" (~2f seconds)~n",[STS])
5125 ; nl )
5126 ; true ),
5127 value(extended_atom_count,EAC),
5128 value(extended_clause_count,ECC),
5129 format("% After shifting: ~d atoms",[EAC]),
5130 ( value(aux_atom_count,AAC), AAC > 0
5131 -> format(" (including new atoms)",[])
5132 ; true ),
5133 format(", ~d clauses~n",[ECC]),
5134 flush_output,
5135
5136 nmquery_aux(Rules2),
5137 % temp?
5138 retractall(macro(maxstep,true,_)),
5139 set(solver,Solver).
5140
5141nmquery(Label,_MaxStep) :-
5142 atomic(Label),
5143 value(mode,history),
5144 !,
5145 fatal_error("Can't pass maxstep along with query in history mode. ~n",[]).
5146
5147%nmquery(Label,_) :-
5148% atomic(Label),
5149% value(mode,basic),
5150% fatal_error("Use sat instead of nmquery under basic mode. ",[]).
5151
5152nmquery_aux(Rules) :-
5153 retractall(query_rule(_)),
5154 retractall(query_rule_schema(_)),
5155 retractall(query_rule_body(_,_)),
5156 retractall((_H<-_B)),
5157
5158 % The last query executed might have introduced auxiliary atoms, so
5159 % reset atom_count to its original value to eliminate these
5160 value(domain_atom_count,DAC),
5161 iset(atom_count,DAC),
5162
5163 insert_query_rules(Rules),
5164
5165 process_query_rule_schemas,
5166
5167 retractall(query_clause(_)), % why here?
5168 generate_completion_clauses(query), !, % red cut
5169
5170 call_sat(notify,Out1,Out2,VarTable,CompactTime),
5171 extract_info(Out1,Out2,VarTable,Ans,Models,TimeMsg,Other),
5172 !,
5173 ( Ans == "UNSAT"
5174 -> report_time(CompactTime,TimeMsg),
5175 seen,
5176 ( value(mode,transition)
5177 -> macro(maxstep,true,MaxStep),
5178 format("No solution with maxstep ~w.~n~n",[MaxStep])
5179 ; ! ),
5180 fail
5181 ; Ans == "SAT"
5182 -> report_time(CompactTime,TimeMsg),
5183 show_models(Models,query)
5184 ; format("~n~s~n",[Other]), seen, !, fail ).
5185
5186
5187
5202
("UNSAT",_,_,"UNSAT",_,"Contradiction found during compaction.",_).
5204
5205extract_info("SAT",_,VT,"SAT",Models,"Solution found during compaction.",_) :-
5206 current_input(CurIn),
5207 set_input(VT),
5208 get_renamed_vars(Vars),
5209 ( value(file_io,false) -> rm_pipe(VT) ; close(VT) ),
5210 set_input(CurIn),
5211 rebuild_models([[]],Vars,Models).
5212
5213extract_info(Out1,Out2,VarTable,Ans,Models,TimeMsg,Other) :-
5214 ( value(verbose,true)
5215 -> format("% Reading output file(s) from SAT solver...",[]),
5216 flush_output
5217 ; true ),
5218 current_input(CurIn),
5219 ( value(compact,true)
5220 -> set_input(VarTable),
5221 get_renamed_vars(Vars),
5222 ( value(file_io,false) -> rm_pipe(VarTable) ; close(VarTable) )
5223 ; true ),
5224 set_input(Out1),
5225 value(solver,Solver),
5226 extract_info_aux(Solver,Out2,Ans,Models0,TimeMsg,Other),
5227 ( ( Ans \= "SAT", Ans \= "UNSAT" )
5228 -> cleanup_after_extract(Out1,Out2),
5229 fatal_error("Cannot read SAT solver output files.",[])
5230 ; true ),
5231 ( value(verbose,true)
5232 -> format(" done.~n",[]),
5233 flush_output
5234 ; true ),
5235 set_input(CurIn),
5236 ( Ans == "SAT", value(compact,true)
5237 -> rebuild_models(Models0,Vars,Models)
5238 ; Models = Models0 ),
5239 cleanup_after_extract(Out1,Out2).
5240
5241
(Out1,Out2) :-
5243 5244 ( value(file_io,false)
5245 -> rm_pipe(Out1),
5246 ( nonvar(Out2) -> rm_pipe(Out2) ; true )
5247 ; close(Out1) ),
5248
5249 5250 common_file_delete(timetable),
5251 common_file_delete(record).
5252
5253
(sato,_,Ans,Models,TimeMsg,Other) :-
5255 !,
5256 read_sato_answer(Ans),
5257 ( Ans = "UNSAT"
5258 -> read_sato_time(TimeMsg)
5259 ; Ans = "SAT"
5260 -> read_sato_models(Models),
5261 read_sato_time(TimeMsg)
5262 ; Other = Ans ).
5263
5264extract_info_aux(sato(_),_,Ans,Models,TimeMsg,Other) :-
5265 !,
5266 extract_info_aux(sato,_,Ans,Models,TimeMsg,Other).
5267
5268extract_info_aux(sato_old,_,Ans,Models,TimeMsg,Other) :-
5269 !,
5270 read_sato_old_answer(Ans),
5271 ( Ans == "UNSAT"
5272 -> read_sato_time(TimeMsg)
5273 ; Ans == "SAT"
5274 -> read_sato_old_models(Models),
5275 read_sato_time(TimeMsg)
5276 ; Other = Ans ).
5277
5278extract_info_aux(sato_old(_),_,Ans,Models,TimeMsg,Other) :-
5279 !,
5280 extract_info_aux(sato_old,_,Ans,Models,TimeMsg,Other).
5281
5282extract_info_aux(relsat,_,Ans,Models,TimeMsg,Other) :-
5283 !,
5284 read_relsat_lines(Ans,Models,PrepTime,SolveTime,Other,_),
5285 get_number(PrepTime,PrepNum,_),
5286 get_number(SolveTime,SolveNum,_),
5287 TotalNum is PrepNum + SolveNum,
5288 format_to_charlist(TotalTime,"~d",[TotalNum]),
5289 ccalc_format_time(TotalTime,PrepTime,SolveTime,TimeMsg).
5290
5291extract_info_aux(relsat_old,_,Ans,[Model],TimeMsg,Other) :-
5292 !,
5293 read_relsat_old_prep_time(PrepTime),
5294 read_relsat_old_answer(Ans),
5295 ( Ans == "SAT"
5296 -> read_relsat_old_model(Model)
5297 ; Ans == "UNSAT"
5298 -> true
5299 ; Other = Ans ),
5300 read_relsat_old_solve_time(SolveTime),
5301 get_number(PrepTime,PrepNum,_),
5302 get_number(SolveTime,SolveNum,_),
5303 TotalNum is PrepNum + SolveNum,
5304 format_to_charlist(TotalTime,"~d",[TotalNum]),
5305 ccalc_format_time(TotalTime,PrepTime,SolveTime,TimeMsg).
5306
5307extract_info_aux(relsat_old(_),_,Ans,[Model],TimeMsg,Other) :-
5308 !,
5309 extract_info_aux(relsat_old,_,Ans,[Model],TimeMsg,Other).
5310
5311extract_info_aux(satz,Out2,Ans,[Model],TimeMsg,Other) :-
5312 !,
5313 read_line(Line),
5314 ( Line == end_of_file
5315 -> ( var(Ans) -> Ans = "No solution was found." ; true ),
5316 ( var(TimeMsg) -> TimeMsg = "Solution time not reported." ; true ),
5317 ( var(Model) -> Model = [] ; true )
5318 ; prefix(Line,"****the instance is satisfiable *****",_)
5319 -> Ans = "SAT",
5320 ( nonvar(Out2)
5321 -> current_input(CurIn),
5322 open(Out2,read,Out2S),
5323 set_input(Out2S),
5324 extract_info_aux(satz,_,_,[Model],_,_),
5325 close(Out2S),
5326 set_input(CurIn)
5327 ; true ),
5328 ( ( var(Model) ; var(TimeMsg) )
5329 -> extract_info_aux(satz,Out2,Ans,[Model],TimeMsg,Other)
5330 ; true )
5331 ; prefix(Line,"****the instance is unsatisfiable *****",_)
5332 -> Ans = "UNSAT",
5333 ( var(TimeMsg)
5334 -> extract_info_aux(satz,Out2,Ans,[Model],TimeMsg,Other)
5335 ; true )
5336 ; prefix(Line,"Program terminated in ",RestLine)
5337 -> get_until(RestLine," ",TimeStr,_),
5338 append("Solution time: ",TimeStr,TimeStr2),
5339 append(TimeStr2," seconds.",TimeMsg),
5340 ( ( var(Ans) ; Ans = "SAT", var(Model) )
5341 -> extract_info_aux(satz,Out2,Ans,[Model],TimeMsg,Other)
5342 ; true )
5343 ; get_positive_numbers(Line,Model)
5344 -> ( ( var(Ans) ; var(TimeMsg) )
5345 -> extract_info_aux(satz,Out2,Ans,[Model],TimeMsg,Other)
5346 ; true )
5347 ; extract_info_aux(satz,Out2,Ans,[Model],TimeMsg,Other) ).
5348
5349extract_info_aux(satz-rand,_,Ans,[Model],TimeMsg,Other) :-
5350 !,
5351 read_satz_rand_answer(Ans,Model),
5352 ( Ans == "UNSAT" ; Ans == "SAT" ; Other = Ans ), !,
5353 read_satz_rand_time(TimeMsg).
5354
5355extract_info_aux(grasp,_,Ans,Models,TimeMsg,Other) :-
5356 !,
5357 read_grasp_info(Ans,Models,PrepTime,SolveTime,TotalTime,Msg),
5358 ccalc_format_time(TotalTime,PrepTime,SolveTime,TimeMsg0),
5359 ( var(Msg)
5360 -> TimeMsg = TimeMsg0
5361 ; format_to_charlist(TimeMsg1,"~nResources exceeded... search aborted.",[]),
5362 append(TimeMsg0,TimeMsg1,TimeMsg) ),
5363 ( Ans \== "SAT", Ans \== "UNSAT"
5364 -> Other = Ans
5365 ; true ).
5366
5367extract_info_aux(walksat,_,Ans,Models,TimeMsg,Other) :-
5368 !,
5369 read_walksat_preamble,
5370 read_walksat_preamble,
5371 read_walksat_models(Models),
5372 read_walksat_time(TimeMsg),
5373 read_walksat_answer(Ans),
5374 ( Ans \== "SAT", Ans \== "UNSAT"
5375 -> Other = Ans
5376 ; true ).
5377
5378extract_info_aux(zchaff,_,Ans,[Model],TimeMsg,Other) :-
5379 !,
5380 read_zchaff_answer(Ans),
5381 ( Ans == "SAT"
5382 -> read_zchaff_model(Model)
5383 ; Ans == "UNSAT"
5384 -> true
5385 ; Other = Ans ),
5386 read_zchaff_time(TimeMsg).
5387
5388extract_info_aux(mchaff,Out2,Ans,Models,TimeMsg,Other) :-
5389 !,
5390 current_input(Out1),
5391 set_input(Out2),
5392 read_mchaff_models(Models),
5393 set_input(Out1),
5394 read_mchaff_answer(Ans0),
5395 read_mchaff_time(TimeMsg),
5396 ( Ans0 == "UNSAT", Models == [] ->
5397 5398 5399 Ans = "UNSAT"
5400 ; ( Ans0 == "SAT" ; Ans0 == "UNSAT" ) ->
5401 5402 5403 5404 Ans = "SAT"
5405 ; Ans = Ans0,
5406 Other = Ans0 ).
5407
5408extract_info_aux(_,_,_,_,_,_) :-
5409 fatal_error("Unknown sat solver!",[]).
5410
5411
5412read_sato_answer(Ans) :-
5413 read_line(Line),
5414 ( Line = end_of_file
5415 -> Ans = "No solution was found."
5416 ; Line = "The clause set is unsatisfiable."
5417 -> Ans = "UNSAT"
5418 ; Line = "Model #1: (indices of true atoms)"
5419 -> Ans = "SAT"
5421 ; Line = "Warning: There is only one input clause. sato ignores this trivial case. "
5422 -> Ans = Line
5423 ; read_sato_answer(Ans) )
5423.
5424
5425
5426read_sato_models([Model|Rest]) :-
5427 read_line(_),
5428 read_line(NextLine),
5429 get_positive_numbers(NextLine,Model),
5430 read_line(_),
5431 read_line(NextLine1),
5432 ( prefix(NextLine1,"Model",_)
5433 -> read_sato_models(Rest)
5434 ; Rest = []).
5435
5436
5437read_sato_old_answer(Ans) :-
5438 read_line(Line),
5439 ( Line = end_of_file
5440 -> Ans = "No solution was found."
5441 ; Line = "UNSAT"
5442 -> Ans = Line
5443 ; Line = "SAT"
5444 -> Ans = Line
5446 ; Line = "Warning: There is only one input clause. sato ignores this trivial case. "
5447 -> Ans = Line
5448 ; read_sato_old_answer(Ans) )
5448.
5449
5450
5451read_sato_old_models([Model|Rest]) :-
5452 read_line(NextLine),
5453 get_positive_numbers(NextLine,Model),
5454 read_line(_),
5455 read_line(NextLine1),
5456 (NextLine1 = "SAT"
5457 -> read_sato_old_models(Rest)
5458 ; Rest = []).
5459
5460
5461read_sato_time(TimeMsg) :-
5462 read_line(Line),
5463 ( Line == end_of_file ->
5464 TimeMsg = "Solution time: unknown"
5465 ; prefix(Line,"run time (seconds)",TotalStr) ->
5466 read_line(Line2),
5467 prefix(Line2," build time",PrepStr),
5468 read_line(Line3),
5469 prefix(Line3," search time",SolveStr),
5470 ccalc_format_time(TotalStr,PrepStr,SolveStr,TimeMsg)
5471 ; read_sato_time(TimeMsg) ).
5472
5473read_satz_rand_time(TimeMsg) :-
5474 read_line(Line),
5475 ( Line == end_of_file ->
5476 TimeMsg = "Solution time: unknown."
5477 ; prefix(Line,"Program terminated in ",RestLine) ->
5478 get_until(RestLine," ",TimeStr,_),
5479 append("Solution time: ",TimeStr,TimeStr2),
5480 append(TimeStr2," seconds.",TimeMsg)
5481 ; read_satz_rand_time(TimeMsg) ).
5482
5483
5484read_satz_rand_answer(Ans,Model) :-
5485 read_line(Line),
5486 ( Line == end_of_file
5487 -> Ans = "No solution was found."
5488 ; prefix(Line," trial",_)
5489 -> read_line(_),
5490 read_line(ModelLine),
5491 read_satz_rand_answer(Ans,_),
5492 ( Ans == "SAT"
5493 -> get_positive_numbers(ModelLine,Model)
5494 ; true )
5495 ; prefix(Line,"****the instance is satisfiable *****",_)
5496 -> Ans = "SAT"
5497 ; prefix(Line,"****the instance is unsatisfiable *****",_)
5498 -> Ans = "UNSAT"
5499 ; read_satz_rand_answer(Ans,Model) ).
5500
5504
5505read_relsat_lines(Ans,Models,PrepTime,SolveTime,Other,Time) :-
5506 read_line(Line),
5507 ( Line == "c Processing phase stats: " ->
5508 5509 read_relsat_lines(Ans,Models,_,SolveTime,Other,PrepTime)
5510 ; Line == "c Solution phase stats: " ->
5511 5512 read_relsat_lines(Ans,Models,PrepTime,_,Other,SolveTime),
5513 5514 5515 Time = "0"
5516 ; ( prefix(Line,"c Seconds elapsed (real time): ",TimeStr)
5517 ; prefix(Line,"c Seconds Elapsed (real time) : ",TimeStr) ) ->
5518 5519 5520 5521 get_until(TimeStr," ",Time,_),
5522 read_relsat_lines(Ans,Models,PrepTime,SolveTime,Other,_)
5523 ; prefix(Line,"Solution",_) ->
5524 5525 between(Line,_SolNum,ModelStr,": "),
5526 get_positive_numbers(ModelStr,Model),
5527 5528 5529 read_relsat_lines(Ans,RestModels,PrepTime,SolveTime,Other,Time),
5530 5531 5532 5533 5534 5535 Models = [Model|RestModels]
5536 ; Line == "SAT" ->
5537 Ans = Line,
5538 5539 5540 read_relsat_lines(_,Models,PrepTime,SolveTime,_,Time)
5541 ; Line == "UNSAT" ->
5542 Ans = Line,
5543 5544 5545 read_relsat_lines(_,_,PrepTime,SolveTime,_,Time)
5546 ; Line == end_of_file ->
5547 5548 5549 5550 5551 Models = [],
5552 Other = "No solution was found.",
5553 PrepTime = "0",
5554 SolveTime = "0",
5555 Time = "0"
5556 ; read_relsat_lines(Ans,Models,PrepTime,SolveTime,Other,Time) ).
5557
5558
5559read_relsat_old_prep_time(PrepTime) :-
5560 read_line(Line),
5561 ( Line = end_of_file ->
5562 PrepTime = "0"
5563 ; prefix(Line,"c Preprocessing instance:",Rem) ->
5564 between(Rem,"in "," seconds",PrepTime)
5565 ; read_relsat_old_prep_time(PrepTime) ).
5566
5567
5568read_relsat_old_answer(Ans) :-
5569 read_line(Line),
5570 ( Line == "UNSAT" ->
5571 Ans = Line
5572 ; Line == "SAT" ->
5573 Ans = Line
5574 ; Line == end_of_line ->
5575 Ans = "No solution was found."
5576 ; read_relsat_old_answer(Ans) ).
5577
5578
5579read_relsat_old_model(Model) :-
5580 read_line(Line),
5581 get_positive_numbers(Line,Model).
5582
5583
5584read_relsat_old_solve_time(SolveTime) :-
5585 read_line(Line),
5586 ( Line == end_of_file ->
5587 SolveTime = "0"
5588 ; prefix(Line,"Seconds Elapsed (real time) : ",TimeString) ->
5589 get_until(TimeString," ",SolveTime,_)
5590 ; read_relsat_old_solve_time(SolveTime) ).
5591
5592read_grasp_info(Ans,Models,PrepTime,SolveTime,TotalTime,Msg) :-
5593 read_line(Line0),
5594 ( Line0 == end_of_file ->
5595 Ans = "No solution was found.",
5596 Models = [],
5597 PrepTime = "unknown",
5598 SolveTime = "unknown",
5599 TotalTime = "unknown"
5600 ; drop_spaces(Line0,Line),
5601 ( prefix(Line,"Done creating structures. Elapsed time: ",PrepTime) ->
5602 read_grasp_info(Ans,Models,_,SolveTime,TotalTime,Msg)
5603 ; Line == "GRASP Information: Computed solution" ->
5604 read_line(_),
5605 read_line(_),
5606 read_line(ModelLine),
5607 read_grasp_info(_,RestModels,_,SolveTime,TotalTime,Msg),
5608 get_numbers(ModelLine,Lits),
5609 read_grasp_models(RestModels,Lits,Models),
5610 Ans = "SAT"
5611 ; prefix(Line,"Done searching.... RESOURCES EXCEEDED. Elapsed time: ",
5612 SolveTime) ->
5613 Msg = "Resources exceeded... search aborted.",
5614 read_grasp_info(_,Models,PrepTime,_,TotalTime,_)
5615 ; prefix(Line,
5616 "Done searching.... SATISFIABLE INSTANCE. Elapsed time: ",
5617 SolveTime) ->
5618 Ans = "SAT",
5619 read_grasp_info(_,Models,PrepTime,_,TotalTime,Msg)
5620 ; prefix(Line,
5621 "Done searching.... UNSATISFIABLE INSTANCE. Elapsed time: ",
5622 SolveTime) ->
5623 Ans = "UNSAT",
5624 read_grasp_info(_,Models,PrepTime,_,TotalTime,Msg)
5625 ; prefix(Line,"Terminating GRASP. Total time: ",TotalTime) ->
5626 read_grasp_info(Ans,Models,PrepTime,SolveTime,_,Msg)
5627 ; read_grasp_info(Ans,Models,PrepTime,SolveTime,TotalTime,Msg) ) ).
5628
5629
5630read_grasp_models(InModels,Lits,OutModels) :-
5631 value(num,N),
5632 5633 iset(num_models,N),
5634 findall( M,
5635 ( read_grasp_models_aux(Lits,1,M),
5636 \+ member(M,InModels),
5637 ( value(num_models,all)
5638 -> true
5639 ; decr(num_models,_) )),
5640 LineModels ),
5641 append(InModels,LineModels,OutModels).
5642
5643read_grasp_models_aux([],Num,Model) :-
5644 5645 5646 5647 5648 5649 5650 \+ value(num_models,0),
5651 ( value(extended_atom_count,AC) -> true ; value(atom_count,AC) ),
5652 ( Num > AC
5653 -> Model = []
5654 ; NextNum is Num + 1,
5655 read_grasp_models_aux([],NextNum,RestModel),
5656 ( Model = RestModel
5657 ; \+ value(num_models,0),
5658 Model = [Num|RestModel] )).
5659
5660read_grasp_models_aux([L|Lits],Num,Model) :-
5661 5662 5663 5664 5665 \+ value(num_models,0),
5666 NextNum is Num + 1,
5667 ( L = Num
5668 -> read_grasp_models_aux(Lits,NextNum,RestModel),
5669 Model = [Num|RestModel]
5670 ; L is -Num
5671 -> read_grasp_models_aux(Lits,NextNum,RestModel),
5672 Model = RestModel
5673 ; read_grasp_models_aux([L|Lits],NextNum,RestModel),
5674 ( Model = RestModel
5675 ; \+ value(num_models,0),
5676 Model = [Num|RestModel] )).
5677
5678
5679read_walksat_preamble :-
5680 read_line(Line),
5681 ( Line == "" ->
5682 true
5683 ; read_walksat_preamble ).
5684
5685
5686read_walksat_models(Models) :-
5687 read_line(Line),
5688 ( ( Line == end_of_file ; Line == "" ) ->
5689 Models = []
5690 ; prefix(Line,"Begin assign with lowest # bad = 0",_) ->
5691 read_walksat_model(Model),
5692 read_walksat_models(RestModels),
5693 Models = [Model|RestModels]
5694 ; read_walksat_models(Models) ).
5695
5696
5697read_walksat_model(Model) :-
5698 read_line(Line),
5699 ( Line == "End assign" ->
5700 Model = []
5701 ; get_positive_numbers(Line,FirstVars),
5702 read_walksat_model(RestVars),
5703 append(FirstVars,RestVars,Model) ).
5704
5705
5706read_walksat_time(TimeMsg) :-
5707 read_line(Line),
5708 ( Line == end_of_file ->
5709 TimeMsg = "Solution time: unknown."
5710 ; prefix(Line,"total elapsed seconds = ",Time) ->
5711 format_to_charlist(TimeMsg,"Solution time: ~s seconds.",[Time])
5712 ; read_walksat_time(TimeMsg) ).
5713
5714
5715read_walksat_answer(Ans) :-
5716 read_line(Line),
5717 ( Line = end_of_file
5718 -> Ans = "No solution was found."
5719 ; Line = "ASSIGNMENT FOUND"
5720 -> Ans = "SAT"
5721 ; Line = "ASSIGNMENT NOT FOUND"
5722 -> Ans = "UNSAT"
5723 ; read_walksat_answer(Ans) ).
5724
5725
5726read_zchaff_answer(Ans) :-
5727 read_line(Line),
5728 ( Line == end_of_file
5729 -> Ans = "No solution was found."
5730 ; Line == "Verify Solution successful. Instance satisfiable"
5731 -> Ans = "SAT"
5732 ; Line == "Instance unsatisfiable"
5733 -> Ans = "UNSAT"
5734 ; read_zchaff_answer(Ans) ).
5735
5736
5737read_zchaff_model(Model) :-
5738 read_line(Line),
5739 get_positive_numbers(Line,Model).
5740
5741
5742read_zchaff_time(TimeMsg) :-
5743 read_line(Line),
5744 ( Line == end_of_file ->
5745 TimeMsg = "Solution time: unknown."
5746 ; prefix(Line,"Total Run Time",RestLine) ->
5747 drop_spaces(RestLine,TimeStr),
5748 format_to_charlist(TimeMsg,"Solution time: ~s seconds.",[TimeStr])
5749 ; read_zchaff_time(TimeMsg) ).
5750
5751
5752read_mchaff_answer(Ans) :-
5753 read_line(Line),
5754 ( Line == end_of_file ->
5755 Ans = "No solution was found."
5756 ; prefix(Line,"Satisfyable instance",_) ->
5757 Ans = "SAT"
5758 ; prefix(Line,"Unsatisfiable instance",_) ->
5759 Ans = "UNSAT"
5760 ; read_mchaff_answer(Ans) ).
5761
5762
5763read_mchaff_time(TimeMsg) :-
5764 read_line(Line),
5765 ( Line == end_of_file ->
5766 TimeMsg = "Solution time: unknown."
5767 ; prefix(Line,"UserTimeForSearch: ",SearchTime0) ->
5768 read_line(Line2),
5769 prefix(Line2,"TotalUserTime: ",TotalTime),
5770 get_number(SearchTime0,SearchNum,_),
5771 get_number(TotalTime,TotalNum,_),
5772 PrepNum is max(TotalNum - SearchNum,0),
5773 format_to_charlist(SearchTime,"~2f",[SearchNum]),
5774 format_to_charlist(PrepTime,"~2f",[PrepNum]),
5775 ccalc_format_time(TotalTime,PrepTime,SearchTime,TimeMsg)
5776 ; read_mchaff_time(TimeMsg) ).
5777
5778
5783
5784read_mchaff_models(Models) :-
5785 value(num,N),
5786 5787 iset(num_models,N),
5788 read_mchaff_models_aux([],Models).
5789
5790read_mchaff_models_aux(InModels,OutModels) :-
5791 5792 read_line(Line),
5793 ( prefix(Line,"\"[",ModelBits)
5794 -> 5795 5796 5797 findall( M,
5798 ( read_mchaff_models_aux2(ModelBits,1,M),
5799 \+ member(M,InModels),
5800 5801 5802 ( value(num_models,all)
5803 -> true
5804 ; decr(num_models,_) )),
5805 LineModels ),
5806 append(InModels,LineModels,NewModels),
5807 read_mchaff_models_aux(NewModels,OutModels)
5808 ; OutModels = InModels ).
5809
5810
5828
5829read_mchaff_models_aux2([Bit|RestBits],Index,Model) :-
5830 5831 ( value(num_models,0)
5832 -> false
5833
5834 5835 5836 ; Bit == 93,
5837 ( value(mode,transition)
5838 -> value(extended_atom_count,AC)
5839 ; value(atom_count,AC) ),
5840 Index > AC
5841 -> Model = []
5842
5843 ; NextIndex is Index + 1,
5844 ( Bit == 93
5845 -> 5846 5847 read_mchaff_models_aux2([Bit|RestBits],NextIndex,RestModel)
5848 ; 5849 read_mchaff_models_aux2(RestBits,NextIndex,RestModel) ),
5850 ( Bit == 49 5851 -> Model = [Index|RestModel]
5852 ; Bit == 48 5853 -> Model = RestModel
5854 ; 5855 ( Model = RestModel
5856 ; ( value(num_models,0)
5857 -> false
5858 ; Model = [Index|RestModel] )))).
5859
5860
5861bits_to_numbers(String,Nums) :- bits_to_numbers(String,Nums,1).
5862bits_to_numbers([Bit|RestBits],Nums,Index) :-
5863 Index2 is Index + 1,
5864 ( Bit == 49 -> 5865 bits_to_numbers(RestBits,RestNums,Index2),
5866 Nums = [Index|RestNums]
5867 ; ( Bit == 48 ; Bit == 88 ) -> 5868 bits_to_numbers(RestBits,Nums,Index2)
5869 ; Nums = [] ).
5870
5879ccalc_format_time(TotalLine,PrepLine,SolveLine,Msg) :-
5880 drop_spaces(TotalLine,TotalStr),
5881 get_until(TotalStr," ",Total,_),
5882 append("Solution time: ",Total,Msg1),
5883 append(Msg1," seconds (prep ",Msg2),
5884 drop_spaces(PrepLine,PrepStr),
5885 get_until(PrepStr," ",Prep,_),
5886 append(Msg2,Prep,Msg3),
5887 append(Msg3," seconds, search ",Msg4),
5888 drop_spaces(SolveLine,SolveStr),
5889 get_until(SolveStr," ",Solve,_),
5890 append(Msg4,Solve,Msg5),
5891 append(Msg5," seconds)",Msg).
5892
5893
5899
5900rebuild_models([],_,[]).
5901
5902rebuild_models([CModel|RestCModels],Vars,[RModel|RestRModels]) :-
5903 rebuild_model(CModel,Vars,RModel),
5904 rebuild_models(RestCModels,Vars,RestRModels).
5905
5906rebuild_model(_,[],[]).
5907
5908rebuild_model(CModel,[[R,-1]|RestVars],[R|RestR]) :-
5909 rebuild_model(CModel,RestVars,RestR).
5910
5911rebuild_model(CModel,[[_,-2]|RestVars],RestR) :-
5912 rebuild_model(CModel,RestVars,RestR).
5913
5914rebuild_model(CModel,[[R,C]|RestVars],[R|RestR]) :-
5915 member(C,CModel),
5916 rebuild_model(CModel,RestVars,RestR).
5917
5918rebuild_model(CModel,[_|RestVars],RestR) :-
5919 rebuild_model(CModel,RestVars,RestR).
5920
5921
5922get_renamed_vars([Var|RestVars]) :-
5923 read_line(Line),
5924 get_numbers(Line,Var),
5925 get_renamed_vars(RestVars).
5926get_renamed_vars([]).
5927
5928
5931
5932report_time([CompactTime,Lockfile],Msg) :-
5933 ( value(timed,true)
5934 -> ( nonvar(CompactTime)
5935 -> see(CompactTime),
5936 wait(Lockfile),
5937 parse_time(T), !,
5938 seen,
5939 format("% Compact time: ~2f seconds.~n",[T]),
5940 common_file_delete(CompactTime)
5941 ; true ),
5942 format("% ~s~n",[Msg])
5943 ; true ),
5944 nl.
5945
5946clausify_wff(Wff,Nss) :-
5947 findall( Ns,
5948 ( gcnf(Wff,Css),
5949 member(Ms,Css),
5950 sort(Ms,Ns),
5951 \+ tautology(Ns) ),
5952 Nss ).
5953
5954universal_closure(Wff,NewWff) :-
5955 find_free_variables(Wff,Vs),
5956 wrap_univ_quantifiers(Vs,Wff,NewWff).
5957
5959gcnf(W,Cs) :-
5960 negation_normal_form(W,W11),
5962 do_term_expansion(W11,W1),
5963 nnf_to_cnf(W1,Cs0,Aux),
5964 append(Cs0,Aux,Cs).
5965
5966nnf_to_cnf(W1,Cs,AuxCs) :-
5967 ( W1 = false
5968 -> Cs = [[]],
5969 AuxCs = []
5970 ; W1 = true
5971 -> Cs = [],
5972 AuxCs = []
5973 ; distribute_or_over_and(W1,Cs,AuxCs) ).
5974
5975
5976gdnf(W,Cs) :-
5977 negation_normal_form(W,W1),
5978 value(optimize,Opt),
5979 iset(optimize,false),
5980 nnf_to_dnf(W1,Cs,_),
5981 iset(optimize,Opt).
5982
5983
5984nnf_to_dnf(W,Cs,AuxCs) :-
5985 ( W = false
5986 -> Cs = [],
5987 AuxCs = []
5988 ; W = true
5989 -> Cs = [[]],
5990 AuxCs = []
5991 ; distribute_and_over_or(W,Cs,AuxCs) ).
5992
5993negation_normal_form(A,E) :-
5994 equiv(A,A1),
5995 !,
5996 negation_normal_form(A1,E).
5997
5998negation_normal_form((A && B),E) :-
5999 !,
6000 negation_normal_form(A,A1),
6001 ( A1 = false
6002 -> E = false
6003 ; A1 = true
6004 -> negation_normal_form(B,E)
6005 ; negation_normal_form(B,B1),
6006 ( B1 = false
6007 -> E = false
6008 ; B1 = true
6009 -> E = A1
6010 ; E = (A1 && B1) ) ).
6011
6012negation_normal_form((A ++ B),E) :-
6013 !,
6014 negation_normal_form(A,A1),
6015 ( A1 = false
6016 -> negation_normal_form(B,E)
6017 ; A1 = true
6018 -> E = true
6019 ; negation_normal_form(B,B1),
6020 ( B1 = false
6021 -> E = A1
6022 ; B1 = true
6023 -> E = true
6024 ; E = (A1 ++ B1) ) ).
6025
6026negation_normal_form(-A,E) :-
6027 !,
6028 ( ( value(debug,true)
6029 -> extended_test(A)
6030 ; test(A) )
6031 -> ( call(A)
6032 -> E = false
6033 ; E = true )
6034 ; integer(A)
6035 -> B is 0 - A,
6036 E = B
6037 ; E = -A ).
6038
6039negation_normal_form(A,E) :-
6040 ( ( value(debug,true)
6041 -> extended_test(A)
6042 ; test(A) )
6043 -> ( call(A)
6044 -> E = true
6045 ; E = false )
6046 ; E = A ).
6047
6048extended_test(A) :-
6049 ( A =.. [=,A1,A2]
6050 -> ( ( (evaluable_expr(A1) ; object(A1)),
6051 (evaluable_expr(A2) ; object(A2)) )
6052 -> test(A)
6053 ; fatal_error("Invalid expression (~w).", [A]) )
6054 ; test(A) ).
6055
6057replace_false_with_negative_literal_list([L|Ls],[L1|L1s]) :-
6058 replace_false_with_negative_literal(L,L1),
6059 replace_false_with_negative_literal_list(Ls,L1s).
6060replace_false_with_negative_literal_list([],[]).
6061%*/
6062
6063/*
6064replace_false_with_negative_literal_list(Fs,Ns) :-
6065 replace_false_with_negative_literal_list(Fs,[],Ns).
6066replace_false_with_negative_literal_list([L|Ls],Acc,newL) :-
6067 replace_false_with_negative_literal(L,L1),
6068 append(Acc,[L1],Acc1),
6069 replace_false_with_negative_literal_list(Ls,Acc1,newL).
6070replace_false_with_negative_literal_list([],newL,newL).
6071*/
6072
6073%equiv(((T: A eq true)=(T: B eq true)), ((T: A eq true)<->(T: B eq true))).
6074%equiv(((A eq true)=(B eq true)), ((A eq true)<->(B eq true))).
6075equiv((A <-> B),((-A ++ B) && (A ++ -B))).
6076equiv((A ->> B),(-A ++ B)).
6077%equiv((A , B),( A && B)).
6078equiv((A & B),( A && B)).
6079equiv(-Wff,NewWff) :- equivnot(Wff,NewWff).
6080
6081equiv([/\X|A],E) :-
6082% tuple_to_list(X,Vs),
6083 Vs=[X],
6084 find_computed_variables(Vs,Us),
6085 renaming_subst(Vs,Sub),
6086 subst_free(A,A1,Sub),
6087 findall((A1,Us),bind_vars(Sub),As),
6088 replace_false_with_negative_literal_list(As,Cs),
6089 unify_computed_variables(Cs,Bs,Us),
6090 conjoin_list(Bs,E0),
6091 eval_expr(E0,E). % why this was added? to evaluate arithmetic inside constant
6092
6093
6094equiv([\/X|A],E) :-
6095 Vs=[X],
6096% tuple_to_list(X,Vs),
6097 find_computed_variables(Vs,Us),
6098 renaming_subst(Vs,Sub),
6099 subst_free(A,A1,Sub),
6100 findall((A1,Us),bind_vars(Sub),As),
6101 replace_false_with_negative_literal_list(As,Cs),
6102 unify_computed_variables(Cs,Bs,Us),
6103 disjoin_list(Bs,E0),
6104%^format("~nE0 is : ",[]),
6105%^print_list([E0]),
6106 eval_expr(E0,E).
6107
6108
6109find_computed_variables([],[]).
6110find_computed_variables([V|Vs],Us) :-
6111 ( var_sort(V,computed)
6112 -> Us = [V|Us1],
6113 find_computed_variables(Vs,Us1)
6114 ; find_computed_variables(Vs,Us) ).
6115
6116unify_computed_variables([],[],_).
6117unify_computed_variables([(A,Us)|As],[A|Bs],Us) :-
6118 unify_computed_variables(As,Bs,Us).
6119
6120% We separate the negative Wffs to take advantage of indexing.
6121equivnot((A <-> B),((A && -B) ++ (-A && B))).
6122equivnot((A ->> B),(A && -B)).
6123equivnot((A , B),(-A ++ -B)).
6124equivnot((A & B),(-A ++ -B)).
6125equivnot((A && B),(-A ++ -B)).
6126equivnot((A ++ B),(-A && -B)).
6127equivnot((-A),A).
6128equivnot([/\X|A],[\/X|(-A)]).
6129equivnot([\/X|A],[/\X|(-A)]).
6130
6131or(true,_,true) :-
6132 !.
6133or(_,true,true) :-
6134 !.
6135or(A,false,A) :-
6136 !.
6137or(false,A,A) :-
6138 !.
6139or(A,B,(A ++ B)).
6140
6141
6142and(false,_,false) :-
6143 !.
6144and(_,false,false) :-
6145 !.
6146and(A,true,A) :-
6147 !.
6148and(true,A,A) :-
6149 !.
6150and(A,B,(A && B)).
6151
6152
6153
6154renaming_subst([],[]).
6155renaming_subst([N|Ns],[=(N,_)|Sub]) :-
6156 renaming_subst(Ns,Sub).
6157
6158
6159
6162
6163tuple_to_list((A,Bs),[A|As]) :-
6164 !,
6165 tuple_to_list(Bs,As).
6166tuple_to_list(A,[A]).
6167
6168list_to_tuple([A,A1|As],(A,Bs)) :-
6169 !,
6170 list_to_tuple([A1|As],Bs).
6171list_to_tuple([A],A).
6172list_to_tuple([],true).
6173
6174semituple_to_list((A;Bs),[A|As]) :-
6175 !,
6176 semituple_to_list(Bs,As).
6177semituple_to_list(A,[A]).
6178
6179list_to_semituple([A,A1|As],(A;Bs)) :-
6180 !,
6181 list_to_semituple([A1|As],Bs).
6182list_to_semituple([A],A).
6183list_to_semituple([],false).
6184
6186conjoin_list([],true).
6187conjoin_list([A|As],Wff) :-
6188 conjoin_list(As,Wff1),
6189 ( Wff1 = true
6190 -> Wff = A
6191 ; Wff = (A && Wff1) ).
6192
6194disjoin_list([],false).
6195disjoin_list([A|As],Wff) :-
6196 disjoin_list(As,Wff1),
6197 ( Wff1 = false
6198 -> Wff = A
6199 ; Wff = (A ++ Wff1) ).
6200
6201tuple_to_conjunct(A,B) :-
6202 tuple_to_list(A,C),
6203 conjoin_list(C,B).
6204
6207replace_comma_with_and(L,L1) :-
6208 tuples_to_conjs(L,L1).
6210
6221replace_comma_with_and_1([],true).
6222replace_comma_with_and_1([A|As],(B & Bs)) :-
6223 conjoin_tuple(A,B),
6224 replace_comma_with_and_1(As,Bs).
6225
6226conjoin_tuple((A,As),Wff) :-
6227 conjoin_tuple(As,Wff1),
6228 ( Wff1 = true
6229 -> Wff = A
6230 ; Wff = (A & Wff1) ).
6231conjoin_tuple(A,A).
6232
6233
6279
6280distribute_or_over_and(F,Result,Aux) :-
6281 distribute_or_over_and(F,Result,Aux,_,_,_,_,_),
6282 !.
6283
6285distribute_or_over_and([[]],[],[],1,[[]],[],[],1) :- !.
6286
6287distribute_or_over_and([],[[]],[],1,[],[],[],1) :- !.
6288
6289distribute_or_over_and([[A]],Pos,PosAux,PosN,Neg,NegVar,NegAux,NegN) :-
6290 !,
6291 distribute_or_over_and(A,Pos,PosAux,PosN,Neg,NegVar,NegAux,NegN).
6292
6293distribute_or_over_and([[A|B]],Pos,PosAux,PosN,Neg,NegVar,NegAux,NegN) :-
6294 !,
6295 distribute_or_over_and(([[A]]&&[B]),Pos,PosAux,PosN,Neg,NegVar,NegAux,NegN).
6296
6297distribute_or_over_and([A|B],Pos,PosAux,PosN,Neg,NegVar,NegAux,NegN) :-
6298 !,
6299 distribute_or_over_and(([A]++B),Pos,PosAux,PosN,Neg,NegVar,NegAux,NegN).
6300
6301% Convert a disjunction to CNF
6302distribute_or_over_and((A ++ B),Pos,PosAux,PosN,Neg,NegVar,NegAux,NegN) :-
6303 !,
6304 distribute_or_over_and(A,PosA,PosAuxA,PosNA,NegA,NegVarA,NegAuxA,NegNA),
6305 distribute_or_over_and(B,PosB,PosAuxB,PosNB,NegB,NegVarB,NegAuxB,NegNB),
6306
6307 % calculate the number of clauses generated if neither A nor B, only A,
6308 % or only B (respectively) is replaced with an auxiliary atom. (It's
6309 % never valuable to replace both, because the number of clauses saved by
6310 % avoiding distribution is always outweighed by the number of clauses
6311 % generated by auxiliary clauses.)
6312
6313 N00 is PosNA * PosNB,
6314 N10 is PosNB + PosNA + NegNA,
6315 N01 is PosNA + PosNB + NegNB,
6316
6317 % optimize positive formula A ++ B
6318 ( ( value(optimize,false)
6319 ; N00 =< N10, N00 =< N01 )
6320 -> % replace neither A nor B with auxiliary atoms: i.e. simply perform
6321 % distribution, by disjoining each disjunct from A with each disjunct
6322 % of B in turn and then conjoining all of these resulting disjunctions
6323 findall( R,
6324 ( member(DA,PosA),
6325 member(DB,PosB),
6326 append(DA,DB,R) ),
6327 Pos ),
6328 PosN is N00,
6329
6330 % No new auxiliary clauses were added, so simply append the clauses
6331 % generated for A and for B
6332 append(PosAuxA,PosAuxB,PosAux),
6333
6334 % Since no aux. clauses were introduced, the negations of A and B
6335 % were not used, and therefore none of the auxiliary atoms in those
6336 % formulae were instantiated. Thus, we append the atoms from A and B
6337 % and return them.
6338 append(NegVarA,NegVarB,NegVar)
6339
6340 ; N10 =< N01
6341 -> % replace A with an auxiliary atom. Thus the formula itself will
6342 % become K ++ B, which will then be distributed, and we'll also add
6343 % clauses to define K <-> A. The latter is of course -K ++ A and
6344 % K ++ -A, so this is where we use the optimized negation of A we
6345 % calculated in the recursive call. So first we must bind all of the
6346 % uninstantiated variables representing auxiliary atoms in -A.
6347 bind_all_vars(NegVarA),
6348
6349 % assign a new auxiliary atom to replace A
6350 ( value(extended_atom_count,_)
6351 -> incr(extended_atom_count,K)
6352 ; incr(atom_count,K) ),
6353 NegK is -K,
6354
6355 % distribute K ++ B, by simply adding K to each conjunct of B
6356 append_to_each(K,PosB,Pos),
6357
6358 % similarly generate clauses for -K ++ A
6359 append_to_each(NegK,PosA,PosAux1),
6360
6361 % similarly generate clauses for K ++ -A
6362 append_to_each(K,NegA,PosAux2),
6363
6364 % collect the newly defined auxiliary clauses with those defined
6365 % for all the subformulae used, and return
6366 append(PosAuxA,PosAuxB,PosAuxAB),
6367 append(PosAux1,PosAux2,PosAux12),
6368 append(PosAuxAB,PosAux12,PosAuxAB12),
6369 append(PosAuxAB12,NegAuxA,PosAux),
6370 PosN is PosNB,
6371 NegVar = NegVarB
6372
6373 ; % replace B with an auxiliary atom -- analogous to the previous case
6374 bind_all_vars(NegVarB),
6375 ( value(extended_atom_count,_)
6376 -> incr(extended_atom_count,K)
6377 ; incr(atom_count,K) ),
6378 NegK is -K,
6379 append_to_each(K,PosA,Pos),
6380 append_to_each(NegK,PosB,PosAux1),
6381 append_to_each(K,NegB,PosAux2),
6382 append(PosAuxA,PosAuxB,PosAuxAB),
6383 append(PosAux1,PosAux2,PosAux12),
6384 append(PosAuxAB,PosAux12,PosAuxAB12),
6385 append(PosAuxAB12,NegAuxB,PosAux),
6386 PosN is PosNA,
6387 NegVar = NegVarA ),
6388
6389 % optimize formula's negation (-A && -B). This is easy since -A and -B
6390 % are both in CNF after recursion-- no distribution is necessary.
6391 append(NegA,NegB,Neg),
6392 append(NegAuxA,NegAuxB,NegAux),
6393 NegN is NegNA + NegNB.
6394
6395% Convert a conjunction to CNF
6396distribute_or_over_and((A && B),Pos,PosAux,PosN,Neg,NegVar,NegAux,NegN) :-
6397 !,
6398 distribute_or_over_and(A,PosA,PosAuxA,PosNA,NegA,NegVarA,NegAuxA,NegNA),
6399 distribute_or_over_and(B,PosB,PosAuxB,PosNB,NegB,NegVarB,NegAuxB,NegNB),
6400
6401 % optimize formula (A && B) -- this is easy since A and B are already
6402 % in CNF after recursion
6403 append(PosA,PosB,Pos),
6404 append(PosAuxA,PosAuxB,PosAux),
6405 PosN is PosNA + PosNB,
6406
6407 % optimize formula's negation (-A ++ -B). This requires distributing
6408 % disjunction over conjunction and possibly introducing auxiliary atoms;
6409 % it's analagous to the converting the positive form of a disjunction,
6410 % above.
6411
6412 N00 is NegNA * NegNB,
6413 N10 is NegNB + PosNA + NegNA,
6414 N01 is NegNA + PosNB + NegNB,
6415 ( ( value(optimize,false)
6416 ; N00 =< N10, N00 =< N01 )
6417 -> % replace neither A nor B
6418 findall( R,
6419 ( member(DA,NegA),
6420 member(DB,NegB),
6421 append(DA,DB,R) ),
6422 Neg ),
6423 NegVar = [],
6424 append(NegAuxA,NegAuxB,NegAux),
6425 NegN = N00
6426 ; N10 =< N01
6427 -> % replace A. K and NegK are deliberately unbound here; they'll be
6428 % bound at a higher level of the expression tree if this subformula
6429 % is ever used
6430 bind_all_vars(NegVarA),
6431 NegVar = [[K,NegK]|NegVarB],
6432 append_to_each(K,NegB,Neg),
6433 append_to_each(NegK,NegA,NegAux1),
6434 append_to_each(K,PosA,NegAux2),
6435 append(NegAuxA,NegAuxB,NegAuxAB),
6436 append(NegAux1,NegAux2,NegAux12),
6437 append(NegAuxAB,NegAux12,NegAuxAB12),
6438 append(NegAuxAB12,PosAuxA,NegAux),
6439 NegN = NegNB
6440 ; % replace B. K and NegK are unbound; see comment above.
6441 bind_all_vars(NegVarB),
6442 NegVar = [[K,NegK]|NegVarA],
6443 append_to_each(K,NegA,Neg),
6444 append_to_each(NegK,NegB,NegAux1),
6445 append_to_each(K,PosB,NegAux2),
6446 append(NegAuxA,NegAuxB,NegAuxAB),
6447 append(NegAux1,NegAux2,NegAux12),
6448 append(NegAuxAB,NegAux12,NegAuxAB12),
6449 append(NegAuxAB12,PosAuxB,NegAux),
6450 NegN = NegNA ).
6451
6453distribute_or_over_and(-A,E,[],1,NegE,[],[],1) :-
6454 !,
6455 distribute_or_over_and(A,NegE,_,_,E,_,_,_).
6456
6458distribute_or_over_and(A,[[E]],[],1,[[NegE]],[],[],1) :-
6459 ( find_atom_integer(A,E)
6460 -> NegE is -E
6461 ; integer(A),
6462 A >= 0,
6463 ( value(extended_atom_count,AC) -> true ; value(atom_count,AC) ),
6464 A =< AC
6465 -> E = A,
6466 NegE is -E
6467 ; integer(A),
6468 A =< 0,
6469 NegA is -A
6470 -> distribute_or_over_and(NegA,[[NegE]],_,_,[[E]],_,_,_)
6471 ; subst_functor(eq,=,A,A1),
6472 fatal_error("~q is not an atomicFormula.",[A1]) ).
6473
6474
6486
6487distribute_and_over_or(F,Result,Aux) :-
6488 distribute_and_over_or(F,Result,Aux,_,_,_,_,_),
6489 !.
6490
6491distribute_and_over_or((A && B),Pos,PosAux,PosN,Neg,NegVar,NegAux,NegN) :-
6492 !,
6493 distribute_and_over_or(A,PosA,PosAuxA,PosNA,NegA,NegVarA,NegAuxA,NegNA),
6494 distribute_and_over_or(B,PosB,PosAuxB,PosNB,NegB,NegVarB,NegAuxB,NegNB),
6495
6496 N00 is PosNA * PosNB,
6497 N10 is PosNB + PosNA + NegNA,
6498 N01 is PosNA + PosNB + NegNB,
6499
6500 % optimize formula A && B
6501 ( ( value(optimize,false)
6502 ; N00 =< N10, N00 =< N01 )
6503 -> findall( R,
6504 ( member(DA,PosA),
6505 member(DB,PosB),
6506 append(DA,DB,R) ),
6507 Pos ),
6508 PosN is N00,
6509 append(PosAuxA,PosAuxB,PosAux),
6510 append(NegVarA,NegVarB,NegVar)
6511
6512 ; N10 =< N01
6513 -> % replace A
6514 bind_all_vars(NegVarA),
6515 ( value(extended_atom_count,_)
6516 -> incr(extended_atom_count,K)
6517 ; incr(atom_count,K) ),
6518 NegK is -K,
6519 append_to_each(K,PosB,Pos),
6520 negate_lits(NegA,NegatedNegA),
6521 append_to_each(NegK,NegatedNegA,PosAux1),
6522 negate_lits(PosA,NegatedPosA),
6523 append_to_each(K,NegatedPosA,PosAux2),
6524 append(PosAuxA,PosAuxB,PosAuxAB),
6525 append(PosAux1,PosAux2,PosAux12),
6526 append(PosAuxAB,PosAux12,PosAuxAB12),
6527 append(PosAuxAB12,NegAuxA,PosAux),
6528 PosN is PosNB,
6529 NegVar = NegVarB
6530 ; % replace B
6531 bind_all_vars(NegVarB),
6532 ( value(extended_atom_count,_)
6533 -> incr(extended_atom_count,K)
6534 ; incr(atom_count,K) ),
6535 NegK is -K,
6536 append_to_each(K,PosA,Pos),
6537 negate_lits(NegB,NegatedNegB),
6538 append_to_each(NegK,NegatedNegB,PosAux1),
6539 negate_lits(PosB,NegatedPosB),
6540 append_to_each(K,NegatedPosB,PosAux2),
6541 append(PosAuxA,PosAuxB,PosAuxAB),
6542 append(PosAux1,PosAux2,PosAux12),
6543 append(PosAuxAB,PosAux12,PosAuxAB12),
6544 append(PosAuxAB12,NegAuxB,PosAux),
6545 PosN is PosNA,
6546 NegVar = NegVarA ),
6547
6548 % optimize formula's negation (-A ++ -B)
6549 append(NegA,NegB,Neg),
6550 append(NegAuxA,NegAuxB,NegAux),
6551 NegN is NegNA + NegNB.
6552
6553distribute_and_over_or((A ++ B),Pos,PosAux,PosN,Neg,NegVar,NegAux,NegN) :-
6554 !,
6555 distribute_and_over_or(A,PosA,PosAuxA,PosNA,NegA,NegVarA,NegAuxA,NegNA),
6556 distribute_and_over_or(B,PosB,PosAuxB,PosNB,NegB,NegVarB,NegAuxB,NegNB),
6557
6558 % optimize formula (A ++ B)
6559 append(PosA,PosB,Pos),
6560 append(PosAuxA,PosAuxB,PosAux),
6561 PosN is PosNA + PosNB,
6562
6563 % optimize formula's negation (-A && -B)
6564 N00 is NegNA * NegNB,
6565 N10 is NegNB + PosNA + NegNA,
6566 N01 is NegNA + PosNB + NegNB,
6567
6568 ( ( value(optimize,false)
6569 ; N00 =< N10, N00 =< N01 )
6570 -> % replace neither A nor B with auxiliary atoms
6571 findall( R,
6572 ( member(DA,NegA),
6573 member(DB,NegB),
6574 append(DA,DB,R) ),
6575 Neg ),
6576 NegVar = [],
6577 append(NegAuxA,NegAuxB,NegAux),
6578 NegN is N00
6579 ; N10 =< N01
6580 -> % replace A. K and NegK are deliberately unbound here; they'll be
6581 % bound at a higher level of the expression tree if this subformula
6582 % is ever used
6583 bind_all_vars(NegVarA),
6584 NegVar = [[K,NegK]|NegVarB],
6585 append_to_each(K,NegB,Neg),
6586 negate_lits(PosA,NegatedPosA),
6587 append_to_each(NegK,NegatedPosA,NegAux1),
6588 negate_lits(NegA,NegatedNegA),
6589 append_to_each(K,NegatedNegA,NegAux2),
6590 append(NegAuxA,NegAuxB,NegAuxAB),
6591 append(NegAux1,NegAux2,NegAux12),
6592 append(NegAuxAB,NegAux12,NegAuxAB12),
6593 append(NegAuxAB12,PosAuxA,NegAux),
6594 NegN is NegNB
6595 ; % replace B. K and NegK are unbound; see comment above.
6596 bind_all_vars(NegVarB),
6597 NegVar = [[K,NegK]|NegVarA],
6598 append_to_each(K,NegA,Neg),
6599 negate_lits(PosB,NegatedPosB),
6600 append_to_each(NegK,NegatedPosB,NegAux1),
6601 negate_lits(NegB,NegatedNegB),
6602 append_to_each(K,NegatedNegB,NegAux2),
6603 append(NegAuxA,NegAuxB,NegAuxAB),
6604 append(NegAux1,NegAux2,NegAux12),
6605 append(NegAuxAB,NegAux12,NegAuxAB12),
6606 append(NegAuxAB12,PosAuxB,NegAux),
6607 NegN is NegNB ).
6608
6610
6611distribute_and_over_or(A,Pos,PosAux,PosN,Neg,NegVar,NegAux,NegN) :-
6612 distribute_or_over_and(A,Pos,PosAux,PosN,Neg,NegVar,NegAux,NegN).
6613
6614
6617
6618bind_all_vars([]).
6619
6620bind_all_vars([[V,NegV]|Vs]) :-
6621 ( value(extended_atom_count,_)
6622 -> incr(extended_atom_count,K)
6623 ; incr(atom_count,K) ),
6624 V = K,
6625 NegV is -K,
6626 bind_all_vars(Vs).
6627
(Xs,Ys) :-
6631 ( value(extended_atom_count,M) -> true ; value(atom_count,M) ),
6632 ( value(extended_clause_count,N) -> true ; value(clause_count,N) ),
6633 value(query_clause_count,QCC),
6634 length(Xs,N1),
6635 length(Ys,N2),
6636 Num is (N + N1 + N2 + QCC),
6637 format("p cnf ~w ~w~n",[M,Num]).
6638
(Xs,Ys) :-
6640 ( value(extended_atom_count,M) -> true ; value(atom_count,M) ),
6641 ( value(extended_clause_count,N) -> true ; value(clause_count,N) ),
6642 value(query_clause_count,QCC),
6643 length(Xs,N1),
6644 length(Ys,N2),
6645 Num is (N + N1 + N2 + QCC),
6646 M1 is M+1,
6647 format("p cnf ~w ~w~n",[M1,Num]).
6648
(Xs,Ys,Zs) :-
6650 ( value(extended_atom_count,M) -> true ; value(atom_count,M) ),
6651 ( value(extended_clause_count,N) -> true ; value(clause_count,N) ),
6652 length(Xs,N1),
6653 length(Ys,N2),
6654 length(Zs,N3),
6655 Num is (N + N1 + N2 + N3),
6656 format("p cnf ~w ~w~n",[M,Num]).
6657
6660
6661write_clauses([]).
6662
6663write_clauses([C|Cs]) :-
6664 write_clause(C), write_clauses(Cs).
6665
6666
6667write_clause([]) :-
6668 write(0), nl.
6669
6670write_clause([L|Ls]) :-
6671 write(L), write(' '), write_clause(Ls).
6672
6673
6674get_numbers(String,Nums) :-
6675 drop_spaces(String,NewS),
6676 ( NewS = []
6677 -> Nums = []
6678 ; get_number(NewS,Num,Rest),
6679 Nums = [Num|Nums1],
6680 get_numbers(Rest,Nums1) ).
6681
6682get_positive_numbers(String,Nums) :-
6683 drop_spaces(String,NewS),
6684 ( NewS = []
6685 -> Nums = []
6686 ; get_number(NewS,Num,Rest),
6687 ( Num > 0
6688 -> Nums = [Num|Nums1]
6689 ; Nums = Nums1 ),
6690 get_positive_numbers(Rest,Nums1) ).
6691
6692
6693drop_spaces([C|Cs],Cs1) :-
6694 ( (C = 32; C = 9) -> drop_spaces(Cs,Cs1)
6695 ; Cs1 = [C|Cs] ).
6696drop_spaces([],[]).
6697
6698get_number(String,Num,Rest) :-
6699 get_until(String,[32,10],Chars,Rest),
6700 common_number_chars(Num,Chars).
6701
6702get_until([Char|Cs],Delimiters,[],Cs) :-
6703 member(Char,Delimiters), !.
6704get_until([C|Cs],Delimiters,[C|Chars],Rest) :-
6705 get_until(Cs,Delimiters,Chars,Rest).
6706get_until([],_,[],[]).
6707
6708
6723
6724
6730is_attribute(A,Attr) :-
6731 A =.. [AName|AConstArgs],
6732 Attr =.. [AttrName| AttrConstArgs],
6733 prefix(AttrConstArgs,AConstArgs,_),
6736 consts_to_sorts(AConstArgs,ASortArgs),
6737 consts_to_sorts(AttrConstArgs,AttrSortArgs),
6738 A1 =.. [AName|ASortArgs],
6739 Attr1 =.. [AttrName|AttrSortArgs],
6740 attribute0(A1,Attr1),
6741 !.
6742
6743get_attribute(FL,A,(Attr=Arg2)) :- 6744 A =.. [_FA|ArgsA], 6745 FL =.. [FFL|ArgsFL], 6746 (=(FFL,eq) 6747 -> ArgsFL = [Arg1,Arg3] 6748 ; Arg1 = FL), 6749 Arg1 =.. [FArg1|ArgsArg1], 6750 is_attribute(A,Arg1),
6751 append(ArgsA,ArgsAttr,ArgsArg1), 6752 (\==(FFL,eq) 6753 -> Arg2 = true
6754 ; Arg2 = Arg3),
6755 Attr =.. [FArg1|ArgsAttr]. % to =.. [to]
6756
6757
6758display_attributes(A,Attrs) :-
6759 ( A = (A1 eq V)
6760 ; A1 = A ), !,
6761 A1 =.. [FA|ArgsA],
6762 list_to_tuple(ArgsA,TupleA),
6763 ( TupleA == true
6764 -> format("~w(",[FA])
6765 ; format("~w(~w,",[FA,TupleA]) ) ,
6766 !,
6767 display_attrs(Attrs),
6768 !,
6769 display_others(A,Attrs),
6770 !,
6771 write(')'),
6772 ( A = (A1 eq V), V \= true
6773 -> format("=~w",[V])
6774 ; true ),
6775 write(' ').
6776
6777display_attrs([]) :- !.
6778display_attrs([A]) :-
6779 write(A).
6780display_attrs([A|As]) :-
6781 write(A),
6782 write(','),
6783 display_attrs(As).
6784
6785
6786display_others(A,Attrs) :-
6787 get_others(A,Attrs,Others0),
6788 remove_duplicates(Others0,Others),
6789 !,
6790 (Others = []
6791 -> true
6792 ; write(','),
6793 display_attrs(Others) ).
6794
6798get_others(A,Attrs,Others) :-
6799 functor(A,FA,NA),
6800 domain_schema(_,Cs),
6801 member(C,Cs),
6802 functor(C,FA,NA),
6803 findall((Attr:false),
6804 (attribute0(C,Attr0),is_different_attr(A,Attr0,Attrs,Attr)),
6805 Others).
6806
6807is_different_attr0(_Attr0,[]).
6808is_different_attr0(Attr0,[(Attr1:_)|Attrs]) :-
6809 functor(Attr0,FAttr,_NAttr),
6810 Attr1 =.. [FAttr1|_ArgsAttr1],
6811 FAttr \== FAttr1,
6812 is_different_attr0(Attr0,Attrs).
6813
6814is_different_attr(A,Attr0,Attrs,Attr) :-
6815 is_different_attr0(Attr0,Attrs),
6816
6817 A =.. [_FA|ArgsA],
6818
6819 functor(Attr0,FAttr,NAttr),
6820
6821 domain(simpleFluent,Fs),
6822 functor(Attr2,FAttr,NAttr),
6823 member(Attr2,Fs),
6824 Attr2 =.. [FAttr|ArgsAttr0],
6825
6826 append(ArgsA,ArgsAttr,ArgsAttr0),
6827 Attr =.. [FAttr|ArgsAttr].
6828
6838
6839show_models(Models,QueryMode) :-
6840 ( Models = [_Model1,_Model2|_Rest]
6841 -> show_models(Models,QueryMode,1,true)
6842 ; show_models(Models,QueryMode,1,false) ).
6843
6844show_models([Model|Rest],QueryMode,Num,Label) :-
6845 common_statistics(_),
6846
6847 6848 ( Label == true
6849 -> ( QueryMode == (query)
6850 -> format("Solution ~w:~n~n",[Num])
6851 ; (QueryMode == sat),
6852 ( ( value(mode,history); value(mode,transition) )
6853 -> format("State ~w:~n~n",[Num])
6854 ; format("Satisfying Interpretation ~w:~n~n",[Num]) ))
6855 ; true ),
6856
6857 6858 ( (QueryMode == query)
6859 -> domain(step,Ts),
6860 show_model(Model,[none|Ts])
6861 ; value(mode,basic)
6862 -> show_model(Model,[none])
6863 ; show_model(Model,[none,0]) ),
6864
6865 NextNum is Num+1,
6866 show_models(Rest,QueryMode,NextNum,Label).
6867
6868show_models([],_,_,_).
6869
6870
6871show_model(_,[]) :- nl.
6872
6873show_model(Model,[T|Ts]) :-
6874 6875 6876 ( value(extended_atom_count,AC) -> true ; value(atom_count,AC) ),
6877 ( T \= none
6878 -> format("~w: ",[T]), flush_output,
6879 ( domain(simpleFluentAtomicFormula,[Fl0|_]),
6880 find_atom_integer((T : Fl0),FirstFlNum),
6881 ( NextT is T+1,
6882 find_atom_integer((NextT : Fl0),NextStepNum)
6883 ; NextStepNum is AC + 1 )
6884 ; FirstFlNum is AC + 1,
6885 NextStepNum = FirstFlNum ),
6886 ( domain(actionAtomicFormula,[Act0|_]),
6887 find_atom_integer((T : Act0),FirstActNum)
6888 ; FirstActNum is AC + 1 ),
6889 iset(displayed_fluent,true)
6890 ; FirstFlNum = 0,
6891 ( domain(simpleFluentAtomicFormula,Fls),
6892 member(Fl0,Fls),
6893 find_atom_integer((0 : Fl0),FirstActNum)
6894 ; FirstActNum is AC + 1 ),
6895 NextStepNum = FirstActNum,
6896 iset(displayed_fluent,false) ),
6897 !,
6898
6899 6900
6901 6902 ( suffix([PosN|RestModel0],Model),
6903
6904 6905 6906 6907 ( PosN >= FirstActNum
6908 -> RestModel1 = [PosN|RestModel0]
6909 ; find_atom_integer(PosA,PosN),
6910
6911 6912 6913 ( ( T == none, PosA \= (_T : _Fl), PosFl = PosA
6914 ; T \= none, PosA = (T : PosFl) )
6915 -> in_show_list(PosA),
6916 ( value(displayed_fluent,false)
6917 -> iset(displayed_fluent,true)
6918 ; true ),
6919 show_fluent(PosFl),
6920 fail
6921 6922 ; RestModel1 = [PosN|RestModel0] ) )
6923 ; RestModel1 = [] ),
6924 !,
6925
6926 6927 ( show_spec(Specs),
6928 ( member(negative,Specs)
6929 ; member(all,Specs)
6930 ; member(-_,Specs) )
6931 -> ( iterate_negative(NegN,Model,FirstFlNum,FirstActNum),
6932 find_atom_integer(NegA,NegN),
6933 in_show_list((-NegA)),
6934 ( T == none -> NegFl = NegA ; NegA = (T: NegFl) ),
6935 ( value(displayed_fluent,false)
6936 -> iset(displayed_fluent,true)
6937 ; true ),
6938 show_fluent((-NegFl)),
6939 fail
6940 ; true )
6941 ; true ),
6942
6943 ( value(displayed_fluent,true) -> format("~n~n",[]) ; true ),
6944 retractall(value(displayed_fluent,_)),
6945 dm,
6946 6947 ( T \= none,
6948 Ts \= []
6949 -> ( domain(actionAtomicFormula,AAFs) -> true ; AAFs = [] ),
6950 iset(displayed_action,false),
6951 ( suffix([ActN|RestModel2],RestModel1),
6952 ( ActN >= NextStepNum
6953 -> RestModel3 = [ActN|RestModel2]
6954 ; find_atom_integer(ActA,ActN),
6955 ActA = (T : Act),
6956 member(Act,AAFs),
6957 in_show_list(ActA)
6958 -> get_all_attributes(T,Act,RestModel2,Attrs),
6959 ( value(displayed_action,false)
6960 -> iset(displayed_action,true),
6961 format("ACTIONS: ",[])
6962 ; true ),
6963 ( Attrs == []
6964 -> show_fluent(Act)
6965 ; display_attributes(Act,Attrs) ),
6966 fail )
6967 ; RestModel3 = RestModel1 ),
6968
6969 6970 ( show_spec(Specs),
6971 ( member(negative,Specs)
6972 ; member(all,Specs)
6973 ; member(-_,Specs) )
6974 -> ( iterate_negative(NegN,RestModel1,FirstActNum,NextStepNum),
6975 find_atom_integer(NegA,NegN),
6976 in_show_list((-NegA)),
6977 ( T == none -> NegFl = NegA ; NegA = (T: NegFl) ),
6978 ( value(displayed_action,false)
6979 -> iset(displayed_action,true),
6980 format("ACTIONS: ",[])
6981 ; true ),
6982 show_fluent((-NegFl)),
6983 fail
6984 ; true )
6985 ; true ),
6986
6987 ( value(displayed_action,true) -> format("~n~n",[]) ; true ),
6988 retractall(value(displayed_action,_)),
6989 show_model(RestModel3,Ts)
6990
6991 ; show_model(RestModel1,Ts) ).
6992
6993dm.
6994iterate_negative(Start,Model,Start,End) :-
6995 Start =< End,
6996 ( Model == []
6997 ; Model = [M|_],
6998 Start < M ).
6999
7000iterate_negative(N,[Start|Ms],Start,End) :-
7001 Next is Start + 1,
7002 Next < End,
7003 iterate_negative(N,Ms,Next,End).
7004
7005iterate_negative(N,Model,Start,End) :-
7006 Next is Start + 1,
7007 Next < End,
7008 iterate_negative(N,Model,Next,End).
7009
7010get_all_attributes(T,Act,Model,Attrs) :-
7011 ( Act = (Act1 eq _V)
7012 ; Act1 = Act ), !,
7013 Act1 =.. [ActName|Args],
7014 consts_to_sorts(Args,ArgSorts),
7015 ActTemplate =.. [ActName|ArgSorts],
7016 findall( AttrStr,
7017 ( attribute0(ActTemplate,AttrTemplate),
7018 AttrTemplate =.. [AttrName|AttrArgSorts],
7019 append(ArgSorts,RestAttrArgSorts,AttrArgSorts),
7020 consts_to_sorts(RestAttrArgs,RestAttrArgSorts),
7021 append(Args,RestAttrArgs,AttrArgs),
7022 Attr =.. [AttrName|AttrArgs],
7023 atom_integer((T:Attr eq V),N),
7024 ordered_memberchk(N,Model),
7025 get_attribute((Attr eq V),Act1,AttrStr) ),
7026 Attrs ),
7027 !.
7028
7029show_fluent(-F) :-
7030 ( F =.. [eq,Arg1,Arg2]
7031 -> ( ab(Arg1)
7032 -> true
7033 ; Arg2 == true
7034 -> format("-~w ",[Arg1])
7035 ; Arg2 == false
7036 -> format("~w ",[Arg1])
7037 7038 ; true )
7039 ; format("-~w ",[F]) ),
7040 flush_output,
7041 !.
7042
7043show_fluent(F) :-
7044 ( F =.. [eq,Arg1,Arg2]
7045 -> ( ab(Arg1)
7046 -> true
7047 ; Arg2 == true
7048 -> format("~w ",[Arg1])
7049 ; Arg2 == false
7050 -> format("-~w ",[Arg1])
7051 ; format("~w=~w ",[Arg1,Arg2]) )
7052 ; format("~w ",[F]) ),
7053 flush_output.
7054
7055
7056count_atoms(N) :-
7057 findall(x,atom_integer(_,_),S), length(S,N).
7058count_rule_schemas(N) :-
7059 findall(x,rule_schema(_),S), length(S,N).
7060count_rules(N) :-
7061 findall(x,db_fetch_rule((_<=_)),S), length(S,N).
7062
7063complement_list([F|Fs],[G|Gs]) :-
7064 comp(F,G),
7065 complement_list(Fs,Gs).
7066complement_list([],[]).
7067
7068comp(-F,F) :-
7069 !.
7070comp(F,-F).
7071
7073value(var_counter,-3).
7074value(dynamic_detected,false).
7075value(additive_detected,false).
7076value(mode,basic).
7077value(models_labeled,false).
7078value(max_no_of_clauses_in_internal_db,400000).
7080value(max_no_of_clauses_to_optimize,8). 7081value(query_counter,-1).
7082value(debug,true).
7083
7084
7085show_options :-
7086 nl,
7087 ( value(solver,Solver)
7088 -> format(" solver = ~w~n",[Solver]),
7089 ( value(solver_opts(Solver),Opts)
7090 -> format(" solver_opts(~w) = '~w'~n",[Solver,Opts])
7091 ; true )
7092 ; true ),
7093 member(Option,[num,dir,file_io,timed,verbose,compact,optimize,
7094 eliminate_tautologies]),
7095 ( value(Option,Value)
7096 -> format(" ~w = ~w~n",[Option,Value])
7097 ; true ),
7098 fail.
7099
7100show_options.
7101
7102show_parameters :- show_options.
7103
7104
7105reset_options :-
7106 7107 7108 value(ccalc_dir,D),
7109 format_to_atom(DefaultOptsFile,'~woptions.std',[D]),
7110 compile(DefaultOptsFile),
7111 environ('PWD',P),
7112 format_to_atom(UserOptsFile,'~w/options.std',[P]),
7113 ( common_file_exists(UserOptsFile)
7114 -> compile(UserOptsFile)
7115 ; true ).
7116
7117reset_parameters :- reset_options.
7118
7119
7120show_atoms :-
7121 atom_integer(A,I),
7122 format("~n~d. ~w",[I,A]),
7123 fail.
7124show_atoms.
7125
7126
7127show_problems :- show_problem(_).
7128
7129show_problem(Label) :-
7130 7131 show_plan(Label),
7132 fail.
7133show_problem(Label) :-
7134 show_query(Label),
7135 fail.
7136show_problem(_).
7137
7138show_queries :- show_query(_).
7139
7140show_query(Label) :-
7141 query_problem(Label,MaxStep,Rules),
7142 format("~n<<query ~q>>",[Label]),
7143 format("~nmaxstep :: ~q;",[MaxStep]),
7144 show_formulas(Rules),
7145 write('.'),
7146 nl,
7147 fail.
7148show_query(_).
7149
7150show_formulas((A;B)) :-
7151 !,
7152 show_formulas(A),
7153 write(';'),
7154 show_formulas(B).
7155show_formulas(A) :-
7156 format("~n ~w",[A]).
7157
7158show_clauses :-
7159 clause(Cs),
7160 nl,
7161 show_clause(Cs),
7162 fail.
7163show_clauses.
7164
7178
7179show_clause([]).
7180show_clause([N|Ns]) :-
7181 show_literal(N),
7182 ( Ns = []
7183 -> write('.')
7184 ; write(' ++ ') ),
7185 show_clause(Ns).
7186
7187show_literal(N) :-
7188 ( N = 0
7189 -> write(false)
7190 ; N > 0
7191 -> ( find_atom_integer(A,N)
7192 -> show_atom(A)
7193 ; write(N) )
7194 ; M is 0-N,
7195 ( find_atom_integer(A,M)
7196 -> show_atom(-A)
7197 ; write(N) ) ).
7198
7199
7200% show_atom(X) :- write(X), !.
7201
7202show_atom(A) :-
7203 ( ( A = (T:(A0 eq true)) ; A = -((T:(A0 eq false))) )
7204 -> format('~w:~w',[T,A0])
7205 ; ( A = (T:(A0 eq false)); A = -((T:(A0 eq true))) )
7206 -> format('-(~w:~w)',[T,A0])
7207 ; A = -((T:(A0 eq V)))
7208 -> format('~w:~w\\=~w',[T,A0,V])
7209 ; A = (T : (A0 eq V))
7210 -> format('~w:~w=~w',[T,A0,V])
7211
7212 ; ( A = (A0 eq true) ; A = -((A0 eq false)) )
7213 -> format('~w',[A0])
7214 ; ( A = (A0 eq false); A = -((A0 eq true)) )
7215 -> format('-~w',[A0])
7216 ; A = -((A0 eq V))
7217 -> format('~w\\=~w',[A0,V])
7218 ; A = (A0 eq V)
7219 -> format('~w=~w',[A0,V])
7220 ; write(A) ),
7221 !.
7222
7223show_schemas :-
7224 rule_schema(Rule),
7225 write(Rule),
7226 nl,
7227 fail.
7228show_schemas.
7229
7230
7237
7243
7244find_saved_atom_integer(A,N) :-
7245 ( saved_atom_integer(A,N)
7246 -> true
7247 ; atom_integer(A,N) ),
7248 !.
7249
7250show_rules(H) :-
7251 ( H = -A
7252 -> db_fetch_rule((N<=L)),
7253 ( N > 0
7254 -> fail
7255 ; M is 0-N,
7256 find_saved_atom_integer(A1,M),
7257 A = A1,
7258 nl, show_rule((N,L)), fail )
7259 ; db_fetch_rule((N<=L)),
7260 ( N < 0
7261 -> fail
7262 ; N = 0
7263 -> H = false,
7264 nl, show_rule((N,L)), fail
7265 ; find_saved_atom_integer(A1,N),
7266 H = A1,
7267 nl, show_rule((N,L)), fail ) ).
7268show_rules(_).
7269
7270show_rules :-
7271 db_fetch_rule((N<=L)),
7272 nl,
7273 show_rule((N,L)),
7274 fail.
7275show_rules.
7276
7277show_rule((N,L)) :-
7278 show_head([N]),
7279 db_fetch_rule(rule_body(L,Ns1)),
7280 ( Ns1 == []
7281 -> write('.')
7282 ; write(' <= '),
7283 show_body(Ns1) ).
7284
7285show_query_rules :-
7286 db_fetch_query_rule((N<-L)),
7287 nl,
7288 show_query_rule((N,L)),
7289 fail.
7290show_query_rules.
7291
7292show_query_rule((N,L)) :-
7293 show_head([N]),
7294 write(' <= '),
7295 db_fetch_query_rule(query_rule_body(L,Ns1)),
7296 show_body(Ns1).
7297
7298
7299show_head([N|Ns]) :-
7300 show_rule_literal(N),
7301 ( Ns = []
7302 -> true
7303 ; write(' ++ ') ),
7304 show_head(Ns).
7305show_head([]).
7306
7307show_body([N|Ns]) :-
7308 show_rule_literal(N),
7309 ( Ns = []
7310 -> true
7311 ; write(',') ),
7312 show_body(Ns).
7313show_body([]) :- write('.').
7314
7315show_rule_literal(N) :-
7316 ( N = 0
7317 -> write(false)
7318 ; N > 0
7319 -> ( find_saved_atom_integer(A,N)
7320 -> show_atom(A)
7321 ; write(N) )
7322 ; M is 0-N,
7323 ( find_saved_atom_integer(A,M)
7324 -> show_atom(-A)
7325 ; write(N) ) ).
7326
7327
7328next(T,T1) :- T1 is T+1.
7329
7330% time(T) :- domain(time,Ts), member(T,Ts).
7331
7332rule_bodies_for_literal(N,Nss) :-
7333 findall(Ns,( db_fetch_rule((N<=L)), db_fetch_rule(rule_body(L,Ns)) ),Nss).
7334
7335query_rule_bodies_for_literal(N,Nss) :-
7336 findall(Ns,( db_fetch_query_rule((N<-L)), db_fetch_query_rule(query_rule_body(L,Ns)) ),Nss).
7337
7338find_free_variables(Wff,Vs) :-
7339 find_free_variables(Wff,[],Vs), close_list(Vs).
7340
7341find_free_variables(X,_Bound,_Vs) :-
7342 var(X),
7343 !.
7344find_free_variables(Term,Bound,Vs) :-
7345 atom(Term),
7346 var_sort(Term,_S),
7347 ( member(Term,Bound)
7348 -> true
7349 ; member(Term,Vs) ),
7350 !.
7351find_free_variables([/\X|W],Bound,Vs) :-
7352 !,
7353 find_free_variables(W,[X|Bound],Vs).
7354
7355% find_free_variables([\/'L'\/'B'|loc('B1')eq 'B'],[],_60854) ?
7356
7357find_free_variables([\/X|W],Bound,Vs) :-
7358 !,
7359 find_free_variables(W,[X|Bound],Vs).
7360
7361find_free_variables(Term,Bound,Vs) :-
7362 functor(Term,_,N),
7363 free_variables_arg(Term,0,N,Bound,Vs).
7364
7365
7366free_variables_arg(_Term,N,N,_Bound,_Vs) :-
7367 !.
7368free_variables_arg(Term,M,N,Bound,Vs) :-
7369 M1 is M+1,
7370 arg(M1,Term,A),
7371 find_free_variables(A,Bound,Vs),
7372 free_variables_arg(Term,M1,N,Bound,Vs).
7373
7374close_list([]) :-
7375 !.
7376close_list([_|Xs]) :- close_list(Xs).
7377
7378
7379
7380% - - - - - - - - - - - - - - - - - - - - - - - - - - - -%
7381% Procedures related to show/1.
7382% - - - - - - - - - - - - - - - - - - - - - - - - - - - -%
7383
7384in_show_list(Atom) :-
7385 % if no show spec was specified, default to 'positive'
7386 ( show_spec(Specs) ->
7387 true
7388 ; Specs = [positive] ),
7389
7390 % extract the constant from the atom
7391 ( Atom = (_T : Const)
7392 ; Atom = -((_T:Const))
7393 ; Atom = -Const
7394 ; Const = Atom ),
7395 !,
7396
7397 % if the atom is an action, check to see whether it's an abnormality
7398 % predicate. If so, display it only if the show list includes 'ab' or
7399 % that specific abnormality predicate. If it's a normal action, always
7400 % display if it's positive, and never if it's negative.
7401 %
7402 % Update: All positive normal (i.e. non-ab) actions are not shown anymore.
7403 % We additionally check if the action atom is a ground instance of one of
7404 % the Specs naming specific constants. (i.e. if the action has been
7405 % specified using the "show" command/predicate.
7406 % -- Selim T. Erdogan, 2 Mar 2008
7407 %
7408 ( ( domain(actionAtomicFormula,Acts),
7409 member(Const,Acts) )
7410 -> ( ab(AbTerm),
7411 is_ground_instance(Const,AbTerm)
7412 -> member(Spec,Specs),
7413 ( Spec == all
7414 -> true
7415 ; Spec == ab
7416 -> Atom \= -(_)
7417 ; is_ground_instance(Atom,Spec) )
7418 ; Atom \= -(_),
7419 Const \= (contribution(_,_) eq _),
7420 Const \= (accumulatedContribution(_,_) eq _),
7421 % The updated part is the addition below
7422 % -- Selim T. Erdogan, 2 Mar 2008
7423 member(Spec,Specs),
7424 ( Spec == all
7425 ; Spec == positive
7426 ; is_ground_instance(Atom,Spec) ) )
7427
7428
7429 % If Atom isn't an action, then it's displayed if:
7430 % 'all' is one of the show specs; or
7431 % 'positive' is one of the show specs, and Atom is neither the negation
7432 % of a positive atom nor a constant with a value of 'none'; or
7433 % 'negative' is one of the show specs, and Atom is the negation of a
7434 % positive atom or a constant with a value of 'none'; or
7435 % Atom is a ground instance of one of the Specs naming specific
7436 % constants.
7437 ; member(Spec,Specs),
7438 ( Spec == all
7439 ; Spec == positive,
7440 \+ Atom = -_Atom2,
7441 \+ Const = (_FL eq none)
7442 ; Spec == negative,
7443 ( Atom = -_Atom2 ; Const = (_FL eq none) )
7444 ; is_ground_instance(Atom,Spec) )), !.
7445
7446
7454
7455is_ground_instance([],[]) :- !.
7456
7457is_ground_instance([A|As],[S|Ss]) :-
7458 !,
7459 is_ground_instance(A,S),
7460 is_ground_instance(As,Ss).
7461
7463is_ground_instance(Atom,Atom).
7464
7466is_ground_instance(Atom,Spec) :-
7467 var_sort(Spec,Sort),
7468 const_to_sort(Atom,Sort).
7469
7471is_ground_instance(Atom,Spec) :-
7472 \+ functor(Spec,:,_),
7473 Atom = (_T2: FL),
7474 !,
7475 is_ground_instance(FL,Spec).
7476
7477% If Spec omits a value, it matches any value in Atom.
7478is_ground_instance(Atom,Spec) :-
7479 \+ functor(Spec,eq,_),
7480 Atom = (FL eq _Val),
7481 !,
7482 is_ground_instance(FL,Spec).
7483
7485is_ground_instance(Atom,Spec) :-
7486 Spec =.. [SF],
7487 Atom =.. [AF|AArgs], AArgs \= [],
7488 !,
7489 is_ground_instance(AF,SF).
7490
7492is_ground_instance(Atom,Spec) :-
7493 Atom =.. [AF|AArgs], AArgs \= [],
7494 Spec =.. [SF|SArgs], SArgs \= [],
7495 !,
7496 is_ground_instance(AF,SF),
7497 is_ground_instance(AArgs,SArgs).
7498
7499
7500
7521
7522valid_spec([Spec]) :-
7523 member(Spec,[positive,negative,ab,all,none]),
7524 !,
7525 ( consts(Spec,_)
7526 -> nonfatal_error("~s~w~s~w~s~n~s~w~s~n~s~w~s~s~n~s~n",
7527 ["Show spec '",Spec,"' is ambiguous. '",Spec,
7528 "' is a reserved keyword",
7529 " in show statements; to refer to the constant '",Spec,
7530 "', please include a",
7531 " timestamp, argument list, or value (for example, 'show ",
7532 Spec,"=V'"," for some",
7533 " variable V of the appropriate type)."]),
7534 fail
7535 ; true ).
7536
7537valid_spec([-Term]) :-
7538 valid_spec([Term]).
7539
7540valid_spec([Term]) :-
7541 % A spec may include a time step; if so, it must be a valid step
7542 ( Term = (T: Term0)
7543 -> domain(step,Ts),
7544 member(T,Ts)
7545 ; Term0 = Term ),
7546
7547 % A spec may include a value
7548 ( Term0 = (Fl eq Val)
7549 -> Term1 = Term0
7550 ; Fl = Term0,
7551 Term1 = (Term0 eq Val) ),
7552
7553 functor(Fl,F,N),
7554 ( functor_spec(F/N),
7555 find_free_variables(Term1,[V|Vs])
7556 -> renaming_subst([V|Vs],Sub),
7557 subst_free(Term1,Term2,Sub)
7558 ; N = 0
7559 -> consts(F,N1),
7560 % if constant F has N1 arguments, make a list of that many variables
7561 nth(N1,Vs,X), last(Vs,X), !,
7562 Term11 =.. [F|Vs],
7563 Term2 = (Term11 eq Val)
7564 ; Term2 = Term0 ),
7565 !,
7566
7567 ( ( domain(simpleFluentAtomicFormula,Fs)
7568 ; domain(sdFluentAtomicFormula,Fs) ),
7569 member(Term2,Fs)
7570 -> true
7571 ; domain(rigidAtomicFormula,Rs), member(Term2,Rs)
7572 -> var(T)
7573 ; domain(actionAtomicFormula,As), member(Term2,As),
7574 ( ( var(N1) -> AbN = N ; AbN = N1 ),
7575 ab(AbTerm),
7576 functor(AbTerm,F,AbN)
7577 -> true
7578 % Update: Now we allow for filtering of actions
7579 % -- Selim T. Erdogan, 2 Mar 2008
7580 %
7581 % ; nonfatal_error("Actions and attributes are not filtered!",[]) )
7582 ; true )
7583 ; domain(attributeAtomicFormula,Ats), member(Term2,Ats)
7584 % Update: Now we allow for filtering of actions
7585 % -- Selim T. Erdogan, 2 Mar 2008
7586 %
7587 % -> nonfatal_error("Actions and attributes are not filtered!",[]) ).
7588 -> true ).
7589
7590valid_spec([Term]) :-
7591 nonfatal_error("Show spec (~w) does not have an instance.~n",[Term]).
7592
7593valid_spec([]).
7594
7595valid_spec([H|T]) :-
7596 valid_spec([H]),
7597 !,
7598 valid_spec(T).
7599
7600valid_spec(Spec) :-
7601 nonfatal_error("Show spec (~w) does not have an instance.",[Spec]).
7602
7606
7607bind_vars_to_names([=(Var,Var)|Names]) :-
7608 bind_vars_to_names(Names).
7609bind_vars_to_names([]).
7610
7611read_and_expand(Term,ExpandedTerm) :-
7612 read_term(Term,[variable_names(Names)]),
7613 bind_vars_to_names(Names),
7614 do_term_expansion0(Term,TermTree),
7615 leaf_element(TermTree,ExpandedTerm).
7616
7617do_term_expansion0(Term,NewTerm) :-
7618 do_term_expansion1(Term,Term1),
7619 do_term_expansion(Term1,NewTerm).
7620
7621do_term_expansion1((:- query Q), (:- query Q)) :-
7622 \+ value(mode,history), !.
7623
7624do_term_expansion1((:- nmquery Q), (:- nmquery Q)) :-
7625 \+ value(mode,history), !.
7626
7627do_term_expansion1((:- macros A), (:- macros A)) :- !.
7628
7629do_term_expansion1(Term,NewTerm) :-
7630 do_one_expansion1(Term,Term1,Flag),
7631 ( Flag == true
7632 -> do_term_expansion1(Term1,NewTerm)
7633 ; NewTerm = Term1 ).
7634
7635do_one_expansion1(Term,NewTerm,Flag) :-
7636 ( var(Term)
7637 -> NewTerm = Term
7638 ; macro1(Term,NewTerm)
7639 -> Flag = true
7640 ; functor(Term,F,N), 7641 functor(NewTerm,F,N), 7642 do_one_expansion_arg1(Term,1,N,NewTerm,Flag) )
7642.
7643
7646do_one_expansion_arg1(_C,M,N,_D,_Flag) :-
7647 M > N,
7648 !.
7649do_one_expansion_arg1(C,M,N,D,Flag) :-
7650 arg(M,C,A),
7651 do_one_expansion1(A,B,Flag),
7652 arg(M,D,B),
7653 M1 is M+1,
7654 do_one_expansion_arg1(C,M1,N,D,Flag).
7655
7656%%%%%%%%%%%%%
7657
7658do_term_expansion((:- query Q), (:- query Q)) :-
7659 \+ value(mode,history), !.
7660
7661do_term_expansion((:- nmquery Q), (:- nmquery Q)) :-
7662 \+ value(mode,history), !.
7663
7664do_term_expansion((:- macros A), (:- macros A)) :- !.
7665
7666do_term_expansion(Term,NewTerm) :-
7667 do_one_expansion(Term,Term1,Flag),
7668 ( Flag == true
7669 -> do_term_expansion(Term1,NewTerm)
7670 ; NewTerm = Term1 ).
7671
7672do_one_expansion(((maxstep):: M), ((maxstep):: M),_) :- !.
7673 7674
7675do_one_expansion(Term,NewTerm,Flag) :-
7676 ( var(Term)
7677 -> NewTerm = Term
7678 ; ( macro(Term,Call,NewTerm), call(Call))
7679 -> Flag = true
7680 ; functor(Term,F,N), 7681 functor(NewTerm,F,N), 7682 do_one_expansion_arg(Term,1,N,NewTerm,Flag) )
7682.
7683
7686do_one_expansion_arg(_C,M,N,_D,_Flag) :-
7687 M > N,
7688 !.
7689do_one_expansion_arg(C,M,N,D,Flag) :-
7690 arg(M,C,A),
7691 do_one_expansion(A,B,Flag),
7692 arg(M,D,B),
7693 M1 is M+1,
7694 do_one_expansion_arg(C,M1,N,D,Flag).
7695
7696
7697leaf_element((A;B),X) :-
7698 !,
7699 (leaf_element(A,X); leaf_element(B,X)).
7700leaf_element(A,A).
7701
7702
7703read_rules(Rules) :-
7705 write('enter query (then ctrl-d)'),
7706 nl,
7707 read_formulas([],Rules).
7708
7709read_formulas(SoFar,Formula) :-
7710 read_and_expand(Term0,_Term),
7711 ( Term0 == end_of_file
7712 -> format("~n^D~n",[]),
7713 reverse(SoFar,Formula)
7714 ; read_formulas([Term0|SoFar],Formula)).
7715
7716
7717read_time(Time) :-
7718 nl,
7719 write('enter time (>= 1)'),
7720 nl,
7721 read_and_expand(_T0,T),
7722 ( T == end_of_file
7723 -> Time = 1
7724 ; integer(T), T >= 1
7725 -> Time = T
7726 ; read_time(Time) ).
7727
7728
7729fatal_error(FormatString,Args) :-
7730 nl,
7731 format("Error: ",[]),
7732 format(FormatString,Args),
7733 nl,
7734 close_abort.
7735
7736nonfatal_error(FormatString,Args) :-
7737 nl,
7738 format("Warning: ",[]),
7739 format(FormatString,Args),
7740 nl.
7741
7742
7743
7747
7749
7750shift_atoms_and_clauses(Time) :-
7751 7752 ( retract((atom_integer(_,_) :- atom_integer_extension(_,_)))
7753 -> true
7754 ; true ),
7755 retractall(atom_integer_extension(_,_)),
7756 retractall(clause(_)),
7757
7758 ( Time == 0
7759 -> 7760 7761 value(atom_count_0,AC),
7762 value(clause_count_0,CC)
7763 ; Time == 1
7764 -> 7765 7766 value(atom_count,AC),
7767 value(clause_count,CC)
7768 ; fail ),
7769 !,
7770 iset(extended_atom_count,AC),
7771 iset(extended_clause_count,CC),
7772
7773 write_shifted_clauses(Time,0,0).
7774
7775shift_atoms_and_clauses(Time) :-
7776 value(atom_count_0,AC0),
7777 value(atom_count,AC),
7778 Shift is AC - AC0,
7779 EAC is (Shift * Time) + AC0,
7780 iset(extended_atom_count,EAC),
7781
7782 value(clause_count_0,CC0),
7783 value(clause_count,CC),
7784 ECC is ((CC - CC0) * Time) + CC0,
7785 iset(extended_clause_count,ECC),
7786
7787 enumerate_atom_extension(1,Time,Shift),
7788 assertz( (atom_integer(A,I) :- atom_integer_extension(A,I)) ),
7789 value(rigid_count,RC),
7790 write_shifted_clauses(Time,Shift,RC).
7791
7798
7799enumerate_atom_extension(MaxTime,MaxTime,_) :- !.
7800
7801enumerate_atom_extension(Time,_,Shift) :-
7802 IShift is Time * Shift,
7803 value(atom_count_0,AC0),
7804 atom_integer((T:A),I),
7805 I > AC0,
7806 ShiftedT is T + Time,
7807 ShiftedI is I + IShift,
7808 assertz(atom_integer_extension((ShiftedT:A),ShiftedI)),
7809 fail.
7810
7811enumerate_atom_extension(Time,MaxTime,Shift) :-
7812 Time2 is Time + 1,
7813 enumerate_atom_extension(Time2,MaxTime,Shift).
7814
7815write_shifted_clauses(_,_,_) :-
7816 assertz((clause(C) :- clause0(C))),
7817 fail.
7818
7819write_shifted_clauses(0,_,_) :- !.
7820
7821write_shifted_clauses(_,_,_) :-
7822 assertz((clause(C) :- clause1(C))),
7823 fail.
7824
7825write_shifted_clauses(1,_,_) :- !.
7826
7827write_shifted_clauses(MaxTime,Shift,Base) :-
7828 write_shifted_clauses(2,MaxTime,Shift,Base).
7829
7830write_shifted_clauses(Time,_MaxTime,Shift,Base) :-
7831 TShift is (Time - 1) * Shift,
7832 assertz(( clause(C) :-
7833 clause1(C1),
7834 map_clause_shift(C1,TShift,Base,C) )),
7835 fail.
7836
7837write_shifted_clauses(MaxTime,MaxTime,_,_) :- !.
7838
7839write_shifted_clauses(Time,MaxTime,Shift,Base) :-
7840 Time1 is Time + 1,
7841 write_shifted_clauses(Time1,MaxTime,Shift,Base).
7842
7844map_clause_shift([],_,_,[]).
7845map_clause_shift([M|Ms],Shift,BC,[N|Ns]) :-
7846 ( M > 0
7847 -> ( M =< BC
7848 -> N = M
7849 ; N is M + Shift )
7850 ; P is 0 - M,
7851 ( P =< BC
7852 -> N = M
7853 ; N is M - Shift ) ),
7854 map_clause_shift(Ms,Shift,BC,Ns).
7855
7856
7857
7861
7865
7866system_value(Call) :- system(Call,_Value).
7867
7868
7873
7874time_system(Call,Time) :- time_system(Call,nobackground,Time).
7875
7879
7880time_system(Call,nobackground,Time) :-
7881 common_tmpname(Temp),
7882 format_to_atom(Call2,"(time sh -c '~w') 2> ~w",[Call,Temp]),
7883 system_value(Call2),
7884 safe_see(Temp),
7885 parse_time(Time), !,
7886 seen,
7887 common_file_delete(Temp).
7888
7893
7894time_system(Call,background,Time) :-
7895 common_tmpname(Time),
7896 format_to_atom(Call2,"(time sh -c '~w') 2> ~w &",[Call,Time]),
7897 system_value(Call2).
7898
7903
7904time_system(Call,background,Time,Lockfile) :-
7905 common_tmpname(Lockfile),
7906 format_to_atom(LockCall,"lockfile ~w",[Lockfile]),
7907 system_value(LockCall),
7908 common_tmpname(Time),
7909 format_to_atom(BkgdCall,"((time sh -c '~w') 2> ~w ; rm -f ~w) &",
7910 [Call,Time,Lockfile]),
7911 system_value(BkgdCall).
7912
7914
7915wait(Lockfile) :-
7916 format_to_atom(Call,"lockfile ~w ; rm -f ~w",[Lockfile,Lockfile]),
7917 system_value(Call).
7918
7919
7921
7922parse_time(Time) :-
7923 read_line(Line),
7924 ( Line == end_of_file
7925 -> !, fail
7926 ; ( prefix(Line,"user",RestLine)
7927 ; prefix(Line,"sys",RestLine) ),
7928 drop_spaces(RestLine,TimeStr),
7929 ( ( between(TimeStr,HrStr,RestTimeStr,":"),
7930 between(RestTimeStr,MinStr,SecStr,":")
7931 ; between(TimeStr,HrStr,RestTimeStr,"h"),
7932 between(RestTimeStr,MinStr,RestTimeStr2,"m"),
7933 between(RestTimeStr2,SecStr,_,"s") )
7934 -> get_number(HrStr,Hr,_),
7935 get_number(MinStr,Min,_),
7936 get_number(SecStr,Sec,_),
7937 Time1 is 3600*Hr+60*Min+Sec
7938 ; ( between(TimeStr,MinStr,SecStr,":")
7939 ; between(TimeStr,MinStr,RestStr,"m"),
7940 between(RestStr,SecStr,_,"s") )
7941 -> get_number(MinStr,Min,_),
7942 get_number(SecStr,Sec,_),
7943 Time1 is 60*Min+Sec
7944 ; get_number(TimeStr,Time1,_) ),
7945 ( parse_time(Time2)
7946 -> Time is Time1 + Time2
7947 ; Time is Time1 )
7948 ; parse_time(Time) ).
7949
7950
7953
7954make_pipe(P) :-
7955 common_tmpname(P),
7956 format_to_atom(Call,"mkfifo ~w",[P]),
7957 system(Call).
7958
7959
7962
7963rm_pipe(P) :-
7964 ( atom(P),
7965 ( common_file_exists(P)
7966 -> common_file_delete(P)
7967 ; true ) ).
7971
7972
7973
7977
7978print_stream(P) :-
7979 current_input(C),
7980 set_input(P),
7981 repeat,
7982 read_line(L),
7983 ( L \= end_of_file
7984 -> format("~s~n",[L]),
7985 fail
7986 ; true ),
7987 set_input(C).
7988
7989
7995
7996close_all_streams :-
7997 value(ccalc_dir,CCDir),
7998 format_to_atom(CCalcName,"~wccalc.pl",[CCDir]),
7999 ( current_stream(F,_,S),
8000 \+ integer(F),
8001 F \= '',
8002 F \= CCalcName,
8003 close(S),
8004 fail
8005 ; true ).
8006
8007
8008%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
8009%% Other Utilities
8010%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
8011
8012%-----------------------------------------------------------------------------%
8013% check_grules
8014%-----------------------------------------------------------------------------%
8015
8016check_grules :-
8017 (A<=B),
8018 ( common_ground((A<=B))
8019 -> true
8020 ; nl, write('Not Ground: '), write((A<=B)) ),
8021 fail.
8022check_grules.
8023
8024
8025%-----------------------------------------------------------------------------%
8026% show_grules
8027%-----------------------------------------------------------------------------%
8028
8029show_grules :-
8030 (A<=B),
8031 nl,
8032 write((A<=B)),
8033 fail.
8034show_grules.
8035
8039
8040max(A, B, C) :- ( A < B -> C = B; C = A ).
8041max(A, B, C, D) :- max(A,B,E), max(E,C,D).
8042
8043min(A, B, C) :- ( A < B -> C = A; C = B ).
8044
8045
8049
8050functor_spec(Spec) :-
8051 Spec = F/N, atom(F), integer(N), N >= 0,
8052 domain_schema(_,L), functor(T,F,N), member(T,L).
8053
8054
8058
8059close_abort :- seen, told, ( value(noabort,true) -> fail ; abort ).
8060
8061
8065
8066next_time(T,N,T) :- T =< N.
8067next_time(M,N,T) :- M < N, M1 is M+1, next_time(M1,N,T).
8068
8069next_time(T,T).
8070next_time(M,T) :- M1 is M+1, next_time(M1,T).
8071
8072
8076
8077prefix([C|Cs],[C|Ps],After) :-
8078 prefix(Cs,Ps,After).
8079prefix(Cs,[],Cs).
8080
8081
8085
8086common_sublist([],[]).
8087common_sublist([E|Sublist],[E|List]) :-
8088 common_sublist(Sublist,List).
8089common_sublist(E,[_|List]) :-
8090 common_sublist(E,List).
8091
8092
8096
8097exact_sublist(List,Pat,After) :-
8098 prefix(List,Pat,After).
8099exact_sublist([_|Cs],Pat,After) :-
8100 exact_sublist(Cs,Pat,After).
8101
8102
8106
8107between(List,Before,After,Between) :-
8108 exact_sublist(List,Before,Rem1),
8109 prefix(Rem1,Between,Rem2),
8110 prefix(Rem2,After,_).
8111
8112
8116
8118print_list([L|Ls]) :-
8119 ( is_list(L)
8120 -> print_list(L)
8121 ; format("~n~w ", [L])),
8122 print_list(Ls).
8123print_list([]) :-
8124 format("~n",[]).
8125
8129
8130
8134
8135member_check(X,[X|_Xs]) :- !.
8136member_check(X,[Y|Ys]) :- X \= Y, member_check(X,Ys).
8137
8138
8142
8143display_atoms([L|Ls]) :-
8144 atom_integer(A, L),
8145 format("~w ", [A]),
8146 display_atoms(Ls).
8147display_atoms([]) :- format("~n", []).
8148
8149
8153
8154subtract([], _, []).
8155subtract([Element|Elements], Set, Difference) :-
8156 member_check(Element,Set),
8157 !,
8158 subtract(Elements, Set, Difference).
8159subtract([Element|Elements], Set, [Element|Difference]) :-
8160 subtract(Elements, Set, Difference).
8161
8162ordered_memberchk(X,[X|_]) :- !.
8163ordered_memberchk(X,[Y|Ys]) :-
8164 X > Y,
8165 ordered_memberchk(X,Ys).
8166
8167
8168append_to_each(_,[],[]).
8169
8170append_to_each(K,[C|Cs],[[K|C]|Cs2]) :-
8171 append_to_each(K,Cs,Cs2).
8172
8173
8177
8178:- set_dirs. 8179:- initialize. 8180:- reset_options. 8181:- format("~n~nCausal Calculator: Version 2.0.~n",[]). 8182:- format("Type 'help.' for online help.~n~n~n",[]).