zchaff_base.h

这是一种很好的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 __BASIC_CLASSES__
#define __BASIC_CLASSES__

#include <assert.h>
#include <iostream>
#include <vector>

#include "zchaff_header.h"

#define UNKNOWN   	2
#define NULL_CLAUSE  	-1

#define VOLATILE_GID   -1
#define	PERMANENT_GID 	0
//#define KEEP_LIT_CLAUSES
typedef int ClauseIdx; //used to refer a clause. Because of dynamic 
// allocation of vector storage, no pointer is allowered

#ifndef _CLS_STATUS_
#define _CLS_STATUS_
enum CLAUSE_STATUS
{
    ORIGINAL_CL,
    CONFLICT_CL,
    DELETED_CL,
    PROBE_CL,
    UNKNOWN_CL
};
#endif

/**Class**********************************************************************

  Synopsis    [Definition of a literal]

  Description [A literal is a variable with phase. Two things specify a literal: 
               its "sign", and its variable index. 

	       Each clause that has more than 1 literal contains two special literals.
	       They are being "watched". A literal is marked with 2 bits: 
	       00->not watched; 11->watched, direction = 1;  01->watched, dir = -1; 
	       10 is not valid. These two bits occupy the least significant bits
	       of the literal. 

	       Each literal is represented by a 32 bit signed integer. The higher 29
	       bits represent the variable index. At most 2**28 varialbes are
	       allowed. If the sign of this integer is negative, it means that it is
	       not a valid literal. It could be a clause index or a deleted literal 
	       pool element. The 3rd least significant bit is used to mark its sign. 
	       0->positive, 1->negative. 

	       The literals are collected in a storage space called literal
	       pool. An element in a literal pool can be a literal or a special
	       spacing element to indicate the termination of a clause. The 
	       spacing elements has negative value of the clause index.]

		Right Hand spacing element has the clause id, so why is it not less than 0?

  SeeAlso     [CDatabase, CClause]

******************************************************************************/

class CLitPoolElement
{
protected:
    int32 _val;

public:
    //constructors & destructors
    CLitPoolElement(void):_val(0)	{}

    ~CLitPoolElement() 			{}

    //member access function
    int & val(void) {
	return _val;
    }

    int s_var(void) { //stands for signed variable, i.e. 2*var_idx + sign
	return _val>>2;
    }

    unsigned var_index(void) {
	return _val>>3; 
    }

    unsigned var_sign(void) { 
	return ( (_val>> 2)& 0x1); 
    }

    void set (int s_var) {
	_val = (s_var << 2);
    }

    void set(int vid, int sign) { 
	_val = (((vid<<1) + sign)<< 2); 
    }

    //followings are for manipulate watched literals
    int direction (void) {
	return ((_val&0x03) - 2);
    }

    bool is_watched(void) {
	return ((_val&0x03) != 0);
    }

    void unwatch(void) {
	_val = _val & (~0x3);
    }

    void set_watch(int dir) {
	_val = _val + dir + 2;
    }

    //following are used for spacing (e.g. indicate clause's end)
    bool is_literal(void) {
	return _val > 0;
    }

    void set_clause_index(int cl_idx) {
	_val = - cl_idx;
    }

    ClauseIdx get_clause_index(void) {
	assert (_val <= 0);
	return -_val; 
    }

    //misc functions
    unsigned find_clause_index(void) {
	CLitPoolElement * ptr;
	for (ptr = this; ptr->is_literal(); ++ ptr);
	return ptr->get_clause_index();
    }

    //every class should have a dump function and a self check function
    void dump(ostream & os= cout);

    friend ostream & operator << ( ostream & os, CLitPoolElement & l) { 
	l.dump(os); 
	return os;
    }
};


