pass projection vars to approxmc

meelgroup · Nov 15, 2024 · 608a2d2 · 608a2d2
1 parent 27ca48d
commit 608a2d2
Show file tree

Hide file tree

Showing 16 changed files with 46 additions and 15 deletions.
diff --git a/include/stp/Sat/ApxMC.h b/include/stp/Sat/ApxMC.h
@@ -74,7 +74,7 @@ class ApxMC : public SATSolver
 
   virtual uint32_t newVar();
 
-  virtual uint32_t newProjVar();
+  virtual uint32_t newProjVar(uint32_t x);
 
   void setVerbosity(int v);
 

diff --git a/include/stp/Sat/CMSGen.h b/include/stp/Sat/CMSGen.h
@@ -67,7 +67,7 @@ namespace stp
 
   virtual uint8_t modelValue(uint32_t x) const;
 
-  virtual uint32_t newProjVar();
+  virtual uint32_t newProjVar(uint32_t x);
 
   virtual uint32_t newVar();
 

diff --git a/include/stp/Sat/CryptoMinisat5.h b/include/stp/Sat/CryptoMinisat5.h
@@ -64,7 +64,7 @@ namespace stp
 
   virtual uint8_t modelValue(uint32_t x) const;
 
-  virtual uint32_t newProjVar();
+  virtual uint32_t newProjVar(uint32_t x);
 
   virtual uint32_t newVar();
 

diff --git a/include/stp/Sat/MinisatCore.h b/include/stp/Sat/MinisatCore.h
@@ -70,7 +70,7 @@ namespace stp
   uint8_t value(uint32_t x) const;
 
   virtual uint32_t newVar();
-  virtual uint32_t newProjVar();
+  virtual uint32_t newProjVar(uint32_t x);
 
   void setVerbosity(int v);
 

diff --git a/include/stp/Sat/SATSolver.h b/include/stp/Sat/SATSolver.h
@@ -82,7 +82,7 @@ class SATSolver
 
   virtual uint32_t newVar() = 0;
 
-  virtual uint32_t newProjVar() = 0;
+  virtual uint32_t newProjVar(uint32_t x) = 0;
 
   virtual unsigned long nVars() const = 0;
 

diff --git a/include/stp/Sat/SimplifyingMinisat.h b/include/stp/Sat/SimplifyingMinisat.h
@@ -57,7 +57,7 @@ class SimplifyingMinisat : public SATSolver
   virtual uint8_t modelValue(uint32_t x) const;
 
   virtual uint32_t newVar();
-  virtual uint32_t newProjVar();
+  virtual uint32_t newProjVar(uint32_t x);
 
   unsigned long nVars() const;
 

diff --git a/include/stp/Sat/UniSamp.h b/include/stp/Sat/UniSamp.h
@@ -77,7 +77,7 @@ class UniSamp : public SATSolver
 
   virtual uint8_t modelValue(uint32_t x) const;
 
-  virtual uint32_t newProjVar();
+  virtual uint32_t newProjVar(uint32_t x);
 
   virtual uint32_t newVar();
 

diff --git a/lib/Sat/ApxMC.cpp b/lib/Sat/ApxMC.cpp
@@ -109,7 +109,8 @@ bool ApxMC::solve(bool& timeout_expired) // Search without assumptions.
 
   // CMSat::lbool ret = s->solve(); // TODO AS
   std::cout << "c [stp->appmc] ApxMC solving instance with " << arjun->nVars()
-            << " variables" << std::endl;
+            << " variables, " << sampling_vars_orig.size() << " projection vars"
+            << std::endl;
 
   vector<uint32_t> sampling_vars;
   for (uint32_t i = 0; i < arjun->nVars(); i++)
@@ -131,7 +132,16 @@ bool ApxMC::solve(bool& timeout_expired) // Search without assumptions.
   sc.iter2 = 0;
 
   if (sampling_vars_orig.size() == 0)
+  {
     sampling_vars_orig = sampling_vars;
+    std::cout << "c [stp->appmc] Setting all variables as projection vars "
+              << std::endl;
+  }
+  else
+  {
+    std::cout << "c [stp->appmc] Using " << sampling_vars_orig.size()
+              << " projection vars " << std::endl;
+  }
 
   arjun->set_sampl_vars(sampling_vars_orig);
   sampling_vars = arjun->run_backwards();
@@ -180,14 +190,19 @@ uint8_t ApxMC::modelValue(uint32_t x) const
   return true;
 }
 
