Skip to content

A
abc
Commit 72404d1f by Alan Mishchenko
Options

Proof-logging in the updated solver.

parent bb96fa36
Showing with 524 additions and 391 deletions
src/sat/bsat/satProof.c
...@@ -18,7 +18,7 @@ ...@@ -18,7 +18,7 @@
***********************************************************************/ ***********************************************************************/
#include "satSolver.h" #include "satSolver2.h"
#include "vec.h" #include "vec.h"
#include "aig.h" #include "aig.h"
...@@ -33,30 +33,41 @@ ABC_NAMESPACE_IMPL_START ...@@ -33,30 +33,41 @@ ABC_NAMESPACE_IMPL_START
Label is initialized to 0. Label is initialized to 0.
Root clauses are 1-based. They are marked by prepending bit 1; Root clauses are 1-based. They are marked by prepending bit 1;
*/ */
/*
typedef struct satset_t satset;
struct satset_t
{
unsigned learnt : 1;
unsigned mark : 1;
unsigned partA : 1;
unsigned nEnts : 29;
int Id;
lit pEnts[0];
};
#define satset_foreach_entry( p, c, h, s ) \
for ( h = s; (h < veci_size(p)) && (((c) = satset_read(p, h)), 1); h += satset_size(c->nEnts) )
*/
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
typedef struct Sat_Set_t_ Sat_Set_t; static inline satset* Proof_NodeRead (Vec_Int_t* p, cla h ) { return satset_read( (veci*)p, h ); }
struct Sat_Set_t_ 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 ); }
int nEnts; static inline int Proof_NodeSize (int nEnts) { return sizeof(satset)/4 + nEnts; }
int Label;
int pEnts[0];
};
static inline int Sat_SetCheck( Vec_Int_t * p, Sat_Set_t * pNode ) { return (int *)pNode > Vec_IntArray(p) && (int *)pNode < Vec_IntLimit(p); } #define Proof_ForeachNode( p, pNode, hNode ) \
static inline int Sat_SetId( Vec_Int_t * p, Sat_Set_t * pNode ) { return (int *)pNode - Vec_IntArray(p); } satset_foreach_entry( ((veci*)p), pNode, hNode, 1 )
static inline Sat_Set_t * Sat_SetFromId( Vec_Int_t * p, int i ) { return (Sat_Set_t *)(Vec_IntArray(p) + i); } #define Proof_ForeachNodeVec( pVec, p, pNode, i ) \
static inline int Sat_SetSize( Sat_Set_t * pNode ) { return pNode->nEnts + 2; } for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_NodeRead(p, Vec_IntEntry(pVec,i))); i++ )
#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] >> 1))), 1); i++ )
#define Proof_NodeForeachFanin2( p, pNode, pFanin, iFanin, i ) \
for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = ((pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(p, pNode->pEnts[i] >> 1))), ((iFanin) = ((pNode->pEnts[i] & 1) ? pNode->pEnts[i] >> 1 : 0)), 1); i++ )
#define Sat_PoolForEachSet( p, pNode, i ) \
for ( i = 1; (i < Vec_IntSize(p)) && ((pNode) = Sat_SetFromId(p, Vec_IntEntry(p,i))); i += Sat_SetSize(pNode) )
#define Sat_SetForEachSet( p, pSet, pNode, i ) \
for ( i = 0; (i < pSet->nEnts) && (((pNode) = ((pSet->pEnts[i] & 1) ? NULL : Sat_SetFromId(p, pSet->pEnts[i]))), 1); i++ )
#define Sat_VecForEachSet( pVec, p, pNode, i ) \
for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Sat_SetFromId(p, Vec_IntEntry(pVec,i))); i++ )
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
...@@ -64,7 +75,7 @@ static inline int Sat_SetSize( Sat_Set_t * pNode ) { re ...@@ -64,7 +75,7 @@ static inline int Sat_SetSize( Sat_Set_t * pNode ) { re
/**Function************************************************************* /**Function*************************************************************
Synopsis [Recursively visits useful proof nodes.] Synopsis [Collects all resolution nodes belonging to the proof.]
Description [] Description []
...@@ -73,48 +84,20 @@ static inline int Sat_SetSize( Sat_Set_t * pNode ) { re ...@@ -73,48 +84,20 @@ static inline int Sat_SetSize( Sat_Set_t * pNode ) { re
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Sat_ProofReduceOne( Vec_Int_t * p, Sat_Set_t * pNode, int * pnSize, Vec_Int_t * vStack ) Vec_Int_t * Proof_CollectAll( Vec_Int_t * p )
{ {
Sat_Set_t * pNext; Vec_Int_t * vUsed;
int i, NodeId; satset * pNode;
if ( pNode->Label ) int hNode;
return pNode->Label; vUsed = Vec_IntAlloc( 1000 );
// start with node Proof_ForeachNode( p, pNode, hNode )
pNode->Label = 1; Vec_IntPush( vUsed, hNode );
Vec_IntPush( vStack, Sat_SetId(p, pNode) ); return vUsed;
// perform DFS search
while ( Vec_IntSize(vStack) )
{
NodeId = Vec_IntPop( vStack );
if ( NodeId & 1 ) // extrated second time
{
pNode = Sat_SetFromId( p, NodeId ^ 1 );
pNode->Label = *pnSize;
*pnSize += Sat_SetSize(pNode);
// update fanins
Sat_SetForEachSet( p, pNode, pNext, i )
if ( pNext )
pNode->pEnts[i] = pNext->Label;
continue;
}
// extracted first time
// add second time
Vec_IntPush( vStack, NodeId ^ 1 );
// add its anticedents
pNode = Sat_SetFromId( p, NodeId );
Sat_SetForEachSet( p, pNode, pNext, i )
if ( pNext && !pNext->Label )
{
pNext->Label = 1;
Vec_IntPush( vStack, Sat_SetId(p, pNode) ); // add first time
}
}
return pNode->Label;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Recursively visits useful proof nodes.] Synopsis [Cleans collected resultion nodes belonging to the proof.]
Description [] Description []
...@@ -123,63 +106,55 @@ int Sat_ProofReduceOne( Vec_Int_t * p, Sat_Set_t * pNode, int * pnSize, Vec_Int_ ...@@ -123,63 +106,55 @@ int Sat_ProofReduceOne( Vec_Int_t * p, Sat_Set_t * pNode, int * pnSize, Vec_Int_
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
/* void Proof_CleanCollected( Vec_Int_t * vProof, Vec_Int_t * vUsed )
int Sat_ProofReduce_rec( Vec_Int_t * p, Sat_Set_t * pNode, int * pnSize )
{ {
int * pBeg; satset * pNode;
assert( Sat_SetCheck(p, pNode) ); int hNode;
if ( pNode->Label ) Proof_ForeachNodeVec( vUsed, vProof, pNode, hNode )
return pNode->Label; pNode->Id = 0;
for ( pBeg = pNode->pEnts; pBeg < pNode->pEnts + pNode->nEnts; pBeg++ )
if ( !(*pBeg & 1) )
*pBeg = Sat_ProofReduce_rec( p, Sat_SetFromId(p, *pBeg), pnSize );
pNode->Label = *pnSize;
*pnSize += Sat_SetSize(pNode);
return pNode->Label;
} }
*/
/**Function************************************************************* /**Function*************************************************************
Synopsis [Reduces the proof to contain only roots and their children.] Synopsis [Recursively visits useful proof nodes.]
Description [The result is updated proof and updated roots.] Description []
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Sat_ProofReduce( Vec_Int_t * p, Vec_Int_t * vRoots ) void Proof_CollectUsedInt( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed, Vec_Int_t * vStack )
{ {
int i, nSize = 1; satset * pNext;
int * pBeg, * pEnd, * pNew; int i, hNode;
Vec_Int_t * vStack; if ( pNode->Id )
Sat_Set_t * pNode; return;
// mark used nodes // start with node
vStack = Vec_IntAlloc( 1000 ); pNode->Id = 1;
Sat_VecForEachSet( vRoots, p, pNode, i ) Vec_IntPush( vStack, Proof_NodeHandle(p, pNode) << 1 );
vRoots->pArray[i] = Sat_ProofReduceOne( p, pNode, &nSize, vStack ); // perform DFS search
Vec_IntFree( vStack ); while ( Vec_IntSize(vStack) )
// compact proof
pNew = Vec_IntArray(p) + 1;
Sat_PoolForEachSet( p, pNode, i )
{ {
if ( !pNode->Label ) hNode = Vec_IntPop( vStack );
if ( hNode & 1 ) // extrated second time
{
Vec_IntPush( vUsed, hNode >> 1 );
continue; continue;
assert( pNew - Vec_IntArray(p) == pNode->Label ); }
pNode->Label = 0; // extracted first time
pBeg = (int *)pNode; Vec_IntPush( vStack, hNode ^ 1 ); // add second time
pEnd = pBeg + Sat_SetSize(pNode); // add its anticedents ;
while ( pBeg < pEnd ) pNode = Proof_NodeRead( p, hNode >> 1 );
*pNew++ = *pBeg++; Proof_NodeForeachFanin( p, pNode, pNext, i )
if ( pNext && !pNext->Id )
{
pNext->Id = 1;
Vec_IntPush( vStack, Proof_NodeHandle(p, pNext) << 1 ); // add first time
}
} }
// report the result }
printf( "The proof was reduced from %d to %d (by %6.2f %%)\n",
Vec_IntSize(p), nSize, 100.0 * (Vec_IntSize(p) - nSize) / Vec_IntSize(p) );
assert( pNew - Vec_IntArray(p) == nSize );
Vec_IntShrink( p, nSize );
}
/**Function************************************************************* /**Function*************************************************************
...@@ -192,80 +167,51 @@ void Sat_ProofReduce( Vec_Int_t * p, Vec_Int_t * vRoots ) ...@@ -192,80 +167,51 @@ void Sat_ProofReduce( Vec_Int_t * p, Vec_Int_t * vRoots )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Sat_ProofLabel( Vec_Int_t * p, Sat_Set_t * pNode, Vec_Int_t * vUsed, Vec_Int_t * vStack ) void Proof_CollectUsedRec( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed )
{ {
Sat_Set_t * pNext; satset * pNext;
int i, NodeId; int i;
if ( pNode->Label ) if ( pNode->Id )
return; return;
// start with node pNode->Id = 1;
pNode->Label = 1; Proof_NodeForeachFanin( p, pNode, pNext, i )
Vec_IntPush( vStack, Sat_SetId(p, pNode) ); if ( pNext && !pNext->Id )
// perform DFS search Proof_CollectUsedRec( p, pNext, vUsed );
while ( Vec_IntSize(vStack) ) Vec_IntPush( vUsed, Proof_NodeHandle(p, pNode) );
{
NodeId = Vec_IntPop( vStack );
if ( NodeId & 1 ) // extrated second time
{
Vec_IntPush( vUsed, NodeId ^ 1 );
continue;
}
// extracted first time
// add second time
Vec_IntPush( vStack, NodeId ^ 1 );
// add its anticedents
pNode = Sat_SetFromId( p, NodeId );
Sat_SetForEachSet( p, pNode, pNext, i )
if ( pNext && !pNext->Label )
{
pNext->Label = 1;
Vec_IntPush( vStack, Sat_SetId(p, pNode) ); // add first time
}
}
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Computes UNSAT core.] Synopsis [Recursively visits useful proof nodes.]
Description [The result is the array of root clause indexes.] Description []
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Vec_Int_t * Sat_ProofCore( Vec_Int_t * p, int nRoots, int * pBeg, int * pEnd ) Vec_Int_t * Proof_CollectUsed( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hRoot )
{ {
unsigned * pSeen; Vec_Int_t * vUsed, * vStack;
Vec_Int_t * vCore, * vUsed, * vStack; assert( (hRoot > 0) ^ (vRoots != NULL) );
Sat_Set_t * pNode;
int i;
// collect visited clauses
vUsed = Vec_IntAlloc( 1000 ); vUsed = Vec_IntAlloc( 1000 );
vStack = Vec_IntAlloc( 1000 ); vStack = Vec_IntAlloc( 1000 );
while ( pBeg < pEnd ) if ( hRoot )
Sat_ProofLabel( p, Sat_SetFromId(p, *pBeg++), vUsed, vStack ); // Proof_CollectUsedInt( vProof, Proof_NodeRead(vProof, hRoot), vUsed, vStack );
Vec_IntFree( vStack ); Proof_CollectUsedRec( vProof, Proof_NodeRead(vProof, hRoot), vUsed );
// find the core else
vCore = Vec_IntAlloc( 1000 );
pSeen = ABC_CALLOC( unsigned, Aig_BitWordNum(nRoots) );
Sat_VecForEachSet( vUsed, p, pNode, i )
{ {
pNode->Label = 0; satset * pNode;
for ( pBeg = pNode->pEnts; pBeg < pNode->pEnts + pNode->nEnts; pBeg++ ) int i;
if ( (*pBeg & 1) && !Aig_InfoHasBit(pBeg, *pBeg>>1) ) Proof_ForeachNodeVec( vRoots, vProof, pNode, i )
{ // Proof_CollectUsedInt( vProof, pNode, vUsed, vStack );
Aig_InfoSetBit( pBeg, *pBeg>>1 ); Proof_CollectUsedRec( vProof, pNode, vUsed );
Vec_IntPush( vCore, (*pBeg>>1)-1 );
}
} }
Vec_IntFree( vUsed ); Vec_IntFree( vStack );
ABC_FREE( pSeen ); return vUsed;
return vCore;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Performs one resultion step.] Synopsis [Performs one resultion step.]
...@@ -277,12 +223,14 @@ Vec_Int_t * Sat_ProofCore( Vec_Int_t * p, int nRoots, int * pBeg, int * pEnd ) ...@@ -277,12 +223,14 @@ Vec_Int_t * Sat_ProofCore( Vec_Int_t * p, int nRoots, int * pBeg, int * pEnd )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 ) satset * Proof_ResolveOne( Vec_Int_t * p, satset * c1, satset * c2 )
{ {
satset * c;
int i, k, Id, Var = -1, Count = 0; int i, k, Id, Var = -1, Count = 0;
// find resolution variable // find resolution variable
for ( i = 0; i < c1->nEnts; i++ ) for ( i = 0; i < (int)c1->nEnts; i++ )
for ( k = 0; k < c2->nEnts; k++ ) for ( k = 0; k < (int)c2->nEnts; k++ )
if ( (c1->pEnts[i] ^ c2->pEnts[k]) == 1 ) if ( (c1->pEnts[i] ^ c2->pEnts[k]) == 1 )
{ {
Var = (c1->pEnts[i] >> 1); Var = (c1->pEnts[i] >> 1);
...@@ -302,7 +250,7 @@ Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 ) ...@@ -302,7 +250,7 @@ Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 )
Id = Vec_IntSize( p ); Id = Vec_IntSize( p );
Vec_IntPush( p, 0 ); // placeholder Vec_IntPush( p, 0 ); // placeholder
Vec_IntPush( p, 0 ); Vec_IntPush( p, 0 );
for ( i = 0; i < c1->nEnts; i++ ) for ( i = 0; i < (int)c1->nEnts; i++ )
{ {
if ( (c1->pEnts[i] >> 1) == Var ) if ( (c1->pEnts[i] >> 1) == Var )
continue; continue;
...@@ -312,7 +260,7 @@ Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 ) ...@@ -312,7 +260,7 @@ Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 )
if ( k == Vec_IntSize(p) ) if ( k == Vec_IntSize(p) )
Vec_IntPush( p, c1->pEnts[i] ); Vec_IntPush( p, c1->pEnts[i] );
} }
for ( i = 0; i < c2->nEnts; i++ ) for ( i = 0; i < (int)c2->nEnts; i++ )
{ {
if ( (c2->pEnts[i] >> 1) == Var ) if ( (c2->pEnts[i] >> 1) == Var )
continue; continue;
...@@ -322,8 +270,9 @@ Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 ) ...@@ -322,8 +270,9 @@ Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 )
if ( k == Vec_IntSize(p) ) if ( k == Vec_IntSize(p) )
Vec_IntPush( p, c2->pEnts[i] ); Vec_IntPush( p, c2->pEnts[i] );
} }
Vec_IntWriteEntry( p, Id, Vec_IntSize(p) - Id - 2 ); c = Proof_NodeRead( p, Id );
return Sat_SetFromId( p, Id ); c->nEnts = Vec_IntSize(p) - Id - 2;
return c;
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -337,13 +286,15 @@ Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 ) ...@@ -337,13 +286,15 @@ Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Sat_Set_t * Sat_ProofCheckGetOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vResolves, int iAnt ) satset * Proof_CheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vResolves, int iAnt )
{ {
Sat_Set_t * pAnt; satset * pAnt;
if ( iAnt & 1 ) if ( iAnt & 1 )
return Sat_SetFromId( vClauses, iAnt >> 1 ); return Proof_NodeRead( vClauses, iAnt >> 1 );
pAnt = Sat_SetFromId( vProof, iAnt ); assert( iAnt > 0 );
return Sat_SetFromId( vResolves, pAnt->Label ); pAnt = Proof_NodeRead( vProof, iAnt >> 1 );
assert( pAnt->Id > 0 );
return Proof_NodeRead( vResolves, pAnt->Id );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -357,117 +308,247 @@ Sat_Set_t * Sat_ProofCheckGetOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_ ...@@ -357,117 +308,247 @@ Sat_Set_t * Sat_ProofCheckGetOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Sat_ProofCheck( Vec_Int_t * vClauses, Vec_Int_t * vProof, int iRoot ) void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot )
{ {
Vec_Int_t * vOrigs, * vStack, * vUsed, * vResolves; Vec_Int_t * vUsed, * vResolves;
Sat_Set_t * pSet, * pSet0, * pSet1; satset * pSet, * pSet0, * pSet1;
int i, k; int i, k, Counter = 0;
// collect original clauses
vOrigs = Vec_IntAlloc( 1000 );
Vec_IntPush( vOrigs, -1 );
Sat_PoolForEachSet( vClauses, pSet, i )
Vec_IntPush( vOrigs, Sat_SetId(vClauses, pSet) );
// collect visited clauses // collect visited clauses
vUsed = Vec_IntAlloc( 1000 ); vUsed = Proof_CollectUsed( vProof, NULL, hRoot );
vStack = Vec_IntAlloc( 1000 ); Proof_CleanCollected( vProof, vUsed );
Sat_ProofLabel( vProof, Sat_SetFromId(vProof, iRoot), vUsed, vStack );
Vec_IntFree( vStack );
// perform resolution steps // perform resolution steps
vResolves = Vec_IntAlloc( 1000 ); vResolves = Vec_IntAlloc( 1000 );
Vec_IntPush( vResolves, -1 ); Vec_IntPush( vResolves, -1 );
Sat_VecForEachSet( vUsed, vProof, pSet, i ) Proof_ForeachNodeVec( vUsed, vProof, pSet, i )
{ {
pSet0 = Sat_ProofCheckGetOne( vOrigs, vProof, vResolves, pSet->pEnts[0] ); pSet0 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] );
for ( k = 1; k < pSet->nEnts; k++ ) for ( k = 1; k < (int)pSet->nEnts; k++ )
{ {
pSet1 = Sat_ProofCheckGetOne( vOrigs, vProof, vResolves, pSet->pEnts[k] ); pSet1 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] );
pSet0 = Sat_ProofResolve( vResolves, pSet0, pSet1 ); pSet0 = Proof_ResolveOne( vResolves, pSet0, pSet1 );
} }
pSet->Label = Sat_SetId( vResolves, pSet0 ); pSet->Id = Proof_NodeHandle( vResolves, pSet0 );
Counter++;
} }
// clean the proof // clean the proof
Sat_VecForEachSet( vUsed, vProof, pSet, i ) Proof_ForeachNodeVec( vUsed, vProof, pSet, i )
pSet->Label = 0; pSet->Id = 0;
// compare the final clause // compare the final clause
if ( pSet0->nEnts > 0 ) if ( pSet0->nEnts > 0 )
printf( "Cound not derive the empty clause\n" ); printf( "Cound not derive the empty clause\n" );
Vec_IntFree( vResolves ); Vec_IntFree( vResolves );
Vec_IntFree( vUsed ); Vec_IntFree( vUsed );
Vec_IntFree( vOrigs );
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Creates variable map.] Synopsis [Recursively visits useful proof nodes.]
Description [1=A, 2=B, neg=global] Description []
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Sat_ProofVarMapCheck( Vec_Int_t * vClauses, Vec_Int_t * vVarMap ) int Sat_ProofReduceOne( Vec_Int_t * p, satset * pNode, int * pnSize, Vec_Int_t * vStack )
{ {
Sat_Set_t * pSet; satset * pNext;
int i, k, fSeeA, fSeeB; int i, NodeId;
// make sure all clauses are either A or B if ( pNode->Id )
Sat_PoolForEachSet( vClauses, pSet, i ) return pNode->Id;
// start with node
pNode->Id = 1;
Vec_IntPush( vStack, Proof_NodeHandle(p, pNode) );
// perform DFS search
while ( Vec_IntSize(vStack) )
{ {
fSeeA = fSeeB = 0; NodeId = Vec_IntPop( vStack );
for ( k = 0; k < pSet->nEnts; k++ ) if ( NodeId & 1 ) // extrated second time
{ {
fSeeA += (Vec_IntEntry(vVarMap, pSet->pEnts[k]) == 1); pNode = Proof_NodeRead( p, NodeId ^ 1 );
fSeeB += (Vec_IntEntry(vVarMap, pSet->pEnts[k]) == 2); pNode->Id = *pnSize;
*pnSize += Proof_NodeSize(pNode->nEnts);
// update fanins
Proof_NodeForeachFanin( p, pNode, pNext, i )
if ( pNext )
pNode->pEnts[i] = pNext->Id;
continue;
} }
if ( fSeeA && fSeeB ) // extracted first time
printf( "VarMap error!\n" ); // add second time
Vec_IntPush( vStack, NodeId ^ 1 );
// add its anticedents
pNode = Proof_NodeRead( p, NodeId );
Proof_NodeForeachFanin( p, pNode, pNext, i )
if ( pNext && !pNext->Id )
{
pNext->Id = 1;
Vec_IntPush( vStack, Proof_NodeHandle(p, pNode) ); // add first time
}
}
return pNode->Id;
}
/**Function*************************************************************
Synopsis [Reduces the proof to contain only roots and their children.]
Description [The result is updated proof and updated roots.]
SideEffects []
SeeAlso []
***********************************************************************/
void Sat_ProofReduce( Vec_Int_t * p, Vec_Int_t * vRoots )
{
int i, nSize = 1;
int * pBeg, * pEnd, * pNew;
Vec_Int_t * vStack;
satset * pNode;
// mark used nodes
vStack = Vec_IntAlloc( 1000 );
Proof_ForeachNodeVec( vRoots, p, pNode, i )
vRoots->pArray[i] = Sat_ProofReduceOne( p, pNode, &nSize, vStack );
Vec_IntFree( vStack );
// compact proof
pNew = Vec_IntArray(p) + 1;
Proof_ForeachNode( p, pNode, i )
{
if ( !pNode->Id )
continue;
assert( pNew - Vec_IntArray(p) == pNode->Id );
pNode->Id = 0;
pBeg = (int *)pNode;
pEnd = pBeg + Proof_NodeSize(pNode->nEnts);
while ( pBeg < pEnd )
*pNew++ = *pBeg++;
}
// report the result
printf( "The proof was reduced from %d to %d (by %6.2f %%)\n",
Vec_IntSize(p), nSize, 100.0 * (Vec_IntSize(p) - nSize) / Vec_IntSize(p) );
assert( pNew - Vec_IntArray(p) == nSize );
Vec_IntShrink( p, nSize );
}
/**Function*************************************************************
Synopsis [Computes UNSAT core.]
Description [The result is the array of root clause indexes.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Sat_ProofCore( Vec_Int_t * vProof, int nRoots, Vec_Int_t * vRoots )
{
unsigned * pSeen;
Vec_Int_t * vCore, * vUsed;
satset * pNode;
int i, * pBeg;
// collect visited clauses
vUsed = Proof_CollectUsed( vProof, vRoots, 0 );
// find the core
vCore = Vec_IntAlloc( 1000 );
pSeen = ABC_CALLOC( unsigned, Aig_BitWordNum(nRoots) );
Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
{
pNode->Id = 0;
for ( pBeg = pNode->pEnts; pBeg < pNode->pEnts + pNode->nEnts; pBeg++ )
if ( (*pBeg & 1) && !Aig_InfoHasBit(pBeg, *pBeg>>1) )
{
Aig_InfoSetBit( pBeg, *pBeg>>1 );
Vec_IntPush( vCore, (*pBeg>>1)-1 );
}
} }
Vec_IntFree( vUsed );
ABC_FREE( pSeen );
return vCore;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Computes interpolant of the proof.] Synopsis [Computes interpolant of the proof.]
Description [Assuming that res vars are recorded, too...] Description [Aassuming that global vars and A-clauses are marked.]
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vProof, int iRoot, Vec_Int_t * vClauses, Vec_Int_t * vVarMap ) Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot, Vec_Int_t * vGlobVars )
{ {
Vec_Int_t * vOrigs, * vUsed, * vStack; Vec_Int_t * vUsed;
Aig_Man_t * pAig; Aig_Man_t * pAig;
Sat_Set_t * pSet;
int i; int i;
Sat_ProofVarMapCheck( vClauses, vVarMap );
// collect original clauses
vOrigs = Vec_IntAlloc( 1000 );
Vec_IntPush( vOrigs, -1 );
Sat_PoolForEachSet( vClauses, pSet, i )
Vec_IntPush( vOrigs, Sat_SetId(vClauses, pSet) );
// collect visited clauses // collect visited clauses
vUsed = Vec_IntAlloc( 1000 ); vUsed = Proof_CollectUsed( vProof, NULL, hRoot );
vStack = Vec_IntAlloc( 1000 );
Sat_ProofLabel( vProof, Sat_SetFromId(vProof, iRoot), vUsed, vStack );
Vec_IntFree( vStack );
// start the AIG // start the AIG
pAig = Aig_ManStart( 10000 ); pAig = Aig_ManStart( 10000 );
pAig->pName = Aig_UtilStrsav( "interpol" ); pAig->pName = Aig_UtilStrsav( "interpol" );
for ( i = 0; i < Vec_IntSize(vVarMap); i++ ) for ( i = 0; i < Vec_IntSize(vGlobVars); i++ )
if ( Vec_IntEntry(vVarMap, i) < 0 ) Aig_ObjCreatePi( pAig );
Aig_ObjCreatePi( pAig );
return pAig; return pAig;
} }
/*
Sat_ProofTest(
&s->clauses, // clauses
&s->proof_clas, // proof clauses
&s->proof_vars, // proof variables
NULL, // proof roots
veci_begin(&s->claProofs)[clause_read(s, s->iLearntLast)->Id)], // one root
&s->glob_vars ); // global variables (for interpolation)
*/
/**Function*************************************************************
Synopsis [Computes interpolant of the proof.]
Description [Aassuming that global vars and A-clauses are marked.]
SideEffects []
SeeAlso []
***********************************************************************/
void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pVars, veci * pRoots, int hRoot, veci * pGlobVars )
{
Vec_Int_t * vClauses = (Vec_Int_t *)pClauses;
Vec_Int_t * vProof = (Vec_Int_t *)pProof;
Vec_Int_t * vVars = (Vec_Int_t *)pVars;
Vec_Int_t * vRoots = (Vec_Int_t *)pRoots;
Vec_Int_t * vGlobVars = (Vec_Int_t *)pGlobVars;
Vec_Int_t * vUsed;
// int i, Entry;
// collect visited clauses
vUsed = Proof_CollectUsed( vProof, NULL, hRoot );
Proof_CleanCollected( vProof, vUsed );
// Vec_IntForEachEntry( vUsed, Entry, i )
// printf( "%d ", Entry );
// printf( "\n" );
printf( "Found %d useful resolution nodes.\n", Vec_IntSize(vUsed) );
Vec_IntFree( vUsed );
vUsed = Proof_CollectAll( vProof );
printf( "Found %d total resolution nodes.\n", Vec_IntSize(vUsed) );
Vec_IntFree( vUsed );
Proof_Check( vClauses, vProof, hRoot );
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/sat/bsat/satSolver2.c
...@@ -86,12 +86,12 @@ struct varinfo_t ...@@ -86,12 +86,12 @@ struct varinfo_t
unsigned val : 2; // variable value unsigned val : 2; // variable value
unsigned pol : 1; // last polarity unsigned pol : 1; // last polarity
unsigned glo : 1; // global variable unsigned glo : 1; // global variable
unsigned tag : 3; // conflict analysis tags unsigned tag : 4; // conflict analysis tags
unsigned lev : 25; // variable level unsigned lev : 24; // variable level
}; };
int var_is_global (sat_solver2* s, int v) { return s->vi[v].glo; } int var_is_global (sat_solver2* s, int v) { return s->vi[v].glo; }
void var_set_global(sat_solver2* s, int v, int glo) { s->vi[v].glo = glo; } void var_set_global(sat_solver2* s, int v, int glo) { s->vi[v].glo = glo; if (glo) veci_push(&s->glob_vars, v); }
static inline int var_value (sat_solver2* s, int v) { return s->vi[v].val; } static inline int var_value (sat_solver2* s, int v) { return s->vi[v].val; }
static inline int var_polar (sat_solver2* s, int v) { return s->vi[v].pol; } static inline int var_polar (sat_solver2* s, int v) { return s->vi[v].pol; }
...@@ -104,13 +104,13 @@ static inline void var_set_level (sat_solver2* s, int v, int lev) { s->vi[v ...@@ -104,13 +104,13 @@ static inline void var_set_level (sat_solver2* s, int v, int lev) { s->vi[v
// variable tags // variable tags
static inline int var_tag (sat_solver2* s, int v) { return s->vi[v].tag; } static inline int var_tag (sat_solver2* s, int v) { return s->vi[v].tag; }
static inline void var_set_tag (sat_solver2* s, int v, int tag) { static inline void var_set_tag (sat_solver2* s, int v, int tag) {
assert( tag > 0 && tag < 8 ); assert( tag > 0 && tag < 16 );
if ( s->vi[v].tag == 0 ) if ( s->vi[v].tag == 0 )
veci_push( &s->tagged, v ); veci_push( &s->tagged, v );
s->vi[v].tag = tag; s->vi[v].tag = tag;
} }
static inline void var_add_tag (sat_solver2* s, int v, int tag) { static inline void var_add_tag (sat_solver2* s, int v, int tag) {
assert( tag > 0 && tag < 8 ); assert( tag > 0 && tag < 16 );
if ( s->vi[v].tag == 0 ) if ( s->vi[v].tag == 0 )
veci_push( &s->tagged, v ); veci_push( &s->tagged, v );
s->vi[v].tag |= tag; s->vi[v].tag |= tag;
...@@ -139,44 +139,30 @@ static inline void solver2_clear_marks(sat_solver2* s) { ...@@ -139,44 +139,30 @@ static inline void solver2_clear_marks(sat_solver2* s) {
veci_resize(&s->mark_levels,0); veci_resize(&s->mark_levels,0);
} }
// other inlines
//static inline int var_reason (sat_solver2* s, int v) { return (s->reasons[v]&1) ? 0 : s->reasons[v] >> 1; }
//static inline int lit_reason (sat_solver2* s, int l) { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)] >> 1; }
static inline int var_reason (sat_solver2* s, int v) { return s->reasons[v]; }
static inline int lit_reason (sat_solver2* s, int l) { return s->reasons[lit_var(l)]; }
//================================================================================================= //=================================================================================================
// Clause datatype + minor functions: // Clause datatype + minor functions:
typedef struct satset_t satset; static inline satset* clause_read (sat_solver2* s, cla h) { return satset_read( &s->clauses, h ); }
struct satset_t static inline cla clause_handle (sat_solver2* s, satset* c) { return satset_handle( &s->clauses, c ); }
{ static inline int clause_check (sat_solver2* s, satset* c) { return satset_check( &s->clauses, c ); }
unsigned learnt : 1; static inline int clause_proofid(sat_solver2* s, satset* c) { return c->learnt ? veci_begin(&s->claProofs)[c->Id]<<1 : (clause_handle(s,c)<<1) | 1; }
unsigned mark : 1;
unsigned partA : 1; //static inline int var_reason (sat_solver2* s, int v) { return (s->reasons[v]&1) ? 0 : s->reasons[v] >> 1; }
unsigned nLits : 29; //static inline int lit_reason (sat_solver2* s, int l) { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)] >> 1; }
int Id; //static inline satset* var_unit_clause(sat_solver2* s, int v) { return (s->reasons[v]&1) ? clause_read(s, s->reasons[v] >> 1) : NULL; }
lit pLits[0]; //static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(i && !s->reasons[v]); s->reasons[v] = (i << 1) | 1; }
}; static inline int var_reason (sat_solver2* s, int v) { return s->reasons[v]; }
static inline int lit_reason (sat_solver2* s, int l) { return s->reasons[lit_var(l)]; }
static inline satset* get_clause (sat_solver2* s, int c) { return c ? (satset*)(veci_begin(&s->clauses) + c) : NULL; } static inline satset* var_unit_clause(sat_solver2* s, int v) { return clause_read(s, s->units[v]); }
static inline cla clause_id (sat_solver2* s, satset* c) { return (cla)((int *)c - veci_begin(&s->clauses)); } static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++; }
static inline int clause_size (int nLits) { return sizeof(satset)/4 + nLits; }
static inline int clause_proofid(sat_solver2* s, satset* c) { return c->learnt ? veci_begin(&s->claProofs)[c->Id]<<1 : (clause_id(s,c)<<1) | 1; }
// these two only work after creating a clause before the solver is called // these two only work after creating a clause before the solver is called
int clause_is_partA (sat_solver2* s, int cid) { return get_clause(s, cid)->partA; } int clause_is_partA (sat_solver2* s, int h) { return clause_read(s, h)->partA; }
void clause_set_partA(sat_solver2* s, int cid, int partA) { get_clause(s, cid)->partA = partA; } void clause_set_partA(sat_solver2* s, int h, int partA) { clause_read(s, h)->partA = partA; }
int clause_id(sat_solver2* s, int h) { return clause_read(s, h)->Id; }
//static inline satset* var_unit_clause(sat_solver2* s, int v) { return (s->reasons[v]&1) ? get_clause(s, s->reasons[v] >> 1) : NULL; }
//static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(i && !s->reasons[v]); s->reasons[v] = (i << 1) | 1; }
static inline satset* var_unit_clause(sat_solver2* s, int v) { return get_clause(s, s->units[v]); }
static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++; }
#define sat_solver_foreach_clause( s, c, i ) \ #define sat_solver_foreach_clause( s, c, h ) satset_foreach_entry( &s->clauses, c, h, 1 )
for ( i = 1; (i < s->nMemSize) && (((c) = get_clause(s, i)), 1); i += clause_size(c->nLits) ) #define sat_solver_foreach_learnt( s, c, h ) satset_foreach_entry( &s->clauses, c, h, s->iLearntFirst )
#define sat_solver_foreach_learnt( s, c, i ) \
for ( i = s->iFirstLearnt; (i < s->nMemSize) && (((c) = get_clause(s, i)), 1); i += clause_size(c->nLits) )
//================================================================================================= //=================================================================================================
// Simple helpers: // Simple helpers:
...@@ -219,7 +205,7 @@ static inline int proof_chain_stop( sat_solver2* s ) ...@@ -219,7 +205,7 @@ static inline int proof_chain_stop( sat_solver2* s )
int RetValue = s->iStartChain; int RetValue = s->iStartChain;
satset* c = (satset*)(veci_begin(&s->proof_clas) + s->iStartChain); satset* c = (satset*)(veci_begin(&s->proof_clas) + s->iStartChain);
assert( s->iStartChain > 0 && s->iStartChain < veci_size(&s->proof_clas) ); assert( s->iStartChain > 0 && s->iStartChain < veci_size(&s->proof_clas) );
c->nLits = veci_size(&s->proof_clas) - s->iStartChain - 2; c->nEnts = veci_size(&s->proof_clas) - s->iStartChain - 2;
s->iStartChain = 0; s->iStartChain = 0;
return RetValue; return RetValue;
} }
...@@ -396,11 +382,11 @@ static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proo ...@@ -396,11 +382,11 @@ static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proo
assert(nLits < 1 || lit_var(begin[0]) < s->size); assert(nLits < 1 || lit_var(begin[0]) < s->size);
assert(nLits < 2 || lit_var(begin[1]) < s->size); assert(nLits < 2 || lit_var(begin[1]) < s->size);
// add memory if needed // add memory if needed
if ( veci_size(&s->clauses) + clause_size(nLits) > s->clauses.cap ) if ( veci_size(&s->clauses) + satset_size(nLits) > s->clauses.cap )
{ {
int nMemAlloc = s->clauses.cap ? 2 * s->clauses.cap : (1 << 20); int nMemAlloc = s->clauses.cap ? 2 * s->clauses.cap : (1 << 20);
s->clauses.ptr = ABC_REALLOC( int, veci_begin(&s->clauses), nMemAlloc ); s->clauses.ptr = ABC_REALLOC( int, veci_begin(&s->clauses), nMemAlloc );
memset( veci_begin(&s->clauses) + s->clauses.cap, 0, sizeof(int) * (nMemAlloc - s->clauses.cap) ); // memset( veci_begin(&s->clauses) + s->clauses.cap, 0, sizeof(int) * (nMemAlloc - s->clauses.cap) );
// printf( "Reallocing from %d to %d...\n", s->clauses.cap, nMemAlloc ); // printf( "Reallocing from %d to %d...\n", s->clauses.cap, nMemAlloc );
s->clauses.cap = nMemAlloc; s->clauses.cap = nMemAlloc;
if ( veci_size(&s->clauses) == 0 ) if ( veci_size(&s->clauses) == 0 )
...@@ -408,10 +394,11 @@ static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proo ...@@ -408,10 +394,11 @@ static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proo
} }
// create clause // create clause
c = (satset*)(veci_begin(&s->clauses) + veci_size(&s->clauses)); c = (satset*)(veci_begin(&s->clauses) + veci_size(&s->clauses));
((int*)c)[0] = 0;
c->learnt = learnt; c->learnt = learnt;
c->nLits = nLits; c->nEnts = nLits;
for (i = 0; i < nLits; i++) for (i = 0; i < nLits; i++)
c->pLits[i] = begin[i]; c->pEnts[i] = begin[i];
// assign clause ID // assign clause ID
if ( learnt ) if ( learnt )
{ {
...@@ -434,14 +421,14 @@ static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proo ...@@ -434,14 +421,14 @@ static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proo
// extend storage // extend storage
Cid = veci_size(&s->clauses); Cid = veci_size(&s->clauses);
s->clauses.size += clause_size(nLits); s->clauses.size += satset_size(nLits);
assert( veci_size(&s->clauses) <= s->clauses.cap ); assert( veci_size(&s->clauses) <= s->clauses.cap );
assert(((ABC_PTRUINT_T)c & 3) == 0); assert(((ABC_PTRUINT_T)c & 3) == 0);
// remember the last one and first learnt // remember the last one and first learnt
s->fLastConfId = Cid; s->iLearntLast = Cid;
if ( learnt && s->iFirstLearnt == -1 ) if ( learnt && s->iLearntFirst == -1 )
s->iFirstLearnt = Cid; s->iLearntFirst = Cid;
// watch the clause // watch the clause
if ( nLits > 1 ){ if ( nLits > 1 ){
...@@ -614,9 +601,9 @@ static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first) ...@@ -614,9 +601,9 @@ static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first)
return -1; return -1;
proof_chain_start( s, conf ); proof_chain_start( s, conf );
assert( veci_size(&s->tagged) == 0 ); assert( veci_size(&s->tagged) == 0 );
for ( i = skip_first; i < (int)conf->nLits; i++ ) for ( i = skip_first; i < (int)conf->nEnts; i++ )
{ {
x = lit_var(conf->pLits[i]); x = lit_var(conf->pEnts[i]);
if ( var_level(s,x) ) if ( var_level(s,x) )
var_set_tag(s, x, 1); var_set_tag(s, x, 1);
else else
...@@ -627,11 +614,11 @@ static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first) ...@@ -627,11 +614,11 @@ static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first)
for (i = s->qtail-1; i >= (veci_begin(&s->trail_lim))[0]; i--){ for (i = s->qtail-1; i >= (veci_begin(&s->trail_lim))[0]; i--){
x = lit_var(s->trail[i]); x = lit_var(s->trail[i]);
if (var_tag(s,x)){ if (var_tag(s,x)){
satset* c = get_clause(s, var_reason(s,x)); satset* c = clause_read(s, var_reason(s,x));
if (c){ if (c){
proof_chain_resolve( s, c, x ); proof_chain_resolve( s, c, x );
for (j = 1; j < (int)c->nLits; j++) { for (j = 1; j < (int)c->nEnts; j++) {
x = lit_var(c->pLits[j]); x = lit_var(c->pEnts[j]);
if ( var_level(s,x) ) if ( var_level(s,x) )
var_set_tag(s, x, 1); var_set_tag(s, x, 1);
else else
...@@ -664,14 +651,14 @@ static int solver2_lit_removable_rec(sat_solver2* s, int v) ...@@ -664,14 +651,14 @@ static int solver2_lit_removable_rec(sat_solver2* s, int v)
return (var_tag(s,v) & 4) > 0; return (var_tag(s,v) & 4) > 0;
// skip decisions on a wrong level // skip decisions on a wrong level
c = get_clause(s, var_reason(s,v)); c = clause_read(s, var_reason(s,v));
if ( c == NULL ){ if ( c == NULL ){
var_add_tag(s,v,2); var_add_tag(s,v,2);
return 0; return 0;
} }
for ( i = 1; i < (int)c->nLits; i++ ){ for ( i = 1; i < (int)c->nEnts; i++ ){
x = lit_var(c->pLits[i]); x = lit_var(c->pEnts[i]);
if (var_tag(s,x) & 1) if (var_tag(s,x) & 1)
solver2_lit_removable_rec(s, x); solver2_lit_removable_rec(s, x);
else{ else{
...@@ -715,9 +702,9 @@ static int solver2_lit_removable(sat_solver2* s, int x) ...@@ -715,9 +702,9 @@ static int solver2_lit_removable(sat_solver2* s, int x)
veci_push(&s->stack, x ^ 1 ); veci_push(&s->stack, x ^ 1 );
} }
x >>= 1; x >>= 1;
c = get_clause(s, var_reason(s,x)); c = clause_read(s, var_reason(s,x));
for (i = 1; i < (int)c->nLits; i++){ for (i = 1; i < (int)c->nEnts; i++){
x = lit_var(c->pLits[i]); x = lit_var(c->pEnts[i]);
if (var_tag(s,x) || !var_level(s,x)) if (var_tag(s,x) || !var_level(s,x))
continue; continue;
if (!var_reason(s,x) || !var_lev_mark(s,x)){ if (!var_reason(s,x) || !var_lev_mark(s,x)){
...@@ -749,11 +736,11 @@ static void solver2_logging_order(sat_solver2* s, int x) ...@@ -749,11 +736,11 @@ static void solver2_logging_order(sat_solver2* s, int x)
} }
veci_push(&s->stack, x ^ 1 ); veci_push(&s->stack, x ^ 1 );
x >>= 1; x >>= 1;
c = get_clause(s, var_reason(s,x)); c = clause_read(s, var_reason(s,x));
// if ( !c ) // if ( !c )
// printf( "solver2_logging_order(): Error in conflict analysis!!!\n" ); // printf( "solver2_logging_order(): Error in conflict analysis!!!\n" );
for (i = 1; i < (int)c->nLits; i++){ for (i = 1; i < (int)c->nEnts; i++){
x = lit_var(c->pLits[i]); x = lit_var(c->pEnts[i]);
if ( !var_level(s,x) || (var_tag(s,x) & 1) ) if ( !var_level(s,x) || (var_tag(s,x) & 1) )
continue; continue;
veci_push(&s->stack, x << 1); veci_push(&s->stack, x << 1);
...@@ -762,6 +749,22 @@ static void solver2_logging_order(sat_solver2* s, int x) ...@@ -762,6 +749,22 @@ static void solver2_logging_order(sat_solver2* s, int x)
} }
} }
static void solver2_logging_order_rec(sat_solver2* s, int x)
{
satset* c;
int i, y;
if ( (var_tag(s,x) & 8) )
return;
c = clause_read(s, var_reason(s,x));
for (i = 1; i < (int)c->nEnts; i++){
y = lit_var(c->pEnts[i]);
if ( var_level(s,y) && (var_tag(s,y) & 1) == 0 )
solver2_logging_order_rec(s, y);
}
var_add_tag(s, x, 8);
veci_push(&s->min_step_order, x);
}
static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt) static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
{ {
int cnt = 0; int cnt = 0;
...@@ -780,8 +783,8 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt) ...@@ -780,8 +783,8 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
assert(c != 0); assert(c != 0);
if (c->learnt) if (c->learnt)
act_clause_bump(s,c); act_clause_bump(s,c);
for ( j = (int)(p != lit_Undef); j < (int)c->nLits; j++){ for ( j = (int)(p != lit_Undef); j < (int)c->nEnts; j++){
x = lit_var(c->pLits[j]); x = lit_var(c->pEnts[j]);
assert(x >= 0 && x < s->size); assert(x >= 0 && x < s->size);
if ( var_tag(s, x) ) if ( var_tag(s, x) )
continue; continue;
...@@ -795,13 +798,13 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt) ...@@ -795,13 +798,13 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
if (var_level(s,x) == solver2_dlevel(s)) if (var_level(s,x) == solver2_dlevel(s))
cnt++; cnt++;
else else
veci_push(learnt,c->pLits[j]); veci_push(learnt,c->pEnts[j]);
} }
while (!var_tag(s, lit_var(s->trail[ind--]))); while (!var_tag(s, lit_var(s->trail[ind--])));
p = s->trail[ind+1]; p = s->trail[ind+1];
c = get_clause(s, lit_reason(s,p)); c = clause_read(s, lit_reason(s,p));
cnt--; cnt--;
if ( cnt == 0 ) if ( cnt == 0 )
break; break;
...@@ -818,8 +821,8 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt) ...@@ -818,8 +821,8 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
// simplify (full) // simplify (full)
veci_resize(&s->min_lit_order, 0); veci_resize(&s->min_lit_order, 0);
for (i = j = 1; i < veci_size(learnt); i++){ for (i = j = 1; i < veci_size(learnt); i++){
// if (!solver2_lit_removable_rec(s,lit_var(lits[i]))) // changed to vars!!! // if (!solver2_lit_removable( s,lit_var(lits[i])) )
if (!solver2_lit_removable( s,lit_var(lits[i])) ) if (!solver2_lit_removable_rec(s,lit_var(lits[i]))) // changed to vars!!!
lits[j++] = lits[i]; lits[j++] = lits[i];
} }
...@@ -830,16 +833,17 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt) ...@@ -830,16 +833,17 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
veci_resize(&s->min_step_order, 0); veci_resize(&s->min_step_order, 0);
vars = veci_begin(&s->min_lit_order); vars = veci_begin(&s->min_lit_order);
for (i = 0; i < veci_size(&s->min_lit_order); i++) for (i = 0; i < veci_size(&s->min_lit_order); i++)
solver2_logging_order( s, vars[i] ); // solver2_logging_order( s, vars[i] );
solver2_logging_order_rec( s, vars[i] );
// add them in the reverse order // add them in the reverse order
vars = veci_begin(&s->min_step_order); vars = veci_begin(&s->min_step_order);
for (i = veci_size(&s->min_step_order); i > 0; ) { i--; for (i = veci_size(&s->min_step_order); i > 0; ) { i--;
c = get_clause(s, var_reason(s,vars[i])); c = clause_read(s, var_reason(s,vars[i]));
proof_chain_resolve( s, c, vars[i] ); proof_chain_resolve( s, c, vars[i] );
for ( k = 1; k < (int)c->nLits; k++ ) for ( k = 1; k < (int)c->nEnts; k++ )
{ {
x = lit_var(c->pLits[k]); x = lit_var(c->pEnts[k]);
if ( var_level(s,x) == 0 ) if ( var_level(s,x) == 0 )
proof_chain_resolve( s, NULL, x ); proof_chain_resolve( s, NULL, x );
} }
...@@ -908,8 +912,8 @@ satset* solver2_propagate(sat_solver2* s) ...@@ -908,8 +912,8 @@ satset* solver2_propagate(sat_solver2* s)
s->simpdb_props--; s->simpdb_props--;
for (i = j = begin; i < end; ){ for (i = j = begin; i < end; ){
c = get_clause(s,*i); c = clause_read(s,*i);
lits = c->pLits; lits = c->pEnts;
// Make sure the false literal is data[1]: // Make sure the false literal is data[1]:
false_lit = lit_neg(p); false_lit = lit_neg(p);
...@@ -924,7 +928,7 @@ satset* solver2_propagate(sat_solver2* s) ...@@ -924,7 +928,7 @@ satset* solver2_propagate(sat_solver2* s)
*j++ = *i; *j++ = *i;
else{ else{
// Look for new watch: // Look for new watch:
stop = lits + c->nLits; stop = lits + c->nEnts;
for (k = lits + 2; k < stop; k++){ for (k = lits + 2; k < stop; k++){
if (var_value(s, lit_var(*k)) != !lit_sign(*k)){ if (var_value(s, lit_var(*k)) != !lit_sign(*k)){
lits[1] = *k; lits[1] = *k;
...@@ -939,9 +943,9 @@ satset* solver2_propagate(sat_solver2* s) ...@@ -939,9 +943,9 @@ satset* solver2_propagate(sat_solver2* s)
int fLitIsFalse = (var_value(s, Var) == !lit_sign(lits[0])); int fLitIsFalse = (var_value(s, Var) == !lit_sign(lits[0]));
// Log production of top-level unit clause: // Log production of top-level unit clause:
proof_chain_start( s, c ); proof_chain_start( s, c );
for ( k = 1; k < (int)c->nLits; k++ ) for ( k = 1; k < (int)c->nEnts; k++ )
{ {
int x = lit_var(c->pLits[k]); int x = lit_var(c->pEnts[k]);
assert( var_level(s, x) == 0 ); assert( var_level(s, x) == 0 );
proof_chain_resolve( s, NULL, x ); proof_chain_resolve( s, NULL, x );
} }
...@@ -955,7 +959,7 @@ satset* solver2_propagate(sat_solver2* s) ...@@ -955,7 +959,7 @@ satset* solver2_propagate(sat_solver2* s)
var_set_unit_clause(s, Var, Cid); var_set_unit_clause(s, Var, Cid);
else{ else{
// Empty clause derived: // Empty clause derived:
proof_chain_start( s, get_clause(s,Cid) ); proof_chain_start( s, clause_read(s,Cid) );
proof_chain_resolve( s, NULL, Var ); proof_chain_resolve( s, NULL, Var );
proof_id = proof_chain_stop( s ); proof_id = proof_chain_stop( s );
clause_new( s, lits, lits, 1, proof_id ); clause_new( s, lits, lits, 1, proof_id );
...@@ -965,7 +969,7 @@ satset* solver2_propagate(sat_solver2* s) ...@@ -965,7 +969,7 @@ satset* solver2_propagate(sat_solver2* s)
*j++ = *i; *j++ = *i;
// Clause is unit under assignment: // Clause is unit under assignment:
if (!solver2_enqueue(s,lits[0], *i)){ if (!solver2_enqueue(s,lits[0], *i)){
confl = get_clause(s,*i++); confl = clause_read(s,*i++);
// Copy the remaining watches: // Copy the remaining watches:
while (i < end) while (i < end)
*j++ = *i++; *j++ = *i++;
...@@ -984,18 +988,18 @@ WatchFound: i++; ...@@ -984,18 +988,18 @@ WatchFound: i++;
static void clause_remove(sat_solver2* s, satset* c) static void clause_remove(sat_solver2* s, satset* c)
{ {
assert(lit_neg(c->pLits[0]) < s->size*2); assert(lit_neg(c->pEnts[0]) < s->size*2);
assert(lit_neg(c->pLits[1]) < s->size*2); assert(lit_neg(c->pEnts[1]) < s->size*2);
veci_remove(solver2_wlist(s,lit_neg(c->pLits[0])),clause_id(s,c)); veci_remove(solver2_wlist(s,lit_neg(c->pEnts[0])),clause_handle(s,c));
veci_remove(solver2_wlist(s,lit_neg(c->pLits[1])),clause_id(s,c)); veci_remove(solver2_wlist(s,lit_neg(c->pEnts[1])),clause_handle(s,c));
if (c->learnt){ if (c->learnt){
s->stats.learnts--; s->stats.learnts--;
s->stats.learnts_literals -= c->nLits; s->stats.learnts_literals -= c->nEnts;
}else{ }else{
s->stats.clauses--; s->stats.clauses--;
s->stats.clauses_literals -= c->nLits; s->stats.clauses_literals -= c->nEnts;
} }
} }
...@@ -1004,8 +1008,8 @@ static lbool clause_simplify(sat_solver2* s, satset* c) ...@@ -1004,8 +1008,8 @@ static lbool clause_simplify(sat_solver2* s, satset* c)
{ {
int i; int i;
assert(solver2_dlevel(s) == 0); assert(solver2_dlevel(s) == 0);
for (i = 0; i < (int)c->nLits; i++){ for (i = 0; i < (int)c->nEnts; i++){
if (var_value(s, lit_var(c->pLits[i])) == lit_sign(c->pLits[i])) if (var_value(s, lit_var(c->pEnts[i])) == lit_sign(c->pEnts[i]))
return l_True; return l_True;
} }
return l_False; return l_False;
...@@ -1026,8 +1030,8 @@ int sat_solver2_simplify(sat_solver2* s) ...@@ -1026,8 +1030,8 @@ int sat_solver2_simplify(sat_solver2* s)
int* cls = (int*)veci_begin(cs); int* cls = (int*)veci_begin(cs);
int i, j; int i, j;
for (j = i = 0; i < veci_size(cs); i++){ for (j = i = 0; i < veci_size(cs); i++){
satset* c = get_clause(s,cls[i]); satset* c = clause_read(s,cls[i]);
if (lit_reason(s,c->pLits[0]) != cls[i] && if (lit_reason(s,c->pEnts[0]) != cls[i] &&
clause_simplify(s,c) == l_True) clause_simplify(s,c) == l_True)
clause_remove(s,c), Counter++; clause_remove(s,c), Counter++;
else else
...@@ -1067,7 +1071,7 @@ void solver2_reducedb(sat_solver2* s) ...@@ -1067,7 +1071,7 @@ void solver2_reducedb(sat_solver2* s)
{ {
assert( c->Id == k ); assert( c->Id == k );
c->mark = 0; c->mark = 0;
if ( c->nLits > 2 && lit_reason(s,c->pLits[0]) != Cid && (k < nLearnts/2 || pActs[k] < extra_lim) ) if ( c->nEnts > 2 && lit_reason(s,c->pEnts[0]) != Cid && (k < nLearnts/2 || pActs[k] < extra_lim) )
{ {
c->mark = 1; c->mark = 1;
Counter++; Counter++;
...@@ -1216,14 +1220,15 @@ sat_solver2* sat_solver2_new(void) ...@@ -1216,14 +1220,15 @@ sat_solver2* sat_solver2_new(void)
veci_new(&s->mark_levels); veci_new(&s->mark_levels);
veci_new(&s->min_lit_order); veci_new(&s->min_lit_order);
veci_new(&s->min_step_order); veci_new(&s->min_step_order);
veci_new(&s->glob_vars);
veci_new(&s->proof_clas); veci_push(&s->proof_clas, -1); veci_new(&s->proof_clas); veci_push(&s->proof_clas, -1);
veci_new(&s->proof_vars); veci_push(&s->proof_vars, -1); veci_new(&s->proof_vars); veci_push(&s->proof_vars, -1);
veci_new(&s->claActs); veci_push(&s->claActs, -1); veci_new(&s->claActs); veci_push(&s->claActs, -1);
veci_new(&s->claProofs); veci_push(&s->claProofs, -1); veci_new(&s->claProofs); veci_push(&s->claProofs, -1);
// initialize other // initialize other
s->iFirstLearnt = -1; // the first learnt clause s->iLearntFirst = -1; // the first learnt clause
s->fLastConfId = -1; // the last learnt clause s->iLearntLast = -1; // the last learnt clause
#ifdef USE_FLOAT_ACTIVITY #ifdef USE_FLOAT_ACTIVITY
s->var_inc = 1; s->var_inc = 1;
s->cla_inc = 1; s->cla_inc = 1;
...@@ -1245,9 +1250,9 @@ sat_solver2* sat_solver2_new(void) ...@@ -1245,9 +1250,9 @@ sat_solver2* sat_solver2_new(void)
if ( s->fProofLogging ) if ( s->fProofLogging )
{ {
s->proof_clas.cap = (1 << 20); s->proof_clas.cap = (1 << 20);
s->proof_clas.ptr = ABC_ALLOC( int, s->proof_clas.cap ); s->proof_clas.ptr = ABC_REALLOC( int, s->proof_clas.ptr, s->proof_clas.cap );
s->proof_vars.cap = (1 << 20); s->proof_vars.cap = (1 << 20);
s->proof_vars.ptr = ABC_ALLOC( int, s->proof_clas.cap ); s->proof_vars.ptr = ABC_REALLOC( int, s->proof_vars.ptr, s->proof_clas.cap );
} }
return s; return s;
} }
...@@ -1294,10 +1299,19 @@ void sat_solver2_setnvars(sat_solver2* s,int n) ...@@ -1294,10 +1299,19 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
void sat_solver2_delete(sat_solver2* s) void sat_solver2_delete(sat_solver2* s)
{ {
satset * c = clause_read(s, s->iLearntLast);
// report statistics // report statistics
assert( veci_size(&s->proof_clas) == veci_size(&s->proof_vars) ); assert( veci_size(&s->proof_clas) == veci_size(&s->proof_vars) );
printf( "Used %6.2f Mb for proof-logging. Unit clauses = %d.\n", 8.0 * veci_size(&s->proof_clas) / (1<<20), s->nUnits ); printf( "Used %6.2f Mb for proof-logging. Unit clauses = %d.\n", 8.0 * veci_size(&s->proof_clas) / (1<<20), s->nUnits );
Sat_ProofTest(
&s->clauses, // clauses
&s->proof_clas, // proof clauses
&s->proof_vars, // proof variables
NULL, // proof roots
veci_begin(&s->claProofs)[c->Id], // one root
&s->glob_vars ); // global variables (for interpolation)
// delete vectors // delete vectors
veci_delete(&s->order); veci_delete(&s->order);
veci_delete(&s->trail_lim); veci_delete(&s->trail_lim);
...@@ -1309,6 +1323,7 @@ void sat_solver2_delete(sat_solver2* s) ...@@ -1309,6 +1323,7 @@ void sat_solver2_delete(sat_solver2* s)
veci_delete(&s->mark_levels); veci_delete(&s->mark_levels);
veci_delete(&s->min_lit_order); veci_delete(&s->min_lit_order);
veci_delete(&s->min_step_order); veci_delete(&s->min_step_order);
veci_delete(&s->glob_vars);
veci_delete(&s->proof_clas); veci_delete(&s->proof_clas);
veci_delete(&s->proof_vars); veci_delete(&s->proof_vars);
veci_delete(&s->claActs); veci_delete(&s->claActs);
...@@ -1320,7 +1335,10 @@ void sat_solver2_delete(sat_solver2* s) ...@@ -1320,7 +1335,10 @@ void sat_solver2_delete(sat_solver2* s)
int i; int i;
if ( s->wlists ) if ( s->wlists )
for (i = 0; i < s->size*2; i++) for (i = 0; i < s->size*2; i++)
{
// printf( "%d ", s->wlists[i].size );
veci_delete(&s->wlists[i]); veci_delete(&s->wlists[i]);
}
ABC_FREE(s->wlists ); ABC_FREE(s->wlists );
ABC_FREE(s->vi ); ABC_FREE(s->vi );
ABC_FREE(s->trail ); ABC_FREE(s->trail );
...@@ -1461,7 +1479,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim ...@@ -1461,7 +1479,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
// lbool* values = s->assigns; // lbool* values = s->assigns;
lit* i; lit* i;
s->fLastConfId = -1; s->iLearntLast = -1;
// set the external limits // set the external limits
// s->nCalls++; // s->nCalls++;
...@@ -1542,7 +1560,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim ...@@ -1542,7 +1560,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
veci_push(&s->trail_lim,s->qtail); veci_push(&s->trail_lim,s->qtail);
if (!solver2_enqueue(s,p,0)) if (!solver2_enqueue(s,p,0))
{ {
satset* r = get_clause(s, lit_reason(s,p)); satset* r = clause_read(s, lit_reason(s,p));
if (r != NULL) if (r != NULL)
{ {
satset* confl = r; satset* confl = r;
......
src/sat/bsat/satSolver2.h
...@@ -41,39 +41,41 @@ struct sat_solver2_t; ...@@ -41,39 +41,41 @@ struct sat_solver2_t;
typedef struct sat_solver2_t sat_solver2; typedef struct sat_solver2_t sat_solver2;
extern sat_solver2* sat_solver2_new(void); extern sat_solver2* sat_solver2_new(void);
extern void sat_solver2_delete(sat_solver2* s); extern void sat_solver2_delete(sat_solver2* s);
extern int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end); extern int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end);
extern int sat_solver2_simplify(sat_solver2* s); extern int sat_solver2_simplify(sat_solver2* s);
extern int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); extern int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
extern void sat_solver2_setnvars(sat_solver2* s,int n); extern void sat_solver2_setnvars(sat_solver2* s,int n);
extern void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ); extern void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
extern void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * p ); extern void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * p );
extern int * Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars ); extern int * Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars );
extern void Sat_Solver2DoubleClauses( sat_solver2 * p, int iVar ); extern void Sat_Solver2DoubleClauses( sat_solver2 * p, int iVar );
// trace recording // trace recording
extern void sat_solver2TraceStart( sat_solver2 * pSat, char * pName ); extern void sat_solver2TraceStart( sat_solver2 * pSat, char * pName );
extern void sat_solver2TraceStop( sat_solver2 * pSat ); extern void sat_solver2TraceStop( sat_solver2 * pSat );
extern void sat_solver2TraceWrite( sat_solver2 * pSat, int * pBeg, int * pEnd, int fRoot ); extern void sat_solver2TraceWrite( sat_solver2 * pSat, int * pBeg, int * pEnd, int fRoot );
// clause storage // clause storage
extern void sat_solver2_store_alloc( sat_solver2 * s ); extern void sat_solver2_store_alloc( sat_solver2 * s );
extern void sat_solver2_store_write( sat_solver2 * s, char * pFileName ); extern void sat_solver2_store_write( sat_solver2 * s, char * pFileName );
extern void sat_solver2_store_free( sat_solver2 * s ); extern void sat_solver2_store_free( sat_solver2 * s );
extern void sat_solver2_store_mark_roots( sat_solver2 * s ); extern void sat_solver2_store_mark_roots( sat_solver2 * s );
extern void sat_solver2_store_mark_clauses_a( sat_solver2 * s ); extern void sat_solver2_store_mark_clauses_a( sat_solver2 * s );
extern void * sat_solver2_store_release( sat_solver2 * s ); extern void * sat_solver2_store_release( sat_solver2 * s );
// global variables // global variables
extern int var_is_global (sat_solver2* s, int v); extern int var_is_global (sat_solver2* s, int v);
extern void var_set_global(sat_solver2* s, int v, int glo); extern void var_set_global(sat_solver2* s, int v, int glo);
// clause grouping (these two only work after creating a clause before the solver is called) // clause grouping (these two only work after creating a clause before the solver is called)
extern int clause_is_partA (sat_solver2* s, int cid); extern int clause_is_partA (sat_solver2* s, int handle);
extern void clause_set_partA(sat_solver2* s, int cid, int partA); extern void clause_set_partA(sat_solver2* s, int handle, int partA);
// other clause functions
extern int clause_id(sat_solver2* s, int h);
//================================================================================================= //=================================================================================================
// Solver representation: // Solver representation:
...@@ -83,75 +85,105 @@ typedef struct varinfo_t varinfo; ...@@ -83,75 +85,105 @@ typedef struct varinfo_t varinfo;
struct sat_solver2_t struct sat_solver2_t
{ {
int size; // nof variables int size; // nof variables
int cap; // size of varmaps int cap; // size of varmaps
int qhead; // Head index of queue. int qhead; // Head index of queue.
int qtail; // Tail index of queue. int qtail; // Tail index of queue.
int root_level; // Level of first proper decision. int root_level; // Level of first proper decision.
int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'. int simpdb_assigns; // Number of top-level assignments at last 'simplifyDB()'.
int simpdb_props; // Number of propagations before next 'simplifyDB()'. int simpdb_props; // Number of propagations before next 'simplifyDB()'.
double random_seed; double random_seed;
double progress_estimate; double progress_estimate;
int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything
int fNotUseRandom; // do not allow random decisions with a fixed probability int fNotUseRandom; // do not allow random decisions with a fixed probability
// int fSkipSimplify; // set to one to skip simplification of the clause database // int fSkipSimplify; // set to one to skip simplification of the clause database
int fProofLogging; // enable proof-logging int fProofLogging; // enable proof-logging
// clauses // clauses
veci clauses; // clause memory veci clauses; // clause memory
veci* wlists; // watcher lists (for each literal) veci* wlists; // watcher lists (for each literal)
int iFirstLearnt; // the first learnt clause int iLearntFirst; // the first learnt clause
int iLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final)
// activities // activities
#ifdef USE_FLOAT_ACTIVITY #ifdef USE_FLOAT_ACTIVITY
double var_inc; // Amount to bump next variable with. double var_inc; // Amount to bump next variable with.
double var_decay; // INVERSE decay factor for variable activity: stores 1/decay. double var_decay; // INVERSE decay factor for variable activity: stores 1/decay.
float cla_inc; // Amount to bump next clause with. float cla_inc; // Amount to bump next clause with.
float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay. float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay.
double* activity; // A heuristic measurement of the activity of a variable. double* activity; // A heuristic measurement of the activity of a variable.
#else #else
int var_inc; // Amount to bump next variable with. int var_inc; // Amount to bump next variable with.
int cla_inc; // Amount to bump next clause with. int cla_inc; // Amount to bump next clause with.
unsigned* activity; // A heuristic measurement of the activity of a variable. unsigned* activity; // A heuristic measurement of the activity of a variable.
#endif #endif
veci claActs; // clause activities veci claActs; // clause activities
veci claProofs; // clause proofs veci claProofs; // clause proofs
// internal state // internal state
varinfo * vi; // variable information varinfo * vi; // variable information
lit* trail; // sequence of assignment and implications lit* trail; // sequence of assignment and implications
int* orderpos; // Index in variable order. int* orderpos; // Index in variable order.
cla* reasons; // reason clauses cla* reasons; // reason clauses
cla* units; // unit clauses cla* units; // unit clauses
veci tagged; // (contains: var) veci tagged; // (contains: var)
veci stack; // (contains: var) veci stack; // (contains: var)
veci order; // Variable order. (heap) (contains: var) veci order; // Variable order. (heap) (contains: var)
veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int) veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int)
veci temp_clause; // temporary storage for a CNF clause veci temp_clause; // temporary storage for a CNF clause
veci model; // If problem is solved, this vector contains the model (contains: lbool). veci model; // If problem is solved, this vector contains the model (contains: lbool).
veci conf_final; // If problem is unsatisfiable (possibly under assumptions), veci conf_final; // If problem is unsatisfiable (possibly under assumptions),
// this vector represent the final conflict clause expressed in the assumptions. // this vector represent the final conflict clause expressed in the assumptions.
veci mark_levels; // temporary storage for labeled levels veci mark_levels; // temporary storage for labeled levels
veci min_lit_order; // ordering of removable literals veci min_lit_order; // ordering of removable literals
veci min_step_order;// ordering of resolution steps veci min_step_order; // ordering of resolution steps
veci glob_vars; // global variables
// proof logging // proof logging
veci proof_clas; // sequence of proof clauses veci proof_clas; // sequence of proof clauses
veci proof_vars; // sequence of proof variables veci proof_vars; // sequence of proof variables
int iStartChain; // temporary variable to remember beginning of the current chain in proof logging int iStartChain; // temporary variable to remember beginning of the current chain in proof logging
int fLastConfId; // in proof-logging mode, the ID of the final conflict clause (conf_final) int nUnits; // the total number of unit clauses
int nUnits; // the total number of unit clauses
// statistics // statistics
stats_t stats; stats_t stats;
ABC_INT64_T nConfLimit; // external limit on the number of conflicts ABC_INT64_T nConfLimit; // external limit on the number of conflicts
ABC_INT64_T nInsLimit; // external limit on the number of implications ABC_INT64_T nInsLimit; // external limit on the number of implications
int nRuntimeLimit; // external limit on runtime int nRuntimeLimit; // external limit on runtime
};
typedef struct satset_t satset;
struct satset_t
{
unsigned learnt : 1;
unsigned mark : 1;
unsigned partA : 1;
unsigned nEnts : 29;
int Id;
lit pEnts[0];
}; };
static inline satset* satset_read (veci* p, cla h ) { return h ? (satset*)(veci_begin(p) + h) : NULL; }
static inline cla satset_handle (veci* p, satset* c) { return (cla)((int *)c - veci_begin(p)); }
static inline int satset_check (veci* p, satset* c) { return (int*)c > veci_begin(p) && (int*)c < veci_begin(p) + veci_size(p); }
static inline int satset_size (int nLits) { return sizeof(satset)/4 + nLits; }
static inline void satset_print (satset * c) {
int i;
printf( "{ " );
for ( i = 0; i < (int)c->nEnts; i++ )
printf( "%d ", (c->pEnts[i] & 1)? -(c->pEnts[i] >> 1) : c->pEnts[i] >> 1 );
printf( "}\n" );
}
#define satset_foreach_entry( p, c, h, s ) \
for ( h = s; (h < veci_size(p)) && (((c) = satset_read(p, h)), 1); h += satset_size(c->nEnts) )
//=================================================================================================
// Public APIs:
static inline int sat_solver2_nvars(sat_solver2* s) static inline int sat_solver2_nvars(sat_solver2* s)
{ {
return s->size; return s->size;
...@@ -213,6 +245,8 @@ static inline int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom) ...@@ -213,6 +245,8 @@ static inline int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom)
return fNotUseRandomOld; return fNotUseRandomOld;
} }
extern void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pVars, veci * pRoots, int hRoot, veci * pGlobVars );
ABC_NAMESPACE_HEADER_END ABC_NAMESPACE_HEADER_END
#endif #endif
src/sat/bsat/satVec.h
...@@ -29,15 +29,15 @@ ABC_NAMESPACE_HEADER_START ...@@ -29,15 +29,15 @@ ABC_NAMESPACE_HEADER_START
// vector of 32-bit intergers (added for 64-bit portability) // vector of 32-bit intergers (added for 64-bit portability)
struct veci_t { struct veci_t {
int size;
int cap; int cap;
int size;
int* ptr; int* ptr;
}; };
typedef struct veci_t veci; typedef struct veci_t veci;
static inline void veci_new (veci* v) { static inline void veci_new (veci* v) {
v->size = 0;
v->cap = 4; v->cap = 4;
v->size = 0;
v->ptr = (int*)ABC_ALLOC( char, sizeof(int)*v->cap); v->ptr = (int*)ABC_ALLOC( char, sizeof(int)*v->cap);
} }
...@@ -68,8 +68,8 @@ static inline void veci_remove(veci* v, int e) ...@@ -68,8 +68,8 @@ static inline void veci_remove(veci* v, int e)
// vector of 32- or 64-bit pointers // vector of 32- or 64-bit pointers
struct vecp_t { struct vecp_t {
int size;
int cap; int cap;
int size;
void** ptr; void** ptr;
}; };
typedef struct vecp_t vecp; typedef struct vecp_t vecp;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment