Allow incremental building of the CNF from AIGs using Tseitin.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1056 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/extlib-abc/aig/cnf/cnfWrite.c b/src/extlib-abc/aig/cnf/cnfWrite.c
index b04efcb025f47b5c6e3b1daee13797cee847d96f..7aa8f11fd1c78044952ef3be269eff4d92f1533a 100644 (file)
--- a/src/extlib-abc/aig/cnf/cnfWrite.c
+++ b/src/extlib-abc/aig/cnf/cnfWrite.c
@@ -318,6 +318,97 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
     return pCnf;\r
 }\r
 \r
+// Create a new partial CNF with just the extra bits versus the old CNF.\r
+// This uses the Tseitin transform of Cnf_DeriveSimple\r
+// NB. We assume there will only be one more PO than last time.\r
+Cnf_Dat_t * Cnf_DeriveSimple_Additional( Aig_Man_t * p, Cnf_Dat_t * old )\r
+{\r
+    Aig_Obj_t * pObj;\r
+    Cnf_Dat_t * pCnf;\r
+    int OutVar, PoVar, pVars[32], * pLits, ** pClas;\r
+    int i, nLiterals, nClauses;\r
+\r
+    // calculate the worst case number of literals and clauses\r
+    nLiterals = 1 + 7 * Aig_ManNodeNum(p) + Aig_ManPoNum( p );\r
+    nClauses = 1 + 3 * Aig_ManNodeNum(p) + Aig_ManPoNum( p );\r
+\r
+    // allocate CNF\r
+    pCnf = ALLOC( Cnf_Dat_t, 1 );\r
+    memset( pCnf, 0, sizeof(Cnf_Dat_t) );\r
+    pCnf->pClauses = ALLOC( int *, nClauses + 1 );\r
+    pCnf->pClauses[0] = ALLOC( int, nLiterals );\r
+\r
+    // create room for variable numbers\r
+    pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(p) );\r
+    memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) );\r
+\r
+    // This is the index of the highest CNF variable number.\r
+    //printf("Old number of vars: %d\n", old->nVars);\r
+\r
+    //Copy over the prior allocation of variables to the new variables\r
+    memcpy(pCnf->pVarNums, old->pVarNums, sizeof(int) * old->nVars);\r
+\r
+    assert (pCnf->pVarNums[Aig_ManConst1(p)->Id] ==1);\r
+    int Number = old->nVars+1;\r
+\r
+    // assign variables to the PIs\r
+    int newPI = 0;\r
+    Aig_ManForEachPi( p, pObj, i )\r
+       if (pCnf->pVarNums[pObj->Id] == -1) // new!\r
+               pCnf->pVarNums[pObj->Id] = Number++;\r
+\r
+    //printf("new PI Nodes: %d\n", Number - (old->nVars+1));\r
+\r
+    // assign the clauses\r
+    pLits = pCnf->pClauses[0];\r
+    pClas = pCnf->pClauses;\r
+    Aig_ManForEachNode( p, pObj, i )\r
+    {\r
+        OutVar = pCnf->pVarNums[ pObj->Id ];\r
+\r
+        if (pCnf->pVarNums[pObj->Id] == -1)\r
+        {\r
+               OutVar = Number++;\r
+               pCnf->pVarNums[pObj->Id] = OutVar;\r
+        }\r
+        else\r
+               {\r
+               // This skips over variables that have already been generated.\r
+                       continue;\r
+               }\r
+\r
+        pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];\r
+        pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];\r
+\r
+        // positive phase\r
+        *pClas++ = pLits;\r
+        *pLits++ = 2 * OutVar;\r
+        *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj);\r
+        *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj);\r
+        // negative phase\r
+        *pClas++ = pLits;\r
+        *pLits++ = 2 * OutVar + 1;\r
+        *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj);\r
+        *pClas++ = pLits;\r
+        *pLits++ = 2 * OutVar + 1;\r
+        *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj);\r
+    }\r
+\r
+    pCnf->nVars = Number;\r
+    //printf("New number of vars: %d\n",  pCnf->nVars);\r
+\r
+    // WE ASSUME THERE WILL ONLY BE ONE NEW PO.\r
+    pObj = Vec_PtrEntry(p->vPos, Vec_PtrSize(p->vPos)-1);\r
+    OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];\r
+    *pClas++ = pLits;\r
+    *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);\r
+\r
+    pCnf->nClauses = pClas - pCnf->pClauses;\r
+    pCnf->pClauses[pCnf->nClauses] = pLits;\r
+    pCnf->nLiterals = -1; // not maintained.\r
+\r
+    return pCnf;\r
+}\r
 \r
 /**Function*************************************************************\r
 \r

diff --git a/src/extlib-abc/cnf_short.h b/src/extlib-abc/cnf_short.h
index df815d9fc3ef48375601314b9b105d73e515cab1..e8a158742feffc15c405f4e7e2184314ee4df6e2 100644 (file)
--- a/src/extlib-abc/cnf_short.h
+++ b/src/extlib-abc/cnf_short.h
@@ -149,6 +149,8 @@ extern Vec_Ptr_t *     Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPre
 extern void            Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover );\r
 extern Cnf_Dat_t *     Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs );\r
 extern Cnf_Dat_t *     Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs );\r
+// NB: This is an STP function...\r
+extern Cnf_Dat_t * Cnf_DeriveSimple_Additional( Aig_Man_t * p, Cnf_Dat_t * old );\r
 \r
 #ifdef __cplusplus\r
 }\r