-uint32_t ApxMC::newProjVar()
+uint32_t ApxMC::newProjVar(uint32_t x)
 {
+  sampling_vars_orig.push_back(x + 1);
+  std::cout << "c [stp->appmc] ApxMC adding new proj variable " << x
+            << std::endl;
   return 42;
 }
 
 uint32_t ApxMC::newVar()
 {
   arjun->new_var();
+  std::cout << "c [stp->appmc] ApxMC adding new variable " << arjun->nVars() - 1
+            << std::endl;
   return arjun->nVars() - 1;
 }
 

diff --git a/lib/Sat/CMSGen.cpp b/lib/Sat/CMSGen.cpp
@@ -117,7 +117,7 @@ uint8_t CMSGenC::modelValue(uint32_t x) const
   return (s->get_model().at(x) == CMSGen::l_True);
 }
 
-uint32_t CMSGenC::newProjVar()
+uint32_t CMSGenC::newProjVar(uint32_t x)
 {
   return 42;
 }

diff --git a/lib/Sat/MinisatCore.cpp b/lib/Sat/MinisatCore.cpp
@@ -101,7 +101,7 @@ uint8_t MinisatCore::modelValue(uint32_t x) const
   return Minisat::toInt(s->modelValue(x));
 }
 
-uint32_t MinisatCore::newProjVar()
+uint32_t MinisatCore::newProjVar(uint32_t x)
 {
   return 42;
 }
@@ -135,4 +135,4 @@ bool MinisatCore::simplify()
 {
   return s->simplify();
 }
-}
+} // namespace stp
diff --git a/lib/Sat/SimplifyingMinisat.cpp b/lib/Sat/SimplifyingMinisat.cpp
@@ -99,7 +99,7 @@ uint32_t SimplifyingMinisat::newVar()
   return s->newVar();
 }
 
-uint32_t SimplifyingMinisat::newProjVar()
+uint32_t SimplifyingMinisat::newProjVar(uint32_t x)
 {
   return 42;
 }

diff --git a/lib/Sat/UniSamp.cpp b/lib/Sat/UniSamp.cpp
@@ -215,7 +215,7 @@ uint8_t UniSamp::modelValue(uint32_t x) const
   return (unigen_models.at(samples_generated).at(x) > 0);
 }
 
-uint32_t UniSamp::newProjVar()
+uint32_t UniSamp::newProjVar(uint32_t x)
 {
   return 42;
 }

diff --git a/lib/ToSat/ToCNFAIG.cpp b/lib/ToSat/ToCNFAIG.cpp
@@ -167,10 +167,16 @@ void ToCNFAIG::fill_node_to_var(Cnf_Dat_t* cnfData,
         Aig_Obj_t* pObj;
         pObj = (Aig_Obj_t*)Vec_PtrEntry(mgr.aigMgr->vPis, b[i].symbol_index);
         v[i] = cnfData->pVarNums[pObj->Id];
+        if (uf.counting_mode || uf.sampling_mode)
+        {
+          cnfData->lProjVars[v[i]] = 1;
+        }
+
+        std::cout << "n: " << n << " v: " << v[i] << std::endl;
       }
     }
 
     nodeToVars.insert(make_pair(n, v));
   }
 }
-}
+} // namespace stp
diff --git a/lib/ToSat/ToSATAIG.cpp b/lib/ToSat/ToSATAIG.cpp
@@ -147,7 +147,14 @@ void ToSATAIG::add_cnf_to_solver(SATSolver& satSolver, Cnf_Dat_t* cnfData)
   // Create a new sat variable for each of the variables in the CNF.
   int satV = satSolver.nVars();
   for (int i = 0; i < cnfData->nVars - satV; i++)
+  {
     satSolver.newVar();
+    if (cnfData->lProjVars[i] == 1)
+    {
+      std::cout << "proj var: " << i << std::endl;
+      satSolver.newProjVar(i); // TODO AS check for off by one
+    }
+  }
 
   SATSolver::vec_literals satSolverClause;
   for (int i = 0; i < cnfData->nClauses; i++)

diff --git a/lib/extlib-abc/aig/cnf/cnfWrite.c b/lib/extlib-abc/aig/cnf/cnfWrite.c
@@ -230,6 +230,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
     pCnf->pClauses = ALLOC( int *, nClauses + 1 );
     pCnf->pClauses[0] = ALLOC( int, nLiterals );
     pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
+    pCnf->lProjVars = ALLOC(  int, nLiterals );
 
     // create room for variable numbers
     pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(p->pManAig) );

diff --git a/lib/extlib-abc/cnf.h b/lib/extlib-abc/cnf.h
@@ -78,6 +78,8 @@ struct Cnf_Dat_t_
     int             nClauses;        // the number of CNF clauses
     int **          pClauses;        // the CNF clauses
     int *           pVarNums;        // the number of CNF variable for each node ID (-1 if unused)
+    int *           lProjVars;       // projection variables
+
 };
 
 // the cut used to represent node in the AIG