abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions
sscSat.c File Reference
#include "sscInt.h"
#include "sat/cnf/cnf.h"
#include "aig/gia/giaAig.h"

Go to the source code of this file.

Functions

static ABC_NAMESPACE_IMPL_START int Ssc_ObjSatLit (Ssc_Man_t *p, int Lit)
 DECLARATIONS ///. More...
 
static void Gia_ManAddClausesMux (Ssc_Man_t *p, Gia_Obj_t *pNode)
 FUNCTION DEFINITIONS ///. More...
 
static void Gia_ManAddClausesSuper (Ssc_Man_t *p, Gia_Obj_t *pNode, Vec_Int_t *vSuper)
 
static void Ssc_ManCollectSuper_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vSuper)
 
static void Ssc_ManCollectSuper (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vSuper)
 
static void Ssc_ManCnfAddToFrontier (Ssc_Man_t *p, int Id, Vec_Int_t *vFront)
 
static void Ssc_ManCnfNodeAddToSolver (Ssc_Man_t *p, int NodeId)
 
void Ssc_ManStartSolver (Ssc_Man_t *p)
 
void Ssc_ManCollectSatPattern (Ssc_Man_t *p, Vec_Int_t *vPattern)
 
Vec_Int_t * Ssc_ManFindPivotSat (Ssc_Man_t *p)
 
int Ssc_ManCheckEquivalence (Ssc_Man_t *p, int iRepr, int iNode, int fCompl)
 

Function Documentation

static void Gia_ManAddClausesMux ( Ssc_Man_t *  p,
Gia_Obj_t *  pNode 
)
static

FUNCTION DEFINITIONS ///.

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

