reduce-historical/r37/packages/redlog/cltab.red

% ----------------------------------------------------------------------
% $Id: cltab.red,v 1.9 1999/04/13 13:11:03 sturm Exp $
% ----------------------------------------------------------------------
% Copyright (c) 1995-1999 Andreas Dolzmann and Thomas Sturm
% ----------------------------------------------------------------------
% $Log: cltab.red,v $
% Revision 1.9  1999/04/13 13:11:03  sturm
% Updated comments for exported procedures.
%
% Revision 1.8  1999/04/11 10:20:12  sturm
% Added call to rl_nnf in cl_gentheo1 such that non-positive formulas
% are treated as intended by rlgentheo now.
%
% Revision 1.7  1999/03/22 17:08:08  dolzmann
% Changed copyright information.
%
% Revision 1.6  1996/10/07 11:45:58  sturm
% Added fluids for CVS and copyright information.
%
% Revision 1.5  1996/10/01 10:17:26  reiske
% Added verbosity output in cl_atab.
%
% Revision 1.4  1996/09/30 16:57:28  sturm
% Switched to new tableau code.
%
% Revision 1.3  1996/08/01 11:44:59  reiske
% Major changes:
% New implementation of tableau method.
% Added procedure cl_gentheo.
%
% Revision 1.2  1996/07/07 14:34:21  sturm
% Turned some cl calls into service calls.
%
% Revision 1.1  1996/03/22 10:31:34  sturm
% Moved and split.
%
% ----------------------------------------------------------------------
lisp <<
   fluid '(cl_tab_rcsid!* cl_tab_copyright!*);
   cl_tab_rcsid!* := "$Id: cltab.red,v 1.9 1999/04/13 13:11:03 sturm Exp $";
   cl_tab_copyright!* := "(c) 1995-1999 by A. Dolzmann and T. Sturm"
>>;

module cltab;
% Common logic tableau method. Submodule of [cl].

procedure cl_tab(f,cdl);
   % Common logic tableau; simplification. [f] is a formula; [cdl] is
   % a list of atomic formulas. Returns a formula. The result is a
   % case distiction on the atomic formulas in [cdl] in conjunction
   % with corresponding specializations of [f].
   cl_mktf cl_tab1(f,cdl);

