abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
satUtil.c File Reference
#include <stdio.h>
#include <assert.h>
#include "satSolver.h"
#include "satSolver2.h"

Go to the source code of this file.

Functions

static
ABC_NAMESPACE_IMPL_START void 
Sat_SolverClauseWriteDimacs (FILE *pFile, clause *pC, int fIncrement)
 DECLARATIONS ///. More...
 
void Sat_SolverWriteDimacs (sat_solver *p, char *pFileName, lit *assumpBegin, lit *assumpEnd, int incrementVars)
 
void Sat_Solver2WriteDimacs (sat_solver2 *p, char *pFileName, lit *assumpBegin, lit *assumpEnd, int incrementVars)
 
void Sat_SolverPrintStats (FILE *pFile, sat_solver *p)
 
void Sat_Solver2PrintStats (FILE *pFile, sat_solver2 *s)
 
int Sat_Solver2GetVarMem (sat_solver2 *s)
 
int * Sat_SolverGetModel (sat_solver *p, int *pVars, int nVars)
 
int * Sat_Solver2GetModel (sat_solver2 *p, int *pVars, int nVars)
 
void Sat_SolverDoubleClauses (sat_solver *p, int iVar)
 

Function Documentation

int* Sat_Solver2GetModel ( sat_solver2 p,
int *  pVars,
int  nVars 
)

Function*************************************************************

Synopsis [Returns a counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 287 of file satUtil.c.

288 {
289  int * pModel;
290  int i;
291  pModel = ABC_CALLOC( int, nVars+1 );
292  for ( i = 0; i < nVars; i++ )
293  pModel[i] = sat_solver2_var_value(p, pVars[i]);
294  return pModel;
295 }
static int sat_solver2_var_value(sat_solver2 *s, int v)
Definition: satSolver2.h:210
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
int Sat_Solver2GetVarMem ( sat_solver2 s)

Function*************************************************************

Synopsis [Returns the number of bytes used for each variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 240 of file satUtil.c.

241 {
242  int Mem = 0;
243  Mem += (sizeof(s->activity[0]) == 4) ? sizeof(unsigned) : sizeof(double); // activity
244  Mem += 2 * sizeof(veci); // wlists
245  Mem += sizeof(int); // vi (variable info)
246  Mem += sizeof(int); // trail
247  Mem += sizeof(int); // orderpos
248  Mem += sizeof(int); // reasons
249  Mem += sizeof(int); // units
250  Mem += sizeof(int); // order
251  Mem += sizeof(int); // model
252  return Mem;
253 }
struct veci_t veci
Definition: satVec.h:36
unsigned * activity
Definition: satSolver2.h:112
void Sat_Solver2PrintStats ( FILE *  pFile,
sat_solver2 s 
)

Function*************************************************************

Synopsis [Writes the given clause in a file in DIMACS format.]

Description []

SideEffects []

SeeAlso []

Definition at line 210 of file satUtil.c.

211 {
212  printf( "starts : %10d\n", (int)s->stats.starts );
213  printf( "conflicts : %10d\n", (int)s->stats.conflicts );
214  printf( "decisions : %10d\n", (int)s->stats.decisions );
215  printf( "propagations : %10d\n", (int)s->stats.propagations );
216 // printf( "inspects : %10d\n", (int)s->stats.inspects );
217 // printf( "inspects2 : %10d\n", (int)s->stats.inspects2 );
218 /*
219  printf( "memory for variables %.1f MB (free %6.2f %%) and clauses %.1f MB (free %6.2f %%)\n",
220  1.0 * Sat_Solver2GetVarMem(s) * s->size / (1<<20),
221  100.0 * (s->cap - s->size) / s->cap,
222  4.0 * (s->clauses.cap + s->learnts.cap) / (1<<20),
223  100.0 * (s->clauses.cap - s->clauses.size +
224  s->learnts.cap - s->learnts.size) /
225  (s->clauses.cap + s->learnts.cap) );
226 */
227 }
ABC_INT64_T decisions
Definition: satVec.h:154
stats_t stats
Definition: satSolver2.h:172
ABC_INT64_T conflicts
Definition: satVec.h:154
ABC_INT64_T propagations
Definition: satVec.h:154
unsigned starts
Definition: satVec.h:153
void Sat_Solver2WriteDimacs ( sat_solver2 p,
char *  pFileName,
lit assumpBegin,
lit assumpEnd,
int  incrementVars 
)

Definition at line 123 of file satUtil.c.

124 {
125  Sat_Mem_t * pMem = &p->Mem;
126  FILE * pFile;
127  clause * c;
128  int i, k, nUnits;
129 
130  // count the number of unit clauses
131  nUnits = 0;
132  for ( i = 0; i < p->size; i++ )
133  if ( p->levels[i] == 0 && p->assigns[i] != 3 )
134  nUnits++;
135 
136  // start the file
137  pFile = fopen( pFileName, "wb" );
138  if ( pFile == NULL )
139  {
140  printf( "Sat_SolverWriteDimacs(): Cannot open the ouput file.\n" );
141  return;
142  }
143 // fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
144  fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0)-1+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(int)(assumpEnd-assumpBegin) );
145 
146  // write the original clauses
147  Sat_MemForEachClause2( pMem, c, i, k )
148  Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
149 
150  // write the learned clauses
151 // Sat_MemForEachLearned( pMem, c, i, k )
152 // Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
153 
154  // write zero-level assertions
155  for ( i = 0; i < p->size; i++ )
156  if ( p->levels[i] == 0 && p->assigns[i] != 3 ) // varX
157  fprintf( pFile, "%s%d%s\n",
158  (p->assigns[i] == 1)? "-": "", // var0
159  i + (int)(incrementVars>0),
160  (incrementVars) ? " 0" : "");
161 
162  // write the assump
163  if (assumpBegin) {
164  for (; assumpBegin != assumpEnd; assumpBegin++) {
165  fprintf( pFile, "%s%d%s\n",
166  lit_sign(*assumpBegin)? "-": "",
167  lit_var(*assumpBegin) + (int)(incrementVars>0),
168  (incrementVars) ? " 0" : "");
169  }
170  }
171 
172  fprintf( pFile, "\n" );
173  fclose( pFile );
174 }
#define Sat_MemForEachClause2(p, c, i, k)
Definition: satClause.h:122
static int lit_var(lit l)
Definition: satVec.h:145
Sat_Mem_t Mem
Definition: satSolver2.h:129
static ABC_NAMESPACE_IMPL_START void Sat_SolverClauseWriteDimacs(FILE *pFile, clause *pC, int fIncrement)
DECLARATIONS ///.
Definition: satUtil.c:50
for(p=first;p->value< newval;p=p->next)
if(last==0)
Definition: sparse_int.h:34
static int size
Definition: cuddSign.c:86
static int lit_sign(lit l)
Definition: satVec.h:146
static int Sat_MemEntryNum(Sat_Mem_t *p, int lrn)
Definition: satClause.h:99
char * assigns
Definition: satSolver2.h:142
void Sat_SolverClauseWriteDimacs ( FILE *  pFile,
clause pC,
int  fIncrement 
)
static

