summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c2
-rw-r--r--src/proof/cec/cecSat.c119
-rw-r--r--src/sat/satoko/solver.c1
-rw-r--r--src/sat/satoko/solver_api.c9
-rw-r--r--src/sat/satoko/watch_list.h2
5 files changed, 108 insertions, 25 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 52684f8c..4c37242d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -43019,7 +43019,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// Jf_ManTestCnf( pAbc->pGia );
// Gia_ManCheckFalseTest( pAbc->pGia, nFrames );
// Gia_ParTest( pAbc->pGia, nWords, nProcs );
-
+Cec2_ManSimulateTest( pAbc->pGia );
// printf( "\nThis command is currently disabled.\n\n" );
return 0;
usage:
diff --git a/src/proof/cec/cecSat.c b/src/proof/cec/cecSat.c
index 9e85e49d..aba53318 100644
--- a/src/proof/cec/cecSat.c
+++ b/src/proof/cec/cecSat.c
@@ -55,6 +55,7 @@ struct Cec2_Man_t_
Vec_Wrd_t * vSims; // CI simulation info
Vec_Int_t * vNodesNew; // nodes
Vec_Int_t * vObjSatPairs; // nodes
+ Vec_Int_t * vCexTriples; // nodes
};
static inline int Cec2_ObjSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjCopyArray(p, Gia_ObjId(p, pObj)); }
@@ -352,11 +353,9 @@ static inline word * Cec2_ObjSim( Gia_Man_t * p, int iObj )
{
return Vec_WrdEntryP( p->vSims, p->nSimWords * iObj );
}
-static inline void Cec2_ObjSimSetPiBit( Gia_Man_t * p, int iObj, int Bit )
+static inline void Cec2_ObjSimSetInputBit( Gia_Man_t * p, int iObj, int Bit )
{
word * pSim = Cec2_ObjSim( p, iObj );
- p->iPatsPi = (p->iPatsPi == 64 * p->nSimWords - 1) ? 1 : p->iPatsPi + 1;
- assert( p->iPatsPi > 0 && p->iPatsPi < 64 * p->nSimWords );
if ( Abc_InfoHasBit( (unsigned*)pSim, p->iPatsPi ) != Bit )
Abc_InfoXorBit( (unsigned*)pSim, p->iPatsPi );
}
@@ -421,7 +420,7 @@ static inline int Cec2_ObjSimEqual( Gia_Man_t * p, int iObj0, int iObj1 )
return 1;
}
}
-static inline void Cec2_ObjSimPi( Gia_Man_t * p, int iObj )
+static inline void Cec2_ObjSimCi( Gia_Man_t * p, int iObj )
{
int w;
word * pSim = Cec2_ObjSim( p, iObj );
@@ -433,7 +432,7 @@ void Cec2_ManSimulateCis( Gia_Man_t * p )
{
int i, Id;
Gia_ManForEachCiId( p, Id, i )
- Cec2_ObjSimPi( p, Id );
+ Cec2_ObjSimCi( p, Id );
p->iPatsPi = 1;
}
Abc_Cex_t * Cec2_ManDeriveCex( Gia_Man_t * p, int iOut, int iPat )
@@ -471,15 +470,28 @@ void Cec2_ManSaveCis( Gia_Man_t * p )
Gia_ManForEachCiId( p, Id, i )
Vec_WrdPush( p->vSimsPi, Cec2_ObjSim(p, Id)[w] );
}
-void Cec2_ManSimulate( Gia_Man_t * p )
+void Cec2_ManSimulate( Gia_Man_t * p, Vec_Int_t * vTriples )
{
extern void Cec2_ManSimClassRefineOne( Gia_Man_t * p, int iRepr );
- Gia_Obj_t * pObj; int i;
- Cec2_ManSaveCis( p );
+ Gia_Obj_t * pObj;
+ int i, iRepr, iObj, Entry;
+ //Cec2_ManSaveCis( p );
Gia_ManForEachAnd( p, pObj, i )
Cec2_ObjSimAnd( p, i );
if ( p->pReprs == NULL )
return;
+ if ( vTriples )
+ {
+ Vec_IntForEachEntryTriple( vTriples, iRepr, iObj, Entry, i )
+ {
+ word * pSim0 = Cec2_ObjSim( p, iRepr );
+ word * pSim1 = Cec2_ObjSim( p, iObj );
+ int iPat = Abc_Lit2Var(Entry);
+ int fPhase = Abc_LitIsCompl(Entry);
+ if ( (fPhase ^ Abc_InfoHasBit((unsigned *)pSim0, iPat)) == Abc_InfoHasBit((unsigned *)pSim1, iPat) )
+ printf( "ERROR: Pattern %d did not disprove pair %d and %d.\n", iPat, iRepr, iObj );
+ }
+ }
Gia_ManForEachClass0( p, i )
Cec2_ManSimClassRefineOne( p, i );
}
@@ -570,7 +582,8 @@ void Cec2_ManCreateClasses( Gia_Man_t * p )
int nWords = p->nSimWords;
int * pTable, nTableSize, i, Key;
// allocate representation
- assert( p->pReprs == NULL );
+ ABC_FREE( p->pReprs );
+ ABC_FREE( p->pNexts );
p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
p->pNexts = ABC_FALLOC( int, Gia_ManObjNum(p) );
// hash each node by its simulation info
@@ -618,7 +631,7 @@ Cec2_Man_t * Cec2_ManCreate( Gia_Man_t * pAig, Cec2_Par_t * pPars )
{
Cec2_Man_t * p;
Gia_Obj_t * pObj; int i;
- assert( Gia_ManRegNum(pAig) == 0 );
+ //assert( Gia_ManRegNum(pAig) == 0 );
p = ABC_CALLOC( Cec2_Man_t, 1 );
memset( p, 0, sizeof(Cec2_Man_t) );
p->pPars = pPars;
@@ -637,6 +650,7 @@ Cec2_Man_t * Cec2_ManCreate( Gia_Man_t * pAig, Cec2_Par_t * pPars )
p->vFanins = Vec_PtrAlloc( 100 );
p->vNodesNew = Vec_IntAlloc( 100 );
p->vObjSatPairs = Vec_IntAlloc( 100 );
+ p->vCexTriples = Vec_IntAlloc( 100 );
// remember pointer to the solver in the AIG manager
pAig->pData = p->pSat;
return p;
@@ -652,12 +666,53 @@ void Cec2_ManDestroy( Cec2_Man_t * p )
Vec_PtrFreeP( &p->vFanins );
Vec_IntFreeP( &p->vNodesNew );
Vec_IntFreeP( &p->vObjSatPairs );
+ Vec_IntFreeP( &p->vCexTriples );
ABC_FREE( p );
}
/**Function*************************************************************
+ Synopsis [Verify counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cec2_ManVerify_rec( Gia_Man_t * p, int iObj, satoko_t * pSat )
+{
+ int Value0, Value1;
+ Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+ if ( iObj == 0 ) return 0;
+ if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
+ return pObj->fMark1;
+ Gia_ObjSetTravIdCurrentId(p, iObj);
+ if ( Gia_ObjIsCi(pObj) )
+ return pObj->fMark1 = var_polarity(pSat, Cec2_ObjSatId(p, pObj)) == LIT_TRUE;
+ assert( Gia_ObjIsAnd(pObj) );
+ Value0 = Cec2_ManVerify_rec( p, Gia_ObjFaninId0(pObj, iObj), pSat ) ^ Gia_ObjFaninC0(pObj);
+ Value1 = Cec2_ManVerify_rec( p, Gia_ObjFaninId1(pObj, iObj), pSat ) ^ Gia_ObjFaninC1(pObj);
+ return pObj->fMark1 = Value0 & Value1;
+}
+void Cec2_ManVerify( Gia_Man_t * p, int iObj0, int iObj1, int fPhase, satoko_t * pSat )
+{
+// int val0 = var_polarity(pSat, Cec2_ObjSatId(p, Gia_ManObj(p, iObj0))) == LIT_TRUE;
+// int val1 = var_polarity(pSat, Cec2_ObjSatId(p, Gia_ManObj(p, iObj1))) == LIT_TRUE;
+ int Value0, Value1;
+ Gia_ManIncrementTravId( p );
+ Value0 = Cec2_ManVerify_rec( p, iObj0, pSat );
+ Value1 = Cec2_ManVerify_rec( p, iObj1, pSat );
+ if ( (Value0 ^ Value1) == fPhase )
+ printf( "CEX verification FAILED for obj %d and obj %d.\n", iObj0, iObj1 );
+// else
+// printf( "CEX verification succeeded for obj %d and obj %d.\n", iObj0, iObj1 );;
+}
+
+/**Function*************************************************************
+
Synopsis [Internal simulation APIs.]
Description []
@@ -707,6 +762,7 @@ int Cec2_ManSolveTwo( Cec2_Man_t * p, int iObj0, int iObj1, int fPhase )
Gia_ManIncrementTravId( p->pNew );
Cec2_ManCollect_rec( p, iObj0 );
Cec2_ManCollect_rec( p, iObj1 );
+//printf( "%d ", Vec_IntSize(p->vNodesNew) );
// solve direct
satoko_assump_push( p->pSat, Abc_Var2Lit(iVar0, 1) );
satoko_assump_push( p->pSat, Abc_Var2Lit(iVar1, fPhase) );
@@ -722,6 +778,8 @@ int Cec2_ManSolveTwo( Cec2_Man_t * p, int iObj0, int iObj1, int fPhase )
satoko_assump_pop( p->pSat );
satoko_assump_pop( p->pSat );
}
+ //if ( status == SATOKO_SAT )
+ // Cec2_ManVerify( p->pNew, iObj0, iObj1, fPhase, p->pSat );
Gia_ManForEachObjVec( p->vNodesNew, p->pNew, pObj, i )
Cec2_ObjCleanSatId( p->pNew, pObj );
return status;
@@ -735,8 +793,10 @@ int Cec2_ManSweepNode( Cec2_Man_t * p, int iObj )
status = Cec2_ManSolveTwo( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl );
if ( status == SATOKO_SAT )
{
+ p->pAig->iPatsPi = (p->pAig->iPatsPi == 64 * p->pAig->nSimWords - 1) ? 1 : p->pAig->iPatsPi + 1;
+ assert( p->pAig->iPatsPi > 0 && p->pAig->iPatsPi < 64 * p->pAig->nSimWords );
Vec_IntForEachEntryDouble( p->vObjSatPairs, IdAig, IdSat, i )
- Cec2_ObjSimSetPiBit( p->pAig, IdAig, var_value(p->pSat, IdSat) == LIT_TRUE );
+ Cec2_ObjSimSetInputBit( p->pAig, IdAig, var_polarity(p->pSat, IdSat) == LIT_TRUE );
RetValue = 0;
}
else if ( status == SATOKO_UNSAT )
@@ -751,13 +811,14 @@ int Cec2_ManSweepNode( Cec2_Man_t * p, int iObj )
assert( 0 );
}
satoko_rollback( p->pSat );
+ p->pSat->stats.n_conflicts = 0;
return RetValue;
}
int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars )
{
Cec2_Man_t * pMan;
Gia_Obj_t * pObj, * pRepr, * pObjNew;
- int i, fDisproved = 1;
+ int i, Iter, fDisproved = 1;
// check if any output trivially fails under all-0 pattern
Gia_ManSetPhase( p );
@@ -770,10 +831,11 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars )
return 0;
}
}
+
// simulate one round and create classes
Cec2_ManSimAlloc( p, pPars->nSimWords );
Cec2_ManSimulateCis( p );
- Cec2_ManSimulate( p );
+ Cec2_ManSimulate( p, NULL );
if ( pPars->fIsMiter && !Cec2_ManSimulateCos(p) ) // cex detected
return 0;
Cec2_ManCreateClasses( p );
@@ -784,7 +846,7 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars )
for ( i = 0; i < pPars->nSimRounds; i++ )
{
Cec2_ManSimulateCis( p );
- Cec2_ManSimulate( p );
+ Cec2_ManSimulate( p, NULL );
if ( pPars->fIsMiter && !Cec2_ManSimulateCos(p) ) // cex detected
return 0;
if ( pPars->fVerbose )
@@ -792,33 +854,34 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars )
}
// perform sweeping
pMan = Cec2_ManCreate( p, pPars );
- while ( fDisproved )
+ for ( Iter = 0; fDisproved; Iter++ )
{
fDisproved = 0;
Cec2_ManSimulateCis( p );
+ Vec_IntClear( pMan->vCexTriples );
Gia_ManForEachAnd( p, pObj, i )
{
- pObj->fMark1 = 0;
- if ( ~pObj->Value ) // skip swept nodes
- continue;
- assert( !Gia_ObjProved(p, i) && !Gia_ObjFailed(p, i) );
pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 || Gia_ObjFanin1(pObj)->fMark1;
if ( pObj->fMark1 ) // skip nodes in the TFO of a disproved one
continue;
+ if ( ~pObj->Value ) // skip swept nodes
+ continue;
+ if ( !~Gia_ObjFanin0(pObj)->Value || !~Gia_ObjFanin1(pObj)->Value ) // skip fanouts of non-swept nodes
+ continue;
+ assert( !Gia_ObjProved(p, i) && !Gia_ObjFailed(p, i) );
// duplicate the node
pObj->Value = Gia_ManHashAnd( pMan->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
if ( Vec_IntSize(&pMan->pNew->vCopies) == Abc_Lit2Var(pObj->Value) )
{
pObjNew = Gia_ManObj( pMan->pNew, Abc_Lit2Var(pObj->Value) );
pObjNew->fMark0 = Gia_ObjIsMuxType( pObjNew );
+ Gia_ObjSetPhase( pMan->pNew, pObjNew );
Vec_IntPush( &pMan->pNew->vCopies, -1 );
}
assert( Vec_IntSize(&pMan->pNew->vCopies) == Gia_ManObjNum(pMan->pNew) );
pRepr = Gia_ObjReprObj( p, i );
if ( pRepr == NULL || pRepr->fMark1 )
continue;
- //if ( Gia_ObjIsConst0(pRepr) )
- // continue;
if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) )
{
assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) );
@@ -827,13 +890,20 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars )
}
if ( Cec2_ManSweepNode(pMan, i) )
continue;
+ pObj->Value = ~0;
+ //Vec_IntPushThree( pMan->vCexTriples, Gia_ObjId(p, pRepr), i, Abc_Var2Lit(p->iPatsPi, pObj->fPhase ^ pRepr->fPhase) );
// mark nodes as disproved
- pRepr->fMark1 = pObj->fMark1 = 1;
fDisproved = 1;
+ if ( Iter > 5 )
+ continue;
+ if ( Gia_ObjIsAnd(pRepr) )
+ pRepr->fMark1 = 1;
+ pObj->fMark1 = 1;
}
if ( fDisproved )
{
- Cec2_ManSimulate( p );
+ //printf( "The number of pattern = %d.\n", p->iPatsPi );
+ Cec2_ManSimulate( p, pMan->vCexTriples );
if ( pPars->fIsMiter && !Cec2_ManSimulateCos(p) ) // cex detected
break;
}
@@ -841,6 +911,7 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars )
Gia_ManEquivPrintClasses( p, pPars->fVeryVerbose, 0 );
}
Cec2_ManDestroy( pMan );
+ //Gia_ManEquivPrintClasses( p, 1, 0 );
return p->pCexSeq ? 0 : 1;
}
void Cec2_ManSimulateTest( Gia_Man_t * p )
@@ -848,6 +919,8 @@ void Cec2_ManSimulateTest( Gia_Man_t * p )
abctime clk = Abc_Clock();
Cec2_Par_t Pars, * pPars = &Pars;
Cec2_SetDefaultParams( pPars );
+// Gia_ManComputeGiaEquivs( p, 100000, 0 );
+// Gia_ManEquivPrintClasses( p, 1, 0 );
Cec2_ManPerformSweeping( p, pPars );
Abc_PrintTime( 1, "SAT sweeping time", Abc_Clock() - clk );
}
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index 3e5fc8ee..3738129b 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -364,6 +364,7 @@ static inline void solver_analyze_final(solver_t *s, unsigned lit)
{
int i;
+ vec_uint_clear(s->final_conflict);
vec_uint_push_back(s->final_conflict, lit);
if (solver_dlevel(s) == 0)
return;
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index e4fd88b7..f758a1ef 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -356,10 +356,15 @@ void satoko_rollback(satoko_t *s)
vec_uint_shrink(s->originals, s->book_cl_orig);
vec_uint_shrink(s->learnts, s->book_cl_lrnt);
/* Shrink variable related vectors */
+ for (i = s->book_vars; i < 2 * vec_char_size(s->assigns); i++)
+ vec_wl_at(s->watches, i)->size = 0;
+ s->watches->size = s->book_vars;
vec_act_shrink(s->activity, s->book_vars);
vec_uint_shrink(s->levels, s->book_vars);
vec_uint_shrink(s->reasons, s->book_vars);
+ vec_uint_shrink(s->stamps, s->book_vars);
vec_char_shrink(s->assigns, s->book_vars);
+ vec_char_shrink(s->seen, s->book_vars);
vec_char_shrink(s->polarity, s->book_vars);
solver_rebuild_order(s);
/* Rewind solver and cancel level 0 assignments to the trail */
@@ -369,6 +374,10 @@ void satoko_rollback(satoko_t *s)
s->book_cl_lrnt = 0;
s->book_vars = 0;
s->book_trail = 0;
+ if (!s->book_vars) {
+ s->all_clauses->size = 0;
+ s->all_clauses->wasted = 0;
+ }
}
void satoko_mark_cone(satoko_t *s, int * pvars, int n_vars)
diff --git a/src/sat/satoko/watch_list.h b/src/sat/satoko/watch_list.h
index 49f419f2..a36ab2bb 100644
--- a/src/sat/satoko/watch_list.h
+++ b/src/sat/satoko/watch_list.h
@@ -154,7 +154,7 @@ static inline vec_wl_t *vec_wl_alloc(unsigned cap)
static inline void vec_wl_free(vec_wl_t *vec_wl)
{
unsigned i;
- for (i = 0; i < vec_wl->size; i++)
+ for (i = 0; i < vec_wl->cap; i++)
watch_list_free(vec_wl->watch_lists + i);
satoko_free(vec_wl->watch_lists);
satoko_free(vec_wl);
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-06 06:43:59 +0000