Code for AIG rewriting with ABC. This code is not currently enabled by default.

I'll enable it when I understand when it's useful.

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

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index f365ded0becd29c292a64fd1d50b9e47ea13004a..3e5f2a783c781d0e986957853fe9593243311da5 100644 (file)
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -117,6 +117,8 @@ namespace BEEV
 
     bool exit_after_CNF;
 
+    bool enable_AIG_rewrites_flag;
+
     // Available back-end SAT solvers.
     enum SATSolvers
       {
@@ -230,6 +232,8 @@ namespace BEEV
 
       exit_after_CNF=false;
 
+      enable_AIG_rewrites_flag = false;
+
     } //End of constructor for UserDefinedFlags
 
   }; //End of struct UserDefinedFlags

diff --git a/src/to-sat/AIG/BBNodeAIG.h b/src/to-sat/AIG/BBNodeAIG.h
index f9fec0a01124331656b6e59918a38613db50adc5..eacd91f476ad9705d27b476339b5c1e46bb2c3ac 100644 (file)
--- a/src/to-sat/AIG/BBNodeAIG.h
+++ b/src/to-sat/AIG/BBNodeAIG.h
@@ -59,6 +59,9 @@ public:
     // If the pointer is odd. Then it's the NOT of the pointer one less.
        Aig_Obj_t * n;
 
+       // After dag aware rewriting the symbol stays at the same position in the vector of PIs.
+       // To get it's CNF variable number we get the node at the same position.
+       int symbol_index;
 
        BBNodeAIG()
        {
@@ -100,12 +103,10 @@ public:
                return n < other.n;
        }
 
-
-
        void print() const
-{
+       {
           print(n);
-}
+       }
 
 };
 }

diff --git a/src/to-sat/AIG/BBNodeManagerAIG.cpp b/src/to-sat/AIG/BBNodeManagerAIG.cpp
new file mode 100644 (file)
index 0000000..ff1bd68
--- /dev/null
+++ b/src/to-sat/AIG/BBNodeManagerAIG.cpp
@@ -0,0 +1,84 @@
+#include "BBNodeManagerAIG.h"
+
+namespace BEEV
+{
+
+  void
+  BBNodeManagerAIG::toCNF(const BBNodeAIG& top, Cnf_Dat_t*& cnfData, ToSATBase::ASTNodeToSATVar& nodeToVar, const UserDefinedFlags& uf)
+  {
+    assert(cnfData == NULL);
+
+    Aig_ObjCreatePo(aigMgr, top.n);
+    Aig_ManCleanup(aigMgr); // remove nodes not connected to the PO.
+    Aig_ManCheck(aigMgr); // check that AIG looks ok.
+
+    assert(Aig_ManPoNum(aigMgr) == 1);
+
+    // UseZeroes gives assertion errors.
+    // Rewriting is sometimes very slow. Can it be configured to be faster?
+    // What about refactoring???
+
+    if (uf.enable_AIG_rewrites_flag)
+      {
+          int nodeCount = aigMgr->nObjs[AIG_OBJ_AND];
+          if (uf.stats_flag)
+            cerr << "Nodes before AIG rewrite:" << nodeCount <<endl;
+
+          Dar_LibStart();
+          Aig_Man_t * pTemp;
+          Dar_RwrPar_t Pars, * pPars = &Pars;
+          Dar_ManDefaultRwrParams( pPars );
+          //pPars->fUpdateLevel =0;
+          //pPars->fUseZeros = 1;
+
+          for (int i=0; i < 3;i++)
+          {
+            aigMgr = Aig_ManDup( pTemp = aigMgr, 0 );
+            Aig_ManStop( pTemp );
+            Dar_ManRewrite( aigMgr, pPars );
+
+            aigMgr = Aig_ManDup( pTemp = aigMgr, 0 );
+            Aig_ManStop( pTemp );
+
+            if (uf.stats_flag)
+              cerr << "After rewrite [" << i << "]  nodes:" << aigMgr->nObjs[AIG_OBJ_AND] << endl;
+
+            if (nodeCount == aigMgr->nObjs[AIG_OBJ_AND])
+              break;
+          }
+      }
+    cnfData = Cnf_Derive(aigMgr, 0);
+
+    BBNodeManagerAIG::SymbolToBBNode::const_iterator it;
+
+    assert(nodeToVar.size() ==0);
+
+    // Each symbol maps to a vector of CNF variables.
+    for (it = symbolToBBNode.begin(); it != symbolToBBNode.end(); it++)
+      {
+        const ASTNode& n = it->first;
+        const vector<BBNodeAIG> &b = it->second;
+        assert (nodeToVar.find(n) == nodeToVar.end());
+
+        const int width = (n.GetType() == BOOLEAN_TYPE) ? 1: n.GetValueWidth();
+
+        // INT_MAX for parts of symbols that didn't get encoded.
+        vector<unsigned> v(width, ~((unsigned) 0));
+
+        for (unsigned i = 0; i < b.size(); i++)
+          {
+            if (!b[i].IsNull())
+              {
+                Aig_Obj_t * pObj;
+                pObj = (Aig_Obj_t*)Vec_PtrEntry( aigMgr->vPis, b[i].symbol_index );
+                v[i] = cnfData->pVarNums[pObj->Id];
+              }
+          }
+
+        nodeToVar.insert(make_pair(n, v));
+      }
+    assert(cnfData != NULL);
+  }
+}
+
+

