ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
resSat.c File Reference
#include "base/abc/abc.h"
#include "resInt.h"
#include "aig/hop/hop.h"
#include "sat/bsat/satSolver.h"
Include dependency graph for resSat.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START int Res_SatAddConst1 (sat_solver *pSat, int iVar, int fCompl)
 DECLARATIONS ///.
 
int Res_SatAddEqual (sat_solver *pSat, int iVar0, int iVar1, int fCompl)
 
int Res_SatAddAnd (sat_solver *pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1)
 
void * Res_SatProveUnsat (Abc_Ntk_t *pAig, Vec_Ptr_t *vFanins)
 FUNCTION DEFINITIONS ///.
 
void * Res_SatSimulateConstr (Abc_Ntk_t *pAig, int fOnSet)
 
int Res_SatSimulate (Res_Sim_t *p, int nPatsLimit, int fOnSet)
 

Function Documentation

◆ Res_SatAddAnd()

int Res_SatAddAnd ( sat_solver * pSat,
int iVar,
int iVar0,
int iVar1,
int fCompl0,
int fCompl1 )
extern

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

Synopsis [Adds constraints for the two-input AND-gate.]

Description []

SideEffects []

SeeAlso []

Definition at line 385 of file resSat.c.

386{
387 lit Lits[3];
388
389 Lits[0] = toLitCond( iVar, 1 );
390 Lits[1] = toLitCond( iVar0, fCompl0 );
391 if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
392 return 0;
393
394 Lits[0] = toLitCond( iVar, 1 );
395 Lits[1] = toLitCond( iVar1, fCompl1 );
396 if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
397 return 0;
398
399 Lits[0] = toLitCond( iVar, 0 );
400 Lits[1] = toLitCond( iVar0, !fCompl0 );
401 Lits[2] = toLitCond( iVar1, !fCompl1 );
402 if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
403 return 0;
404
405 return 1;
406}
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
lit
int lit
Definition satVec.h:130
Here is the caller graph for this function:

◆ Res_SatAddConst1()

int Res_SatAddConst1 ( sat_solver * pSat,
int iVar,
int fCompl )
extern

DECLARATIONS ///.

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

FileName [resSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Resynthesis package.]

Synopsis [Interface with the SAT solver.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 15, 2007.]

Revision [

Id
resSat.c,v 1.00 2007/01/15 00:00:00 alanmi Exp

]

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

Synopsis [Asserts equality of the variable to a constant.]

Description []

SideEffects []

SeeAlso []

Definition at line 338 of file resSat.c.

339{
340 lit Lit = toLitCond( iVar, fCompl );
341 if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) )
342 return 0;
343 return 1;
344}
Here is the caller graph for this function:

◆ Res_SatAddEqual()

int Res_SatAddEqual ( sat_solver * pSat,
int iVar0,
int iVar1,
int fCompl )
extern

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

