zchaff_header.h

命题逻辑的求解器,2004年SAT竞赛第一名的求解器

/*********************************************************************
 Copyright 2000-2004, Princeton University.  All rights reserved. 
 By using this software the USER indicates that he or she has read, 
 understood and will comply with the following:

 --- Princeton University hereby grants USER nonexclusive permission 
 to use, copy and/or modify this software for internal, noncommercial,
 research purposes only. Any distribution, including commercial sale 
 or license, of this software, copies of the software, its associated 
 documentation and/or modifications of either is strictly prohibited 
 without the prior consent of Princeton University.  Title to copyright
 to this software and its associated documentation shall at all times 
 remain with Princeton University.  Appropriate copyright notice shall 
 be placed on all software copies, and a complete copy of this notice 
 shall be included in all copies of the associated documentation.  
 No right is  granted to use in advertising, publicity or otherwise 
 any trademark,  service mark, or the name of Princeton University. 


 --- This software and any associated documentation is provided "as is" 

 PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS 
 OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A 
 PARTICULAR PURPOSE, OR THAT  USE OF THE SOFTWARE, MODIFICATIONS, OR 
 ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, 
 TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.  

 Princeton University shall not be liable under any circumstances for 
 any direct, indirect, special, incidental, or consequential damages 
 with respect to any claim by USER or any third party on account of 
 or arising from the use, or inability to use, this software or its 
 associated documentation, even if Princeton University has been advised
 of the possibility of those damages.
*********************************************************************/
#ifndef __ZCHAFF_INCLUDE__
#define __ZCHAFF_INCLUDE__

#define WORD_SIZE 4
//#define WORD_SIZE 8

//#define SELF_CHECK_ON
//#define DEBUG_ON

using namespace std;

extern int _global_debug_level;
extern int _global_check_level;

#ifndef __FUNCTION__
# define __FUNCTION__ ((char*)0)
#endif

#ifndef __FILE__
# define __FILE__ 0
#endif

#ifndef __LINE__
# define __LINE__ 0
#endif

#define _POSITION_  __FUNCTION__, __FILE__, __LINE__

#ifdef DEBUG_ON
# define DBG(x)		x
# define DBG0(x)	{if(_global_debug_level >= 1){x;}}
# define DBG1(x)	{if(_global_debug_level >= 2){x;}}
# define DBG2(x)	{if(_global_debug_level >= 3){x;}}
#else
# define DBG(x)		
# define DBG0(x)
# define DBG1(x)
# define DBG2(x)
#endif

#ifdef SELF_CHECK_ON
# define CHECK(x)	x
# define CHECK1(x)	{if(_global_check_level >= 1){x;}}
# define CHECK2(x)	{if(_global_check_level >= 2){x;}}
#else
# define CHECK(x)	
# define CHECK1(x)
# define CHECK2(x)
#endif

#if WORD_SIZE == 4
#define WORD_WIDTH 	32
typedef	unsigned	uint32;
typedef int		int32;
typedef long long	long64;
#elif WORD_SIZE == 8
#define WORD_WIDTH 	64
typedef	unsigned int 	uint32;
typedef int		int32;
typedef long		long64;
#endif

void fatal(char * fun, char * file, int lineno, char * fmt, ...);
void warning(char * fun, char * file, int lineno, char * fmt, ...);
double get_cpu_time();

#endif