Skip to content

A
abc
Commit 429f52ce by Alan Mishchenko
Options

Experiments with SAT sweeping.

parent bc010af4
Showing with 74 additions and 28 deletions
abclib.dsp
......@@ -5027,6 +5027,10 @@ SOURCE=.\src\proof\cec\cecPat.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\cec\cecSat.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\cec\cecSeq.c
# End Source File
# Begin Source File
......
src/aig/gia/gia.h
......@@ -194,6 +194,7 @@ struct Gia_Man_t_
int MappedDelay; // delay after mapping
// bit-parallel simulation
int iPatsPi;
int nSimWords;
Vec_Wrd_t * vSims;
Vec_Wrd_t * vSimsPi;
Vec_Int_t * vClassOld;
......@@ -982,24 +983,26 @@ static inline void Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num ) { p
static inline int Gia_ObjIsConst( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == 0; }
static inline int Gia_ObjIsHead( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) > 0; }
static inline int Gia_ObjIsNone( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) == 0; }
static inline int Gia_ObjIsTail( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) == 0; }
static inline int Gia_ObjIsNone( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) <= 0; }
static inline int Gia_ObjIsTail( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) <= 0; }
static inline int Gia_ObjIsClass( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) || Gia_ObjNext(p, Id) > 0; }
static inline int Gia_ObjHasSameRepr( Gia_Man_t * p, int i, int k ) { assert( k ); return i? (Gia_ObjRepr(p, i) == Gia_ObjRepr(p, k) && Gia_ObjRepr(p, i) != GIA_VOID) : Gia_ObjRepr(p, k) == 0; }
static inline int Gia_ObjIsFailedPair( Gia_Man_t * p, int i, int k ) { assert( k ); return i? (Gia_ObjFailed(p, i) || Gia_ObjFailed(p, k)) : Gia_ObjFailed(p, k); }
static inline int Gia_ClassIsPair( Gia_Man_t * p, int i ) { assert( Gia_ObjIsHead(p, i) ); assert( Gia_ObjNext(p, i) ); return Gia_ObjNext(p, Gia_ObjNext(p, i)) == 0; }
static inline int Gia_ClassIsPair( Gia_Man_t * p, int i ) { assert( Gia_ObjIsHead(p, i) ); assert( Gia_ObjNext(p, i) ); return Gia_ObjNext(p, Gia_ObjNext(p, i)) <= 0; }
static inline void Gia_ClassUndoPair( Gia_Man_t * p, int i ) { assert( Gia_ClassIsPair(p,i) ); Gia_ObjSetRepr(p, Gia_ObjNext(p, i), GIA_VOID); Gia_ObjSetNext(p, i, 0); }
#define Gia_ManForEachConst( p, i ) \
for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsConst(p, i) ) {} else
#define Gia_ManForEachClass( p, i ) \
for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsHead(p, i) ) {} else
#define Gia_ManForEachClass0( p, i ) \
for ( i = 0; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsHead(p, i) ) {} else
#define Gia_ManForEachClassReverse( p, i ) \
for ( i = Gia_ManObjNum(p) - 1; i > 0; i-- ) if ( !Gia_ObjIsHead(p, i) ) {} else
#define Gia_ClassForEachObj( p, i, iObj ) \
for ( assert(Gia_ObjIsHead(p, i)), iObj = i; iObj; iObj = Gia_ObjNext(p, iObj) )
for ( assert(Gia_ObjIsHead(p, i)), iObj = i; iObj > 0; iObj = Gia_ObjNext(p, iObj) )
#define Gia_ClassForEachObj1( p, i, iObj ) \
for ( assert(Gia_ObjIsHead(p, i)), iObj = Gia_ObjNext(p, i); iObj; iObj = Gia_ObjNext(p, iObj) )
for ( assert(Gia_ObjIsHead(p, i)), iObj = Gia_ObjNext(p, i); iObj > 0; iObj = Gia_ObjNext(p, iObj) )
static inline int Gia_ObjFoffsetId( Gia_Man_t * p, int Id ) { return Vec_IntEntry( p->vFanout, Id ); }
......@@ -1585,6 +1588,7 @@ extern void Gia_ManSwapPos( Gia_Man_t * p, int i );
extern Vec_Int_t * Gia_ManSaveValue( Gia_Man_t * p );
extern void Gia_ManLoadValue( Gia_Man_t * p, Vec_Int_t * vValues );
extern Vec_Int_t * Gia_ManFirstFanouts( Gia_Man_t * p );
extern void Gia_ManDetectMuxes( Gia_Man_t * p );
/*=== giaCTas.c ===========================================================*/
typedef struct Tas_Man_t_ Tas_Man_t;
......
src/aig/gia/giaEquiv.c
......@@ -485,7 +485,7 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
if ( fVerbose )
{
// int Ent;
Abc_Print( 1, "Const0 = " );
Abc_Print( 1, "Const0 (%d) = ", Counter0 );
Gia_ManForEachConst( p, i )
Abc_Print( 1, "%d ", i );
Abc_Print( 1, "\n" );
......
src/aig/gia/giaUtil.c
......@@ -2050,6 +2050,25 @@ void Gia_AigerWriteLut( Gia_Man_t * p, char * pFileName )
Vec_WrdFree( vTruths );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManDetectMuxes( Gia_Man_t * p )
{
Gia_Obj_t * pObj, * pNodeT, * pNodeE; int i;
Gia_ManForEachObj( p, pObj, i );
if ( Gia_ObjIsAnd(pObj) && Gia_ObjRecognizeMux(pObj, &pNodeT, &pNodeE) )
pObj->fMark0 = 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/base/wlc/wlcSim.c
......@@ -43,13 +43,13 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
static inline word * Wlc_ObjSim( Gia_Man_t * p, int iObj )
{
return Vec_WrdEntryP( p->vSims, p->iPatsPi * iObj );
return Vec_WrdEntryP( p->vSims, p->nSimWords * iObj );
}
static inline void Wlc_ObjSimPi( Gia_Man_t * p, int iObj )
{
int w;
word * pSim = Wlc_ObjSim( p, iObj );
for ( w = 0; w < p->iPatsPi; w++ )
for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = Gia_ManRandomW( 0 );
}
static inline void Wlc_ObjSimRo( Gia_Man_t * p, int iObj )
......@@ -57,7 +57,7 @@ static inline void Wlc_ObjSimRo( Gia_Man_t * p, int iObj )
int w;
word * pSimRo = Wlc_ObjSim( p, iObj );
word * pSimRi = Wlc_ObjSim( p, Gia_ObjRoToRiId(p, iObj) );
for ( w = 0; w < p->iPatsPi; w++ )
for ( w = 0; w < p->nSimWords; w++ )
pSimRo[w] = pSimRi[w];
}
static inline void Wlc_ObjSimCo( Gia_Man_t * p, int iObj )
......@@ -67,10 +67,10 @@ static inline void Wlc_ObjSimCo( Gia_Man_t * p, int iObj )
word * pSimCo = Wlc_ObjSim( p, iObj );
word * pSimDri = Wlc_ObjSim( p, Gia_ObjFaninId0(pObj, iObj) );
if ( Gia_ObjFaninC0(pObj) )
for ( w = 0; w < p->iPatsPi; w++ )
for ( w = 0; w < p->nSimWords; w++ )
pSimCo[w] = ~pSimDri[w];
else
for ( w = 0; w < p->iPatsPi; w++ )
for ( w = 0; w < p->nSimWords; w++ )
pSimCo[w] = pSimDri[w];
}
static inline void Wlc_ObjSimAnd( Gia_Man_t * p, int iObj )
......@@ -81,16 +81,16 @@ static inline void Wlc_ObjSimAnd( Gia_Man_t * p, int iObj )
word * pSim0 = Wlc_ObjSim( p, Gia_ObjFaninId0(pObj, iObj) );
word * pSim1 = Wlc_ObjSim( p, Gia_ObjFaninId1(pObj, iObj) );
if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
for ( w = 0; w < p->iPatsPi; w++ )
for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = ~pSim0[w] & ~pSim1[w];
else if ( Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) )
for ( w = 0; w < p->iPatsPi; w++ )
for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = ~pSim0[w] & pSim1[w];
else if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
for ( w = 0; w < p->iPatsPi; w++ )
for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = pSim0[w] & ~pSim1[w];
else
for ( w = 0; w < p->iPatsPi; w++ )
for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = pSim0[w] & pSim1[w];
}
......@@ -135,7 +135,7 @@ Vec_Ptr_t * Wlc_NtkSimulate( Wlc_Ntk_t * p, Vec_Int_t * vNodes, int nWords, int
// allocate simulation info for one timeframe
Vec_WrdFreeP( &pGia->vSims );
pGia->vSims = Vec_WrdStart( Gia_ManObjNum(pGia) * nWords );
pGia->iPatsPi = nWords;
pGia->nSimWords = nWords;
// allocate resulting simulation info
vRes = Vec_PtrAlloc( Vec_IntSize(vNodes) );
Wlc_NtkForEachObjVec( vNodes, p, pWlcObj, i )
......@@ -188,7 +188,7 @@ Vec_Ptr_t * Wlc_NtkSimulate( Wlc_Ntk_t * p, Vec_Int_t * vNodes, int nWords, int
printf( "Replaced %d dangling internal bits with constant 0.\n", Counter );
}
Vec_WrdFreeP( &pGia->vSims );
pGia->iPatsPi = 0;
pGia->nSimWords = 0;
Gia_ManStop( pGia );
return vRes;
}
......
src/misc/util/utilTruth.h
......@@ -1631,6 +1631,14 @@ static inline int Abc_TtFindFirstBit( word * pIn, int nVars )
return 64*w + Abc_Tt6FirstBit(pIn[w]);
return -1;
}
static inline int Abc_TtFindFirstBit2( word * pIn, int nWords )
{
int w;
for ( w = 0; w < nWords; w++ )
if ( pIn[w] )
return 64*w + Abc_Tt6FirstBit(pIn[w]);
return -1;
}
static inline int Abc_TtFindFirstDiffBit( word * pIn1, word * pIn2, int nVars )
{
int w, nWords = Abc_TtWordNum(nVars);
......@@ -1639,6 +1647,14 @@ static inline int Abc_TtFindFirstDiffBit( word * pIn1, word * pIn2, int nVars )
return 64*w + Abc_Tt6FirstBit(pIn1[w] ^ pIn2[w]);
return -1;
}
static inline int Abc_TtFindFirstDiffBit2( word * pIn1, word * pIn2, int nWords )
{
int w;
for ( w = 0; w < nWords; w++ )
if ( pIn1[w] ^ pIn2[w] )
return 64*w + Abc_Tt6FirstBit(pIn1[w] ^ pIn2[w]);
return -1;
}
static inline int Abc_TtFindFirstZero( word * pIn, int nVars )
{
int w, nWords = Abc_TtWordNum(nVars);
......
src/proof/cec/module.make
......@@ -6,6 +6,7 @@ SRC += src/proof/cec/cecCec.c \
src/proof/cec/cecIso.c \
src/proof/cec/cecMan.c \
src/proof/cec/cecPat.c \
src/proof/cec/cecSat.c \
src/proof/cec/cecSeq.c \
src/proof/cec/cecSolve.c \
src/proof/cec/cecSplit.c \
......
src/sat/bmc/bmcGen.c
......@@ -46,13 +46,13 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
static inline word * Gia_ManMoObj( Gia_Man_t * p, int iObj )
{
return Vec_WrdEntryP( p->vSims, iObj * p->iPatsPi );
return Vec_WrdEntryP( p->vSims, iObj * p->nSimWords );
}
static inline void Gia_ManMoSetCi( Gia_Man_t * p, int iObj )
{
int w;
word * pSims = Gia_ManMoObj( p, iObj );
for ( w = 0; w < p->iPatsPi; w++ )
for ( w = 0; w < p->nSimWords; w++ )
pSims[w] = Gia_ManRandomW( 0 );
}
static inline void Gia_ManMoSimAnd( Gia_Man_t * p, int iObj )
......@@ -65,19 +65,19 @@ static inline void Gia_ManMoSimAnd( Gia_Man_t * p, int iObj )
if ( Gia_ObjFaninC0(pObj) )
{
if ( Gia_ObjFaninC1(pObj) )
for ( w = 0; w < p->iPatsPi; w++ )
for ( w = 0; w < p->nSimWords; w++ )
pSims[w] = ~(pSims0[w] | pSims1[w]);
else
for ( w = 0; w < p->iPatsPi; w++ )
for ( w = 0; w < p->nSimWords; w++ )
pSims[w] = ~pSims0[w] & pSims1[w];
}
else
{
if ( Gia_ObjFaninC1(pObj) )
for ( w = 0; w < p->iPatsPi; w++ )
for ( w = 0; w < p->nSimWords; w++ )
pSims[w] = pSims0[w] & ~pSims1[w];
else
for ( w = 0; w < p->iPatsPi; w++ )
for ( w = 0; w < p->nSimWords; w++ )
pSims[w] = pSims0[w] & pSims1[w];
}
}
......@@ -89,12 +89,12 @@ static inline void Gia_ManMoSetCo( Gia_Man_t * p, int iObj )
word * pSims0 = Gia_ManMoObj( p, Gia_ObjFaninId0(pObj, iObj) );
if ( Gia_ObjFaninC0(pObj) )
{
for ( w = 0; w < p->iPatsPi; w++ )
for ( w = 0; w < p->nSimWords; w++ )
pSims[w] = ~pSims0[w];
}
else
{
for ( w = 0; w < p->iPatsPi; w++ )
for ( w = 0; w < p->nSimWords; w++ )
pSims[w] = pSims0[w];
}
}
......@@ -102,7 +102,7 @@ void Gia_ManMoFindSimulate( Gia_Man_t * p, int nWords )
{
int i, iObj;
Gia_ManRandomW( 1 );
p->iPatsPi = nWords;
p->nSimWords = nWords;
if ( p->vSims )
Vec_WrdFill( p->vSims, nWords * Gia_ManObjNum(p), 0 );
else
......
src/sat/satoko/satoko.h
......@@ -83,7 +83,7 @@ extern void satoko_destroy(satoko_t *);
extern void satoko_default_opts(satoko_opts_t *);
extern void satoko_configure(satoko_t *, satoko_opts_t *);
extern int satoko_parse_dimacs(char *, satoko_t **);
extern void satoko_add_variable(satoko_t *, char);
extern int satoko_add_variable(satoko_t *, char);
extern int satoko_add_clause(satoko_t *, unsigned *, unsigned);
extern void satoko_assump_push(satoko_t *s, unsigned);
extern void satoko_assump_pop(satoko_t *s);
......
src/sat/satoko/solver_api.c
......@@ -216,7 +216,7 @@ int satoko_simplify(solver_t * s)
return SATOKO_OK;
}
void satoko_add_variable(solver_t *s, char sign)
int satoko_add_variable(solver_t *s, char sign)
{
unsigned var = vec_act_size(s->activity);
vec_wl_push(s->watches);
......@@ -231,6 +231,7 @@ void satoko_add_variable(solver_t *s, char sign)
heap_insert(s->var_order, var);
if (s->marks)
vec_char_push_back(s->marks, 0);
return var;
}
int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size)
......@@ -351,6 +352,7 @@ void satoko_rollback(satoko_t *s)
clause_unwatch(s, cdb_cref(s->all_clauses, (unsigned *)cl_to_remove[i]));
cl_to_remove[i]->f_mark = 1;
}
satoko_free(cl_to_remove);
vec_uint_shrink(s->originals, s->book_cl_orig);
vec_uint_shrink(s->learnts, s->book_cl_lrnt);
/* Shrink variable related vectors */
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment