Skip to content

A
abc
Commit c265d244 by Alan Mishchenko
Options

Added learned clause recycling to the SAT solver (may impact bmc2, bmc3, dsat, etc).

parent 685faae8
Showing with 727 additions and 276 deletions
abclib.dsp
......@@ -1199,6 +1199,10 @@ SOURCE=.\src\sat\csat\csat_apis.h
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\sat\bsat\satClause.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\bsat\satInter.c
# End Source File
# Begin Source File
......
src/aig/aig/aigRepar.c
......@@ -54,13 +54,13 @@ static inline void Aig_ManInterAddBuffer( sat_solver2 * pSat, int iVarA, int iVa
Lits[1] = toLitCond( iVarB, !fCompl );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
clause2_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVarA, 1 );
Lits[1] = toLitCond( iVarB, fCompl );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
clause2_set_partA( pSat, Cid, 1 );
}
/**Function*************************************************************
......@@ -85,28 +85,28 @@ static inline void Aig_ManInterAddXor( sat_solver2 * pSat, int iVarA, int iVarB,
Lits[2] = toLitCond( iVarC, 1 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
clause2_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVarA, !fCompl );
Lits[1] = toLitCond( iVarB, 0 );
Lits[2] = toLitCond( iVarC, 0 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
clause2_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVarA, fCompl );
Lits[1] = toLitCond( iVarB, 1 );
Lits[2] = toLitCond( iVarC, 0 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
clause2_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVarA, fCompl );
Lits[1] = toLitCond( iVarB, 0 );
Lits[2] = toLitCond( iVarC, 1 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
clause2_set_partA( pSat, Cid, 1 );
}
/**Function*************************************************************
......@@ -152,7 +152,7 @@ void Aig_ManInterTest( Aig_Man_t * pMan, int fVerbose )
for ( i = 0; i < pCnf->nClauses; i++ )
{
Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] );
clause_set_partA( pSat, Cid, 1 );
clause2_set_partA( pSat, Cid, 1 );
}
// add clauses of B
......@@ -283,7 +283,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose )
for ( i = 0; i < pCnf->nClauses; i++ )
{
Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] );
clause_set_partA( pSat, Cid, k==0 );
clause2_set_partA( pSat, Cid, k==0 );
}
// add equality p[k] == A1/B1
Aig_ManForEachCo( pMan, pObj, i )
......@@ -293,7 +293,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose )
for ( i = 0; i < pCnf->nClauses; i++ )
{
Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] );
clause_set_partA( pSat, Cid, k==0 );
clause2_set_partA( pSat, Cid, k==0 );
}
// add comparator (!p[k] ^ A2/B2) == or[k]
Vec_IntClear( vVars );
......@@ -303,7 +303,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose )
Vec_IntPush( vVars, toLitCond(ShiftOr[k] + i, 1) );
}
Cid = sat_solver2_addclause( pSat, Vec_IntArray(vVars), Vec_IntArray(vVars) + Vec_IntSize(vVars) );
clause_set_partA( pSat, Cid, k==0 );
clause2_set_partA( pSat, Cid, k==0 );
// return to normal
Cnf_DataLift( pCnf, -ShiftCnf[k]-pCnf->nVars );
}
......@@ -362,7 +362,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose )
for ( i = 0; i < pCnfInter->nClauses; i++ )
{
Cid = sat_solver2_addclause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] );
clause_set_partA( pSat, Cid, c==0 );
clause2_set_partA( pSat, Cid, c==0 );
}
// connect to the inputs
Aig_ManForEachCi( pInter, pObj, i )
......
src/misc/vec/vecSet.h
......@@ -210,10 +210,11 @@ static inline double Vec_ReportMemory( Vec_Set_t * p )
***********************************************************************/
static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize )
{
word * pPage = p->pPages[p->iPage];
int nWords = Vec_SetWordNum( nSize );
assert( nWords < (1 << p->nPageSize) );
p->nEntries++;
if ( Vec_SetLimit( p->pPages[p->iPage] ) + nWords > (1 << p->nPageSize) )
assert( nWords + 3 < (1 << p->nPageSize) );
// need two extra at the begining of the page and one extra in the end
if ( Vec_SetLimit(pPage) + nWords >= (1 << p->nPageSize) )
{
if ( ++p->iPage == p->nPagesAlloc )
{
......@@ -223,12 +224,14 @@ static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize )
}
if ( p->pPages[p->iPage] == NULL )
p->pPages[p->iPage] = ABC_ALLOC( word, (1 << p->nPageSize) );
Vec_SetWriteLimit( p->pPages[p->iPage], 2 );
p->pPages[p->iPage][1] = ~0;
pPage = p->pPages[p->iPage];
Vec_SetWriteLimit(pPage, 2);
pPage[1] = ~0;
}
if ( pArray )
memcpy( p->pPages[p->iPage] + Vec_SetLimit(p->pPages[p->iPage]), pArray, sizeof(int) * nSize );
Vec_SetIncLimit( p->pPages[p->iPage], nWords );
memcpy( pPage + Vec_SetLimit(pPage), pArray, sizeof(int) * nSize );
p->nEntries++;
Vec_SetIncLimit( pPage, nWords );
return Vec_SetHandCurrent(p) - nWords;
}
static inline int Vec_SetAppendS( Vec_Set_t * p, int nSize )
......
src/sat/bsat/satClause.h 0 → 100644
/**CFile****************************************************************
FileName [satMem.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT solver.]
Synopsis [Memory management.]
Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 1, 2004.]
Revision [$Id: satMem.h,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__sat__bsat__satMem_h
#define ABC__sat__bsat__satMem_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "misc/util/abc_global.h"
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// STRUCTURE DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
//=================================================================================================
// Clause datatype + minor functions:
typedef int lit;
typedef int cla;
typedef struct clause_t clause;
struct clause_t
{
unsigned lrn : 1;
unsigned mark : 1;
unsigned partA : 1;
unsigned lbd : 8;
unsigned size : 21;
lit lits[0];
};
// learned clauses have "hidden" literal (c->lits[c->size]) to store clause ID
// data-structure for logging entries
// memory is allocated in 2^nPageSize word-sized pages
// the first 'word' of each page are stores the word limit
// although clause memory pieces are aligned to 64-bit words
// the integer clause handles are in terms of 32-bit unsigneds
// allowing for the first bit to be used for labeling 2-lit clauses
typedef struct Sat_Mem_t_ Sat_Mem_t;
struct Sat_Mem_t_
{
int nEntries[2]; // entry count
int BookMarkH[2]; // bookmarks for handles
int BookMarkE[2]; // bookmarks for entries
int iPage[2]; // current memory page
int nPageSize; // page log size in terms of ints
unsigned uPageMask; // page mask
unsigned uLearnedMask; // learned mask
int nPagesAlloc; // page count allocated
int ** pPages; // page pointers
};
static inline int Sat_MemLimit( int * p ) { return p[0]; }
static inline int Sat_MemIncLimit( int * p, int nInts ) { return p[0] += nInts; }
static inline void Sat_MemWriteLimit( int * p, int nInts ) { p[0] = nInts; }
static inline int Sat_MemHandPage( Sat_Mem_t * p, cla h ) { return h >> p->nPageSize; }
static inline int Sat_MemHandShift( Sat_Mem_t * p, cla h ) { return h & p->uPageMask; }
static inline int Sat_MemIntSize( int size, int lrn ) { return (size + 2 + lrn) & ~01; }
static inline int Sat_MemClauseSize( clause * p ) { return Sat_MemIntSize(p->size, p->lrn); }
//static inline clause * Sat_MemClause( Sat_Mem_t * p, int i, int k ) { assert(i <= p->iPage[i&1] && k <= Sat_MemLimit(p->pPages[i])); return (clause *)(p->pPages[i] + k ); }
static inline clause * Sat_MemClause( Sat_Mem_t * p, int i, int k ) { return (clause *)(p->pPages[i] + k); }
//static inline clause * Sat_MemClauseHand( Sat_Mem_t * p, cla h ) { assert(Sat_MemHandPage(p, h) <= p->iPage[(h & p->uLearnedMask) > 0]); assert(Sat_MemHandShift(p, h) >= 2 && Sat_MemHandShift(p, h) < (int)p->uLearnedMask); return Sat_MemClause( p, Sat_MemHandPage(p, h), Sat_MemHandShift(p, h) ); }
static inline clause * Sat_MemClauseHand( Sat_Mem_t * p, cla h ) { return Sat_MemClause( p, Sat_MemHandPage(p, h), Sat_MemHandShift(p, h) ); }
static inline int Sat_MemEntryNum( Sat_Mem_t * p, int lrn ) { return p->nEntries[lrn]; }
static inline cla Sat_MemHand( Sat_Mem_t * p, int i, int k ) { return (i << p->nPageSize) | k; }
static inline cla Sat_MemHandCurrent( Sat_Mem_t * p, int lrn ) { return (p->iPage[lrn] << p->nPageSize) | Sat_MemLimit( p->pPages[p->iPage[lrn]] ); }
static inline double Sat_MemMemoryHand( Sat_Mem_t * p, cla h ) { return 1.0 * ((Sat_MemHandPage(p, h) + 2)/2 * (1 << (p->nPageSize+2)) + Sat_MemHandShift(p, h) * 4); }
static inline double Sat_MemMemoryUsed( Sat_Mem_t * p, int lrn ) { return Sat_MemMemoryHand( p, Sat_MemHandCurrent(p, lrn) ); }
static inline double Sat_MemMemoryAllUsed( Sat_Mem_t * p ) { return Sat_MemMemoryUsed( p, 0 ) + Sat_MemMemoryUsed( p, 1 ); }
static inline double Sat_MemMemoryAll( Sat_Mem_t * p ) { return 1.0 * (p->iPage[0] + p->iPage[1] + 2) * (1 << (p->nPageSize+2)); }
// p is memory storage
// c is clause pointer
// i is page number
// k is page offset
#define Sat_MemForEachClause( p, c, i, k ) \
for ( i = 0; i <= p->iPage[0]; i += 2 ) \
for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) )
#define Sat_MemForEachLearned( p, c, i, k ) \
for ( i = 1; i <= p->iPage[1]; i += 2 ) \
for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) )
////////////////////////////////////////////////////////////////////////
/// GLOBAL VARIABLES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
static inline int clause_from_lit( lit l ) { return l + l + 1; }
static inline int clause_is_lit( cla h ) { return (h & 1); }
static inline lit clause_read_lit( cla h ) { return (lit)(h >> 1); }
static inline int clause_learnt_h( Sat_Mem_t * p, cla h ) { return (h & p->uLearnedMask) > 0; }
static inline int clause_learnt( clause * c ) { return c->lrn; }
static inline int clause_id( clause * c ) { assert(c->lrn); return c->lits[c->size]; }
static inline int clause_size( clause * c ) { return c->size; }
static inline lit * clause_begin( clause * c ) { return c->lits; }
static inline lit * clause_end( clause * c ) { return c->lits + c->size; }
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" );
}
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocating vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Sat_MemAlloc_( Sat_Mem_t * p, int nPageSize )
{
assert( nPageSize > 8 && nPageSize < 32 );
memset( p, 0, sizeof(Sat_Mem_t) );
p->nPageSize = nPageSize;
p->uLearnedMask = (unsigned)(1 << nPageSize);
p->uPageMask = (unsigned)((1 << nPageSize) - 1);
p->nPagesAlloc = 256;
p->pPages = ABC_CALLOC( int *, p->nPagesAlloc );
p->pPages[0] = ABC_ALLOC( int, (1 << p->nPageSize) );
p->pPages[1] = ABC_ALLOC( int, (1 << p->nPageSize) );
p->iPage[0] = 0;
p->iPage[1] = 1;
Sat_MemWriteLimit( p->pPages[0], 2 );
Sat_MemWriteLimit( p->pPages[1], 2 );
}
static inline Sat_Mem_t * Sat_MemAlloc( int nPageSize )
{
Sat_Mem_t * p;
p = ABC_CALLOC( Sat_Mem_t, 1 );
Sat_MemAlloc_( p, nPageSize );
return p;
}
/**Function*************************************************************
Synopsis [Resetting vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Sat_MemRestart( Sat_Mem_t * p )
{
p->nEntries[0] = 0;
p->nEntries[1] = 0;
p->iPage[0] = 0;
p->iPage[1] = 1;
Sat_MemWriteLimit( p->pPages[0], 2 );
Sat_MemWriteLimit( p->pPages[1], 2 );
}
/**Function*************************************************************
Synopsis [Sets the bookmark.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Sat_MemBookMark( Sat_Mem_t * p )
{
p->BookMarkH[0] = Sat_MemHandCurrent( p, 0 );
p->BookMarkH[1] = Sat_MemHandCurrent( p, 1 );
p->BookMarkE[0] = p->nEntries[0];
p->BookMarkE[1] = p->nEntries[1];
}
static inline void Sat_MemRollBack( Sat_Mem_t * p )
{
p->nEntries[0] = p->BookMarkE[0];
p->nEntries[1] = p->BookMarkE[1];
p->iPage[0] = Sat_MemHandPage( p, p->BookMarkH[0] );
p->iPage[1] = Sat_MemHandPage( p, p->BookMarkH[1] );
Sat_MemWriteLimit( p->pPages[0], Sat_MemHandShift( p, p->BookMarkH[0] ) );
Sat_MemWriteLimit( p->pPages[1], Sat_MemHandShift( p, p->BookMarkH[1] ) );
}
/**Function*************************************************************
Synopsis [Freeing vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Sat_MemFree_( Sat_Mem_t * p )
{
int i;
for ( i = 0; i < p->nPagesAlloc; i++ )
ABC_FREE( p->pPages[i] );
ABC_FREE( p->pPages );
}
static inline void Sat_MemFree( Sat_Mem_t * p )
{
Sat_MemFree_( p );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Creates new clause.]
Description [The resulting clause is fully initialized.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Sat_MemAppend( Sat_Mem_t * p, int * pArray, int nSize, int lrn )
{
clause * c;
int * pPage = p->pPages[p->iPage[lrn]];
int nInts = Sat_MemIntSize( nSize, lrn );
assert( nInts + 3 < (1 << p->nPageSize) );
// need two extra at the begining of the page and one extra in the end
if ( Sat_MemLimit(pPage) + nInts >= (1 << p->nPageSize) )
{
p->iPage[lrn] += 2;
if ( p->iPage[lrn] >= p->nPagesAlloc )
{
p->pPages = ABC_REALLOC( int *, p->pPages, p->nPagesAlloc * 2 );
memset( p->pPages + p->nPagesAlloc, 0, sizeof(int *) * p->nPagesAlloc );
p->nPagesAlloc *= 2;
}
if ( p->pPages[p->iPage[lrn]] == NULL )
p->pPages[p->iPage[lrn]] = ABC_ALLOC( int, (1 << p->nPageSize) );
pPage = p->pPages[p->iPage[lrn]];
Sat_MemWriteLimit( pPage, 2 );
}
pPage[Sat_MemLimit(pPage)] = 0;
c = (clause *)(pPage + Sat_MemLimit(pPage));
c->size = nSize;
c->lrn = lrn;
if ( pArray )
memcpy( c->lits, pArray, sizeof(int) * nSize );
if ( lrn )
c->lits[c->size] = p->nEntries[1];
p->nEntries[lrn]++;
Sat_MemIncLimit( pPage, nInts );
return Sat_MemHandCurrent(p, lrn) - nInts;
}
/**Function*************************************************************
Synopsis [Shrinking vector size.]
Description []
SideEffects [This procedure does not update the number of entries.]
SeeAlso []
***********************************************************************/
static inline void Sat_MemShrink( Sat_Mem_t * p, int h, int lrn )
{
assert( clause_learnt_h(p, h) == lrn );
assert( h && h <= Sat_MemHandCurrent(p, lrn) );
p->iPage[lrn] = Sat_MemHandPage(p, h);
Sat_MemWriteLimit( p->pPages[p->iPage[lrn]], Sat_MemHandShift(p, h) );
}
/**Function*************************************************************
Synopsis [Compacts learned clauses by removing marked entries.]
Description [Returns the number of remaining entries.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Sat_MemCompactLearned( Sat_Mem_t * p, int fDoMove )
{
clause * c;
int i, k, iNew = 1, kNew = 2, nInts, Counter = 0;
// iterate through the learned clauses
Sat_MemForEachLearned( p, c, i, k )
{
assert( c->lrn );
// skip marked entry
if ( c->mark )
continue;
// compute entry size
nInts = Sat_MemClauseSize(c);
assert( !(nInts & 1) );
// check if we need to scroll to the next page
if ( kNew + nInts >= (1 << p->nPageSize) )
{
// set the limit of the current page
if ( fDoMove )
Sat_MemWriteLimit( p->pPages[iNew], kNew );
// move writing position to the new page
iNew += 2;
kNew = 2;
}
if ( fDoMove )
{
// make sure the result is the same as previous dry run
assert( c->lits[c->size] == Sat_MemHand(p, iNew, kNew) );
// only copy the clause if it has changed
if ( i != iNew || k != kNew )
{
memmove( p->pPages[iNew] + kNew, c, sizeof(int) * nInts );
// c = Sat_MemClause( p, iNew, kNew ); // assersions do not hold during dry run
c = (clause *)(p->pPages[iNew] + kNew);
assert( nInts == Sat_MemClauseSize(c) );
}
// set the new ID value
c->lits[c->size] = Counter;
}
else // remember the address of the clause in the new location
c->lits[c->size] = Sat_MemHand(p, iNew, kNew);
// update writing position
kNew += nInts;
assert( iNew <= i && kNew < (1 << p->nPageSize) );
// update counter
Counter++;
}
if ( fDoMove )
{
// update the page count
p->iPage[1] = iNew;
// set the limit of the last page
Sat_MemWriteLimit( p->pPages[iNew], kNew );
// update the counter
p->nEntries[1] = Counter;
}
return Counter;
}
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/sat/bsat/satSolver.c
......@@ -29,6 +29,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
ABC_NAMESPACE_IMPL_START
//#define LEARNT_MAX_START 0
#define LEARNT_MAX_START 20000
#define LEARNT_MAX_INCRE 1000
#define SAT_USE_ANALYZE_FINAL
//=================================================================================================
......@@ -127,39 +131,6 @@ int sat_solver_get_var_value(sat_solver* s, int v)
}
//=================================================================================================
// Clause datatype + minor functions:
struct clause_t
{
int size_learnt;
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; }
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_nlits(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 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); }
......@@ -257,7 +228,7 @@ static inline void act_var_rescale(sat_solver* s) {
s->var_inc *= 1e-100;
}
static inline void act_clause_rescale(sat_solver* s) {
// static int Total = 0;
// static clock_t Total = 0;
clause** cs = (clause**)veci_begin(&s->learnts);
int i;//, clk = clock();
for (i = 0; i < veci_size(&s->learnts); i++){
......@@ -267,8 +238,8 @@ static inline void act_clause_rescale(sat_solver* s) {
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 );
// 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;
......@@ -313,24 +284,21 @@ static inline void act_var_rescale(sat_solver* s) {
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;
static clock_t Total = 0;
clock_t clk = clock();
for (i = 0; i < vecp_size(&s->learnts); i++){
unsigned a = clause_activity2(cs[i]);
clause_setactivity2(cs[i], a >> 14);
}
unsigned* activity = (unsigned *)veci_begin(&s->act_clas);
int i;
for (i = 0; i < veci_size(&s->act_clas); i++)
activity[i] >>= 14;
s->cla_inc >>= 14;
s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
// Total += clock() - clk;
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)
......@@ -356,16 +324,16 @@ static inline void act_var_bump_factor(sat_solver* s, int v) {
if (s->orderpos[v] != -1)
order_update(s,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)
unsigned* act = (unsigned *)veci_begin(&s->act_clas) + c->lits[c->size];
*act += s->cla_inc;
if ( *act & 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); }
static inline void act_clause_decay(sat_solver* s) { s->cla_inc += (s->cla_inc >> 10); }
#endif
......@@ -416,13 +384,30 @@ static void sortrnd(void** array, int size, int(*comp)(const void *, const void
//=================================================================================================
// Clause functions:
static inline int sat_clause_compute_lbd( sat_solver* s, clause* c )
{
int i, lev, minl = 0, lbd = 0;
for (i = 0; i < (int)c->size; i++)
{
lev = var_level(s, lit_var(c->lits[i]));
if ( !(minl & (1 << (lev & 31))) )
{
minl |= 1 << (lev & 31);
lbd++;
// printf( "%d ", lev );
}
}
// printf( " -> %d\n", lbd );
return lbd;
}
/* pre: size > 1 && no variable occurs twice
*/
static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
{
int size;
clause* c;
int h, i;
int h;
assert(end - begin > 1);
assert(learnt >= 0 && learnt < 2);
......@@ -433,20 +418,33 @@ static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
{
veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(clause_from_lit(begin[1])));
veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(clause_from_lit(begin[0])));
s->stats.clauses++;
s->stats.clauses_literals += size;
return 0;
}
// create new clause
h = Vec_SetAppend( &s->Mem, NULL, size + learnt + 1 ) << 1;
// h = Vec_SetAppend( &s->Mem, NULL, size + learnt + 1 + 1 ) << 1;
h = Sat_MemAppend( &s->Mem, begin, size, learnt );
assert( !(h & 1) );
c = clause_read( s, h );
if ( s->hLearnts == -1 && learnt )
s->hLearnts = h;
c->size_learnt = (size << 1) | learnt;
for (i = 0; i < size; i++)
c->lits[i] = begin[i];
if (learnt)
*((float*)&c->lits[size]) = 0.0;
{
c = clause_read( s, h );
c->lbd = sat_clause_compute_lbd( s, c );
assert( clause_id(c) == veci_size(&s->act_clas) );
// veci_push(&s->learned, h);
// act_clause_bump(s,clause_read(s, h));
veci_push(&s->act_clas, (1<<10));
s->stats.learnts++;
s->stats.learnts_literals += size;
}
else
{
s->stats.clauses++;
s->stats.clauses_literals += size;
}
assert(begin[0] >= 0);
assert(begin[0] < s->size*2);
......@@ -541,6 +539,7 @@ static void sat_solver_record(sat_solver* s, veci* cls)
lit* end = begin + veci_size(cls);
int h = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : 0;
sat_solver_enqueue(s,*begin,h);
assert(veci_size(cls) > 0);
///////////////////////////////////
// add clause to internal storage
......@@ -550,15 +549,13 @@ static void sat_solver_record(sat_solver* s, veci* cls)
assert( RetValue );
}
///////////////////////////////////
assert(veci_size(cls) > 0);
/*
if (h != 0) {
// veci_push(&s->learnts,c);
// act_clause_bump(s,c);
act_clause_bump(s,clause_read(s, h));
s->stats.learnts++;
s->stats.learnts_literals += veci_size(cls);
}
*/
}
......@@ -602,7 +599,7 @@ static int sat_solver_lit_removable(sat_solver* s, int x, int minl)
clause* c = clause_read(s, s->reasons[v]);
lit* lits = clause_begin(c);
int i;
for (i = 1; i < clause_nlits(c); i++){
for (i = 1; i < clause_size(c); i++){
int v = lit_var(lits[i]);
if (!var_tag(s,v) && var_level(s, v)){
if (s->reasons[v] != 0 && ((1 << (var_level(s, v) & 31)) & minl)){
......@@ -681,7 +678,7 @@ static void sat_solver_analyze_final(sat_solver* s, int hConf, int skip_first)
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_nlits(conf); i++)
for (i = skip_first ? 1 : 0; i < clause_size(conf); i++)
{
int x = lit_var(clause_begin(conf)[i]);
if (var_level(s, x) > 0)
......@@ -705,7 +702,7 @@ static void sat_solver_analyze_final(sat_solver* s, int hConf, int skip_first)
else{
clause* c = clause_read(s, s->reasons[x]);
int* lits = clause_begin(c);
for (j = 1; j < clause_nlits(c); j++)
for (j = 1; j < clause_size(c); j++)
if (var_level(s, lit_var(lits[j])) > 0)
var_set_tag(s, lit_var(lits[j]), 1);
}
......@@ -717,7 +714,6 @@ static void sat_solver_analyze_final(sat_solver* s, int hConf, int skip_first)
#endif
static void sat_solver_analyze(sat_solver* s, int h, veci* learnt)
{
lit* trail = s->trail;
......@@ -741,15 +737,18 @@ static void sat_solver_analyze(sat_solver* s, int h, veci* learnt)
}
}else{
clause* c = clause_read(s, h);
// if (clause_learnt(c))
// act_clause_bump(s,c);
if (clause_learnt(c))
act_clause_bump(s,c);
lits = clause_begin(c);
//printlits(lits,lits+clause_nlits(c)); printf("\n");
for (j = (p == lit_Undef ? 0 : 1); j < clause_nlits(c); j++){
//printlits(lits,lits+clause_size(c)); printf("\n");
for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){
int x = lit_var(lits[j]);
if (var_tag(s, x) == 0 && var_level(s, x) > 0){
var_set_tag(s, x, 1);
act_var_bump(s,x);
// bump variables propaged by the LBD=2 clause
// if ( s->reasons[x] && clause_read(s, s->reasons[x])->lbd <= 2 )
// act_var_bump(s,x);
if (var_level(s,x) == sat_solver_dl(s))
cnt++;
else
......@@ -785,6 +784,7 @@ static void sat_solver_analyze(sat_solver* s, int h, veci* learnt)
veci_resize(learnt,j);
s->stats.tot_literals += j;
// clear tags
solver2_clear_tags(s,0);
......@@ -836,7 +836,7 @@ int sat_solver_propagate(sat_solver* s)
int*i, *j;
s->stats.propagations++;
s->simpdb_props--;
// s->simpdb_props--;
//printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
for (i = j = begin; i < end; ){
......@@ -875,7 +875,7 @@ int sat_solver_propagate(sat_solver* s)
*j++ = *i;
else{
// Look for new watch:
lit* stop = lits + clause_nlits(c);
lit* stop = lits + clause_size(c);
lit* k;
for (k = lits + 2; k < stop; k++){
if (var_value(s, lit_var(*k)) != !lit_sign(*k)){
......@@ -887,6 +887,8 @@ int sat_solver_propagate(sat_solver* s)
*j++ = *i;
// Clause is unit under assignment:
if ( c->lrn )
c->lbd = sat_clause_compute_lbd(s, c);
if (!sat_solver_enqueue(s,lits[0], *i)){
hConfl = *i++;
// Copy the remaining watches:
......@@ -913,16 +915,20 @@ sat_solver* sat_solver_new(void)
{
sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver));
Vec_SetAlloc_(&s->Mem, 15);
// Vec_SetAlloc_(&s->Mem, 15);
Sat_MemAlloc_(&s->Mem, 14);
s->hLearnts = -1;
s->hBinary = Vec_SetAppend( &s->Mem, NULL, 3 ) << 1;
s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0 );
s->binary = clause_read( s, s->hBinary );
s->binary->size_learnt = (2 << 1);
s->nLearntMax = LEARNT_MAX_START;
// initialize vectors
veci_new(&s->order);
veci_new(&s->trail_lim);
veci_new(&s->tagged);
// veci_new(&s->learned);
veci_new(&s->act_clas);
veci_new(&s->stack);
// veci_new(&s->model);
veci_new(&s->act_vars);
......@@ -945,14 +951,14 @@ sat_solver* sat_solver_new(void)
s->var_inc = 1;
s->cla_inc = 1;
s->var_decay = (float)(1 / 0.95 );
s->cla_decay = (float)(1 / 0.999 );
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->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);
......@@ -1035,12 +1041,15 @@ void sat_solver_setnvars(sat_solver* s,int n)
void sat_solver_delete(sat_solver* s)
{
Vec_SetFree_( &s->Mem );
// Vec_SetFree_( &s->Mem );
Sat_MemFree_( &s->Mem );
// delete vectors
veci_delete(&s->order);
veci_delete(&s->trail_lim);
veci_delete(&s->tagged);
// veci_delete(&s->learned);
veci_delete(&s->act_clas);
veci_delete(&s->stack);
// veci_delete(&s->model);
veci_delete(&s->act_vars);
......@@ -1073,12 +1082,10 @@ void sat_solver_delete(sat_solver* s)
void sat_solver_rollback( sat_solver* s )
{
int i;
Vec_SetRestart( &s->Mem );
Sat_MemRestart( &s->Mem );
s->hLearnts = -1;
s->hBinary = Vec_SetAppend( &s->Mem, NULL, 3 ) << 1;
s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0 );
s->binary = clause_read( s, s->hBinary );
s->binary->size_learnt = (2 << 1);
veci_resize(&s->trail_lim, 0);
veci_resize(&s->order, 0);
......@@ -1100,8 +1107,8 @@ void sat_solver_rollback( sat_solver* s )
s->cla_inc = (1 << 11);
#endif
s->root_level = 0;
s->simpdb_assigns = 0;
s->simpdb_props = 0;
// s->simpdb_assigns = 0;
// s->simpdb_props = 0;
s->random_seed = 91648253;
s->progress_estimate = 0;
s->verbosity = 0;
......@@ -1145,116 +1152,138 @@ double sat_solver_memory( sat_solver* s )
Mem += s->order.cap * sizeof(int);
Mem += s->trail_lim.cap * sizeof(int);
Mem += s->tagged.cap * sizeof(int);
// Mem += s->learned.cap * sizeof(int);
Mem += s->stack.cap * sizeof(int);
Mem += s->act_vars.cap * sizeof(int);
Mem += s->act_clas.cap * sizeof(int);
Mem += s->temp_clause.cap * sizeof(int);
Mem += s->conf_final.cap * sizeof(int);
Mem += Vec_ReportMemory( &s->Mem );
Mem += Sat_MemMemoryAll( &s->Mem );
return Mem;
}
int sat_solver_simplify(sat_solver* s)
{
assert(sat_solver_dl(s) == 0);
if (sat_solver_propagate(s) != 0)
return false;
return true;
}
/*
static void clause_remove(sat_solver* s, clause* c)
void sat_solver_reducedb(sat_solver* s)
{
lit* lits = clause_begin(c);
assert(lit_neg(lits[0]) < s->size*2);
assert(lit_neg(lits[1]) < s->size*2);
static clock_t TimeTotal = 0;
clock_t clk = clock();
Sat_Mem_t * pMem = &s->Mem;
int nLearnedOld = veci_size(&s->act_clas);
int * act_clas = veci_begin(&s->act_clas);
int * pPerm, * pArray, * pSortValues, nCutoffValue;
int i, k, j, Id, Counter, CounterStart, nSelected;
clause * c;
assert( s->nLearntMax > 0 );
assert( nLearnedOld == Sat_MemEntryNum(pMem, 1) );
assert( nLearnedOld == (int)s->stats.learnts );
s->nDBreduces++;
// printf( "Calling reduceDB with %d learned clause limit.\n", s->nLearntMax );
s->nLearntMax = LEARNT_MAX_START + LEARNT_MAX_INCRE * s->nDBreduces;
// return;
// create sorting values
pSortValues = ABC_ALLOC( int, nLearnedOld );
Sat_MemForEachLearned( pMem, c, i, k )
{
Id = clause_id(c);
pSortValues[Id] = (((7 - Abc_MinInt(c->lbd, 7)) << 28) | (act_clas[Id] >> 4));
// pSortValues[Id] = act[Id];
assert( pSortValues[Id] >= 0 );
}
// preserve 1/20 of last clauses
CounterStart = nLearnedOld - (s->nLearntMax / 20);
//veci_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
//veci_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
// preserve 3/4 of most active clauses
nSelected = nLearnedOld*5/10;
assert(lits[0] < s->size*2);
veci_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(clause_nlits(c) > 2 ? c : clause_from_lit(lits[1])));
veci_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(clause_nlits(c) > 2 ? c : clause_from_lit(lits[0])));
// find non-decreasing permutation
pPerm = Abc_MergeSortCost( pSortValues, nLearnedOld );
assert( pSortValues[pPerm[0]] <= pSortValues[pPerm[nLearnedOld-1]] );
nCutoffValue = pSortValues[pPerm[nLearnedOld-nSelected]];
ABC_FREE( pPerm );
// ActCutOff = ABC_INFINITY;
if (clause_learnt(c)){
// mark learned clauses to remove
Counter = j = 0;
Sat_MemForEachLearned( pMem, c, i, k )
{
assert( c->mark == 0 );
if ( Counter++ > CounterStart || clause_size(c) < 3 || pSortValues[clause_id(c)] > nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) )
act_clas[j++] = act_clas[clause_id(c)];
else // delete
{
c->mark = 1;
s->stats.learnts_literals -= clause_size(c);
s->stats.learnts--;
s->stats.learnts_literals -= clause_nlits(c);
}else{
s->stats.clauses--;
s->stats.clauses_literals -= clause_nlits(c);
}
}
static lbool clause_simplify(sat_solver* s, clause* c)
{
lit* lits = clause_begin(c);
int i;
assert(sat_solver_dl(s) == 0);
for (i = 0; i < clause_nlits(c); i++){
lbool sig = !lit_sign(lits[i]); sig += sig - 1;
if (s->assignss[lit_var(lits[i])] == sig)
return l_True;
}
return l_False;
}
*/
assert( s->stats.learnts == (unsigned)j );
assert( Counter == nLearnedOld );
veci_resize(&s->act_clas,j);
ABC_FREE( pSortValues );
int sat_solver_simplify(sat_solver* s)
{
// clause** reasons;
// int type;
assert(sat_solver_dl(s) == 0);
// update ID of each clause to be its new handle
Counter = Sat_MemCompactLearned( pMem, 0 );
assert( Counter == (int)s->stats.learnts );
if (sat_solver_propagate(s) != 0)
return false;
// update reasons
for ( i = 0; i < s->size; i++ )
{
if ( !s->reasons[i] ) // no reason
continue;
if ( clause_is_lit(s->reasons[i]) ) // 2-lit clause
continue;
if ( !clause_learnt_h(pMem, s->reasons[i]) ) // problem clause
continue;
c = clause_read( s, s->reasons[i] );
assert( c->mark == 0 );
s->reasons[i] = clause_id(c); // updating handle here!!!
}
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]);
// update watches
for ( i = 0; i < s->size*2; i++ )
{
pArray = veci_begin(&s->wlists[i]);
for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
{
if ( clause_is_lit(pArray[k]) ) // 2-lit clause
pArray[j++] = pArray[k];
else if ( !clause_learnt_h(pMem, pArray[k]) ) // problem clause
pArray[j++] = pArray[k];
else
cls[j++] = cls[i];
{
c = clause_read(s, pArray[k]);
if ( !c->mark ) // useful learned clause
pArray[j++] = clause_id(c); // updating handle here!!!
}
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_nlits((clause*)x) > 2 && (clause_nlits((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 / veci_size(&s->learnts); // Remove any clause below this activity
clause** learnts = (clause**)veci_begin(&s->learnts);
clause** reasons = s->reasons;
veci_resize(&s->wlists[i],j);
}
sat_solver_sort(veci_begin(&s->learnts), veci_size(&s->learnts), &clause_cmp);
// perform final move of the clauses
Counter = Sat_MemCompactLearned( pMem, 1 );
assert( Counter == (int)s->stats.learnts );
for (i = j = 0; i < veci_size(&s->learnts) / 2; i++){
if (clause_nlits(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
clause_remove(s,learnts[i]);
else
learnts[j++] = learnts[i];
}
for (; i < veci_size(&s->learnts); i++){
if (clause_nlits(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];
// report the results
TimeTotal += clock() - clk;
if ( s->fVerbose )
{
Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) ",
s->stats.learnts, nLearnedOld, 100.0 * s->stats.learnts / nLearnedOld );
Abc_PrintTime( 1, "Time", TimeTotal );
}
veci_resize(&s->learnts,j);
}
*/
int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
{
......@@ -1308,9 +1337,6 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
// create new clause
clause_create_new(s,begin,j,0);
s->stats.clauses++;
s->stats.clauses_literals += j - begin;
return true;
}
......@@ -1335,7 +1361,7 @@ void luby_test()
printf( "\n" );
}
static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT64_T nof_learnts)
static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
{
// double var_decay = 0.95;
// double clause_decay = 0.999;
......@@ -1395,36 +1421,37 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
var_set_level(s, lit_var(learnt_clause.ptr[0]), 0);
#endif
act_var_decay(s);
// act_clause_decay(s);
act_clause_decay(s);
}else{
// NO CONFLICT
int next;
if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
// Reached bound on number of conflicts:
if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
s->progress_estimate = sat_solver_progress(s);
sat_solver_canceluntil(s,s->root_level);
veci_delete(&learnt_clause);
return l_Undef; }
// Reached bound on number of conflicts:
if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) ||
(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:
if (sat_solver_dl(s) == 0 && !s->fSkipSimplify)
sat_solver_simplify(s);
// if (nof_learnts >= 0 && veci_size(&s->learnts) - s->qtail >= nof_learnts)
// Reduce the set of learnt clauses:
// sat_solver_reducedb(s);
// if (s->nLearntMax && veci_size(&s->learned) - s->qtail >= s->nLearntMax)
if (s->nLearntMax && veci_size(&s->act_clas) >= s->nLearntMax)
sat_solver_reducedb(s);
// New variable decision:
s->stats.decisions++;
......@@ -1463,7 +1490,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
{
int restart_iter = 0;
ABC_INT64_T nof_conflicts;
ABC_INT64_T nof_learnts = sat_solver_nclauses(s) / 3;
// ABC_INT64_T nof_learnts = sat_solver_nclauses(s) / 3;
lbool status = l_Undef;
lit* i;
......@@ -1623,8 +1650,8 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
fflush(stdout);
}
nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) );
status = sat_solver_search(s, nof_conflicts, nof_learnts);
nof_learnts = nof_learnts * 11 / 10; //*= 1.1;
status = sat_solver_search(s, nof_conflicts);
// nof_learnts = nof_learnts * 11 / 10; //*= 1.1;
// quit the loop if reached an external limit
if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
break;
......
src/sat/bsat/satSolver.h
......@@ -28,6 +28,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include <string.h>
#include <assert.h>
#include "satClause.h"
#include "satVec.h"
#include "misc/vec/vecSet.h"
......@@ -79,8 +80,8 @@ extern void * sat_solver_store_release( sat_solver * s );
//=================================================================================================
// Solver representation:
struct clause_t;
typedef struct clause_t clause;
//struct clause_t;
//typedef struct clause_t clause;
struct varinfo_t;
typedef struct varinfo_t varinfo;
......@@ -93,7 +94,7 @@ struct sat_solver_t
int qtail; // Tail index of queue.
// clauses
Vec_Set_t Mem;
Sat_Mem_t Mem;
int hLearnts; // the first learnt clause
int hBinary; // the special binary clause
clause * binary;
......@@ -137,8 +138,13 @@ struct sat_solver_t
double random_seed;
double progress_estimate;
int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything
int fVerbose;
stats_t stats;
int nLearntMax; // max number of learned clauses
int nDBreduces; // number of DB reductions
// veci learned; // contain learnt clause handles
veci act_clas; // contain clause activities
ABC_INT64_T nConfLimit; // external limit on the number of conflicts
ABC_INT64_T nInsLimit; // external limit on the number of implications
......@@ -166,6 +172,11 @@ struct sat_solver_t
veci temp_clause; // temporary storage for a CNF clause
};
static inline clause * clause_read( sat_solver * s, cla h )
{
return Sat_MemClauseHand( &s->Mem, h );
}
static int sat_solver_var_value( sat_solver* s, int v )
{
assert( v >= 0 && v < s->size );
......
src/sat/bsat/satSolver2.c
......@@ -136,28 +136,28 @@ static inline void solver2_clear_marks(sat_solver2* s) {
//=================================================================================================
// Clause datatype + minor functions:
static inline satset* clause_read (sat_solver2* s, cla h) { return (h & 1) ? satset_read(&s->learnts, h>>1) : satset_read(&s->clauses, h>>1); }
static inline cla clause_handle (sat_solver2* s, satset* c) { return c->learnt ? (satset_handle(&s->learnts, c)<<1)|1: satset_handle(&s->clauses, c)<<1; }
static inline int clause_check (sat_solver2* s, satset* c) { return c->learnt ? satset_check(&s->learnts, c) : satset_check(&s->clauses, c); }
static inline int clause_proofid(sat_solver2* s, satset* c, int partA) { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (satset_handle(&s->clauses, c)<<2) | (partA<<1) | 1; }
static inline int clause_is_used(sat_solver2* s, cla h) { return (h & 1) ? ((h >> 1) < s->hLearntPivot) : ((h >> 1) < s->hClausePivot); }
static inline satset* clause2_read (sat_solver2* s, cla h) { return (h & 1) ? satset_read(&s->learnts, h>>1) : satset_read(&s->clauses, h>>1); }
static inline cla clause2_handle (sat_solver2* s, satset* c) { return c->learnt ? (satset_handle(&s->learnts, c)<<1)|1: satset_handle(&s->clauses, c)<<1; }
static inline int clause2_check (sat_solver2* s, satset* c) { return c->learnt ? satset_check(&s->learnts, c) : satset_check(&s->clauses, c); }
static inline int clause2_proofid(sat_solver2* s, satset* c, int partA) { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (satset_handle(&s->clauses, c)<<2) | (partA<<1) | 1; }
static inline int clause2_is_used(sat_solver2* s, cla h) { return (h & 1) ? ((h >> 1) < s->hLearntPivot) : ((h >> 1) < s->hClausePivot); }
//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 satset* var_unit_clause(sat_solver2* s, int v) { return (s->reasons[v]&1) ? clause_read(s, s->reasons[v] >> 1) : NULL; }
//static inline satset* var_unit_clause(sat_solver2* s, int v) { return (s->reasons[v]&1) ? clause2_read(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 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* var_unit_clause(sat_solver2* s, int v) { return clause_read(s, s->units[v]); }
static inline satset* var_unit_clause(sat_solver2* s, int v) { return clause2_read(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++;
}
//static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size); s->units[v] = i; s->nUnits++; }
// these two only work after creating a clause before the solver is called
int clause_is_partA (sat_solver2* s, int h) { return clause_read(s, h)->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; }
int clause2_is_partA (sat_solver2* s, int h) { return clause2_read(s, h)->partA; }
void clause2_set_partA(sat_solver2* s, int h, int partA) { clause2_read(s, h)->partA = partA; }
int clause2_id(sat_solver2* s, int h) { return clause2_read(s, h)->Id; }
//=================================================================================================
// Simple helpers:
......@@ -172,7 +172,7 @@ static inline void proof_chain_start( sat_solver2* s, satset* c )
{
if ( s->fProofLogging )
{
int ProofId = clause_proofid(s, c, 0);
int ProofId = clause2_proofid(s, c, 0);
assert( ProofId > 0 );
veci_resize( &s->temp_proof, 0 );
veci_push( &s->temp_proof, 0 );
......@@ -186,7 +186,7 @@ static inline void proof_chain_resolve( sat_solver2* s, satset* cls, int Var )
if ( s->fProofLogging )
{
satset* c = cls ? cls : var_unit_clause( s, Var );
int ProofId = clause_proofid(s, c, var_is_partA(s,Var));
int ProofId = clause2_proofid(s, c, var_is_partA(s,Var));
assert( ProofId > 0 );
veci_push( &s->temp_proof, ProofId );
}
......@@ -291,7 +291,7 @@ static inline void act_var_rescale(sat_solver2* s) {
activity[i] *= 1e-100;
s->var_inc *= 1e-100;
}
static inline void act_clause_rescale(sat_solver2* s) {
static inline void act_clause2_rescale(sat_solver2* s) {
static int Total = 0;
float * claActs = (float *)veci_begin(&s->claActs);
int i;
......@@ -311,15 +311,15 @@ static inline void act_var_bump(sat_solver2* s, int v) {
if (s->orderpos[v] != -1)
order_update(s,v);
}
static inline void act_clause_bump(sat_solver2* s, satset*c) {
static inline void act_clause2_bump(sat_solver2* s, satset*c) {
float * claActs = (float *)veci_begin(&s->claActs);
assert( c->Id < veci_size(&s->claActs) );
claActs[c->Id] += s->cla_inc;
if (claActs[c->Id] > (float)1e20)
act_clause_rescale(s);
act_clause2_rescale(s);
}
static inline void act_var_decay(sat_solver2* s) { s->var_inc *= s->var_decay; }
static inline void act_clause_decay(sat_solver2* s) { s->cla_inc *= s->cla_decay; }
static inline void act_clause2_decay(sat_solver2* s) { s->cla_inc *= s->cla_decay; }
#else
......@@ -331,7 +331,7 @@ static inline void act_var_rescale(sat_solver2* s) {
s->var_inc >>= 19;
s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) );
}
static inline void act_clause_rescale(sat_solver2* s) {
static inline void act_clause2_rescale(sat_solver2* s) {
// static int Total = 0;
int i;//, clk = clock();
unsigned * claActs = (unsigned *)veci_begin(&s->claActs);
......@@ -351,22 +351,22 @@ static inline void act_var_bump(sat_solver2* s, int v) {
if (s->orderpos[v] != -1)
order_update(s,v);
}
static inline void act_clause_bump(sat_solver2* s, satset*c) {
static inline void act_clause2_bump(sat_solver2* s, satset*c) {
unsigned * claActs = (unsigned *)veci_begin(&s->claActs);
assert( c->Id > 0 && c->Id < veci_size(&s->claActs) );
claActs[c->Id] += s->cla_inc;
if (claActs[c->Id] & 0x80000000)
act_clause_rescale(s);
act_clause2_rescale(s);
}
static inline void act_var_decay(sat_solver2* s) { s->var_inc += (s->var_inc >> 4); }
static inline void act_clause_decay(sat_solver2* s) { s->cla_inc += (s->cla_inc >> 10); }
static inline void act_clause2_decay(sat_solver2* s) { s->cla_inc += (s->cla_inc >> 10); }
#endif
//=================================================================================================
// Clause functions:
static int clause_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id)
static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id)
{
satset* c;
int i, Cid, nLits = end - begin;
......@@ -404,7 +404,7 @@ static int clause_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, i
if ( proof_id )
veci_push(&s->claProofs, proof_id);
if ( nLits > 2 )
act_clause_bump( s,c );
act_clause2_bump( s,c );
// extend storage
Cid = (veci_size(&s->learnts) << 1) | 1;
s->learnts.size += satset_size(nLits);
......@@ -475,7 +475,7 @@ static inline int solver2_enqueue(sat_solver2* s, lit l, cla from)
/*
if ( solver2_dlevel(s) == 0 )
{
satset * c = from ? clause_read( s, from ) : NULL;
satset * c = from ? clause2_read( s, from ) : NULL;
Abc_Print(1, "Enqueing var %d on level %d with reason clause ", v, solver2_dlevel(s) );
if ( c )
satset_print( c );
......@@ -554,7 +554,7 @@ static void solver2_record(sat_solver2* s, veci* cls, int proof_id)
{
lit* begin = veci_begin(cls);
lit* end = begin + veci_size(cls);
cla Cid = clause_create_new(s,begin,end,1, proof_id);
cla Cid = clause2_create_new(s,begin,end,1, proof_id);
assert(veci_size(cls) > 0);
if ( veci_size(cls) == 1 )
{
......@@ -607,7 +607,7 @@ void Solver::analyzeFinal(satset* confl, bool skip_first)
Var x = var(trail[i]);
if (seen[x]){
GClause r = reason[x];
if (r == GClause_NULL){
if (r == Gclause2_NULL){
assert(level[x] > 0);
conflict.push(~trail[i]);
}else{
......@@ -647,7 +647,7 @@ 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--){
x = lit_var(s->trail[i]);
if (var_tag(s,x)){
satset* c = clause_read(s, var_reason(s,x));
satset* c = clause2_read(s, var_reason(s,x));
if (c){
proof_chain_resolve( s, c, x );
satset_foreach_var( c, x, j, 1 ){
......@@ -680,7 +680,7 @@ static int solver2_lit_removable_rec(sat_solver2* s, int v)
return (var_tag(s,v) & 4) > 0;
// skip decisions on a wrong level
c = clause_read(s, var_reason(s,v));
c = clause2_read(s, var_reason(s,v));
if ( c == NULL ){
var_add_tag(s,v,2);
return 0;
......@@ -730,7 +730,7 @@ static int solver2_lit_removable(sat_solver2* s, int x)
veci_push(&s->stack, x ^ 1 );
}
x >>= 1;
c = clause_read(s, var_reason(s,x));
c = clause2_read(s, var_reason(s,x));
satset_foreach_var( c, x, i, 1 ){
if (var_tag(s,x) || !var_level(s,x))
continue;
......@@ -763,7 +763,7 @@ static void solver2_logging_order(sat_solver2* s, int x)
}
veci_push(&s->stack, x ^ 1 );
x >>= 1;
c = clause_read(s, var_reason(s,x));
c = clause2_read(s, var_reason(s,x));
// if ( !c )
// Abc_Print(1, "solver2_logging_order(): Error in conflict analysis!!!\n" );
satset_foreach_var( c, x, i, 1 ){
......@@ -781,7 +781,7 @@ static void solver2_logging_order_rec(sat_solver2* s, int x)
int i, y;
if ( (var_tag(s,x) & 8) )
return;
c = clause_read(s, var_reason(s,x));
c = clause2_read(s, var_reason(s,x));
satset_foreach_var( c, y, i, 1 )
if ( var_level(s,y) && (var_tag(s,y) & 1) == 0 )
solver2_logging_order_rec(s, y);
......@@ -806,7 +806,7 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
while ( 1 ){
assert(c != 0);
if (c->learnt)
act_clause_bump(s,c);
act_clause2_bump(s,c);
satset_foreach_var( c, x, j, (int)(p > 0) ){
assert(x >= 0 && x < s->size);
if ( var_tag(s, x) )
......@@ -827,7 +827,7 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
while (!var_tag(s, lit_var(s->trail[ind--])));
p = s->trail[ind+1];
c = clause_read(s, lit_reason(s,p));
c = clause2_read(s, lit_reason(s,p));
cnt--;
if ( cnt == 0 )
break;
......@@ -862,7 +862,7 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
// add them in the reverse order
vars = veci_begin(&s->min_step_order);
for (i = veci_size(&s->min_step_order); i > 0; ) { i--;
c = clause_read(s, var_reason(s,vars[i]));
c = clause2_read(s, var_reason(s,vars[i]));
proof_chain_resolve( s, c, vars[i] );
satset_foreach_var(c, x, k, 1)
if ( var_level(s,x) == 0 )
......@@ -930,7 +930,7 @@ satset* solver2_propagate(sat_solver2* s)
s->stats.propagations++;
for (i = j = begin; i < end; ){
c = clause_read(s,*i);
c = clause2_read(s,*i);
lits = c->pEnts;
// Make sure the false literal is data[1]:
......@@ -968,7 +968,7 @@ satset* solver2_propagate(sat_solver2* s)
}
proof_id = proof_chain_stop( s );
// get a new clause
Cid = clause_create_new( s, &Lit, &Lit + 1, 1, proof_id );
Cid = clause2_create_new( s, &Lit, &Lit + 1, 1, proof_id );
assert( (var_unit_clause(s, Var) == NULL) != fLitIsFalse );
// if variable already has unit clause, it must be with the other polarity
// in this case, we should derive the empty clause here
......@@ -976,18 +976,18 @@ satset* solver2_propagate(sat_solver2* s)
var_set_unit_clause(s, Var, Cid);
else{
// Empty clause derived:
proof_chain_start( s, clause_read(s,Cid) );
proof_chain_start( s, clause2_read(s,Cid) );
proof_chain_resolve( s, NULL, Var );
proof_id = proof_chain_stop( s );
s->hProofLast = proof_id;
// clause_create_new( s, &Lit, &Lit, 1, proof_id );
// clause2_create_new( s, &Lit, &Lit, 1, proof_id );
}
}
*j++ = *i;
// Clause is unit under assignment:
if (!solver2_enqueue(s,Lit, *i)){
confl = clause_read(s,*i++);
confl = clause2_read(s,*i++);
// Copy the remaining watches:
while (i < end)
*j++ = *i++;
......@@ -1052,7 +1052,7 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
if ( learnt_clause.size == 1 )
var_set_level( s, lit_var(learnt_clause.ptr[0]), 0 );
act_var_decay(s);
act_clause_decay(s);
act_clause2_decay(s);
}else{
// NO CONFLICT
......@@ -1327,7 +1327,7 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end)
assert( i == begin || lit_var(*(i-1)) != lit_var(*i) );
// consider the value of this literal
if ( var_value(s, lit_var(*i)) == lit_sign(*i) ) // this clause is always true
return clause_create_new( s, begin, end, 0, 0 ); // add it anyway, to preserve proper clause count
return clause2_create_new( s, begin, end, 0, 0 ); // add it anyway, to preserve proper clause count
if ( var_value(s, lit_var(*i)) == varX ) // unassigned literal
iFree = i;
else
......@@ -1341,7 +1341,7 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end)
*begin = temp;
// create a new clause
Cid = clause_create_new( s, begin, end, 0, 0 );
Cid = clause2_create_new( s, begin, end, 0, 0 );
// handle unit clause
if ( count+1 == end-begin )
......@@ -1358,13 +1358,13 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end)
{
// Log production of top-level unit clause:
int x, k, proof_id, CidNew;
satset* c = clause_read(s, Cid);
satset* c = clause2_read(s, Cid);
proof_chain_start( s, c );
satset_foreach_var( c, x, k, 1 )
proof_chain_resolve( s, NULL, x );
proof_id = proof_chain_stop( s );
// generate a new clause
CidNew = clause_create_new( s, begin, begin+1, 1, proof_id );
CidNew = clause2_create_new( s, begin, begin+1, 1, proof_id );
var_set_unit_clause( s, lit_var(begin[0]), CidNew );
if ( !solver2_enqueue(s,begin[0],Cid) )
assert( 0 );
......@@ -1458,7 +1458,7 @@ void sat_solver2_reducedb(sat_solver2* s)
for ( i = 0; i < s->size; i++ )
if ( s->reasons[i] && (s->reasons[i] & 1) )
{
c = clause_read( s, s->reasons[i] );
c = clause2_read( s, s->reasons[i] );
assert( c->mark == 0 );
s->reasons[i] = (c->Id << 1) | 1;
}
......@@ -1470,7 +1470,7 @@ void sat_solver2_reducedb(sat_solver2* s)
for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
if ( !(pArray[k] & 1) ) // problem clause
pArray[j++] = pArray[k];
else if ( !(c = clause_read(s, pArray[k]))->mark ) // useful learned clause
else if ( !(c = clause2_read(s, pArray[k]))->mark ) // useful learned clause
pArray[j++] = (c->Id << 1) | 1;
veci_resize(&s->wlists[i],j);
}
......@@ -1479,7 +1479,7 @@ void sat_solver2_reducedb(sat_solver2* s)
for ( i = 0; i < s->size; i++ )
if ( s->units[i] && (s->units[i] & 1) )
{
c = clause_read( s, s->units[i] );
c = clause2_read( s, s->units[i] );
assert( c->mark == 0 );
s->units[i] = (c->Id << 1) | 1;
}
......@@ -1544,7 +1544,7 @@ void sat_solver2_rollback( sat_solver2* s )
{
cla* pArray = veci_begin(&s->wlists[i]);
for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
if ( clause_is_used(s, pArray[k]) )
if ( clause2_is_used(s, pArray[k]) )
pArray[j++] = pArray[k];
veci_resize(&s->wlists[i],j);
}
......@@ -1759,7 +1759,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
assert(var(p) < nVars());
if (!solver2_assume(p)){
GClause r = reason[var(p)];
if (r != GClause_NULL){
if (r != Gclause2_NULL){
satset* confl;
if (r.isLit()){
confl = propagate_tmpbin;
......@@ -1792,7 +1792,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
veci_push(&s->trail_lim,s->qtail);
if (!solver2_enqueue(s,p,0))
{
satset* r = clause_read(s, lit_reason(s,p));
satset* r = clause2_read(s, lit_reason(s,p));
if (r != NULL)
{
satset* confl = r;
......
src/sat/bsat/satSolver2.h
......@@ -28,6 +28,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include <string.h>
#include <assert.h>
#include "satClause.h"
#include "satVec.h"
#include "misc/vec/vecSet.h"
......@@ -63,10 +64,10 @@ extern void Sat_Solver2DoubleClauses( sat_solver2 * p, int iVar );
extern int var_is_partA (sat_solver2* s, int v);
extern void var_set_partA(sat_solver2* s, int v, int partA);
// clause grouping (these two only work after creating a clause before the solver is called)
extern int clause_is_partA (sat_solver2* s, int handle);
extern void clause_set_partA(sat_solver2* s, int handle, int partA);
extern int clause2_is_partA (sat_solver2* s, int handle);
extern void clause2_set_partA(sat_solver2* s, int handle, int partA);
// other clause functions
extern int clause_id(sat_solver2* s, int h);
extern int clause2_id(sat_solver2* s, int h);
// proof-based APIs
extern void * Sat_ProofCore( sat_solver2 * s );
......@@ -274,7 +275,7 @@ static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fComp
Lits[0] = toLitCond( iVar, fCompl );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 1 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
clause2_set_partA( pSat, Cid, 1 );
return 1;
}
static inline int sat_solver2_add_buffer( sat_solver2 * pSat, int iVarA, int iVarB, int fCompl, int fMark )
......@@ -287,13 +288,13 @@ static inline int sat_solver2_add_buffer( sat_solver2 * pSat, int iVarA, int iVa
Lits[1] = toLitCond( iVarB, !fCompl );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
clause2_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVarA, 1 );
Lits[1] = toLitCond( iVarB, fCompl );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
clause2_set_partA( pSat, Cid, 1 );
return 2;
}
static inline int sat_solver2_add_and( sat_solver2 * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fMark )
......@@ -305,20 +306,20 @@ static inline int sat_solver2_add_and( sat_solver2 * pSat, int iVar, int iVar0,
Lits[1] = toLitCond( iVar0, fCompl0 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
clause2_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVar, 1 );
Lits[1] = toLitCond( iVar1, fCompl1 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
clause2_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVar, 0 );
Lits[1] = toLitCond( iVar0, !fCompl0 );
Lits[2] = toLitCond( iVar1, !fCompl1 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
clause2_set_partA( pSat, Cid, 1 );
return 3;
}
static inline int sat_solver2_add_xor( sat_solver2 * pSat, int iVarA, int iVarB, int iVarC, int fCompl, int fMark )
......@@ -332,28 +333,28 @@ static inline int sat_solver2_add_xor( sat_solver2 * pSat, int iVarA, int iVarB,
Lits[2] = toLitCond( iVarC, 1 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
clause2_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVarA, !fCompl );
Lits[1] = toLitCond( iVarB, 0 );
Lits[2] = toLitCond( iVarC, 0 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
clause2_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVarA, fCompl );
Lits[1] = toLitCond( iVarB, 1 );
Lits[2] = toLitCond( iVarC, 0 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
clause2_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVarA, fCompl );
Lits[1] = toLitCond( iVarB, 0 );
Lits[2] = toLitCond( iVarC, 1 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
clause2_set_partA( pSat, Cid, 1 );
return 4;
}
static inline int sat_solver2_add_constraint( sat_solver2 * pSat, int iVar, int iVar2, int fCompl, int fMark )
......@@ -366,13 +367,13 @@ static inline int sat_solver2_add_constraint( sat_solver2 * pSat, int iVar, int
Lits[1] = toLitCond( iVar2, 0 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
clause2_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVar, fCompl );
Lits[1] = toLitCond( iVar2, 1 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
clause2_set_partA( pSat, Cid, 1 );
return 2;
}
......
src/sat/bsat/satUtil.c
......@@ -30,14 +30,18 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*
struct clause_t
{
int size_learnt;
unsigned size : 24;
unsigned lbd : 6;
unsigned leant : 1;
unsigned mark : 1;
lit lits[0];
};
static inline int clause_size( clause* c ) { return c->size_learnt >> 1; }
static inline int clause_size( clause* c ) { return c->size; }
static inline lit* clause_begin( clause* c ) { return c->lits; }
*/
static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement );
......@@ -127,6 +131,7 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBe
***********************************************************************/
void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement )
{
/*
lit * pLits = clause_begin(pC);
int nLits = clause_size(pC);
int i;
......@@ -136,6 +141,7 @@ void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement )
if ( fIncrement )
fprintf( pFile, "0" );
fprintf( pFile, "\n" );
*/
}
/**Function*************************************************************
......
src/sat/bsat/satVec.h
......@@ -127,8 +127,6 @@ static inline void vecp_remove(vecp* v, void* e)
#endif
#endif
typedef int lit;
typedef int cla;
typedef char lbool;
static const int var_Undef = -1;
......
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