zchaff_wrapper.wrp

这是一种很好的SAT解析器。通过它

}

EXTERN int SAT_NumDecisions	(SAT_Manager mng)
{
    CSolver * solver = (CSolver*) mng;	
    int n = solver->num_decisions();
    TRACE (trace_os << "SAT_NumDecisions\t" << mng << "\t" << n << endl;);
    return n;
}

EXTERN int SAT_NumDecisionsStackConf	(SAT_Manager mng)
{
    CSolver * solver = (CSolver*) mng;	
    int n = solver->num_decisions_stack_conf();
    TRACE (trace_os << "SAT_NumDecisions_Stack_Conf\t" << mng << "\t" << n << endl;);
    return n;
}

EXTERN int SAT_NumDecisionsVsids	(SAT_Manager mng)
{
    CSolver * solver = (CSolver*) mng;	
    int n = solver->num_decisions_vsids();
    TRACE (trace_os << "SAT_NumDecisions_Vsids\t" << mng << "\t" << n << endl;);
    return n;
}

EXTERN int SAT_NumDecisionsShrinking	(SAT_Manager mng)
{
    CSolver * solver = (CSolver*) mng;	
    int n = solver->num_decisions_shrinking();
    TRACE (trace_os << "SAT_NumDecisions_Shrinking\t" << mng << "\t" << n << endl;);
    return n;
}

EXTERN int SAT_NumShrinkings	(SAT_Manager mng)
{
    CSolver * solver = (CSolver*) mng;	
    int n = solver->num_shrinkings();
    TRACE (trace_os << "SAT_NumShrinkings\t" << mng << "\t" << n << endl;);
    return n;
}

EXTERN int SAT_Random_Seed	(SAT_Manager mng)
{
    CSolver * solver = (CSolver*) mng;	
    int n = solver->random_seed();
    TRACE (trace_os << "SAT_Random_Seed\t" << mng << "\t" << n << endl;);
    return n;
}



EXTERN long64 SAT_NumImplications	(SAT_Manager mng)
{
    CSolver * solver = (CSolver*) mng;	
    long64 n = solver->num_implications();
    TRACE (trace_os << "SAT_NumImplications\t" << mng << "\t" << n << endl;);
    return n;
}

EXTERN int SAT_MaxDLevel	(SAT_Manager mng)
{
    CSolver * solver = (CSolver*) mng;	
    int n = solver->max_dlevel();
    TRACE (trace_os << "SAT_MaxDLevel\t" << mng << "\t" << n << endl;);
    return n;
}

EXTERN float SAT_AverageBubbleMove	(SAT_Manager mng)
{
    CSolver * solver = (CSolver*) mng;	
    float n = ((float) solver->total_bubble_move()) / 
	(solver->num_added_literals() - solver->init_num_literals());
    TRACE (trace_os << "SAT_AverageBubbleMove\t" << mng << "\t" << n << endl;);
    return n;
}


EXTERN int SAT_GetFirstClause(SAT_Manager mng)
{
    CSolver * solver = (CSolver*) mng;	
    TRACE (trace_os << "SAT_GetFirstClause\t" << mng << "\t";);
    for (unsigned i=0; i< solver->clauses().size(); ++i)
	if ( solver->clause(i).status() != DELETED_CL) {
	    TRACE ( trace_os << i << endl; );
	    return i;
	}
    TRACE ( trace_os << -1 << endl; );
    return -1;
}

EXTERN int SAT_GetClauseType (SAT_Manager mng, int cl_idx)
{
    CSolver * solver = (CSolver*) mng;	
    int type = solver->clause(cl_idx).status();
    TRACE (trace_os << "SAT_GetClauseType\t" << mng << "\t" << type << endl;);
    return type;
}


EXTERN int SAT_IsSetClauseGroupID( SAT_Manager mng, int cl_idx, int id)
{
    CSolver * solver = (CSolver*) mng;	
    int r = solver->clause(cl_idx).gid(id);
    TRACE (trace_os << "SAT_IsSetClauseGroupID\t" << mng
	   << " " << cl_idx << " " << id << "\t" << r << endl;);
    return r;
}

