summaryrefslogtreecommitdiffstats
path: root/src/sat/msat/msatSolverApi.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/msat/msatSolverApi.c')
-rw-r--r--src/sat/msat/msatSolverApi.c488
1 files changed, 488 insertions, 0 deletions
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c
new file mode 100644
index 00000000..ba506993
--- /dev/null
+++ b/src/sat/msat/msatSolverApi.c
@@ -0,0 +1,488 @@
+/**CFile****************************************************************
+
+ FileName [msatSolverApi.c]
+
+ PackageName [A C version of SAT solver MINISAT, originally developed
+ in C++ by Niklas Een and Niklas Sorensson, Chalmers University of
+ Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
+
+ Synopsis [APIs of the SAT solver.]
+
+ Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - January 1, 2004.]
+
+ Revision [$Id: msatSolverApi.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "msatInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Simple SAT solver APIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Msat_SolverReadVarNum( Msat_Solver_t * p ) { return p->nVars; }
+int Msat_SolverReadVarAllocNum( Msat_Solver_t * p ) { return p->nVarsAlloc;}
+int Msat_SolverReadDecisionLevel( Msat_Solver_t * p ) { return Msat_IntVecReadSize(p->vTrailLim); }
+int * Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p ) { return p->pLevel; }
+Msat_Clause_t ** Msat_SolverReadReasonArray( Msat_Solver_t * p ) { return p->pReasons; }
+Msat_Lit_t Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var ) { return p->pAssigns[Var]; }
+Msat_ClauseVec_t * Msat_SolverReadLearned( Msat_Solver_t * p ) { return p->vLearned; }
+Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p ) { return p->pvWatched; }
+int * Msat_SolverReadAssignsArray( Msat_Solver_t * p ) { return p->pAssigns; }
+int * Msat_SolverReadModelArray( Msat_Solver_t * p ) { return p->pModel; }
+int Msat_SolverReadBackTracks( Msat_Solver_t * p ) { return p->nBackTracks; }
+Msat_MmStep_t * Msat_SolverReadMem( Msat_Solver_t * p ) { return p->pMem; }
+int * Msat_SolverReadSeenArray( Msat_Solver_t * p ) { return p->pSeen; }
+int Msat_SolverIncrementSeenId( Msat_Solver_t * p ) { return ++p->nSeenId; }
+void Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose ) { p->fVerbose = fVerbose; }
+void Msat_SolverClausesIncrement( Msat_Solver_t * p ) { p->nClausesAlloc++; }
+void Msat_SolverClausesDecrement( Msat_Solver_t * p ) { p->nClausesAlloc--; }
+void Msat_SolverClausesIncrementL( Msat_Solver_t * p ) { p->nClausesAllocL++; }
+void Msat_SolverClausesDecrementL( Msat_Solver_t * p ) { p->nClausesAllocL--; }
+void Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p ) { Msat_ClauseSetTypeA( Msat_ClauseVecReadEntry( p->vClauses, Msat_ClauseVecReadSize(p->vClauses)-1 ), 1 ); }
+void Msat_SolverMarkClausesStart( Msat_Solver_t * p ) { p->nClausesStart = Msat_ClauseVecReadSize(p->vClauses); }
+
+/**Function*************************************************************
+
+ Synopsis [Reads the clause with the given number.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Msat_Clause_t * Msat_SolverReadClause( Msat_Solver_t * p, int Num )
+{
+ int nClausesP;
+ assert( Num < p->nClauses );
+ nClausesP = Msat_ClauseVecReadSize( p->vClauses );
+ if ( Num < nClausesP )
+ return Msat_ClauseVecReadEntry( p->vClauses, Num );
+ return Msat_ClauseVecReadEntry( p->vLearned, Num - nClausesP );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads the clause with the given number.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Msat_ClauseVec_t * Msat_SolverReadAdjacents( Msat_Solver_t * p )
+{
+ return p->vAdjacents;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads the clause with the given number.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Msat_IntVec_t * Msat_SolverReadConeVars( Msat_Solver_t * p )
+{
+ return p->vConeVars;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads the clause with the given number.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Msat_IntVec_t * Msat_SolverReadVarsUsed( Msat_Solver_t * p )
+{
+ return p->vVarsUsed;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Allocates the solver.]
+
+ Description [After the solver is allocated, the procedure
+ Msat_SolverClean() should be called to set the number of variables.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc,
+ double dClaInc, double dClaDecay,
+ double dVarInc, double dVarDecay,
+ bool fVerbose )
+{
+ Msat_Solver_t * p;
+ int i;
+
+ assert(sizeof(Msat_Lit_t) == sizeof(unsigned));
+ assert(sizeof(float) == sizeof(unsigned));
+
+ p = ALLOC( Msat_Solver_t, 1 );
+ memset( p, 0, sizeof(Msat_Solver_t) );
+
+ p->nVarsAlloc = nVarsAlloc;
+ p->nVars = 0;
+
+ p->nClauses = 0;
+ p->vClauses = Msat_ClauseVecAlloc( 512 );
+ p->vLearned = Msat_ClauseVecAlloc( 512 );
+
+ p->dClaInc = dClaInc;
+ p->dClaDecay = dClaDecay;
+ p->dVarInc = dVarInc;
+ p->dVarDecay = dVarDecay;
+
+ p->pdActivity = ALLOC( double, p->nVarsAlloc );
+ for ( i = 0; i < p->nVarsAlloc; i++ )
+ p->pdActivity[i] = 0;
+
+ p->pAssigns = ALLOC( int, p->nVarsAlloc );
+ p->pModel = ALLOC( int, p->nVarsAlloc );
+ for ( i = 0; i < p->nVarsAlloc; i++ )
+ p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
+// p->pOrder = Msat_OrderAlloc( p->pAssigns, p->pdActivity, p->nVarsAlloc );
+ p->pOrder = Msat_OrderAlloc( p );
+
+ p->pvWatched = ALLOC( Msat_ClauseVec_t *, 2 * p->nVarsAlloc );
+ for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
+ p->pvWatched[i] = Msat_ClauseVecAlloc( 16 );
+ p->pQueue = Msat_QueueAlloc( p->nVarsAlloc );
+
+ p->vTrail = Msat_IntVecAlloc( p->nVarsAlloc );
+ p->vTrailLim = Msat_IntVecAlloc( p->nVarsAlloc );
+ p->pReasons = ALLOC( Msat_Clause_t *, p->nVarsAlloc );
+ memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVarsAlloc );
+ p->pLevel = ALLOC( int, p->nVarsAlloc );
+ for ( i = 0; i < p->nVarsAlloc; i++ )
+ p->pLevel[i] = -1;
+ p->dRandSeed = 91648253;
+ p->fVerbose = fVerbose;
+ p->dProgress = 0.0;
+// p->pModel = Msat_IntVecAlloc( p->nVarsAlloc );
+ p->pMem = Msat_MmStepStart( 10 );
+
+ p->vConeVars = Msat_IntVecAlloc( p->nVarsAlloc );
+ p->vAdjacents = Msat_ClauseVecAlloc( p->nVarsAlloc );
+ for ( i = 0; i < p->nVarsAlloc; i++ )
+ Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) );
+ p->vVarsUsed = Msat_IntVecAlloc( p->nVarsAlloc );
+ Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 );
+
+
+ p->pSeen = ALLOC( int, p->nVarsAlloc );
+ memset( p->pSeen, 0, sizeof(int) * p->nVarsAlloc );
+ p->nSeenId = 1;
+ p->vReason = Msat_IntVecAlloc( p->nVarsAlloc );
+ p->vTemp = Msat_IntVecAlloc( p->nVarsAlloc );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Resizes the solver.]
+
+ Description [Assumes that the solver contains some clauses, and that
+ it is currently between the calls. Resizes the solver to accomodate
+ more variables.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc )
+{
+ int nVarsAllocOld, i;
+
+ nVarsAllocOld = p->nVarsAlloc;
+ p->nVarsAlloc = nVarsAlloc;
+
+ p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc );
+ for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
+ p->pdActivity[i] = 0;
+
+ p->pAssigns = REALLOC( int, p->pAssigns, p->nVarsAlloc );
+ p->pModel = REALLOC( int, p->pModel, p->nVarsAlloc );
+ for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
+ p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
+
+// Msat_OrderRealloc( p->pOrder, p->pAssigns, p->pdActivity, p->nVarsAlloc );
+ Msat_OrderSetBounds( p->pOrder, p->nVarsAlloc );
+
+ p->pvWatched = REALLOC( Msat_ClauseVec_t *, p->pvWatched, 2 * p->nVarsAlloc );
+ for ( i = 2 * nVarsAllocOld; i < 2 * p->nVarsAlloc; i++ )
+ p->pvWatched[i] = Msat_ClauseVecAlloc( 16 );
+
+ Msat_QueueFree( p->pQueue );
+ p->pQueue = Msat_QueueAlloc( p->nVarsAlloc );
+
+ p->pReasons = REALLOC( Msat_Clause_t *, p->pReasons, p->nVarsAlloc );
+ p->pLevel = REALLOC( int, p->pLevel, p->nVarsAlloc );
+ for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
+ {
+ p->pReasons[i] = NULL;
+ p->pLevel[i] = -1;
+ }
+
+ p->pSeen = REALLOC( int, p->pSeen, p->nVarsAlloc );
+ for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
+ p->pSeen[i] = 0;
+
+ Msat_IntVecGrow( p->vTrail, p->nVarsAlloc );
+ Msat_IntVecGrow( p->vTrailLim, p->nVarsAlloc );
+
+ // make sure the array of adjucents has room to store the variable numbers
+ for ( i = Msat_ClauseVecReadSize(p->vAdjacents); i < p->nVarsAlloc; i++ )
+ Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) );
+ Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prepares the solver.]
+
+ Description [Cleans the solver assuming that the problem will involve
+ the given number of variables (nVars). This procedure is useful
+ for many small (incremental) SAT problems, to prevent the solver
+ from being reallocated each time.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Msat_SolverClean( Msat_Solver_t * p, int nVars )
+{
+ int i;
+ // free the clauses
+ int nClauses;
+ Msat_Clause_t ** pClauses;
+
+ assert( p->nVarsAlloc >= nVars );
+ p->nVars = nVars;
+ p->nClauses = 0;
+
+ nClauses = Msat_ClauseVecReadSize( p->vClauses );
+ pClauses = Msat_ClauseVecReadArray( p->vClauses );
+ for ( i = 0; i < nClauses; i++ )
+ Msat_ClauseFree( p, pClauses[i], 0 );
+// Msat_ClauseVecFree( p->vClauses );
+ Msat_ClauseVecClear( p->vClauses );
+
+ nClauses = Msat_ClauseVecReadSize( p->vLearned );
+ pClauses = Msat_ClauseVecReadArray( p->vLearned );
+ for ( i = 0; i < nClauses; i++ )
+ Msat_ClauseFree( p, pClauses[i], 0 );
+// Msat_ClauseVecFree( p->vLearned );
+ Msat_ClauseVecClear( p->vLearned );
+
+// FREE( p->pdActivity );
+ for ( i = 0; i < p->nVars; i++ )
+ p->pdActivity[i] = 0;
+
+// Msat_OrderFree( p->pOrder );
+// Msat_OrderClean( p->pOrder, p->nVars, NULL );
+ Msat_OrderSetBounds( p->pOrder, p->nVars );
+
+ for ( i = 0; i < 2 * p->nVars; i++ )
+// Msat_ClauseVecFree( p->pvWatched[i] );
+ Msat_ClauseVecClear( p->pvWatched[i] );
+// FREE( p->pvWatched );
+// Msat_QueueFree( p->pQueue );
+ Msat_QueueClear( p->pQueue );
+
+// FREE( p->pAssigns );
+ for ( i = 0; i < p->nVars; i++ )
+ p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
+// Msat_IntVecFree( p->vTrail );
+ Msat_IntVecClear( p->vTrail );
+// Msat_IntVecFree( p->vTrailLim );
+ Msat_IntVecClear( p->vTrailLim );
+// FREE( p->pReasons );
+ memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVars );
+// FREE( p->pLevel );
+ for ( i = 0; i < p->nVars; i++ )
+ p->pLevel[i] = -1;
+// Msat_IntVecFree( p->pModel );
+// Msat_MmStepStop( p->pMem, 0 );
+ p->dRandSeed = 91648253;
+ p->dProgress = 0.0;
+
+// FREE( p->pSeen );
+ memset( p->pSeen, 0, sizeof(int) * p->nVars );
+ p->nSeenId = 1;
+// Msat_IntVecFree( p->vReason );
+ Msat_IntVecClear( p->vReason );
+// Msat_IntVecFree( p->vTemp );
+ Msat_IntVecClear( p->vTemp );
+// printf(" The number of clauses remaining = %d (%d).\n", p->nClausesAlloc, p->nClausesAllocL );
+// FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Frees the solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Msat_SolverFree( Msat_Solver_t * p )
+{
+ int i;
+
+ // free the clauses
+ int nClauses;
+ Msat_Clause_t ** pClauses;
+//printf( "clauses = %d. learned = %d.\n", Msat_ClauseVecReadSize( p->vClauses ),
+// Msat_ClauseVecReadSize( p->vLearned ) );
+
+ nClauses = Msat_ClauseVecReadSize( p->vClauses );
+ pClauses = Msat_ClauseVecReadArray( p->vClauses );
+ for ( i = 0; i < nClauses; i++ )
+ Msat_ClauseFree( p, pClauses[i], 0 );
+ Msat_ClauseVecFree( p->vClauses );
+
+ nClauses = Msat_ClauseVecReadSize( p->vLearned );
+ pClauses = Msat_ClauseVecReadArray( p->vLearned );
+ for ( i = 0; i < nClauses; i++ )
+ Msat_ClauseFree( p, pClauses[i], 0 );
+ Msat_ClauseVecFree( p->vLearned );
+
+ FREE( p->pdActivity );
+ Msat_OrderFree( p->pOrder );
+
+ for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
+ Msat_ClauseVecFree( p->pvWatched[i] );
+ FREE( p->pvWatched );
+ Msat_QueueFree( p->pQueue );
+
+ FREE( p->pAssigns );
+ FREE( p->pModel );
+ Msat_IntVecFree( p->vTrail );
+ Msat_IntVecFree( p->vTrailLim );
+ FREE( p->pReasons );
+ FREE( p->pLevel );
+
+ Msat_MmStepStop( p->pMem, 0 );
+
+ nClauses = Msat_ClauseVecReadSize( p->vAdjacents );
+ pClauses = Msat_ClauseVecReadArray( p->vAdjacents );
+ for ( i = 0; i < nClauses; i++ )
+ Msat_IntVecFree( (Msat_IntVec_t *)pClauses[i] );
+ Msat_ClauseVecFree( p->vAdjacents );
+ Msat_IntVecFree( p->vConeVars );
+ Msat_IntVecFree( p->vVarsUsed );
+
+ FREE( p->pSeen );
+ Msat_IntVecFree( p->vReason );
+ Msat_IntVecFree( p->vTemp );
+ FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prepares the solver to run on a subset of variables.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Msat_SolverPrepare( Msat_Solver_t * p, Msat_IntVec_t * vVars )
+{
+
+ int i;
+ // undo the previous data
+ for ( i = 0; i < p->nVarsAlloc; i++ )
+ {
+ p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
+ p->pReasons[i] = NULL;
+ p->pLevel[i] = -1;
+ p->pdActivity[i] = 0.0;
+ }
+
+ // set the new variable order
+ Msat_OrderClean( p->pOrder, vVars );
+
+ Msat_QueueClear( p->pQueue );
+ Msat_IntVecClear( p->vTrail );
+ Msat_IntVecClear( p->vTrailLim );
+ p->dProgress = 0.0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sets up the truth tables.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Msat_SolverSetupTruthTables( unsigned uTruths[][2] )
+{
+ int m, v;
+ // set up the truth tables
+ for ( m = 0; m < 32; m++ )
+ for ( v = 0; v < 5; v++ )
+ if ( m & (1 << v) )
+ uTruths[v][0] |= (1 << m);
+ // make adjustments for the case of 6 variables
+ for ( v = 0; v < 5; v++ )
+ uTruths[v][1] = uTruths[v][0];
+ uTruths[5][0] = 0;
+ uTruths[5][1] = ~((unsigned)0);
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 22:08:55 +0000