mirror of https://github.com/YosysHQ/abc.git
Version abc80116
This commit is contained in:
Alan Mishchenko
parent
4a61139de0
commit
61850d5942
8
abc.dsp
8
abc.dsp
|
|
@ -1170,6 +1170,10 @@ SOURCE=.\src\sat\bsat\satInter.c
|
|||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\bsat\satInterA.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\bsat\satMem.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
|
@ -2870,6 +2874,10 @@ SOURCE=.\src\aig\aig\aigHaig.c
|
|||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\aig\aigInter.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\aig\aigMan.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
|
|
|||
|
|
@ -0,0 +1,174 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [aigInter.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [AIG package.]
|
||||
|
||||
Synopsis [Interpolate two AIGs.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - April 28, 2007.]
|
||||
|
||||
Revision [$Id: aigInter.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "aig.h"
|
||||
#include "cnf.h"
|
||||
#include "satStore.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose )
|
||||
{
|
||||
void * pSatCnf = NULL;
|
||||
Inta_Man_t * pManInter;
|
||||
Aig_Man_t * pRes;
|
||||
sat_solver * pSat;
|
||||
Cnf_Dat_t * pCnfOn, * pCnfOff;
|
||||
Vec_Int_t * vVarsAB;
|
||||
Aig_Obj_t * pObj, * pObj2;
|
||||
int Lits[3], status, i;
|
||||
int clk = clock();
|
||||
|
||||
assert( Aig_ManPiNum(pManOn) == Aig_ManPiNum(pManOff) );
|
||||
|
||||
// derive CNFs
|
||||
pCnfOn = Cnf_Derive( pManOn, 0 );
|
||||
pCnfOff = Cnf_Derive( pManOff, 0 );
|
||||
// pCnfOn = Cnf_DeriveSimple( pManOn, 0 );
|
||||
// pCnfOff = Cnf_DeriveSimple( pManOff, 0 );
|
||||
Cnf_DataLift( pCnfOff, pCnfOn->nVars );
|
||||
|
||||
// start the solver
|
||||
pSat = sat_solver_new();
|
||||
sat_solver_store_alloc( pSat );
|
||||
sat_solver_setnvars( pSat, pCnfOn->nVars + pCnfOff->nVars );
|
||||
|
||||
// add clauses of A
|
||||
for ( i = 0; i < pCnfOn->nClauses; i++ )
|
||||
{
|
||||
if ( !sat_solver_addclause( pSat, pCnfOn->pClauses[i], pCnfOn->pClauses[i+1] ) )
|
||||
{
|
||||
Cnf_DataFree( pCnfOn );
|
||||
Cnf_DataFree( pCnfOff );
|
||||
sat_solver_delete( pSat );
|
||||
return NULL;
|
||||
}
|
||||
}
|
||||
sat_solver_store_mark_clauses_a( pSat );
|
||||
|
||||
// add clauses of B
|
||||
for ( i = 0; i < pCnfOff->nClauses; i++ )
|
||||
{
|
||||
if ( !sat_solver_addclause( pSat, pCnfOff->pClauses[i], pCnfOff->pClauses[i+1] ) )
|
||||
{
|
||||
Cnf_DataFree( pCnfOn );
|
||||
Cnf_DataFree( pCnfOff );
|
||||
sat_solver_delete( pSat );
|
||||
return NULL;
|
||||
}
|
||||
}
|
||||
|
||||
// add PI clauses
|
||||
// collect the common variables
|
||||
vVarsAB = Vec_IntAlloc( Aig_ManPiNum(pManOn) );
|
||||
Aig_ManForEachPi( pManOn, pObj, i )
|
||||
{
|
||||
Vec_IntPush( vVarsAB, pCnfOn->pVarNums[pObj->Id] );
|
||||
pObj2 = Aig_ManPi( pManOff, i );
|
||||
|
||||
Lits[0] = toLitCond( pCnfOn->pVarNums[pObj->Id], 0 );
|
||||
Lits[1] = toLitCond( pCnfOff->pVarNums[pObj2->Id], 1 );
|
||||
if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
|
||||
assert( 0 );
|
||||
Lits[0] = toLitCond( pCnfOn->pVarNums[pObj->Id], 1 );
|
||||
Lits[1] = toLitCond( pCnfOff->pVarNums[pObj2->Id], 0 );
|
||||
if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
|
||||
assert( 0 );
|
||||
}
|
||||
Cnf_DataFree( pCnfOn );
|
||||
Cnf_DataFree( pCnfOff );
|
||||
sat_solver_store_mark_roots( pSat );
|
||||
if ( fVerbose )
|
||||
{
|
||||
PRT( "Prepare", clock() - clk );
|
||||
}
|
||||
|
||||
/*
|
||||
status = sat_solver_simplify(pSat);
|
||||
if ( status == 0 )
|
||||
{
|
||||
Vec_IntFree( vVarsAB );
|
||||
Cnf_DataFree( pCnfOn );
|
||||
Cnf_DataFree( pCnfOff );
|
||||
sat_solver_delete( pSat );
|
||||
return NULL;
|
||||
}
|
||||
*/
|
||||
|
||||
// solve the problem
|
||||
clk = clock();
|
||||
status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
|
||||
if ( fVerbose )
|
||||
{
|
||||
PRT( "Solving", clock() - clk );
|
||||
}
|
||||
if ( status == l_False )
|
||||
{
|
||||
pSatCnf = sat_solver_store_release( pSat );
|
||||
// printf( "unsat\n" );
|
||||
}
|
||||
else if ( status == l_True )
|
||||
{
|
||||
// printf( "sat\n" );
|
||||
}
|
||||
else
|
||||
{
|
||||
// printf( "undef\n" );
|
||||
}
|
||||
sat_solver_delete( pSat );
|
||||
if ( pSatCnf == NULL )
|
||||
{
|
||||
printf( "The SAT problem is not unsat.\n" );
|
||||
Vec_IntFree( vVarsAB );
|
||||
return NULL;
|
||||
}
|
||||
|
||||
// create the resulting manager
|
||||
pManInter = Inta_ManAlloc();
|
||||
pRes = Inta_ManInterpolate( pManInter, pSatCnf, vVarsAB, fVerbose );
|
||||
Inta_ManFree( pManInter );
|
||||
|
||||
Vec_IntFree( vVarsAB );
|
||||
Sto_ManFree( pSatCnf );
|
||||
return pRes;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -3,6 +3,7 @@ SRC += src/aig/aig/aigCheck.c \
|
|||
src/aig/aig/aigFanout.c \
|
||||
src/aig/aig/aigFrames.c \
|
||||
src/aig/aig/aigHaig.c \
|
||||
src/aig/aig/aigInter.c \
|
||||
src/aig/aig/aigMan.c \
|
||||
src/aig/aig/aigMem.c \
|
||||
src/aig/aig/aigMffc.c \
|
||||
|
|
|
|||
|
|
@ -133,6 +133,7 @@ extern Cnf_Man_t * Cnf_ManStart();
|
|||
extern void Cnf_ManStop( Cnf_Man_t * p );
|
||||
extern Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
|
||||
extern void Cnf_DataFree( Cnf_Dat_t * p );
|
||||
extern void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus );
|
||||
extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );
|
||||
void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );
|
||||
/*=== cnfMap.c ========================================================*/
|
||||
|
|
|
|||
|
|
@ -128,6 +128,28 @@ void Cnf_DataFree( Cnf_Dat_t * p )
|
|||
free( p );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Writes CNF into a file.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
int v;
|
||||
Aig_ManForEachObj( p->pMan, pObj, v )
|
||||
if ( p->pVarNums[pObj->Id] )
|
||||
p->pVarNums[pObj->Id] += nVarsPlus;
|
||||
for ( v = 0; v < p->nLiterals; v++ )
|
||||
p->pClauses[0][v] += 2*nVarsPlus;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Writes CNF into a file.]
|
||||
|
|
|
|||
|
|
@ -104,6 +104,7 @@ static int Abc_CommandEspresso ( Abc_Frame_t * pAbc, int argc, char ** arg
|
|||
static int Abc_CommandGen ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
//static int Abc_CommandXyz ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandDouble ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandInter ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
|
||||
static int Abc_CommandQuaVar ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
|
|
@ -281,6 +282,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
|
|||
Cmd_CommandAdd( pAbc, "Various", "gen", Abc_CommandGen, 0 );
|
||||
// Cmd_CommandAdd( pAbc, "Various", "xyz", Abc_CommandXyz, 1 );
|
||||
Cmd_CommandAdd( pAbc, "Various", "double", Abc_CommandDouble, 1 );
|
||||
Cmd_CommandAdd( pAbc, "Various", "inter", Abc_CommandInter, 1 );
|
||||
Cmd_CommandAdd( pAbc, "Various", "test", Abc_CommandTest, 0 );
|
||||
|
||||
Cmd_CommandAdd( pAbc, "Various", "qvar", Abc_CommandQuaVar, 1 );
|
||||
|
|
@ -6198,6 +6200,77 @@ usage:
|
|||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Abc_CommandInter( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
FILE * pOut, * pErr;
|
||||
Abc_Ntk_t * pNtk, * pNtkRes, * pNtk1, * pNtk2;
|
||||
char ** pArgvNew;
|
||||
int nArgcNew;
|
||||
int c, fDelete1, fDelete2;
|
||||
int fVerbose;
|
||||
extern Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose );
|
||||
|
||||
pNtk = Abc_FrameReadNtk(pAbc);
|
||||
pOut = Abc_FrameReadOut(pAbc);
|
||||
pErr = Abc_FrameReadErr(pAbc);
|
||||
|
||||
// set defaults
|
||||
fVerbose = 0;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'v':
|
||||
fVerbose ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
|
||||
pArgvNew = argv + globalUtilOptind;
|
||||
nArgcNew = argc - globalUtilOptind;
|
||||
if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
|
||||
return 1;
|
||||
if ( nArgcNew == 0 )
|
||||
{
|
||||
printf( "Deriving new circuit structure for the current network.\n" );
|
||||
Abc_ObjXorFaninC( Abc_NtkPo(pNtk2,0), 0 );
|
||||
}
|
||||
pNtkRes = Abc_NtkInter( pNtk1, pNtk2, fVerbose );
|
||||
if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
|
||||
if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
|
||||
|
||||
if ( pNtkRes == NULL )
|
||||
{
|
||||
fprintf( pErr, "Command has failed.\n" );
|
||||
return 0;
|
||||
}
|
||||
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
fprintf( pErr, "usage: inter [-vh] <fileOnSet> <fileOffSet>\n" );
|
||||
fprintf( pErr, "\t derives interpolant of two networks (onset and offset)\n" );
|
||||
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
|
||||
fprintf( pErr, "\t-h : print the command usage\n");
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
|
@ -6311,7 +6384,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
|
||||
extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
|
||||
// extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
|
||||
extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
|
||||
// extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
|
||||
extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
|
||||
extern void Abc_NtkDarTestBlif( char * pFileName );
|
||||
|
||||
|
|
@ -6464,7 +6537,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
return 0;
|
||||
}
|
||||
*/
|
||||
|
||||
/*
|
||||
if ( Abc_NtkIsStrash(pNtk) )
|
||||
{
|
||||
fprintf( stdout, "Currently only works for logic circuits.\n" );
|
||||
|
|
@ -6482,7 +6555,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
}
|
||||
// replace the current network
|
||||
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
|
||||
|
||||
*/
|
||||
|
||||
// Abc_NtkDarHaigRecord( pNtk );
|
||||
// Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose );
|
||||
|
|
|
|||
|
|
@ -1482,6 +1482,54 @@ Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
|
|||
return pNtkAig;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Interplates two networks.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
|
||||
{
|
||||
extern Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose );
|
||||
Abc_Ntk_t * pNtkAig;
|
||||
Aig_Man_t * pManOn, * pManOff, * pManAig;
|
||||
if ( Abc_NtkCoNum(pNtkOn) != 1 || Abc_NtkCoNum(pNtkOff) != 1 )
|
||||
{
|
||||
printf( "Currently works only for single output networks.\n" );
|
||||
return NULL;
|
||||
}
|
||||
if ( Abc_NtkCiNum(pNtkOn) != Abc_NtkCiNum(pNtkOff) )
|
||||
{
|
||||
printf( "The number of PIs should be the same.\n" );
|
||||
return NULL;
|
||||
}
|
||||
// create internal AIGs
|
||||
pManOn = Abc_NtkToDar( pNtkOn, 0 );
|
||||
if ( pManOn == NULL )
|
||||
return NULL;
|
||||
pManOff = Abc_NtkToDar( pNtkOff, 0 );
|
||||
if ( pManOff == NULL )
|
||||
return NULL;
|
||||
// derive the interpolant
|
||||
pManAig = Aig_ManInter( pManOn, pManOff, fVerbose );
|
||||
if ( pManAig == NULL )
|
||||
{
|
||||
printf( "Interpolant computation failed.\n" );
|
||||
return NULL;
|
||||
}
|
||||
Aig_ManStop( pManOn );
|
||||
Aig_ManStop( pManOff );
|
||||
// create logic network
|
||||
pNtkAig = Abc_NtkFromDar( pNtkOn, pManAig );
|
||||
Aig_ManStop( pManAig );
|
||||
return pNtkAig;
|
||||
}
|
||||
|
||||
|
||||
#include "ntl.h"
|
||||
|
||||
|
|
|
|||
|
|
@ -100,7 +100,7 @@ Res_Man_t * Res_ManAlloc( Res_Par_t * pPars )
|
|||
p->pPars = pPars;
|
||||
p->pWin = Res_WinAlloc();
|
||||
p->pSim = Res_SimAlloc( pPars->nSimWords );
|
||||
p->pMan = Int_ManAlloc( 512 );
|
||||
p->pMan = Int_ManAlloc();
|
||||
p->vMem = Vec_IntAlloc( 0 );
|
||||
p->vResubs = Vec_VecStart( pPars->nCands );
|
||||
p->vResubsW = Vec_VecStart( pPars->nCands );
|
||||
|
|
|
|||
|
|
@ -1,5 +1,6 @@
|
|||
SRC += src/sat/bsat/satMem.c \
|
||||
src/sat/bsat/satInter.c \
|
||||
src/sat/bsat/satInterA.c \
|
||||
src/sat/bsat/satSolver.c \
|
||||
src/sat/bsat/satStore.c \
|
||||
src/sat/bsat/satTrace.c \
|
||||
|
|
|
|||
|
|
@ -99,7 +99,7 @@ static inline void Int_ManProofSet( Int_Man_t * p, Sto_Cls_t * pCls, int n
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Int_Man_t * Int_ManAlloc( int nVarsAlloc )
|
||||
Int_Man_t * Int_ManAlloc()
|
||||
{
|
||||
Int_Man_t * p;
|
||||
// allocate the manager
|
||||
|
|
|
|||
|
|
@ -0,0 +1,970 @@
|
|||
/**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 "aig.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
// variable assignments
|
||||
static const lit LIT_UNDEF = 0xffffffff;
|
||||
|
||||
// interpolation manager
|
||||
struct Inta_Man_t_
|
||||
{
|
||||
// clauses of the problems
|
||||
Sto_Man_t * pCnf; // the set of CNF clauses for A and B
|
||||
Vec_Int_t * vVarsAB; // the array of global variables
|
||||
// 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)
|
||||
// interpolation data
|
||||
Aig_Man_t * pAig; // the AIG manager for recording the interpolant
|
||||
int * pVarTypes; // variable type (size nVars) [1=A, 0=B, <0=AB]
|
||||
Aig_Obj_t ** pInters; // storage for interpolants as truth tables (size nClauses)
|
||||
int nIntersAlloc; // the allocated size of truth table array
|
||||
// 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
|
||||
};
|
||||
|
||||
// procedure to get hold of the clauses' truth table
|
||||
static inline Aig_Obj_t ** Inta_ManAigRead( Inta_Man_t * pMan, Sto_Cls_t * pCls ) { return pMan->pInters + pCls->Id; }
|
||||
static inline void Inta_ManAigClear( Inta_Man_t * pMan, Aig_Obj_t ** p ) { *p = Aig_ManConst0(pMan->pAig); }
|
||||
static inline void Inta_ManAigFill( Inta_Man_t * pMan, Aig_Obj_t ** p ) { *p = Aig_ManConst1(pMan->pAig); }
|
||||
static inline void Inta_ManAigCopy( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = *q; }
|
||||
static inline void Inta_ManAigAnd( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_And(pMan->pAig, *p, *q); }
|
||||
static inline void Inta_ManAigOr( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_Or(pMan->pAig, *p, *q); }
|
||||
static inline void Inta_ManAigOrNot( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_Or(pMan->pAig, *p, Aig_Not(*q)); }
|
||||
static inline void Inta_ManAigOrVar( Inta_Man_t * pMan, Aig_Obj_t ** p, int v ) { *p = Aig_Or(pMan->pAig, *p, Aig_IthVar(pMan->pAig, v)); }
|
||||
static inline void Inta_ManAigOrNotVar( Inta_Man_t * pMan, Aig_Obj_t ** p, int v ) { *p = Aig_Or(pMan->pAig, *p, Aig_Not(Aig_IthVar(pMan->pAig, v))); }
|
||||
|
||||
// reading/writing the proof for a clause
|
||||
static inline int Inta_ManProofGet( Inta_Man_t * p, Sto_Cls_t * pCls ) { return p->pProofNums[pCls->Id]; }
|
||||
static inline void Inta_ManProofSet( Inta_Man_t * p, Sto_Cls_t * pCls, int n ) { p->pProofNums[pCls->Id] = n; }
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Allocate proof manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Inta_Man_t * Inta_ManAlloc()
|
||||
{
|
||||
Inta_Man_t * p;
|
||||
// allocate the manager
|
||||
p = (Inta_Man_t *)malloc( sizeof(Inta_Man_t) );
|
||||
memset( p, 0, sizeof(Inta_Man_t) );
|
||||
// verification
|
||||
p->nResLitsAlloc = (1<<16);
|
||||
p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc );
|
||||
// parameters
|
||||
p->fProofWrite = 0;
|
||||
p->fProofVerif = 1;
|
||||
return p;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Count common variables in the clauses of A and B.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Inta_ManGlobalVars( Inta_Man_t * p )
|
||||
{
|
||||
Sto_Cls_t * pClause;
|
||||
int LargeNum = -100000000;
|
||||
int Var, nVarsAB, v;
|
||||
|
||||
// mark the variable encountered in the clauses of A
|
||||
Sto_ManForEachClauseRoot( p->pCnf, pClause )
|
||||
{
|
||||
if ( !pClause->fA )
|
||||
break;
|
||||
for ( v = 0; v < (int)pClause->nLits; v++ )
|
||||
p->pVarTypes[lit_var(pClause->pLits[v])] = 1;
|
||||
}
|
||||
|
||||
// check variables that appear in clauses of B
|
||||
nVarsAB = 0;
|
||||
Sto_ManForEachClauseRoot( p->pCnf, pClause )
|
||||
{
|
||||
if ( pClause->fA )
|
||||
continue;
|
||||
for ( v = 0; v < (int)pClause->nLits; v++ )
|
||||
{
|
||||
Var = lit_var(pClause->pLits[v]);
|
||||
if ( p->pVarTypes[Var] == 1 ) // var of A
|
||||
{
|
||||
// change it into a global variable
|
||||
nVarsAB++;
|
||||
p->pVarTypes[Var] = LargeNum;
|
||||
}
|
||||
}
|
||||
}
|
||||
assert( nVarsAB <= Vec_IntSize(p->vVarsAB) );
|
||||
|
||||
// order global variables
|
||||
nVarsAB = 0;
|
||||
Vec_IntForEachEntry( p->vVarsAB, Var, v )
|
||||
p->pVarTypes[Var] = -(1+nVarsAB++);
|
||||
|
||||
// check that there is no extra global variables
|
||||
for ( v = 0; v < p->pCnf->nVars; v++ )
|
||||
assert( p->pVarTypes[v] != LargeNum );
|
||||
return nVarsAB;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Resize proof manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Inta_ManResize( Inta_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 );
|
||||
|
||||
// compute the number of common variables
|
||||
Inta_ManGlobalVars( p );
|
||||
|
||||
// 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 );
|
||||
|
||||
// check if resizing of truth tables is needed
|
||||
if ( p->nIntersAlloc < p->pCnf->nClauses )
|
||||
{
|
||||
p->nIntersAlloc = p->pCnf->nClauses;
|
||||
p->pInters = (Aig_Obj_t **) realloc( p->pInters, sizeof(Aig_Obj_t *) * p->nIntersAlloc );
|
||||
}
|
||||
memset( p->pInters, 0, sizeof(Aig_Obj_t *) * p->pCnf->nClauses );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Deallocate proof manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Inta_ManFree( Inta_Man_t * p )
|
||||
{
|
||||
/*
|
||||
printf( "Runtime stats:\n" );
|
||||
PRT( "BCP ", p->timeBcp );
|
||||
PRT( "Trace ", p->timeTrace );
|
||||
PRT( "TOTAL ", p->timeTotal );
|
||||
*/
|
||||
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 Inta_ManPrintClause( Inta_Man_t * p, Sto_Cls_t * pClause )
|
||||
{
|
||||
int i;
|
||||
printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Inta_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 Inta_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 Inta_ManPrintInterOne( Inta_Man_t * p, Sto_Cls_t * pClause )
|
||||
{
|
||||
printf( "Clause %2d : ", pClause->Id );
|
||||
// Extra_PrintBinary___( stdout, Inta_ManAigRead(p, pClause), (1 << p->nVarsAB) );
|
||||
printf( "\n" );
|
||||
}
|
||||
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Adds one clause to the watcher list.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline void Inta_ManWatchClause( Inta_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 Inta_ManEnqueue( Inta_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 Inta_ManCancelUntil( Inta_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 * Inta_ManPropagateOne( Inta_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])
|
||||
Inta_ManWatchClause( p, pCur, pCur->pLits[1] );
|
||||
break;
|
||||
}
|
||||
if ( i < (int)pCur->nLits ) // found new watch
|
||||
continue;
|
||||
|
||||
// clause is unit - enqueue new implication
|
||||
if ( Inta_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 * Inta_ManPropagate( Inta_Man_t * p, int Start )
|
||||
{
|
||||
Sto_Cls_t * pClause;
|
||||
int i;
|
||||
int clk = clock();
|
||||
for ( i = Start; i < p->nTrailSize; i++ )
|
||||
{
|
||||
pClause = Inta_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 Inta_ManProofWriteOne( Inta_Man_t * p, Sto_Cls_t * pClause )
|
||||
{
|
||||
Inta_ManProofSet( p, pClause, ++p->Counter );
|
||||
|
||||
if ( p->fProofWrite )
|
||||
{
|
||||
int v;
|
||||
fprintf( p->pFile, "%d", Inta_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 Inta_ManProofTraceOne( Inta_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 );
|
||||
|
||||
if ( p->pCnf->nClausesA )
|
||||
Inta_ManAigCopy( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pConflict) );
|
||||
|
||||
// follow the trail backwards
|
||||
PrevId = Inta_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( Inta_ManProofGet(p, pReason) > 0 );
|
||||
p->Counter++;
|
||||
if ( p->fProofWrite )
|
||||
fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Inta_ManProofGet(p, pReason) );
|
||||
PrevId = p->Counter;
|
||||
|
||||
if ( p->pCnf->nClausesA )
|
||||
{
|
||||
if ( p->pVarTypes[Var] == 1 ) // var of A
|
||||
Inta_ManAigOr( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pReason) );
|
||||
else
|
||||
Inta_ManAigAnd( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pReason) );
|
||||
}
|
||||
|
||||
// resolve the temporary resolvent with the reason clause
|
||||
if ( p->fProofVerif )
|
||||
{
|
||||
int v1, v2;
|
||||
if ( fPrint )
|
||||
Inta_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 );
|
||||
}
|
||||
|
||||
// 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 )
|
||||
Inta_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 );
|
||||
Inta_ManPrintClause( p, pConflict );
|
||||
Inta_ManPrintResolvent( p->pResLits, p->nResLits );
|
||||
Inta_ManPrintClause( p, pFinal );
|
||||
}
|
||||
}
|
||||
p->timeTrace += clock() - clk;
|
||||
|
||||
// return the proof pointer
|
||||
if ( p->pCnf->nClausesA )
|
||||
{
|
||||
// Inta_ManPrintInterOne( p, pFinal );
|
||||
}
|
||||
Inta_ManProofSet( p, pFinal, p->Counter );
|
||||
return p->Counter;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Records the proof for one clause.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Inta_ManProofRecordOne( Inta_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 ( !Inta_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
|
||||
{
|
||||
assert( 0 ); // impossible
|
||||
return 0;
|
||||
}
|
||||
|
||||
// propagate the assumptions
|
||||
pConflict = Inta_ManPropagate( p, p->nRootSize );
|
||||
if ( pConflict == NULL )
|
||||
{
|
||||
assert( 0 ); // cannot prove
|
||||
return 0;
|
||||
}
|
||||
|
||||
// construct the proof
|
||||
Inta_ManProofTraceOne( p, pConflict, pClause );
|
||||
|
||||
// undo to the root level
|
||||
Inta_ManCancelUntil( p, p->nRootSize );
|
||||
|
||||
// add large clauses to the watched lists
|
||||
if ( pClause->nLits > 1 )
|
||||
{
|
||||
Inta_ManWatchClause( p, pClause, pClause->pLits[0] );
|
||||
Inta_ManWatchClause( p, pClause, pClause->pLits[1] );
|
||||
return 1;
|
||||
}
|
||||
assert( pClause->nLits == 1 );
|
||||
|
||||
// if the clause proved is unit, add it and propagate
|
||||
if ( !Inta_ManEnqueue( p, pClause->pLits[0], pClause ) )
|
||||
{
|
||||
assert( 0 ); // impossible
|
||||
return 0;
|
||||
}
|
||||
|
||||
// propagate the assumption
|
||||
pConflict = Inta_ManPropagate( p, p->nRootSize );
|
||||
if ( pConflict )
|
||||
{
|
||||
// construct the proof
|
||||
Inta_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 Inta_ManProcessRoots( Inta_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 )
|
||||
{
|
||||
Inta_ManWatchClause( p, pClause, pClause->pLits[0] );
|
||||
Inta_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 ( !Inta_ManEnqueue( p, pClause->pLits[0], pClause ) )
|
||||
{
|
||||
// detected root level conflict
|
||||
printf( "Error in Inta_ManProcessRoots(): Detected a root-level conflict too early!\n" );
|
||||
assert( 0 );
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
// propagate the root unit clauses
|
||||
pClause = Inta_ManPropagate( p, 0 );
|
||||
if ( pClause )
|
||||
{
|
||||
// detected root level conflict
|
||||
Inta_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 [Records the proof.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Inta_ManPrepareInter( Inta_Man_t * p )
|
||||
{
|
||||
Sto_Cls_t * pClause;
|
||||
int Var, VarAB, v;
|
||||
|
||||
// set interpolants for root clauses
|
||||
Sto_ManForEachClauseRoot( p->pCnf, pClause )
|
||||
{
|
||||
if ( !pClause->fA ) // clause of B
|
||||
{
|
||||
Inta_ManAigFill( p, Inta_ManAigRead(p, pClause) );
|
||||
// Inta_ManPrintInterOne( p, pClause );
|
||||
continue;
|
||||
}
|
||||
// clause of A
|
||||
Inta_ManAigClear( p, Inta_ManAigRead(p, pClause) );
|
||||
for ( v = 0; v < (int)pClause->nLits; v++ )
|
||||
{
|
||||
Var = lit_var(pClause->pLits[v]);
|
||||
if ( p->pVarTypes[Var] < 0 ) // global var
|
||||
{
|
||||
VarAB = -p->pVarTypes[Var]-1;
|
||||
assert( VarAB >= 0 && VarAB < Vec_IntSize(p->vVarsAB) );
|
||||
if ( lit_sign(pClause->pLits[v]) ) // negative var
|
||||
Inta_ManAigOrNotVar( p, Inta_ManAigRead(p, pClause), VarAB );
|
||||
else
|
||||
Inta_ManAigOrVar( p, Inta_ManAigRead(p, pClause), VarAB );
|
||||
}
|
||||
}
|
||||
// Inta_ManPrintInterOne( p, pClause );
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Computes interpolant for the given CNF.]
|
||||
|
||||
Description [Takes the interpolation manager, the CNF deriving by the SAT
|
||||
solver, which includes ClausesA, ClausesB, and learned clauses. Additional
|
||||
arguments are the vector of variables common to AB and the verbosiness flag.
|
||||
Returns the AIG manager with a single output, containing the interpolant.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose )
|
||||
{
|
||||
Aig_Man_t * pRes;
|
||||
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;
|
||||
p->vVarsAB = vVarsAB;
|
||||
p->pAig = pRes = Aig_ManStart( 10000 );
|
||||
Aig_IthVar( p->pAig, Vec_IntSize(p->vVarsAB) - 1 );
|
||||
|
||||
// adjust the manager
|
||||
Inta_ManResize( p );
|
||||
|
||||
// prepare the interpolant computation
|
||||
Inta_ManPrepareInter( 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
|
||||
Sto_ManForEachClauseRoot( p->pCnf, pClause )
|
||||
Inta_ManProofWriteOne( p, pClause );
|
||||
|
||||
// propagate root level assignments
|
||||
if ( Inta_ManProcessRoots( p ) )
|
||||
{
|
||||
// if there is no conflict, consider learned clauses
|
||||
Sto_ManForEachClause( p->pCnf, pClause )
|
||||
{
|
||||
if ( pClause->fRoot )
|
||||
continue;
|
||||
if ( !Inta_ManProofRecordOne( p, pClause ) )
|
||||
{
|
||||
RetValue = 0;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// stop the proof
|
||||
if ( p->fProofWrite )
|
||||
{
|
||||
fclose( p->pFile );
|
||||
p->pFile = NULL;
|
||||
}
|
||||
|
||||
if ( fVerbose )
|
||||
{
|
||||
PRT( "Interpo", 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;
|
||||
}
|
||||
|
||||
Aig_ObjCreatePo( pRes, *Inta_ManAigRead( p, p->pCnf->pTail ) );
|
||||
Aig_ManCleanup( pRes );
|
||||
|
||||
p->pAig = NULL;
|
||||
return pRes;
|
||||
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -71,6 +71,7 @@ static inline int lit_var (lit l) { return l >> 1; }
|
|||
static inline int lit_sign (lit l) { return l & 1; }
|
||||
static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
|
||||
static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
|
||||
static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; }
|
||||
|
||||
|
||||
//=================================================================================================
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [pr.h]
|
||||
FileName [satStore.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
|
|
@ -18,11 +18,13 @@
|
|||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef __PR_H__
|
||||
#define __PR_H__
|
||||
#ifndef __SAT_STORE_H__
|
||||
#define __SAT_STORE_H__
|
||||
|
||||
#include "satSolver.h"
|
||||
|
||||
/*
|
||||
The trace of SAT solving contains the original clause of the problem
|
||||
The trace of SAT solving contains the original clauses of the problem
|
||||
along with the learned clauses derived during SAT solving.
|
||||
The first line of the resulting file contains 3 numbers instead of 2:
|
||||
c <num_vars> <num_all_clauses> <num_root_clauses>
|
||||
|
|
@ -54,7 +56,18 @@ extern "C" {
|
|||
/// BASIC TYPES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/*
|
||||
typedef unsigned lit;
|
||||
// variable/literal conversions (taken from MiniSat)
|
||||
static inline lit toLit (int v) { return v + v; }
|
||||
static inline lit toLitCond(int v, int c) { return v + v + (c != 0); }
|
||||
static inline lit lit_neg (lit l) { return l ^ 1; }
|
||||
static inline int lit_var (lit l) { return l >> 1; }
|
||||
static inline int lit_sign (lit l) { return l & 1; }
|
||||
static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
|
||||
static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
|
||||
static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; }
|
||||
*/
|
||||
|
||||
typedef struct Sto_Cls_t_ Sto_Cls_t;
|
||||
struct Sto_Cls_t_
|
||||
|
|
@ -87,16 +100,6 @@ struct Sto_Man_t_
|
|||
char * pChunkLast; // the last memory chunk
|
||||
};
|
||||
|
||||
// variable/literal conversions (taken from MiniSat)
|
||||
static inline lit toLit (int v) { return v + v; }
|
||||
static inline lit toLitCond(int v, int c) { return v + v + (c != 0); }
|
||||
static inline lit lit_neg (lit l) { return l ^ 1; }
|
||||
static inline int lit_var (lit l) { return l >> 1; }
|
||||
static inline int lit_sign (lit l) { return l & 1; }
|
||||
static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
|
||||
static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
|
||||
static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; }
|
||||
|
||||
// iterators through the clauses
|
||||
#define Sto_ManForEachClause( p, pCls ) for( pCls = p->pHead; pCls; pCls = pCls->pNext )
|
||||
#define Sto_ManForEachClauseRoot( p, pCls ) for( pCls = p->pHead; pCls && pCls->fRoot; pCls = pCls->pNext )
|
||||
|
|
@ -121,10 +124,16 @@ extern Sto_Man_t * Sto_ManLoadClauses( char * pFileName );
|
|||
|
||||
/*=== satInter.c ==========================================================*/
|
||||
typedef struct Int_Man_t_ Int_Man_t;
|
||||
extern Int_Man_t * Int_ManAlloc( int nVarsAlloc );
|
||||
extern Int_Man_t * Int_ManAlloc();
|
||||
extern void Int_ManFree( Int_Man_t * p );
|
||||
extern int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult );
|
||||
|
||||
/*=== satInterA.c ==========================================================*/
|
||||
typedef struct Inta_Man_t_ Inta_Man_t;
|
||||
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 );
|
||||
|
||||
#ifdef __cplusplus
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
Loading…
Reference in New Issue