summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2007-09-30 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2007-09-30 08:01:00 -0700
commite54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (patch)
treede3ffe87c3e17950351e3b7d97fa18318bd5ea9a /src/sat/bsat
parent7d7e60f2dc84393cd4c5db22d2eaf7b1fb1a79b2 (diff)
downloadabc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.tar.gz
abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.tar.bz2
abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.zip
Version abc70930
Diffstat (limited to 'src/sat/bsat')
-rw-r--r--src/sat/bsat/module.make6
-rw-r--r--src/sat/bsat/satInter.c991
-rw-r--r--src/sat/bsat/satMem.c527
-rw-r--r--src/sat/bsat/satMem.h78
-rw-r--r--src/sat/bsat/satSolver.c1358
-rw-r--r--src/sat/bsat/satSolver.h191
-rw-r--r--src/sat/bsat/satStore.c437
-rw-r--r--src/sat/bsat/satStore.h137
-rw-r--r--src/sat/bsat/satTrace.c109
-rw-r--r--src/sat/bsat/satUtil.c234
-rw-r--r--src/sat/bsat/satVec.h83
11 files changed, 0 insertions, 4151 deletions
diff --git a/src/sat/bsat/module.make b/src/sat/bsat/module.make
deleted file mode 100644
index 563c8dfc..00000000
--- a/src/sat/bsat/module.make
+++ /dev/null
@@ -1,6 +0,0 @@
-SRC += src/sat/bsat/satMem.c \
- src/sat/bsat/satInter.c \
- src/sat/bsat/satSolver.c \
- src/sat/bsat/satStore.c \
- src/sat/bsat/satTrace.c \
- src/sat/bsat/satUtil.c
diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c
deleted file mode 100644
index b52cd6c7..00000000
--- a/src/sat/bsat/satInter.c
+++ /dev/null
@@ -1,991 +0,0 @@
-/**CFile****************************************************************
-
- FileName [satInter.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [SAT sat_solver.]
-
- Synopsis [Interpolation package.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: satInter.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
-
-***********************************************************************/
-
-#include <stdio.h>
-#include <stdlib.h>
-#include <string.h>
-#include <assert.h>
-#include <time.h>
-#include "satStore.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-// variable assignments
-static const lit LIT_UNDEF = 0xffffffff;
-
-// interpolation manager
-struct Int_Man_t_
-{
- // clauses of the problems
- Sto_Man_t * pCnf; // the set of CNF clauses for A and B
- // various parameters
- int fVerbose; // verbosiness flag
- int fProofVerif; // verifies the proof
- int fProofWrite; // writes the proof file
- int nVarsAlloc; // the allocated size of var arrays
- int nClosAlloc; // the allocated size of clause arrays
- // internal BCP
- int nRootSize; // the number of root level assignments
- int nTrailSize; // the number of assignments made
- lit * pTrail; // chronological order of assignments (size nVars)
- lit * pAssigns; // assignments by variable (size nVars)
- char * pSeens; // temporary mark (size nVars)
- Sto_Cls_t ** pReasons; // reasons for each assignment (size nVars)
- Sto_Cls_t ** pWatches; // watched clauses for each literal (size 2*nVars)
- // interpolation data
- int nVarsAB; // the number of global variables
- char * pVarTypes; // variable type (size nVars) [1=A, 0=B, <0=AB]
- unsigned * pInters; // storage for interpolants as truth tables (size nClauses)
- int nIntersAlloc; // the allocated size of truth table array
- int nWords; // the number of words in the truth table
- // proof recording
- int Counter; // counter of resolved clauses
- int * pProofNums; // the proof numbers for each clause (size nClauses)
- FILE * pFile; // the file for proof recording
- // internal verification
- lit * pResLits; // the literals of the resolvent
- int nResLits; // the number of literals of the resolvent
- int nResLitsAlloc;// the number of literals of the resolvent
- // runtime stats
- int timeBcp; // the runtime for BCP
- int timeTrace; // the runtime of trace construction
- int timeTotal; // the total runtime of interpolation
-};
-
-// procedure to get hold of the clauses' truth table
-static inline unsigned * Int_ManTruthRead( Int_Man_t * p, Sto_Cls_t * pCls ) { return p->pInters + pCls->Id * p->nWords; }
-static inline void Int_ManTruthClear( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = 0; }
-static inline void Int_ManTruthFill( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = ~0; }
-static inline void Int_ManTruthCopy( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = q[i]; }
-static inline void Int_ManTruthAnd( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] &= q[i]; }
-static inline void Int_ManTruthOr( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= q[i]; }
-static inline void Int_ManTruthOrNot( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= ~q[i]; }
-
-// reading/writing the proof for a clause
-static inline int Int_ManProofGet( Int_Man_t * p, Sto_Cls_t * pCls ) { return p->pProofNums[pCls->Id]; }
-static inline void Int_ManProofSet( Int_Man_t * p, Sto_Cls_t * pCls, int n ) { p->pProofNums[pCls->Id] = n; }
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Allocate proof manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Int_Man_t * Int_ManAlloc( int nVarsAlloc )
-{
- Int_Man_t * p;
- // allocate the manager
- p = (Int_Man_t *)malloc( sizeof(Int_Man_t) );
- memset( p, 0, sizeof(Int_Man_t) );
- // verification
- p->nResLitsAlloc = (1<<16);
- p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc );
- // parameters
- p->fProofWrite = 0;
- p->fProofVerif = 1;
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis [Count common variables in the clauses of A and B.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Int_ManGlobalVars( Int_Man_t * p )
-{
- Sto_Cls_t * pClause;
- int Var, nVarsAB, v;
-
- // mark the variable encountered in the clauses of A
- Sto_ManForEachClauseRoot( p->pCnf, pClause )
- {
- if ( !pClause->fA )
- break;
- for ( v = 0; v < (int)pClause->nLits; v++ )
- p->pVarTypes[lit_var(pClause->pLits[v])] = 1;
- }
-
- // check variables that appear in clauses of B
- nVarsAB = 0;
- Sto_ManForEachClauseRoot( p->pCnf, pClause )
- {
- if ( pClause->fA )
- continue;
- for ( v = 0; v < (int)pClause->nLits; v++ )
- {
- Var = lit_var(pClause->pLits[v]);
- if ( p->pVarTypes[Var] == 1 ) // var of A
- {
- // change it into a global variable
- nVarsAB++;
- p->pVarTypes[Var] = -1;
- }
- }
- }
-
- // order global variables
- nVarsAB = 0;
- for ( v = 0; v < p->pCnf->nVars; v++ )
- if ( p->pVarTypes[v] == -1 )
- p->pVarTypes[v] -= nVarsAB++;
-//printf( "There are %d global variables.\n", nVarsAB );
- return nVarsAB;
-}
-
-/**Function*************************************************************
-
- Synopsis [Resize proof manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Int_ManResize( Int_Man_t * p )
-{
- // check if resizing is needed
- if ( p->nVarsAlloc < p->pCnf->nVars )
- {
- // find the new size
- if ( p->nVarsAlloc == 0 )
- p->nVarsAlloc = 1;
- while ( p->nVarsAlloc < p->pCnf->nVars )
- p->nVarsAlloc *= 2;
- // resize the arrays
- p->pTrail = (lit *) realloc( p->pTrail, sizeof(lit) * p->nVarsAlloc );
- p->pAssigns = (lit *) realloc( p->pAssigns, sizeof(lit) * p->nVarsAlloc );
- p->pSeens = (char *) realloc( p->pSeens, sizeof(char) * p->nVarsAlloc );
- p->pVarTypes = (char *) realloc( p->pVarTypes, sizeof(char) * p->nVarsAlloc );
- p->pReasons = (Sto_Cls_t **)realloc( p->pReasons, sizeof(Sto_Cls_t *) * p->nVarsAlloc );
- p->pWatches = (Sto_Cls_t **)realloc( p->pWatches, sizeof(Sto_Cls_t *) * p->nVarsAlloc*2 );
- }
-
- // clean the free space
- memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars );
- memset( p->pSeens , 0, sizeof(char) * p->pCnf->nVars );
- memset( p->pVarTypes, 0, sizeof(char) * p->pCnf->nVars );
- memset( p->pReasons , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars );
- memset( p->pWatches , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 );
-
- // compute the number of common variables
- p->nVarsAB = Int_ManGlobalVars( p );
- // compute the number of words in the truth table
- p->nWords = (p->nVarsAB <= 5 ? 1 : (1 << (p->nVarsAB - 5)));
-
- // check if resizing of clauses is needed
- if ( p->nClosAlloc < p->pCnf->nClauses )
- {
- // find the new size
- if ( p->nClosAlloc == 0 )
- p->nClosAlloc = 1;
- while ( p->nClosAlloc < p->pCnf->nClauses )
- p->nClosAlloc *= 2;
- // resize the arrays
- p->pProofNums = (int *) realloc( p->pProofNums, sizeof(int) * p->nClosAlloc );
- }
- memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses );
-
- // check if resizing of truth tables is needed
- if ( p->nIntersAlloc < p->nWords * p->pCnf->nClauses )
- {
- p->nIntersAlloc = p->nWords * p->pCnf->nClauses;
- p->pInters = (unsigned *) realloc( p->pInters, sizeof(unsigned) * p->nIntersAlloc );
- }
-// memset( p->pInters, 0, sizeof(unsigned) * p->nWords * p->pCnf->nClauses );
-}
-
-/**Function*************************************************************
-
- Synopsis [Deallocate proof manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Int_ManFree( Int_Man_t * p )
-{
-/*
- printf( "Runtime stats:\n" );
-PRT( "BCP ", p->timeBcp );
-PRT( "Trace ", p->timeTrace );
-PRT( "TOTAL ", p->timeTotal );
-*/
- free( p->pInters );
- free( p->pProofNums );
- free( p->pTrail );
- free( p->pAssigns );
- free( p->pSeens );
- free( p->pVarTypes );
- free( p->pReasons );
- free( p->pWatches );
- free( p->pResLits );
- free( p );
-}
-
-
-
-
-/**Function*************************************************************
-
- Synopsis [Prints the clause.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Int_ManPrintClause( Int_Man_t * p, Sto_Cls_t * pClause )
-{
- int i;
- printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Int_ManProofGet(p, pClause) );
- for ( i = 0; i < (int)pClause->nLits; i++ )
- printf( " %d", pClause->pLits[i] );
- printf( " }\n" );
-}
-
-/**Function*************************************************************
-
- Synopsis [Prints the resolvent.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Int_ManPrintResolvent( lit * pResLits, int nResLits )
-{
- int i;
- printf( "Resolvent: {" );
- for ( i = 0; i < nResLits; i++ )
- printf( " %d", pResLits[i] );
- printf( " }\n" );
-}
-
-/**Function*************************************************************
-
- Synopsis [Records the proof.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Extra_PrintBinary__( FILE * pFile, unsigned Sign[], int nBits )
-{
- int Remainder, nWords;
- int w, i;
-
- Remainder = (nBits%(sizeof(unsigned)*8));
- nWords = (nBits/(sizeof(unsigned)*8)) + (Remainder>0);
-
- for ( w = nWords-1; w >= 0; w-- )
- for ( i = ((w == nWords-1 && Remainder)? Remainder-1: 31); i >= 0; i-- )
- fprintf( pFile, "%c", '0' + (int)((Sign[w] & (1<<i)) > 0) );
-}
-
-/**Function*************************************************************
-
- Synopsis [Prints the interpolant for one clause.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Int_ManPrintInterOne( Int_Man_t * p, Sto_Cls_t * pClause )
-{
- printf( "Clause %2d : ", pClause->Id );
- Extra_PrintBinary__( stdout, Int_ManTruthRead(p, pClause), (1 << p->nVarsAB) );
- printf( "\n" );
-}
-
-
-
-/**Function*************************************************************
-
- Synopsis [Adds one clause to the watcher list.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Int_ManWatchClause( Int_Man_t * p, Sto_Cls_t * pClause, lit Lit )
-{
- assert( lit_check(Lit, p->pCnf->nVars) );
- if ( pClause->pLits[0] == Lit )
- pClause->pNext0 = p->pWatches[lit_neg(Lit)];
- else
- {
- assert( pClause->pLits[1] == Lit );
- pClause->pNext1 = p->pWatches[lit_neg(Lit)];
- }
- p->pWatches[lit_neg(Lit)] = pClause;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Records implication.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Int_ManEnqueue( Int_Man_t * p, lit Lit, Sto_Cls_t * pReason )
-{
- int Var = lit_var(Lit);
- if ( p->pAssigns[Var] != LIT_UNDEF )
- return p->pAssigns[Var] == Lit;
- p->pAssigns[Var] = Lit;
- p->pReasons[Var] = pReason;
- p->pTrail[p->nTrailSize++] = Lit;
-//printf( "assigning var %d value %d\n", Var, !lit_sign(Lit) );
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Records implication.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Int_ManCancelUntil( Int_Man_t * p, int Level )
-{
- lit Lit;
- int i, Var;
- for ( i = p->nTrailSize - 1; i >= Level; i-- )
- {
- Lit = p->pTrail[i];
- Var = lit_var( Lit );
- p->pReasons[Var] = NULL;
- p->pAssigns[Var] = LIT_UNDEF;
-//printf( "cancelling var %d\n", Var );
- }
- p->nTrailSize = Level;
-}
-
-/**Function*************************************************************
-
- Synopsis [Propagate one assignment.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline Sto_Cls_t * Int_ManPropagateOne( Int_Man_t * p, lit Lit )
-{
- Sto_Cls_t ** ppPrev, * pCur, * pTemp;
- lit LitF = lit_neg(Lit);
- int i;
- // iterate through the literals
- ppPrev = p->pWatches + Lit;
- for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev )
- {
- // make sure the false literal is in the second literal of the clause
- if ( pCur->pLits[0] == LitF )
- {
- pCur->pLits[0] = pCur->pLits[1];
- pCur->pLits[1] = LitF;
- pTemp = pCur->pNext0;
- pCur->pNext0 = pCur->pNext1;
- pCur->pNext1 = pTemp;
- }
- assert( pCur->pLits[1] == LitF );
-
- // if the first literal is true, the clause is satisfied
- if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] )
- {
- ppPrev = &pCur->pNext1;
- continue;
- }
-
- // look for a new literal to watch
- for ( i = 2; i < (int)pCur->nLits; i++ )
- {
- // skip the case when the literal is false
- if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] )
- continue;
- // the literal is either true or unassigned - watch it
- pCur->pLits[1] = pCur->pLits[i];
- pCur->pLits[i] = LitF;
- // remove this clause from the watch list of Lit
- *ppPrev = pCur->pNext1;
- // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1])
- Int_ManWatchClause( p, pCur, pCur->pLits[1] );
- break;
- }
- if ( i < (int)pCur->nLits ) // found new watch
- continue;
-
- // clause is unit - enqueue new implication
- if ( Int_ManEnqueue(p, pCur->pLits[0], pCur) )
- {
- ppPrev = &pCur->pNext1;
- continue;
- }
-
- // conflict detected - return the conflict clause
- return pCur;
- }
- return NULL;
-}
-
-/**Function*************************************************************
-
- Synopsis [Propagate the current assignments.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Sto_Cls_t * Int_ManPropagate( Int_Man_t * p, int Start )
-{
- Sto_Cls_t * pClause;
- int i;
- int clk = clock();
- for ( i = Start; i < p->nTrailSize; i++ )
- {
- pClause = Int_ManPropagateOne( p, p->pTrail[i] );
- if ( pClause )
- {
-p->timeBcp += clock() - clk;
- return pClause;
- }
- }
-p->timeBcp += clock() - clk;
- return NULL;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Writes one root clause into a file.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Int_ManProofWriteOne( Int_Man_t * p, Sto_Cls_t * pClause )
-{
- Int_ManProofSet( p, pClause, ++p->Counter );
-
- if ( p->fProofWrite )
- {
- int v;
- fprintf( p->pFile, "%d", Int_ManProofGet(p, pClause) );
- for ( v = 0; v < (int)pClause->nLits; v++ )
- fprintf( p->pFile, " %d", lit_print(pClause->pLits[v]) );
- fprintf( p->pFile, " 0 0\n" );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Traces the proof for one clause.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFinal )
-{
- Sto_Cls_t * pReason;
- int i, v, Var, PrevId;
- int fPrint = 0;
- int clk = clock();
-
- // collect resolvent literals
- if ( p->fProofVerif )
- {
- assert( (int)pConflict->nLits <= p->nResLitsAlloc );
- memcpy( p->pResLits, pConflict->pLits, sizeof(lit) * pConflict->nLits );
- p->nResLits = pConflict->nLits;
- }
-
- // mark all the variables in the conflict as seen
- for ( v = 0; v < (int)pConflict->nLits; v++ )
- p->pSeens[lit_var(pConflict->pLits[v])] = 1;
-
- // start the anticedents
-// pFinal->pAntis = Vec_PtrAlloc( 32 );
-// Vec_PtrPush( pFinal->pAntis, pConflict );
-
- if ( p->pCnf->nClausesA )
- Int_ManTruthCopy( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pConflict), p->nWords );
-
- // follow the trail backwards
- PrevId = Int_ManProofGet(p, pConflict);
- for ( i = p->nTrailSize - 1; i >= 0; i-- )
- {
- // skip literals that are not involved
- Var = lit_var(p->pTrail[i]);
- if ( !p->pSeens[Var] )
- continue;
- p->pSeens[Var] = 0;
-
- // skip literals of the resulting clause
- pReason = p->pReasons[Var];
- if ( pReason == NULL )
- continue;
- assert( p->pTrail[i] == pReason->pLits[0] );
-
- // add the variables to seen
- for ( v = 1; v < (int)pReason->nLits; v++ )
- p->pSeens[lit_var(pReason->pLits[v])] = 1;
-
-
- // record the reason clause
- assert( Int_ManProofGet(p, pReason) > 0 );
- p->Counter++;
- if ( p->fProofWrite )
- fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Int_ManProofGet(p, pReason) );
- PrevId = p->Counter;
-
- if ( p->pCnf->nClausesA )
- {
- if ( p->pVarTypes[Var] == 1 ) // var of A
- Int_ManTruthOr( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pReason), p->nWords );
- else
- Int_ManTruthAnd( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pReason), p->nWords );
- }
-
- // resolve the temporary resolvent with the reason clause
- if ( p->fProofVerif )
- {
- int v1, v2;
- if ( fPrint )
- Int_ManPrintResolvent( p->pResLits, p->nResLits );
- // check that the var is present in the resolvent
- for ( v1 = 0; v1 < p->nResLits; v1++ )
- if ( lit_var(p->pResLits[v1]) == Var )
- break;
- if ( v1 == p->nResLits )
- printf( "Recording clause %d: Cannot find variable %d in the temporary resolvent.\n", pFinal->Id, Var );
- if ( p->pResLits[v1] != lit_neg(pReason->pLits[0]) )
- printf( "Recording clause %d: The resolved variable %d is in the wrong polarity.\n", pFinal->Id, Var );
- // remove this variable from the resolvent
- assert( lit_var(p->pResLits[v1]) == Var );
- p->nResLits--;
- for ( ; v1 < p->nResLits; v1++ )
- p->pResLits[v1] = p->pResLits[v1+1];
- // add variables of the reason clause
- for ( v2 = 1; v2 < (int)pReason->nLits; v2++ )
- {
- for ( v1 = 0; v1 < p->nResLits; v1++ )
- if ( lit_var(p->pResLits[v1]) == lit_var(pReason->pLits[v2]) )
- break;
- // if it is a new variable, add it to the resolvent
- if ( v1 == p->nResLits )
- {
- if ( p->nResLits == p->nResLitsAlloc )
- printf( "Recording clause %d: Ran out of space for intermediate resolvent.\n, pFinal->Id" );
- p->pResLits[ p->nResLits++ ] = pReason->pLits[v2];
- continue;
- }
- // if the variable is the same, the literal should be the same too
- if ( p->pResLits[v1] == pReason->pLits[v2] )
- continue;
- // the literal is different
- printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id );
- }
- }
-
-// Vec_PtrPush( pFinal->pAntis, pReason );
- }
-
- // unmark all seen variables
-// for ( i = p->nTrailSize - 1; i >= 0; i-- )
-// p->pSeens[lit_var(p->pTrail[i])] = 0;
- // check that the literals are unmarked
-// for ( i = p->nTrailSize - 1; i >= 0; i-- )
-// assert( p->pSeens[lit_var(p->pTrail[i])] == 0 );
-
- // use the resulting clause to check the correctness of resolution
- if ( p->fProofVerif )
- {
- int v1, v2;
- if ( fPrint )
- Int_ManPrintResolvent( p->pResLits, p->nResLits );
- for ( v1 = 0; v1 < p->nResLits; v1++ )
- {
- for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ )
- if ( pFinal->pLits[v2] == p->pResLits[v1] )
- break;
- if ( v2 < (int)pFinal->nLits )
- continue;
- break;
- }
- if ( v1 < p->nResLits )
- {
- printf( "Recording clause %d: The final resolvent is wrong.\n", pFinal->Id );
- Int_ManPrintClause( p, pConflict );
- Int_ManPrintResolvent( p->pResLits, p->nResLits );
- Int_ManPrintClause( p, pFinal );
- }
- }
-p->timeTrace += clock() - clk;
-
- // return the proof pointer
- if ( p->pCnf->nClausesA )
- {
-// Int_ManPrintInterOne( p, pFinal );
- }
- Int_ManProofSet( p, pFinal, p->Counter );
- return p->Counter;
-}
-
-/**Function*************************************************************
-
- Synopsis [Records the proof for one clause.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Int_ManProofRecordOne( Int_Man_t * p, Sto_Cls_t * pClause )
-{
- Sto_Cls_t * pConflict;
- int i;
-
- // empty clause never ends up there
- assert( pClause->nLits > 0 );
- if ( pClause->nLits == 0 )
- printf( "Error: Empty clause is attempted.\n" );
-
- // add assumptions to the trail
- assert( !pClause->fRoot );
- assert( p->nTrailSize == p->nRootSize );
- for ( i = 0; i < (int)pClause->nLits; i++ )
- if ( !Int_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
- {
- assert( 0 ); // impossible
- return 0;
- }
-
- // propagate the assumptions
- pConflict = Int_ManPropagate( p, p->nRootSize );
- if ( pConflict == NULL )
- {
- assert( 0 ); // cannot prove
- return 0;
- }
-
- // construct the proof
- Int_ManProofTraceOne( p, pConflict, pClause );
-
- // undo to the root level
- Int_ManCancelUntil( p, p->nRootSize );
-
- // add large clauses to the watched lists
- if ( pClause->nLits > 1 )
- {
- Int_ManWatchClause( p, pClause, pClause->pLits[0] );
- Int_ManWatchClause( p, pClause, pClause->pLits[1] );
- return 1;
- }
- assert( pClause->nLits == 1 );
-
- // if the clause proved is unit, add it and propagate
- if ( !Int_ManEnqueue( p, pClause->pLits[0], pClause ) )
- {
- assert( 0 ); // impossible
- return 0;
- }
-
- // propagate the assumption
- pConflict = Int_ManPropagate( p, p->nRootSize );
- if ( pConflict )
- {
- // construct the proof
- Int_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty );
- if ( p->fVerbose )
- printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id );
- return 0;
- }
-
- // update the root level
- p->nRootSize = p->nTrailSize;
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Propagate the root clauses.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Int_ManProcessRoots( Int_Man_t * p )
-{
- Sto_Cls_t * pClause;
- int Counter;
-
- // make sure the root clauses are preceeding the learnt clauses
- Counter = 0;
- Sto_ManForEachClause( p->pCnf, pClause )
- {
- assert( (int)pClause->fA == (Counter < (int)p->pCnf->nClausesA) );
- assert( (int)pClause->fRoot == (Counter < (int)p->pCnf->nRoots) );
- Counter++;
- }
- assert( p->pCnf->nClauses == Counter );
-
- // make sure the last clause if empty
- assert( p->pCnf->pTail->nLits == 0 );
-
- // go through the root unit clauses
- p->nTrailSize = 0;
- Sto_ManForEachClauseRoot( p->pCnf, pClause )
- {
- // create watcher lists for the root clauses
- if ( pClause->nLits > 1 )
- {
- Int_ManWatchClause( p, pClause, pClause->pLits[0] );
- Int_ManWatchClause( p, pClause, pClause->pLits[1] );
- }
- // empty clause and large clauses
- if ( pClause->nLits != 1 )
- continue;
- // unit clause
- assert( lit_check(pClause->pLits[0], p->pCnf->nVars) );
- if ( !Int_ManEnqueue( p, pClause->pLits[0], pClause ) )
- {
- // detected root level conflict
- printf( "Error in Int_ManProcessRoots(): Detected a root-level conflict too early!\n" );
- assert( 0 );
- return 0;
- }
- }
-
- // propagate the root unit clauses
- pClause = Int_ManPropagate( p, 0 );
- if ( pClause )
- {
- // detected root level conflict
- Int_ManProofTraceOne( p, pClause, p->pCnf->pEmpty );
- if ( p->fVerbose )
- printf( "Found root level conflict!\n" );
- return 0;
- }
-
- // set the root level
- p->nRootSize = p->nTrailSize;
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Records the proof.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Int_ManPrepareInter( Int_Man_t * p )
-{
- // elementary truth tables
- unsigned uTruths[8][8] = {
- { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
- { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
- { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
- { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
- { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 },
- { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF },
- { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF },
- { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF }
- };
- Sto_Cls_t * pClause;
- int Var, VarAB, v;
- assert( p->nVarsAB <= 8 );
-
- // set interpolants for root clauses
- Sto_ManForEachClauseRoot( p->pCnf, pClause )
- {
- if ( !pClause->fA ) // clause of B
- {
- Int_ManTruthFill( Int_ManTruthRead(p, pClause), p->nWords );
-// Int_ManPrintInterOne( p, pClause );
- continue;
- }
- // clause of A
- Int_ManTruthClear( Int_ManTruthRead(p, pClause), p->nWords );
- for ( v = 0; v < (int)pClause->nLits; v++ )
- {
- Var = lit_var(pClause->pLits[v]);
- if ( p->pVarTypes[Var] < 0 ) // global var
- {
- VarAB = -p->pVarTypes[Var]-1;
- assert( VarAB >= 0 && VarAB < p->nVarsAB );
- if ( lit_sign(pClause->pLits[v]) ) // negative var
- Int_ManTruthOrNot( Int_ManTruthRead(p, pClause), uTruths[VarAB], p->nWords );
- else
- Int_ManTruthOr( Int_ManTruthRead(p, pClause), uTruths[VarAB], p->nWords );
- }
- }
-// Int_ManPrintInterOne( p, pClause );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes interpolant for the given CNF.]
-
- Description [Returns the number of common variable found and interpolant.
- Returns 0, if something did not work.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult )
-{
- Sto_Cls_t * pClause;
- int RetValue = 1;
- int clkTotal = clock();
-
- // check that the CNF makes sense
- assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
- p->pCnf = pCnf;
- p->fVerbose = fVerbose;
- *ppResult = NULL;
-
- // adjust the manager
- Int_ManResize( p );
-
- // prepare the interpolant computation
- Int_ManPrepareInter( p );
-
- // construct proof for each clause
- // start the proof
- if ( p->fProofWrite )
- {
- p->pFile = fopen( "proof.cnf_", "w" );
- p->Counter = 0;
- }
-
- // write the root clauses
- Sto_ManForEachClauseRoot( p->pCnf, pClause )
- Int_ManProofWriteOne( p, pClause );
-
- // propagate root level assignments
- if ( Int_ManProcessRoots( p ) )
- {
- // if there is no conflict, consider learned clauses
- Sto_ManForEachClause( p->pCnf, pClause )
- {
- if ( pClause->fRoot )
- continue;
- if ( !Int_ManProofRecordOne( p, pClause ) )
- {
- RetValue = 0;
- break;
- }
- }
- }
-
- // stop the proof
- if ( p->fProofWrite )
- {
- fclose( p->pFile );
- p->pFile = NULL;
- }
-
- if ( fVerbose )
- {
- printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n",
- p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,
- 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots),
- 1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
-p->timeTotal += clock() - clkTotal;
- }
-
- *ppResult = Int_ManTruthRead( p, p->pCnf->pTail );
- return p->nVarsAB;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/bsat/satMem.c b/src/sat/bsat/satMem.c
deleted file mode 100644
index bb234f66..00000000
--- a/src/sat/bsat/satMem.c
+++ /dev/null
@@ -1,527 +0,0 @@
-/**CFile****************************************************************
-
- FileName [satMem.c]
-
- 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.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "satMem.h"
-#include "extra.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-struct Sat_MmFixed_t_
-{
- // information about individual entries
- int nEntrySize; // the size of one entry
- int nEntriesAlloc; // the total number of entries allocated
- int nEntriesUsed; // the number of entries in use
- int nEntriesMax; // the max number of entries in use
- char * pEntriesFree; // the linked list of free entries
-
- // this is where the memory is stored
- int nChunkSize; // the size of one chunk
- int nChunksAlloc; // the maximum number of memory chunks
- int nChunks; // the current number of memory chunks
- char ** pChunks; // the allocated memory
-
- // statistics
- int nMemoryUsed; // memory used in the allocated entries
- int nMemoryAlloc; // memory allocated
-};
-
-struct Sat_MmFlex_t_
-{
- // information about individual entries
- int nEntriesUsed; // the number of entries allocated
- char * pCurrent; // the current pointer to free memory
- char * pEnd; // the first entry outside the free memory
-
- // this is where the memory is stored
- int nChunkSize; // the size of one chunk
- int nChunksAlloc; // the maximum number of memory chunks
- int nChunks; // the current number of memory chunks
- char ** pChunks; // the allocated memory
-
- // statistics
- int nMemoryUsed; // memory used in the allocated entries
- int nMemoryAlloc; // memory allocated
-};
-
-struct Sat_MmStep_t_
-{
- int nMems; // the number of fixed memory managers employed
- Sat_MmFixed_t ** pMems; // memory managers: 2^1 words, 2^2 words, etc
- int nMapSize; // the size of the memory array
- Sat_MmFixed_t ** pMap; // maps the number of bytes into its memory manager
-};
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Allocates memory pieces of fixed size.]
-
- Description [The size of the chunk is computed as the minimum of
- 1024 entries and 64K. Can only work with entry size at least 4 byte long.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Sat_MmFixed_t * Sat_MmFixedStart( int nEntrySize )
-{
- Sat_MmFixed_t * p;
-
- p = ALLOC( Sat_MmFixed_t, 1 );
- memset( p, 0, sizeof(Sat_MmFixed_t) );
-
- p->nEntrySize = nEntrySize;
- p->nEntriesAlloc = 0;
- p->nEntriesUsed = 0;
- p->pEntriesFree = NULL;
-
- if ( nEntrySize * (1 << 10) < (1<<16) )
- p->nChunkSize = (1 << 10);
- else
- p->nChunkSize = (1<<16) / nEntrySize;
- if ( p->nChunkSize < 8 )
- p->nChunkSize = 8;
-
- p->nChunksAlloc = 64;
- p->nChunks = 0;
- p->pChunks = ALLOC( char *, p->nChunksAlloc );
-
- p->nMemoryUsed = 0;
- p->nMemoryAlloc = 0;
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sat_MmFixedStop( Sat_MmFixed_t * p, int fVerbose )
-{
- int i;
- if ( p == NULL )
- return;
- if ( fVerbose )
- {
- printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n",
- p->nEntrySize, p->nChunkSize, p->nChunks );
- printf( " Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n",
- p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc );
- }
- for ( i = 0; i < p->nChunks; i++ )
- free( p->pChunks[i] );
- free( p->pChunks );
- free( p );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-char * Sat_MmFixedEntryFetch( Sat_MmFixed_t * p )
-{
- char * pTemp;
- int i;
-
- // check if there are still free entries
- if ( p->nEntriesUsed == p->nEntriesAlloc )
- { // need to allocate more entries
- assert( p->pEntriesFree == NULL );
- if ( p->nChunks == p->nChunksAlloc )
- {
- p->nChunksAlloc *= 2;
- p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc );
- }
- p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize );
- p->nMemoryAlloc += p->nEntrySize * p->nChunkSize;
- // transform these entries into a linked list
- pTemp = p->pEntriesFree;
- for ( i = 1; i < p->nChunkSize; i++ )
- {
- *((char **)pTemp) = pTemp + p->nEntrySize;
- pTemp += p->nEntrySize;
- }
- // set the last link
- *((char **)pTemp) = NULL;
- // add the chunk to the chunk storage
- p->pChunks[ p->nChunks++ ] = p->pEntriesFree;
- // add to the number of entries allocated
- p->nEntriesAlloc += p->nChunkSize;
- }
- // incrememt the counter of used entries
- p->nEntriesUsed++;
- if ( p->nEntriesMax < p->nEntriesUsed )
- p->nEntriesMax = p->nEntriesUsed;
- // return the first entry in the free entry list
- pTemp = p->pEntriesFree;
- p->pEntriesFree = *((char **)pTemp);
- return pTemp;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sat_MmFixedEntryRecycle( Sat_MmFixed_t * p, char * pEntry )
-{
- // decrement the counter of used entries
- p->nEntriesUsed--;
- // add the entry to the linked list of free entries
- *((char **)pEntry) = p->pEntriesFree;
- p->pEntriesFree = pEntry;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description [Relocates all the memory except the first chunk.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sat_MmFixedRestart( Sat_MmFixed_t * p )
-{
- int i;
- char * pTemp;
-
- // deallocate all chunks except the first one
- for ( i = 1; i < p->nChunks; i++ )
- free( p->pChunks[i] );
- p->nChunks = 1;
- // transform these entries into a linked list
- pTemp = p->pChunks[0];
- for ( i = 1; i < p->nChunkSize; i++ )
- {
- *((char **)pTemp) = pTemp + p->nEntrySize;
- pTemp += p->nEntrySize;
- }
- // set the last link
- *((char **)pTemp) = NULL;
- // set the free entry list
- p->pEntriesFree = p->pChunks[0];
- // set the correct statistics
- p->nMemoryAlloc = p->nEntrySize * p->nChunkSize;
- p->nMemoryUsed = 0;
- p->nEntriesAlloc = p->nChunkSize;
- p->nEntriesUsed = 0;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Sat_MmFixedReadMemUsage( Sat_MmFixed_t * p )
-{
- return p->nMemoryAlloc;
-}
-
-
-
-/**Function*************************************************************
-
- Synopsis [Allocates entries of flexible size.]
-
- Description [Can only work with entry size at least 4 byte long.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Sat_MmFlex_t * Sat_MmFlexStart()
-{
- Sat_MmFlex_t * p;
-
- p = ALLOC( Sat_MmFlex_t, 1 );
- memset( p, 0, sizeof(Sat_MmFlex_t) );
-
- p->nEntriesUsed = 0;
- p->pCurrent = NULL;
- p->pEnd = NULL;
-
- p->nChunkSize = (1 << 12);
- p->nChunksAlloc = 64;
- p->nChunks = 0;
- p->pChunks = ALLOC( char *, p->nChunksAlloc );
-
- p->nMemoryUsed = 0;
- p->nMemoryAlloc = 0;
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sat_MmFlexStop( Sat_MmFlex_t * p, int fVerbose )
-{
- int i;
- if ( p == NULL )
- return;
- if ( fVerbose )
- {
- printf( "Flexible memory manager: Chunk size = %d. Chunks used = %d.\n",
- p->nChunkSize, p->nChunks );
- printf( " Entries used = %d. Memory used = %d. Memory alloc = %d.\n",
- p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc );
- }
- for ( i = 0; i < p->nChunks; i++ )
- free( p->pChunks[i] );
- free( p->pChunks );
- free( p );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-char * Sat_MmFlexEntryFetch( Sat_MmFlex_t * p, int nBytes )
-{
- char * pTemp;
- // check if there are still free entries
- if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd )
- { // need to allocate more entries
- if ( p->nChunks == p->nChunksAlloc )
- {
- p->nChunksAlloc *= 2;
- p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc );
- }
- if ( nBytes > p->nChunkSize )
- {
- // resize the chunk size if more memory is requested than it can give
- // (ideally, this should never happen)
- p->nChunkSize = 2 * nBytes;
- }
- p->pCurrent = ALLOC( char, p->nChunkSize );
- p->pEnd = p->pCurrent + p->nChunkSize;
- p->nMemoryAlloc += p->nChunkSize;
- // add the chunk to the chunk storage
- p->pChunks[ p->nChunks++ ] = p->pCurrent;
- }
- assert( p->pCurrent + nBytes <= p->pEnd );
- // increment the counter of used entries
- p->nEntriesUsed++;
- // keep track of the memory used
- p->nMemoryUsed += nBytes;
- // return the next entry
- pTemp = p->pCurrent;
- p->pCurrent += nBytes;
- return pTemp;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Sat_MmFlexReadMemUsage( Sat_MmFlex_t * p )
-{
- return p->nMemoryAlloc;
-}
-
-
-
-
-
-/**Function*************************************************************
-
- Synopsis [Starts the hierarchical memory manager.]
-
- Description [This manager can allocate entries of any size.
- Iternally they are mapped into the entries with the number of bytes
- equal to the power of 2. The smallest entry size is 8 bytes. The
- next one is 16 bytes etc. So, if the user requests 6 bytes, he gets
- 8 byte entry. If we asks for 25 bytes, he gets 32 byte entry etc.
- The input parameters "nSteps" says how many fixed memory managers
- are employed internally. Calling this procedure with nSteps equal
- to 10 results in 10 hierarchically arranged internal memory managers,
- which can allocate up to 4096 (1Kb) entries. Requests for larger
- entries are handed over to malloc() and then free()ed.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Sat_MmStep_t * Sat_MmStepStart( int nSteps )
-{
- Sat_MmStep_t * p;
- int i, k;
- p = ALLOC( Sat_MmStep_t, 1 );
- p->nMems = nSteps;
- // start the fixed memory managers
- p->pMems = ALLOC( Sat_MmFixed_t *, p->nMems );
- for ( i = 0; i < p->nMems; i++ )
- p->pMems[i] = Sat_MmFixedStart( (8<<i) );
- // set up the mapping of the required memory size into the corresponding manager
- p->nMapSize = (4<<p->nMems);
- p->pMap = ALLOC( Sat_MmFixed_t *, p->nMapSize+1 );
- p->pMap[0] = NULL;
- for ( k = 1; k <= 4; k++ )
- p->pMap[k] = p->pMems[0];
- for ( i = 0; i < p->nMems; i++ )
- for ( k = (4<<i)+1; k <= (8<<i); k++ )
- p->pMap[k] = p->pMems[i];
-//for ( i = 1; i < 100; i ++ )
-//printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize );
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis [Stops the memory manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose )
-{
- int i;
- for ( i = 0; i < p->nMems; i++ )
- Sat_MmFixedStop( p->pMems[i], fVerbose );
- free( p->pMems );
- free( p->pMap );
- free( p );
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates the entry.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-char * Sat_MmStepEntryFetch( Sat_MmStep_t * p, int nBytes )
-{
- if ( nBytes == 0 )
- return NULL;
- if ( nBytes > p->nMapSize )
- {
-// printf( "Allocating %d bytes.\n", nBytes );
- return ALLOC( char, nBytes );
- }
- return Sat_MmFixedEntryFetch( p->pMap[nBytes] );
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Recycles the entry.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes )
-{
- if ( nBytes == 0 )
- return;
- if ( nBytes > p->nMapSize )
- {
- free( pEntry );
- return;
- }
- Sat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Sat_MmStepReadMemUsage( Sat_MmStep_t * p )
-{
- int i, nMemTotal = 0;
- for ( i = 0; i < p->nMems; i++ )
- nMemTotal += p->pMems[i]->nMemoryAlloc;
- return nMemTotal;
-}
diff --git a/src/sat/bsat/satMem.h b/src/sat/bsat/satMem.h
deleted file mode 100644
index 5c5ddd9c..00000000
--- a/src/sat/bsat/satMem.h
+++ /dev/null
@@ -1,78 +0,0 @@
-/**CFile****************************************************************
-
- FileName [satMem.h]
-
- 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 __SAT_MEM_H__
-#define __SAT_MEM_H__
-
-////////////////////////////////////////////////////////////////////////
-/// INCLUDES ///
-////////////////////////////////////////////////////////////////////////
-
-//#include "leaks.h"
-#include <stdio.h>
-#include <stdlib.h>
-
-////////////////////////////////////////////////////////////////////////
-/// PARAMETERS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// STRUCTURE DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Sat_MmFixed_t_ Sat_MmFixed_t;
-typedef struct Sat_MmFlex_t_ Sat_MmFlex_t;
-typedef struct Sat_MmStep_t_ Sat_MmStep_t;
-
-////////////////////////////////////////////////////////////////////////
-/// GLOBAL VARIABLES ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// MACRO DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-// fixed-size-block memory manager
-extern Sat_MmFixed_t * Sat_MmFixedStart( int nEntrySize );
-extern void Sat_MmFixedStop( Sat_MmFixed_t * p, int fVerbose );
-extern char * Sat_MmFixedEntryFetch( Sat_MmFixed_t * p );
-extern void Sat_MmFixedEntryRecycle( Sat_MmFixed_t * p, char * pEntry );
-extern void Sat_MmFixedRestart( Sat_MmFixed_t * p );
-extern int Sat_MmFixedReadMemUsage( Sat_MmFixed_t * p );
-// flexible-size-block memory manager
-extern Sat_MmFlex_t * Sat_MmFlexStart();
-extern void Sat_MmFlexStop( Sat_MmFlex_t * p, int fVerbose );
-extern char * Sat_MmFlexEntryFetch( Sat_MmFlex_t * p, int nBytes );
-extern int Sat_MmFlexReadMemUsage( Sat_MmFlex_t * p );
-// hierarchical memory manager
-extern Sat_MmStep_t * Sat_MmStepStart( int nSteps );
-extern void Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose );
-extern char * Sat_MmStepEntryFetch( Sat_MmStep_t * p, int nBytes );
-extern void Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes );
-extern int Sat_MmStepReadMemUsage( Sat_MmStep_t * p );
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
deleted file mode 100644
index 439d9e76..00000000
--- a/src/sat/bsat/satSolver.c
+++ /dev/null
@@ -1,1358 +0,0 @@
-/**************************************************************************************************
-MiniSat -- Copyright (c) 2005, Niklas Sorensson
-http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
-
-Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
-associated documentation files (the "Software"), to deal in the Software without restriction,
-including without limitation the rights to use, copy, modify, merge, publish, distribute,
-sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in all copies or
-substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
-NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
-DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
-OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
-**************************************************************************************************/
-// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
-
-#include <stdio.h>
-#include <assert.h>
-#include <string.h>
-#include <math.h>
-
-#include "satSolver.h"
-
-//#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-
-//=================================================================================================
-// Debug:
-
-//#define VERBOSEDEBUG
-
-// For derivation output (verbosity level 2)
-#define L_IND "%-*d"
-#define L_ind sat_solver_dlevel(s)*3+3,sat_solver_dlevel(s)
-#define L_LIT "%sx%d"
-#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
-
-// Just like 'assert()' but expression will be evaluated in the release version as well.
-static inline void check(int expr) { assert(expr); }
-
-static void printlits(lit* begin, lit* end)
-{
- int i;
- for (i = 0; i < end - begin; i++)
- printf(L_LIT" ",L_lit(begin[i]));
-}
-
-//=================================================================================================
-// Random numbers:
-
-
-// Returns a random float 0 <= x < 1. Seed must never be 0.
-static inline double drand(double* seed) {
- int q;
- *seed *= 1389796;
- q = (int)(*seed / 2147483647);
- *seed -= (double)q * 2147483647;
- return *seed / 2147483647; }
-
-
-// Returns a random integer 0 <= x < size. Seed must never be 0.
-static inline int irand(double* seed, int size) {
- return (int)(drand(seed) * size); }
-
-
-//=================================================================================================
-// Predeclarations:
-
-static void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *));
-
-//=================================================================================================
-// Clause datatype + minor functions:
-
-struct clause_t
-{
- int size_learnt;
- lit lits[0];
-};
-
-static inline int clause_size (clause* c) { return c->size_learnt >> 1; }
-static inline lit* clause_begin (clause* c) { return c->lits; }
-static inline int clause_learnt (clause* c) { return c->size_learnt & 1; }
-static inline float clause_activity (clause* c) { return *((float*)&c->lits[c->size_learnt>>1]); }
-static inline void clause_setactivity(clause* c, float a) { *((float*)&c->lits[c->size_learnt>>1]) = a; }
-
-//=================================================================================================
-// Encode literals in clause pointers:
-
-static inline clause* clause_from_lit (lit l) { return (clause*)((unsigned long)l + (unsigned long)l + 1); }
-static inline bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); }
-static inline lit clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); }
-
-//=================================================================================================
-// Simple helpers:
-
-static inline int sat_solver_dlevel(sat_solver* s) { return veci_size(&s->trail_lim); }
-static inline vecp* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; }
-static inline void vecp_remove(vecp* v, void* e)
-{
- void** ws = vecp_begin(v);
- int j = 0;
- for (; ws[j] != e ; j++);
- assert(j < vecp_size(v));
- for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1];
- vecp_resize(v,vecp_size(v)-1);
-}
-
-//=================================================================================================
-// Variable order functions:
-
-static inline void order_update(sat_solver* s, int v) // updateorder
-{
- int* orderpos = s->orderpos;
- double* activity = s->activity;
- int* heap = veci_begin(&s->order);
- int i = orderpos[v];
- int x = heap[i];
- int parent = (i - 1) / 2;
-
- assert(s->orderpos[v] != -1);
-
- while (i != 0 && activity[x] > activity[heap[parent]]){
- heap[i] = heap[parent];
- orderpos[heap[i]] = i;
- i = parent;
- parent = (i - 1) / 2;
- }
- heap[i] = x;
- orderpos[x] = i;
-}
-
-static inline void order_assigned(sat_solver* s, int v)
-{
-}
-
-static inline void order_unassigned(sat_solver* s, int v) // undoorder
-{
- int* orderpos = s->orderpos;
- if (orderpos[v] == -1){
- orderpos[v] = veci_size(&s->order);
- veci_push(&s->order,v);
- order_update(s,v);
-//printf( "+%d ", v );
- }
-}
-
-static inline int order_select(sat_solver* s, float random_var_freq) // selectvar
-{
- int* heap;
- double* activity;
- int* orderpos;
-
- lbool* values = s->assigns;
-
- // Random decision:
- if (drand(&s->random_seed) < random_var_freq){
- int next = irand(&s->random_seed,s->size);
- assert(next >= 0 && next < s->size);
- if (values[next] == l_Undef)
- return next;
- }
-
- // Activity based decision:
-
- heap = veci_begin(&s->order);
- activity = s->activity;
- orderpos = s->orderpos;
-
-
- while (veci_size(&s->order) > 0){
- int next = heap[0];
- int size = veci_size(&s->order)-1;
- int x = heap[size];
-
- veci_resize(&s->order,size);
-
- orderpos[next] = -1;
-
- if (size > 0){
- double act = activity[x];
-
- int i = 0;
- int child = 1;
-
-
- while (child < size){
- if (child+1 < size && activity[heap[child]] < activity[heap[child+1]])
- child++;
-
- assert(child < size);
-
- if (act >= activity[heap[child]])
- break;
-
- heap[i] = heap[child];
- orderpos[heap[i]] = i;
- i = child;
- child = 2 * child + 1;
- }
- heap[i] = x;
- orderpos[heap[i]] = i;
- }
-
-//printf( "-%d ", next );
- if (values[next] == l_Undef)
- return next;
- }
-
- return var_Undef;
-}
-
-//=================================================================================================
-// Activity functions:
-
-static inline void act_var_rescale(sat_solver* s) {
- double* activity = s->activity;
- int i;
- for (i = 0; i < s->size; i++)
- activity[i] *= 1e-100;
- s->var_inc *= 1e-100;
-}
-
-static inline void act_var_bump(sat_solver* s, int v) {
- s->activity[v] += s->var_inc;
- if (s->activity[v] > 1e100)
- act_var_rescale(s);
- //printf("bump %d %f\n", v-1, activity[v]);
- if (s->orderpos[v] != -1)
- order_update(s,v);
-}
-
-static inline void act_var_bump_factor(sat_solver* s, int v) {
- s->activity[v] += (s->var_inc * s->factors[v]);
- if (s->activity[v] > 1e100)
- act_var_rescale(s);
- //printf("bump %d %f\n", v-1, activity[v]);
- if (s->orderpos[v] != -1)
- order_update(s,v);
-}
-
-static inline void act_var_decay(sat_solver* s) { s->var_inc *= s->var_decay; }
-
-static inline void act_clause_rescale(sat_solver* s) {
- clause** cs = (clause**)vecp_begin(&s->learnts);
- int i;
- for (i = 0; i < vecp_size(&s->learnts); i++){
- float a = clause_activity(cs[i]);
- clause_setactivity(cs[i], a * (float)1e-20);
- }
- s->cla_inc *= (float)1e-20;
-}
-
-
-static inline void act_clause_bump(sat_solver* s, clause *c) {
- float a = clause_activity(c) + s->cla_inc;
- clause_setactivity(c,a);
- if (a > 1e20) act_clause_rescale(s);
-}
-
-static inline void act_clause_decay(sat_solver* s) { s->cla_inc *= s->cla_decay; }
-
-//=================================================================================================
-// Clause functions:
-
-/* pre: size > 1 && no variable occurs twice
- */
-static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
-{
- int size;
- clause* c;
- int i;
-
- assert(end - begin > 1);
- assert(learnt >= 0 && learnt < 2);
- size = end - begin;
-// c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
- c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
-#else
- c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) );
-#endif
-
- c->size_learnt = (size << 1) | learnt;
- assert(((unsigned int)c & 1) == 0);
-
- for (i = 0; i < size; i++)
- c->lits[i] = begin[i];
-
- if (learnt)
- *((float*)&c->lits[size]) = 0.0;
-
- assert(begin[0] >= 0);
- assert(begin[0] < s->size*2);
- assert(begin[1] >= 0);
- assert(begin[1] < s->size*2);
-
- assert(lit_neg(begin[0]) < s->size*2);
- assert(lit_neg(begin[1]) < s->size*2);
-
- //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
- //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
-
- vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
- vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
-
- return c;
-}
-
-
-static void clause_remove(sat_solver* s, clause* c)
-{
- lit* lits = clause_begin(c);
- assert(lit_neg(lits[0]) < s->size*2);
- assert(lit_neg(lits[1]) < s->size*2);
-
- //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
- //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
-
- assert(lits[0] < s->size*2);
- vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
- vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
-
- if (clause_learnt(c)){
- s->stats.learnts--;
- s->stats.learnts_literals -= clause_size(c);
- }else{
- s->stats.clauses--;
- s->stats.clauses_literals -= clause_size(c);
- }
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
- free(c);
-#else
- Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
-#endif
-}
-
-
-static lbool clause_simplify(sat_solver* s, clause* c)
-{
- lit* lits = clause_begin(c);
- lbool* values = s->assigns;
- int i;
-
- assert(sat_solver_dlevel(s) == 0);
-
- for (i = 0; i < clause_size(c); i++){
- lbool sig = !lit_sign(lits[i]); sig += sig - 1;
- if (values[lit_var(lits[i])] == sig)
- return l_True;
- }
- return l_False;
-}
-
-//=================================================================================================
-// Minor (solver) functions:
-
-void sat_solver_setnvars(sat_solver* s,int n)
-{
- int var;
-
- if (s->cap < n){
-
- while (s->cap < n) s->cap = s->cap*2+1;
-
- s->wlists = (vecp*) realloc(s->wlists, sizeof(vecp)*s->cap*2);
- s->activity = (double*) realloc(s->activity, sizeof(double)*s->cap);
- s->factors = (double*) realloc(s->factors, sizeof(double)*s->cap);
- s->assigns = (lbool*) realloc(s->assigns, sizeof(lbool)*s->cap);
- s->orderpos = (int*) realloc(s->orderpos, sizeof(int)*s->cap);
- s->reasons = (clause**)realloc(s->reasons, sizeof(clause*)*s->cap);
- s->levels = (int*) realloc(s->levels, sizeof(int)*s->cap);
- s->tags = (lbool*) realloc(s->tags, sizeof(lbool)*s->cap);
- s->trail = (lit*) realloc(s->trail, sizeof(lit)*s->cap);
- }
-
- for (var = s->size; var < n; var++){
- vecp_new(&s->wlists[2*var]);
- vecp_new(&s->wlists[2*var+1]);
- s->activity [var] = 0;
- s->factors [var] = 0;
- s->assigns [var] = l_Undef;
- s->orderpos [var] = veci_size(&s->order);
- s->reasons [var] = (clause*)0;
- s->levels [var] = 0;
- s->tags [var] = l_Undef;
-
- /* does not hold because variables enqueued at top level will not be reinserted in the heap
- assert(veci_size(&s->order) == var);
- */
- veci_push(&s->order,var);
- order_update(s, var);
- }
-
- s->size = n > s->size ? n : s->size;
-}
-
-
-static inline bool enqueue(sat_solver* s, lit l, clause* from)
-{
- lbool* values = s->assigns;
- int v = lit_var(l);
- lbool val = values[v];
-#ifdef VERBOSEDEBUG
- printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
-#endif
-
- lbool sig = !lit_sign(l); sig += sig - 1;
- if (val != l_Undef){
- return val == sig;
- }else{
- // New fact -- store it.
-#ifdef VERBOSEDEBUG
- printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
-#endif
- int* levels = s->levels;
- clause** reasons = s->reasons;
-
- values [v] = sig;
- levels [v] = sat_solver_dlevel(s);
- reasons[v] = from;
- s->trail[s->qtail++] = l;
-
- order_assigned(s, v);
- return true;
- }
-}
-
-
-static inline void assume(sat_solver* s, lit l){
- assert(s->qtail == s->qhead);
- assert(s->assigns[lit_var(l)] == l_Undef);
-#ifdef VERBOSEDEBUG
- printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l));
-#endif
- veci_push(&s->trail_lim,s->qtail);
- enqueue(s,l,(clause*)0);
-}
-
-
-static void sat_solver_canceluntil(sat_solver* s, int level) {
- lit* trail;
- lbool* values;
- clause** reasons;
- int bound;
- int c;
-
- if (sat_solver_dlevel(s) <= level)
- return;
-
- trail = s->trail;
- values = s->assigns;
- reasons = s->reasons;
- bound = (veci_begin(&s->trail_lim))[level];
-
- ////////////////////////////////////////
- // added to cancel all assignments
-// if ( level == -1 )
-// bound = 0;
- ////////////////////////////////////////
-
- for (c = s->qtail-1; c >= bound; c--) {
- int x = lit_var(trail[c]);
- values [x] = l_Undef;
- reasons[x] = (clause*)0;
- }
-
- for (c = s->qhead-1; c >= bound; c--)
- order_unassigned(s,lit_var(trail[c]));
-
- s->qhead = s->qtail = bound;
- veci_resize(&s->trail_lim,level);
-}
-
-static void sat_solver_record(sat_solver* s, veci* cls)
-{
- lit* begin = veci_begin(cls);
- lit* end = begin + veci_size(cls);
- clause* c = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0;
- enqueue(s,*begin,c);
-
- ///////////////////////////////////
- // add clause to internal storage
- if ( s->pStore )
- {
- extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
- int RetValue = Sto_ManAddClause( s->pStore, begin, end );
- assert( RetValue );
- }
- ///////////////////////////////////
-
- assert(veci_size(cls) > 0);
-
- if (c != 0) {
- vecp_push(&s->learnts,c);
- act_clause_bump(s,c);
- s->stats.learnts++;
- s->stats.learnts_literals += veci_size(cls);
- }
-}
-
-
-static double sat_solver_progress(sat_solver* s)
-{
- lbool* values = s->assigns;
- int* levels = s->levels;
- int i;
-
- double progress = 0;
- double F = 1.0 / s->size;
- for (i = 0; i < s->size; i++)
- if (values[i] != l_Undef)
- progress += pow(F, levels[i]);
- return progress / s->size;
-}
-
-//=================================================================================================
-// Major methods:
-
-static bool sat_solver_lit_removable(sat_solver* s, lit l, int minl)
-{
- lbool* tags = s->tags;
- clause** reasons = s->reasons;
- int* levels = s->levels;
- int top = veci_size(&s->tagged);
-
- assert(lit_var(l) >= 0 && lit_var(l) < s->size);
- assert(reasons[lit_var(l)] != 0);
- veci_resize(&s->stack,0);
- veci_push(&s->stack,lit_var(l));
-
- while (veci_size(&s->stack) > 0){
- clause* c;
- int v = veci_begin(&s->stack)[veci_size(&s->stack)-1];
- assert(v >= 0 && v < s->size);
- veci_resize(&s->stack,veci_size(&s->stack)-1);
- assert(reasons[v] != 0);
- c = reasons[v];
-
- if (clause_is_lit(c)){
- int v = lit_var(clause_read_lit(c));
- if (tags[v] == l_Undef && levels[v] != 0){
- if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
- veci_push(&s->stack,v);
- tags[v] = l_True;
- veci_push(&s->tagged,v);
- }else{
- int* tagged = veci_begin(&s->tagged);
- int j;
- for (j = top; j < veci_size(&s->tagged); j++)
- tags[tagged[j]] = l_Undef;
- veci_resize(&s->tagged,top);
- return false;
- }
- }
- }else{
- lit* lits = clause_begin(c);
- int i, j;
-
- for (i = 1; i < clause_size(c); i++){
- int v = lit_var(lits[i]);
- if (tags[v] == l_Undef && levels[v] != 0){
- if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
-
- veci_push(&s->stack,lit_var(lits[i]));
- tags[v] = l_True;
- veci_push(&s->tagged,v);
- }else{
- int* tagged = veci_begin(&s->tagged);
- for (j = top; j < veci_size(&s->tagged); j++)
- tags[tagged[j]] = l_Undef;
- veci_resize(&s->tagged,top);
- return false;
- }
- }
- }
- }
- }
-
- return true;
-}
-
-static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
-{
- lit* trail = s->trail;
- lbool* tags = s->tags;
- clause** reasons = s->reasons;
- int* levels = s->levels;
- int cnt = 0;
- lit p = lit_Undef;
- int ind = s->qtail-1;
- lit* lits;
- int i, j, minl;
- int* tagged;
-
- veci_push(learnt,lit_Undef);
-
- do{
- assert(c != 0);
-
- if (clause_is_lit(c)){
- lit q = clause_read_lit(c);
- assert(lit_var(q) >= 0 && lit_var(q) < s->size);
- if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
- tags[lit_var(q)] = l_True;
- veci_push(&s->tagged,lit_var(q));
- act_var_bump(s,lit_var(q));
- if (levels[lit_var(q)] == sat_solver_dlevel(s))
- cnt++;
- else
- veci_push(learnt,q);
- }
- }else{
-
- if (clause_learnt(c))
- act_clause_bump(s,c);
-
- lits = clause_begin(c);
- //printlits(lits,lits+clause_size(c)); printf("\n");
- for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){
- lit q = lits[j];
- assert(lit_var(q) >= 0 && lit_var(q) < s->size);
- if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
- tags[lit_var(q)] = l_True;
- veci_push(&s->tagged,lit_var(q));
- act_var_bump(s,lit_var(q));
- if (levels[lit_var(q)] == sat_solver_dlevel(s))
- cnt++;
- else
- veci_push(learnt,q);
- }
- }
- }
-
- while (tags[lit_var(trail[ind--])] == l_Undef);
-
- p = trail[ind+1];
- c = reasons[lit_var(p)];
- cnt--;
-
- }while (cnt > 0);
-
- *veci_begin(learnt) = lit_neg(p);
-
- lits = veci_begin(learnt);
- minl = 0;
- for (i = 1; i < veci_size(learnt); i++){
- int lev = levels[lit_var(lits[i])];
- minl |= 1 << (lev & 31);
- }
-
- // simplify (full)
- for (i = j = 1; i < veci_size(learnt); i++){
- if (reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lits[i],minl))
- lits[j++] = lits[i];
- }
-
- // update size of learnt + statistics
- s->stats.max_literals += veci_size(learnt);
- veci_resize(learnt,j);
- s->stats.tot_literals += j;
-
- // clear tags
- tagged = veci_begin(&s->tagged);
- for (i = 0; i < veci_size(&s->tagged); i++)
- tags[tagged[i]] = l_Undef;
- veci_resize(&s->tagged,0);
-
-#ifdef DEBUG
- for (i = 0; i < s->size; i++)
- assert(tags[i] == l_Undef);
-#endif
-
-#ifdef VERBOSEDEBUG
- printf(L_IND"Learnt {", L_ind);
- for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i]));
-#endif
- if (veci_size(learnt) > 1){
- int max_i = 1;
- int max = levels[lit_var(lits[1])];
- lit tmp;
-
- for (i = 2; i < veci_size(learnt); i++)
- if (levels[lit_var(lits[i])] > max){
- max = levels[lit_var(lits[i])];
- max_i = i;
- }
-
- tmp = lits[1];
- lits[1] = lits[max_i];
- lits[max_i] = tmp;
- }
-#ifdef VERBOSEDEBUG
- {
- int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0;
- printf(" } at level %d\n", lev);
- }
-#endif
-}
-
-
-clause* sat_solver_propagate(sat_solver* s)
-{
- lbool* values = s->assigns;
- clause* confl = (clause*)0;
- lit* lits;
-
- //printf("sat_solver_propagate\n");
- while (confl == 0 && s->qtail - s->qhead > 0){
- lit p = s->trail[s->qhead++];
- vecp* ws = sat_solver_read_wlist(s,p);
- clause **begin = (clause**)vecp_begin(ws);
- clause **end = begin + vecp_size(ws);
- clause **i, **j;
-
- s->stats.propagations++;
- s->simpdb_props--;
-
- //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
- for (i = j = begin; i < end; ){
- if (clause_is_lit(*i)){
-// s->stats.inspects2++;
- *j++ = *i;
- if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
- confl = s->binary;
- (clause_begin(confl))[1] = lit_neg(p);
- (clause_begin(confl))[0] = clause_read_lit(*i++);
- // Copy the remaining watches:
-// s->stats.inspects2 += end - i;
- while (i < end)
- *j++ = *i++;
- }
- }else{
- lit false_lit;
- lbool sig;
-
- lits = clause_begin(*i);
-
- // Make sure the false literal is data[1]:
- false_lit = lit_neg(p);
- if (lits[0] == false_lit){
- lits[0] = lits[1];
- lits[1] = false_lit;
- }
- assert(lits[1] == false_lit);
- //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n");
-
- // If 0th watch is true, then clause is already satisfied.
- sig = !lit_sign(lits[0]); sig += sig - 1;
- if (values[lit_var(lits[0])] == sig){
- *j++ = *i;
- }else{
- // Look for new watch:
- lit* stop = lits + clause_size(*i);
- lit* k;
- for (k = lits + 2; k < stop; k++){
- lbool sig = lit_sign(*k); sig += sig - 1;
- if (values[lit_var(*k)] != sig){
- lits[1] = *k;
- *k = false_lit;
- vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
- goto next; }
- }
-
- *j++ = *i;
- // Clause is unit under assignment:
- if (!enqueue(s,lits[0], *i)){
- confl = *i++;
- // Copy the remaining watches:
-// s->stats.inspects2 += end - i;
- while (i < end)
- *j++ = *i++;
- }
- }
- }
- next:
- i++;
- }
-
- s->stats.inspects += j - (clause**)vecp_begin(ws);
- vecp_resize(ws,j - (clause**)vecp_begin(ws));
- }
-
- return confl;
-}
-
-static inline int clause_cmp (const void* x, const void* y) {
- return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }
-
-void sat_solver_reducedb(sat_solver* s)
-{
- int i, j;
- double extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity
- clause** learnts = (clause**)vecp_begin(&s->learnts);
- clause** reasons = s->reasons;
-
- sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
-
- for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
- if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
- clause_remove(s,learnts[i]);
- else
- learnts[j++] = learnts[i];
- }
- for (; i < vecp_size(&s->learnts); i++){
- if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim)
- clause_remove(s,learnts[i]);
- else
- learnts[j++] = learnts[i];
- }
-
- //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j);
-
-
- vecp_resize(&s->learnts,j);
-}
-
-static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_learnts)
-{
- int* levels = s->levels;
- double var_decay = 0.95;
- double clause_decay = 0.999;
- double random_var_freq = 0.02;
-
- sint64 conflictC = 0;
- veci learnt_clause;
- int i;
-
- assert(s->root_level == sat_solver_dlevel(s));
-
- s->nRestarts++;
- s->stats.starts++;
- s->var_decay = (float)(1 / var_decay );
- s->cla_decay = (float)(1 / clause_decay);
- veci_resize(&s->model,0);
- veci_new(&learnt_clause);
-
- // use activity factors in every even restart
- if ( (s->nRestarts & 1) && veci_size(&s->act_vars) > 0 )
- for ( i = 0; i < s->act_vars.size; i++ )
- act_var_bump_factor(s, s->act_vars.ptr[i]);
-
- for (;;){
- clause* confl = sat_solver_propagate(s);
- if (confl != 0){
- // CONFLICT
- int blevel;
-
-#ifdef VERBOSEDEBUG
- printf(L_IND"**CONFLICT**\n", L_ind);
-#endif
- s->stats.conflicts++; conflictC++;
- if (sat_solver_dlevel(s) == s->root_level){
- veci_delete(&learnt_clause);
- return l_False;
- }
-
- veci_resize(&learnt_clause,0);
- sat_solver_analyze(s, confl, &learnt_clause);
- blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level;
- blevel = s->root_level > blevel ? s->root_level : blevel;
- sat_solver_canceluntil(s,blevel);
- sat_solver_record(s,&learnt_clause);
- act_var_decay(s);
- act_clause_decay(s);
-
- }else{
- // NO CONFLICT
- int next;
-
- if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
- // Reached bound on number of conflicts:
- s->progress_estimate = sat_solver_progress(s);
- sat_solver_canceluntil(s,s->root_level);
- veci_delete(&learnt_clause);
- return l_Undef; }
-
- if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit ||
- s->nInsLimit && s->stats.inspects > s->nInsLimit )
- {
- // 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_dlevel(s) == 0 && !s->fSkipSimplify)
- // Simplify the set of problem clauses:
- sat_solver_simplify(s);
-
- if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
- // Reduce the set of learnt clauses:
- sat_solver_reducedb(s);
-
- // New variable decision:
- s->stats.decisions++;
- next = order_select(s,(float)random_var_freq);
-
- if (next == var_Undef){
- // Model found:
- lbool* values = s->assigns;
- int i;
- veci_resize(&s->model, 0);
- for (i = 0; i < s->size; i++)
- veci_push(&s->model,(int)values[i]);
- sat_solver_canceluntil(s,s->root_level);
- veci_delete(&learnt_clause);
-
- /*
- veci apa; veci_new(&apa);
- for (i = 0; i < s->size; i++)
- veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i))));
- printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n");
- veci_delete(&apa);
- */
-
- return l_True;
- }
-
- assume(s,lit_neg(toLit(next)));
- }
- }
-
- return l_Undef; // cannot happen
-}
-
-//=================================================================================================
-// External solver functions:
-
-sat_solver* sat_solver_new(void)
-{
- sat_solver* s = (sat_solver*)malloc(sizeof(sat_solver));
- memset( s, 0, sizeof(sat_solver) );
-
- // initialize vectors
- vecp_new(&s->clauses);
- vecp_new(&s->learnts);
- veci_new(&s->order);
- veci_new(&s->trail_lim);
- veci_new(&s->tagged);
- veci_new(&s->stack);
- veci_new(&s->model);
- veci_new(&s->act_vars);
-
- // initialize arrays
- s->wlists = 0;
- s->activity = 0;
- s->factors = 0;
- s->assigns = 0;
- s->orderpos = 0;
- s->reasons = 0;
- s->levels = 0;
- s->tags = 0;
- s->trail = 0;
-
-
- // initialize other vars
- s->size = 0;
- s->cap = 0;
- s->qhead = 0;
- s->qtail = 0;
- s->cla_inc = 1;
- s->cla_decay = 1;
- s->var_inc = 1;
- s->var_decay = 1;
- s->root_level = 0;
- s->simpdb_assigns = 0;
- s->simpdb_props = 0;
- s->random_seed = 91648253;
- s->progress_estimate = 0;
- s->binary = (clause*)malloc(sizeof(clause) + sizeof(lit)*2);
- s->binary->size_learnt = (2 << 1);
- s->verbosity = 0;
-
- s->stats.starts = 0;
- s->stats.decisions = 0;
- s->stats.propagations = 0;
- s->stats.inspects = 0;
- s->stats.conflicts = 0;
- s->stats.clauses = 0;
- s->stats.clauses_literals = 0;
- s->stats.learnts = 0;
- s->stats.learnts_literals = 0;
- s->stats.max_literals = 0;
- s->stats.tot_literals = 0;
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
- s->pMem = NULL;
-#else
- s->pMem = Sat_MmStepStart( 10 );
-#endif
- return s;
-}
-
-
-void sat_solver_delete(sat_solver* s)
-{
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
- int i;
- for (i = 0; i < vecp_size(&s->clauses); i++)
- free(vecp_begin(&s->clauses)[i]);
- for (i = 0; i < vecp_size(&s->learnts); i++)
- free(vecp_begin(&s->learnts)[i]);
-#else
- Sat_MmStepStop( s->pMem, 0 );
-#endif
-
- // delete vectors
- vecp_delete(&s->clauses);
- vecp_delete(&s->learnts);
- veci_delete(&s->order);
- veci_delete(&s->trail_lim);
- veci_delete(&s->tagged);
- veci_delete(&s->stack);
- veci_delete(&s->model);
- veci_delete(&s->act_vars);
- free(s->binary);
-
- // delete arrays
- if (s->wlists != 0){
- int i;
- for (i = 0; i < s->size*2; i++)
- vecp_delete(&s->wlists[i]);
-
- // if one is different from null, all are
- free(s->wlists );
- free(s->activity );
- free(s->factors );
- free(s->assigns );
- free(s->orderpos );
- free(s->reasons );
- free(s->levels );
- free(s->trail );
- free(s->tags );
- }
-
- sat_solver_store_free(s);
- free(s);
-}
-
-
-bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
-{
- lit *i,*j;
- int maxvar;
- lbool* values;
- lit last;
-
- if (begin == end) return false;
-
- //printlits(begin,end); printf("\n");
- // insertion sort
- maxvar = lit_var(*begin);
- for (i = begin + 1; i < end; i++){
- lit l = *i;
- maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
- for (j = i; j > begin && *(j-1) > l; j--)
- *j = *(j-1);
- *j = l;
- }
- sat_solver_setnvars(s,maxvar+1);
-// sat_solver_setnvars(s, lit_var(*(end-1))+1 );
-
- //printlits(begin,end); printf("\n");
- values = s->assigns;
-
- // delete duplicates
- last = lit_Undef;
- for (i = j = begin; i < end; i++){
- //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]));
- lbool sig = !lit_sign(*i); sig += sig - 1;
- if (*i == lit_neg(last) || sig == values[lit_var(*i)])
- return true; // tautology
- else if (*i != last && values[lit_var(*i)] == l_Undef)
- last = *j++ = *i;
- }
-
- //printf("final: "); printlits(begin,j); printf("\n");
-
- if (j == begin) // empty clause
- return false;
-
- ///////////////////////////////////
- // add clause to internal storage
- if ( s->pStore )
- {
- extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
- int RetValue = Sto_ManAddClause( s->pStore, begin, j );
- assert( RetValue );
- }
- ///////////////////////////////////
-
- if (j - begin == 1) // unit clause
- return enqueue(s,*begin,(clause*)0);
-
- // create new clause
- vecp_push(&s->clauses,clause_new(s,begin,j,0));
-
-
- s->stats.clauses++;
- s->stats.clauses_literals += j - begin;
-
- return true;
-}
-
-
-bool sat_solver_simplify(sat_solver* s)
-{
- clause** reasons;
- int type;
-
- assert(sat_solver_dlevel(s) == 0);
-
- if (sat_solver_propagate(s) != 0)
- return false;
-
- if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
- return true;
-
- reasons = s->reasons;
- for (type = 0; type < 2; type++){
- vecp* cs = type ? &s->learnts : &s->clauses;
- clause** cls = (clause**)vecp_begin(cs);
-
- int i, j;
- for (j = i = 0; i < vecp_size(cs); i++){
- if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] &&
- clause_simplify(s,cls[i]) == l_True)
- clause_remove(s,cls[i]);
- else
- cls[j++] = cls[i];
- }
- vecp_resize(cs,j);
- }
-
- s->simpdb_assigns = s->qhead;
- // (shouldn't depend on 'stats' really, but it will do for now)
- s->simpdb_props = (int)(s->stats.clauses_literals + s->stats.learnts_literals);
-
- return true;
-}
-
-
-int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit, sint64 nConfLimitGlobal, sint64 nInsLimitGlobal)
-{
- sint64 nof_conflicts = 100;
- sint64 nof_learnts = sat_solver_nclauses(s) / 3;
- lbool status = l_Undef;
- lbool* values = s->assigns;
- lit* i;
-
- // set the external limits
- s->nCalls++;
- s->nRestarts = 0;
- s->nConfLimit = 0;
- s->nInsLimit = 0;
- if ( nConfLimit )
- s->nConfLimit = s->stats.conflicts + nConfLimit;
- if ( nInsLimit )
- s->nInsLimit = s->stats.inspects + nInsLimit;
- if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) )
- s->nConfLimit = nConfLimitGlobal;
- if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) )
- s->nInsLimit = nInsLimitGlobal;
-
- //printf("solve: "); printlits(begin, end); printf("\n");
- for (i = begin; i < end; i++){
- switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){
- case 1: /* l_True: */
- break;
- case 0: /* l_Undef */
- assume(s, *i);
- if (sat_solver_propagate(s) == NULL)
- break;
- // fallthrough
- case -1: /* l_False */
- sat_solver_canceluntil(s, 0);
- return l_False;
- }
- }
- s->nCalls2++;
-
- s->root_level = sat_solver_dlevel(s);
-
- if (s->verbosity >= 1){
- printf("==================================[MINISAT]===================================\n");
- printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n");
- printf("| | Clauses Literals | Limit Clauses Literals Lit/Cl | |\n");
- printf("==============================================================================\n");
- }
-
- while (status == l_Undef){
- double Ratio = (s->stats.learnts == 0)? 0.0 :
- s->stats.learnts_literals / (double)s->stats.learnts;
-
- if (s->verbosity >= 1)
- {
- printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n",
- (double)s->stats.conflicts,
- (double)s->stats.clauses,
- (double)s->stats.clauses_literals,
- (double)nof_learnts,
- (double)s->stats.learnts,
- (double)s->stats.learnts_literals,
- Ratio,
- s->progress_estimate*100);
- fflush(stdout);
- }
- status = sat_solver_search(s, nof_conflicts, nof_learnts);
- nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5;
- nof_learnts = nof_learnts * 11 / 10; //*= 1.1;
-
- // quit the loop if reached an external limit
- if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
- {
-// printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
- break;
- }
- if ( s->nInsLimit && s->stats.inspects > s->nInsLimit )
- {
-// printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
- break;
- }
- }
- if (s->verbosity >= 1)
- printf("==============================================================================\n");
-
- sat_solver_canceluntil(s,0);
-
- ////////////////////////////////////////////////
- if ( status == l_False && s->pStore )
- {
- extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
- int RetValue = Sto_ManAddClause( s->pStore, NULL, NULL );
- assert( RetValue );
- }
- ////////////////////////////////////////////////
- return status;
-}
-
-
-int sat_solver_nvars(sat_solver* s)
-{
- return s->size;
-}
-
-
-int sat_solver_nclauses(sat_solver* s)
-{
- return vecp_size(&s->clauses);
-}
-
-
-int sat_solver_nconflicts(sat_solver* s)
-{
- return (int)s->stats.conflicts;
-}
-
-//=================================================================================================
-// Clause storage functions:
-
-void sat_solver_store_alloc( sat_solver * s )
-{
- extern void * Sto_ManAlloc();
- assert( s->pStore == NULL );
- s->pStore = Sto_ManAlloc();
-}
-
-void sat_solver_store_write( sat_solver * s, char * pFileName )
-{
- extern void Sto_ManDumpClauses( void * p, char * pFileName );
- if ( s->pStore ) Sto_ManDumpClauses( s->pStore, pFileName );
-}
-
-void sat_solver_store_free( sat_solver * s )
-{
- extern void Sto_ManFree( void * p );
- if ( s->pStore ) Sto_ManFree( s->pStore );
- s->pStore = NULL;
-}
-
-void sat_solver_store_mark_roots( sat_solver * s )
-{
- extern void Sto_ManMarkRoots( void * p );
- if ( s->pStore ) Sto_ManMarkRoots( s->pStore );
-}
-
-void sat_solver_store_mark_clauses_a( sat_solver * s )
-{
- extern void Sto_ManMarkClausesA( void * p );
- if ( s->pStore ) Sto_ManMarkClausesA( s->pStore );
-}
-
-void * sat_solver_store_release( sat_solver * s )
-{
- void * pTemp;
- if ( s->pStore == NULL )
- return NULL;
- pTemp = s->pStore;
- s->pStore = NULL;
- return pTemp;
-}
-
-//=================================================================================================
-// Sorting functions (sigh):
-
-static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *))
-{
- int i, j, best_i;
- void* tmp;
-
- for (i = 0; i < size-1; i++){
- best_i = i;
- for (j = i+1; j < size; j++){
- if (comp(array[j], array[best_i]) < 0)
- best_i = j;
- }
- tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
- }
-}
-
-
-static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed)
-{
- if (size <= 15)
- selectionsort(array, size, comp);
-
- else{
- void* pivot = array[irand(seed, size)];
- void* tmp;
- int i = -1;
- int j = size;
-
- for(;;){
- do i++; while(comp(array[i], pivot)<0);
- do j--; while(comp(pivot, array[j])<0);
-
- if (i >= j) break;
-
- tmp = array[i]; array[i] = array[j]; array[j] = tmp;
- }
-
- sortrnd(array , i , comp, seed);
- sortrnd(&array[i], size-i, comp, seed);
- }
-}
-
-void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *))
-{
- double seed = 91648253;
- sortrnd(array,size,comp,&seed);
-}
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
deleted file mode 100644
index 542b9895..00000000
--- a/src/sat/bsat/satSolver.h
+++ /dev/null
@@ -1,191 +0,0 @@
-/**************************************************************************************************
-MiniSat -- Copyright (c) 2005, Niklas Sorensson
-http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
-
-Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
-associated documentation files (the "Software"), to deal in the Software without restriction,
-including without limitation the rights to use, copy, modify, merge, publish, distribute,
-sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in all copies or
-substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
-NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
-DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
-OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
-**************************************************************************************************/
-// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
-
-#ifndef satSolver_h
-#define satSolver_h
-
-#ifdef _WIN32
-#define inline __inline // compatible with MS VS 6.0
-#endif
-
-#include "satVec.h"
-#include "satMem.h"
-
-//=================================================================================================
-// Simple types:
-
-// does not work for c++
-//typedef int bool;
-#ifndef __cplusplus
-#ifndef bool
-#define bool int
-#endif
-#endif
-
-static const bool true = 1;
-static const bool false = 0;
-
-typedef int lit;
-typedef char lbool;
-
-#ifndef SINT64
-#define SINT64
-
-#ifdef _WIN32
-typedef signed __int64 sint64; // compatible with MS VS 6.0
-#else
-typedef long long sint64;
-#endif
-
-#endif
-
-static const int var_Undef = -1;
-static const lit lit_Undef = -2;
-
-static const lbool l_Undef = 0;
-static const lbool l_True = 1;
-static const lbool l_False = -1;
-
-static inline lit toLit (int v) { return v + v; }
-static inline lit toLitCond(int v, int c) { return v + v + (c != 0); }
-static inline lit lit_neg (lit l) { return l ^ 1; }
-static inline int lit_var (lit l) { return l >> 1; }
-static inline int lit_sign (lit l) { return l & 1; }
-static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
-static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
-
-
-//=================================================================================================
-// Public interface:
-
-struct sat_solver_t;
-typedef struct sat_solver_t sat_solver;
-
-extern sat_solver* sat_solver_new(void);
-extern void sat_solver_delete(sat_solver* s);
-
-extern bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end);
-extern bool sat_solver_simplify(sat_solver* s);
-extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit, sint64 nConfLimitGlobal, sint64 nInsLimitGlobal);
-
-extern int sat_solver_nvars(sat_solver* s);
-extern int sat_solver_nclauses(sat_solver* s);
-extern int sat_solver_nconflicts(sat_solver* s);
-
-extern void sat_solver_setnvars(sat_solver* s,int n);
-
-struct stats_t
-{
- sint64 starts, decisions, propagations, inspects, conflicts;
- sint64 clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;
-};
-typedef struct stats_t stats;
-
-extern void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
-extern void Sat_SolverPrintStats( FILE * pFile, sat_solver * p );
-extern int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars );
-extern void Sat_SolverDoubleClauses( sat_solver * p, int iVar );
-
-// trace recording
-extern void Sat_SolverTraceStart( sat_solver * pSat, char * pName );
-extern void Sat_SolverTraceStop( sat_solver * pSat );
-extern void Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot );
-
-// clause storage
-extern void sat_solver_store_alloc( sat_solver * s );
-extern void sat_solver_store_write( sat_solver * s, char * pFileName );
-extern void sat_solver_store_free( sat_solver * s );
-extern void sat_solver_store_mark_roots( sat_solver * s );
-extern void sat_solver_store_mark_clauses_a( sat_solver * s );
-extern void * sat_solver_store_release( sat_solver * s );
-
-//=================================================================================================
-// Solver representation:
-
-struct clause_t;
-typedef struct clause_t clause;
-
-struct sat_solver_t
-{
- int size; // nof variables
- int cap; // size of varmaps
- int qhead; // Head index of queue.
- int qtail; // Tail index of queue.
-
- // clauses
- vecp clauses; // List of problem constraints. (contains: clause*)
- vecp learnts; // List of learnt clauses. (contains: clause*)
-
- // activities
- double var_inc; // Amount to bump next variable with.
- double var_decay; // INVERSE decay factor for variable activity: stores 1/decay.
- float cla_inc; // Amount to bump next clause with.
- float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay.
-
- vecp* wlists; //
- double* activity; // A heuristic measurement of the activity of a variable.
- lbool* assigns; // Current values of variables.
- int* orderpos; // Index in variable order.
- clause** reasons; //
- int* levels; //
- lit* trail;
-
- clause* binary; // A temporary binary clause
- lbool* tags; //
- veci tagged; // (contains: var)
- veci stack; // (contains: var)
-
- veci order; // Variable order. (heap) (contains: var)
- veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int)
- veci model; // If problem is solved, this vector contains the model (contains: lbool).
-
- int root_level; // Level of first proper decision.
- int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
- int simpdb_props; // Number of propagations before next 'simplifyDB()'.
- double random_seed;
- double progress_estimate;
- int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything
-
- stats stats;
-
- sint64 nConfLimit; // external limit on the number of conflicts
- sint64 nInsLimit; // external limit on the number of implications
-
- veci act_vars; // variables whose activity has changed
- double* factors; // the activity factors
- int nRestarts; // the number of local restarts
- int nCalls; // the number of local restarts
- int nCalls2; // the number of local restarts
-
- Sat_MmStep_t * pMem;
-
- int fSkipSimplify; // set to one to skip simplification of the clause database
-
- // clause store
- void * pStore;
-
- // trace recording
- FILE * pFile;
- int nClauses;
- int nRoots;
-};
-
-#endif
diff --git a/src/sat/bsat/satStore.c b/src/sat/bsat/satStore.c
deleted file mode 100644
index 7c1d7132..00000000
--- a/src/sat/bsat/satStore.c
+++ /dev/null
@@ -1,437 +0,0 @@
-/**CFile****************************************************************
-
- FileName [satStore.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [SAT solver.]
-
- Synopsis [Records the trace of SAT solving in the CNF form.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: satStore.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
-
-***********************************************************************/
-
-#include <stdio.h>
-#include <stdlib.h>
-#include <string.h>
-#include <assert.h>
-#include <time.h>
-#include "satStore.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Fetches memory.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-char * Sto_ManMemoryFetch( Sto_Man_t * p, int nBytes )
-{
- char * pMem;
- if ( p->pChunkLast == NULL || nBytes > p->nChunkSize - p->nChunkUsed )
- {
- pMem = (char *)malloc( p->nChunkSize );
- *(char **)pMem = p->pChunkLast;
- p->pChunkLast = pMem;
- p->nChunkUsed = sizeof(char *);
- }
- pMem = p->pChunkLast + p->nChunkUsed;
- p->nChunkUsed += nBytes;
- return pMem;
-}
-
-/**Function*************************************************************
-
- Synopsis [Frees memory manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sto_ManMemoryStop( Sto_Man_t * p )
-{
- char * pMem, * pNext;
- if ( p->pChunkLast == NULL )
- return;
- for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext )
- free( pMem );
- free( pMem );
-}
-
-/**Function*************************************************************
-
- Synopsis [Reports memory usage in bytes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Sto_ManMemoryReport( Sto_Man_t * p )
-{
- int Total;
- char * pMem, * pNext;
- if ( p->pChunkLast == NULL )
- return 0;
- Total = p->nChunkUsed;
- for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext )
- Total += p->nChunkSize;
- return Total;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Allocate proof manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Sto_Man_t * Sto_ManAlloc()
-{
- Sto_Man_t * p;
- // allocate the manager
- p = (Sto_Man_t *)malloc( sizeof(Sto_Man_t) );
- memset( p, 0, sizeof(Sto_Man_t) );
- // memory management
- p->nChunkSize = (1<<16); // use 64K chunks
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis [Deallocate proof manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sto_ManFree( Sto_Man_t * p )
-{
- Sto_ManMemoryStop( p );
- free( p );
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds one clause to the manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Sto_ManAddClause( Sto_Man_t * p, lit * pBeg, lit * pEnd )
-{
- Sto_Cls_t * pClause;
- lit Lit, * i, * j;
- int nSize;
-
- // process the literals
- if ( pBeg < pEnd )
- {
- // insertion sort
- for ( i = pBeg + 1; i < pEnd; i++ )
- {
- Lit = *i;
- for ( j = i; j > pBeg && *(j-1) > Lit; j-- )
- *j = *(j-1);
- *j = Lit;
- }
- // make sure there is no duplicated variables
- for ( i = pBeg + 1; i < pEnd; i++ )
- if ( lit_var(*(i-1)) == lit_var(*i) )
- {
- printf( "The clause contains two literals of the same variable: %d and %d.\n", *(i-1), *i );
- return 0;
- }
- // check the largest var size
- p->nVars = STO_MAX( p->nVars, lit_var(*(pEnd-1)) + 1 );
- }
-
- // get memory for the clause
- nSize = sizeof(Sto_Cls_t) + sizeof(lit) * (pEnd - pBeg);
- pClause = (Sto_Cls_t *)Sto_ManMemoryFetch( p, nSize );
- memset( pClause, 0, sizeof(Sto_Cls_t) );
-
- // assign the clause
- pClause->Id = p->nClauses++;
- pClause->nLits = pEnd - pBeg;
- memcpy( pClause->pLits, pBeg, sizeof(lit) * (pEnd - pBeg) );
-
- // add the clause to the list
- if ( p->pHead == NULL )
- p->pHead = pClause;
- if ( p->pTail == NULL )
- p->pTail = pClause;
- else
- {
- p->pTail->pNext = pClause;
- p->pTail = pClause;
- }
-
- // add the empty clause
- if ( pClause->nLits == 0 )
- {
- if ( p->pEmpty )
- {
- printf( "More than one empty clause!\n" );
- return 0;
- }
- p->pEmpty = pClause;
- }
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Mark all clauses added so far as root clauses.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sto_ManMarkRoots( Sto_Man_t * p )
-{
- Sto_Cls_t * pClause;
- p->nRoots = 0;
- Sto_ManForEachClause( p, pClause )
- {
- pClause->fRoot = 1;
- p->nRoots++;
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Mark all clauses added so far as clause of A.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sto_ManMarkClausesA( Sto_Man_t * p )
-{
- Sto_Cls_t * pClause;
- p->nClausesA = 0;
- Sto_ManForEachClause( p, pClause )
- {
- pClause->fA = 1;
- p->nClausesA++;
- }
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Writes the stored clauses into a file.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName )
-{
- FILE * pFile;
- Sto_Cls_t * pClause;
- int i;
- // start the file
- pFile = fopen( pFileName, "w" );
- if ( pFile == NULL )
- {
- printf( "Error: Cannot open output file (%s).\n", pFileName );
- return;
- }
- // write the data
- fprintf( pFile, "p %d %d %d %d\n", p->nVars, p->nClauses, p->nRoots, p->nClausesA );
- Sto_ManForEachClause( p, pClause )
- {
- for ( i = 0; i < (int)pClause->nLits; i++ )
- fprintf( pFile, " %d", lit_print(pClause->pLits[i]) );
- fprintf( pFile, "\n" );
- }
- fprintf( pFile, " 0\n" );
- fclose( pFile );
-}
-
-/**Function*************************************************************
-
- Synopsis [Reads one literal from file.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Sto_ManLoadNumber( FILE * pFile, int * pNumber )
-{
- int Char, Number = 0, Sign = 0;
- // skip space-like chars
- do {
- Char = fgetc( pFile );
- if ( Char == EOF )
- return 0;
- } while ( Char == ' ' || Char == '\t' || Char == '\r' || Char == '\n' );
- // read the literal
- while ( 1 )
- {
- // get the next character
- Char = fgetc( pFile );
- if ( Char == ' ' || Char == '\t' || Char == '\r' || Char == '\n' )
- break;
- // check that the char is a digit
- if ( (Char < '0' || Char > '9') && Char != '-' )
- {
- printf( "Error: Wrong char (%c) in the input file.\n", Char );
- return 0;
- }
- // check if this is a minus
- if ( Char == '-' )
- Sign = 1;
- else
- Number = 10 * Number + Char;
- }
- // return the number
- *pNumber = Sign? -Number : Number;
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Reads CNF from file.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Sto_Man_t * Sto_ManLoadClauses( char * pFileName )
-{
- FILE * pFile;
- Sto_Man_t * p;
- Sto_Cls_t * pClause;
- char pBuffer[1024];
- int nLits, nLitsAlloc, Counter, Number;
- lit * pLits;
-
- // start the file
- pFile = fopen( pFileName, "r" );
- if ( pFile == NULL )
- {
- printf( "Error: Cannot open input file (%s).\n", pFileName );
- return NULL;
- }
-
- // create the manager
- p = Sto_ManAlloc();
-
- // alloc the array of literals
- nLitsAlloc = 1024;
- pLits = (lit *)malloc( sizeof(lit) * nLitsAlloc );
-
- // read file header
- p->nVars = p->nClauses = p->nRoots = p->nClausesA = 0;
- while ( fgets( pBuffer, 1024, pFile ) )
- {
- if ( pBuffer[0] == 'c' )
- continue;
- if ( pBuffer[0] == 'p' )
- {
- sscanf( pBuffer + 1, "%d %d %d %d", p->nVars, p->nClauses, p->nRoots, p->nClausesA );
- break;
- }
- printf( "Warning: Skipping line: \"%s\"\n", pBuffer );
- }
-
- // read the clauses
- nLits = 0;
- while ( Sto_ManLoadNumber(pFile, &Number) )
- {
- if ( Number == 0 )
- {
- int RetValue;
- RetValue = Sto_ManAddClause( p, pLits, pLits + nLits );
- assert( RetValue );
- nLits = 0;
- continue;
- }
- if ( nLits == nLitsAlloc )
- {
- nLitsAlloc *= 2;
- pLits = (lit *)realloc( pLits, sizeof(lit) * nLitsAlloc );
- }
- pLits[ nLits++ ] = lit_read(Number);
- }
- if ( nLits > 0 )
- printf( "Error: The last clause was not saved.\n" );
-
- // count clauses
- Counter = 0;
- Sto_ManForEachClause( p, pClause )
- Counter++;
-
- // check the number of clauses
- if ( p->nClauses != Counter )
- {
- printf( "Error: The actual number of clauses (%d) is different than declared (%d).\n", Counter, p->nClauses );
- Sto_ManFree( p );
- return NULL;
- }
-
- free( pLits );
- fclose( pFile );
- return p;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h
deleted file mode 100644
index 346b59df..00000000
--- a/src/sat/bsat/satStore.h
+++ /dev/null
@@ -1,137 +0,0 @@
-/**CFile****************************************************************
-
- FileName [pr.h]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Proof recording.]
-
- Synopsis [External declarations.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: pr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __PR_H__
-#define __PR_H__
-
-/*
- The trace of SAT solving contains the original clause of the problem
- along with the learned clauses derived during SAT solving.
- The first line of the resulting file contains 3 numbers instead of 2:
- c <num_vars> <num_all_clauses> <num_root_clauses>
-*/
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-#ifdef _WIN32
-#define inline __inline // compatible with MS VS 6.0
-#endif
-
-#ifndef PRT
-#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
-#endif
-
-#define STO_MAX(a,b) ((a) > (b) ? (a) : (b))
-
-////////////////////////////////////////////////////////////////////////
-/// INCLUDES ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// PARAMETERS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// BASIC TYPES ///
-////////////////////////////////////////////////////////////////////////
-
-typedef unsigned lit;
-
-typedef struct Sto_Cls_t_ Sto_Cls_t;
-struct Sto_Cls_t_
-{
- Sto_Cls_t * pNext; // the next clause
- Sto_Cls_t * pNext0; // the next 0-watch
- Sto_Cls_t * pNext1; // the next 0-watch
- int Id; // the clause ID
- unsigned fA : 1; // belongs to A
- unsigned fRoot : 1; // original clause
- unsigned fVisit : 1; // visited clause
- unsigned nLits : 24; // the number of literals
- lit pLits[0]; // literals of this clause
-};
-
-typedef struct Sto_Man_t_ Sto_Man_t;
-struct Sto_Man_t_
-{
- // general data
- int nVars; // the number of variables
- int nRoots; // the number of root clauses
- int nClauses; // the number of all clauses
- int nClausesA; // the number of clauses of A
- Sto_Cls_t * pHead; // the head clause
- Sto_Cls_t * pTail; // the tail clause
- Sto_Cls_t * pEmpty; // the empty clause
- // memory management
- int nChunkSize; // the number of bytes in a chunk
- int nChunkUsed; // the number of bytes used in the last chunk
- char * pChunkLast; // the last memory chunk
-};
-
-// variable/literal conversions (taken from MiniSat)
-static inline lit toLit (int v) { return v + v; }
-static inline lit toLitCond(int v, int c) { return v + v + (c != 0); }
-static inline lit lit_neg (lit l) { return l ^ 1; }
-static inline int lit_var (lit l) { return l >> 1; }
-static inline int lit_sign (lit l) { return l & 1; }
-static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
-static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
-static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; }
-
-// iterators through the clauses
-#define Sto_ManForEachClause( p, pCls ) for( pCls = p->pHead; pCls; pCls = pCls->pNext )
-#define Sto_ManForEachClauseRoot( p, pCls ) for( pCls = p->pHead; pCls && pCls->fRoot; pCls = pCls->pNext )
-
-////////////////////////////////////////////////////////////////////////
-/// MACRO DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== satStore.c ==========================================================*/
-extern Sto_Man_t * Sto_ManAlloc();
-extern void Sto_ManFree( Sto_Man_t * p );
-extern int Sto_ManAddClause( Sto_Man_t * p, lit * pBeg, lit * pEnd );
-extern int Sto_ManMemoryReport( Sto_Man_t * p );
-extern void Sto_ManMarkRoots( Sto_Man_t * p );
-extern void Sto_ManMarkClausesA( Sto_Man_t * p );
-extern void Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName );
-extern Sto_Man_t * Sto_ManLoadClauses( char * pFileName );
-
-/*=== satInter.c ==========================================================*/
-typedef struct Int_Man_t_ Int_Man_t;
-extern Int_Man_t * Int_ManAlloc( int nVarsAlloc );
-extern void Int_ManFree( Int_Man_t * p );
-extern int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult );
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/sat/bsat/satTrace.c b/src/sat/bsat/satTrace.c
deleted file mode 100644
index 111e8dfb..00000000
--- a/src/sat/bsat/satTrace.c
+++ /dev/null
@@ -1,109 +0,0 @@
-/**CFile****************************************************************
-
- FileName [satTrace.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [SAT sat_solver.]
-
- Synopsis [Records the trace of SAT solving in the CNF form.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: satTrace.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
-
-***********************************************************************/
-
-#include <stdio.h>
-#include <assert.h>
-#include "satSolver.h"
-
-/*
- The trace of SAT solving contains the original clause of the problem
- along with the learned clauses derived during SAT solving.
- The first line of the resulting file contains 3 numbers instead of 2:
- c <num_vars> <num_all_clauses> <num_root_clauses>
-*/
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Start the trace recording.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sat_SolverTraceStart( sat_solver * pSat, char * pName )
-{
- assert( pSat->pFile == NULL );
- pSat->pFile = fopen( pName, "w" );
- fprintf( pSat->pFile, " \n" );
- pSat->nClauses = 0;
- pSat->nRoots = 0;
-}
-
-/**Function*************************************************************
-
- Synopsis [Stops the trace recording.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sat_SolverTraceStop( sat_solver * pSat )
-{
- if ( pSat->pFile == NULL )
- return;
- rewind( pSat->pFile );
- fprintf( pSat->pFile, "p %d %d %d", sat_solver_nvars(pSat), pSat->nClauses, pSat->nRoots );
- fclose( pSat->pFile );
- pSat->pFile = NULL;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Writes one clause into the trace file.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot )
-{
- if ( pSat->pFile == NULL )
- return;
- pSat->nClauses++;
- pSat->nRoots += fRoot;
- for ( ; pBeg < pEnd ; pBeg++ )
- fprintf( pSat->pFile, " %d", lit_print(*pBeg) );
- fprintf( pSat->pFile, " 0\n" );
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
deleted file mode 100644
index 62f3c208..00000000
--- a/src/sat/bsat/satUtil.c
+++ /dev/null
@@ -1,234 +0,0 @@
-/**CFile****************************************************************
-
- FileName [satUtil.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [C-language MiniSat solver.]
-
- Synopsis [Additional SAT solver procedures.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: satUtil.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
-
-***********************************************************************/
-
-#include <stdio.h>
-#include <assert.h>
-#include "satSolver.h"
-#include "extra.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-struct clause_t
-{
- int size_learnt;
- lit lits[0];
-};
-
-static inline int clause_size( clause* c ) { return c->size_learnt >> 1; }
-static inline lit* clause_begin( clause* c ) { return c->lits; }
-
-static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement );
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Write the clauses in the solver into a file in DIMACS format.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars )
-{
- FILE * pFile;
- void ** pClauses;
- int nClauses, i;
-
- // count the number of clauses
- nClauses = p->clauses.size + p->learnts.size;
- for ( i = 0; i < p->size; i++ )
- if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
- nClauses++;
-
- // start the file
- pFile = fopen( pFileName, "wb" );
- if ( pFile == NULL )
- {
- printf( "Sat_SolverWriteDimacs(): Cannot open the ouput file.\n" );
- return;
- }
- fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
- fprintf( pFile, "p cnf %d %d\n", p->size, nClauses );
-
- // write the original clauses
- nClauses = p->clauses.size;
- pClauses = p->clauses.ptr;
- for ( i = 0; i < nClauses; i++ )
- Sat_SolverClauseWriteDimacs( pFile, pClauses[i], incrementVars );
-
- // write the learned clauses
- nClauses = p->learnts.size;
- pClauses = p->learnts.ptr;
- for ( i = 0; i < nClauses; i++ )
- Sat_SolverClauseWriteDimacs( pFile, pClauses[i], incrementVars );
-
- // write zero-level assertions
- for ( i = 0; i < p->size; i++ )
- if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
- fprintf( pFile, "%s%d%s\n",
- (p->assigns[i] == l_False)? "-": "",
- i + (int)(incrementVars>0),
- (incrementVars) ? " 0" : "");
-
- // write the assumptions
- if (assumptionsBegin) {
- for (; assumptionsBegin != assumptionsEnd; assumptionsBegin++) {
- fprintf( pFile, "%s%d%s\n",
- lit_sign(*assumptionsBegin)? "-": "",
- lit_var(*assumptionsBegin) + (int)(incrementVars>0),
- (incrementVars) ? " 0" : "");
- }
- }
-
- fprintf( pFile, "\n" );
- fclose( pFile );
-}
-
-/**Function*************************************************************
-
- Synopsis [Writes the given clause in a file in DIMACS format.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement )
-{
- lit * pLits = clause_begin(pC);
- int nLits = clause_size(pC);
- int i;
-
- for ( i = 0; i < nLits; i++ )
- fprintf( pFile, "%s%d ", (lit_sign(pLits[i])? "-": ""), lit_var(pLits[i]) + (int)(fIncrement>0) );
- if ( fIncrement )
- fprintf( pFile, "0" );
- fprintf( pFile, "\n" );
-}
-
-/**Function*************************************************************
-
- Synopsis [Writes the given clause in a file in DIMACS format.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sat_SolverPrintStats( FILE * pFile, sat_solver * p )
-{
-// printf( "calls : %8d (%d)\n", (int)p->nCalls, (int)p->nCalls2 );
- printf( "starts : %8d\n", (int)p->stats.starts );
- printf( "conflicts : %8d\n", (int)p->stats.conflicts );
- printf( "decisions : %8d\n", (int)p->stats.decisions );
- printf( "propagations : %8d\n", (int)p->stats.propagations );
- printf( "inspects : %8d\n", (int)p->stats.inspects );
-// printf( "inspects2 : %8d\n", (int)p->stats.inspects2 );
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns a counter-example.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars )
-{
- int * pModel;
- int i;
- pModel = ALLOC( int, nVars );
- for ( i = 0; i < nVars; i++ )
- {
- assert( pVars[i] >= 0 && pVars[i] < p->size );
- pModel[i] = (int)(p->model.ptr[pVars[i]] == l_True);
- }
- return pModel;
-}
-
-/**Function*************************************************************
-
- Synopsis [Duplicates all clauses, complements unit clause of the given var.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sat_SolverDoubleClauses( sat_solver * p, int iVar )
-{
- clause * pClause;
- lit Lit, * pLits;
- int RetValue, nClauses, nVarsOld, nLitsOld, nLits, c, v;
- // get the number of variables
- nVarsOld = p->size;
- nLitsOld = 2 * p->size;
- // extend the solver to depend on two sets of variables
- sat_solver_setnvars( p, 2 * p->size );
- // duplicate implications
- for ( v = 0; v < nVarsOld; v++ )
- if ( p->assigns[v] != l_Undef )
- {
- Lit = nLitsOld + toLitCond( v, p->assigns[v]==l_False );
- if ( v == iVar )
- Lit = lit_neg(Lit);
- RetValue = sat_solver_addclause( p, &Lit, &Lit + 1 );
- assert( RetValue );
- }
- // duplicate clauses
- nClauses = vecp_size(&p->clauses);
- for ( c = 0; c < nClauses; c++ )
- {
- pClause = p->clauses.ptr[c];
- nLits = clause_size(pClause);
- pLits = clause_begin(pClause);
- for ( v = 0; v < nLits; v++ )
- pLits[v] += nLitsOld;
- RetValue = sat_solver_addclause( p, pLits, pLits + nLits );
- assert( RetValue );
- for ( v = 0; v < nLits; v++ )
- pLits[v] -= nLitsOld;
- }
-}
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h
deleted file mode 100644
index d7fce5c0..00000000
--- a/src/sat/bsat/satVec.h
+++ /dev/null
@@ -1,83 +0,0 @@
-/**************************************************************************************************
-MiniSat -- Copyright (c) 2005, Niklas Sorensson
-http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
-
-Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
-associated documentation files (the "Software"), to deal in the Software without restriction,
-including without limitation the rights to use, copy, modify, merge, publish, distribute,
-sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in all copies or
-substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
-NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
-DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
-OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
-**************************************************************************************************/
-// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
-
-#ifndef satVec_h
-#define satVec_h
-
-#include <stdlib.h>
-
-// vector of 32-bit intergers (added for 64-bit portability)
-struct veci_t {
- int size;
- int cap;
- int* ptr;
-};
-typedef struct veci_t veci;
-
-static inline void veci_new (veci* v) {
- v->size = 0;
- v->cap = 4;
- v->ptr = (int*)malloc(sizeof(int)*v->cap);
-}
-
-static inline void veci_delete (veci* v) { free(v->ptr); }
-static inline int* veci_begin (veci* v) { return v->ptr; }
-static inline int veci_size (veci* v) { return v->size; }
-static inline void veci_resize (veci* v, int k) { v->size = k; } // only safe to shrink !!
-static inline void veci_push (veci* v, int e)
-{
- if (v->size == v->cap) {
- int newsize = v->cap * 2;//+1;
- v->ptr = (int*)realloc(v->ptr,sizeof(int)*newsize);
- v->cap = newsize; }
- v->ptr[v->size++] = e;
-}
-
-
-// vector of 32- or 64-bit pointers
-struct vecp_t {
- int size;
- int cap;
- void** ptr;
-};
-typedef struct vecp_t vecp;
-
-static inline void vecp_new (vecp* v) {
- v->size = 0;
- v->cap = 4;
- v->ptr = (void**)malloc(sizeof(void*)*v->cap);
-}
-
-static inline void vecp_delete (vecp* v) { free(v->ptr); }
-static inline void** vecp_begin (vecp* v) { return v->ptr; }
-static inline int vecp_size (vecp* v) { return v->size; }
-static inline void vecp_resize (vecp* v, int k) { v->size = k; } // only safe to shrink !!
-static inline void vecp_push (vecp* v, void* e)
-{
- if (v->size == v->cap) {
- int newsize = v->cap * 2;//+1;
- v->ptr = (void**)realloc(v->ptr,sizeof(void*)*newsize);
- v->cap = newsize; }
- v->ptr[v->size++] = e;
-}
-
-
-#endif
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-07 19:13:01 +0000