diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-25 18:08:48 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-25 18:08:48 -0800 |
commit | d2db956a618fd9be1915a6c66b063c894e540fee (patch) | |
tree | 0b2df03a20bfccd0b2d1eab44cfd456a1070c244 /src/sat/bsat/satUtil.c | |
parent | 0f594b78fae6f45cee463fe47e6f2c0fb33abaf2 (diff) | |
download | abc-d2db956a618fd9be1915a6c66b063c894e540fee.tar.gz abc-d2db956a618fd9be1915a6c66b063c894e540fee.tar.bz2 abc-d2db956a618fd9be1915a6c66b063c894e540fee.zip |
Started experiments with a new solver.
Diffstat (limited to 'src/sat/bsat/satUtil.c')
-rw-r--r-- | src/sat/bsat/satUtil.c | 62 |
1 files changed, 55 insertions, 7 deletions
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c index 0ce40acd..c8569606 100644 --- a/src/sat/bsat/satUtil.c +++ b/src/sat/bsat/satUtil.c @@ -21,6 +21,7 @@ #include <stdio.h> #include <assert.h> #include "satSolver.h" +#include "satSolver2.h" ABC_NAMESPACE_IMPL_START @@ -148,13 +149,36 @@ void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement ) ***********************************************************************/ 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 ); +// printf( "calls : %10d (%d)\n", (int)p->nCalls, (int)p->nCalls2 ); + printf( "starts : %10d\n", (int)p->stats.starts ); + printf( "conflicts : %10d\n", (int)p->stats.conflicts ); + printf( "decisions : %10d\n", (int)p->stats.decisions ); + printf( "propagations : %10d\n", (int)p->stats.propagations ); + printf( "inspects : %10d\n", (int)p->stats.inspects ); +// printf( "inspects2 : %10d\n", (int)p->stats.inspects2 ); +} + +/**Function************************************************************* + + Synopsis [Writes the given clause in a file in DIMACS format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * p ) +{ +// printf( "calls : %10d (%d)\n", (int)p->nCalls, (int)p->nCalls2 ); + printf( "starts : %10d\n", (int)p->stats.starts ); + printf( "conflicts : %10d\n", (int)p->stats.conflicts ); + printf( "decisions : %10d\n", (int)p->stats.decisions ); + printf( "propagations : %10d\n", (int)p->stats.propagations ); + printf( "inspects : %10d\n", (int)p->stats.inspects ); +// printf( "inspects2 : %10d\n", (int)p->stats.inspects2 ); + printf( "memory : %10d\n", p->nMemSize ); } /**Function************************************************************* @@ -183,6 +207,30 @@ int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars ) /**Function************************************************************* + Synopsis [Returns a counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars ) +{ + int * pModel; + int i; + pModel = ABC_CALLOC( int, nVars+1 ); + 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 [] |