Synopsis [Asserts equality of two variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 357 of file resSat.c.

358{
359 lit Lits[2];
360
361 Lits[0] = toLitCond( iVar0, 0 );
362 Lits[1] = toLitCond( iVar1, !fCompl );
363 if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
364 return 0;
365
366 Lits[0] = toLitCond( iVar0, 1 );
367 Lits[1] = toLitCond( iVar1, fCompl );
368 if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
369 return 0;
370
371 return 1;
372}
Here is the caller graph for this function:

◆ Res_SatProveUnsat()

void * Res_SatProveUnsat ( Abc_Ntk_t * pAig,
Vec_Ptr_t * vFanins )

FUNCTION DEFINITIONS ///.

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

Synopsis [Loads AIG into the SAT solver for checking resubstitution.]

Description []

SideEffects []

SeeAlso []

Definition at line 52 of file resSat.c.

53{
54 void * pCnf = NULL;
55 sat_solver * pSat;
56 Vec_Ptr_t * vNodes;
57 Abc_Obj_t * pObj;
58 int i, nNodes, status;
59
60 // make sure fanins contain POs of the AIG
61 pObj = (Abc_Obj_t *)Vec_PtrEntry( vFanins, 0 );
62 assert( pObj->pNtk == pAig && Abc_ObjIsPo(pObj) );
63
64 // collect reachable nodes
65 vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize );
66
67 // assign unique numbers to each node
68 nNodes = 0;
69 Abc_AigConst1(pAig)->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
70 Abc_NtkForEachPi( pAig, pObj, i )
71 pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
72 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
73 pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
74 Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pObj, i ) // useful POs
75 pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
76
77 // start the solver
78 pSat = sat_solver_new();
79 sat_solver_store_alloc( pSat );
80
81 // add clause for the constant node
82 Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
83 // add clauses for AND gates
84 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
85 Res_SatAddAnd( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy,
86 (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, (int)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
87 Vec_PtrFree( vNodes );
88 // add clauses for POs
89 Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pObj, i )
90 Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy,
91 (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
92 // add trivial clauses
93 pObj = (Abc_Obj_t *)Vec_PtrEntry(vFanins, 0);
94 Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // care-set
95 pObj = (Abc_Obj_t *)Vec_PtrEntry(vFanins, 1);
96 Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // on-set
97
98 // bookmark the clauses of A
99 sat_solver_store_mark_clauses_a( pSat );
100
101 // duplicate the clauses
102 pObj = (Abc_Obj_t *)Vec_PtrEntry(vFanins, 1);
103 Sat_SolverDoubleClauses( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy );
104 // add the equality constraints
105 Vec_PtrForEachEntryStart( Abc_Obj_t *, vFanins, pObj, i, 2 )
106 Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, ((int)(ABC_PTRUINT_T)pObj->pCopy) + nNodes, 0 );
107
108 // bookmark the roots
109 sat_solver_store_mark_roots( pSat );
110
111 // solve the problem
112 status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
113 if ( status == l_False )
114 {
115 pCnf = sat_solver_store_release( pSat );
116// printf( "unsat\n" );
117 }
118 else if ( status == l_True )
119 {
120// printf( "sat\n" );
121 }
122 else
123 {
124// printf( "undef\n" );
125 }
126 sat_solver_delete( pSat );
127 return pCnf;
128}
Abc_Obj_t
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
Abc_NtkForEachPi
#define Abc_NtkForEachPi(pNtk, pPi, i)
Definition abc.h:516
Abc_NtkDfsNodes
ABC_DLL Vec_Ptr_t * Abc_NtkDfsNodes(Abc_Ntk_t *pNtk, Abc_Obj_t **ppNodes, int nNodes)
Definition abcDfs.c:151
Abc_AigConst1
ABC_DLL Abc_Obj_t * Abc_AigConst1(Abc_Ntk_t *pNtk)
Definition abcAig.c:683
l_True
#define l_True
Definition bmcBmcS.c:35
l_False
#define l_False
Definition bmcBmcS.c:36
sat_solver
#define sat_solver
Definition cecSatG2.c:34
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
Res_SatAddEqual
int Res_SatAddEqual(sat_solver *pSat, int iVar0, int iVar1, int fCompl)
Definition resSat.c:357
Res_SatAddAnd
int Res_SatAddAnd(sat_solver *pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1)
Definition resSat.c:385
Res_SatAddConst1
ABC_NAMESPACE_IMPL_START int Res_SatAddConst1(sat_solver *pSat, int iVar, int fCompl)
DECLARATIONS ///.
Definition resSat.c:338
sat_solver_new
sat_solver * sat_solver_new(void)
Definition satSolver.c:1137
sat_solver_store_mark_clauses_a
void sat_solver_store_mark_clauses_a(sat_solver *s)
Definition satSolver.c:2417
sat_solver_store_alloc
void sat_solver_store_alloc(sat_solver *s)
Definition satSolver.c:2389
sat_solver_store_mark_roots
void sat_solver_store_mark_roots(sat_solver *s)
Definition satSolver.c:2412
sat_solver_store_release
void * sat_solver_store_release(sat_solver *s)
Definition satSolver.c:2422
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
Sat_SolverDoubleClauses
void Sat_SolverDoubleClauses(sat_solver *p, int iVar)
Definition satUtil.c:312
if
if(last==0)
Definition sparse_int.h:34
Abc_Obj_t_::pNtk
Abc_Ntk_t * pNtk
Definition abc.h:130
Abc_Obj_t_::pCopy
Abc_Obj_t * pCopy
Definition abc.h:148
assert
#define assert(ex)
Definition util_old.h:213
Vec_PtrForEachEntryStart
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition vecPtr.h:57
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Res_SatSimulate()

int Res_SatSimulate ( Res_Sim_t * p,
int nPatsLimit,
int fOnSet )

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

Synopsis [Loads AIG into the SAT solver for constrained simulation.]

Description [Returns 1 if the required number of patterns are found. Returns 0 if the solver ran out of time or proved a constant. In the latter, case one of the flags, fConst0 or fConst1, are set to 1.]

SideEffects []

SeeAlso []

Definition at line 212 of file resSat.c.

