summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/bsat')
-rw-r--r--src/sat/bsat/satInterP.c68
-rw-r--r--src/sat/bsat/satSolver.c8
-rw-r--r--src/sat/bsat/satSolver.h8
-rw-r--r--src/sat/bsat/satStore.c4
-rw-r--r--src/sat/bsat/satStore.h4
5 files changed, 76 insertions, 16 deletions
diff --git a/src/sat/bsat/satInterP.c b/src/sat/bsat/satInterP.c
index 414879b6..efd03dd3 100644
--- a/src/sat/bsat/satInterP.c
+++ b/src/sat/bsat/satInterP.c
@@ -916,19 +916,20 @@ void Intp_ManUnsatCoreVerify( Sto_Man_t * pCnf, Vec_Int_t * vCore )
SeeAlso []
***********************************************************************/
-void Intp_ManUnsatCore_rec( Vec_Ptr_t * vAntClas, int iThis, Vec_Int_t * vCore, int nRoots, Vec_Int_t * vVisited )
+void Intp_ManUnsatCore_rec( Vec_Ptr_t * vAntClas, int iThis, Vec_Int_t * vCore, int nRoots, Vec_Str_t * vVisited, int fLearned )
{
// int i, iStop, iStart;
Vec_Int_t * vAnt;
int i, Entry;
// skip visited clauses
- if ( Vec_IntEntry( vVisited, iThis ) )
+ if ( Vec_StrEntry( vVisited, iThis ) )
return;
- Vec_IntWriteEntry( vVisited, iThis, 1 );
+ Vec_StrWriteEntry( vVisited, iThis, 1 );
// add a root clause to the core
if ( iThis < nRoots )
{
- Vec_IntPush( vCore, iThis );
+ if ( !fLearned )
+ Vec_IntPush( vCore, iThis );
return;
}
// iterate through the clauses
@@ -939,7 +940,10 @@ void Intp_ManUnsatCore_rec( Vec_Ptr_t * vAntClas, int iThis, Vec_Int_t * vCore,
vAnt = (Vec_Int_t *)Vec_PtrEntry( vAntClas, iThis - nRoots );
Vec_IntForEachEntry( vAnt, Entry, i )
// Intp_ManUnsatCore_rec( vAntClas, Vec_IntEntry(vAnties, i), vCore, nRoots, vVisited );
- Intp_ManUnsatCore_rec( vAntClas, Entry, vCore, nRoots, vVisited );
+ Intp_ManUnsatCore_rec( vAntClas, Entry, vCore, nRoots, vVisited, fLearned );
+ // collect learned clause
+ if ( fLearned )
+ Vec_IntPush( vCore, iThis );
}
/**Function*************************************************************
@@ -956,10 +960,10 @@ void Intp_ManUnsatCore_rec( Vec_Ptr_t * vAntClas, int iThis, Vec_Int_t * vCore,
SeeAlso []
***********************************************************************/
-void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose )
+void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fLearned, int fVerbose )
{
Vec_Int_t * vCore;
- Vec_Int_t * vVisited;
+ Vec_Str_t * vVisited;
Sto_Cls_t * pClause;
int RetValue = 1;
abctime clkTotal = Abc_Clock();
@@ -1021,7 +1025,7 @@ void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose )
if ( fVerbose )
{
- ABC_PRT( "Core", Abc_Clock() - clkTotal );
+// ABC_PRT( "Core", Abc_Clock() - clkTotal );
printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f MB\n",
p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,
1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots),
@@ -1031,9 +1035,9 @@ p->timeTotal += Abc_Clock() - clkTotal;
// derive the UNSAT core
vCore = Vec_IntAlloc( 1000 );
- vVisited = Vec_IntStart( p->pCnf->pEmpty->Id+1 );
- Intp_ManUnsatCore_rec( p->vAntClas, p->pCnf->pEmpty->Id, vCore, p->pCnf->nRoots, vVisited );
- Vec_IntFree( vVisited );
+ vVisited = Vec_StrStart( p->pCnf->pEmpty->Id+1 );
+ Intp_ManUnsatCore_rec( p->vAntClas, p->pCnf->pEmpty->Id, vCore, p->pCnf->nRoots, vVisited, fLearned );
+ Vec_StrFree( vVisited );
if ( fVerbose )
printf( "Root clauses = %d. Learned clauses = %d. UNSAT core size = %d.\n",
p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, Vec_IntSize(vCore) );
@@ -1041,6 +1045,48 @@ p->timeTotal += Abc_Clock() - clkTotal;
return vCore;
}
+/**Function*************************************************************
+
+ Synopsis [Prints learned clauses in terms of original problem varibles.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Intp_ManUnsatCorePrintForBmc( FILE * pFile, Sto_Man_t * pCnf, void * vCore0, void * vVarMap0 )
+{
+ Vec_Int_t * vCore = (Vec_Int_t *)vCore0;
+ Vec_Int_t * vVarMap = (Vec_Int_t *)vVarMap0;
+ Vec_Ptr_t * vClaMap;
+ Sto_Cls_t * pClause;
+ int v, i, iClause, fCompl, iObj, iFrame;
+ // create map of clause
+ vClaMap = Vec_PtrAlloc( pCnf->nClauses );
+ Sto_ManForEachClause( pCnf, pClause )
+ Vec_PtrPush( vClaMap, pClause );
+ // print clauses
+ fprintf( pFile, "UNSAT contains %d learned clauses:\n", Vec_IntSize(vCore) );
+ Vec_IntForEachEntry( vCore, iClause, i )
+ {
+ pClause = (Sto_Cls_t *)Vec_PtrEntry(vClaMap, iClause);
+ fprintf( pFile, "%6d : %6d : ", i, iClause - pCnf->nRoots );
+ for ( v = 0; v < (int)pClause->nLits; v++ )
+ {
+ fCompl = Abc_LitIsCompl(pClause->pLits[v]);
+ iObj = Vec_IntEntry(vVarMap, 2*Abc_Lit2Var(pClause->pLits[v]));
+ iFrame = Vec_IntEntry(vVarMap, 2*Abc_Lit2Var(pClause->pLits[v])+1);
+ fprintf( pFile, "%s%d(%d) ", fCompl ? "!":"", iObj, iFrame );
+ }
+ if ( pClause->nLits == 0 )
+ fprintf( pFile, "Empty" );
+ fprintf( pFile, "\n" );
+ }
+ Vec_PtrFree( vClaMap );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 922f1eb7..5ea0b348 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1153,6 +1153,7 @@ void sat_solver_delete(sat_solver* s)
// veci_delete(&s->model);
veci_delete(&s->act_vars);
veci_delete(&s->unit_lits);
+ veci_delete(&s->pivot_vars);
veci_delete(&s->temp_clause);
veci_delete(&s->conf_final);
@@ -1490,10 +1491,17 @@ void sat_solver_rollback( sat_solver* s )
int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
{
+ int fVerbose = 0;
lit *i,*j;
int maxvar;
lit last;
assert( begin < end );
+ if ( fVerbose )
+ {
+ for ( i = begin; i < end; i++ )
+ printf( "%s%d ", (*i)&1 ? "!":"", (*i)>>1 );
+ printf( "\n" );
+ }
veci_resize( &s->temp_clause, 0 );
for ( i = begin; i < end; i++ )
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index fb19490c..ccb7d6c4 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -170,6 +170,7 @@ struct sat_solver_t
int nCalls; // the number of local restarts
int nCalls2; // the number of local restarts
veci unit_lits; // variables whose activity has changed
+ veci pivot_vars; // pivot variables
int fSkipSimplify; // set to one to skip simplification of the clause database
int fNotUseRandom; // do not allow random decisions with a fixed probability
@@ -255,7 +256,12 @@ static inline void sat_solver_bookmark(sat_solver* s)
memcpy( s->activity2, s->activity, sizeof(unsigned) * s->iVarPivot );
}
}
-
+static inline void sat_solver_set_pivot_variables( sat_solver* s, int * pPivots, int nPivots )
+{
+ s->pivot_vars.cap = nPivots;
+ s->pivot_vars.size = nPivots;
+ s->pivot_vars.ptr = pPivots;
+}
static inline int sat_solver_count_usedvars(sat_solver* s)
{
int i, nVars = 0;
diff --git a/src/sat/bsat/satStore.c b/src/sat/bsat/satStore.c
index fab13666..ad055efe 100644
--- a/src/sat/bsat/satStore.c
+++ b/src/sat/bsat/satStore.c
@@ -320,9 +320,9 @@ void Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName )
{
for ( i = 0; i < (int)pClause->nLits; i++ )
fprintf( pFile, " %d", lit_print(pClause->pLits[i]) );
- fprintf( pFile, "\n" );
+ fprintf( pFile, " 0\n" );
}
- fprintf( pFile, " 0\n" );
+// fprintf( pFile, " 0\n" );
fclose( pFile );
}
diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h
index 960f391a..f2480a7d 100644
--- a/src/sat/bsat/satStore.h
+++ b/src/sat/bsat/satStore.h
@@ -142,8 +142,8 @@ extern void * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void
typedef struct Intp_Man_t_ Intp_Man_t;
extern Intp_Man_t * Intp_ManAlloc();
extern void Intp_ManFree( Intp_Man_t * p );
-extern void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose );
-
+extern void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fLearned, int fVerbose );
+extern void Intp_ManUnsatCorePrintForBmc( FILE * pFile, Sto_Man_t * pCnf, void * vCore, void * vVarMap );
ABC_NAMESPACE_HEADER_END
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-28 18:27:48 +0000