DECLARATIONS ///.

FUNCTION DEFINITIONS ///.

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

FileName [satUtil.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [C-language MiniSat solver.]

Synopsis [Additional SAT solver procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:
satUtil.c,v 1.4 2005/09/16 22:55:03 casem Exp

]

Function*************************************************************

Synopsis [Writes the given clause in a file in DIMACS format.]

Description []

SideEffects []

SeeAlso []

Definition at line 50 of file satUtil.c.

51 {
52  int i;
53  for ( i = 0; i < (int)pC->size; i++ )
54  fprintf( pFile, "%s%d ", (lit_sign(pC->lits[i])? "-": ""), lit_var(pC->lits[i]) + (fIncrement>0) );
55  if ( fIncrement )
56  fprintf( pFile, "0" );
57  fprintf( pFile, "\n" );
58 }
lit lits[0]
Definition: satClause.h:56
static int lit_var(lit l)
Definition: satVec.h:145
static int lit_sign(lit l)
Definition: satVec.h:146
unsigned size
Definition: satClause.h:55
void Sat_SolverDoubleClauses ( sat_solver p,
int  iVar 
)

Function*************************************************************

Synopsis [Duplicates all clauses, complements unit clause of the given var.]

Description []

SideEffects []

SeeAlso []

Definition at line 308 of file satUtil.c.

309 {
310  assert( 0 );
311 /*
312  clause * pClause;
313  lit Lit, * pLits;
314  int RetValue, nClauses, nVarsOld, nLitsOld, nLits, c, v;
315  // get the number of variables
316  nVarsOld = p->size;
317  nLitsOld = 2 * p->size;
318  // extend the solver to depend on two sets of variables
319  sat_solver_setnvars( p, 2 * p->size );
320  // duplicate implications
321  for ( v = 0; v < nVarsOld; v++ )
322  if ( p->assigns[v] != l_Undef )
323  {
324  Lit = nLitsOld + toLitCond( v, p->assigns[v]==l_False );
325  if ( v == iVar )
326  Lit = lit_neg(Lit);
327  RetValue = sat_solver_addclause( p, &Lit, &Lit + 1 );
328  assert( RetValue );
329  }
330  // duplicate clauses
331  nClauses = vecp_size(&p->clauses);
332  for ( c = 0; c < nClauses; c++ )
333  {
334  pClause = (clause *)p->clauses.ptr[c];
335  nLits = clause_size(pClause);
336  pLits = clause_begin(pClause);
337  for ( v = 0; v < nLits; v++ )
338  pLits[v] += nLitsOld;
339  RetValue = sat_solver_addclause( p, pLits, pLits + nLits );
340  assert( RetValue );
341  for ( v = 0; v < nLits; v++ )
342  pLits[v] -= nLitsOld;
343  }
344 */
345 }
#define assert(ex)
Definition: util_old.h:213
int* Sat_SolverGetModel ( sat_solver p,
int *  pVars,
int  nVars 
)

Function*************************************************************

Synopsis [Returns a counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 266 of file satUtil.c.

267 {
268  int * pModel;
269  int i;
270  pModel = ABC_CALLOC( int, nVars+1 );
271  for ( i = 0; i < nVars; i++ )
272  pModel[i] = sat_solver_var_value(p, pVars[i]);
273  return pModel;
274 }
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
void Sat_SolverPrintStats ( FILE *  pFile,
sat_solver p 
)

Function*************************************************************

Synopsis [Writes the given clause in a file in DIMACS format.]

Description []

SideEffects []

SeeAlso []

Definition at line 188 of file satUtil.c.

189 {
190 // printf( "calls : %10d (%d)\n", (int)p->nCalls, (int)p->nCalls2 );
191  printf( "starts : %10d\n", (int)p->stats.starts );
192  printf( "conflicts : %10d\n", (int)p->stats.conflicts );
193  printf( "decisions : %10d\n", (int)p->stats.decisions );
194  printf( "propagations : %10d\n", (int)p->stats.propagations );
195 // printf( "inspects : %10d\n", (int)p->stats.inspects );
196 // printf( "inspects2 : %10d\n", (int)p->stats.inspects2 );
197 }
ABC_INT64_T decisions
Definition: satVec.h:154
stats_t stats
Definition: satSolver.h:156
ABC_INT64_T conflicts
Definition: satVec.h:154
ABC_INT64_T propagations
Definition: satVec.h:154
unsigned starts
Definition: satVec.h:153
void Sat_SolverWriteDimacs ( sat_solver p,
char *  pFileName,
lit assumpBegin,
lit assumpEnd,
int  incrementVars 
)

Function*************************************************************

Synopsis [Write the clauses in the solver into a file in DIMACS format.]

Description []

SideEffects []

SeeAlso []

Definition at line 71 of file satUtil.c.

72 {
73  Sat_Mem_t * pMem = &p->Mem;
74  FILE * pFile;
75  clause * c;
76  int i, k, nUnits;
77 
78  // count the number of unit clauses
79  nUnits = 0;
80  for ( i = 0; i < p->size; i++ )
81  if ( p->levels[i] == 0 && p->assigns[i] != 3 )
82  nUnits++;
83 
84  // start the file
85  pFile = fopen( pFileName, "wb" );
86  if ( pFile == NULL )
87  {
88  printf( "Sat_SolverWriteDimacs(): Cannot open the ouput file.\n" );
89  return;
90  }
91 // fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
92  fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0)-1+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(int)(assumpEnd-assumpBegin) );
93 
94  // write the original clauses
95  Sat_MemForEachClause( pMem, c, i, k )
96  Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
97 
98  // write the learned clauses
99 // Sat_MemForEachLearned( pMem, c, i, k )
100 // Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
101 
102  // write zero-level assertions
103  for ( i = 0; i < p->size; i++ )
104  if ( p->levels[i] == 0 && p->assigns[i] != 3 ) // varX
105  fprintf( pFile, "%s%d%s\n",
106  (p->assigns[i] == 1)? "-": "", // var0
107  i + (int)(incrementVars>0),
108  (incrementVars) ? " 0" : "");
109 
110  // write the assump
111  if (assumpBegin) {
112  for (; assumpBegin != assumpEnd; assumpBegin++) {
113  fprintf( pFile, "%s%d%s\n",
114  lit_sign(*assumpBegin)? "-": "",
115  lit_var(*assumpBegin) + (int)(incrementVars>0),
116  (incrementVars) ? " 0" : "");
117  }
118  }
119 
120  fprintf( pFile, "\n" );
121  fclose( pFile );
122 }
Sat_Mem_t Mem
Definition: satSolver.h:99
static int lit_var(lit l)
Definition: satVec.h:145
char * assigns
Definition: satSolver.h:130
static ABC_NAMESPACE_IMPL_START void Sat_SolverClauseWriteDimacs(FILE *pFile, clause *pC, int fIncrement)
DECLARATIONS ///.
Definition: satUtil.c:50
for(p=first;p->value< newval;p=p->next)
if(last==0)
Definition: sparse_int.h:34
static int size
Definition: cuddSign.c:86
static int lit_sign(lit l)
Definition: satVec.h:146
#define Sat_MemForEachClause(p, c, i, k)
Definition: satClause.h:117
static int Sat_MemEntryNum(Sat_Mem_t *p, int lrn)
Definition: satClause.h:99
int * levels
Definition: satSolver.h:129