diff options
Diffstat (limited to 'src/sat/asat/added.c')
-rw-r--r-- | src/sat/asat/added.c | 126 |
1 files changed, 0 insertions, 126 deletions
diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c deleted file mode 100644 index d7f5b104..00000000 --- a/src/sat/asat/added.c +++ /dev/null @@ -1,126 +0,0 @@ -/**CFile**************************************************************** - - FileName [added.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: added.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include <stdio.h> -#include <assert.h> -#include "solver.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 inline int lit_var(lit l) { return l >> 1; } -static inline int lit_sign(lit l) { return (l & 1); } - -static void Asat_ClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement ); - - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Write the clauses in the solver into a file in DIMACS format.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_SolverWriteDimacs( solver * p, char * pFileName ) -{ - 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" ); - 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++ ) - Asat_ClauseWriteDimacs( pFile, pClauses[i], 1 ); - - // write the learned clauses - nClauses = p->learnts.size; - pClauses = p->learnts.ptr; - for ( i = 0; i < nClauses; i++ ) - Asat_ClauseWriteDimacs( pFile, pClauses[i], 1 ); - - // 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 0\n", (p->assigns[i] == l_False)? "-": "", i + 1 ); - - fprintf( pFile, "\n" ); - fclose( pFile ); -} - -/**Function************************************************************* - - Synopsis [Writes the given clause in a file in DIMACS format.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_ClauseWriteDimacs( 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" ); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |