https://github.com/theoremprover-museum/CLIN
Raw File
Tip revision: e7082fbde3634286f458d64846699ae488fe18f3 authored by Michael Kohlhase on 22 December 2016, 09:28:55 UTC
initial commit, thanks to David Plaisted
Tip revision: e7082fb
bug.report


	Bug reports and fixes:

	1. in file fls, procedure
                          create_r(MRefs1) :-
                                bagof1(X, (Y,Z)^in_fls(Y,Z), Refs1),
                                       ^
                ------------->  bagof1(Z, (Y,Z)^in_fls(Y,Z), Refs1),
                                       ^
        2. In file hyper, the first clause of procedure
                          hl_user(...) :-
                                hl_user_literal_U(...),
                                hl_literals(Lns1, ..., T1,CS2,CR2).
                                                       ^^
                ------------->  hl_literals(Lns1, ..., Ts1,CS2,CR2).
                                                       ^^^
        3. In file hyper, the second clause of procedure
                          proc_C(_,_,_,[],_,_,0,[],...) :- !.
                                    ^^
                ------------->  proc_C(_,_,[],_,_,0,[],...) :- !.
        4. In file interp, the second clause of procedure
                          ubfsupp_o_1(Cn1,V11,V12,V1,W1,CSize1) :-
                                supplement_clause(0,CN1,...), !.
                ------------->  ubfsupp_o_1(Cn1,V11,V12,V1,W1,CN1,CSize1) :-
                                                              ^^^^
                                supplement_clause(0,CN1,...), !.
        5. In file pc, procedures print_clause_list/1 and print_clause_list_1/1
           are redefined. They have already defined in file auxiliary.
        6. In file simplify, the first clause of procedure
                                duplicate_deletion_2(...) :-
                                        ...
                                        binary_max_ind(CT1,CT2,CI3,Up),
                                                                ^
                                        ...
                ------------->  duplicate_deletion_2(...) :-
                                        ...
                                        binary_max_ind(CT1,CT2,CT3,Up),
                                                                ^
                                        ...

	7.

        I fixed this problem is instdel some time ago.  Changed:

        %%% we assume that input clauses are not instances of any clause.
        %%% we take one clause sent_C, then check if it is deleted or not,
        %%%     if not, we put it as sent_c.
             instdel_1(Clist) :-
                clause(sent_C(cl(_,_,by([Ln11,Ln12|Lns1],V11,V11,Clist,_),0,
                        CS1,CR1,CT1,_,_)),true,Ref1),
                clause(sent_C(C2),true,Ref1),
                instdel_ckinst([Ln11,Ln12|Lns1],CS1,CR1,CT1,C2),
                fail.

        to

        %%% we assume that input clauses are not instances of any clause.
        %%% we take one clause sent_C, then check if it is deleted or not,
        %%%     if not, we put it as sent_c.
             instdel_1(Clist) :-
                clause(sent_C(cl(_,_,by([Ln11,Ln12|Lns1],V11,V11,Clist,_),0,
                        CS1,CR1,CT1,_,_)),true,Ref1),
                clause(sent_C(C2),true,Ref1),
        --->    erase(Ref1),
                instdel_ckinst([Ln11,Ln12|Lns1],CS1,CR1,CT1,C2),
                fail.

	8. 

	In PC prover, sometimes it will cause looping when out_model_rc is
	set to print out models or relevant clauses. The fix is: 

	reduce_set_1([],_,(Ctail,Nctail),L,_,_,_,unsat,[L|Ctail],Nctail) :- !.

	is changed to

	reduce_set_1([],_,(Ctail,Nctail),L,_,_,_,unsat,[L|Ctail],[Nctail]) :- !.
								 ^^^^^^^^	
back to top