luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Version abc80307

This commit is contained in:
Alan Mishchenko 2008-03-07 08:01:00 -08:00
parent 8bd19a27bf
commit 8eeecc5175
18 changed files with 1191 additions and 59 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Makefile
View File

@ -24,7 +24,7 @@ MODULES := src/base/abc src/base/abci src/base/cmd \
default: $(PROG)
#OPTFLAGS := -DNDEBUG -O3
OPTFLAGS := -g -O
OPTFLAGS := -g -O -DLIN64
CFLAGS += -Wall -Wno-unused-function $(OPTFLAGS) $(patsubst %, -I%, $(MODULES))
CXXFLAGS += $(CFLAGS)

4
abc.dsp
View File

@ -1178,6 +1178,10 @@ SOURCE=.\src\sat\bsat\satInterA.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bsat\satInterP.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bsat\satMem.c
# End Source File
# Begin Source File

7
readme
View File

@ -21,6 +21,13 @@ Several things to try if it does not compile on your platform:
compiling ABC with gcc. Please try installing this library from
http://tiswww.case.edu/php/chet/readline/rltop.html
To compile the latest version of ABC, you may need to define "LIN" or "LIN64"
(depending on whether you are using 32- or 64-bit Linux).
For example, instead of
OPTFLAGS := -g -O
use
OPTFLAGS := -g -O -DLIN64
in Makefile.
Finally, run regression test:
abc>>> so regtest.script

12
src/aig/aig/aigInter.c
View File

@ -162,7 +162,17 @@ clk = clock();
pRes = Inta_ManInterpolate( pManInter, pSatCnf, vVarsAB, fVerbose );
Inta_ManFree( pManInter );
timeInt += clock() - clk;
/*
// test UNSAT core computation
{
Intp_Man_t * pManProof;
Vec_Int_t * vCore;
pManProof = Intp_ManAlloc();
vCore = Intp_ManUnsatCore( pManProof, pSatCnf, 0 );
Intp_ManFree( pManProof );
Vec_IntFree( vCore );
}
*/
Vec_IntFree( vVarsAB );
Sto_ManFree( pSatCnf );
return pRes;

60
src/aig/kit/cloud.c
View File

