/*-----------------------------------------------------------------------

File  : can_treeanalyze.h

Author: Stephan Schulz

Contents
 
  Functions for analysing and marking dependency trees for clauses.

  Copyright 1998, 1999 by the author.
  This code is released under the GNU General Public Licence and
  the GNU Lesser General Public License.
  See the file COPYING in the main E directory for details..
  Run "eprover -h" for contact information.

Changes

<1> Tue Mar 23 02:07:15 MET 1999
    New

-----------------------------------------------------------------------*/

#ifndef CAN_TREEANALYZE

#define CAN_TREEANALYZE

#include <can_infstate.h>


/*---------------------------------------------------------------------*/
/*                    Data type declarations                           */
/*---------------------------------------------------------------------*/




/*---------------------------------------------------------------------*/
/*                Exported Functions and Variables                     */
/*---------------------------------------------------------------------*/

#define PROOF_DIST_INFINITY LONG_MAX /* It's magic */
#define PROOF_DIST_DEFAULT  10 /* Default for non-proofs */


#endif

/*---------------------------------------------------------------------*/
/*                        End of File                                  */
/*---------------------------------------------------------------------*/