/**Class**********************************************************************

  Synopsis    [Definition of a clause]

  Description [A clause is consisted of a certain number of literals. 
               All literals are collected in a single large vector, called
	       literal pool. Each clause has a pointer to the beginning position
	       of it's literals in the pool. 
	       
	       Zchaff support incremental SAT. Clauses can be added or deleted
	       from the database during search. To accomodate this feature, some 
	       modifications are needed.

	       Clauses can be generated during search by conflict driven analysis.
	       Conflict clauses are generated by a resolution process. 
	       Therefore, if after one search, some clauses got deleted, then 
	       some of the learned conflict clause may be invalidated. To maintain
	       the integrity of the clause database, it is necessary to keep track
	       of the clauses that are involved in the resolution process for a
	       certain conflict clause so that when those clauses are deleted,
	       the conflict clause should also be deleted. 
	       
	       The scheme we implement is similar to the scheme described in:
	       Ofer Strichman, Pruning techniques for the SAT-based Bounded Model 
	       Checking Problems, in Proc. 11th Advanced Research Working Conference on 
	       Correct Hardware Design and Verification Methods (CHARME'01)
	       ]

  SeeAlso     [CDatabase]

******************************************************************************/
class CClause
{
protected:
    CLitPoolElement *	_first_lit;	//pointer to the first literal in literal pool
    unsigned 		_num_lits ;	//number of literals
    CLAUSE_STATUS 	_status	: 3;	//indicate if this clause has been deleted or not
    unsigned		_id	: 29;	//the unique ID of a clause
    unsigned		_gflag;		//the clause group id flag, maximum allow WORD_WIDTH groups
    int                 _activity;
    int                 _sat_lit_idx;
    
public:

//constructors & destructors
    CClause(void){
	_status = UNKNOWN_CL;
	_sat_lit_idx=0;
    }

    ~CClause() {}

//initialization & clear up
    void init(CLitPoolElement * head, unsigned num_lits, unsigned gflag) { //initialization of a clause
	_first_lit = head;
	_num_lits = num_lits;
	_gflag = gflag;
    }

//member access function
    int & activity(void){
        return _activity;
    }
 
    int & sat_lit_idx (void){
        return _sat_lit_idx;
    }
 
    CLitPoolElement * literals(void) 	{ 	//literals()[i] is it's the i-th literal
	return _first_lit; 
    }	

    CLitPoolElement & literal(int idx) 	{ 	//return the idx-th literal
	return *(_first_lit + idx); 
    }

    CLitPoolElement * & first_lit(void) {	//use it only if you want to modify _first_lit
	return _first_lit; 
    }

    unsigned & num_lits(void) { 
	return _num_lits; 
    }

    unsigned id(void) {
	return _id;
    }

    void set_id(int id) {
	_id = id;
    }

    CLAUSE_STATUS status(void) { 
	return _status; 
    }

    void set_status(CLAUSE_STATUS st) { 
	_status = st;
    }

//manipulate the group flag
    unsigned & gflag(void) {
	return _gflag;
    }

    bool gid (int i) {
	assert (i>=1 && i<= WORD_WIDTH);
	return (( _gflag & (1<<(i-1))) != 0);
    }

    void set_gid (int i) {
	assert (i>=1 && i<= WORD_WIDTH);
	_gflag |= (1<<(i-1));
    }

    void clear_gid(int i) {
	assert (i>=1 && i<= WORD_WIDTH);
	_gflag &= ~(1<<(i-1));
    }

//misc function
    bool self_check(void);

    void dump(ostream & os = cout); 

    friend ostream & operator << ( ostream & os, CClause & cl) { 
	cl.dump(os); 
	return os;
    }
};


/**Class**********************************************************************

  Synopsis    [Definition of a variable]

  Description [CVariable contains the necessary information for a variable.]

  SeeAlso     [CDatabase]

******************************************************************************/
class CVariable 
{
protected:
    unsigned _value		: 2;	//it can take 3 values, 0, 1 and UNKNOWN

    bool _marked		: 1;	//used in conflict analysis.
    
    unsigned _new_cl_phase	: 2;	//it can take 3 value 
    //0: pos phase, 1: neg phase, UNKNOWN : not in new clause;
    //It is used to keep track of literals appearing
    //in newly added clause so that 
    //a. each variable can only appearing in one phase
    //b. same literal won't appear more than once.
    bool _enable_branch 	: 1;	//if this variable is enabled in branch selection

