satVec.h File Reference

#include "misc/util/abc_global.h"

Go to the source code of this file.

Data Structures
struct	veci_t
struct	vecp_t
struct	stats_t

Macros
#define	false   0
#define	true   1

Typedefs
typedef struct veci_t	veci
typedef struct vecp_t	vecp
typedef int	lit
typedef int	cla
typedef char	lbool
typedef struct stats_t	stats_t

Functions
static void	veci_new (veci *v)
static void	veci_delete (veci *v)
static int *	veci_begin (veci *v)
static int	veci_size (veci *v)
static void	veci_resize (veci *v, int k)
static int	veci_pop (veci *v)
static void	veci_push (veci *v, int e)
static void	veci_remove (veci *v, int e)
static void	vecp_new (vecp *v)
static void	vecp_delete (vecp *v)
static void **	vecp_begin (vecp *v)
static int	vecp_size (vecp *v)
static void	vecp_resize (vecp *v, int k)
static void	vecp_push (vecp *v, void *e)
static void	vecp_remove (vecp *v, void *e)
static lit	toLit (int v)
static lit	toLitCond (int v, int c)
static lit	lit_neg (lit l)
static int	lit_var (lit l)
static int	lit_sign (lit l)
static int	lit_print (lit l)
static lit	lit_read (int s)
static int	lit_check (lit l, int n)

Variables
static const int	var_Undef = -1
static const lit	lit_Undef = -2
static const lbool	l_Undef = 0
static const lbool	l_True = 1
static const lbool	l_False = -1

Macro Definition Documentation

#define false   0

Definition at line 123 of file satVec.h.

#define true   1

Definition at line 126 of file satVec.h.

Typedef Documentation

typedef int cla

Definition at line 131 of file satVec.h.

typedef char lbool

Definition at line 133 of file satVec.h.

typedef int lit

Definition at line 130 of file satVec.h.

typedef struct stats_t stats_t

Definition at line 157 of file satVec.h.

typedef struct veci_t veci

Definition at line 36 of file satVec.h.

typedef struct vecp_t vecp

Definition at line 85 of file satVec.h.

Function Documentation

static int lit_check ( lit  l, int  n  )

inlinestatic

Definition at line 149 of file satVec.h.

{ return l >= 0 && lit_var(l) < n;                  }

static lit lit_neg ( lit  l )

inlinestatic

Definition at line 144 of file satVec.h.

{ return l ^ 1; }

static int lit_print ( lit  l )

inlinestatic

Definition at line 147 of file satVec.h.

{ return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }

static lit lit_read ( int  s )

inlinestatic

Definition at line 148 of file satVec.h.

{ return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }

static int lit_sign ( lit  l )

inlinestatic

Definition at line 146 of file satVec.h.

{ return l & 1; }

static int lit_var ( lit  l )

inlinestatic

Definition at line 145 of file satVec.h.

{ return l >> 1; }

static lit toLit ( int  v )

inlinestatic

Definition at line 142 of file satVec.h.

{ return v + v; }

static lit toLitCond ( int  v, int  c  )

inlinestatic

Definition at line 143 of file satVec.h.

{ return v + v + (c != 0); }

static int* veci_begin ( veci *  v )

inlinestatic

Definition at line 45 of file satVec.h.

{ return v->ptr;  }

static void veci_delete ( veci *  v )

inlinestatic

Definition at line 44 of file satVec.h.

{ ABC_FREE(v->ptr);   }

static void veci_new ( veci *  v )

inlinestatic

Definition at line 38 of file satVec.h.

                                      {
    v->cap  = 4;
    v->size = 0;
    v->ptr  = (int*)ABC_ALLOC( char, sizeof(int)*v->cap);
}

static int veci_pop ( veci *  v )

inlinestatic

Definition at line 52 of file satVec.h.

{ assert(v->size); return v->ptr[--v->size]; }

static void veci_push ( veci *  v, int  e  )

inlinestatic

Definition at line 53 of file satVec.h.

{
    if (v->size == v->cap) {
//        int newsize = v->cap * 2;//+1;
        int newsize = (v->cap < 4) ? v->cap * 2 : (v->cap / 2) * 3;
        v->ptr = ABC_REALLOC( int, v->ptr, newsize );
        if ( v->ptr == NULL )
        {
            printf( "Failed to realloc memory from %.1f MB to %.1f MB.\n", 
                1.0 * v->cap / (1<<20), 1.0 * newsize / (1<<20) );
            fflush( stdout );
        }
        v->cap = newsize; }
    v->ptr[v->size++] = e;
}

static void veci_remove ( veci *  v, int  e  )

inlinestatic

Definition at line 68 of file satVec.h.

{
    int * ws = (int*)veci_begin(v);
    int    j  = 0;
    for (; ws[j] != e  ; j++);
    assert(j < veci_size(v));
    for (; j < veci_size(v)-1; j++) ws[j] = ws[j+1];
    veci_resize(v,veci_size(v)-1);
}

static void veci_resize ( veci *  v, int  k  )

inlinestatic

Definition at line 47 of file satVec.h.

                                                    { 
    assert(k <= v->size); 
//    memset( veci_begin(v) + k, -1, sizeof(int) * (veci_size(v) - k) );
    v->size = k;         
} // only safe to shrink !!

static int veci_size ( veci *  v )

inlinestatic

Definition at line 46 of file satVec.h.

{ return v->size; }

static void** vecp_begin ( vecp *  v )

inlinestatic

Definition at line 94 of file satVec.h.

{ return v->ptr;  }

static void vecp_delete ( vecp *  v )

inlinestatic

Definition at line 93 of file satVec.h.

{ ABC_FREE(v->ptr);   }

static void vecp_new ( vecp *  v )

inlinestatic

Definition at line 87 of file satVec.h.

                                      {
    v->size = 0;
    v->cap  = 4;
    v->ptr  = (void**)ABC_ALLOC( char, sizeof(void*)*v->cap);
}

static void vecp_push ( vecp *  v, void *  e  )

inlinestatic

Definition at line 97 of file satVec.h.

{
    if (v->size == v->cap) {
//        int newsize = v->cap * 2;//+1;
        int newsize = (v->cap < 4) ? v->cap * 2 : (v->cap / 2) * 3;
        v->ptr = ABC_REALLOC( void*, v->ptr, newsize );
        v->cap = newsize; }
    v->ptr[v->size++] = e;
}

static void vecp_remove ( vecp *  v, void *  e  )

inlinestatic

Definition at line 106 of file satVec.h.

{
    void** ws = vecp_begin(v);
    int    j  = 0;
    for (; ws[j] != e  ; j++);
    assert(j < vecp_size(v));
    for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1];
    vecp_resize(v,vecp_size(v)-1);
}

static void vecp_resize ( vecp *  v, int  k  )

inlinestatic

Definition at line 96 of file satVec.h.

{ assert(k <= v->size); v->size = k;    } // only safe to shrink !!

static int vecp_size ( vecp *  v )

inlinestatic

Definition at line 95 of file satVec.h.

{ return v->size; }

Variable Documentation

const lbool l_False = -1

static

Definition at line 140 of file satVec.h.

const lbool l_True = 1

static

Definition at line 139 of file satVec.h.

const lbool l_Undef = 0

static

Definition at line 138 of file satVec.h.

const lit lit_Undef = -2

static

Definition at line 136 of file satVec.h.

const int var_Undef = -1

static

Definition at line 135 of file satVec.h.