https://github.com/theoremprover-museum/CLIN
Tip revision: e7082fbde3634286f458d64846699ae488fe18f3 authored by Michael Kohlhase on 22 December 2016, 09:28:55 UTC
initial commit, thanks to David Plaisted
initial commit, thanks to David Plaisted
Tip revision: e7082fb
xvisor
%%% XVISOR
%%%
%%% This is an expert system for the prover.
%%% The top level supervisor is intended to help users to run their
%%% problems without knowing details about the prover.
%%%
%%% The following is the language for users of this expert system:
%%% problem_list.
%%% ...
%%% end.
%%%
%%% The following is the language for experts:
%%% expert_rule(support_list(S))
%%% expert_rule(time_limit_coef(F))
%%% expert_rule(literal_bound(L))
%%%
%%% The algorithm is the following:
%%% read in problems in an unsolved list UL
%%% set T = least_time_bound
%%% make SL empty
%%% while T =< greatest_time_bound
%%% while we have next strategy S
%%% while we have unsolved problem P in UL
%%% solve P with S within T
%%% if P is solved
%%% then delete P from UL and put P in SL
%%% endwhile
%%% if UL is empty
%%% then print out 'all done' and return
%%% endwhile
%%% T = 2*T
%%% endwhile
%%% print out solved problems in SL and unsolved problems in UL
%%% Two modes are provided for top level supervisor:
%%% batch mode: To use it, set(super_batch) should be executed.
%%% A file containing a list of problems and commands
%%% is the only argument of prove(_).
%%% The list of problems are listed as follows:
%%% prove(prob1).
%%% prove(prob2).
%%% ...
%%% prove(probn).
%%% real time mode: the problem to be solved is the only argument of
%%% prove(_). Users can use assign_cmd(least_time_bound,V) and
%%% assign_cmd(greatest_time_bound,V) to set up the time bounds.
%%% Default is real time mode.
%%%
%%% If a strategy is not complete and it caused a satisfiable result
%%% for a problem P, then we don't consider this strategy with
%%% increased time bound afterwards for P.
%%%
%%% If a problem P failed with errors too_many _input_variables or
%%% format_error_input_file, then P is removed from the unsolved
%%% problem list.
%%%
%%% If user doesn't specify necessary clauses for u, o, or n support
%%% for a problem P, we don't deal with this here.
%%% The prover would fail at interpretation before trying to prove
%%% P.
%%%
%%% Clear database for supervisor.
%%% Set initial values for supervisor.
%%% Read problem list.
%%% Set initial time limit.
%%% Try to solve all problems.
%%% Reset option values.
xvisor(File) :-
not(not(xvisor_clear)),
not(not(xvisor_set)),
not(not(xvisor_read_problems(File))),
not(not(set_initial_time_limit)),
solve_all_problems,
reset_options, !.
%%% Clear database for supervisor.
xvisor_clear :-
abolish(no_try,2),
abolish(prob_tried_round0,2),
abolish(solved_prob,1),
abolish(tried_round0,1),
abolish(unsolved_prob,1), !.
%%% Set options.
xvisor_set :-
set(slidepriority),
assign_cmd(small_proof_size_bound,100), !.
%%% If batch mode, the problem are listed in the given file.
xvisor_read_problems(File) :-
super_batch, !,
read_and_assert_problems_file(File), !.
%%% If not batch mode, the given file is the problem itself.
xvisor_read_problems(File) :-
assertz(unsolved_prob(File)),
assertz(prob_tried_round0(File,0)).
%%% Read in problem lists and assert useful information.
read_and_assert_problems_file(File) :-
seeing(Input),
see(File), !,
interp_problems_file,
seen,
see(Input).
%%% Interpret the commands in the input file.
interp_problems_file :-
read(Term),
Term \== 'end_of_file', !,
interp_problems_file(Term), !,
interp_problems_file.
interp_problems_file.
%%% unsolved problems are stored in two forms:
%%% unsolved_prob(P)
%%% prob_tried_round0(P,X)
%%% X is for controlling the execution of round 0.
%%% If a problem P is executed once in a time limit T, then X is set to 1.
%%% So round 0 won't be executed thereafter with other strategies in T.
%%% X should be reset for all unsolved problems if the time limit is
%%% increased.
interp_problems_file(prove(P)) :-
assertz(unsolved_prob(P)),
assertz(prob_tried_round0(P,0)), !.
interp_problems_file(Term) :-
write_line(5,'ERROR: Wrong input -> ',Term), !, fail.
%%% Set initial time limit as least time bound.
set_initial_time_limit :-
least_time_bound(T),
assign_cmd(time_limit,T).
%%% Try all problems in one strategy, then next strategy.
%%% If there are unsolved problems when all strategies are tried,
%%% increase the time limit, and try again from the first strategy and
%%% first unsolved problem.
%%% solve_all_problems will stop if either time limit is advanced
%%% and is greater than greatest time bound, or all problems are solved.
solve_all_problems :-
next_strategy(S),
solve_problems_strategy(S),
print_success_message, !.
solve_all_problems :-
next_time_limit,
reset_tried_round0, !,
solve_all_problems.
solve_all_problems :-
write_line(5,'Solved problems:'),
print_solved_problems,
write_line(5,'Unsolved problems:'),
print_unsolved_problems.
%%% If solve_problems_strategy succeeds and there are still unsolved
%%% problems, then something must be wrong.
print_success_message :-
unsolved_prob(_),
write_line(5,'ERROR: Something must be wrong.'), !.
%%% Otherwise, all problems are solved.
print_success_message :-
write_line(5,'All problems solved.').
%%% Try with next strategy.
next_strategy(S) :-
expert_rule(R),
what_expert_rule(R,S).
%%% Execute rules until support strategy.
what_expert_rule(support_list(S),S) :-
assign_cmd(support_list,S), !.
what_expert_rule(X,_) :-
X =.. [F,A],
assign_cmd(F,A), !, fail.
what_expert_rule(_,_) :-
fail.
%%% Try all unsolved problems one by one with a certain strategy.
solve_problems_strategy(S) :-
unsolved_prob(P),
\+ no_try(P,S),
hk_tried_round0(P),
write_line(5,'Try: ',P),
solve_one_problem(P), !.
solve_problems_strategy(_) :-
unsolved_prob(_), !, fail.
solve_problems_strategy(_).
%%% If prove_1 fails, check if there is an error or no user support
%%% clauses if user support strategy is specified.
solve_one_problem(P) :-
\+ not(not(prove_1(P))),
!,
analyze_failure(P).
%%% If prove_1 succeeds, check if the problem was proved or not,
%%% and update information accordingly.
solve_one_problem(P) :-
hk_problem(P), !,
fail.
analyze_failure(P) :-
error('too_many_input_variables'),
remove_problem(P), !, fail.
analyze_failure(P) :-
error('Syntactic error in input file !'),
remove_problem(P), !, fail.
%%% Set tried_round0 properly for the next problem to be tried.
hk_tried_round0(P) :-
abolish(tried_round0,1),
prob_tried_round0(P,X),
assert(tried_round0(X)), !.
%%% If the problem is solved, move it to solved_problem list.
%%% Otherwise, update the tried_round0 status for tried problems.
hk_problem(P) :-
stop_this_problem(P),
remove_problem(P), !.
hk_problem(P) :-
update_tried_round0(P), !.
remove_problem(P) :-
retract(unsolved_prob(P)),
retract(prob_tried_round0(P,_)),
assertz(solved_prob(P)).
%%% If the problem is proved, or if the problem is satisfiable and
%%% the strategy used was a complete strategy.
stop_this_problem(P) :-
prove_result(unsatisfiable), !.
stop_this_problem(P) :-
support_list(Sup), !,
prove_result(satisfiable),
!, process_satisfiable_case(P,Sup).
%%% If the strategy is complete, then the problem was solved.
%%% Otherwise, delete all such strategies.
process_satisfiable_case(_,Sup) :-
complete_strategy(Sup), !.
process_satisfiable_case(P,Sup) :-
assert(no_try(P,Sup)), !, fail.
%%% Update tried_round0 information for the problem to avoid executing
%%% round 0 more than once in a certain time limit.
update_tried_round0(P) :-
prob_tried_round0(P,1), !.
update_tried_round0(P) :-
retract(prob_tried_round0(P,_)),
assert(prob_tried_round0(P,1)).
%%% Update time_limit.
%%% If time_limit is greater than greatest_time_bound, fails.
next_time_limit :-
time_limit(T),
get_time_limit_multiple(F),
T2 is F*T,
greatest_time_bound(GT), !,
T2 =< GT,
assign_cmd(time_limit,T2), !.
get_time_limit_multiple(F) :-
time_limit_multiple(F), !.
get_time_limit_multiple(2).
%%% Reset the tried_round0 status for all unsolved problems,
%%% so that round 0 will be executed for new time_limit.
reset_tried_round0 :-
abolish(prob_tried_round0,2),
reset_tried_round0_1.
reset_tried_round0_1 :-
unsolved_prob(P),
assert(prob_tried_round0(P,0)),
fail.
reset_tried_round0_1.
%%% Print out solved problems.
print_solved_problems :-
retract(solved_prob(P)),
write_line(10,P),
fail.
print_solved_problems.
%%% Print out unsolved problems.
print_unsolved_problems :-
retract(unsolved_prob(P)),
retract(prob_tried_round0(P,_)),
write_line(10,P),
fail.
print_unsolved_problems.
%%% Reset options to default values.
reset_options :-
clear(slidepriority),
assign_cmd(small_proof_size_bound,100),
assign_cmd(support_list,[b,f]),
assign_cmd(literal_bound,0),
assign_cmd(time_limit,2000),
abolish(time_limit_coef,1).