summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/proof/cec/cecSat.c49
-rw-r--r--src/proof/cec/cecSynth.c52
-rw-r--r--src/sat/satoko/solver.c2
3 files changed, 79 insertions, 24 deletions
diff --git a/src/proof/cec/cecSat.c b/src/proof/cec/cecSat.c
index 025668d3..fc53d503 100644
--- a/src/proof/cec/cecSat.c
+++ b/src/proof/cec/cecSat.c
@@ -61,6 +61,7 @@ struct Cec2_Man_t_
Vec_Int_t * vObjSatPairs; // nodes
Vec_Int_t * vCexTriples; // nodes
// statistics
+ int nPatterns;
int nSatSat;
int nSatUnsat;
int nSatUndec;
@@ -100,7 +101,7 @@ void Cec2_SetDefaultParams( Cec2_Par_t * p )
p->nItersMax = 10; // max number of iterations
p->nConfLimit = 1000; // conflict limit at a node
p->fIsMiter = 0; // this is a miter
- p->fUseCones = 0; // use logic cones
+ p->fUseCones = 0; // use logic cones
p->fVeryVerbose = 0; // verbose stats
p->fVerbose = 0; // verbose stats
}
@@ -487,18 +488,18 @@ 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, Vec_Int_t * vTriples, Cec2_Man_t * pMan )
+int Cec2_ManSimulate( Gia_Man_t * p, Vec_Int_t * vTriples, Cec2_Man_t * pMan )
{
extern void Cec2_ManSimClassRefineOne( Gia_Man_t * p, int iRepr );
abctime clk = Abc_Clock();
Gia_Obj_t * pObj;
- int i, iRepr, iObj, Entry;
+ int i, iRepr, iObj, Entry, Count = 0;
//Cec2_ManSaveCis( p );
Gia_ManForEachAnd( p, pObj, i )
Cec2_ObjSimAnd( p, i );
pMan->timeSim += Abc_Clock() - clk;
if ( p->pReprs == NULL )
- return;
+ return 0;
if ( vTriples )
{
Vec_IntForEachEntryTriple( vTriples, iRepr, iObj, Entry, i )
@@ -508,13 +509,17 @@ void Cec2_ManSimulate( Gia_Man_t * p, Vec_Int_t * vTriples, Cec2_Man_t * pMan )
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 );
+ {
+ //printf( "ERROR: Pattern %d did not disprove pair %d and %d.\n", iPat, iRepr, iObj );
+ Count++;
+ }
}
}
clk = Abc_Clock();
Gia_ManForEachClass0( p, i )
Cec2_ManSimClassRefineOne( p, i );
pMan->timeRefine += Abc_Clock() - clk;
+ return Count;
}
void Cec2_ManSimAlloc( Gia_Man_t * p, int nWords )
{
@@ -677,6 +682,7 @@ Cec2_Man_t * Cec2_ManCreate( Gia_Man_t * pAig, Cec2_Par_t * pPars )
p->vSatVars = Vec_IntAlloc( 100 );
p->vObjSatPairs = Vec_IntAlloc( 100 );
p->vCexTriples = Vec_IntAlloc( 100 );
+ p->pSat->opts.conf_limit = pPars->nConfLimit;
// remember pointer to the solver in the AIG manager
pAig->pData = p->pSat;
return p;
@@ -849,12 +855,13 @@ int Cec2_ManSweepNode( Cec2_Man_t * p, int iObj )
if ( status == SATOKO_SAT )
{
p->nSatSat++;
+ p->nPatterns++;
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_ObjSimSetInputBit( p->pAig, IdAig, var_polarity(p->pSat, IdSat) == LIT_TRUE );
- RetValue = 0;
p->timeSatSat += Abc_Clock() - clk;
+ RetValue = 0;
}
else if ( status == SATOKO_UNSAT )
{
@@ -862,14 +869,15 @@ int Cec2_ManSweepNode( Cec2_Man_t * p, int iObj )
pObj->Value = Abc_LitNotCond( pRepr->Value, fCompl );
Gia_ObjSetProved( p->pAig, iObj );
p->timeSatUnsat += Abc_Clock() - clk;
+ RetValue = 1;
}
else
{
p->nSatUndec++;
assert( status == SATOKO_UNDEC );
Gia_ObjSetFailed( p->pAig, iObj );
- assert( 0 );
p->timeSatUndec += Abc_Clock() - clk;
+ RetValue = 2;
}
if ( p->pPars->fUseCones )
return RetValue;
@@ -895,6 +903,7 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN
int i, Iter, fDisproved = 1;
// check if any output trivially fails under all-0 pattern
+ Gia_ManRandomW( 1 );
Gia_ManSetPhase( p );
if ( pPars->fIsMiter )
{
@@ -902,7 +911,7 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN
if ( pObj->fPhase )
{
p->pCexSeq = Cec2_ManDeriveCex( p, i, -1 );
- return 0;
+ goto finalize;
}
}
@@ -911,7 +920,7 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN
Cec2_ManSimulateCis( p );
Cec2_ManSimulate( p, NULL, pMan );
if ( pPars->fIsMiter && !Cec2_ManSimulateCos(p) ) // cex detected
- return 0;
+ goto finalize;
Cec2_ManCreateClasses( p, pMan );
Cec2_ManPrintStats( p, pPars, pMan );
@@ -921,7 +930,7 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN
Cec2_ManSimulateCis( p );
Cec2_ManSimulate( p, NULL, pMan );
if ( pPars->fIsMiter && !Cec2_ManSimulateCos(p) ) // cex detected
- return 0;
+ goto finalize;
Cec2_ManPrintStats( p, pPars, pMan );
}
// perform sweeping
@@ -929,14 +938,12 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN
for ( Iter = 0; fDisproved && Iter < pPars->nItersMax; Iter++ )
{
fDisproved = 0;
+ pMan->nPatterns = 0;
Cec2_ManSimulateCis( p );
Vec_IntClear( pMan->vCexTriples );
Gia_ManForEachAnd( p, pObj, 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
+ if ( ~pObj->Value || Gia_ObjFailed(p, i) ) // skip swept nodes and failed nodes
continue;
if ( !~Gia_ObjFanin0(pObj)->Value || !~Gia_ObjFanin1(pObj)->Value ) // skip fanouts of non-swept nodes
continue;
@@ -952,7 +959,7 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN
}
assert( Vec_IntSize(&pMan->pNew->vCopies) == Gia_ManObjNum(pMan->pNew) );
pRepr = Gia_ObjReprObj( p, i );
- if ( pRepr == NULL || pRepr->fMark1 || !~pRepr->Value )
+ if ( pRepr == NULL || !~pRepr->Value )
continue;
if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) )
{
@@ -964,18 +971,13 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN
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
fDisproved = 1;
- //if ( Iter > 5 )
- continue;
- if ( Gia_ObjIsAnd(pRepr) )
- pRepr->fMark1 = 1;
- pObj->fMark1 = 1;
}
if ( fDisproved )
{
- //printf( "The number of pattern = %d.\n", p->iPatsPi );
- Cec2_ManSimulate( p, pMan->vCexTriples, pMan );
+ int Fails = Cec2_ManSimulate( p, pMan->vCexTriples, pMan );
+ if ( Fails && pPars->fVerbose )
+ printf( "Failed to resimulate %d times with pattern = %d (total = %d).\n", Fails, pMan->nPatterns, pPars->nSimWords * 64 );
if ( pPars->fIsMiter && !Cec2_ManSimulateCos(p) ) // cex detected
break;
}
@@ -993,6 +995,7 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN
(*ppNew)->pName = Abc_UtilStrsav( p->pName );
(*ppNew)->pSpec = Abc_UtilStrsav( p->pSpec );
}
+finalize:
Cec2_ManDestroy( pMan );
//Gia_ManEquivPrintClasses( p, 1, 0 );
return p->pCexSeq ? 0 : 1;
diff --git a/src/proof/cec/cecSynth.c b/src/proof/cec/cecSynth.c
index c00723bc..6e5fd221 100644
--- a/src/proof/cec/cecSynth.c
+++ b/src/proof/cec/cecSynth.c
@@ -372,6 +372,58 @@ int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars )
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Gia_ManTestOnePair_rec( sat_solver * pSat, Gia_Man_t * p, int iObj, Vec_Int_t * vSatVar )
+{
+ Gia_Obj_t * pObj;
+ int iVar, iVar0, iVar1;
+ if ( Vec_IntEntry(vSatVar, iObj) >= 0 )
+ return Vec_IntEntry(vSatVar, iObj);
+ iVar = sat_solver_addvar(pSat);
+ Vec_IntWriteEntry( vSatVar, iObj, iVar );
+ pObj = Gia_ManObj( p, iObj );
+ if ( Gia_ObjIsAnd(pObj) )
+ {
+ iVar0 = Gia_ManTestOnePair_rec( pSat, p, Gia_ObjFaninId0(pObj, iObj), vSatVar );
+ iVar1 = Gia_ManTestOnePair_rec( pSat, p, Gia_ObjFaninId1(pObj, iObj), vSatVar );
+ sat_solver_add_and( pSat, iVar, iVar0, iVar1, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
+ }
+ return iVar;
+}
+int Gia_ManTestOnePair( Gia_Man_t * p, int iObj1, int iObj2, int fPhase )
+{
+ int Lits[2] = {1}, status;
+ sat_solver * pSat = sat_solver_new();
+ Vec_Int_t * vSatVar = Vec_IntStartFull( Gia_ManObjNum(p) );
+ Vec_IntWriteEntry( vSatVar, 0, sat_solver_addvar(pSat) );
+ sat_solver_addclause( pSat, Lits, Lits + 1 );
+ Gia_ManTestOnePair_rec( pSat, p, iObj1, vSatVar );
+ Gia_ManTestOnePair_rec( pSat, p, iObj2, vSatVar );
+ Lits[0] = Abc_Var2Lit( Vec_IntEntry(vSatVar, iObj1), 1 );
+ Lits[1] = Abc_Var2Lit( Vec_IntEntry(vSatVar, iObj2), fPhase );
+ status = sat_solver_solve( pSat, Lits, Lits + 2, 0, 0, 0, 0 );
+ if ( status == l_False )
+ {
+ Lits[0] = Abc_LitNot( Lits[0] );
+ Lits[1] = Abc_LitNot( Lits[1] );
+ status = sat_solver_solve( pSat, Lits, Lits + 2, 0, 0, 0, 0 );
+ }
+ Vec_IntFree( vSatVar );
+ sat_solver_delete( pSat );
+ return status;
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index 368ece2f..a72e39f7 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -639,7 +639,7 @@ char solver_search(solver_t *s)
/* No conflict */
unsigned next_lit;
- if (solver_rst(s)) {
+ if (solver_rst(s) || solver_check_limits(s) == 0) {
b_queue_clean(s->bq_lbd);
solver_cancel_until(s, 0);
return SATOKO_UNDEC;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 20:21:31 +0000