@ -105,8 +105,8 @@ clk2 = clock();
dd->nSignCur = 1;
dd->tUnique[0].s = dd->nSignCur;
dd->tUnique[0].v = CLOUD_CONST_INDEX;
dd->tUnique[0].e = CLOUD_VOID;
dd->tUnique[0].t = CLOUD_VOID;
dd->tUnique[0].e = NULL;
dd->tUnique[0].t = NULL;
dd->one = dd->tUnique;
dd->zero = Cloud_Not(dd->one);
dd->nNodesCur = 1;
@ -256,7 +256,7 @@ CloudNode * Cloud_MakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudN
if ( Cloud_IsComplement(t) )
{
pRes = cloudMakeNode( dd, v, Cloud_Not(t), Cloud_Not(e) );
if ( pRes != CLOUD_VOID )
if ( pRes != NULL )
pRes = Cloud_Not(pRes);
}
else
@ -314,7 +314,7 @@ CloudNode * cloudMakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNo
printf( "Cloud needs restart!\n" );
// fflush( stdout );
// exit(1);
return CLOUD_VOID;
return NULL;
}
// create the node
entryUnique->s = dd->nSignCur;
@ -367,7 +367,7 @@ CloudNode * cloudBddAnd( CloudManager * dd, CloudNode * f, CloudNode * g )
cacheEntry = dd->tCaches[CLOUD_OPER_AND] + cloudHashCudd2(f, g, dd->shiftCache[CLOUD_OPER_AND]);
// cacheEntry = dd->tCaches[CLOUD_OPER_AND] + cloudHashBuddy2(f, g, dd->shiftCache[CLOUD_OPER_AND]);
r = cloudCacheLookup2( cacheEntry, dd->nSignCur, f, g );
if ( r != CLOUD_VOID )
if ( r != NULL )
{
dd->nCacheHits++;
return r;
@ -419,16 +419,16 @@ CloudNode * cloudBddAnd( CloudManager * dd, CloudNode * f, CloudNode * g )
else
t = cloudBddAnd( dd, gv, fv );
if ( t == CLOUD_VOID )
return CLOUD_VOID;
if ( t == NULL )
return NULL;
if ( fnv <= gnv )
e = cloudBddAnd( dd, fnv, gnv );
else
e = cloudBddAnd( dd, gnv, fnv );
if ( e == CLOUD_VOID )
return CLOUD_VOID;
if ( e == NULL )
return NULL;
if ( t == e )
r = t;
@ -437,15 +437,15 @@ CloudNode * cloudBddAnd( CloudManager * dd, CloudNode * f, CloudNode * g )
if ( Cloud_IsComplement(t) )
{
r = cloudMakeNode( dd, var, Cloud_Not(t), Cloud_Not(e) );
if ( r == CLOUD_VOID )
return CLOUD_VOID;
if ( r == NULL )
return NULL;
r = Cloud_Not(r);
}
else
{
r = cloudMakeNode( dd, var, t, e );
if ( r == CLOUD_VOID )
return CLOUD_VOID;
if ( r == NULL )
return NULL;
}
}
cloudCacheInsert2( cacheEntry, dd->nSignCur, f, g, r );
@ -484,8 +484,8 @@ static inline CloudNode * cloudBddAnd_gate( CloudManager * dd, CloudNode * f, Cl
******************************************************************************/
CloudNode * Cloud_bddAnd( CloudManager * dd, CloudNode * f, CloudNode * g )
{
if ( Cloud_Regular(f) == CLOUD_VOID || Cloud_Regular(g) == CLOUD_VOID )
return CLOUD_VOID;
if ( Cloud_Regular(f) == NULL || Cloud_Regular(g) == NULL )
return NULL;
CLOUD_ASSERT(f);
CLOUD_ASSERT(g);
if ( dd->tCaches[CLOUD_OPER_AND] == NULL )
@ -507,14 +507,14 @@ CloudNode * Cloud_bddAnd( CloudManager * dd, CloudNode * f, CloudNode * g )
CloudNode * Cloud_bddOr( CloudManager * dd, CloudNode * f, CloudNode * g )
{
CloudNode * res;
if ( Cloud_Regular(f) == CLOUD_VOID || Cloud_Regular(g) == CLOUD_VOID )
return CLOUD_VOID;
if ( Cloud_Regular(f) == NULL || Cloud_Regular(g) == NULL )
return NULL;
CLOUD_ASSERT(f);
CLOUD_ASSERT(g);
if ( dd->tCaches[CLOUD_OPER_AND] == NULL )
cloudCacheAllocate( dd, CLOUD_OPER_AND );
res = cloudBddAnd_gate( dd, Cloud_Not(f), Cloud_Not(g) );
res = Cloud_NotCond( res, res != CLOUD_VOID );
res = Cloud_NotCond( res, res != NULL );
return res;
}
@ -532,18 +532,18 @@ CloudNode * Cloud_bddOr( CloudManager * dd, CloudNode * f, CloudNode * g )
CloudNode * Cloud_bddXor( CloudManager * dd, CloudNode * f, CloudNode * g )
{
CloudNode * t0, * t1, * r;
if ( Cloud_Regular(f) == CLOUD_VOID || Cloud_Regular(g) == CLOUD_VOID )
return CLOUD_VOID;
if ( Cloud_Regular(f) == NULL || Cloud_Regular(g) == NULL )
return NULL;
CLOUD_ASSERT(f);
CLOUD_ASSERT(g);
if ( dd->tCaches[CLOUD_OPER_AND] == NULL )
cloudCacheAllocate( dd, CLOUD_OPER_AND );
t0 = cloudBddAnd_gate( dd, f, Cloud_Not(g) );
if ( t0 == CLOUD_VOID )
return CLOUD_VOID;
if ( t0 == NULL )
return NULL;
t1 = cloudBddAnd_gate( dd, Cloud_Not(f), g );
if ( t1 == CLOUD_VOID )
return CLOUD_VOID;
if ( t1 == NULL )
return NULL;
r = Cloud_bddOr( dd, t0, t1 );
return r;
}
@ -631,7 +631,7 @@ CloudNode * Cloud_Support( CloudManager * dd, CloudNode * n )
if ( support[i] == 1 )
{
res = Cloud_bddAnd( dd, res, dd->vars[i] );
if ( res == CLOUD_VOID )
if ( res == NULL )
break;
}
FREE( support );
@ -831,8 +831,8 @@ CloudNode * Cloud_GetOneCube( CloudManager * dd, CloudNode * bFunc )
// try to find the cube with the negative literal
res = Cloud_GetOneCube( dd, bFunc0 );
if ( res == CLOUD_VOID )
return CLOUD_VOID;
if ( res == NULL )
return NULL;
if ( res != dd->zero )
{
@ -842,8 +842,8 @@ CloudNode * Cloud_GetOneCube( CloudManager * dd, CloudNode * bFunc )
{
// try to find the cube with the positive literal
res = Cloud_GetOneCube( dd, bFunc1 );
if ( res == CLOUD_VOID )
return CLOUD_VOID;
if ( res == NULL )
return NULL;
assert( res != dd->zero );
res = Cloud_bddAnd( dd, res, dd->vars[Cloud_V(bFunc)] );
}
@ -873,7 +873,7 @@ void Cloud_bddPrint( CloudManager * dd, CloudNode * Func )
while ( 1 )
{
Cube = Cloud_GetOneCube( dd, Func );
if ( Cube == CLOUD_VOID || Cube == dd->zero )
if ( Cube == NULL || Cube == dd->zero )
break;
if ( fFirst ) fFirst = 0;
else printf( " + " );

18
src/aig/kit/cloud.h
View File

@ -27,6 +27,7 @@ extern "C" {
#include <stdlib.h>
#include <assert.h>
#include <time.h>
#include "port_type.h"
#ifdef _WIN32
#define inline __inline // compatible with MS VS 6.0
@ -162,9 +163,6 @@ struct cloudCacheEntry3 // the three-argument cache
// parameters
#define CLOUD_NODE_BITS 23
#define CLOUD_ONE ((unsigned)0x00000001)
#define CLOUD_NOT_ONE ((unsigned)0xfffffffe)
#define CLOUD_VOID ((unsigned)0x00000000)
#define CLOUD_CONST_INDEX ((unsigned)0x0fffffff)
#define CLOUD_MARK_ON ((unsigned)0x10000000)
@ -182,10 +180,10 @@ struct cloudCacheEntry3 // the three-argument cache
#define cloudHashCudd3(f,g,h,s) (((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2 + (unsigned)(h)) * DD_P3) >> (s))
// node complementation (using node)
#define Cloud_Regular(p) ((CloudNode*)(((unsigned)(p)) & CLOUD_NOT_ONE)) // get the regular node (w/o bubble)
#define Cloud_Not(p) ((CloudNode*)(((unsigned)(p)) ^ CLOUD_ONE)) // complement the node
#define Cloud_NotCond(p,c) (((int)(c))? Cloud_Not(p):(p)) // complement the node conditionally
#define Cloud_IsComplement(p) ((int)(((unsigned)(p)) & CLOUD_ONE)) // check if complemented
#define Cloud_Regular(p) ((CloudNode*)(((PORT_PTRUINT_T)(p)) & ~01)) // get the regular node (w/o bubble)
#define Cloud_Not(p) ((CloudNode*)(((PORT_PTRUINT_T)(p)) ^ 01)) // complement the node
#define Cloud_NotCond(p,c) ((CloudNode*)(((PORT_PTRUINT_T)(p)) ^ (c))) // complement the node conditionally
#define Cloud_IsComplement(p) ((int)(((PORT_PTRUINT_T)(p)) & 01)) // check if complemented
// checking constants (using node)
#define Cloud_IsConstant(p) (((Cloud_Regular(p))->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX)
#define cloudIsConstant(p) (((p)->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX)
@ -204,9 +202,9 @@ struct cloudCacheEntry3 // the three-argument cache
#define cloudNodeIsMarked(p) ((int)((p)->v & CLOUD_MARK_ON))
// cache lookups and inserts (using node)
#define cloudCacheLookup1(p,sign,f) (((p)->s == (sign) && (p)->a == (f))? ((p)->r): (CLOUD_VOID))
#define cloudCacheLookup2(p,sign,f,g) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g))? ((p)->r): (CLOUD_VOID))
#define cloudCacheLookup3(p,sign,f,g,h) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g) && (p)->c == (h))? ((p)->r): (CLOUD_VOID))
#define cloudCacheLookup1(p,sign,f) (((p)->s == (sign) && (p)->a == (f))? ((p)->r): (0))
#define cloudCacheLookup2(p,sign,f,g) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g))? ((p)->r): (0))
#define cloudCacheLookup3(p,sign,f,g,h) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g) && (p)->c == (h))? ((p)->r): (0))
// cache inserts
#define cloudCacheInsert1(p,sign,f,r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->r = (r)))
#define cloudCacheInsert2(p,sign,f,g,r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->r = (r)))

9
src/base/abci/abcDar.c
View File

@ -266,6 +266,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Abc_NtkAddDummyBoxNames( pNtkNew );
else
{
/*
{
int i, k, iFlop, Counter = 0;
FILE * pFile;
@ -285,6 +286,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
fclose( pFile );
//printf( "\n" );
}
*/
assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) );
nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtkNew) );
Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
@ -1622,11 +1624,14 @@ timeInt = 0;
}
else
pNtkInter1 = Abc_NtkInterOne( pNtkOn1, pNtkOff1, fVerbose );
Abc_NtkAppend( pNtkInter, pNtkInter1, 1 );
if ( pNtkInter1 )
{
Abc_NtkAppend( pNtkInter, pNtkInter1, 1 );
Abc_NtkDelete( pNtkInter1 );
}
Abc_NtkDelete( pNtkOn1 );
Abc_NtkDelete( pNtkOff1 );
Abc_NtkDelete( pNtkInter1 );
}
// PRT( "CNF", timeCnf );
// PRT( "SAT", timeSat );