Synopsis [Addes clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 49 of file sscSat.c.

50 {
51  Gia_Obj_t * pNodeI, * pNodeT, * pNodeE;
52  int pLits[4], LitF, LitI, LitT, LitE, RetValue;
53  assert( !Gia_IsComplement( pNode ) );
54  assert( Gia_ObjIsMuxType( pNode ) );
55  // get nodes (I = if, T = then, E = else)
56  pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
57  // get the Litiable numbers
58  LitF = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNode) );
59  LitI = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNodeI) );
60  LitT = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNodeT) );
61  LitE = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNodeE) );
62 
63  // f = ITE(i, t, e)
64 
65  // i' + t' + f
66  // i' + t + f'
67  // i + e' + f
68  // i + e + f'
69 
70  // create four clauses
71  pLits[0] = Abc_LitNotCond(LitI, 1);
72  pLits[1] = Abc_LitNotCond(LitT, 1);
73  pLits[2] = Abc_LitNotCond(LitF, 0);
74  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
75  assert( RetValue );
76  pLits[0] = Abc_LitNotCond(LitI, 1);
77  pLits[1] = Abc_LitNotCond(LitT, 0);
78  pLits[2] = Abc_LitNotCond(LitF, 1);
79  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
80  assert( RetValue );
81  pLits[0] = Abc_LitNotCond(LitI, 0);
82  pLits[1] = Abc_LitNotCond(LitE, 1);
83  pLits[2] = Abc_LitNotCond(LitF, 0);
84  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
85  assert( RetValue );
86  pLits[0] = Abc_LitNotCond(LitI, 0);
87  pLits[1] = Abc_LitNotCond(LitE, 0);
88  pLits[2] = Abc_LitNotCond(LitF, 1);
89  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
90  assert( RetValue );
91 
92  // two additional clauses
93  // t' & e' -> f'
94  // t & e -> f
95 
96  // t + e + f'
97  // t' + e' + f
98 
99  if ( LitT == LitE )
100  {
101 // assert( fCompT == !fCompE );
102  return;
103  }
104 
105  pLits[0] = Abc_LitNotCond(LitT, 0);
106  pLits[1] = Abc_LitNotCond(LitE, 0);
107  pLits[2] = Abc_LitNotCond(LitF, 1);
108  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
109  assert( RetValue );
110  pLits[0] = Abc_LitNotCond(LitT, 1);
111  pLits[1] = Abc_LitNotCond(LitE, 1);
112  pLits[2] = Abc_LitNotCond(LitF, 0);
113  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
114  assert( RetValue );
115 }
Ssc_ObjSatLit
static ABC_NAMESPACE_IMPL_START int Ssc_ObjSatLit(Ssc_Man_t *p, int Lit)
DECLARATIONS ///.
Definition: sscSat.c:32
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Abc_LitNotCond
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Gia_Obj_t_
Definition: gia.h:75
Gia_ObjIsMuxType
int Gia_ObjIsMuxType(Gia_Obj_t *pNode)
Definition: giaUtil.c:885
Gia_IsComplement
static int Gia_IsComplement(Gia_Obj_t *p)
Definition: gia.h:380
Gia_ObjRecognizeMux
Gia_Obj_t * Gia_ObjRecognizeMux(Gia_Obj_t *pNode, Gia_Obj_t **ppNodeT, Gia_Obj_t **ppNodeE)
Definition: giaUtil.c:959
assert
#define assert(ex)
Definition: util_old.h:213
Gia_Obj2Lit
static int Gia_Obj2Lit(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:433
static void Gia_ManAddClausesSuper ( Ssc_Man_t *  p,
Gia_Obj_t *  pNode,
Vec_Int_t *  vSuper 
)
static

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

Synopsis [Addes clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 128 of file sscSat.c.

129 {
130  int i, RetValue, Lit, LitNode, pLits[2];
131  assert( !Gia_IsComplement(pNode) );
132  assert( Gia_ObjIsAnd( pNode ) );
133  // suppose AND-gate is A & B = C
134  // add !A => !C or A + !C
135  // add !B => !C or B + !C
136  LitNode = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNode) );
137  Vec_IntForEachEntry( vSuper, Lit, i )
138  {
139  pLits[0] = Ssc_ObjSatLit( p, Lit );
140  pLits[1] = Abc_LitNot( LitNode );
141  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
142  assert( RetValue );
143  // update literals
144  Vec_IntWriteEntry( vSuper, i, Abc_LitNot(pLits[0]) );
145  }
146  // add A & B => C or !A + !B + C
147  Vec_IntPush( vSuper, LitNode );
148  RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vSuper), Vec_IntArray(vSuper) + Vec_IntSize(vSuper) );
149  assert( RetValue );
150  (void) RetValue;
151 }
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Ssc_ObjSatLit
static ABC_NAMESPACE_IMPL_START int Ssc_ObjSatLit(Ssc_Man_t *p, int Lit)
DECLARATIONS ///.
Definition: sscSat.c:32
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Abc_LitNot
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Gia_IsComplement
static int Gia_IsComplement(Gia_Obj_t *p)
Definition: gia.h:380
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Gia_Obj2Lit
static int Gia_Obj2Lit(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:433
int Ssc_ManCheckEquivalence ( Ssc_Man_t *  p,
int  iRepr,
int  iNode,
int  fCompl 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 348 of file sscSat.c.

349 {
350  int pLitsSat[2], RetValue;
351  abctime clk;
352  assert( iRepr != iNode );
353  if ( iRepr > iNode )
354  return l_Undef;
355  assert( iRepr < iNode );
356 // if ( p->nTimeOut )
357 // sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );
358 
359  // create CNF
360  if ( iRepr )
361  Ssc_ManCnfNodeAddToSolver( p, iRepr );
362  Ssc_ManCnfNodeAddToSolver( p, iNode );
363  sat_solver_compress( p->pSat );
364 
365  // order the literals
366  pLitsSat[0] = Abc_Var2Lit( Ssc_ObjSatVar(p, iRepr), 0 );
367  pLitsSat[1] = Abc_Var2Lit( Ssc_ObjSatVar(p, iNode), fCompl ^ (int)(iRepr > 0) );
368 
369  // solve under assumptions
370  // A = 1; B = 0
371  clk = Abc_Clock();
372  RetValue = sat_solver_solve( p->pSat, pLitsSat, pLitsSat + 2, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
373  if ( RetValue == l_False )
374  {
375  pLitsSat[0] = Abc_LitNot( pLitsSat[0] ); // compl
376  pLitsSat[1] = Abc_LitNot( pLitsSat[1] ); // compl
377  RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
378  assert( RetValue );
379  p->timeSatUnsat += Abc_Clock() - clk;
380  }
381  else if ( RetValue == l_True )
382  {
383  Ssc_ManCollectSatPattern( p, p->vPattern );
384  p->timeSatSat += Abc_Clock() - clk;
385  return l_True;
386  }
387  else // if ( RetValue1 == l_Undef )
388  {
389  p->timeSatUndec += Abc_Clock() - clk;
390  return l_Undef;
391  }
392 
393  // if the old node was constant 0, we already know the answer
394  if ( iRepr == 0 )
395  return l_False;
396 
397  // solve under assumptions
398  // A = 0; B = 1
399  clk = Abc_Clock();
400  RetValue = sat_solver_solve( p->pSat, pLitsSat, pLitsSat + 2, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
401  if ( RetValue == l_False )
402  {
403  pLitsSat[0] = Abc_LitNot( pLitsSat[0] );
404  pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
405  RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
406  assert( RetValue );
407  p->timeSatUnsat += Abc_Clock() - clk;
408  }
409  else if ( RetValue == l_True )
410  {
411  Ssc_ManCollectSatPattern( p, p->vPattern );
412  p->timeSatSat += Abc_Clock() - clk;
413  return l_True;
414  }
415  else // if ( RetValue1 == l_Undef )
416  {
417  p->timeSatUndec += Abc_Clock() - clk;
418  return l_Undef;
419  }
420  return l_False;
421 }
Ssc_ObjSatVar
static int Ssc_ObjSatVar(Ssc_Man_t *p, int iObj)
MACRO DEFINITIONS ///.
Definition: sscInt.h:90
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
l_Undef
#define l_Undef
Definition: SolverTypes.h:86
sat_solver_solve
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
sat_solver_compress
static void sat_solver_compress(sat_solver *s)
Definition: satSolver.h:217
Ssc_ManCollectSatPattern
void Ssc_ManCollectSatPattern(Ssc_Man_t *p, Vec_Int_t *vPattern)
Definition: sscSat.c:315
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
l_True
#define l_True
Definition: SolverTypes.h:84
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Ssc_ManCnfNodeAddToSolver
static void Ssc_ManCnfNodeAddToSolver(Ssc_Man_t *p, int NodeId)
Definition: sscSat.c:208
Abc_LitNot
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
l_False
#define l_False
Definition: SolverTypes.h:85
assert
#define assert(ex)
Definition: util_old.h:213
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
static void Ssc_ManCnfAddToFrontier ( Ssc_Man_t *  p,
int  Id,
Vec_Int_t *  vFront 
)
static

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

Synopsis [Updates the solver clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 196 of file sscSat.c.

197 {
198  Gia_Obj_t * pObj;
199  assert( Id > 0 );
200  if ( Ssc_ObjSatVar(p, Id) )
201  return;
202  pObj = Gia_ManObj( p->pFraig, Id );
203  Ssc_ObjSetSatVar( p, Id, p->nSatVars++ );
204  sat_solver_setnvars( p->pSat, p->nSatVars + 100 );
205  if ( Gia_ObjIsAnd(pObj) )
206  Vec_IntPush( vFront, Id );
207 }
Ssc_ObjSatVar
static int Ssc_ObjSatVar(Ssc_Man_t *p, int iObj)
MACRO DEFINITIONS ///.
Definition: sscInt.h:90
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Gia_Obj_t_
Definition: gia.h:75
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Ssc_ObjSetSatVar
static void Ssc_ObjSetSatVar(Ssc_Man_t *p, int iObj, int Num)
Definition: sscInt.h:91
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
assert
#define assert(ex)
Definition: util_old.h:213
static void Ssc_ManCnfNodeAddToSolver ( Ssc_Man_t *  p,
int  NodeId 
)
static

Definition at line 208 of file sscSat.c.

209 {
210  Gia_Obj_t * pNode;
211  int i, k, Id, Lit;
212  abctime clk;
213  assert( NodeId > 0 );
214  // quit if CNF is ready
215  if ( Ssc_ObjSatVar(p, NodeId) )
216  return;
217 clk = Abc_Clock();
218  // start the frontier
219  Vec_IntClear( p->vFront );
220  Ssc_ManCnfAddToFrontier( p, NodeId, p->vFront );
221  // explore nodes in the frontier
222  Gia_ManForEachObjVec( p->vFront, p->pFraig, pNode, i )
223  {
224  // create the supergate
225  assert( Ssc_ObjSatVar(p, Gia_ObjId(p->pFraig, pNode)) );
226  if ( Gia_ObjIsMuxType(pNode) )
227  {
228  Vec_IntClear( p->vFanins );
229  Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId0p( p->pFraig, Gia_ObjFanin0(pNode) ) );
230  Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId0p( p->pFraig, Gia_ObjFanin1(pNode) ) );
231  Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId1p( p->pFraig, Gia_ObjFanin0(pNode) ) );
232  Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId1p( p->pFraig, Gia_ObjFanin1(pNode) ) );
233  Vec_IntForEachEntry( p->vFanins, Id, k )
234  Ssc_ManCnfAddToFrontier( p, Id, p->vFront );
235  Gia_ManAddClausesMux( p, pNode );
236  }
237  else
238  {
239  Ssc_ManCollectSuper( p->pFraig, pNode, p->vFanins );
240  Vec_IntForEachEntry( p->vFanins, Lit, k )
241  Ssc_ManCnfAddToFrontier( p, Abc_Lit2Var(Lit), p->vFront );
242  Gia_ManAddClausesSuper( p, pNode, p->vFanins );
243  }
244  assert( Vec_IntSize(p->vFanins) > 1 );
245  }
246 p->timeCnfGen += Abc_Clock() - clk;
247 }
Ssc_ObjSatVar
static int Ssc_ObjSatVar(Ssc_Man_t *p, int iObj)
MACRO DEFINITIONS ///.
Definition: sscInt.h:90
Gia_ManAddClausesMux
static void Gia_ManAddClausesMux(Ssc_Man_t *p, Gia_Obj_t *pNode)
FUNCTION DEFINITIONS ///.
Definition: sscSat.c:49
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Gia_ObjFaninId1p
static int Gia_ObjFaninId1p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:464
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Gia_Obj_t_
Definition: gia.h:75
Ssc_ManCollectSuper
static void Ssc_ManCollectSuper(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vSuper)
Definition: sscSat.c:176
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Gia_ManAddClausesSuper
static void Gia_ManAddClausesSuper(Ssc_Man_t *p, Gia_Obj_t *pNode, Vec_Int_t *vSuper)
Definition: sscSat.c:128
else
else
Definition: sparse_int.h:55
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
Gia_ObjIsMuxType
int Gia_ObjIsMuxType(Gia_Obj_t *pNode)
Definition: giaUtil.c:885
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Ssc_ManCnfAddToFrontier
static void Ssc_ManCnfAddToFrontier(Ssc_Man_t *p, int Id, Vec_Int_t *vFront)
Definition: sscSat.c:196
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Gia_ObjFaninId0p
static int Gia_ObjFaninId0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:463
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntPushUnique
static int Vec_IntPushUnique(Vec_Int_t *p, int Entry)
Definition: vecInt.h:832
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
void Ssc_ManCollectSatPattern ( Ssc_Man_t *  p,
Vec_Int_t *  vPattern 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 315 of file sscSat.c.

316 {
317  Gia_Obj_t * pObj;
318  int i;
319  Vec_IntClear( vPattern );
320  Gia_ManForEachCi( p->pFraig, pObj, i )
321  Vec_IntPush( vPattern, sat_solver_var_value(p->pSat, Ssc_ObjSatVar(p, Gia_ObjId(p->pFraig, pObj))) );
322 }
Ssc_ObjSatVar
static int Ssc_ObjSatVar(Ssc_Man_t *p, int iObj)
MACRO DEFINITIONS ///.
Definition: sscInt.h:90
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Gia_Obj_t_
Definition: gia.h:75
sat_solver_var_value
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
static void Ssc_ManCollectSuper ( Gia_Man_t *  p,
Gia_Obj_t *  pObj,
Vec_Int_t *  vSuper 
)
static

Definition at line 176 of file sscSat.c.

177 {
178  assert( !Gia_IsComplement(pObj) );
179  assert( Gia_ObjIsAnd(pObj) );
180  Vec_IntClear( vSuper );
181  Ssc_ManCollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper );
182  Ssc_ManCollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper );
183 }
Gia_ObjChild0
static Gia_Obj_t * Gia_ObjChild0(Gia_Obj_t *pObj)
Definition: gia.h:457
Gia_ObjChild1
static Gia_Obj_t * Gia_ObjChild1(Gia_Obj_t *pObj)
Definition: gia.h:458
Gia_IsComplement
static int Gia_IsComplement(Gia_Obj_t *p)
Definition: gia.h:380
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
Ssc_ManCollectSuper_rec
static void Ssc_ManCollectSuper_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vSuper)
Definition: sscSat.c:165
static void Ssc_ManCollectSuper_rec ( Gia_Man_t *  p,
Gia_Obj_t *  pObj,
Vec_Int_t *  vSuper 
)
static

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

