summaryrefslogtreecommitdiffstats
path: root/src/sat/msat/msatSolverCore.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/msat/msatSolverCore.c')
-rw-r--r--src/sat/msat/msatSolverCore.c212
1 files changed, 0 insertions, 212 deletions
diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c
deleted file mode 100644
index f9fee73c..00000000
--- a/src/sat/msat/msatSolverCore.c
+++ /dev/null
@@ -1,212 +0,0 @@
-/**CFile****************************************************************
-
- FileName [msatSolverCore.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 [The SAT solver core procedures.]
-
- Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - January 1, 2004.]
-
- Revision [$Id: msatSolverCore.c,v 1.2 2004/05/12 03:37:40 satrajit Exp $]
-
-***********************************************************************/
-
-#include "msatInt.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Adds one variable to the solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-bool Msat_SolverAddVar( Msat_Solver_t * p, int Level )
-{
- if ( p->nVars == p->nVarsAlloc )
- Msat_SolverResize( p, 2 * p->nVarsAlloc );
- p->pLevel[p->nVars] = Level;
- p->nVars++;
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds one clause to the solver's clause database.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-bool Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * vLits )
-{
- Msat_Clause_t * pC;
- bool Value;
- Value = Msat_ClauseCreate( p, vLits, 0, &pC );
- if ( pC != NULL )
- Msat_ClauseVecPush( p->vClauses, pC );
-// else if ( p->fProof )
-// Msat_ClauseCreateFake( p, vLits );
- return Value;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns search-space coverage. Not extremely reliable.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-double Msat_SolverProgressEstimate( Msat_Solver_t * p )
-{
- double dProgress = 0.0;
- double dF = 1.0 / p->nVars;
- int i;
- for ( i = 0; i < p->nVars; i++ )
- if ( p->pAssigns[i] != MSAT_VAR_UNASSIGNED )
- dProgress += pow( dF, p->pLevel[i] );
- return dProgress / p->nVars;
-}
-
-/**Function*************************************************************
-
- Synopsis [Prints statistics about the solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Msat_SolverPrintStats( Msat_Solver_t * p )
-{
- printf("C solver (%d vars; %d clauses; %d learned):\n",
- p->nVars, Msat_ClauseVecReadSize(p->vClauses), Msat_ClauseVecReadSize(p->vLearned) );
- printf("starts : %lld\n", p->Stats.nStarts);
- printf("conflicts : %lld\n", p->Stats.nConflicts);
- printf("decisions : %lld\n", p->Stats.nDecisions);
- printf("propagations : %lld\n", p->Stats.nPropagations);
- printf("inspects : %lld\n", p->Stats.nInspects);
-}
-
-/**Function*************************************************************
-
- Synopsis [Top-level solve.]
-
- Description [If using assumptions (non-empty 'assumps' vector), you must
- call 'simplifyDB()' first to see that no top-level conflict is present
- (which would put the solver in an undefined state. If the last argument
- is given (vProj), the solver enumerates through the satisfying solutions,
- which are projected on the variables listed in this array. Note that the
- variables in the array may be complemented, in which case the derived
- assignment for the variable is complemented.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit, int nTimeLimit )
-{
- Msat_SearchParams_t Params = { 0.95, 0.999 };
- double nConflictsLimit, nLearnedLimit;
- Msat_Type_t Status;
- int timeStart = clock();
- int64 nConflictsOld = p->Stats.nConflicts;
- int64 nDecisionsOld = p->Stats.nDecisions;
-
-// p->pFreq = ALLOC( int, p->nVarsAlloc );
-// memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc );
-
- if ( vAssumps )
- {
- int * pAssumps, nAssumps, i;
-
- assert( Msat_IntVecReadSize(p->vTrailLim) == 0 );
-
- nAssumps = Msat_IntVecReadSize( vAssumps );
- pAssumps = Msat_IntVecReadArray( vAssumps );
- for ( i = 0; i < nAssumps; i++ )
- {
- if ( !Msat_SolverAssume(p, pAssumps[i]) || Msat_SolverPropagate(p) )
- {
- Msat_QueueClear( p->pQueue );
- Msat_SolverCancelUntil( p, 0 );
- return MSAT_FALSE;
- }
- }
- }
- p->nLevelRoot = Msat_SolverReadDecisionLevel(p);
- p->nClausesInit = Msat_ClauseVecReadSize( p->vClauses );
- nConflictsLimit = 100;
- nLearnedLimit = Msat_ClauseVecReadSize(p->vClauses) / 3;
- Status = MSAT_UNKNOWN;
- p->nBackTracks = (int)p->Stats.nConflicts;
- while ( Status == MSAT_UNKNOWN )
- {
- if ( p->fVerbose )
- printf("Solving -- conflicts=%d learnts=%d progress=%.4f %%\n",
- (int)nConflictsLimit, (int)nLearnedLimit, p->dProgress*100);
- Status = Msat_SolverSearch( p, (int)nConflictsLimit, (int)nLearnedLimit, nBackTrackLimit, &Params );
- nConflictsLimit *= 1.5;
- nLearnedLimit *= 1.1;
- // if the limit on the number of backtracks is given, quit the restart loop
- if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit )
- break;
- // if the runtime limit is exceeded, quit the restart loop
- if ( nTimeLimit > 0 && clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC )
- break;
- }
- Msat_SolverCancelUntil( p, 0 );
- p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks;
-/*
- PRT( "True solver runtime", clock() - timeStart );
- // print the statistics
- {
- int i, Counter = 0;
- for ( i = 0; i < p->nVars; i++ )
- if ( p->pFreq[i] > 0 )
- {
- printf( "%d ", p->pFreq[i] );
- Counter++;
- }
- if ( Counter )
- printf( "\n" );
- printf( "Total = %d. Used = %d. Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts );
- PRT( "Time", clock() - timeStart );
- }
-*/
- return Status;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-27 04:37:45 +0000