1 /*----------------------------------------------------------------------- 2 3 File : can_treeanalyze.h 4 5 Author: Stephan Schulz 6 7 Contents 8 9 Functions for analysing and marking dependency trees for clauses. 10 11 Copyright 1998, 1999 by the author. 12 This code is released under the GNU General Public Licence and 13 the GNU Lesser General Public License. 14 See the file COPYING in the main E directory for details.. 15 Run "eprover -h" for contact information. 16 17 Changes 18 19 <1> Tue Mar 23 02:07:15 MET 1999 20 New 21 22 -----------------------------------------------------------------------*/ 23 24 #ifndef CAN_TREEANALYZE 25 26 #define CAN_TREEANALYZE 27 28 #include <can_infstate.h> 29 30 31 /*---------------------------------------------------------------------*/ 32 /* Data type declarations */ 33 /*---------------------------------------------------------------------*/ 34 35 36 37 38 /*---------------------------------------------------------------------*/ 39 /* Exported Functions and Variables */ 40 /*---------------------------------------------------------------------*/ 41 42 #define PROOF_DIST_INFINITY LONG_MAX /* It's magic */ 43 #define PROOF_DIST_DEFAULT 10 /* Default for non-proofs */ 44 45 46 #endif 47 48 /*---------------------------------------------------------------------*/ 49 /* End of File */ 50 /*---------------------------------------------------------------------*/ 51 52 53 54 55 56