213{
214 Vec_Int_t * vLits;
215 Vec_Ptr_t * vPats;
216 sat_solver * pSat;
217 int RetValue = -1; // Suppress "might be used uninitialized"
218 int i, k, value, status, Lit, Var, iPat;
219 abctime clk = Abc_Clock();
220
221//printf( "Looking for %s: ", fOnSet? "onset " : "offset" );
222
223 // decide what problem should be solved
224 Lit = toLitCond( (int)(ABC_PTRUINT_T)Abc_NtkPo(p->pAig,1)->pCopy, !fOnSet );
225 if ( fOnSet )
226 {
227 iPat = p->nPats1;
228 vPats = p->vPats1;
229 }
230 else
231 {
232 iPat = p->nPats0;
233 vPats = p->vPats0;
234 }
235 assert( iPat < nPatsLimit );
236
237 // derive the SAT solver
238 pSat = (sat_solver *)Res_SatSimulateConstr( p->pAig, fOnSet );
239 pSat->fSkipSimplify = 1;
240 status = sat_solver_simplify( pSat );
241 if ( status == 0 )
242 {
243 if ( iPat == 0 )
244 {
245// if ( fOnSet )
246// p->fConst0 = 1;
247// else
248// p->fConst1 = 1;
249 RetValue = 0;
250 }
251 goto finish;
252 }
253
254 // enumerate through the SAT assignments
255 RetValue = 1;
256 vLits = Vec_IntAlloc( 32 );
257 for ( k = iPat; k < nPatsLimit; k++ )
258 {
259 // solve with the assumption
260// status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
261 status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
262 if ( status == l_False )
263 {
264//printf( "Const %d\n", !fOnSet );
265 if ( k == 0 )
266 {
267 if ( fOnSet )
268 p->fConst0 = 1;
269 else
270 p->fConst1 = 1;
271 RetValue = 0;
272 }
273 break;
274 }
275 else if ( status == l_True )
276 {
277 // save the pattern
278 Vec_IntClear( vLits );
279 for ( i = 0; i < p->nTruePis; i++ )
280 {
281 Var = (int)(ABC_PTRUINT_T)Abc_NtkPi(p->pAig,i)->pCopy;
282// value = (int)(pSat->model.ptr[Var] == l_True);
283 value = sat_solver_var_value(pSat, Var);
284 if ( value )
285 Abc_InfoSetBit( (unsigned *)Vec_PtrEntry(vPats, i), k );
286 Lit = toLitCond( Var, value );
287 Vec_IntPush( vLits, Lit );
288// printf( "%d", value );
289 }
290// printf( "\n" );
291
292 status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
293 if ( status == 0 )
294 {
295 k++;
296 RetValue = 1;
297 break;
298 }
299 }
300 else
301 {
302//printf( "Undecided\n" );
303 if ( k == 0 )
304 RetValue = 0;
305 else
306 RetValue = 1;
307 break;
308 }
309 }
310 Vec_IntFree( vLits );
311//printf( "Found %d patterns\n", k - iPat );
312
313 // set the new number of patterns
314 if ( fOnSet )
315 p->nPats1 = k;
316 else
317 p->nPats0 = k;
318
319finish:
320
321 sat_solver_delete( pSat );
322p->timeSat += Abc_Clock() - clk;
323 return RetValue;
324}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
value
ABC_NAMESPACE_IMPL_START typedef signed char value
Definition cadical_kitten.c:19
p
Cube * p
Definition exorList.c:222
Var
int Var
Definition exorList.c:228
Res_SatSimulateConstr
void * Res_SatSimulateConstr(Abc_Ntk_t *pAig, int fOnSet)
Definition resSat.c:141
sat_solver_simplify
int sat_solver_simplify(sat_solver *s)
Definition satSolver.c:1515
sat_solver_t::fSkipSimplify
int fSkipSimplify
Definition satSolver.h:182
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Res_SatSimulateConstr()

void * Res_SatSimulateConstr ( Abc_Ntk_t * pAig,
int fOnSet )

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

Synopsis [Loads AIG into the SAT solver for constrained simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 141 of file resSat.c.

142{
143 sat_solver * pSat;
144 Vec_Ptr_t * vFanins;
145 Vec_Ptr_t * vNodes;
146 Abc_Obj_t * pObj;
147 int i, nNodes;
148
149 // start the array
150 vFanins = Vec_PtrAlloc( 2 );
151 pObj = Abc_NtkPo( pAig, 0 );
152 Vec_PtrPush( vFanins, pObj );
153 pObj = Abc_NtkPo( pAig, 1 );
154 Vec_PtrPush( vFanins, pObj );
155
156 // collect reachable nodes
157 vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize );
158
159 // assign unique numbers to each node
160 nNodes = 0;
161 Abc_AigConst1(pAig)->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
162 Abc_NtkForEachPi( pAig, pObj, i )
163 pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
164 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
165 pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
166 Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pObj, i ) // useful POs
167 pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
168
169 // start the solver
170 pSat = sat_solver_new();
171
172 // add clause for the constant node
173 Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
174 // add clauses for AND gates
175 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
176 Res_SatAddAnd( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy,
177 (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, (int)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
178 Vec_PtrFree( vNodes );
179 // add clauses for the first PO
180 pObj = Abc_NtkPo( pAig, 0 );
181 Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy,
182 (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
183 // add clauses for the second PO
184 pObj = Abc_NtkPo( pAig, 1 );
185 Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy,
186 (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
187
188 // add trivial clauses
189 pObj = Abc_NtkPo( pAig, 0 );
190 Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // care-set
191
192 pObj = Abc_NtkPo( pAig, 1 );
193 Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, !fOnSet ); // on-set
194
195 Vec_PtrFree( vFanins );
196 return pSat;
197}
Here is the call graph for this function:
Here is the caller graph for this function: