projection variables are supported for counting

meelgroup · Nov 24, 2024 · 9e3a210 · 9e3a210
1 parent 4202ac9
commit 9e3a210
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 7 deletions.
diff --git a/include/stp/ToSat/ToCNFAIG.h b/include/stp/ToSat/ToCNFAIG.h
@@ -38,6 +38,7 @@ class ASTtoCNF;
 class ToCNFAIG // not copyable
 {
   UserDefinedFlags& uf;
+  STPMgr* bm;
 
   void dag_aware_aig_rewrite(const bool needAbsRef, BBNodeManagerAIG& mgr);
 
@@ -46,7 +47,7 @@ class ToCNFAIG // not copyable
                         BBNodeManagerAIG& mgr);
 
 public:
-  ToCNFAIG(UserDefinedFlags& _uf) : uf(_uf) {}
+  ToCNFAIG(STPMgr* _bm, UserDefinedFlags& _uf) : uf(_uf), bm(_bm) {}
 
   void toCNF(const BBNodeAIG& top, Cnf_Dat_t*& cnfData,
              ToSATBase::ASTNodeToSATVar& nodeToVars, bool needAbsRef,

diff --git a/include/stp/ToSat/ToSATAIG.h b/include/stp/ToSat/ToSATAIG.h
@@ -81,7 +81,7 @@ class DLL_PUBLIC ToSATAIG : public ToSATBase
   bool cbIsDestructed() { return cb == NULL; }
 
   ToSATAIG(STPMgr* bm, ArrayTransformer* at)
-      : ToSATBase(bm), toCNF(bm->UserFlags)
+      : ToSATBase(bm), toCNF(bm, bm->UserFlags)
   {
     cb = NULL;
     init();
@@ -90,7 +90,7 @@ class DLL_PUBLIC ToSATAIG : public ToSATBase
 
   ToSATAIG(STPMgr* bm, simplifier::constantBitP::ConstantBitPropagation* cb_,
            ArrayTransformer* at)
-      : ToSATBase(bm), cb(cb_), toCNF(bm->UserFlags)
+      : ToSATBase(bm), cb(cb_), toCNF(bm, bm->UserFlags)
   {
     cb = cb_;
     init();

diff --git a/lib/ToSat/ToCNFAIG.cpp b/lib/ToSat/ToCNFAIG.cpp
@@ -35,7 +35,7 @@ void addVariables(BBNodeManagerAIG& mgr, Cnf_Dat_t*& cnfData,
   // Each symbol maps to a vector of CNF variables.
   for (it = mgr.symbolToBBNode.begin(); it != mgr.symbolToBBNode.end(); it++)
   {
-    const ASTNode& n = it->first;
+    ASTNode& n = const_cast<ASTNode&>(it->first);
     const vector<BBNodeAIG>& b = it->second;
 
     const int width = (n.GetType() == BOOLEAN_TYPE) ? 1 : n.GetValueWidth();
@@ -151,10 +151,13 @@ void ToCNFAIG::fill_node_to_var(Cnf_Dat_t* cnfData,
   // Each symbol maps to a vector of CNF variables.
   for (it = mgr.symbolToBBNode.begin(); it != mgr.symbolToBBNode.end(); it++)
   {
-    const ASTNode& n = it->first;
+    ASTNode& n = const_cast<ASTNode&>(it->first);
     const vector<BBNodeAIG>& b = it->second;
     assert(nodeToVars.find(n) == nodeToVars.end());
-
+    if (bm->isProjSymbol(n))
+      std::cout << "proj symbol" << n.GetName() << std::endl;
+    else
+      std::cout << "not proj symbol" << n.GetName() << std::endl;
     const int width = (n.GetType() == BOOLEAN_TYPE) ? 1 : n.GetValueWidth();
 
     // INT_MAX for parts of symbols that didn't get encoded.
@@ -170,7 +173,8 @@ void ToCNFAIG::fill_node_to_var(Cnf_Dat_t* cnfData,
         if (uf.counting_mode || uf.sampling_mode)
         {
           // TODO AS keep check for projection variables here
-          cnfData->lProjVars[v[i]] = 1;
+          if(bm->isProjSymbol(n))
+            cnfData->lProjVars[v[i]] = 1;
         }
       }
     }