From 608a2d2a4c5307efce898f0f904d491de4c278b1 Mon Sep 17 00:00:00 2001 From: Arijit Shaw Date: Fri, 15 Nov 2024 16:16:57 -0500 Subject: [PATCH] pass projection vars to approxmc --- include/stp/Sat/ApxMC.h | 2 +- include/stp/Sat/CMSGen.h | 2 +- include/stp/Sat/CryptoMinisat5.h | 2 +- include/stp/Sat/MinisatCore.h | 2 +- include/stp/Sat/SATSolver.h | 2 +- include/stp/Sat/SimplifyingMinisat.h | 2 +- include/stp/Sat/UniSamp.h | 2 +- lib/Sat/ApxMC.cpp | 19 +++++++++++++++++-- lib/Sat/CMSGen.cpp | 2 +- lib/Sat/MinisatCore.cpp | 4 ++-- lib/Sat/SimplifyingMinisat.cpp | 2 +- lib/Sat/UniSamp.cpp | 2 +- lib/ToSat/ToCNFAIG.cpp | 8 +++++++- lib/ToSat/ToSATAIG.cpp | 7 +++++++ lib/extlib-abc/aig/cnf/cnfWrite.c | 1 + lib/extlib-abc/cnf.h | 2 ++ 16 files changed, 46 insertions(+), 15 deletions(-) diff --git a/include/stp/Sat/ApxMC.h b/include/stp/Sat/ApxMC.h index 612376b7..ee9a57ff 100644 --- 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 index 4eb99781..6c29f9ef 100644 --- 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 index e7388f56..8d894b61 100644 --- 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 index 2590688f..437fc202 100644 --- 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 index e4f32594..94292603 100644 --- 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 index af5e3063..1c6c01a9 100644 --- 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 index 8ba7fdcc..660daee6 100644 --- 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 index 9f4d6827..0dc06cb9 100644 --- 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 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 index fa8acae3..5e41628f 100644 --- 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 index 68650e45..339bf9f1 100644 --- 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 index 2e726658..7cbd4013 100644 --- 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 index 487aa9b7..6fed1252 100644 --- 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 index 14b06151..c5bffa64 100644 --- 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 index 5e00e961..7aa09d70 100644 --- 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 index 2e485059..32763234 100644 --- 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 index 3305f5ea..c46a7f83 100644 --- 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