EXTERN void SAT_ClearClauseGroupID( SAT_Manager mng, int cl_idx, int id)
{
    CSolver * solver = (CSolver*) mng;	
    TRACE (trace_os << "SAT_ClearClauseGroupID\t" 
	   << mng << " " << cl_idx << " " << id << endl;);
    solver->clause(cl_idx).clear_gid(id);
}

EXTERN void SAT_SetClauseGroupID( SAT_Manager mng, int cl_idx, int id)
{
    CSolver * solver = (CSolver*) mng;	
    TRACE (trace_os << "SAT_SetClauseGroupID\t" << mng 
	   << " " << cl_idx << " " << id << endl;);
    solver->clause(cl_idx).set_gid(id);
}

EXTERN int SAT_GetNextClause	(SAT_Manager mng, int cl_idx)
{
    CSolver * solver = (CSolver*) mng;	
    TRACE ( trace_os << "SAT_GetNextClause\t" << mng << " " << cl_idx <<"\t";);
    for (unsigned i= cl_idx + 1; i< solver->clauses().size(); ++i)
	if ( solver->clause(i).status() != DELETED_CL) {
	    TRACE (trace_os << i << endl;);
	    return i;
	}
    TRACE (trace_os << -1 << endl;);
    return -1;
}

EXTERN int SAT_GetClauseNumLits(SAT_Manager mng, int cl_idx)
{
    CSolver * solver = (CSolver*) mng;	
    int n = solver->clause(cl_idx).num_lits();
    TRACE ( trace_os << "SAT_GetClauseNumLits\t" << mng 
	    << " " << cl_idx <<"\t" << n << endl;);
    return n;
}

EXTERN void SAT_GetClauseLits(SAT_Manager mng, int cl_idx,  int * lits)
{
    CSolver * solver = (CSolver*) mng;	
    TRACE ( trace_os << "SAT_GetClauseLits\t" << mng 
	    << " " << cl_idx; );
    for (unsigned i=0; i< solver->clause(cl_idx).num_lits(); ++i) {
	lits[i] = solver->clause(cl_idx).literal(i).s_var();
	TRACE( trace_os << " " << lits[i];);
    }
    TRACE (trace_os << endl;);
}

EXTERN void SAT_EnableConfClsDeletion(SAT_Manager mng)
{
    CSolver * solver = (CSolver*) mng;	
    TRACE ( trace_os << "SAT_EnableConfClsDeletion\t" << mng << endl;);
    solver->enable_cls_deletion(true);
}

EXTERN void SAT_DisableConfClsDeletion(SAT_Manager mng)
{
    CSolver * solver = (CSolver*) mng;	
    TRACE ( trace_os << "SAT_DisableConfClsDeletion\t" << mng << endl;);
    solver->enable_cls_deletion(false);
}

EXTERN void SAT_CleanUpDatabase (SAT_Manager mng)
{
    CSolver * solver = (CSolver*) mng;	
    TRACE ( trace_os << "SAT_CleanUpDatabase\t" << mng<< endl; );
    solver->clean_up_dbase();    
}


EXTERN void SAT_GenClsAnd2	(SAT_Manager mng, 
				 int a,
				 int b,
				 int o,
				 int gid = 0 )
{
    CSolver * solver = (CSolver*) mng;	
    CClause_Gen cls_gen;
    TRACE ( trace_os << "SAT_GenClsAnd2\t" << mng
	    <<" " << a << " " << b << " " << o << " " << gid << endl; );
    cls_gen.and2 (*solver, a, b, o, gid);
}

EXTERN void SAT_GenClsAndN	(SAT_Manager mng, 
				 int * inputs,
				 int num_inputs,
				 int o,
				 int gid = 0) 
{
    CSolver * solver = (CSolver*) mng;	
    CClause_Gen cls_gen;
    TRACE ( trace_os << "SAT_GenClsAndN\t" << mng << " ";
	    for (int i=0; i< num_inputs; ++i) 
	    trace_os << inputs[i] << " " ; 
	    trace_os << num_inputs << " " << o << " " << gid << endl;);
    cls_gen.and_n (*solver, inputs, num_inputs, o, gid);

}

