abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
satChecker.c File Reference
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/vec/vec.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void Sat_PrintClause (Vec_Vec_t *vClauses, int Clause)
 DECLARATIONS ///. More...
 
int Sat_ProofResolve (Vec_Vec_t *vClauses, int Result, int Clause1, int Clause2)
 
void Sat_ProofChecker (char *pFileName)
 

Function Documentation

ABC_NAMESPACE_IMPL_START void Sat_PrintClause ( Vec_Vec_t vClauses,
int  Clause 
)

DECLARATIONS ///.

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

FileName [satChecker.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT sat_solver.]

Synopsis [Resolution proof checker.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 51 of file satChecker.c.

52 {
53  Vec_Int_t * vClause;
54  int i, Entry;
55  printf( "Clause %d: {", Clause );
56  vClause = Vec_VecEntry( vClauses, Clause );
57  Vec_IntForEachEntry( vClause, Entry, i )
58  printf( " %d", Entry );
59  printf( " }\n" );
60 }
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static Vec_Ptr_t * Vec_VecEntry(Vec_Vec_t *p, int i)
Definition: vecVec.h:271
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
void Sat_ProofChecker ( char *  pFileName)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 119 of file satChecker.c.

120 {
121  FILE * pFile;
122  Vec_Vec_t * vClauses;
123  int c, i, Num, RetValue, Counter, Counter2, Clause1, Clause2;
124  int RetValue;
125  // open the file
126  pFile = fopen( pFileName, "r" );
127  if ( pFile == NULL )
128  return;
129  // count the number of clauses
130  Counter = Counter2 = 0;
131  while ( (c = fgetc(pFile)) != EOF )
132  {
133  Counter += (c == '\n');
134  Counter2 += (c == '*');
135  }
136  vClauses = Vec_VecStart( Counter+1 );
137  printf( "The proof contains %d roots and %d resolution steps.\n", Counter-Counter2, Counter2 );
138  // read the clauses
139  rewind( pFile );
140  for ( i = 1 ; ; i++ )
141  {
142  RetValue = RetValue = fscanf( pFile, "%d", &Num );
143  if ( RetValue != 1 )
144  break;
145  assert( Num == i );
146  while ( (c = fgetc( pFile )) == ' ' );
147  if ( c == '*' )
148  {
149  RetValue = fscanf( pFile, "%d %d", &Clause1, &Clause2 );
150  assert( RetValue == 2 );
151  RetValue = fscanf( pFile, "%d", &Num );
152  assert( RetValue == 1 );
153  assert( Num == 0 );
154  if ( !Sat_ProofResolve( vClauses, i, Clause1, Clause2 ) )
155  {
156  printf( "Error detected in the resolution proof.\n" );
157  Vec_VecFree( vClauses );
158  fclose( pFile );
159  return;
160  }
161  }
162  else
163  {
164  ungetc( c, pFile );
165  while ( 1 )
166  {
167  RetValue = fscanf( pFile, "%d", &Num );
168  assert( RetValue == 1 );
169  if ( Num == 0 )
170  break;
171  Vec_VecPush( vClauses, i, (void *)Num );
172  }
173  RetValue = fscanf( pFile, "%d", &Num );
174  assert( RetValue == 1 );
175  assert( Num == 0 );
176  }
177  }
178  assert( i-1 == Counter );
179  if ( Vec_IntSize( Vec_VecEntry(vClauses, Counter) ) != 0 )
180  printf( "The last clause is not empty.\n" );
181  else
182  printf( "The empty clause is derived.\n" );
183  Vec_VecFree( vClauses );
184  fclose( pFile );
185 }
static void Vec_VecPush(Vec_Vec_t *p, int Level, void *Entry)
Definition: vecVec.h:456
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
static int Counter
static Vec_Vec_t * Vec_VecStart(int nSize)
Definition: vecVec.h:168
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define assert(ex)
Definition: util_old.h:213
static Vec_Ptr_t * Vec_VecEntry(Vec_Vec_t *p, int i)
Definition: vecVec.h:271
int Sat_ProofResolve(Vec_Vec_t *vClauses, int Result, int Clause1, int Clause2)
Definition: satChecker.c:73
VOID_HACK rewind()
int Sat_ProofResolve ( Vec_Vec_t vClauses,
int  Result,
int  Clause1,
int  Clause2 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 73 of file satChecker.c.

74 {
75  Vec_Int_t * vResult = Vec_VecEntry( vClauses, Result );
76  Vec_Int_t * vClause1 = Vec_VecEntry( vClauses, Clause1 );
77  Vec_Int_t * vClause2 = Vec_VecEntry( vClauses, Clause2 );
78  int Entry1, Entry2, ResVar;
79  int i, j, Counter = 0;
80 
81  Vec_IntForEachEntry( vClause1, Entry1, i )
82  Vec_IntForEachEntry( vClause2, Entry2, j )
83  if ( Entry1 == -Entry2 )
84  {
85  ResVar = Entry1;
86  Counter++;
87  }
88  if ( Counter != 1 )
89  {
90  printf( "Error: Clause %d = Resolve(%d, %d): The number of pivot vars is %d.\n",
91  Result, Clause1, Clause2, Counter );
92  Sat_PrintClause( vClauses, Clause1 );
93  Sat_PrintClause( vClauses, Clause2 );
94  return 0;
95  }
96  // create new clause
97  assert( Vec_IntSize(vResult) == 0 );
98  Vec_IntForEachEntry( vClause1, Entry1, i )
99  if ( Entry1 != ResVar && Entry1 != -ResVar )
100  Vec_IntPushUnique( vResult, Entry1 );
101  assert( Vec_IntSize(vResult) + 1 == Vec_IntSize(vClause1) );
102  Vec_IntForEachEntry( vClause2, Entry2, i )
103  if ( Entry2 != ResVar && Entry2 != -ResVar )
104  Vec_IntPushUnique( vResult, Entry2 );
105  return 1;
106 }
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
ABC_NAMESPACE_IMPL_START void Sat_PrintClause(Vec_Vec_t *vClauses, int Clause)
DECLARATIONS ///.
Definition: satChecker.c:51
if(last==0)
Definition: sparse_int.h:34
static int Counter
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define assert(ex)
Definition: util_old.h:213
static Vec_Ptr_t * Vec_VecEntry(Vec_Vec_t *p, int i)
Definition: vecVec.h:271
static int Vec_IntPushUnique(Vec_Int_t *p, int Entry)
Definition: vecInt.h:832
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54