    int _implied_sign		: 1;	//when a var is implied, here is the sign (1->negative, 0->positive)

    ClauseIdx _antecedent	;   	//used in conflict analysis. 

    int _dlevel; 			//decision level this variable being assigned

    int _assgn_stack_pos;	;	//the position where it is in the assignment stack

    int _lits_count[2];			//how many literals are there with this variable. (two phases)
 
    int _2_lits_count[2];			//how many literals are there with this variable. (two phases)


    vector<CLitPoolElement *> _watched[2];	//watched literals of this var. 0: pos phase, 1: neg phase

#ifdef KEEP_LIT_CLAUSES
    vector<ClauseIdx> _lit_clauses[2];	//this will keep track of ALL the appearance of the variable in clauses
    //note this will increase the database size by upto a factor of 2
#endif
    int _scores[2];			//the score used for decision making

    int _var_score_pos;			//keep track of this variable's position in the sorted score array

public:
//constructors & destructors
    CVariable(void) {
	init();
	_lits_count[0] = _lits_count[1] = 0;
        _2_lits_count[0] = _2_lits_count[1] = 0;
    }

    ~CVariable() {}

    void init(void) {
	_value = UNKNOWN; 
	_antecedent=NULL_CLAUSE; 
	_marked = false;
	_dlevel = -1; 
	_assgn_stack_pos = -1;
	_new_cl_phase = UNKNOWN;	
	_scores[0] = _scores[1] = 0;
	//_conf_scores[0] = _conf_scores[1] = 0;
	_enable_branch = true;
    }
//member access function
    int & score(int i) 	{ 
	return _scores[i]; 
    }

    int & two_lits_count(int i){
        return _2_lits_count[i];
    }
    
    int score(void)	{ 
//	return 1;	//this will make a fixed order branch heuristic
	int result=score(0)>score(1)?score(0):score(1);
	if(_dlevel==0) result =-1;
	return result;
    }

    int & var_score_pos(void) {
	return _var_score_pos; 
    }
    
    void set_var_score_pos(int pos) {
	_var_score_pos = pos;
    }

    unsigned value(void) { 
	return _value;
    }

    void set_value(unsigned v) {
	_value = v;
    }

    int & dlevel(void) { 
	return _dlevel;
    }

    int get_dlevel(void) {
	return _dlevel;
    }

    void set_dlevel(int dl) {
	_dlevel = dl;
    }

    int & assgn_stack_pos(void) {
	return _assgn_stack_pos;
    }

    int & lits_count(int i) { 
	return _lits_count[i];
    }

    bool is_marked(void) { 
	return _marked; 
    }    
    
    int get_implied_sign(void) {
	return _implied_sign;
    }
    
    void set_implied_sign(int sign) {
	_implied_sign = sign;
    }

    unsigned new_cl_phase(void) { 
	return _new_cl_phase; 
    } 

    void set_new_cl_phase(unsigned phase) { 
	_new_cl_phase = phase; 
    }

    void set_marked(void) { 
	_marked = true; 
    }

    void clear_marked(void) { 
	_marked = false; 
    }

    ClauseIdx & antecedent(void) { 
	return _antecedent; 
    }
    
    ClauseIdx get_antecedent(void) { 
	return _antecedent; 
    }
    
    void set_antecedent(ClauseIdx cl) {
	_antecedent = cl;
    }

    vector<CLitPoolElement *> & watched(int i) { 
	return _watched[i]; 
    }

    void enable_branch(void) {
	_enable_branch = true;
    }

    void disable_branch(void) {
	_enable_branch = false;
    }

    bool is_branchable(void) {
	return _enable_branch;
    }
#ifdef KEEP_LIT_CLAUSES
    vector<ClauseIdx> & lit_clause(int i) {
	return _lit_clauses[i]; 
    }
#endif    

//misc function
    bool self_check(void);

    void  dump(ostream & os=cout);

    friend ostream & operator << ( ostream & os, CVariable & v) { 
	v.dump(os); 
	return os;
    }
};

#endif