Synopsis [Collects the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 165 of file sscSat.c.

166 {
167  // stop at complements, PIs, and MUXes
168  if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) || Gia_ObjIsMuxType(pObj) )
169  {
170  Vec_IntPushUnique( vSuper, Gia_Obj2Lit(p, pObj) );
171  return;
172  }
173  Ssc_ManCollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper );
174  Ssc_ManCollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper );
175 }
Gia_ObjChild0
static Gia_Obj_t * Gia_ObjChild0(Gia_Obj_t *pObj)
Definition: gia.h:457
Gia_ObjChild1
static Gia_Obj_t * Gia_ObjChild1(Gia_Obj_t *pObj)
Definition: gia.h:458
Gia_ObjIsMuxType
int Gia_ObjIsMuxType(Gia_Obj_t *pNode)
Definition: giaUtil.c:885
Gia_IsComplement
static int Gia_IsComplement(Gia_Obj_t *p)
Definition: gia.h:380
Vec_IntPushUnique
static int Vec_IntPushUnique(Vec_Int_t *p, int Entry)
Definition: vecInt.h:832
Gia_ObjIsCi
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Gia_Obj2Lit
static int Gia_Obj2Lit(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:433
Ssc_ManCollectSuper_rec
static void Ssc_ManCollectSuper_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vSuper)
Definition: sscSat.c:165
Vec_Int_t* Ssc_ManFindPivotSat ( Ssc_Man_t *  p)