4
src/base/abci/abcDelay.c
View File

@ -33,11 +33,12 @@ static inline void Abc_ObjSetArrival( Abc_Obj_t * pNode, float Time ) { pNode-
static inline void Abc_ObjSetRequired( Abc_Obj_t * pNode, float Time ) { pNode->pNtk->pLutTimes[3*pNode->Id+1] = Time; }
static inline void Abc_ObjSetSlack( Abc_Obj_t * pNode, float Time ) { pNode->pNtk->pLutTimes[3*pNode->Id+2] = Time; }
extern void * Abc_FrameReadLibLut();
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Sorts the pins in the decreasing order of delays.]
@ -95,7 +96,6 @@ void Abc_NtkDelayTraceSortPins( Abc_Obj_t * pNode, int * pPinPerm, float * pPinD
***********************************************************************/
float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib )
{
extern void * Abc_FrameReadLibLut();
int fUseSorting = 0;
int pPinPerm[32];
float pPinDelays[32];

2
src/base/abci/abcGen.c
View File

@ -131,7 +131,7 @@ void Abc_GenSorter( char * pFileName, int nVars )
fprintf( pFile, " y%02d=%0*d", k, nDigits, Counter++ );
fprintf( pFile, "\n" );
Counter -= nVars;
for ( i = 1; i < nVars-2; i++ )
for ( i = 1; i < 2*nVars-2; i++ )
{
fprintf( pFile, ".subckt Layer%d", (i&1) );
for ( k = 0; k < nVars; k++ )

125
src/base/abci/abcSat.c
View File

@ -590,6 +590,16 @@ int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
nVars = ABC_MIN( nVars, 10 );
ASat_SolverSetPrefVars( pSat, pPrefVars, nVars );
}
*/
/*
Abc_NtkForEachObj( pNtk, pNode, i )
{
if ( !pNode->fMarkA )
continue;
printf( "%10s : ", Abc_ObjName(pNode) );
printf( "%3d\n", (int)pNode->pCopy );
}
printf( "\n" );
*/
RetValue = 1;
Quits :
@ -876,6 +886,121 @@ finish:
/**Function*************************************************************
Synopsis [Writes CNF for the sorter with N inputs asserting Q ones.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens )
{
extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
extern void * Abc_FrameGetGlobalFrame();
extern Abc_Ntk_t * Abc_FrameReadNtk( void * p );
char Command[100];
void * pAbc;
Abc_Ntk_t * pNtk;
Abc_Obj_t * pObj, * ppNodes[2], * ppRoots[2];
Vec_Ptr_t * vNodes;
FILE * pFile;
int i, Counter;
if ( nQueens <= 0 && nQueens >= nVars )
{
printf( "The number of queens (Q = %d) should belong to the interval: 0 < Q < %d.\n", nQueens, nQueens, nVars );
return;
}
assert( nQueens > 0 && nQueens < nVars );
pAbc = Abc_FrameGetGlobalFrame();
// generate sorter
sprintf( Command, "gen -s -N %d sorter%d.blif", nVars, nVars );
if ( Cmd_CommandExecute( pAbc, Command ) )
{
fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
return;
}
// read the file
sprintf( Command, "read sorter%d.blif; strash", nVars );
if ( Cmd_CommandExecute( pAbc, Command ) )
{
fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
return;
}
// get the current network
pNtk = Abc_FrameReadNtk(pAbc);
// collect the nodes for the given two primary outputs
ppNodes[0] = Abc_NtkPo( pNtk, nVars - nQueens - 1 );
ppNodes[1] = Abc_NtkPo( pNtk, nVars - nQueens );
ppRoots[0] = Abc_ObjFanin0( ppNodes[0] );
ppRoots[1] = Abc_ObjFanin0( ppNodes[1] );
vNodes = Abc_NtkDfsNodes( pNtk, ppRoots, 2 );
// assign CNF variables
Counter = 0;
Abc_NtkForEachObj( pNtk, pObj, i )
pObj->pCopy = (void *)~0;
Abc_NtkForEachPi( pNtk, pObj, i )
pObj->pCopy = (void *)Counter++;
Vec_PtrForEachEntry( vNodes, pObj, i )
pObj->pCopy = (void *)Counter++;
/*
OutVar = pCnf->pVarNums[ pObj->Id ];
pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];
// positive phase
*pClas++ = pLits;
*pLits++ = 2 * OutVar;
*pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj);
*pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj);
// negative phase
*pClas++ = pLits;
*pLits++ = 2 * OutVar + 1;
*pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj);
*pClas++ = pLits;
*pLits++ = 2 * OutVar + 1;
*pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj);
*/
// add clauses for these nodes
pFile = fopen( pFileName, "w" );
fprintf( pFile, "c CNF for %d-bit sorter with %d bits set to 1 generated by ABC.\n", nVars, nQueens );
fprintf( pFile, "p cnf %d %d\n", Counter, 3 * Vec_PtrSize(vNodes) + 2 );
Vec_PtrForEachEntry( vNodes, pObj, i )
{
// positive phase
fprintf( pFile, "%d %s%d %s%d 0\n", 1+(int)pObj->pCopy,
Abc_ObjFaninC0(pObj)? "" : "-", 1+(int)Abc_ObjFanin0(pObj)->pCopy,
Abc_ObjFaninC1(pObj)? "" : "-", 1+(int)Abc_ObjFanin1(pObj)->pCopy );
// negative phase
fprintf( pFile, "-%d %s%d 0\n", 1+(int)pObj->pCopy,
Abc_ObjFaninC0(pObj)? "-" : "", 1+(int)Abc_ObjFanin0(pObj)->pCopy );
fprintf( pFile, "-%d %s%d 0\n", 1+(int)pObj->pCopy,
Abc_ObjFaninC1(pObj)? "-" : "", 1+(int)Abc_ObjFanin1(pObj)->pCopy );
}
Vec_PtrFree( vNodes );
/*
*pClas++ = pLits;
*pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
*/
// assert the first literal to zero
fprintf( pFile, "%s%d 0\n",
Abc_ObjFaninC0(ppNodes[0])? "" : "-", 1+(int)Abc_ObjFanin0(ppNodes[0])->pCopy );
// assert the second literal to one
fprintf( pFile, "%s%d 0\n",
Abc_ObjFaninC0(ppNodes[1])? "-" : "", 1+(int)Abc_ObjFanin0(ppNodes[1])->pCopy );
fclose( pFile );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

8
src/base/cmd/cmd.c
View File

@ -168,17 +168,17 @@ int CmdCommandTime( Abc_Frame_t * pAbc, int argc, char **argv )
}
pAbc->TimeTotal += pAbc->TimeCommand;
fprintf( pAbc->Out, "elapse: %3.2f seconds, total: %3.2f seconds\n",
(float)(1.0 * pAbc->TimeCommand / CLOCKS_PER_SEC), (float)(1.0 * pAbc->TimeTotal / CLOCKS_PER_SEC) );
fprintf( pAbc->Out, "elapse: %3.2f seconds, total: %3.2f seconds\n",
pAbc->TimeCommand, pAbc->TimeTotal );
/*
{
FILE * pTable;
pTable = fopen( "runtimes.txt", "a+" );
fprintf( pTable, "%4.2f\n", (float)pAbc->TimeCommand / CLOCKS_PER_SEC );
fprintf( pTable, "%4.2f\n", pAbc->TimeCommand );
fclose( pTable );
}
*/
pAbc->TimeCommand = 0;
pAbc->TimeCommand = 0.0;
return 0;
usage:

6
src/base/cmd/cmdUtils.c
View File

@ -92,7 +92,7 @@ int CmdCommandDispatch( Abc_Frame_t * pAbc, int argc, char **argv )
Abc_Command * pCommand;
char * value;
int fError;
int clk;
double clk;
if ( argc == 0 )
return 0;
@ -121,10 +121,10 @@ int CmdCommandDispatch( Abc_Frame_t * pAbc, int argc, char **argv )
}
// execute the command
clk = Extra_CpuTime();
clk = Extra_CpuTimeDouble();
pFunc = (int (*)(Abc_Frame_t *, int, char **))pCommand->pFunc;
fError = (*pFunc)( pAbc, argc, argv );
pAbc->TimeCommand += (Extra_CpuTime() - clk);
pAbc->TimeCommand += Extra_CpuTimeDouble() - clk;
// automatic execution of arbitrary command after each command
// usually this is a passive command ...

72
src/base/io/io.c
View File

@ -58,6 +58,7 @@ static int IoCommandWriteList ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWritePla ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteVerLib ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteSortCnf( Abc_Frame_t * pAbc, int argc, char **argv );
extern int glo_fMapped;
@ -111,6 +112,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "write_pla", IoCommandWritePla, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_verilog", IoCommandWriteVerilog, 0 );
// Cmd_CommandAdd( pAbc, "I/O", "write_verlib", IoCommandWriteVerLib, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_sorter_cnf", IoCommandWriteSortCnf, 0 );
}
/**Function*************************************************************
@ -2010,6 +2012,76 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandWriteSortCnf( Abc_Frame_t * pAbc, int argc, char **argv )
{
char * pFileName;
int c;
int nVars = 16;
int nQueens = 4;
extern void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NQh" ) ) != EOF )
{
switch ( c )
{
case 'N':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
nVars = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nVars <= 0 )
goto usage;
break;
case 'Q':
if ( globalUtilOptind >= argc )
{
fprintf( stdout, "Command line switch \"-Q\" should be followed by an integer.\n" );
goto usage;
}
nQueens = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nQueens <= 0 )
goto usage;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc != globalUtilOptind + 1 )
goto usage;
// get the output file name
pFileName = argv[globalUtilOptind];
Abc_NtkWriteSorterCnf( pFileName, nVars, nQueens );
// call the corresponding file writer
return 0;
usage:
fprintf( pAbc->Err, "usage: write_sorter_cnf [-N <num>] [-Q <num>] <file>\n" );
fprintf( pAbc->Err, "\t write CNF for the sorter\n" );
fprintf( pAbc->Err, "\t-N num : the number of sorter bits [default = %d]\n", nVars );
fprintf( pAbc->Err, "\t-Q num : the number of bits to be asserted to 1 [default = %d]\n", nQueens );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

4
src/base/main/mainInt.h
View File

@ -61,8 +61,8 @@ struct Abc_Frame_t_
FILE * Err;
FILE * Hst;
// used for runtime measurement
PORT_INT64_T TimeCommand; // the runtime of the last command
PORT_INT64_T TimeTotal; // the total runtime of all commands
double TimeCommand; // the runtime of the last command
double TimeTotal; // the total runtime of all commands
// temporary storage for structural choices
Vec_Ptr_t * vStore; // networks to be used by choice
// decomposition package

1
src/misc/extra/extra.h
View File

@ -607,6 +607,7 @@ extern unsigned Extra_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux
extern long Extra_CpuTime();
extern double Extra_CpuTimeDouble();
extern int Extra_GetSoftDataLimit();
extern void Extra_UtilGetoptReset();
extern int Extra_UtilGetopt( int argc, char *argv[], char *optstring );

22
src/misc/extra/extraUtilUtil.c
View File

@ -344,20 +344,36 @@ void (*Extra_UtilMMoutOfMemory)() = Extra_UtilMMout_Of_Memory;
SeeAlso []
***********************************************************************/
#if defined(NT) || defined(NT64) || defined(WIN32)
long Extra_CpuTime()
{
return clock();
}
/**Function*************************************************************
Synopsis [util_cpu_time()]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
#if defined(NT) || defined(NT64) || defined(WIN32)
double Extra_CpuTimeDouble()
{
return (double)clock()/CLOCKS_PER_SEC;
}
#else
#include <sys/time.h>
#include <sys/resource.h>
#include <unistd.h>
long Extra_CpuTime()
double Extra_CpuTimeDouble()
{
struct rusage ru;
getrusage(RUSAGE_SELF, &ru);
return (long)(CLOCKS_PER_SEC * ((double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000));
return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000;
}
#endif

888
src/sat/bsat/satInterP.c Normal file
View File

@ -0,0 +1,888 @@
/**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"
#include "vec.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// variable assignments
static const lit LIT_UNDEF = 0xffffffff;
// interpolation manager
struct Intp_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)
// proof data
Vec_Int_t * vAnties; // anticedents for all clauses
Vec_Int_t * vBreaks; // beginnings of anticedents for each clause
// 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
};
// reading/writing the proof for a clause
static inline int Intp_ManProofGet( Intp_Man_t * p, Sto_Cls_t * pCls ) { return p->pProofNums[pCls->Id]; }
static inline void Intp_ManProofSet( Intp_Man_t * p, Sto_Cls_t * pCls, int n ) { p->pProofNums[pCls->Id] = n; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocate proof manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Intp_Man_t * Intp_ManAlloc()
{
Intp_Man_t * p;
// allocate the manager
p = (Intp_Man_t *)malloc( sizeof(Intp_Man_t) );
memset( p, 0, sizeof(Intp_Man_t) );
// verification
p->nResLitsAlloc = (1<<16);
p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc );
// proof recording
p->vAnties = Vec_IntAlloc( 1000 );
p->vBreaks = Vec_IntAlloc( 1000 );
// parameters
p->fProofWrite = 0;
p->fProofVerif = 1;
return p;
}
/**Function*************************************************************
Synopsis [Resize proof manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Intp_ManResize( Intp_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 = (int *) realloc( p->pVarTypes, sizeof(int) * 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(int) * 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 );
// 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 );
}
/**Function*************************************************************
Synopsis [Deallocate proof manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Intp_ManFree( Intp_Man_t * p )
{
/*
printf( "Runtime stats:\n" );
PRT( "BCP ", p->timeBcp );
PRT( "Trace ", p->timeTrace );
PRT( "TOTAL ", p->timeTotal );
*/
Vec_IntFree( p->vAnties );
Vec_IntFree( p->vBreaks );
// 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 Intp_ManPrintClause( Intp_Man_t * p, Sto_Cls_t * pClause )
{
int i;
printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Intp_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 Intp_ManPrintResolvent( lit * pResLits, int nResLits )
{
int i;
printf( "Resolvent: {" );
for ( i = 0; i < nResLits; i++ )
printf( " %d", pResLits[i] );
printf( " }\n" );
}
/**Function*************************************************************
Synopsis [Prints the interpolant for one clause.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Intp_ManPrintInterOne( Intp_Man_t * p, Sto_Cls_t * pClause )
{
printf( "Clause %2d : ", pClause->Id );
// Extra_PrintBinary___( stdout, Intp_ManAigRead(p, pClause), (1 << p->nVarsAB) );
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Adds one clause to the watcher list.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Intp_ManWatchClause( Intp_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 Intp_ManEnqueue( Intp_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 Intp_ManCancelUntil( Intp_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 * Intp_ManPropagateOne( Intp_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])
Intp_ManWatchClause( p, pCur, pCur->pLits[1] );
break;
}
if ( i < (int)pCur->nLits ) // found new watch
continue;
// clause is unit - enqueue new implication
if ( Intp_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 * Intp_ManPropagate( Intp_Man_t * p, int Start )
{
Sto_Cls_t * pClause;
int i;
int clk = clock();
for ( i = Start; i < p->nTrailSize; i++ )
{
pClause = Intp_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 Intp_ManProofWriteOne( Intp_Man_t * p, Sto_Cls_t * pClause )
{
Intp_ManProofSet( p, pClause, ++p->Counter );
if ( p->fProofWrite )
{
int v;
fprintf( p->pFile, "%d", Intp_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 Intp_ManProofTraceOne( Intp_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 );
assert( pFinal->Id == Vec_IntSize(p->vBreaks) );
Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) );
Vec_IntPush( p->vAnties, pConflict->Id );
// if ( p->pCnf->nClausesA )
// Intp_ManAigCopy( p, Intp_ManAigRead(p, pFinal), Intp_ManAigRead(p, pConflict) );
// follow the trail backwards
PrevId = Intp_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( Intp_ManProofGet(p, pReason) > 0 );
p->Counter++;
if ( p->fProofWrite )
fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Intp_ManProofGet(p, pReason) );
PrevId = p->Counter;
// if ( p->pCnf->nClausesA )
// {
// if ( p->pVarTypes[Var] == 1 ) // var of A
// Intp_ManAigOr( p, Intp_ManAigRead(p, pFinal), Intp_ManAigRead(p, pReason) );
// else
// Intp_ManAigAnd( p, Intp_ManAigRead(p, pFinal), Intp_ManAigRead(p, pReason) );
// }
// resolve the temporary resolvent with the reason clause
if ( p->fProofVerif )
{
int v1, v2;
if ( fPrint )
Intp_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 );
Vec_IntPush( p->vAnties, pReason->Id );
}
// 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 )
Intp_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 );
Intp_ManPrintClause( p, pConflict );
Intp_ManPrintResolvent( p->pResLits, p->nResLits );
Intp_ManPrintClause( p, pFinal );
}
}
p->timeTrace += clock() - clk;
// return the proof pointer
// if ( p->pCnf->nClausesA )
// {
// Intp_ManPrintInterOne( p, pFinal );
// }
Intp_ManProofSet( p, pFinal, p->Counter );
return p->Counter;
}
/**Function*************************************************************
Synopsis [Records the proof for one clause.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Intp_ManProofRecordOne( Intp_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 ( !Intp_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
{
assert( 0 ); // impossible
return 0;
}
// propagate the assumptions
pConflict = Intp_ManPropagate( p, p->nRootSize );
if ( pConflict == NULL )
{
assert( 0 ); // cannot prove
return 0;
}
// construct the proof
Intp_ManProofTraceOne( p, pConflict, pClause );
// undo to the root level
Intp_ManCancelUntil( p, p->nRootSize );
// add large clauses to the watched lists
if ( pClause->nLits > 1 )
{
Intp_ManWatchClause( p, pClause, pClause->pLits[0] );
Intp_ManWatchClause( p, pClause, pClause->pLits[1] );
return 1;
}
assert( pClause->nLits == 1 );
// if the clause proved is unit, add it and propagate
if ( !Intp_ManEnqueue( p, pClause->pLits[0], pClause ) )
{
assert( 0 ); // impossible
return 0;
}
// propagate the assumption
pConflict = Intp_ManPropagate( p, p->nRootSize );
if ( pConflict )
{
// construct the proof
Intp_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 Intp_ManProcessRoots( Intp_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 )
{
Intp_ManWatchClause( p, pClause, pClause->pLits[0] );
Intp_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 ( !Intp_ManEnqueue( p, pClause->pLits[0], pClause ) )
{
// detected root level conflict
printf( "Error in Intp_ManProcessRoots(): Detected a root-level conflict too early!\n" );
assert( 0 );
return 0;
}
}
// propagate the root unit clauses
pClause = Intp_ManPropagate( p, 0 );
if ( pClause )
{
// detected root level conflict
Intp_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 [Recursively computes the UNSAT core.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Intp_ManUnsatCore_rec( Vec_Int_t * vAnties, Vec_Int_t * vBreaks, int iThis, Vec_Int_t * vCore, int nRoots )
{
int i, iStop, iStart;
// skip of this clause was visited
iStart = Vec_IntEntry( vBreaks, iThis );
if ( iStart == -1 )
return;
// mark this clause as visited
Vec_IntWriteEntry( vBreaks, iThis, -1 );
// add a root clause to the core
if ( iThis < nRoots )
{
Vec_IntPush( vCore, iThis );
return;
}
// iterate through the clauses
iStop = Vec_IntEntry( vBreaks, iThis+1 );
for ( i = iStart; i < iStop; i++ )
Intp_ManUnsatCore_rec( vAnties, vBreaks, Vec_IntEntry(vAnties, i), vCore, nRoots );
}
/**Function*************************************************************
Synopsis [Computes UNSAT core of the satisfiablity problem.]
Description [Takes the interpolation manager, the CNF deriving by the SAT
solver, which includes the root clauses and the learned clauses. Returns
the array of integers representing the number of root clauses that are in
the UNSAT core.]
SideEffects []
SeeAlso []
***********************************************************************/
void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose )
{
Vec_Int_t * vCore;
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;
// adjust the manager
Intp_ManResize( 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
Vec_IntClear( p->vAnties );
Vec_IntFill( p->vBreaks, p->pCnf->nRoots, 0 );
Sto_ManForEachClauseRoot( p->pCnf, pClause )
Intp_ManProofWriteOne( p, pClause );
// propagate root level assignments
if ( Intp_ManProcessRoots( p ) )
{
// if there is no conflict, consider learned clauses
Sto_ManForEachClause( p->pCnf, pClause )
{
if ( pClause->fRoot )
continue;
if ( !Intp_ManProofRecordOne( p, pClause ) )
{
RetValue = 0;
break;
}
}
}
// add the last breaker
assert( p->pCnf->pEmpty->Id == Vec_IntSize(p->vBreaks) - 1 );
Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) );
// stop the proof
if ( p->fProofWrite )
{
fclose( p->pFile );
p->pFile = NULL;
}
if ( fVerbose )
{
PRT( "Core", clock() - clkTotal );
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;
}
// derive the UNSAT core
vCore = Vec_IntAlloc( 1000 );
Intp_ManUnsatCore_rec( p->vAnties, p->vBreaks, p->pCnf->pEmpty->Id, vCore, p->pCnf->nRoots );
if ( fVerbose )
printf( "Root clauses = %d. Learned clauses = %d. UNSAT core size = %d.\n",
p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, Vec_IntSize(vCore) );
return vCore;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

6
src/sat/bsat/satStore.h
View File

@ -135,6 +135,12 @@ extern Inta_Man_t * Inta_ManAlloc();
extern void Inta_ManFree( Inta_Man_t * p );
extern void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose );
/*=== satInterP.c ==========================================================*/
typedef struct Intp_Man_t_ Intp_Man_t;
extern Intp_Man_t * Intp_ManAlloc();
extern void Intp_ManFree( Intp_Man_t * p );
extern void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose );
#ifdef __cplusplus
}
#endif