diff --git a/src/to-sat/AIG/BBNodeManagerAIG.h b/src/to-sat/AIG/BBNodeManagerAIG.h
index db12056ed471fdf91d5ec604cc43c777a65385ce..451199b765c1ea86e949a264ee9f75be2b6f29fb 100644 (file)
--- a/src/to-sat/AIG/BBNodeManagerAIG.h
+++ b/src/to-sat/AIG/BBNodeManagerAIG.h
@@ -107,75 +107,7 @@ public:
                 return BBNodeAIG(Aig_ManConst0(aigMgr));
         }
 
-        void toCNF_experimental(BBNodeAIG& top, Cnf_Dat_t*& cnfData, ToSATBase::ASTNodeToSATVar& nodeToVar)
-        {
-          //cerr << "SAFDASDF";
-
-          // copied from darScript.c: Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig )
-          /*
-           Dar_LibStart();
-           Aig_Man_t * pTemp1, *pTemp2;
-           Dar_RwrPar_t Pars, * pPars = &Pars;
-           Dar_ManDefaultRwrParams( pPars );
-           Dar_ManRewrite( aigMgr, pPars );
-           Aig_ManCheck(aigMgr); // check that AIG looks ok.
-           Dar_LibStop();
-           */
-
-          //assert(Aig_ManPoNum(aigMgr) == 1);
-
-          //Aig_NtkReassignIds( aigMgr );
-          // fix the levels
-          //Aig_ManUpdateLevel( aigMgr, Aig_ManPo(aigMgr,0));
-          //Aig_ManVerifyLevel( aigMgr );
-
-
-          // assert(Aig_ManPoNum(aigMgr) == 1);
-
-          //Dar_RwrPar_t  pPars;
-          //Dar_ManDefaultRwrParams( &pPars );
-          //Dar_ManRewrite( aigMgr, &pPars );
-        }
-
-        void
-        toCNF(BBNodeAIG& top, Cnf_Dat_t*& cnfData, ToSATBase::ASTNodeToSATVar& nodeToVar)
-        {
-          assert(cnfData == NULL);
-
-          Aig_ObjCreatePo(aigMgr, top.n);
-          Aig_ManCleanup( aigMgr); // remove nodes not connected to the PO.
-          Aig_ManCheck(aigMgr); // check that AIG looks ok.
-
-          assert(Aig_ManPoNum(aigMgr) == 1);
-
-          // Cnf_Derive gives errors sometimes.
-          //cnfData = Cnf_DeriveSimple(aigMgr, 0);
-          cnfData = Cnf_Derive(aigMgr, 0);
-
-          BBNodeManagerAIG::SymbolToBBNode::const_iterator it;
-
-          assert(nodeToVar.size() ==0);
-
-          // Each symbol maps to a vector of CNF variables.
-          for (it = symbolToBBNode.begin(); it != symbolToBBNode.end(); it++)
-            {
-              const ASTNode& n = it->first;
-              const vector<BBNodeAIG> &b = it->second;
-              assert (nodeToVar.find(n) == nodeToVar.end());
-
-              const int width = (n.GetType() == BOOLEAN_TYPE) ? 1: n.GetValueWidth();
-              vector<unsigned> v(width, ~((unsigned) 0));
-
-              for (unsigned i = 0; i < b.size(); i++)
-                {
-                  if (!b[i].IsNull())
-                    v[i] = cnfData->pVarNums[b[i].n->Id];
-                }
-
-              nodeToVar.insert(make_pair(n, v));
-            }
-          assert(cnfData != NULL);
-        }
+        void toCNF(const BBNodeAIG& top, Cnf_Dat_t*& cnfData, ToSATBase::ASTNodeToSATVar& nodeToVar, const UserDefinedFlags& uf);
 
         // The same symbol always needs to return the same AIG node,
         // if it doesn't you will get the wrong answer.
@@ -201,7 +133,7 @@ public:
                         return it->second[i];
 
                 it->second[i] = BBNodeAIG(Aig_ObjCreatePi(aigMgr));
-
+                it->second[i].symbol_index = aigMgr->vPis->nSize-1;
                 return it->second[i];
         }
 

diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp
index d79fe27e04fbe4ac04b60f17157de1bd60d50341..6ea8b0b8b0c2b5e596ba2119a77cb3124937ea9d 100644 (file)
--- a/src/to-sat/AIG/ToSATAIG.cpp
+++ b/src/to-sat/AIG/ToSATAIG.cpp
@@ -24,7 +24,7 @@ namespace BEEV
       Cnf_Dat_t* cnfData = NULL;
 
       bm->GetRunTimes()->start(RunTimes::CNFConversion);
-      mgr.toCNF(BBFormula, cnfData, nodeToSATVar);
+      mgr.toCNF(BBFormula, cnfData, nodeToSATVar,bm->UserFlags);
       bm->GetRunTimes()->stop(RunTimes::CNFConversion);
 
       // Free the memory in the AIGs.