Definition at line 323 of file sscSat.c.

324 {
325  Vec_Int_t * vInit;
326  int status = sat_solver_solve( p->pSat, NULL, NULL, p->pPars->nBTLimit, 0, 0, 0 );
327  if ( status == l_False )
328  return (Vec_Int_t *)(ABC_PTRINT_T)1;
329  if ( status == l_Undef )
330  return NULL;
331  assert( status == l_True );
332  vInit = Vec_IntAlloc( Gia_ManCiNum(p->pFraig) );
333  Ssc_ManCollectSatPattern( p, vInit );
334  return vInit;
335 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
l_Undef
#define l_Undef
Definition: SolverTypes.h:86
sat_solver_solve
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
Ssc_ManCollectSatPattern
void Ssc_ManCollectSatPattern(Ssc_Man_t *p, Vec_Int_t *vPattern)
Definition: sscSat.c:315
l_True
#define l_True
Definition: SolverTypes.h:84
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Gia_ManCiNum
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
l_False
#define l_False
Definition: SolverTypes.h:85
assert
#define assert(ex)
Definition: util_old.h:213
void Ssc_ManStartSolver ( Ssc_Man_t *  p)

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

Synopsis [Starts the SAT solver for constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 261 of file sscSat.c.

262 {
263  Aig_Man_t * pMan = Gia_ManToAigSimple( p->pFraig );
264  Cnf_Dat_t * pDat = Cnf_Derive( pMan, 0 );
265  Gia_Obj_t * pObj;
266  sat_solver * pSat;
267  int i, status;
268  assert( p->pSat == NULL && p->vId2Var == NULL );
269  assert( Aig_ManObjNumMax(pMan) == Gia_ManObjNum(p->pFraig) );
270  Aig_ManStop( pMan );
271  // save variable mapping
272  p->nSatVarsPivot = p->nSatVars = pDat->nVars;
273  p->vId2Var = Vec_IntStart( Gia_ManCandNum(p->pAig) + Gia_ManCandNum(p->pCare) + 10 ); // mapping of each node into its SAT var
274  p->vVar2Id = Vec_IntStart( Gia_ManCandNum(p->pAig) + Gia_ManCandNum(p->pCare) + 10 ); // mapping of each SAT var into its node
275  Ssc_ObjSetSatVar( p, 0, pDat->pVarNums[0] );
276  Gia_ManForEachCi( p->pFraig, pObj, i )
277  {
278  int iObj = Gia_ObjId( p->pFraig, pObj );
279  Ssc_ObjSetSatVar( p, iObj, pDat->pVarNums[iObj] );
280  }
281 //Cnf_DataWriteIntoFile( pDat, "dump.cnf", 1, NULL, NULL );
282  // start the SAT solver
283  pSat = sat_solver_new();
284  sat_solver_setnvars( pSat, pDat->nVars + 1000 );
285  for ( i = 0; i < pDat->nClauses; i++ )
286  {
287  if ( !sat_solver_addclause( pSat, pDat->pClauses[i], pDat->pClauses[i+1] ) )
288  {
289  Cnf_DataFree( pDat );
290  sat_solver_delete( pSat );
291  return;
292  }
293  }
294  Cnf_DataFree( pDat );
295  status = sat_solver_simplify( pSat );
296  if ( status == 0 )
297  {
298  sat_solver_delete( pSat );
299  return;
300  }
301  p->pSat = pSat;
302 }
Llb_Mgr_t_::pAig
Aig_Man_t * pAig
Definition: llb3Image.c:49
Gia_ManToAigSimple
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition: giaAig.c:367
Cnf_Derive
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition: cnfCore.c:165
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Cnf_Dat_t_::nClauses
int nClauses
Definition: cnf.h:61
Cnf_Dat_t_::nVars
int nVars
Definition: cnf.h:59
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Cnf_Dat_t_::pVarNums
int * pVarNums
Definition: cnf.h:63
Cnf_Dat_t_
Definition: cnf.h:56
Gia_Obj_t_
Definition: gia.h:75
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Cnf_Dat_t_::pClauses
int ** pClauses
Definition: cnf.h:62
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Ssc_ObjSetSatVar
static void Ssc_ObjSetSatVar(Ssc_Man_t *p, int iObj, int Num)
Definition: sscInt.h:91
Gia_ManCandNum
static int Gia_ManCandNum(Gia_Man_t *p)
Definition: gia.h:394
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
sat_solver_simplify
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
sat_solver_t
Definition: satSolver.h:91
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static ABC_NAMESPACE_IMPL_START int Ssc_ObjSatLit ( Ssc_Man_t *  p,
int  Lit 
)
inlinestatic

DECLARATIONS ///.

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

FileName [sscSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT sweeping under constraints.]

Synopsis [SAT procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 29, 2008.]

Revision [

Id:
sscSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp

]

Definition at line 32 of file sscSat.c.

32 { return Abc_Var2Lit( Ssc_ObjSatVar(p, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit) ); }
Ssc_ObjSatVar
static int Ssc_ObjSatVar(Ssc_Man_t *p, int iObj)
MACRO DEFINITIONS ///.
Definition: sscInt.h:90
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264