summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/aig/aigInter.c174
-rw-r--r--src/aig/aig/module.make1
-rw-r--r--src/aig/cnf/cnf.h1
-rw-r--r--src/aig/cnf/cnfMan.c22
-rw-r--r--src/base/abci/abc.c79
-rw-r--r--src/base/abci/abcDar.c48
-rw-r--r--src/map/pcm/module.make0
-rw-r--r--src/map/ply/module.make0
-rw-r--r--src/opt/res/resCore.c2
-rw-r--r--src/sat/bsat/module.make1
-rw-r--r--src/sat/bsat/satInter.c2
-rw-r--r--src/sat/bsat/satInterA.c970
-rw-r--r--src/sat/bsat/satSolver.h1
-rw-r--r--src/sat/bsat/satStore.h39
14 files changed, 1320 insertions, 20 deletions
diff --git a/src/aig/aig/aigInter.c b/src/aig/aig/aigInter.c
new file mode 100644
index 00000000..b3bc28b2
--- /dev/null
+++ b/src/aig/aig/aigInter.c
@@ -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 ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index 667ceec1..ffe6141c 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -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 \
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index 77c87f3f..5726469f 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -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 ========================================================*/
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index 4ac06b48..47bc0b67 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -139,6 +139,28 @@ void Cnf_DataFree( Cnf_Dat_t * p )
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.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
{
FILE * pFile;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1108238c..0a27ee15 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -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 );
@@ -6209,6 +6211,77 @@ usage:
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 []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandDouble( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
@@ -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 );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 439c3383..16a772ce 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -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"
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
deleted file mode 100644
index e69de29b..00000000
--- a/src/map/pcm/module.make
+++ /dev/null
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
deleted file mode 100644
index e69de29b..00000000
--- a/src/map/ply/module.make
+++ /dev/null
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index b22f0f5e..cb448fc0 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -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 );
diff --git a/src/sat/bsat/module.make b/src/sat/bsat/module.make
index 563c8dfc..1e52cc0a 100644
--- a/src/sat/bsat/module.make
+++ b/src/sat/bsat/module.make
@@ -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 \
diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c
index 8759aa09..8e07e9f6 100644
--- a/src/sat/bsat/satInter.c
+++ b/src/sat/bsat/satInter.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
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c
new file mode 100644
index 00000000..513a9044
--- /dev/null
+++ b/src/sat/bsat/satInterA.c
@@ -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 ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index ca2954d2..c1bf32a7 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -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; }
//=================================================================================================
diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h
index 346b59df..b66abc8f 100644
--- a/src/sat/bsat/satStore.h
+++ b/src/sat/bsat/satStore.h
@@ -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
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 05:17:35 +0000