procedure cl_tab1(f,cdl);
   % Common logic tableau subroutine. [f] is a formula; [cdl] is a
   % list of atomic formulas. Returns a list of consed pairs of $(...,
   % (\phi_i . c_i), ...)$, where $c_i$ is in [cdl] and $\phi_i$ is a
   % specialization of [f] wrt. $c_i$.
   begin scalar w,ff,resl;
      for each atf in cdl do <<
	 ff := rl_simpl(f,{atf},-1);
	 if ff neq 'inctheo and ff neq 'false then
	    if (w := assoc(ff,resl)) then
	       cdr w := rl_simpl(rl_mkn('or,{atf,cdr w}),nil,-1)
	    else
	       resl := (ff . atf) . resl
      >>;
      return resl
   end;

procedure cl_mktf(resl);
   % Common logic make tableau formula. [resl] is a list of consed
   % pairs. Returns a formula. Uses a heuristic approach whether to
   % use the simplifier or not. Depends on the facilities of
   % [rl_simpl].
   begin scalar w,flg;
      w := resl;
      while w do
	 if (rl_tvalp caar w) or (cl_atfp caar w) then <<
	    w := nil;
	    flg := T
	 >> else
	    w := cdr w;
      return
	 if flg then
	    rl_simpl(rl_mkn('or,for each x in resl collect
      	       rl_mkn('and,{cdr x,car x})),nil,-1)
      	 else
	    rl_mkn('or,for each x in resl collect
      	       rl_mkn('and,{cdr x,car x}));
   end;

procedure cl_atab(f);
   % Common logic automatic tableau; simplification. [f] is a formula.
   % Returns a simplified equivalent of [f] or [f] itself. The result
   % is obtained by trying [cl_tab] with case distictions on the signs
   % of terms in [f] as [cdl].
   begin scalar w;
      w := cl_atab1 f;
      return if w then
	 cl_mktf w
      else
	 f  
   end;

procedure cl_atab1(f);
   % Common logic new automatic tableau subroutine. [f] is a formula.
   % Returns [nil] or a resl.
   begin scalar cdl,cdll,atnum,atnumold,atnumnf,nresl,resl,dpth;
      atnum := cl_atnum f;
      atnumold := atnum;
      cdll:= rl_a2cdl cl_atml f;
      if !*rlverbose then <<
	 ioto_tprin2t {atnum," = 100%"};
	 dpth := length cdll
      >>;
      while cdll do <<
 	 cdl := car cdll;
 	 cdll := cdr cdll;
	 nresl := cl_tab1(f,cdl);
 	 atnumnf := cl_atnum cl_mktf nresl;
      	 if !*rlverbose then <<
	    ioto_prin2 {"[",dpth,": ",atnumnf,"] "};
	    dpth := dpth - 1
	 >>;
	 if atnumnf < atnum then <<
    	    resl := nresl;
    	    atnum := atnumnf
	 >>
      >>;
      if !*rlverbose then
	 if atnum < atnumold then
	    ioto_tprin2t {"Success: ",atnumold," -> ",atnum}
      	 else
	    ioto_tprin2t {"No success, returning the original formula"};
      return resl
   end;

procedure cl_itab(f);
   % Common logic iterative tableau; simplification. [f] is a formula.
   % Returns a simplified equivalent of [f] or [f] itself. The result
   % is obtained by iterative application of [cl_atab]. Depends on the
   % switch [rltabib]. With [rltabib] on, the iteration is not
   % performed on the entire formula but on the single sepcialization
   % branches.
   if !*rltabib then cl_itab2 f else cl_itab1 f;

procedure cl_itab1(f);
   % Common logic iterative tableau subroutine. [f] is a formula.
   % The switch [rltabib] is off. Returns a formula.
   begin scalar w,res;
      w := cl_atab1 f;
      while w do <<
	 res := cl_mktf w;
      	 if !*rlverbose then
	    ioto_tprin2t {"Recomputing tableau."};
	 w:= cl_atab1 res
      >>;
      return res or f
   end;

procedure cl_itab2(f);
   % Common logic iterative tableau subroutine. [f] is a formula.
   % Iterate branchwise. Returns a formula.
   begin scalar w;
      w := cl_atab1 f;
      return if w then
	 cl_mktf for each res in w collect (cl_itab2 car res) . cdr res
      else
	 f
   end;

procedure cl_gentheo(theo,f,bvl);
   % Common logic generate theory. [theo] is THEORY; [f] is a
   % quantifier-free formula; [bvl] is a list of variables. Returns a
   % pair $(\Theta . \phi)$, where $\Theta$ is a THEORY extending
   % [theo] by inequalities, and $\phi$ is a formula such that $\Theta
   % \models \phi \longleftrightarrow [f]$. The additional assumptions
   % in $\Theta$ do not involve variables in [bvl].
   begin scalar w;
      w := cl_gentheo0(f,bvl);
      return rl_thsimpl(union(theo,car w)) . cdr w
   end;

procedure cl_gentheo0(f,bvl);
   % Generate theory. [f] is a quantifier-free formula; [bvl] is a
   % list of variables. Returns a pair $\theta . \phi$ where $\theta$
   % is a list of inequations not containing variables from [bvl], and
   % $\phi$ is a quantifier-free formula such that $\bigwedge \theta
   % \longrightarrow ([f] \longleftrightarrow \phi)$.
   begin scalar w,res,theo;
      while car (w:=cl_gentheo1(f,bvl)) do <<
	 res := cdr w;
	 theo := cdr res . theo;
	 f := car res
      >>;
      return theo . f
   end;

procedure cl_gentheo1(f,bvl);
   % Generate theory subroutine. [f] is a formula; [bvl] is a list of
   % variables. Returns a consed pair (flag . res).
   begin scalar cdl,result,nres,flag,theo;
      result := f;
      cdl := rl_getineq(rl_nnf f,bvl);
      for each ineq in cdl do <<
	 nres := rl_simpl(f,{ineq},-1) . ineq;
 	 if not cl_cmpfp(result,car nres) then <<
    	    result := car nres;
	    theo := cdr nres;
	    flag := T
 	 >>
      >>;
      return flag . (result . theo)
   end;

procedure cl_cmpfp(f,nf);
   % Generate theory compare formulas predicate. [f] and [nf] are
   % quantifier-free formulas. Returns a Boolean.
   cl_atnum f < cl_atnum nf;

endmodule;  % [cltab]

end;  % of file