%%% MAIN %%% %%% This section contains the main procedure. %%% %%% Two input file formats: %%% A. CLAUSE FORMAT: %%% For clauses p(X) or q(Y),not(P(a)) would be expressed as %%% [p(X),q(X)]. %%% [not p(a)]. %%% %%% B. SPRFN FORMAT: %%% For above clauses %%% p(X) :- not q(X). %%% false :- p(a). %%% %%% The internal form of clauses Clause_I is: %%% cl(Size,Nv,by(Cn,V1,V2,V,W),Input,sp(S1,S2,S3),ds(R1,R2,R3), %%% Replace,Flags,Priority) %%% Size is the size of the clause. %%% Nv is the number of non-ground literals %%% Cn is the clause linearized form. %%% V1 and V2 are variable lists in the clause for occurs check. %%% V is the variable list in the clause for computing ground form. %%% W is a list: %%% [W1,W2,...,Wn] %%% where Wi is the variable list in literal i for computing ground %%% form of literal i. %%% Input is 1 if the clause is input clause. Otherwise 0. %%% S1,S2,S3 record the support status. %%% 1 represents supported, 0 not supported. %%% S1 for user suported, S2 for backward supported, and %%% S3 for forward supported. %%% R1,R2,R3 record the distance. %%% S1 for user distance, S2 for backward distance, and %%% S3 for forward distance. %%% Replace is 1 if the clause is an instance of replace rules, %%% 0 otherwise. %%% Flags is the replacement field. %%% If a literal is not used for replacement, then 1. %%% Otherwise 0. %%% Priority is %%% a. If sliding priority is specified, then %%% Priority = pr(PS,PD,PL,PR,P) where %%% PS = integer(size_coef*(max size of literals)) %%% PD = integer(depth_coef*depth) %%% PL = integer(literal_coef*(number of literals)) %%% PR = integer(relevance_coef*max(B+F,U)) %%% B, F and U are backward, forward, and user distances %%% respectively. %%% P is max(PS,PD,PL,PR) %%% b. If sliding priority is not specified, then %%% Priority = pr(0,0,0,0,0) %%% %%% Prove the theorem in File. %%% If user_control is specified, then File is the problem to be solved. %%% Otherwise, File may be the problem itself or a file containg %%% a list of problems depending if batch mode is used. prove(File) :- user_control, !, prove_1(File), !, fail. prove(File) :- xvisor(File), !, fail. %%% prove_1 fails in the following cases: %%% Read erroneous commands in interp. %%% No user support clauses if user support strategy is specified %%% in interp. %%% %%% Clear the database to avoid the interference of the assertions from %%% the previous run. %%% Call interpreter to assert clauses with internal format. %%% If automatic control, check if the input is a horn set. %%% Try to solve the given problem. %%% Print out statistics for the tried problem. %%% Reset flags due to horn set. %%% If user_control, reset options that are set in the spec. of the problem. prove_1(Prob) :- not(not(clear_database)), assert(file_name(Prob)), !, interp, not(not(set_real_time_limit)), check_horn_set, try, not(not(summary)), reset_by_horn_set, not(not(postproc)), !. %%% CLEAR DATABASE %%% %%% Clear the database so that the remanants from the previous problem won't %%% affect the proof of the current problem. clear_database :- % clearing the database. abolish(infer_visited,4), abolish(ordering_inference,1), abolish(clause_largest_length,1), abolish(cps_A,5), % data structure for spc. abolish(cps_I,6), % data structure for spc. abolish(cps_O,5), % data structure for spc. abolish(cps_U,5), % data structure for spc. abolish(cps_V,5), % data structure for spc. abolish(sp_size,1), % small proof size. abolish(db_erased,1), % release memory. abolish(du,2), % temporary assertions in unit simp. abolish(error,1), % error indication. abolish(file_name,1), % file name. abolish(in_fls,2), % release memory. abolish(last_hyperlink_time,1),% time spent on last hyper-linking. abolish(lit_G,4), % general literal list. abolish(lit_S,4), % literal list from supported clauses. abolish(lit_N_G,5), % literal list for replacements. abolish(lit_N_V,5), % literal list for replacements. abolish(lit_ST_G,5), % literal list for replacements. abolish(lit_ST_V,5), % literal list for replacements. abolish(lit_U,3), % literal list from unit clauses. abolish(no_user_clauses,0), % set in interp. abolish(nonvar_depth_weight,2), % depth weight for non-variable. abolish(nonvar_size_weight,2), % size weight for non-variable. abolish(nu,1), % used in duplicate deletion. abolish(num,1), % for numbering printed stuff. abolish(number_inclauses,1), % number of input clauses. abolish(ou,2), % temporary assertions in unit simp. abolish(out_model_rc,0), % clear flag for pc prover. abolish(pc_time,1), % record total pc prover time. abolish(proof_type,1), % proof type. abolish(prove_result,1), % record the proof result. abolish(replace_rule_1,5), % replace rules. abolish(replace_rule_2,5), % replace rules. abolish(sent_INST,1), % temp. clauses in hyper-linking. abolish(sent_T,1), % temp. clauses in hyper-linking. abolish(sent_c,1), % temp. clauses. abolish(session_no,1), % store session no. abolish(start_time,1), % starting time of the proof. abolish(uparg,6), % used in duplicate deletion. abolish(updated_arguments,0), % used in duplicate deletion. abolish(user_support,1), % user support indicator. abolish(user_supportset,1), % user support list. abolish(var_depth_weight,2), % depth weight for all variables. abolish(var_size_weight,2), % size weight for all variables. abolish(wu_bound,1), % current hyper-link workunit bound. session_deletions, !. % deletions done before a session. % delete assertions of the previous session. session_deletions :- abolish(current_support,1), % recording current support strategy. abolish(num_supp,1), % Nth support strategy in support list. abolish(old_C,1), % old clauses. abolish(over_litbound,0), % indicator, too many literals. abolish(over_numvars,0), % indicator, too many variables. abolish(over_priohl,0), % indicator, over priority. abolish(over_relevance,0), % indicator, over relevance. abolish(priority_bound,1), % current priority bound. abolish(prio_wu,3), % counter for different priorities. abolish(round_no,1), % current round number. abolish(round_time,2), % the time at end of each round. abolish(same_db_supp,1), % support round strategy having % unchanged assertions. abolish(total_numhl,1), % total number of instances so far. abolish(total_wu,1). % total work units so far. %%% Set real time limit. %%% Default is no change. set_real_time_limit :- \+ user_control, time_limit(X), set_real_time_limit(X), !. set_real_time_limit :- time_limit(X), set_real_time_limit(X), !. set_real_time_limit(T) :- time_limit_coef(F), abolish(real_time_limit,1), Temp is F*T, floor(Temp, RTL), assert(real_time_limit(RTL)). set_real_time_limit(T) :- abolish(real_time_limit,1), assert(real_time_limit(T)). %%% If user_control, then no effect. %%% If the input is Horn-set, then set delete_all_instances. check_horn_set :- user_control, !. check_horn_set :- check_horn_set_2, check_horn_set_1. check_horn_set_1 :- sent_C(cl(_,_,by(Cn1,_,_,_,_),_,_,_,_,_,_)), check_horn_clause(Cn1), !. % succeed if not horn set. check_horn_set_1 :- % If horn set. set(delete_all_instances). check_horn_clause(Cn1) :- % fail if horn clause. horn_clause(Cn1), !, fail. check_horn_clause(_). % If not horn set. %%% If delete_all_instances is set initially, return 1, otherwise 0. check_horn_set_2 :- delete_all_instances, !. check_horn_set_2 :- assert_once(check_horn_set_saved). %%% Reset the delete_all instances if necessary. %%% If delete_all_instances is not set initially, delete it. reset_by_horn_set :- retract(check_horn_set_saved), !, clear(delete_all_instances). reset_by_horn_set. %%% %%% REPORT OUT %%% %%% Report the summary of the proof. summary :- cputime(T), nl, write_line(5,'SUMMARY:'), report_file, settings, check_print_pc_model_rc, report_proof(T), !. %%% Print out filename and number of input clauses of the underlying problem. report_file :- file_name(File), write_line(5,'Underlying-File: ',File), number_inclauses(IN), write_line(5,'Number-Of-Input-Clauses: ',IN). %%% Print out options set for the underlying problem. settings :- member(X,[ outCagen, outCahl, outCainst, outCasimp, outfls, outhl, outhllits, outpc, outpcin, depth_coef(_), literal_coef(_), max_no_clauses(_), relevance_bound(_), relevance_coef(_), size_coef(_), start_no_clauses(_), start_no_clauses_coef(_), support_list(_), time_limit(_), time_limit_coef(_), time_limit_multiple(_), back_literalbound(_), small_proof_size_bound(_), for_literalbound(_), literal_bound(_), user_literalbound(_), start_wu_bound(_), count_all_literals, delete_all_instances, delete_nf_instances, do_hyper_linking, ground_disting_after_match, ground_restriction, ground_substitution, hl_literal_reordering, realfls, replace_literal_reordering, replacement, simple_small_proof_check, size_by_clause, slidepriority, small_proof_check, small_proof_check_all, spc_literal_reordering, sum_of_measures, super_batch, tautology_deletion, unit_resolution, user_control ]), call(X), write_line(15,'',X), fail. settings. %%% Print out information about the try of the underlying problem. report_proof(T) :- report_trystatus, report_proof_type, report_session_round_no, report_number_C_space, report_PrWu_bounds, report_pc_time, report_total_time(T). %%% What is the status of the try. report_trystatus :- tab(25),write('What: '), prove_result(PR), write(PR),nl,!. %%% If the underlying problem was proved, how it was proved. %%% If was proved by small proof checker, print out small proof size. report_proof_type :- report_proof_type_1(PT), report_proof_type_2(PT). report_proof_type_1(PT) :- proof_type(PT), write_line(25,'Proof-Type: ',PT), !. report_proof_type_1(_). report_proof_type_2(PT) :- PT == 'SP', sp_size(N1), write_line(25,'Small_Proof_Size: ',N1), !. report_proof_type_2(_). %%% Print out how many rounds in the final session. report_session_round_no :- session_no(SessionNo), round_no(RoundNo), write_line(25,'Number-Of-Sessions: ',SessionNo), write_line(25,'Number-Of-Rounds: ',RoundNo). %%% Print out how many clauses at the end. report_number_C_space :- get_C_number_space(0,0,M,S), write_line(25,'Number-Of-Clauses-Retained: ',M), write_line(25,'Space-Used-In-Units: ',S). get_C_number_space(M1,S1,M2,S2) :- retract(sent_C(cl(Z,_,_,_,_,_,_,_,_))), MM is M1 + 1, SS is S1 + Z, !, get_C_number_space(MM,SS,M2,S2). get_C_number_space(M,S,M,S). %%% Print out information about sliding priority. report_PrWu_bounds :- slidepriority, report_PrWu_bounds_1, !. report_PrWu_bounds. report_PrWu_bounds_1 :- priority_bound(PrioBound), write_line(25,'Priority-Bound: ',PrioBound), wu_bound(WUBound), write_line(25,'Work-Unit-Bound: ',WUBound), !. report_PrWu_bounds_1. %%% Print out total PC time used. report_pc_time :- tab(25),write('PC-Prover-Time: '), report_pc_time_1. report_pc_time_1 :- pc_time(PCTIME), write(PCTIME), nl, !. report_pc_time_1 :- write(0), nl. %%% Print out total CPU time used. report_total_time(T) :- start_time(Start_Time), Used_Time is T - Start_Time, write_line(25,'Total-Time: ',Used_Time). %%% Print out model or relevant clauses to the proof by PC prover. check_print_pc_model_rc :- outpc, print_pc_model_rc. check_print_pc_model_rc. print_pc_model_rc :- prove_result('satisfiable'), print_pc_model_rc_1, !. print_pc_model_rc :- proof_type('PC'), print_pc_model_rc_1, !. print_pc_model_rc. print_pc_model_rc_1 :- compute_fls(FMS), assert(out_model_rc), run_pc_mr(FMS), abolish(out_model_rc,0), !. run_pc_mr(FMS) :- outpcin, write_line(5,'Input to PC:'), print_clause_list(FMS), intell_pc(FMS,_). run_pc_mr(FMS) :- intell_pc(FMS,_). %%% Postprocess commands in input file. postproc :- user_control, file_name(File), seeing(Input), see(File), read_till_end_input, postproc_1, seen, see(Input), !. postproc. %%% Read input until the command end_of_input. read_till_end_input :- repeat, read(Term), Term == 'end_of_input'. postproc_1 :- read(Term), Term \== 'end_of_file', postproc_1(Term), !, postproc_1. postproc_1. %%% Perform actions according to the command. postproc_1(set(X)) :- set(X). postproc_1(clear(X)) :- clear(X). postproc_1(assign(X,V)) :- assign_cmd(X,V). postproc_1(delete(X,V)) :- delete(X,V). postproc_1(Term) :- write_line(5,'ERROR: Wrong input -> ',Term), !, fail.