satClause.h File Reference

#include "misc/util/abc_global.h"

Include dependency graph for satClause.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	clause_t
struct	Sat_Mem_t_

Macros
#define	LEARNT_MAX_START_DEFAULT   10000
	INCLUDES ///.
#define	LEARNT_MAX_INCRE_DEFAULT   1000
#define	LEARNT_MAX_RATIO_DEFAULT   50
#define	Sat_MemForEachClause(p, c, i, k)
#define	Sat_MemForEachClause2(p, c, i, k)
#define	Sat_MemForEachLearned(p, c, i, k)

Typedefs
typedef struct clause_t	clause
	STRUCTURE DEFINITIONS ///.
typedef struct Sat_Mem_t_	Sat_Mem_t

Macro Definition Documentation

LEARNT_MAX_INCRE_DEFAULT

#define LEARNT_MAX_INCRE_DEFAULT   1000

Definition at line 38 of file satClause.h.

LEARNT_MAX_RATIO_DEFAULT

#define LEARNT_MAX_RATIO_DEFAULT   50

Definition at line 39 of file satClause.h.

LEARNT_MAX_START_DEFAULT

#define LEARNT_MAX_START_DEFAULT   10000

INCLUDES ///.

CFile****************************************************************

FileName [satMem.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT solver.]

Synopsis [Memory management.]

Author [Alan Mishchenko alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 1, 2004.]

Revision [

Id

satMem.h,v 1.0 2004/01/01 1:00:00 alanmi Exp

] PARAMETERS ///

Definition at line 37 of file satClause.h.

Sat_MemForEachClause

#define Sat_MemForEachClause	(		p,
			c,
			i,
			k )

Value:

    for ( i = 0; i <= p->iPage[0]; i += 2 )     \
        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) ) if ( i == 0 && k == 2 ) {} else

Definition at line 118 of file satClause.h.

#define Sat_MemForEachClause( p, c, i, k )      \
    for ( i = 0; i <= p->iPage[0]; i += 2 )     \
        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) ) if ( i == 0 && k == 2 ) {} else

Sat_MemForEachClause2

#define Sat_MemForEachClause2	(		p,
			c,
			i,
			k )

Value:

    for ( i = 0; i <= p->iPage[0]; i += 2 )     \
        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize2(c) ) if ( i == 0 && k == 2 ) {} else

Definition at line 123 of file satClause.h.

#define Sat_MemForEachClause2( p, c, i, k )      \
    for ( i = 0; i <= p->iPage[0]; i += 2 )     \
        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize2(c) ) if ( i == 0 && k == 2 ) {} else

Sat_MemForEachLearned

#define Sat_MemForEachLearned	(		p,
			c,
			i,
			k )

Value:

    for ( i = 1; i <= p->iPage[1]; i += 2 )     \
        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) )

Definition at line 127 of file satClause.h.

#define Sat_MemForEachLearned( p, c, i, k )     \
    for ( i = 1; i <= p->iPage[1]; i += 2 )     \
        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) )

Typedef Documentation

clause

typedef struct clause_t clause

STRUCTURE DEFINITIONS ///.

Definition at line 48 of file satClause.h.

Sat_Mem_t

typedef struct Sat_Mem_t_ Sat_Mem_t

Definition at line 70 of file satClause.h.