1% Program: The Causal Calculator
    2% File: ccalc.pl
    3% Version: 2.0
    4% Language: SISCtus Prolog 3.7.1, SWI Prolog 5.2.3
    5% Date: 12/6/1997
    6% Last Revised: 4/7/2003
    7
    8% Determine which version of Prolog is being used and load the appropriate
    9% include file for CCalc.  Each supported version of Prolog implements either
   10% the current_prolog_flag/2 or prolog_flag/2 predicate, but not both, so both
   11% must be checked to ensure compatibility.
   12/*
   13:- ( predicate_property(current_prolog_flag(_,_),built_in)
   14     -> current_prolog_flag(version,Ver)
   15   ; predicate_property(prolog_flag(_,_),built_in)
   16     -> prolog_flag(version,Ver)
   17   ; format("Error: CCalc must be run under SICStus Prolog 3.7.1 or~n",[]),
   18     format("   later, or SWI-Prolog 3.3.4 or later.~n",[]),
   19     close_abort ),
   20   name(Ver,VerName),
   21   % test whether version name starts with "SICStus"
   22   ( VerName = [0'S,0'I,0'C,0'S,0't,0'u,0's|_]
   23     -> ensure_loaded('sicstus.pl')
   24   ; ensure_loaded('swi.pl') ).
   25*/
   26%:- module(ccalc,[]).
   27is_sicstus:- \+ current_prolog_flag(version_data,swi(_,_,_,_)).
   28
   29%?- is_sicstus -> prolog_flag(single_var_warnings,_,off) ; true.
   30
   31?- is_sicstus -> ensure_loaded('sicstus.pl') ; ensure_loaded('swi.pl') .   32
   33% dynamic predicates differ from the others in that they can be modified while
   34%  the program is running. We use dynamic predicates to store some 
   35%  information in the database.
   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,
   42%   integer_atom/2, integer_atom_extension/2, saved_integer_atom/2, 
   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 )).  % value is not totally retracted during initialization
   48
   49
   50% <= is for storing rules
   51% <- is for storing query rules 
   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
   60%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   61%% loadf(+File) : main routine for reading input files and grounding them. 
   62%%     File : either a single file name in atom, or multiple files in list 
   63%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   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,   % construct domain/2, which is a database of 
   76                        %  sort vs ground instances 
   77   ( show_spec(S) 
   78     -> \+ \+ valid_spec(S)
   79   ; true ),
   80
   81   enumerate_atoms,     % construct hash table for 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,  % generate grounded rules
   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),   % this also involves translation of 
  100                                          %  multi-valued logic to 
  101                                          %  propositional logic
  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  
  126%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  127%% include_file(File,IncludeDir,RuleSchema)
  128%% (second argument is optional)
  129%%
  130%% File : either a single file name in atom, or multiple files in list format.
  131%% IncludeDir: directory to include in the search path (used when one input
  132%%   file includes another)
  133%% RuleSchema: 0 => read static laws at time 0
  134%%             1 => read static laws at time 1 & dynamic laws
  135%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  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
  147%^ dis: should disallow a list of list.
  148
  149% single file name
  150include_file(File,IncludeDir,RuleSchema) :- 
  151   \+ list(File),   % instead of atom(File), for swi compatibility on []
  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
  169%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  170%% determine_full_filename(File,IncludeDir,FullName) :
  171%% (second argument is optional)
  172%%    When a file is loaded, try these directories in order:
  173%%       IncludeDir, which is the directory containing the file currently
  174%%          being read in the case of an include statement inside another file
  175%%       None (i.e. take File as an absolute filename)
  176%%       The current working directory in the Unix shell
  177%%       The value of the user-specified 'dir' option
  178%%       The directory from which CCalc was loaded
  179%%    If the file doesn't exist in any of these locations, return an error.
  180%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  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
  201% determine_path(Filename,Path) takes a Filename, and returns the Path to
  202% that filename, which is the whole filename up to and including the final
  203% slash (but not anything after that)
  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) :-  % 47 is code for slash
  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
  226%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  227%% read_file(+Files) : read files 
  228%% 
  229%%   The mode is set to the basic mode by default. First read 'static0.std'.
  230%%   This declares basic objects and an exogenieity assumption for initial
  231%%   states. Then read the main Files. The rules (schema) will be stored in 
  232%%   rule_schema/1. While reading them, as soon as history mode condition 
  233%%   is detected, CCalc will turn into history mode. If dynamic laws are 
  234%%   detected in the middle, they'll be skipped in this first reading.
  235%%   But after then, CCalc will turn into the transition mode and read 
  236%%   Files again for the dynamic laws to be stored in rule_schema1/1 for 
  237%%   later shifting. If additive constants are used, CCalc will process 
  238%%   additive files.
  239%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  240
  241read_file(Files) :-
  242   include_file('static0.std',0), 
  243   iset(dynamic_detected,false),  % static0 contains sdFluent
  244   include_file(Files,0), % the mode will turn to history mode if 
  245                              % the files contain macros maxstep outside
  246                              % query 
  247   ( (value(dynamic_detected,true), \+ value(mode,history))
  248     -> iset(mode,transition), 
  249        filter_static1_dynamic(Files)  % this will store in rule_schema1
  250   ; true ),
  251
  252   ( value(additive_detected,true)  % if additive fluent or action is detected
  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
  280%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  281%% read and dispatch 
  282%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  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
  376/*
  377include_file0(File,IncludeDir) :- 
  378   \+ list(File),   % instead of atom(File), for swi compatibility on []
  379   !,
  380   seeing(OldInput),
  381   ( determine_full_filename(File,IncludeDir,AbsFile)
  382     -> true
  383   ; fatal_error("File \'~w\' not found.",[File]) ),
  384   ( (RuleSchema==1 ; 
  385      member(File,['static0.std']))
  386     -> true
  387   ; write('% loading file '),
  388     write(AbsFile), nl ), 
  389   flush_output,
  390   safe_see(AbsFile),
  391   read_pass(RuleSchema),
  392   seen, 
  393   see(OldInput).
  394*/
  395
  396     
  397%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  398%% dispatch to declaration handlers 
  399%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  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
  517%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  518%% declaration handlers
  519%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  520
  521%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  522%% process_macros: Read :- macro section and store them in macro/3.
  523%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  524
  525process_macros((A;B)) :-
  526   !, 
  527   process_macros(A), 
  528   process_macros(B).
  529
  530% for compatibility
  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  % doesn't need to include this as a macro
  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
  555%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  556% subst_vars_for_macro_vars(C,D,Vs) : substitute prolog 
  557%    variables (e.g., _29599) for macro variables (e.g., #1)
  558%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  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
  576%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  577% subst_free
  578% substitute free variables in Term into Prolog variable. 
  579% Doesn't do anything with bound variables.
  580% substitution is done with respect to substitution list Sub.
  581%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  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
  619%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  620% subst_functor(F,G,T,NT) : substitute functor
  621%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  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
  643%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  644%% type checking procedures : may be used in where condition 
  645%%  in macro expansion 
  646%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  647
  648%-----------------------------------------------------------------------------%
  649% composite_sort(+S) : check whether sort name S is a composite sort
  650%-----------------------------------------------------------------------------%
  651
  652complex_sort(S) :-  
  653   functor(S,_,1), !. 
  654
  655%-----------------------------------------------------------------------------%
  656% composite_sort(+S) : check whether sort name S is a composite sort
  657%-----------------------------------------------------------------------------%
  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
  673%-----------------------------------------------------------------------------%
  674% constant(+C) : check whether C is a constant
  675%-----------------------------------------------------------------------------%
  676
  677% macro
  678is_constant(var(Sort,_)) :- 
  679   composite_sort(Sort), !. 
  680
  681% variable
  682is_constant(C) :-  
  683   var_sort(C,Sort), composite_sort(Sort), !.
  684
  685% name
  686% To speed up, we only check the name of functor and arity, but 
  687%  don't check if the arguments belong to appropriate sorts. 
  688%  This doesn't allow distinguishing two constants with the same 
  689%  functor and arity, but it doesn't seem to be much problem
  690is_constant(C) :- 
  691   !,
  692   functor(C,F,N),
  693   consts(F,N).   % refers to constants database
  694
  695%-----------------------------------------------------------------------------%
  696% object(+C) : check whether C is an object
  697%-----------------------------------------------------------------------------%
  698
  699object(O) :-
  700   functor(O,F,N), 
  701   objs(F,N).
  702
  703%-----------------------------------------------------------------------------%
  704% expr(+C) : 
  705%    check whether C is an expression that wil
  706%    It's also used to substitute values for constants where constants
  707%    are used in place of values. (e.g., C1+C2 )
  708%-----------------------------------------------------------------------------%
  709
  710expr(-(Expr)) :- expr(Expr), !.
  711
  712expr(Expr) :-
  713  functor(Expr,F,2),      % binary operator
  714  !,
  715  member_check(F,['+','-','*','/','//','rem','mod','gcd','min','max','**',
  716            '>','<','=<','>=','=']).
  717
  718expr(Expr) :-          
  719   functor(Expr,F,1),     % unary operator
  720   !,
  721   member_check(F,['abs']).
  722
  723
  724%-----------------------------------------------------------------------------%
  725% rigid(+R) : check whether R is a rigid constan
  726%-----------------------------------------------------------------------------%
  727
  728% macro
  729rigid(var(rigid(_S),_)) :- !.  
  730
  731% variable
  732rigid(R) :- % variable  %^jo- problem?
  733   var_sort(R, rigid(_)), !.
  734
  735% name - similar to constant
  736rigid(R) :-
  737   !,
  738   functor(R,F,N),
  739   rigids(F,N).
  740
  741
  742%-----------------------------------------------------------------------------%
  743% rigid_atom(+R) : check whether R is a rigid atom. 
  744%                   used to skip putting the rule with a rigid atom in the 
  745%                   head in rule_schema1 in transition mode
  746%-----------------------------------------------------------------------------%
  747
  748rigid_atom(R) :-   % boolean
  749   rigid(R), !.
  750rigid_atom(-R) :-  % boolean
  751   rigid(R), !.    
  752rigid_atom(R eq _) :-
  753   rigid(R), !.
  754rigid_atom(R = _) :-
  755   rigid(R), !.
  756
  757
  758%-----------------------------------------------------------------------------%
  759% composite_var(+V) : check whether V is a variable for composite sor
  760%-----------------------------------------------------------------------------%
  761
  762composite_var(V) :-
  763   var_sort(V,Sort),
  764   composite_sort(Sort), !.
  765
  766
  767%-----------------------------------------------------------------------------%
  768% is_var(+V) : check whether V is a variable
  769%-----------------------------------------------------------------------------%
  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
  788%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  789%% constants
  790%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  791
  792%-----------------------------------------------------------------------------%
  793% simpleFluent_constant(+C) : 
  794%    Checks whether C is a simple fluent constant.
  795%-----------------------------------------------------------------------------%
  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
  812%-----------------------------------------------------------------------------%
  813% sdFluent_constant(+C) : 
  814%    Checks whether C is a statically determined fluent constant.
  815%-----------------------------------------------------------------------------%
  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
  832%-----------------------------------------------------------------------------%
  833% fluent_constant(+C) : 
  834%    Checks whether C is a statically determined fluent constant.
  835%-----------------------------------------------------------------------------%
  836
  837fluent_constant(C) :-
  838   ( simpleFluent_constant(C); sdFluent_constant(C) ). 
  839
  840
  841%-----------------------------------------------------------------------------%
  842% action constants
  843%-----------------------------------------------------------------------------%
  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
  869%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  870%% atoms
  871%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  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
  902%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  903%% formulas
  904%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  905
  906%-----------------------------------------------------------------------------%
  907% simpleFluent_formula
  908%-----------------------------------------------------------------------------%
  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
  927%-----------------------------------------------------------------------------%
  928% fluent_formula
  929%-----------------------------------------------------------------------------%
  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
  949%-----------------------------------------------------------------------------%
  950% action formula
  951%-----------------------------------------------------------------------------%
  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
  974%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  975%% has_no_constants(Formula) 
  976%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  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
  998%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  999%% process_sorts
 1000%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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 % compatible([S|As],[S|Bs]) 
 1022                  %^jo- multiple inheritance without common supersort 
 1023                  %     is now allowed. - potential error?
 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
 1047%^jo common ancestor check. Why was it necessary?
 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
 1056% check whether Sort is predeclared as a sort
 1057
 1058is_sort(Sort) :-
 1059  ( Sort = atomicFormula
 1060    -> true 
 1061  ; find_sort(Sort,_) ).
 1062
 1063
 1064%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1065%% find_sort(+Sort,?Ancestors) Returns the list of ancestors of Sort if found.
 1066%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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) % recursively find
 1075   ; find_sort(Nodes,Sort,As1,As) ).
 1076
 1077%descendant_sort(Child,Child).
 1078
 1079descendant_sort(Child,Ancestor) :-
 1080   find_sort(Child,Ancestor_List), member_check(Ancestor, Ancestor_List).
 1081
 1082
 1083
 1084%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1085%% add_subsort(+Sort,+SubSort) : add subsort SubSort to sort Sort
 1086%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1087
 1088add_subsort(Sort,Sub) :-
 1089   get_ccsorts(Nodes),
 1090   add_subsort(Nodes,Sort,Sub,[],NewNodes),
 1091   put_ccsorts(NewNodes).
 1092
 1093
 1094%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1095%% add_subsort(OldNodes,Sort,Sub,Ancestors,NewNodes1) :
 1096%%   replace OldNodes by NewNodes1 whose Sort node includes Sub in its subsort list
 1097%    Ancestors used to keep record to check cycle in sorts declaration
 1098%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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      % if Sort is the right super sort to add the subsort Sub
 1105     -> ( member(Sub,[S|Ancestors])
 1106          -> report_cycle([S|Ancestors],Sub)
 1107        ; ( member(node(Sub,_),NewSubs)  % if the subsort is already 
 1108                                         % in the subsort list of the node
 1109            -> NewSubs1 = NewSubs        % no change in the subsort list
 1110            ;  ( find_sort(Sub,_), find_nodes([Sub],SubNodes)
 1111                 -> append(NewSubs,SubNodes,NewSubs1)
 1112                 ;  append(NewSubs,[node(Sub,[])],NewSubs1) ) ), 
 1113                    % otherwise add the subsort Sub
 1114                    % to the subsort list
 1115
 1116   	  NewNodes1 = [node(S,NewSubs1)|NewNodes] )  % construct new node which include
 1117                                                     % the new subsort
 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
 1129%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1130%% declare_composite_sorts : declare composite sorts for each sort 
 1131%%             introduced. processed just after process_sorts
 1132%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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
 1206%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1207%% process_variables
 1208%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1209
 1210% Note: is_sort(S) is to check that sort declarations
 1211% precede var declarations in included problem files.
 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)   % if V is already declared as a variable of 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
 1263%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1264%% process_objects
 1265%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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))  % if C is already in domain_schema
 1287      -> true                             % just skip
 1288   ; ( retract(domain_schema(S,Cs))       % otherwise insert C
 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), %^%^ (S \== boolean),
 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
 1325% generate_range_sort(+M,+N,-RangeSort) 
 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)),  % integer >> RangeSort? 
 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
 1349%-----------------------------------------------------------------------------%
 1350% process additive
 1351%-----------------------------------------------------------------------------%
 1352
 1353% assert rule schemas for every additive fluent and action
 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), % M and N is the range
 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), % M and N is the range
 1367   fail.
 1368process_additive.
 1369
 1370
 1371%-----------------------------------------------------------------------------%
 1372% additive fluents and actions
 1373%-----------------------------------------------------------------------------%
 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
 1387% check duplicates
 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
 1407%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1408%% process_constants
 1409%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1410
 1411%-----------------------------------------------------------------------------%
 1412% register_constants(C): construct consts/2 to speed up deciding
 1413%                         if something is a constant
 1414%-----------------------------------------------------------------------------%
 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
 1424%-----------------------------------------------------------------------------%
 1425% register_rigids(C): construct rigids/2 to speed up deciding
 1426%                         if something is a rigid constant
 1427%-----------------------------------------------------------------------------%
 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
 1438%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1439% register_boolean_constants(C): construct boolean_constants/2 
 1440%  to speed up deciding if something is a boolean constant
 1441%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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
 1453%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1454%% process_constant : process constant declaration section
 1455%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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
 1611%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1612%% Conversion
 1613%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1614
 1615%-----------------------------------------------------------------------------%
 1616%  sorts_to_vars(+Sorts,-Vars) : Transform a list of sort names to a list of
 1617%      corresponding distinct variables.
 1618%      tail recursion
 1619%-----------------------------------------------------------------------------%
 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
 1634%-----------------------------------------------------------------------------%
 1635%  vars_to_sorts(+Vars,-Sorts) : Transform a list of variables to a list of
 1636%      corresponding sort names in a tail recursive way
 1637%-----------------------------------------------------------------------------%
 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
 1650%-----------------------------------------------------------------------------%
 1651%  tuples_to_conjs(+Tuples,-Conjs) : Transform a list of Tuple to a list of
 1652%      corresponding conjunction in a tail recursive way
 1653%-----------------------------------------------------------------------------%
 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
 1666%-----------------------------------------------------------------------------%
 1667%  consts_to_sorts(+Consts,-Sorts) : Transform a list of Constants to a list of
 1668%      corresponding sort names in a tail recursive way
 1669%-----------------------------------------------------------------------------%
 1670
 1671% const_to_sort(C,S) : convert const into sort . inefficient
 1672
 1673const_to_sort(C,S) :- domain(S,Cs), member(C,Cs).
 1674
 1675%-------
 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
 1727%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1728%% process_include
 1729%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1730
 1731process_include((A;B)) :-
 1732   !,
 1733   process_include(A), 
 1734   process_include(B).
 1735
 1736/*
 1737process_include((A:[(S->S1)|Ls])) :-
 1738   !,
 1739%   ( determine_full_filename(A,_IncludeDir,AbsFile)
 1740%     -> true
 1741%   ; fatal_error("File \'~w\' not found.",[A]) ),
 1742%   format_to_atom(RenCmd,"mv ~w ~w", [A,tmp]),
 1743%   system(RenCmd),
 1744   format_to_atom(ReplaceCmd, "sed 's/~w/~w/g' ~w > ~w.~w",[S,S1,A,A,S1]),
 1745   system(ReplaceCmd),
 1746   append_name(A,'.', Adot),
 1747   append_name(Adot,S1,A1),
 1748   process_include((A1:Ls)).
 1749
 1750process_include((A:[])) :-
 1751   process_include(A).
 1752*/
 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  % doesn't need to include this as a macro
 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
 1792%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1793%% process_show
 1794%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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
 1837% valid_show_spec appears to perform a task similar to valid_spec, except
 1838% that valid_show_spec is called when no objects have been defined yet, in
 1839% which case terms can't be grounded to determine if they're valid specs
 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
 1872%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1873%% process_tests
 1874%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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
 2002%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2003%% insert rules 
 2004%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2005
 2006%-----------------------------------------------------------------------------%
 2007% insert_rule_schema
 2008%-----------------------------------------------------------------------------%
 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
 2018%-----------------------------------------------------------------------------%
 2019% insert_inertia_rules
 2020%-----------------------------------------------------------------------------%
 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
 2042%-----------------------------------------------------------------------------%
 2043% insert_attribute_rules
 2044%-----------------------------------------------------------------------------%
 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
 2153%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2154%% instantiate_sorts : ground domain_schema/2 to produce domain/2
 2155%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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,_)  % skip since already constructed
 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]),  % subs first
 2169     ( domain_schema(S,Cs) 
 2170       -> true 
 2171     ; Cs = [] ),
 2172     instantiate_sorts_in_terms(Cs,Ancestors), % in args
 2173     instantiate_terms(Cs,Es1),
 2174     subsorts_extension(Subs,Es2),   % after instantiate_sort(Subs,_) above
 2175                                     % subsorts_extension(Subs,_) returns
 2176                                     % all subsorts of Sort S
 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
 2186%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2187%% instantiate_sorts_in_terms(
 2188%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2189
 2190instantiate_sorts_in_terms([],_Ancestors).
 2191
 2192instantiate_sorts_in_terms([C|Cs],Ancestors) :-
 2193   C =.. [_|Sorts],  % arguments
 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
 2205%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2206%% find_nodes(+Sorts,-Nodes) 
 2207%%   Sorts : a list of sorts
 2208%%   Nodes : corresponding nodes in ccsorts
 2209%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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
 2222%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2223%% find_node(+Graph,+Sort,-Nodes) : find node for Sort in ccsorts Graph
 2224%%   Graph : ccsorts in process
 2225%%   Sort  : sort name
 2226%%   Nodes : corresponding nodes in ccsorts
 2227%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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
 2237%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2238%% subsorts_extension(+Subs,-Es) : returns all ground instances in domain/2
 2239%%                                 of nodes in Subs
 2240%%  Subs : list of nodes in ccsorts
 2241%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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
 2250%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2251%% instantiate_terms(+Cs,-Ds) : Cs : [alive(turkey)] Ds : [alive(turkey1) alive(turkey2)]
 2252%%   Cs : list of objects or constants whose arguements are sort names
 2253%%   Ds : list of objects or constants whose arguements are replaced 
 2254%%          with ground instances
 2255%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2256%findall(on(_21109,_21110),user:bind_vars_to_terms([_21109=[a,b],_21110=[a,b,table]]),[on(a,a),on(a,b),on(a,table),on(b,a),on(b,b),on(b,table)|_23722],_23722) 
 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
 2297%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2298%% enumerate_atoms
 2299%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2300%
 2301% Determines all ground atoms in the theory, based on the object and
 2302% constant declarations.  Each atom will be assigned an integer (in
 2303% an unbroken sequence).  After all atoms have been enumerated, the variable
 2304% atom_count will be set to the number of atoms.  The variable
 2305% original_atom_count is also set to the number of atoms; while atom_count
 2306% will be incremented as new atoms are added during rule grounding
 2307% and completion, original_atom_count will not, and it will therefore always
 2308% show the number of "real" atoms (not auxiliary atoms) in the theory.
 2309%
 2310% In transition mode, some atoms will need to be shifted to later time units
 2311% during the query process; it is therefore necessary to enumerate the atoms
 2312% in a manner which makes it clear which atoms should be shifted and which
 2313% should not.  This is accomplished by first enumerating all atoms
 2314% corresponding to rigid constants, then fluents at time 0, then actions and
 2315% attributes at time 0, and finally fluents at time 1.  At the end of the
 2316% procedure, the variables atom_count and original_atom_count are set as above.
 2317% In addition, rigid_count, fluent_count, and action_count will store the
 2318% number of rigid constants, fluents, and actions, respectively.  (The latter
 2319% two represent the number of fluents or actions at *each* time step, not
 2320% the total number.)  Also, static0_atom_count will store the number of rigid
 2321% constants and fluents together; this is the number of atoms at the start of
 2322% the sequence which will not need to be shifted during a query.
 2323%
 2324% History and basic mode don't need shifting, but the atoms are still processed
 2325% in the same order, continuing the pattern beyond time step 1.  The
 2326% show_models procedure relies on this ordering for efficient display of
 2327% solutions.  The various atom counts stored for transition mode aren't stored
 2328% for the other modes -- only atom_count and original_atom_count.
 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
 2394%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2395%% renumber atoms prior to shifting
 2396%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2397
 2398renumber_atoms :-
 2399
 2400   % During rule grounding and completion, new atoms may be introduced to
 2401   % simplify some of the clauses.  These atoms will be added to the end of
 2402   % the sequence.  However, some of these new atoms appear in clauses
 2403   % corresponding to time step 0 and don't need to be shifted during
 2404   % transition mode.  We need to
 2405   % move these atoms down to the portion of the atom sequence which isn't
 2406   % shifted.  Also, since new atoms for time 0 will appear before
 2407   % fluents for time 0, we need to move new atoms for time 1 to appear
 2408   % before fluents for time 1, so that each time unit is shifted the same
 2409   % way.  The sequence of atoms looks like the following:
 2410   %
 2411   %     Before shift:			After shift:
 2412   %     -------------			------------
 2413   %     Rigid constants		Rigid constants
 2414   %     Fluents at time 0		New atoms for time 0 (from rules
 2415   %     Actions/attributes at time 0	   & completion)
 2416   %     Fluents at time 1		Fluents at time 0
 2417   %     New atoms from rules		Actions/attributes at time 0
 2418   %        (time 0 & 1)		New atoms for time 1 (from rules
 2419   %     New atoms from completion	   & completion)
 2420   %        (time 0 & 1)		Fluents at time 1
 2421   %
 2422   % Several counters were set during enumeration of the atoms which tell how
 2423   % large each section is: rigid_count, fluent_count, action_count,
 2424   % and new_atom_count hold the number of rigid fluents, fluents,
 2425   % actions/attributes, and new atoms, respectively.
 2426   % static0_new_atom_count holds the number of auxiliary atoms corresponding
 2427   % to time unit 0 only.
 2428   %
 2429   % After this procedure has completed, static0_atom_count will be changed
 2430   % to reflect the total number of atoms which will not be shifted, including
 2431   % new atoms of both kinds.
 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   % The Level variables store the highest index for each type of atom, and
 2443   % the Shift variables store the amount by which that type will be shifted.
 2444   % See the table above for a depiction of the relative ordering of atom
 2445   % types before and after shifting.
 2446   %
 2447   % atoms with an index <= Level1 won't be moved -- these are rigid constants
 2448   % atoms with Level1 < index <= Level2 will be shifted upward -- these are
 2449   %    fluents at time 0 and actions/attributes at time 0
 2450   % atoms with Level2 < index <= Level3 will be shifted upward -- these are
 2451   %    fluents at time 1
 2452   % atoms with Level3 < index <= Level4 will be shifted downward to the gap
 2453   %    above Level1 -- these are new atoms generated by rules at time 0
 2454   % atoms with Level4 < index <= Level5 will be shifted downward to the gap
 2455   %    above Level2 -- these are new atoms generated by rules at time 1
 2456   % atoms with Level5 < index <= Level6 will be shifted downward to the gap
 2457   %    between Level4 and Level1 -- these are new atoms generated by 
 2458   %    completion at time 0
 2459   % atoms with index > Level6 will be shifted downward to the gap between
 2460   %    Level4 and Level2 -- these are new atoms generated by completion at
 2461   %    time 1
 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,   % NAR includes NAR0 + NAR1
 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   % For each clause, shift all of the literals in the clause to match the
 2514   % shifted atoms
 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
 2539%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2540%% Procedures used in process_rule_schemas
 2541%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2542
 2543%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2544%% decode_macro 
 2545%% ex) (p=var(sort(p))<=p=var(sort(p))&&p=var(sort(p)))
 2546%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2547
 2548% generate a variable V_Sort_Identifier and assert
 2549get_var(Sort,Identifier,Var) :-  
 2550   name('V',[ListV]),
 2551   name('_',[ListUS]),
 2552   ( Sort =.. [F,A]
 2553     -> name(F,ListF),
 2554        ( A =.. [A1,R]  % disk*
 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
 2578% need to be changed
 2579get_sort(Var,ValSort) :-
 2580   atom(Var), 
 2581   var_sort(Var,CompositeSort), 
 2582   !, % variable
 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
 2628%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2629%% expand_boolean % this should be done when the constant isn't an argument
 2630%% ex) edge(0,2) -> edge(0,2)eq true , before binding
 2631%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2632% macro
 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
 2639% variable
 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
 2647% name
 2648boolean_constant(C) :-
 2649   !,
 2650   functor(C,F,N),
 2651   boolean_constants(F,N).
 2652
 2653
 2654% should be top down construction 
 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
 2751%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2752%% postprocessing_after_binding
 2753%% ex) edge(1,1+2) -> edge(1,3)
 2754%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2755% as soon as arguments are evaluated, C = V -> C eq V is done.
 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
 2790%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2791%% replace_false_with_negative_literal
 2792%% ex) edge(0,2) eq false -> -(edge(0,2) eq true) after binding
 2793%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2794%^ macro would be better? - no it's slower
 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
 2818%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2819
 2820%^ note
 2821%^ decode macro and expand boolean put together; conflict - 
 2822%^ decode-macro should be bottom up for var processing
 2823%^ while expand-boolean should be top-down to avoid(/\A eq true)
 2824
 2825%%%%%%%%%%%%%%%%%%%%%%
 2826% evaluable_expr(+Expr) : check whether Expr is an evaulable expression
 2827%                        used in eval_expr
 2828%%%%%%%%%%%%%%%%%%%%%%
 2829evaluable_expr(Expr) :- number(Expr), !.
 2830%evaluable_expr(Expr) :- var_sort(Expr,S), \+ composite_sort(S), !.
 2831                           % caused N=1. : in decode_nested_constants_in_rule
 2832evaluable_expr(-(Expr)) :- evaluable_expr(Expr), !.
 2833evaluable_expr(Expr) :-
 2834   functor(Expr,F,2), 
 2835   !,                    % binary operator
 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) :-          % unary operator
 2842   functor(Expr,F,1), 
 2843   !,
 2844   ( member_check(F,['abs'])
 2845     -> arg(1,Expr,FirstArg), evaluable_expr(FirstArg) ).
 2846
 2847
 2848%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2849%% eval_expr
 2850%% ex) edge(1,1+2) -> edge(1,3)
 2851%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2852% as soon as arguments are evaluated, C = V -> C eq V is done.
 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]  % to call prolog to evaluate =
 2862             ; Schema1 = Schema ),          %  in evaluable expression
 2863             ( call(Schema1)
 2864               -> EvaluatedSchema=true
 2865             ; EvaluatedSchema=false )
 2866        ; EvaluatedSchema is Schema)  % otherwise error
 2867   ; functor(Schema,F,N),
 2868     ( ( (F == '='),arg(1,Schema,C),is_constant(C) ) 
 2869          % since decode_nested_constants was executed before, 
 2870          %  the remaining C = X should all turn into C eq X 
 2871          %  if C is a constant
 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
 2889%---------------------------------------------------------------------
 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 == '=')  % instead of =:=. car1=:=car2 will not do; instead car1==car2
 2905                 %  it's okay because the condition will be called after
 2906                 %  evaluating expression arguments.
 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.  % loop ends here
 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
 3114%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 3115% decode_nested_constants(+Formula,-Formula1,-CVs)  
 3116%   Formula:  may contain nested constants
 3117%   Formula1: nested constants are replaced with variables
 3118%   CVs:      a list of (T: C eq V)
 3119%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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           % besides constants, arithmetic expression between constants
 3126           % (e.g., C1+C2 where C1 and C2 are constants) or test 
 3127           % predicates(e.g., nextTo(C1,C2) where nextTo is a user defined
 3128           % constants) should also be considered in unfolding
 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
 3152%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 3153% unfold_nested_constants(+C,-C1,+Acc,-CVs,+Step,?F0,+N0,?Arity0)
 3154%   C: constants or expressions to unfold
 3155%   C1: constant whose nested constants are replaced with variables
 3156%   Acc: accumulation of CVs
 3157%   CVs: a list which contains (T: C eq V) where C is a nested constant
 3158%   Step: time stamp for elements in CVs
 3159%   F0,N0,Arity0 : functor,current argument index and arity of a 
 3160%                  constant that contains this constant C as an argument
 3161%                  used to check whether C should be replaced with a variable.
 3162%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 3163
 3164% exception to unfold nested constants: @< and == are used to 
 3165%   to compare constants themselves, so arguments shouldn't be unfolded
 3166unfold_nested_constants((A@<B),(A@<B),Acc,Acc,_Step,_,_,_) :- !.
 3167unfold_nested_constants((A==B),(A==B),Acc,Acc,_Step,_,_,_) :- !.
 3168
 3169% if K = -1, outermost functor
 3170unfold_nested_constants((T:C),D,Acc,CVs,Step,F0,N0,Arity0) :-
 3171% D may be C1 or V1 depending on whether C itself should be replaced 
 3172%  with a variable
 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                          % if the binding is already in the list
 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) :-
 3190% D may be C1 or V1
 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)  % problem?
 3199                          % if the binding is already in the list
 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
 3219%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 3220% skip_unfolding(+Functor,+N,+Arity): check the condition
 3221%   whether a constant should be replaced with a variable.
 3222%   1. if a constant is the outermost one
 3223%   2. if a constant of composite sort is expected as an argument
 3224%      (e.g., contribution(a,ac))
 3225%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 3226skip_unfolding(_,-1,_) :- !.   % condition 1
 3227skip_unfolding(F,N,Arity) :-   % condition 2
 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
 3267%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 3268%% separate_cvpairs(+CVs,+AccQ,-QCVs,-UCVs)
 3269%%   CVs : a list of (T: C eq V)
 3270%%   AccQ : quantified variables
 3271%%   QCVs : subset of CVS where C contains a variable in AccQ 
 3272%%          (or quantified)
 3273%%   UCVs : subset of CVS where C does not contain a variable 
 3274%%          in AccQ (or unquantified)
 3275%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 3276separate_cvpairs(CVs,AccQ,QCVs,UCVs) :-
 3277   find_unquantified_cvpairs(CVs,AccQ,UCVs),
 3278   subtract(CVs,UCVs,QCVs).
 3279
 3280%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 3281%% find_unquantified_cvpairs(+CVs,+AccQ,-UCVs)
 3282%%   CVs : a list of (T: C eq V)
 3283%%   AccQ : quantified variables
 3284%%   UCVs : subset of CVS where C does not contain a variable
 3285%%          in AccQ (or unquantified)
 3286%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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
 3293%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 3294%% find_cvpairs_containing_quantifier(+Q,+CVs,-QCVs)
 3295%%   Q: quantified variable
 3296%%   CVs: a list of (T: C eq V)
 3297%%   QCVs: subset of CVs where C contains a variable Q
 3298%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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
 3311%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 3312%% constant_has_quantified_variable(C,Va) : check whether
 3313%%     a variable appears as arguments of C
 3314%%   C : constant (from (T: C eq V) in CVs )
 3315%%   Va: variable (from quantified variable list)
 3316%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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
 3343%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 3344% used in macro expansion 
 3345%^ by additive fluent in 'by' clause
 3346%^ doesn't work for now
 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
 3356%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 3357%% decode_nested_constants_in_fact(Formula,Formula1)
 3358%%   : decode nested constants in fact in query.
 3359%%     Differently from a rule, CVs should be explicitly
 3360%%     quantified by universal quantifiers
 3361%%    Formula :  
 3362%%    Formula1: 
 3363%%    ex) 
 3364%%         :- query
 3365%%         0:  c(d(N,N1))
 3366%%       -> Call: decode_nested_constants_in_fact((0:c(d('N','N1'))),_2425) ? s
 3367%%          Exit: decode_nested_constants_in_fact((0:c(d('N','N1'))),[/\'V_boolean-11'|(0:d('N','N1')eq 'V_boolean-11')->>(0:c('V_boolean-11'))]) ? 
 3368%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 3369decode_nested_constants_in_fact(Formula,Formula1) :-
 3370   decode_nested_constants(Formula,Formula2,CVs), 
 3371%   make_univ_quantified_formula_from_cvpairs(Formula2,CVs,Formula1).
 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
 3495%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 3496
 3497% bind_vars/2 is used to bind variables with appropriate constants. 
 3498% Here is a trace showing how bind_vars/2 works:
 3499%+      1      1 Call: bind_vars(['V_F'=_36123]) ? 
 3500%        2      2 Call: var('V_F',_36581) ? 
 3501%        2      2 Exit: var('V_F',fluent) ? 
 3502%        3      2 Call: domain(fluent,_37266) ? 
 3503%        3      2 Exit: domain(fluent,[alive,loaded(g1),loaded(g2)]) ? 
 3504% +      4      2 Call: bind_vars([]) ? 
 3505% +      4      2 Exit: bind_vars([]) ? 
 3506%?+      1      1 Exit: bind_vars(['V_F'=alive]) ?
 3507
 3508%^jo- should this routine be able to handle var(sort(#1))?
 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
 3521% Stage is either 'domain' or 'query', depending on whether it's the domain
 3522% description or the query that's being completed
 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
 3686%%%%
 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
 3721% store_clauses asserts clauses using the appropriate predicate.
 3722% Stage is 'domain' or 'query'; Mode is 'transition', 'basic', or 'history';
 3723% Phase is 0 or 1 (since in transition mode clauses for time 0 and clauses
 3724% for time 1 are asserted using separate predicates, since only the latter
 3725% are shifted to later time units).
 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
 3776%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 3777%% write_clauses_for_eq 
 3778%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 3779
 3780%^jo- domain check > 1 here
 3781% boolean only - apply to other domains with cardinality 2.
 3782
 3783% write_clauses_for_eq can be applied to specific time steps by passing a
 3784% list of steps.  (This is necessary for transition mode, in which clauses
 3785% for time steps 0 and 1 must be generated at different times to avoid
 3786% problems with shifting.)  If write_clauses_for_eq/0 is called, it simply
 3787% passes the value of the entire step domain to write_clauses_for_eq/1.
 3788% Stage is either 'domain' or 'query'.  This parameter determines what should
 3789% be done with the clauses generated if CCalc is in transition mode -- assert
 3790% the clauses in the database if 'domain', or write the clauses directly if
 3791% 'query'.
 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          % find fluent(L) whose value sort L has more than 
 3800          % two objects in its domain
 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   % write clauses for rigid constants only when processing time 0
 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
 4004%   Term = r TermTree3 = col(0)eq 1++col(0)eq 2++col(0)eq 3
 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
 4024%---------------------------------------------------------------------
 4025
 4026%^jo? is_hashed? 
 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	% This is a workaround to handle the dash in satz-rand, which
 4039	% confuses name/2 since atoms can't have dashes
 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
 4050%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 4051%% set(Option,Value) : sets various user options
 4052%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 4053
 4054set(solver,Value) :-
 4055   !,
 4056   lowercase(Value,Value2),
 4057   % check whether choice of solver is a valid choice, and whether current
 4058   % number of interpretations is appropriate for that solver
 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     -> % set 'num' to its current value so that any warnings for this
 4084        % solver/num combination are displayed
 4085        set(num,NumValue)
 4086   ; true ).
 4087
 4088set(num,Value) :-
 4089   % restricts the value of num to a valid choice for the current SAT solver.
 4090   % Some solvers can return only a single interpretation, others can return N
 4091   % interpretations for any integer N, and some can return 'all'
 4092   % interpretations.
 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
 4137% If no solver is currently defined, display a warning if the new value of num
 4138% is other than 1, but set it anyway.
 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   % make sure there's a slash at the end of the path -- add one if not
 4149   format_to_chars("~w",[Value],V),
 4150   common_last(V,C),
 4151   ( C == 47	% check if path ends in a slash
 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
 4188% internal 'set' procedure, for use within ccalc -- doesn't perform any
 4189% error checking
 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 
 4215% - -  - -  - -  - -  - -  - -  - -  - -  - -  - -  - -  - -  - -  - -%
 4216% Calling the sat solvers.
 4217% - -  - -  - -  - -  - -  - -  - -  - -  - -  - -  - -  - -  - -  - -%
 4218
 4219% call_sat sends the input clauses to the SAT solver.  It also calls any
 4220% optional programs being used (e.g. compact and sort).
 4221%
 4222% If file I/O is being used (via the command 'set(file_io,true)'), the input
 4223% is first written to a file; this is passed first to compact (if that option
 4224% is enabled), then to sort (also optional), and finally to the SAT solver.
 4225% If instead pipe I/O is used ('set(file_io,false)', the default), all the
 4226% processes are started running in the background with pipes between them, and
 4227% then the input is written to the first pipe in the chain.
 4228%
 4229% The first argument to call_sat is Notify.  If Notify is not 'notify', all
 4230% output is suppressed.  (This was formerly used to prevent unnecessary output
 4231% when a solution was being verified.  At this time, CCalc no longer supports
 4232% verification, but the Notify argument is still available in case it's needed
 4233% later.)
 4234%
 4235% The other three arguments to call_sat are Out1, Out2, and VarTable.  These
 4236% are output arguments which will contain the streams corresponding to the
 4237% output files/pipes from the SAT solver.  Only mchaff uses both Out1 and Out2;
 4238% the other solvers leave Out2 unbound.  If compact finds a solution on its
 4239% own, Out1 will contain either "SAT" or "UNSAT" instead of a stream.
 4240% VarTable holds the stream containing the variable table generated by compact
 4241% if it's being used, and is unbound otherwise.
 4242
 4243% Out1 is either "SAT" or "UNSAT" if compact solved the problem, or a stream
 4244% containing the first output file from the SAT solver otherwise.  Out2 is a
 4245% stream containing the second output file if the solver is mchaff, and is
 4246% unbound otherwise.  VarTable is a stream containing the variable table from
 4247% compact if it's used, and unbound otherwise.
 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   % If file I/O is being used, write the input to a file.  Otherwise, create
 4261   % a pipe to which CCalc will write the input later.
 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   % Run compact -- if file_io is true, it will run to completion, or if
 4272   % file_io is false, it will run in the background
 4273   ( value(compact,true)
 4274     -> call_compact(Notify,In,CompactAns,SolvIn,VarTable0,CompactTime,
 4275                     Lockfile)
 4276   ; SolvIn = In ),
 4277
 4278   % If compact determined the satisfiability of the theory, we don't need to
 4279   % call the SAT solver, but can simply return the answer.  If compact was
 4280   % unable to determine whether the theory is satisfiable or not, or if we
 4281   % aren't using compact, or if we're using pipe I/O and haven't called
 4282   % compact yet, then we must then call the SAT solver.
 4283   ( nonvar(CompactAns)
 4284     -> Out1 = CompactAns,
 4285	open(VarTable0,read,VarTable)
 4286   ; % sort
 4287
 4288     % If file I/O is used, run the SAT solver now.  If pipe I/O is used,
 4289     % start the SAT solver running in the background and create pipes to/from
 4290     % it.
 4291     call_solver(Notify,Solver,SolvIn,SolvOut1,SolvOut2), 
 4292
 4293     % If pipe I/O is used, start writing the input (now that all of the
 4294     % processes are running in the background, waiting for it)
 4295     ( value(file_io,false)
 4296       -> open(In,write,InStrm),
 4297	  ( value(compact,true)
 4298	    -> open(VarTable0,read,VarTable)
 4299	  ; true ),
 4300
 4301	  % If mchaff is the solver, and pipe I/O is being used, open the
 4302	  % second output pipe now.  (If it is opened earlier, CCalc blocks;
 4303	  % if it's opened later, mChaff blocks.)
 4304	  ( value(solver,mchaff)
 4305	    -> open(SolvOut2,read,Out2)
 4306	  ; true ),
 4307
 4308	  % write the SAT solver input to the pipe
 4309	  write_input(Notify,InStrm),
 4310	  close(InStrm),
 4311          rm_pipe(In),
 4312
 4313	  % if compact is on, read its result and pass the compacted theory
 4314	  % on to the SAT solver.  If compact found the answer on its own,
 4315	  % return that; otherwise wait for the solver to terminate.
 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     ; % If we're using file I/O, open the second output file for mchaff now.
 4326       % For satz, pass the filename for the second output along instead of
 4327       % opening it; this file is only created if the theory is satisfiable,
 4328       % so CCalc will wait until it's sure the answer is SAT before it tried
 4329       % to open the solution file.
 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   % If pipe I/O is being used, create all of the pipes to/from compact and
 4349   % start it running in the background.  If file I/O is being used, run
 4350   % compact to completion on the input.
 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   % Remember the current input stream (so we can return to it later)
 4392   current_input(CurIn),
 4393
 4394   % Read the output compact sent to stderr.  This will contain information
 4395   % about compact's search process; in particular, it will be noted here
 4396   % if compact found a contradiction in the input (in which case the theory
 4397   % is unsatisfiable and we don't even need to call the SAT solver).  Also,
 4398   % compact has been modified to print the DIMACS header ("p cnf ...") for
 4399   % the compacted theory to stderr.  If this header indicates that the
 4400   % compacted theory has 0 atoms, it means that compact was able to resolve
 4401   % all variables, and hence the theory is satisfiable (and again we don't
 4402   % need to call the SAT solver).  If the compacted theory has at least one
 4403   % atom but 0 clauses, the header is modified to indicate 1 clause, and the
 4404   % tautological clause "1 -1 0" is passed along with it to the SAT solver.
 4405   % (Many solvers don't like empty theories.)  Otherwise, the header is simply
 4406   % passed on to the SAT solver.
 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   % Check to make sure the SAT solver executable is available.
 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   % Create I/O pipes (or files if file_io option is set)
 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   % Determine name and command line for selected solver
 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   % If file I/O is being used, call the SAT solver now, and open the first
 4511   % output file for reading once it's done.  If pipe I/O is being used, start
 4512   % solver running in the background, and open the first output pipe for
 4513   % reading so it doesn't block.  (mchaff doesn't open its second output file
 4514   % until after its input pipe is open, so CCalc will block if it tries to
 4515   % open Out2 now.)
 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
 4538% Create the file used to pass options to mChaff.  Most of the options are
 4539% always the same; these are contained in the files 'mchaff-opts.smj.1' and
 4540% 'mchaff-opts.smj.2' in the solvers directory.  The options which are changed
 4541% for each call by CCalc are added between the contents of those two files
 4542% and passed to mChaff.
 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   % If there are no clauses, print a warning and write a dummy tautological
 4576   % clause for the SAT solver (since some of them don't like 0 clauses).
 4577   ( TC == 0
 4578     -> % compact and sort don't need the DIMACS header ('p cnf # #'); the
 4579	% SAT solvers do.
 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   % otherwise, write all the clauses to the input pipe/file
 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
 4632% - -  - -  - -  - -  - -  - -  - -  - -  - -  - -  - -  - -  - -  - -%
 4633% The user level query and planning procedures.
 4634% - -  - -  - -  - -  - -  - -  - -  - -  - -  - -  - -  - -  - -  - -%
 4635
 4636output :- extract_info("SAT",M,_,_,_DMIKLESTODO1,_DMIKLESTODO2,_DMIKLESTODO3), show_models(M,sat).
 4637
 4638% sat/0 tests the causal theory for satisfiability.  No facts are used.
 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
 4734%%% When its argument is atomic, query/1 assumes that the argument is a 
 4735%%% problem label.  Owise, it assumes that it is a problem description.
 4736
 4737
 4738% Query in transition mode should be treated likewise in history mode 
 4739% because rules may refer to time explicitly. To do that, we need to 
 4740% construct domain/2 again based on step [0..maxStep] every time we 
 4741% invoke a query in transition mode. This could be inefficient, but
 4742% unavoidable for now. We could check if the maxstep is same as before,
 4743% skip constructing domain/2 for slight improvement. (this is not done 
 4744% yet, but not difficult)
 4745
 4746
 4747%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 4748%% query(Label) : process the monotonic query labelled by Label
 4749%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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
 4776% verifying unsolvable query
 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   % The last query executed might have introduced auxiliary atoms, so
 4912   % reset atom_count to its original value to eliminate these
 4913   value(domain_atom_count,DAC),
 4914   iset(atom_count,DAC),
 4915
 4916   do_term_expansion(Rules,Rules1),  % should expand because in transition 
 4917                                       % mode it may have not properly decoded
 4918                                       % because step was limited to [0,1]
 4919                                       % while any time stamps could have been
 4920                                       % mentioned %? can we skip this?
 4921   replace_comma_with_and(Rules1,Rules11),
 4922
 4923   % This code was modified to improve efficiency.  Previously, all of the
 4924   % query clauses were conjoined, and then this large formula was processed
 4925   % and converted to CNF.  However, if several of the query clauses had
 4926   % quantified variables, the quantifiers would be moved to the outside, so
 4927   % that subformulae which didn't need to be under the scope of those
 4928   % quantifiers would nonetheless be repeated many times when the quantified
 4929   % variable was grounded.  Instead, CCalc now processes each query clause
 4930   % and converts it to CNF separately, and *then* conjoins them all, to avoid
 4931   % clause explosion.
 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
 4969%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 4970%% nmquery(Label) : process the nonmonotonic query labelled by Label
 4971%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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
 5063%nmquery(Label) :- 
 5064%   atomic(Label),
 5065%   value(mode,basic), 
 5066%   fatal_error("Use sat instead of nmquery under basic mode. ",[]).
 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
 5188% extract_info(Out1,Out2,VarTable,Ans,Model,TimeMsg,Other)
 5189% The first two arguments are input, the rest are output.
 5190% Out1 and Out2 are the names of the pipes containing output data from the
 5191% SAT solver.  (Out2 is used only for some solvers, like mChaff, which returns
 5192% search information in one file and the models themselves in another.)
 5193% ANS is either "SAT" or "UNSAT"; Model is a list of atoms assigned true in the
 5194% satisfying assignment (if ANS is SAT); TimeMsg is the message from the sat
 5195% solver regarding solution time.
 5196%
 5197% The argument 'Other' is currently not used.  Formerly, Other was bound only
 5198% when CCalc encountered unexpected output from the solver and could not
 5199% determine whether the answer was SAT or UNSAT, in which case Other contained
 5200% a message about the unexpected output.  Now, however, extract_info prints
 5201% an error message and aborts when this happens.
 5202
 5203extract_info("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
 5242cleanup_after_extract(Out1,Out2) :-
 5243   % Close the output pipes/files.  If they're pipes, delete them, too.
 5244   ( value(file_io,false)
 5245     -> rm_pipe(Out1),
 5246	( nonvar(Out2) -> rm_pipe(Out2) ; true )
 5247   ; close(Out1) ),
 5248
 5249   % Delete unnecessary files create by some SAT solvers
 5250   common_file_delete(timetable),
 5251   common_file_delete(record).
 5252
 5253
 5254extract_info_aux(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     % if mchaff says the instance is unsatisfiable and doesn't
 5398     % return any solutions, it really is unsatisfiable
 5399     Ans = "UNSAT"
 5400   ; ( Ans0 == "SAT" ; Ans0 == "UNSAT" ) ->
 5401     % if mchaff says the instance is unsatisfiable, but returns
 5402     % some solutions to it, then there are *some* solutions, but
 5403     % not as many as requested with the num option
 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"