summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-02-16 14:23:52 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2012-02-16 14:23:52 -0800
commitf1dba69c576a9b995f87673ce6d6ccbaddf647b6 (patch)
tree6b6e602c726082ee95dcb71a1d8e6b7359dc966c /src/sat
parentce945006e13d380d85e4ceba77b780f1690af160 (diff)
downloadabc-f1dba69c576a9b995f87673ce6d6ccbaddf647b6.tar.gz
abc-f1dba69c576a9b995f87673ce6d6ccbaddf647b6.tar.bz2
abc-f1dba69c576a9b995f87673ce6d6ccbaddf647b6.zip
Improved memory management of proof-logging and propagated changes.
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bsat/satProof.c236
-rw-r--r--src/sat/bsat/satSolver.c53
-rw-r--r--src/sat/bsat/satSolver.h4
-rw-r--r--src/sat/bsat/satSolver2.c136
-rw-r--r--src/sat/bsat/satSolver2.h28
-rw-r--r--src/sat/bsat/satSolver_old.c1766
-rw-r--r--src/sat/bsat/satSolver_old.h210
-rw-r--r--src/sat/bsat/satTruth.c34
-rw-r--r--src/sat/bsat/satTruth.h2
-rw-r--r--src/sat/bsat/vecRec.h396
-rw-r--r--src/sat/bsat/vecSet.h247
11 files changed, 448 insertions, 2664 deletions
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index 1eaf4407..dcb02bcd 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -22,18 +22,16 @@
#include "src/misc/vec/vec.h"
#include "src/aig/aig/aig.h"
#include "satTruth.h"
-#include "vecRec.h"
+#include "vecSet.h"
ABC_NAMESPACE_IMPL_START
/*
- Proof is represented as a vector of integers.
- The first entry is -1.
- A resolution record is represented by a handle (an offset in this array).
+ Proof is represented as a vector of records.
+ A resolution record is represented by a handle (an offset in this vector).
A resolution record entry is <size><label><ant1><ant2>...<antN>
- Label is initialized to 0.
- Root clauses are given by their handles.
+ Label is initialized to 0. Root clauses are given by their handles.
They are marked by bitshifting by 2 bits up and setting the LSB to 1
*/
@@ -58,26 +56,25 @@ struct satset_t
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static inline satset* Proof_NodeRead (Vec_Int_t* p, cla h) { return satset_read( (veci*)p, h ); }
-//static inline cla Proof_NodeHandle (Vec_Int_t* p, satset* c) { return satset_handle( (veci*)p, c ); }
-//static inline int Proof_NodeCheck (Vec_Int_t* p, satset* c) { return satset_check( (veci*)p, c ); }
-static inline int Proof_NodeSize (int nEnts) { return sizeof(satset)/4 + nEnts; }
-
-static inline satset* Proof_ResolveRead (Vec_Rec_t* p, cla h) { return (satset*)Vec_RecEntryP(p, h); }
+static inline satset* Proof_ClauseRead ( Vec_Int_t* p, cla h ) { assert( h > 0 ); return satset_read( (veci *)p, h ); }
+static inline satset* Proof_NodeRead ( Vec_Set_t* p, cla h ) { assert( h > 0 ); return (satset*)Vec_SetEntry( p, h ); }
+static inline int Proof_NodeWordNum ( int nEnts ) { assert( nEnts > 0 ); return 1 + ((nEnts + 1) >> 1); }
// iterating through nodes in the proof
-#define Proof_ForeachNode( p, pNode, h ) \
- for ( h = 1; (h < Vec_IntSize(p)) && ((pNode) = Proof_NodeRead(p, h)); h += Proof_NodeSize(pNode->nEnts) )
+#define Proof_ForeachClauseVec( pVec, p, pNode, i ) \
+ for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_ClauseRead(p, Vec_IntEntry(pVec,i))); i++ )
#define Proof_ForeachNodeVec( pVec, p, pNode, i ) \
for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_NodeRead(p, Vec_IntEntry(pVec,i))); i++ )
+#define Proof_ForeachNodeVec1( pVec, p, pNode, i ) \
+ for ( i = 1; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_NodeRead(p, Vec_IntEntry(pVec,i))); i++ )
// iterating through fanins of a proof node
-#define Proof_NodeForeachFanin( p, pNode, pFanin, i ) \
- for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = (pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(p, pNode->pEnts[i] >> 2)), 1); i++ )
+#define Proof_NodeForeachFanin( pProof, pNode, pFanin, i ) \
+ for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = (pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(pProof, pNode->pEnts[i] >> 2)), 1); i++ )
#define Proof_NodeForeachLeaf( pClauses, pNode, pLeaf, i ) \
- for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pClauses, pNode->pEnts[i] >> 2) : NULL), 1); i++ )
-#define Proof_NodeForeachFaninLeaf( p, pClauses, pNode, pFanin, i ) \
- for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pClauses, pNode->pEnts[i] >> 2) : Proof_NodeRead(p, pNode->pEnts[i] >> 2)); i++ )
+ for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_ClauseRead(pClauses, pNode->pEnts[i] >> 2) : NULL), 1); i++ )
+#define Proof_NodeForeachFaninLeaf( pProof, pClauses, pNode, pFanin, i ) \
+ for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_ClauseRead(pClauses, pNode->pEnts[i] >> 2) : Proof_NodeRead(pProof, pNode->pEnts[i] >> 2)); i++ )
////////////////////////////////////////////////////////////////////////
@@ -86,48 +83,6 @@ static inline satset* Proof_ResolveRead (Vec_Rec_t* p, cla h) { return (sats
/**Function*************************************************************
- Synopsis [Returns the number of proof nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Proof_CountAll( Vec_Int_t * p )
-{
- satset * pNode;
- int hNode, Counter = 0;
- Proof_ForeachNode( p, pNode, hNode )
- Counter++;
- return Counter;
-}
-
-/**Function*************************************************************
-
- Synopsis [Collects all resolution nodes belonging to the proof.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Int_t * Proof_CollectAll( Vec_Int_t * p )
-{
- Vec_Int_t * vUsed;
- satset * pNode;
- int hNode;
- vUsed = Vec_IntAlloc( 1000 );
- Proof_ForeachNode( p, pNode, hNode )
- Vec_IntPush( vUsed, hNode );
- return vUsed;
-}
-
-/**Function*************************************************************
-
Synopsis [Cleans collected resultion nodes belonging to the proof.]
Description []
@@ -137,7 +92,7 @@ Vec_Int_t * Proof_CollectAll( Vec_Int_t * p )
SeeAlso []
***********************************************************************/
-void Proof_CleanCollected( Vec_Int_t * vProof, Vec_Int_t * vUsed )
+void Proof_CleanCollected( Vec_Set_t * vProof, Vec_Int_t * vUsed )
{
satset * pNode;
int hNode;
@@ -147,7 +102,7 @@ void Proof_CleanCollected( Vec_Int_t * vProof, Vec_Int_t * vUsed )
/**Function*************************************************************
- Synopsis [Recursively visits useful proof nodes.]
+ Synopsis [Marks useful nodes of the proof.]
Description []
@@ -156,7 +111,7 @@ void Proof_CleanCollected( Vec_Int_t * vProof, Vec_Int_t * vUsed )
SeeAlso []
***********************************************************************/
-void Proof_CollectUsed_iter( Vec_Int_t * vProof, int hNode, Vec_Int_t * vUsed, Vec_Int_t * vStack )
+void Proof_CollectUsed_iter( Vec_Set_t * vProof, int hNode, Vec_Int_t * vUsed, Vec_Int_t * vStack )
{
satset * pNext, * pNode = Proof_NodeRead( vProof, hNode );
int i;
@@ -198,46 +153,33 @@ void Proof_CollectUsed_iter( Vec_Int_t * vProof, int hNode, Vec_Int_t * vUsed, V
SeeAlso []
***********************************************************************/
-Vec_Int_t * Proof_CollectUsedIter( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hRoot )
+Vec_Int_t * Proof_CollectUsedIter( Vec_Set_t * vProof, Vec_Int_t * vRoots, int fSort )
{
+ int fVerify = 0;
Vec_Int_t * vUsed, * vStack;
int clk = clock();
int i, Entry, iPrev = 0;
- assert( (hRoot > 0) ^ (vRoots != NULL) );
vUsed = Vec_IntAlloc( 1000 );
vStack = Vec_IntAlloc( 1000 );
- if ( hRoot )
- Proof_CollectUsed_iter( vProof, hRoot, vUsed, vStack );
- else
- {
- Vec_IntForEachEntry( vRoots, Entry, i )
+ Vec_IntForEachEntry( vRoots, Entry, i )
+ if ( Entry >= 0 )
Proof_CollectUsed_iter( vProof, Entry, vUsed, vStack );
- }
Vec_IntFree( vStack );
// Abc_PrintTime( 1, "Iterative clause collection time", clock() - clk );
-
-/*
- // verify topological order
- iPrev = 0;
- Vec_IntForEachEntry( vUsed, Entry, i )
- {
- printf( "%d ", Entry - iPrev );
- iPrev = Entry;
- }
-*/
clk = clock();
-// Vec_IntSort( vUsed, 0 );
Abc_Sort( Vec_IntArray(vUsed), Vec_IntSize(vUsed) );
// Abc_PrintTime( 1, "Postprocessing with sorting time", clock() - clk );
-
// verify topological order
- iPrev = 0;
- Vec_IntForEachEntry( vUsed, Entry, i )
+ if ( fVerify )
{
- if ( iPrev >= Entry )
- printf( "Out of topological order!!!\n" );
- assert( iPrev < Entry );
- iPrev = Entry;
+ iPrev = 0;
+ Vec_IntForEachEntry( vUsed, Entry, i )
+ {
+ if ( iPrev >= Entry )
+ printf( "Out of topological order!!!\n" );
+ assert( iPrev < Entry );
+ iPrev = Entry;
+ }
}
return vUsed;
}
@@ -253,7 +195,7 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Int_t * vProof, Vec_Int_t * vRoots, int h
SeeAlso []
***********************************************************************/
-void Proof_CollectUsed_rec( Vec_Int_t * vProof, int hNode, Vec_Int_t * vUsed )
+void Proof_CollectUsed_rec( Vec_Set_t * vProof, int hNode, Vec_Int_t * vUsed )
{
satset * pNext, * pNode = Proof_NodeRead( vProof, hNode );
int i;
@@ -277,19 +219,14 @@ void Proof_CollectUsed_rec( Vec_Int_t * vProof, int hNode, Vec_Int_t * vUsed )
SeeAlso []
***********************************************************************/
-Vec_Int_t * Proof_CollectUsedRec( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hRoot )
+Vec_Int_t * Proof_CollectUsedRec( Vec_Set_t * vProof, Vec_Int_t * vRoots )
{
Vec_Int_t * vUsed;
- assert( (hRoot > 0) ^ (vRoots != NULL) );
+ int i, Entry;
vUsed = Vec_IntAlloc( 1000 );
- if ( hRoot )
- Proof_CollectUsed_rec( vProof, hRoot, vUsed );
- else
- {
- int i, Entry;
- Vec_IntForEachEntry( vRoots, Entry, i )
+ Vec_IntForEachEntry( vRoots, Entry, i )
+ if ( Entry >= 0 )
Proof_CollectUsed_rec( vProof, Entry, vUsed );
- }
return vUsed;
}
@@ -307,7 +244,7 @@ Vec_Int_t * Proof_CollectUsedRec( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hR
SeeAlso []
***********************************************************************/
-void Sat_ProofReduceCheck_rec( Vec_Int_t * vProof, Vec_Int_t * vClauses, satset * pNode, int hClausePivot, Vec_Ptr_t * vVisited )
+void Sat_ProofReduceCheck_rec( Vec_Set_t * vProof, Vec_Int_t * vClauses, satset * pNode, int hClausePivot, Vec_Ptr_t * vVisited )
{
satset * pFanin;
int k;
@@ -323,7 +260,7 @@ void Sat_ProofReduceCheck_rec( Vec_Int_t * vProof, Vec_Int_t * vClauses, satset
}
void Sat_ProofReduceCheckOne( sat_solver2 * s, int iLearnt, Vec_Ptr_t * vVisited )
{
- Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs;
+ Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs;
Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
Vec_Int_t * vRoots = (Vec_Int_t *)&s->claProofs;
int hProofNode = Vec_IntEntry( vRoots, iLearnt );
@@ -357,26 +294,24 @@ void Sat_ProofReduceCheck( sat_solver2 * s )
***********************************************************************/
void Sat_ProofReduce( sat_solver2 * s )
{
- Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs;
+ Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs;
Vec_Int_t * vRoots = (Vec_Int_t *)&s->claProofs;
Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
int fVerbose = 0;
Vec_Int_t * vUsed;
satset * pNode, * pFanin;
- int i, k, hTemp, hNewHandle = 1, clk = clock();
+ int i, k, hTemp, clk = clock();
static int TimeTotal = 0;
// collect visited nodes
- vUsed = Proof_CollectUsedIter( vProof, vRoots, 0 );
-// printf( "The proof uses %d out of %d proof nodes (%.2f %%)\n",
-// Vec_IntSize(vUsed), Proof_CountAll(vProof),
-// 100.0 * Vec_IntSize(vUsed) / Proof_CountAll(vProof) );
+ vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 );
// relabel nodes to use smaller space
+ Vec_SetShrinkS( vProof, 1 );
Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
{
- pNode->Id = hNewHandle; hNewHandle += Proof_NodeSize(pNode->nEnts);
+ pNode->Id = Vec_SetAppendS( vProof, 2+pNode->nEnts );
Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k )
if ( (pNode->pEnts[k] & 1) == 0 ) // proof node
pNode->pEnts[k] = (pFanin->Id << 2) | (pNode->pEnts[k] & 2);
@@ -384,26 +319,27 @@ void Sat_ProofReduce( sat_solver2 * s )
assert( (int*)pFanin >= Vec_IntArray(vClauses) && (int*)pFanin < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) );
}
// update roots
- Proof_ForeachNodeVec( vRoots, vProof, pNode, i )
+ Proof_ForeachNodeVec1( vRoots, vProof, pNode, i )
Vec_IntWriteEntry( vRoots, i, pNode->Id );
// compact the nodes
Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
{
hTemp = pNode->Id; pNode->Id = 0;
- memmove( Vec_IntArray(vProof) + hTemp, pNode, sizeof(int)*Proof_NodeSize(pNode->nEnts) );
+ memmove( Vec_SetEntry(vProof, hTemp), pNode, sizeof(word)*Proof_NodeWordNum(pNode->nEnts) );
}
+ Vec_SetWriteEntryNum( vProof, Vec_IntSize(vUsed) );
Vec_IntFree( vUsed );
// report the result
if ( fVerbose )
{
- printf( "The proof was reduced from %10d to %10d integers (by %6.2f %%) ",
- Vec_IntSize(vProof), hNewHandle, 100.0 * (Vec_IntSize(vProof) - hNewHandle) / Vec_IntSize(vProof) );
+ printf( "The proof was reduced from %6.2f Mb to %6.2f Mb (by %6.2f %%) ",
+ 1.0 * Vec_SetMemory(vProof) / (1<<20), 1.0 * Vec_SetMemoryS(vProof) / (1<<20),
+ 100.0 * (Vec_SetMemory(vProof) - Vec_SetMemoryS(vProof)) / Vec_SetMemory(vProof) );
TimeTotal += clock() - clk;
Abc_PrintTime( 1, "Time", TimeTotal );
}
- Vec_IntShrink( vProof, hNewHandle );
-
+ Vec_SetShrink( vProof, Vec_SetHandCurrentS(vProof) );
Sat_ProofReduceCheck( s );
}
@@ -419,7 +355,7 @@ void Sat_ProofReduce( sat_solver2 * s )
SeeAlso []
***********************************************************************/
-int Sat_ProofCheckResolveOne( Vec_Rec_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp )
+int Sat_ProofCheckResolveOne( Vec_Set_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp )
{
satset * c;
int h, i, k, Var = -1, Count = 0;
@@ -452,9 +388,9 @@ int Sat_ProofCheckResolveOne( Vec_Rec_t * p, satset * c1, satset * c2, Vec_Int_t
if ( (c2->pEnts[i] >> 1) != Var )
Vec_IntPushUnique( vTemp, c2->pEnts[i] );
// create new resolution entry
- h = Vec_RecPush( p, Vec_IntArray(vTemp), Vec_IntSize(vTemp) );
+ h = Vec_SetAppend( p, Vec_IntArray(vTemp), Vec_IntSize(vTemp) );
// return the new entry
- c = Proof_ResolveRead( p, h );
+ c = Proof_NodeRead( p, h );
c->nEnts = Vec_IntSize(vTemp)-2;
return h;
}
@@ -470,15 +406,15 @@ int Sat_ProofCheckResolveOne( Vec_Rec_t * p, satset * c1, satset * c2, Vec_Int_t
SeeAlso []
***********************************************************************/
-satset * Sat_ProofCheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Rec_t * vResolves, int iAnt )
+satset * Sat_ProofCheckReadOne( Vec_Int_t * vClauses, Vec_Set_t * vProof, Vec_Set_t * vResolves, int iAnt )
{
satset * pAnt;
if ( iAnt & 1 )
- return Proof_NodeRead( vClauses, iAnt >> 2 );
+ return Proof_ClauseRead( vClauses, iAnt >> 2 );
assert( iAnt > 0 );
pAnt = Proof_NodeRead( vProof, iAnt >> 2 );
assert( pAnt->Id > 0 );
- return Proof_ResolveRead( vResolves, pAnt->Id );
+ return Proof_NodeRead( vResolves, pAnt->Id );
}
/**Function*************************************************************
@@ -495,24 +431,21 @@ satset * Sat_ProofCheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Re
void Sat_ProofCheck( sat_solver2 * s )
{
Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
- Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs;
- Vec_Rec_t * vResolves;
+ Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs;
+ Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots;
+ Vec_Set_t * vResolves;
Vec_Int_t * vUsed, * vTemp;
satset * pSet, * pSet0, * pSet1;
int i, k, hRoot, Handle, Counter = 0, clk = clock();
-// if ( s->hLearntLast < 0 )
-// return;
-// hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
hRoot = s->hProofLast;
if ( hRoot == -1 )
return;
-
// collect visited clauses
- vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
+ vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 );
Proof_CleanCollected( vProof, vUsed );
// perform resolution steps
vTemp = Vec_IntAlloc( 1000 );
- vResolves = Vec_RecAlloc();
+ vResolves = Vec_SetAlloc();
Proof_ForeachNodeVec( vUsed, vProof, pSet, i )
{
pSet0 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] );
@@ -520,25 +453,23 @@ void Sat_ProofCheck( sat_solver2 * s )
{
pSet1 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] );
Handle = Sat_ProofCheckResolveOne( vResolves, pSet0, pSet1, vTemp );
- pSet0 = Proof_ResolveRead( vResolves, Handle );
+ pSet0 = Proof_NodeRead( vResolves, Handle );
}
pSet->Id = Handle;
-//printf( "Clause for proof %d: ", Vec_IntEntry(vUsed, i) );
-//satset_print( pSet0 );
Counter++;
}
Vec_IntFree( vTemp );
// clean the proof
Proof_CleanCollected( vProof, vUsed );
// compare the final clause
- printf( "Used %6.2f Mb for resolvents.\n", 4.0 * Vec_RecSize(vResolves) / (1<<20) );
+ printf( "Used %6.2f Mb for resolvents.\n", 1.0 * Vec_SetMemory(vResolves) / (1<<20) );
if ( pSet0->nEnts > 0 )
printf( "Derived clause with %d lits instead of the empty clause. ", pSet0->nEnts );
else
printf( "Proof verification successful. " );
Abc_PrintTime( 1, "Time", clock() - clk );
// cleanup
- Vec_RecFree( vResolves );
+ Vec_SetFree( vResolves );
Vec_IntFree( vUsed );
}
@@ -554,7 +485,7 @@ void Sat_ProofCheck( sat_solver2 * s )
SeeAlso []
***********************************************************************/
-Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vUsed, int fUseIds )
+Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Set_t * vProof, Vec_Int_t * vUsed, int fUseIds )
{
Vec_Int_t * vCore;
satset * pNode, * pFanin;
@@ -571,12 +502,11 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_
}
}
// clean core clauses and reexpress core in terms of clause IDs
- Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
+ Proof_ForeachClauseVec( vCore, vClauses, pNode, i )
{
assert( (int*)pNode < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) );
pNode->mark = 0;
if ( fUseIds )
-// Vec_IntWriteEntry( vCore, i, pNode->Id - 1 );
Vec_IntWriteEntry( vCore, i, pNode->Id );
}
return vCore;
@@ -644,8 +574,9 @@ void Sat_ProofInterpolantCheckVars( sat_solver2 * s, Vec_Int_t * vGloVars )
void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
{
Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
- Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs;
+ Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs;
Vec_Int_t * vGlobVars = (Vec_Int_t *)pGloVars;
+ Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots;
Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap;
satset * pNode, * pFanin;
Aig_Man_t * pAig;
@@ -661,7 +592,7 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
Sat_ProofInterpolantCheckVars( s, vGlobVars );
// collect visited nodes
- vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
+ vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 );
// collect core clauses (cleans vUsed and vCore)
vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 0 );
@@ -678,7 +609,7 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
// copy the numbers out and derive interpol for clause
vCoreNums = Vec_IntAlloc( Vec_IntSize(vCore) );
- Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
+ Proof_ForeachClauseVec( vCore, vClauses, pNode, i )
{
if ( pNode->partA )
{
@@ -719,7 +650,7 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
Aig_ManCleanup( pAig );
// move the results back
- Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
+ Proof_ForeachClauseVec( vCore, vClauses, pNode, i )
pNode->Id = Vec_IntEntry( vCoreNums, i );
Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
pNode->Id = 0;
@@ -745,8 +676,9 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
{
Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
- Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs;
+ Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs;
Vec_Int_t * vGlobVars = (Vec_Int_t *)pGloVars;
+ Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots;
Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap;
satset * pNode, * pFanin;
Tru_Man_t * pTru;
@@ -755,9 +687,6 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
word * pRes = ABC_ALLOC( word, nWords );
int i, k, iVar, Lit, Entry, hRoot;
assert( nVars > 0 && nVars <= 16 );
-// if ( s->hLearntLast < 0 )
-// return NULL;
-// hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
hRoot = s->hProofLast;
if ( hRoot == -1 )
return NULL;
@@ -765,7 +694,7 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
Sat_ProofInterpolantCheckVars( s, vGlobVars );
// collect visited nodes
- vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
+ vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 );
// collect core clauses (cleans vUsed and vCore)
vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 0 );
@@ -779,7 +708,7 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
// copy the numbers out and derive interpol for clause
vCoreNums = Vec_IntAlloc( Vec_IntSize(vCore) );
- Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
+ Proof_ForeachClauseVec( vCore, vClauses, pNode, i )
{
if ( pNode->partA )
{
@@ -808,7 +737,7 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k )
{
// assert( pFanin->Id < 2*Aig_ManObjNumMax(pAig) );
- assert( pFanin->Id <= Tru_ManHandleMax(pTru) );
+// assert( pFanin->Id <= Tru_ManHandleMax(pTru) );
if ( k == 0 )
// pObj = Aig_ObjFromLit( pAig, pFanin->Id );
pRes = Tru_ManCopyNotCond( pRes, Tru_ManFunc(pTru, pFanin->Id & ~1), nWords, pFanin->Id & 1 );
@@ -829,7 +758,7 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
// Aig_ManCleanup( pAig );
// move the results back
- Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
+ Proof_ForeachClauseVec( vCore, vClauses, pNode, i )
pNode->Id = Vec_IntEntry( vCoreNums, i );
Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
pNode->Id = 0;
@@ -856,18 +785,15 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
void * Sat_ProofCore( sat_solver2 * s )
{
Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
- Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs;
+ Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs;
+ Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots;
Vec_Int_t * vCore, * vUsed;
int hRoot;
-// if ( s->hLearntLast < 0 )
-// return NULL;
-// hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
hRoot = s->hProofLast;
if ( hRoot == -1 )
return NULL;
-
// collect visited clauses
- vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
+ vUsed = Proof_CollectUsedIter( vProof, vRoots, 0 );
// collect core clauses
vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 1 );
Vec_IntFree( vUsed );
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 8a3cbc33..181d152a 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -71,11 +71,6 @@ static inline int irand(double* seed, int size) {
//=================================================================================================
-// Predeclarations:
-
-static void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *));
-
-//=================================================================================================
// Variable datatype + minor functions:
static const int var0 = 1;
@@ -90,12 +85,12 @@ struct varinfo_t
unsigned lev : 28; // variable level
};
-static inline int var_level (sat_solver* s, int v) { return s->levels[v]; }
-static inline int var_value (sat_solver* s, int v) { return s->assigns[v]; }
+static inline int var_level (sat_solver* s, int v) { return s->levels[v]; }
+static inline int var_value (sat_solver* s, int v) { return s->assigns[v]; }
static inline int var_polar (sat_solver* s, int v) { return s->polarity[v]; }
-static inline void var_set_level (sat_solver* s, int v, int lev) { s->levels[v] = lev; }
-static inline void var_set_value (sat_solver* s, int v, int val) { s->assigns[v] = val; }
+static inline void var_set_level (sat_solver* s, int v, int lev) { s->levels[v] = lev; }
+static inline void var_set_value (sat_solver* s, int v, int val) { s->assigns[v] = val; }
static inline void var_set_polar (sat_solver* s, int v, int pol) { s->polarity[v] = pol; }
// variable tags
@@ -130,7 +125,7 @@ int sat_solver_get_var_value(sat_solver* s, int v)
assert( 0 );
return 0;
}
-
+
//=================================================================================================
// Clause datatype + minor functions:
@@ -140,6 +135,8 @@ struct clause_t
lit lits[0];
};
+static inline clause* clause_read (sat_solver* s, int h) { return (clause *)Vec_SetEntry(&s->Mem, h>>1); }
+
static inline int clause_nlits (clause* c) { return c->size_learnt >> 1; }
static inline lit* clause_begin (clause* c) { return c->lits; }
static inline int clause_learnt (clause* c) { return c->size_learnt & 1; }
@@ -155,21 +152,18 @@ static inline void clause_print (clause* c) {
printf( "}\n" );
}
-static inline clause* clause_read( sat_solver* s, int h ) { return (clause *)Vec_RecEntryP(&s->Mem, h); }
-static inline int clause_size( int nLits, int fLearnt ) { int a = nLits + fLearnt + 1; return a + (a & 1); }
-
//=================================================================================================
// Encode literals in clause pointers:
-static inline int clause_from_lit (lit l) { return l + l + 1; }
-static inline int clause_is_lit (int h) { return (h & 1); }
-static inline lit clause_read_lit (int h) { return (lit)(h >> 1); }
+static inline int clause_from_lit (lit l) { return l + l + 1; }
+static inline int clause_is_lit (int h) { return (h & 1); }
+static inline lit clause_read_lit (int h) { return (lit)(h >> 1); }
//=================================================================================================
// Simple helpers:
-static inline int sat_solver_dl(sat_solver* s) { return veci_size(&s->trail_lim); }
-static inline veci* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; }
+static inline int sat_solver_dl(sat_solver* s) { return veci_size(&s->trail_lim); }
+static inline veci* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; }
//=================================================================================================
// Variable order functions:
@@ -418,15 +412,6 @@ static void sortrnd(void** array, int size, int(*comp)(const void *, const void
}
}
-void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *))
-{
-// int i;
- double seed = 91648253;
- sortrnd(array,size,comp,&seed);
-// for ( i = 1; i < size; i++ )
-// assert(comp(array[i-1], array[i])<0);
-}
-
//=================================================================================================
// Clause functions:
@@ -451,9 +436,9 @@ static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
}
// create new clause
- h = Vec_RecAppend( &s->Mem, clause_size(size, learnt) );
- c = clause_read( s, h );
+ h = Vec_SetAppend( &s->Mem, NULL, size + learnt + 1 ) << 1;
assert( !(h & 1) );
+ c = clause_read( s, h );
if ( s->hLearnts == -1 && learnt )
s->hLearnts = h;
c->size_learnt = (size << 1) | learnt;
@@ -927,9 +912,9 @@ sat_solver* sat_solver_new(void)
{
sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver));
- Vec_RecAlloc_(&s->Mem);
+ Vec_SetAlloc_(&s->Mem);
s->hLearnts = -1;
- s->hBinary = Vec_RecAppend( &s->Mem, clause_size(2, 0) );
+ s->hBinary = Vec_SetAppend( &s->Mem, NULL, 3 ) << 1;
s->binary = clause_read( s, s->hBinary );
s->binary->size_learnt = (2 << 1);
@@ -1049,7 +1034,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
void sat_solver_delete(sat_solver* s)
{
- Vec_RecFree_( &s->Mem );
+ Vec_SetFree_( &s->Mem );
// delete vectors
veci_delete(&s->order);
@@ -1087,10 +1072,10 @@ void sat_solver_delete(sat_solver* s)
void sat_solver_rollback( sat_solver* s )
{
int i;
- Vec_RecRestart( &s->Mem );
+ Vec_SetRestart( &s->Mem );
s->hLearnts = -1;
- s->hBinary = Vec_RecAppend( &s->Mem, clause_size(2, 0) );
+ s->hBinary = Vec_SetAppend( &s->Mem, NULL, 3 ) << 1;
s->binary = clause_read( s, s->hBinary );
s->binary->size_learnt = (2 << 1);
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 30b3742b..de102227 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -29,7 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include <assert.h>
#include "satVec.h"
-#include "vecRec.h"
+#include "vecSet.h"
ABC_NAMESPACE_HEADER_START
@@ -92,7 +92,7 @@ struct sat_solver_t
int qtail; // Tail index of queue.
// clauses
- Vec_Rec_t Mem;
+ Vec_Set_t Mem;
int hLearnts; // the first learnt clause
int hBinary; // the special binary clause
clause * binary;
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 5a54a64e..34908f13 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -172,10 +172,12 @@ static inline void proof_chain_start( sat_solver2* s, satset* c )
{
if ( s->fProofLogging )
{
- s->iStartChain = veci_size(&s->proofs);
- veci_push(&s->proofs, 0);
- veci_push(&s->proofs, 0);
- veci_push(&s->proofs, clause_proofid(s, c, 0) );
+ int ProofId = clause_proofid(s, c, 0);
+ assert( ProofId > 0 );
+ veci_resize( &s->temp_proof, 0 );
+ veci_push( &s->temp_proof, 0 );
+ veci_push( &s->temp_proof, 0 );
+ veci_push( &s->temp_proof, ProofId );
}
}
@@ -183,12 +185,10 @@ static inline void proof_chain_resolve( sat_solver2* s, satset* cls, int Var )
{
if ( s->fProofLogging )
{
-// int CapOld = (&s->proofs)->cap;
satset* c = cls ? cls : var_unit_clause( s, Var );
- veci_push(&s->proofs, clause_proofid(s, c, var_is_partA(s,Var)) );
-// printf( "%d %d ", clause_proofid(s, c), Var );
-// if ( (&s->proofs)->cap > CapOld )
-// printf( "Resized proof from %d to %d.\n", CapOld, (&s->proofs)->cap );
+ int ProofId = clause_proofid(s, c, var_is_partA(s,Var));
+ assert( ProofId > 0 );
+ veci_push( &s->temp_proof, ProofId );
}
}
@@ -196,12 +196,10 @@ static inline int proof_chain_stop( sat_solver2* s )
{
if ( s->fProofLogging )
{
- int RetValue = s->iStartChain;
- satset* c = (satset*)(veci_begin(&s->proofs) + s->iStartChain);
- assert( s->iStartChain > 0 && s->iStartChain < veci_size(&s->proofs) );
- c->nEnts = veci_size(&s->proofs) - s->iStartChain - 2;
- s->iStartChain = 0;
- return RetValue;
+ int h = Vec_SetAppend( &s->Proofs, veci_begin(&s->temp_proof), veci_size(&s->temp_proof) );
+ satset * c = (satset *)Vec_SetEntry( &s->Proofs, h );
+ c->nEnts = veci_size(&s->temp_proof) - 2;
+ return h;
}
return 0;
}
@@ -1119,20 +1117,6 @@ sat_solver2* sat_solver2_new(void)
{
sat_solver2* s = (sat_solver2 *)ABC_CALLOC( char, sizeof(sat_solver2) );
- // initialize vectors
- veci_new(&s->order);
- veci_new(&s->trail_lim);
- veci_new(&s->tagged);
- veci_new(&s->stack);
- veci_new(&s->temp_clause);
- veci_new(&s->conf_final);
- veci_new(&s->mark_levels);
- veci_new(&s->min_lit_order);
- veci_new(&s->min_step_order);
- veci_new(&s->learnt_live);
- veci_new(&s->claActs); veci_push(&s->claActs, -1);
- veci_new(&s->claProofs); veci_push(&s->claProofs, -1);
-
#ifdef USE_FLOAT_ACTIVITY2
s->var_inc = 1;
s->cla_inc = 1;
@@ -1156,6 +1140,23 @@ sat_solver2* sat_solver2_new(void)
s->nLearntMax = 0;
s->fVerbose = 0;
+ // initialize vectors
+ veci_new(&s->order);
+ veci_new(&s->trail_lim);
+ veci_new(&s->tagged);
+ veci_new(&s->stack);
+ veci_new(&s->temp_clause);
+ veci_new(&s->temp_proof);
+ veci_new(&s->conf_final);
+ veci_new(&s->mark_levels);
+ veci_new(&s->min_lit_order);
+ veci_new(&s->min_step_order);
+ veci_new(&s->learnt_live);
+ veci_new(&s->claActs); veci_push(&s->claActs, -1);
+ veci_new(&s->claProofs); veci_push(&s->claProofs, -1);
+ if ( s->fProofLogging )
+ Vec_SetAlloc_( &s->Proofs );
+
// prealloc clause
assert( !s->clauses.ptr );
s->clauses.cap = (1 << 20);
@@ -1166,21 +1167,17 @@ sat_solver2* sat_solver2_new(void)
s->learnts.cap = (1 << 20);
s->learnts.ptr = ABC_ALLOC( int, s->learnts.cap );
veci_push(&s->learnts, -1);
- // prealloc proofs
- if ( s->fProofLogging )
- {
- assert( !s->proofs.ptr );
- s->proofs.cap = (1 << 20);
- s->proofs.ptr = ABC_ALLOC( int, s->proofs.cap );
- veci_push(&s->proofs, -1);
- }
+
// initialize clause pointers
- s->hLearntLast = -1; // the last learnt clause
- s->hProofLast = -1; // the last proof ID
- s->hClausePivot = 1; // the pivot among clauses
- s->hLearntPivot = 1; // the pivot moang learned clauses
- s->iVarPivot = 0; // the pivot among the variables
- s->iSimpPivot = 0; // marker of unit-clauses
+ s->hLearntLast = -1; // the last learnt clause
+ s->hProofLast = -1; // the last proof ID
+ // initialize rollback
+ s->iVarPivot = 0; // the pivot for variables
+ s->iTrailPivot = 0; // the pivot for trail
+ s->iProofPivot = 0; // the pivot for proof records
+ s->hClausePivot = 1; // the pivot for problem clause
+ s->hLearntPivot = 1; // the pivot for learned clause
+ s->hProofPivot = 1; // the pivot for proof records
return s;
}
@@ -1241,35 +1238,38 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
void sat_solver2_delete(sat_solver2* s)
{
-// veci * pCore;
+ int fVerify = 0;
+ if ( fVerify )
+ {
+ veci * pCore = Sat_ProofCore( s );
+ printf( "UNSAT core contains %d clauses (%6.2f %%).\n", veci_size(pCore), 100.0*veci_size(pCore)/veci_size(&s->clauses) );
+ veci_delete( pCore );
+ ABC_FREE( pCore );
+ if ( s->fProofLogging )
+ Sat_ProofCheck( s );
+ }
// report statistics
- printf( "Used %6.2f Mb for proof-logging. Unit clauses = %d.\n", 2.0 * veci_size(&s->proofs) / (1<<20), s->nUnits );
-/*
- pCore = Sat_ProofCore( s );
- printf( "UNSAT core contains %d clauses (%6.2f %%).\n", veci_size(pCore), 100.0*veci_size(pCore)/veci_size(&s->clauses) );
- veci_delete( pCore );
- ABC_FREE( pCore );
+ printf( "Used %6.2f Mb for proof-logging. Unit clauses = %d.\n", 1.0 * Vec_SetMemory(&s->Proofs) / (1<<20), s->nUnits );
- if ( s->fProofLogging )
- Sat_ProofCheck( s );
-*/
// delete vectors
veci_delete(&s->order);
veci_delete(&s->trail_lim);
veci_delete(&s->tagged);
veci_delete(&s->stack);
veci_delete(&s->temp_clause);
+ veci_delete(&s->temp_proof);
veci_delete(&s->conf_final);
veci_delete(&s->mark_levels);
veci_delete(&s->min_lit_order);
veci_delete(&s->min_step_order);
veci_delete(&s->learnt_live);
- veci_delete(&s->proofs);
veci_delete(&s->claActs);
veci_delete(&s->claProofs);
veci_delete(&s->clauses);
veci_delete(&s->learnts);
+// veci_delete(&s->proofs);
+ Vec_SetFree_( &s->Proofs );
// delete arrays
if (s->vi != 0){
@@ -1514,11 +1514,13 @@ void sat_solver2_rollback( sat_solver2* s )
{
int i, k, j;
assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size );
- assert( s->iSimpPivot >= 0 && s->iSimpPivot <= s->qtail );
+ assert( s->iTrailPivot >= 0 && s->iTrailPivot <= s->qtail );
+ assert( s->iProofPivot >= 0 && s->iProofPivot <= Vec_SetEntryNum(&s->Proofs) );
assert( s->hClausePivot >= 1 && s->hClausePivot <= veci_size(&s->clauses) );
assert( s->hLearntPivot >= 1 && s->hLearntPivot <= veci_size(&s->learnts) );
+ assert( s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(&s->Proofs) );
// reset implication queue
- solver2_canceluntil_rollback( s, s->iSimpPivot );
+ solver2_canceluntil_rollback( s, s->iTrailPivot );
// update order
if ( s->iVarPivot < s->size )
{
@@ -1558,7 +1560,9 @@ void sat_solver2_rollback( sat_solver2* s )
veci_resize(&s->claActs, first->Id);
if ( s->fProofLogging ) {
veci_resize(&s->claProofs, first->Id);
- Sat_ProofReduce( s );
+ Vec_SetWriteEntryNum(&s->Proofs, s->iProofPivot);
+ Vec_SetShrink(&s->Proofs, s->hProofPivot);
+// Sat_ProofReduce( s );
}
s->stats.learnts = first->Id-1;
veci_resize(&s->learnts, s->hLearntPivot);
@@ -1600,12 +1604,16 @@ void sat_solver2_rollback( sat_solver2* s )
s->stats.learnts_literals = 0;
s->stats.tot_literals = 0;
// initialize clause pointers
- s->hLearntLast = -1; // the last learnt clause
- s->hProofLast = -1; // the last proof ID
- s->hClausePivot = 1; // the pivot among clauses
- s->hLearntPivot = 1; // the pivot among learned clauses
- s->iVarPivot = 0; // the pivot among the variables
- s->iSimpPivot = 0; // marker of unit-clauses
+ s->hLearntLast = -1; // the last learnt clause
+ s->hProofLast = -1; // the last proof ID
+
+ // initialize rollback
+ s->iVarPivot = 0; // the pivot for variables
+ s->iTrailPivot = 0; // the pivot for trail
+ s->iProofPivot = 0; // the pivot for proof records
+ s->hClausePivot = 1; // the pivot for problem clause
+ s->hLearntPivot = 1; // the pivot for learned clause
+ s->hProofPivot = 1; // the pivot for proof records
}
}
@@ -1803,7 +1811,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
printf("==============================================================================\n");
solver2_canceluntil(s,0);
- assert( s->qhead == s->qtail );
+// assert( s->qhead == s->qtail );
// if ( status == l_True )
// sat_solver2_verify( s );
return status;
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index 4b1eec61..ffbae964 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -29,6 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include <assert.h>
#include "satVec.h"
+#include "vecSet.h"
ABC_NAMESPACE_HEADER_START
@@ -112,16 +113,19 @@ struct sat_solver2_t
veci clauses; // clause memory
veci learnts; // learnt memory
veci* wlists; // watcher lists (for each literal)
+ veci claActs; // clause activities
+ veci claProofs; // clause proofs
int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final)
int hProofLast; // in proof-logging mode, the ID of the final conflict clause (conf_final)
- int hClausePivot; // the pivot among problem clause
- int hLearntPivot; // the pivot among learned clause
- int iVarPivot; // the pivot among the variables
- int iSimpPivot; // marker of unit-clauses
int nof_learnts; // the number of clauses to trigger reduceDB
- veci claActs; // clause activities
- veci claProofs; // clause proofs
+ // rollback
+ int iVarPivot; // the pivot for variables
+ int iTrailPivot; // the pivot for trail
+ int iProofPivot; // the pivot for proof records
+ int hClausePivot; // the pivot for problem clause
+ int hLearntPivot; // the pivot for learned clause
+ int hProofPivot; // the pivot for proof records
// internal state
varinfo2 * vi; // variable information
@@ -146,8 +150,8 @@ struct sat_solver2_t
veci learnt_live; // remaining clauses after reduce DB
// proof logging
- veci proofs; // sequence of proof records
- int iStartChain; // temporary variable to remember beginning of the current chain in proof logging
+ Vec_Set_t Proofs; // sequence of proof records
+ veci temp_proof; // temporary place to store proofs
int nUnits; // the total number of unit clauses
// statistics
@@ -251,10 +255,12 @@ static inline int sat_solver2_set_learntmax(sat_solver2* s, int nLearntMax)
static inline void sat_solver2_bookmark(sat_solver2* s)
{
assert( s->qhead == s->qtail );
- s->hLearntPivot = veci_size(&s->learnts);
- s->hClausePivot = veci_size(&s->clauses);
s->iVarPivot = s->size;
- s->iSimpPivot = s->qhead;
+ s->iTrailPivot = s->qhead;
+ s->iProofPivot = Vec_SetEntryNum(&s->Proofs);
+ s->hClausePivot = veci_size(&s->clauses);
+ s->hLearntPivot = veci_size(&s->learnts);
+ s->hProofPivot = Vec_SetHandCurrent(&s->Proofs);
}
static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark )
diff --git a/src/sat/bsat/satSolver_old.c b/src/sat/bsat/satSolver_old.c
deleted file mode 100644
index 4d851d0f..00000000
--- a/src/sat/bsat/satSolver_old.c
+++ /dev/null
@@ -1,1766 +0,0 @@
-/**************************************************************************************************
-MiniSat -- Copyright (c) 2005, Niklas Sorensson
-http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
-
-Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
-associated documentation files (the "Software"), to deal in the Software without restriction,
-including without limitation the rights to use, copy, modify, merge, publish, distribute,
-sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in all copies or
-substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
-NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
-DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
-OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
-**************************************************************************************************/
-// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
-
-#include <stdio.h>
-#include <assert.h>
-#include <string.h>
-#include <math.h>
-
-#include "satSolver.h"
-#include "satStore.h"
-
-ABC_NAMESPACE_IMPL_START
-
-//#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-#define SAT_USE_ANALYZE_FINAL
-
-//=================================================================================================
-// Debug:
-
-//#define VERBOSEDEBUG
-
-// For derivation output (verbosity level 2)
-#define L_IND "%-*d"
-#define L_ind sat_solver_dl(s)*2+2,sat_solver_dl(s)
-#define L_LIT "%sx%d"
-#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
-
-// Just like 'assert()' but expression will be evaluated in the release version as well.
-static inline void check(int expr) { assert(expr); }
-
-static void printlits(lit* begin, lit* end)
-{
- int i;
- for (i = 0; i < end - begin; i++)
- printf(L_LIT" ",L_lit(begin[i]));
-}
-
-//=================================================================================================
-// Random numbers:
-
-
-// Returns a random float 0 <= x < 1. Seed must never be 0.
-static inline double drand(double* seed) {
- int q;
- *seed *= 1389796;
- q = (int)(*seed / 2147483647);
- *seed -= (double)q * 2147483647;
- return *seed / 2147483647; }
-
-
-// Returns a random integer 0 <= x < size. Seed must never be 0.
-static inline int irand(double* seed, int size) {
- return (int)(drand(seed) * size); }
-
-
-//=================================================================================================
-// Predeclarations:
-
-static void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *));
-
-//=================================================================================================
-// Clause datatype + minor functions:
-
-struct clause_t
-{
- int size_learnt;
- lit lits[0];
-};
-
-static inline int clause_size (clause* c) { return c->size_learnt >> 1; }
-static inline lit* clause_begin (clause* c) { return c->lits; }
-static inline int clause_learnt (clause* c) { return c->size_learnt & 1; }
-static inline float clause_activity (clause* c) { return *((float*)&c->lits[c->size_learnt>>1]); }
-static inline unsigned clause_activity2 (clause* c) { return *((unsigned*)&c->lits[c->size_learnt>>1]); }
-static inline void clause_setactivity (clause* c, float a) { *((float*)&c->lits[c->size_learnt>>1]) = a; }
-static inline void clause_setactivity2 (clause* c, unsigned a) { *((unsigned*)&c->lits[c->size_learnt>>1]) = a; }
-static inline void clause_print (clause* c) {
- int i;
- printf( "{ " );
- for ( i = 0; i < clause_size(c); i++ )
- printf( "%d ", (clause_begin(c)[i] & 1)? -(clause_begin(c)[i] >> 1) : clause_begin(c)[i] >> 1 );
- printf( "}\n" );
-}
-
-//=================================================================================================
-// Encode literals in clause pointers:
-
-static inline clause* clause_from_lit (lit l) { return (clause*)((ABC_PTRUINT_T)l + (ABC_PTRUINT_T)l + 1); }
-static inline int clause_is_lit (clause* c) { return ((ABC_PTRUINT_T)c & 1); }
-static inline lit clause_read_lit (clause* c) { return (lit)((ABC_PTRUINT_T)c >> 1); }
-
-//=================================================================================================
-// Simple helpers:
-
-static inline int sat_solver_dl(sat_solver* s) { return veci_size(&s->trail_lim); }
-static inline vecp* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; }
-
-//=================================================================================================
-// Variable order functions:
-
-static inline void order_update(sat_solver* s, int v) // updateorder
-{
- int* orderpos = s->orderpos;
- int* heap = veci_begin(&s->order);
- int i = orderpos[v];
- int x = heap[i];
- int parent = (i - 1) / 2;
-
- assert(s->orderpos[v] != -1);
-
- while (i != 0 && s->activity[x] > s->activity[heap[parent]]){
- heap[i] = heap[parent];
- orderpos[heap[i]] = i;
- i = parent;
- parent = (i - 1) / 2;
- }
- heap[i] = x;
- orderpos[x] = i;
-}
-
-static inline void order_assigned(sat_solver* s, int v)
-{
-}
-
-static inline void order_unassigned(sat_solver* s, int v) // undoorder
-{
- int* orderpos = s->orderpos;
- if (orderpos[v] == -1){
- orderpos[v] = veci_size(&s->order);
- veci_push(&s->order,v);
- order_update(s,v);
-//printf( "+%d ", v );
- }
-}
-
-static inline int order_select(sat_solver* s, float random_var_freq) // selectvar
-{
- int* heap;
- int* orderpos;
-
- lbool* values = s->assigns;
-
- // Random decision:
- if (drand(&s->random_seed) < random_var_freq){
- int next = irand(&s->random_seed,s->size);
- assert(next >= 0 && next < s->size);
- if (values[next] == l_Undef)
- return next;
- }
-
- // Activity based decision:
-
- heap = veci_begin(&s->order);
- orderpos = s->orderpos;
-
-
- while (veci_size(&s->order) > 0){
- int next = heap[0];
- int size = veci_size(&s->order)-1;
- int x = heap[size];
-
- veci_resize(&s->order,size);
-
- orderpos[next] = -1;
-
- if (size > 0){
-
- int i = 0;
- int child = 1;
-
-
- while (child < size){
- if (child+1 < size && s->activity[heap[child]] < s->activity[heap[child+1]])
- child++;
-
- assert(child < size);
-
- if (s->activity[x] >= s->activity[heap[child]])
- break;
-
- heap[i] = heap[child];
- orderpos[heap[i]] = i;
- i = child;
- child = 2 * child + 1;
- }
- heap[i] = x;
- orderpos[heap[i]] = i;
- }
-
-//printf( "-%d ", next );
- if (values[next] == l_Undef)
- return next;
- }
-
- return var_Undef;
-}
-
-//=================================================================================================
-// Activity functions:
-
-#ifdef USE_FLOAT_ACTIVITY
-
-static inline void act_var_rescale(sat_solver* s) {
- double* activity = s->activity;
- int i;
- for (i = 0; i < s->size; i++)
- activity[i] *= 1e-100;
- s->var_inc *= 1e-100;
-}
-static inline void act_clause_rescale(sat_solver* s) {
- static int Total = 0;
- clause** cs = (clause**)vecp_begin(&s->learnts);
- int i, clk = clock();
- for (i = 0; i < vecp_size(&s->learnts); i++){
- float a = clause_activity(cs[i]);
- clause_setactivity(cs[i], a * (float)1e-20);
- }
- s->cla_inc *= (float)1e-20;
-
- Total += clock() - clk;
- printf( "Rescaling... Cla inc = %10.3f Conf = %10d ", s->cla_inc, s->stats.conflicts );
- Abc_PrintTime( 1, "Time", Total );
-}
-static inline void act_var_bump(sat_solver* s, int v) {
- s->activity[v] += s->var_inc;
- if (s->activity[v] > 1e100)
- act_var_rescale(s);
- if (s->orderpos[v] != -1)
- order_update(s,v);
-}
-static inline void act_var_bump_global(sat_solver* s, int v) {
- s->activity[v] += (s->var_inc * 3.0 * s->pGlobalVars[v]);
- if (s->activity[v] > 1e100)
- act_var_rescale(s);
- if (s->orderpos[v] != -1)
- order_update(s,v);
-}
-static inline void act_var_bump_factor(sat_solver* s, int v) {
- s->activity[v] += (s->var_inc * s->factors[v]);
- if (s->activity[v] > 1e100)
- act_var_rescale(s);
- if (s->orderpos[v] != -1)
- order_update(s,v);
-}
-static inline void act_clause_bump(sat_solver* s, clause *c) {
- float a = clause_activity(c) + s->cla_inc;
- clause_setactivity(c,a);
- if (a > 1e20) act_clause_rescale(s);
-}
-static inline void act_var_decay(sat_solver* s) { s->var_inc *= s->var_decay; }
-static inline void act_clause_decay(sat_solver* s) { s->cla_inc *= s->cla_decay; }
-
-#else
-
-static inline void act_var_rescale(sat_solver* s) {
- unsigned* activity = s->activity;
- int i;
- for (i = 0; i < s->size; i++)
- activity[i] >>= 19;
- s->var_inc >>= 19;
- s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) );
-}
-static inline void act_clause_rescale(sat_solver* s) {
- static int Total = 0;
- clause** cs = (clause**)vecp_begin(&s->learnts);
- int i, clk = clock();
- for (i = 0; i < vecp_size(&s->learnts); i++){
- unsigned a = clause_activity2(cs[i]);
- clause_setactivity2(cs[i], a >> 14);
- }
- s->cla_inc >>= 14;
- s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
-
-// Total += clock() - clk;
-// printf( "Rescaling... Cla inc = %5d Conf = %10d ", s->cla_inc, s->stats.conflicts );
-// Abc_PrintTime( 1, "Time", Total );
-}
-static inline void act_var_bump(sat_solver* s, int v) {
- s->activity[v] += s->var_inc;
- if (s->activity[v] & 0x80000000)
- act_var_rescale(s);
- if (s->orderpos[v] != -1)
- order_update(s,v);
-}
-static inline void act_var_bump_global(sat_solver* s, int v) {}
-static inline void act_var_bump_factor(sat_solver* s, int v) {}
-static inline void act_clause_bump(sat_solver* s, clause*c) {
- unsigned a = clause_activity2(c) + s->cla_inc;
- clause_setactivity2(c,a);
- if (a & 0x80000000)
- act_clause_rescale(s);
-}
-static inline void act_var_decay(sat_solver* s) { s->var_inc += (s->var_inc >> 4); }
-static inline void act_clause_decay(sat_solver* s) { s->cla_inc += (s->cla_inc >> 10); }
-
-#endif
-
-
-//=================================================================================================
-// Clause functions:
-
-/* pre: size > 1 && no variable occurs twice
- */
-static clause* clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
-{
- int size;
- clause* c;
- int i;
-
- assert(end - begin > 1);
- assert(learnt >= 0 && learnt < 2);
- size = end - begin;
-
- // do not allocate memory for the two-literal problem clause
- if ( size == 2 && !learnt )
- {
- vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(clause_from_lit(begin[1])));
- vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(clause_from_lit(begin[0])));
- return NULL;
- }
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
- c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
-#else
- c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) );
-#endif
-
- c->size_learnt = (size << 1) | learnt;
- assert(((ABC_PTRUINT_T)c & 1) == 0);
-
- for (i = 0; i < size; i++)
- c->lits[i] = begin[i];
-
- if (learnt)
- *((float*)&c->lits[size]) = 0.0;
-
- assert(begin[0] >= 0);
- assert(begin[0] < s->size*2);
- assert(begin[1] >= 0);
- assert(begin[1] < s->size*2);
-
- assert(lit_neg(begin[0]) < s->size*2);
- assert(lit_neg(begin[1]) < s->size*2);
-
- //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
- //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
-
- vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
- vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
-
- return c;
-}
-
-
-//=================================================================================================
-// Minor (solver) functions:
-
-static inline int sat_solver_enqueue(sat_solver* s, lit l, clause* from)
-{
- lbool* values = s->assigns;
- int v = lit_var(l);
- lbool val = values[v];
- lbool sig;
-#ifdef VERBOSEDEBUG
- printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
-#endif
-
- sig = !lit_sign(l); sig += sig - 1;
- if (val != l_Undef){
- return val == sig;
- }else{
- int* levels = s->levels;
- clause** reasons = s->reasons;
- // New fact -- store it.
-#ifdef VERBOSEDEBUG
- printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
-#endif
- values [v] = sig;
- levels [v] = sat_solver_dl(s);
- reasons[v] = from;
- s->trail[s->qtail++] = l;
-
- order_assigned(s, v);
- return true;
- }
-}
-
-
-static inline int sat_solver_assume(sat_solver* s, lit l){
- assert(s->qtail == s->qhead);
- assert(s->assigns[lit_var(l)] == l_Undef);
-#ifdef VERBOSEDEBUG
- printf(L_IND"assume("L_LIT") ", L_ind, L_lit(l));
- printf( "act = %.20f\n", s->activity[lit_var(l)] );
-#endif
- veci_push(&s->trail_lim,s->qtail);
- return sat_solver_enqueue(s,l,(clause*)0);
-}
-
-
-static void sat_solver_canceluntil(sat_solver* s, int level) {
- lit* trail;
- lbool* values;
- clause** reasons;
- int bound;
- int lastLev;
- int c;
-
- if (sat_solver_dl(s) <= level)
- return;
-
- trail = s->trail;
- values = s->assigns;
- reasons = s->reasons;
- bound = (veci_begin(&s->trail_lim))[level];
- lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1];
-
- ////////////////////////////////////////
- // added to cancel all assignments
-// if ( level == -1 )
-// bound = 0;
- ////////////////////////////////////////
-
- for (c = s->qtail-1; c >= bound; c--) {
- int x = lit_var(trail[c]);
- values [x] = l_Undef;
- reasons[x] = (clause*)0;
- if ( c < lastLev )
- s->polarity[x] = !lit_sign(trail[c]);
- }
-
- for (c = s->qhead-1; c >= bound; c--)
- order_unassigned(s,lit_var(trail[c]));
-
- s->qhead = s->qtail = bound;
- veci_resize(&s->trail_lim,level);
-}
-
-static void sat_solver_record(sat_solver* s, veci* cls)
-{
- lit* begin = veci_begin(cls);
- lit* end = begin + veci_size(cls);
- clause* c = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : (clause*)0;
- sat_solver_enqueue(s,*begin,c);
-
- ///////////////////////////////////
- // add clause to internal storage
- if ( s->pStore )
- {
- int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end );
- assert( RetValue );
- }
- ///////////////////////////////////
-
- assert(veci_size(cls) > 0);
-
- if (c != 0) {
- vecp_push(&s->learnts,c);
- act_clause_bump(s,c);
- s->stats.learnts++;
- s->stats.learnts_literals += veci_size(cls);
- }
-}
-
-
-static double sat_solver_progress(sat_solver* s)
-{
- lbool* values = s->assigns;
- int* levels = s->levels;
- int i;
-
- double progress = 0;
- double F = 1.0 / s->size;
- for (i = 0; i < s->size; i++)
- if (values[i] != l_Undef)
- progress += pow(F, levels[i]);
- return progress / s->size;
-}
-
-//=================================================================================================
-// Major methods:
-
-static int sat_solver_lit_removable(sat_solver* s, lit l, int minl)
-{
- lbool* tags = s->tags;
- clause** reasons = s->reasons;
- int* levels = s->levels;
- int top = veci_size(&s->tagged);
-
- assert(lit_var(l) >= 0 && lit_var(l) < s->size);
- assert(reasons[lit_var(l)] != 0);
- veci_resize(&s->stack,0);
- veci_push(&s->stack,lit_var(l));
-
- while (veci_size(&s->stack) > 0){
- clause* c;
- int v = veci_begin(&s->stack)[veci_size(&s->stack)-1];
- assert(v >= 0 && v < s->size);
- veci_resize(&s->stack,veci_size(&s->stack)-1);
- assert(reasons[v] != 0);
- c = reasons[v];
-
- if (clause_is_lit(c)){
- int v = lit_var(clause_read_lit(c));
- if (tags[v] == l_Undef && levels[v] != 0){
- if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
- veci_push(&s->stack,v);
- tags[v] = l_True;
- veci_push(&s->tagged,v);
- }else{
- int* tagged = veci_begin(&s->tagged);
- int j;
- for (j = top; j < veci_size(&s->tagged); j++)
- tags[tagged[j]] = l_Undef;
- veci_resize(&s->tagged,top);
- return false;
- }
- }
- }else{
- lit* lits = clause_begin(c);
- int i, j;
-
- for (i = 1; i < clause_size(c); i++){
- int v = lit_var(lits[i]);
- if (tags[v] == l_Undef && levels[v] != 0){
- if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
-
- veci_push(&s->stack,lit_var(lits[i]));
- tags[v] = l_True;
- veci_push(&s->tagged,v);
- }else{
- int* tagged = veci_begin(&s->tagged);
- for (j = top; j < veci_size(&s->tagged); j++)
- tags[tagged[j]] = l_Undef;
- veci_resize(&s->tagged,top);
- return false;
- }
- }
- }
- }
- }
-
- return true;
-}
-
-
-/*_________________________________________________________________________________________________
-|
-| analyzeFinal : (p : Lit) -> [void]
-|
-| Description:
-| Specialized analysis procedure to express the final conflict in terms of assumptions.
-| Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
-| stores the result in 'out_conflict'.
-|________________________________________________________________________________________________@*/
-/*
-void Solver::analyzeFinal(Clause* confl, bool skip_first)
-{
- // -- NOTE! This code is relatively untested. Please report bugs!
- conflict.clear();
- if (root_level == 0) return;
-
- vec<char>& seen = analyze_seen;
- for (int i = skip_first ? 1 : 0; i < confl->size(); i++){
- Var x = var((*confl)[i]);
- if (level[x] > 0)
- seen[x] = 1;
- }
-
- int start = (root_level >= trail_lim.size()) ? trail.size()-1 : trail_lim[root_level];
- for (int i = start; i >= trail_lim[0]; i--){
- Var x = var(trail[i]);
- if (seen[x]){
- GClause r = reason[x];
- if (r == GClause_NULL){
- assert(level[x] > 0);
- conflict.push(~trail[i]);
- }else{
- if (r.isLit()){
- Lit p = r.lit();
- if (level[var(p)] > 0)
- seen[var(p)] = 1;
- }else{
- Clause& c = *r.clause();
- for (int j = 1; j < c.size(); j++)
- if (level[var(c[j])] > 0)
- seen[var(c[j])] = 1;
- }
- }
- seen[x] = 0;
- }
- }
-}
-*/
-
-#ifdef SAT_USE_ANALYZE_FINAL
-
-static void sat_solver_analyze_final(sat_solver* s, clause* conf, int skip_first)
-{
- int i, j, start;
- veci_resize(&s->conf_final,0);
- if ( s->root_level == 0 )
- return;
- assert( veci_size(&s->tagged) == 0 );
-// assert( s->tags[lit_var(p)] == l_Undef );
-// s->tags[lit_var(p)] = l_True;
- for (i = skip_first ? 1 : 0; i < clause_size(conf); i++)
- {
- int x = lit_var(clause_begin(conf)[i]);
- if (s->levels[x] > 0)
- {
- s->tags[x] = l_True;
- veci_push(&s->tagged,x);
- }
- }
-
- start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->root_level];
- for (i = start; i >= (veci_begin(&s->trail_lim))[0]; i--){
- int x = lit_var(s->trail[i]);
- if (s->tags[x] == l_True){
- if (s->reasons[x] == NULL){
- assert(s->levels[x] > 0);
- veci_push(&s->conf_final,lit_neg(s->trail[i]));
- }else{
- clause* c = s->reasons[x];
- if (clause_is_lit(c)){
- lit q = clause_read_lit(c);
- assert(lit_var(q) >= 0 && lit_var(q) < s->size);
- if (s->levels[lit_var(q)] > 0)
- {
- s->tags[lit_var(q)] = l_True;
- veci_push(&s->tagged,lit_var(q));
- }
- }
- else{
- int* lits = clause_begin(c);
- for (j = 1; j < clause_size(c); j++)
- if (s->levels[lit_var(lits[j])] > 0)
- {
- s->tags[lit_var(lits[j])] = l_True;
- veci_push(&s->tagged,lit_var(lits[j]));
- }
- }
- }
- }
- }
- for (i = 0; i < veci_size(&s->tagged); i++)
- s->tags[veci_begin(&s->tagged)[i]] = l_Undef;
- veci_resize(&s->tagged,0);
-}
-
-#endif
-
-
-static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
-{
- lit* trail = s->trail;
- lbool* tags = s->tags;
- clause** reasons = s->reasons;
- int* levels = s->levels;
- int cnt = 0;
- lit p = lit_Undef;
- int ind = s->qtail-1;
- lit* lits;
- int i, j, minl;
- int* tagged;
-
- veci_push(learnt,lit_Undef);
-
- do{
- assert(c != 0);
-
- if (clause_is_lit(c)){
- lit q = clause_read_lit(c);
- assert(lit_var(q) >= 0 && lit_var(q) < s->size);
- if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
- tags[lit_var(q)] = l_True;
- veci_push(&s->tagged,lit_var(q));
- act_var_bump(s,lit_var(q));
- if (levels[lit_var(q)] == sat_solver_dl(s))
- cnt++;
- else
- veci_push(learnt,q);
- }
- }else{
-
- if (clause_learnt(c))
- act_clause_bump(s,c);
-
- lits = clause_begin(c);
- //printlits(lits,lits+clause_size(c)); printf("\n");
- for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){
- lit q = lits[j];
- assert(lit_var(q) >= 0 && lit_var(q) < s->size);
- if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
- tags[lit_var(q)] = l_True;
- veci_push(&s->tagged,lit_var(q));
- act_var_bump(s,lit_var(q));
- if (levels[lit_var(q)] == sat_solver_dl(s))
- cnt++;
- else
- veci_push(learnt,q);
- }
- }
- }
-
- while (tags[lit_var(trail[ind--])] == l_Undef);
-
- p = trail[ind+1];
- c = reasons[lit_var(p)];
- cnt--;
-
- }while (cnt > 0);
-
- *veci_begin(learnt) = lit_neg(p);
-
- lits = veci_begin(learnt);
- minl = 0;
- for (i = 1; i < veci_size(learnt); i++){
- int lev = levels[lit_var(lits[i])];
- minl |= 1 << (lev & 31);
- }
-
- // simplify (full)
- for (i = j = 1; i < veci_size(learnt); i++){
- if (reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lits[i],minl))
- lits[j++] = lits[i];
- }
-
- // update size of learnt + statistics
- veci_resize(learnt,j);
- s->stats.tot_literals += j;
-
- // clear tags
- tagged = veci_begin(&s->tagged);
- for (i = 0; i < veci_size(&s->tagged); i++)
- tags[tagged[i]] = l_Undef;
- veci_resize(&s->tagged,0);
-
-#ifdef DEBUG
- for (i = 0; i < s->size; i++)
- assert(tags[i] == l_Undef);
-#endif
-
-#ifdef VERBOSEDEBUG
- printf(L_IND"Learnt {", L_ind);
- for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i]));
-#endif
- if (veci_size(learnt) > 1){
- int max_i = 1;
- int max = levels[lit_var(lits[1])];
- lit tmp;
-
- for (i = 2; i < veci_size(learnt); i++)
- if (levels[lit_var(lits[i])] > max){
- max = levels[lit_var(lits[i])];
- max_i = i;
- }
-
- tmp = lits[1];
- lits[1] = lits[max_i];
- lits[max_i] = tmp;
- }
-#ifdef VERBOSEDEBUG
- {
- int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0;
- printf(" } at level %d\n", lev);
- }
-#endif
-}
-
-
-clause* sat_solver_propagate(sat_solver* s)
-{
- lbool* values = s->assigns;
- clause* confl = (clause*)0;
- lit* lits;
- lit false_lit;
- lbool sig;
-
- //printf("sat_solver_propagate\n");
- while (confl == 0 && s->qtail - s->qhead > 0){
- lit p = s->trail[s->qhead++];
- vecp* ws = sat_solver_read_wlist(s,p);
- clause **begin = (clause**)vecp_begin(ws);
- clause **end = begin + vecp_size(ws);
- clause **i, **j;
-
- s->stats.propagations++;
- s->simpdb_props--;
-
- //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
- for (i = j = begin; i < end; ){
- if (clause_is_lit(*i)){
-
- int Lit = clause_read_lit(*i);
- sig = !lit_sign(Lit); sig += sig - 1;
- if (values[lit_var(Lit)] == sig){
- *j++ = *i++;
- continue;
- }
-
- *j++ = *i;
- if (!sat_solver_enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
- confl = s->binary;
- (clause_begin(confl))[1] = lit_neg(p);
- (clause_begin(confl))[0] = clause_read_lit(*i++);
- // Copy the remaining watches:
- while (i < end)
- *j++ = *i++;
- }
- }else{
-
- lits = clause_begin(*i);
-
- // Make sure the false literal is data[1]:
- false_lit = lit_neg(p);
- if (lits[0] == false_lit){
- lits[0] = lits[1];
- lits[1] = false_lit;
- }
- assert(lits[1] == false_lit);
- //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n");
-
- // If 0th watch is true, then clause is already satisfied.
- sig = !lit_sign(lits[0]); sig += sig - 1;
- if (values[lit_var(lits[0])] == sig){
- *j++ = *i;
- }else{
- // Look for new watch:
- lit* stop = lits + clause_size(*i);
- lit* k;
- for (k = lits + 2; k < stop; k++){
- lbool sig = lit_sign(*k); sig += sig - 1;
- if (values[lit_var(*k)] != sig){
- lits[1] = *k;
- *k = false_lit;
- vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
- goto next; }
- }
-
- *j++ = *i;
- // Clause is unit under assignment:
- if (!sat_solver_enqueue(s,lits[0], *i)){
- confl = *i++;
- // Copy the remaining watches:
- while (i < end)
- *j++ = *i++;
- }
- }
- }
- next:
- i++;
- }
-
- s->stats.inspects += j - (clause**)vecp_begin(ws);
- vecp_resize(ws,j - (clause**)vecp_begin(ws));
- }
-
- return confl;
-}
-
-//=================================================================================================
-// External solver functions:
-
-sat_solver* sat_solver_new(void)
-{
- sat_solver* s = (sat_solver*)ABC_ALLOC( char, sizeof(sat_solver));
- memset( s, 0, sizeof(sat_solver) );
-
- // initialize vectors
- vecp_new(&s->clauses);
- vecp_new(&s->learnts);
- veci_new(&s->order);
- veci_new(&s->trail_lim);
- veci_new(&s->tagged);
- veci_new(&s->stack);
- veci_new(&s->model);
- veci_new(&s->act_vars);
- veci_new(&s->temp_clause);
- veci_new(&s->conf_final);
-
- // initialize arrays
- s->wlists = 0;
- s->activity = 0;
- s->factors = 0;
- s->assigns = 0;
- s->orderpos = 0;
- s->reasons = 0;
- s->levels = 0;
- s->tags = 0;
- s->trail = 0;
-
-
- // initialize other vars
- s->size = 0;
- s->cap = 0;
- s->qhead = 0;
- s->qtail = 0;
-#ifdef USE_FLOAT_ACTIVITY
- s->var_inc = 1;
- s->cla_inc = 1;
- s->var_decay = (float)(1 / 0.95 );
- s->cla_decay = (float)(1 / 0.999 );
-#else
- s->var_inc = (1 << 5);
- s->cla_inc = (1 << 11);
-#endif
- s->root_level = 0;
- s->simpdb_assigns = 0;
- s->simpdb_props = 0;
- s->random_seed = 91648253;
- s->progress_estimate = 0;
- s->binary = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2);
- s->binary->size_learnt = (2 << 1);
- s->verbosity = 0;
-
- s->stats.starts = 0;
- s->stats.decisions = 0;
- s->stats.propagations = 0;
- s->stats.inspects = 0;
- s->stats.conflicts = 0;
- s->stats.clauses = 0;
- s->stats.clauses_literals = 0;
- s->stats.learnts = 0;
- s->stats.learnts_literals = 0;
- s->stats.tot_literals = 0;
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
- s->pMem = NULL;
-#else
- s->pMem = Sat_MmStepStart( 10 );
-#endif
- return s;
-}
-
-void sat_solver_setnvars(sat_solver* s,int n)
-{
- int var;
-
- if (s->cap < n){
- int old_cap = s->cap;
- while (s->cap < n) s->cap = s->cap*2+1;
-
- s->wlists = ABC_REALLOC(vecp, s->wlists, s->cap*2);
-#ifdef USE_FLOAT_ACTIVITY
- s->activity = ABC_REALLOC(double, s->activity, s->cap);
-#else
- s->activity = ABC_REALLOC(unsigned, s->activity, s->cap);
-#endif
- s->factors = ABC_REALLOC(double, s->factors, s->cap);
- s->assigns = ABC_REALLOC(lbool, s->assigns, s->cap);
- s->orderpos = ABC_REALLOC(int, s->orderpos, s->cap);
- s->reasons = ABC_REALLOC(clause*,s->reasons, s->cap);
- s->levels = ABC_REALLOC(int, s->levels, s->cap);
- s->tags = ABC_REALLOC(lbool, s->tags, s->cap);
- s->trail = ABC_REALLOC(lit, s->trail, s->cap);
- s->polarity = ABC_REALLOC(char, s->polarity, s->cap);
- memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(vecp) );
- }
-
- for (var = s->size; var < n; var++){
- assert(!s->wlists[2*var].size);
- assert(!s->wlists[2*var+1].size);
- if ( s->wlists[2*var].ptr == NULL )
- vecp_new(&s->wlists[2*var]);
- if ( s->wlists[2*var+1].ptr == NULL )
- vecp_new(&s->wlists[2*var+1]);
-#ifdef USE_FLOAT_ACTIVITY
- s->activity[var] = 0;
-#else
- s->activity[var] = (1<<10);
-#endif
- s->factors [var] = 0;
- s->assigns [var] = l_Undef;
- s->orderpos [var] = veci_size(&s->order);
- s->reasons [var] = (clause*)0;
- s->levels [var] = 0;
- s->tags [var] = l_Undef;
- s->polarity [var] = 0;
-
- /* does not hold because variables enqueued at top level will not be reinserted in the heap
- assert(veci_size(&s->order) == var);
- */
- veci_push(&s->order,var);
- order_update(s, var);
- }
-
- s->size = n > s->size ? n : s->size;
-}
-
-void sat_solver_delete(sat_solver* s)
-{
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
- int i;
- for (i = 0; i < vecp_size(&s->clauses); i++)
- ABC_FREE(vecp_begin(&s->clauses)[i]);
- for (i = 0; i < vecp_size(&s->learnts); i++)
- ABC_FREE(vecp_begin(&s->learnts)[i]);
-#else
- Sat_MmStepStop( s->pMem, 0 );
-#endif
-
- // delete vectors
- vecp_delete(&s->clauses);
- vecp_delete(&s->learnts);
- veci_delete(&s->order);
- veci_delete(&s->trail_lim);
- veci_delete(&s->tagged);
- veci_delete(&s->stack);
- veci_delete(&s->model);
- veci_delete(&s->act_vars);
- veci_delete(&s->temp_clause);
- veci_delete(&s->conf_final);
- ABC_FREE(s->binary);
-
- // delete arrays
- if (s->wlists != 0){
- int i;
- for (i = 0; i < s->cap*2; i++)
- vecp_delete(&s->wlists[i]);
- ABC_FREE(s->wlists );
- ABC_FREE(s->activity );
- ABC_FREE(s->factors );
- ABC_FREE(s->assigns );
- ABC_FREE(s->orderpos );
- ABC_FREE(s->reasons );
- ABC_FREE(s->levels );
- ABC_FREE(s->trail );
- ABC_FREE(s->tags );
- ABC_FREE(s->polarity );
- }
-
- sat_solver_store_free(s);
- ABC_FREE(s);
-}
-
-void sat_solver_rollback( sat_solver* s )
-{
- int i;
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
- for (i = 0; i < vecp_size(&s->clauses); i++)
- ABC_FREE(vecp_begin(&s->clauses)[i]);
- for (i = 0; i < vecp_size(&s->learnts); i++)
- ABC_FREE(vecp_begin(&s->learnts)[i]);
-#else
- Sat_MmStepRestart( s->pMem );
-#endif
- vecp_resize(&s->clauses, 0);
- vecp_resize(&s->learnts, 0);
- veci_resize(&s->trail_lim, 0);
- veci_resize(&s->order, 0);
- for ( i = 0; i < s->size*2; i++ )
- s->wlists[i].size = 0;
-
- // initialize other vars
- s->size = 0;
-// s->cap = 0;
- s->qhead = 0;
- s->qtail = 0;
-#ifdef USE_FLOAT_ACTIVITY
- s->var_inc = 1;
- s->cla_inc = 1;
- s->var_decay = (float)(1 / 0.95 );
- s->cla_decay = (float)(1 / 0.999 );
-#else
- s->var_inc = (1 << 5);
- s->cla_inc = (1 << 11);
-#endif
- s->root_level = 0;
- s->simpdb_assigns = 0;
- s->simpdb_props = 0;
- s->random_seed = 91648253;
- s->progress_estimate = 0;
- s->verbosity = 0;
-
- s->stats.starts = 0;
- s->stats.decisions = 0;
- s->stats.propagations = 0;
- s->stats.inspects = 0;
- s->stats.conflicts = 0;
- s->stats.clauses = 0;
- s->stats.clauses_literals = 0;
- s->stats.learnts = 0;
- s->stats.learnts_literals = 0;
- s->stats.tot_literals = 0;
-}
-
-
-static void clause_remove(sat_solver* s, clause* c)
-{
- lit* lits = clause_begin(c);
- assert(lit_neg(lits[0]) < s->size*2);
- assert(lit_neg(lits[1]) < s->size*2);
-
- //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
- //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
-
- assert(lits[0] < s->size*2);
- vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
- vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
-
- if (clause_learnt(c)){
- s->stats.learnts--;
- s->stats.learnts_literals -= clause_size(c);
- }else{
- s->stats.clauses--;
- s->stats.clauses_literals -= clause_size(c);
- }
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
- ABC_FREE(c);
-#else
- Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
-#endif
-}
-
-static lbool clause_simplify(sat_solver* s, clause* c)
-{
- lit* lits = clause_begin(c);
- lbool* values = s->assigns;
- int i;
-
- assert(sat_solver_dl(s) == 0);
-
- for (i = 0; i < clause_size(c); i++){
- lbool sig = !lit_sign(lits[i]); sig += sig - 1;
- if (values[lit_var(lits[i])] == sig)
- return l_True;
- }
- return l_False;
-}
-
-int sat_solver_simplify(sat_solver* s)
-{
- clause** reasons;
- int type;
-
- assert(sat_solver_dl(s) == 0);
-
- if (sat_solver_propagate(s) != 0)
- return false;
-
- if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
- return true;
-
- reasons = s->reasons;
- for (type = 0; type < 2; type++){
- vecp* cs = type ? &s->learnts : &s->clauses;
- clause** cls = (clause**)vecp_begin(cs);
-
- int i, j;
- for (j = i = 0; i < vecp_size(cs); i++){
- if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] &&
- clause_simplify(s,cls[i]) == l_True)
- clause_remove(s,cls[i]);
- else
- cls[j++] = cls[i];
- }
- vecp_resize(cs,j);
- }
-
- s->simpdb_assigns = s->qhead;
- // (shouldn't depend on 'stats' really, but it will do for now)
- s->simpdb_props = (int)(s->stats.clauses_literals + s->stats.learnts_literals);
-
- return true;
-}
-
-
-static int clause_cmp (const void* x, const void* y) {
- return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }
-
-void sat_solver_reducedb(sat_solver* s)
-{
- int i, j;
- double extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity
- clause** learnts = (clause**)vecp_begin(&s->learnts);
- clause** reasons = s->reasons;
-
- sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
-
- for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
- if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
- clause_remove(s,learnts[i]);
- else
- learnts[j++] = learnts[i];
- }
- for (; i < vecp_size(&s->learnts); i++){
- if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim)
- clause_remove(s,learnts[i]);
- else
- learnts[j++] = learnts[i];
- }
-
- //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j);
-
-
- vecp_resize(&s->learnts,j);
-}
-
-int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
-{
- clause * c;
- lit *i,*j;
- int maxvar;
- lbool* values;
- lit last;
-
- veci_resize( &s->temp_clause, 0 );
- for ( i = begin; i < end; i++ )
- veci_push( &s->temp_clause, *i );
- begin = veci_begin( &s->temp_clause );
- end = begin + veci_size( &s->temp_clause );
-
- if (begin == end)
- return false;
-
- //printlits(begin,end); printf("\n");
- // insertion sort
- maxvar = lit_var(*begin);
- for (i = begin + 1; i < end; i++){
- lit l = *i;
- maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
- for (j = i; j > begin && *(j-1) > l; j--)
- *j = *(j-1);
- *j = l;
- }
- sat_solver_setnvars(s,maxvar+1);
-// sat_solver_setnvars(s, lit_var(*(end-1))+1 );
-
- ///////////////////////////////////
- // add clause to internal storage
- if ( s->pStore )
- {
- int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end );
- assert( RetValue );
- }
- ///////////////////////////////////
-
- //printlits(begin,end); printf("\n");
- values = s->assigns;
-
- // delete duplicates
- last = lit_Undef;
- for (i = j = begin; i < end; i++){
- //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]));
- lbool sig = !lit_sign(*i); sig += sig - 1;
- if (*i == lit_neg(last) || sig == values[lit_var(*i)])
- return true; // tautology
- else if (*i != last && values[lit_var(*i)] == l_Undef)
- last = *j++ = *i;
- }
-// j = i;
-
- if (j == begin) // empty clause
- return false;
-
- if (j - begin == 1) // unit clause
- return sat_solver_enqueue(s,*begin,(clause*)0);
-
- // create new clause
- c = clause_create_new(s,begin,j,0);
- if ( c )
- vecp_push(&s->clauses,c);
-
-
- s->stats.clauses++;
- s->stats.clauses_literals += j - begin;
-
- return true;
-}
-
-
-double luby(double y, int x)
-{
- int size, seq;
- for (size = 1, seq = 0; size < x+1; seq++, size = 2*size + 1);
- while (size-1 != x){
- size = (size-1) >> 1;
- seq--;
- x = x % size;
- }
- return pow(y, (double)seq);
-}
-
-void luby_test()
-{
- int i;
- for ( i = 0; i < 20; i++ )
- printf( "%d ", (int)luby(2,i) );
- printf( "\n" );
-}
-
-static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT64_T nof_learnts)
-{
- int* levels = s->levels;
- double var_decay = 0.95;
- double clause_decay = 0.999;
- double random_var_freq = s->fNotUseRandom ? 0.0 : 0.02;
-
- ABC_INT64_T conflictC = 0;
- veci learnt_clause;
- int i;
-
- assert(s->root_level == sat_solver_dl(s));
-
- s->nRestarts++;
- s->stats.starts++;
-// s->var_decay = (float)(1 / var_decay ); // move this to sat_solver_new()
-// s->cla_decay = (float)(1 / clause_decay); // move this to sat_solver_new()
- veci_resize(&s->model,0);
- veci_new(&learnt_clause);
-
- // use activity factors in every even restart
- if ( (s->nRestarts & 1) && veci_size(&s->act_vars) > 0 )
-// if ( veci_size(&s->act_vars) > 0 )
- for ( i = 0; i < s->act_vars.size; i++ )
- act_var_bump_factor(s, s->act_vars.ptr[i]);
-
- // use activity factors in every restart
- if ( s->pGlobalVars && veci_size(&s->act_vars) > 0 )
- for ( i = 0; i < s->act_vars.size; i++ )
- act_var_bump_global(s, s->act_vars.ptr[i]);
-
- for (;;){
- clause* confl = sat_solver_propagate(s);
- if (confl != 0){
- // CONFLICT
- int blevel;
-
-#ifdef VERBOSEDEBUG
- printf(L_IND"**CONFLICT**\n", L_ind);
-#endif
- s->stats.conflicts++; conflictC++;
- if (sat_solver_dl(s) == s->root_level){
-#ifdef SAT_USE_ANALYZE_FINAL
- sat_solver_analyze_final(s, confl, 0);
-#endif
- veci_delete(&learnt_clause);
- return l_False;
- }
-
- veci_resize(&learnt_clause,0);
- sat_solver_analyze(s, confl, &learnt_clause);
- blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level;
- blevel = s->root_level > blevel ? s->root_level : blevel;
- sat_solver_canceluntil(s,blevel);
- sat_solver_record(s,&learnt_clause);
-#ifdef SAT_USE_ANALYZE_FINAL
-// if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0; // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions)
- if ( learnt_clause.size == 1 ) s->levels[lit_var(learnt_clause.ptr[0])] = 0;
-#endif
- act_var_decay(s);
- act_clause_decay(s);
-
- }else{
- // NO CONFLICT
- int next;
-
- if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
- // Reached bound on number of conflicts:
- s->progress_estimate = sat_solver_progress(s);
- sat_solver_canceluntil(s,s->root_level);
- veci_delete(&learnt_clause);
- return l_Undef; }
-
- if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) ||
-// (s->nInsLimit && s->stats.inspects > s->nInsLimit) )
- (s->nInsLimit && s->stats.propagations > s->nInsLimit) )
- {
- // Reached bound on number of conflicts:
- s->progress_estimate = sat_solver_progress(s);
- sat_solver_canceluntil(s,s->root_level);
- veci_delete(&learnt_clause);
- return l_Undef;
- }
-
- if (sat_solver_dl(s) == 0 && !s->fSkipSimplify)
- // Simplify the set of problem clauses:
- sat_solver_simplify(s);
-
-// if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
- // Reduce the set of learnt clauses:
-// sat_solver_reducedb(s);
-
- // New variable decision:
- s->stats.decisions++;
- next = order_select(s,(float)random_var_freq);
-
- if (next == var_Undef){
- // Model found:
- lbool* values = s->assigns;
- int i;
- veci_resize(&s->model, 0);
- for (i = 0; i < s->size; i++)
- veci_push(&s->model,(int)values[i]);
- sat_solver_canceluntil(s,s->root_level);
- veci_delete(&learnt_clause);
-
- /*
- veci apa; veci_new(&apa);
- for (i = 0; i < s->size; i++)
- veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i))));
- printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n");
- veci_delete(&apa);
- */
-
- return l_True;
- }
-
- if ( s->polarity[next] ) // positive polarity
- sat_solver_assume(s,toLit(next));
- else
- sat_solver_assume(s,lit_neg(toLit(next)));
- }
- }
-
- return l_Undef; // cannot happen
-}
-
-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)
-{
- int restart_iter = 0;
- ABC_INT64_T nof_conflicts;
- ABC_INT64_T nof_learnts = sat_solver_nclauses(s) / 3;
- lbool status = l_Undef;
- lbool* values = s->assigns;
- lit* i;
-
- ////////////////////////////////////////////////
- if ( s->fSolved )
- {
- if ( s->pStore )
- {
- int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
- assert( RetValue );
- }
- return l_False;
- }
- ////////////////////////////////////////////////
-
- // set the external limits
- s->nCalls++;
- s->nRestarts = 0;
- s->nConfLimit = 0;
- s->nInsLimit = 0;
- if ( nConfLimit )
- s->nConfLimit = s->stats.conflicts + nConfLimit;
- if ( nInsLimit )
-// s->nInsLimit = s->stats.inspects + nInsLimit;
- s->nInsLimit = s->stats.propagations + nInsLimit;
- if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) )
- s->nConfLimit = nConfLimitGlobal;
- if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) )
- s->nInsLimit = nInsLimitGlobal;
-
-#ifndef SAT_USE_ANALYZE_FINAL
-
- //printf("solve: "); printlits(begin, end); printf("\n");
- for (i = begin; i < end; i++){
- switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){
- case 1: // l_True:
- break;
- case 0: // l_Undef
- sat_solver_assume(s, *i);
- if (sat_solver_propagate(s) == NULL)
- break;
- // fallthrough
- case -1: // l_False
- sat_solver_canceluntil(s, 0);
- return l_False;
- }
- }
- s->root_level = sat_solver_dl(s);
-
-#endif
-
-/*
- // Perform assumptions:
- root_level = assumps.size();
- for (int i = 0; i < assumps.size(); i++){
- Lit p = assumps[i];
- assert(var(p) < nVars());
- if (!sat_solver_assume(p)){
- GClause r = reason[var(p)];
- if (r != GClause_NULL){
- Clause* confl;
- if (r.isLit()){
- confl = propagate_tmpbin;
- (*confl)[1] = ~p;
- (*confl)[0] = r.lit();
- }else
- confl = r.clause();
- analyzeFinal(confl, true);
- conflict.push(~p);
- }else
- conflict.clear(),
- conflict.push(~p);
- cancelUntil(0);
- return false; }
- Clause* confl = propagate();
- if (confl != NULL){
- analyzeFinal(confl), assert(conflict.size() > 0);
- cancelUntil(0);
- return false; }
- }
- assert(root_level == decisionLevel());
-*/
-
-#ifdef SAT_USE_ANALYZE_FINAL
- // Perform assumptions:
- s->root_level = end - begin;
- for ( i = begin; i < end; i++ )
- {
- lit p = *i;
- assert(lit_var(p) < s->size);
- veci_push(&s->trail_lim,s->qtail);
- if (!sat_solver_enqueue(s,p,(clause*)0))
- {
- clause * r = s->reasons[lit_var(p)];
- if (r != NULL)
- {
- clause* confl;
- if (clause_is_lit(r))
- {
- confl = s->binary;
- (clause_begin(confl))[1] = lit_neg(p);
- (clause_begin(confl))[0] = clause_read_lit(r);
- }
- else
- confl = r;
- sat_solver_analyze_final(s, confl, 1);
- veci_push(&s->conf_final, lit_neg(p));
- }
- else
- {
- veci_resize(&s->conf_final,0);
- veci_push(&s->conf_final, lit_neg(p));
- // the two lines below are a bug fix by Siert Wieringa
- if (s->levels[lit_var(p)] > 0)
- veci_push(&s->conf_final, p);
- }
- sat_solver_canceluntil(s, 0);
- return l_False;
- }
- else
- {
- clause* confl = sat_solver_propagate(s);
- if (confl != NULL){
- sat_solver_analyze_final(s, confl, 0);
- assert(s->conf_final.size > 0);
- sat_solver_canceluntil(s, 0);
- return l_False; }
- }
- }
- assert(s->root_level == sat_solver_dl(s));
-#endif
-
- s->nCalls2++;
-
- if (s->verbosity >= 1){
- printf("==================================[MINISAT]===================================\n");
- printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n");
- printf("| | Clauses Literals | Limit Clauses Literals Lit/Cl | |\n");
- printf("==============================================================================\n");
- }
-
- while (status == l_Undef){
-// int nConfs = 0;
- double Ratio = (s->stats.learnts == 0)? 0.0 :
- s->stats.learnts_literals / (double)s->stats.learnts;
- if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
- break;
-
- if (s->verbosity >= 1)
- {
- printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n",
- (double)s->stats.conflicts,
- (double)s->stats.clauses,
- (double)s->stats.clauses_literals,
- (double)nof_learnts,
- (double)s->stats.learnts,
- (double)s->stats.learnts_literals,
- Ratio,
- s->progress_estimate*100);
- fflush(stdout);
- }
- nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) );
-//printf( "%d ", (int)nof_conflicts );
-// nConfs = s->stats.conflicts;
- status = sat_solver_search(s, nof_conflicts, nof_learnts);
-// if ( status == l_True )
-// printf( "%d ", s->stats.conflicts - nConfs );
-
-// nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5;
- nof_learnts = nof_learnts * 11 / 10; //*= 1.1;
-//printf( "%d ", s->stats.conflicts );
- // quit the loop if reached an external limit
- if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
- {
-// printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
- break;
- }
-// if ( s->nInsLimit && s->stats.inspects > s->nInsLimit )
- if ( s->nInsLimit && s->stats.propagations > s->nInsLimit )
- {
-// printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
- break;
- }
- if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
- break;
- }
-//printf( "\n" );
- if (s->verbosity >= 1)
- printf("==============================================================================\n");
-
- sat_solver_canceluntil(s,0);
-
- ////////////////////////////////////////////////
- if ( status == l_False && s->pStore )
- {
- int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
- assert( RetValue );
- }
- ////////////////////////////////////////////////
- return status;
-}
-
-
-int sat_solver_nvars(sat_solver* s)
-{
- return s->size;
-}
-
-
-int sat_solver_nclauses(sat_solver* s)
-{
- return vecp_size(&s->clauses);
-}
-
-
-int sat_solver_nconflicts(sat_solver* s)
-{
- return (int)s->stats.conflicts;
-}
-
-//=================================================================================================
-// Clause storage functions:
-
-void sat_solver_store_alloc( sat_solver * s )
-{
- assert( s->pStore == NULL );
- s->pStore = Sto_ManAlloc();
-}
-
-void sat_solver_store_write( sat_solver * s, char * pFileName )
-{
- if ( s->pStore ) Sto_ManDumpClauses( (Sto_Man_t *)s->pStore, pFileName );
-}
-
-void sat_solver_store_free( sat_solver * s )
-{
- if ( s->pStore ) Sto_ManFree( (Sto_Man_t *)s->pStore );
- s->pStore = NULL;
-}
-
-int sat_solver_store_change_last( sat_solver * s )
-{
- if ( s->pStore ) return Sto_ManChangeLastClause( (Sto_Man_t *)s->pStore );
- return -1;
-}
-
-void sat_solver_store_mark_roots( sat_solver * s )
-{
- if ( s->pStore ) Sto_ManMarkRoots( (Sto_Man_t *)s->pStore );
-}
-
-void sat_solver_store_mark_clauses_a( sat_solver * s )
-{
- if ( s->pStore ) Sto_ManMarkClausesA( (Sto_Man_t *)s->pStore );
-}
-
-void * sat_solver_store_release( sat_solver * s )
-{
- void * pTemp;
- if ( s->pStore == NULL )
- return NULL;
- pTemp = s->pStore;
- s->pStore = NULL;
- return pTemp;
-}
-
-//=================================================================================================
-// Sorting functions (sigh):
-
-static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *))
-{
- int i, j, best_i;
- void* tmp;
-
- for (i = 0; i < size-1; i++){
- best_i = i;
- for (j = i+1; j < size; j++){
- if (comp(array[j], array[best_i]) < 0)
- best_i = j;
- }
- tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
- }
-}
-
-
-static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed)
-{
- if (size <= 15)
- selectionsort(array, size, comp);
-
- else{
- void* pivot = array[irand(seed, size)];
- void* tmp;
- int i = -1;
- int j = size;
-
- for(;;){
- do i++; while(comp(array[i], pivot)<0);
- do j--; while(comp(pivot, array[j])<0);
-
- if (i >= j) break;
-
- tmp = array[i]; array[i] = array[j]; array[j] = tmp;
- }
-
- sortrnd(array , i , comp, seed);
- sortrnd(&array[i], size-i, comp, seed);
- }
-}
-
-void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *))
-{
-// int i;
- double seed = 91648253;
- sortrnd(array,size,comp,&seed);
-// for ( i = 1; i < size; i++ )
-// assert(comp(array[i-1], array[i])<0);
-}
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/sat/bsat/satSolver_old.h b/src/sat/bsat/satSolver_old.h
deleted file mode 100644
index d2228f79..00000000
--- a/src/sat/bsat/satSolver_old.h
+++ /dev/null
@@ -1,210 +0,0 @@
-/**************************************************************************************************
-MiniSat -- Copyright (c) 2005, Niklas Sorensson
-http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
-
-Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
-associated documentation files (the "Software"), to deal in the Software without restriction,
-including without limitation the rights to use, copy, modify, merge, publish, distribute,
-sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in all copies or
-substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
-NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
-DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
-OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
-**************************************************************************************************/
-// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
-
-#ifndef ABC__sat__bsat__satSolver_old_h
-#define ABC__sat__bsat__satSolver_old_h
-
-
-#include <stdio.h>
-#include <stdlib.h>
-#include <string.h>
-#include <assert.h>
-
-#include "satVec.h"
-#include "satMem.h"
-
-ABC_NAMESPACE_HEADER_START
-
-//#define USE_FLOAT_ACTIVITY
-
-//=================================================================================================
-// Public interface:
-
-struct sat_solver_t;
-typedef struct sat_solver_t sat_solver;
-
-extern sat_solver* sat_solver_new(void);
-extern void sat_solver_delete(sat_solver* s);
-
-extern int sat_solver_addclause(sat_solver* s, lit* begin, lit* end);
-extern int sat_solver_simplify(sat_solver* s);
-extern 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);
-extern void sat_solver_rollback( sat_solver* s );
-
-extern int sat_solver_nvars(sat_solver* s);
-extern int sat_solver_nclauses(sat_solver* s);
-extern int sat_solver_nconflicts(sat_solver* s);
-
-extern void sat_solver_setnvars(sat_solver* s,int n);
-
-extern void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
-extern void Sat_SolverPrintStats( FILE * pFile, sat_solver * p );
-extern int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars );
-extern void Sat_SolverDoubleClauses( sat_solver * p, int iVar );
-
-// trace recording
-extern void Sat_SolverTraceStart( sat_solver * pSat, char * pName );
-extern void Sat_SolverTraceStop( sat_solver * pSat );
-extern void Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot );
-
-// clause storage
-extern void sat_solver_store_alloc( sat_solver * s );
-extern void sat_solver_store_write( sat_solver * s, char * pFileName );
-extern void sat_solver_store_free( sat_solver * s );
-extern void sat_solver_store_mark_roots( sat_solver * s );
-extern void sat_solver_store_mark_clauses_a( sat_solver * s );
-extern void * sat_solver_store_release( sat_solver * s );
-
-//=================================================================================================
-// Solver representation:
-
-struct clause_t;
-typedef struct clause_t clause;
-
-struct sat_solver_t
-{
- int size; // nof variables
- int cap; // size of varmaps
- int qhead; // Head index of queue.
- int qtail; // Tail index of queue.
-
- // clauses
- vecp clauses; // List of problem constraints. (contains: clause*)
- vecp learnts; // List of learnt clauses. (contains: clause*)
-
- // activities
-#ifdef USE_FLOAT_ACTIVITY
- double var_inc; // Amount to bump next variable with.
- double var_decay; // INVERSE decay factor for variable activity: stores 1/decay.
- float cla_inc; // Amount to bump next clause with.
- float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay.
- double* activity; // A heuristic measurement of the activity of a variable.
-#else
- int var_inc; // Amount to bump next variable with.
- int cla_inc; // Amount to bump next clause with.
- unsigned*activity; // A heuristic measurement of the activity of a variable.
-#endif
-
- vecp* wlists; //
- lbool* assigns; // Current values of variables.
- int* orderpos; // Index in variable order.
- clause** reasons; //
- int* levels; //
- lit* trail;
- char* polarity;
-
- clause* binary; // A temporary binary clause
- lbool* tags; //
- veci tagged; // (contains: var)
- veci stack; // (contains: var)
-
- veci order; // Variable order. (heap) (contains: var)
- veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int)
- veci model; // If problem is solved, this vector contains the model (contains: lbool).
- veci conf_final; // If problem is unsatisfiable (possibly under assumptions),
- // this vector represent the final conflict clause expressed in the assumptions.
-
- int root_level; // Level of first proper decision.
- int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
- int simpdb_props; // Number of propagations before next 'simplifyDB()'.
- double random_seed;
- double progress_estimate;
- int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything
-
- stats_t stats;
-
- ABC_INT64_T nConfLimit; // external limit on the number of conflicts
- ABC_INT64_T nInsLimit; // external limit on the number of implications
- int nRuntimeLimit; // external limit on runtime
-
- veci act_vars; // variables whose activity has changed
- double* factors; // the activity factors
- int nRestarts; // the number of local restarts
- int nCalls; // the number of local restarts
- int nCalls2; // the number of local restarts
-
- Sat_MmStep_t * pMem;
-
- int fSkipSimplify; // set to one to skip simplification of the clause database
- int fNotUseRandom; // do not allow random decisions with a fixed probability
-
- int * pGlobalVars; // for experiments with global vars during interpolation
- // clause store
- void * pStore;
- int fSolved;
-
- // trace recording
- FILE * pFile;
- int nClauses;
- int nRoots;
-
- veci temp_clause; // temporary storage for a CNF clause
-};
-
-static int sat_solver_var_value( sat_solver* s, int v )
-{
- assert( s->model.ptr != NULL && v < s->size );
- return (int)(s->model.ptr[v] == l_True);
-}
-static int sat_solver_var_literal( sat_solver* s, int v )
-{
- assert( s->model.ptr != NULL && v < s->size );
- return toLitCond( v, s->model.ptr[v] != l_True );
-}
-static void sat_solver_act_var_clear(sat_solver* s)
-{
- int i;
- for (i = 0; i < s->size; i++)
- s->activity[i] = 0.0;
- s->var_inc = 1.0;
-}
-static void sat_solver_compress(sat_solver* s)
-{
- if ( s->qtail != s->qhead )
- {
- int RetValue = sat_solver_simplify(s);
- assert( RetValue != 0 );
- }
-}
-
-static int sat_solver_final(sat_solver* s, int ** ppArray)
-{
- *ppArray = s->conf_final.ptr;
- return s->conf_final.size;
-}
-
-static int sat_solver_set_runtime_limit(sat_solver* s, int Limit)
-{
- int nRuntimeLimit = s->nRuntimeLimit;
- s->nRuntimeLimit = Limit;
- return nRuntimeLimit;
-}
-
-static int sat_solver_set_random(sat_solver* s, int fNotUseRandom)
-{
- int fNotUseRandomOld = s->fNotUseRandom;
- s->fNotUseRandom = fNotUseRandom;
- return fNotUseRandomOld;
-}
-
-ABC_NAMESPACE_HEADER_END
-
-#endif
diff --git a/src/sat/bsat/satTruth.c b/src/sat/bsat/satTruth.c
index 7d69f558..dc5644b3 100644
--- a/src/sat/bsat/satTruth.c
+++ b/src/sat/bsat/satTruth.c
@@ -19,7 +19,7 @@
***********************************************************************/
#include "satTruth.h"
-#include "vecRec.h"
+#include "vecSet.h"
ABC_NAMESPACE_IMPL_START
@@ -39,7 +39,7 @@ struct Tru_Man_t_
int nEntrySize; // the size of one entry in 'int'
int nTableSize; // hash table size
int * pTable; // hash table
- Vec_Rec_t * pMem; // memory for truth tables
+ Vec_Set_t * pMem; // memory for truth tables
word * pZero; // temporary truth table
int hIthVars[16]; // variable handles
int nTableLookups;
@@ -53,7 +53,7 @@ struct Tru_One_t_
word pTruth[0]; // truth table
};
-static inline Tru_One_t * Tru_ManReadOne( Tru_Man_t * p, int h ) { return h ? (Tru_One_t *)Vec_RecEntryP(p->pMem, h) : NULL; }
+static inline Tru_One_t * Tru_ManReadOne( Tru_Man_t * p, int h ) { return h ? (Tru_One_t *)Vec_SetEntry(p->pMem, h) : NULL; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -140,7 +140,7 @@ void Tru_ManResize( Tru_Man_t * p )
*pSpot = pThis->Handle;
Counter++;
}
- assert( Counter == Vec_RecEntryNum(p->pMem) );
+ assert( Counter == Vec_SetEntryNum(p->pMem) );
ABC_FREE( pTableOld );
}
@@ -163,7 +163,7 @@ int Tru_ManInsert( Tru_Man_t * p, word * pTruth )
if ( Tru_ManEqual1(pTruth, p->nWords) )
return 1;
p->nTableLookups++;
- if ( Vec_RecEntryNum(p->pMem) > 2 * p->nTableSize )
+ if ( Vec_SetEntryNum(p->pMem) > 2 * p->nTableSize )
Tru_ManResize( p );
fCompl = pTruth[0] & 1;
if ( fCompl )
@@ -172,7 +172,7 @@ int Tru_ManInsert( Tru_Man_t * p, word * pTruth )
if ( *pSpot == 0 )
{
Tru_One_t * pEntry;
- *pSpot = Vec_RecAppend( p->pMem, p->nEntrySize );
+ *pSpot = Vec_SetAppend( p->pMem, NULL, p->nEntrySize );
assert( (*pSpot & 1) == 0 );
pEntry = Tru_ManReadOne( p, *pSpot );
Tru_ManCopy( pEntry->pTruth, pTruth, p->nWords );
@@ -215,7 +215,7 @@ Tru_Man_t * Tru_ManAlloc( int nVars )
p->nEntrySize = (sizeof(Tru_One_t) + p->nWords * sizeof(word))/sizeof(int);
p->nTableSize = 8147;
p->pTable = ABC_CALLOC( int, p->nTableSize );
- p->pMem = Vec_RecAlloc();
+ p->pMem = Vec_SetAlloc();
// initialize truth tables
p->pZero = ABC_ALLOC( word, p->nWords );
for ( i = 0; i < nVars; i++ )
@@ -247,8 +247,8 @@ Tru_Man_t * Tru_ManAlloc( int nVars )
***********************************************************************/
void Tru_ManFree( Tru_Man_t * p )
{
- printf( "Lookups = %d. Entries = %d.\n", p->nTableLookups, Vec_RecEntryNum(p->pMem) );
- Vec_RecFree( p->pMem );
+ printf( "Lookups = %d. Entries = %d.\n", p->nTableLookups, Vec_SetEntryNum(p->pMem) );
+ Vec_SetFree( p->pMem );
ABC_FREE( p->pZero );
ABC_FREE( p->pTable );
ABC_FREE( p );
@@ -287,25 +287,9 @@ word * Tru_ManFunc( Tru_Man_t * p, int h )
assert( (h & 1) == 0 );
if ( h == 0 )
return p->pZero;
- assert( Vec_RecChunk(h) );
return Tru_ManReadOne( p, h )->pTruth;
}
-/**Function*************************************************************
-
- Synopsis [Returns stored truth table]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Tru_ManHandleMax( Tru_Man_t * p )
-{
- return p->pMem->hCurrent;
-}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/bsat/satTruth.h b/src/sat/bsat/satTruth.h
index 2f17b6f0..dcbf6526 100644
--- a/src/sat/bsat/satTruth.h
+++ b/src/sat/bsat/satTruth.h
@@ -77,7 +77,7 @@ extern void Tru_ManFree( Tru_Man_t * p );
extern word * Tru_ManVar( Tru_Man_t * p, int v );
extern word * Tru_ManFunc( Tru_Man_t * p, int h );
extern int Tru_ManInsert( Tru_Man_t * p, word * pTruth );
-extern int Tru_ManHandleMax( Tru_Man_t * p );
+//extern int Tru_ManHandleMax( Tru_Man_t * p );
ABC_NAMESPACE_HEADER_END
diff --git a/src/sat/bsat/vecRec.h b/src/sat/bsat/vecRec.h
deleted file mode 100644
index 82d7183d..00000000
--- a/src/sat/bsat/vecRec.h
+++ /dev/null
@@ -1,396 +0,0 @@
-/**CFile****************************************************************
-
- FileName [vecRec.h]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Resizable arrays.]
-
- Synopsis [Array of records.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: vecRec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef ABC__sat__bsat__vecRec_h
-#define ABC__sat__bsat__vecRec_h
-
-
-////////////////////////////////////////////////////////////////////////
-/// INCLUDES ///
-////////////////////////////////////////////////////////////////////////
-
-#include <stdio.h>
-
-ABC_NAMESPACE_HEADER_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// PARAMETERS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// BASIC TYPES ///
-////////////////////////////////////////////////////////////////////////
-
-// data-structure for logging entries
-// memory is allocated in 'p->Mask+1' int chunks
-// the first 'int' of each entry cannot be 0
-typedef struct Vec_Rec_t_ Vec_Rec_t;
-struct Vec_Rec_t_
-{
- int Mask; // mask for the log size
- int hCurrent; // current position
- int hShadow; // current position
- int nEntries; // total number of entries
- int nChunks; // total number of chunks
- int nChunksAlloc; // the number of allocated chunks
- int ** pChunks; // the chunks
-};
-
-////////////////////////////////////////////////////////////////////////
-/// MACRO DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-// p is vector of records
-// Size is given by the user
-// Handle is returned to the user
-// c (chunk) and s (shift) are variables used here
-#define Vec_RecForEachEntry( p, Size, Handle, c, s ) \
- for ( c = 1; c <= p->nChunks; c++ ) \
- for ( s = 0; p->pChunks[c][s] && ((Handle) = (((c)<<16)|(s))); s += Size, assert(s < p->Mask) )
-
-#define Vec_RecForEachEntryStart( p, Size, Handle, c, s, hStart ) \
- for ( c = Vec_RecChunk(hStart), s = Vec_RecShift(hStart); c <= p->nChunks; c++, s = 0 ) \
- for ( ; p->pChunks[c][s] && ((Handle) = (((c)<<16)|(s))); s += Size, assert(s < p->Mask) )
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline Vec_Rec_t * Vec_RecAlloc()
-{
- Vec_Rec_t * p;
- p = ABC_CALLOC( Vec_Rec_t, 1 );
- p->Mask = (1 << 15) - 1; // chunk size = 2^15 ints = 128 Kb
- p->hCurrent = (1 << 16);
- p->nChunks = 1;
- p->nChunksAlloc = 16;
- p->pChunks = ABC_CALLOC( int *, p->nChunksAlloc );
- p->pChunks[0] = NULL;
- p->pChunks[1] = ABC_ALLOC( int, (1 << 16) );
- p->pChunks[1][0] = 0;
- return p;
-}
-static inline void Vec_RecAlloc_( Vec_Rec_t * p )
-{
-// Vec_Rec_t * p;
-// p = ABC_CALLOC( Vec_Rec_t, 1 );
- memset( p, 0, sizeof(Vec_Rec_t) );
- p->Mask = (1 << 15) - 1; // chunk size = 2^15 ints = 128 Kb
- p->hCurrent = (1 << 16);
- p->nChunks = 1;
- p->nChunksAlloc = 16;
- p->pChunks = ABC_CALLOC( int *, p->nChunksAlloc );
- p->pChunks[0] = NULL;
- p->pChunks[1] = ABC_ALLOC( int, (1 << 16) );
- p->pChunks[1][0] = 0;
-// return p;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Vec_RecChunk( int i )
-{
- return i>>16;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Vec_RecShift( int i )
-{
- return i&0xFFFF;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Vec_RecSize( Vec_Rec_t * p )
-{
- return Vec_RecChunk(p->hCurrent) * (p->Mask + 1);
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Vec_RecEntryNum( Vec_Rec_t * p )
-{
- return p->nEntries;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Vec_RecEntry( Vec_Rec_t * p, int i )
-{
- assert( i <= p->hCurrent );
- return p->pChunks[Vec_RecChunk(i)][Vec_RecShift(i)];
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int * Vec_RecEntryP( Vec_Rec_t * p, int i )
-{
- assert( i <= p->hCurrent );
- return p->pChunks[Vec_RecChunk(i)] + Vec_RecShift(i);
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Vec_RecRestart( Vec_Rec_t * p )
-{
- p->hCurrent = (1 << 16);
- p->nChunks = 1;
- p->nEntries = 0;
- p->pChunks[1][0] = 0;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Vec_RecShrink( Vec_Rec_t * p, int h )
-{
- int i;
- assert( Vec_RecEntry(p, h) == 0 );
- for ( i = Vec_RecChunk(h)+1; i < p->nChunksAlloc; i++ )
- ABC_FREE( p->pChunks[i] );
- p->nChunks = Vec_RecChunk(h);
- p->hCurrent = h;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Vec_RecFree( Vec_Rec_t * p )
-{
- int i;
- for ( i = 0; i < p->nChunksAlloc; i++ )
- ABC_FREE( p->pChunks[i] );
- ABC_FREE( p->pChunks );
- ABC_FREE( p );
-}
-static inline void Vec_RecFree_( Vec_Rec_t * p )
-{
- int i;
- for ( i = 0; i < p->nChunksAlloc; i++ )
- ABC_FREE( p->pChunks[i] );
- ABC_FREE( p->pChunks );
-// ABC_FREE( p );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Vec_RecAppend( Vec_Rec_t * p, int nSize )
-{
- assert( nSize <= p->Mask );
- assert( Vec_RecEntry(p, p->hCurrent) == 0 );
- assert( Vec_RecChunk(p->hCurrent) == p->nChunks );
- if ( Vec_RecShift(p->hCurrent) + nSize >= p->Mask )
- {
- if ( ++p->nChunks == p->nChunksAlloc )
- {
- p->pChunks = ABC_REALLOC( int *, p->pChunks, p->nChunksAlloc * 2 );
- memset( p->pChunks + p->nChunksAlloc, 0, sizeof(int *) * p->nChunksAlloc );
- p->nChunksAlloc *= 2;
- }
- if ( p->pChunks[p->nChunks] == NULL )
- p->pChunks[p->nChunks] = ABC_ALLOC( int, (p->Mask + 1) );
- p->pChunks[p->nChunks][0] = 0;
- p->hCurrent = p->nChunks << 16;
- }
- p->hCurrent += nSize;
- *Vec_RecEntryP(p, p->hCurrent) = 0;
- p->nEntries++;
- return p->hCurrent - nSize;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Vec_RecPush( Vec_Rec_t * p, int * pArray, int nSize )
-{
- int Handle = Vec_RecAppend( p, nSize );
- memmove( Vec_RecEntryP(p, Handle), pArray, sizeof(int) * nSize );
- return Handle;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Vec_RecSetShadow( Vec_Rec_t * p, int hShadow )
-{
- p->hShadow = hShadow;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Vec_RecReadShadow( Vec_Rec_t * p )
-{
- return p->hShadow;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Vec_RecAppendShadow( Vec_Rec_t * p, int nSize )
-{
- if ( Vec_RecShift(p->hShadow) + nSize >= p->Mask )
- p->hShadow = ((Vec_RecChunk(p->hShadow) + 1) << 16);
- p->hShadow += nSize;
- return p->hShadow - nSize;
-}
-
-
-ABC_NAMESPACE_HEADER_END
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/sat/bsat/vecSet.h b/src/sat/bsat/vecSet.h
new file mode 100644
index 00000000..e95c3332
--- /dev/null
+++ b/src/sat/bsat/vecSet.h
@@ -0,0 +1,247 @@
+/**CFile****************************************************************
+
+ FileName [vecSet.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT solvers.]
+
+ Synopsis [Multi-page dynamic array.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: vecSet.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__sat__bsat__vecSet_h
+#define ABC__sat__bsat__vecSet_h
+
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+// data-structure for logging entries
+// memory is allocated in 2^16 word-sized pages
+// the first 'word' of each page is used storing additional data
+// the first 'int' of additional data stores the word limit
+// the second 'int' of the additional data stores the shadow word limit
+
+typedef struct Vec_Set_t_ Vec_Set_t;
+struct Vec_Set_t_
+{
+ int nEntries; // entry count
+ int iPage; // current page
+ int iPageS; // shadow page
+ int nPagesAlloc; // page count allocated
+ word ** pPages; // page pointers
+};
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int Vec_SetHandPage( int h ) { return h >> 16; }
+static inline int Vec_SetHandShift( int h ) { return h & 0xFFFF; }
+
+static inline word * Vec_SetEntry( Vec_Set_t * p, int h ) { return p->pPages[Vec_SetHandPage(h)] + Vec_SetHandShift(h); }
+static inline int Vec_SetEntryNum( Vec_Set_t * p ) { return p->nEntries; }
+static inline void Vec_SetWriteEntryNum( Vec_Set_t * p, int i){ p->nEntries = i; }
+
+static inline int Vec_SetLimit( word * p ) { return ((int*)p)[0]; }
+static inline int Vec_SetLimitS( word * p ) { return ((int*)p)[1]; }
+
+static inline int Vec_SetIncLimit( word * p, int nWords ) { return ((int*)p)[0] += nWords; }
+static inline int Vec_SetIncLimitS( word * p, int nWords ) { return ((int*)p)[1] += nWords; }
+
+static inline void Vec_SetWriteLimit( word * p, int nWords ) { ((int*)p)[0] = nWords; }
+static inline void Vec_SetWriteLimitS( word * p, int nWords ) { ((int*)p)[1] = nWords; }
+
+static inline int Vec_SetHandCurrent( Vec_Set_t * p ) { return (p->iPage << 16) + Vec_SetLimit(p->pPages[p->iPage]); }
+static inline int Vec_SetHandCurrentS( Vec_Set_t * p ) { return (p->iPageS << 16) + Vec_SetLimitS(p->pPages[p->iPageS]); }
+
+static inline int Vec_SetHandMemory( Vec_Set_t * p, int h ) { return Vec_SetHandPage(h) * 0x8FFFF + Vec_SetHandShift(h) * 8; }
+static inline int Vec_SetMemory( Vec_Set_t * p ) { return Vec_SetHandMemory(p, Vec_SetHandCurrent(p)); }
+static inline int Vec_SetMemoryS( Vec_Set_t * p ) { return Vec_SetHandMemory(p, Vec_SetHandCurrentS(p)); }
+static inline int Vec_SetMemoryAll( Vec_Set_t * p ) { return (p->iPage+1) * 0x8FFFF; }
+
+// Type is the Set type
+// pVec is vector of set
+// nSize should be given by the user
+// pSet is the pointer to the set
+// p (page) and s (shift) are variables used here
+#define Vec_SetForEachEntry( Type, pVec, nSize, pSet, p, s ) \
+ for ( p = 0; p <= pVec->iPage; p++ ) \
+ for ( s = 1; s < Vec_SetLimit(pVec->pPages[p]) && ((pSet) = (Type)(pVec->pPages[p] + (s))); s += nSize )
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Allocating vector.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Vec_SetAlloc_( Vec_Set_t * p )
+{
+ memset( p, 0, sizeof(Vec_Set_t) );
+ p->nPagesAlloc = 256;
+ p->pPages = ABC_CALLOC( word *, p->nPagesAlloc );
+ p->pPages[0] = ABC_ALLOC( word, 0x10000 );
+ p->pPages[0][0] = ~0;
+ Vec_SetWriteLimit( p->pPages[0], 1 );
+}
+static inline Vec_Set_t * Vec_SetAlloc()
+{
+ Vec_Set_t * p;
+ p = ABC_CALLOC( Vec_Set_t, 1 );
+ Vec_SetAlloc_( p );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Resetting vector.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Vec_SetRestart( Vec_Set_t * p )
+{
+ p->nEntries = 0;
+ p->iPage = 0;
+ p->iPageS = 0;
+ p->pPages[0][0] = ~0;
+ Vec_SetWriteLimit( p->pPages[0], 1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Freeing vector.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Vec_SetFree_( Vec_Set_t * p )
+{
+ int i;
+ for ( i = 0; i < p->nPagesAlloc; i++ )
+ ABC_FREE( p->pPages[i] );
+ ABC_FREE( p->pPages );
+}
+static inline void Vec_SetFree( Vec_Set_t * p )
+{
+ Vec_SetFree_( p );
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Appending entries to vector.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize )
+{
+ int nWords = (nSize + 1) >> 1;
+ assert( nWords < 0x10000 );
+ p->nEntries++;
+ if ( Vec_SetLimit( p->pPages[p->iPage] ) + nWords > 0x10000 )
+ {
+ if ( ++p->iPage == p->nPagesAlloc )
+ {
+ p->pPages = ABC_REALLOC( word *, p->pPages, p->nPagesAlloc * 2 );
+ memset( p->pPages + p->nPagesAlloc, 0, sizeof(word *) * p->nPagesAlloc );
+ p->nPagesAlloc *= 2;
+ }
+ if ( p->pPages[p->iPage] == NULL )
+ p->pPages[p->iPage] = ABC_ALLOC( word, 0x10000 );
+ p->pPages[p->iPage][0] = ~0;
+ Vec_SetWriteLimit( p->pPages[p->iPage], 1 );
+ }
+ if ( pArray )
+ memmove( p->pPages[p->iPage] + Vec_SetLimit(p->pPages[p->iPage]), pArray, sizeof(int) * nSize );
+ Vec_SetIncLimit( p->pPages[p->iPage], nWords );
+ return Vec_SetHandCurrent(p) - nWords;
+}
+static inline int Vec_SetAppendS( Vec_Set_t * p, int nSize )
+{
+ int nWords = (nSize + 1) >> 1;
+ assert( nWords < 0x10000 );
+ if ( Vec_SetLimitS( p->pPages[p->iPageS] ) + nWords > 0x10000 )
+ Vec_SetWriteLimitS( p->pPages[++p->iPageS], 1 );
+ Vec_SetIncLimitS( p->pPages[p->iPageS], nWords );
+ return Vec_SetHandCurrentS(p) - nWords;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Shrinking vector size.]
+
+ Description []
+
+ SideEffects [This procedure does not update the number of entries.]
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Vec_SetShrink( Vec_Set_t * p, int h )
+{
+ assert( h <= Vec_SetHandCurrent(p) );
+ p->iPage = Vec_SetHandPage(h);
+ Vec_SetWriteLimit( p->pPages[p->iPage], Vec_SetHandShift(h) );
+}
+static inline void Vec_SetShrinkS( Vec_Set_t * p, int h )
+{
+ assert( h <= Vec_SetHandCurrent(p) );
+ p->iPageS = Vec_SetHandPage(h);
+ Vec_SetWriteLimitS( p->pPages[p->iPageS], Vec_SetHandShift(h) );
+}
+
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 21:01:05 +0000