EXTERN void SAT_GenClsOr2	(SAT_Manager mng, 
			 int a,
			 int b,
			 int o,
				 int gid = 0) 
{
    CSolver * solver = (CSolver*) mng;	
    CClause_Gen cls_gen;
    TRACE ( trace_os << "SAT_GenClsOr2\t" << mng
	    <<" " << a << " " << b << " " << o << " " << gid << endl; );
    cls_gen.or2 (*solver, a, b, o, gid);
}

EXTERN void SAT_GenClsOrN	(SAT_Manager mng, 
				 int * inputs,
				 int num_inputs,
				 int o, 
				 int gid = 0 )
{
    CSolver * solver = (CSolver*) mng;	
    CClause_Gen cls_gen;
    TRACE ( trace_os << "SAT_GenClsOrN\t" << mng << " ";
	    for (int i=0; i< num_inputs; ++i) 
	    trace_os << inputs[i] << " " ; 
	    trace_os << num_inputs << " " << o << " " << gid << endl;);
    cls_gen.or_n (*solver, inputs, num_inputs, o, gid);
}

EXTERN void SAT_GenClsNand2	(SAT_Manager mng, 
				 int a,
				 int b,
				 int o,
				 int gid = 0)
{
    CSolver * solver = (CSolver*) mng;	
    CClause_Gen cls_gen;
    TRACE ( trace_os << "SAT_GenClsNand2\t" << mng
	    <<" " << a << " " << b << " " << o << " " << gid << endl; );
    cls_gen.nand2 (*solver, a, b, o, gid);
}


EXTERN void SAT_GenClsNandN	(SAT_Manager mng, 
				 int * inputs,
				 int num_inputs,
				 int o, 
				 int gid = 0 )
{
    CSolver * solver = (CSolver*) mng;	
    CClause_Gen cls_gen;
    TRACE ( trace_os << "SAT_GenClsNandN\t" << mng << " ";
	    for (int i=0; i< num_inputs; ++i) 
	    trace_os << inputs[i] << " " ; 
	    trace_os << num_inputs << " " << o << " " << gid << endl;);
    cls_gen.nand_n (*solver, inputs, num_inputs, o, gid);
}


EXTERN void SAT_GenClsNor2	(SAT_Manager mng, 
				 int a,
				 int b,	
				 int o, 
				 int gid = 0 )
{
    CSolver * solver = (CSolver*) mng;	
    CClause_Gen cls_gen;
    TRACE ( trace_os << "SAT_GenClsNor2\t" << mng
	    <<" " << a << " " << b << " " << o << " " << gid << endl; );
    cls_gen.nor2 (*solver, a, b, o, gid);
}


EXTERN void SAT_GenClsNorN	(SAT_Manager mng, 
				 int * inputs,
				 int num_inputs,
				 int o, 
				 int gid = 0 )
{
    CSolver * solver = (CSolver*) mng;	
    CClause_Gen cls_gen;
    TRACE ( trace_os << "SAT_GenClsNorN\t" << mng << " ";
	    for (int i=0; i< num_inputs; ++i) 
	    trace_os << inputs[i] << " " ; 
	    trace_os << num_inputs << " " << o << " " << gid << endl;);
    cls_gen.nor_n (*solver, inputs, num_inputs, o, gid);
}

EXTERN void SAT_GenClsXor	(SAT_Manager mng, 
				 int a,
				 int b,	
				 int o,
				 int gid = 0)
{
    CSolver * solver = (CSolver*) mng;	
    CClause_Gen cls_gen;
    TRACE ( trace_os << "SAT_GenClsXor2\t" << mng
	    <<" " << a << " " << b << " " << o << " " << gid << endl; );
    cls_gen.xor2 (*solver, a, b, o, gid);
}

EXTERN void SAT_GenClsNot	(SAT_Manager mng, 
				 int a,
				 int o,
				 int gid = 0)
{
    CSolver * solver = (CSolver*) mng;	
    CClause_Gen cls_gen;
    TRACE ( trace_os << "SAT_GenClsNot\t" << mng
	    <<" " << a << " " << o << " " << gid << endl; );
    cls_gen.not1 (*solver, a, o, gid);
}